Documentation

MIPRE.Axioms

The blueprint's proof-level \leanok claims, guarded #

\leanok is two marks. Inside a statement environment it claims the statement is formalized; inside \begin{proof} it claims the proof is. The second is the project's central claim -- CLAUDE.md's three artifacts, and rule 3 of planning/formalization-plan.md, rest on MIPRE/ being the one thing that is true because this repository says so -- and until now it was maintained by hand. The evidence behind all 27 marks was one audit, planning/lean-coverage.md, run against 80 modules and 1502 declarations; the tree is 122 and 2467, so two thirds of the named surface postdates it, and it is already wrong in one direction, listing MIPRE.syncValue_le_quantumValue as carrying sorryAx when it is proved.

#guard_sorry_free (MIPRE/Foundations/GuardSorryFree.lean) fails the build if any name it is given depends on sorryAx, and scripts/lean-coverage.py checks that the set of names guarded here and in the vendored guard files is exactly the set the blueprint marks with a proof-level \leanok. A mark without a guard is an unchecked assertion about this project's own mathematics; a guard without a mark is a leftover that will one day be read as one. Both are now build failures.

The three vendored trees have carried such a guard from the start (MIPRE/Background/{LIDT,Repetition,Orthonormalization}/Axioms.lean), for the reason CONTRIBUTING.md gives about the sorry exception: it is what keeps the exception from being a loophole. The mathematics this project imports was machine-guarded; the mathematics it writes itself was not. Names defined in the vendored trees stay guarded there, where the imports are already paid for -- except MIPRE.gowers_hatami, whose module imports only Foundations.Distances and Mathlib and which had no guard of its own.

Adding a declaration here is not how to claim it: mark the blueprint proof, and the check will tell you the guard is missing.

lem:mipstar-poly-sub: the paper's class is contained in the computable one (MIPRE/Foundations/ClassMIPStarTab.lean).

The padded adapter and the simultaneous seeded CL theorem (answer reduction, AR-2) #

Introspection mixing, conditioning, and graph rejection sampling #

Detyped presentations, query routing, and finite-game soundness #

The finite-game result uses the same answer alphabets. It does not discharge the ambient wrapper, answer-cutoff, or runtime obligations.

The proved Shoup construction and its consumers #

#guard_sorry_free excludes sorryAx; exact guards additionally exclude any replacement unproved assumption. The former imported construction is now the proved theorem MIPRE.LowDegree.exists_shoup_irreducible, witnessed directly by the specified ambient program. The public constructor and both effective consumers below depend only on Lean's standard axioms. The companion ledger's historical admission remains unchanged; these guards describe the Lean proof.

Introspection construction, induction stages, and final extraction #

Executable introspection answer parsing and guarded source calls #

Introspection continuation: guarded normalizers and complete auxiliary game #

Canonical introspection compiler, finite kernel and QLD transport #

Blocks of an index type #

Blueprint lem:qld-sublines, the measure-preserving half of a block decomposition: an assignment to a sum index type is a pair of assignments to the summands, uniform and independent, together with the bookkeeping -- rewriting under nested sums, reordering them, and pulling a constant out -- that a block decomposition then needs.

cor:compression-from-answer-reduction: the pipeline with its supplied stages (MIPRE/Background/Pipeline.lean).

lem:correlation-sets-basic and lem:tsirelson-conditional: the correlation sets and the separation from an upper semidecider (MIPRE/Foundations/Correlations.lean, MIPRE/Foundations/Tsirelson/Conditional.lean).

The Positivstellensatz route to cor:tsirelson: lem:cone-archimedean, lem:cone-state-gns, lem:cqc-compact, thm:nc-positivstellensatz, lem:sos-certificates, lem:valco-upper-re and cor:tsirelson (MIPRE/Foundations/NCPoly/, MIPRE/Foundations/GNS.lean, MIPRE/Foundations/Tsirelson/, MIPRE/Tsirelson.lean).

thm:separation: the explicit separation through the recursion theorem (MIPRE/Foundations/Tsirelson/Separation.lean, MIPRE/Tsirelson.lean).

