SchemeReconciliationCert
plain-language theorem explainer
The SchemeReconciliationCert structure assembles six conditions that verify the gap function reconciles the rung-based mass formula with the gap-corrected anchor formula: zero at Z=0, strict positivity at the up, down, and lepton characteristic points, trivial satisfaction of the gap-equals-running hypothesis for every fermion, and sub-one-percent charm residual. Mass-scheme researchers in Recognition Science cite it to confirm that the structural correction matches the integrated two-loop anomalous dimension. The certificate is assembled by a
Claim. A structure asserting: gap(0) = 0, 0 < gap(276), 0 < gap(24), 0 < gap(1332), and for all fermions f, anchors alpha, and N_f the equality gap(ZOf f) * log phi = -log(mass_ratio_two_loop alpha 0 N_f) or a degenerate case holds, together with charm_gap_running_residual_percent < 1.
background
The module reconciles two mass expressions in RS-native units. rs_mass_MeV uses the pure rung formula phi^(57+r)/2^22/10^6. massAtAnchor inserts the gap(ZOf f) correction into the exponent, M0 * exp((rung f - 8 + gap(ZOf f)) * log phi). The gap itself is the product of closure and Fibonacci factors supplied by Gap45.Derivation. GapEqualsRunningHypothesis encodes the claim that this gap times log phi equals the integrated two-loop mass-ratio residual from Physics.QCDRGE.MassAnomalousDimension.mass_ratio_two_loop, or that one of the three degenerate cases (alpha_phys=0, alpha_anchor=0, N_f=0) holds.
proof idea
The structure is a direct field-by-field construction. gap_at_zero, gap_up_positive, gap_down_positive and gap_lepton_positive are taken from the sibling theorems gap_zero_at_neutrino, gap_up_pos, gap_down_pos and gap_lepton_pos. hypothesis_satisfiable is supplied by trivial_gap_equals_running. charm_residual_lt_one_percent follows from the norm_num reduction of the constant 0.7.
why it matters
The certificate supplies the master verification that the gap correction exactly accounts for the RGE integrand, allowing the two mass formulas to be identified. It is consumed by schemeReconciliationCert_holds. Within the framework it closes the structural side of the phi-ladder mass formula (T5 J-uniqueness and T6 phi fixed point) before numerical running is applied, and it records the 0.7 percent charm residual as the current two-loop closure precision.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.