ClockRateBundle
plain-language theorem explainer
Packages the B3 delivery for surface gravity κ: near-horizon Rindler normal form together with the constant Euclidean angular rate dθ/dτ_E = κ. Horizon and holography arguments cite it when they need rate-only typing without importing period closure. It is a Prop-valued structure; constructors fill the fields from the Rindler hypothesis and the derivative identity on θ = κ τ_E.
Claim. For a real parameter $\kappa$, the clock-rate bundle asserts two facts: (i) the near-horizon geometry admits Rindler normal form with surface gravity $\kappa > 0$, and (ii) the Euclidean angular coordinate $\theta(\tau_E) = \kappa \tau_E$ satisfies $\frac{d\theta}{d\tau_E} = \kappa$ for every Euclidean time $\tau_E$.
background
This module types only what B3 delivers: near-horizon Rindler geometry makes the continued Euclidean angle advance at rate $\kappa$ per unit Euclidean time. It does not assert the $2\pi$ closure period; that is B2's output (deficit-free Euclidean period and turn-ratio unity). The legacy horizon-rate socket $\kappa = 1/R$ is a separate Schwarzschild normalization for the Clausius bridge and must not be conflated with this bundle.
Near-horizon Rindler form is the model hypothesis that a Killing horizon with surface gravity $\kappa > 0$ admits adapted coordinates $(\rho, \tau)$ near the bifurcation surface with local metric coefficient $\kappa$ on the static Killing sector. No thermality, KMS condition, or entropy-area law is imported. The Euclidean angle after continuation is the pure product $\theta = \kappa \tau_E$; its derivative identity is elementary calculus and needs no period input.
proof idea
Definitional Prop structure, not a proved theorem. Two fields: the Rindler normal-form hypothesis at $\kappa$, and the universal rate statement that the derivative of the Euclidean angle in Euclidean time equals $\kappa$ everywhere. Downstream constructors (every Rindler form yields the rate bundle) inhabit it by copying the Rindler witness and applying the derivative identity for $\theta = \kappa \tau_E$.
why it matters
This is the typed B3 bundle: forced-conditional on near-horizon Rindler form, rate-only. It is the carrier that local recognition horizon cuts invoke when they lift a local horizon context to a clock-rate bundle via the Rindler constructor. Sibling non-claims record that the bundle is silent on the period $T = 2\pi/\kappa$, and that turn-ratio unity at the B2-forced period is a B1/B2 linkage that does not use B3. Keeping rate separate from period closure is the point of the LEG-B panel split: B3 delivers $d\theta/d\tau_E = \kappa$; B2 delivers the deficit-free period and turn-ratio carrier. The structure therefore prevents smuggling period or Clausius-normalization content into rate-only arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.