The commuting-operator track (planning/mipco-track.md, Phase 0): lem:compressible-criterion-nested, lem:mipco-sub-core, thm:halting-co and thm:mipco-eq-core, the last two from a gap compression sound in ValueModel.commuting (MIPRE.GapCompression.Sound), which MIPRE.gapCompressionCo_sound provides (thm:mipco-eq-core-unconditional, below). The reduction and the classes are generic in a value model (MIPRE/Foundations/ValueModel.lean, the Halting/ modules and Foundations/ClassMIPStarComputable.lean); the commuting-operator instances are MIPRE/Foundations/ClassMIPCo.lean and MIPRE/MIPCo.lean.

The commuting-operator track, Phase 1(a) (planning/mipco-track.md §5): the commutation-preserving dilation, lem:co-dilation, and the attainment of ω_co on projective strategies, thm:co-value-projective (MIPRE/Foundations/OperatorMatrix.lean, MIPRE/Foundations/HalmosDilation.lean, MIPRE/Foundations/CommutingDilation.lean).

The commuting-operator track, Phase 1(b) and (c) (planning/mipco-track.md §5): the commuting-operator value as a supremum of model values, lem:co-value-model (MIPRE/Foundations/POVMValue.lean); the ancilla extension of a bipartite model, lem:ancilla-extension (MIPRE/Foundations/AncillaModel.lean); the soundness chain of compression in a value model, lem:compress-sound-in, and its composition, thm:pipeline-sound-in (MIPRE/Foundations/Pipeline/Compress.lean); and MIP^co = coRE from the three stages' clauses, cor:mipco-from-stages (MIPRE/MIPCo.lean).

The commuting-operator track, Phase 2 (planning/mipco-track.md §5): strategies in a model read in ω_co, lem:model-strategy-co (MIPRE/Foundations/CommutingModel.lean); the repetition bound in ω_co and parallel repetition sound there, lem:repetition-sound-bound-co and thm:parallel-repetition-co (MIPRE/Background/Repetition/Soundness.lean, Verifier.lean, VerifierCo.lean, MIPRE/Foundations/Pipeline/Repetition.lean); oracularization in a bipartite model and in ω_co, lem:oracular-soundness-model and lem:oracular-soundness-co (MIPRE/Foundations/OracularModel.lean); post-processing and detyping in a model, lem:transports-model (MIPRE/Foundations/OracularModel.lean, MIPRE/Foundations/CL/DetypingModel.lean); and oracularization sound in both value models, thm:oracularization-in-model (MIPRE/Foundations/OracularValue.lean, MIPRE/Foundations/Pipeline/Oracularization.lean).

The commuting-operator track, Phase 3 (planning/mipco-track.md §5): projective strategies in a bipartite model and their operations, lem:model-proj-strategy, and their reading in the two models, lem:model-proj-strategy-values (MIPRE/Foundations/ModelStrategy.lean); the seeded CL test sound in the tensor-product model, lem:lidt-sound-in-tensor (MIPRE/Background/LIDT/ModelSoundness.lean); and answer reduction sound in ω_co given that test's soundness in the commuting-operator model, thm:ar-sound-co (MIPRE/Background/AnswerReduction/SoundFinal.lean, Instance.lean). The answer-reduction chain itself is restated in a model under its existing guards.

The commuting-operator track, Phase 4 (planning/mipco-track.md §5): local isometries of bipartite models, lem:local-isometry (MIPRE/Foundations/LocalIsometry.lean); moving registers along them, lem:ancilla-isometries (MIPRE/Foundations/AncillaIsometry.lean); the register model, lem:register-model (MIPRE/Foundations/Introspection/RegisterModel.lean); the ancilla extension of a tensor-product model, lem:tensor-expand (MIPRE/Foundations/TensorExpand.lean); the one-sided ancilla extension, lem:one-sided-extension (MIPRE/Foundations/AncillaDilation.lean); the projective dilation in a star-ordered ring, lem:kraus-dilation (MIPRE/Foundations/KrausDilation.lean); domination of POVM strategies and approximation by projective ones, lem:povm-domination (MIPRE/Foundations/POVMDomination.lean, MIPRE/Foundations/Introspection/SourcePaddingValue.lean); reductions of POVM strategies, lem:povm-reduction (MIPRE/Foundations/POVMReduction.lean, MIPRE/Foundations/ModelOver.lean); the Pauli basis test sound in the tensor-product model, lem:qld-sound-in-tensor (MIPRE/Background/QLD/Soundness.lean since Phase 5, as the tensor-product instance of thm:qld, with the definitions in MIPRE/Background/QLD/ModelSoundness.lean); and introspection sound in every value model where that test is, thm:intro-sound-co (MIPRE/Background/Introspection/Compiler.lean). The introspection analysis itself is restated in a model under its existing guards.

