top_required_phi_exponent
The definition assigns the real number 104.80972375767824 as the phi-exponent required to match the top quark's PDG mass from its Recognition Science massAtAnchor value. Heavy-quark mass auditors cite it when verifying whether a single extra exponent closes all three channels. It enters as a plain constant definition with no computational steps.
claimThe required exponent in the phi-ladder for the top quark mass under the current bridge equals $104.80972375767824$.
background
The module computes raw SI masses for charm, bottom, and top quarks using the coherent energy scale E_coh_SI from the neutron-lifetime route together with the massAtAnchor values from the phi-ladder. These raw values lie many orders of magnitude below the PDG masses, indicating that the existing bridge does not yet derive the observed GeV-scale masses. The three required_phi_exponent constants record the precise extra exponents needed in the mass formula yardstick * phi^(rung - 8 + gap(Z)) to reach the PDG values.
proof idea
The declaration is introduced directly as a real-number constant with an empty proof body.
why it matters in Recognition Science
It supplies one of the three numerical inputs to the HeavyQuarkClosureObstructionCert structure, which concludes that the required exponents differ across the charm, bottom, and top channels. This prevents misinterpretation of the mass scorecards as complete derivations and flags the need for an additional mass-sector bridge. The obstruction aligns with the Recognition Science forcing chain landmarks, particularly the phi-ladder construction and the eight-tick octave.
scope and limits
- Does not derive the numerical value from prior axioms or lemmas.
- Does not claim that any single extra exponent suffices for all heavy quarks.
- Does not address the physical origin of the required exponents.
formal statement (Lean)
55def top_required_phi_exponent : ℝ := 104.80972375767824
proof body
Definition body.
56