Full hiding rigidity from the actual game and extracted Pauli bounds

The X/Hide-zero test supplies the induction base, and the Z/Sample/Introspect tests supply every prefix estimate. Consequently the final theorem assumes only the primitive extracted Pauli bounds, actual game success, and the projectivity needed for the cross-party coarse-grainings. Its bound is uniform over all hiding levels and includes malformed answer mass.

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 measurements are POVMs in its algebras, and the honest Pauli readouts enter as smulKron 1 _.

def MIPRE.Introspection.TypedEstimates.hidingPauliBudget (ℓ : ℕ) (e δX ηZ : ℝ) : ℝ

A single explicit Bob budget at every hiding level.

Equations

• MIPRE.Introspection.TypedEstimates.hidingPauliBudget ℓ e δX ηZ = 6 ^ ℓ * ((94 + 48 * ↑ℓ ^ 2) * e + 2 * δX + 24 * ηZ)

theorem MIPRE.Introspection.TypedEstimates.hidingPauliBudget_eq_uniform (ℓ : ℕ) (e δX ηZ : ℝ) : hidingPauliBudget ℓ e δX ηZ = hidingUniformBudget ℓ e (4 * ηZ + 12 * e) (4 * e + 2 * δX)

theorem MIPRE.Introspection.TypedEstimates.hiding_register_rigidity_of_pauli {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) ℬ)) {ε δX ηZ : ℝ} (hfail : 1 - (Ξ.reg (ι → F)).povmValue (parsedGame E X Z P L projectPauli D DP) MA MB ≤ ε) (qX qZ : κ → ZMod 2) (hqX : ∀ (z : κ → ZMod 2), (P X).eval z = qX) (hqZ : ∀ (z : κ → ZMod 2), (P Z).eval z = qZ) (hPX : IsPVMIn (MA (QuestionType.pauli X, qX)).op) (hX : ∑ x : Option (ι → F), (Ξ.reg (ι → F)).stateSqNorm ((POVMIn.map (pauliProjection projectPauli) (MA (QuestionType.pauli X, qX))).op x - smulKron 1 (Honest.pauliXReadout x)) ≤ δX) (hZ : ∑ z : Option (ι → F), (Ξ.reg (ι → F)).snorm ((Ξ.reg (ι → F)).πB ((POVMIn.map (pauliProjection projectPauli) (MB (QuestionType.pauli Z, qZ))).op z - smulKron 1 (readout some z))) ^ 2 ≤ ηZ) (w : Bool) (hL : (L w).SupportedOn Finset.univ) (hS : IsPVMIn (MA (QuestionType.sample w, 0)).op) (hMA : ∀ (j : Fin ℓ), IsPVMIn (MA (QuestionType.hide w j, 0)).op) (hMB : ∀ (j : Fin ℓ), IsPVMIn (MB (QuestionType.hide w j, 0)).op) (j : Fin ℓ) : hidingBobError L w hL Ξ MB j ≤ hidingPauliBudget ℓ (↑(TypeGraph.edges E X Z ℓ).card * ε) δX ηZ ∧ hidingAliceError L w hL Ξ MA j ≤ 4 * ↑(TypeGraph.edges E X Z ℓ).card * ε + 2 * hidingPauliBudget ℓ (↑(TypeGraph.edges E X Z ℓ).card * ε) δX ηZ

Complete hiding rigidity in the extracted register state. There is no assumed hiding or prefix conclusion, and no symmetry premise on DP. The two primitive Pauli errors are same-party distances: Alice X and Bob Z.