Holography Moving Recognition Horizon Cut Active Exterior Bits Extend Cut

The moving cut

A recognition ledger, a discrete record of events, can be sliced by a boundary called a cut. The cut separates exterior bits, which are visible, from interior bits, which are not. In the Recognition Science framework, a fixed cut has a known rule: the heat crossing it equals the change in the exterior potential. The declaration activeExteriorBits_extendCut extends this rule to the first genuinely moving cut, one that gains a new exterior aperture.

The theorem states a simple identity. If you take an existing cut and append one new exterior bit, the new count of active exterior bits equals the old count plus the value of the newly exposed bit. The new bit is either 0 or 1, so the count either stays the same or increases by exactly one. This is not an approximation or a limit; it is an exact statement about finite sums, proved in the machine-checked library of formal theorems.

The consequence is a clean heat rule. The heat across the moving cut, defined as the difference in active exterior bits between the old and new states, is exactly the value of the newly posted bit. If the bit is 1, the heat is one unit. If the bit is 0, the heat is zero. The framework models this as the first varying-context move: one new exterior-private aperture is appended while every old exterior and seam reading is preserved.

The theorem also preserves the structure of the context. The one-sided horizon record count increases by one, and the Rindler rate, the boost parameter attached to the context, is inherited unchanged. The new context is not postulated independently; its one-sided record law is derived from the old context's law. This makes the extension a theorem about moving boundaries, not a new assumption.

What the declaration does not claim is as important as what it proves. It does not supply a smooth interpolation between the old and new cuts. It does not introduce null covectors, Raychaudhuri's equation, Ricci curvature, or a sourced field equation. The theorem is discrete and exact, and it stops there. The framework proves the moving-cut identity; it does not derive the smooth spacetime geometry that might sit above it.

/--
The active-bit count of the extended cut is the old count plus the newly
exposed bit.
-/
theorem activeExteriorBits_extendCut {a s b r : ℕ} {kappa : ℝ}
    {H : LocalHorizonContext a s b r kappa}
    (c : LocalCut H) (x : ZMod 2) :
    activeExteriorBits (extendCut c x) =
      activeExteriorBits c + postedBitValue x := by
  unfold activeExteriorBits extendCut ofExteriorReading
  rw [Fin.sum_univ_castSucc]
  simp [compA, snocReading]
  ring

/-- Exact moving-cut heat: only the newly exposed bit is posted. -/
theorem movingStepHeat_extendCut {a s b r : ℕ} {kappa : ℝ}
    {H : LocalHorizonContext a s b r kappa}
    (c : LocalCut H) (x : ZMod 2) :
    movingStepHeat c (extendCut c x) = postedBitValue x := by
  unfold movingStepHeat
  rw [activeExteriorBits_extendCut]
  ring

@[simp] theorem extendContext_horizonRecord
    {a s b r : ℕ} {kappa : ℝ}
    (H : LocalHorizonContext a s b r kappa) :
    (extendContext H).horizonRecord = H.horizonRecord + 1 :=
  rfl

What this page does not claim

The theorem does not provide a smooth interpolation between the old and new cuts. The theorem does not introduce null covectors, Raychaudhuri's equation, Ricci curvature, or a sourced field equation. The theorem does not claim that every appended bit contributes heat; a posted 0 grows capacity without heat.

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