predict_mass_sdgt
plain-language theorem explainer
predict_mass_sdgt defines the SDGT mass prediction as the sector yardstick multiplied by phi raised to the power of the adjusted rung. Particle physicists modeling masses on the phi-ladder in Recognition Science cite this definition to obtain explicit formulas for leptons, quarks, and electroweak states. It is a direct algebraic composition of the yardstick, rung_sdgt, gap, and cross_sector_shift functions with no additional lemmas.
Claim. The SDGT mass prediction for sector $s$ and particle name $n$ is $m = A_s · φ^{r_{sdgt}(s,n) - 8 + g(s,n) + σ(s)}$, where $A_s$ is the sector yardstick, $r_{sdgt}$ is the SDGT rung, $g(s,n)$ is the gap computed from the charge index $Z$, and $σ(s)$ is the cross-sector shift.
background
The AnchorPolicy module supplies concrete mass formulas on the phi-ladder for the four sectors (Lepton, UpQuark, DownQuark, Electroweak). The yardstick $A_s$ is $2^{B_{pow}(s)} E_{coh} φ^{r_0(s)}$, taken from the Anchor module. The local gap function extracts a logarithmic correction from the charge index $Z$ of the named particle via chargeMap. Upstream, Gap45.Derivation.gap supplies the fixed gap value 45 as the product of closure and Fibonacci factors, while cross_sector_shift adds +12 for down quarks to correct for cube-edge traversal.
proof idea
This is a direct definition that multiplies the yardstick function by Constants.phi raised to the explicit exponent built from rung_sdgt, the local gap, the constant -8, and cross_sector_shift. No tactics or lemmas are invoked; the body is the literal formula implementation.
why it matters
The definition realizes the Recognition Science mass formula yardstick · φ^(rung - 8 + gap(Z)) with the SDGT rung and sector shift. It sits inside the Masses domain and supports numerical predictions once rung_sdgt and gap are supplied. No parent theorems are recorded in the used_by edges, so its role remains that of a concrete anchor for spectrum calculations on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.