chain_unique_given_edge_pair
The declaration shows that if natural numbers a, b, c, d satisfy the partition a + 2b + 2c + d = 55 and middle sum b + c = 17, and begin with the edge-symmetric pair a = 13 = E+1, b = 11 = E-1, then the values are forced to c = 6 and d = 8. Mass enumeration researchers in Recognition Science cite this conditional uniqueness when fixing the generation steps to the observed quartet. The proof is a short tactic sequence that substitutes the two equalities and solves the resulting linear system with omega.
claimLet $a, b, c, d$ be natural numbers. If $a + 2b + 2c + d = 55$, $b + c = 17$, $a = 13$, and $b = 11$, then $a = 13$, $b = 11$, $c = 6$, and $d = 8$.
background
In the Step Value Enumeration module the focus is on narrowing the identification of generation-step values as Q₃ cube invariants at D=3. The module documentation states that 13 = E + 1, 11 = E - 1, 6 = F, and 8 = V, where E(D) := D * 2^(D-1) is the edge count of the D-cube. The partition constraint a + 2b + 2c + d = 55 encodes the total N₃ = 55 while b + c = 17 is the middle pair sum W = 17. Upstream results include the definition of E from SpectralEmergence and the structural properties proved in SectorDependentTorsion that establish these integers as Q₃ cell counts.
proof idea
The proof substitutes the hypotheses a = 13 and b = 11. It then applies omega to deduce c = 6 from the middle equation and d = 8 from the partition equation. Finally it constructs the required conjunction of equalities.
why it matters in Recognition Science
This result supports the parent theorem current_chain_unique_modulo_edge_pair_filter by supplying the conditional uniqueness under the edge-pair filter. It contributes to the module's enumeration of finite alternatives for the endpoint pair under explicit natural cube invariant constraints, as described in the module documentation. Within the Recognition framework it helps close the gap between proved Q₃ invariants and their use as generation steps, relating to the D=3 forcing step.
scope and limits
- Does not establish the values without assuming the edge pair (13,11).
- Does not prove uniqueness over all possible partitions, only under the given middle and total sums.
- Does not address why these invariants appear as steps rather than other cube counts.
- Does not derive the partition sum 55 or middle 17 from more primitive axioms.
formal statement (Lean)
164theorem chain_unique_given_edge_pair
165 (a b c d : ℕ)
166 (h_chain_partition : a + 2*b + 2*c + d = 55)
167 (h_middle : b + c = 17)
168 (h_a_eq : a = 13) -- E+1
169 (h_b_eq : b = 11) -- E-1
170 :
171 a = 13 ∧ b = 11 ∧ c = 6 ∧ d = 8 := by
proof body
Tactic-mode proof.
172 subst h_a_eq h_b_eq
173 have hc : c = 6 := by omega
174 have hd : d = 8 := by omega
175 exact ⟨rfl, rfl, hc, hd⟩
176
177/-- The chain (13, 11, 6, 8) is uniquely determined by the edge-pair filter
178 (13 = E+1, 11 = E-1) plus the partition and middle constraints.
179
180This is a CONDITIONAL UNIQUENESS result: given that the chain contains the
181edge-symmetric pair (E+1, E-1) as its leading two values, the remaining
182values are forced. -/