Holography Horizon Clock Rate Near Horizon Rindler Form

What the horizon rate declaration establishes

In general relativity, a Killing horizon (a boundary where a time-translation symmetry becomes lightlike) has a surface gravity, a number that measures how strongly the horizon holds onto things. The declaration NearHorizonRindlerForm in the Recognition Science library records the existence of this rate parameter, named kappa, and asserts it is positive. It is a ledger, a discrete record of events, entry: there exists a rate; it does not import any physics about heat, quantum fields, or entropy.

The geometric premise is a Rindler normal form: near the horizon, adapted coordinates make the local metric coefficient equal to kappa on the static Killing sector. This is a modeling choice, not a derived theorem. What the library proves is the consequence for a clock: the continued Euclidean angle theta advances at rate kappa per unit Euclidean time, written dtheta/dtau_E = kappa. The proof is pure calculus on the definition theta = kappa * tau_E. Every Rindler form yields this rate bundle, a package containing the form and the rate law.

The declaration is deliberately silent on the period. It does not assert the full-turn time 2*pi/kappa; that closure is a separate output. The library includes an explicit fence theorem stating that the rate law alone does not pin a closure time. A second theorem shows that at the B2-forced period, the turn ratio is unity, but that linkage does not use this B3 rate. The declaration also carries no field about the period at all, a silence recorded as a theorem that is trivially true.

In Recognition Science, this is the B3 delivery: it types the rate only. The legacy Schwarzschild normalization kappa = 1/R, used in a Clausius bridge, is an independent modeling socket, not part of this rate-only bundle. The physical commitment that the mismatch leg is a positive real eigenvalue, not complex or unit, is a hypothesis or model, not a theorem of this framework.

What a reader can now see: the declaration pins the angular rate to the surface gravity, and it does so without claiming the period, thermality, or the entropy-area law. The consequence is that any further claim about horizon periodicity must come from a different, later leg of the framework, not from this rate entry.

/-- **Near-horizon Rindler normal form (MODEL).** A Killing horizon with surface
gravity `κ > 0` admits adapted coordinates `(ρ, τ)` near the bifurcation surface with
local metric coefficient `κ` on the static Killing sector. This module records only the
existence of the rate parameter; no thermality, KMS, or entropy-area law is imported. -/
structure NearHorizonRindlerForm (kappa : ℝ) : Prop where
  kappa_pos : 0 < kappa

/-- **B3 rate (THEOREM).** The continued recognition clock advances Euclidean angle at
rate `κ`: `dθ/dτ_E = κ` for all `τ_E`. Pure calculus on `θ = κ τ_E`; no period input. -/
theorem euclideanAngle_rate (kappa : ℝ) (hk : 0 < kappa) (tauE : ℝ) :
    HasDerivAt (euclideanAngle kappa) kappa tauE := by
  unfold euclideanAngle
  simpa using (hasDerivAt_id (x := tauE)).const_mul kappa

/-- **Fence theorem (THEOREM).** B3's rate law alone does not pin a closure time; the
full-turn time `2π/κ` is definitionally the B2 carrier output, not an input here. -/
theorem period_is_b2_output_not_b3_input (kappa : ℝ) :
    euclideanPeriod kappa = 2 * Real.pi / kappa := rfl

/-- **Explicit non-claim:** `ClockRateBundle` carries no field about `T = 2π/κ`. -/
theorem clockRateBundle_silent_on_period {kappa : ℝ} (_h : ClockRateBundle kappa) :
    True := trivial

What this page does not claim

The declaration does not assert the 2*pi/kappa period or any closure time. It does not import thermality, KMS, or the entropy-area law. The legacy Schwarzschild normalization kappa = 1/R is not part of this rate-only bundle.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Holography/HorizonClockRate.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: