Holography Horizon One Sided Cut Marg A Image Univ

The one-sided cut

A physical system split by a boundary into two regions, A and B, with a shared seam between them. The whole system obeys one global rule: the sum of all its parts is zero, a parity constraint. The question is what an observer on side A, who cannot see side B, can learn about her own region. The theorem margA_image_univ, part of a machine-checked library of formal theorems, answers that the accessible record on side A is complete: every possible configuration of A's private vertices and the seam appears in the global set of allowed states. The single global constraint does not restrict what A can see at all.

The proof works by construction. For any desired configuration on A and the seam, one can fill in the rest of the universe with a compensating pattern so the global sum stays zero. This construction, called compA, shows the projection from the full set of closed configurations onto A's part is surjective. The same argument applies to side B alone and to the union of A and B. Each side's accessible marginal is its full vertex count, and the seam itself is fully realized by each side independently. This is the mathematical heart of the result: a one-sided trace over a hidden interior does not erase information on the visible side.

The consequence is a counting identity. If side A has a private vertices and the seam has s vertices, then A's marginal has 2^(a+s) states, and B's has 2^(s+b). The joint marginal of A and B together has 2^(a+s+b) states. Summing the two sides' counts gives 2^(a+s) times 2^(s+b), which exceeds the joint count by a factor of 2^s. In logarithmic terms, bits A plus bits B equals bits of the union plus s. The seam is double-posted: each side carries its own full copy of the seam record, so adding the two sides counts the seam twice.

In Recognition Science, this double-posting is what forces the additive reading of horizon entropy, the κ = 4 per-pixel count. The framework models a horizon as a one-sided causal cut: the exterior observer cannot condition on the causally-hidden interior, so the accessible record is a trace over the interior. The theorem proves that each side's trace independently realizes every seam bit, so the horizon record exceeds the joint record by exactly the seam. At the physical domino face, where each pixel has two private and two shared vertices, the seam is two bits per severed edge and each pixel's accessible marginal is four bits.

What the declaration does not claim is the physical identification itself. The theorem proves a conditional: if horizon entropy sums the per-side accessible marginals, then the horizon record double-posts the seam. The premise that a horizon is a one-sided causal cut is stated as an explicit assumption, not derived. The falsifier is sharp: if the interior were accessible, the joint marginal would give κ = 1 and the area law would fail by a factor of four.

/-- **Exterior side is fully readable.** Every exterior-side reading extends to a closed
configuration, so the marginal image is all of `2^(a+s)`. -/
theorem margA_image_univ (a s b r : ℕ) :
    (closedSet a s b r).image projA = Finset.univ := by
  apply Finset.eq_univ_of_forall
  rintro ⟨gA, gS⟩
  refine Finset.mem_image.mpr ⟨compA gA gS, Finset.mem_filter.mpr ⟨Finset.mem_univ _, ?_⟩, ?_⟩
  · exact compA_closed gA gS
  · rfl

/-- Exterior-side accessible marginal in bits: `a + s`. -/
theorem margA_bits (a s b r : ℕ) :
    Nat.log2 (((closedSet a s b r).image projA).card) = a + s := by
  rw [margA_card, Nat.log2_eq_log_two]; exact Nat.log_pow one_lt_two _

theorem margB_bits (a s b r : ℕ) :
    Nat.log2 (((closedSet a s b r).image projB).card) = s + b := by
  rw [margB_card, Nat.log2_eq_log_two]; exact Nat.log_pow one_lt_two _

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

/-- **κ = 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; that identification is an explicit premise, not a derived result. The declaration does not establish the Bekenstein area law itself, only the counting identity that supports one of its terms. The result does not apply to cuts where the two sides can exchange information across the seam.

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: