characteristic/EI: discharge abstract loss-only obligation (sharpened proper-strict criterion) (#55)

## Summary

Discharges the abstract loss-only obligation flagged open in
`proofs/agda/characteristic/RecipeNonTriviality.agda` (`--
Mode-is-loss-only : ¬ NonLossOnly ModeAxis -- ^^^ open obligation`).

The literal claim `¬ NonLossOnly ModeAxis` is **false**: the un-refined
`NonLossOnly` counts *reflexive* identity steps as "strict", so it is
vacuously satisfied by every axis with a multi-inhabitant decoration.
Rather than paper over the gap, this PR:

1. **Proves the vacuity explicitly** —
`NonLossOnly-holds-vacuously-for-Mode`.
2. **Sharpens the criterion** to the intended irreflexive reading (cf.
`ChoreoInjective.agda`: "strict (non-reflexive) steps") —
`ProperlyStrict` / `ProperNonLossOnly`.
3. **Retains the positive case** — `ChoreoAxis-proper-non-loss-only`.
4. **Discharges the obligation** — `Mode-is-not-proper-non-loss-only`.

## Verification
- `--safe --without-K`, **zero postulates, zero escape pragmas**.
- Full characteristic lane typechecks (`agda -i proofs/agda
proofs/agda/characteristic/All.agda`, exit 0) on a clean
true-`origin/main` base.

## Scope
- **EI-2 unchanged**: remains `[CLOSED-NEG]` (terminated-negative). Not
reopened.
- Retraction **R-2026-05-18** honoured — no retracted vocabulary
reinstated.
- Commit author = 6759885+hyperpolymath@users.noreply.github.com.

## Note: branch replanted
This branch was force-updated. The earlier push had drifted onto
**#54**'s base (`docs/echo-types-master-map`) and bundled `README.md` +
the whole `docs/echo-types/MAP.adoc` — not part of this change. It is
now replanted onto true `origin/main` (`2ca3122`) and contains the
**single Agda proof file only**. The MAP.adoc status tag for this work
is posted as a review comment on #54 (which owns that file), per "link,
don't duplicate".

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

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

Author: hyperpolymath

proofs/agda/characteristic/RecipeNonTriviality.agda

@@ -124,6 +124,9 @@ open import EchoLinear                            using
   ; linear≤linear
   ; linear≤affine
   ; affine≤affine
+  ; LEcho
+  ; degradeMode
+  ; affine-all-equal
   )
 open import EchoGraded                            using
   ( Grade
@@ -138,7 +141,12 @@ open import EchoGraded                            using
   ; residue≤forget
   ; forget≤forget
   )
