Cosmology Polarized Birth Interface Spine

The spine and its claims

A recognition ledger, a discrete record of events, can assign a charge to each cell in a growing diamond or octahedron: positive on one side, negative on the other, zero on the central column. The boundary where the charge changes is the active interface, the set of edges the ledger must distinguish. The question is where that interface can live as the shape grows.

In two dimensions, the diamond's cells form a square grid with a central column at x = 0. The charge flips only when a step crosses that column, so every edge connecting cells of different charge must touch it. The proof shows that the entire active interface is confined to this spine, a line of cells whose length is 2t + 1 at radius t, while the full diamond contains 2t² + 2t + 1 cells. The interface fraction therefore falls as roughly 1/t: the cost of recognition localizes to a curve, not the area.

The same structure holds in three dimensions, the dimension the forcing chain selects. The octahedron's spine is the disk x = 0, a two-dimensional diamond with 2t² + 2t + 1 cells, while the full octahedron has a volume of order t³. Every charge-flipping edge touches this disk, and the interface fraction again falls as 1/t. The active surface sits on a codimension-one set, a fact proved as a theorem in the machine-checked library of formal theorems, not as a numerical observation.

Together with the companion result that the carried state is exactly three locked domains for every radius, the spine confinement closes both halves of a sub-extensivity picture: the carried domains are constant in size, and the active interface is a vanishing fraction of the world. In plain terms, the ledger's work does not spread through the volume; it concentrates on a thin boundary. This is a structural claim about where cost lives, not a statement about any particular physical material.

What the proof does not do is count the exact number of interface edges. The spine confinement and the spine cardinality are theorems, but the precise edge count, numerically 8t - 4 ordered edges in two dimensions, would require a separate enumeration of the edge set. The sub-extensivity content, that the cost lives on a lower-dimensional surface, is exactly the spine confinement plus the cardinality, and both are established.

/-- **Every active edge touches the spine.** For the polarized diamond field, any two adjacent cells
of different charge have an endpoint on the spine `x = 0`. The charge `sign(x)` flips only between
columns `x = -1, 0, 1`, and a charge-flipping adjacency must step the `x`-coordinate across `0`, so
one endpoint sits on the spine. Pure case analysis: split the `sign` on each endpoint, then the
unit-distance adjacency forces the spine. -/
theorem bichromatic_endpoint_on_spine (t : ℕ) (a b : Vtx t)
    (hadj : adj a.val b.val) (hc : polarized t a ≠ polarized t b) :
    a.val.1 = 0 ∨ b.val.1 = 0 := by
  unfold adj at hadj
  simp only [polarized] at hc
  split_ifs at hc <;> omega

/-- **The whole recognition-active interface is on the spine.** Every bichromatic edge in the
interface list (the forced distinctions the engine posts on the birth field) has an endpoint on the
spine `x = 0`. This is the exact list `InterfaceComponentBound.Diamond.mono_le_interface_succ` bounds,
now shown to be spine-confined. -/
theorem interface_on_spine (t : ℕ) :
    ∀ p ∈ (edges t).filter (fun q => decide (polarized t q.1 ≠ polarized t q.2)),
      p.1.val.1 = 0 ∨ p.2.val.1 = 0 := by
  intro p hp
  rw [List.mem_filter] at hp
  obtain ⟨hpe, hpc⟩ := hp
  rw [mem_edges] at hpe
  rw [decide_eq_true_eq] at hpc
  exact bichromatic_endpoint_on_spine t p.1 p.2 hpe hpc

/-- **The 2-D spine is `2t + 1` cells.** The interface of the birth field is confined to this
codimension-1 set (a 1-D ball), which is `Θ(t)` while the world is `Θ(t²)`. -/
theorem spine_card (t : ℕ) : (spine t).card = 2 * t + 1 := by
  rw [spine_eq_image, Finset.card_image_of_injective _ (by
    intro u v h; simpa using h)]
  rw [Int.card_Icc]
  omega

/-- **The 2-D spine is `2t + 1` cells.** The interface of the birth field is confined to this
codimension-1 set (a 1-D ball), which is `Θ(t)` while the world is `Θ(t²)`. -/
theorem spine_card (t : ℕ) : (spine t).card = 2 * t + 1 := by
  rw [spine_eq_image, Finset.card_image_of_injective _ (by
    intro u v h; simpa using h)]
  rw [Int.card_Icc]
  omega

/-- **The whole recognition-active interface is on the spine.** Every bichromatic edge in the
interface list (the forced distinctions the engine posts on the birth field) has an endpoint on the
spine `x = 0`. This is the exact list `InterfaceComponentBound.Diamond.mono_le_interface_succ` bounds,
now shown to be spine-confined. -/
theorem interface_on_spine (t : ℕ) :
    ∀ p ∈ (edges t).filter (fun q => decide (polarized t q.1 ≠ polarized t q.2)),
      p.1.val.1 = 0 ∨ p.2.val.1 = 0 := by
  intro p hp
  rw [List.mem_filter] at hp
  obtain ⟨hpe, hpc⟩ := hp
  rw [mem_edges] at hpe
  rw [decide_eq_true_eq] at hpc
  exact bichromatic_endpoint_on_spine t p.1 p.2 hpe hpc

What this page does not claim

The proof does not establish the exact number of interface edges, only their confinement to the spine. The spine confinement is a theorem about a discrete model, not a claim about any continuous physical spacetime. The result does not by itself derive the fine-structure constant or any other specific coupling constant.

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/Cosmology/PolarizedBirthInterface.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: