anchor_r0_structural_identities
plain-language theorem explainer
The canonical anchor r0 assignment obeys the four structural filter constraints used in the yardstick choice-set search: down is negative, lepton exceeds electroweak, electroweak exceeds up, and the four sector values sum to the fixed r0 target. Anyone checking that the anchor survives the O1 combinatorial filter cites this. The proof is a four-goal refine that unpacks the principle-level order lemmas and rewrites the sum identity.
Claim. For the anchor $r_0$ sector assignment $A$, one has $A_{\mathrm{down}} < 0$, $A_{\mathrm{lepton}} > A_{\mathrm{ew}}$, $A_{\mathrm{ew}} > A_{\mathrm{up}}$, and $A_{\mathrm{lepton}} + A_{\mathrm{up}} + A_{\mathrm{down}} + A_{\mathrm{ew}} = S_{r_0}$, where $S_{r_0}$ is the fixed $r_0$ sum target.
background
The module treats the O1 yardstick discussion as a finite combinatorial search: four candidate $B_{\mathrm{pow}}$ values and four candidate $r_0$ values are assigned to the four mass sectors (lepton, up, down, electroweak) by enumerating permutations, then filtered by structural constraints. Valid choice sets collapse to singletons under those filters.
Here $r_0$ is the sector rung offset in the mass yardstick formula (yardstick times $\varphi$ to a rung power). The anchor assignment is the distinguished sector-to-value map used throughout the mass ladder. The structural filter demands a sign condition on the down sector, two strict orderings among lepton, electroweak, and up, and a fixed four-term sum equal to a named target $S_{r_0}$.
Upstream, the Yardstick Assignment Principle already proves the corresponding order triple and the sum-matching identity for the principle-level $r_0$ data; this theorem only specializes those facts to the concrete anchor record.
proof idea
Four-goal refine on the conjunction. The first three goals are one-line simpa rewrites of anchorR0Assignment against the three conjuncts of YardstickAssignmentPrinciple.r0_order_constraints (down negative; lepton above electroweak; electroweak above up). The fourth goal rewrites the four-term sector sum, using add_comm, add_left_comm, and add_assoc to match the order in r0_sum_target_matches_principle.symm.
why it matters
This is the bridge from principle-level $r_0$ identities to the boolean structural filter on the anchor assignment. The sole downstream consumer is anchor_r0_constraints_from_principle, which packages the four identities into r0StructuralConstraints anchorR0Assignment = true via decide_eq_true, so the anchor survives the O1 choice-set filter.
In the broader Recognition picture the $r_0$ offsets sit inside the mass formula on the $\varphi$-ladder (yardstick $\cdot \varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$). Pinning a unique anchor $r_0$ assignment under structural constraints is part of showing the yardstick sector map is forced rather than free, consistent with the forcing chain that already fixes $\varphi$ (T6) and the eight-tick octave (T7).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.