IndisputableMonolith.Holography.SeamLedgerDischarge

   1import IndisputableMonolith.Holography.SeamTransferCore
   2
   3/-!
   4# SeamLedgerDischarge: typing the R1–R4 residue and pushing B2 below the anomaly reading
   5
   6**Derivation-captain acceptance 2026-07-05** (residues `derive_20260705_135226` [R1],
   7`derive_20260705_155804` [R2], `derive_20260705_171355` [R3], `derive_20260705_184734`
   8[R4], Opus-critic passed): the four conjuncts of `ConservingSeamPricing` are grounded
   9in ledger language. This module TYPES that residue in its WEAKEST honest form and
  10proves that B2 (the deficit-free period `β = 2π/κ` is the UNIQUE zero of the
  11per-cycle seam cost) survives a strict weakening of the fourth conjunct: the exact
  12character-anomaly reading `Tr(W)/2 − 1` is NOT load-bearing for the B2 zero set.
  13
  14## What is THEOREM here (all Lean, no sorry, no axioms)
  15
  161. **The trace bound (THEOREM, the key new lemma).** A pairing-CONSERVING transfer
  17   with real eigenvalue `x > 0` has `Tr W = x + x⁻¹ ≥ 2`, with equality iff `x = 1`
  18   (`conserving_trace_bound`). Route: `preserves_pairForm_iff_det_one` (R2's ledger
  19   conservation IS unimodularity) + `balanced_trace` (Cayley–Hamilton) + AM–GM.
  202. **B2 from the weak premise (THEOREM, FORCED-CONDITIONAL).** For ANY trace
  21   reading `f` with `f 2 = 0` (calibration) and `f t ≠ 0` for `t > 2`
  22   (faithfulness), `LedgerClosurePricing` forces `C κ T = 0 ↔ T = 2π/κ`
  23   (`b2_unique_zero_of_ledgerClosure`). No `J`, no `cosh`, no anomaly normalization
  24   enters the zero-set argument.
  253. **The bridge (THEOREM).** At the anomaly reading `f = (·/2 − 1)`, the weak
  26   premise is EQUIVALENT to `ConservingSeamPricing` (`anomalyLedger_iff_conserving`);
  27   the existing chain `seamTransferPricing_of_conserving` →
  28   `censusPricing_of_seamTransfer` → `b2_unique_zero_of_conserving` is then CITED,
  29   never re-proved, to recover `C = J(turnRatio)` and B2.
  304. **Non-vacuity (THEOREM).** `turnRatioCost` satisfies the weak premise via the
  31   `hyperbolicWitness` family (`ledgerClosurePricing_turnRatioCost`), and every
  32   reading `R` is realized by its own induced cost
  33   (`ledgerClosurePricing_readingCost`).
  345. **Tightness (THEOREM).** Dropping faithfulness or calibration KILLS the
  35   discharge (`faithfulness_is_load_bearing`, `calibration_is_load_bearing`): the
  36   weakening is honest — nothing weaker closes B2.
  37
  38## What stays OPEN (do not overclaim)
  39
  40- **B3**: the identification of `κ` with the horizon's continued clock rate is
  41  typed elsewhere and remains OPEN; R3's `turnRatio` delivery is conditional on it.
  42- **Physical instantiation**: that the ACTUAL seam cost functional satisfies
  43  `LedgerClosurePricing` for some `TraceReading` — i.e., that the physical seam's
  44  closure action, cost report, and audit discipline realize R1–R4 — is the residue.
  45  The prose R1–R4 ground each conjunct in T2 double-entry language; the Lean premise
  46  is tagged **MODEL-until-derived**. Every consumer below is **FORCED-CONDITIONAL**;
  47  the weakest link sets the tag (`soul.mdc`).
  48-/
  49
  50namespace IndisputableMonolith
  51namespace Holography
  52namespace SeamLedgerDischarge
  53
  54open SeamTransferCore TurnRatioCarrier
  55
  56/-! ## Scalar AM–GM half: `x + x⁻¹ ≥ 2` on positives, tight exactly at 1 -/
  57
  58/-- AM–GM for a positive real and its reciprocal: `2 ≤ x + x⁻¹`. This is the
  59scalar engine of the discharge: it converts "delivered eigenvalue exists and is
  60positive" into a one-sided bound on the ONLY audit invariant (the trace). -/
  61theorem two_le_add_inv {x : ℝ} (hx : 0 < x) : 2 ≤ x + x⁻¹ := by
  62  have h1 : x * x⁻¹ = 1 := mul_inv_cancel₀ (ne_of_gt hx)
  63  nlinarith [sq_nonneg (x - 1), hx, h1]
  64
  65/-- The AM–GM bound is tight EXACTLY at `x = 1`: `x + x⁻¹ = 2 ↔ x = 1` on
  66positives. The unique-zero structure of B2 lives entirely in this equivalence. -/
  67theorem add_inv_eq_two_iff {x : ℝ} (hx : 0 < x) : x + x⁻¹ = 2 ↔ x = 1 := by
  68  constructor
  69  · intro h
  70    have hx0 : x ≠ 0 := ne_of_gt hx
  71    have h1 : x * x⁻¹ = 1 := mul_inv_cancel₀ hx0
  72    have hsq : (x - 1) * (x - 1) = 0 := by nlinarith [h, h1, hx]
  73    have h0 : x - 1 = 0 := by
  74      rcases mul_eq_zero.mp hsq with h' | h' <;> exact h'
  75    linarith
  76  · rintro rfl
  77    norm_num
  78
  79/-! ## The key new lemma (B): conservation + positive delivery bound the trace -/
  80
  81/-- **R2 + R3 force the trace (THEOREM).** A transfer conserving the double-entry
  82pairing form (R2, the ledger conservation sentence — converted to `det = 1` by
  83`preserves_pairForm_iff_det_one`, CITED) with a real eigenvalue `x ≠ 0` (R3, the
  84delivered leg) has `Tr W = x + x⁻¹`, by `balanced_trace` (CITED, Cayley–Hamilton).
  85The reciprocal leg is derived, never posited (the circularity fence). -/
  86theorem conserving_trace_eq {W : Matrix (Fin 2) (Fin 2) ℝ} {x : ℝ}
  87    (hcons : ∀ u v, pairForm (W.mulVec u) (W.mulVec v) = pairForm u v)
  88    (hx : 0 < x) (h : HasRealEigen W x) :
  89    W.trace = x + x⁻¹ :=
  90  balanced_trace ((preserves_pairForm_iff_det_one W).mp hcons) (ne_of_gt hx) h
  91
  92/-- **The conserving trace is bounded below by 2 (THEOREM).** Any pairing-conserving
  93transfer with positive delivered eigenvalue has trace at least the identity's. -/
  94theorem conserving_trace_ge_two {W : Matrix (Fin 2) (Fin 2) ℝ} {x : ℝ}
  95    (hcons : ∀ u v, pairForm (W.mulVec u) (W.mulVec v) = pairForm u v)
  96    (hx : 0 < x) (h : HasRealEigen W x) :
  97    2 ≤ W.trace := by
  98  rw [conserving_trace_eq hcons hx h]
  99  exact two_le_add_inv hx
 100
 101/-- **The trace hits 2 exactly at unit delivery (THEOREM).** `Tr W = 2 ↔ x = 1`:
 102the entire zero-set content of B2, expressed on the audit invariant alone. -/
 103theorem conserving_trace_eq_two_iff {W : Matrix (Fin 2) (Fin 2) ℝ} {x : ℝ}
 104    (hcons : ∀ u v, pairForm (W.mulVec u) (W.mulVec v) = pairForm u v)
 105    (hx : 0 < x) (h : HasRealEigen W x) :
 106    W.trace = 2 ↔ x = 1 := by
 107  rw [conserving_trace_eq hcons hx h]
 108  exact add_inv_eq_two_iff hx
 109
 110/-- **The key new lemma, bundled (THEOREM):** for pairing-conserving `W` with real
 111eigenvalue `x > 0`, `Tr W = x + x⁻¹ ≥ 2`, with equality iff `x = 1`. This is what
 112lets the discharge below run on ANY calibrated faithful trace reading, not just the
 113character anomaly: the trace separates "deficit-free" from "mismatched" all by
 114itself. -/
 115theorem conserving_trace_bound {W : Matrix (Fin 2) (Fin 2) ℝ} {x : ℝ}
 116    (hcons : ∀ u v, pairForm (W.mulVec u) (W.mulVec v) = pairForm u v)
 117    (hx : 0 < x) (h : HasRealEigen W x) :
 118    W.trace = x + x⁻¹ ∧ 2 ≤ W.trace ∧ (W.trace = 2 ↔ x = 1) :=
 119  ⟨conserving_trace_eq hcons hx h, conserving_trace_ge_two hcons hx h,
 120    conserving_trace_eq_two_iff hcons hx h⟩
 121
 122/-! ## The typed residue premise (R1–R4, weakest honest form) -/
 123
 124/-- **The R4 residue, weakened to its zero-set content.** R4 (audit invariance: the
 125reported cost is a conjugation class function, because debit/credit are roles and any
 126invertible recombination of the pair fiber is an audit-equivalent relabeling) plus
 127`sl2_add_inv` (CITED from `SeamTransferCore`: the trace is the unique conjugation
 128invariant of a unimodular 2×2 transfer) says the cost reads `W` only through
 129`Tr W`. We type the CONCLUSION of that argument — a single reading function of the
 130trace — plus the two minimal audit normalizations a zero-set theorem needs:
 131
 132* `calibrated`: the identity closure (trace 2, unit delivery) is free. This is a
 133  point condition at ONE trace value, the weakest calibration usable.
 134* `faithful`: a genuine mismatch is not free. Weakened from strict monotonicity on
 135  `[2, ∞)`: nonvanishing on `(2, ∞)` is strictly weaker (strict mono + `f 2 = 0`
 136  implies it), and `(2, ∞)` is EXACTLY the trace range of conserving transfers with
 137  positive non-unit delivery (`conserving_trace_bound`), so nothing weaker can close
 138  B2 — `faithfulness_is_load_bearing` below proves the necessity.
 139
 140Crucially, `f = fun t => t/2 − 1` (the character anomaly) is NOT baked in: the exact
 141anomaly reading is not load-bearing for B2's zero set. -/
 142structure TraceReading where
 143  /-- The reading function: R4's class-function property, factored through the trace
 144  (the unique conjugation invariant at `det = 1`, per `sl2_add_inv`, CITED). -/
 145  f : ℝ → ℝ
 146  /-- Calibration (R4, ledger normalization): the identity closure — no mismatch,
 147  trace 2 — posts zero cost. -/
 148  calibrated : f 2 = 0
 149  /-- Faithfulness (R4, audit discipline): a strictly imbalanced closure — trace
 150  strictly above the identity's — cannot read as free. Stated only on `(2, ∞)`, the
 151  exact realizable range; the weakest condition that closes B2. -/
 152  faithful : ∀ t : ℝ, 2 < t → f t ≠ 0
 153
 154/-- **The typed R1–R4 premise (MODEL until derived).** For each `(κ, T)` the seam's
 155closure action is:
 156
 157* **R1 (linearity, carried by the type):** a matrix `W : Matrix (Fin 2) (Fin 2) ℝ`
 158  on the 2d pair fiber — the additive composition of double-entry postings, banked
 159  from T2, is the linearity; no spectral form is posited.
 160* **R2 (conservation):** `W` conserves the double-entry pairing form `pairForm`
 161  (the oriented debit/credit cross-exposure); a closure that changed it would post
 162  a debit without matching credit, violating T2. No determinant is NAMED here;
 163  `preserves_pairForm_iff_det_one` (CITED) converts.
 164* **R3 (delivery):** the delivered leg scales by the turn ratio `x = κT/(2π)`
 165  (`HasRealEigen W (turnRatio κ T)`); the `2π` is B1's exponential-lattice closure
 166  geometry, `κ` is B3's clock rate (typed, OPEN). No other eigenvalue is posited.
 167* **R4 (weakened reading):** the reported cost is `R.f (Tr W)` for the fixed
 168  calibrated, faithful reading `R` — NOT necessarily the character anomaly.
 169
 170STATUS: **MODEL-until-derived** from the seam ledger. Consumers below are
 171**FORCED-CONDITIONAL** on this premise; the weakest link sets the tag. -/
 172def LedgerClosurePricing (R : TraceReading) (C : ℝ → ℝ → ℝ) : Prop :=
 173  ∀ kappa T : ℝ, 0 < kappa → 0 < T →
 174    ∃ W : Matrix (Fin 2) (Fin 2) ℝ,
 175      (∀ u v, pairForm (W.mulVec u) (W.mulVec v) = pairForm u v) ∧
 176      HasRealEigen W (turnRatio kappa T) ∧
 177      C kappa T = R.f W.trace
 178
 179/-! ## (C) The B2 discharge from the weak premise -/
 180
 181/-- **B2 from the weak residue (THEOREM, FORCED-CONDITIONAL on
 182`LedgerClosurePricing`).** For ANY calibrated faithful trace reading, the
 183deficit-free period `β = 2π/κ` is the UNIQUE zero of the per-cycle cost:
 184
 185* off the period, `turnRatio ≠ 1` (`turnRatio_eq_one_iff`, CITED), so the trace is
 186  strictly above 2 (`conserving_trace_bound`) and faithfulness forbids a zero;
 187* at the period, `turnRatio = 1`, the trace is exactly 2, and calibration fires.
 188
 189The character anomaly appears NOWHERE: the B2 zero set is forced by conservation,
 190delivery, calibration, and faithfulness alone. -/
 191theorem b2_unique_zero_of_ledgerClosure (R : TraceReading) (C : ℝ → ℝ → ℝ)
 192    (h : LedgerClosurePricing R C) (kappa T : ℝ) (hk : 0 < kappa) (hT : 0 < T) :
 193    C kappa T = 0 ↔ T = DeficitFreePeriod.euclideanPeriod kappa := by
 194  obtain ⟨W, hcons, heig, hC⟩ := h kappa T hk hT
 195  have hx : 0 < turnRatio kappa T := turnRatio_pos hk hT
 196  rw [hC]
 197  constructor
 198  · intro h0
 199    by_contra hne
 200    have hx1 : turnRatio kappa T ≠ 1 := fun h1 =>
 201      hne ((turnRatio_eq_one_iff kappa T hk).mp h1)
 202    have htr2 : W.trace ≠ 2 := fun heq =>
 203      hx1 ((conserving_trace_eq_two_iff hcons hx heig).mp heq)
 204    have hgt : 2 < W.trace :=
 205      lt_of_le_of_ne (conserving_trace_ge_two hcons hx heig) (Ne.symm htr2)
 206    exact R.faithful W.trace hgt h0
 207  · intro hTeq
 208    have hx1 : turnRatio kappa T = 1 := (turnRatio_eq_one_iff kappa T hk).mpr hTeq
 209    have htr : W.trace = 2 := by
 210      rw [conserving_trace_eq hcons hx heig, hx1]
 211      norm_num
 212    rw [htr]
 213    exact R.calibrated
 214
 215/-! ## (D) The bridge to the existing chain at the anomaly reading -/
 216
 217/-- The character-anomaly reading: `f t = t/2 − 1`, calibrated (`f 2 = 0`) and
 218faithful (`f t > 0` for `t > 2`). This is ONE admissible reading among many; the
 219discharge above never needs it. It exists to connect to the landed chain. -/
 220noncomputable def anomalyReading : TraceReading where
 221  f := fun t => t / 2 - 1
 222  calibrated := by norm_num
 223  faithful := by
 224    intro t ht
 225    have hpos : 0 < t / 2 - 1 := by linarith
 226    exact ne_of_gt hpos
 227
 228@[simp] theorem anomalyReading_apply (t : ℝ) :
 229    anomalyReading.f t = t / 2 - 1 := rfl
 230
 231/-- **The bridge (THEOREM).** If the reading IS the character anomaly, the weak
 232premise implies `ConservingSeamPricing` (CITED from `SeamTransferCore`): the pieces
 233are literally the same conjuncts, with `R.f (Tr W)` definitionally `charAnomaly W`. -/
 234theorem conservingSeamPricing_of_anomalyLedger (C : ℝ → ℝ → ℝ)
 235    (h : LedgerClosurePricing anomalyReading C) :
 236    SeamTransferCore.ConservingSeamPricing C := by
 237  intro kappa T hk hT
 238  obtain ⟨W, hcons, heig, hC⟩ := h kappa T hk hT
 239  refine ⟨W, hcons, heig, ?_⟩
 240  rw [hC]
 241  exact anomalyReading_apply W.trace
 242
 243/-- **The anomaly instance is exactly the landed premise (THEOREM).** At the
 244character-anomaly reading, `LedgerClosurePricing` and `ConservingSeamPricing` are
 245equivalent: the weak premise strictly GENERALIZES the landed one (any other
 246calibrated faithful reading is also admitted), losing nothing at the anomaly point. -/
 247theorem anomalyLedger_iff_conserving (C : ℝ → ℝ → ℝ) :
 248    LedgerClosurePricing anomalyReading C ↔
 249      SeamTransferCore.ConservingSeamPricing C := by
 250  constructor
 251  · exact conservingSeamPricing_of_anomalyLedger C
 252  · intro h kappa T hk hT
 253    obtain ⟨W, hcons, heig, hC⟩ := h kappa T hk hT
 254    exact ⟨W, hcons, heig, hC.trans rfl⟩
 255
 256/-- **CensusPricing through the chain (THEOREM, CITED).** Anomaly-read ledger
 257pricing yields `CensusPricing` via `seamTransferPricing_of_conserving` and
 258`censusPricing_of_seamTransfer` — cited, never re-proved. -/
 259theorem censusPricing_of_anomalyLedger (C : ℝ → ℝ → ℝ)
 260    (h : LedgerClosurePricing anomalyReading C) :
 261    TurnRatioCarrier.CensusPricing C :=
 262  censusPricing_of_seamTransfer C
 263    (seamTransferPricing_of_conserving C
 264      (conservingSeamPricing_of_anomalyLedger C h))
 265
 266/-- **The cost is J of the turn ratio (THEOREM, FORCED-CONDITIONAL).** At the
 267anomaly reading, the weak premise forces `C κ T = J(κT/2π)` — the full T5 pricing,
 268recovered by citation of the landed chain. -/
 269theorem cost_eq_J_of_anomalyLedger (C : ℝ → ℝ → ℝ)
 270    (h : LedgerClosurePricing anomalyReading C)
 271    (kappa T : ℝ) (hk : 0 < kappa) (hT : 0 < T) :
 272    C kappa T = Cost.Jcost (turnRatio kappa T) :=
 273  censusPricing_of_anomalyLedger C h kappa T hk hT
 274
 275/-- **B2 through the landed chain (THEOREM, CITED).** At the anomaly reading the B2
 276discharge also follows from `b2_unique_zero_of_conserving` — consistency check that
 277the weak route and the landed route agree on the zero set. -/
 278theorem b2_unique_zero_of_anomalyLedger (C : ℝ → ℝ → ℝ)
 279    (h : LedgerClosurePricing anomalyReading C)
 280    (kappa T : ℝ) (hk : 0 < kappa) (hT : 0 < T) :
 281    C kappa T = 0 ↔ T = DeficitFreePeriod.euclideanPeriod kappa :=
 282  b2_unique_zero_of_conserving C
 283    (conservingSeamPricing_of_anomalyLedger C h) kappa T hk hT
 284
 285/-! ## (E) Non-vacuity witnesses -/
 286
 287/-- **Non-vacuity (THEOREM).** The turn-ratio cost satisfies the weak premise at
 288the anomaly reading, witnessed by the `hyperbolicWitness` family (CITED, witness
 289only — never the construction, per the circularity fence). -/
 290theorem ledgerClosurePricing_turnRatioCost :
 291    LedgerClosurePricing anomalyReading TurnRatioCarrier.turnRatioCost := by
 292  intro kappa T hk hT
 293  have hx : 0 < turnRatio kappa T := turnRatio_pos hk hT
 294  have hdet : (hyperbolicWitness (turnRatio kappa T)).det = 1 :=
 295    hyperbolicWitness_det _ (ne_of_gt hx)
 296  refine ⟨hyperbolicWitness (turnRatio kappa T),
 297    (preserves_pairForm_iff_det_one _).mpr hdet,
 298    hyperbolicWitness_eigen _, ?_⟩
 299  have hJ : SeamTransferCore.charAnomaly (hyperbolicWitness (turnRatio kappa T))
 300      = Cost.Jcost (turnRatio kappa T) :=
 301    charAnomaly_eq_J hdet hx (hyperbolicWitness_eigen _)
 302  calc TurnRatioCarrier.turnRatioCost kappa T
 303      = Cost.Jcost (turnRatio kappa T) := rfl
 304    _ = SeamTransferCore.charAnomaly (hyperbolicWitness (turnRatio kappa T)) :=
 305        hJ.symm
 306    _ = anomalyReading.f (hyperbolicWitness (turnRatio kappa T)).trace := rfl
 307
 308/-- **Non-vacuity for EVERY reading (THEOREM).** Each `TraceReading` is realized by
 309its own induced cost `R.f (x + x⁻¹)` via the hyperbolic witness family: the weak
 310premise is inhabited at every admissible reading, so its generality is not vacuous. -/
 311theorem ledgerClosurePricing_readingCost (R : TraceReading) :
 312    LedgerClosurePricing R
 313      (fun kappa T => R.f (turnRatio kappa T + (turnRatio kappa T)⁻¹)) := by
 314  intro kappa T hk hT
 315  have hx : 0 < turnRatio kappa T := turnRatio_pos hk hT
 316  have hdet : (hyperbolicWitness (turnRatio kappa T)).det = 1 :=
 317    hyperbolicWitness_det _ (ne_of_gt hx)
 318  have hcons : ∀ u v, pairForm ((hyperbolicWitness (turnRatio kappa T)).mulVec u)
 319      ((hyperbolicWitness (turnRatio kappa T)).mulVec v) = pairForm u v :=
 320    (preserves_pairForm_iff_det_one _).mpr hdet
 321  refine ⟨hyperbolicWitness (turnRatio kappa T), hcons,
 322    hyperbolicWitness_eigen _, ?_⟩
 323  have htr := conserving_trace_eq hcons hx (hyperbolicWitness_eigen _)
 324  exact congrArg R.f htr.symm
 325
 326/-! ## Tightness: the weakening is exactly as weak as B2 allows -/
 327
 328/-- **Faithfulness is load-bearing (THEOREM).** Dropping `faithful` (keeping the
 329calibrated reading `f ≡ 0`) admits the identically-zero cost, whose zero set
 330contains periods OFF the deficit-free period: B2's uniqueness fails. So the
 331faithfulness clause of `TraceReading` is necessary, not decorative. -/
 332theorem faithfulness_is_load_bearing :
 333    ∃ C : ℝ → ℝ → ℝ,
 334      (∀ kappa T : ℝ, 0 < kappa → 0 < T →
 335        ∃ W : Matrix (Fin 2) (Fin 2) ℝ,
 336          (∀ u v, pairForm (W.mulVec u) (W.mulVec v) = pairForm u v) ∧
 337          HasRealEigen W (turnRatio kappa T) ∧
 338          C kappa T = (fun _ : ℝ => (0 : ℝ)) W.trace) ∧
 339      ∃ kappa T : ℝ, 0 < kappa ∧ 0 < T ∧ C kappa T = 0 ∧
 340        T ≠ DeficitFreePeriod.euclideanPeriod kappa := by
 341  refine ⟨fun _ _ => 0, ?_, 1, 1, one_pos, one_pos, rfl, ?_⟩
 342  · intro kappa T hk hT
 343    have hx : 0 < turnRatio kappa T := turnRatio_pos hk hT
 344    exact ⟨hyperbolicWitness (turnRatio kappa T),
 345      (preserves_pairForm_iff_det_one _).mpr
 346        (hyperbolicWitness_det _ (ne_of_gt hx)),
 347      hyperbolicWitness_eigen _, rfl⟩
 348  · intro hTeq
 349    have h1 : turnRatio 1 1 = 1 := (turnRatio_eq_one_iff 1 1 one_pos).mpr hTeq
 350    have hpi : (3 : ℝ) < Real.pi := Real.pi_gt_three
 351    have h2pi : (2 : ℝ) * Real.pi ≠ 0 := by positivity
 352    unfold TurnRatioCarrier.turnRatio at h1
 353    rw [div_eq_one_iff_eq h2pi] at h1
 354    linarith
 355
 356/-- **Calibration is load-bearing (THEOREM).** Dropping `calibrated` (keeping the
 357faithful reading `f ≡ 1`) admits the constant cost `1`, which has NO zero at all:
 358the deficit-free period would not be a zero, and B2's existence half fails. -/
 359theorem calibration_is_load_bearing :
 360    ∃ C : ℝ → ℝ → ℝ,
 361      (∀ kappa T : ℝ, 0 < kappa → 0 < T →
 362        ∃ W : Matrix (Fin 2) (Fin 2) ℝ,
 363          (∀ u v, pairForm (W.mulVec u) (W.mulVec v) = pairForm u v) ∧
 364          HasRealEigen W (turnRatio kappa T) ∧
 365          C kappa T = (fun _ : ℝ => (1 : ℝ)) W.trace) ∧
 366      ∀ kappa T : ℝ, C kappa T ≠ 0 := by
 367  refine ⟨fun _ _ => 1, ?_, fun _ _ => one_ne_zero⟩
 368  intro kappa T hk hT
 369  have hx : 0 < turnRatio kappa T := turnRatio_pos hk hT
 370  exact ⟨hyperbolicWitness (turnRatio kappa T),
 371    (preserves_pairForm_iff_det_one _).mpr
 372      (hyperbolicWitness_det _ (ne_of_gt hx)),
 373    hyperbolicWitness_eigen _, rfl⟩
 374
 375/-! ## Certificate -/
 376
 377/-- Bundled certificate for the R1–R4 discharge: the trace bound is forced by
 378conservation and positive delivery; B2 holds under EVERY calibrated faithful
 379reading (the character anomaly is not load-bearing for the zero set); the anomaly
 380instance is exactly the landed `ConservingSeamPricing`; and the premise is
 381inhabited. All fields unconditional THEOREMs; the physical instantiation of
 382`LedgerClosurePricing` for the actual seam stays the named MODEL premise, consumed
 383only by the FORCED-CONDITIONAL discharge theorems, stated separately. -/
 384structure SeamLedgerDischargeCert : Prop where
 385  trace_forced : ∀ (W : Matrix (Fin 2) (Fin 2) ℝ) (x : ℝ),
 386    (∀ u v, pairForm (W.mulVec u) (W.mulVec v) = pairForm u v) →
 387    0 < x → HasRealEigen W x →
 388    W.trace = x + x⁻¹ ∧ 2 ≤ W.trace ∧ (W.trace = 2 ↔ x = 1)
 389  b2_any_reading : ∀ (R : TraceReading) (C : ℝ → ℝ → ℝ),
 390    LedgerClosurePricing R C → ∀ kappa T : ℝ, 0 < kappa → 0 < T →
 391      (C kappa T = 0 ↔ T = DeficitFreePeriod.euclideanPeriod kappa)
 392  anomaly_bridge : ∀ C : ℝ → ℝ → ℝ,
 393    LedgerClosurePricing anomalyReading C ↔
 394      SeamTransferCore.ConservingSeamPricing C
 395  nonvacuous : LedgerClosurePricing anomalyReading TurnRatioCarrier.turnRatioCost
 396
 397/-- The certificate holds. -/
 398theorem seamLedgerDischargeCert : SeamLedgerDischargeCert where
 399  trace_forced := fun _ _ hcons hx h => conserving_trace_bound hcons hx h
 400  b2_any_reading := fun R C h kappa T hk hT =>
 401    b2_unique_zero_of_ledgerClosure R C h kappa T hk hT
 402  anomaly_bridge := anomalyLedger_iff_conserving
 403  nonvacuous := ledgerClosurePricing_turnRatioCost
 404
 405end SeamLedgerDischarge
 406end Holography
 407end IndisputableMonolith
 408