Bit-list query formulas for the numbered detyping sampler

These identities connect the semantic CL construction to the executable router's graph-prefix and content-suffix operations. Prefix validity for forwarded content queries is derived from the original numbered prefix.

theorem MIPRE.CL.Detyping.toBits_zero (s : ℕ) : toBits 0 = List.replicate s false

theorem MIPRE.CL.Detyping.graphBits_zero {T : Type u_1} [Fintype T] [DecidableEq T] : graphBits 0 = List.replicate (graphDim T) false

theorem MIPRE.CL.Detyping.graph_part_ofBits {T : Type u_1} [Fintype T] [DecidableEq T] {s : ℕ} (z : Cost.BitStr) (hz : List.length z = graphDim T + s) : pull Function.Embedding.inl (pull (registerEquiv s).toEmbedding (ofBits (graphDim T + s) z)) = graphOfBits (List.take (graphDim T) z)

theorem MIPRE.CL.Detyping.content_part_ofBits {T : Type u_1} [Fintype T] [DecidableEq T] {s : ℕ} (z : Cost.BitStr) (hz : List.length z = graphDim T + s) : pull Function.Embedding.inr (pull (registerEquiv s).toEmbedding (ofBits (graphDim T + s) z)) = ofBits s (List.drop (graphDim T) z)

theorem MIPRE.CL.Detyping.toBits_register_graph {T : Type u_1} [Fintype T] [DecidableEq T] (s : ℕ) (g : Graph.Coord T → 𝔽₂) : toBits (push (registerEquiv s).toEmbedding (push Function.Embedding.inl g)) = graphBits g ++ List.replicate s false

theorem MIPRE.CL.Detyping.toBits_register_content {T : Type u_1} [Fintype T] [DecidableEq T] (s : ℕ) (v : Fin s → 𝔽₂) : toBits (push (registerEquiv s).toEmbedding (push Function.Embedding.inr v)) = List.replicate (graphDim T) false ++ toBits v

