Encyclopedia Cosmology Cosmology Polarized Birth Interface Count Interface Length Eq Card

ARTICLE 5 claims 5 theorems

Cosmology Polarized Birth Interface Count Interface Length Eq Card

A machine-checked theorem counts the exact number of forced distinctions a growing polarized structure posts, and shows the cost of recognition tracks activity, not volume.

Verify this page

The exact interface count

The declaration interface_length_eq_card is a theorem in the framework's machine-checked library of formal theorems. It establishes that the length of a certain list of edges equals the cardinality of a certain set of edges. In plain terms, it proves that two different ways of counting the same thing give the same answer: the number of ordered edges in the recognition-active interface, as computed by a list, equals the number of those edges as computed by a set. This is a foundational step, because it lets the framework reason about the interface using whichever representation is more convenient.

The context is a discrete model of a growing world. The framework imagines a ledger, a discrete record of events, where each event is a forced distinction between neighboring points. The interface is the collection of these forced distinctions at a given time. The theorem shows that in a two-dimensional diamond-shaped world of radius t, the interface has exactly 8t - 4 ordered edges. This number counts each adjacency in both directions, so the undirected perimeter is half that, 4t - 2. The proof works by showing a bijection: every bichromatic edge has exactly one endpoint on the central spine and one neighbor beside it, so the edge is fully described by a position along the spine, a side, and an orientation.

The important consequence is that this count grows by exactly 8 edges per time step, a constant independent of the world's size. Even as the world's area grows like t squared, the number of new forced distinctions posted each cycle stays fixed at 8. This is the literal statement of a compute-watch principle: the cost of recognition scales with the interface activity, not with the volume. In the three-dimensional case, which the forcing chain selects, the same count lifts to a surface. There the interface is a disk, and the exact ordered count is 8t squared minus 8t plus 4. The per-cycle increment is then 16t, which grows linearly with the radius, not constant. This is the honest three-dimensional statement: in three dimensions, forced recognition activity per cycle grows with the size of the growing surface, though it remains sub-extensive compared to the volume.

What the declaration does not claim is also important. It does not claim that the physical universe is actually a discrete lattice of this exact shape. The framework models the world this way; the theorem is about the model. It also does not claim that the total cost of a full run is constant. The total growth over a run from radius 1 to T is 8T - 8 in two dimensions and 8T squared minus 8T in three, which is sub-extensive against the brute-force spacetime cost of volume times cycles. The theorem establishes a precise count within the model, not a statement about the empirical cosmos.

THEOREM interface_length_eq_card · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCount.lean
interface_length_eq_card · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCount.lean:65 
/-- **Bridge: the interface edge-list length equals the Finset cardinality.** The `toList` edge set
filtered to bichromatic pairs has length equal to the cardinality of the bichromatic edge `Finset`,
because the edge list is `Nodup` (a `Finset.toList`) and filtering preserves `Nodup`. -/
theorem interface_length_eq_card (t : ℕ) :
    ((edges t).filter (fun p => decide (polarized t p.1 ≠ polarized t p.2))).length = (B t).card := by
  have hnd : ((edges t).filter (fun p => decide (polarized t p.1 ≠ polarized t p.2))).Nodup := by
    apply List.Nodup.filter
    exact Finset.nodup_toList _
  rw [← List.toFinset_card_of_nodup hnd]
  congr 1
  ext q
  obtain ⟨a, b⟩ := q
  simp only [List.mem_toFinset, List.mem_filter, mem_edges, decide_eq_true_eq, B,
    Finset.mem_filter, Finset.mem_univ, true_and]
THEOREM interface_length_eq_card · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCount.lean
interface_length_eq_card · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCount.lean:65 
/-- **Bridge: the interface edge-list length equals the Finset cardinality.** The `toList` edge set
filtered to bichromatic pairs has length equal to the cardinality of the bichromatic edge `Finset`,
because the edge list is `Nodup` (a `Finset.toList`) and filtering preserves `Nodup`. -/
theorem interface_length_eq_card (t : ℕ) :
    ((edges t).filter (fun p => decide (polarized t p.1 ≠ polarized t p.2))).length = (B t).card := by
  have hnd : ((edges t).filter (fun p => decide (polarized t p.1 ≠ polarized t p.2))).Nodup := by
    apply List.Nodup.filter
    exact Finset.nodup_toList _
  rw [← List.toFinset_card_of_nodup hnd]
  congr 1
  ext q
  obtain ⟨a, b⟩ := q
  simp only [List.mem_toFinset, List.mem_filter, mem_edges, decide_eq_true_eq, B,
    Finset.mem_filter, Finset.mem_univ, true_and]
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_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]

What this page does not claim

The theorem does not claim that physical space is a discrete lattice of this shape. It does not claim that the total cost of a full run is constant in any dimension. It does not claim that the interface count is a measured quantity from 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