Holography Deficit Free Period Deficit Cost Pos Of Not Period

The deficit cost

In the Recognition Science framework, a ledger (a discrete record of events) tracks a repeating process by a phase angle. A perfect return means the phase comes back to its starting value. The framework defines the cost (the price of an imperfect return) as C(δ) = 1 − cos δ, where δ is the phase deficit, the amount by which the return misses perfect closure. This is the squared chord distance on a circle: the straight-line gap between the returned point and the starting point, halved. The formula is not chosen arbitrarily; it is the unique cost function forced by the framework's five plain conditions, applied to the circular carrier of the clock.

The theorem deficitCost_pos_of_not_period states a precise fact: if a phase deficit δ is not an integer multiple of 2π, then the cost is strictly positive. In symbols, if there is no integer n with δ = n·2π, then 0 < C(δ). This is a machine-checked proof in the framework's library of formal theorems. The companion theorem deficitCost_eq_zero_iff gives the exact converse: the cost vanishes if and only if δ is an integer multiple of 2π. Together they draw a sharp line: perfect returns happen exactly at multiples of the full circle, and every other return carries a positive price.

The theorem also supports a minimal-period result. For a process running at rate κ, the cost of a return after time T is C(κT). The set of positive times with zero cost has a least element, namely 2π/κ (euclideanPeriod_isLeast). This is the shortest time for a deficit-free return. The number 2π is not inserted by hand; it emerges as the smallest positive zero of the cost function itself, which is the unique J-form on the forced circular carrier.

In Recognition Science, this chain connects to a physics bridge. With two named model premises, the deficit-free period forces the saturating value S = 2πER for horizon entropy (bekenstein_saturation_from_deficit_free_period). The theorem deficitCost_pos_of_not_period itself does not make that bridge. It only establishes the positivity of the cost off the lattice. The bridge is conditional on the premises HorizonRate (κ = 1/R) and ClausiusForm (S = βE), which are model choices, not derived facts. The theorem does not prove that any physical horizon actually satisfies those premises, nor does it prove the full Bekenstein bound for all states. Those remain open targets.

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

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

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

What this page does not claim

The theorem does not prove that any physical horizon satisfies the HorizonRate or ClausiusForm premises. The theorem does not prove the full Bekenstein bound for all states, only the saturating case under the two model premises. The theorem does not derive the value of 2π from first principles; it takes it as the smallest positive zero of 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: