Documentation

MIPRE.Foundations.Introspection.AdaptiveAnswerDecode

Updating the full answer after an adaptive stage #

The decoder overwrites precisely the visited coordinates and retains the unvisited tail. Valid answers therefore report the new prefix even after mixing and dilation change their old coordinate label. The malformed outcome remains none; no assertion that its mass vanishes is used.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the recovered measurement is a POVM in any ordered ⋆-ring.

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

Overwrite the determined prefix while retaining the unvisited answer tail.

Equations
Instances For
    source
    theorem MIPRE.Introspection.advancePrefix_outputPrefix_fixed {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (k : ℕ) (y : ι → F) (hy : P.outputPrefix k y = y) (z : Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) :
    P.outputPrefix (k + 1) (advancePrefix P k y z) = advancePrefix P k y z

    Every fixed old prefix remains fixed after inserting arbitrary current coordinates; no membership in the linear map's image is required.

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

    A decoded valid answer reports the actual advanced prefix automatically.

    source
    theorem MIPRE.Introspection.stageAnswerDecode_recover_some {ι : 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] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (k : ℕ) (y x : ι → F) (a : A) (hy : P.outputPrefix k x = y) :
    stageAnswerDecode P k y (stageAnswerCoordinate P k y (some (x, a))) (some (x, a)) = some (x, a)

    On the old deterministic graph, decoding recovers the entire answer whenever its old prefix agrees with the branch.

    source
    theorem MIPRE.Introspection.stageAnswerDecode_recover {ι : 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] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (k : ℕ) (y : ι → F) (a : Option ((ι → F) × A)) (ha : ∀ (x : ι → F) (b : A), a = some (x, b) → P.outputPrefix k x = y) :
    stageAnswerDecode P k y (stageAnswerCoordinate P k y a) a = a

    Recovery includes the malformed outcome, with no hypothesis on its mass.

    source
    theorem MIPRE.Introspection.advancePrefix_coordinate_of_outputPrefix {ι : Type u_1} {F : Type u_2} [Fintype ι] [DecidableEq ι] [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (k : ℕ) (y x : ι → F) (hy : P.outputPrefix k x = y) :
    advancePrefix P k y ((coordinateRestrict (P.factorOfPrefix k y)) x) = P.outputPrefix (k + 1) x

    For a full answer with the correct old prefix, advancing by its actual selected coordinates gives precisely its reported next prefix.

    source
    theorem MIPRE.Introspection.stageAnswerDecode_next {ι : 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] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (k : ℕ) (y : ι → F) (z : Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) (a : Option ((ι → F) × A)) :
    stageAnswerDecode P k y z a = Option.map (fun (p : (ι → F) × A) => (advancePrefix P k y z + (CL.proj (stageRemaining P (k + 1) (advancePrefix P k y z))) p.1, p.2)) a

    Once the next prefix is named, the update depends only on that prefix and its remaining answer tail.

    source
    theorem MIPRE.Introspection.stageAnswerRefinementPOVM_decode_recover {ι : 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] {ℓ : ℕ} {R : Type u_4} [Ring R] [StarRing R] [PartialOrder R] [StarOrderedRing R] {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (k : ℕ) (y : ι → F) (M : POVMIn (Option ((ι → F) × A)) R) (hsupport : ∀ (x : ι → F) (a : A), P.outputPrefix k x ≠ y → M.op (some (x, a)) = 0) :
    POVMIn.map (fun (p : (Fin (Fintype.card ↥(P.factorOfPrefix k y)) → F) × Option ((ι → F) × A)) => stageAnswerDecode P k y p.1 p.2) (stageAnswerRefinementPOVM P k y M) = M

    The actual stage refinement followed by the updating decoder recovers the old residual measurement under its exact old-prefix support invariant. There is deliberately no vanishing hypothesis for the malformed effect.