AnchorEq
AnchorEq defines the predicate that a candidate map Z' from species to integers preserves the gap residues of the standard anchor map Z. Researchers checking mass-ladder consistency or running ablation tests on the phi-ladder would cite this predicate to test whether a modified Z map keeps Fgap values unchanged. The declaration is a direct equational definition with no proof steps or lemmas.
claimLet $Z' : Species → ℤ$ be any candidate map. Then AnchorEq$(Z')$ holds if and only if Fgap$(Z'(i)) = $ Fgap$(Z(i))$ for every species $i$, where Fgap is the gap function and $Z$ is the standard anchor integer assignment.
background
Species is the inductive type that classifies the canonical particles (fermions together with W, Z, H) used throughout the mass framework. The standard map Z assigns an integer to each species via the anchor relation, depending on charge sector and the six-fold quantization of Q. Fgap is the abbreviation for the gap function applied to these integers; it supplies the residue that enters the mass formula on the phi-ladder.
proof idea
The declaration is a direct definition: it simply writes the universal quantification ∀ i, Fgap (Z' i) = Fgap (Z i). No lemmas or tactics are invoked; the body is the predicate itself.
why it matters in Recognition Science
AnchorEq supplies the interface used by ablation_contradictions to assert that the three transformations Z_dropPlus4, Z_dropQ4 and Z_break6Q all violate residue equality. It also supports the lemma anchorEq_implies_Zeq_nonneg, which recovers pointwise agreement on nonnegative values once an injectivity hypothesis on Fgap is added. In the Recognition Science setting the predicate therefore tests whether any candidate Z map can still satisfy the certified anchor that underlies the mass formula and the eight-tick octave.
scope and limits
- Does not assert that any concrete transformed map satisfies the equality.
- Does not compute explicit numerical values of Fgap or Z.
- Does not invoke the J-function or the forcing chain T0–T8.
- Does not prove uniqueness of the standard Z map.
formal statement (Lean)
34def AnchorEq (Z' : Species → Int) : Prop := ∀ i, Fgap (Z' i) = Fgap (Z i)
proof body
Definition body.
35
36/-- If anchor-equality holds for a transformed Z, then Z' must agree with Z on nonnegative values. -/