row_anchor_charm_up_ratio_exp
plain-language theorem explainer
The anchor mass ratio of the charm quark to the up quark equals exp(11 log phi). Researchers checking Recognition Science within-family quark ratios on the phi-ladder cite this when confirming the anchor bridge. The short tactic proof applies the general anchor_ratio lemma after fixing equal Z values and a rung difference of eleven.
Claim. $m_0(c)/m_0(u)=e^{11 log phi}$, where $m_0(f)$ denotes the native anchor mass $M_0 exp(((rung(f)-8+gap(ZOf(f)))log phi)$ for fermion $f$.
background
massAtAnchor(f) is the native anchor expression $M_0 exp(((rung f : R) - 8 + gap(ZOf f)) log phi)$. The anchor_ratio theorem states that when ZOf f = ZOf g the ratio massAtAnchor f / massAtAnchor g simplifies to exp(((rung f - rung g) log phi)). rung assigns .u to 4 and .c to 15, so the difference is 11. This declaration sits inside the Quark Absolute Bridge Score Card module, whose MODULE_DOC describes Phase 0 P0-Q rows that verify agreement between the anchor bridge and the structural rs_mass_MeV formula on u/c/t within-family ratios.
proof idea
The tactic proof first obtains ZOf .c = ZOf .u by decide, invokes anchor_ratio .c .u on that hypothesis to produce the exponential form, then proves the rung difference equals 11 by simp [rung] followed by norm_num, and finishes with simpa [hr] using the earlier result.
why it matters
This supplies the exponential form that row_anchor_charm_up_ratio_rpow rewrites as phi^11, completing one of the within-family ratio checks listed in the module's Phase 0 rows. It relies on the rung assignments that encode the eight-tick octave structure and on the phi fixed point from the T5-T6 forcing chain. The absolute MeV bridge remains open, as noted in the MODULE_DOC falsifier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.