Guarded coarse maps for the actual adjacent hiding test

The earlier fine label retains only its preceding prefix, current dual output, and remaining tail. The next map uses the later prefix as a key. A separate dummy outcome handles malformed answers and prefix mismatches, so each keyed map is total on the entire answer alphabet and defines a complete measurement.

def MIPRE.Introspection.TypedEstimates.hidingCoarse {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {A : Type u_6} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) : ParsedAnswer (ι → F) A PauliAnswer → Option ((ι → F) × (ι → F) × (ι → F))

The fine outcome retained at hiding level k+1. Off-format answers have their own outcome; unused coordinates of a well-formed answer are discarded.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.Introspection.TypedEstimates.hidingCoarse P k x✝ = none

noncomputable def MIPRE.Introspection.TypedEstimates.hidingNextGuarded {F : Type u_3} {ι : Type u_4} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) : Option (ι → F) → Option ((ι → F) × (ι → F) × (ι → F)) → Option ((ι → F) × (ι → F) × (ι → F))

Process a retained fine outcome using the later prefix. On a prefix mismatch the output is the dummy label, rather than an incomplete family.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.Introspection.TypedEstimates.hidingNextGuarded P k x✝¹ x✝ = none

theorem MIPRE.Introspection.TypedEstimates.hidingNextGuarded_factor {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {A : Type u_6} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (k : ℕ) (y yp x z : ι → F) (hmatch : P.outputPrefix k y = P.outputPrefix k z) : hidingNextGuarded P k (some z) (hidingCoarse P k (ParsedAnswer.hide y yp x)) = hidingNextEarlier P k (some z) (ParsedAnswer.hide y yp x)

On matching prefixes, the new keyed map factors through exactly the previous hiding label; no raw discarded tail coordinates are needed.

theorem MIPRE.Introspection.TypedEstimates.hiding_next_accepts_guarded {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {A : Type u_6} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} [Fintype PauliType] [DecidableEq PauliType] [Fintype PauliAnswer] [Fintype F] [DecidableEq F] [Fintype A] (L : Bool → CL.CLFun F ι ℓ) (X Z : PauliType) (projectPauli : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : PauliType → PauliType → PauliAnswer → PauliAnswer → Bool) (w : Bool) (k j : Fin ℓ) (hk : ↑k + 1 = ↑j) (hL : (L w).SupportedOn Finset.univ) {a b : ParsedAnswer (ι → F) A PauliAnswer} (h : TypedPredicate.check L X Z projectPauli D DP (QuestionType.hide w k) (QuestionType.hide w j) a b = true) : hidingNextGuarded (L w) (↑k) (hidingNextLater (L w) (↑k) b).1 (hidingCoarse (L w) (↑k) a) = (hidingNextLater (L w) (↑k) b).2

The actual parsed check implies equality of the guarded coarse outcomes. No support or in-image hypothesis on the answers is used.