characteristic/EI: discharge n=3 enumeration (obl 4) + generic forward direction (obl 5 fwd)

Stacked on #55 (uses the Axis / ProperNonLossOnly / ProperlyStrict
machinery introduced there). Re-target to main after #55 merges.

Two residual EI-2 obligations discharged in their defensible form,
in the same formal shape as the existing n=2 exhibits:

* Obligation 4 (n=3): rmg-cell-action + RoleModeGrade-has-non-trivial-cell
  + recipe-non-triviality-concrete-n3. Mechanical extension of the
  concrete enumeration to the 3D RoleModeGrade construction; reuses
  RoleModeGrade.trace-non-trivial-cell, adds no new mathematical
  content beyond the PreservesDistinct certificate + enumeration entry.

* Obligation 5 (FORWARD half), generically: ProperNonLossOnly =>
  distinguishing-step, and generic-2cell-forward (composition with any
  pointwise-identity second-axis step). choreo-instantiates-generic-
  forward links the concrete cells to the generic statement. The
  forward direction needs neither decidable equality on D nor a live
  decoration -- a sharpening of the file's own meta-claim. The REVERSE
  half remains walled by extensionality under --safe (unchanged).

EI-2 verdict UNCHANGED ([CLOSED-NEG] / PATH B): neither reopened nor
terminated; residual obligations discharged exactly as the proper-
strict sharpening discharged the loss-only obligation. Honours
retraction R-2026-05-18 (no retracted vocabulary). Full characteristic
lane typechecks --safe --without-K, zero postulates, zero escape
pragmas.

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

Author: hyperpolymath

proofs/agda/characteristic/RecipeNonTriviality.agda

@@ -156,6 +156,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
@@ -299,6 +303,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)
 --
@@ -327,6 +370,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
@@ -340,6 +385,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)
 --
@@ -564,6 +626,84 @@ Mode-is-not-proper-non-loss-only
         (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)
 --