Hiding tests using coordinate-independent quotient comparisons

The old exact dual comparison implies the quotient comparison, preserving honest completeness. Conversely, quotient acceptance gives the old hiding predicate after deterministic answer decoding. Raw prefixes and tails retain the original checks. Neither direction assumes that a claimed prefix is attainable; obtaining legal source queries is a separate executable obligation.

@[reducible, inline]

abbrev MIPRE.Introspection.AuxiliaryQuotient.RegisterHideAnswer (F : Type u_3) (ι : Type u_4) : Type (max u_3 u_4)

Equations

• MIPRE.Introspection.AuxiliaryQuotient.RegisterHideAnswer F ι = ((ι → F) × (ι → F) × (ι → F))

noncomputable def MIPRE.Introspection.AuxiliaryQuotient.decodeHide {F : Type u_1} [Field F] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (a : RegisterHideAnswer F ι) : RegisterHideAnswer F ι

Equations

• MIPRE.Introspection.AuxiliaryQuotient.decodeHide P a = (a.1, (MIPRE.Introspection.AuxiliaryDual.decodeDual P a.1) a.2.1, a.2.2)

noncomputable def MIPRE.Introspection.AuxiliaryQuotient.decodeRead {F : Type u_1} [Field F] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {A : Type u_3} (P : CL.CLFun F ι ℓ) (a : (ι → F) × (ι → F) × A) : (ι → F) × (ι → F) × A

Equations

• MIPRE.Introspection.AuxiliaryQuotient.decodeRead P a = (a.1, (MIPRE.Introspection.AuxiliaryDual.decodeDual P a.1) a.2.1, a.2.2)

def MIPRE.Introspection.AuxiliaryQuotient.hidingNext {F : Type u_1} [Field F] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (u v : RegisterHideAnswer F ι) : Prop

Replace only the new dual block's representative by its quotient class.

Equations

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

theorem MIPRE.Introspection.AuxiliaryQuotient.hidingNext_of_legacy {F : Type u_1} [Field F] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (k : ℕ) (u v : RegisterHideAnswer F ι) (h : CLChecks.hidingNext P k u v) : hidingNext P k u v

theorem MIPRE.Introspection.AuxiliaryQuotient.hidingNext_sound {F : Type u_1} [Field F] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) {k : ℕ} (hk : k + 1 < ℓ) (u v : RegisterHideAnswer F ι) (h : hidingNext P k u v) : CLChecks.hidingNext P k (decodeHide P u) (decodeHide P v)

def MIPRE.Introspection.AuxiliaryQuotient.hidingPauli {F : Type u_1} [Field F] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (x : ι → F) (v : RegisterHideAnswer F ι) : Prop

The first hiding edge uses the same quotient relaxation.

Equations

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

theorem MIPRE.Introspection.AuxiliaryQuotient.hidingPauli_of_legacy {F : Type u_1} [Field F] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (x : ι → F) (v : RegisterHideAnswer F ι) (h : CLChecks.hidingPauli P x v) : hidingPauli P x v

theorem MIPRE.Introspection.AuxiliaryQuotient.hidingPauli_sound {F : Type u_1} [Field F] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (hℓ : 0 < ℓ) (x : ι → F) (v : RegisterHideAnswer F ι) (h : hidingPauli P x v) : CLChecks.hidingPauli P x (decodeHide P v)

theorem MIPRE.Introspection.AuxiliaryQuotient.hidingRead_sound {F : Type u_1} [Field F] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {A : Type u_3} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (u : RegisterHideAnswer F ι) (v : (ι → F) × (ι → F) × A) (h : CLChecks.hidingRead P u v) : CLChecks.hidingRead P (decodeHide P u) (decodeRead P v)

The final hiding/Read comparison survives the same decoding on both answers.