def
definition
def or abbrev
standardModelConservation
show as:
view Lean formalization →
formal statement (Lean)
250def standardModelConservation : List (String × String) := [
proof body
Definition body.
251 ("Energy", "Time translation"),
252 ("Momentum", "Space translation"),
253 ("Angular momentum", "Rotation"),
254 ("Electric charge", "U(1)_em"),
255 ("Color charge", "SU(3)_c"),
256 ("Weak isospin", "SU(2)_L (broken)"),
257 ("Baryon number", "U(1)_B (approximate)"),
258 ("Lepton number", "U(1)_L (approximate)")
259]
260
261/-! ## Falsification Criteria -/
262
263/-- Noether's theorem would be falsified by:
264 1. Conserved quantity without corresponding symmetry
265 2. Symmetry without conservation (in isolated system)
266 3. Energy/momentum violation in isolated systems
267
268 But this is mathematically proven above - it CANNOT be falsified
269 as a mathematical theorem. Physical applications could fail if
270 the symmetry assumptions don't hold. -/