The Pauli extraction for the introspection game and the source bound from it, in a bipartite model: lem:intro-pauli-extraction and lem:intro-extracted-soundness (MIPRE/Background/Introspection/RestrictedSoundness.lean, RestrictedProfileSoundness.lean), which replace the tensor-product statements of the removed PauliExtraction.lean.

The commuting-operator track, Phase 5 (planning/mipco-track.md §5): isomorphisms of bipartite models and what they carry, lem:model-iso, and those between extensions, lem:extension-isos (MIPRE/Foundations/ModelIso.lean); readings of an extension, lem:model-reading (MIPRE/Foundations/ModelReading.lean); embeddings, lem:model-embedding (MIPRE/Foundations/ModelEmbedding.lean); the seeded test moved between models, lem:lidt-model-transport (MIPRE/Background/LIDT/ModelTransport.lean); the commutant of a matrix amplification, lem:ampl-commutant, and the extension of a commuting-operator model, lem:co-extension (MIPRE/Foundations/AmplCommutant.lean); the seeded test in those extensions, lem:lidt-sound-co-expand (MIPRE/Background/LIDT/CoExpand.lean); scalar matrices on a register, lem:register-action (MIPRE/Foundations/EPRContraction.lean); the state calculus and Parseval in a model, lem:model-state-calculus and lem:model-parseval (MIPRE/Foundations/ModelCalculus.lean); the Pauli basis test sound in the commuting-operator model given the seeded test, lem:qld-sound-co (MIPRE/Background/QLD/Soundness.lean); and MIP^co = coRE from the seeded test alone, cor:mipco-from-lidt (MIPRE/MIPCo.lean). The Pauli basis analysis itself is restated in a model under the guards of MIPRE/Background/QLD/Axioms.lean.

The commuting-operator track, Phase 6 (planning/mipco-track.md §5, C6a): finite pairs and their ancilla extensions, lem:finite-pair-expand (MIPRE/Foundations/FinitePairExpand.lean); ω_co approached in dyadic pairs since C6b, lem:co-value-finite-pair (MIPRE/Background/Repetition/{TracialApprox,DyadicApprox}.lean); answer reduction and the Pauli basis test from the seeded test in dyadic pairs, thm:ar-sound-co-fin and lem:qld-approx-co-fin; and the conditional theorem, cor:mipco-from-lidt-fin (MIPRE/MIPCo.lean).

The commuting-operator track, C6b's II₁ orthonormalization tier (planning/c6b-plan.md, T1): a centre-valued trace for a von Neumann algebra with a faithful tracial vector functional, lem:center-valued-trace (MIPRE/Background/Orthonormalization/{CenterTrace,CenterTraceClauses, CenterComparison}.lean); de la Salle's Theorem 1.2 without abelian projections, thm:orthonormalization-no-abelian (NoAbelian.lean); and in a finite pair, cor:orthonormalization-finite-pair (FinitePairOrtho.lean).

The commuting-operator track, the rest of C6b's II₁ tier (planning/c6b-plan.md, T2–T5): unital dyadic matrix units and Pauli sites, lem:dyadic-units-closure and lem:pauli-sites-units (MIPRE/Foundations/MatUnits.lean); no abelian projections under dyadic units and a vector trace, thm:no-abelian-dyadic, and the closure of dyadic pairs, lem:dyadic-pair-closure (MIPRE/Foundations/DyadicPair.lean); the twisted Pauli algebra, lem:pauli-algebra (MIPRE/Background/Repetition/PauliAlgebra.lean); amplification by it, lem:amplification-dyadic (Amplify.lean); and orthonormalization in a dyadic pair, cor:orthonormalization-dyadic-pair (MIPRE/Background/Orthonormalization/DyadicOrtho.lean). The value lemma restated to dyadic pairs keeps its guard in the C6a block above.

