Holography Horizon Clock Rate

Horizon clock rate

In general relativity, surface gravity κ measures the strength of a black hole's pull at its horizon. Near that horizon, time behaves strangely: an observer far away sees clocks there run slower and slower. The holography horizon clock rate is the rate at which a recognition clock, a discrete record of events, advances when viewed through the Euclidean continuation, a mathematical trick that turns time into a spatial angle. The framework's module proves that this angular advance happens at exactly the rate κ per unit of Euclidean time.

The core result is a pure calculus statement. The module defines the Euclidean angle as θ = κ τ_E, where τ_E is Euclidean time. It then proves, as a theorem, that the derivative dθ/dτ_E equals κ for all τ_E. This is the B3 rate-only typing: it establishes the rate of the clock's advance, but deliberately says nothing about when the clock completes a full turn. That closure period, 2π/κ, is the output of a separate part of the framework, B2, which handles the period and the turn ratio.

The module is careful about what it does not claim. It does not import thermality, KMS conditions, or any entropy-area law. It only records the existence of the rate parameter κ in a near-horizon Rindler normal form, a coordinate system adapted to a Killing horizon. The structure NearHorizonRindlerForm simply requires κ > 0. From that premise, the theorem clockRateBundle_of_rindler shows that every such Rindler form yields the full rate bundle: the rate law holds for all Euclidean times.

In Recognition Science, this rate law is one leg of a larger argument about how recognition events behave near a horizon. The framework's library, a machine-checked collection of formal theorems, proves the rate law and bundles it with the Rindler premise. The module also includes a fence theorem, period_is_b2_output_not_b3_input, which states that the full-turn time 2π/κ is definitionally the B2 carrier output, not an input here. This separation keeps the rate-only claim clean and prevents conflation with the legacy Schwarzschild normalization κ = 1/R, which is a separate socket for the Clausius bridge.

What this establishes in plain language: near a horizon, the recognition clock ticks at a rate set by surface gravity, and that rate law is a proved theorem, not an assumption. The module also grounds a hyperbolic mismatch class, a positive real eigenvalue not equal to ±1, which connects to the framework's SeamTransferCore. The practical consequence is that the rate of the clock is fixed and knowable, while the full period remains a separate, later result.

/-- **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

/-- Algebraic form of the rate law (the panel's `dθ/dτ_E = κ`). -/
theorem euclideanAngle_deriv_eq (kappa : ℝ) (hk : 0 < kappa) (tauE : ℝ) :
    deriv (euclideanAngle kappa) tauE = kappa :=
  (euclideanAngle_rate kappa hk tauE).deriv

/-- **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

/-- Every Rindler form yields the rate bundle. -/
theorem clockRateBundle_of_rindler {kappa : ℝ} (h : NearHorizonRindlerForm kappa) :
    ClockRateBundle kappa where
  rindler := h
  rate := fun tauE => euclideanAngle_deriv_eq kappa h.kappa_pos tauE

/-- **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

/-- The Clausius-bridge normalization `κ = 1/R` is an independent MODEL socket; it is
not part of the B3 rate-only delivery above. -/
theorem legacy_horizonRate_is_separate (kappa R : ℝ) :
    DeficitFreePeriod.HorizonRate kappa R ↔ kappa = 1 / R :=
  Iff.rfl

What this page does not claim

This module does not assert the 2π closure period; that is B2's output. The rate law alone does not imply thermality or any entropy-area relation. The legacy HorizonRate normalization κ = 1/R is not part of this B3 rate-only delivery.

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: