row_charm_up_structural_anchor_agree
plain-language theorem explainer
This theorem shows that the ratio of structural mass predictions for the charm and up quarks matches the ratio obtained from the anchor mass formula. Researchers deriving quark masses within the Recognition Science phi-ladder framework would cite it to verify internal consistency of the P0-Q bridge rows. The proof proceeds as a direct rewrite using the already-proved structural and anchor ratio theorems for the charm-up pair.
Claim. The ratio of the structural charm-quark mass prediction to the up-quark mass prediction equals the ratio of the anchor mass expression at charm to the anchor mass expression at up: $ (structural charm mass) / (structural up mass) = (anchor mass at charm) / (anchor mass at up) $, where structural masses are the phi-power formulas from the Verification module and anchor masses follow the exponential rung-plus-gap formula.
background
The Quark Absolute Bridge Score Card module deepens QuarkScoreCard by showing exact agreement on within-family ratios for the u/c/t sector. Structural predictions are defined as charm_quark_pred = phi^45 / 2000000 and up_quark_pred = phi^34 / 2000000. Anchor masses are given by massAtAnchor(f) = M0 * exp( ((rung f - 8 + gap(ZOf f)) * log phi) ). Upstream row_structural_charm_up_ratio_rpow states the structural ratio equals phi^11; row_anchor_charm_up_ratio_rpow states the anchor ratio equals phi^11, both obtained from the rung difference of 11 between charm and up.
proof idea
This is a one-line wrapper proof. It applies the rewrite tactic to the goal by substituting row_structural_charm_up_ratio_rpow on the left-hand side and row_anchor_charm_up_ratio_rpow on the right-hand side.
why it matters
The theorem populates the charm_up_ratio_agrees field inside quarkAbsoluteBridgeScoreCardCert_holds, which certifies the full scorecard. It fills the P0-Q01 bridge row in the physical derivation plan. Within the Recognition Science framework it confirms that the phi-ladder mass formula (yardstick times phi to the power rung-8+gap) yields ratios identical to the structural predictions, supporting the self-similar fixed point phi and the eight-tick octave. The module records that the absolute MeV bridge remains partial pending SI calibration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.