anchor_r0_matches_canonical
plain-language theorem explainer
The anchor map of rung offsets r0 onto the four particle sectors equals the canonical closed-form r0 assignment. Anyone checking uniqueness of the yardstick r0 choice set cites this equality. The proof is a one-line native_decide comparison of the two concrete records.
Claim. The anchor assignment of rung offsets $r_0$ to the four sectors equals the canonical formulas: lepton $4W-6$, up-type $2W+A$, down-type $E_{\mathrm{total}}-W$, electroweak $3W+4$.
background
This module treats the O1 yardstick discussion as a finite combinatorial search. One starts from four candidate $B_{\mathrm{pow}}$ values and four candidate $r_0$ values, enumerates all sector-to-value assignments (permutations), and filters by the structural constraints of the yardstick principle. Under those filters both choice sets collapse to singletons.
An $R_0$ assignment is a record assigning an integer rung offset to each of the four sectors: lepton, up-quark, down-quark, and electroweak. The anchor assignment is the record whose components are the existing sector-wise $r_0$ values from the mass-anchor layer. The canonical assignment is the closed-form record with lepton $4W-6$, up $2W+A$, down $E_{\mathrm{total}}-W$, and electroweak $3W+4$.
The theorem asserts these two records are definitionally equal as concrete data.
proof idea
One-line wrapper: native_decide evaluates both sides as concrete integer records and accepts the equality. No algebraic lemmas are invoked; the check is purely computational on the unfolded definitions of the anchor and canonical assignments.
why it matters
Feeds the uniqueness theorem anchor_is_unique_valid_r0, which rewrites the valid-$r_0$ set as a singleton and uses this equality to place the anchor inside that set. Together they close the $r_0$ half of the module's claim that the filtered choice sets collapse to singletons.
In the broader Recognition framework this pins the sector rung offsets that enter the mass formula (yardstick times $\phi$ to a rung power with gap corrections). Matching anchor data to the canonical formulas is the verification step that the combinatorial filter recovers the physically used assignment rather than some other permutation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.