Actual Sample tests bound the conditional adaptive Z error

The product-form hypothesis is only the current strategy's induction form. Its conditional Z-commutator estimate follows from actual parsed-game success and primitive Pauli-Z extraction. All malformed Introspect answers remain in the common option-valued residual alphabet.

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 readouts enter as smulKron 1 _.

theorem MIPRE.Introspection.readout_some_comp {I : Type u_4} {C : Type u_5} [Fintype I] [DecidableEq I] [Fintype C] [DecidableEq C] (g : I → C) (c : C) : readout (fun (i : I) => some (g i)) (some c) = readout g c

theorem MIPRE.Introspection.readout_none_comp {I : Type u_4} {C : Type u_5} [Fintype I] [DecidableEq I] [Fintype C] [DecidableEq C] (g : I → C) : readout (fun (i : I) => some (g i)) none = 0

theorem MIPRE.Introspection.option_readout_commutator_sum {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {I : Type u_4} {C : Type u_5} {B : Type u_6} [Fintype I] [DecidableEq I] [Fintype C] [DecidableEq C] [Fintype B] (Ψ : BipartiteModel 𝒞 (Matrix I I 𝒜) ℬ) (g : I → C) (M : B → Matrix I I 𝒜) : ∑ b : B, ∑ c : Option C, Ψ.stateSqNorm (M b * smulKron 1 (readout (fun (i : I) => some (g i)) c) - smulKron 1 (readout (fun (i : I) => some (g i)) c) * M b) = ∑ b : B, ∑ c : C, Ψ.stateSqNorm (M b * smulKron 1 (readout g c) - smulKron 1 (readout g c) * M b)

The impossible none ideal contributes zero, without splitting the actual measurement's outcome alphabet.

theorem MIPRE.Introspection.TypedEstimates.introspect_adaptiveZ_commutator {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {PauliType : Type u_4} {PauliAnswer : Type u_5} {F : Type u_6} {ι : Type u_7} {κ : Type u_8} {A : Type u_9} [Fintype PauliType] [DecidableEq PauliType] [Fintype PauliAnswer] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] [Fintype A] {ℓ : ℕ} [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] [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 ≤ ε) (q : κ → ZMod 2) (hq : ∀ (z : κ → ZMod 2), (P Z).eval z = q) (w : Bool) (hS : IsPVMIn (MB (QuestionType.sample w, 0)).op) (hZ : ∑ z : Option (ι → F), (Ξ.reg (ι → F)).snorm ((Ξ.reg (ι → F)).πB ((POVMIn.map (pauliProjection projectPauli) (MB (QuestionType.pauli Z, q))).op z - smulKron 1 (readout some z))) ^ 2 ≤ η) (hL : (L w).SupportedOn Finset.univ) (k : ℕ) (M : (y : ι → F) → Option ((ι → F) × A) → Matrix (↥(stageRemaining (L w) k y) → F) (↥(stageRemaining (L w) k y) → F) 𝒜) (hform : ∀ (a : Option ((ι → F) × A)), (POVMIn.map introspectPair (MA (QuestionType.introspect w, 0))).op a = ∑ y : ι → F, prefixResidualOp (L w) k y (M y a)) : ∑ y : ι → F, prefixWeight (L w) k y * ∑ a : Option ((ι → F) × A), ∑ z : Fin (Fintype.card ↥((L w).factorOfPrefix k y)) → F, (Ξ.reg (↥(stageRemaining (L w) k y) → F)).stateSqNorm (M y a * registerReadout (stageSplit (L w) hL k y) Weyl.wZ LinearMap.id z - registerReadout (stageSplit (L w) hL k y) Weyl.wZ LinearMap.id z * M y a) ≤ 64 * η + 224 * ↑(TypeGraph.edges E X Z ℓ).card * ε

The actual Sample joint measurement supplies the conditional Z estimate for a strategy in the current adaptive product form. The prefix law, local registers, and ideal readout identification are all discharged internally.