Detyped conditionally linear functions

The construction of types.tex, def:detyped-CL: run the graph sampler, then the selected typed presentation on an independent register. An invalid graph view selects a zero presentation that still consumes the whole content register. The conditional law retains the common content seed of both players.

This file constructs the presentations and proves their law. The ambient program and its runtime are the separate lem:detype-sampler obligation.

def MIPRE.CL.CLFun.zeroOn {F : Type u_1} {ι : Type u_2} [Semiring F] [DecidableEq ι] (S : Finset ι) (ℓ : ℕ) : CLFun F ι ℓ

A zero presentation whose first factor consumes S, with empty later factors.

Equations

• MIPRE.CL.CLFun.zeroOn S 0 = MIPRE.CL.CLFun.zero
• MIPRE.CL.CLFun.zeroOn S ℓ.succ = MIPRE.CL.CLFun.cons S 0 fun (x : ι → F) => MIPRE.CL.CLFun.zeroOn ∅ ℓ

theorem MIPRE.CL.CLFun.zeroOn_exactlyOn {F : Type u_1} {ι : Type u_2} [Semiring F] [DecidableEq ι] (S : Finset ι) (ℓ : ℕ) (h : ℓ = 0 → S = ∅) : (zeroOn S ℓ).ExactlyOn S

The zero fallback still partitions all registers when at least one level is available.

theorem MIPRE.CL.CLFun.eval_truncate_zeroOn {F : Type u_1} {ι : Type u_2} [Semiring F] [DecidableEq ι] [Fintype ι] (S : Finset ι) (ℓ j : ℕ) (x : ι → F) : (truncate j (zeroOn S ℓ)).eval x = 0

Every marginal of the fallback returns zero.

@[simp]

theorem MIPRE.CL.CLFun.eval_zeroOn {F : Type u_1} {ι : Type u_2} [Semiring F] [DecidableEq ι] [Fintype ι] (S : Finset ι) (ℓ : ℕ) (x : ι → F) : (zeroOn S ℓ).eval x = 0

theorem MIPRE.CL.CLFun.mapOfPrefix_zeroOn {F : Type u_1} {ι : Type u_2} [Semiring F] [DecidableEq ι] [Fintype ι] (S : Finset ι) (ℓ j : ℕ) (x : ι → F) : (zeroOn S ℓ).mapOfPrefix j x = 0

Fallback linear queries are zero for all prefixes and levels.

theorem MIPRE.CL.CLFun.factorOfPrefix_zeroOn {F : Type u_1} {ι : Type u_2} [Semiring F] [DecidableEq ι] [Fintype ι] (S : Finset ι) (ℓ j : ℕ) (x : ι → F) : (zeroOn S ℓ).factorOfPrefix j x = if ℓ = 0 ∨ j ≠ 0 then ∅ else S

Only the first fallback level has a nonempty factor.

@[reducible, inline]

abbrev MIPRE.CL.Detyping.Coord (T : Type u_3) (ι : Type u_4) : Type (max u_3 u_4)

The graph register followed by the content register.

Equations

• MIPRE.CL.Detyping.Coord T ι = (MIPRE.CL.Graph.Coord T ⊕ ι)

noncomputable def MIPRE.CL.Detyping.select {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (w : Bool) (g : Graph.Coord T → ZMod 2) : Option T

A graph view selects its decoded vertex exactly when its opposite neighbor bit is one. On graph-sampler outputs this is the paper's nonzero opposite-block test.

Equations

• MIPRE.CL.Detyping.select E w g = match MIPRE.CL.Graph.decode E fun (p : Bool × T) => g (w, p) with | some u => if g (!w, true, u) = 1 then some u else none | none => none

theorem MIPRE.CL.Detyping.select_eq_some_iff {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (w : Bool) (g : Graph.Coord T → ZMod 2) (u : T) : select E w g = some u ↔ (fun (p : Bool × T) => g (w, p)) = Graph.encode E u ∧ g (!w, true, u) = 1

The exact specification of successful type selection.

theorem MIPRE.CL.Detyping.select_output {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (w : Bool) (g : Graph.Coord T → ZMod 2) : select E w ((Graph.presentation E w).eval g) = select E w g

Type selection is unchanged by passing from a seed to the sampled graph view.

theorem MIPRE.CL.Detyping.select_eq_none_iff {T : Type u_1} [Fintype T] [DecidableEq T] (E : T → T → Prop) [DecidableRel E] (w : Bool) (g : Graph.Coord T → ZMod 2) : select E w g = none ↔ ¬Graph.localValid E w g

Selection fails exactly on locally invalid seeds.

def MIPRE.CL.Detyping.selected {T : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : T → CLFun (ZMod 2) ι ℓ) (u : Option T) : CLFun (ZMod 2) ι ℓ

The selected content presentation, with a register-consuming zero fallback.

Equations

• MIPRE.CL.Detyping.selected P (some u_1) = P u_1
• MIPRE.CL.Detyping.selected P none = MIPRE.CL.CLFun.zeroOn Finset.univ ℓ

noncomputable def MIPRE.CL.Detyping.presentation {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (w : Bool) (P : T → CLFun (ZMod 2) ι ℓ) : CLFun (ZMod 2) (Coord T ι) (ℓ + 2)

The detyped presentation has the two graph levels followed by the typed levels.

Equations

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

theorem MIPRE.CL.Detyping.disjoint_registers {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] : Disjoint (Finset.map Function.Embedding.inl Finset.univ) (Finset.map Function.Embedding.inr Finset.univ)

The graph and content registers are disjoint.

theorem MIPRE.CL.Detyping.union_registers {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] : Finset.map Function.Embedding.inl Finset.univ ∪ Finset.map Function.Embedding.inr Finset.univ = Finset.univ

The graph and content registers exhaust the ambient space.

theorem MIPRE.CL.Detyping.presentation_exactlyOn {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (w : Bool) (P : T → CLFun (ZMod 2) ι ℓ) (hP : ∀ (t : T), (P t).ExactlyOn Finset.univ) (hℓ : 0 < ℓ) : (presentation E w P).ExactlyOn Finset.univ

The full detyped sampler partitions its registers on every branch, including rejection.

theorem MIPRE.CL.Detyping.presentation_eval {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (E : T → T → Prop) [DecidableRel E] (w : Bool) (P : T → CLFun (ZMod 2) ι ℓ) (hP : ∀ (t : T), (P t).ExactlyOn Finset.univ) (hℓ : 0 < ℓ) (x : Coord T ι → ZMod 2) : (presentation E w P).eval x = Sum.elim ((Graph.presentation E w).eval (pull Function.Embedding.inl x)) ((selected P (select E w (pull Function.Embedding.inl x))).eval (pull Function.Embedding.inr x))

The output consists of the sampled graph view and exactly the selected typed output.

theorem MIPRE.CL.Detyping.card_coord {T : Type u_1} {ι : Type u_2} [Fintype T] [DecidableEq T] [Fintype ι] [DecidableEq ι] : Fintype.card (Coord T ι) = 4 * Fintype.card T + Fintype.card ι

The ambient dimension is exactly the graph dimension plus the content dimension.