required_exponents_not_equal
plain-language theorem explainer
required_exponents_not_equal establishes that the phi-exponents needed to match PDG masses for charm, bottom, and top quarks from the current massAtAnchor values are pairwise distinct. Mass-model auditors cite it to certify that no single adjustment closes all three heavy-quark channels under the existing bridge. The proof is a direct numerical comparison obtained by unfolding the three constant definitions and invoking norm_num.
Claim. Let $r_c$, $r_b$, and $r_t$ be the real numbers required by the phi-ladder mass formula to reproduce the PDG masses of the charm, bottom, and top quarks from the given massAtAnchor values. Then $r_c ≠ r_b$, $r_b ≠ r_t$, and $r_c ≠ r_t$.
background
The Heavy Quark Full-Closure Obstruction module records the numerical obstruction to deriving heavy-quark masses from the current non-mass dimensional bridge. It uses E_coh_SI approximately 2.4101e-16 eV together with RS-native massAtAnchor values (charm ≈ 4981.65, bottom ≈ 8248.93, top ≈ 89392.14) to show that raw SI masses lie many orders below PDG values. The sibling definitions charm_required_phi_exponent, bottom_required_phi_exponent, and top_required_phi_exponent compute the distinct exponents needed for each quark on the phi-ladder.
proof idea
The proof unfolds the definitions of charm_required_phi_exponent, bottom_required_phi_exponent, and top_required_phi_exponent, then applies norm_num to verify the three inequalities hold numerically.
why it matters
The result supplies the exponents_split field inside heavyQuarkClosureObstructionCert_holds, the audit certificate that the current bridge plus massAtAnchor does not derive the heavy-quark GeV masses. It aligns with the mass formula yardstick * phi^(rung - 8 + gap(Z)) on the phi-ladder and underscores the need for a further mass-sector bridge. The module states explicitly that this is an audit certificate, not a physics theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.