Holography Horizon Clock Rate Euclidean Angle Deriv Eq

The rate law

In the study of horizons, a useful coordinate system is the Rindler frame, which describes what an observer accelerating at a constant rate sees. Near a horizon, this frame has a special property: a quantity called surface gravity, written κ, sets the pace of a clock. The Recognition Science declaration euclideanAngle_deriv_eq establishes the precise rate: the continued Euclidean angle θ advances at rate κ per unit Euclidean time τ_E, so dθ/dτ_E = κ.

The theorem is a pure calculus statement. It defines the Euclidean angle as θ = κ τ_E, then proves its derivative is κ. The proof uses only the derivative of the identity function multiplied by a constant; no physics is imported. The declaration's full form is: for any positive κ and any τ_E, the derivative of (κ τ_E) with respect to τ_E equals κ.

The framework labels this the B3 rate-only typing. It deliberately types only what the near-horizon geometry delivers: the rate. It does not assert the 2π closure period, the time for a full turn. That period, 2π/κ, is the output of a separate module called B2, which handles the deficit-free period and the turn ratio. The rate law alone cannot pin down a closure time; the full-turn time is definitionally the B2 carrier output, not an input here.

In Recognition Science, this rate law is one leg in a chain that connects horizon geometry to a recognition clock. The framework models the horizon as a place where a discrete record of events, a ledger, advances. The theorem says the clock's hand moves at a steady angular speed near the horizon, but it is silent on when the hand completes a circle. That silence is explicit: the bundle of properties that follows from the Rindler form carries no field about the period.

The declaration also separates itself from an older normalization. A legacy socket sets κ = 1/R for a Schwarzschild radius R, but that is an independent model choice, not part of this rate-only delivery. The theorem proves the derivative; it does not prove thermality, KMS condition, or entropy-area law. Those are absent from the module by design.

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

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

What this page does not claim

The theorem does not assert the 2π closure period for a full turn. The theorem does not import thermality, KMS condition, or entropy-area law. The theorem does not establish the legacy Schwarzschild normalization κ = 1/R.

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: