The quantitative hiding-prefix chain in the actual typed game

Every earlier reported question prefix propagates from Hide to Introspect. The error depends quadratically on the number of remaining chain edges and linearly on the actual ordered-edge count, with no answer-cardinality loss.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the state is a model Ψ, the measurements MA are in the first player's algebra and MB in the second's, and the estimates are the first player's state distances Ψ.stateSqNorm. The model enters only through aux_agreement_estimate, same_side_via_common_other and hiding_chain_uniform, each of which takes it explicitly, so the second player's chain (TypedPrefixChainBob.lean) is the same argument in the swapped model Ψ.swap, whose state distance Ψ.swap.stateSqNorm is the second player's.

theorem MIPRE.Introspection.TypedEstimates.prefix_chain_step_estimate {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 ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (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) 𝒜) (MB : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) ℬ) {ε : ℝ} (hfail : 1 - Ψ.povmValue (parsedGame E X Z P L projectPauli D DP) MA MB ≤ ε) (w : Bool) (hL : (L w).SupportedOn Finset.univ) (j : Fin ℓ) (m : ℕ) (hm : m ≤ ↑j) (i : ℕ) (hi : i < ℓ - ↑j + 1) : ∑ z : Option (ι → F), Ψ.stateSqNorm ((POVMIn.map (reportedPrefix (L w) m (prefixChainType j i)) (MA (Sum.inr (prefixChainType j i, w), 0))).op z - (POVMIn.map (reportedPrefix (L w) m (prefixChainType j (i + 1))) (MA (Sum.inr (prefixChainType j (i + 1), w), 0))).op z) ≤ 8 * ↑(TypeGraph.edges E X Z ℓ).card * ε

The actual next path edge and the loop at its later endpoint compare the two Alice prefix measurements with loss 8 |E| ε.

theorem MIPRE.Introspection.TypedEstimates.hiding_introspect_prefix_estimate {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 ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (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) 𝒜) (MB : CL.Detyping.Question (QuestionType PauliType ℓ) κ → POVMIn (ParsedAnswer (ι → F) A PauliAnswer) ℬ) {ε : ℝ} (hfail : 1 - Ψ.povmValue (parsedGame E X Z P L projectPauli D DP) MA MB ≤ ε) (w : Bool) (hL : (L w).SupportedOn Finset.univ) (j : Fin ℓ) (m : ℕ) (hm : m ≤ ↑j) : ∑ z : Option (ι → F), Ψ.stateSqNorm ((POVMIn.map (reportedPrefix (L w) m (AuxType.hide j)) (MA (QuestionType.hide w j, 0))).op z - (POVMIn.map (reportedPrefix (L w) m AuxType.introspect) (MA (QuestionType.introspect w, 0))).op z) ≤ ↑(ℓ - ↑j + 1) ^ 2 * (8 * ↑(TypeGraph.edges E X Z ℓ).card * ε)

Every prefix present at Hide j is close to the same Introspect prefix on Alice's side, through the actual hiding chain and its consistency loops. Malformed answers are included as the none outcome throughout.