euclideanAngle_rate
plain-language theorem explainer
After Euclidean continuation the horizon angle is the linear map θ = κ τ_E, and its derivative with respect to Euclidean time is exactly the surface gravity κ at every τ_E. Horizon-clock and Rindler analyses cite this as the B3 rate law. The proof is pure calculus: unfold the definition and apply the constant-multiple rule to the identity map.
Claim. For every surface gravity $\kappa > 0$ and every Euclidean time $\tau_E \in \mathbb{R}$, the map $\tau_E \mapsto \kappa \, \tau_E$ is differentiable at $\tau_E$ with derivative $\kappa$. Equivalently, $d\theta/d\tau_E = \kappa$ holds pointwise, where $\theta(\tau_E) = \kappa \, \tau_E$ is the continued Euclidean angle.
background
This module types only the B3 delivery of the horizon clock: near-horizon Rindler geometry makes the continued Euclidean angle advance at rate κ per unit Euclidean time. It deliberately does not assert 2π closure; that period is B2's output (deficit-free Euclidean period and turn-ratio unity). The legacy Schwarzschild socket κ = 1/R is a separate Clausius-bridge normalization and must not be conflated with this rate.
The Euclidean angle is defined by pure multiplication: θ(κ, τ_E) := κ · τ_E. The positivity hypothesis κ > 0 matches the geometric regime in which surface gravity is a positive scale for the Rindler wedge. No ledger period, turn ratio, or deficit data enters the signature.
Downstream, the algebraic form of the same law is obtained by reading off the derivative from this HasDerivAt witness.
proof idea
One short tactic proof. Unfold the definition of the Euclidean angle to κ · τ_E. Apply the standard calculus fact that the identity map has derivative 1 at τ_E, then multiply by the constant κ (hasDerivAt_id.const_mul). A simpa closes the goal. No geometric or holographic lemmas are invoked; the rate is definitional calculus.
why it matters
This is the formal B3 rate theorem on the 2026-07-06 holography panel: dθ/dτ_E = κ with no period input. It feeds the sibling algebraic restatement that deriv(θ) = κ, which is the form the panel quotes, and sits under the typed B3 clock-rate bundle conditioned on near-horizon Rindler form.
In the broader Recognition holography stack it separates rate typing (B3) from period typing (B2). That separation keeps the eight-tick and deficit-free period story from being smuggled into a pure Rindler derivative. Anyone building clock-rate bundles, turn-ratio carriers, or seam-ledger discharge at the horizon cites this as the calculus spine of the continued recognition clock.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.