Encyclopedia Cosmology Cosmology Polarized Birth Domains Polarized Carried Subextensive

ARTICLE 3 claims 3 theorems

Cosmology Polarized Birth Domains Polarized Carried Subextensive

A pattern of plus and minus charges installed at the start of a cosmic cycle can be stored as just three regions, no matter how large the universe grows.

Verify this page

The carried birth field

A ledger (a discrete record of events) in the Recognition Science framework tracks how much information a growing universe must keep. When a new cycle begins, the framework installs a simple charge pattern: a fine half with value +1, a coarse half with value −1, and a central spine of zeros. The question is how many separate regions the framework must remember to store this pattern as it expands.

The answer, established as a theorem in the framework's machine-checked library, is exactly three, independent of the radius. The positive half forms one connected region, the negative half another, and the spine a third. A universe with Θ(t²) cells in two dimensions, or Θ(t³) in three, is therefore carried by a constant number of super-regions. The fraction of stored components relative to volume shrinks to zero as the universe grows, the sharpest possible form of sub-extensivity.

The proof works by assigning each cell a height that decreases along edges of the same charge, forcing every cell to descend to one of three roots: (1,0), (−1,0), or (0,0) in two dimensions, with the analogous triple in three. Since every cell connects to a root and there are only three roots, the component count cannot exceed three. A separate argument shows it cannot be fewer, because the three charge values are mutually distinct.

In Recognition Science, this makes the North-Star claim "carry each region at the coarsest φ-rung its recognition allows" exact for the birth configuration. The result is a theorem, not a numerical approximation. It holds for the forced conjugate birth field the shell creation installs each cadence cycle.

The theorem does not cover what happens after birth. The live engine then diffuses the spine by forced resolution, creating additional small interface components. Those are bounded above by a separate interface bound, not counted here. The O(1) statement is exact only for the initial polarized configuration, not for the evolved state.

THEOREM polarized_carried_subextensive · polarized_carried_subextensive · IndisputableMonolith/Cosmology/PolarizedBirthDomains.lean
polarized_carried_subextensive · IndisputableMonolith/Cosmology/PolarizedBirthDomains.lean:264 
/-- **Carried-state sub-extensivity for the birth field (2-D).** The polarized diamond fills
`2t² + 2t + 1` cells (Phase 49) but is carried as exactly 3 super-regions, so the carried state times
the radius is at most the area for every `t ≥ 1`: `3 t ≤ card (ball t)`, the carried cost is `O(1)`
while the world is `Θ(t²)`. -/
theorem polarized_carried_subextensive (t : ℕ) (ht : 1 ≤ t) :
    comp (Fmono t) = 3 ∧ 3 * t ≤ (InterfaceComponentBound.Diamond.ball t).card := by
  refine ⟨polarized_components_eq_three t ht, ?_⟩
  rw [LatticeBallVolume.Diamond.card_ball]
  nlinarith [ht]
THEOREM polarized_carried_subextensive · polarized_carried_subextensive · IndisputableMonolith/Cosmology/PolarizedBirthDomains.lean
polarized_carried_subextensive · IndisputableMonolith/Cosmology/PolarizedBirthDomains.lean:264 
/-- **Carried-state sub-extensivity for the birth field (2-D).** The polarized diamond fills
`2t² + 2t + 1` cells (Phase 49) but is carried as exactly 3 super-regions, so the carried state times
the radius is at most the area for every `t ≥ 1`: `3 t ≤ card (ball t)`, the carried cost is `O(1)`
while the world is `Θ(t²)`. -/
theorem polarized_carried_subextensive (t : ℕ) (ht : 1 ≤ t) :
    comp (Fmono t) = 3 ∧ 3 * t ≤ (InterfaceComponentBound.Diamond.ball t).card := by
  refine ⟨polarized_components_eq_three t ht, ?_⟩
  rw [LatticeBallVolume.Diamond.card_ball]
  nlinarith [ht]
THEOREM clos_someRoot_of_descent · comp_le_of_roots · IndisputableMonolith/Cosmology/PolarizedBirthDomains.lean
clos_someRoot_of_descent · IndisputableMonolith/Cosmology/PolarizedBirthDomains.lean:47 
/-- **Descent toward a finite set of roots.** If a height `h : V → ℕ` vanishes only on the cells in
`roots`, and every cell of positive height has an edge (in either orientation) to a strictly-lower
cell, then every cell is connected to some root in `roots`. Strong induction on `h v`, exactly as
`InterfaceComponentBound.clos_root_of_descent` but with several roots instead of one. -/
theorem clos_someRoot_of_descent [Finite V] (E : List (V × V)) (h : V → ℕ) (roots : List V)
    (hzero : ∀ v, h v = 0 → v ∈ roots)
    (hdesc : ∀ v, h v ≠ 0 → ∃ u, ((v, u) ∈ E ∨ (u, v) ∈ E) ∧ h u < h v) :
    ∀ v, ∃ r ∈ roots, clos E v r := by
  have e := clos_equiv E
  have H : ∀ n, ∀ v, h v = n → ∃ r ∈ roots, clos E v r := by
    intro n
    induction n using Nat.strong_induction_on with
    | _ n ih =>
      intro v hv
      rcases Nat.eq_zero_or_pos (h v) with h0 | hpos
      · exact ⟨v, hzero v h0, e.refl v⟩
      · have hvne : h v ≠ 0 := by omega
        obtain ⟨u, hedge, hlt⟩ := hdesc v hvne
        have hvu : clos E v u := by
          rcases hedge with he | he
          · exact Relation.EqvGen.rel v u he
          · exact e.symm (Relation.EqvGen.rel u v he)
        obtain ⟨r, hr, hur⟩ := ih (h u) (by omega) u rfl
        exact ⟨r, hr, e.trans hvu hur⟩
  intro v
  exact H (h v) v rfl
comp_le_of_roots · IndisputableMonolith/Cosmology/PolarizedBirthDomains.lean:74 
/-- **Few roots bound the component count.** If every cell's component is represented by some root in
`roots`, the number of components is at most `roots.length`. (The quotient map, restricted to the
roots, hits every class.) -/
theorem comp_le_of_roots [Finite V] (E : List (V × V)) (roots : List V)
    (hcov : ∀ v : V, ∃ r ∈ roots, clos E v r) : comp E ≤ roots.length := by
  classical
  haveI : Fintype (Quotient (cs E)) := Fintype.ofFinite _
  have himg : (Finset.univ : Finset (Quotient (cs E)))
      ⊆ roots.toFinset.image (Quotient.mk (cs E)) := by
    intro q _
    obtain ⟨v, rfl⟩ := Quotient.exists_rep q
    obtain ⟨r, hr, hvr⟩ := hcov v
    rw [Finset.mem_image]
    exact ⟨r, List.mem_toFinset.2 hr, Quotient.sound ((clos_equiv E).symm hvr)⟩
  calc comp E = Fintype.card (Quotient (cs E)) := by
            rw [comp, Nat.card_eq_fintype_card]
    _ = (Finset.univ : Finset (Quotient (cs E))).card := by rw [Finset.card_univ]
    _ ≤ (roots.toFinset.image (Quotient.mk (cs E))).card := Finset.card_le_card himg
    _ ≤ roots.toFinset.card := Finset.card_image_le
    _ ≤ roots.length := List.toFinset_card_le roots

What this page does not claim

The theorem does not apply to the evolved state after forced resolution diffuses the spine. The result does not bound the number of interface components created by the live engine. The O(1) carried state is not claimed for arbitrary charge fields, only the polarized birth field.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND