anchorEq_implies_Zeq_nonneg
plain-language theorem explainer
If a candidate map Z' satisfies AnchorEq, meaning Fgap(Z' i) equals Fgap(Z i) for every species i, and Fgap is injective on nonnegative integers, then Z' i equals Z i whenever both values are nonnegative. Researchers certifying mass anchors or ruling out ablations cite this to enforce uniqueness on the nonnegative domain. The proof extracts the residue equality at i and applies the injectivity hypothesis directly.
Claim. Suppose $Z' : Species → ℤ$ satisfies $F_{gap}(Z'(i)) = F_{gap}(Z(i))$ for all species $i$. Assume $F_{gap}$ is injective on nonnegative integers. Then for any species $i$ with $Z(i) ≥ 0$ and $Z'(i) ≥ 0$, one has $Z'(i) = Z(i)$.
background
The Ablation module examines candidate maps Z' that preserve gap residues of the original anchor. AnchorEq is the predicate ∀ i, Fgap(Z' i) = Fgap(Z i). Fgap is the gap function abbrev from AnchorPolicyCertified. Z is the integer map from Masses.Anchor that assigns values via quadratic terms in Q6 for each sector (lepton, up-quark, down-quark). Species is the inductive type enumerating fermions plus W, Z, H bosons. The lemma operates under the nonnegativity assumptions supplied in its hypotheses.
proof idea
The proof is a one-line wrapper. It obtains the equality Fgap(Z' i) = Fgap(Z i) by specializing the AnchorEq hypothesis at i. It then feeds this equality together with the two nonnegativity hypotheses into the supplied injectivity statement for Fgap to conclude Z' i = Z i.
why it matters
This lemma closes a potential loophole in anchor certification by showing that residue-preserving maps cannot differ on nonnegative values. It supports the module's broader ablation contradictions by enforcing uniqueness under the certified anchor policy. The result aligns with the Recognition framework's emphasis on the Z-map and nonnegative residues in the mass ladder construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.