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

Z

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 186@[simp] def Z (sector : Anchor.Sector) (Q : ℚ) : ℤ :=

proof body

Definition body.

 187  let Q6 : ℤ := (6 : ℤ) * Q.num / Q.den
 188  match sector with
 189  | .Lepton      => (Q6 ^ (2 : ℕ)) + (Q6 ^ (4 : ℕ))
 190  | .UpQuark     => 4 + (Q6 ^ (2 : ℕ)) + (Q6 ^ (4 : ℕ))
 191  | .DownQuark   => 4 + (Q6 ^ (2 : ℕ)) + (Q6 ^ (4 : ℕ))
 192  | .Electroweak => 0
 193
 194end ChargeIndex
 195
 196/-! ## Summary: Parameter-Free Derivation
 197
 198All sector constants trace back to:
 1991. D = 3 (dimension, from T9 linking)
 2002. cube_edges(D) = 12 (hypercube formula)
 2013. active_edges_per_tick = 1 (atomic tick, from T2)
 2024. passive_field_edges = 11 (12 - 1)
 2035. wallpaper_groups = 17 (crystallographic, Fedorov 1891)
 204
 205NO free parameters. NO fitting to mass data.
 206-/
 207
 208end Masses
 209end IndisputableMonolith

used by (40)

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

… and 10 more

depends on (16)

Lean names referenced from this declaration's body.