span_up_eq_2E
plain-language theorem explainer
The equality 13 + 11 = 2 times the edge count of the three-dimensional cube holds by direct arithmetic. Researchers verifying the geometric structure of up-quark spans in sector-dependent torsion would cite it to close one conjunct in the forcing argument. The proof reduces to a single native decision procedure that evaluates both sides in natural numbers.
Claim. $13 + 11 = 2 · (3 · 2^{2})$
background
The SDGT Forcing Theorem shows that sector-dependent generation torsion is forced rather than merely compatible. Three constraints act: the three overlapping consecutive-pair spans must partition N₃ = 55, only the lepton pair sums to 17, and charge asymmetry forces the end spans to be unequal. This selects the unique ordering 13, 11, 6, 8 for up, lepton, and down sectors respectively.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic. The tactic evaluates the left-hand sum and the right-hand expression built from the cube-edge definition d · 2^(d-1) at d = 3, then confirms numerical identity.
why it matters
The result supplies one conjunct in the corollary that the spans are cube-geometric. It therefore supports the uniqueness claim stated in the module documentation for the SDGT assignment. The four step values themselves remain open; they are verified as Q₃ cell counts but not yet derived from a single principle. The equality is consistent with the framework landmark that spatial dimension equals 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.