r0_constraints_force_canonical
plain-language theorem explainer
Any integer r0 assignment to the lepton, up, down, and electroweak sectors that sits in the finite candidate pool and meets the yardstick principle constraints equals the canonical r0 assignment. Yardstick and mass-ladder uniqueness arguments cite this collapse. The proof converts principle constraints to the structural boolean filter, places the assignment in the valid list, and uses that that list is already a singleton.
Claim. Let $a$ assign integers $r_0$ to the lepton, up, down, and electroweak sectors. If $a$ lies in the finite enumeration of all sector-to-value permutations of the four candidate $r_0$ values, and if $a$ satisfies the yardstick principle constraints (equivalent to the structural sum and role filters), then $a$ equals the canonical $r_0$ assignment.
background
This module treats the O1 yardstick discussion as a finite combinatorial search. One starts from four candidate $r_0$ values and four candidate $B_{\mathrm{pow}}$ values, enumerates all sector-to-value assignments (permutations), and filters by the structural constraints used in the yardstick analysis. Under those filters both choice sets collapse to singletons.
An $r_0$ assignment is a four-tuple of integers (lepton, up, down, electroweak). The full pool is the list of all such permutations of the candidate values. Principle constraints are the mathematically stated yardstick conditions; structural constraints are their boolean-filter form on that pool. Valid assignments are the pool members that pass the structural filter.
The module already records that the valid $r_0$ list is a singleton equal to the canonical assignment. The present theorem packages that fact for any assignment known only to lie in the pool and to satisfy the principle side of the constraint equivalence.
proof idea
Short tactic proof. First apply the equivalence between principle and structural constraints to obtain that the structural boolean holds. Unfold the valid list as the pool filtered by that boolean, and discharge membership via the list-filter introduction rule from pool membership plus the structural flag. Rewrite with the prior singleton theorem for the valid $r_0$ list, then simplify to conclude equality with the canonical assignment.
why it matters
In Recognition Science the mass formula is yardstick times $\varphi$ to a rung offset involving a sector gap. The $r_0$ integers are the sector offsets in that yardstick layer; uniqueness of their assignment is part of making the O1 yardstick story a forced choice rather than a free fit.
The module goal is explicit: after structural filtering, both the $B_{\mathrm{pow}}$ and $r_0$ choice sets are singletons. This theorem is the $r_0$ forcing statement under pool membership plus principle constraints. A nearby unrestricted variant (cube-hierarchy fixed affine roles and lepton-vs-EW depth gap, no finite-pool hypothesis) is documented in the same file; together they close the combinatorial side of yardstick assignment.
No downstream consumers are wired yet in the graph. The natural landing spots are verification theorems that quote a unique canonical $r_0$ when discharging mass-ladder or anchor obligations tied to the yardstick principle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.