IndisputableMonolith.Holography.DeficitFreePeriod

   1import Mathlib
   2import IndisputableMonolith.Holography.KeystoneFactorThree
   3
   4/-!
   5# Deficit-Free Period: 2π/κ forced by holonomy closure (LEG-B core chain)
   6
   7**Status: THEOREM for the mathematical chain; the physics bridge carries two named
   8MODEL premises.** This module is the canonical formalization of the LEG-B derive
   9captain's accepted derivation steps (`rs-bekenstein-legb-loop` on Steve, physics-critic
  10gated; journal entries `derive_20260702_065112`, `derive_20260702_082715`,
  11`derive_20260702_090702`, all ACCEPT, zero rejections), promoting the banked scratch
  12leaves (`state/bekenstein_legb_closed/legb_exp_period_lattice.lean`,
  13`legb_clausius_to_bekenstein.lean`, `legb_eight_tick_circle_period.lean`) into one
  14auditable canonical chain.
  15
  16## The chain (what is proved here)
  17
  181. **Holonomy carrier (THEOREM, definitional + lattice).** The per-cycle phase-return
  19   map of a clocked recognition cycle at rate `κ` is `h(T) = exp(iκT)`. The return is
  20   exact (`h(T) = 1`) iff `κT ∈ 2πℤ` (`holonomy_eq_one_iff_lattice`,
  21   `holonomy_eq_one_iff`). This is the U(1) target the 8-tick clock embeds into
  22   (`legb_eight_tick_circle_period`; `EightTickSubperiodExclusion` for the discrete
  23   exclusion of subperiods).
  24
  252. **Deficit-cost functional (THEOREM).** The recognition cost of an imperfect return
  26   with phase deficit `δ` is `C(δ) = 1 − cos δ = ½‖1 − exp(iδ)‖²`
  27   (`deficitCost_eq_half_normSq`): the squared chord distance between the returned
  28   phase and perfect closure, i.e. the J-cost quadratic form on the U(1) carrier. It
  29   is nonnegative (`deficitCost_nonneg`), vanishes EXACTLY on `2πℤ`
  30   (`deficitCost_eq_zero_iff`), is strictly positive off the lattice
  31   (`deficitCost_pos_of_not_period`), and has a strict quadratic minimum at closure:
  32   critical point at 0 with second derivative `cos 0 = 1 > 0`
  33   (`deficitCost_hasDerivAt`, `deficitCost_critical_at_zero`,
  34   `deficitCost_second_deriv_pos_at_zero`).
  35
  363. **Minimal positive deficit-free period (THEOREM).** For `κ > 0` the set of
  37   positive deficit-free return times `{T > 0 | C(κT) = 0}` has LEAST element
  38   `β = 2π/κ` (`euclideanPeriod_isLeast`). This is the target the derive captain holds
  39   as `legb_minimal_positive_period`, landed here canonically. 2π is not chosen: it is
  40   the smallest positive zero of the deficit cost, which is itself the unique J-form
  41   on the forced U(1) carrier.
  42
  434. **Physics bridge (CONDITIONAL on two named MODEL premises).** With
  44   `HorizonRate κ R` (the static-horizon phase rate is `κ = 1/R`, the
  45   Schwarzschild/Rindler surface-gravity convention in the ledger normalization) and
  46   `ClausiusForm S E β` (the static-horizon entropy is the thermal `S = βE` at the
  47   Euclidean period), the deficit-free period forces
  48   `S = 2πER` (`bekenstein_saturation_from_deficit_free_period`), the exact
  49   SATURATING value of the Casini/Bekenstein form consumed by
  50   `KeystoneFactorThree` (`totalEntropyBound_saturating_case`).
  51
  52## What this does NOT close (honest boundary)
  53
  54This module derives the MAGNITUDE of the Euclidean period (2π/κ, forced) and the
  55SATURATING value `S = 2πER` for the thermal/Clausius state. It does NOT discharge
  56LEG-B proper (`KeystoneFactorThree.TotalEntropyBekensteinBound` as a bound for ALL
  57states, which is Casini's relative-entropy positivity statement) and it does not
  58derive the two MODEL premises:
  59
  60- `ClausiusForm` imports the first law / KMS-thermality of the horizon state. The
  61  captain's open target `legb_kms_window_unique` (uniqueness of the KMS analytic
  62  window) is the derivation route.
  63- `HorizonRate` imports the surface-gravity normalization `κ = 1/R`. The Live Bet 2
  64  audit (R = 2GE kernel-derivability) tracks its status; see the master plan.
  65
  66The weakest link sets the tag: consumers of the bridge theorems are CONDITIONAL.
  67The lattice/minimality chain (items 1-3) is unconditional and axiom-clean.
  68
  69Provenance: `plans/RS_Bekenstein_Quarter_Master_Plan_20260702.html` (LEG-B);
  70`glm/bekenstein_legb/DERIVATION_LOG.md`. The seam-modular verdict
  71(`SeamModularHamiltonian`) killed the classical GF(2) route to 2π, so this
  72holonomy/KMS lane is the only live route, as steered on 2026-07-02.
  73-/
  74
  75namespace IndisputableMonolith
  76namespace Holography
  77namespace DeficitFreePeriod
  78
  79open Complex
  80
  81/-- The per-cycle holonomy carrier: the phase-return map `h(T) = exp(iκT)` of a
  82clocked recognition cycle running at rate `κ` for time `T`. Accepted derive step
  83`derive_20260702_065112`: the 8-tick clock embeds in U(1) and its per-cycle return is
  84this exponential (see `legb_eight_tick_circle_period` for the discrete embedding). -/
  85noncomputable def holonomy (kappa T : ℝ) : ℂ :=
  86  Complex.exp (kappa * T * Complex.I)
  87
  88/-- The deficit-cost functional: the recognition cost of a phase deficit `δ`,
  89`C(δ) = 1 − cos δ`. Accepted derive step `derive_20260702_082715`. Equivalently the
  90squared chord distance `½‖1 − exp(iδ)‖²` (see `deficitCost_eq_half_normSq`), the
  91J-cost quadratic form on the U(1) carrier. -/
  92noncomputable def deficitCost (δ : ℝ) : ℝ :=
  93  1 - Real.cos δ
  94
  95/-- The Euclidean period forced by deficit-free closure: `β = 2π/κ`. -/
  96noncomputable def euclideanPeriod (kappa : ℝ) : ℝ :=
  97  2 * Real.pi / kappa
  98
  99/-- Named MODEL premise (Clausius form): the static-horizon entropy is the thermal
 100entropy `S = βE` at Euclidean period `β`. This is the first-law/KMS-thermality input;
 101its derivation route is the captain's open `legb_kms_window_unique` target. -/
 102def ClausiusForm (S E beta : ℝ) : Prop :=
 103  S = beta * E
 104
 105/-- Named MODEL premise (horizon rate): the static-horizon phase rate is `κ = 1/R`
 106(surface-gravity convention in the ledger normalization; Live Bet 2 tracks its
 107kernel-derivability). -/
 108def HorizonRate (kappa R : ℝ) : Prop :=
 109  kappa = 1 / R
 110
 111/-! ## The deficit-cost functional is the chord-distance J-form on U(1) -/
 112
 113/-- `C(δ) = ½‖1 − exp(iδ)‖²`: the deficit cost is exactly half the squared chord
 114distance between the returned phase and perfect closure. -/
 115theorem deficitCost_eq_half_normSq (δ : ℝ) :
 116    deficitCost δ = (1 / 2) * Complex.normSq (1 - Complex.exp (δ * Complex.I)) := by
 117  have hre : (1 - Complex.exp ((δ : ℂ) * Complex.I)).re = 1 - Real.cos δ := by
 118    simp [Complex.sub_re, Complex.exp_ofReal_mul_I_re]
 119  have him : (1 - Complex.exp ((δ : ℂ) * Complex.I)).im = -Real.sin δ := by
 120    simp [Complex.sub_im, Complex.exp_ofReal_mul_I_im]
 121  rw [Complex.normSq_apply, hre, him]
 122  have hpyth := Real.sin_sq_add_cos_sq δ
 123  unfold deficitCost
 124  nlinarith [hpyth]
 125
 126/-- The deficit cost is nonnegative. -/
 127theorem deficitCost_nonneg (δ : ℝ) : 0 ≤ deficitCost δ := by
 128  unfold deficitCost
 129  linarith [Real.cos_le_one δ]
 130
 131/-- The zero set of the deficit cost is EXACTLY the lattice `2πℤ`: perfect closure
 132happens at integer numbers of full turns and nowhere else. -/
 133theorem deficitCost_eq_zero_iff (δ : ℝ) :
 134    deficitCost δ = 0 ↔ ∃ n : ℤ, δ = (n : ℝ) * (2 * Real.pi) := by
 135  unfold deficitCost
 136  constructor
 137  · intro h
 138    have hcos : Real.cos δ = 1 := by linarith
 139    obtain ⟨n, hn⟩ := (Real.cos_eq_one_iff δ).mp hcos
 140    exact ⟨n, hn.symm⟩
 141  · rintro ⟨n, rfl⟩
 142    have := Real.cos_int_mul_two_pi n
 143    linarith
 144
 145/-- Strict positivity off the closure lattice: any phase deficit not a whole number
 146of turns costs strictly positive recognition (accepted derive step
 147`derive_20260702_090702`). -/
 148theorem deficitCost_pos_of_not_period (δ : ℝ)
 149    (h : ¬∃ n : ℤ, δ = (n : ℝ) * (2 * Real.pi)) :
 150    0 < deficitCost δ := by
 151  rcases lt_or_eq_of_le (deficitCost_nonneg δ) with hpos | heq
 152  · exact hpos
 153  · exact absurd ((deficitCost_eq_zero_iff δ).mp heq.symm) h
 154
 155/-! ## Local convexity at closure: strict quadratic minimum -/
 156
 157/-- The deficit cost is differentiable with derivative `sin δ`. -/
 158theorem deficitCost_hasDerivAt (δ : ℝ) :
 159    HasDerivAt deficitCost (Real.sin δ) δ := by
 160  have h := (Real.hasDerivAt_cos δ).const_sub (1 : ℝ)
 161  simpa [deficitCost] using h
 162
 163/-- Closure is a critical point: the derivative of the deficit cost vanishes at
 164`δ = 0`. -/
 165theorem deficitCost_critical_at_zero : HasDerivAt deficitCost 0 0 := by
 166  simpa using deficitCost_hasDerivAt 0
 167
 168/-- The second derivative at closure is `cos 0 = 1 > 0`: the derivative `sin` has
 169slope 1 at `δ = 0`, so closure is a strict quadratic minimum of the deficit cost
 170(accepted derive step `derive_20260702_090702`: local convexity `C''(0) = 1`). -/
 171theorem deficitCost_second_deriv_pos_at_zero :
 172    HasDerivAt Real.sin 1 0 := by
 173  simpa using Real.hasDerivAt_sin 0
 174
 175/-! ## Holonomy closure ↔ deficit-free ↔ the 2πℤ lattice -/
 176
 177/-- The holonomy returns exactly (`h(T) = 1`) iff `κT` lies on the `2πℤ` lattice. -/
 178theorem holonomy_eq_one_iff_lattice (kappa T : ℝ) :
 179    holonomy kappa T = 1 ↔ ∃ n : ℤ, kappa * T = (n : ℝ) * (2 * Real.pi) := by
 180  unfold holonomy
 181  rw [Complex.exp_eq_one_iff]
 182  constructor
 183  · rintro ⟨n, hn⟩
 184    refine ⟨n, ?_⟩
 185    have h2 : ((kappa * T : ℝ) : ℂ) * Complex.I =
 186        (((n : ℝ) * (2 * Real.pi) : ℝ) : ℂ) * Complex.I := by
 187      push_cast
 188      linear_combination hn
 189    have h3 := mul_right_cancel₀ Complex.I_ne_zero h2
 190    exact_mod_cast h3
 191  · rintro ⟨n, hn⟩
 192    refine ⟨n, ?_⟩
 193    have hC : ((kappa : ℂ) * (T : ℂ)) = (n : ℂ) * (2 * (Real.pi : ℂ)) := by
 194      exact_mod_cast hn
 195    calc (kappa : ℂ) * (T : ℂ) * Complex.I
 196        = ((n : ℂ) * (2 * (Real.pi : ℂ))) * Complex.I := by rw [hC]
 197      _ = (n : ℂ) * (2 * (Real.pi : ℂ) * Complex.I) := by ring
 198
 199/-- Deficit-free return and exact holonomy closure are the SAME condition: the
 200deficit cost of the accumulated phase vanishes iff the holonomy returns to 1. -/
 201theorem holonomy_deficit_free_iff (kappa T : ℝ) :
 202    deficitCost (kappa * T) = 0 ↔ holonomy kappa T = 1 := by
 203  rw [deficitCost_eq_zero_iff, holonomy_eq_one_iff_lattice]
 204
 205/-- Exact return times are the lattice `T ∈ (2π/κ)ℤ` (the canonical form of the
 206banked `legb_exp_period_lattice`, both directions). -/
 207theorem holonomy_eq_one_iff (kappa T : ℝ) (hk : kappa ≠ 0) :
 208    holonomy kappa T = 1 ↔ ∃ n : ℤ, T = (n : ℝ) * (2 * Real.pi / kappa) := by
 209  rw [holonomy_eq_one_iff_lattice]
 210  constructor
 211  · rintro ⟨n, hn⟩
 212    refine ⟨n, ?_⟩
 213    have h1 : T * kappa = (n : ℝ) * (2 * Real.pi) := by linarith [hn]
 214    have h2 : T = (n : ℝ) * (2 * Real.pi) / kappa := eq_div_of_mul_eq hk h1
 215    rw [h2, mul_div_assoc]
 216  · rintro ⟨n, rfl⟩
 217    refine ⟨n, ?_⟩
 218    field_simp
 219
 220/-! ## The minimal positive deficit-free period is 2π/κ -/
 221
 222/-- **The headline (LEG-B `legb_minimal_positive_period`, landed canonically).**
 223For `κ > 0`, the set of positive deficit-free return times has least element
 224`β = 2π/κ`. 2π is forced: it is the smallest positive zero of the deficit-cost
 225functional, which is itself the J-form on the forced U(1) carrier. -/
 226theorem euclideanPeriod_isLeast (kappa : ℝ) (hk : 0 < kappa) :
 227    IsLeast {T : ℝ | 0 < T ∧ deficitCost (kappa * T) = 0} (euclideanPeriod kappa) := by
 228  constructor
 229  · refine ⟨div_pos (by positivity) hk, ?_⟩
 230    rw [deficitCost_eq_zero_iff]
 231    refine ⟨1, ?_⟩
 232    unfold euclideanPeriod
 233    push_cast
 234    field_simp
 235  · rintro T ⟨hT, hzero⟩
 236    rw [deficitCost_eq_zero_iff] at hzero
 237    obtain ⟨n, hn⟩ := hzero
 238    have h2pi : (0 : ℝ) < 2 * Real.pi := by positivity
 239    have hnR : (0 : ℝ) < (n : ℝ) := by
 240      have hprod : (0 : ℝ) < (n : ℝ) * (2 * Real.pi) := hn ▸ mul_pos hk hT
 241      nlinarith
 242    have hnZ : (1 : ℤ) ≤ n := by exact_mod_cast Int.cast_pos.mp hnR
 243    have hn1 : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hnZ
 244    have hT_eq : T = (n : ℝ) * (2 * Real.pi) / kappa :=
 245      eq_div_of_mul_eq (ne_of_gt hk) (by linarith [hn])
 246    unfold euclideanPeriod
 247    rw [hT_eq]
 248    have hnum : 2 * Real.pi ≤ (n : ℝ) * (2 * Real.pi) := by
 249      nlinarith [Real.pi_pos]
 250    rw [div_eq_mul_inv, div_eq_mul_inv]
 251    exact mul_le_mul_of_nonneg_right hnum (inv_nonneg.mpr hk.le)
 252
 253/-! ## The physics bridge: deficit-free period → S = 2πER (saturating case) -/
 254
 255/-- **CONDITIONAL bridge.** Given the two named MODEL premises (`HorizonRate`:
 256`κ = 1/R`; `ClausiusForm`: `S = βE` at the deficit-free Euclidean period
 257`β = 2π/κ`), the entropy of the static horizon is exactly `S = 2πER`: the
 258SATURATING value of the Bekenstein/Casini form. Canonical form of the banked
 259`legb_clausius_to_bekenstein`. -/
 260theorem bekenstein_saturation_from_deficit_free_period
 261    (S E R kappa : ℝ) (hR : 0 < R)
 262    (hRate : HorizonRate kappa R)
 263    (hClausius : ClausiusForm S E (euclideanPeriod kappa)) :
 264    S = 2 * Real.pi * E * R := by
 265  unfold HorizonRate at hRate
 266  unfold ClausiusForm euclideanPeriod at hClausius
 267  subst hRate
 268  rw [hClausius]
 269  have hR' : R ≠ 0 := ne_of_gt hR
 270  field_simp
 271
 272/-- The saturating thermal state satisfies the `KeystoneFactorThree` bound form with
 273equality. NOTE the honest scope: this shows the CLAUSIUS STATE saturates the bound
 274form; it is NOT the general bound for arbitrary states (LEG-B proper, still OPEN with
 275the derive captain). -/
 276theorem totalEntropyBound_saturating_case
 277    (S E R kappa : ℝ) (hR : 0 < R)
 278    (hRate : HorizonRate kappa R)
 279    (hClausius : ClausiusForm S E (euclideanPeriod kappa)) :
 280    KeystoneFactorThree.TotalEntropyBekensteinBound S E R := by
 281  have h := bekenstein_saturation_from_deficit_free_period S E R kappa hR hRate hClausius
 282  unfold KeystoneFactorThree.TotalEntropyBekensteinBound
 283  linarith
 284
 285/-! ## Certificate -/
 286
 287/-- Bundled certificate for the deficit-free-period chain: the deficit cost is
 288nonnegative with zero set exactly `2πℤ`, deficit-free return IS holonomy closure,
 289the minimal positive deficit-free period is `2π/κ`, and (given the two named MODEL
 290premises) the static-horizon entropy saturates at `S = 2πER`. The first four fields
 291are unconditional THEOREMs; the last is the CONDITIONAL physics bridge. -/
 292structure DeficitFreePeriodCert : Prop where
 293  cost_nonneg : ∀ δ : ℝ, 0 ≤ deficitCost δ
 294  cost_zero_iff : ∀ δ : ℝ, deficitCost δ = 0 ↔ ∃ n : ℤ, δ = (n : ℝ) * (2 * Real.pi)
 295  holonomy_iff : ∀ kappa T : ℝ, deficitCost (kappa * T) = 0 ↔ holonomy kappa T = 1
 296  minimal_period : ∀ kappa : ℝ, 0 < kappa →
 297    IsLeast {T : ℝ | 0 < T ∧ deficitCost (kappa * T) = 0} (euclideanPeriod kappa)
 298  saturation : ∀ S E R kappa : ℝ, 0 < R → HorizonRate kappa R →
 299    ClausiusForm S E (euclideanPeriod kappa) → S = 2 * Real.pi * E * R
 300
 301/-- The certificate holds. -/
 302theorem deficitFreePeriodCert : DeficitFreePeriodCert where
 303  cost_nonneg := deficitCost_nonneg
 304  cost_zero_iff := deficitCost_eq_zero_iff
 305  holonomy_iff := holonomy_deficit_free_iff
 306  minimal_period := euclideanPeriod_isLeast
 307  saturation := bekenstein_saturation_from_deficit_free_period
 308
 309end DeficitFreePeriod
 310end Holography
 311end IndisputableMonolith
 312