Encyclopedia Cosmology Cosmology Polarized Birth Interface Count Edge Structure
ARTICLE 5 claims 5 theorems
Cosmology Polarized Birth Interface Count Edge Structure
A machine-checked theorem pins down exactly where a growing field's forced distinctions appear: only on a thin central spine, never in the bulk.
The edge structure theorem
In a discrete lattice model, imagine coloring each point either black or white according to a rule that changes over time. The recognition events, the forced distinctions the model posts, occur only where a black point touches a white point. The edge_structure theorem characterizes these boundary edges completely: every such edge has exactly one endpoint on the central spine (the line where the first coordinate is zero) and the other endpoint immediately to its left or right, at the same height. No boundary edge can skip, tilt, or reach deeper into the bulk. This is a structural fact, proved for both the two-dimensional diamond and the three-dimensional octahedron versions of the model.
The theorem is a formal statement in the framework's machine-checked library of formal theorems. It says that if two neighboring points carry different colors, then one of them lies on the spine and the other is a direct horizontal neighbor of it. In two dimensions, the spine is a line segment; in three dimensions, it is a flat disk. The proof is short and purely combinatorial: it unfolds the definition of adjacency and the coloring rule, then lets an arithmetic solver finish the case split. The same structure appears in both dimensions, which is why the counting theorems that build on it look so similar.
This structural fact is the foundation for exact counts. In two dimensions, the number of such boundary edges at radius t is exactly 8t - 4; in three dimensions, it is 8t² - 8t + 4. The per-cycle growth differs: in 2D the interface adds exactly 8 edges each step, independent of the world's size, while in 3D it adds 16t edges, growing linearly with the radius. Over a full run from radius 1 to T, the total new edges are 8(T-1) in 2D and 8T(T-1) in 3D. These totals scale as the surface area of the growing region, not its volume, which is the precise sense in which the model's cost tracks recognition activity rather than raw size.
In Recognition Science, this theorem is part of a larger derivation: the framework models reality as a discrete ledger of recognition events, and this result shows that the cost of running the ledger is sub-extensive. The theorem does not claim that the physical universe is a lattice, nor that the coloring rule is fundamental physics. It establishes a combinatorial fact about a specific model, and the model's relevance to cosmology rests on the forcing chain that selects three dimensions, not on this theorem alone.
THEOREM edge_structure · 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_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_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
What this page does not claim
The physical universe is a discrete lattice with this exact coloring rule. The edge structure theorem alone establishes the framework's cosmological claims. The counting results apply to any model other than the specific 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/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 forcing chain select three spatial dimensions from the recognition cost function?
- What physical interpretation does the framework give to the discrete lattice and its coloring rule?
- How does the sub-extensive interface growth connect to the framework's account of cosmological expansion?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM edge_structure · 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 <;> omegaEvery boundary edge has exactly one endpoint on the central spine and the other endpoint immediately to its left or right, at the same height. edge_structure · 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]In two dimensions, the number of boundary edges at radius t is exactly 8t - 4. interface_card_eq · 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]In three dimensions, the number of boundary edges at radius t is exactly 8t² - 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] omegaIn two dimensions, the interface grows by exactly 8 edges each step, independent of the world's size. interface_increment_const · 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] omegaIn three dimensions, the interface grows by 16t edges per step, linearly with the radius. interface_increment_linear · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCount.lean