pith. machine review for the scientific record. sign in
theorem proved term proof

Z_lepton_decomposition

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)

  84theorem Z_lepton_decomposition :
  85    (1 : ℤ) * (-6) ^ 2 = 36 ∧
  86    (1 : ℤ) * (-6) ^ 4 = 1296 ∧
  87    (36 : ℤ) + 1296 = 1332 := by

proof body

Term-mode proof.

  88  refine ⟨by norm_num, by norm_num, by norm_num⟩
  89
  90/-- Consistency: the derived Z equals 1332, matching Anchor.lean's hardcoded value. -/

depends on (3)

Lean names referenced from this declaration's body.