Quotient hiding comparisons in the complete typed predicate

The quotient comparisons accept every legacy accepted tuple. Deterministic answer decoding restores legacy acceptance on every raw question and answer, including consistency loops and both orientations of auxiliary edges.

noncomputable def MIPRE.Introspection.AuxiliaryQuotient.decodeAnswer {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {A : Type u_4} [Field F] {ι : Type u_5} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) : QuestionType PauliType ℓ → ParsedAnswer (ι → F) A PauliAnswer → ParsedAnswer (ι → F) A PauliAnswer

Decode only dual coordinates, with the CL function selected by question side.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.Introspection.AuxiliaryQuotient.decodeAnswer L x✝¹ x✝ = x✝

@[simp]

theorem MIPRE.Introspection.AuxiliaryQuotient.fits_decodeAnswer {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {A : Type u_4} [Field F] {ι : Type u_5} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (t : QuestionType PauliType ℓ) (a : ParsedAnswer (ι → F) A PauliAnswer) : TypedPredicate.fits t (decodeAnswer L t a) = TypedPredicate.fits t a

Decoding preserves the answer constructor and hence the format check.

noncomputable def MIPRE.Introspection.AuxiliaryQuotient.directed {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {A : Type u_4} [Field F] {ι : Type u_5} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (X Z : PauliType) (projectPauli : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) : QuestionType PauliType ℓ → QuestionType PauliType ℓ → ParsedAnswer (ι → F) A PauliAnswer → ParsedAnswer (ι → F) A PauliAnswer → Bool

The directed tests with the two exact dual comparisons replaced by quotient comparisons.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.Introspection.AuxiliaryQuotient.directed L X Z projectPauli D x✝³ x✝² x✝¹ x✝ = true

theorem MIPRE.Introspection.AuxiliaryQuotient.directed_of_legacy {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {A : Type u_4} [Field F] {ι : Type u_5} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (X Z : PauliType) (project : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (t u : QuestionType PauliType ℓ) (a b : ParsedAnswer (ι → F) A PauliAnswer) (h : TypedPredicate.directed L X Z project D t u a b = true) : directed L X Z project D t u a b = true

Every legacy directed comparison implies the quotient comparison.

theorem MIPRE.Introspection.AuxiliaryQuotient.directed_sound {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {A : Type u_4} [Field F] {ι : Type u_5} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (X Z : PauliType) (project : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (t u : QuestionType PauliType ℓ) (a b : ParsedAnswer (ι → F) A PauliAnswer) (h : directed L X Z project D t u a b = true) : TypedPredicate.directed L X Z project D t u (decodeAnswer L t a) (decodeAnswer L u b) = true

Every quotient directed comparison becomes a legacy comparison after decoding.

noncomputable def MIPRE.Introspection.AuxiliaryQuotient.check {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {A : Type u_4} [Field F] {ι : Type u_5} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (X Z : PauliType) (project : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (DP : PauliType → PauliType → PauliAnswer → PauliAnswer → Bool) (t u : QuestionType PauliType ℓ) (a b : ParsedAnswer (ι → F) A PauliAnswer) : Bool

Complete typed predicate with quotient hiding comparisons. All format, consistency, Pauli and source-game checks are unchanged.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Introspection.AuxiliaryQuotient.check_of_legacy {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {A : Type u_4} [Field F] {ι : Type u_5} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (X Z : PauliType) (project : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (DP : PauliType → PauliType → PauliAnswer → PauliAnswer → Bool) (t u : QuestionType PauliType ℓ) (a b : ParsedAnswer (ι → F) A PauliAnswer) (h : TypedPredicate.check L X Z project D DP t u a b = true) : check L X Z project D DP t u a b = true

Legacy acceptance always implies quotient acceptance, including both orientations.

theorem MIPRE.Introspection.AuxiliaryQuotient.check_sound {PauliType : Type u_1} {PauliAnswer : Type u_2} {F : Type u_3} {A : Type u_4} [Field F] {ι : Type u_5} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (L : Bool → CL.CLFun F ι ℓ) (X Z : PauliType) (project : PauliAnswer → ι → F) (D : (ι → F) → (ι → F) → A → A → Bool) (hL : ∀ (w : Bool), (L w).SupportedOn Finset.univ) (DP : PauliType → PauliType → PauliAnswer → PauliAnswer → Bool) (t u : QuestionType PauliType ℓ) (a b : ParsedAnswer (ι → F) A PauliAnswer) (h : check L X Z project D DP t u a b = true) : TypedPredicate.check L X Z project D DP t u (decodeAnswer L t a) (decodeAnswer L u b) = true

Every accepted quotient tuple is accepted by the legacy predicate after decoding. This statement covers every raw answer, rather than only sampler outputs.