A concrete adjacent hiding rigidity step in the actual parsed game

The state has the extracted EPR seed and an arbitrary normalized auxiliary state. Only the preceding fine estimate and the Introspect-prefix estimate are induction inputs. The actual game supplies the conditional relation and propagates the required normalizer through its hiding/Read/Introspect chain.

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 operators enter as smulKron 1 _.

theorem MIPRE.Introspection.TypedEstimates.hiding_next_register_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) (hintro : ∑ 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 ≤ δ) : ∑ 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 + 48 * ↑(ℓ - ↑j + 1) ^ 2) * ↑(TypeGraph.edges E X Z ℓ).card * ε + 6 * δ + 3 * εfine

The actual next Hide measurement is rigid with no dimension or answer alphabet factor. All ideal commutation, mirror, and accepted-answer facts are proved from the construction. The remaining inputs are the preceding fine rigidity and the Introspect-prefix estimate from sampling/Pauli extraction.