Actual Read tests bound the conditional adaptive dual-X error

The current product-form equality identifies the full Introspect measurement. The honest dual marginal factors into the prefix projector and the current selected-register dual readout. Its local labels inject into the tested global alphabet, so discarding the remaining nonnegative commutator terms introduces no cardinality factor. No same-party distance is coarse-grained.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the extracted register state is the register model Ξ.reg (ι → F) of a normalized auxiliary model Ξ, the product form is one of matrices over the remaining registers with entries in its first algebra, and the honest dual readout enters as smulKron 1 _.

noncomputable def MIPRE.Introspection.adaptiveDualLabel {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (p : (y : ι → F) × (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F)) : Option ((ι → F) × (ι → F))

The local dual outcome is embedded in the actual option-valued readout alphabet, retaining the prefix which selected its register.

Equations

• MIPRE.Introspection.adaptiveDualLabel P k p = some (p.fst, (MIPRE.Introspection.coordinateInsert (P.factorOfPrefix k p.fst)) p.snd)

theorem MIPRE.Introspection.adaptiveDualLabel_injective {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) : Function.Injective (adaptiveDualLabel P k)

theorem MIPRE.Introspection.adaptiveDualLabel_sum_le {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (f : Option ((ι → F) × (ι → F)) → ℝ) (hf : ∀ (z : Option ((ι → F) × (ι → F))), 0 ≤ f z) : ∑ p : (y : ι → F) × (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F), f (adaptiveDualLabel P k p) ≤ ∑ z : Option ((ι → F) × (ι → F)), f z

theorem MIPRE.Introspection.adaptiveX_reassembled_commutator_le {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {𝒞 : Type u_3} {𝒜 : Type u_4} {ℬ : Type u_5} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ 𝒜] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) {A : Type u_6} [Fintype A] (M : (y : ι → F) → A → Matrix (↥(stageRemaining P k y) → F) (↥(stageRemaining P k y) → F) 𝒜) : ∑ y : ι → F, prefixWeight P k y * ∑ a : A, ∑ z : Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F, (Ξ.reg (↥(stageRemaining P k y) → F)).stateSqNorm (M y a * registerReadout (stageSplit P hP k y) Weyl.wX (CL.lperp (coordinateLinear (CLChecks.stageLinear P k y))) z - registerReadout (stageSplit P hP k y) Weyl.wX (CL.lperp (coordinateLinear (CLChecks.stageLinear P k y))) z * M y a) ≤ ∑ a : A, ∑ z : Option ((ι → F) × (ι → F)), (Ξ.reg (ι → F)).stateSqNorm ((∑ y : ι → F, prefixResidualOp P k y (M y a)) * smulKron 1 (Honest.readDualOp P k hP z) - smulKron 1 (Honest.readDualOp P k hP z) * ∑ y : ι → F, prefixResidualOp P k y (M y a))

The actual global coarse dual commutator controls the concrete adaptive weighted dual-X commutator, with coefficient one.

theorem MIPRE.Introspection.TypedEstimates.introspect_adaptiveX_commutator {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {𝒞 : Type u_3} {𝒜 : Type u_4} {ℬ : Type u_5} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {PauliType : Type u_6} {PauliAnswer : Type u_7} {κ : Type u_8} {A : Type u_9} [Fintype PauliType] [DecidableEq PauliType] [Fintype PauliAnswer] [Fintype κ] [DecidableEq κ] [Fintype A] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [StarModule ℂ ℬ] [PartialOrder ℬ] [StarOrderedRing ℬ] [StarProper ℬ] (E : PauliType → PauliType → Bool) (X Z : PauliType) (P : PauliType → CL.CLFun (ZMod 2) κ 3) (L : Bool → CL.CLFun F ι ℓ) (projectPauli : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : PauliType → PauliType → (κ → ZMod 2) → (κ → ZMod 2) → PauliAnswer → PauliAnswer → Bool) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (hΞ : ‖Ξ.ψ‖ = 1) (MA : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) 𝒜)) (MB : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) (Matrix (ι → F) (ι → F) ℬ)) {ε δ : ℝ} (hfail : 1 - (Ξ.reg (ι → F)).povmValue (parsedGame E X Z P L projectPauli D DP) MA MB ≤ ε) (w : Bool) (hL : (L w).SupportedOn Finset.univ) (j : Fin ℓ) (hMA : IsPVMIn (MA (QuestionType.hide w j, 0)).op) (hMB : IsPVMIn (MB (QuestionType.read w, 0)).op) (hfine : ∑ i : Option ((ι → F) × (ι → F) × (ι → F)), (Ξ.reg (ι → F)).xSqNorm ((POVMIn.map (hidingCoarse (L w) ↑j) (MA (QuestionType.hide w j, 0))).op i) (smulKron 1 (Honest.hideCoarseOp (L w) (↑j) hL i)) ≤ δ) (M : (y : ι → F) → Option ((ι → F) × A) → Matrix (↥(stageRemaining (L w) (↑j) y) → F) (↥(stageRemaining (L w) (↑j) y) → F) 𝒜) (hform : ∀ (a : Option ((ι → F) × A)), (POVMIn.map introFullPair (MA (QuestionType.introspect w, 0))).op a = ∑ y : ι → F, prefixResidualOp (L w) (↑j) y (M y a)) : ∑ y : ι → F, prefixWeight (L w) (↑j) y * ∑ a : Option ((ι → F) × A), ∑ z : Fin (Fintype.card ↥((L w).factorOfPrefix (↑j) y)) → F, (Ξ.reg (↥(stageRemaining (L w) (↑j) y) → F)).stateSqNorm (M y a * registerReadout (stageSplit (L w) hL (↑j) y) Weyl.wX (CL.lperp (coordinateLinear (CLChecks.stageLinear (L w) (↑j) y))) z - registerReadout (stageSplit (L w) hL (↑j) y) Weyl.wX (CL.lperp (coordinateLinear (CLChecks.stageLinear (L w) (↑j) y))) z * M y a) ≤ 16 * ((32 * ↑(ℓ - ↑j) ^ 2 + 6) * ↑(TypeGraph.edges E X Z ℓ).card * ε + 4 * δ)

Actual parsed-game success and hiding rigidity supply the conditional dual-X commutator estimate for the current adaptive product form.