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

ZOf

show as:
view Lean formalization →

ZOf maps each of the twelve Standard Model fermions to an integer Z built from its reduced charge index q̃. Mass-ratio derivations in the Recognition framework cite this map when placing a species on the phi-ladder at the anchor scale. The definition is a direct case split on sectorOf f that adds the constant 4 only for quarks and returns zero for neutrinos.

claimFor a fermion $f$ with reduced charge index $q̃$, define $Z(f) = 4 + q̃^2 + q̃^4$ when $f$ is a quark, $Z(f) = q̃^2 + q̃^4$ when $f$ is a charged lepton, and $Z(f) = 0$ when $f$ is a neutrino.

background

The RSBridge.Anchor module supplies the interface between the recognition framework and the Standard Model fermion spectrum. Fermion is the inductive type that enumerates the six quarks, three charged leptons and three neutrinos. ZOf computes the integer label Z_i that enters the gap function F(Z) = ln(1 + Z/φ)/ln(φ) at the anchor scale μ⋆, where this F is the closed form claimed to equal the integrated RG residue f_i(μ⋆).

proof idea

The definition performs a direct case split on the sector returned by sectorOf f. For up and down sectors it adds the constant 4 to the quadratic and quartic terms in tildeQ f; for leptons it omits the constant; for neutrinos it returns zero. No lemmas are invoked; the expression is the explicit closed form.

why it matters in Recognition Science

ZOf supplies the discrete index that appears in every anchor mass ratio and in the mass formula yardstick * φ^(rung - 8 + gap(Z)). It is invoked by the anchor_ratio theorem and by the Z_eq equalities in QuarkAnchorDerivation, thereby linking the eight-tick octave (T7) and the phi-ladder to the observed quark and lepton spectrum. The definition closes the structural step that converts equal-Z species into pure φ-powers.

scope and limits

Lean usage

theorem bottom_Z_eq : ZOf Fermion.b = 24 := rfl

formal statement (Lean)

  50def ZOf (f : Fermion) : ℤ :=

proof body

Definition body.

  51  let q := tildeQ f
  52  match sectorOf f with
  53  | .up | .down => 4 + q*q + q*q*q*q
  54  | .lepton     =>     q*q + q*q*q*q
  55  | .neutrino   => 0
  56
  57/-- The display function F(Z) = ln(1 + Z/φ) / ln(φ).
  58
  59    This is the **closed form** that the integrated RG residue is claimed to equal
  60    at the anchor scale μ⋆. The claim is:
  61      `f_i(μ⋆) = gap(ZOf i)`
  62    where `f_i(μ⋆)` is the integral of the mass anomalous dimension.
  63
  64    **Properties**:
  65    - F(0) = 0
  66    - F is monotonically increasing for Z > -φ
  67    - For large Z: F(Z) ≈ log_φ(Z)
  68
  69    **Canonical values** (charged fermions):
  70    - F(24)   ≈ 5.74   (down quarks, q̃ = -2)
  71    - F(276)  ≈ 10.69  (up quarks, q̃ = +4)
  72    - F(1332) ≈ 13.95  (leptons, q̃ = -6) -/

used by (40)

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

… and 10 more

depends on (31)

Lean names referenced from this declaration's body.

… and 1 more