endpoint_pairs_not_unique
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.
claimThere 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 in Recognition Science
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.
scope and limits
- Does not prove uniqueness of the endpoint pair under the natural invariants.
- Does not derive the list of natural invariants from the forcing chain.
- Does not extend to dimensions other than 3.
- Does not incorporate rung or gap structure from the phi-ladder.
formal statement (Lean)
119theorem endpoint_pairs_not_unique :
120 ∃ (a₁ d₁ a₂ d₂ : ℕ),
121 a₁ ∈ natural_invariants_D3 ∧ d₁ ∈ natural_invariants_D3 ∧ a₁ + d₁ = 21 ∧
122 a₂ ∈ natural_invariants_D3 ∧ d₂ ∈ natural_invariants_D3 ∧ a₂ + d₂ = 21 ∧
123 (a₁, d₁) ≠ (a₂, d₂) ∧
124 a₁ ≠ 11 ∧ a₁ ≠ 6 ∧ d₁ ≠ 11 ∧ d₁ ≠ 6 ∧
125 a₂ ≠ 11 ∧ a₂ ≠ 6 ∧ d₂ ≠ 11 ∧ d₂ ≠ 6 := by
proof body
Term-mode proof.
126 refine ⟨13, 8, 14, 7, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
127 all_goals simp [natural_invariants_D3]
128
129/-! ## Constraint 3: The current chain (13, 11, 6, 8) satisfies all structural constraints -/
130
131/-- The current chain satisfies the partition constraint. -/