Pith. sign in
module module high

IndisputableMonolith.Holography.DeficitFreePeriod

show as:
view Lean formalization →

Defines the per-cycle holonomy carrier h(T)=exp(i κ T) for a clocked recognition cycle at rate κ, together with the deficit cost of incomplete Euclidean closure and the unique deficit-free period 2π/κ. Holography and Bekenstein-loop workers cite it as the B2 geometric core. The module packages the U(1) embedding of the eight-tick clock, nonnegativity and criticality of the deficit, and the Clausius/horizon-rate interfaces used downstream.

claimFor a recognition cycle at surface gravity (clock rate) $\kappa>0$ and Euclidean duration $T$, the holonomy is $h(T)=e^{i\kappa T}\in U(1)$. The deficit cost is a nonnegative function of the phase mismatch that vanishes if and only if $\kappa T\in 2\pi\mathbb{Z}$. The unique positive deficit-free period is the Euclidean period $T_E=2\pi/\kappa$.

background

Recognition Science holography (LEG-B) treats near-horizon thermodynamics as a clocked recognition cycle. The eight-tick octave embeds in $U(1)$: continuous time $T$ advances a phase at rate $\kappa$, so the per-cycle return map is the holonomy $h(T)=\exp(i\kappa T)$. Accepted derive step derive_20260702_065112 records that discrete embedding (cf. the eight-tick circle period).

A mismatch from full $2\pi$ turns produces a geometric deficit. The module prices that mismatch by a deficit cost built from the squared norm of the holonomy defect: nonnegative, zero precisely on full periods, critical at zero mismatch, with positive second derivative there. This is the continuum carrier for the later real-turn-ratio cost $C(T)=J(\kappa T/2\pi)$ with $J(x)=(x+x^{-1})/2-1$ (T5).

The local setting sits under the Factor-3 Keystone import: conditional exclusion structure for microstate readings, not unconditional physics. Horizon rate and Clausius-form interfaces are typed here so B3 can attach Rindler $d\theta/d\tau_E=\kappa$ without smuggling period closure.

proof idea

Definition-first module with supporting calculus lemmas, not a single theorem. Holonomy is the standard complex exponential on the circle. Deficit cost is identified with half the squared norm of the phase defect; nonnegativity, the zero-iff-period characterization, and strict positivity off-period are immediate from that identity. Differentiability, criticality at zero mismatch, and positive second derivative at zero are one-variable real-analysis facts about that quadratic-type cost. Euclidean period is the unique positive $T$ with $\kappa T=2\pi$. Clausius and horizon-rate abbreviations expose the thermodynamic reading without extra proof burden.

why it matters in Recognition Science

This is the B2 geometric core of the Bekenstein LEG-B loop. HorizonClockRate imports it and deliberately types only B3: near-horizon Rindler advance $d\theta/d\tau_E=\kappa$, refusing to assert $2\pi$ closure; that closure is this module's Euclidean period, consumed with TurnRatioCarrier's turn-ratio identity. TurnRatioCarrier prices the continued eight-tick cycle as $C(T)=J(\kappa T/2\pi)$ on the real turn ratio, so the deficit-free locus here is exactly where that cost vanishes.

Framework landmarks: T5 $J$-uniqueness supplies the cost shape used once the turn ratio is real; T7 eight-tick octave justifies the $U(1)$ embedding of the discrete clock. Downstream holography therefore separates rate (B3) from period (B2) cleanly, which is the panel-accepted split for the horizon thermodynamics argument.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (20)