ablation_contradictions
plain-language theorem explainer
ablation_contradictions defines the proposition that anchor equality fails for three ablations of the Z map: omitting the plus-four offset on positive tildeQ, omitting the fourth-power term, and replacing the six-Q integerization with a broken three-Q version. A physicist examining stability of the certified anchor in the Recognition Science mass ladder would cite this to show that the original residues cannot be recovered after these changes. The definition is assembled as a direct conjunction of three negated AnchorEq predicates.
Claim. Let $Z$ be the integer map on fermion species from the anchor relation and let $Fgap$ be the gap function. The proposition asserts that the map $Z'$ obtained by setting the additive offset to zero for positive $tildeQ$ satisfies $¬∀i. Fgap(Z'(i))=Fgap(Z(i))$, and likewise for the map omitting the fourth-power term and for the map recomputed with broken integerization $tildeQ'=3Q$.
background
AnchorEq requires that for every species the gap function on the candidate map agrees exactly with the gap on the original Z. Z_dropPlus4 drops the additive four for positive tildeQ while retaining the quadratic and quartic terms; Z_dropQ4 drops the quartic term everywhere; Z_break6Q recomputes using the broken tildeQ_broken3. These definitions sit in the Ablation module and import the base Z map from Masses.Anchor together with the tildeQ assignment from RSBridge.Anchor.
proof idea
The definition is a direct conjunction of the three negated AnchorEq statements applied to Z_dropPlus4, Z_dropQ4, and Z_break6Q respectively. No lemmas or tactics are used beyond the already-defined ablation maps and the AnchorEq predicate.
why it matters
The definition encodes the claim that anchor equality cannot survive these modifications, thereby reinforcing uniqueness of the certified Z map inside the Recognition Science mass formula. It supports the integerization step that feeds the phi-ladder construction of particle masses and the overall forcing chain from T0 to T8. No downstream uses are recorded, so the declaration functions as a standalone incompatibility statement for ablation analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.