Documentation

MIPRE.Background.LIDT.Co.Tactic.QuantumNonneg

Conservative nonnegativity tactic for the symmetric model #

This file provides the opt-in tactic sym_nonneg for recurring LDT goals of shape 0 ≤ ... involving positive effects, tensor placements, and expectation values in a symmetric model S : SymModel 𝔓 K: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Tactic/QuantumNonneg.lean in the port of planning/c6b-plan.md (milestone M0, section "Port conventions"). The tactic intentionally does not register any global @[positivity] extensions: callers must import this module and invoke the tactic at the proof sites where they want the controlled automation.

The vendored tactic is called quantum_nonneg, and the port's macro has a name of its own as a precaution. No file of M0 imports the vendored syntax (only the vendored LDT/Preliminaries/Defs.lean imports it), but 228 of the 312 vendored LDT modules have it in their import closure (every vendored module from Preliminaries/Defs.lean on); a later stage that imports one of them for its classical content would see two quantum_nonneg syntaxes, the vendored one calling the matrix lemmas, and every call would be an ambiguous parse. The macro is the vendored one with each lemma replaced by its fully qualified MIPRE.LIDT.Co counterpart (the placement lemmas of Co/Basic/QuantumState.lean, the submeasurement lemmas of Co/Basic/SubMeasurementCore.lean), plus one fallback, map_nonneg, for a positive operator pushed along an order-preserving map other than the two placements (a SubMeas.map along any ⋆-homomorphism, for instance).

The search is deliberately shallow. It tries the local wrappers used throughout the LDT quantum layer, decomposes finite sums and nonnegative scalar multiples, and leaves scalar side goals to positivity/nlinarith. Since S.opTensor A B is the abbreviation S.L A * S.R B, a product S.L A * S.R B needs no rewrite before the tactic (the vendored callers rewrite with leftTensor_mul_rightTensor_eq_opTensor first; doing so here is harmless).

Not ported #

The vendored file declares no theorem or definition, only the syntax node quantumNonneg of quantum_nonneg; its counterpart is the syntax node symNonneg of sym_nonneg, renamed so that a port file may import vendored modules that have the vendored syntax in their closure (above). The vendored example is translated below, with the call sites listed there.

source
def symNonneg :
Lean.ParserDescr

sym_nonneg proves small, canonical nonnegativity goals in the LDT quantum layer of the symmetric model.

It is meant for goals built from:

  • positive expectation lemmas (VecState.ev_adjoint_self_nonneg, VecState.ev_nonneg_of_psd),
  • tensor positivity (SymModel.opTensor_nonneg, SymModel.leftTensor_nonneg, SymModel.rightTensor_nonneg, and map_nonneg for any other order-preserving map),
  • Hermitian sandwich positivity (IsSelfAdjoint.conjugate_nonneg),
  • finite sums and nonnegative scalar multiples, and
  • scalar leaves discharged by positivity/nlinarith.

This is a conservative tactic macro rather than global automation; it should be used explicitly at representative proof sites and extended only after measuring performance on the affected files.

Equations
Instances For