Holography Horizon One Sided Cut Horizon One Sided Cut Cert

The one-sided cut theorem

In physics, a horizon is a boundary that hides one side from the other. An observer outside a black hole cannot condition on events inside it. The Recognition Science framework models this asymmetry with a discrete record of events called a ledger, a bookkeeping system where every event is posted to an account. The declaration horizonOneSidedCutCert is a machine-checked theorem in the framework's library of formal theorems. It proves that when a horizon is modeled as a one-sided causal cut, the shared edge records at the cut are privately duplicated, one full copy on each side.

The theorem works with exact linear algebra over the field ZMod 2, which is arithmetic where 1 + 1 = 0. A globally closed ledger, one with a single balanced parity constraint, is split into four parts: the exterior side's private vertices, the seam of severed-edge endpoints shared by both sides, the interior side's private vertices, and the rest of the closed universe. The two regions that share the seam are the exterior side A and the interior side B. The central results, seam_posted_by_A and seam_posted_by_B, prove that each side independently realizes all 2^s possible seam readings, where s is the number of seam bits. This means the severed-edge records are posted twice, once by each side, so summing the two sides double-posts the seam.

The key identity, seam_identity, states that the bits on side A plus the bits on side B equal the bits on the joint region plus s, the seam bit count. This is the double-posting: summing the two sides overcounts the joint by exactly the seam. Given the premise that horizon entropy sums the per-side accessible marginals, the theorem horizon_record_double_posts_seam shows the horizon record exceeds the joint by the seam. At the physical domino face, where each cube-face pixel has 2 private and 2 shared vertices, the seam is 2 bits per severed edge and each pixel's accessible marginal is 4 bits, reproducing the known κ = 4 per-pixel count.

The theorem does not claim that a physical horizon is a one-sided causal cut. That identification is a named premise, HorizonIsOneSidedCut, which is strictly weaker than the prior assumption of per-pixel record additivity. The theorem proves the mathematical forcing: a one-sided trace implies private duplicated seam records, which implies the additive sum reading. The falsifier is sharp: if horizon entropy were the joint marginal, meaning the interior were accessible, then κ = 1 and S = A/4 would fail by a factor of 4.

What this changes is the status of a key assumption in the Bekenstein master plan. The additivity of per-pixel records, previously assumed, is now derived from causal one-sidedness. The theorem replaces a premise with a consequence, sharpening the framework's account of horizon entropy.

/-- Verify-target certificate handle (`#print axioms`-gated). -/
theorem horizonOneSidedCutCert : horizon_carries_one_side :=
  horizon_carries_one_side_holds

/-- **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 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

/-- **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

/-- **κ = 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 physical horizon is a one-sided causal cut, which remains a named premise. The theorem does not derive the Bekenstein bound or the full area law, only the per-pixel additive reading. The theorem does not claim that the interior is inaccessible in any absolute sense, only that the exterior observer cannot condition on it.

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: