Sync from GitHub AHMADALIPARR/cpsc-qft@9b102cf: remove Axioms.lean

README.md

@@ -15,7 +15,7 @@ tags:
 - quantum-computing
 ---
 
-> Mirrored from [https://github.com/AHMADALIPARR/cpsc-qft](https://github.com/AHMADALIPARR/cpsc-qft) at commit `eacf0fa`. Part of the **SnapKitty October 2026 main drop**. Paper: [Snapkitty/cpsc-qft-paper](https://huggingface.co/datasets/Snapkitty/cpsc-qft-paper).
+> Mirrored from [https://github.com/AHMADALIPARR/cpsc-qft](https://github.com/AHMADALIPARR/cpsc-qft) at commit `9b102cf`. Part of the **SnapKitty October 2026 main drop**. Paper: [Snapkitty/cpsc-qft-paper](https://huggingface.co/datasets/Snapkitty/cpsc-qft-paper).
 
 <!--
 Copyright (c) 2026 Ahmad Ali Parr and others.

lean/CPSC/Axioms.lean

@@ -1,89 +0,0 @@
-import CPSC.Certificate
-
-/-
-Copyright (c) 2026 Ahmad Ali Parr and others.
-
-SPDX-License-Identifier: LicenseRef-CPSC-ESCL-1.0 OR AGPL-3.0-only
--/
-
-/-!
-Operator axioms.
-
-These are not proved. They are the commutation facts the compiler is allowed
-to use. A later matrix development has to discharge them; until then every
-lemma in `CPSC.Lemmas` is conditional on this file.
--/
-
-
-namespace CPSC
-
-axiom Unitary : Type
-
-axiom idU : Unitary
-
-axiom mul : Unitary → Unitary → Unitary
-
-axiom gateOp : GateKind → Unitary
-
-/-- Commutation with magnetization, the λ = 0 invariant. -/
-axiom commMag : Unitary → Prop
-
-/-- Commutation with ∏ X, the λ ≠ 0 invariant. -/
-axiom commSpin : Unitary → Prop
-
-axiom id_comm_mag : commMag idU
-
-axiom id_comm_spin : commSpin idU
-
-axiom mul_comm_mag (U V : Unitary) :
-    commMag U → commMag V → commMag (mul U V)
-
-axiom mul_comm_spin (U V : Unitary) :
-    commSpin U → commSpin V → commSpin (mul U V)
-
-axiom mul_assoc (U V W : Unitary) :
-    mul (mul U V) W = mul U (mul V W)
-
-axiom mul_id_left (U : Unitary) : mul idU U = U
-
-axiom mul_id_right (U : Unitary) : mul U idU = U
-
-axiom zz_mag (i j : Nat) : commMag (gateOp (.zz i j))
-
-axiom zz_spin (i j : Nat) : commSpin (gateOp (.zz i j))
-
-axiom z_mag (i : Nat) : commMag (gateOp (.loneZ i))
-
-axiom pair_spin (i j : Nat) : commSpin (gateOp (.parityEvenPair i j))
-
-axiom flip_spin (i : Nat) : commSpin (gateOp (.transverseFlip i))
-
-axiom flip_not_mag (i : Nat) : ¬ commMag (gateOp (.transverseFlip i))
-
-axiom pair_not_mag (i j : Nat) : ¬ commMag (gateOp (.parityEvenPair i j))
-
-axiom z_not_spin (i : Nat) : ¬ commSpin (gateOp (.loneZ i))
-
-/-- Bridge: the Boolean analyzer is sound for magnetization. -/
-axiom mag_of_bool (g : GateKind) :
-    preservesMagnetization g = true → commMag (gateOp g)
-
-/-- Bridge: the Boolean analyzer is sound for the spin flip. -/
-axiom spin_of_bool (g : GateKind) :
-    preservesSpinFlip g = true → commSpin (gateOp g)
-
-/-- Completeness: exact evolution generated by a commuting Hamiltonian stays in the sector. -/
-axiom exact_evolution_in_manifold
-    (mode : Mode) (H : Unitary) :
-    (mode = .ising → commMag H) →
-    (mode = .spinFlip → commSpin H) →
-    (mode = .ising → commMag H) ∧ (mode = .spinFlip → commSpin H)
-
-/-- A rejected generator is not repaired by right-multiplication. -/
-axiom reject_not_absorbed_mag (g : GateKind) (V : Unitary) :
-    ¬ commMag (gateOp g) → ¬ commMag (mul (gateOp g) V)
-
-axiom reject_not_absorbed_spin (g : GateKind) (V : Unitary) :
-    ¬ commSpin (gateOp g) → ¬ commSpin (mul (gateOp g) V)
-
-end CPSC