Encyclopedia Holography Holography Turn Ratio Carrier

ARTICLE 6 claims 5 theorems 1 model

Holography Turn Ratio Carrier

A holographic cycle's cost is set by the ratio of its period to a natural closure time, and only one period escapes a positive cost.

Verify this page

The turn ratio carrier

In the Recognition Science framework, a holographic system cycles through eight recognition events and then returns to its starting state. The turn ratio carrier is the mathematical object that prices each cycle: it takes the ratio of the actual cycle period T to a reference period 2π/κ, where κ is a system parameter, and feeds that ratio into the framework's fundamental cost function J(x) = (x + 1/x)/2 − 1. The cost of a cycle is therefore C(T) = J(κT/2π). This is a definitional choice, a model of how recognition cost accrues per cycle, not a derived law.

The central result is a theorem: the cost is zero if and only if the period T equals the reference period 2π/κ. Any other period carries a strictly positive cost. This singles out one period as the unique deficit-free closure time. The theorem also rules out multiples of this period: if the system takes n times the reference period to close, for any integer n ≥ 2, the cost is strictly positive, equal to (n−1)²/(2n). So zero-cost closure forces n = 1, meaning the system must close exactly once per reference period, with no repeated cycles.

Why does this matter? The framework uses this to kill a competing idea. One might try to extend the cost function J to complex numbers and apply it to the phase of a returned wave, rather than to the real turn ratio. The framework proves this phase-based approach fails: the cost computed from a phase is never positive, so it cannot penalize any deviation from the reference period, and it vanishes for every multiple of 2π, so it cannot distinguish the unique zero-cost period from its multiples. The turn ratio carrier, by contrast, does exactly that.

The framework also proves that extending J to complex numbers is not a forced move. Two different extensions both agree with J on the positive real line, yet they differ at the imaginary unit, and one of them even vanishes at a point other than 1. This shows that any attempt to price recognition cost using complex phases involves an arbitrary choice, not a unique consequence of the framework.

Finally, the framework shows what happens in the flat-space limit, where κ approaches zero. The cost of any fixed period diverges, and the reference period itself diverges. There is no finite period with zero cost, no residual thermality, and accumulated cost over repeated cycles grows without bound. This establishes a clean contrast: the turn ratio carrier only produces a unique zero-cost period when the system parameter κ is positive.

In plain terms, the turn ratio carrier is the framework's way of saying that a holographic cycle must close at exactly one specific time, and any other timing costs energy. The framework proves this using only the real turn ratio, and it demonstrates that alternative approaches based on complex phases cannot achieve the same result.

MODEL turnRatioCost · IndisputableMonolith/Holography/TurnRatioCarrier.lean
turnRatioCost · IndisputableMonolith/Holography/TurnRatioCarrier.lean:79 
/-- 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)
THEOREM turnRatioCost_eq_zero_iff · IndisputableMonolith/Holography/TurnRatioCarrier.lean
turnRatioCost_eq_zero_iff · IndisputableMonolith/Holography/TurnRatioCarrier.lean:106 
/-- **Headline (B2 math half): the deficit-free period is the UNIQUE zero of the
per-cycle cost.** `C(T) = 0 ↔ T = 2π/κ`. Strictly stronger than minimality
(`DeficitFreePeriod.euclideanPeriod_isLeast`): no other positive period, lattice or
not, deficit or excess, has zero cost. Pure T5 (`Cost.Jcost_eq_zero_iff`). -/
theorem turnRatioCost_eq_zero_iff (kappa T : ℝ) (hk : 0 < kappa) (hT : 0 < T) :
    turnRatioCost kappa T = 0 ↔ T = DeficitFreePeriod.euclideanPeriod kappa := by
  unfold turnRatioCost
  rw [Cost.Jcost_eq_zero_iff _ (turnRatio_pos hk hT)]
  exact turnRatio_eq_one_iff kappa T hk
THEOREM turnRatioCost_cover_pos · IndisputableMonolith/Holography/TurnRatioCarrier.lean
turnRatioCost_cover_pos · IndisputableMonolith/Holography/TurnRatioCarrier.lean:147 
/-- **KMS-window discharge, positivity half:** every `n ≥ 2` sheeted cover (Euclidean
angle `2πn`) carries strictly positive per-cycle cost. The excess-angle branch is
cost-excluded by the same T5 inequality as the deficit branch. -/
theorem turnRatioCost_cover_pos (kappa : ℝ) (hk : 0 < kappa) (n : ℕ) (hn : 2 ≤ n) :
    0 < turnRatioCost kappa (n * DeficitFreePeriod.euclideanPeriod kappa) := by
  unfold turnRatioCost
  rw [turnRatio_cover kappa hk n]
  have hpos : (0 : ℝ) < n := by exact_mod_cast Nat.lt_of_lt_of_le Nat.zero_lt_two hn
  have hne : (n : ℝ) ≠ 1 := by
    have : (1 : ℝ) < n := by exact_mod_cast Nat.lt_of_lt_of_le Nat.one_lt_two hn
    exact ne_of_gt this
  exact Cost.Jcost_pos_of_ne_one _ hpos hne
THEOREM phaseCost_nonpos · IndisputableMonolith/Holography/TurnRatioCarrier.lean
phaseCost_nonpos · IndisputableMonolith/Holography/TurnRatioCarrier.lean:190 
/-- **Poison lemma (sign death):** the phase-branch cost is NEVER strictly positive,
so it cannot penalize any deficit. The phase branch cannot force the period. -/
theorem phaseCost_nonpos (δ : ℝ) : phaseCost δ ≤ 0 := by
  rw [phaseCost_eq]
  linarith [Real.cos_le_one δ]
THEOREM u1_extension_not_unique · IndisputableMonolith/Holography/TurnRatioCarrier.lean
u1_extension_not_unique · IndisputableMonolith/Holography/TurnRatioCarrier.lean:252 
/-- **Kernel record: the U(1)/ℂ extension of `J` is underdetermined.** Two extensions
agree with `Cost.Jcost` on all of `ℝ₊` yet disagree at `I`. Any argument that "extends
J to the phase and reads off the period" is choosing its conclusion. -/
theorem u1_extension_not_unique :
    ∃ J₁ J₂ : ℂ → ℝ,
      (∀ x : ℝ, 0 < x → J₁ (x : ℂ) = Cost.Jcost x) ∧
      (∀ x : ℝ, 0 < x → J₂ (x : ℂ) = Cost.Jcost x) ∧
      ∃ z : ℂ, J₁ z ≠ J₂ z := by
  refine ⟨Jprime, Jsecond, fun x _ => Jprime_agrees x, fun x hx => Jsecond_agrees x hx,
    Complex.I, ?_⟩
  rw [Jprime_I, Jsecond_I]
  norm_num
THEOREM turnRatioCost_unbounded_near_zero_kappa · IndisputableMonolith/Holography/TurnRatioCarrier.lean
turnRatioCost_unbounded_near_zero_kappa · IndisputableMonolith/Holography/TurnRatioCarrier.lean:297 
/-- 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]

What this page does not claim

The framework does not prove that the turn ratio carrier is the only possible way to price recognition cost. The framework does not derive the value of κ from first principles; it treats κ as a given parameter. The framework does not show that the phase-based cost is the correct cost for any physical system; it only shows that this particular extension fails.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND