euclideanPeriod
plain-language theorem explainer
Defines the Euclidean period β = 2π/κ as the candidate minimal positive return time for a clocked recognition cycle at surface gravity κ. Anyone working the LEG-B holonomy-to-Bekenstein chain cites this as the named period that later theorems prove is least among deficit-free returns. The body is a one-line arithmetic definition, not a derived equality.
Claim. For a real surface gravity $\kappa$, the Euclidean period is $\beta(\kappa) := 2\pi/\kappa$.
background
This module formalizes the LEG-B core chain: deficit-free holonomy closure forces a unique minimal positive period, which (under two named model premises) saturates the Bekenstein form. The carrier is the U(1) phase-return map $h(T)=\exp(i\kappa T)$; exact return holds iff $\kappa T\in 2\pi\mathbb{Z}$.
The recognition cost of a phase deficit $\delta$ is the chordal J-form $C(\delta)=1-\cos\delta=\tfrac12|1-e^{i\delta}|^2$. It is nonnegative, vanishes exactly on $2\pi\mathbb{Z}$, and has a strict quadratic minimum at closure. The set of positive times with $C(\kappa T)=0$ is therefore a discrete lattice scaled by $1/\kappa$.
The Euclidean period names the obvious positive generator of that lattice. Downstream theorems then prove it is the least element and feed it into the Clausius/KMS bridge $S=\beta E$.
proof idea
Pure definition: unfold to $2\cdot\pi/\kappa$. No lemmas, no tactics. Later results such as euclideanPeriod_isLeast do the work of showing this value is the least positive zero of the deficit cost along the ray $T\mapsto\kappa T$.
why it matters
Names the period that the headline theorem proves is least among positive deficit-free returns, and that the conditional Bekenstein bridge uses as the thermal $\beta$. The certificate structure packages nonnegativity of the cost, zero-set lattice, holonomy equivalence, minimality of this period, and (given HorizonRate $\kappa=1/R$ and ClausiusForm $S=\beta E$) saturation $S=2\pi E R$.
Horizon-clock results treat this period as a B2 carrier output, not a B3 input: at $\beta$ the turn ratio is unity by B1/B2 linkage alone. In the broader RS forcing picture this is where the continuous U(1) holonomy meets the eight-tick discrete clock: $2\pi$ is forced as the smallest positive zero of the unique J-form on that carrier, not chosen by hand.
The physics bridge remains conditional on the two named model premises; the open captain target is uniqueness of the KMS window that would discharge ClausiusForm.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.