The actual adaptive computational readout

Reading a seed and retaining its CL prefix and selected next coordinates is exactly the prefix projector tensored with the next local Z measurement. The outcome type remembers the prefix, so the selected register can vary.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the readouts are register operators over ℂ, and their relabelling identities (registerOp_readout_fst, registerOp_readout_pair) are unchanged. They enter the first player's algebra Matrix I I 𝒜 as smulKron 1, so the factorizations through a register split (registerReadout_wZ) and through the prefix reinsertion prefixResidualOp (prefixResidualOp_readout, adaptiveZ_readout_factor) are identities of block matrices over any algebra 𝒜. The one step they share: X ⊗ (P ⊗ N), read along e : I ≃ J × R, is regSplitHom e applied to the block matrix (X ⊗ N) ⊗ P.

theorem MIPRE.Introspection.registerOp_readout_fst {I : Type u_1} {J : Type u_2} {R : Type u_3} {C : Type u_4} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype R] [DecidableEq R] [Fintype C] [DecidableEq C] (e : I ≃ J × R) (f : J → C) (c : C) : registerOp e (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (readout f c) 1) = readout (fun (i : I) => f (e i).1) c

theorem MIPRE.Introspection.registerOp_readout_pair {I : Type u_1} {J : Type u_2} {R : Type u_3} {C : Type u_4} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype R] [DecidableEq R] [Fintype C] [DecidableEq C] (e : I ≃ J × R) (f : J → C) (c : C) {D : Type u_5} [Fintype D] [DecidableEq D] (g : R → D) (d : D) : registerOp e (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (readout f c) (readout g d)) = readout (fun (i : I) => (f (e i).1, g (e i).2)) (c, d)

theorem MIPRE.Introspection.registerReadout_wZ {F : Type u_2} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {𝒜 : Type u_3} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] {I : Type u_4} {R : Type u_5} [Fintype I] [DecidableEq I] [Fintype R] [DecidableEq R] {n : ℕ} (e : I ≃ (Fin n → F) × R) (L : (Fin n → F) →ₗ[F] Fin n → F) (z : Fin n → F) : registerReadout e Weyl.wZ L z = smulKron 1 (readout (fun (i : I) => L (e i).1) z)

The Z readout of a linear map on the selected coordinates of a register is the readout of the map on those coordinates, as a register operator.

theorem MIPRE.Introspection.prefixResidualOp_readout {ι : 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) {C : Type u_4} [Fintype C] [DecidableEq C] (g : (↥(stageRemaining P k y) → F) → C) (z : C) : prefixResidualOp P k y (smulKron 1 (readout g z)) = smulKron 1 (readout (fun (x : ι → F) => ((CL.CLFun.truncate k P).eval x, g ((ambientSplit (CLChecks.prefixRegister P k y)) x).2)) (y, z))

A register readout reinserted behind its prefix projector is the joint readout of the prefix and of the residual label.

noncomputable def MIPRE.Introspection.adaptiveZOutcome {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] [Field F] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (x : ι → F) : (y : ι → F) × (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F)

The actual seed coarse-graining keeps the CL prefix and its selected next register.

Equations

• MIPRE.Introspection.adaptiveZOutcome P k x = ⟨(MIPRE.CL.CLFun.truncate k P).eval x, (MIPRE.Introspection.coordinateRestrict (P.factorOfPrefix k ((MIPRE.CL.CLFun.truncate k P).eval x))) x⟩

theorem MIPRE.Introspection.adaptiveZ_readout_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 (readout (adaptiveZOutcome P k) ⟨y, z⟩) = prefixResidualOp P k y (registerReadout (stageSplit P hP k y) Weyl.wZ LinearMap.id z)

Exact factorization of the actual adaptive Z readout, including zero-weight prefixes.