pith. machine review for the scientific record. sign in
def definition def or abbrev high

Z_dropQ4

show as:
view Lean formalization →

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.

claimFor 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  23noncomputable def Z_dropQ4 (i : Species) : Int :=

proof body

Definition body.

  24  if tildeQ i > 0 then 4 + (tildeQ i)^2 else 0
  25
  26/-- Break the integerization ˜Q = 6Q by using ˜Q' = 3Q (integerized) instead. -/
  27-- Provided above as a parameter `tildeQ_broken3`.
  28
  29/-- Recompute Z with the broken integerization. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (8)

Lean names referenced from this declaration's body.