Pith. sign in
def

anchorR0Assignment

definition
show as:
module
IndisputableMonolith.Verification.YardstickAssignmentChoiceSet
domain
Verification
line
787 · github
papers citing
none yet

plain-language theorem explainer

Packages the four sector φ-exponent offsets from the geometric anchor into one r0 assignment record (lepton, up, down, electroweak). Anyone checking that the yardstick choice-set collapses to a singleton cites this as the concrete candidate. The body is a pure structure literal wiring each field to the corresponding sector value of the anchor map r0.

Claim. Define the anchor $r_0$ assignment as the four-tuple of integer sector offsets $(r_0(\mathrm{lepton}), r_0(\mathrm{up}), r_0(\mathrm{down}), r_0(\mathrm{EW}))$ taken from the geometric anchor map on sectors.

background

The module treats O1 yardstick assignment as a finite combinatorial search: four candidate $B_{\mathrm{pow}}$ values and four candidate $r_0$ values are permuted across sectors, then filtered by structural constraints. Valid choice sets collapse to singletons for both $B_{\mathrm{pow}}$ and $r_0$.

An $r_0$ assignment is a four-field integer record (lepton, up, down, electroweak). The upstream anchor map $r_0$ supplies derived $\varphi$-exponent offsets per sector from wallpaper and cube geometry: lepton $4W-6$, up $2W+A$, down $E_{\mathrm{total}}-W$, electroweak $3W+4$ (numerically $62,35,-5,55$ for the standard constants). Those offsets enter the mass formula as rung shifts on the $\varphi$-ladder.

proof idea

Definitional construction only: build the $R0Assignment$ structure by setting each field to the corresponding sector case of the anchor map $r_0$ (lepton, up quark, down quark, electroweak). No lemmas or tactics; the equality to the canonical assignment is discharged later by native decision.

why it matters

This is the concrete geometric candidate that the O1 enumeration must recover. Downstream, it is shown equal to the canonical $r_0$ record, to satisfy the structural filter (down negative, lepton $>\mathrm{EW}>$ up, and the sum target), and to lie in the valid $r_0$ assignment set; uniqueness of that set then pins the yardstick. In the broader RS mass story the $r_0$ offsets are the sector-dependent rung corrections on the $\varphi$-ladder (yardstick $\cdot\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$), so fixing them by geometry rather than fit is part of closing the mass-assignment side of the forcing chain.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.