Concrete tensor support of an adaptive CL prefix projector

A claimed prefix selects its used coordinates even outside the image of the CL map. Membership in its fibre depends only on those coordinates. The ideal prefix projector therefore acts as identity on their complement under the explicit coordinate restriction equivalence.

theorem MIPRE.Introspection.CLChecks.truncate_fibre_of_agree {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (k : ℕ) (y x x' : ι → F) (hag : ∀ i ∈ prefixRegister P k y, x i = x' i) (hx : (CL.CLFun.truncate k P).eval x = y) : (CL.CLFun.truncate k P).eval x' = y

Agreement on the registers selected by a claimed prefix preserves its fibre, without assuming that the claimed prefix is attainable.

theorem MIPRE.Introspection.CLChecks.truncate_fibre_congr {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (k : ℕ) (y x x' : ι → F) (hag : ∀ i ∈ prefixRegister P k y, x i = x' i) : (CL.CLFun.truncate k P).eval x = y ↔ (CL.CLFun.truncate k P).eval x' = y

theorem MIPRE.Introspection.CLChecks.truncate_fibre_proj {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) : (CL.CLFun.truncate k P).eval x = y ↔ (CL.CLFun.truncate k P).eval ((CL.proj (prefixRegister P k y)) x) = y

theorem MIPRE.Introspection.Honest.insertRegister_ambientSplit {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] (V : Finset ι) (x : ι → F) : insertRegister V ((ambientSplit V) x).1 = (CL.proj V) x

def MIPRE.Introspection.Honest.prefixProjector {F : Type u_1} {ι : Type u_2} [Field F] [DecidableEq F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (y : ι → F) : Matrix (↥(CLChecks.prefixRegister P k y) → F) (↥(CLChecks.prefixRegister P k y) → F) ℂ

The actual prefix projector on exactly the already used coordinates.

Equations

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

theorem MIPRE.Introspection.Honest.readout_ambientSplit {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] {Y : Type u_3} [Fintype Y] [DecidableEq Y] (V : Finset ι) (f : (ι → F) → Y) (g : (↥V → F) → Y) (y : Y) (hf : ∀ (x : ι → F), f x = y ↔ g ((ambientSplit V) x).1 = y) : readout f y = registerOp (ambientSplit V) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (readout g y) 1)

A general diagonal readout factorization under a concrete register split.

theorem MIPRE.Introspection.Honest.hidingPrefixOp_factor {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} [Algebra (ZMod 2) F] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (y : ι → F) : hidingPrefixOp P k (some y) = registerOp (ambientSplit (CLChecks.prefixRegister P k y)) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (prefixProjector P k y) 1)

The adaptive ideal prefix has no action on unused coordinates. This is an exact matrix identity for every claimed prefix, including empty fibres.