top_charm_ratio
plain-language theorem explainer
The theorem shows that the ratio of the predicted top quark mass to the predicted charm quark mass equals exactly the sixth power of the golden ratio. Researchers verifying quark mass hierarchies against the phi-ladder in Recognition Science would cite this when scoring structural predictions. The proof is a term-mode reduction that unfolds the two mass predicates, confirms positivity of the common denominator, and applies field simplification to cancel all other factors.
Claim. The ratio of the top quark mass prediction to the charm quark mass prediction equals $phi^6$, where $phi$ is the golden ratio.
background
Recognition Science places quark masses on the phi-ladder via the formula yardstick times $phi$ raised to (rung minus 8 plus gap), with gap defined as the product of closure and Fibonacci factors. The gap derivation establishes this product equals 45, fixing the charm rung at 45 and the top rung at 51 in the present predictions. The module imports the scale function that returns $phi^k$ and treats experimental PDG values as quarantined constants rather than derived quantities.
proof idea
The term proof first unfolds the definitions of the top and charm quark predictions. It then constructs a positivity witness for the denominator $phi^{45}/2000000$ via power positivity and norm_num. Field simplification then cancels the common factors, leaving exactly $phi^6$.
why it matters
This declaration supplies the P0-Q structural row used by the QuarkScoreCard and the TopQuarkMassScoreCard. It realizes the six-rung gap between top and charm on the phi-ladder, consistent with the self-similar fixed point of phi and the eight-tick octave structure. The result closes one verification step for the multi-GeV top mass scale without invoking the full gap correction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.