Pith. sign in
module module moderate

IndisputableMonolith.Verification.QuarkForwardPipeline

show as:
view Lean formalization →

Forward mass pipeline for the six quarks (and the electron) at the RS anchor scale μ*. Defines each species mass from the master φ-ladder law with sector yardstick and rung/gap data fixed upstream. Verification readers cite it for the concrete positive mass constants used in coordinate-unification and numerical checks. The module is largely definitional: named mass values plus positivity lemmas assembled from Anchor and MassLaw.

claimAt the canonical anchor $\mu^*$, the forward quark masses $m_u,m_c,m_t,m_d,m_s,m_b$ (and $m_e$) are the positive reals given by the master mass law $m = Y\,\varphi^{r-8+\mathrm{gap}(Z)}$, with sector yardstick $Y>0$ and rung/gap data from the RS charge integerization map.

background

Recognition Science places every stable species on a φ-ladder: mass equals a sector yardstick times $\varphi$ raised to a rung offset that includes an eight-tick shift and a charge-gap term. The master formula lives in MassLaw; Anchor centralises the parameter-free constants in the Model layer without claiming experimental fit.

ZMapForcing supplies the integerization scale closure used to fix charge coordinates (smallest positive even scale $k=6$ in the parity-constrained class). QuarkCoordinateUnification then shows that the two common quark mass coordinate conventions are equivalent once a single reference mass is fixed.

This module sits in Verification: it materialises the forward values $m_u,\ldots,m_b$ (and $m_e$) and records positivity, so downstream checks can quote named constants rather than re-expanding the ladder formula.

proof idea

Definition-and-positivity module, not a deep proof development. Each mass constant is introduced by applying the master mass law at the anchor with the species rung/gap data. Positivity lemmas (yardstick_pos, m_up_pos, and siblings) discharge $m>0$ from positivity of the yardstick and of $\varphi$-powers. No multi-step tactic argument; the content is packaging of upstream Anchor/MassLaw data for the quark sector.

why it matters in Recognition Science

Gives Verification a single forward pipeline for quark (and electron) masses so coordinate-unification and numerical audits share one set of named constants. It sits on MassLaw's φ-ladder formula, Anchor's derived constants, and ZMapForcing's charge integerization, and aligns with QuarkCoordinateUnification's claim that the two quark coordinate conventions represent the same positive mass law once a reference is fixed.

In the broader RS chain this is the concrete mass-layer readout of the φ-ladder (primer mass formula: yardstick $\cdot\varphi^{\mathrm{rung}-8+\mathrm{gap}(Z)}$), not a forcing step T0–T8. used_by is empty in the graph snapshot; the module is an export surface for verification consumers rather than a lemma feeding a named parent theorem inside the monolith.

scope and limits

depends on (5)

Lean names referenced from this declaration's body.

declarations in this module (28)