An actual adjacent hiding rigidity step on the EPR seed

All ideal measurements, commutation facts, exact mirrors, and label identities are explicit. The remaining quantitative inputs are the preceding fine error, the next prefix marginal error, and the actual parsed game's failure.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the EPR seed is the register model Ξ.reg (ι → F) of a model Ξ --- the seed alone being the instance in which Ξ is trivial --- the strategy is a pair of POVM families of matrices over ι → F with entries in Ξ's algebras, and an honest register operator P acts as smulKron 1 P. The exact mirrors of the honest operators are the mirror identity of the register model (BipartiteModel.reg_mirror), the honest operators being symmetric.

theorem MIPRE.Introspection.TypedEstimates.hiding_next_seed_rigidity {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) ℬ)) {ε η εfine : ℝ} (hfail : 1 - (Ξ.reg (ι → F)).povmValue (parsedGame E X Z P L projectPauli D DP) MA MB ≤ ε) (w : Bool) (k j : Fin ℓ) (hk : ↑k + 1 = ↑j) (hL : (L w).SupportedOn Finset.univ) (hMA : IsPVMIn (MA (QuestionType.hide w k, 0)).op) (hMB : IsPVMIn (MB (QuestionType.hide w j, 0)).op) (hfine : ∑ i : Option ((ι → F) × (ι → F) × (ι → F)), (Ξ.reg (ι → F)).xSqNorm ((POVMIn.map (hidingCoarse (L w) ↑k) (MA (QuestionType.hide w k, 0))).op i) (smulKron 1 (Honest.hideCoarseOp (L w) (↑k) hL i)) ≤ εfine) (hnorm : ∑ y : Option (ι → F), (Ξ.reg (ι → F)).snorm ((Ξ.reg (ι → F)).πB (∑ z : Option ((ι → F) × (ι → F) × (ι → F)), (POVMIn.map (hidingNextLater (L w) ↑k) (MB (QuestionType.hide w j, 0))).op (y, z) - smulKron 1 (Honest.hidingPrefixOp (L w) (↑j) y))) ^ 2 ≤ η) : ∑ z : Option (Honest.HideLabel F ι), (Ξ.reg (ι → F)).xSqNorm (smulKron 1 (Honest.hideCoarseOp (L w) (↑j) hL z)) ((POVMIn.map (hidingCoarse (L w) ↑j) (MB (QuestionType.hide w j, 0))).op z) ≤ 6 * ↑(TypeGraph.edges E X Z ℓ).card * ε + 3 * η + 3 * εfine

A single actual adjacent hiding test propagates fine honest rigidity to the next level with error 6 |E| ε + 3 η + 3 εfine. This theorem assumes no ideal commutation, exact-mirror, or accepted-answer contract.