`topological_conservation_certificate`

proved

show as: view math explainer →

module: IndisputableMonolith.Foundation.TopologicalConservation
domain: Foundation
line: 249 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Foundation.TopologicalConservation on GitHub at line 249.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 246    5. **BIJECTION**: 3 charges ↔ 3 face-pairs ↔ 3 axes of Q₃
 247    6. **STRONGER THAN NOETHER**: Integer-valued + unconditional
 248    7. **CHARGE ALGEBRA**: Charges closed under + and − -/
 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 : ℝ)) :=
 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.