Holography Deficit Free Period Deficit Cost Second Deriv Pos At Zero

The shape of a perfect return

In the Recognition Science framework, a recognition event is a discrete record of an observation, and the framework's central claim is that the cost of recognition is forced by logic, not chosen. One piece of that machinery is a cost function that measures how far a clock's phase is from closing its loop. The declaration deficitCost_second_deriv_pos_at_zero is a small but load-bearing theorem about that function: it proves that the cost has a strict minimum at the point of perfect closure, meaning the cost rises quadratically as the phase moves away from zero.

The cost function itself is simple. For a phase deficit δ, the cost is C(δ) = 1 − cos δ. This is the squared chord distance between the returned phase and perfect closure on a circle, so it is always nonnegative and vanishes exactly when δ is a multiple of 2π. The theorem in question states that the second derivative of this cost at δ = 0 is 1, which is positive. That single fact, combined with the zero being at a critical point, guarantees the minimum is genuine and quadratic, not flat. In plain terms: a clock that misses its return by a small amount pays a cost proportional to the square of that miss, so small errors are cheap but not free.

This quadratic shape is what forces the fundamental period. The framework's library proves that for a clock running at rate κ, the set of positive return times with zero cost has a least element, namely 2π/κ. That period is not chosen; it is the smallest positive zero of the cost function, which is itself the unique form forced by the framework's axioms. The second-derivative theorem is the local anchor for that global result: it certifies that the zero at 0 is an isolated minimum, so the next zero must be exactly one full cycle away.

In Recognition Science, this period feeds a physical bridge. With two named model premises, the static-horizon phase rate κ = 1/R and the thermal form S = βE, the deficit-free period forces the saturating entropy S = 2πER. But those premises are models, not theorems: the first imports the surface-gravity normalization, the second imports the first law of horizon thermodynamics. The mathematical chain from the cost function to the period is unconditional and axiom-clean; the physics bridge is conditional on those two choices.

What the declaration does not claim is just as important. It does not prove that the cost function is the only possible one, nor does it derive the two model premises. It does not discharge the full Bekenstein bound for all states, which requires a relative-entropy positivity statement. The theorem is a local fact about a specific function, and its power comes from being part of a larger forced chain, not from standing alone.

/-- The second derivative at closure is `cos 0 = 1 > 0`: the derivative `sin` has
slope 1 at `δ = 0`, so closure is a strict quadratic minimum of the deficit cost
(accepted derive step `derive_20260702_090702`: local convexity `C''(0) = 1`). -/
theorem deficitCost_second_deriv_pos_at_zero :
    HasDerivAt Real.sin 1 0 := by
  simpa using Real.hasDerivAt_sin 0

/-- The deficit cost is nonnegative. -/
theorem deficitCost_nonneg (δ : ℝ) : 0 ≤ deficitCost δ := by
  unfold deficitCost
  linarith [Real.cos_le_one δ]

/-- 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 the cost function is the unique possible one. The theorem does not derive the two model premises HorizonRate and ClausiusForm. The theorem does not discharge the full Bekenstein bound for all states.

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: