Adds 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.
Model card: restore full README from GitHub, add commercial license option
