Encyclopedia Holography Holography Deficit Free Period Deficit Cost Eq Half Norm Sq

ARTICLE 4 claims 4 theorems

Holography Deficit Free Period Deficit Cost Eq Half Norm Sq

A machine-checked theorem shows the cost of missing a perfect cycle is the squared distance on a circle, which forces the period 2π/κ.

Verify this page

The deficit cost

The declaration deficitCost_eq_half_normSq establishes a precise geometric identity for a quantity called the deficit cost. In plain terms, the deficit cost measures how far a cyclic process is from closing perfectly. The theorem states that this cost equals one half the squared Euclidean distance between the point representing perfect closure and the point representing the actual, imperfect return on the unit circle in the complex plane. This is the same as the squared length of the chord connecting those two points on the circle, divided by two.

This identity is not an isolated curiosity. It is the quadratic form of the J-cost, the unique cost function forced by the framework's five conditions. The theorem is proved in the machine-checked library of formal theorems, meaning the derivation is verified by a computer and is axiom-clean. The identity is the foundation for a chain of results about the period of a clocked recognition cycle. The cost is always nonnegative, it is zero exactly when the phase deficit is an integer multiple of 2π, and it is strictly positive otherwise. The function has a strict quadratic minimum at zero, with a positive second derivative, confirming that perfect closure is a stable equilibrium.

From this identity, the framework derives the minimal positive deficit-free period. For a cycle running at rate κ, the set of positive return times with zero cost has a least element, which is exactly 2π/κ. This period is not chosen as a convention; it is forced by the geometry of the cost function. The number 2π is the smallest positive zero of the deficit cost, which itself is the unique J-form on the forced U(1) carrier. This result is unconditional and axiom-clean.

In Recognition Science, this chain connects to a physics bridge. With two named model premises, the ledger (a discrete record of events) identifies the horizon rate as κ = 1/R and the entropy as the thermal form S = βE. Under these premises, the deficit-free period forces the saturation value S = 2πER, the exact saturating value of the Bekenstein bound. This bridge is conditional on those two premises, which are not derived here.

What the declaration does not claim is equally important. It does not prove the full Bekenstein bound for all states, which is a statement about relative entropy. It does not derive the two model premises: the Clausius form, which imports the first law and thermality of the horizon state, and the horizon rate, which imports the surface-gravity normalization. These remain open targets. The mathematical chain, however, is unconditional and complete.

THEOREM deficitCost_eq_half_normSq · IndisputableMonolith/Holography/DeficitFreePeriod.lean
deficitCost_eq_half_normSq · IndisputableMonolith/Holography/DeficitFreePeriod.lean:113 
/-- `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_nonneg · deficitCost_eq_zero_iff · deficitCost_pos_of_not_period · IndisputableMonolith/Holography/DeficitFreePeriod.lean
deficitCost_nonneg · IndisputableMonolith/Holography/DeficitFreePeriod.lean:126 
/-- The deficit cost is nonnegative. -/
theorem deficitCost_nonneg (δ : ℝ) : 0 ≤ deficitCost δ := by
  unfold deficitCost
  linarith [Real.cos_le_one δ]
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 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 Bekenstein bound for all states is not proved here. The two model premises, ClausiusForm and HorizonRate, are not derived. The theorem does not claim that 2π is chosen by convention; it is forced by the cost function.

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