Introspection soundness from local-isometry image estimates

This assembles the actual transported strategy and its image-complement completion. Primitive estimates can be stated on the ideal register state, as in Pauli extraction, for the image effects of the original measurements. No future normalized measurement or transported game-success assumption is required. The full projected answer alphabet includes malformed outcomes.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the original strategy lives in any model M, and the local isometries are one local isometry of models Φ from M into the register model Ξ.reg (ι → F). Its homomorphisms are not unital, so the transported measurements are completed by the image complement (LocalIsometry.transportA), whose mass the state distance controls (IsometricCompletionError).

theorem MIPRE.Introspection.TypedEstimates.quantumValue_ge_of_isometric_images {F ι A : Type} {PauliType : Type u_1} {PauliAnswer : Type u_2} {κ : Type u_3} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype A] [Nonempty A] [Fintype PauliType] [DecidableEq PauliType] [Fintype PauliAnswer] [Fintype κ] [DecidableEq κ] {ℓ : ℕ} {𝒞 𝒜 ℬ : Type u} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] {𝒞₀ : Type u_4} {𝒜₀ : Type u_5} {ℬ₀ : Type u_6} [Ring 𝒞₀] [StarRing 𝒞₀] [Algebra ℂ 𝒞₀] [Ring 𝒜₀] [StarRing 𝒜₀] [Algebra ℂ 𝒜₀] [Ring ℬ₀] [StarRing ℬ₀] [Algebra ℂ ℬ₀] [PartialOrder 𝒜₀] [StarOrderedRing 𝒜₀] [PartialOrder ℬ₀] [StarOrderedRing ℬ₀] (E : PauliType → PauliType → Bool) (X Z : PauliType) (P : PauliType → CL.CLFun (ZMod 2) κ 3) (L : Bool → CL.CLFun F ι ℓ) (hL : ∀ (w : Bool), (L w).ExactlyOn Finset.univ) (projectPauli : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : PauliType → PauliType → (κ → ZMod 2) → (κ → ZMod 2) → PauliAnswer → PauliAnswer → Bool) (ω : ValueModel) (G : Game (ι → F) (ι → F) A A) (hμ : ∀ (x y : ι → F), G.μ x y = CL.clDist (L false).eval (L true).eval x y) (hD : G.D = D) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (hΞ : ‖Ξ.ψ‖ = 1) (hω : ω.DominatesPOVM Ξ) (M : BipartiteModel 𝒞₀ 𝒜₀ ℬ₀) (hM : ‖M.ψ‖ = 1) (Φ : M.LocalIsometry (Ξ.reg (ι → F))) (MA : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) 𝒜₀) (MB : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) ℬ₀) (hMA : ∀ (q : CL.Detyping.Question (QuestionType PauliType ℓ) κ), IsPVMIn (MA q).op) (hMB : ∀ (q : CL.Detyping.Question (QuestionType PauliType ℓ) κ), IsPVMIn (MB q).op) (qX qZ : κ → ZMod 2) (hqX : ∀ (z : κ → ZMod 2), (P X).eval z = qX) (hqZ : ∀ (z : κ → ZMod 2), (P Z).eval z = qZ) {t : ℝ} (ht : 0 ≤ t) (hstate : ‖Φ.W M.ψ - (Ξ.reg (ι → F)).ψ‖ ^ 2 ≤ t) (hfail : 1 - M.povmValue (parsedGame E X Z P L projectPauli D DP) MA MB ≤ t) (hX : ∑ x : Option (ι → F), (Ξ.reg (ι → F)).stateSqNorm (Φ.ΦA ((POVMIn.map (pauliProjection projectPauli) (MA (QuestionType.pauli X, qX))).op x) - smulKron 1 (Honest.pauliXReadout x)) ≤ t) (hZ : ∑ z : Option (ι → F), (Ξ.reg (ι → F)).swap.stateSqNorm (Φ.ΦB ((POVMIn.map (pauliProjection projectPauli) (MB (QuestionType.pauli Z, qZ))).op z) - smulKron 1 (readout some z)) ≤ t) : 1 - extractedSoundnessCoefficient ℓ ↑(TypeGraph.edges E X Z ℓ).card * iteratedRoot (6 * ℓ + 1) t ≤ ω.val G

The complete finite-game soundness argument with the original strategy and an actual local isometry. Primitive image estimates and the state bound are the only extraction inputs; all subsequent strategies are constructed.