chain_unique_given_edge_pair
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.