Encyclopedia Cosmology Cosmology Polarized Birth Interface Count Interface Increment Const

ARTICLE 4 claims 4 theorems

Cosmology Polarized Birth Interface Count Interface Increment Const

In a two-dimensional model of cosmic birth, the boundary of newly distinguished structure grows by exactly eight edges per step, no matter how large the world becomes.

Verify this page

The constant interface increment

A growing lattice, a discrete grid of points, where each step marks a new layer of structure. The declaration interface_increment_const concerns the interface: the set of edges that separate regions of different polarization, a distinction the model treats as a unit of recognition activity. The theorem proves that in the two-dimensional diamond lattice, as the radius increases from t to t+1, the number of such ordered edges grows by exactly 8, independent of t. The total edge count at radius t is 8t - 4, so the difference between consecutive radii is always 8. This is a machine-checked result in the framework's library of formal theorems, with no unproved assumptions beyond the standard logical axioms.

The constant increment is surprising because the world itself grows much faster. The number of lattice points inside the diamond scales as the square of the radius, roughly t², so the volume expands quadratically. Yet the recognition-active boundary, the interface where distinctions are posted, adds only a fixed number of edges per step. In the framework's language, cost tracks recognition activity, not volume: the per-cycle cost remains O(1) even as the world size grows as Θ(t²). The proof works by showing each interface edge has exactly one endpoint on the central spine (x = 0) and one neighbor on either side, with a choice of side and orientation, giving a bijection to a set of size 8t - 4.

In three dimensions, the picture changes. The same construction on an octahedral lattice gives an interface that is a two-dimensional surface, with edge count 8t² - 8t + 4. The per-cycle increment is then 16t, which grows linearly with the radius, not constant. The framework's honest three-dimensional statement is that recognition activity per cycle is Θ(t), still sub-extensive against the Θ(t³) volume but not constant. The constant increment is therefore a special feature of the two-dimensional case, not a general law.

What the declaration does not claim: it does not say that the physical universe has a constant recognition cost per cycle. That claim would require the three-dimensional result, which is linear, not constant. It also does not claim that the interface increment is the same in all dimensions; the octahedral case explicitly contradicts that. Finally, it does not claim that the interface count itself is constant; only the difference between consecutive radii is constant in 2D.

THEOREM interface_increment_const · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCount.lean
interface_increment_const · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCount.lean:227 
/-- **Constant per-cycle recognition activity (the compute-watch law, in Lean).** Advancing the
diamond birth field by one cadence cycle (`t → t + 1`) adds exactly `8` ordered interface edges,
*independent of `t`* and hence independent of the world volume (which grows as `Θ(t²)`). The forced
distinctions the engine must post per cycle are `O(1)`, so the simulation's cost scales with
recognition activity, never with volume. -/
theorem interface_increment_const (t : ℕ) (ht : 1 ≤ t) :
    (B (t + 1)).card - (B t).card = 8 := by
  rw [interface_card_eq (t + 1) (by omega), interface_card_eq t ht]
  omega
