def
definition
standardModelConservation
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.QFT.NoetherTheorem on GitHub at line 250.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
247/-! ## Standard Model Conservation Laws -/
248
249/-- Standard Model conservation laws and their symmetries. -/
250def standardModelConservation : List (String × String) := [
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. -/
271structure NoetherFalsifier where
272 /-- Type of apparent violation. -/
273 violation : String
274 /-- Resolution (if any). -/
275 resolution : String
276
277/-- Known apparent violations and their resolutions. -/
278def apparentViolations : List NoetherFalsifier := [
279 ⟨"Energy non-conservation in expanding universe",
280 "Time translation symmetry is broken by cosmological expansion"⟩,