Encyclopedia Holography Holography Horizon Clock Rate Euclidean Angle Rate

ARTICLE 3 claims 3 theorems

Holography Horizon Clock Rate Euclidean Angle Rate

A small theorem about a clock near a black hole horizon: the angle of its hands advances at a constant rate, and nothing more.

The rate law

In the geometry of a black hole, the region just outside the event horizon can be described by a simplified model called Rindler space. In that model, a clock held at a fixed distance from the horizon ticks at a rate that depends on how strongly gravity pulls there. The Recognition Science declaration euclideanAngle_rate formalizes one piece of that picture: it states that the continued Euclidean angle of the clock's hand, written θ, advances at a steady rate κ per unit of Euclidean time τ_E. In symbols, dθ/dτ_E = κ. This is a pure calculus statement: the angle is simply defined as θ = κ τ_E, and the derivative follows immediately.

The declaration is a theorem in the framework's machine-checked library of formal theorems. It assumes only that the surface gravity κ is positive, which is the physical condition that a horizon exists at all. It does not import any deeper physics: no thermality, no quantum field theory, no entropy-area law. The proof is a one-line application of the derivative of a linear function. The result is therefore solid but deliberately narrow.

What the declaration does not claim is just as important as what it proves. It does not assert that the angle completes a full 2π turn after any particular time. The period of the clock, the time for one full revolution, is a separate result in the framework, derived from a different principle (the B2 closure condition). The rate law here is silent on that period. It also does not identify κ with any specific physical quantity such as 1/R for a Schwarzschild radius; that identification is a separate modeling choice, not part of this theorem.

In Recognition Science, this rate law serves as one rung in a longer chain of results connecting horizon geometry to thermodynamic behavior. But taken alone, it is a modest and precise statement: near a horizon, the Euclidean clock hand sweeps at a constant angular speed. The value of that speed is set by the surface gravity, and the theorem guarantees the uniformity of the sweep, not the length of the cycle.

THEOREM euclideanAngle_rate · IndisputableMonolith/Holography/HorizonClockRate.lean
/-- **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
THEOREM clockRateBundle_silent_on_period · IndisputableMonolith/Holography/HorizonClockRate.lean
clockRateBundle_silent_on_period · IndisputableMonolith/Holography/HorizonClockRate.lean:82
/-- **Explicit non-claim:** `ClockRateBundle` carries no field about `T = 2π/κ`. -/
theorem clockRateBundle_silent_on_period {kappa : ℝ} (_h : ClockRateBundle kappa) :
    True := trivial
THEOREM period_is_b2_output_not_b3_input · IndisputableMonolith/Holography/HorizonClockRate.lean
period_is_b2_output_not_b3_input · IndisputableMonolith/Holography/HorizonClockRate.lean:72
/-- **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

What this page does not claim

The theorem does not prove that the clock completes a full cycle in time 2π/κ. The theorem does not identify κ with any specific normalization such as 1/R. The theorem does not import thermality, KMS condition, or entropy-area relations.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND