Exact next-prefix factorization of the adaptive replacement

The old prefix and current Z projector combine into the actual next prefix projector. The remaining coordinates are transported by their proved set equality, with the same auxiliary space for every branch.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): a dilated residual operator is a block matrix over the ancilla of block matrices over the remaining coordinates, with entries in any algebra 𝒜, so the auxiliary system lives inside the algebra. The reassociation ((R → F) × H) × A ≃ (R → F) × (H × A), which moved the ancilla next to the auxiliary space, becomes the exchange of the two layers (BipartiteModel.layerSwap), which moves the ancilla inside, next to the algebra; the next residual operator (nextResidualOp) is this exchange relabelled along the set equality of the remaining coordinates, a unital ⋆-homomorphism along which projectivity is pushed forward. The entry formulas (prefixResidualOp_apply, adaptiveReplacementJointOp_apply) have their entries in the algebra, and the next-prefix factorization is proved entrywise, as before.

def MIPRE.Introspection.registerSetEquiv {ι : Type u_1} {F : Type u_2} {S T : Finset ι} (h : S = T) : (↥S → F) ≃ (↥T → F)

Transport an assignment between literally equal coordinate subsets.

Equations

• MIPRE.Introspection.registerSetEquiv h = { toFun := fun (x : ↥S → F) (i : ↥T) => x ⟨↑i, ⋯⟩, invFun := fun (x : ↥T → F) (i : ↥S) => x ⟨↑i, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

theorem MIPRE.Introspection.nextRemaining_eq {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (y : ι → F) (z : Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) : stageRemaining P (k + 1) (advancePrefix P k y z) = stageRemaining P k y \ P.factorOfPrefix k y

noncomputable def MIPRE.Introspection.nextResidualOp {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {ℓ : ℕ} {𝒜 : Type u_4} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] {T : Type u_5} [Fintype T] [DecidableEq T] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (y : ι → F) (z : Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) (N : Matrix T T (Matrix (↥(stageRemaining P k y \ P.factorOfPrefix k y) → F) (↥(stageRemaining P k y \ P.factorOfPrefix k y) → F) 𝒜)) : Matrix (↥(stageRemaining P (k + 1) (advancePrefix P k y z)) → F) (↥(stageRemaining P (k + 1) (advancePrefix P k y z)) → F) (Matrix T T 𝒜)

Pull the dilated remaining operator into the actual next-prefix carrier: the ancilla layer is moved inside (layerSwap), and the remaining coordinates are relabelled along their proved set equality.

Equations

• MIPRE.Introspection.nextResidualOp P hP k y z N = (MIPRE.submatrixHom (MIPRE.Introspection.registerSetEquiv ⋯)) (MIPRE.BipartiteModel.layerSwap N)

theorem MIPRE.Introspection.nextResidualOp_isPVM {ι : Type u_1} {F : Type u_2} {A : Type u_3} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {ℓ : ℕ} {𝒜 : Type u_4} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] {T : Type u_5} [Fintype T] [DecidableEq T] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (y : ι → F) (z : Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) (N : A → Matrix T T (Matrix (↥(stageRemaining P k y \ P.factorOfPrefix k y) → F) (↥(stageRemaining P k y \ P.factorOfPrefix k y) → F) 𝒜)) (hN : IsPVMIn N) : IsPVMIn (nextResidualOp P hP k y z ∘ N)

theorem MIPRE.Introspection.advancePrefix_fibre {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (y : ι → F) (hy : y ∈ prefixOutcomes P k) (z : Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) (x : ι → F) : (CL.CLFun.truncate (k + 1) P).eval x = advancePrefix P k y z ↔ adaptiveLinearOutcome P k x = ⟨y, z⟩

theorem MIPRE.Introspection.prefixResidualOp_apply {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {ℓ : ℕ} {𝒜 : Type u_4} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (y : ι → F) (M : Matrix (↥(stageRemaining P k y) → F) (↥(stageRemaining P k y) → F) 𝒜) (x x' : ι → F) : prefixResidualOp P k y M x x' = if (∀ i ∈ CLChecks.prefixRegister P k y, x i = x' i) ∧ (CL.CLFun.truncate k P).eval x = y then M (fun (i : ↥(stageRemaining P k y)) => x ↑i) fun (i : ↥(stageRemaining P k y)) => x' ↑i else 0

An entry of a reinserted residual operator: the entry of the residual operator on the remaining coordinates if the prefix coordinates agree and lie in the fibre of the prefix, and zero otherwise.

theorem MIPRE.Introspection.adaptiveLinearOutcome_eq_iff {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (y : ι → F) (z : Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) (x : ι → F) : adaptiveLinearOutcome P k x = ⟨y, z⟩ ↔ (CL.CLFun.truncate k P).eval x = y ∧ (coordinateLinear (CLChecks.stageLinear P k y)) ((coordinateRestrict (P.factorOfPrefix k y)) x) = z

theorem MIPRE.Introspection.coordinateRestrict_eq_iff {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] (S : Finset ι) (x x' : ι → F) : (coordinateRestrict S) x = (coordinateRestrict S) x' ↔ ∀ i ∈ S, x i = x' i

theorem MIPRE.Introspection.adaptiveReplacementJointOp_apply {ι : Type u_1} {F : Type u_2} {A : Type u_3} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {ℓ : ℕ} {𝒜 : Type u_4} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] {T : Type u_5} [Fintype T] [DecidableEq T] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (D : AdaptiveDilationFamily P k 𝒜 T A) (y : ι → F) (z : Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) (a : A) (x x' : ι → F) : adaptiveReplacementJointOp P hP k D ⟨y, (z, a)⟩ x x' = if ((∀ i ∈ CLChecks.prefixRegister P k y, x i = x' i) ∧ ∀ i ∈ P.factorOfPrefix k y, x i = x' i) ∧ (CL.CLFun.truncate k P).eval x = y ∧ (coordinateLinear (CLChecks.stageLinear P k y)) ((coordinateRestrict (P.factorOfPrefix k y)) x) = z then BipartiteModel.layerSwap (D y z a) (fun (i : ↥(stageRemaining P k y \ P.factorOfPrefix k y)) => x ↑i) fun (i : ↥(stageRemaining P k y \ P.factorOfPrefix k y)) => x' ↑i else 0

theorem MIPRE.Introspection.adaptiveReplacementJointOp_next_factor {ι : Type u_1} {F : Type u_2} {A : Type u_3} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype A] [DecidableEq A] {ℓ : ℕ} {𝒜 : Type u_4} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] {T : Type u_5} [Fintype T] [DecidableEq T] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (D : AdaptiveDilationFamily P k 𝒜 T A) (y : ι → F) (hy : y ∈ prefixOutcomes P k) (z : Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) (a : A) : adaptiveReplacementJointOp P hP k D ⟨y, (z, a)⟩ = prefixResidualOp P (k + 1) (advancePrefix P k y z) (nextResidualOp P hP k y z (D y z a))

Every attainable old-prefix block is exactly a next-prefix residual block. The current coordinate outcome may be outside the linear image; both sides then vanish, without imposing a support hypothesis on D.