endpoint_pairs_summing_to_21
plain-language theorem explainer
This definition enumerates the four ordered pairs of natural invariants summing to 21 after excluding the middle pair {11,6}. Researchers analyzing generation steps or the mass ladder in Recognition Science cite it when checking endpoint constraints from the N3=55 partition. The definition is a direct list of pairs drawn from the Q3 cube-invariant set {13,11,6,8}.
Claim. The ordered pairs $(a,d)$ of natural numbers with $a+d=21$ drawn from the Q$_3$ cube invariants excluding the middle pair already assigned to 11 and 6.
background
The Step Value Enumeration module narrows the remaining open step after SectorDependentTorsion proves that {13,11,6,8} are the Q3 cube invariants at D=3. The endpoint constraint follows from the partition N3=55 with middle value W=17, leaving sum 21 for the endpoints a and d. Natural invariants here are the explicit counts 13=V+F-C, 11=E-A, 6=F, 8=V.
proof idea
Direct definition that lists the four ordered pairs satisfying the sum from the natural set. The accompanying comment records the exclusion rule for middle values and less natural chains.
why it matters
The declaration makes explicit the finite alternatives for the endpoint pair, supporting the module claim that uniqueness requires additional structural constraints beyond the natural invariant set. It feeds the analysis that {13,8} is the unique pair under those constraints and touches the open modeling choice of which cube invariants are allowed, relating to the phi-ladder and T5 J-uniqueness in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.