def
definition
negCharge
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 217.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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
243 2. **EXACTLY CONSERVED**: Invariant at every tick of every trajectory
244 3. **D = 3 REQUIRED**: 3 independent charges only in D = 3
245 4. **THREE CHARGES**: Electric charge, baryon number, lepton number
246 5. **BIJECTION**: 3 charges ↔ 3 face-pairs ↔ 3 axes of Q₃
247 6. **STRONGER THAN NOETHER**: Integer-valued + unconditional