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

Z

show as:
view Lean formalization →

This abbrev supplies the canonical integer Z map for each fermion species by forwarding directly to the upstream ZOf computation. Mass-ladder and ablation researchers cite it when they require the anchor Z values without duplicating sector logic. The definition is a one-line alias that forwards to the RSBridge ZOf.

claimFor a fermion species $f$, define $Z(f) := Z_{Of}(f)$, where $Z_{Of}$ returns the integer $q^2 + q^4$ (plus 4 for up or down quarks) from the rescaled charge $q = 6Q$ of $f$.

background

The AnchorPolicyCertified module supplies a certificate-based interface that replaces an earlier axiom for Standard-Model RG residues. It lets Lean derive per-species closeness to gap(Z) and equal-Z degeneracy bounds once external residue intervals are supplied. Species is the alias for Fermion. The integer map Z is the one used by the anchor relation (Paper 1). Upstream ZOf implements the explicit formula: for leptons it is $q^2 + q^4$, for quarks it adds the offset 4, and for neutrinos it is zero.

proof idea

One-line wrapper that applies the ZOf definition from RSBridge.Anchor.

why it matters in Recognition Science

Z supplies the reference map for the AnchorEq predicate and the ablation_contradictions check in the Ablation module. Those results verify that alternative integerizations (drop-plus-4, drop-Q4, break-6Q) fail to preserve the certified residues. The declaration therefore closes the dependency on the mass-framework Z computation for downstream physics statements such as atomic-radii inequalities.

scope and limits

formal statement (Lean)

  41abbrev Z (f : Species) : Int := ZOf f

proof body

Definition body.

  42

used by (40)

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

… and 10 more

depends on (5)

Lean names referenced from this declaration's body.