anchor_r0_constraints_from_principle
plain-language theorem explainer
The canonical anchor assignment of sector r0 values passes the structural boolean filter used in the O1 yardstick choice-set enumeration. Anyone verifying that the RS mass-anchor r0 tuple is an admissible combinatorial choice would cite this. The proof unpacks four already-proved structural identities, turns each into a decide-true fact, and simplifies the constraint predicate to true.
Claim. The anchor $r_0$ assignment (lepton, up-quark, down-quark, electroweak sectors filled by the standard anchor formulas) satisfies the structural constraint check: down-sector $r_0<0$, lepton $r_0$ strictly above electroweak $r_0$, electroweak $r_0$ strictly above up-quark $r_0$, and the four values sum to the fixed $r_0$ sum target.
background
The module treats O1 as a finite combinatorial search: take the four candidate $r_0$ values and the four sectors (lepton, up, down, electroweak), enumerate sector-to-value assignments, and keep only those that pass structural filters from the yardstick discussion. Under those filters the valid $r_0$ choice set collapses to a singleton.
The anchor assignment is the concrete map that fills each sector by the standard anchor $r_0$ formula for that sector. The structural constraint predicate is a boolean conjunction of four decidable checks: down-sector value negative; lepton above electroweak; electroweak above up; and the four values sum to a fixed target constant.
Upstream, a companion lemma already proves those four inequalities and the sum identity as mathematical propositions (not as decide facts). This theorem only bridges those propositions into the boolean filter the enumerator uses.
proof idea
Term/tactic hybrid, not a wrapper. Destructure the four identities from the structural-identities lemma (down negative, lepton $>$ electroweak, electroweak $>$ up, sum equals target). For each identity apply decide_eq_true to obtain a decide ... = true fact. Unfold the structural-constraint predicate and simp with those four decide facts, which discharges the boolean conjunction to true.
why it matters
In the O1 yardstick program the claim is that structural filters alone force a unique $r_0$ assignment. Showing the anchor assignment itself lies inside the filtered set is the positive half of that story: the physically intended tuple is admissible, not an external exception.
The module framing is explicit: after enumeration and filtering, valid choice sets collapse to singletons for both $B_{\mathrm{pow}}$ and $r_0$. This theorem is the anchor-side membership certificate for the current $r_0$ constraint set. No downstream consumers are wired yet in the graph; it is a leaf verification fact ready for the enumerated-choice closure summary.
Framework context: yardstick and $r_0$ sit in the mass-ladder layer (masses as yardstick times $\varphi$ raised to rung offsets with sector gaps). The result does not touch T5--T8 forcing, RCL, or the alpha band; it is pure assignment hygiene for the mass-anchor side of verification.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.