THEOREM interface_card_eq · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCount.lean
interface_card_eq · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCount.lean:132 
/-- **The exact 2-D interface edge count is `8t - 4`** (ordered edges). The bichromatic edge set is in
bijection with `{interior spine y} × {side, orientation}`: every bichromatic edge has exactly one
spine endpoint `(0, y)` and one neighbour `(±1, y)` sharing the `y`-coordinate, so the edge is fully
determined by `(y, side, orientation)` with `|y| ≤ t - 1`. -/
theorem interface_card_eq (t : ℕ) (ht : 1 ≤ t) : (B t).card = 8 * t - 4 := by
  rw [← idx_card t ht]
  refine Finset.card_bij' (fun p _ => edgeIndex t p) (fun a ha => edgeFromIndex t a ha) ?_ ?_ ?_ ?_
  · -- hi : edgeIndex maps B into idx
    rintro ⟨a, b⟩ hp
    simp only [B, Finset.mem_filter, Finset.mem_univ, true_and] at hp
    obtain ⟨hadj, hpol⟩ := hp
    have hbm := b.property
    have ham := a.property
    rw [InterfaceComponentBound.Diamond.mem_ball_iff] at ham hbm
    show edgeIndex t (a, b) ∈ idx t
    rcases edge_structure t a b hadj hpol with ⟨h0, hbpm, hyeq⟩ | ⟨h0, hapm, hyeq⟩
    · dsimp only [edgeIndex]
      rw [if_pos h0, idx]
      have key : b.val.2.natAbs ≤ t - 1 := by
        have hb : b.val.1.natAbs + b.val.2.natAbs ≤ t := by
          have hmem := b.property
          rwa [InterfaceComponentBound.Diamond.mem_ball_iff] at hmem
        have h1 : b.val.1.natAbs = 1 := by rcases hbpm with hb1 | hb1 <;> rw [hb1] <;> decide
        omega
      have hbnd : a.val.2 ∈ Finset.Icc (-(t : ℤ) + 1) ((t : ℤ) - 1) := by
        rw [Finset.mem_Icc, hyeq]
        omega
      exact Finset.mem_product.mpr ⟨hbnd, Finset.mem_univ _⟩
    · have hne : ¬ (a.val.1 = 0) := by rcases hapm with h | h <;> omega
      dsimp only [edgeIndex]
      rw [if_neg hne, idx]
      have key : a.val.2.natAbs ≤ t - 1 := by
        have ha : a.val.1.natAbs + a.val.2.natAbs ≤ t := by
          have hmem := a.property
          rwa [InterfaceComponentBound.Diamond.mem_ball_iff] at hmem
        have h1 : a.val.1.natAbs = 1 := by rcases hapm with ha1 | ha1 <;> rw [ha1] <;> decide
        omega
      have hbnd : b.val.2 ∈ Finset.Icc (-(t : ℤ) + 1) ((t : ℤ) - 1) := by
        rw [Finset.mem_Icc, ← hyeq]
        omega
      exact Finset.mem_product.mpr ⟨hbnd, Finset.mem_univ _⟩
  · -- hj : edgeFromIndex maps idx into B
    rintro a ha
    show edgeFromIndex t a ha ∈ B t
    simp only [B, Finset.mem_filter, Finset.mem_univ, true_and]
    unfold edgeFromIndex
    split
    · refine ⟨?_, ?_⟩
      · unfold adj; dsimp only; split <;> omega
      · simp only [polarized]; dsimp only; split_ifs <;> omega
    · refine ⟨?_, ?_⟩
      · unfold adj; dsimp only; split <;> omega
      · simp only [polarized]; dsimp only; split_ifs <;> omega
  · -- left_inv : edgeFromIndex (edgeIndex p) = p
    rintro ⟨a, b⟩ hp
    simp only [B, Finset.mem_filter, Finset.mem_univ, true_and] at hp
    obtain ⟨hadj, hpol⟩ := hp
    rcases edge_structure t a b hadj hpol with ⟨h0, hbpm, hyeq⟩ | ⟨h0, hapm, hyeq⟩
    · apply Prod.ext
      · apply Subtype.ext
        simp only [edgeIndex, edgeFromIndex, h0]
        rw [Prod.ext_iff]
        exact ⟨h0.symm, rfl⟩
      · apply Subtype.ext
        simp only [edgeIndex, edgeFromIndex, h0]
        rw [Prod.ext_iff]
        refine ⟨?_, hyeq⟩
        rcases hbpm with hb1 | hb1 <;> simp [hb1]
    · have hne : ¬ (a.val.1 = 0) := by rcases hapm with h | h <;> omega
      apply Prod.ext
      · apply Subtype.ext
        simp only [edgeIndex, edgeFromIndex, if_neg hne]
        rw [Prod.ext_iff]
        refine ⟨?_, hyeq.symm⟩
        rcases hapm with ha1 | ha1 <;> simp [ha1]
      · apply Subtype.ext
        simp only [edgeIndex, edgeFromIndex, if_neg hne]
        rw [Prod.ext_iff]
        rcases edge_structure t a b hadj hpol with ⟨h0', _, _⟩ | ⟨h0', _, _⟩
        · exact absurd h0' hne
        · exact ⟨h0'.symm, rfl⟩
  · -- right_inv : edgeIndex (edgeFromIndex a) = a
    rintro a ha
    obtain ⟨y, side, orient⟩ := a
    show edgeIndex t (edgeFromIndex t (y, side, orient) ha) = (y, side, orient)
    cases orient <;> cases side <;>
      simp [edgeFromIndex, edgeIndex]
THEOREM interface_increment_const · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCount.lean
interface_increment_const · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCount.lean:227 
/-- **Constant per-cycle recognition activity (the compute-watch law, in Lean).** Advancing the
diamond birth field by one cadence cycle (`t → t + 1`) adds exactly `8` ordered interface edges,
*independent of `t`* and hence independent of the world volume (which grows as `Θ(t²)`). The forced
distinctions the engine must post per cycle are `O(1)`, so the simulation's cost scales with
recognition activity, never with volume. -/
theorem interface_increment_const (t : ℕ) (ht : 1 ≤ t) :
    (B (t + 1)).card - (B t).card = 8 := by
  rw [interface_card_eq (t + 1) (by omega), interface_card_eq t ht]
  omega
THEOREM interface_increment_linear · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCount.lean
interface_increment_linear · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCount.lean:421 
/-- **Linear per-cycle recognition activity (3-D).** Advancing the octahedron birth field by one
cadence cycle (`t → t + 1`) adds exactly `16t` ordered interface edges. Unlike the 2-D case (where the
increment is the constant `8`), in three dimensions the forced recognition activity per cycle grows
`Θ(t)`: the interface is a 2-D surface whose area grows linearly per shell. This is the honest 3-D
form of the compute-watch law: cost per cycle still tracks recognition activity, but in D = 3 that
activity is `Θ(t)`, not `O(1)`, because the recognition-active interface is a growing codim-1 disk. -/
theorem interface_increment_linear (t : ℕ) (ht : 1 ≤ t) :
    (B (t + 1)).card - (B t).card = 16 * t := by
  rw [interface_card_eq (t + 1) (by omega), interface_card_eq t ht]
  have e : (t + 1) ^ 2 = t ^ 2 + 2 * t + 1 := by ring
  have hsq : t ≤ t ^ 2 := by nlinarith [ht]
  rw [e]
  omega

What this page does not claim

The constant increment does not apply to three dimensions, where the increment is linear. The interface count itself is not constant; only the difference between consecutive radii is constant in 2D. The declaration does not establish a constant recognition cost for the physical universe.

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/PolarizedBirthInterfaceCount.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