agda(EchoGraded): per-decoration composition rung

Grade decoration commutes with composition. Headlines:

* ≤g-prop — the order _≤g_ is propositional (each (g1, g2) pair has
  at most one inhabitant). Six refl-clauses, one per constructor.
  Pattern-matches go through under --without-K because each pair has
  exactly one inhabitant.
* ≤g-⊔g-left, ≤g-⊔g-right, ≤g-⊔g-univ — exhibit _⊔g_ as the
  categorical join in _≤g_ (two upper bounds + universal property).
* degrade-compose — per-decoration composition law: for any
  factoring g1 ≤g g2 ≤g g3 and any direct p13 : g1 ≤g g3,
  degrade p23 (degrade p12 e) ≡ degrade p13 e. Corollary of
  degrade-comp + ≤g-prop.
* degrade-via-join — same statement restated through the join:
  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: agda proofs/agda/All.agda and agda proofs/agda/Smoke.agda
both exit 0 under --safe --without-K. No postulates introduced.

Docs updated: composition.md §6 (decoration commuting now Partial,
grade case Landed), roadmap.md (corresponding entry promoted from
unblocked to partial), CLAUDE.md (current rung state).

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

Author: hyperpolymath

CLAUDE.md

@@ -138,7 +138,38 @@ work to `main` and refresh all documentation:
    name, the commits folded in, the remaining open pieces of the
    milestone, and the proposed smallest useful next advance.
 
-## Current rung state (2026-04-23)
+## Current rung state (2026-04-27)
+
+Just landed: **Per-decoration composition rung** in `EchoGraded.agda`.
+The grade decoration commutes with composition. Headlines:
+
+* `≤g-prop` — the order `_≤g_` is propositional (each (g1, g2) pair
+  has at most one inhabitant). Six refl-clauses, one per constructor.
+* `≤g-⊔g-left`, `≤g-⊔g-right`, `≤g-⊔g-univ` — exhibit `_⊔g_` as the
+  categorical join in `_≤g_` (two upper bounds + universal property).
+* `degrade-compose` — per-decoration composition law: for any
+  factoring `g1 ≤g g2 ≤g g3` and any direct `p13 : g1 ≤g g3`,
+  `degrade p23 (degrade p12 e) ≡ degrade p13 e`. Corollary of
+  `degrade-comp` + `≤g-prop`.
+* `degrade-via-join` — same statement restated through the join
+  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.
+
+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
+  decoration's underlying order, prove it propositional, prove the
+  existing `*-comp` lemma against it.
+
+---
+
+## Previous rung state (2026-04-23)
 
 Just consolidated: **Budgeted recursive-surface rung** (on top of
 the earlier **Pentagon rung**). Folded in:

docs/echo-types/composition.md

@@ -231,9 +231,16 @@ Collecting the above:
 5. **(Open) Tolerance calculus.** For approximate echoes, tolerances
    compose with a Lipschitz-like law.
 
-6. **(Open) Decoration commuting.** Role, grade, linearity, and
+6. **(Partial) Decoration commuting.** Role, grade, linearity, and
    modal decorations commute with composition under conditions to be
-   identified.
+   identified. The grade case is **landed**: `EchoGraded.degrade-compose`
+   shows that any factoring of a `g1 ≤g g3` transition through an
+   intermediate `g2` collapses to the same degraded echo, proved as a
+   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.
 
 ---
 
@@ -259,7 +266,11 @@ Ranked by unblock-value. (1) and (2) landed; (3) onwards is open.
    approximate setting. This is where axis 2 of the taxonomy gets
    teeth.
 6. **Decoration commuting.** Per-decoration lemmas in the existing
