Z_dropPlus4
plain-language theorem explainer
The drop-plus-four map supplies an ablated integer assignment for species that omits the additive four offset applied to up-type quarks in the standard anchor map Z. Ablation studies testing the uniqueness of the certified anchor relation would invoke this variant. It is realized by a direct conditional on the sign of the charge index.
Claim. Let $q̃(i)$ be the charge index of species $i$. Define the ablated map by $Z_{drop+4}(i) = q̃(i)^2 + q̃(i)^4$ if $q̃(i) > 0$, and $0$ otherwise.
background
The anchor integer map Z assigns to leptons the sum of squares and fourth powers of the scaled charge Q6 = 6Q, while quarks receive an extra additive four. The charge index q̃ takes value four for up quarks, negative two for down quarks, negative six for charged leptons, and zero for neutrinos and gauge bosons. Species is the inductive type that enumerates the standard model fermions together with the W, Z, and Higgs bosons. This construction lives in the Ablation module whose purpose is to generate variants that lead to contradictions with the certified anchor equality.
proof idea
The definition expands directly to a piecewise expression: when the charge index is positive it returns the sum of its square and fourth power; otherwise it returns zero. It imports the q̃ map from the RSBridge and RungConstructor modules to evaluate the condition and the value.
why it matters
The map enters the definition of ablation_contradictions, which asserts that none of the three ablations (drop plus four, drop Q to the four, break six Q) can satisfy the anchor equality AnchorEq. This supports the claim that the full structure of Z, including the quark offset, is required for consistency with the certified anchor policy in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.