-open import EchoCharacteristic                    using (collapse)
+open import EchoCharacteristic                    using
+  ( collapse
+  ; echo-true
+  ; echo-false
+  ; echo-true≢echo-false
+  )
 open import characteristic.RoleGraded             using
   ( RoleGEcho
   ; applyRole
@@ -158,6 +166,10 @@ open import characteristic.ModeGraded             using
   ( MGEcho     to ModeGEcho
   ; applyGrade to applyGradeM
   )
+open import characteristic.RoleModeGrade          using
+  ( applyAll
+  ; trace-non-trivial-cell
+  )
 
 ------------------------------------------------------------------------
 -- Definitions of "non-trivial" for the formal theorem
@@ -301,6 +313,45 @@ ModeGrade-no-non-identity-cell :
   NonIdentity modegrade-cell-action → ⊥
 ModeGrade-no-non-identity-cell (x , px) = px refl
 
+------------------------------------------------------------------------
+-- n=3 — RoleModeGrade (EI-2 obligation 4, formal enumeration form)
+--
+-- The 3D construction's pairwise/triple commutations are already
+-- discharged in characteristic.RoleModeGrade (all by `refl`). What
+-- was only stated there as a prose tracker entry — that the 3D
+-- construction has its non-trivial cell *because* it contains the
+-- non-loss-only axis Role — is here promoted to the SAME formal
+-- shape as the n=2 exhibits above. This is the mechanical extension
+-- of the concrete enumeration from n=2 to n=3 (obligation 4); it
+-- adds no new mathematical content over RoleModeGrade, only the
+-- formal `PreservesDistinct` certificate and an enumeration entry.
+--
+-- The unique live triple cell is (c⊑s, linear≤linear, keep≤keep);
+-- `applyAll` at that cell computes to `client-to-server` (proved in
+-- RoleModeGrade as `trace-non-trivial-cell`), so the n=3 cell action
+-- preserves distinctness via the same Choreo distinguishing pair.
+------------------------------------------------------------------------
+
+rmg-cell-action : RoleEcho Client true → RoleEcho Server true
+rmg-cell-action e = applyAll c⊑s linear≤linear keep≤keep e
+
+rmg-cell-action-equals-c2s :
+  ∀ (e : RoleEcho Client true) →
+  rmg-cell-action e ≡ client-to-server e
+rmg-cell-action-equals-c2s = trace-non-trivial-cell
+
+RoleModeGrade-has-non-trivial-cell :
+  PreservesDistinct rmg-cell-action
+RoleModeGrade-has-non-trivial-cell =
+  rg-input₁ , rg-input₂ , rg-inputs-distinct , rmg-images-distinct
+  where
+    rmg-images-distinct :
+      rmg-cell-action rg-input₁ ≢ rmg-cell-action rg-input₂
+    rmg-images-distinct p =
+      rg-images-distinct
+        (trans (sym (rmg-cell-action-equals-c2s rg-input₁))
+               (trans p (rmg-cell-action-equals-c2s rg-input₂)))
+
 ------------------------------------------------------------------------
 -- The recipe-non-triviality theorem (concrete form)
 --
@@ -329,6 +380,8 @@ data ConstructionWithStatus : Set where
                       ConstructionWithStatus
   mg-trivial        : (NonIdentity modegrade-cell-action → ⊥) →
                       ConstructionWithStatus
+  rmg-non-trivial   : PreservesDistinct rmg-cell-action →
+                      ConstructionWithStatus
 
 -- The recipe-non-triviality theorem (concrete enumeration form):
 -- each of the three 2D constructions has the non-triviality status
@@ -342,6 +395,23 @@ recipe-non-triviality-concrete =
   , rm-non-trivial RoleMode-has-non-trivial-cell
   , mg-trivial ModeGrade-no-non-identity-cell
 
+-- The recipe-non-triviality theorem extended to n=3: the three n=2
+-- constructions plus the 3D RoleModeGrade construction, each with
+-- the non-triviality status predicted by the hypothesis (non-trivial
+-- iff the tuple contains a non-loss-only axis; RoleModeGrade is
+-- non-trivial because it contains Role). This discharges EI-2
+-- obligation 4 in the same formal enumeration shape as the n=2 case.
+recipe-non-triviality-concrete-n3 :
+  ConstructionWithStatus
+  × ConstructionWithStatus
+  × ConstructionWithStatus
+  × ConstructionWithStatus
+recipe-non-triviality-concrete-n3 =
+    rg-non-trivial  RoleGraded-has-non-trivial-cell
+  , rm-non-trivial  RoleMode-has-non-trivial-cell
+  , mg-trivial      ModeGrade-no-non-identity-cell
+  , rmg-non-trivial RoleModeGrade-has-non-trivial-cell
+
 ------------------------------------------------------------------------
 -- §<<abstract>> — Generic abstract axis machinery (partial)
 --
@@ -359,7 +429,14 @@ recipe-non-triviality-concrete =
 --
 -- Status of the generic form:
 --   * Axis record: defined.
---   * NonLossOnly predicate: defined.
+--   * NonLossOnly predicate: defined (and shown vacuous — see
+--     `NonLossOnly-holds-vacuously-for-Mode`).
+--   * ProperNonLossOnly predicate (sharpened, irreflexive): defined.
+--   * Choreo certified under the sharpened predicate
+--     (`ChoreoAxis-proper-non-loss-only`).
+--   * Mode loss-only under the sharpened predicate: DISCHARGED
+--     (`Mode-is-not-proper-non-loss-only`). This is the abstract
+--     obligation previously flagged open.
 --   * Generic 2D family: requires decidable equality and a live
 --     decoration; partial scaffolding below.
 --   * Generic forward direction: not yet proved.
@@ -433,40 +510,209 @@ ChoreoAxis-non-loss-only =
   Client , Server , c⊑s , choreo-c⊑s-strict
 
 ------------------------------------------------------------------------
--- Mode is loss-only at the abstract level.
---
--- The strict step linear≤affine has transport `weaken` =
--- collapse-to-residue, which collapses Echo collapse tt (multiple
--- inhabitants) to EchoR ⊤ TrivialCert tt (one inhabitant up to
--- TrivialCert structure). All inputs map to the same output, so
--- the step has no distinguishing pair.
---
--- Formalising "no distinguishing pair" requires showing that
--- distinct inputs map to equal outputs, which is the
--- collapse-residue-same property. EchoLinear has
--- weaken-collapses-distinction : weaken echo-true ≡ weaken echo-false
--- as the formal certificate. We can lift this to "Mode is not
--- non-loss-only" — i.e., Mode does not satisfy NonLossOnly.
---
--- However: NonLossOnly only requires the EXISTENCE of *some* strict
--- step with a distinguishing pair. Mode has only one strict step
--- (linear≤affine), and we need to show it has no distinguishing
--- pair. This requires examining all pairs of inputs in
--- LEcho linear and showing they all map to equal outputs under
--- weaken — which involves the universal property of LEcho linear.
---
--- This is straightforward but requires more machinery (LEcho's
--- definition unfolds to Echo collapse tt; collapse-to-residue's
--- behaviour on all such inputs; uniqueness of the residue).
---
--- Left as an open obligation in the abstract section. The concrete
--- forward direction above (rolegraded-cell-action,
--- rolemode-cell-action) does not depend on this abstract
--- formalisation.
+-- Why `Mode-is-loss-only : ¬ NonLossOnly ModeAxis` cannot be proved
+-- as literally stated — and the sharpening that discharges it.
+--
+-- The flagged obligation was `¬ NonLossOnly ModeAxis`. That claim is
+-- FALSE under the `NonLossOnly` predicate above, and the file below
+-- proves it false rather than papering over the gap.
+--
+-- The defect is in `IsStrict`/`NonLossOnly`: a step counts as
+-- "strict" merely if it carries a distinguishing pair. But the
+-- *reflexive* steps `m ≤m m` transport by the identity
+-- (`degradeMode linear≤linear e = e` definitionally), and the
+-- identity trivially preserves distinguishability whenever the
+-- decoration has ≥2 separable inhabitants. So *every* axis with a
+-- multi-inhabitant decoration satisfies `NonLossOnly` via a
+-- reflexive step — the predicate is vacuously true and does not
+-- discriminate loss-only axes at all. `Mode` is no exception:
+-- `NonLossOnly-holds-vacuously-for-Mode` below exhibits the witness
+-- explicitly, which is exactly why `¬ NonLossOnly ModeAxis` is
+-- unprovable.
+--
+-- The rigorous fix is to SHARPEN the criterion to the intended
+-- reading (cf. ChoreoInjective.agda: "at least one of its strict
+-- (non-reflexive) steps"): a *proper* strict step must move between
+-- DISTINCT decorations. Under that sharpened predicate
+-- (`ProperNonLossOnly`):
+--
+--   * Choreo still certifies (c⊑s : Client ≢ Server, distinguishing
+--     transport) — the positive case is not lost.
+--   * Mode does NOT certify: its only inter-decoration step is
+--     linear≤affine, whose transport `weaken` lands in `LEcho affine`
+--     where `affine-all-equal` forces ALL outputs equal, so no
+--     distinguishing pair can exist. The reflexive steps are now
+--     excluded by the `distinct` requirement.
+--
+-- This discharges the abstract obligation in its defensible form:
+-- `Mode-is-not-proper-non-loss-only`. It does NOT affect the
+-- terminated-negative EI-2 verdict (see TERMINATION NOTICE / the
+-- EI-2 STATUS banners and docs/EI2_REPORT.adoc); it removes a
+-- residual proof-debt comment from the abstract section and
+-- sharpens the underlying criterion.
+------------------------------------------------------------------------
+
+-- The original predicate is vacuously satisfied by Mode via the
+-- reflexive linear step. This is the concrete reason
+-- `¬ NonLossOnly ModeAxis` is FALSE (not merely "hard").
+ModeAxis : Axis
+ModeAxis = record
+  { D   = Mode
+  ; _≤_ = _≤m_
+  ; F   = LEcho
+  ; t   = degradeMode
+  }
+
+mode-linear-reflexive-strict : IsStrict ModeAxis linear≤linear
+mode-linear-reflexive-strict = record
+  { x     = echo-true
+  ; y     = echo-false
+  ; x≢y   = echo-true≢echo-false
+  ; tx≢ty = echo-true≢echo-false
+  }
+
+NonLossOnly-holds-vacuously-for-Mode : NonLossOnly ModeAxis
+NonLossOnly-holds-vacuously-for-Mode =
+  linear , linear , linear≤linear , mode-linear-reflexive-strict
+
+------------------------------------------------------------------------
+-- Sharpened criterion: a *proper* strict step moves between DISTINCT
+-- decorations. This excludes reflexive identity steps, which carry
+-- no information-preserving transport content of their own.
 ------------------------------------------------------------------------
 
--- Mode-is-loss-only : ¬ NonLossOnly ModeAxis
--- ^^^ open obligation; requires more LEcho machinery.
+record ProperlyStrict (a : Axis) {d1 d2 : Axis.D a}
+                      (le : Axis._≤_ a d1 d2) : Set where
+  open Axis a
+  field
+    distinct : d1 ≢ d2
+    x y      : F d1
+    x≢y      : x ≢ y
+    tx≢ty    : t le x ≢ t le y
+
+ProperNonLossOnly : Axis → Set
+ProperNonLossOnly a =
+  Σ (Axis.D a) (λ d1 →
+  Σ (Axis.D a) (λ d2 →
+  Σ (Axis._≤_ a d1 d2) (λ le →
+    ProperlyStrict a le)))
+
+------------------------------------------------------------------------
+-- The sharpening keeps the positive case: Choreo still certifies,
+-- now via the genuinely proper step c⊑s (Client ≢ Server).
+------------------------------------------------------------------------
+
+ChoreoAxis-proper-non-loss-only : ProperNonLossOnly ChoreoAxis
+ChoreoAxis-proper-non-loss-only =
+  Client , Server , c⊑s , record
+    { distinct = λ ()
+    ; x        = rg-input₁
+    ; y        = rg-input₂
+    ; x≢y      = rg-inputs-distinct
+    ; tx≢ty    = rg-images-distinct
+    }
+
+------------------------------------------------------------------------
+-- The discharged obligation: Mode is loss-only under the sharpened
+-- (proper-step) criterion. Case analysis on the mode order:
+--
+--   * linear≤linear / affine≤affine — reflexive; `distinct` is
+--     `m ≡ m → ⊥`, refuted by `refl`.
+--   * linear≤affine — the unique inter-decoration step; its
+--     transport `degradeMode linear≤affine = weaken` lands in
+--     `LEcho affine`, where `affine-all-equal` makes every pair of
+--     outputs equal, contradicting `tx≢ty`.
+------------------------------------------------------------------------
+
+Mode-is-not-proper-non-loss-only : ProperNonLossOnly ModeAxis → ⊥
+Mode-is-not-proper-non-loss-only
+  (linear , linear , linear≤linear , ps) = ProperlyStrict.distinct ps refl
+Mode-is-not-proper-non-loss-only
+  (affine , affine , affine≤affine , ps) = ProperlyStrict.distinct ps refl
+Mode-is-not-proper-non-loss-only
+  (linear , affine , linear≤affine , ps) =
+    ProperlyStrict.tx≢ty ps
+      (affine-all-equal
+        (degradeMode linear≤affine (ProperlyStrict.x ps))
+        (degradeMode linear≤affine (ProperlyStrict.y ps)))
+
+------------------------------------------------------------------------
+-- Generic forward direction (EI-2 obligation 5, FORWARD half)
+--
+-- The §<<abstract>> header above speculated that the generic forward
+-- direction needs decidable equality on D plus a designated "live"
+-- decoration. That over-estimates the requirement: once the
+-- criterion is stated in its sharpened (proper-step) form, the
+-- forward direction follows directly from `ProperlyStrict`. A
+-- properly-non-loss-only axis exhibits a step whose transport is a
+-- distinctness-preserving (hence non-identity-acting) map. No
+-- decidable equality and no live decoration are needed; this is a
+-- sharpening of the file's own meta-claim about the requirement.
+--
+-- This discharges the FORWARD half of obligation 5 generically. The
+-- REVERSE half (no-NLO ⇒ every cell trivial) is unaffected and
+-- remains walled off by needing extensionality under --safe (see the
+-- §<<abstract>> note and PATH A/B below). The EI-2 verdict is
+-- UNCHANGED: this neither reopens nor terminates EI-2 (cf. the
+-- TERMINATION NOTICE and docs/EI2_REPORT.adoc); it discharges a
+-- residual obligation in its defensible form, exactly as the
+-- proper-strict sharpening did for the loss-only obligation.
+------------------------------------------------------------------------
+
+-- Forward, bare form: a properly-non-loss-only axis has a step whose
+-- transport preserves distinctness (is non-trivial).
+ProperNonLossOnly⇒distinguishing-step :
+  ∀ (a : Axis) → ProperNonLossOnly a →
+  Σ (Axis.D a) (λ d1 →
+  Σ (Axis.D a) (λ d2 →
+  Σ (Axis._≤_ a d1 d2) (λ le →
+    PreservesDistinct (Axis.t a le))))
+ProperNonLossOnly⇒distinguishing-step a (d1 , d2 , le , ps) =
+  d1 , d2 , le ,
+  ( ProperlyStrict.x ps
+  , ProperlyStrict.y ps
+  , ProperlyStrict.x≢y ps
+  , ProperlyStrict.tx≢ty ps )
+
+-- Forward, 2D-cell form: composing that distinguishing step with ANY
+-- second-axis step whose action on the codomain is the identity
+-- still yields a cell whose composed action preserves distinctness.
+-- The identity hypothesis is supplied POINTWISE (∀ z → gB z ≡ z) —
+-- which every concrete reflexive second-axis step satisfies by
+-- `refl` — so the proof never invokes function extensionality.
+generic-2cell-forward :
+  ∀ (a : Axis) {d1 d2 : Axis.D a} (le : Axis._≤_ a d1 d2)
+    (ps : ProperlyStrict a le)
+    (gB : Axis.F a d2 → Axis.F a d2) →
+  (∀ z → gB z ≡ z) →
+  PreservesDistinct (λ w → gB (Axis.t a le w))
+generic-2cell-forward a le ps gB gB-id =
+    ProperlyStrict.x ps
+  , ProperlyStrict.y ps
+  , ProperlyStrict.x≢y ps
+  , λ eq → ProperlyStrict.tx≢ty ps
+             (trans (sym (gB-id (Axis.t a le (ProperlyStrict.x ps))))
+                    (trans eq
+                           (gB-id (Axis.t a le (ProperlyStrict.y ps)))))
+
+-- The concrete cells are instances of the generic forward direction:
+-- ChoreoAxis is properly-non-loss-only via c⊑s, and the second-axis
+-- contribution in the concrete n=2/n=3 cells is pointwise-identity
+-- (`applyGrade keep≤keep` / `applyMode linear≤linear`, both `refl`).
+-- This is the link between the concrete enumeration above and the
+-- generic statement (non-vacuity witness; no duplication of content).
+choreo-instantiates-generic-forward :
+  PreservesDistinct (λ w → (λ z → z) (Axis.t ChoreoAxis c⊑s w))
+choreo-instantiates-generic-forward =
+  generic-2cell-forward ChoreoAxis c⊑s
+    (record
+      { distinct = λ ()
+      ; x        = rg-input₁
+      ; y        = rg-input₂
+      ; x≢y      = rg-inputs-distinct
+      ; tx≢ty    = rg-images-distinct
+      })
+    (λ z → z) (λ z → refl)
 
 ------------------------------------------------------------------------
 -- Summary (prose; the formal content is above)