The information retained by a hiding prefix

These identities hold for arbitrary claimed outputs. They justify processing the next hiding test from the preceding coarse outcome, without assuming that an answer belongs to the image of the CL map.

theorem MIPRE.Introspection.CLChecks.prefixRegister_mono {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (y : ι → F) {k m : ℕ} (hkm : k ≤ m) : prefixRegister P k y ⊆ prefixRegister P m y

Longer claimed prefixes retain all the registers of shorter prefixes.

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

Taking a shorter prefix of a claimed prefix does not change it.

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

Equal preceding prefixes choose the same next register, including on answers outside the image of the sampler.

theorem MIPRE.Introspection.CLChecks.dualReadout_congr {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (k : ℕ) (y : ι → F) {x t : ι → F} (h : ∀ i ∈ T, x i = t i) : dualReadout P k y x = dualReadout P k y t

A dual readout only uses coordinates in the presentation's support.

theorem MIPRE.Introspection.CLChecks.dualReadout_proj_compl_prefix {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (k : ℕ) (y x : ι → F) : dualReadout P k y ((CL.proj (prefixRegister P k y)ᶜ) x) = dualReadout P k y x

The next dual readout can be computed from the tail retained by the previous hiding measurement.

theorem MIPRE.Introspection.CLChecks.tail_proj_tail {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (y x : ι → F) {k m : ℕ} (hkm : k ≤ m) : (CL.proj (prefixRegister P m y)ᶜ) ((CL.proj (prefixRegister P k y)ᶜ) x) = (CL.proj (prefixRegister P m y)ᶜ) x

Removing an earlier prefix does not change any later tail.