IndisputableMonolith.Holography.TurnRatioCarrier

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.Holography.DeficitFreePeriod
   4import IndisputableMonolith.Holography.EightTickSubperiodExclusion
   5
   6/-!
   7# TurnRatioCarrier: the B2 core priced on the real turn ratio (LEG-B)
   8
   9**Panel decision 2026-07-04** (`state/panel/bekenstein_legb_20260704_20260704_142417.json`,
  10plan `plans/Bekenstein_LEGB_Loop_And_Derivation_Plan_20260704.html`): price the per-cycle
  11recognition cost of the continued 8-tick cycle as `J` of the REAL TURN RATIO
  12
  13  `C(T) = J(κT / 2π)`,   `J(x) = (x + x⁻¹)/2 − 1`  (T5, `Cost.Jcost`),
  14
  15not as any extension of `J` to the returned U(1) phase. The ratio carrier applies T5 on
  16`ℝ₊` where it is a THEOREM (`Cost.Jcost_eq_zero_iff`), and in one inequality it sees the
  17deficit (`x < 1`), the excess (`x > 1`), and every `n`-sheeted cover
  18(`J(n) = (n−1)²/(2n) > 0` for `n ≥ 2`). Consequences landed here:
  19
  201. **Unique zero-cost period (THEOREM).** `C(T) = 0 ↔ T = 2π/κ` for `κ, T > 0`
  21   (`turnRatioCost_eq_zero_iff`): the deficit-free period is not merely the MINIMAL
  22   positive closure time (`DeficitFreePeriod.euclideanPeriod_isLeast`) but the UNIQUE
  23   zero of the per-cycle cost. Strict positivity off the period is
  24   `turnRatioCost_pos_of_ne_period`.
  252. **KMS-window discharge (THEOREM).** Every `n ≥ 2` lattice multiple (the n-sheeted
  26   Euclidean cover, angle `2πn`) carries strictly positive cost
  27   (`turnRatioCost_cover_pos`, value `Jcost_cover_value`), so zero-cost closure forces
  28   `n = 1` (`lattice_period_zero_cost_iff`) with NO window hypothesis. This retires the
  29   `legb_kms_window_unique` window premise on the cost side.
  303. **Phase-branch poison lemma (THEOREM).** The J-FORMULA applied verbatim to the
  31   returned unit phase gives `cos δ − 1 ≤ 0` (`phaseCost_nonpos`): never strictly
  32   positive, so it cannot penalize any deficit, and it vanishes on EVERY cover
  33   (`phaseCost_vanishes_on_covers`), so it can never single out `n = 1`. The phase
  34   branch is dead in-kernel. (Distinct object from `DeficitFreePeriod.deficitCost
  35   = 1 − cos δ`, the chord form, which is nonneg but equally lattice-blind at covers.)
  364. **U(1)-extension underdetermination (THEOREM).** Two extensions of `J` to `ℂ`
  37   (`Jprime`, `Jsecond`) that AGREE with `Cost.Jcost` on `ℝ₊` yet differ at `I`, one of
  38   which vanishes at `I ≠ 1` (`u1_extension_zero_set_not_forced`): the kernel record
  39   that "extend J off the reals" is a CHOICE, not a forced object, killing the
  40   extend-J-to-U(1) route to B2.
  415. **Flat-space limit (THEOREM).** As `κ → 0⁺` the cost of any fixed period diverges
  42   (`turnRatioCost_unbounded_near_zero_kappa`) and the forced period itself diverges
  43   (`euclideanPeriod_unbounded`): no horizon, no finite zero-cost period, no residual
  44   thermality. Accumulated cost over repeated positive-cost cycles is unbounded
  45   (`accumulatedCost_unbounded`).
  466. **Once-per-closure census record (THEOREM, by `decide`).** On the forced substrate,
  47   the witness 8-walk posts each admissible sector EXACTLY once per closure, while its
  48   `n = 2` retrace (a closed 16-walk) is census-complete but DOUBLE-POSTS every sector
  49   (`eight_tick_multiple_exclusion`). This is the discrete once-per-closure content the
  50   `CensusPricing` premise prices; it also records that
  51   `EightTickSubperiodExclusion` alone (proper divisors {1,2,4}) does NOT exclude
  52   multiples: the multiple side is a posting-discipline fact, not a census-absence fact.
  53
  54## The honest residual (do not overclaim)
  55
  56The ONE remaining physics premise is `CensusPricing`: the fixed-point per-cycle cost of
  57the continued cycle IS `J` of the delivered/required closure ratio, posted once per
  58closure. Given it, B2 discharges carrier-agnostically
  59(`b2_unique_zero_of_censusPricing`). Until `CensusPricing` is derived from the seam
  60ledger, consumers are FORCED-CONDITIONAL on this one named premise (tag per `soul.mdc`:
  61the weakest link sets the tag). Its under-posting half is the landed
  62`EightTickSubperiodExclusion`; its over-posting half is the double-posting record here.
  63-/
  64
  65namespace IndisputableMonolith
  66namespace Holography
  67namespace TurnRatioCarrier
  68
  69open Complex
  70
  71/-! ## The carrier: the real turn ratio and its J-cost -/
  72
  73/-- The turn ratio: the fraction of one full turn the continued clock at rate `κ`
  74sweeps in Euclidean time `T`. The `2π` is the full-turn angle (kernel of
  75`Complex.exp`, `DeficitFreePeriod.holonomy_eq_one_iff_lattice`), not a temperature. -/
  76noncomputable def turnRatio (kappa T : ℝ) : ℝ :=
  77  kappa * T / (2 * Real.pi)
  78
  79/-- The per-cycle recognition cost priced on the turn ratio: `C(T) = J(κT/2π)` with
  80`J` the unique T5 cost (`Cost.Jcost`). -/
  81noncomputable def turnRatioCost (kappa T : ℝ) : ℝ :=
  82  Cost.Jcost (turnRatio kappa T)
  83
  84theorem turnRatio_pos {kappa T : ℝ} (hk : 0 < kappa) (hT : 0 < T) :
  85    0 < turnRatio kappa T := by
  86  unfold turnRatio
  87  positivity
  88
  89/-- The turn ratio is `1` exactly at the deficit-free period `T = 2π/κ`. -/
  90theorem turnRatio_eq_one_iff (kappa T : ℝ) (hk : 0 < kappa) :
  91    turnRatio kappa T = 1 ↔ T = DeficitFreePeriod.euclideanPeriod kappa := by
  92  have hpi : (0 : ℝ) < Real.pi := Real.pi_pos
  93  have hk0 : kappa ≠ 0 := ne_of_gt hk
  94  unfold turnRatio DeficitFreePeriod.euclideanPeriod
  95  rw [div_eq_one_iff_eq (by positivity), eq_div_iff hk0]
  96  constructor
  97  · intro h; linarith
  98  · intro h; linarith
  99
 100/-- The cost is nonnegative for positive rate and period (T5 AM-GM,
 101`Cost.Jcost_nonneg`). -/
 102theorem turnRatioCost_nonneg {kappa T : ℝ} (hk : 0 < kappa) (hT : 0 < T) :
 103    0 ≤ turnRatioCost kappa T :=
 104  Cost.Jcost_nonneg (turnRatio_pos hk hT)
 105
 106/-- **Headline (B2 math half): the deficit-free period is the UNIQUE zero of the
 107per-cycle cost.** `C(T) = 0 ↔ T = 2π/κ`. Strictly stronger than minimality
 108(`DeficitFreePeriod.euclideanPeriod_isLeast`): no other positive period, lattice or
 109not, deficit or excess, has zero cost. Pure T5 (`Cost.Jcost_eq_zero_iff`). -/
 110theorem turnRatioCost_eq_zero_iff (kappa T : ℝ) (hk : 0 < kappa) (hT : 0 < T) :
 111    turnRatioCost kappa T = 0 ↔ T = DeficitFreePeriod.euclideanPeriod kappa := by
 112  unfold turnRatioCost
 113  rw [Cost.Jcost_eq_zero_iff _ (turnRatio_pos hk hT)]
 114  exact turnRatio_eq_one_iff kappa T hk
 115
 116/-- Strict positivity off the deficit-free period: any other positive period, deficit
 117or excess, costs strictly positive recognition per cycle. -/
 118theorem turnRatioCost_pos_of_ne_period (kappa T : ℝ) (hk : 0 < kappa) (hT : 0 < T)
 119    (hne : T ≠ DeficitFreePeriod.euclideanPeriod kappa) :
 120    0 < turnRatioCost kappa T := by
 121  rcases lt_or_eq_of_le (turnRatioCost_nonneg hk hT) with hpos | heq
 122  · exact hpos
 123  · exact absurd ((turnRatioCost_eq_zero_iff kappa T hk hT).mp heq.symm) hne
 124
 125/-- T5 reciprocity on the carrier: a deficit (ratio `x`) and its reciprocal excess
 126(ratio `1/x`) cost the same (`Cost.Jcost_symm`). -/
 127theorem turnRatioCost_reciprocal (kappa T : ℝ) (hk : 0 < kappa) (hT : 0 < T) :
 128    Cost.Jcost (turnRatio kappa T) = Cost.Jcost (turnRatio kappa T)⁻¹ :=
 129  Cost.Jcost_symm (turnRatio_pos hk hT)
 130
 131/-! ## The n-sheeted covers: positive cost, KMS window discharged -/
 132
 133/-- The turn ratio of the `n`-fold cover of the deficit-free period is exactly `n`. -/
 134theorem turnRatio_cover (kappa : ℝ) (hk : 0 < kappa) (n : ℕ) :
 135    turnRatio kappa (n * DeficitFreePeriod.euclideanPeriod kappa) = n := by
 136  have hpi : Real.pi ≠ 0 := ne_of_gt Real.pi_pos
 137  have hk0 : kappa ≠ 0 := ne_of_gt hk
 138  unfold turnRatio DeficitFreePeriod.euclideanPeriod
 139  field_simp
 140
 141/-- The panel's cover-cost value: `J(n) = (n−1)²/(2n)` (from `Cost.Jcost_eq_sq`). -/
 142theorem Jcost_cover_value (n : ℕ) (hn : 1 ≤ n) :
 143    Cost.Jcost (n : ℝ) = ((n : ℝ) - 1) ^ 2 / (2 * n) := by
 144  have hn0 : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
 145  exact Cost.Jcost_eq_sq hn0
 146
 147/-- **KMS-window discharge, positivity half:** every `n ≥ 2` sheeted cover (Euclidean
 148angle `2πn`) carries strictly positive per-cycle cost. The excess-angle branch is
 149cost-excluded by the same T5 inequality as the deficit branch. -/
 150theorem turnRatioCost_cover_pos (kappa : ℝ) (hk : 0 < kappa) (n : ℕ) (hn : 2 ≤ n) :
 151    0 < turnRatioCost kappa (n * DeficitFreePeriod.euclideanPeriod kappa) := by
 152  unfold turnRatioCost
 153  rw [turnRatio_cover kappa hk n]
 154  have hpos : (0 : ℝ) < n := by exact_mod_cast Nat.lt_of_lt_of_le Nat.zero_lt_two hn
 155  have hne : (n : ℝ) ≠ 1 := by
 156    have : (1 : ℝ) < n := by exact_mod_cast Nat.lt_of_lt_of_le Nat.one_lt_two hn
 157    exact ne_of_gt this
 158  exact Cost.Jcost_pos_of_ne_one _ hpos hne
 159
 160/-- **KMS-window discharge, uniqueness form:** among ALL lattice periods
 161`T = n·(2π/κ)` (`n ≥ 1`), zero cost holds exactly at `n = 1`. No window hypothesis
 162`β < 2·(2π/κ)` is needed: the cost functional itself excludes every multiple. -/
 163theorem lattice_period_zero_cost_iff (kappa : ℝ) (hk : 0 < kappa) (n : ℕ) (hn : 1 ≤ n) :
 164    turnRatioCost kappa (n * DeficitFreePeriod.euclideanPeriod kappa) = 0 ↔ n = 1 := by
 165  have hpos : (0 : ℝ) < n := by
 166    have hn' : 0 < n := by omega
 167    exact_mod_cast hn'
 168  unfold turnRatioCost
 169  rw [turnRatio_cover kappa hk n, Cost.Jcost_eq_zero_iff _ hpos]
 170  exact_mod_cast Nat.cast_eq_one (R := ℝ)
 171
 172/-! ## The phase branch is poison: sign-dead and lattice-blind -/
 173
 174/-- The J-FORMULA applied verbatim to the returned unit phase `exp(iδ)` (real part
 175reading). This is the object the derive captain kept reaching for; the next two
 176theorems record in-kernel why it can never work. -/
 177noncomputable def phaseCost (δ : ℝ) : ℝ :=
 178  ((Complex.exp (δ * Complex.I) + (Complex.exp (δ * Complex.I))⁻¹) / 2 - 1).re
 179
 180/-- The phase-branch cost evaluates to `cos δ − 1`. -/
 181theorem phaseCost_eq (δ : ℝ) : phaseCost δ = Real.cos δ - 1 := by
 182  unfold phaseCost
 183  rw [← Complex.exp_neg, ← neg_mul, Complex.exp_mul_I, Complex.exp_mul_I,
 184    Complex.cos_neg, Complex.sin_neg]
 185  have h : (Complex.cos δ + Complex.sin δ * Complex.I +
 186      (Complex.cos δ + -Complex.sin δ * Complex.I)) / 2 - 1 = Complex.cos δ - 1 := by
 187    ring
 188  rw [h, Complex.sub_re, Complex.cos_ofReal_re, Complex.one_re]
 189
 190/-- **Poison lemma (sign death):** the phase-branch cost is NEVER strictly positive,
 191so it cannot penalize any deficit. The phase branch cannot force the period. -/
 192theorem phaseCost_nonpos (δ : ℝ) : phaseCost δ ≤ 0 := by
 193  rw [phaseCost_eq]
 194  linarith [Real.cos_le_one δ]
 195
 196/-- **Poison lemma (lattice blindness):** the phase-branch cost vanishes on EVERY
 197`n`-sheeted cover, so it can never single out `n = 1`. Contrast
 198`turnRatioCost_cover_pos`. -/
 199theorem phaseCost_vanishes_on_covers (n : ℤ) : phaseCost ((n : ℝ) * (2 * Real.pi)) = 0 := by
 200  rw [phaseCost_eq, Real.cos_int_mul_two_pi]
 201  ring
 202
 203/-! ## The U(1) extension of J is a choice: two agreeing extensions that disagree -/
 204
 205/-- The naive real-part extension of the J-formula to `ℂ`. -/
 206noncomputable def JextRe (z : ℂ) : ℝ := ((z + z⁻¹) / 2 - 1).re
 207
 208/-- `JextRe` agrees with the T5 cost on the reals. -/
 209theorem JextRe_agrees (x : ℝ) : JextRe (x : ℂ) = Cost.Jcost x := by
 210  unfold JextRe Cost.Jcost
 211  have h : ((x : ℂ) + (x : ℂ)⁻¹) / 2 - 1 = ((x + x⁻¹) / 2 - 1 : ℝ) := by
 212    push_cast
 213    ring
 214  rw [h, Complex.ofReal_re]
 215
 216/-- First counterexample extension: agrees with `J` on `ℝ` (where `im = 0`), differs
 217off it. -/
 218noncomputable def Jprime (z : ℂ) : ℝ := (1 + z.im ^ 2) * JextRe z
 219
 220/-- Second counterexample extension: also agrees with `J` on `ℝ₊`, also differs off
 221it, and has a DIFFERENT zero set. -/
 222noncomputable def Jsecond (z : ℂ) : ℝ := (z.re ^ 2 / Complex.normSq z) * JextRe z
 223
 224theorem Jprime_agrees (x : ℝ) : Jprime (x : ℂ) = Cost.Jcost x := by
 225  unfold Jprime
 226  rw [JextRe_agrees]
 227  simp
 228
 229theorem Jsecond_agrees (x : ℝ) (hx : 0 < x) : Jsecond (x : ℂ) = Cost.Jcost x := by
 230  have hx0 : x ≠ 0 := ne_of_gt hx
 231  unfold Jsecond
 232  rw [JextRe_agrees]
 233  rw [Complex.normSq_ofReal, Complex.ofReal_re]
 234  have h1 : x ^ 2 / (x * x) = 1 := by
 235    field_simp
 236  rw [h1, one_mul]
 237
 238theorem JextRe_I : JextRe Complex.I = -1 := by
 239  unfold JextRe
 240  rw [Complex.inv_I]
 241  simp
 242
 243theorem Jprime_I : Jprime Complex.I = -2 := by
 244  unfold Jprime
 245  rw [JextRe_I]
 246  norm_num [Complex.I_im]
 247
 248theorem Jsecond_I : Jsecond Complex.I = 0 := by
 249  unfold Jsecond
 250  simp [Complex.I_re]
 251
 252/-- **Kernel record: the U(1)/ℂ extension of `J` is underdetermined.** Two extensions
 253agree with `Cost.Jcost` on all of `ℝ₊` yet disagree at `I`. Any argument that "extends
 254J to the phase and reads off the period" is choosing its conclusion. -/
 255theorem u1_extension_not_unique :
 256    ∃ J₁ J₂ : ℂ → ℝ,
 257      (∀ x : ℝ, 0 < x → J₁ (x : ℂ) = Cost.Jcost x) ∧
 258      (∀ x : ℝ, 0 < x → J₂ (x : ℂ) = Cost.Jcost x) ∧
 259      ∃ z : ℂ, J₁ z ≠ J₂ z := by
 260  refine ⟨Jprime, Jsecond, fun x _ => Jprime_agrees x, fun x hx => Jsecond_agrees x hx,
 261    Complex.I, ?_⟩
 262  rw [Jprime_I, Jsecond_I]
 263  norm_num
 264
 265/-- **Kernel record: the zero set of an agreeing extension is not forced.** `Jsecond`
 266agrees with `J` on `ℝ₊` yet vanishes at `I ≠ 1`: imposing "zero iff closure" on an
 267extension ASSUMES B2's conclusion rather than deriving it. -/
 268theorem u1_extension_zero_set_not_forced :
 269    ∃ J' : ℂ → ℝ,
 270      (∀ x : ℝ, 0 < x → J' (x : ℂ) = Cost.Jcost x) ∧
 271      J' Complex.I = 0 ∧ (Complex.I : ℂ) ≠ 1 := by
 272  refine ⟨Jsecond, fun x hx => Jsecond_agrees x hx, Jsecond_I, ?_⟩
 273  intro h
 274  have := congrArg Complex.im h
 275  simp at this
 276
 277/-! ## Flat-space limit: no horizon, no finite zero-cost period, no bound -/
 278
 279/-- As `κ → 0⁺` the deficit-free period diverges: below any bound `M` there is a rate
 280threshold under which the period exceeds `M`. No finite periodicity survives in flat
 281space. -/
 282theorem euclideanPeriod_unbounded (M : ℝ) :
 283    ∃ κ₀ : ℝ, 0 < κ₀ ∧ ∀ kappa : ℝ, 0 < kappa → kappa < κ₀ →
 284      M < DeficitFreePeriod.euclideanPeriod kappa := by
 285  have hpi : (0 : ℝ) < Real.pi := Real.pi_pos
 286  have hA : (0 : ℝ) < max M 1 := lt_max_of_lt_right one_pos
 287  refine ⟨2 * Real.pi / max M 1, by positivity, ?_⟩
 288  intro kappa hk hklt
 289  unfold DeficitFreePeriod.euclideanPeriod
 290  have h1 : max M 1 < 2 * Real.pi / kappa := by
 291    rw [lt_div_iff₀ hk]
 292    calc max M 1 * kappa < max M 1 * (2 * Real.pi / max M 1) := by
 293          exact mul_lt_mul_of_pos_left hklt hA
 294      _ = 2 * Real.pi := by field_simp
 295  exact lt_of_le_of_lt (le_max_left M 1) h1
 296
 297/-- As `κ → 0⁺` the per-cycle cost of any FIXED period diverges past every bound: the
 298turn ratio collapses to `0⁺` and `J` blows up. Flat space admits no finite-cost
 299closure at any finite period; no residual thermality survives. -/
 300theorem turnRatioCost_unbounded_near_zero_kappa (T : ℝ) (hT : 0 < T) (M : ℝ) :
 301    ∃ κ₀ : ℝ, 0 < κ₀ ∧ ∀ kappa : ℝ, 0 < kappa → kappa < κ₀ →
 302      M < turnRatioCost kappa T := by
 303  have hpi : (0 : ℝ) < Real.pi := Real.pi_pos
 304  set A : ℝ := max M 0 with hA
 305  have hA0 : 0 ≤ A := le_max_right M 0
 306  have hMA : M ≤ A := le_max_left M 0
 307  have hden : (0 : ℝ) < 2 * A + 4 := by linarith
 308  refine ⟨2 * Real.pi / (T * (2 * A + 4)), by positivity, ?_⟩
 309  intro kappa hk hklt
 310  have hx : 0 < turnRatio kappa T := turnRatio_pos hk hT
 311  -- the ratio is small: x < 1/(2A+4)
 312  have hxlt : turnRatio kappa T < 1 / (2 * A + 4) := by
 313    unfold turnRatio
 314    rw [div_lt_div_iff₀ (by positivity) hden]
 315    have h1 : kappa * (T * (2 * A + 4)) < 2 * Real.pi := by
 316      have := mul_lt_mul_of_pos_right hklt (by positivity : (0:ℝ) < T * (2 * A + 4))
 317      calc kappa * (T * (2 * A + 4))
 318          < 2 * Real.pi / (T * (2 * A + 4)) * (T * (2 * A + 4)) := this
 319        _ = 2 * Real.pi := by field_simp
 320    calc kappa * T * (2 * A + 4) = kappa * (T * (2 * A + 4)) := by ring
 321      _ < 2 * Real.pi := h1
 322      _ = 1 * (2 * Real.pi) := by ring
 323  -- hence the reciprocal is large: 2A+4 < x⁻¹
 324  have hinv : 2 * A + 4 < (turnRatio kappa T)⁻¹ := by
 325    have hprod : turnRatio kappa T * (2 * A + 4) < 1 := (lt_div_iff₀ hden).mp hxlt
 326    have hxx : turnRatio kappa T * (2 * A + 4) <
 327        turnRatio kappa T * (turnRatio kappa T)⁻¹ := by
 328      rw [mul_inv_cancel₀ (ne_of_gt hx)]
 329      exact hprod
 330    exact lt_of_mul_lt_mul_left hxx hx.le
 331  -- and J(x) ≥ x⁻¹/2 − 1 dominates
 332  have hJ : (turnRatio kappa T)⁻¹ / 2 - 1 ≤ Cost.Jcost (turnRatio kappa T) := by
 333    unfold Cost.Jcost
 334    nlinarith [hx.le]
 335  unfold turnRatioCost
 336  nlinarith [hJ, hinv, hMA]
 337
 338/-- Accumulated cost over `N` cycles at per-cycle cost `c`. -/
 339def accumulatedCost (N : ℕ) (c : ℝ) : ℝ := N * c
 340
 341/-- Any strictly positive per-cycle cost accumulates past every bound (Archimedean):
 342a deficit or excess closure cannot persist at the fixed point. -/
 343theorem accumulatedCost_unbounded (c : ℝ) (hc : 0 < c) (B : ℝ) :
 344    ∃ N : ℕ, B < accumulatedCost N c := by
 345  obtain ⟨N, hN⟩ := exists_nat_gt (B / c)
 346  refine ⟨N, ?_⟩
 347  unfold accumulatedCost
 348  rwa [div_lt_iff₀ hc] at hN
 349
 350/-! ## Once per closure: the single cycle posts each sector once, the double cover
 351posts each twice (kernel `decide`) -/
 352
 353open EightTickSubperiodExclusion in
 354/-- How many times a walk's cycle representatives (visits minus the closing return)
 355post into a given admissible orbit. -/
 356def visitCount (s : PixelLocal.FaceCfg) (fs : List (Fin 4)) (orbit : List Nat) : ℕ :=
 357  ((walkVisits s fs).dropLast.filter (fun c => orbit.contains c.val)).length
 358
 359/-- The census witness walk of `EightTickSubperiodExclusion`
 360(`0→1→3→7→15→14→10→8→0`). -/
 361def witnessWalk : List (Fin 4) := [0, 1, 2, 3, 0, 2, 1, 3]
 362
 363open EightTickSubperiodExclusion in
 364/-- **Once-per-closure record (THEOREM, kernel `decide`).** The witness 8-walk closes
 365and posts each of the four admissible sectors EXACTLY once; its `n = 2` retrace (a
 366closed 16-walk, the discrete 2-sheeted cover) is census-complete but posts each sector
 367EXACTLY twice. The multiple branch is not a census-absence fact (the cover still sees
 368all sectors, so `EightTickSubperiodExclusion` alone cannot exclude it): it is a
 369DOUBLE-POSTING fact, which is precisely the over-posting half of the `CensusPricing`
 370premise. -/
 371theorem eight_tick_multiple_exclusion :
 372    (walkEnd 0 witnessWalk = 0 ∧
 373      visitCount 0 witnessWalk [0] = 1 ∧
 374      visitCount 0 witnessWalk [3, 6, 12, 9] = 1 ∧
 375      visitCount 0 witnessWalk [5, 10] = 1 ∧
 376      visitCount 0 witnessWalk [15] = 1) ∧
 377    (walkEnd 0 (witnessWalk ++ witnessWalk) = 0 ∧
 378      censusComplete 0 (witnessWalk ++ witnessWalk) = true ∧
 379      visitCount 0 (witnessWalk ++ witnessWalk) [0] = 2 ∧
 380      visitCount 0 (witnessWalk ++ witnessWalk) [3, 6, 12, 9] = 2 ∧
 381      visitCount 0 (witnessWalk ++ witnessWalk) [5, 10] = 2 ∧
 382      visitCount 0 (witnessWalk ++ witnessWalk) [15] = 2) := by
 383  decide
 384
 385/-! ## The named premise and the carrier-agnostic B2 discharge -/
 386
 387/-- **The one remaining physics premise (`CensusPricing` /
 388`CensusClosureNormalization`), NAMED and TYPED.** The fixed-point per-cycle
 389recognition cost of the continued cycle at rate `κ` and Euclidean period `T` is `J` of
 390the turn ratio (the delivered/required closure fraction), posted once per closure.
 391Under-posting half: `EightTickSubperiodExclusion` (proper sub-periods destroy the
 392census). Over-posting half: `eight_tick_multiple_exclusion` (covers double-post).
 393STATUS: MODEL until derived from the seam ledger; consumers of the discharge below are
 394FORCED-CONDITIONAL on it. -/
 395def CensusPricing (C : ℝ → ℝ → ℝ) : Prop :=
 396  ∀ kappa T : ℝ, 0 < kappa → 0 < T → C kappa T = Cost.Jcost (turnRatio kappa T)
 397
 398/-- The turn-ratio cost itself satisfies the pricing premise (non-vacuity witness). -/
 399theorem turnRatioCost_censusPricing : CensusPricing turnRatioCost :=
 400  fun _ _ _ _ => rfl
 401
 402/-- **B2, carrier-agnostic, discharged from the named premise.** ANY per-cycle cost
 403functional satisfying `CensusPricing` has the deficit-free period `2π/κ` as its UNIQUE
 404zero: deficits, excesses, and every `n ≥ 2` cover all cost strictly positive
 405recognition, and the cost accumulates without bound (`accumulatedCost_unbounded`).
 406FORCED-CONDITIONAL: the tag is set by the `CensusPricing` premise. -/
 407theorem b2_unique_zero_of_censusPricing (C : ℝ → ℝ → ℝ) (hC : CensusPricing C)
 408    (kappa T : ℝ) (hk : 0 < kappa) (hT : 0 < T) :
 409    C kappa T = 0 ↔ T = DeficitFreePeriod.euclideanPeriod kappa := by
 410  rw [hC kappa T hk hT]
 411  exact turnRatioCost_eq_zero_iff kappa T hk hT
 412
 413/-! ## Certificate -/
 414
 415/-- Bundled certificate for the turn-ratio carrier: unique zero at the deficit-free
 416period, strict positivity off it, positive cost on every `n ≥ 2` cover (KMS window
 417discharged without a window hypothesis), the phase branch sign-dead and lattice-blind,
 418the U(1) extension underdetermined, and the flat-space limits correct. All fields are
 419unconditional THEOREMs; the physics premise (`CensusPricing`) is consumed only by
 420`b2_unique_zero_of_censusPricing`, which is stated separately. -/
 421structure TurnRatioCarrierCert : Prop where
 422  unique_zero : ∀ kappa T : ℝ, 0 < kappa → 0 < T →
 423    (turnRatioCost kappa T = 0 ↔ T = DeficitFreePeriod.euclideanPeriod kappa)
 424  pos_off_period : ∀ kappa T : ℝ, 0 < kappa → 0 < T →
 425    T ≠ DeficitFreePeriod.euclideanPeriod kappa → 0 < turnRatioCost kappa T
 426  cover_pos : ∀ kappa : ℝ, 0 < kappa → ∀ n : ℕ, 2 ≤ n →
 427    0 < turnRatioCost kappa (n * DeficitFreePeriod.euclideanPeriod kappa)
 428  phase_dead : ∀ δ : ℝ, phaseCost δ ≤ 0
 429  phase_lattice_blind : ∀ n : ℤ, phaseCost ((n : ℝ) * (2 * Real.pi)) = 0
 430  extension_not_unique : ∃ J₁ J₂ : ℂ → ℝ,
 431    (∀ x : ℝ, 0 < x → J₁ (x : ℂ) = Cost.Jcost x) ∧
 432    (∀ x : ℝ, 0 < x → J₂ (x : ℂ) = Cost.Jcost x) ∧
 433    ∃ z : ℂ, J₁ z ≠ J₂ z
 434  flat_space_period : ∀ M : ℝ, ∃ κ₀ : ℝ, 0 < κ₀ ∧ ∀ kappa : ℝ,
 435    0 < kappa → kappa < κ₀ → M < DeficitFreePeriod.euclideanPeriod kappa
 436
 437/-- The certificate holds. -/
 438theorem turnRatioCarrierCert : TurnRatioCarrierCert where
 439  unique_zero := turnRatioCost_eq_zero_iff
 440  pos_off_period := turnRatioCost_pos_of_ne_period
 441  cover_pos := fun kappa hk n hn => turnRatioCost_cover_pos kappa hk n hn
 442  phase_dead := phaseCost_nonpos
 443  phase_lattice_blind := phaseCost_vanishes_on_covers
 444  extension_not_unique := u1_extension_not_unique
 445  flat_space_period := euclideanPeriod_unbounded
 446
 447end TurnRatioCarrier
 448end Holography
 449end IndisputableMonolith
 450