theorem MIPRE.CL.Detyping.numbered_marginal_graph {T : Type u_1} [Fintype T] [DecidableEq T] {s ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (w : Player) (P : T → CLFun 𝔽₂ (Fin s) ℓ) (j : ℕ) (hj : j ≤ 2) (z : Cost.BitStr) (hz : List.length z = graphDim T + s) : toBits ((CLFun.truncate j (numbered E w P)).eval (ofBits (graphDim T + s) z)) = graphBits ((CLFun.truncate j (Graph.presentation E w.toBool)).eval (graphOfBits (List.take (graphDim T) z))) ++ List.replicate s false

Through the first two levels only graph bits are nonzero.

theorem MIPRE.CL.Detyping.numbered_marginal_content {T : Type u_1} [Fintype T] [DecidableEq T] {s ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (w : Player) (P : T → CLFun 𝔽₂ (Fin s) ℓ) (hP : ∀ (t : T), (P t).ExactlyOn Finset.univ) (hℓ : 0 < ℓ) (r : ℕ) (z : Cost.BitStr) (hz : List.length z = graphDim T + s) : toBits ((CLFun.truncate (r + 2) (numbered E w P)).eval (ofBits (graphDim T + s) z)) = graphBits ((Graph.presentation E w.toBool).eval (graphOfBits (List.take (graphDim T) z))) ++ toBits ((CLFun.truncate r (selected P (select E w.toBool (graphOfBits (List.take (graphDim T) z))))).eval (ofBits s (List.drop (graphDim T) z)))

Later marginals append the selected typed marginal to the complete graph view.

theorem MIPRE.CL.Detyping.numbered_linear_graph {T : Type u_1} [Fintype T] [DecidableEq T] {s ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (w : Player) (P : T → CLFun 𝔽₂ (Fin s) ℓ) (k : ℕ) (hk : k < 2) (u y : Cost.BitStr) (hu : List.length u = graphDim T + s) (hy : List.length y = graphDim T + s) : toBits (((numbered E w P).mapOfPrefix k (ofBits (graphDim T + s) u)) (ofBits (graphDim T + s) y)) = graphBits (((Graph.presentation E w.toBool).mapOfPrefix k (graphOfBits (List.take (graphDim T) u))) (graphOfBits (List.take (graphDim T) y))) ++ List.replicate s false

Graph-level linear queries append a zero content block.

theorem MIPRE.CL.Detyping.numbered_linear_content {T : Type u_1} [Fintype T] [DecidableEq T] {s ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (w : Player) (P : T → CLFun 𝔽₂ (Fin s) ℓ) (r : ℕ) (u y : Cost.BitStr) (hu : List.length u = graphDim T + s) (hy : List.length y = graphDim T + s) : toBits (((numbered E w P).mapOfPrefix (r + 2) (ofBits (graphDim T + s) u)) (ofBits (graphDim T + s) y)) = List.replicate (graphDim T) false ++ toBits (((selected P (select E w.toBool (graphOfBits (List.take (graphDim T) u)))).mapOfPrefix r (ofBits s (List.drop (graphDim T) u))) (ofBits s (List.drop (graphDim T) y)))

Content-level linear queries prepend a zero graph block.

def MIPRE.CL.Detyping.indicatorVec {ι : Type u_2} [DecidableEq ι] (S : Finset ι) : ι → 𝔽₂

Equations

• MIPRE.CL.Detyping.indicatorVec S i = if i ∈ S then 1 else 0

theorem MIPRE.CL.Detyping.toBits_indicator_equiv {ι : Type u_2} [DecidableEq ι] {s : ℕ} (e : ι ≃ Fin s) (S : Finset ι) : toBits (push e.toEmbedding (indicatorVec S)) = indicatorBits (Finset.map e.toEmbedding S)

theorem MIPRE.CL.Detyping.indicatorBits_register_graph {T : Type u_1} [Fintype T] [DecidableEq T] {s : ℕ} (S : Finset (Graph.Coord T)) : indicatorBits (Finset.map (registerEquiv s).toEmbedding (Finset.map Function.Embedding.inl S)) = indicatorBits (Finset.map graphEquiv.toEmbedding S) ++ List.replicate s false

theorem MIPRE.CL.Detyping.indicatorBits_register_content {T : Type u_1} [Fintype T] [DecidableEq T] {s : ℕ} (S : Finset (Fin s)) : indicatorBits (Finset.map (registerEquiv s).toEmbedding (Finset.map Function.Embedding.inr S)) = List.replicate (graphDim T) false ++ indicatorBits S

theorem MIPRE.CL.Detyping.numbered_factor_graph {T : Type u_1} [Fintype T] [DecidableEq T] {s ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (w : Player) (P : T → CLFun 𝔽₂ (Fin s) ℓ) (k : ℕ) (hk : k < 2) (u : Cost.BitStr) (hu : List.length u = graphDim T + s) : indicatorBits ((numbered E w P).factorOfPrefix k (ofBits (graphDim T + s) u)) = indicatorBits (Finset.map graphEquiv.toEmbedding ((Graph.presentation E w.toBool).factorOfPrefix k (graphOfBits (List.take (graphDim T) u)))) ++ List.replicate s false

Graph factors append zero membership bits for the content register.

theorem MIPRE.CL.Detyping.numbered_factor_content {T : Type u_1} [Fintype T] [DecidableEq T] {s ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (w : Player) (P : T → CLFun 𝔽₂ (Fin s) ℓ) (r : ℕ) (u : Cost.BitStr) (hu : List.length u = graphDim T + s) : indicatorBits ((numbered E w P).factorOfPrefix (r + 2) (ofBits (graphDim T + s) u)) = List.replicate (graphDim T) false ++ indicatorBits ((selected P (select E w.toBool (graphOfBits (List.take (graphDim T) u)))).factorOfPrefix r (ofBits s (List.drop (graphDim T) u)))

Content factors prepend zero membership bits for the graph register.

theorem MIPRE.CL.Detyping.take_graph_append {T : Type u_1} [Fintype T] [DecidableEq T] (g : Graph.Coord T → 𝔽₂) (v : Cost.BitStr) : List.take (graphDim T) (graphBits g ++ v) = graphBits g

theorem MIPRE.CL.Detyping.drop_graph_append {T : Type u_1} [Fintype T] [DecidableEq T] (g : Graph.Coord T → 𝔽₂) (v : Cost.BitStr) : List.drop (graphDim T) (graphBits g ++ v) = v

theorem MIPRE.CL.Detyping.numbered_selected_prefix {T : Type u_1} [Fintype T] [DecidableEq T] {s ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (w : Player) (P : T → CLFun 𝔽₂ (Fin s) ℓ) (hP : ∀ (t : T), (P t).ExactlyOn Finset.univ) (hℓ : 0 < ℓ) (r : ℕ) (hr : 1 ≤ r) (u : Cost.BitStr) (hu : ∃ (x : Fin (graphDim T + s) → 𝔽₂), u = toBits ((CLFun.truncate (r + 1) (numbered E w P)).eval x)) {t : T} (ht : select E w.toBool (graphOfBits (List.take (graphDim T) u)) = some t) : ∃ (v : Fin s → 𝔽₂), List.drop (graphDim T) u = toBits ((CLFun.truncate (r - 1) (P t)).eval v)

A selected type receives a prefix that is valid for the original typed sampler.