equalZ_residue_of_cert
If two species share the same integer charge Z, their residue values differ by at most twice the certified epsilon width of the common gap interval. Researchers certifying mass anchors or residue bounds in the Recognition framework cite this to control degeneracy within equal-Z sectors. The proof transfers per-species Ires intervals into the shared Igap interval via validity and applies the absolute-difference width bound.
claimLet $C$ be an anchor certificate. Suppose $Valid(Z, F_{gap}, C)$ holds and $res(i) ∈ C.Ires(i)$ for each species $i$. Then for any species $i,j$ with $Z(i)=Z(j)$, $|res(i)-res(j)| ≤ 2·C.eps(Z(i))$.
background
AnchorCert packages per-species residue intervals Ires together with charge-wise eps widths and centers; Valid requires that each Igap interval contains both the display value Fgap(Z i) and the corresponding Ires interval. The lemma lives in Recognition.Certification and relies on interval membership and width operations to certify anchor policies for the mass ladder. Upstream, le_trans from ArithmeticFromLogic chains the interval bounds, while Z and Species from the Masses and Physics modules supply the charge map used in the hypothesis.
proof idea
Extract Ires-in-Igap containments from the Valid hypothesis. Use Z-equality to equate the two Igap intervals and apply le_trans to place both res i and res j inside the single interval Igap C (Z i). Invoke abs_sub_le_width_of_memI on that common interval to obtain the difference bound. Simplify the width of Igap to 2·eps(Z i) and finish by simpa.
why it matters in Recognition Science
The lemma supplies the equal-Z degeneracy bound invoked by equalZ_residue_from_cert in AnchorPolicyCertified, thereby completing the certified consequences of anchor certificates. It supports residue control on the phi-ladder by limiting variation inside each charge sector and closes one step in the chain from certificate validity to mass-anchor bounds.
scope and limits
- Does not prove exact equality of residues, only an upper bound.
- Does not apply when Z(i) ≠ Z(j).
- Does not constrain the M0 or center fields of the certificate.
- Does not depend on the concrete definition of Fgap beyond the Valid assumption.
Lean usage
theorem use_site (C : AnchorCert Species) (hC : Valid Z Fgap C) (res : Species → ℝ) (hres : ∀ i, memI (C.Ires i) (res i)) {i j : Species} (hZ : Z i = Z j) : |res i - res j| ≤ 2 * C.eps (Z i) := equalZ_residue_of_cert hC res hres hZformal statement (Lean)
81lemma equalZ_residue_of_cert {Species : Type} {Z : Species → Int} {Fgap : Int → ℝ}
82 {C : AnchorCert Species} (hC : Valid Z Fgap C)
83 (res : Species → ℝ) (hres : ∀ i, memI (C.Ires i) (res i))
84 {i j : Species} (hZ : Z i = Z j) :
85 |res i - res j| ≤ 2 * C.eps (Z i) := by
proof body
Tactic-mode proof.
86 have hI_i : (Igap C (Z i)).lo ≤ (C.Ires i).lo ∧ (C.Ires i).hi ≤ (Igap C (Z i)).hi :=
87 hC.Ires_in_Igap i
88 have hI_j : (Igap C (Z j)).lo ≤ (C.Ires j).lo ∧ (C.Ires j).hi ≤ (Igap C (Z j)).hi :=
89 hC.Ires_in_Igap j
90 have hres_i : memI (Igap C (Z i)) (res i) := by
91 have hr0 := hres i
92 exact ⟨le_trans hI_i.1 hr0.1, le_trans hr0.2 hI_i.2⟩
93 have hres_j : memI (Igap C (Z i)) (res j) := by
94 have hr0 := hres j
95 have hlo_j : (Igap C (Z i)).lo ≤ (C.Ires j).lo := by simpa [hZ] using hI_j.1
96 have hhi_j : (C.Ires j).hi ≤ (Igap C (Z i)).hi := by simpa [hZ] using hI_j.2
97 exact ⟨le_trans hlo_j hr0.1, le_trans hr0.2 hhi_j⟩
98 have hbound :=
99 abs_sub_le_width_of_memI (I := Igap C (Z i)) (x := res i) (y := res j) hres_i hres_j
100 have hw :
101 width (Igap C (Z i)) = 2 * C.eps (Z i) := by
102 simp [Igap, width]
103 ring
104 simpa [hw, two_mul] using hbound
105
106/-! ### Zero-width anchor certificate (exact equality) -/
107
108/-- Zero-width certificate: each interval collapses to the center value `Fgap(Z i)`. -/