current_chain_middle
plain-language theorem explainer
The declaration establishes that the middle pair of the current chain sums to 17 via the identity 11 + 6 = 17. Researchers enumerating generation steps on the Recognition Science phi-ladder would cite this when constraining Q3 cube invariants at D=3 to match the partition N3 = 55. The proof reduces to a single numerical normalization step.
Claim. The middle pair of the current chain satisfies $11 + 6 = 17$.
background
Recognition Science enumerates generation step values as Q3 cube invariants at three spatial dimensions. The four values are 13 = V + F - C, 11 = E - A, 6 = F, and 8 = V, where these arise from Euler characteristic V-E+F=2 at the boundary and active/passive edge counts per tick. The module narrows the gap between proved cell counts and their identification as generation steps by proving structural constraints on pairs summing to 17.
proof idea
The proof is a one-line wrapper applying norm_num to confirm the arithmetic equality 11 + 6 = 17.
why it matters
This result supports narrowing the open forcing step by confirming the lepton middle pair sums to 17, consistent with the endpoint sum of 21 from the N3 = 55 partition. It contributes to the enumeration of finite alternatives under natural cube invariant constraints, as described in the module doc. The context ties to the forcing chain at D=3 and the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.