Cosmology Polarized Birth Interface Spine Card

The spine cardinality

In discrete geometry, a lattice ball of radius t is the set of integer points within a certain distance of the origin. In two dimensions with the diamond metric, that ball has area 2t² + 2t + 1. The spine is the subset of that ball where the first coordinate is zero: a vertical segment. The theorem spine_card proves this segment contains exactly 2t + 1 points. The proof is a direct computation: the spine is the image of the interval from -t to t under the map y ↦ (0, y), and the cardinality of that image is 2t + 1.

In three dimensions, the ball is an octahedron with volume given by the centered-octahedral number, Θ(t³). The spine is the disk where the first coordinate is zero, a two-dimensional diamond. The theorem spine_card for the octahedron proves this disk contains exactly 2t² + 2t + 1 points. The proof again identifies the spine as the image of the two-dimensional diamond under the map (y, z) ↦ (0, y, z), and the cardinality follows from the two-dimensional ball count. In both cases, the spine is a codimension-1 set: a curve inside an area, a surface inside a volume.

In Recognition Science, these counts carry physical meaning. The framework models a discrete ledger of recognition events, where each cell carries a charge sign. The spine is where that sign changes. The theorem interface_on_spine proves that every edge connecting cells of opposite charge has an endpoint on the spine. The charge flips only across the plane x = 0, so any adjacency that changes sign must touch that plane. Therefore the entire recognition-active interface, the set of forced distinctions, is confined to the spine.

The consequence is sub-extensivity. The interface lives on a set of size Θ(t^{d-1}) while the world has size Θ(t^d). The fraction of the world that is interface falls as 1/t. The theorem interface_subextensive states this as an inequality: the spine cardinality times the radius is at most the ball cardinality. This is a structural result, not a numerical coincidence. The cost of recognition localizes to a lower-dimensional surface, and that localization is proved exactly.

The spine_card declaration does not count the interface edges themselves. The docstring notes that the exact number of ordered edges in 2D is numerically 8t - 4, but that count is not a theorem in the library. It would require enumerating the full edge list. The theorem proves confinement to the spine and the spine's cardinality; it does not prove a separate edge count. The sub-extensivity claim rests entirely on those two proved facts.

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

/-- **Interface sub-extensivity (2-D).** The recognition-active interface of the birth field is
confined to the spine, a set of `2t + 1` cells, so `spine · t ≤ area`: the interface fraction falls
as `~ 1/t`. The cost lives on a 1-D curve while the world is the 2-D area `2t² + 2t + 1`. -/
theorem interface_subextensive (t : ℕ) (ht : 1 ≤ t) :
    (spine t).card = 2 * t + 1 ∧
      (spine t).card * t ≤ (InterfaceComponentBound.Diamond.ball t).card := by
  refine ⟨spine_card t, ?_⟩
  rw [spine_card t, LatticeBallVolume.Diamond.card_ball]
  nlinarith [ht]

What this page does not claim

The exact number of interface edges is not proved, only the spine cardinality and confinement. The spine_card theorem does not establish any property of the recognition dynamics beyond the static lattice structure. The framework does not claim that the spine is the only place where recognition activity occurs, only where charge changes.

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: