conservation_is_unconditional

formal source

 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
 248    7. **CHARGE ALGEBRA**: Charges closed under + and − -/
 249theorem topological_conservation_certificate :
 250    independent_charge_count 3 = 3 ∧
 251    (∀ D, D ≠ 3 → independent_charge_count D = 0) ∧
 252    independent_charge_count 3 = face_pairs 3 ∧
 253    Fintype.card SMCharge = 3 ∧
 254    Function.Bijective charge_to_axis ∧
 255    (∀ (N : ℕ) (Q : TopologicalCharge N) (traj : Trajectory N),
 256      IsVariationalTrajectory traj →
 257      ∀ t, Q.value (traj t) = Q.value (traj 0)) ∧
 258    (∃ (N : ℕ) (Q : NoetherCharge N) (c : Configuration N),
 259      ¬∃ n : ℤ, Q.value c = (n : ℝ)) :=
 260  ⟨three_charges_at_D3,
 261   no_charges_at_other_D,