Pith. sign in
module module high

IndisputableMonolith.Holography.HorizonClockRate

show as:
view Lean formalization →

Near-horizon Rindler normal form records that a Killing horizon with surface gravity κ > 0 admits adapted coordinates (ρ, τ) carrying a local rate parameter κ on the static Killing sector. The module packages that rate into a clock-rate bundle and Euclidean angle, and marks the geometric period as a B2 output, without importing thermality, KMS, or entropy-area laws. Horizon-cut work cites it to keep geometric κ separate from the deficit-free period chain. Structure is definitional packaging plus short separation lemmas.

claimA Killing horizon with surface gravity $\kappa > 0$ admits near-bifurcation adapted coordinates $(\rho, \tau)$ whose static Killing sector carries the local metric coefficient $\kappa$. The module defines the associated Euclidean angle, a clock-rate bundle from the Rindler data, and records that the geometric period $2\pi/\kappa$ is a B2 output (not a B3 input), with turn-ratio unity at that period and the clock-rate bundle silent on the period identity.

background

In the holography stack, LEG-B derives the deficit-free period $\beta = 2\pi/\kappa$ from holonomy closure and prices the per-cycle recognition cost as $C(T) = J(\kappa T / 2\pi)$, with $J(x) = (x + x^{-1})/2 - 1$ the T5 cost. Upstream modules DeficitFreePeriod, TurnRatioCarrier, and SeamLedgerDischarge establish that $\beta$ is the unique zero of the per-cycle seam cost under conserving seam pricing.

This module isolates the geometric rate parameter itself. Near-horizon Rindler normal form is a MODEL premise: existence of adapted coordinates with coefficient $\kappa$, nothing more. No KMS condition, Unruh temperature, or area law is assumed. Sibling objects include the Euclidean angle (and its rate and derivative identities), a clock-rate bundle assembled from the Rindler data, a hyperbolic mismatch class, and markers that the period is a B2 output rather than a B3 input.

The local setting is deliberately thin: record that a clock rate exists and stays silent on the period identity, so later legs can import $\kappa$ without smuggling thermality.

proof idea

This is largely a definition and packaging module, not a deep derivation. Near-horizon Rindler form and the clock-rate bundle are data carriers for the geometric rate. Assembly lemmas build the bundle from the Rindler normal form; Euclidean-angle lemmas relate the angle and its derivative to $\kappa$. Short theorems mark the period as a B2 output (not a B3 input), assert turn-ratio unity at the B2 period, and record that the clock-rate bundle is silent on the period identity. A legacy separation lemma keeps an older horizon-rate name from collapsing into this package. Analytic content is inherited from the upstream period and turn-ratio facts.

why it matters in Recognition Science

LocalRecognitionHorizonCut imports this module to join LEG-A one-sided cuts with posted-record heat and the B2 period chain on one shared context. By exposing only the rate parameter and refusing thermality imports, it keeps geometric $\kappa$ available to horizon-sum and Clausius-record arguments without begging the Bekenstein question. It sits on the LEG-B spine (deficit-free period, turn-ratio carrier, seam-ledger discharge) and feeds the local recognition horizon cut that double-posts the seam. Framework landmarks in play are the T5 $J$-cost on the real turn ratio and the eight-tick cycle priced through that cost; the module itself does not force $D = 3$ or the alpha band.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (11)