IndisputableMonolith.Holography.TurnRatioCarrier
Defines the turn ratio: the fraction of one full 2π holonomy turn a Euclidean clock at rate κ sweeps in time T, plus its J-cost. Horizon-clock and seam-transfer modules cite the zero-cost characterization that the ratio equals one exactly on the deficit-free lattice period. Lemmas are elementary: positivity, reciprocity, and cover identities reduce to Cost and the holonomy lattice.
claimThe turn ratio is $r(\kappa,T)=\kappa T/(2\pi)$. Its recognition cost is $J(r)$ with $J(x)=(x+x^{-1})/2-1$. One has $J(r)\ge 0$, $J(r)=0$ iff $r=1$ (equivalently $\kappa T$ lies on the $2\pi$-holonomy lattice), $J(r)=J(1/r)$, and $J(r)>0$ off the deficit-free period.
background
LEG-B of the Bekenstein-Hawking coefficient program needs a deficit-free Euclidean period. DeficitFreePeriod forces the continuum closure $T=2\pi/\kappa$ from holonomy of $\mathrm{Complex.exp}$ (kernel of the exponential, not a temperature). EightTickSubperiodExclusion supplies the discrete half: no proper divisor of the 8-tick octave realizes an admissible census, so the period is the full turn.
This module packages the dimensionless fraction of that full turn actually swept by a continued clock at rate $\kappa$ over Euclidean time $T$. The Cost module supplies the unique J-cost $J(x)=(x+x^{-1})/2-1$. Composing $J$ with the turn ratio yields a nonnegative scalar that vanishes exactly when the geometry closes without conical deficit.
proof idea
Definition-and-lemmas module, not a deep derivation. The turn ratio is the plain quotient $\kappa T/(2\pi)$; its cost is $J$ of that quotient. Positivity, the iff characterizing vanishing cost by ratio equal to one, reciprocity under $r\mapsto 1/r$, and the cover-value identities are one-line or short algebraic consequences of Cost and of DeficitFreePeriod's holonomy-lattice characterization. The lattice-period zero-cost lemma simply rephrases that vanishing criterion in period language.
why it matters in Recognition Science
Imported by HorizonClockRate, which types only B3's rate law $d\theta/d\tau_E=\kappa$ and explicitly defers $2\pi$ closure to this module's ratio-equals-one criterion together with DeficitFreePeriod. Also imported by SeamTransferCore: there the per-closure recognition cost on the seam double-entry pair fiber is the character anomaly $C=\mathrm{Tr}(W)/2-1$, the same algebraic shape as $J$. The carrier therefore links the discrete eight-tick octave (T7) to continuum holonomy: full turn means ratio one and zero J-cost; any conical subperiod carries strictly positive cost.
scope and limits
- Does not derive surface gravity κ; treats it as an input rate.
- Does not give 2π/κ a KMS or thermal reading; 2π is holonomy angle only.
- Does not prove eight-tick subperiod exclusion (upstream module).
- Does not construct the seam transfer operator W.
- Does not re-prove J-uniqueness; that is upstream in Cost (T5).
used by (2)
depends on (3)
declarations in this module (39)
-
def
turnRatio -
def
turnRatioCost -
theorem
turnRatio_pos -
theorem
turnRatio_eq_one_iff -
theorem
turnRatioCost_nonneg -
theorem
turnRatioCost_eq_zero_iff -
theorem
turnRatioCost_pos_of_ne_period -
theorem
turnRatioCost_reciprocal -
theorem
turnRatio_cover -
theorem
Jcost_cover_value -
theorem
turnRatioCost_cover_pos -
theorem
lattice_period_zero_cost_iff -
def
phaseCost -
theorem
phaseCost_eq -
theorem
phaseCost_nonpos -
theorem
phaseCost_vanishes_on_covers -
def
JextRe -
theorem
JextRe_agrees -
def
Jprime -
def
Jsecond -
theorem
Jprime_agrees -
theorem
Jsecond_agrees -
theorem
JextRe_I -
theorem
Jprime_I -
theorem
Jsecond_I -
theorem
u1_extension_not_unique -
theorem
u1_extension_zero_set_not_forced -
theorem
euclideanPeriod_unbounded -
theorem
turnRatioCost_unbounded_near_zero_kappa -
def
accumulatedCost -
theorem
accumulatedCost_unbounded -
def
visitCount -
def
witnessWalk -
theorem
eight_tick_multiple_exclusion -
def
CensusPricing -
theorem
turnRatioCost_censusPricing -
theorem
b2_unique_zero_of_censusPricing -
structure
TurnRatioCarrierCert -
theorem
turnRatioCarrierCert