Reading prefixes from arbitrary claimed CL outputs

The sampling test coarse-grains the entire answer alphabet, not merely the image of the CL map. The prefix map therefore follows the claimed output's coordinate branches and does not apply the stage linear maps again.

def MIPRE.CL.CLFun.outputPrefix {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} : CLFun F ι ℓ → ℕ → (ι → F) → ι → F

Extract the first k register components from any claimed output.

Equations

• x✝¹.outputPrefix 0 x✝ = 0
• MIPRE.CL.CLFun.zero.outputPrefix n.succ x✝ = 0
• (MIPRE.CL.CLFun.cons S L₁ next).outputPrefix k.succ x✝ = (MIPRE.CL.proj S) x✝ + (next ((MIPRE.CL.proj S) x✝)).outputPrefix k ((MIPRE.CL.proj Sᶜ) x✝)

@[simp]

theorem MIPRE.CL.CLFun.outputPrefix_zero {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CLFun F ι ℓ) (y : ι → F) : P.outputPrefix 0 y = 0

@[simp]

theorem MIPRE.CL.CLFun.outputPrefix_cons {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (S : Finset ι) (L : RegLinear F S) (next : (ι → F) → CLFun F ι ℓ) (k : ℕ) (y : ι → F) : (cons S L next).outputPrefix (k + 1) y = (proj S) y + (next ((proj S) y)).outputPrefix k ((proj Sᶜ) y)

theorem MIPRE.CL.CLFun.SupportedOn.proj_eval_cons {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {S T : Finset ι} {L : RegLinear F S} {next : (ι → F) → CLFun F ι ℓ} (hP : (cons S L next).SupportedOn T) (z : ι → F) : (proj S) ((cons S L next).eval z) = L z ∧ (proj Sᶜ) ((cons S L next).eval z) = (next (L z)).eval ((proj Sᶜ) z)

An honest output's first register and remainder recover the two construction branches.

theorem MIPRE.CL.CLFun.SupportedOn.outputPrefix_eval {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (k : ℕ) (z : ι → F) : P.outputPrefix k (P.eval z) = (CLFun.truncate k P).eval z

The sampling check can compute the honest marginal from the complete claimed output.

theorem MIPRE.CL.CLFun.ExactlyOn.outputPrefix_self {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CLFun F ι ℓ} {T : Finset ι} (hP : P.ExactlyOn T) (y : ι → F) : P.outputPrefix ℓ ((proj T) y) = (proj T) y

No image-membership condition is used to compute prefixes of claimed answers.

theorem MIPRE.CL.CLFun.ExactlyOn.outputPrefix_univ {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CLFun F ι ℓ} (hP : P.ExactlyOn Finset.univ) (y : ι → F) : P.outputPrefix ℓ y = y

For a full CL presentation, the full claimed prefix is every answer vector.