charm_required_phi_exponent
plain-language theorem explainer
The definition supplies the numeric value 100.60116086852311 as the phi-exponent required to scale the RS-native charm anchor to the PDG mass under the existing bridge. Mass-sector auditors cite it when testing whether a single extra exponent can close all three heavy-quark channels. It enters as a direct real literal with no reduction steps.
Claim. The real constant \(k_c\) satisfying \(m_{\text{charm, PDG}} = m_{\text{anchor, charm}} \times \phi^{k_c}\) in the Recognition Science mass formula equals 100.60116086852311.
background
The module records the numerical obstruction to full heavy-quark closure under the current non-mass dimensional bridge. It deploys E_coh_SI (approximately 2.4101e-16 eV) from the neutron-lifetime route together with RS-native massAtAnchor values (charm approximately 4981.65) to show that raw SI masses lie many orders below PDG values. The phi-ladder mass formula therefore cannot reach observed GeV-scale charm, bottom, or top masses without an additional sector bridge. This definition supplies the charm-channel exponent used in the obstruction certificate.
proof idea
One-line definition that directly assigns the floating-point literal; no lemmas or tactics are invoked.
why it matters
The value populates the charm_required_phi_exponent field inside HeavyQuarkClosureObstructionCert, whose exponents_split clause records that the three required exponents differ. The parent structure certifies that no single universal extra phi-exponent closes the heavy-quark sector under the present bridge. It therefore supports the module's audit conclusion that a further mass-sector bridge must still be proved and touches the open question of completing the mass derivation for heavy quarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.