Encyclopedia Holography Holography Deficit Free Period Holonomy Deficit Free Iff
ARTICLE 5 claims 4 theorems 1 model
Holography Deficit Free Period Holonomy Deficit Free Iff
A machine-checked theorem ties a cycle's exact return to a cost being zero, and the smallest such return time is forced to be 2π/κ.
The return condition
In classical mathematics, a periodic process of rate κ returns to its starting phase exactly when the elapsed time T satisfies κT = 2πn for some integer n. The Recognition Science declaration holonomy_deficit_free_iff restates this fact in the framework's own terms: the recognition cost of a phase deficit, defined as 1 − cos(κT), equals zero if and only if the holonomy, the complex phase return exp(iκT), equals 1. This is a proved theorem in the framework's machine-checked library of formal theorems, with no framework-specific axioms.
The cost function itself is not arbitrary. It is the squared chord distance between the returned phase and perfect closure, half the squared norm of 1 − exp(iδ). The theorem deficitCost_eq_zero_iff proves this cost vanishes exactly on the lattice 2πℤ, and deficitCost_pos_of_not_period proves it is strictly positive off that lattice. The cost is nonnegative everywhere, has a critical point at zero, and its second derivative there is positive, so closure is a strict quadratic minimum. These facts compose into the main result: for κ > 0, the smallest positive return time is 2π/κ. The number 2π is not chosen; it is the smallest positive zero of the cost function, which is itself the unique J-form on the forced U(1) carrier.
The framework then attaches a physics bridge, but that bridge is conditional on two named model premises. The first, HorizonRate, sets the static-horizon phase rate to κ = 1/R, the Schwarzschild/Rindler surface-gravity convention. The second, ClausiusForm, sets the static-horizon entropy to the thermal S = βE at the Euclidean period. With both premises, the deficit-free period forces S = 2πER, the exact saturating value of the Casini/Bekenstein form. This saturation result is a theorem, but it inherits the MODEL tag from its premises.
What the declaration does not claim is as important as what it proves. It does not discharge the full Bekenstein bound for all states, which is Casini's relative-entropy positivity statement. It does not derive the two model premises: the Clausius form imports the first law or KMS thermality of the horizon state, and the HorizonRate premise imports the surface-gravity normalization. The lattice and minimality chain is unconditional and axiom-clean; the physics bridge is conditional on premises that remain open targets. The framework's own honesty boundary names these exactly.
THEOREM holonomy_deficit_free_iff · IndisputableMonolith/Holography/DeficitFreePeriod.lean
/-- Deficit-free return and exact holonomy closure are the SAME condition: the
deficit cost of the accumulated phase vanishes iff the holonomy returns to 1. -/
theorem holonomy_deficit_free_iff (kappa T : ℝ) :
deficitCost (kappa * T) = 0 ↔ holonomy kappa T = 1 := by
rw [deficitCost_eq_zero_iff, holonomy_eq_one_iff_lattice]
THEOREM deficitCost_eq_half_normSq · IndisputableMonolith/Holography/DeficitFreePeriod.lean
/-- `C(δ) = ½‖1 − exp(iδ)‖²`: the deficit cost is exactly half the squared chord
distance between the returned phase and perfect closure. -/
theorem deficitCost_eq_half_normSq (δ : ℝ) :
deficitCost δ = (1 / 2) * Complex.normSq (1 - Complex.exp (δ * Complex.I)) := by
have hre : (1 - Complex.exp ((δ : ℂ) * Complex.I)).re = 1 - Real.cos δ := by
simp [Complex.sub_re, Complex.exp_ofReal_mul_I_re]
have him : (1 - Complex.exp ((δ : ℂ) * Complex.I)).im = -Real.sin δ := by
simp [Complex.sub_im, Complex.exp_ofReal_mul_I_im]
rw [Complex.normSq_apply, hre, him]
have hpyth := Real.sin_sq_add_cos_sq δ
unfold deficitCost
nlinarith [hpyth]
THEOREM deficitCost_eq_zero_iff · deficitCost_pos_of_not_period · IndisputableMonolith/Holography/DeficitFreePeriod.lean
/-- The zero set of the deficit cost is EXACTLY the lattice `2πℤ`: perfect closure
happens at integer numbers of full turns and nowhere else. -/
theorem deficitCost_eq_zero_iff (δ : ℝ) :
deficitCost δ = 0 ↔ ∃ n : ℤ, δ = (n : ℝ) * (2 * Real.pi) := by
unfold deficitCost
constructor
· intro h
have hcos : Real.cos δ = 1 := by linarith
obtain ⟨n, hn⟩ := (Real.cos_eq_one_iff δ).mp hcos
exact ⟨n, hn.symm⟩
· rintro ⟨n, rfl⟩
have := Real.cos_int_mul_two_pi n
linarith
/-- Strict positivity off the closure lattice: any phase deficit not a whole number
of turns costs strictly positive recognition (accepted derive step
`derive_20260702_090702`). -/
theorem deficitCost_pos_of_not_period (δ : ℝ)
(h : ¬∃ n : ℤ, δ = (n : ℝ) * (2 * Real.pi)) :
0 < deficitCost δ := by
rcases lt_or_eq_of_le (deficitCost_nonneg δ) with hpos | heq
· exact hpos
· exact absurd ((deficitCost_eq_zero_iff δ).mp heq.symm) h
THEOREM euclideanPeriod_isLeast · IndisputableMonolith/Holography/DeficitFreePeriod.lean
/-- **The headline (LEG-B `legb_minimal_positive_period`, landed canonically).**
For `κ > 0`, the set of positive deficit-free return times has least element
`β = 2π/κ`. 2π is forced: it is the smallest positive zero of the deficit-cost
functional, which is itself the J-form on the forced U(1) carrier. -/
theorem euclideanPeriod_isLeast (kappa : ℝ) (hk : 0 < kappa) :
IsLeast {T : ℝ | 0 < T ∧ deficitCost (kappa * T) = 0} (euclideanPeriod kappa) := by
constructor
· refine ⟨div_pos (by positivity) hk, ?_⟩
rw [deficitCost_eq_zero_iff]
refine ⟨1, ?_⟩
unfold euclideanPeriod
push_cast
field_simp
· rintro T ⟨hT, hzero⟩
rw [deficitCost_eq_zero_iff] at hzero
obtain ⟨n, hn⟩ := hzero
have h2pi : (0 : ℝ) < 2 * Real.pi := by positivity
have hnR : (0 : ℝ) < (n : ℝ) := by
have hprod : (0 : ℝ) < (n : ℝ) * (2 * Real.pi) := hn ▸ mul_pos hk hT
nlinarith
have hnZ : (1 : ℤ) ≤ n := by exact_mod_cast Int.cast_pos.mp hnR
have hn1 : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hnZ
have hT_eq : T = (n : ℝ) * (2 * Real.pi) / kappa :=
eq_div_of_mul_eq (ne_of_gt hk) (by linarith [hn])
unfold euclideanPeriod
rw [hT_eq]
have hnum : 2 * Real.pi ≤ (n : ℝ) * (2 * Real.pi) := by
nlinarith [Real.pi_pos]
rw [div_eq_mul_inv, div_eq_mul_inv]
exact mul_le_mul_of_nonneg_right hnum (inv_nonneg.mpr hk.le)
MODEL bekenstein_saturation_from_deficit_free_period · IndisputableMonolith/Holography/DeficitFreePeriod.lean
/-- **CONDITIONAL bridge.** Given the two named MODEL premises (`HorizonRate`:
`κ = 1/R`; `ClausiusForm`: `S = βE` at the deficit-free Euclidean period
`β = 2π/κ`), the entropy of the static horizon is exactly `S = 2πER`: the
SATURATING value of the Bekenstein/Casini form. Canonical form of the banked
`legb_clausius_to_bekenstein`. -/
theorem bekenstein_saturation_from_deficit_free_period
(S E R kappa : ℝ) (hR : 0 < R)
(hRate : HorizonRate kappa R)
(hClausius : ClausiusForm S E (euclideanPeriod kappa)) :
S = 2 * Real.pi * E * R := by
unfold HorizonRate at hRate
unfold ClausiusForm euclideanPeriod at hClausius
subst hRate
rw [hClausius]
have hR' : R ≠ 0 := ne_of_gt hR
field_simp
What this page does not claim
The declaration does not prove the full Bekenstein bound for all states. The declaration does not derive the two model premises HorizonRate and ClausiusForm. The declaration does not claim the physics bridge is unconditional; it is conditional on the named premises.
Verify this page
Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:
$ lake env lean IndisputableMonolith/Holography/DeficitFreePeriod.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)
A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.
Derived articles
This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:
- What is the derivation route for the uniqueness of the KMS analytic window that would discharge the ClausiusForm premise?
- What is the status of the Live Bet 2 audit for the kernel-derivability of R = 2GE that would discharge the HorizonRate premise?
- What does the full Bekenstein bound for all states, as Casini's relative-entropy positivity statement, require beyond the saturating case?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM holonomy_deficit_free_iff · IndisputableMonolith/Holography/DeficitFreePeriod.lean
/-- Deficit-free return and exact holonomy closure are the SAME condition: the deficit cost of the accumulated phase vanishes iff the holonomy returns to 1. -/ theorem holonomy_deficit_free_iff (kappa T : ℝ) : deficitCost (kappa * T) = 0 ↔ holonomy kappa T = 1 := by rw [deficitCost_eq_zero_iff, holonomy_eq_one_iff_lattice]The recognition cost of a phase deficit, defined as 1 − cos(κT), equals zero if and only if the holonomy, the complex phase return exp(iκT), equals 1. holonomy_deficit_free_iff · IndisputableMonolith/Holography/DeficitFreePeriod.leanTHEOREM deficitCost_eq_half_normSq · IndisputableMonolith/Holography/DeficitFreePeriod.lean
/-- `C(δ) = ½‖1 − exp(iδ)‖²`: the deficit cost is exactly half the squared chord distance between the returned phase and perfect closure. -/ theorem deficitCost_eq_half_normSq (δ : ℝ) : deficitCost δ = (1 / 2) * Complex.normSq (1 - Complex.exp (δ * Complex.I)) := by have hre : (1 - Complex.exp ((δ : ℂ) * Complex.I)).re = 1 - Real.cos δ := by simp [Complex.sub_re, Complex.exp_ofReal_mul_I_re] have him : (1 - Complex.exp ((δ : ℂ) * Complex.I)).im = -Real.sin δ := by simp [Complex.sub_im, Complex.exp_ofReal_mul_I_im] rw [Complex.normSq_apply, hre, him] have hpyth := Real.sin_sq_add_cos_sq δ unfold deficitCost nlinarith [hpyth]The cost function is the squared chord distance between the returned phase and perfect closure, half the squared norm of 1 − exp(iδ). deficitCost_eq_half_normSq · IndisputableMonolith/Holography/DeficitFreePeriod.leanTHEOREM deficitCost_eq_zero_iff · deficitCost_pos_of_not_period · IndisputableMonolith/Holography/DeficitFreePeriod.lean
/-- The zero set of the deficit cost is EXACTLY the lattice `2πℤ`: perfect closure happens at integer numbers of full turns and nowhere else. -/ theorem deficitCost_eq_zero_iff (δ : ℝ) : deficitCost δ = 0 ↔ ∃ n : ℤ, δ = (n : ℝ) * (2 * Real.pi) := by unfold deficitCost constructor · intro h have hcos : Real.cos δ = 1 := by linarith obtain ⟨n, hn⟩ := (Real.cos_eq_one_iff δ).mp hcos exact ⟨n, hn.symm⟩ · rintro ⟨n, rfl⟩ have := Real.cos_int_mul_two_pi n linarith/-- Strict positivity off the closure lattice: any phase deficit not a whole number of turns costs strictly positive recognition (accepted derive step `derive_20260702_090702`). -/ theorem deficitCost_pos_of_not_period (δ : ℝ) (h : ¬∃ n : ℤ, δ = (n : ℝ) * (2 * Real.pi)) : 0 < deficitCost δ := by rcases lt_or_eq_of_le (deficitCost_nonneg δ) with hpos | heq · exact hpos · exact absurd ((deficitCost_eq_zero_iff δ).mp heq.symm) hThe cost vanishes exactly on the lattice 2πℤ, and is strictly positive off that lattice. deficitCost_eq_zero_iff · deficitCost_pos_of_not_period · IndisputableMonolith/Holography/DeficitFreePeriod.leanTHEOREM euclideanPeriod_isLeast · IndisputableMonolith/Holography/DeficitFreePeriod.lean
/-- **The headline (LEG-B `legb_minimal_positive_period`, landed canonically).** For `κ > 0`, the set of positive deficit-free return times has least element `β = 2π/κ`. 2π is forced: it is the smallest positive zero of the deficit-cost functional, which is itself the J-form on the forced U(1) carrier. -/ theorem euclideanPeriod_isLeast (kappa : ℝ) (hk : 0 < kappa) : IsLeast {T : ℝ | 0 < T ∧ deficitCost (kappa * T) = 0} (euclideanPeriod kappa) := by constructor · refine ⟨div_pos (by positivity) hk, ?_⟩ rw [deficitCost_eq_zero_iff] refine ⟨1, ?_⟩ unfold euclideanPeriod push_cast field_simp · rintro T ⟨hT, hzero⟩ rw [deficitCost_eq_zero_iff] at hzero obtain ⟨n, hn⟩ := hzero have h2pi : (0 : ℝ) < 2 * Real.pi := by positivity have hnR : (0 : ℝ) < (n : ℝ) := by have hprod : (0 : ℝ) < (n : ℝ) * (2 * Real.pi) := hn ▸ mul_pos hk hT nlinarith have hnZ : (1 : ℤ) ≤ n := by exact_mod_cast Int.cast_pos.mp hnR have hn1 : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hnZ have hT_eq : T = (n : ℝ) * (2 * Real.pi) / kappa := eq_div_of_mul_eq (ne_of_gt hk) (by linarith [hn]) unfold euclideanPeriod rw [hT_eq] have hnum : 2 * Real.pi ≤ (n : ℝ) * (2 * Real.pi) := by nlinarith [Real.pi_pos] rw [div_eq_mul_inv, div_eq_mul_inv] exact mul_le_mul_of_nonneg_right hnum (inv_nonneg.mpr hk.le)For κ > 0, the smallest positive return time is 2π/κ. euclideanPeriod_isLeast · IndisputableMonolith/Holography/DeficitFreePeriod.leanMODEL bekenstein_saturation_from_deficit_free_period · IndisputableMonolith/Holography/DeficitFreePeriod.lean
/-- **CONDITIONAL bridge.** Given the two named MODEL premises (`HorizonRate`: `κ = 1/R`; `ClausiusForm`: `S = βE` at the deficit-free Euclidean period `β = 2π/κ`), the entropy of the static horizon is exactly `S = 2πER`: the SATURATING value of the Bekenstein/Casini form. Canonical form of the banked `legb_clausius_to_bekenstein`. -/ theorem bekenstein_saturation_from_deficit_free_period (S E R kappa : ℝ) (hR : 0 < R) (hRate : HorizonRate kappa R) (hClausius : ClausiusForm S E (euclideanPeriod kappa)) : S = 2 * Real.pi * E * R := by unfold HorizonRate at hRate unfold ClausiusForm euclideanPeriod at hClausius subst hRate rw [hClausius] have hR' : R ≠ 0 := ne_of_gt hR field_simpWith both premises, the deficit-free period forces S = 2πER, the exact saturating value of the Casini/Bekenstein form. bekenstein_saturation_from_deficit_free_period · IndisputableMonolith/Holography/DeficitFreePeriod.lean