Coordinate transport of adaptive auxiliary registers

These identities transport the actual coordinate bijection, including on unattained claimed outputs. They do not identify canonical dual representatives.

theorem MIPRE.Introspection.CLChecks.map_compl {ι : Type u_2} {κ : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] (e : ι ≃ κ) (S : Finset ι) : Finset.map e.toEmbedding Sᶜ = (Finset.map e.toEmbedding S)ᶜ

theorem MIPRE.Introspection.CLChecks.outputPrefix_reindex {F : Type u_1} {ι : Type u_2} {κ : Type u_3} [Field F] [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] {ℓ : ℕ} (e : ι ≃ κ) (P : CL.CLFun F ι ℓ) (k : ℕ) (y : ι → F) : (CL.CLFun.reindex e P).outputPrefix k ((CL.reindexEquiv e) y) = (CL.reindexEquiv e) (P.outputPrefix k y)

theorem MIPRE.Introspection.CLChecks.prefixRegister_reindex {F : Type u_1} {ι : Type u_2} {κ : Type u_3} [Field F] [Fintype ι] [DecidableEq ι] [Fintype κ] [DecidableEq κ] {ℓ : ℕ} (e : ι ≃ κ) (P : CL.CLFun F ι ℓ) (k : ℕ) (y : ι → F) : prefixRegister (CL.CLFun.reindex e P) k ((CL.reindexEquiv e) y) = Finset.map e.toEmbedding (prefixRegister P k y)