Commit History
5 days ago
-
Sync from GitHub AHMADALIPARR/cpsc-qft@2603e23: axiom-free Operator.lean, axiom audit
Verified signatureAdds lean/CPSC/Operator.lean and lean/Audit.lean, switches CPSC.lean imports from Axioms to Operator, rewrites Lemmas.lean as the Boolean-to-operator bridge, and adds paper/OPERATOR_PROOFS.md. Verified before sync: lake build succeeds on Lean 4.22.0; Audit.lean lists only propext, Classical.choice, Quot.sound; pytest 14 passed.5736180
