Encyclopedia Cosmology Cosmology Polarized Birth Interface Count Interface Increment Linear

ARTICLE 3 claims 3 theorems

Cosmology Polarized Birth Interface Count Interface Increment Linear

In a three-dimensional lattice, the number of newly distinguished edges per cycle grows in proportion to the radius, not at a constant rate.

Verify this page

The linear increment

In Recognition Science, a framework that models reality as a discrete ledger of recognition events, a lattice of points grows over successive cycles. At each cycle, the framework marks which neighboring points hold different states, and the set of edges connecting them is called the interface. The declaration interface_increment_linear establishes a precise count for this interface in three dimensions.

The theorem states that when the radius of the lattice increases from t to t + 1, the number of ordered interface edges grows by exactly 16t. This means the growth is linear in the radius: as the world expands, the number of new distinctions posted each cycle increases proportionally with its size. The total interface at radius t is given by the formula 8t² - 8t + 4, and the increment follows directly from subtracting the counts at successive radii.

The result contrasts with the two-dimensional case, where the interface grows by a constant 8 edges per cycle regardless of world size. In three dimensions, the recognition-active interface is a growing disk, not a fixed band, so the activity per cycle scales with the radius. This distinction matters for the framework's compute-watch principle: the cost of recognition tracks the interface activity, not the volume of the world.

The theorem is proved in the machine-checked library of formal theorems, with no unproven assumptions beyond the standard logical axioms. It is a statement about the counting of edges in a defined lattice structure, not a claim about physical space itself. The framework models three-dimensional space through this kind of lattice, but the bridge from recognition events to physical geometry remains a target for future work.

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

What this page does not claim

The theorem does not claim that physical space itself is a lattice. The result does not establish the physical recognition-to-linking bridge. The linear increment does not imply that total recognition cost scales with volume.

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