bottom_required_phi_exponent
plain-language theorem explainer
The definition bottom_required_phi_exponent supplies the real constant 102.02875053742147 as the phi-exponent needed to scale the raw massAtAnchor value for the bottom quark up to its PDG mass under the existing bridge. Mass-sector auditors cite this value when checking whether a single extra exponent can close all three heavy-quark channels. It is introduced by direct literal assignment with no lemmas or reduction steps.
Claim. Let $r_b$ be the real exponent satisfying $m_b = m_{anchor} · ϕ^{r_b}$ for the bottom quark under the current non-mass bridge. Then $r_b = 102.02875053742147$.
background
The module records that raw SI masses obtained from E_coh_SI ≈ 2.4101e-16 eV and the listed massAtAnchor values (bottom ≈ 8248.93) fall many orders of magnitude below PDG masses. This definition isolates the precise extra phi-exponent required for the bottom channel alone. The module functions as an audit certificate rather than a derivation, preventing scorecards from being read as first-principles results.
proof idea
The declaration is a direct constant definition that assigns the literal 102.02875053742147. No lemmas are invoked and no tactics are executed.
why it matters
The value is unfolded inside the theorem required_exponents_not_equal, which proves the three required exponents are pairwise distinct by norm_num. It is also a field of the structure HeavyQuarkClosureObstructionCert that certifies the absence of any universal extra phi-exponent across charm, bottom and top. This supports the module's audit conclusion that a further mass-sector bridge must still be proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.