Holography Deficit Free Period Bekenstein Saturation From Deficit Free Period

The saturation result

The Bekenstein bound is a limit from black hole thermodynamics: the entropy S of a system of energy E confined to a region of size R cannot exceed 2πER (in units where the gravitational constant and speed of light are set to one). It is a statement about how much information a physical system can hold. The Recognition Science framework, which derives physical structure from the cost of recognition events, has a machine-checked theorem that reproduces this bound as an equality, not an inequality, for a specific thermal state.

The theorem, bekenstein_saturation_from_deficit_free_period, starts with a clock. The framework models a recognition cycle as a phase that returns to its starting point. The cost of an imperfect return, defined as deficit cost, is the squared distance between the returned phase and perfect closure: C(δ) = 1 − cos δ. This cost is zero exactly when the phase returns to a multiple of 2π. For a cycle running at rate κ, the smallest positive time T for which the cost is zero is forced to be T = 2π/κ. This is a theorem: the period is not chosen but derived from the cost function.

The physics bridge then applies this to a horizon. Two named assumptions are needed. First, HorizonRate sets the horizon's phase rate to κ = 1/R, the standard surface-gravity convention. Second, ClausiusForm sets the entropy to S = βE at the Euclidean period β = 2π/κ, which is the thermal form. Under these two premises, the deficit-free period forces S = 2πER. The machine-checked library proves this equality and shows it saturates the Bekenstein bound, meaning the thermal state hits the limit exactly.

What the declaration does not claim is as important as what it proves. It does not prove the Bekenstein bound as a general inequality for all states; that would require showing relative entropy is positive, a separate open target. It also does not derive the two physical premises. ClausiusForm assumes the horizon state is thermal, and HorizonRate assumes the surface-gravity normalization. Both are model choices, not theorems. The mathematical chain forcing the 2π period is unconditional and axiom-clean; the physics conclusion inherits the assumptions' status.

For the reader, the result is a precise example of how a forced period can become a physical constant. The framework's contribution is not a new bound but a derivation of the bound's saturation for a specific state, with the assumptions laid bare. The general bound remains open; the saturation case is closed.

/-- **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)

/-- **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

/-- 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

What this page does not claim

The general Bekenstein bound for all states is not proved here. The ClausiusForm premise, which assumes horizon thermality, is not derived. The HorizonRate premise, which fixes the surface-gravity normalization, is not derived.

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: