endpoint_pairs_not_unique
plain-language theorem explainer
The theorem establishes that the list of natural D=3 invariants admits at least two distinct pairs summing to 21 that avoid the middle-pair values 11 and 6. Mass-spectrum researchers in Recognition Science cite it to document that endpoint selection for the generation chain stays open without extra structural filters. The term-mode proof simply supplies the concrete witnesses 13 with 8 and 14 with 7, then reduces all membership checks to the explicit list definition by simplification.
Claim. There exist natural numbers $a_1,d_1,a_2,d_2$ in the set of natural invariants at dimension 3 such that $a_1+d_1=21$, $a_2+d_2=21$, the ordered pairs $(a_1,d_1)$ and $(a_2,d_2)$ are distinct, and none of $a_1,d_1,a_2,d_2$ equals 11 or 6.
background
The module narrows the remaining open step in the Recognition Science forcing chain for generation values at D=3. The definition natural_invariants_D3 collects the integers with direct Q_3-combinatorial meaning: vertex count 8, face count 6, passive-edge count 11, and their elementary sums and differences, yielding the explicit list [1,6,7,8,11,12,13,14,15,17,18,20,25,26]. The endpoint sum 21 follows from the partition N_3=55 together with the middle-pair sum 17 already proved unique in the same module.
proof idea
The proof is a one-line term-mode wrapper. It refines the existential quantifier with the concrete witnesses 13,8,14,7 and discharges every membership goal by the tactic simp [natural_invariants_D3], which unfolds the list definition and verifies the arithmetic sums.
why it matters
The result is used by the downstream theorem thirteen_natural_interpretations, which records three equivalent natural-invariant readings of the value 13. It belongs to the enumeration that makes explicit the modeling choice of the natural-invariant set, as stated in the module documentation. This openness is consistent with T8 fixing D=3 and with the phi-ladder mass formula, where endpoint selection still requires additional constraints beyond the cube-cell counts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.