module module moderate

`IndisputableMonolith.Verification.QuarkForwardPipeline`

Forward pipeline that materializes the six quark masses (and the electron) at the RS mass anchor from the master φ-ladder law, sector yardstick, and forced Z-map. Verification authors cite it when they need concrete positive mass values rather than the abstract mass formula. The module is mostly definitions plus positivity lemmas built on Anchor, MassLaw, ZMapForcing, and QuarkCoordinateUnification.

claimAt the RS mass anchor $\mu^*$, the forward mass pipeline assigns positive masses $m_u, m_c, m_t, m_d, m_s, m_b$ (and $m_e$) via the master law $m = Y \, \varphi^{r-8+\mathrm{gap}(Z)}$ with sector yardstick $Y>0$, rung $r$, and the forced integerization map $Z$, under the unified quark coordinate convention.

background

Recognition Science places every stable particle on a $\varphi$-ladder rung. The master mass law (MassLaw) states that mass is coherence energy scaled by a sector yardstick and a rung offset that includes a charge-gap term $\mathrm{gap}(Z)$. Constants and Anchor supply the RS-native yardstick and the parameter-free anchor scale $\mu^*$ at which numerical masses are evaluated; nothing in that layer claims experimental fit.

ZMapForcing packages the integerization closure used for Standard Model charges (smallest positive even scale $k=6$ in the adopted parity class). QuarkCoordinateUnification proves the two common quark mass coordinate conventions are equivalent once a reference mass is fixed, so a single positive mass law can be written without dual bookkeeping.

This verification module sits downstream of those pieces: it names the concrete forward values $m_u,\ldots,m_b$ (and $m_e$) and records positivity, rather than re-deriving the law.

proof idea

Definition-heavy module, not a single theorem. Masses are introduced as instances of the master ladder formula at fixed anchor data (yardstick, rung, gap from the forced $Z$-map). Positivity lemmas (e.g. yardstick and species masses) discharge $m>0$ by composing positivity of the yardstick with positivity of $\varphi$ powers. Coordinate unification is imported so the pipeline need not choose between equivalent quark conventions. No deep tactic scripts: the argument is assembly of upstream closed facts into named forward constants.

why it matters in Recognition Science

Gives the verification layer explicit, positive quark (and electron) masses at $\mu^*$ so later checks can quote numbers instead of the abstract mass functor. It closes the forward direction of the mass story: Anchor and MassLaw supply the law; ZMapForcing fixes the charge integerization; QuarkCoordinateUnification removes convention ambiguity; this module emits the species list. Used_by is empty in the graph snapshot, so it currently acts as a terminal verification surface rather than an intermediate lemma server. Lands in the broader RS mass program (φ-ladder, yardstick, gap term) without touching the T5–T8 forcing chain directly.

scope and limits

Does not claim experimental agreement of predicted masses with PDG values.
Does not re-prove the master mass law, Z-map forcing, or coordinate unification.
Does not derive sector yardsticks or rung assignments from the T0–T8 chain here.
Does not treat neutrino, boson, or composite hadron masses.
Does not assert uniqueness of the anchor $\mu^*$ beyond imported Anchor conventions.

depends on (5)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Masses.Anchor module_import
IndisputableMonolith.Masses.MassLaw module_import
IndisputableMonolith.Masses.ZMapForcing module_import
IndisputableMonolith.Verification.QuarkCoordinateUnification module_import

declarations in this module (28)

def m_up L59
def m_charm L61
def m_top L63
def m_down L65
def m_strange L67
def m_bottom L69
def m_electron L72
theorem yardstick_pos L75
theorem m_up_pos L85
theorem m_charm_pos L86
theorem m_top_pos L87
theorem m_down_pos L88
theorem m_strange_pos L89
theorem m_bottom_pos L90
theorem m_electron_pos L91
theorem charm_to_up_ratio_structural L100
theorem charm_to_up_eq_phi11 L127
theorem bottom_to_strange_eq_phi6 L141
theorem quark_rungs_from_torsion L159
theorem quark_Z_from_charges L171
theorem lepton_Z_from_charge L177
def residue_from_pipeline L185
theorem pipeline_equals_residue_form L190
theorem all_quark_predictions_have_derived_residue_coordinates L197
theorem up_yardstick_components L223
theorem down_yardstick_components L228
structure QuarkNonCircularity L239
def non_circular L250