Z_dropQ4
plain-language theorem explainer
Z_dropQ4 supplies a modified integer mass map that omits the quartic charge term from the standard anchor Z. Researchers testing term necessity in the Recognition Science mass formula would cite this definition during ablation checks on anchor equality. The definition is realized directly by a conditional expression on the sign of the charge index.
Claim. For species $i$, let $q̃(i)$ be its charge index. Define $Z_{dropQ4}(i) := 4 + q̃(i)^2$ if $q̃(i) > 0$ and $0$ otherwise. This removes the $q̃^4$ contribution present in the full anchor map $Z$.
background
The anchor map $Z$ assigns integers to species via their charge index $q̃$, where $q̃$ maps up-type quarks to 4, down-type to -2, charged leptons to -6, and neutrinos to 0. The standard form is $Z = q̃^2 + q̃^4$ for leptons and $4 + q̃^2 + q̃^4$ for quarks after integerization $q̃ = 6Q$. Species is the inductive type covering fermions and the bosons W, Z, H. The ablation module introduces term-dropping variants of $Z$ to probe which contributions are required for the anchor relation to hold.
proof idea
The definition is a direct conditional on the sign of $q̃(i)$ drawn from the upstream tildeQ map for Species. It applies the expression 4 + $q̃^2$ only when positive and defaults to zero, serving as a one-line wrapper for the dropped-quartics case.
why it matters
Z_dropQ4 feeds the ablation_contradictions result, which shows that anchor equality fails under this modification and thereby supports the necessity of the full quartic term in the certified anchor. It connects to the mass formula on the phi-ladder and the integerization step that precedes rung assignment. The definition helps close the case that no reduced Z satisfies the anchor policy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.