schemeReconciliationCert_holds
plain-language theorem explainer
The theorem certifies that the scheme reconciliation certificate holds by confirming the gap function meets its zero and positivity conditions for neutrinos, up-type quarks, down-type quarks, and leptons together with the charm residual bound. A physicist reconciling structural phi-ladder masses against running-mass anomalous dimensions would cite it to close the consistency check between the two mass expressions. The proof is a direct term construction that assembles the component gap theorems into the certificate structure.
Claim. The gap function satisfies $gap(0)=0$, $gap(276)>0$, $gap(24)>0$, $gap(1332)>0$, the gap-equals-running hypothesis is satisfiable, and the percent residual between $gap(276)·log φ$ and the integrated two-loop charm mass-anomalous-dimension residual lies below one.
background
In the Recognition Science mass framework the structural rung formula without gap correction is compared to the anchor-corrected formula that inserts the gap(Z) term into the exponent. The gap function is the positive correction obtained from the logarithm of one plus the charge ratio over phi; it vanishes at zero charge. Upstream results establish gap zero at the neutrino, positive gaps for up-type quarks at 276, down-type quarks at 24, and leptons at 1332, plus the charm residual bound under one percent.
proof idea
The proof is a one-line term-mode wrapper that constructs the SchemeReconciliationCert structure by supplying the gap-zero theorem for neutrinos, the positivity theorems for the up, down, and lepton gaps, the trivial satisfiability witness, and the charm residual bound theorem.
why it matters
This theorem completes the master certificate for mass-scheme reconciliation, linking the phi-ladder mass formula with gap corrections to the two-loop RGE running in the quark sector. It supports overall mass predictions by verifying consistency between structural and running descriptions. No open questions are directly touched, but it closes the charm-sector reconciliation within the stated tolerance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.