current_chain_partition
The arithmetic identity 13 + 2·11 + 2·6 + 8 = 55 confirms that the chosen generation steps partition the total N₃ correctly into endpoint pair {13,8} and middle pair {11,6} with the required multiplicities. Researchers enumerating cube-invariant mass ladders at D=3 would cite this to anchor numerical consistency before exploring alternatives. The proof is a direct one-line normalization of the integer expression.
claimThe current chain satisfies the partition constraint $13 + 2·11 + 2·6 + 8 = 55$, where the endpoint steps are 13 and 8, the middle pair is {11,6} (each with multiplicity two), the middle sum equals W=17, and the total equals N₃=55.
background
Generation steps are identified with Q₃ cube invariants at D=3: 13 = V + F - C = E + 1 (Euler characteristic on the boundary), 11 = E - A (passive edges), 6 = F (faces), and 8 = V (vertices). The middle pair sums to W, defined as the wallpaper group count (17) in Anchor, TauStepDerivation, and MassTopology. The module enumerates finite alternatives under the endpoint constraint a + d = 21 while keeping the middle fixed at W=17, then isolates the current choice as the unique pair satisfying additional natural invariants.
proof idea
One-line wrapper that applies norm_num to the integer equality 13 + 211 + 26 + 8 = 55.
why it matters in Recognition Science
This theorem verifies the partition constraint for the current chain, closing the numerical consistency check inside the step-value enumeration module. The module narrows the remaining gap between proved Q₃ cell counts and their assignment as generation steps (flagged as open in the SDGTForcing docstring) by making the modeling choice of allowed invariants explicit. It sits downstream of the W definitions and supports later uniqueness results such as chain_unique_given_edge_pair.
scope and limits
- Does not derive the step values from the forcing chain T0-T8 without PDG input.
- Does not prove uniqueness of the invariant set itself.
- Does not extend to non-cube or higher-dimensional topologies.
- Does not compute mass ratios or rung placements on the phi-ladder.
formal statement (Lean)
132theorem current_chain_partition :
133 13 + 2*11 + 2*6 + 8 = 55 := by norm_num
proof body
Term-mode proof.
134
135/-- The current chain has middle pair summing to W. -/