Advancing actual adaptive prefix labels

Adding the next selected-coordinate answer preserves the preceding claimed prefix and the next remaining register. For attainable old prefixes, the old label and the new coordinate answer are both recovered exactly. The actual next sampler output is the advance by its selected linear readout.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the last two identities are between the register operators embedded, as smulKron 1 _, in the matrices over any algebra 𝒜, the first player's algebra of a register model; coarse-graining is fibSumIn.

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

Add a current-coordinate answer to the preceding ambient prefix label.

Equations

• MIPRE.Introspection.advancePrefix P k y z = y + (MIPRE.Introspection.coordinateInsert (P.factorOfPrefix k y)) z

theorem MIPRE.Introspection.CLChecks.outputPrefix_eq_of_agree {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (y x : ι → F) (hag : ∀ i ∈ prefixRegister P k y, x i = y i) : P.outputPrefix k x = P.outputPrefix k y

Reading the claimed prefix only uses its selected prefix coordinates.

theorem MIPRE.Introspection.advancePrefix_old_prefix {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (k : ℕ) (y : ι → F) (z : Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) : P.outputPrefix k (advancePrefix P k y z) = P.outputPrefix k y

theorem MIPRE.Introspection.advancePrefix_register {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (k : ℕ) (y : ι → F) (z : Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) : CLChecks.prefixRegister P (k + 1) (advancePrefix P k y z) = CLChecks.prefixRegister P (k + 1) y

The next support depends on the old prefix, and is unchanged by inserting an arbitrary answer on the current selected factor.

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

theorem MIPRE.Introspection.advancePrefix_eval {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (k : ℕ) (x : ι → F) : advancePrefix P k ((CL.CLFun.truncate k P).eval x) ((coordinateLinear (CLChecks.stageLinear P k ((CL.CLFun.truncate k P).eval x))) ((coordinateRestrict (P.factorOfPrefix k ((CL.CLFun.truncate k P).eval x))) x)) = (CL.CLFun.truncate (k + 1) P).eval x

The actual next sampler output is the advanced old label and selected linear result in its concrete finite coordinate presentation.

theorem MIPRE.Introspection.outputPrefix_of_mem_prefixOutcomes {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} [Fintype F] [DecidableEq F] {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (k : ℕ) (y : ι → F) (hy : y ∈ prefixOutcomes P k) : P.outputPrefix k y = y

theorem MIPRE.Introspection.advancePrefix_recover_prefix {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} [Fintype F] [DecidableEq F] {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (k : ℕ) (y : ι → F) (hy : y ∈ prefixOutcomes P k) (z : Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) : P.outputPrefix k (advancePrefix P k y z) = y

theorem MIPRE.Introspection.coordinateRestrict_old_prefix {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} [Fintype F] [DecidableEq F] {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (k : ℕ) (y : ι → F) (hy : y ∈ prefixOutcomes P k) : (coordinateRestrict (P.factorOfPrefix k y)) y = 0

theorem MIPRE.Introspection.advancePrefix_recover_coordinate {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} [Fintype F] [DecidableEq F] {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (k : ℕ) (y : ι → F) (hy : y ∈ prefixOutcomes P k) (z : Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) : (coordinateRestrict (P.factorOfPrefix k y)) (advancePrefix P k y z) = z

theorem MIPRE.Introspection.advancePrefix_injective {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} [Fintype F] [DecidableEq F] {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (k : ℕ) : Function.Injective fun (p : (y : ↥(prefixOutcomes P k)) × (Fin (Fintype.card ↥(P.factorOfPrefix k ↑y)) → F)) => advancePrefix P k (↑p.fst) p.snd

On attainable old prefixes the advanced label uniquely determines both the preceding prefix and the new selected-coordinate answer.

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

The old sampled prefix together with the next selected linear outcome.

Equations

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

theorem MIPRE.Introspection.advancePrefix_adaptiveLinearOutcome {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} [Fintype F] [DecidableEq F] {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (k : ℕ) (x : ι → F) : advancePrefix P k (adaptiveLinearOutcome P k x).fst (adaptiveLinearOutcome P k x).snd = (CL.CLFun.truncate (k + 1) P).eval x

theorem MIPRE.Introspection.advancePrefix_readout {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} [Fintype F] [DecidableEq F] {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (k : ℕ) (v : ι → F) : readout (CL.CLFun.truncate (k + 1) P).eval v = fibSum (readout (adaptiveLinearOutcome P k)) (fun (p : (y : ι → F) × (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F)) => advancePrefix P k p.fst p.snd) v

The next prefix readout is exactly the coarse-graining of the old prefix and current linear readout under the concrete next-label map.

theorem MIPRE.Introspection.adaptiveLinear_readout_factor {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} [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 (adaptiveLinearOutcome P k) ⟨y, z⟩) = prefixResidualOp P k y (registerReadout (stageSplit P hP k y) Weyl.wZ (coordinateLinear (CLChecks.stageLinear P k y)) z)

The actual selected linear outcome factors into the old prefix projector and the local current-stage spectral readout.

theorem MIPRE.Introspection.advancePrefix_projector_assembly {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {𝒜 : Type u_3} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] (P : CL.CLFun F ι ℓ) (hP : P.SupportedOn Finset.univ) (k : ℕ) (v : ι → F) : smulKron 1 (Honest.hidingPrefixOp P (k + 1) (some v)) = fibSumIn (fun (p : (y : ι → F) × (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F)) => prefixResidualOp P k p.fst (registerReadout (stageSplit P hP k p.fst) Weyl.wZ (coordinateLinear (CLChecks.stageLinear P k p.fst)) p.snd)) (fun (p : (y : ι → F) × (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F)) => advancePrefix P k p.fst p.snd) v

Reassembling old-prefix/current-linear projectors by the advanced label gives exactly the next honest prefix measurement.