-   `EchoGraded`, `EchoLinear`, `EchoIndexed` modules.
+   `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.
 
 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/roadmap.md

@@ -58,12 +58,17 @@ Paths marked **[unblocked]** can proceed today. Paths marked
   needing only the relevant half of g's iso structure. Round-trips
   are **deferred** pending a triangle-identity coherence or a stdlib
   `Function.Bundles.Inverse` shim. See `composition.md` §3.
-- **[partial]** Pentagon coherence for three-fold composition.
-  `Echo-comp-iso-pent-B` and `Echo-comp-iso-pent-echo` both `refl`
-  in `Echo.agda`. The full Σ-associativity iso between the two
-  nested Σ-shapes (outer-first carries an extra intermediate
-  `c : C` with `g b ≡ c`; inner-first absorbs it) remains the open
-  piece of pentagon.
+- **[landed]** Pentagon coherence for three-fold composition.
+  Projection lemmas `Echo-comp-iso-pent-B` and `Echo-comp-iso-pent-echo`
+  both `refl` in `Echo.agda`. The full Σ-associativity iso between the
+  two nested Σ-shapes (outer-first carries an extra intermediate
+  `c : C` with `g b ≡ c`; inner-first absorbs it) now ships as
+  `Echo-comp-pent-Σ-assoc-{to, from, from-to, to-from}`. The forward
+  map collapses `c` against `g b ≡ c` and transports the outer
+  h-equation; the backward map sets `c := g b` with `refl`. Both
+  round-trips reduce definitionally once the `g b ≡ c` has been pinned,
+  so this is a strict iso (no transport coherence required) and lives
+  inside `--safe --without-K`. All four pinned in `Smoke.agda`.
 - **[partial]** Budgeted recursive-surface WF on the ordinal track.
   `Ordinal/Buchholz/RecursiveSurfaceBudget.agda` ships
   `BudgetedBT = ℕ × BT`, the budgeted relation `_<ᵇʳᶠᵇ_` with its
@@ -83,9 +88,23 @@ Paths marked **[unblocked]** can proceed today. Paths marked
   (monotone in ε), and `echo-approx-compose` (additive composition
   under a non-expansive outer leg, realising the taxonomy §2
   conjecture). Wired into `All.agda` and `Smoke.agda`.
-- **[unblocked]** Per-decoration composition lemmas in `EchoGraded`,
+- **[partial]** Per-decoration composition lemmas in `EchoGraded`,
   `EchoLinear`, `EchoIndexed`, `EchoChoreo`, `EchoEpistemic`: check
-  each commutes with basic composition.
+  each commutes with basic composition. Grade case **landed** in
+  `EchoGraded.agda` as `degrade-compose` (any factoring of a
+  `g1 ≤g g3` transition through an intermediate `g2` collapses to
+  the same degraded echo) plus `degrade-via-join` (same statement
+  through the join `_⊔g_`), proved from `≤g-prop` (the order is
+  propositional) and `degrade-comp`. Supporting lemmas
+  `≤g-⊔g-left`, `≤g-⊔g-right`, `≤g-⊔g-univ` exhibit `_⊔g_` as the
+  categorical join. Linear case **landed** in `EchoLinear.agda` as
+  `_≤m_`, `≤m-trans`, `degradeMode`, and `degradeMode-comp`
+  (`linear ⊑ linear ⊑ affine ⊑ affine`; `degradeMode-comp` is the
+  per-decoration composition lemma; auxiliary corollaries
+  `degradeMode-id-linear`, `degradeMode-id-affine`,
+  `degradeMode-strict-is-weaken` make the relationship to the
+  existing `weaken` definitional). Indexed / role / modal cases
+  remain unblocked.
 - **[unblocked]** Add example-library Agda files matching
   `examples.md`: start with examples 1–4 already in-suite, then
   example 7 (ordinal collapse is in `EchoOrdinal`); examples 5, 6,
@@ -200,7 +219,8 @@ tractable today:
 8. **Applications chapter: compiler-analysis residue** — 2 days.
    Largest reader value; entirely unblocked.
 9. **Per-decoration composition lemmas** — 1 day each. Useful
-   coverage.
+   coverage. *Grade case landed* (`EchoGraded.degrade-compose`,
+   `degrade-via-join`); linear / indexed / role / modal still open.
 
 Steps 1 and 5–6 are ~5–6 days of honest work that require nothing
 from proof assistants, external repos, or the blocked Buchholz path.

proofs/agda/EchoGraded.agda

@@ -7,7 +7,7 @@ open import EchoCharacteristic using (collapse)
 open import EchoResidue using (EchoR; TrivialCert; collapse-to-residue)
 
 open import Data.Unit.Base using (⊤; tt)
-open import Relation.Binary.PropositionalEquality using (_≡_; refl)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym)
 
 data Grade : Set where
   keep : Grade
@@ -75,3 +75,86 @@ degrade-comp residue≤residue residue≤residue e = refl
 degrade-comp residue≤residue residue≤forget e = refl
 degrade-comp residue≤forget forget≤forget e = refl
 degrade-comp forget≤forget forget≤forget e = refl
+
+-- Each constructor of `_≤g_` is pinned by both its source and target
+-- grades, so the order is propositional: any two proofs of `g1 ≤g g2`
+-- are equal. Pattern-matches go through under `--without-K` because
+-- each (g1, g2) pair has exactly one inhabitant of `_≤g_`.
+≤g-prop : ∀ {g1 g2} (p p' : g1 ≤g g2) → p ≡ p'
+≤g-prop keep≤keep keep≤keep = refl
+≤g-prop keep≤residue keep≤residue = refl
+≤g-prop keep≤forget keep≤forget = refl
+≤g-prop residue≤residue residue≤residue = refl
+≤g-prop residue≤forget residue≤forget = refl
+≤g-prop forget≤forget forget≤forget = refl
+
+-- Join is an upper bound on its left summand.
+≤g-⊔g-left : ∀ g1 g2 → g1 ≤g (g1 ⊔g g2)
+≤g-⊔g-left keep keep = keep≤keep
+≤g-⊔g-left keep residue = keep≤residue
+≤g-⊔g-left keep forget = keep≤forget
+≤g-⊔g-left residue keep = residue≤residue
+≤g-⊔g-left residue residue = residue≤residue
+≤g-⊔g-left residue forget = residue≤forget
+≤g-⊔g-left forget keep = forget≤forget
+≤g-⊔g-left forget residue = forget≤forget
+≤g-⊔g-left forget forget = forget≤forget
+
+-- Join is an upper bound on its right summand.
+≤g-⊔g-right : ∀ g1 g2 → g2 ≤g (g1 ⊔g g2)
+≤g-⊔g-right keep keep = keep≤keep
+≤g-⊔g-right keep residue = residue≤residue
+≤g-⊔g-right keep forget = forget≤forget
+≤g-⊔g-right residue keep = keep≤residue
+≤g-⊔g-right residue residue = residue≤residue
+≤g-⊔g-right residue forget = forget≤forget
+≤g-⊔g-right forget keep = keep≤forget
+≤g-⊔g-right forget residue = residue≤forget
+≤g-⊔g-right forget forget = forget≤forget
+
+-- Universal property of join: anything dominated by both g1 and g2
+-- is dominated by their join. Together with the two upper-bound
+-- lemmas this exhibits `_⊔g_` as the categorical join in `_≤g_`.
+≤g-⊔g-univ :
+  ∀ {g1 g2 g} → g1 ≤g g → g2 ≤g g → (g1 ⊔g g2) ≤g g
+≤g-⊔g-univ keep≤keep p2 = p2
+≤g-⊔g-univ keep≤residue p2 = p2
+≤g-⊔g-univ keep≤forget p2 = p2
+≤g-⊔g-univ residue≤residue keep≤residue = residue≤residue
+≤g-⊔g-univ residue≤residue residue≤residue = residue≤residue
+≤g-⊔g-univ residue≤forget keep≤forget = residue≤forget
+≤g-⊔g-univ residue≤forget residue≤forget = residue≤forget
+≤g-⊔g-univ residue≤forget forget≤forget = forget≤forget
+≤g-⊔g-univ forget≤forget keep≤forget = forget≤forget
+≤g-⊔g-univ forget≤forget residue≤forget = forget≤forget
+≤g-⊔g-univ forget≤forget forget≤forget = forget≤forget
+
+-- Per-decoration composition. The grade decoration commutes with
+-- composition: any factoring of a transition `g1 ≤g g3` through an
+-- intermediate grade `g2` yields the same degraded echo, regardless of
+-- which intermediate is chosen, and is moreover indistinguishable from
+-- the direct degrade. This is the per-decoration analogue of pentagon
+-- coherence — different paths through the decoration order collapse.
+--
+-- The proof is a corollary of `degrade-comp` (associativity along the
+-- chosen factoring) and `≤g-prop` (any two paths through `_≤g_` agree),
+-- so the per-decoration story rests cleanly on those two ingredients.
+degrade-compose :
+  ∀ {g1 g2 g3}
+  (p12 : g1 ≤g g2) (p23 : g2 ≤g g3) (p13 : g1 ≤g g3)
+  (e : GEcho g1) →
+  degrade p23 (degrade p12 e) ≡ degrade p13 e
+degrade-compose p12 p23 p13 e
+  rewrite ≤g-prop p13 (≤g-trans p12 p23) = degrade-comp p12 p23 e
+
+-- Join-action specialisation: degrading directly to a common upper
+-- bound `g` agrees with degrading first to the join `g1 ⊔g g2` and
+-- then onward via the universal arrow. This is the per-decoration
+-- composition law restated through the join structure.
+degrade-via-join :
+  ∀ {g1 g2 g}
+  (p1 : g1 ≤g g) (p2 : g2 ≤g g) (e : GEcho g1) →
+  degrade p1 e
+  ≡ degrade (≤g-⊔g-univ p1 p2) (degrade (≤g-⊔g-left g1 g2) e)
+degrade-via-join {g1} {g2} p1 p2 e =
+  sym (degrade-compose (≤g-⊔g-left g1 g2) (≤g-⊔g-univ p1 p2) p1 e)

proofs/agda/Smoke.agda

@@ -19,8 +19,15 @@ open import Echo using
   ; Echo-comp-iso-to-from
   ; cancel-iso-to
   ; cancel-iso-from
+  ; cancel-iso-from-to
+  ; cancel-iso-to-from
+  ; hom-natural-id
   ; Echo-comp-iso-pent-B
   ; Echo-comp-iso-pent-echo
+  ; Echo-comp-pent-Σ-assoc-to
+  ; Echo-comp-pent-Σ-assoc-from
+  ; Echo-comp-pent-Σ-assoc-from-to
+  ; Echo-comp-pent-Σ-assoc-to-from
   )
 open import EchoCharacteristic using (collapse; echo-true; echo-false; echo-true≢echo-false)
 open import EchoResidue using (EchoR; collapse-to-residue; strict-weakening-collapse; no-section-collapse-to-residue)
@@ -59,13 +66,23 @@ open import EchoLinear using
   ; weaken
   ; strict-linear-example
   ; no-section-weaken
+  ; _≤m_
+  ; ≤m-trans
+  ; degradeMode
+  ; degradeMode-comp
   )
 
 open import EchoGraded using
   ( Grade
   ; degrade
   ; degrade-comp
   ; ⊔g-assoc
+  ; ≤g-prop
+  ; ≤g-⊔g-left
+  ; ≤g-⊔g-right
+  ; ≤g-⊔g-univ
+  ; degrade-compose
+  ; degrade-via-join
   )
 
 open import EchoTropical using