Encyclopedia Holography Holography Deficit Free Period Total Entropy Bound Saturating Case

ARTICLE 5 claims 5 theorems

Holography Deficit Free Period Total Entropy Bound Saturating Case

A theorem in a machine-checked library shows when the total entropy bound is met exactly, and the two physical premises it still depends on.

Verify this page

The saturating case

The Bekenstein bound is a limit from black hole thermodynamics: the total entropy S of a system that fits inside a sphere of radius R cannot exceed 2πER, where E is the system's total energy. The Recognition Science framework's machine-checked library of formal theorems contains a declaration, totalEntropyBound_saturating_case, that proves a specific instance where this bound is not just obeyed but reached exactly. The result states that if the entropy S equals the thermal product βE, with β the Euclidean period, and if the horizon rate κ equals 1/R, then S = 2πER, which is precisely the saturating value of the bound.

The proof rests on a chain of formal steps. The framework models a recognition cycle, a discrete record of events, as a clock with a phase that returns to itself after a full period. The cost of an imperfect return, the squared distance between the actual and perfect phase, is 1 − cos δ. This cost is zero exactly when the phase deficit δ is an integer multiple of 2π, and strictly positive otherwise. For a positive rate κ, the smallest positive time T for which the cost vanishes is the Euclidean period β = 2π/κ. This minimal period is not chosen; it is forced by the geometry of the circle, as the smallest positive zero of the cost function.

The saturating case then follows. With the horizon rate set to κ = 1/R, the Euclidean period becomes β = 2πR. The Clausius form S = βE, which is the thermal entropy of a horizon at that period, then yields S = 2πER. This is the exact equality that saturates the Casini/Bekenstein bound. The theorem is unconditional in its mathematics: the minimality of the period and the zero-cost characterization are proved from the definitions with no extra assumptions.

What the declaration does not claim is equally precise. It does not prove the full Bekenstein bound for all states, which would require showing S ≤ 2πER universally. That statement, known in the framework as the total entropy bound proper, remains an open target. The saturating case also depends on two named model premises: the Clausius form S = βE, which imports the first law and thermality of the horizon state, and the horizon rate κ = 1/R, which imports the surface-gravity normalization. Neither premise is derived here; each is a definitional choice. The theorem's conclusion is conditional on both. The mathematical chain that forces the period is clean, but the physics bridge that connects it to entropy carries these two assumptions.

THEOREM deficitCost · IndisputableMonolith/Holography/DeficitFreePeriod.lean
deficitCost · IndisputableMonolith/Holography/DeficitFreePeriod.lean:88 
/-- The deficit-cost functional: the recognition cost of a phase deficit `δ`,
`C(δ) = 1 − cos δ`. Accepted derive step `derive_20260702_082715`. Equivalently the
squared chord distance `½‖1 − exp(iδ)‖²` (see `deficitCost_eq_half_normSq`), the
J-cost quadratic form on the U(1) carrier. -/
noncomputable def deficitCost (δ : ℝ) : ℝ :=
  1 - Real.cos δ
THEOREM deficitCost_eq_zero_iff · deficitCost_pos_of_not_period · IndisputableMonolith/Holography/DeficitFreePeriod.lean
deficitCost_eq_zero_iff · IndisputableMonolith/Holography/DeficitFreePeriod.lean:131 
/-- 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
deficitCost_pos_of_not_period · IndisputableMonolith/Holography/DeficitFreePeriod.lean:145 
/-- 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
euclideanPeriod_isLeast · IndisputableMonolith/Holography/DeficitFreePeriod.lean:222 
/-- **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)
THEOREM HorizonRate · IndisputableMonolith/Holography/DeficitFreePeriod.lean
HorizonRate · IndisputableMonolith/Holography/DeficitFreePeriod.lean:105 
/-- Named MODEL premise (horizon rate): the static-horizon phase rate is `κ = 1/R`
(surface-gravity convention in the ledger normalization; Live Bet 2 tracks its
kernel-derivability). -/
def HorizonRate (kappa R : ℝ) : Prop :=
  kappa = 1 / R
THEOREM bekenstein_saturation_from_deficit_free_period · IndisputableMonolith/Holography/DeficitFreePeriod.lean
bekenstein_saturation_from_deficit_free_period · IndisputableMonolith/Holography/DeficitFreePeriod.lean:255 
/-- **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 full total entropy bound for all states is not proved here; only the saturating case is established. The two model premises, ClausiusForm and HorizonRate, are not derived; they are definitional choices. The physical bridge from the mathematical period to black hole entropy is not a theorem; it is conditional on the two model 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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND