predict_mass
The master mass law defines predicted particle mass as the product of a sector yardstick and phi raised to the adjusted rung position. Modelers working on fermion spectra or Yukawa couplings cite it to obtain explicit mass values from rung and charge inputs. The definition is a direct algebraic expression that composes the yardstick function with phi exponentiation and the gap correction term.
claimThe predicted mass $m$ of a species in sector $s$ at rung $r$ with charge index $Z$ is $m = y(s) · φ^{r-8 + g(Z)}$, where $y(s)$ is the sector yardstick, $φ$ is the golden ratio, and $g(Z)$ is the recognition gap correction.
background
The module formalizes the master mass formula derived from first principles in Recognition Science. Every stable recognition state occupies a rung on the φ-ladder; mass is proportional to coherence energy scaled by sector yardstick and rung position. The formula reads $m = y(s) · φ^{r-8 + g(Z)}$, where 8 is the fundamental cycle period from the eight-tick octave and $g(Z)$ supplies the charge-based shift.
proof idea
The definition is a direct one-line expression that multiplies the yardstick of the supplied sector by phi raised to the real exponent (rung - 8 + gap_correction Z_val). It draws the gap_correction term from ConstantDerivations and the phi constant from RSNativeUnits.
why it matters in Recognition Science
This definition supplies the core mass engine used by SMVerificationCert to certify all fermion masses positive and by HiggsYukawaBridgeCert to certify Yukawa positivity and phi scaling. It realizes the φ-ladder scaling required by the Recognition Composition Law and the eight-tick octave (period 8) in the T0-T8 forcing chain, with the gap term accounting for the D=3 integration gap of 45.
scope and limits
- Does not compute numerical masses without explicit sector, rung, and Z inputs.
- Does not prove positivity of the resulting mass value.
- Does not define the yardstick function for each sector.
- Does not supply empirical calibration beyond the gap correction term.
Lean usage
def fermionMass (f : Fermion) : ℝ := predict_mass (fermionSector f) (fermionRung f) (fermionZ f)formal statement (Lean)
40noncomputable def predict_mass (sector : Sector) (rung : ℤ) (Z_val : ℤ) : ℝ :=
proof body
Definition body.
41 yardstick sector * (phi ^ ((rung : ℝ) - 8 + gap_correction Z_val))
42
43/-- Mass is positive for any valid configuration. -/