massAtAnchor
plain-language theorem explainer
massAtAnchor defines the Recognition Science anchor mass for each Standard Model fermion on the phi-ladder. Researchers verifying quark mass hierarchies against golden-ratio predictions cite this when checking structural ratios in the QuarkAbsoluteBridgeScoreCard. The definition directly transcribes the mass formula as M0 times phi to the power (rung minus 8 plus gap at Z), expressed via the exponential of the scaled logarithm.
Claim. For a fermion $f$, the anchor mass is $m_*(f) = M_0$ exp$((r(f)-8 + g(Z(f))) $ln$ $phi)$, where $r$ is the rung function, $g(Z) = $ln$(1 + Z/phi)/$ln$ phi$ is the gap, $Z$ is the charge-indexed integer from the Z-map, $M_0$ the base scale, and $phi$ the golden ratio.
background
The RSBridge.Anchor module defines the Fermion inductive type as the twelve Standard Model species (six quarks, three charged leptons, three neutrinos). ZOf maps each species to its integer charge index Z = q̃² + q̃⁴ (+4 for quarks). The gap function is the display map F(Z) = ln(1 + Z/phi)/ln(phi), which the module states equals the integrated RG residue at the anchor scale. The rung function supplies the integer level on the phi-ladder according to lepton or quark sector.
proof idea
This is a direct definition that composes the rung and gap functions into the exponential form of the phi-power law. It evaluates the exponent (rung f - 8 + gap (ZOf f)) times log phi, applies Real.exp, and scales the result by M0. No lemmas or tactics are used beyond the arithmetic primitives.
why it matters
This definition supplies the anchor masses required by QuarkAbsoluteBridgeScoreCardCert and the row theorems that certify ratios such as charm/up = phi^11 and bottom/strange = phi^6. It realizes the mass-at-anchor step of the Single Anchor Phenomenology claim, where gap(ZOf i) approximates the RG integral from ln mu* to ln m_phys. In the framework it instantiates the phi-ladder mass formula, consistent with the eight-tick octave through the rung structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.