Holography Local Recognition Horizon Cut Euclidean Period Is Least For Context

The least period

The declaration euclideanPeriod_isLeast_for_context is a theorem in a machine-checked library of formal theorems. It states a property of a mathematical model, not a direct fact about physical spacetime. The model describes a horizon as a discrete record of events, a ledger, and the theorem concerns the period of a boost, a transformation that mixes time and space coordinates near a horizon.

In this model, a ledger, a discrete record of events, has a cost associated with how it changes. A deficit-free period is a return time after which the ledger's cost shows no net change. The theorem proves that the euclideanPeriod, the boost return period attached to the model's context, is the least positive such period. Formally, it establishes that euclideanPeriod kappa is the smallest positive T for which the deficit cost of kappa * T is zero.

The result is a theorem about the model because it follows from the model's own definitions and premises, which include a one-sided cut configuration and a near-horizon rate form. The library proves this without importing any premise about thermal equilibrium (KMS condition) or entropy. The theorem's conclusion is a property of the model's structure, not an independent physical law.

What the theorem does not claim is important. It does not claim that this period corresponds to a physical temperature or that the model describes Unruh radiation. It does not involve a stress tensor, Ricci tensor, focusing law, or the Einstein equation. The model's exterior record only sees the boundary and seam bits; interior and rest-of-universe data are traced out. The physical identification of the posted flux with horizon heat is a separate modeling choice, not part of this theorem.

/--
The boost return period attached to a local-horizon context is the least
positive deficit-free period. This imports no KMS or entropy premise.
-/
theorem euclideanPeriod_isLeast_for_context {a s b r : ℕ} {kappa : ℝ}
    (H : LocalHorizonContext a s b r kappa) :
    IsLeast {T : ℝ | 0 < T ∧ deficitCost (kappa * T) = 0}
      (euclideanPeriod kappa) :=
  euclideanPeriod_isLeast kappa H.rindler.kappa_pos

/--
The boost return period attached to a local-horizon context is the least
positive deficit-free period. This imports no KMS or entropy premise.
-/
theorem euclideanPeriod_isLeast_for_context {a s b r : ℕ} {kappa : ℝ}
    (H : LocalHorizonContext a s b r kappa) :
    IsLeast {T : ℝ | 0 < T ∧ deficitCost (kappa * T) = 0}
      (euclideanPeriod kappa) :=
  euclideanPeriod_isLeast kappa H.rindler.kappa_pos

What this page does not claim

This theorem does not claim any physical temperature or Unruh effect. This theorem does not involve the Einstein equation or any curvature premise. This theorem does not claim the model's period is the observed Hawking period.

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/LocalRecognitionHorizonCut.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: