pith. machine review for the scientific record. sign in
def definition def or abbrev high

res_down

show as:
view Lean formalization →

The definition supplies the quarter-ladder rung coordinate -16 for the down quark within the Recognition Science mass model. Researchers computing structural quark masses from the phi-ladder cite this value when applying the yardstick scaling formula. It enters as a direct constant assignment that matches the topological position R = -64/4 listed in the Quarter-Ladder Hypothesis.

claimThe rung position assigned to the down quark on the $phi$-ladder is $R_{rm down}=-16$.

background

The module formalizes quark mass derivation under the Quarter-Ladder Hypothesis. Quarks share the same structural base mass as leptons (Sector Gauge B=-22, R0=62) but sit on quarter-integer rungs of the phi-ladder. The down quark receives rung R = -16.00, written as -64/4, consistent with the listed ideal positions and generation spacing steps of 7.75, 2.50, and 5.50 rungs.

proof idea

The declaration is a direct constant definition that evaluates the rational -64/4.

why it matters in Recognition Science

This rung assignment supplies the input coordinate for the down-quark mass entry in the T12 quark masses section. It implements one of the six topological positions required by the Quarter-Ladder Hypothesis to produce masses within a few percent of observation. Light-quark discrepancies are left open for later inclusion of non-perturbative QCD corrections, pending reconciliation with the parameter-free core mass layer.

scope and limits

formal statement (Lean)

  68def res_down : ℚ := -64 / 4

used by (1)

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

depends on (1)

Lean names referenced from this declaration's body.