HeavyQuarkClosureObstructionCert
plain-language theorem explainer
The structure certifies that raw SI masses for charm, bottom, and top quarks lie many orders of magnitude below PDG values while the phi-exponents needed to reach those scales are pairwise distinct. An auditor checking mass derivations in Recognition Science would cite it to document the gap in the current non-mass dimensional bridge. The structure is assembled directly from the precomputed raw_eV, PDG_eV, and required_phi_exponent constants without further lemmas.
Claim. Let $m_c^raw$, $m_b^raw$, $m_t^raw$ be the raw SI masses and $m_c^PDG$, $m_b^PDG$, $m_t^PDG$ the PDG values. Let $r_c$, $r_b$, $r_t$ be the required phi-exponents. The certificate asserts $m_c^raw < m_c^PDG / 10^{18}$, $m_b^raw < m_b^PDG / 10^{18}$, $m_t^raw < m_t^PDG / 10^{18}$, together with $r_c ≠ r_b$, $r_b ≠ r_t$, and $r_c ≠ r_t$.
background
The module records the numerical obstruction to full heavy-quark closure from the current non-mass dimensional bridge. It employs E_coh_SI from the neutron-lifetime route and RS-native massAtAnchor values to obtain raw_eV for charm, bottom, and top. These are compared to PDG masses (charm_PDG_eV = 1.27e9, bottom_PDG_eV = 4.18e9, and the top counterpart) while the required_phi_exponent for each channel is the additional phi power needed to match the PDG scale.
proof idea
The declaration is a structure definition that packages four field assertions. The three below fields are direct inequalities between the pre-defined raw_eV and PDG_eV constants divided by 1e18. The exponents_split field is the conjunction of three pairwise inequalities on the pre-defined required_phi_exponent constants. No tactics or lemmas are applied; the structure simply records these numerical facts as a single certificate object.
why it matters
This certificate is used by the theorem heavyQuarkClosureObstructionCert_holds to witness the obstruction. It fills the audit role described in the module documentation, preventing the mass scorecards from being read as first-principles derivations. In the Recognition Science framework it highlights the gap between the phi-ladder mass formula and the observed heavy-quark spectrum, indicating that the current non-mass dimensional bridge is insufficient and that an additional mass-sector bridge remains to be constructed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.