The actual game controls Alice's next-prefix marginal #
Bob's prefix rigidity follows from Sample and primitive Z extraction. The actual Introspect consistency loop and the exact EPR mirror transfer this estimate to Alice, with no assumed Alice prefix rigidity or alphabet loss.
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 Ξ, and the exact mirror is the
register model's (Honest.hidingPrefixOp_registerState_mirror).
theorem
MIPRE.Introspection.TypedEstimates.introspect_prefix_register_rigidity_alice
{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]
[Algebra (ZMod 2) 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)).stateSqNorm
((POVMIn.map (reportedPrefix (L w) j AuxType.introspect) (MA (QuestionType.introspect w, 0))).op y - smulKron 1 (Honest.hidingPrefixOp (L w) j y)) ≤ 8 * η + 28 * ↑(TypeGraph.edges E X Z ℓ).card * ε
Every Alice Introspect-prefix marginal is controlled by the actual consistency and Sample tests and the primitive Bob-Z error. Malformed and unattainable outcomes remain in the complete option-valued alphabet.