span_up_eq_2E
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 in Recognition Science
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.
scope and limits
- Does not derive the four step values from a single principle.
- Does not prove the full SDGT uniqueness without the remaining conjuncts.
- Does not link the step values to the J-cost function or phi-ladder.
- Does not treat generalizations beyond dimension 3.
formal statement (Lean)
155theorem span_up_eq_2E : (13 + 11 : ℕ) = 2 * cube_edges' 3 := by native_decide