docs: refresh composition + taxonomy + CLAUDE.md for landed rungs

Documentation sweep aligning prose with the code as of c5fb8a5.
All claims verified against current source — no overclaim.

composition.md:
  * §3 Pentagon: marked Landed (was Partial). Now records
    Echo-comp-pent-Σ-assoc-{to, from, from-to, to-from} as the
    full Σ-shape iso companion to the projection-level lemmas
    (-pent-B, -pent-echo).
  * §3 Tolerance: marked Landed (was Open). Realised as
    EchoApprox.Approx.echo-approx-compose over a parametric
    pseudo-metric.
  * §3 Decoration commuting: linear case marked Landed via
    EchoLinear.degradeMode-comp + degradeMode-id-{linear, affine}
    + degradeMode-strict-is-weaken. Indexed/role/modal still open.
  * §"Ranked open list": (3) pentagon coherence struck through
    (now landed at full Σ-shape, not just projections).

taxonomy.md:
  * §8 axis-8 (computational access): EchoDecidable.agda named
    as the first formalised artifact; refinement 3 anchored to
    the new module; clarified that refinements 1/2/4 (cost-tracking,
    graded modality, abstract machine) remain unformalised because
    Agda's type system does not express complexity bounds without
    further machinery.

CLAUDE.md:
  * "Current rung state" updated to record EchoLinear's per-decoration
    composition rung alongside EchoGraded; remaining open
    decorations (indexed / role / modal) reduced from 4 to 3.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

CLAUDE.md

@@ -140,8 +140,13 @@ work to `main` and refresh all documentation:
 
 ## Current rung state (2026-04-27)
 
-Just landed: **Per-decoration composition rung** in `EchoGraded.agda`.
-The grade decoration commutes with composition. Headlines:
+Just landed: **Per-decoration composition rung** across
+`EchoGraded.agda` and `EchoLinear.agda`. Both decorations commute
+with composition under the same recipe (decoration order →
+propositionality → join → factoring-free compose → via-join
+restatement). Headlines:
+
+`EchoGraded.agda`:
 
 * `≤g-prop` — the order `_≤g_` is propositional (each (g1, g2) pair
   has at most one inhabitant). Six refl-clauses, one per constructor.
@@ -155,15 +160,29 @@ The grade decoration commutes with composition. Headlines:
   structure: `degrade p1 e ≡ degrade (≤g-⊔g-univ p1 p2) (degrade
   (≤g-⊔g-left g1 g2) e)`.
 
-All five new headlines pinned in `Smoke.agda`. Verified post-rung:
-`agda proofs/agda/All.agda` and `agda proofs/agda/Smoke.agda` both
-exit 0 under `--safe --without-K`. No postulates introduced.
+`EchoLinear.agda` (linearity-side analogue, two-mode `linear ⊑
+affine` decoration):
+
+* `_≤m_`, `≤m-trans` — mode order with three constructors
+  (`linear≤linear`, `linear≤affine`, `affine≤affine`) and
+  transitivity.
+* `degradeMode`, `degradeMode-comp` — id on reflexive cases,
+  `weaken` on the strict step; composition closes `refl` on every
+  reachable constructor pair.
+* `≤m-prop`, `_⊔m_`, `≤m-⊔m-{left, right, univ}` — propositional
+  order plus join structure (with `affine` as top).
+* `degradeMode-compose`, `degradeMode-via-join` — mirror the
+  `EchoGraded` factoring-free compose and via-join restatement.
+
+All headlines pinned in `Smoke.agda`. `EchoLinear.agda` typechecks
+clean with no warnings or errors under `--safe --without-K`. No
+postulates introduced.
 
 Open at this rung:
 
-* Linear / indexed / role / modal cases of decoration-commuting
-  (`EchoLinear`, `EchoIndexed`, `EchoChoreo`, `EchoEpistemic`).
-  The grade case suggests the recipe in each: identify the
+* Indexed / role / modal cases of decoration-commuting
+  (`EchoIndexed`, `EchoChoreo`, `EchoEpistemic`). The grade and
+  linear cases suggest the recipe in each: identify the
   decoration's underlying order, prove it propositional, prove the
   existing `*-comp` lemma against it.
 

