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

massAtAnchor

show as:
view Lean formalization →

The massAtAnchor definition supplies the explicit formula for the mass of any Standard Model fermion at the recognition anchor scale using rung offset, gap on ZOf, and phi scaling. Researchers deriving quark and lepton hierarchies from the phi-ladder cite it when testing ratio predictions against data. It is a direct definition that composes the supplied rung, gap, and exponential without further lemmas.

claimThe anchor mass of fermion $f$ is $M_0$ times the exponential of $(r(f)-8+g(Z(f)))$ times the natural logarithm of the golden-ratio fixed point, where $r(f)$ is the rung of $f$, $Z(f)$ its charge index, and $g$ the gap function $g(Z)=ln(1+Z/phi)/ln phi$.

background

The RSBridge.Anchor module enumerates the twelve Standard Model fermions via the Fermion inductive type. Rung assigns an integer level to each species by sector (lepton, up-quark, down-quark). Gap is the closed-form residue $g(Z)=ln(1+Z/phi)/ln phi$ supplied by AnchorPolicy. M0 and Constants.phi are imported from the mass framework and CPM constants bundle. This implements the Recognition Science mass formula on the phi-ladder: yardstick times phi to the power (rung minus 8 plus gap(Z)). Upstream results from Gap45.Derivation and AnchorPolicy supply the concrete gap and rung definitions.

proof idea

One-line definition that multiplies the base mass M0 by the exponential of the offset (rung f minus 8 plus gap of ZOf f) times the natural log of phi.

why it matters in Recognition Science

This definition supplies the concrete mass values used by QuarkAbsoluteBridgeScoreCardCert and the ratio theorems (bottom/strange, charm/up, strange/down) to certify phi-power predictions. It realizes the Recognition Science mass formula on the phi-ladder and connects to the forcing chain through T5 J-uniqueness, T6 phi fixed point, and the eight-tick octave. It closes the bridge from abstract recognition composition to observable particle masses at the anchor scale.

scope and limits

formal statement (Lean)

 104noncomputable def massAtAnchor (f : Fermion) : ℝ :=

proof body

Definition body.

 105  M0 * Real.exp (((rung f : ℝ) - 8 + gap (ZOf f)) * Real.log (Constants.phi))
 106

used by (26)

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

depends on (18)

Lean names referenced from this declaration's body.