HorizonRate

The module formalizes the LEG-B deficit-free-period chain: holonomy on the U(1) carrier $h(T)=\exp(i\kappa T)$, the deficit cost $C(\delta)=1-\cos\delta$ (half the squared chord distance to perfect closure, the J-form on that carrier), and the least positive deficit-free return time $\beta=2\pi/\kappa$. Those three steps are unconditional theorems.

The physics bridge that turns $\beta$ into Bekenstein saturation is conditional on two named MODEL premises. This declaration is the first: the static-horizon phase rate equals the reciprocal radius. The companion premise is the Clausius form $S=\beta E$ at the Euclidean period. Both sit outside the pure holonomy/cost lattice and are flagged as model sockets, not kernel theorems.

Ledger units here follow the RS-native gauge ($c=1$, tick and voxel normalized). The equality $\kappa=1/R$ is the surface-gravity convention in that normalization, not a claim about SI surface gravity.

Propositional definition, not a proved statement. The body is the bare equality $\kappa=1/R$; there is no tactic proof, no lemma application, and no reduction. Downstream theorems unfold the name and substitute.

This premise is the normalization socket that converts the forced Euclidean period $\beta=2\pi/\kappa$ into the saturating Bekenstein value $S=2\pi E R$. The conditional bridge theorem applies it together with the Clausius form at $\beta$ to obtain exact saturation; the saturating-case entropy bound then inherits the same hypotheses. The bundled deficit-free-period certificate lists the unconditional cost/period facts plus this conditional bridge as its final field.

A separate HorizonClockRate lemma records the honest non-claim that the rate-only clock bundle is silent on $T=2\pi/\kappa$ and that this $\kappa=1/R$ socket is an independent model leg, not part of the B3 rate delivery. Live Bet 2 tracks kernel-derivability of the premise; until that closes, every Bekenstein-saturation citation in this chain remains conditional on the model equality.