def
definition
addCharges
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Foundation.TopologicalConservation on GitHub at line 212.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
209/-! ## Part 6: Charge Algebra -/
210
211/-- Sum of two topological charges. -/
212def addCharges {N : ℕ} (Q₁ Q₂ : TopologicalCharge N) : TopologicalCharge N where
213 value := fun c => Q₁.value c + Q₂.value c
214 conserved := fun c next h => by rw [Q₁.conserved c next h, Q₂.conserved c next h]
215
216/-- Negation of a topological charge. -/
217def negCharge {N : ℕ} (Q : TopologicalCharge N) : TopologicalCharge N where
218 value := fun c => -Q.value c
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. -/
223theorem total_charge_always_zero {N : ℕ}
224 (Q : TopologicalCharge N)
225 (traj : Trajectory N) (h : IsVariationalTrajectory traj)
226 (h_init : Q.value (traj 0) = 0) :
227 ∀ t, Q.value (traj t) = 0 := by
228 intro t; rw [topological_charge_trajectory_conserved Q traj h t, h_init]
229
230/-- Conservation is unconditional — no symmetry assumption needed. -/
231theorem conservation_is_unconditional {N : ℕ} (Q : TopologicalCharge N)
232 (c next : Configuration N) (h : IsVariationalSuccessor c next) :
233 Q.value next = Q.value c :=
234 Q.conserved c next h
235
236/-! ## Part 7: Summary Certificate -/
237
238/-- **F-012 CERTIFICATE: Topological Conservation**
239
240 Conservation laws in Recognition Science are TOPOLOGICAL, not Noetherian:
241
242 1. **INTEGER-VALUED**: ℤ-valued → automatic quantization