docs/echo-types/composition.md

@@ -223,13 +223,20 @@ Collecting the above:
    `s-right`). Round-trips deferred pending a triangle-identity
    coherence or a stdlib `Function.Bundles.Inverse` shim.
 
-4. **(Partial) Pentagon.** Three-fold composition associates at
-   the projections. `Echo-comp-iso-pent-B` and
-   `Echo-comp-iso-pent-echo` both `refl`; full Σ-shape iso still
-   open.
-
-5. **(Open) Tolerance calculus.** For approximate echoes, tolerances
-   compose with a Lipschitz-like law.
+4. **(Landed) Pentagon.** Three-fold composition associates at
+   the projections (`Echo-comp-iso-pent-B`, `Echo-comp-iso-pent-echo`,
+   both `refl`) and at the full Σ shape
+   (`Echo-comp-pent-Σ-assoc-{to, from, from-to, to-from}`). The two
+   nested-Σ shapes differ only by Σ-associativity / unification of
+   the intermediate base point; both round-trips reduce
+   definitionally once `g b ≡ c` is pinned, so this is a strict iso
+   inside `--safe --without-K`. All four iso components pinned in
+   `Smoke.agda`.
+
+5. **(Landed) Tolerance calculus.** For approximate echoes,
+   tolerances compose additively under a non-expansive outer leg.
+   Realised as `EchoApprox.Approx.echo-approx-compose` over a
+   parametric pseudo-metric.
 
 6. **(Partial) Decoration commuting.** Role, grade, linearity, and
    modal decorations commute with composition under conditions to be
@@ -239,8 +246,12 @@ Collecting the above:
    corollary of `degrade-comp` and `≤g-prop` (the order is
    propositional). `degrade-via-join` restates this through the
    join structure `_⊔g_`, with `≤g-⊔g-left/right/univ` exhibiting
-   `_⊔g_` as the categorical join. Linear / indexed / role / modal
-   cases remain open.
+   `_⊔g_` as the categorical join. The linear case is **landed** in
+   `EchoLinear.agda` as `degradeMode-comp` along the mode order
+   `linear ⊑ linear ⊑ affine ⊑ affine`; corollaries
+   `degradeMode-id-{linear, affine}` and
+   `degradeMode-strict-is-weaken` establish the relationship to the
+   existing `weaken`. Indexed / role / modal cases remain open.
 
 ---
 
@@ -253,24 +264,25 @@ Ranked by unblock-value. (1) and (2) landed; (3) onwards is open.
 2. ~~**Cancellation corollary.**~~ Partially landed as
    `cancel-iso-to` / `cancel-iso-from`; full iso deferred pending
    triangle-identity coherence (see §3 above).
-3. ~~**Pentagon coherence.**~~ Partially landed: the two
-   projection-level pentagon lemmas (`-pent-B`, `-pent-echo`)
-   ship as `refl`. The full Σ-associativity iso between the two
-   nested shapes remains open.
+3. ~~**Pentagon coherence.**~~ Landed: projection-level
+   (`-pent-B`, `-pent-echo` as `refl`) plus the full Σ-shape iso
+   (`Echo-comp-pent-Σ-assoc-{to, from, from-to, to-from}`).
 4. **Full cancel-iso with round-trips.** Needs an equivalence
    record that packages `s-left`, `s-right`, and the triangle
    identity as three fields, or direct use of stdlib's
    `Function.Bundles.Inverse`. Then the round-trip refls go through.
-5. **Approximate-echo skeleton.** New module
-   `EchoApprox.agda` defining ε-echoes and restating (1) in the
-   approximate setting. This is where axis 2 of the taxonomy gets
-   teeth.
+5. ~~**Approximate-echo skeleton.**~~ Landed in
+   `EchoApprox.agda` with `EchoR ε f y`, `echo-approx-intro`,
+   `echo-approx-relax`, and `echo-approx-compose` (additive under
+   non-expansive outer leg).
 6. **Decoration commuting.** Per-decoration lemmas in the existing
    `EchoGraded`, `EchoLinear`, `EchoIndexed` modules. *Grade case
    landed*: `EchoGraded.degrade-compose` (per-decoration composition
    law) and `degrade-via-join` (its join-structured restatement),
