The actual CL continuation on the unvisited registers

The residual presentation follows a claimed output, including an off-image one. It acts only on the complement of the registers already visited. The next local map and register are computed from the original presentation.

def MIPRE.Introspection.CLChecks.residualDepth : ℕ → ℕ → ℕ

Recursively compute the remaining depth, retaining definitional equations.

Equations

• MIPRE.Introspection.CLChecks.residualDepth 0 x✝ = x✝
• MIPRE.Introspection.CLChecks.residualDepth n.succ 0 = 0
• MIPRE.Introspection.CLChecks.residualDepth k.succ ℓ.succ = MIPRE.Introspection.CLChecks.residualDepth k ℓ

def MIPRE.Introspection.CLChecks.residual {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} : CL.CLFun F ι ℓ → (k : ℕ) → (ι → F) → CL.CLFun F ι (residualDepth k ℓ)

Continue after k reported components; the remaining depth is ℓ-k.

Equations

• MIPRE.Introspection.CLChecks.residual x✝¹ 0 x✝ = x✝¹
• MIPRE.Introspection.CLChecks.residual MIPRE.CL.CLFun.zero n.succ x✝ = MIPRE.CL.CLFun.zero
• MIPRE.Introspection.CLChecks.residual (MIPRE.CL.CLFun.cons S L₁ next) k.succ x✝ = MIPRE.Introspection.CLChecks.residual (next ((MIPRE.CL.proj S) x✝)) k ((MIPRE.CL.proj Sᶜ) x✝)

@[simp]

theorem MIPRE.Introspection.CLChecks.residual_zero {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (y : ι → F) : residual P 0 y = P

theorem MIPRE.Introspection.CLChecks.residual_supported {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (k : ℕ) (y : ι → F) : (residual P k y).SupportedOn (T \ prefixRegister P k y)

Every continuation acts only on the coordinates that have not been read.

theorem MIPRE.Introspection.CLChecks.residual_exactlyOn {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.ExactlyOn T) (k : ℕ) (hk : k ≤ ℓ) (y : ι → F) : (residual P k y).ExactlyOn (T \ prefixRegister P k y)

Exact partitioning also survives passing to a continuation.

theorem MIPRE.Introspection.CLChecks.residual_firstFactor {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (y : ι → F) : (residual P k y).factorOfPrefix 0 0 = P.factorOfPrefix k y

The first register of the continuation is the original next register.

def MIPRE.Introspection.CLChecks.stageLinear {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (y : ι → F) : CL.RegLinear F (P.factorOfPrefix k y)

The local linear map at a claimed prefix, with its actual finite-set support.

Equations

• MIPRE.Introspection.CLChecks.stageLinear MIPRE.CL.CLFun.zero x✝¹ x✝ = 0
• MIPRE.Introspection.CLChecks.stageLinear (MIPRE.CL.CLFun.cons S L next) 0 x✝ = L
• MIPRE.Introspection.CLChecks.stageLinear (MIPRE.CL.CLFun.cons S L₁ next) k.succ x✝ = MIPRE.Introspection.CLChecks.stageLinear (next ((MIPRE.CL.proj S) x✝)) k ((MIPRE.CL.proj Sᶜ) x✝)

theorem MIPRE.Introspection.CLChecks.stageLinear_toLinearMap {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (y : ι → F) : (stageLinear P k y).toLinearMap = P.mapOfPrefix k y

theorem MIPRE.Introspection.CLChecks.factorOfPrefix_subset_support {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (k : ℕ) (y : ι → F) : P.factorOfPrefix k y ⊆ T

theorem MIPRE.Introspection.CLChecks.stageFactor_subset_residual {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (k : ℕ) (y : ι → F) : P.factorOfPrefix k y ⊆ T \ prefixRegister P k y

This is the minimal residual support required by the product induction.

theorem MIPRE.Introspection.CLChecks.prefixRegister_step {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (y : ι → F) : prefixRegister P (k + 1) y = prefixRegister P k y ∪ P.factorOfPrefix k y

Passing one stage adds exactly its selected register to the prefix.

theorem MIPRE.Introspection.CLChecks.residualRegister_step {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (T : Finset ι) (k : ℕ) (y : ι → F) : (T \ prefixRegister P k y) \ P.factorOfPrefix k y = T \ prefixRegister P (k + 1) y

Mixing removes precisely the current factor, giving the next residual register.

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

Every next factor is determined by the already reported prefix.

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

Adding the selected next linear answer advances the actual sampler prefix.

theorem MIPRE.Introspection.CLChecks.coordinateRestrict_proj {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {U V : Finset ι} (hUV : U ⊆ V) (x : ι → F) : (coordinateRestrict U) ((CL.proj V) x) = (coordinateRestrict U) x

theorem MIPRE.Introspection.CLChecks.dualReadout_stageLinear {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (k : ℕ) (y x : ι → F) : dualReadout P k y x = (coordinateInsert (P.factorOfPrefix k y)) ((CL.lperp (coordinateLinear (stageLinear P k y))) ((coordinateRestrict (P.factorOfPrefix k y)) x))

The recursive dual answer is exactly the selected coordinate linear readout, transported back into the original register.