S1_at_D3
plain-language theorem explainer
The theorem states that S1(3) equals 20, where S1(d) sums the vertices and edges of the d-dimensional cube. Workers on dimension-forcing arguments cite it to confirm the D=3 coincidence derived from W = 2V + 1 = N0. The proof is a direct native_decide evaluation of the recursive cube definitions.
Claim. $S_1(3) = 20$, where $S_1(d) := V(d) + E(d)$ is the sum of 0-faces and 1-faces of the d-dimensional hypercube.
background
The module SectorDependentTorsion proves that the integers {13, 11, 6, 8} match Q3 cell counts and obey algebraic constraints such as cyclic chains and the partition of 2D^D + 1 = 55. It derives that W = 2V + 1 = N0 holds exclusively for D = 3, supplying a genuine dimension-forcing condition without data input. S1 is the sibling definition S1(d) := cube_vertices' d + cube_edges' d, which equals V + E.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the definition of S1 at argument 3.
why it matters
This result verifies the D=3 cell count that underpins the derived dimension-forcing condition W = 2V + 1 = N0. It supports the eight-tick octave and spatial dimension D = 3 in the T0-T8 forcing chain. The module treats the numerical verification as mathematical scaffolding for the lepton torsion derivation while leaving quark assignments as data-supported hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.