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

tildeQ

show as:
view Lean formalization →

tildeQ supplies the integer charge index q̃ for each of the twelve Standard Model fermions, with values 4 for up-type quarks, -2 for down-type quarks, -6 for charged leptons, and 0 for neutrinos. Mass and ablation calculations in the Recognition framework cite this map when building ZOf and the gap function at the anchor scale. The definition is a direct exhaustive case split on the Fermion inductive type.

claimThe map $q̃ : Fermion → ℤ$ sends the up-type quarks $u,c,t$ to 4, the down-type quarks $d,s,b$ to -2, the charged leptons $e,μ,τ$ to -6, and the neutrinos $ν_1,ν_2,ν_3$ to 0.

background

The RSBridge.Anchor module supplies the bridge from the recognition framework to particle physics by enumerating the twelve Standard Model fermions in the inductive type Fermion and defining the integer charge index q̃ that enters ZOf. ZOf(f) is then 4 + q² + q⁴ for quarks and q² + q⁴ for leptons, which in turn feeds the gap function F(Z) = ln(1 + Z/φ)/ln(φ) used at the anchor scale μ⋆. The module also records the relation to RG transport: the integrated residue ∫γ_i is claimed to equal gap(ZOf i) with tolerance ~1e-6.

proof idea

The definition is a direct pattern match on the Fermion constructors, returning the constant integer for each of the four groups of species.

why it matters in Recognition Science

tildeQ provides the q̃ input required by ZOf, which is used in ablation_contradictions, Z_dropPlus4, Z_dropQ4, electron_Z_value, and the mass ladder constructions. It implements the charge-index step that connects the Recognition framework's phi-ladder and anchor phenomenology to the Standard Model fermion spectrum. Downstream results such as anchorEquality and residueAtAnchor depend on the values fixed here.

scope and limits

formal statement (Lean)

  44def tildeQ : Fermion → ℤ
  45| .u | .c | .t => 4
  46| .d | .s | .b => -2
  47| .e | .mu | .tau => -6
  48| .nu1 | .nu2 | .nu3 => 0
  49

used by (8)

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

depends on (7)

Lean names referenced from this declaration's body.