The dual readout retained along the actual hiding-to-Read chain

The stage and its preceding claimed prefix are fixed before coarse-graining. Every later hiding edge preserves this same pair, including off-image answers.

theorem MIPRE.Introspection.CLChecks.factorOfPrefix_outputPrefix {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (k : ℕ) (y : ι → F) : P.factorOfPrefix k (P.outputPrefix k y) = P.factorOfPrefix k y

theorem MIPRE.Introspection.CLChecks.factorOfPrefix_subset_prefixRegister {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (y : ι → F) : P.factorOfPrefix k y ⊆ prefixRegister P (k + 1) y

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

The prefix and the dual answer on one fixed stage's selected register.

Equations

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

def MIPRE.Introspection.TypedEstimates.hidingForgetTail {F : Type u_3} {ι : Type u_4} : Option ((ι → F) × (ι → F) × (ι → F)) → Option ((ι → F) × (ι → F))

Forgetting only the unused tail of a fine hiding outcome.

Equations

• MIPRE.Introspection.TypedEstimates.hidingForgetTail = Option.map fun (p : (ι → F) × (ι → F) × (ι → F)) => (p.1, p.2.1)

theorem MIPRE.Introspection.TypedEstimates.hidingForgetTail_coarse {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {A : Type u_5} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (j : Fin ℓ) (a : ParsedAnswer (ι → F) A PauliAnswer) : hidingForgetTail (hidingCoarse P (↑j) a) = reportedDual P (↑j) (AuxType.hide j) a

theorem MIPRE.Introspection.TypedEstimates.check_hiding_next_dual {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {A : Type u_5} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} [DecidableEq PauliType] (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) (hL : (L w).SupportedOn Finset.univ) (k j : Fin ℓ) (hk : ↑k + 1 = ↑j) (m : ℕ) (hm : m ≤ ↑k) {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) : reportedDual (L w) m (AuxType.hide k) a = reportedDual (L w) m (AuxType.hide j) b

theorem MIPRE.Introspection.TypedEstimates.check_hiding_read_dual {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {A : Type u_5} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} [DecidableEq PauliType] (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) (hL : (L w).SupportedOn Finset.univ) (k : Fin ℓ) (hk : ↑k + 1 = ℓ) (m : ℕ) (hm : m ≤ ↑k) {a b : ParsedAnswer (ι → F) A PauliAnswer} (h : TypedPredicate.check L X Z projectPauli D DP (QuestionType.hide w k) (QuestionType.read w) a b = true) : reportedDual (L w) m (AuxType.hide k) a = reportedDual (L w) m AuxType.read b

@[simp]

theorem MIPRE.Introspection.TypedEstimates.prefixChainType_read {ℓ : ℕ} (j : Fin ℓ) : prefixChainType j (ℓ - ↑j) = AuxType.read

theorem MIPRE.Introspection.TypedEstimates.prefixChainType_check_dual {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {ι : Type u_4} {A : Type u_5} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} [DecidableEq PauliType] (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) (hL : (L w).SupportedOn Finset.univ) (j : Fin ℓ) (m : ℕ) (hm : m ≤ ↑j) (i : ℕ) (hi : i < ℓ - ↑j) {a b : ParsedAnswer (ι → F) A PauliAnswer} (h : TypedPredicate.check L X Z projectPauli D DP (Sum.inr (prefixChainType j i, w)) (Sum.inr (prefixChainType j (i + 1), w)) a b = true) : reportedDual (L w) m (prefixChainType j i) a = reportedDual (L w) m (prefixChainType j (i + 1)) b

Every edge up to Read preserves one fixed earlier dual readout.