Holography Horizon One Sided Cut Severed Edge Seam Is Two

The doubled seam

In the Recognition Science framework, a ledger (a discrete record of events) tracks every connection between parts of a system. When a system is split by a cut, some edges are severed: they belong to both sides. The declaration severed_edge_seam_is_two proves that each side must independently record all the information on that shared seam, so the seam is posted twice, once by each side. The result is a theorem, not a choice: the mathematics forces the double posting.

The proof works with exact linear algebra over bits (the field with two elements). A closed ledger has one global constraint: the sum of all its bits must be zero. The theorem shows that even with this single constraint, each side's accessible view is full: the exterior side can realize every possible reading of the seam, and so can the interior side. Neither side can omit the seam, because the constraint does not localize onto any proper subregion. Therefore the two sides together carry two full copies of the seam.

For a specific geometry, a cube-face pixel with two private and two shared vertices on each side, the arithmetic is concrete. The exterior side has 4 bits of accessible information, the interior side has 4 bits, and the joint system has 6 bits. The sum of the two sides, 8 bits, exceeds the joint by exactly 2 bits, which is the seam. The declaration severed_edge_seam_is_two states this: each severed edge contributes 2 bits to the total, not 1. This reproduces a known gluing law, D(m+n) − D(m) − D(n) = 2, as a derived consequence rather than an assumption.

The theorem's scope is precise. It proves the mathematical forcing: a one-sided trace implies private duplicated seam records, which implies the additive reading. What it does not prove is the physical identification that a horizon is a one-sided causal cut, the premise that the exterior observer cannot condition on the interior. That premise, named HorizonIsOneSidedCut, is stated explicitly and remains a physical input, not a theorem. The falsifier is sharp: if the interior were accessible, the count would drop to 1 bit per edge and the entropy would fail by a factor of 4.

What the result changes is the status of an assumption. Earlier work had to assume that each pixel posts its own record of its four edges. This theorem derives that additivity from a weaker and more physical premise: causal one-sidedness. The double posting is not an extra rule; it is what a one-sided cut forces.

/-- **The exterior side posts a full private copy of the seam.** Tracing out the interior,
the exterior's accessible marginal realizes ALL `2^s` seam readings — a complete private copy
of every severed-edge record, reconstructed with no access to the interior. -/
theorem seam_posted_by_A (a s b r : ℕ) :
    (closedSet a s b r).image projSeam = Finset.univ := by
  apply Finset.eq_univ_of_forall
  intro gS
  refine Finset.mem_image.mpr ⟨compA (a := a) (b := b) (r := r) 0 gS,
    Finset.mem_filter.mpr ⟨Finset.mem_univ _, ?_⟩, ?_⟩
  · exact compA_closed 0 gS
  · rfl

/-- **The interior side posts a full private copy of the seam.** Symmetrically, tracing out
the exterior, the interior's accessible marginal realizes ALL `2^s` seam readings. Both sides
independently carry the severed-edge records — they are duplicated across the cut. -/
theorem seam_posted_by_B (a s b r : ℕ) :
    (closedSet a s b r).image projSeam = Finset.univ := by
  apply Finset.eq_univ_of_forall
  intro gS
  refine Finset.mem_image.mpr ⟨compB (a := a) (b := b) (r := r) gS 0,
    Finset.mem_filter.mpr ⟨Finset.mem_univ _, ?_⟩, ?_⟩
  · exact compB_closed gS 0
  · rfl

/-- **The severed-edge seam is 2 bits.** A cube-face pixel shares an edge (2 vertices) with
its neighbor: `a = b = s = 2`. The seam bit count is `s = 2`, matching the measured gluing law
`D(m+n) − D(m) − D(n) = 2` of the Phase-0 spectrometer
(`artifacts/bekenstein_phase0_spectrometer_20260702.txt`). -/
theorem severed_edge_seam_is_two (r : ℕ) :
    Nat.log2 (((closedSet 2 2 2 r).image projA).card)
        + Nat.log2 (((closedSet 2 2 2 r).image projB).card)
      = Nat.log2 (((closedSet 2 2 2 r).image projAB).card) + 2 :=
  seam_identity 2 2 2 r

/-- **GIVEN a one-sided cut, the horizon record double-posts the seam.** The horizon record
exceeds the joint boundary marginal by exactly the seam — the additive (`κ = 4`) reading,
forced by causal one-sidedness rather than assumed. -/
theorem horizon_record_double_posts_seam (a s b r horizonRecord : ℕ)
    (h : HorizonSumsPerSide a s b r horizonRecord) :
    horizonRecord = Nat.log2 (((closedSet a s b r).image projAB).card) + s := by
  rw [h]; exact seam_identity a s b r

/-- **The one-sided causal cut premise.** A horizon is a one-sided causal cut: the exterior
observer cannot condition on the causally-hidden interior, so horizon entropy is the SUM of
the two sides' accessible marginals (each side posts its own private record), NOT their joint.
This is the sole physical input; everything below is a theorem. It is strictly weaker than
`PerPixelRecordAdditivity`: additivity is *derived* from it via `seam_identity`. -/
def HorizonSumsPerSide (a s b r : ℕ) (horizonRecord : ℕ) : Prop :=
  horizonRecord
    = Nat.log2 (((closedSet a s b r).image projA).card)
      + Nat.log2 (((closedSet a s b r).image projB).card)

What this page does not claim

The theorem does not prove that a physical horizon is a one-sided causal cut; that remains a stated premise. The theorem does not derive the value of the Bekenstein-Hawking entropy coefficient from first principles. The theorem does not apply to a cut where both sides can access the full joint state.

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