module module

`IndisputableMonolith.Foundation.TopologicalConservation`

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

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Foundation.WindingCharges module_import

depends on (4)

Lean names referenced from this declaration's body.

IndisputableMonolith.Foundation.DimensionForcing module_import
IndisputableMonolith.Foundation.InitialCondition module_import
IndisputableMonolith.Foundation.ParticleGenerations module_import
IndisputableMonolith.Foundation.VariationalDynamics module_import

declarations in this module (27)

structure TopologicalCharge L64
theorem topological_charge_quantized L71
theorem topological_charge_trajectory_conserved L76
theorem charge_at_any_tick L85
def zeroCharge L94
def constCharge L99
def independent_charge_count L111
theorem three_charges_at_D3 L114
theorem no_charges_at_other_D L117
theorem linking_iff_D3 L122
theorem charge_count_equals_face_pairs L127
inductive SMCharge L133
theorem sm_charge_count L139
theorem sm_charges_match_D3 L141
def charge_to_axis L146
theorem charge_to_axis_injective L151
theorem charge_to_axis_surjective L154
theorem charge_to_axis_bijective L160
structure NoetherCharge L166
def logChargeAsNoether L172
def topological_to_noether L177
theorem noether_not_necessarily_quantized L185
def addCharges L212
def negCharge L217
theorem total_charge_always_zero L223
theorem conservation_is_unconditional L231
theorem topological_conservation_certificate L249