IndisputableMonolith.Holography.DeficitFreePeriod
Defines the per-cycle holonomy carrier h(T)=exp(i κ T) for a clocked recognition cycle at rate κ, plus the deficit cost and the Euclidean period of deficit-free closure. Bekenstein/LEG-B holography cites this as the B2 period object. The module records the U(1) embedding of the eight-tick clock and the elementary calculus of the deficit around zero.
claimThe module introduces the holonomy $h(T)=e^{i\kappa T}$ of a cycle at rate $\kappa$, a nonnegative deficit cost of duration $T$ that vanishes exactly on the Euclidean closure period, and related carriers (Clausius form, horizon rate). Elementary identities relate the deficit to a squared norm and establish the second-derivative test at the zero-deficit point.
background
In the LEG-B holography stack, a recognition cycle is clocked at surface-gravity rate $\kappa$. The accepted derive step embeds the discrete eight-tick clock in $U(1)$, so the continuous per-cycle return is the phase map $h(T)=e^{i\kappa T}$. Deficit cost measures failure of holonomy closure: it is zero precisely when $T$ is a Euclidean period that returns the phase to the identity.
Upstream, KeystoneFactorThree supplies only a conditional Factor-3 exclusion structure ("Nothing here is unconditional physics; the value of this module is the exclusion STRUCTURE"). The present module sits on that frame and defines the geometric carriers needed before any cost pricing.
Sibling TurnRatioCarrier later prices the real turn ratio by the T5 $J$-cost, $C(T)=J(\kappa T/2\pi)$ with $J(x)=(x+x^{-1})/2-1$. Here the objects remain the complex holonomy and its deficit, prior to that pricing step.
proof idea
Definition-and-calculus module, not a single deep theorem. It introduces holonomy, deficit cost, Euclidean period, Clausius form, and horizon rate, then proves standard facts: deficit equals half a squared norm, is nonnegative, vanishes iff the period condition holds, is strictly positive off that locus, and has a critical point at zero with positive second derivative. The $U(1)$ exponential is the recorded derive link from the discrete eight-tick embedding to the continuous phase return.
why it matters in Recognition Science
HorizonClockRate imports this module and states that it does not assert $2\pi$ closure; that is B2's output via the Euclidean period defined here (and the turn-ratio identity in TurnRatioCarrier). HorizonClockRate only types the Rindler rate $d\theta/d\tau_E=\kappa$ (B3). TurnRatioCarrier prices per-cycle recognition cost as $J$ of the real turn ratio and relies on the same period infrastructure.
The module therefore supplies the geometric period at which recognition cost can vanish, connecting the T7 eight-tick octave to near-horizon Euclidean thermodynamics inside the LEG-B loop. Without a deficit-free period carrier, the B2/B3 split (closure versus rate-only typing) cannot be stated cleanly.
scope and limits
- Does not prove an unconditional Bekenstein bound or Factor-3 exclusion (upstream remains conditional).
- Does not identify the Rindler angle rate; that is HorizonClockRate (B3 only).
- Does not price the turn ratio by J-cost; that is TurnRatioCarrier.
- Does not derive κ from first principles; κ parametrizes the clocked cycle.
- Does not re-prove the discrete eight-tick embedding beyond the accepted derive pointer.
used by (2)
depends on (1)
declarations in this module (20)
-
def
holonomy -
def
deficitCost -
def
euclideanPeriod -
def
ClausiusForm -
def
HorizonRate -
theorem
deficitCost_eq_half_normSq -
theorem
deficitCost_nonneg -
theorem
deficitCost_eq_zero_iff -
theorem
deficitCost_pos_of_not_period -
theorem
deficitCost_hasDerivAt -
theorem
deficitCost_critical_at_zero -
theorem
deficitCost_second_deriv_pos_at_zero -
theorem
holonomy_eq_one_iff_lattice -
theorem
holonomy_deficit_free_iff -
theorem
holonomy_eq_one_iff -
theorem
euclideanPeriod_isLeast -
theorem
bekenstein_saturation_from_deficit_free_period -
theorem
totalEntropyBound_saturating_case -
structure
DeficitFreePeriodCert -
theorem
deficitFreePeriodCert