Encyclopedia Holography Holography Deficit Free Period Holonomy Eq One Iff Lattice

ARTICLE 4 claims 3 theorems 1 model

Holography Deficit Free Period Holonomy Eq One Iff Lattice

A clock that must return to zero after a full cycle can only do so at exact multiples of its period, and the framework shows why that period is 2π/κ.

Verify this page

The return condition

A ledger, a discrete record of events, that runs a repeated cycle has a natural question: after how much time does the cycle land exactly where it started? For a cycle that advances a phase at a steady rate κ, the answer is the classical one. The phase after time T is κT, and the cycle closes only when this phase is a whole multiple of 2π. The theorem holonomy_eq_one_iff_lattice states this precisely: the return map exp(iκT) equals 1 if and only if κT is an integer multiple of 2π.

The statement is a pure fact about complex exponentials, proved in the machine-checked library of formal theorems. It does not depend on any physical assumption. The same library then defines a deficit cost, a penalty for how far a return falls short of perfect closure, as 1 minus the cosine of the phase deficit. This cost is zero exactly at the lattice points, strictly positive everywhere else, and has a strict minimum at closure. From this, a second theorem shows that for a positive rate κ, the smallest positive time with zero deficit is 2π/κ. That number is not chosen; it is forced by the requirement that the cost vanish.

In Recognition Science, this chain is the mathematical core of a larger argument. The framework models a recognition cycle as embedding into a circle, and this return condition is what the eight-tick clock must satisfy. The framework's library proves the lattice condition and the minimal period unconditionally. It then attaches a physics bridge, but only under two named model premises: that the horizon rate is κ = 1/R and that the entropy takes the Clausius form S = βE. With those premises, the deficit-free period forces the saturating value S = 2πER, the exact bound from the Bekenstein form.

What the declaration does not claim is as important as what it proves. The lattice condition and minimal period are theorems about exponentials and cosines. The physics bridge, the step that connects the period to entropy, is conditional on the two model premises. The framework does not derive those premises here; it does not prove the general Bekenstein bound for all states, which would require Casini's relative-entropy positivity. The bridge is a conditional result, not an unconditional derivation.

THEOREM holonomy_eq_one_iff_lattice · IndisputableMonolith/Holography/DeficitFreePeriod.lean
holonomy_eq_one_iff_lattice · IndisputableMonolith/Holography/DeficitFreePeriod.lean:177 
/-- The holonomy returns exactly (`h(T) = 1`) iff `κT` lies on the `2πℤ` lattice. -/
theorem holonomy_eq_one_iff_lattice (kappa T : ℝ) :
    holonomy kappa T = 1 ↔ ∃ n : ℤ, kappa * T = (n : ℝ) * (2 * Real.pi) := by
  unfold holonomy
  rw [Complex.exp_eq_one_iff]
  constructor
  · rintro ⟨n, hn⟩
    refine ⟨n, ?_⟩
    have h2 : ((kappa * T : ℝ) : ℂ) * Complex.I =
        (((n : ℝ) * (2 * Real.pi) : ℝ) : ℂ) * Complex.I := by
      push_cast
      linear_combination hn
    have h3 := mul_right_cancel₀ Complex.I_ne_zero h2
    exact_mod_cast h3
  · rintro ⟨n, hn⟩
    refine ⟨n, ?_⟩
    have hC : ((kappa : ℂ) * (T : ℂ)) = (n : ℂ) * (2 * (Real.pi : ℂ)) := by
      exact_mod_cast hn
    calc (kappa : ℂ) * (T : ℂ) * Complex.I
        = ((n : ℂ) * (2 * (Real.pi : ℂ))) * Complex.I := by rw [hC]
      _ = (n : ℂ) * (2 * (Real.pi : ℂ) * Complex.I) := by ring
THEOREM deficitCost_eq_zero_iff · deficitCost_pos_of_not_period · deficitCost_critical_at_zero · 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
deficitCost_critical_at_zero · IndisputableMonolith/Holography/DeficitFreePeriod.lean:163 
/-- Closure is a critical point: the derivative of the deficit cost vanishes at
`δ = 0`. -/
theorem deficitCost_critical_at_zero : HasDerivAt deficitCost 0 0 := by
  simpa using deficitCost_hasDerivAt 0
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)
MODEL 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 physics bridge is not an unconditional theorem; it depends on two named model premises. The framework does not derive the general Bekenstein bound for all states, only the saturating case. The theorem does not claim that 2π is chosen; it is the smallest positive zero of the deficit cost.

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