N_diff_eq_edges_at_D3
plain-language theorem explainer
The difference N₂(3) − N₁(3) equals the edge count of the 3-cube. Researchers modeling lepton generation torsion via cube cell counts in Recognition Science would cite this to anchor the derived {11,6} steps. The proof is a direct native computation of the explicit integer values from the cube geometry definitions.
Claim. $N_2(3) - N_1(3)$ equals the number of edges of the 3-cube, where $N_1(d) = 2(V + E) + 1$ and $N_2(d) = 2(V + E + F) + 1$ with $V$, $E$, $F$ the vertex, edge and face counts of the $d$-cube.
background
The Sector-Dependent Generation Torsion module establishes that the integers {13, 11, 6, 8} satisfy the algebraic constraints of Q₃ cell counts and the partition of 2D^D + 1 = 55. N₁(d) and N₂(d) are defined directly from the cube counts S1(d) and S2(d) plus the body term. This rests on the cube geometry from SpectralEmergence (E(d) = D · 2^(D-1) for edges) and the cellular automata step function for local rule application. The module states that lepton torsion {11,6} = {E_pass, F} is fully derived while quark assignments remain data-supported hypotheses.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the concrete arithmetic equality at dimension 3 using the cube edge definitions.
why it matters
This verifies the D=3 edge difference that supports the derived dimension-forcing condition W = 2V + 1 = N₀ holding only at D=3. It aligns with the eight-tick octave and spatial dimension forcing from the T0-T8 chain. No parent theorems are listed in the used-by edges; the result closes a concrete check inside the SDGT module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.