zeroWidthCert_valid
plain-language theorem explainer
The lemma shows that the zero-width certificate built from an arbitrary charge map Z and gap display Fgap meets all three validity conditions. Researchers formalizing minimal anchors in the Recognition mass framework would cite it when verifying base certificates. The proof is a direct tactic construction that applies simplification to the mass bound and linear arithmetic to the two interval inclusions.
Claim. Let $C$ be the zero-width certificate constructed from charge map $Z$ and gap function $F$. Then $C$ satisfies: its lower mass bound is positive; $F(Z(i))$ lies inside the gap interval $I(C,Z(i))$ for every species $i$; and the residue interval of $C$ at $i$ is contained in $I(C,Z(i))$.
background
The Certification module supplies the Valid structure, which encodes the three requirements an AnchorCert must meet relative to a charge map $Z$ and a gap display $F$. The structure demands a strictly positive lower mass bound, membership of each $F(Z(i))$ in the corresponding Igap interval of the certificate, and containment of each residue interval inside its Igap interval. Upstream material includes the canonical identity event at the J-cost minimum and the integer charge map $Z$ that assigns values to lepton, up-quark, and down-quark sectors.
proof idea
The tactic proof refines the Valid record directly. The M0 positivity field is discharged by simplification on the zero-width certificate definition. Each interval condition is handled by first simplifying the definitions of Igap and memI, then applying the constructor tactic followed by linear arithmetic to obtain the required bounds.
why it matters
The result certifies the minimal zero-width case inside the anchor policy, supplying a concrete base object that later certified consequences in AnchorPolicyCertified can reference. It closes a verification step for the residue-to-gap relation that appears in the mass ladder construction. No open scaffolding remains for this particular certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.