The honest dual marginal in the selected mixing coordinates #
Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the honest dual readout enters
the matrices over ι → F with entries in any algebra 𝒜 as smulKron 1 _, and the prefix
factorization is an identity there.
theorem
MIPRE.Introspection.aOp_registerOp_kron
{I : Type u_1}
{J : Type u_2}
{R : Type u_3}
{𝒜 : Type u_4}
[Fintype I]
[DecidableEq I]
[Fintype J]
[DecidableEq J]
[Fintype R]
[DecidableEq R]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
(e : I ≃ J × R)
(X : 𝒜)
(P : Matrix J J ℂ)
(N : Matrix R R ℂ)
:
smulKron X (registerOp e (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) P N)) = (regSplitHom e) (smulKron (smulKron X N) P)
A register operator P ⊗ N, read along e : I ≃ J × R and tensored with X, is the block
matrix (X ⊗ N) ⊗ P over J of block matrices over R, read along the split.
theorem
MIPRE.Introspection.synX_coordinateInsert
{ι : Type u_1}
{F : Type u_2}
[Fintype ι]
[DecidableEq ι]
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
{S : Finset ι}
(L : (Fin (Fintype.card ↥S) → F) →ₗ[F] Fin (Fintype.card ↥S) → F)
(z : Fin (Fintype.card ↥S) → F)
:
Weyl.synOf Weyl.wX (fun (x : Fin (Fintype.card ↥S) → F) => (coordinateInsert S) (L x)) ((coordinateInsert S) z) = Weyl.synOf Weyl.wX (⇑L) z
theorem
MIPRE.Introspection.residualDualOp_stage
{ι : 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)
:
Honest.residualDualOp P k y ((coordinateInsert (P.factorOfPrefix k y)) z) = registerOp (stageSplit P hP k y)
(Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2)
(Weyl.synOf Weyl.wX (⇑(CL.lperp (coordinateLinear (CLChecks.stageLinear P k y)))) z) 1)
The residual dual-X operator reads exactly the current stage's dual linear map and acts as identity on the next continuation.
theorem
MIPRE.Introspection.readDualOp_stage_factor
{ι : Type u_1}
{F : Type u_2}
[Fintype ι]
[DecidableEq ι]
[Field F]
[Fintype F]
[DecidableEq F]
[Algebra (ZMod 2) F]
{ℓ : ℕ}
{𝒜 : Type u_3}
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
(P : CL.CLFun F ι ℓ)
(hP : P.SupportedOn Finset.univ)
(k : ℕ)
(y : ι → F)
(z : Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F)
:
smulKron 1 (Honest.readDualOp P k hP (some (y, (coordinateInsert (P.factorOfPrefix k y)) z))) = prefixResidualOp P k y
(registerReadout (stageSplit P hP k y) Weyl.wX (CL.lperp (coordinateLinear (CLChecks.stageLinear P k y))) z)
The actual honest dual family, including any auxiliary factor, is exactly the prefix-conditioned current X-dual readout consumed by adaptive mixing.