Encyclopedia Cosmology Cosmology Polarized Birth Interface Count Interface Card Eq
ARTICLE 3 claims 3 theorems
Cosmology Polarized Birth Interface Count Interface Card Eq
A machine-checked theorem counts the exact number of boundary distinctions a growing two-dimensional lattice field must post at each step, and the answer is a simple linear formula.
The exact count
In the Recognition Science account, a growing field of discrete sites must record its own changing state. The record is a ledger, a discrete list of forced distinctions between neighboring sites. The declaration interface_card_eq is a theorem in the framework's machine-checked library of formal theorems. It proves that for a two-dimensional diamond-shaped lattice at radius t, the number of ordered edges where neighboring sites differ in their polarization state is exactly 8t - 4.
The formula counts ordered edges, meaning each adjacency between two sites is listed twice, once in each direction. The undirected perimeter is half that, 4t - 2. The proof works by showing a bijection: every such edge has exactly one endpoint on the central spine (where the first coordinate is zero) and one neighbor to the left or right, so the edge is completely determined by a spine position, a side, and an orientation. The count grows linearly with the radius.
The headline consequence is a constant increment. The theorem interface_increment_const proves that as the radius increases from t to t+1, the interface gains exactly 8 new ordered edges, regardless of how large the world has grown. In this model, the cost of recognition scales with the number of these boundary distinctions, not with the total volume of the world, which grows as the square of the radius. The framework reads this as a compute-watch principle: the work per cycle stays constant in two dimensions.
In Recognition Science, the same count lifts to three dimensions, the dimension the forcing chain selects. There the interface is a two-dimensional surface, and the exact ordered count is 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 sub-extensive against the volume but not constant.
The theorem does not claim that the two-dimensional constant increment holds in three dimensions, nor does it say anything about the physical mechanism that would connect this discrete lattice model to the observed cosmos. The bridge from recognition to physical linking remains open. What the theorem establishes is a precise combinatorial fact about a defined model, with the full force of a machine-checked proof.
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]
What this page does not claim
The constant per-cycle increment of 8 holds only in two dimensions, not in three. The theorem does not establish any connection between this lattice model and observed physical reality. The framework's physical recognition-to-linking bridge is not part of this theorem.
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:
- What physical process, if any, corresponds to the discrete lattice and its polarization states in the Recognition Science framework?
- How does the framework derive the three-dimensional spatial dimension that this counting theorem assumes?
- What is the physical interpretation of the recognition-active interface in cosmological terms?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
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]It proves that for a two-dimensional diamond-shaped lattice at radius t, the number of ordered edges where neighboring sites differ in their polarization state 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 theorem interface_increment_const proves that as the radius increases from t to t+1, the interface gains exactly 8 new ordered edges, regardless of how large the world has grown. 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]In Recognition Science, the same count lifts to three dimensions, the dimension the forcing chain selects. interface_card_eq · IndisputableMonolith/Cosmology/PolarizedBirthInterfaceCount.lean