Holography Turn Ratio Carrier Turn Ratio Cost Unbounded Near Zero Kappa

The flat-space limit

In the Recognition Science framework, a recurring cycle has a natural period, the time after which the cycle returns to its starting state. The framework prices each cycle with a cost function, and the theorem turnRatioCost_unbounded_near_zero_kappa describes what happens to that cost as a parameter kappa, which sets the scale of the period, approaches zero from above. The theorem states that for any fixed positive period T and any bound M, there exists a small positive value of kappa such that for all smaller positive kappa, the cost of the cycle exceeds M. In plain language: as kappa tends to zero, the cost of any fixed cycle grows without bound.

The cost function itself is defined as J(x) = (x + 1/x)/2 - 1, where x is the ratio of the cycle's period to the natural period. The theorem follows from the fact that as kappa shrinks, the natural period grows without bound, so the ratio x for any fixed T becomes very small, and the 1/x term in J dominates, driving the cost to infinity. This is a direct consequence of the cost function's reciprocal symmetry: the cost of a ratio and its reciprocal are the same, so a very small ratio costs as much as a very large one.

This result has a clear physical interpretation. It means that in the limit where kappa goes to zero, there is no finite period with zero cost, no residual thermality, and no horizon. The framework's forced period itself diverges, so the system has no natural scale. The accumulated cost over repeated cycles is also unbounded, meaning that the system cannot settle into a stable, low-cost configuration. This is a statement about the absence of a preferred cycle in a flat, scale-free limit.

In Recognition Science, this theorem is part of a larger argument about how the cost function behaves across different regimes. It is one of several results that together show that the cost function J, when applied to the real turn ratio, has a unique zero-cost period and strictly positive cost everywhere else. This particular theorem establishes the behavior in the flat-space limit, where the natural period is pushed to infinity. It does not claim that the cost function is defined or well-behaved at kappa equals zero itself, only that the cost diverges as kappa approaches zero from above.

The theorem is proved in the framework's machine-checked library of formal theorems, meaning it is a verified statement within the framework's axioms. It is a statement about the cost function's behavior, not about any physical system directly. The framework models physical systems, and this theorem describes a property of that model. It is a mathematical fact about the cost function, not an empirical observation.

/-- As `κ → 0⁺` the per-cycle cost of any FIXED period diverges past every bound: the
turn ratio collapses to `0⁺` and `J` blows up. Flat space admits no finite-cost
closure at any finite period; no residual thermality survives. -/
theorem turnRatioCost_unbounded_near_zero_kappa (T : ℝ) (hT : 0 < T) (M : ℝ) :
    ∃ κ₀ : ℝ, 0 < κ₀ ∧ ∀ kappa : ℝ, 0 < kappa → kappa < κ₀ →
      M < turnRatioCost kappa T := by
  have hpi : (0 : ℝ) < Real.pi := Real.pi_pos
  set A : ℝ := max M 0 with hA
  have hA0 : 0 ≤ A := le_max_right M 0
  have hMA : M ≤ A := le_max_left M 0
  have hden : (0 : ℝ) < 2 * A + 4 := by linarith
  refine ⟨2 * Real.pi / (T * (2 * A + 4)), by positivity, ?_⟩
  intro kappa hk hklt
  have hx : 0 < turnRatio kappa T := turnRatio_pos hk hT
  -- the ratio is small: x < 1/(2A+4)
  have hxlt : turnRatio kappa T < 1 / (2 * A + 4) := by
    unfold turnRatio
    rw [div_lt_div_iff₀ (by positivity) hden]
    have h1 : kappa * (T * (2 * A + 4)) < 2 * Real.pi := by
      have := mul_lt_mul_of_pos_right hklt (by positivity : (0:ℝ) < T * (2 * A + 4))
      calc kappa * (T * (2 * A + 4))
          < 2 * Real.pi / (T * (2 * A + 4)) * (T * (2 * A + 4)) := this
        _ = 2 * Real.pi := by field_simp
    calc kappa * T * (2 * A + 4) = kappa * (T * (2 * A + 4)) := by ring
      _ < 2 * Real.pi := h1
      _ = 1 * (2 * Real.pi) := by ring
  -- hence the reciprocal is large: 2A+4 < x⁻¹
  have hinv : 2 * A + 4 < (turnRatio kappa T)⁻¹ := by
    have hprod : turnRatio kappa T * (2 * A + 4) < 1 := (lt_div_iff₀ hden).mp hxlt
    have hxx : turnRatio kappa T * (2 * A + 4) <
        turnRatio kappa T * (turnRatio kappa T)⁻¹ := by
      rw [mul_inv_cancel₀ (ne_of_gt hx)]
      exact hprod
    exact lt_of_mul_lt_mul_left hxx hx.le
  -- and J(x) ≥ x⁻¹/2 − 1 dominates
  have hJ : (turnRatio kappa T)⁻¹ / 2 - 1 ≤ Cost.Jcost (turnRatio kappa T) := by
    unfold Cost.Jcost
    nlinarith [hx.le]
  unfold turnRatioCost
  nlinarith [hJ, hinv, hMA]

/-- The per-cycle recognition cost priced on the turn ratio: `C(T) = J(κT/2π)` with
`J` the unique T5 cost (`Cost.Jcost`). -/
noncomputable def turnRatioCost (kappa T : ℝ) : ℝ :=
  Cost.Jcost (turnRatio kappa T)

/-- Any strictly positive per-cycle cost accumulates past every bound (Archimedean):
a deficit or excess closure cannot persist at the fixed point. -/
theorem accumulatedCost_unbounded (c : ℝ) (hc : 0 < c) (B : ℝ) :
    ∃ N : ℕ, B < accumulatedCost N c := by
  obtain ⟨N, hN⟩ := exists_nat_gt (B / c)
  refine ⟨N, ?_⟩
  unfold accumulatedCost
  rwa [div_lt_iff₀ hc] at hN

What this page does not claim

The theorem does not state that the cost function is undefined at kappa equals zero, only that it diverges as kappa approaches zero from above. It does not claim that no physical system can have a small kappa, only that the cost of any fixed cycle becomes large in that limit. It does not claim that the framework's model of a physical system is correct, only that the cost function behaves in this way within the model.

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/TurnRatioCarrier.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: