Encyclopedia Holography Holography Horizon One Sided Cut Horizon Record Double Posts Seam

ARTICLE 4 claims 4 theorems

Holography Horizon One Sided Cut Horizon Record Double Posts Seam

A theorem about counting bits on a horizon shows why a shared edge gets recorded twice, once from each side, when one side of the cut is hidden.

Verify this page

The double-posted seam

In the Recognition Science framework, a ledger (a discrete record of events) keeps track of information at a boundary. The declaration horizon_record_double_posts_seam proves a precise counting fact about such a boundary when it is cut into two regions. The setup is a global ledger with a single balance constraint, split by a cut into an exterior side, an interior side, and a seam of shared vertices between them. The theorem states that if the horizon record sums the accessible readings from each side, then that record exceeds the joint reading of both sides together by exactly the number of seam bits.

The proof is a piece of linear algebra over the field with two elements. Each side's accessible marginal is its full vertex count, and each side independently realizes every possible seam reading. Summing the two sides therefore double-posts the seam: a shared edge appears once in the exterior's record and once in the interior's record. The identity seam_identity expresses this as an equation: bits of side A plus bits of side B equals bits of the union plus s, where s is the seam size. At the physical domino face, where each pixel has two private and two shared vertices, this gives two bits per severed edge and four bits per pixel, matching the measured gluing law.

What the theorem does not claim is that a horizon is in fact a one-sided causal cut. That identification, the premise that the exterior observer cannot condition on the hidden interior, is a named assumption, HorizonSumsPerSide. The theorem proves the mathematical consequence: given that premise, the additive reading follows. The falsifier is sharp: if the interior were accessible, the joint marginal would give a factor of four different entropy. The framework derives additivity from causal one-sidedness rather than assuming it, but the physical input itself remains a stated premise, not a proved result.

THEOREM horizon_record_double_posts_seam · IndisputableMonolith/Holography/HorizonOneSidedCut.lean
horizon_record_double_posts_seam · IndisputableMonolith/Holography/HorizonOneSidedCut.lean:282 
/-- **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
THEOREM seam_posted_by_A · seam_posted_by_B · IndisputableMonolith/Holography/HorizonOneSidedCut.lean
seam_posted_by_A · IndisputableMonolith/Holography/HorizonOneSidedCut.lean:228 
/-- **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
seam_posted_by_B · IndisputableMonolith/Holography/HorizonOneSidedCut.lean:240 
/-- **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
THEOREM seam_identity · IndisputableMonolith/Holography/HorizonOneSidedCut.lean
seam_identity · IndisputableMonolith/Holography/HorizonOneSidedCut.lean:259 
/-- **The double-posting identity (in bits).** Summing the two sides' accessible marginals
overcounts the joint boundary marginal by **exactly the seam bit count `s`**:
`(a+s) + (s+b) = (a+s+b) + s`. The seam is posted once by each side. This is the symbolic,
all-sizes generalization of `SharedCutMarginal.sum_of_marginals_overcounts_joint_by_shared_bits`
(the `N = 3` `decide` fact). -/
theorem seam_identity (a s b r : ℕ) :
    Nat.log2 (((closedSet a s b r).image projA).card)
        + Nat.log2 (((closedSet a s b r).image projB).card)
      = Nat.log2 (((closedSet a s b r).image projAB).card) + s := by
  rw [margA_bits, margB_bits, margAB_bits]; omega
THEOREM severed_edge_seam_is_two · kappa_per_pixel_is_four · IndisputableMonolith/Holography/HorizonOneSidedCut.lean
severed_edge_seam_is_two · IndisputableMonolith/Holography/HorizonOneSidedCut.lean:292 
/-- **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
kappa_per_pixel_is_four · IndisputableMonolith/Holography/HorizonOneSidedCut.lean:302 
/-- **κ = 4: each pixel's accessible marginal is the full 4 bits.** The exterior-side pixel
(`a = 2` private + `s = 2` seam) realizes all `2^4 = 16` readings — reproducing
`SharedCutMarginal.domino_leftFace_support_card = 16` symbolically. Each pixel posts its own
4-edge record, and summing over pixels double-posts each shared edge: this is `κ = 4`. -/
theorem kappa_per_pixel_is_four (r : ℕ) :
    Nat.log2 (((closedSet 2 2 2 r).image projA).card) = 4 := by
  rw [margA_bits]

What this page does not claim

The theorem does not prove that a horizon is a one-sided causal cut; that is a named premise. The theorem does not derive the value of the Bekenstein-Hawking entropy coefficient from first principles. The theorem does not apply to boundaries where both sides are accessible to the observer.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND