pith. machine review for the scientific record. sign in
def definition def or abbrev

topological_to_noether

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)

 177def topological_to_noether {N : ℕ} (Q : TopologicalCharge N) : NoetherCharge N where
 178  value := fun c => (Q.value c : ℝ)

proof body

Definition body.

 179  conserved := fun c next h => by simp [Q.conserved c next h]
 180
 181/-- **THEOREM (Noether Charges Need Not Be Quantized)**:
 182    There exist Noether charges that take non-integer values.
 183
 184    Proof: log(2) satisfies 0 < log(2) < 1, so it is not an integer. -/

depends on (11)

Lean names referenced from this declaration's body.