span_down_eq_VF
plain-language theorem explainer
The equality equates the sum of the down-quark generation steps 6 and 8 to the vertices plus faces of the three-dimensional cube. It is cited in arguments that the sector-dependent torsion assignment satisfies the Q3 cell counts under the partition and asymmetry constraints. The proof is a direct numerical evaluation via native_decide after unfolding the cube definitions.
Claim. The sum of the down-quark steps equals the vertices plus faces of the three-dimensional cube: $6 + 8 = 2^3 + 2 · 3$.
background
The module establishes that sector-dependent generation torsion is forced by the partition constraint (three overlapping consecutive-pair spans sum to N3 = 55), lepton uniqueness (only {11,6} sums to 17), and charge asymmetry (|Q̃_up| ≠ |Q̃_down|). These select the unique step assignment with up quarks {13,11}, leptons {11,6}, and down quarks {6,8}.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the arithmetic equality after substituting the definitions cube_vertices' d = 2^d and cube_faces' d = 2*d.
why it matters
It confirms that the down-quark steps match the Q3 cell counts, supporting the uniqueness claim of the SDGT forcing theorem. The module documentation states that the four step values are verified as Q3 cell counts but their derivation from a single principle remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.