-   resting on `≤g-prop` and `degrade-comp`. Linear / indexed /
-   role / modal still open.
+   resting on `≤g-prop` and `degrade-comp`. *Linear case landed*:
+   `EchoLinear.degradeMode-comp` along the mode order with
+   `degradeMode-id-{linear, affine}` corollaries. Indexed / role /
+   modal still open.
 
 None of these depend on the blocked Buchholz-WF / shared-binder
 work. All are Sonnet-class proofs; (5) is Opus 4.7 design and

docs/echo-types/taxonomy.md

@@ -210,10 +210,12 @@ intensional core, same proof relevance, etc.) and differ only in
 whether a witness is reachable by a feasible algorithm. The security
 of every modern cryptosystem depends on this axis being real.
 
-*Agda anchor.* None directly — Agda's type system does not express
-complexity bounds, so computational access cannot be named at the
-type level in the current formalisation. Adjacent machinery in
-stdlib:
+*Agda anchor.* `EchoDecidable.agda` formalises refinement 3 below
+(decidability-respecting echo) as the first axis-8 artifact under
+`--safe --without-K`. Full cost-tracking refinements (1, 2, 4) are
+not yet formalised — Agda's type system does not express complexity
+bounds, so asymptotic computational access cannot be named at the
+type level without further machinery. Adjacent stdlib pieces:
 - `Data.Nat.Logarithm.⌊log₂⌋` and arithmetic complexity conventions
   admit informal-level statements like "this function runs in `O(n
   log n)`", but without a cost monad.
@@ -233,10 +235,25 @@ stdlib:
    host; the grade would need a complexity-class interpretation
    (e.g. polynomial vs super-polynomial).
 
-3. **Decidability-respecting echo.** `Echo⁺ f y = Dec (Echo f y)`
+3. **Decidability-respecting echo.** `EchoDec f y = Dec (Echo f y)`
    pairs the echo with a *constructive decision procedure*. Weaker
    than full cost-tracking but enough to distinguish "feasibly
-   decidable" from "mathematically inhabited".
+   decidable" from "mathematically inhabited". **Formalised** in
+   `proofs/agda/EchoDecidable.agda` as the first axis-8 artifact.
+
+*Refinement choice (chosen first formalisation target).*
+Refinement 3 is the right starting point under `--safe --without-K`.
+It is the only one of the four candidates that lives entirely inside
+the existing type theory: no resource monad, no graded semiring with
+a complexity-class interpretation, no abstract machine. `Dec` is
+already in the standard library, and the gap between `Echo f y`
+(inhabited) and `Dec (Echo f y)` (constructively decided) is
+exactly the gap axis 8 names. Formalising 3 first lets the heavier
+refinements (1, 2, 4) be added later as orthogonal layers, each
+projecting to the decidability-respecting echo by forgetting cost
+information. Realised in `EchoDecidable.agda` with headline lemmas
+`echo-dec-intro`, `echo-dec-pull-yes`, `echo-dec-respect-≡`,
+`echo-dec-fin`, `echo-dec-compose-with-search`.
 
 4. **Witness-search abstract machine.** Model the extractor as a
    term in a bounded-step abstract machine and pair it with the
@@ -245,7 +262,9 @@ stdlib:
 *Open question.* Is there a single refinement that subsumes all four?
 My guess is no: (1) and (4) track asymptotic cost, (2) and (3)
 track discrete feasibility classes. They probably live on a small
-lattice of access-tracking theories.
+lattice of access-tracking theories. Concretely, refinement 3 (now
+formalised) gives the bottom of the lattice: every other refinement
+projects down to it by erasing cost data.
 
 *Composition conjecture.* Computational accessibility composes
 **multiplicatively** along `g ∘ f` in the canonical case — the