def definition def or abbrev

`negCharge`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 217def negCharge {N : ℕ} (Q : TopologicalCharge N) : TopologicalCharge N where
 218  value := fun c => -Q.value c

proof body

Definition body.

 219  conserved := fun c next h => by rw [Q.conserved c next h]
 220
 221/-- **THEOREM (Universe Starts Neutral)**:
 222    If a trajectory starts at zero charge, total charge remains zero forever. -/

depends on (7)

Lean names referenced from this declaration's body.

TopologicalCharge in IndisputableMonolith.Foundation.TopologicalConservation decl_use
total in IndisputableMonolith.NavierStokes.DiscreteVorticity decl_use
total in IndisputableMonolith.NumberTheory.RiemannHypothesis.ErrorBudget decl_use
TopologicalCharge in IndisputableMonolith.Physics.TopologicalChargesFromConfigDim decl_use
value in IndisputableMonolith.QFT.SpinStatistics decl_use
trajectory in IndisputableMonolith.Robotics.PIDStabilityFromJCost decl_use
next in IndisputableMonolith.RRF.Hypotheses.EightTick decl_use