IndisputableMonolith.Holography.SeamTransferCore

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.Holography.TurnRatioCarrier
   4
   5/-!
   6# SeamTransferCore: the balanced pair-fiber transfer forces J (LEG-B Phase B)
   7
   8**Panel decision 2026-07-05** (`state/panel/censuspricing_20260705_20260705_125417.json`,
   9judge: Fable over 6 directors; the Scale-Holonomy Trace Core, Phase B): the per-closure
  10recognition cost of a seam crossing at mismatch ratio `x` is the CHARACTER ANOMALY
  11`C = Tr(W)/2 − 1` of the transfer `W` that one closure induces on the seam's
  12double-entry pair fiber. This module lands the per-closure half of that program:
  13
  141. **Balance forces the reciprocal leg (THEOREM, the circularity fence).** The panel's
  15   standing guardrail: never POSIT `W = diag(x, x⁻¹)` (that is J in a trench coat).
  16   Here the delivered leg scaling by `x` is the only scaling assumed; the conjugate
  17   `x⁻¹` is DERIVED: a balanced (`det W = 1`) transfer with real eigenvalue `x ≠ 0`
  18   necessarily has `x⁻¹` as its other eigenvalue (`balanced_conjugate`), because the
  19   product of the eigenvalues IS the determinant, and double-entry balance pins the
  20   determinant to 1. Reciprocity is not a modeling choice: it is conservation.
  21
  222. **The trace is then forced (THEOREM).** `Tr W = x + x⁻¹` (`balanced_trace`), by
  23   Cayley–Hamilton on the 2×2 characteristic polynomial `λ² − Tr·λ + det`. Hence the
  24   character anomaly equals the T5 cost: `Tr(W)/2 − 1 = J(x)` (`charAnomaly_eq_J`).
  25   J appears NOWHERE in the inputs (a determinant condition and one eigenvalue); it
  26   emerges from the algebra.
  27
  283. **The reduction theorem (THEOREM).** `censusPricing_of_seamTransfer`: if for every
  29   `(κ, T)` the physical per-cycle cost is the character anomaly of SOME balanced
  30   transfer whose delivered leg scales by the turn ratio `x = κT/(2π)`, then
  31   `CensusPricing` holds. The pricing premise of `TurnRatioCarrier` (which names J)
  32   is thereby REDUCED to `SeamTransferPricing` (which does not): a 2d pair fiber, a
  33   unit determinant, a delivered-leg eigenvalue, a trace reading. Each conjunct is a
  34   checkable structural fact about the seam; none names the answer.
  35
  364. **The elliptic retrodiction (THEOREM).** The kernel's landed phase-branch poison is
  37   this frame's elliptic class, on the nose: the character anomaly of the rotation
  38   transfer IS `phaseCost` (`charAnomaly_rotation`), and a rotation admits NO real
  39   eigenvalue besides ±1 (`elliptic_no_real_mismatch`) — the elliptic class cannot
  40   carry a genuine mismatch ratio `x > 0, x ≠ 1` at all. The earlier dead end was not
  41   bad luck; it was the wrong conjugacy class, provably.
  42
  435. **The falsifier, made numeric (THEOREM, panel Live Bet 2).** The two landed census
  44   observables of the n-fold retrace (absolute surplus `n − 1` posts per sector,
  45   relative surplus `(n−1)/n` per post) PAIR to exactly `J(n)`
  46   (`surplus_pairing_eq_J`, via the double-entry pairing identity
  47   `Jcost_pairing : J(x) = (x−1)(1−x⁻¹)/2`). The pairing pricing and single-column
  48   (linear) pricing are DISTINGUISHED at the triple cover: `J(3)/J(2) = 8/3 ≠ 2`
  49   (`cover_cost_ratio_eq`, `pricing_discriminated`); the kernel `decide` facts for the
  50   triple retrace (closure, census completeness, exactly-3 posts per sector) are
  51   landed as `witnessWalk3_census`. If the physical seam ever prices the triple cover
  52   at ratio 2, the trace carrier is dead; 8/3 is its signature.
  53
  54## Honest scope (do not overclaim)
  55
  56What is proved here is per-closure matrix algebra plus the reduction: `CensusPricing`
  57now follows from `SeamTransferPricing`. What is NOT proved is that the physical seam
  58DELIVERS such a transfer (that the pair fiber is 2-dimensional over ℝ, that one
  59closure acts on it linearly with the delivered leg scaling by the turn ratio, and that
  60double-entry balance is unimodularity). That residue is typed here as
  61`SeamTransferPricing` and stays MODEL until derived from the seam ledger (T2
  62double-entry + the `PairedCycleFlow` carrier of `SeamCycleCarrier.lean`). The flow
  63half (Fricke ⇒ d'Alembert ⇒ T5 classification) is Phase A, in a sibling module.
  64Consumers remain FORCED-CONDITIONAL; the weakest link sets the tag (`soul.mdc`).
  65-/
  66
  67namespace IndisputableMonolith
  68namespace Holography
  69namespace SeamTransferCore
  70
  71open Matrix
  72
  73/-! ## The pair-fiber transfer: eigenvalue and balance -/
  74
  75/-- `W` has real eigenvalue `x`: some nonzero fiber vector scales by `x` under one
  76closure. For the seam this is the DELIVERED leg: "the crossing delivers `x` per unit
  77required" is a scaling statement, definitional for mismatch ratio `x`. Nothing about
  78the other leg is assumed. -/
  79def HasRealEigen (W : Matrix (Fin 2) (Fin 2) ℝ) (x : ℝ) : Prop :=
  80  ∃ v : Fin 2 → ℝ, v ≠ 0 ∧ W.mulVec v = x • v
  81
  82/-- The character anomaly of a transfer: `Tr(W)/2 − 1`. The unique conjugation-
  83invariant scalar of the closure holonomy, normalized to vanish at the identity. -/
  84noncomputable def charAnomaly (W : Matrix (Fin 2) (Fin 2) ℝ) : ℝ :=
  85  W.trace / 2 - 1
  86
  87/-- **Cayley–Hamilton, evaluated:** the characteristic determinant of a 2×2 transfer
  88is `y² − Tr·y + det`. -/
  89lemma det_sub_smul_one (W : Matrix (Fin 2) (Fin 2) ℝ) (y : ℝ) :
  90    (W - y • (1 : Matrix (Fin 2) (Fin 2) ℝ)).det
  91      = y ^ 2 - W.trace * y + W.det := by
  92  rw [Matrix.det_fin_two, Matrix.trace_fin_two, Matrix.det_fin_two]
  93  simp only [Matrix.sub_apply, Matrix.smul_apply, Matrix.one_apply, smul_eq_mul]
  94  norm_num
  95  ring
  96
  97/-- A real eigenvalue is a root of the characteristic polynomial:
  98`x² − Tr·x + det = 0`. -/
  99lemma eigen_char {W : Matrix (Fin 2) (Fin 2) ℝ} {x : ℝ} (h : HasRealEigen W x) :
 100    x ^ 2 - W.trace * x + W.det = 0 := by
 101  obtain ⟨v, hv, hWv⟩ := h
 102  have hker : (W - x • (1 : Matrix (Fin 2) (Fin 2) ℝ)).mulVec v = 0 := by
 103    rw [Matrix.sub_mulVec, Matrix.smul_mulVec, Matrix.one_mulVec, hWv, sub_self]
 104  have hdet : (W - x • (1 : Matrix (Fin 2) (Fin 2) ℝ)).det = 0 :=
 105    Matrix.exists_mulVec_eq_zero_iff.mp ⟨v, hv, hker⟩
 106  rw [det_sub_smul_one] at hdet
 107  exact hdet
 108
 109/-- **Balance forces the trace (THEOREM).** A balanced (`det = 1`, double-entry
 110conservation) transfer whose delivered leg scales by `x ≠ 0` has trace exactly
 111`x + x⁻¹`. The reciprocal appears in the OUTPUT, derived; it was not an input. -/
 112theorem balanced_trace {W : Matrix (Fin 2) (Fin 2) ℝ} {x : ℝ}
 113    (hdet : W.det = 1) (hx : x ≠ 0) (h : HasRealEigen W x) :
 114    W.trace = x + x⁻¹ := by
 115  have hchar := eigen_char h
 116  rw [hdet] at hchar
 117  field_simp
 118  nlinarith [hchar]
 119
 120/-- **Balance forces the reciprocal leg (THEOREM, the circularity fence honored).**
 121If a balanced transfer has real eigenvalue `x ≠ 0`, then `x⁻¹` is ALSO an eigenvalue:
 122the conjugate column scales by the reciprocal because the eigenvalue product IS the
 123determinant and double-entry pins the determinant to 1. This is the panel's guardrail
 124discharged: `diag(x, x⁻¹)` is never posited; the `x⁻¹` is a consequence of balance. -/
 125theorem balanced_conjugate {W : Matrix (Fin 2) (Fin 2) ℝ} {x : ℝ}
 126    (hdet : W.det = 1) (hx : x ≠ 0) (h : HasRealEigen W x) :
 127    HasRealEigen W x⁻¹ := by
 128  have htr := balanced_trace hdet hx h
 129  have hdet0 : (W - x⁻¹ • (1 : Matrix (Fin 2) (Fin 2) ℝ)).det = 0 := by
 130    rw [det_sub_smul_one, hdet, htr]
 131    field_simp
 132    ring
 133  obtain ⟨v, hv, hker⟩ := Matrix.exists_mulVec_eq_zero_iff.mpr hdet0
 134  refine ⟨v, hv, ?_⟩
 135  have := hker
 136  rw [Matrix.sub_mulVec, Matrix.smul_mulVec, Matrix.one_mulVec,
 137    sub_eq_zero] at this
 138  exact this
 139
 140/-- **The character anomaly of a balanced transfer IS the T5 cost (THEOREM).**
 141`Tr(W)/2 − 1 = J(x)` for the delivered ratio `x > 0`. J is never mentioned in the
 142hypotheses; it emerges from Cayley–Hamilton + balance. -/
 143theorem charAnomaly_eq_J {W : Matrix (Fin 2) (Fin 2) ℝ} {x : ℝ}
 144    (hdet : W.det = 1) (hx : 0 < x) (h : HasRealEigen W x) :
 145    charAnomaly W = Cost.Jcost x := by
 146  unfold charAnomaly Cost.Jcost
 147  rw [balanced_trace hdet (ne_of_gt hx) h]
 148
 149/-! ## Non-vacuity and the balance-reciprocity reading -/
 150
 151/-- Non-vacuity WITNESS ONLY (this is not the construction, per the circularity
 152fence): the hyperbolic transfer `diag(x, x⁻¹)` is balanced and delivers `x`. It
 153shows the structure is inhabited for every ratio; the physical claim is that the
 154SEAM's transfer inhabits it, which stays the named premise below. -/
 155noncomputable def hyperbolicWitness (x : ℝ) : Matrix (Fin 2) (Fin 2) ℝ :=
 156  !![x, 0; 0, x⁻¹]
 157
 158theorem hyperbolicWitness_det (x : ℝ) (hx : x ≠ 0) :
 159    (hyperbolicWitness x).det = 1 := by
 160  unfold hyperbolicWitness
 161  rw [Matrix.det_fin_two_of]
 162  simp [mul_inv_cancel₀ hx]
 163
 164theorem hyperbolicWitness_eigen (x : ℝ) :
 165    HasRealEigen (hyperbolicWitness x) x := by
 166  refine ⟨![1, 0], ?_, ?_⟩
 167  · intro h
 168    have := congrFun h 0
 169    simp at this
 170  · funext i
 171    fin_cases i <;>
 172      simp [hyperbolicWitness, Matrix.mulVec, dotProduct, Fin.sum_univ_two]
 173
 174/-- **Balance = double-entry reciprocity, read on diagonal transfers:** the credit
 175leg is the reciprocal of the debit leg EXACTLY when the transfer is balanced. This
 176is what `det = 1` means on the ledger: the two columns of one posting multiply to
 177the identity. -/
 178theorem diag_balanced_iff (a b : ℝ) :
 179    (!![a, 0; 0, b] : Matrix (Fin 2) (Fin 2) ℝ).det = 1 ↔ a * b = 1 := by
 180  rw [Matrix.det_fin_two_of]
 181  constructor <;> intro h <;> linarith
 182
 183/-! ## The elliptic retrodiction: the phase branch was the wrong conjugacy class -/
 184
 185/-- The rotation transfer (the elliptic class): the closure holonomy of the TIME
 186direction, which closes, as opposed to the mismatch direction, which stretches. -/
 187noncomputable def rotation (θ : ℝ) : Matrix (Fin 2) (Fin 2) ℝ :=
 188  !![Real.cos θ, -Real.sin θ; Real.sin θ, Real.cos θ]
 189
 190theorem rotation_det (θ : ℝ) : (rotation θ).det = 1 := by
 191  unfold rotation
 192  rw [Matrix.det_fin_two_of]
 193  nlinarith [Real.sin_sq_add_cos_sq θ]
 194
 195/-- **The kernel's phase-branch poison IS the elliptic character (THEOREM).** The
 196character anomaly of the rotation transfer equals `phaseCost` — the exact object
 197`TurnRatioCarrier` proved sign-dead (`phaseCost_nonpos`) and lattice-blind
 198(`phaseCost_vanishes_on_covers`). The earlier dead end is retrodicted: it computed
 199the right invariant of the WRONG conjugacy class. -/
 200theorem charAnomaly_rotation (θ : ℝ) :
 201    charAnomaly (rotation θ) = TurnRatioCarrier.phaseCost θ := by
 202  unfold charAnomaly rotation
 203  rw [Matrix.trace_fin_two_of, TurnRatioCarrier.phaseCost_eq]
 204  ring
 205
 206/-- **The elliptic class cannot carry a mismatch (THEOREM).** A rotation admits no
 207real eigenvalue besides ±1: `(x − cos θ)² = cos²θ − 1 ≤ 0` forces `x = cos θ = ±1`.
 208So no genuine ratio `x > 0, x ≠ 1` lives on the elliptic branch; pricing mismatches
 209there was structurally impossible, not merely unlucky. -/
 210theorem elliptic_no_real_mismatch {θ x : ℝ}
 211    (h : HasRealEigen (rotation θ) x) : x = 1 ∨ x = -1 := by
 212  have hchar := eigen_char h
 213  rw [rotation_det] at hchar
 214  have htr : (rotation θ).trace = 2 * Real.cos θ := by
 215    unfold rotation
 216    rw [Matrix.trace_fin_two_of]
 217    ring
 218  rw [htr] at hchar
 219  have hsq : (x - Real.cos θ) ^ 2 = Real.cos θ ^ 2 - 1 := by nlinarith
 220  have hcos1 : Real.cos θ ^ 2 ≤ 1 := by
 221    nlinarith [Real.neg_one_le_cos θ, Real.cos_le_one θ]
 222  have hz1 : (x - Real.cos θ) ^ 2 = 0 := by
 223    nlinarith [sq_nonneg (x - Real.cos θ)]
 224  have hz2 : Real.cos θ ^ 2 = 1 := by nlinarith [sq_nonneg (x - Real.cos θ)]
 225  have hxcos : x = Real.cos θ := by nlinarith [hz1]
 226  have hfac : (Real.cos θ - 1) * (Real.cos θ + 1) = 0 := by nlinarith [hz2]
 227  rcases mul_eq_zero.mp hfac with h1 | h1
 228  · left; rw [hxcos]; linarith
 229  · right; rw [hxcos]; linarith
 230
 231/-! ## Balance discharged: pairing preservation IS unimodularity (Sp(2,ℝ) = SL(2,ℝ)) -/
 232
 233/-- The double-entry pairing form on the 2-dimensional pair fiber: the signed area
 234of the (debit, credit) parallelogram. This is the ledger's conservation object: a
 235posting and its counter-posting span an oriented area, and double-entry says one
 236closure cannot create or destroy it. -/
 237def pairForm (u v : Fin 2 → ℝ) : ℝ := u 0 * v 1 - u 1 * v 0
 238
 239/-- A linear transfer scales the pairing form by exactly its determinant (the 2d
 240symplectic identity). -/
 241lemma pairForm_map (W : Matrix (Fin 2) (Fin 2) ℝ) (u v : Fin 2 → ℝ) :
 242    pairForm (W.mulVec u) (W.mulVec v) = W.det * pairForm u v := by
 243  unfold pairForm
 244  simp [Matrix.mulVec, dotProduct, Fin.sum_univ_two, Matrix.det_fin_two]
 245  ring
 246
 247/-- **Sp(2, ℝ) = SL(2, ℝ): the balance premise discharged (THEOREM).** A transfer
 248on the pair fiber preserves the double-entry pairing form IF AND ONLY IF it is
 249unimodular. `det = 1` is therefore not a structural assumption about the seam: it
 250is double-entry conservation restated. The panel's "why SL(2)?" question is closed
 251by this equivalence: a pairing-preserving flow on a 2d real fiber has nowhere else
 252to live. -/
 253theorem preserves_pairForm_iff_det_one (W : Matrix (Fin 2) (Fin 2) ℝ) :
 254    (∀ u v, pairForm (W.mulVec u) (W.mulVec v) = pairForm u v) ↔ W.det = 1 := by
 255  constructor
 256  · intro h
 257    have h01 := h ![1, 0] ![0, 1]
 258    rw [pairForm_map] at h01
 259    have hbase : pairForm ![1, 0] ![0, 1] = 1 := by
 260      unfold pairForm; simp
 261    rw [hbase, mul_one] at h01
 262    exact h01
 263  · intro h u v
 264    rw [pairForm_map, h, one_mul]
 265
 266/-- **Reciprocity is orientation-blindness (THEOREM).** For a balanced transfer,
 267the trace of the inverse equals the trace: the unoriented invariant of one closure
 268cannot distinguish over-posting by `x` from under-posting by `x⁻¹`. This is the T5
 269reciprocal-symmetry hypothesis supplied by the ledger's column-swap symmetry, as a
 270matrix identity. -/
 271theorem trace_inv_eq_of_det_one {W V : Matrix (Fin 2) (Fin 2) ℝ}
 272    (hdet : W.det = 1) (hWV : W * V = 1) : V.trace = W.trace := by
 273  have hadj : W * W.adjugate = 1 := by
 274    rw [Matrix.mul_adjugate, hdet, one_smul]
 275  have hVW : V * W = 1 := Matrix.mul_eq_one_comm.mp hWV
 276  have hV : V = W.adjugate := by
 277    calc V = V * (W * W.adjugate) := by rw [hadj, mul_one]
 278      _ = (V * W) * W.adjugate := by rw [mul_assoc]
 279      _ = W.adjugate := by rw [hVW, one_mul]
 280  rw [hV, Matrix.adjugate_fin_two, Matrix.trace_fin_two_of, Matrix.trace_fin_two]
 281  ring
 282
 283/-! ## The reduction: CensusPricing from the structural transfer premise -/
 284
 285/-- **The typed structural premise replacing `CensusPricing` (MODEL until derived).**
 286For each `(κ, T)` the seam delivers a BALANCED transfer on its 2-dimensional
 287double-entry pair fiber whose delivered leg scales by the turn ratio, and the
 288physical per-cycle cost is that transfer's character anomaly. Four checkable
 289structural facts — 2d fiber, unit determinant (= double-entry conservation),
 290delivered-leg eigenvalue (= what "mismatch ratio" means), trace reading (= the
 291unique conjugation-invariant scalar) — and NONE of them names J. -/
 292def SeamTransferPricing (C : ℝ → ℝ → ℝ) : Prop :=
 293  ∀ kappa T : ℝ, 0 < kappa → 0 < T →
 294    ∃ W : Matrix (Fin 2) (Fin 2) ℝ,
 295      W.det = 1 ∧
 296      HasRealEigen W (TurnRatioCarrier.turnRatio kappa T) ∧
 297      C kappa T = charAnomaly W
 298
 299/-- **The reduction theorem (THEOREM).** Any cost functional priced by a balanced
 300seam transfer satisfies `CensusPricing`: the pricing premise that named J is now
 301DOWNSTREAM of a premise that does not. Composing with
 302`TurnRatioCarrier.b2_unique_zero_of_censusPricing`, the deficit-free period
 303`β = 2π/κ` is the unique zero of any such functional. -/
 304theorem censusPricing_of_seamTransfer (C : ℝ → ℝ → ℝ)
 305    (h : SeamTransferPricing C) : TurnRatioCarrier.CensusPricing C := by
 306  intro kappa T hk hT
 307  obtain ⟨W, hdet, heig, hC⟩ := h kappa T hk hT
 308  rw [hC]
 309  exact charAnomaly_eq_J hdet (TurnRatioCarrier.turnRatio_pos hk hT) heig
 310
 311/-- Non-vacuity of the premise: the turn-ratio cost itself is transfer-priced (by
 312the hyperbolic witness). Existence check only; the physical identification of the
 313SEAM's transfer stays open. -/
 314theorem seamTransferPricing_turnRatioCost :
 315    SeamTransferPricing TurnRatioCarrier.turnRatioCost := by
 316  intro kappa T hk hT
 317  have hx : 0 < TurnRatioCarrier.turnRatio kappa T :=
 318    TurnRatioCarrier.turnRatio_pos hk hT
 319  refine ⟨hyperbolicWitness (TurnRatioCarrier.turnRatio kappa T),
 320    hyperbolicWitness_det _ (ne_of_gt hx), hyperbolicWitness_eigen _, ?_⟩
 321  rw [charAnomaly_eq_J (hyperbolicWitness_det _ (ne_of_gt hx)) hx
 322    (hyperbolicWitness_eigen _)]
 323  rfl
 324
 325/-- **B2 through the reduction (THEOREM):** for any transfer-priced cost functional,
 326the deficit-free period is the unique zero. The full composition, stated once. -/
 327theorem b2_unique_zero_of_seamTransfer (C : ℝ → ℝ → ℝ)
 328    (h : SeamTransferPricing C) (kappa T : ℝ) (hk : 0 < kappa) (hT : 0 < T) :
 329    C kappa T = 0 ↔ T = DeficitFreePeriod.euclideanPeriod kappa :=
 330  TurnRatioCarrier.b2_unique_zero_of_censusPricing C
 331    (censusPricing_of_seamTransfer C h) kappa T hk hT
 332
 333/-! ## The premise in pure ledger language: conservation, not determinant -/
 334
 335/-- **The premise with the determinant translated away (MODEL until derived).** The
 336seam's per-cycle transfer CONSERVES the double-entry pairing form (the ledger
 337conservation statement, no matrix invariant named), some fiber leg scales by the
 338turn ratio (what "delivered/required mismatch `x`" means), and the physical cost is
 339the transfer's character anomaly. Via `preserves_pairForm_iff_det_one` this implies
 340`SeamTransferPricing`, hence `CensusPricing`, hence B2. Every conjunct is now a
 341LEDGER sentence: conservation, delivery, invariant reading. -/
 342def ConservingSeamPricing (C : ℝ → ℝ → ℝ) : Prop :=
 343  ∀ kappa T : ℝ, 0 < kappa → 0 < T →
 344    ∃ W : Matrix (Fin 2) (Fin 2) ℝ,
 345      (∀ u v, pairForm (W.mulVec u) (W.mulVec v) = pairForm u v) ∧
 346      HasRealEigen W (TurnRatioCarrier.turnRatio kappa T) ∧
 347      C kappa T = charAnomaly W
 348
 349/-- Conservation pricing is transfer pricing (`Sp(2) = SL(2)` applied). -/
 350theorem seamTransferPricing_of_conserving (C : ℝ → ℝ → ℝ)
 351    (h : ConservingSeamPricing C) : SeamTransferPricing C := by
 352  intro kappa T hk hT
 353  obtain ⟨W, hcons, heig, hC⟩ := h kappa T hk hT
 354  exact ⟨W, (preserves_pairForm_iff_det_one W).mp hcons, heig, hC⟩
 355
 356/-- **The full Phase-B chain, stated once (THEOREM):** a pairing-CONSERVING seam
 357transfer delivering the turn ratio prices the census by J, and the deficit-free
 358period `β = 2π/κ` is its unique zero. From ledger conservation to the B2 discharge
 359with no J, no cosh, no determinant, and no diagonal form anywhere in the premise. -/
 360theorem b2_unique_zero_of_conserving (C : ℝ → ℝ → ℝ)
 361    (h : ConservingSeamPricing C) (kappa T : ℝ) (hk : 0 < kappa) (hT : 0 < T) :
 362    C kappa T = 0 ↔ T = DeficitFreePeriod.euclideanPeriod kappa :=
 363  b2_unique_zero_of_seamTransfer C (seamTransferPricing_of_conserving C h) kappa T hk hT
 364
 365/-! ## The falsifier, made numeric (panel Live Bet 2): 8/3 confirms J, 2 kills it -/
 366
 367/-- **The double-entry pairing identity (THEOREM).** `J(x) = (x−1)(1−x⁻¹)/2`: the T5
 368cost is EXACTLY the pairing of the two one-sided relative imbalances of a mismatch
 369(debit-side surplus `x − 1` against credit-side surplus `1 − x⁻¹`), halved for
 370once-per-event posting. This is the ledger reading of J: not an exotic functional,
 371the product of the two column discrepancies any double-entry audit already records. -/
 372theorem Jcost_pairing (x : ℝ) (hx : x ≠ 0) :
 373    Cost.Jcost x = (x - 1) * (1 - x⁻¹) / 2 := by
 374  unfold Cost.Jcost
 375  field_simp
 376  ring
 377
 378/-- The two landed census observables of the n-fold retrace pair to exactly `J(n)`:
 379absolute surplus `n − 1` (posts per sector beyond the census requirement) times
 380relative surplus `(n−1)/n` (excess per delivered post), halved. -/
 381theorem surplus_pairing_eq_J (n : ℕ) (hn : 1 ≤ n) :
 382    ((n : ℝ) - 1) * (((n : ℝ) - 1) / n) / 2 = Cost.Jcost n := by
 383  have hn0 : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
 384  rw [Jcost_pairing _ hn0]
 385  field_simp
 386
 387/-- `J(2) = 1/4` (the double cover). -/
 388theorem Jcost_two : Cost.Jcost 2 = 1 / 4 := by
 389  unfold Cost.Jcost
 390  norm_num
 391
 392/-- `J(3) = 2/3` (the triple cover). -/
 393theorem Jcost_three : Cost.Jcost 3 = 2 / 3 := by
 394  unfold Cost.Jcost
 395  norm_num
 396
 397/-- **The trace-carrier signature: `J(3)/J(2) = 8/3` (THEOREM).** -/
 398theorem cover_cost_ratio_eq : Cost.Jcost 3 / Cost.Jcost 2 = 8 / 3 := by
 399  rw [Jcost_two, Jcost_three]
 400  norm_num
 401
 402/-- **The falsifier record (THEOREM): pairing pricing and linear pricing are
 403distinguished at the triple cover.** Linear (single-column surplus) pricing gives
 404cost ratio `(3−1)/(2−1) = 2`; the double-entry pairing gives `8/3`. A measured or
 405derived seam pricing of the triple retrace at ratio 2 KILLS the trace carrier; 8/3
 406is its confirmation. The two hypotheses are not observationally equivalent. -/
 407theorem pricing_discriminated :
 408    Cost.Jcost 3 / Cost.Jcost 2 ≠ (((3 : ℝ) - 1) / ((2 : ℝ) - 1)) := by
 409  rw [cover_cost_ratio_eq]
 410  norm_num
 411
 412open TurnRatioCarrier EightTickSubperiodExclusion in
 413/-- **The triple retrace census record (THEOREM, kernel `decide`).** The 3-fold
 414retrace of the witness 8-walk (a closed 24-walk) is census-complete and posts each
 415admissible sector EXACTLY 3 times: absolute surplus 2 per sector, relative surplus
 4162/3 per post — the two factors whose pairing is `J(3) = 2/3`
 417(`surplus_pairing_eq_J`). Extends the n = 2 record of
 418`TurnRatioCarrier.eight_tick_multiple_exclusion` to the cover that discriminates
 419the pricing laws. -/
 420theorem witnessWalk3_census :
 421    walkEnd 0 (witnessWalk ++ witnessWalk ++ witnessWalk) = 0 ∧
 422    censusComplete 0 (witnessWalk ++ witnessWalk ++ witnessWalk) = true ∧
 423    visitCount 0 (witnessWalk ++ witnessWalk ++ witnessWalk) [0] = 3 ∧
 424    visitCount 0 (witnessWalk ++ witnessWalk ++ witnessWalk) [3, 6, 12, 9] = 3 ∧
 425    visitCount 0 (witnessWalk ++ witnessWalk ++ witnessWalk) [5, 10] = 3 ∧
 426    visitCount 0 (witnessWalk ++ witnessWalk ++ witnessWalk) [15] = 3 := by
 427  decide
 428
 429/-! ## Certificate -/
 430
 431/-- Bundled certificate for the Phase-B per-closure core: balance forces the
 432reciprocal leg and the trace, the character anomaly is J, the reduction to
 433`CensusPricing` holds, the elliptic branch is retrodicted and mismatch-dead, and
 434the pricing falsifier is discriminating. All fields unconditional THEOREMs; the
 435structural premise (`SeamTransferPricing` for the PHYSICAL seam) is consumed only
 436by the reduction theorem, stated separately. -/
 437structure SeamTransferCoreCert : Prop where
 438  conjugate_forced : ∀ (W : Matrix (Fin 2) (Fin 2) ℝ) (x : ℝ),
 439    W.det = 1 → x ≠ 0 → HasRealEigen W x → HasRealEigen W x⁻¹
 440  anomaly_is_J : ∀ (W : Matrix (Fin 2) (Fin 2) ℝ) (x : ℝ),
 441    W.det = 1 → 0 < x → HasRealEigen W x → charAnomaly W = Cost.Jcost x
 442  reduction : ∀ C : ℝ → ℝ → ℝ,
 443    SeamTransferPricing C → TurnRatioCarrier.CensusPricing C
 444  elliptic_is_phaseCost : ∀ θ : ℝ,
 445    charAnomaly (rotation θ) = TurnRatioCarrier.phaseCost θ
 446  elliptic_mismatch_dead : ∀ θ x : ℝ,
 447    HasRealEigen (rotation θ) x → x = 1 ∨ x = -1
 448  pairing_identity : ∀ x : ℝ, x ≠ 0 → Cost.Jcost x = (x - 1) * (1 - x⁻¹) / 2
 449  falsifier_discriminates :
 450    Cost.Jcost 3 / Cost.Jcost 2 ≠ (((3 : ℝ) - 1) / ((2 : ℝ) - 1))
 451  balance_is_conservation : ∀ W : Matrix (Fin 2) (Fin 2) ℝ,
 452    (∀ u v, pairForm (W.mulVec u) (W.mulVec v) = pairForm u v) ↔ W.det = 1
 453  reciprocity_forced : ∀ W V : Matrix (Fin 2) (Fin 2) ℝ,
 454    W.det = 1 → W * V = 1 → V.trace = W.trace
 455
 456/-- The certificate holds. -/
 457theorem seamTransferCoreCert : SeamTransferCoreCert where
 458  conjugate_forced := fun _ _ hdet hx h => balanced_conjugate hdet hx h
 459  anomaly_is_J := fun _ _ hdet hx h => charAnomaly_eq_J hdet hx h
 460  reduction := censusPricing_of_seamTransfer
 461  elliptic_is_phaseCost := charAnomaly_rotation
 462  elliptic_mismatch_dead := fun _ _ h => elliptic_no_real_mismatch h
 463  pairing_identity := Jcost_pairing
 464  falsifier_discriminates := pricing_discriminated
 465  balance_is_conservation := preserves_pairForm_iff_det_one
 466  reciprocity_forced := fun _ _ hdet hWV => trace_inv_eq_of_det_one hdet hWV
 467
 468end SeamTransferCore
 469end Holography
 470end IndisputableMonolith
 471