pith. machine review for the scientific record. sign in
theorem proved term proof

conservation_is_unconditional

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)

 231theorem conservation_is_unconditional {N : ℕ} (Q : TopologicalCharge N)
 232    (c next : Configuration N) (h : IsVariationalSuccessor c next) :
 233    Q.value next = Q.value c :=

proof body

Term-mode proof.

 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 − -/

depends on (22)

Lean names referenced from this declaration's body.