The commuting-operator track, C6b's port (planning/c6b-plan.md, M0–M1): swap symmetry as three theorems of the symmetric model, lem:sym-model-swap (MIPRE/Background/LIDT/Co/Basic/QuantumState.lean), and the commutativity of points over it, lem:co-commutativity-points (MIPRE/Background/LIDT/Co/CommutativityPoints/BridgeTheorems/ DropBridges.lean and AnswerTheorems.lean). The port is not a vendored tree, so its guards live here. The model itself, def:sym-model, is a definition and carries no proof-level mark.

The doubling and the summed semidefinite form (C6b, M2 and M9 of planning/c6b-plan.md). The order of a finite pair's algebras, lem:finite-pair-order (MIPRE/Foundations/FinitePairOrder.lean); the doubled model of a finite pair as a finite pair, its role average and its abelian projections, lem:doubled-model-finite-pair, lem:doubled-model-role-average and lem:doubled-model-no-abelian (MIPRE/Foundations/Doubling.lean and MIPRE/Background/LIDT/Co/Doubling/); the symmetric strategy, thm:doubled-symmetrization, and orthonormalization in the doubled model, thm:doubled-orthonormalization; the summed form in a commutant with a vector trace, thm:summed-sdp (MIPRE/Foundations/SummedSdp.lean and MIPRE/Background/Orthonormalization/SdpMaximizer.lean), and in the doubled model, cor:summed-sdp-doubled (Co/Doubling/Sdp.lean). The doubled model itself, def:doubled-model, is a definition and carries no proof-level mark.

The rest of the preliminaries and the local-to-global variance inequality (C6b, M3 and M5 of planning/c6b-plan.md): the switch sandwich and the self-consistency calculus over a symmetric model, lem:co-switch-sandwich-self-consistency (MIPRE/Background/LIDT/Co/Preliminaries/SwitchSandwichMain/Completeness.lean, BipartiteSelfConsistency/, SelfConsistency/ and CompletionTransfer.lean), and the local-to-global inequality on any vector state by Gram positivity, lem:co-local-to-global (MIPRE/Background/LIDT/Co/ExpansionHypercubeGraph/).

The Schwartz--Zippel step, the global variance of the points, the commutation of the slice measurements and orthonormalization in a symmetric model (C6b, M4, M6, M7 and M8 of planning/c6b-plan.md): lem:co-schwartz-zippel-step (MIPRE/Background/LIDT/Co/Test/SchwartzZippelStep.lean), lem:co-global-variance-of-points (MIPRE/Background/LIDT/Co/GlobalVariance/), lem:co-commutation-g (MIPRE/Background/LIDT/Co/Commutativity/) and lem:co-orthonormalization (MIPRE/Background/LIDT/Co/MakingMeasurementsProjective/), whose rounding calls the orthonormalization tier in place of the vendored finite-dimensional route.

Self-improvement and pasting in a symmetric model (C6b, M10 and M11 of planning/c6b-plan.md): lem:co-self-improvement (MIPRE/Background/LIDT/Co/SelfImprovement/), whose semidefinite program is M9's summed form through SdpStatementWithSlackness.of_isSummedSdp and whose rounding is M8's orthonormalization, and lem:co-ld-pasting (MIPRE/Background/LIDT/Co/Pasting/).

The end of the port (C6b, M12–M14 of planning/c6b-plan.md): the main induction over a symmetric model, lem:co-main-induction (MIPRE/Background/LIDT/Co/MainInductionStep/Theorems/MainTheorems/Successor.lean); the main theorem in a dyadic pair, thm:co-main-formal (MIPRE/Background/LIDT/Co/Test/MainTheorem/MainFormal.lean), through the main induction in the doubled model and the unsymmetrization of Theorem E, lem:doubled-unsymmetrization (MIPRE/Background/LIDT/Co/Doubling/Unsymmetrization.lean); the canonical-line theorem in a dyadic pair, lem:co-lidt-canonical-line (MIPRE/Background/LIDT/Co/Bridge/), and the model chain to SoundIn, lem:lidt-sound-in-of-model-lidt (MIPRE/Background/LIDT/Co/Chain/); SoundFin, thm:lidt-sound-fin (MIPRE/Background/LIDT/Co/SoundFin.lean); and, without hypothesis, the commuting-operator soundness of compression, the halting reduction to ω_co and MIP^co = coRE, thm:mipco-eq-core-unconditional (MIPRE/MIPCo.lean).