N1_minus_N0
plain-language theorem explainer
N1(3) minus N0(3) equals twice the edge count of the three-cube. Researchers verifying the algebraic structure of the Q3 cell counts in Recognition Science cite this identity to confirm consistency at D=3. The proof consists of a direct numerical evaluation via the native_decide tactic.
Claim. $N_1(3) - N_0(3) = 2 E(3)$ where $N_0(D) = 2V(D) + 1$, $N_1(D) = 2(V(D) + E(D)) + 1$, and $E(D) = D 2^{D-1}$ counts the edges of the D-cube.
background
The Sector-Dependent Generation Torsion module examines cell counts N0 and N1 for the D-cube at D=3. N0(d) is defined as 2 S0(d) + cube_body, which equals 2V + 1, while N1(d) is 2 S1(d) + cube_body, or 2(V + E) + 1. The module documentation states that the assignment of counts to fermion sectors is data-driven, yet the D=3 coincidence W = 2V + 1 = N0 is derived without data.
proof idea
The proof applies the native_decide tactic directly to the concrete natural-number expressions at d=3. It is a one-line wrapper that computes N1 3 - N0 3 and 2 * cube_edges' 3 and confirms their equality by evaluation.
why it matters
This identity confirms the D=3 coincidence in the module documentation, where N0 equals 2V + 1 only at three dimensions and supplies a dimension-forcing condition. It contributes to verifying that the cell counts {13, 11, 6, 8} satisfy the cyclic chain and partition of 2D^D + 1 = 55. The result aligns with the eight-tick octave and D = 3 forcing from the Recognition Science chain (T7, T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.