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

topological_conservation_certificate

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)

 249theorem topological_conservation_certificate :
 250    independent_charge_count 3 = 3 ∧
 251    (∀ D, D ≠ 3 → independent_charge_count D = 0) ∧
 252    independent_charge_count 3 = face_pairs 3 ∧
 253    Fintype.card SMCharge = 3 ∧
 254    Function.Bijective charge_to_axis ∧
 255    (∀ (N : ℕ) (Q : TopologicalCharge N) (traj : Trajectory N),
 256      IsVariationalTrajectory traj →
 257      ∀ t, Q.value (traj t) = Q.value (traj 0)) ∧
 258    (∃ (N : ℕ) (Q : NoetherCharge N) (c : Configuration N),
 259      ¬∃ n : ℤ, Q.value c = (n : ℝ)) :=

proof body

Term-mode proof.

 260  ⟨three_charges_at_D3,
 261   no_charges_at_other_D,
 262   rfl,
 263   sm_charge_count,
 264   charge_to_axis_bijective,
 265   fun N Q traj h => topological_charge_trajectory_conserved Q traj h,
 266   noether_not_necessarily_quantized⟩
 267
 268end TopologicalConservation
 269end Foundation
 270end IndisputableMonolith

depends on (20)

Lean names referenced from this declaration's body.