Exact prefix/dual factorization at every adaptive CL stage

theorem MIPRE.Introspection.Honest.readout_split {I : Type u_1} {J : Type u_2} {K : Type u_3} {Y : Type u_4} {Y₁ : Type u_5} {Y₂ : Type u_6} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype K] [DecidableEq K] [Fintype Y] [DecidableEq Y] [Fintype Y₁] [DecidableEq Y₁] [Fintype Y₂] [DecidableEq Y₂] (e : I ≃ J × K) (f : I → Y) (g : J → Y₁) (r : K → Y₂) (y : Y) (y₁ : Y₁) (y₂ : Y₂) (hf : ∀ (x : I), f x = y ↔ g (e x).1 = y₁ ∧ r (e x).2 = y₂) : readout f y = registerOp e (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (readout g y₁) (readout r y₂))

theorem MIPRE.Introspection.Honest.readout_constant {I : Type u_1} {Y : Type u_4} [Fintype I] [DecidableEq I] [Fintype Y] [DecidableEq Y] (y₀ y : Y) : readout (fun (x : I) => y₀) y = if y₀ = y then 1 else 0

theorem MIPRE.Introspection.Honest.prefixReadout_cons_succ {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {S V : Finset ι} (L : CL.RegLinear F S) (next : (ι → F) → CL.CLFun F ι ℓ) (h : (CL.CLFun.cons S L next).SupportedOn V) (k : ℕ) (y : ι → F) : readout (fun (x : ↥V → F) => (CL.CLFun.truncate (k + 1) (CL.CLFun.cons S L next)).eval (insertRegister V x)) y = registerOp (coordinateSplit S V ⋯) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (Weyl.synOf Weyl.wZ (⇑(coordinateLinear L)) ((coordinateRestrict S) y)) (readout (fun (x : ↥(V \ S) → F) => (CL.CLFun.truncate k (next ((CL.proj S) y))).eval (insertRegister (V \ S) x)) ((CL.proj Sᶜ) y)))

theorem MIPRE.Introspection.Honest.dualRegister_factor {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (V : Finset ι) (h : P.SupportedOn V) (y yp : ι → F) : dualRegister P k V h (y, yp) = readout (fun (x : ↥V → F) => (CL.CLFun.truncate k P).eval (insertRegister V x)) y * Weyl.synOf Weyl.wX (fun (x : ↥V → F) => CLChecks.dualReadout P k y (insertRegister V x)) yp

The actual honest Hide marginal equals the preceding Z prefix multiplied by the current X-dual spectral readout. Earlier dual answers have been summed out in the proved adaptive recursion.

theorem MIPRE.Introspection.Honest.synX_univRestriction {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {Y : Type u_3} [Fintype Y] [DecidableEq Y] (f : (ι → F) → Y) (y : Y) : registerOp univRestriction (Weyl.synOf Weyl.wX (fun (x : ↥Finset.univ → F) => f (insertRegister Finset.univ x)) y) = Weyl.synOf Weyl.wX f y

theorem MIPRE.Introspection.Honest.readDualOp_factor {F : Type u_1} {ι : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (h : P.SupportedOn Finset.univ) (k : ℕ) (y yp : ι → F) : readDualOp P k h (some (y, yp)) = hidingPrefixOp P k (some y) * Weyl.synOf Weyl.wX (CLChecks.dualReadout P k y) yp

The source prefix/dual product is the existing honest Read dual marginal, not a separately stipulated family.

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

The current dual-X readout on exactly the unvisited register.

Equations

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

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

Full concrete tensor factorization under the prefix's own coordinate split, valid uniformly at every CL stage and every claimed prefix/dual label.