Encyclopedia Cosmology Cosmology Polarized Birth Interface Count
ARTICLE 6 claims 6 theorems
Cosmology Polarized Birth Interface Count
The framework's machine-checked library counts the exact boundary of a growing polarized field, and finds the cost of recognition stays constant per cycle in two dimensions.
The interface count
In Recognition Science, the framework that derives physical structure from the cost of recognition events, a central simulation grows a polarized field outward from a point, one cadence cycle at a time. The field's boundary, the set of adjacent sites with opposite polarization, is its recognition-active interface: the only places where the engine posts a forced distinction. The module PolarizedBirthInterfaceCount proves exactly how many such boundary edges exist at each radius, and the answer is a clean polynomial.
For the two-dimensional diamond lattice, the interface is a one-dimensional spine. The theorem interface_card_eq states that at radius t the number of ordered boundary edges is exactly 8t - 4. Each edge has one endpoint on the central spine and one neighbor to its left or right, so the count grows linearly with radius. The headline corollary, interface_increment_const, shows the interface grows by exactly 8 edges per cadence cycle, a constant independent of the world's size. Even as the world's volume grows as Θ(t²), the recognition activity per cycle stays at O(1). This is the literal statement of the compute-watch principle: cost scales with recognition activity, not with volume.
The same count lifts to three dimensions, the dimension the forcing chain selects. There the interface is a two-dimensional surface, a disk in the spine plane x = 0. The theorem Octahedron.interface_card_eq gives the exact ordered count as 8t² - 8t + 4. The per-cycle increment, Octahedron.interface_increment_linear, is 16t, which is Θ(t) rather than O(1). In three dimensions the forced recognition activity per cycle grows linearly with the radius, because the recognition-active interface is a growing disk, not a fixed-size band. Cost still tracks recognition activity; in D = 3 that activity is sub-extensive against the Θ(t³) volume, but it is not constant.
Both namespaces also carry interface_total_growth, the net interface edges introduced over a full forward run from radius 1 to T: 8T - 8 in 2D and 8T² - 8T in 3D. These totals are Θ(T^(D-1)), strictly sub-extensive against the brute-force Θ(T^(D+1)) spacetime cost of volume times cycles. A full run posts Θ(T^(D-1)) net forced distinctions, not Θ(T^(D+1)). The module closes the earlier phase's bound on spine cells by counting the interface edges exactly, and the closed-form run-total is the compute-watch principle's explicit ledger for the whole simulation.
THEOREM edge_structure · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCount.lean
/-- **Structure of a bichromatic edge.** Any adjacent pair of different polarized charge has exactly
one endpoint on the spine `x = 0` and the other at `x = ±1`, and they share the `y`-coordinate. Pure
case analysis on the two `sign(x)` values plus the unit-distance adjacency. This is the workhorse
that pins the edge data to `(y, side, orientation)`. -/
theorem edge_structure (t : ℕ) (a b : Vtx t) (hadj : adj a.val b.val)
(hpol : polarized t a ≠ polarized t b) :
(a.val.1 = 0 ∧ (b.val.1 = 1 ∨ b.val.1 = -1) ∧ a.val.2 = b.val.2) ∨
(b.val.1 = 0 ∧ (a.val.1 = 1 ∨ a.val.1 = -1) ∧ a.val.2 = b.val.2) := by
unfold adj at hadj
simp only [polarized] at hpol
split_ifs at hpol <;> omega
THEOREM interface_card_eq · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCount.lean
/-- **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
/-- **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
/-- **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_linear · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCount.lean
/-- **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_total_growth · interface_total_growth · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCount.lean
/-- **Total interface growth over a forward run (2-D).** The net number of interface edges the
polarized birth introduces over a full run from radius `1` to radius `T` is exactly `8T - 8 = 8(T-1)`,
the difference of the start and end interface sizes. This is `Θ(T)`, sub-extensive against the
brute-force spacetime cost `Θ(T³)` (volume `Θ(T²)` times `T` cycles): the compute-watch total. -/
theorem interface_total_growth (T : ℕ) (hT : 1 ≤ T) :
(B T).card - (B 1).card = 8 * T - 8 := by
rw [interface_card_eq T hT, interface_card_eq 1 (le_refl 1)]
omega
What this page does not claim
The module does not prove the physical recognition-to-linking bridge that connects the topological theorem to observed three-dimensional space. The constant per-cycle increment in two dimensions is not claimed to hold in three dimensions, where the increment grows linearly. The interface count is not claimed to be a measurement of any physical quantity.
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:
- How does the interface count connect to the framework's derivation of three spatial dimensions?
- What physical observable, if any, corresponds to the per-cycle interface increment in two dimensions?
- Does the linear growth of recognition activity in three dimensions leave a measurable signature in the framework's particle ladder?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM edge_structure · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCount.lean
/-- **Structure of a bichromatic edge.** Any adjacent pair of different polarized charge has exactly one endpoint on the spine `x = 0` and the other at `x = ±1`, and they share the `y`-coordinate. Pure case analysis on the two `sign(x)` values plus the unit-distance adjacency. This is the workhorse that pins the edge data to `(y, side, orientation)`. -/ theorem edge_structure (t : ℕ) (a b : Vtx t) (hadj : adj a.val b.val) (hpol : polarized t a ≠ polarized t b) : (a.val.1 = 0 ∧ (b.val.1 = 1 ∨ b.val.1 = -1) ∧ a.val.2 = b.val.2) ∨ (b.val.1 = 0 ∧ (a.val.1 = 1 ∨ a.val.1 = -1) ∧ a.val.2 = b.val.2) := by unfold adj at hadj simp only [polarized] at hpol split_ifs at hpol <;> omegaFor the two-dimensional diamond lattice, the interface is a one-dimensional spine. edge_structure · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCount.leanTHEOREM interface_card_eq · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCount.lean
/-- **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]The theorem interface_card_eq states that at radius t the number of ordered boundary edges is exactly 8t - 4. interface_card_eq · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCount.leanTHEOREM interface_increment_const · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCount.lean
/-- **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] omegaThe headline corollary, interface_increment_const, shows the interface grows by exactly 8 edges per cadence cycle, a constant independent of the world's size. interface_increment_const · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCount.leanTHEOREM interface_card_eq · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCount.lean
/-- **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]The theorem Octahedron.interface_card_eq gives the exact ordered count as 8t² - 8t + 4. interface_card_eq · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCount.leanTHEOREM interface_increment_linear · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCount.lean
/-- **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] omegaThe per-cycle increment, Octahedron.interface_increment_linear, is 16t, which is Θ(t) rather than O(1). interface_increment_linear · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCount.leanTHEOREM interface_total_growth · interface_total_growth · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCount.lean
/-- **Total interface growth over a forward run (2-D).** The net number of interface edges the polarized birth introduces over a full run from radius `1` to radius `T` is exactly `8T - 8 = 8(T-1)`, the difference of the start and end interface sizes. This is `Θ(T)`, sub-extensive against the brute-force spacetime cost `Θ(T³)` (volume `Θ(T²)` times `T` cycles): the compute-watch total. -/ theorem interface_total_growth (T : ℕ) (hT : 1 ≤ T) : (B T).card - (B 1).card = 8 * T - 8 := by rw [interface_card_eq T hT, interface_card_eq 1 (le_refl 1)] omegaA full run posts Θ(T^(D-1)) net forced distinctions, not Θ(T^(D+1)). interface_total_growth · interface_total_growth · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCount.lean