heavyQuarkClosureObstructionCert_holds
plain-language theorem explainer
The theorem certifies that under the current bridge the raw SI masses for charm, bottom and top quarks lie many orders below their PDG values while the required extra phi-exponents differ across the three channels. Mass modelers cite it to flag the absence of a universal extra exponent and the consequent need for a separate mass-sector bridge. The proof is a direct term construction that assembles the four fields of the obstruction certificate from four upstream norm_num lemmas.
Claim. Let $m_c^raw$, $m_b^raw$, $m_t^raw$ be the raw masses in eV obtained from the present non-mass bridge and let $m_c^PDG$, $m_b^PDG$, $m_t^PDG$ be the corresponding PDG values. Let $r_c$, $r_b$, $r_t$ be the extra phi-exponents required to match each PDG mass. Then $m_c^raw < m_c^PDG / 10^{18}$, $m_b^raw < m_b^PDG / 10^{18}$, $m_t^raw < m_t^PDG / 10^{18}$, and $r_c ≠ r_b$, $r_b ≠ r_t$, $r_c ≠ r_t$.
background
The Heavy Quark Full-Closure Obstruction module records a numerical audit under the Recognition Science mass formula (yardstick times phi to the power rung minus eight plus gap(Z)). With E_coh_SI fixed at approximately 2.4101e-16 eV and the listed massAtAnchor values, the raw SI masses for the three heavy quarks fall far short of observation. The structure HeavyQuarkClosureObstructionCert packages this failure into four fields: three strict inequalities showing each raw_eV is less than the PDG value divided by 10^18, plus the statement that the three required phi-exponents are pairwise distinct.
proof idea
The proof is a term-mode record construction. It supplies the charm_below field by the theorem charm_raw_far_below_PDG, the bottom_below field by bottom_raw_far_below_PDG, the top_below field by top_raw_far_below_PDG, and the exponents_split field by required_exponents_not_equal. Each of those four lemmas is proved by unfolding the relevant raw and PDG constants followed by norm_num.
why it matters
The result closes the audit certificate in the masses domain, confirming that the existing bridge together with the phi-ladder cannot reach the observed GeV-scale heavy-quark masses. It therefore isolates the requirement for an additional mass-sector bridge, consistent with the T0-T8 forcing chain where mass relations sit downstream of J-cost and defectDist. No downstream declarations depend on it, leaving open the concrete form of any future bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.