charm_up_ratio
plain-language theorem explainer
The ratio of predicted charm quark mass to up quark mass equals exactly phi to the 11th power, encoding an 11-rung generation gap on the phi-ladder. Quark mass hierarchy verifiers in Recognition Science cite this when building structural scorecards for the up sector. The term-mode proof unfolds the two mass predictions, adds a positivity fact for an intermediate term, and reduces the ratio by field simplification.
Claim. The ratio of the predicted charm quark mass to the predicted up quark mass equals exactly $phi^{11}$, where each prediction is obtained from the Recognition Science mass formula on the phi-ladder using the appropriate rung and gap for the respective quark.
background
The module compares machine-verified mass predictions against PDG 2024 values while treating experimental numbers as imported constants. The phi-ladder implements the mass formula yardstick times phi to the power (rung minus 8 plus gap(Z)). Upstream, Gap45.Derivation defines gap as the product of closure and Fibonacci factors and proves the main theorem that this gap equals 45. AnchorPolicy supplies noncomputable rung and gap functions that dispatch on sector (UpQuark here) and quark name to obtain the integer exponents.
proof idea
The term proof first unfolds charm_quark_pred and up_quark_pred. It then asserts positivity of phi to the 34 over 2 million via div_pos and norm_num. Finally field_simp with the positivity witness cancels all other factors, leaving precisely phi to the 11.
why it matters
The result directly populates the P0-Q structural row in QuarkScoreCard.row_charm_up_ratio, which records m_c over m_u equals phi to the 11. It instantiates the Recognition Science mass formula that descends from the self-similar fixed point phi (T6) and the eight-tick octave structure. No open scaffolding remains for this particular ratio.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.