Holography Local Recognition Horizon Cut Exterior Record Length

The exterior record's length

In the Recognition Science framework, a ledger is a discrete record of events, and the framework studies which ledgers are forced by the cost of recognition. The declaration `exteriorRecord_length` is a theorem about a particular ledger: the exterior record of a local horizon cut. It states that the length of this record is exactly `a + s`, where `a` is the number of exterior-private entries and `s` is the number of seam entries. The proof is a direct simplification of the definition, so the theorem is a bookkeeping fact about the record's structure, not a physical law.

The exterior record is built by concatenating two lists: the exterior-private entries and the seam entries. Interior-private and rest-of-universe entries are traced out, meaning they are not visible in the exterior record. The theorem `exteriorRecord_length` confirms that the record's length is the sum of the two visible parts. This is the first step in showing that the exterior record's potential, a weighted sum of its bits, satisfies a discrete Clausius relation, meaning the heat exchanged along a path equals the change in potential. The length theorem is what makes that proof go through, because it ensures the record has the right shape for the bookkeeping to work.

In Recognition Science, the framework models a horizon as a cut configuration with a shared context. The context includes a one-sided cut model, which forces the horizon record to double-post the seam, and a near-horizon rate model. The exterior record is defined for any closed cut in this context. The length theorem holds for all such cuts, regardless of the specific values of the other parameters. It is a general structural fact about the exterior projection, not a claim about any particular physical system.

What the theorem does not claim is as important as what it does. It does not say anything about the interior of the cut, the rest of the universe, or any curvature or thermality. The declaration's documentation is explicit: no stress tensor, Ricci tensor, focusing law, curvature match, Unruh claim, or Einstein equation occurs in this setting. The exterior record length is a purely combinatorial statement about the visible part of a discrete ledger. It is a necessary ingredient for the record thermodynamics that follows, but it is not itself a statement about spacetime geometry or quantum fields.

theorem exteriorRecord_length {a s b r : ℕ} {kappa : ℝ}
    {H : LocalHorizonContext a s b r kappa}
    (c : LocalCut H) :
    (exteriorRecord c).length = a + s := by
  simp [exteriorRecord]

/--
The exterior-accessible record: exterior-private entries followed by seam
entries. Interior-private and rest-of-universe entries are traced out.
-/
def exteriorRecord {a s b r : ℕ} {kappa : ℝ}
    {H : LocalHorizonContext a s b r kappa}
    (c : LocalCut H) : List Bool :=
  List.ofFn (fun i : Fin a => bitReadout (c.cfg.1 i))
    ++ List.ofFn (fun j : Fin s => bitReadout (c.cfg.2.1 j))

/-- Posted exterior heat is exactly the change of record potential. -/
theorem exteriorStepHeat_eq_potential {a s b r : ℕ} {kappa : ℝ}
    {H : LocalHorizonContext a s b r kappa}
    (c c' : LocalCut H) :
    exteriorStepHeat c c' = exteriorPotential c' - exteriorPotential c := by
  exact recordFlux_eq_weight_sub _ _ (by
    rw [exteriorRecord_length, exteriorRecord_length])

What this page does not claim

The theorem does not establish any property of the interior of the cut or the rest of the universe. The theorem does not involve curvature, thermality, or the Einstein equation in any form. The theorem does not assign a physical meaning to the exterior record beyond its role in the framework's discrete bookkeeping.

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: