NearHorizonRindlerForm
plain-language theorem explainer
Near-horizon Rindler normal form is the model hypothesis that surface gravity κ is strictly positive. Holography and local-horizon constructions cite it as the sole B3 geometric premise before any angular-rate identity. It is a Prop-structure with one field (positivity of κ), not a derived existence theorem.
Claim. The near-horizon Rindler normal form at surface gravity $\kappa \in \mathbb{R}$ is the proposition that $\kappa > 0$. In adapted coordinates $(\rho, \tau)$ near a Killing bifurcation surface this $\kappa$ is the local metric coefficient on the static Killing sector; the structure records only that rate parameter.
background
Module HorizonClockRate isolates the B3 delivery: near-horizon Rindler geometry makes the continued Euclidean angle advance at rate $\kappa$ per unit Euclidean time, i.e. $d\theta/d\tau_E = \kappa$. It deliberately does not assert $2\pi$ closure; that period is B2 output (DeficitFreePeriod.euclideanPeriod, turn-ratio unity). The legacy Schwarzschild socket $\kappa = 1/R$ is a separate Clausius-bridge normalization and must not be conflated with this rate-only typing.
A Killing horizon with surface gravity $\kappa > 0$ admits Rindler-adapted coordinates $(\rho, \tau)$ near the bifurcation surface. The structure packages only the positivity of that coefficient. No thermality, KMS condition, or entropy-area law is imported. Downstream, the Euclidean angle is defined by $\theta = \kappa \tau_E$, so positivity of $\kappa$ is exactly the hypothesis needed to differentiate that map.
proof idea
Definitional Prop-structure, not a proved theorem. The single field is the inequality $0 < \kappa$. No tactics, no upstream lemmas are applied at the declaration site; consumers unpack .kappa_pos when they need the positivity hypothesis for differentiation of the Euclidean angle.
why it matters
This is the typed B3 geometric premise for the whole HorizonClockRate stack. ClockRateBundle is forced-conditional on it: the bundle pairs the Rindler form with the rate law $\forall \tau_E,, \partial_{\tau_E}(\kappa\tau_E)=\kappa$. The constructor clockRateBundle_of_rindler lifts any instance to that bundle via euclideanAngle_deriv_eq. Outside the module, LocalHorizonContext joins the one-sided-cut model, posted-record carrier dimensions, and this near-horizon rate model, still without thermality or curvature premises.
In the Recognition holography panel it separates rate delivery (B3) from period delivery (B2), so the eight-tick / deficit-free period story cannot smuggle a $2\pi$ closure in through the Rindler socket. It does not touch T5–T8 forcing, RCL, or the mass ladder; its role is local geometric hygiene for horizon clock rates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.