Queries for source padding at unchanged depth

The extra zero register is consumed at the first factor. Linear queries are the original queries extended by zero; subsequent factor queries have no extra coordinates. These equations hold for arbitrary prefixes.

theorem MIPRE.Introspection.SourcePadding.pull_proj_union_compl {F : Type u_1} {I : Type u_2} {J : Type u_3} [Field F] [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] (e : I ↪ J) (S : Finset I) (O : Finset J) (hO : Disjoint (Finset.map e Finset.univ) O) (x : J → F) : CL.pull e ((CL.proj (Finset.map e S ∪ O)ᶜ) x) = (CL.proj Sᶜ) (CL.pull e x)

theorem MIPRE.Introspection.SourcePadding.eval_truncate_embed_zeroOn {F : Type u_1} {I : Type u_2} {J : Type u_3} [Field F] [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] (e : I ↪ J) {ℓ : ℕ} (P : CL.CLFun F I ℓ) (O : Finset J) (hO : Disjoint (Finset.map e Finset.univ) O) (j : ℕ) (x : J → F) : (CL.CLFun.truncate j ((CL.CLFun.embed e P).directSum (CL.CLFun.zeroOn O ℓ))).eval x = CL.push e ((CL.CLFun.truncate j P).eval (CL.pull e x))

Every padded marginal is the original marginal extended by zero.

theorem MIPRE.Introspection.SourcePadding.depthFamily_eval_truncate {F : Type u_1} {I : Type u_2} {J : Type u_3} [Field F] [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] {ℓ : ℕ} (e : I ↪ J) (L : Bool → CL.CLFun F I ℓ) (w : Bool) (j : ℕ) (x : J → F) : (CL.CLFun.truncate j (depthFamily e L w)).eval x = CL.push e ((CL.CLFun.truncate j (L w)).eval (CL.pull e x))

theorem MIPRE.Introspection.SourcePadding.pull_attained_prefix {F : Type u_1} {I : Type u_2} {J : Type u_3} [Field F] [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] {ℓ : ℕ} (e : I ↪ J) (L : Bool → CL.CLFun F I ℓ) (w : Bool) (j : ℕ) (u : J → F) (hu : ∃ (x : J → F), u = (CL.CLFun.truncate j (depthFamily e L w)).eval x) : ∃ (x : I → F), CL.pull e u = (CL.CLFun.truncate j (L w)).eval x

theorem MIPRE.Introspection.SourcePadding.mapOfPrefix_embed_zeroOn {F : Type u_1} {I : Type u_2} {J : Type u_3} [Field F] [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] (e : I ↪ J) {ℓ : ℕ} (P : CL.CLFun F I ℓ) (O : Finset J) (hO : Disjoint (Finset.map e Finset.univ) O) (j : ℕ) (u y : J → F) : (((CL.CLFun.embed e P).directSum (CL.CLFun.zeroOn O ℓ)).mapOfPrefix j u) y = CL.push e ((P.mapOfPrefix j (CL.pull e u)) (CL.pull e y))

Zero padding does not change any source linear map query.

theorem MIPRE.Introspection.SourcePadding.factorOfPrefix_embed_zeroOn {F : Type u_1} {I : Type u_2} {J : Type u_3} [Field F] [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] (e : I ↪ J) {ℓ : ℕ} (P : CL.CLFun F I ℓ) (O : Finset J) (hO : Disjoint (Finset.map e Finset.univ) O) (j : ℕ) (u : J → F) : ((CL.CLFun.embed e P).directSum (CL.CLFun.zeroOn O ℓ)).factorOfPrefix j u = Finset.map e (P.factorOfPrefix j (CL.pull e u)) ∪ if ℓ = 0 ∨ j ≠ 0 then ∅ else O

Only the first source factor also consumes the unused coordinates.

theorem MIPRE.Introspection.SourcePadding.depthFamily_mapOfPrefix {F : Type u_1} {I : Type u_2} {J : Type u_3} [Field F] [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] {ℓ : ℕ} (e : I ↪ J) (L : Bool → CL.CLFun F I ℓ) (w : Bool) (j : ℕ) (u y : J → F) : ((depthFamily e L w).mapOfPrefix j u) y = CL.push e (((L w).mapOfPrefix j (CL.pull e u)) (CL.pull e y))

theorem MIPRE.Introspection.SourcePadding.depthFamily_factorOfPrefix {F : Type u_1} {I : Type u_2} {J : Type u_3} [Field F] [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] {ℓ : ℕ} (e : I ↪ J) (L : Bool → CL.CLFun F I ℓ) (hℓ : 0 < ℓ) (w : Bool) (j : ℕ) (u : J → F) : (depthFamily e L w).factorOfPrefix j u = Finset.map e ((L w).factorOfPrefix j (CL.pull e u)) ∪ if j = 0 then (Finset.map e Finset.univ)ᶜ else ∅