charm_required_phi_exponent
The definition supplies the real number 100.60116086852311 as the phi-exponent required to scale the RS-native charm mass anchor to the observed PDG value. Mass-sector auditors cite this constant when verifying that no single extra exponent reconciles all three heavy-quark channels with PDG data. It is introduced as a literal constant computed from the ratio of observed to anchor masses in phi units.
claimThe required phi-exponent for the charm quark is the real number $100.60116086852311$.
background
The module records numerical obstructions in the heavy-quark sector using the coherent energy scale approximately 2.4101e-16 eV together with RS-native massAtAnchor values near 4981.65 for charm. Raw SI masses computed from these anchors lie many orders of magnitude below PDG values, so the current bridge plus massAtAnchor does not derive the observed GeV-scale masses. The definition records the precise additional phi-ladder exponent that would be needed for charm alone as part of an audit certificate preventing misreading of scorecards as first-principles derivations.
proof idea
The declaration is a direct definition that binds the floating-point literal 100.60116086852311. No lemmas or tactics are applied.
why it matters in Recognition Science
The constant enters the HeavyQuarkClosureObstructionCert structure, which certifies that the required exponents for charm, bottom, and top are pairwise unequal and therefore no single universal extra phi-exponent closes the sector. It supports the module conclusion that the current bridge does not derive the heavy-quark GeV masses and highlights the need for a further mass-sector bridge. The value is consistent with the phi-ladder mass formula in which exponents adjust rung positions on the self-similar fixed point.
scope and limits
- Does not derive the PDG charm mass from the Recognition Science axioms.
- Does not claim a universal exponent that works for all heavy quarks.
- Does not provide a closed-form expression for the required exponent.
- Does not resolve the obstruction to full heavy-quark closure.
Lean usage
unfold charm_required_phi_exponent; norm_numformal statement (Lean)
53def charm_required_phi_exponent : ℝ := 100.60116086852311