middle_pairs_summing_to_17
plain-language theorem explainer
The definition enumerates the ordered pairs of natural numbers from the Q3 cube invariants that sum to 17, excluding equal components. Researchers tracing the lepton middle rung in the Recognition mass ladder would cite it when checking partition constraints on the phi-ladder. It is realized by direct listing of the two qualifying pairs drawn from the invariants {11,6}.
Claim. The list of ordered pairs $(b,c)$ of natural numbers satisfying $b+c=17$ that arise from the natural invariants, excluding pairs with equal entries.
background
The module enumerates step values on the phi-ladder at D=3. The four Q3 cube invariants are 13 = V+F-C, 11 = E-A, 6 = F and 8 = V; these appear as generation steps only by matching to PDG data. The middle sum 17 is the partition constraint W=17 extracted from N3=55. Natural invariants here mean the subset {11,6} that survive the Euler and edge-count relations at the cube boundary.
proof idea
Direct definition that returns the explicit list containing the two ordered pairs satisfying the sum condition from the invariants.
why it matters
The definition supplies one of the enumerated alternatives needed to prove that the lepton middle pair is the unique choice compatible with the natural cube invariants. It therefore narrows the open gap flagged in the SDGTForcing module between proved Q3 cell counts and their assignment as generation steps. The parent results are the structural constraints on the current chain partition and the uniqueness statements that follow from this enumeration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.