Sampling supplies the Introspect-prefix rigidity input

The actual Z/Sample and Sample/Introspect tests transfer extracted Pauli-Z rigidity to every Introspect prefix. The only coarse-graining of a distance is between two projective measurements on opposite parties, so the loss is independent of the seed and answer alphabets.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the state is the register model Ξ.reg (ι → F) of a normalized auxiliary model, and the honest Z readouts enter as smulKron 1 _.

theorem MIPRE.Introspection.TypedEstimates.sampling_replace_bob {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {Y : Type u_4} [Fintype Y] (S : Y → 𝒜) (Z Q : Y → ℬ) {e η : ℝ} (hS : ∑ y : Y, Ψ.xSqNorm (S y) (Z y) ≤ e) (hZ : ∑ y : Y, Ψ.snorm (Ψ.πB (Z y - Q y)) ^ 2 ≤ η) : ∑ y : Y, Ψ.xSqNorm (S y) (Q y) ≤ 2 * e + 2 * η

theorem MIPRE.Introspection.TypedEstimates.sampling_common_alice {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {Y : Type u_4} [Fintype Y] (S : Y → 𝒜) (I Q : Y → ℬ) {e η : ℝ} (hI : ∑ y : Y, Ψ.xSqNorm (S y) (I y) ≤ e) (hQ : ∑ y : Y, Ψ.xSqNorm (S y) (Q y) ≤ η) : ∑ y : Y, Ψ.snorm (Ψ.πB (I y - Q y)) ^ 2 ≤ 2 * e + 2 * η

theorem MIPRE.Introspection.TypedEstimates.introspect_prefix_register_rigidity_bob {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {κ : Type u_5} {A : Type u_6} [Fintype PauliType] [DecidableEq PauliType] [Fintype PauliAnswer] [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] [Fintype A] {ℓ : ℕ} {𝒞 : Type u_7} {𝒜 : Type u_8} {ℬ : Type u_9} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [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 ≤ ε) (q : κ → ZMod 2) (hq : ∀ (z : κ → ZMod 2), (P Z).eval z = q) (w : Bool) (hL : (L w).SupportedOn Finset.univ) (hS : IsPVMIn (MA (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 ≤ η) (j : ℕ) : ∑ y : Option (ι → F), (Ξ.reg (ι → F)).snorm ((Ξ.reg (ι → F)).πB ((POVMIn.map (reportedPrefix (L w) j AuxType.introspect) (MB (QuestionType.introspect w, 0))).op y - smulKron 1 (Honest.hidingPrefixOp (L w) j y))) ^ 2 ≤ 4 * η + 12 * ↑(TypeGraph.edges E X Z ℓ).card * ε