Holography Horizon One Sided Cut Domino Face Capacity

The domino face capacity

A black hole horizon, in the Recognition Science account, is a boundary that hides its interior from the outside. The framework models this as a one-sided causal cut: the exterior observer cannot condition on the causally-hidden interior, so the accessible reading of the horizon is a trace over the hidden region. The declaration domino_face_capacity is a theorem in the framework's machine-checked library of formal theorems. It states that for the physical domino face, a cube-face pixel with two private and two shared vertices, the number of distinct accessible states is exactly 16, which is 2^4, hence four bits per pixel.

The proof is exact linear algebra over the field ZMod 2, the two-element field of bits. A globally-closed recognition ledger, one balanced-loop parity constraint, is split by the cut into four parts: exterior private vertices, the seam of shared vertices, interior private vertices, and the rest of the closed universe. The theorem margA_card shows the exterior's accessible marginal is its full vertex count, and margA_bits converts that count to bits. For the domino face, a = 2 private exterior vertices plus s = 2 shared seam vertices gives 2^(2+2) = 16 states, so Nat.log2 of 16 is 4. The declaration kappa_per_pixel_is_four records this same result as a logarithm.

The deeper content is the double-posting of the seam. The theorems seam_posted_by_A and seam_posted_by_B prove that each side independently realizes all 2^s seam readings, meaning the severed-edge records are privately duplicated, one full copy on each side. Summing the two sides therefore double-posts the seam, and seam_identity shows the sum exceeds the joint by exactly the seam bit count. At the domino face, the seam is 2 bits per severed edge, matching the measured gluing law D(m+n) − D(m) − D(n) = 2. This is the additive κ = 4 reading of horizon entropy, forced by the one-sided cut rather than chosen.

What the theorem does not claim is that a physical horizon is in fact a one-sided causal cut. That identification is the explicit named premise HorizonIsOneSidedCut / HorizonSumsPerSide, a hypothesis, not a proved result. The theorem proves the mathematical forcing: a one-sided trace implies private duplicated seam implies additive reading. The physical input remains an assumption, with a sharp falsifier: if horizon entropy were the joint marginal, the interior accessible, then κ = 1 and S = A/4 fails by a factor of 4.

/-- The domino face marginal is `2^4 = 16` closed-config readings, the full raw face
capacity — the symbolic form of `SharedCutMarginal.domino_leftFace_support_card`. -/
theorem domino_face_capacity (r : ℕ) :
    ((closedSet 2 2 2 r).image projA).card = 16 := by
  rw [margA_card]; norm_num

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

/-- **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 named hypothesis. The theorem does not derive the Bekenstein entropy formula S = A/4; it only fixes the per-pixel capacity at four bits. The theorem does not claim the joint marginal reading κ = 1 is impossible in general, only that it contradicts the one-sided-cut premise.

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: