Cosmology Polarized Birth Domains Three Le Comp Of Three Charges

Three charges, three regions

In graph theory, a connected component is a maximal group of vertices linked by edges. The declaration three_le_comp_of_three_charges is a theorem about any finite graph whose vertices carry one of three distinct labels, called charges. It states that if three specific vertices each carry a different charge, then the subgraph containing only edges between vertices of the same charge has at least three connected components. The proof is fully formalized in the framework's machine-checked library of formal theorems, with no unproved assumptions beyond the standard logical axioms.

The theorem is general: it does not depend on the graph's shape, size, or edge count. It holds for any finite graph and any labeling with three distinct values. The proof works by descent: define a height function that decreases along monochromatic edges, then show every vertex connects to one of three roots. Since the three roots carry different charges, no two can lie in the same component, forcing a count of at least three.

In Recognition Science, this theorem becomes a key support for the birth field, the configuration of charges installed at the start of each cycle in the framework's cosmological model. The birth field assigns +1 to one half of a lattice, -1 to the other half, and 0 to the dividing spine. The framework proves that this field has exactly three connected regions, regardless of how large the lattice grows. The result is called carried-state sub-extensivity: a world with Θ(t²) cells is described by just three super-regions, so the ratio of components to volume shrinks to zero.

The theorem does not claim that the three regions remain distinct forever. The framework's live engine later diffuses the spine through forced resolution, creating additional small interface components. Those are bounded by a separate interface bound, not by this theorem. The three-region result is exact only for the static birth configuration, not for the evolving system.

/-- **Three distinct charges force at least three components.** If three cells carry pairwise-distinct
charges, they lie in three distinct monochromatic components (charge is a closure invariant), so the
induced charge map on the quotient hits three values and the component count is at least 3. -/
theorem three_le_comp_of_three_charges {β : Type*} [Finite V] [DecidableEq β] (E : List (V × V))
    (c : V → β) (a b d : V) (hab : c a ≠ c b) (had : c a ≠ c d) (hbd : c b ≠ c d) :
    3 ≤ comp (E.filter (fun p => decide (c p.1 = c p.2))) := by
  classical
  set F := E.filter (fun p => decide (c p.1 = c p.2)) with hF
  haveI : Fintype (Quotient (cs F)) := Fintype.ofFinite _
  set q : Quotient (cs F) → β :=
    Quotient.lift c (fun x y h => clos_mono_charge E c (hF ▸ h)) with hq
  have hqa : q (Quotient.mk (cs F) a) = c a := rfl
  have hqb : q (Quotient.mk (cs F) b) = c b := rfl
  have hqd : q (Quotient.mk (cs F) d) = c d := rfl
  have hsub : ({c a, c b, c d} : Finset β) ⊆ Finset.image q Finset.univ := by
    intro w hw
    rw [Finset.mem_image]
    simp only [Finset.mem_insert, Finset.mem_singleton] at hw
    rcases hw with rfl | rfl | rfl
    · exact ⟨Quotient.mk (cs F) a, Finset.mem_univ _, hqa⟩
    · exact ⟨Quotient.mk (cs F) b, Finset.mem_univ _, hqb⟩
    · exact ⟨Quotient.mk (cs F) d, Finset.mem_univ _, hqd⟩
  have hcard : ({c a, c b, c d} : Finset β).card = 3 := by
    rw [Finset.card_insert_of_not_mem (by simp [hab, had]),
        Finset.card_insert_of_not_mem (by simp [hbd]), Finset.card_singleton]
  calc 3 = ({c a, c b, c d} : Finset β).card := hcard.symm
    _ ≤ (Finset.image q Finset.univ).card := Finset.card_le_card hsub
    _ ≤ (Finset.univ : Finset (Quotient (cs F))).card := Finset.card_image_le
    _ = Fintype.card (Quotient (cs F)) := Finset.card_univ
    _ = comp F := by rw [comp, Nat.card_eq_fintype_card]

/-- The forced conjugate-birth charge on the diamond: `+1` on the fine half `x > 0`, `-1` on the
coarse half `x < 0`, `0` on the `x = 0` spine. -/
def polarized (t : ℕ) (v : Vtx t) : ℤ :=
  if 0 < v.val.1 then 1 else if v.val.1 < 0 then -1 else 0

/-- **The polarized birth field has exactly 3 locked domains, every radius (2-D).** The upper bound
`≤ 3` (descent toward the three roots) meets the lower bound `≥ 3` (the three roots carry the three
distinct charges `+1`, `-1`, `0`, and charge is a closure invariant). So the carried state is exactly
3 for all `t ≥ 1`: the fine half, the coarse half, and the spine. -/
theorem polarized_components_eq_three (t : ℕ) (ht : 1 ≤ t) : comp (Fmono t) = 3 := by
  refine le_antisymm (polarized_components_le_three t ht) ?_
  exact three_le_comp_of_three_charges (edges t) (polarized t)
    ⟨(1, 0), by rw [mem_ball_iff]; omega⟩
    ⟨(-1, 0), by rw [mem_ball_iff]; omega⟩
    ⟨(0, 0), by rw [mem_ball_iff]; omega⟩
    (by simp only [polarized]; dsimp only; decide)
    (by simp only [polarized]; dsimp only; decide)
    (by simp only [polarized]; dsimp only; decide)

What this page does not claim

The theorem does not claim the three regions remain distinct under the live engine's evolution. The theorem does not claim the birth field is the only configuration with three components. The theorem does not claim the framework's cosmological model is physically verified.

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/PolarizedBirthDomains.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: