Valid
plain-language theorem explainer
Valid encodes the three conditions under which an AnchorCert is consistent with a charge map Z and gap display Fgap. Mass-derivation and anchor-policy work cites it to enforce positivity of the M0 bound together with interval containment for both Fgap values and per-species residues. The declaration is a plain structure that directly assembles the three field propositions with no lemmas or tactics.
Claim. A certificate $C$ is valid for charge map $Z$ and gap function $Fgap$ when the lower endpoint of $C$'s $M0$ interval is positive, $Fgap(Z(i))$ lies inside the certified gap interval around $Z(i)$ for every species $i$, and the residue interval of each species is contained inside its corresponding certified gap interval.
background
AnchorCert is the structure that packages an $M0$ interval, a map from species to residue intervals, and per-charge center and eps values that define gap intervals. Igap extracts the closed interval $[center(z)-eps(z),center(z)+eps(z)]$ using the nonnegativity of eps. The module Recognition.Certification supplies the interface between external certificates and the integer charge map Z together with the display function Fgap (an alias for the closed-form gap). Upstream, Z maps sectors and rational charges to integers, M0 is fixed at 1 with a positivity theorem, Species is the inductive type of fermions plus W, Z, H bosons, and Fgap is the gap function used in the certified anchor policy.
proof idea
The declaration is a structure definition whose body consists of the three field assertions M0_pos, Fgap_in and Ires_in_Igap. No lemmas are applied and no tactics are invoked; the structure simply records the conjunction of the three propositions.
why it matters
Valid supplies the hypothesis required by anchor_identity_from_cert and equalZ_residue_from_cert, which in turn feed ml_derivation_falsifiable and the nuclear transmutation cost theorems. It therefore closes the certification step that links external interval data to the phi-ladder mass formula at the anchor point. The definition touches the Recognition framework's anchor policy but leaves open the concrete construction of eps and center values that would discharge a full existence claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.