Holography Deficit Free Period

The deficit-free period

In physics, a periodic process is one that repeats after a fixed interval. The holography deficit-free period is the shortest time T after which a clocked cycle, running at a rate κ, returns exactly to its starting phase with no error. The framework's machine-checked library of formal theorems proves that this time is forced to be 2π/κ. The number 2π is not chosen; it is the smallest positive zero of the cost of an imperfect return, a cost that is itself uniquely determined by the framework's five plain conditions on recognition.

The core object is a phase-return map, written h(T) = exp(iκT). It describes how the phase of a cycle advances over time. A perfect return means h(T) = 1. The cost of falling short, with a phase deficit δ, is C(δ) = 1 − cos δ, which is the squared chord distance between the returned phase and perfect closure. This cost is always nonnegative, vanishes exactly when δ is an integer multiple of 2π, and has a strict quadratic minimum at closure. For a positive rate κ, the set of positive times with zero deficit has a least element, and that least element is 2π/κ. This is the deficit-free period.

The classical cousin is the Euclidean period in thermal physics, where a system at inverse temperature β is periodic in imaginary time with period β. The framework's result reproduces that structure: the deficit-free period plays the role of β. The formal chain shows that the period is not an input but a forced consequence of the cost function. The cost function itself, J(x) = (x + 1/x)/2 − 1, is the unique function satisfying the framework's axioms, and its quadratic form on the unit circle is exactly the deficit cost.

In Recognition Science, the framework models a horizon, such as a black hole's event horizon, as a system with a recognition cycle. Two named model premises connect the period to physics. The first, HorizonRate, sets the phase rate κ equal to 1/R, where R is the horizon radius, matching the Schwarzschild surface-gravity convention. The second, ClausiusForm, states that the horizon entropy S is the thermal product βE, where E is the energy. With these two premises, the deficit-free period forces the saturation value S = 2πER. That value saturates the Bekenstein bound, the maximum entropy a region of size R can hold.

The mathematical chain, items 1 through 3 above, is unconditional and axiom-clean. The physics bridge is conditional on the two named model premises. The module does not discharge the full Bekenstein bound for all states, which is Casini's relative-entropy positivity statement, and it does not derive the two premises themselves. The KMS thermality of the horizon state and the surface-gravity normalization remain open targets. The result is a forced magnitude, not a free parameter, and it lands exactly on the known saturation value.

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

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

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

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

/-- Named MODEL premise (Clausius form): the static-horizon entropy is the thermal
entropy `S = βE` at Euclidean period `β`. This is the first-law/KMS-thermality input;
its derivation route is the captain's open `legb_kms_window_unique` target. -/
def ClausiusForm (S E beta : ℝ) : Prop :=
  S = beta * E

What this page does not claim

This module does not discharge the full Bekenstein bound for all states, only the saturating case. The two model premises, HorizonRate and ClausiusForm, are not derived here. The value 2π is not an arbitrary choice but the smallest positive zero of the deficit cost, which is itself uniquely determined.

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: