Pith. sign in
module module moderate

IndisputableMonolith.Verification.YardstickAssignmentPrinciple

show as:
view Lean formalization →

Records the four sector candidate values of the yardstick power offset B_pow and the related r0 offsets used in RS mass anchoring. Supplies algebraic identities (sums, complements, sign relations) that pin those candidates before any assignment is chosen. Downstream choice-set enumeration imports this module as the fixed value pool. Content is mostly closed-form equalities and small finite checks, not a deep existence proof.

claimFor the four mass sectors, the module fixes candidate yardstick power offsets $B_{\mathrm{pow}}$ and companion offsets $r_0$, together with identities such as $\sum B_{\mathrm{pow}} = A$ and $\sum r_0 = VW + E_{\mathrm{passive}}$, plus lepton/EW complement and sign relations used when assigning sectors to values.

background

Recognition Science mass formulas place each species on a $\varphi$-ladder: mass $\propto$ yardstick $\times \varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$. The yardstick itself is fixed only after sector-level power offsets are chosen. This verification module sits in that assignment layer: it does not derive $\alpha$ or the experimental masses, but freezes the discrete candidate numbers that later combinatorial filters will permute.

Upstream, Constants supplies the RS-native time quantum and related units; AlphaDerivation records the cubic-ledger seed assembly (exact infrared $\alpha^{-1}(0)$ remains open); Masses.Anchor centralises the parameter-free mass constants in the Model layer. Against that backdrop the module names the four-sector $B_{\mathrm{pow}}$ pool and the four-sector $r_0$ pool, plus elementary sum and complement identities that any admissible assignment must respect.

proof idea

Definition-and-identity module rather than a single theorem. It introduces the concrete $B_{\mathrm{pow}}$ and $r_0$ value lists, then proves small algebraic facts: formula rewrites, sector sums equaling named anchors ($A$, $VW+E_{\mathrm{passive}}$), lepton/EW magnitude complements, and sign patterns (e.g. up-type negative vs EW positive). Proofs are direct evaluation and ring/arithmetic simplification on fixed integers or $\varphi$-expressions; no analytic estimates.

why it matters in Recognition Science

Feeds Verification.YardstickAssignmentChoiceSet, which treats O1 as a finite search: start from these four $B_{\mathrm{pow}}$ and four $r_0$ candidates, enumerate sector-to-value permutations, and filter by structural yardstick constraints. Without a frozen candidate pool the choice-set module has nothing to permute. In the broader RS chain this is bookkeeping on the mass-ladder yardstick step (primer mass formula), not a T0–T8 forcing result; it keeps the assignment discussion auditable and finite before any claim of uniqueness or data fit.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (23)