The low-degree half of the answer-reduced sampler, directly answered

Slice P4h of planning/aldous-lyons-track.md: the seeded low-degree test's presentation on the registers regs j (F_q^{D}, D = 2M + 1: the point, the direction, one seed), downsized along the Shoup basis and numbered coordinate by coordinate (ldCl), as a sampler answered by a polynomial-time function of its parameters (CL.DirectSampler), the right factor of the answer-reduced typed sampler (TypedSampler.prodDirect).

The bits of a vector are its coordinates' Shoup bits, t per coordinate (toBits_ld): three runs of t-bit blocks, M point blocks, M direction blocks and one seed block (blocks1_ldBitsV). The MIP* answer reduction answers one copy of the test on such runs (AnswerReduction.StageProg, with six seed blocks there): its run functions margL, linL, facL and their programs are reused unchanged on the one-copy layout, at offset 0 and length M (ldDesc), with a split into M + M + 1 blocks (blocks1). What a query returns, run by run, is comps1_marginal and comps1_map_*; ldAnswer_marginal, ldAnswer_linear and ldAnswer_factor are the answers in bits, and LdFamily.directSampler the sampler, for any parameter routine.

The selector is the high bits of the seed (AnswerReduction.powSel), which the field arithmetic programs compute.

The components of a vector of the registers

def MIPRE.Tailored.AnsRed.Typed.comps1 (j : ℕ) {F : Type u_1} (x : Fin (D j) → F) : (Fin (2 ^ j) → F) × (Fin (2 ^ j) → F) × F

The three components of a vector of the registers: the point, the direction, the seed.

Equations

• MIPRE.Tailored.AnsRed.Typed.comps1 j x = ((MIPRE.Tailored.AnsRed.Typed.regs j).ptOf x, (MIPRE.Tailored.AnsRed.Typed.regs j).dirOf x, x (MIPRE.Tailored.AnsRed.Typed.regs j).coord)

theorem MIPRE.Tailored.AnsRed.Typed.comps1_add (j : ℕ) {F : Type u_1} [Field F] (x y : Fin (D j) → F) : comps1 j (x + y) = comps1 j x + comps1 j y

theorem MIPRE.Tailored.AnsRed.Typed.comps1_putPt (j : ℕ) {F : Type u_1} [Field F] (w : Fin (2 ^ j) → F) : comps1 j ((regs j).putPt w) = (w, 0, 0)

theorem MIPRE.Tailored.AnsRed.Typed.comps1_putDir (j : ℕ) {F : Type u_1} [Field F] (w : Fin (2 ^ j) → F) : comps1 j ((regs j).putDir w) = (0, w, 0)

theorem MIPRE.Tailored.AnsRed.Typed.comps1_proj_coordSet (j : ℕ) {F : Type u_1} [Field F] (x : Fin (D j) → F) : comps1 j ((CL.proj (regs j).coordSet) x) = (0, 0, x (regs j).coord)

def MIPRE.Tailored.AnsRed.Typed.seedPart1 {F : Type u_1} [Field F] (τ : LIDT.CL.Ty) (s : F) : F

The seed component of a line type's first stage.

Equations

• MIPRE.Tailored.AnsRed.Typed.seedPart1 τ s = if τ = MIPRE.LIDT.CL.Ty.point then 0 else s

theorem MIPRE.Tailored.AnsRed.Typed.comps1_seedLin (j : ℕ) {F : Type u_1} [Field F] (τ : LIDT.CL.Ty) (x : Fin (D j) → F) : comps1 j (((regs j).seedLin τ) x) = (0, 0, seedPart1 τ (x (regs j).coord))

theorem MIPRE.Tailored.AnsRed.Typed.comps1_secondLin (j : ℕ) {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {hM : 2 ^ j ∣ Fintype.card F} (S : LIDT.CL.Sel F (2 ^ j) hM) (τ : LIDT.CL.Ty) (s : F) (x : Fin (D j) → F) : comps1 j (((regs j).secondLin S τ s) x) = (0, AnswerReduction.Pcp.dirPart (2 ^ j) S τ s ((regs j).dirOf x), 0)

theorem MIPRE.Tailored.AnsRed.Typed.comps1_marginal (j : ℕ) {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {hM : 2 ^ j ∣ Fintype.card F} (S : LIDT.CL.Sel F (2 ^ j) hM) (τ : LIDT.CL.Ty) {lev : ℕ} (hl : 1 ≤ lev) (x : Fin (D j) → F) : comps1 j ((CL.CLFun.truncate lev ((regs j).pres S τ)).eval x) = (if 3 ≤ lev then (LIDT.CL.Regs.ptMap S τ (x (regs j).coord) (AnswerReduction.Pcp.dirPart (2 ^ j) S τ (x (regs j).coord) ((regs j).dirOf x))) ((regs j).ptOf x) else 0, if 2 ≤ lev then AnswerReduction.Pcp.dirPart (2 ^ j) S τ (x (regs j).coord) ((regs j).dirOf x) else 0, seedPart1 τ (x (regs j).coord))

The marginals, run by run: the line's base point on the point run, the cut-down direction on the direction run for a diagonal line, the seed for a line.

theorem MIPRE.Tailored.AnsRed.Typed.comps1_map_zero (j : ℕ) {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {hM : 2 ^ j ∣ Fintype.card F} (S : LIDT.CL.Sel F (2 ^ j) hM) (τ : LIDT.CL.Ty) (u y : Fin (D j) → F) : comps1 j ((((regs j).pres S τ).mapOfPrefix 0 u) y) = (0, 0, seedPart1 τ (y (regs j).coord))

The first stage map, run by run.

theorem MIPRE.Tailored.AnsRed.Typed.comps1_map_one (j : ℕ) {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {hM : 2 ^ j ∣ Fintype.card F} (S : LIDT.CL.Sel F (2 ^ j) hM) (τ : LIDT.CL.Ty) (u y : Fin (D j) → F) : comps1 j ((((regs j).pres S τ).mapOfPrefix 1 u) y) = (0, AnswerReduction.Pcp.dirPart (2 ^ j) S τ (u (regs j).coord) ((regs j).dirOf y), 0)

The second stage map, run by run.

theorem MIPRE.Tailored.AnsRed.Typed.comps1_map_two (j : ℕ) {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {hM : 2 ^ j ∣ Fintype.card F} (S : LIDT.CL.Sel F (2 ^ j) hM) (τ : LIDT.CL.Ty) (u y : Fin (D j) → F) : comps1 j ((((regs j).pres S τ).mapOfPrefix 2 u) y) = ((LIDT.CL.Regs.ptMap S τ (u (regs j).coord) ((regs j).dirOf u)) ((regs j).ptOf y), 0, 0)

The third stage map, run by run.

The factor spaces, coordinate by coordinate

theorem MIPRE.Tailored.AnsRed.Typed.mem_coordSet_regs (j : ℕ) (r : Fin (D j)) : r ∈ (regs j).coordSet ↔ ↑r = 2 * 2 ^ j

theorem MIPRE.Tailored.AnsRed.Typed.mem_dirSet_regs (j : ℕ) (r : Fin (D j)) : r ∈ (regs j).dirSet ↔ 2 ^ j ≤ ↑r ∧ ↑r < 2 * 2 ^ j

theorem MIPRE.Tailored.AnsRed.Typed.mem_finalSet_regs (j : ℕ) (r : Fin (D j)) : r ∈ (regs j).finalSet ↔ ↑r < 2 ^ j

The bits of a vector of the registers

noncomputable def MIPRE.Tailored.AnsRed.Typed.ldBitsV (j t : ℕ) (ht : 1 ≤ t) (v : Fin (D j) → (SAT.shoupBinField t ht).carrier) : Cost.BitStr

The Shoup bits of a vector of the registers, coordinate by coordinate.

Equations

• MIPRE.Tailored.AnsRed.Typed.ldBitsV j t ht v = ((MIPRE.SAT.shoupBinField t ht).vecBits v).flatten

theorem MIPRE.Tailored.AnsRed.Typed.finProdFinEquiv_symm_mk (j t : ℕ) (r : Fin (D j)) (b : Fin t) (h : ↑r * t + ↑b < D j * t) : finProdFinEquiv.symm ⟨↑r * t + ↑b, h⟩ = (r, b)

theorem MIPRE.Tailored.AnsRed.Typed.toBits_ld (j t : ℕ) (ht : 1 ≤ t) (v : Fin (D j) → (SAT.shoupBinField t ht).carrier) : CL.toBits ((CL.reindexEquiv finProdFinEquiv) ((CL.downsizeEquiv (SAT.shoupPowerBasis t ht)) v)) = ldBitsV j t ht v

The bits of the downsized vector are its coordinates' Shoup bits, in order.

theorem MIPRE.Tailored.AnsRed.Typed.ofBits_ld (j t : ℕ) (ht : 1 ≤ t) (v : Fin (D j) → (SAT.shoupBinField t ht).carrier) : CL.ofBits (D j * t) (ldBitsV j t ht v) = (CL.reindexEquiv finProdFinEquiv) ((CL.downsizeEquiv (SAT.shoupPowerBasis t ht)) v)

theorem MIPRE.Tailored.AnsRed.Typed.exists_ldBitsV (j t : ℕ) (ht : 1 ≤ t) {z : Cost.BitStr} (hz : List.length z = D j * t) : ∃ (v : Fin (D j) → (SAT.shoupBinField t ht).carrier), z = ldBitsV j t ht v

Every bit string of the right length is the bits of a vector of the registers.

theorem MIPRE.Tailored.AnsRed.Typed.vecBits_regs (j t : ℕ) (ht : 1 ≤ t) (v : Fin (D j) → (SAT.shoupBinField t ht).carrier) : (SAT.shoupBinField t ht).vecBits v = (SAT.shoupBinField t ht).vecBits ((regs j).ptOf v) ++ (SAT.shoupBinField t ht).vecBits ((regs j).dirOf v) ++ [(SAT.shoupBinField t ht).toBits (v (regs j).coord)]

The bits of a vector are its three runs of blocks.

def MIPRE.Tailored.AnsRed.Typed.blocks1 (k m' : Cost.Unary) (z : Cost.BitStr) : AnswerReduction.StageProg.Blocks

The three runs of a bit string of M + M + 1 blocks of k bits.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.blocks1_ldBitsV (j t : ℕ) (ht : 1 ≤ t) (v : Fin (D j) → (SAT.shoupBinField t ht).carrier) : blocks1 (Cost.unary t) (Cost.unary (2 ^ j)) (ldBitsV j t ht v) = ((SAT.shoupBinField t ht).vecBits ((regs j).ptOf v), (SAT.shoupBinField t ht).vecBits ((regs j).dirOf v), [(SAT.shoupBinField t ht).toBits (v (regs j).coord)])

def MIPRE.Tailored.AnsRed.Typed.ldInd (j k : ℕ) (F : Finset (Fin (D j))) : Cost.BitStr

The indicator bits of a set of coordinates of the registers, k per coordinate.

Equations

• MIPRE.Tailored.AnsRed.Typed.ldInd j k F = (List.ofFn fun (r : Fin (MIPRE.Tailored.AnsRed.Typed.D j)) => List.replicate k (decide (r ∈ F))).flatten

theorem MIPRE.Tailored.AnsRed.Typed.ldInd_eq_bitsOf (j k : ℕ) (F : Finset (Fin (D j))) : ldInd j k F = AnswerReduction.StageProg.bitsOf (List.ofFn fun (r : Fin (2 ^ j)) => List.replicate k (decide ((regs j).pt r ∈ F)), List.ofFn fun (r : Fin (2 ^ j)) => List.replicate k (decide ((regs j).dir r ∈ F)), [List.replicate k (decide ((regs j).coord ∈ F))])

The downsized presentation in bits

theorem MIPRE.Tailored.AnsRed.Typed.toBits_eval_truncate_ldCl {j t : ℕ} {ht : 1 ≤ t} {hM : 2 ^ j ∣ Fintype.card (Fq t ht)} (S : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM) (τ : LIDT.CL.Ty) (lev : ℕ) (v : Fin (D j) → Fq t ht) : CL.toBits ((CL.CLFun.truncate lev (ldCl t ht S τ)).eval (CL.ofBits (D j * t) (ldBitsV j t ht v))) = ldBitsV j t ht ((CL.CLFun.truncate lev ((regs j).pres S τ)).eval v)

theorem MIPRE.Tailored.AnsRed.Typed.toBits_mapOfPrefix_ldCl {j t : ℕ} {ht : 1 ≤ t} {hM : 2 ^ j ∣ Fintype.card (Fq t ht)} (S : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM) (τ : LIDT.CL.Ty) (lev : ℕ) (u y : Fin (D j) → Fq t ht) : CL.toBits (((ldCl t ht S τ).mapOfPrefix lev (CL.ofBits (D j * t) (ldBitsV j t ht u))) (CL.ofBits (D j * t) (ldBitsV j t ht y))) = ldBitsV j t ht ((((regs j).pres S τ).mapOfPrefix lev u) y)

theorem MIPRE.Tailored.AnsRed.Typed.indicatorBits_factorOfPrefix_ldCl {j t : ℕ} {ht : 1 ≤ t} {hM : 2 ^ j ∣ Fintype.card (Fq t ht)} (S : LIDT.CL.Sel (Fq t ht) (2 ^ j) hM) (τ : LIDT.CL.Ty) (lev : ℕ) (u : Fin (D j) → Fq t ht) : CL.indicatorBits ((ldCl t ht S τ).factorOfPrefix lev (CL.ofBits (D j * t) (ldBitsV j t ht u))) = ldInd j t (((regs j).pres S τ).factorOfPrefix lev u)

The answers of the one-copy test

def MIPRE.Tailored.AnsRed.Typed.ldDesc (j : ℕ) : AnswerReduction.StageProg.Desc

The copy's description: offset 0, length M = 2^j, selector width j, seed 0.

Equations

• MIPRE.Tailored.AnsRed.Typed.ldDesc j = (MIPRE.Cost.unary 0, MIPRE.Cost.unary (2 ^ j), MIPRE.Cost.unary j, MIPRE.Cost.unary 0)

noncomputable def MIPRE.Tailored.AnsRed.Typed.ldAnswer (k : Cost.Unary) (d : AnswerReduction.StageProg.Desc) (τ : ℕ) (m' : Cost.Unary) (kind lev : ℕ) (u y : Cost.BitStr) : Cost.BitStr

The answer of the one-copy test to a query of kind kind at level lev with vectors u, y: the MIP* answer reduction's run functions on runs of M + M + 1 blocks.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.sliceL_zero_full {α : Type u_1} (l : List α) {N : ℕ} (hl : l.length = N) : AnswerReduction.Pcp.sliceL 0 N l = l

theorem MIPRE.Tailored.AnsRed.Typed.placeL_zero_full {α : Type u_1} (fill : α) (w l : List α) (h : w.length = l.length) : AnswerReduction.Pcp.placeL fill 0 w l = w

theorem MIPRE.Tailored.AnsRed.Typed.placeL_zero_one {α : Type u_1} (fill a b : α) : AnswerReduction.Pcp.placeL fill 0 [a] [b] = [a]

theorem MIPRE.Tailored.AnsRed.Typed.ldBitsV_eq_bitsOf {j t : ℕ} {ht : 1 ≤ t} (v : Fin (D j) → (SAT.shoupBinField t ht).carrier) : ldBitsV j t ht v = AnswerReduction.StageProg.bitsOf ((SAT.shoupBinField t ht).vecBits ((regs j).ptOf v), (SAT.shoupBinField t ht).vecBits ((regs j).dirOf v), [(SAT.shoupBinField t ht).toBits (v (regs j).coord)])

theorem MIPRE.Tailored.AnsRed.Typed.seedOf_ldDesc {j t : ℕ} {ht : 1 ≤ t} (s : (SAT.shoupBinField t ht).carrier) : AnswerReduction.StageProg.seedOf (ldDesc j) [(SAT.shoupBinField t ht).toBits s] = (SAT.shoupBinField t ht).toBits s

theorem MIPRE.Tailored.AnsRed.Typed.zeroed_one {t : ℕ} {ht : 1 ≤ t} (a : Cost.BitStr) : AnswerReduction.StageProg.zeroed (Cost.unary t) [a] = [(SAT.shoupBinField t ht).toBits 0]

theorem MIPRE.Tailored.AnsRed.Typed.seedOut_ldDesc {j t : ℕ} {ht : 1 ≤ t} (τ : LIDT.CL.Ty) (s s' : (SAT.shoupBinField t ht).carrier) : AnswerReduction.StageProg.seedOut (Cost.unary t) (ldDesc j) (AnswerReduction.StageProg.tyNat τ) ((SAT.shoupBinField t ht).toBits s) [(SAT.shoupBinField t ht).toBits s'] = [(SAT.shoupBinField t ht).toBits (seedPart1 τ s)]

theorem MIPRE.Tailored.AnsRed.Typed.selDirL_ldDesc {j t : ℕ} {ht : 1 ≤ t} [NeZero (2 ^ j)] {hsz : 2 ^ j ∣ Fintype.card (SAT.shoupBinField t ht).carrier} (S : LIDT.CL.Sel (SAT.shoupBinField t ht).carrier (2 ^ j) hsz) (hjw : j ≤ t) (hχ : ∀ (a : (SAT.shoupBinField t ht).carrier), ↑(S.χ a) = ↑(Introspection.SeedProgram.selector (SAT.shoupBinField t ht) j hjw a)) (s : (SAT.shoupBinField t ht).carrier) (w : Fin (2 ^ j) → (SAT.shoupBinField t ht).carrier) : AnswerReduction.StageProg.selDirL (Cost.unary t) (ldDesc j) ((SAT.shoupBinField t ht).toBits s) ((SAT.shoupBinField t ht).vecBits w) = (SAT.shoupBinField t ht).vecBits (LIDT.CL.zeroBelow (S.χ s) w)

theorem MIPRE.Tailored.AnsRed.Typed.ptMapL_ldDesc {j t : ℕ} {ht : 1 ≤ t} [NeZero (2 ^ j)] {hsz : 2 ^ j ∣ Fintype.card (SAT.shoupBinField t ht).carrier} (S : LIDT.CL.Sel (SAT.shoupBinField t ht).carrier (2 ^ j) hsz) (hjw : j ≤ t) (hχ : ∀ (a : (SAT.shoupBinField t ht).carrier), ↑(S.χ a) = ↑(Introspection.SeedProgram.selector (SAT.shoupBinField t ht) j hjw a)) (τ : LIDT.CL.Ty) (s : (SAT.shoupBinField t ht).carrier) (dir w : Fin (2 ^ j) → (SAT.shoupBinField t ht).carrier) : AnswerReduction.StageProg.ptMapL (Cost.unary t) (ldDesc j) (AnswerReduction.StageProg.tyNat τ) ((SAT.shoupBinField t ht).toBits s) ((SAT.shoupBinField t ht).vecBits dir) ((SAT.shoupBinField t ht).vecBits w) = (SAT.shoupBinField t ht).vecBits ((LIDT.CL.Regs.ptMap S τ s dir) w)

theorem MIPRE.Tailored.AnsRed.Typed.ptOut_ldDesc {j t : ℕ} {ht : 1 ≤ t} [NeZero (2 ^ j)] {hsz : 2 ^ j ∣ Fintype.card (SAT.shoupBinField t ht).carrier} (S : LIDT.CL.Sel (SAT.shoupBinField t ht).carrier (2 ^ j) hsz) (hjw : j ≤ t) (hχ : ∀ (a : (SAT.shoupBinField t ht).carrier), ↑(S.χ a) = ↑(Introspection.SeedProgram.selector (SAT.shoupBinField t ht) j hjw a)) (τ : LIDT.CL.Ty) (s : (SAT.shoupBinField t ht).carrier) (dir pts : Fin (2 ^ j) → (SAT.shoupBinField t ht).carrier) : AnswerReduction.StageProg.ptOut (Cost.unary t) (ldDesc j) (AnswerReduction.StageProg.tyNat τ) ((SAT.shoupBinField t ht).toBits s) ((SAT.shoupBinField t ht).vecBits dir) ((SAT.shoupBinField t ht).vecBits pts) = (SAT.shoupBinField t ht).vecBits ((LIDT.CL.Regs.ptMap S τ s dir) pts)

theorem MIPRE.Tailored.AnsRed.Typed.dirOut_ldDesc {j t : ℕ} {ht : 1 ≤ t} [NeZero (2 ^ j)] {hsz : 2 ^ j ∣ Fintype.card (SAT.shoupBinField t ht).carrier} (S : LIDT.CL.Sel (SAT.shoupBinField t ht).carrier (2 ^ j) hsz) (hjw : j ≤ t) (hχ : ∀ (a : (SAT.shoupBinField t ht).carrier), ↑(S.χ a) = ↑(Introspection.SeedProgram.selector (SAT.shoupBinField t ht) j hjw a)) (τ : LIDT.CL.Ty) (s : (SAT.shoupBinField t ht).carrier) (dirs : Fin (2 ^ j) → (SAT.shoupBinField t ht).carrier) : AnswerReduction.StageProg.dirOut (Cost.unary t) (ldDesc j) (AnswerReduction.StageProg.tyNat τ) ((SAT.shoupBinField t ht).toBits s) ((SAT.shoupBinField t ht).vecBits dirs) = (SAT.shoupBinField t ht).vecBits (AnswerReduction.Pcp.dirPart (2 ^ j) S τ s dirs)

theorem MIPRE.Tailored.AnsRed.Typed.ldAnswer_marginal {j t : ℕ} {ht : 1 ≤ t} [NeZero (2 ^ j)] {hsz : 2 ^ j ∣ Fintype.card (SAT.shoupBinField t ht).carrier} (S : LIDT.CL.Sel (SAT.shoupBinField t ht).carrier (2 ^ j) hsz) (hjw : j ≤ t) (hχ : ∀ (a : (SAT.shoupBinField t ht).carrier), ↑(S.χ a) = ↑(Introspection.SeedProgram.selector (SAT.shoupBinField t ht) j hjw a)) (τ : LIDT.CL.Ty) {lev : ℕ} (hl : 1 ≤ lev) (v : Fin (D j) → (SAT.shoupBinField t ht).carrier) (y : Cost.BitStr) : ldAnswer (Cost.unary t) (ldDesc j) (AnswerReduction.StageProg.tyNat τ) (Cost.unary (2 ^ j)) 1 lev (ldBitsV j t ht v) y = ldBitsV j t ht ((CL.CLFun.truncate lev ((regs j).pres S τ)).eval v)

The marginals of the one-copy test, in bits.

theorem MIPRE.Tailored.AnsRed.Typed.ldAnswer_linear {j t : ℕ} {ht : 1 ≤ t} [NeZero (2 ^ j)] {hsz : 2 ^ j ∣ Fintype.card (SAT.shoupBinField t ht).carrier} (S : LIDT.CL.Sel (SAT.shoupBinField t ht).carrier (2 ^ j) hsz) (hjw : j ≤ t) (hχ : ∀ (a : (SAT.shoupBinField t ht).carrier), ↑(S.χ a) = ↑(Introspection.SeedProgram.selector (SAT.shoupBinField t ht) j hjw a)) (τ : LIDT.CL.Ty) {lev : ℕ} (hl : 1 ≤ lev) (u y : Fin (D j) → (SAT.shoupBinField t ht).carrier) : ldAnswer (Cost.unary t) (ldDesc j) (AnswerReduction.StageProg.tyNat τ) (Cost.unary (2 ^ j)) 2 lev (ldBitsV j t ht u) (ldBitsV j t ht y) = ldBitsV j t ht ((((regs j).pres S τ).mapOfPrefix (lev - 1) u) y)

The stage maps of the one-copy test, in bits.

theorem MIPRE.Tailored.AnsRed.Typed.pt_mem_sets {j : ℕ} (r : Fin (2 ^ j)) : (regs j).pt r ∉ (regs j).coordSet ∧ (regs j).pt r ∉ (regs j).dirSet ∧ (regs j).pt r ∈ (regs j).finalSet

theorem MIPRE.Tailored.AnsRed.Typed.dir_mem_sets {j : ℕ} (r : Fin (2 ^ j)) : (regs j).dir r ∉ (regs j).coordSet ∧ (regs j).dir r ∈ (regs j).dirSet ∧ (regs j).dir r ∉ (regs j).finalSet

theorem MIPRE.Tailored.AnsRed.Typed.coord_mem_sets {j : ℕ} : (regs j).coord ∈ (regs j).coordSet ∧ (regs j).coord ∉ (regs j).dirSet ∧ (regs j).coord ∉ (regs j).finalSet

theorem MIPRE.Tailored.AnsRed.Typed.ldAnswer_factor {j t : ℕ} {ht : 1 ≤ t} [NeZero (2 ^ j)] {hsz : 2 ^ j ∣ Fintype.card (SAT.shoupBinField t ht).carrier} (S : LIDT.CL.Sel (SAT.shoupBinField t ht).carrier (2 ^ j) hsz) (τ : LIDT.CL.Ty) {lev : ℕ} (hl : 1 ≤ lev) (u : Fin (D j) → (SAT.shoupBinField t ht).carrier) (y : Cost.BitStr) : ldAnswer (Cost.unary t) (ldDesc j) (AnswerReduction.StageProg.tyNat τ) (Cost.unary (2 ^ j)) 3 lev (ldBitsV j t ht u) y = ldInd j t (((regs j).pres S τ).factorOfPrefix (lev - 1) u)

The factor spaces of the one-copy test, in indicator bits.

The program

noncomputable def MIPRE.Tailored.AnsRed.Typed.blocks1P (z : Cost.PolyTimeFun AnswerReduction.StageProg.Input Cost.BitStr) : Cost.PolyTimeFun AnswerReduction.StageProg.Input AnswerReduction.StageProg.Blocks

The three runs of the input's u or y, as a program.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.blocks1P_apply (z : Cost.PolyTimeFun AnswerReduction.StageProg.Input Cost.BitStr) (x : AnswerReduction.StageProg.Input) : (blocks1P z).toFun x = blocks1 (AnswerReduction.StageProg.kI.toFun x) (AnswerReduction.StageProg.mI.toFun x) (z.toFun x)

noncomputable def MIPRE.Tailored.AnsRed.Typed.ldProg : Cost.PolyTimeFun AnswerReduction.StageProg.Input Cost.BitStr

The program of the one-copy test.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.ldProg_apply (k : Cost.Unary) (d : AnswerReduction.StageProg.Desc) (τ : ℕ) (m' : Cost.Unary) (kind lev : ℕ) (u y : Cost.BitStr) : ldProg.toFun (k, d, τ, m', kind, lev, u, y) = ldAnswer k d τ m' kind lev u y

noncomputable def MIPRE.Tailored.AnsRed.Typed.kL : Cost.PolyTimeFun CL.DirectInput Cost.Unary

The field width, read off the parameters.

Equations

• MIPRE.Tailored.AnsRed.Typed.kL = MIPRE.AnswerReduction.readU.comp (MIPRE.Cost.PolyTimeFun.treeHead.comp MIPRE.AnswerReduction.pdI)

noncomputable def MIPRE.Tailored.AnsRed.Typed.mL : Cost.PolyTimeFun CL.DirectInput Cost.Unary

The register length M, read off the parameters.

Equations

• MIPRE.Tailored.AnsRed.Typed.mL = MIPRE.AnswerReduction.readU.comp (MIPRE.Cost.PolyTimeFun.treeHead.comp (MIPRE.Cost.PolyTimeFun.treeTail.comp MIPRE.AnswerReduction.pdI))

noncomputable def MIPRE.Tailored.AnsRed.Typed.dL : Cost.PolyTimeFun CL.DirectInput AnswerReduction.StageProg.Desc

The copy's description, read off the parameters.

Equations

• MIPRE.Tailored.AnsRed.Typed.dL = MIPRE.AnswerReduction.readDesc.comp (MIPRE.Cost.PolyTimeFun.treeTail.comp (MIPRE.Cost.PolyTimeFun.treeTail.comp MIPRE.AnswerReduction.pdI))

noncomputable def MIPRE.Tailored.AnsRed.Typed.τL : Cost.PolyTimeFun CL.DirectInput ℕ

The test type's number, read off the type.

Equations

• MIPRE.Tailored.AnsRed.Typed.τL = MIPRE.CL.Detyping.Program.readNat.comp MIPRE.AnswerReduction.tagI

noncomputable def MIPRE.Tailored.AnsRed.Typed.ldAssemble : Cost.PolyTimeFun CL.DirectInput AnswerReduction.StageProg.Input

The one-copy program's input, read off a direct query.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.ldAnswerProg : Cost.PolyTimeFun CL.DirectInput Cost.BitStr

The answer program of the low-degree half: the one-copy program on the parameters.

Equations

• MIPRE.Tailored.AnsRed.Typed.ldAnswerProg = MIPRE.Tailored.AnsRed.Typed.ldProg.comp MIPRE.Tailored.AnsRed.Typed.ldAssemble

noncomputable def MIPRE.Tailored.AnsRed.Typed.ldDimProg : Cost.PolyTimeFun Cost.Data Cost.Unary

The dimension program: (2M + 1) k in unary.

Equations

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

The low-degree half as a directly answered sampler

structure MIPRE.Tailored.AnsRed.Typed.LdFamily : Type

A family of parameters of the low-degree half: the field width t, with q = 2^t, and the selector width j ≤ t, with M = 2^j variables.

• t : ℕ → ℕ

  The field width.

• ht (n : ℕ) : 1 ≤ self.t n
• j : ℕ → ℕ

  The selector width, log₂ M.

• hjt (n : ℕ) : self.j n ≤ self.t n

theorem MIPRE.Tailored.AnsRed.Typed.LdFamily.dvd (F : LdFamily) (n : ℕ) : 2 ^ F.j n ∣ Fintype.card (Fq (F.t n) ⋯)

noncomputable def MIPRE.Tailored.AnsRed.Typed.LdFamily.sel (F : LdFamily) (n : ℕ) : LIDT.CL.Sel (Fq (F.t n) ⋯) (2 ^ F.j n) ⋯

The selector at index n: the high j bits of the seed.

Equations

• F.sel n = MIPRE.AnswerReduction.powSel (F.t n) ⋯ (2 ^ F.j n) (F.j n) ⋯ ⋯

noncomputable def MIPRE.Tailored.AnsRed.Typed.LdFamily.cl (F : LdFamily) (n : ℕ) (τ : LIDT.CL.Ty) : CL.CLFun CL.𝔽₂ (Fin (D (F.j n) * F.t n)) 3

The CL functions at index n: the presentation of the type, downsized and numbered.

Equations

• F.cl n τ = MIPRE.Tailored.AnsRed.Typed.ldCl (F.t n) ⋯ (F.sel n) τ

def MIPRE.Tailored.AnsRed.Typed.LdFamily.pd (F : LdFamily) (n : ℕ) : Cost.Data

The parameters at index n: t and M and the copy's description, in unary.

Equations

• F.pd n = MIPRE.Cost.encode (MIPRE.Cost.unary (F.t n), MIPRE.Cost.unary (2 ^ F.j n), MIPRE.Tailored.AnsRed.Typed.ldDesc (F.j n))

theorem MIPRE.Tailored.AnsRed.Typed.LdFamily.ldAnswerProg_apply (F : LdFamily) (n : ℕ) (τ : LIDT.CL.Ty) (kind lev : ℕ) (u y : Cost.BitStr) : ldAnswerProg.toFun (F.pd n, Cost.encode τ, kind, lev, u, y) = ldAnswer (Cost.unary (F.t n)) (ldDesc (F.j n)) (AnswerReduction.StageProg.tyNat τ) (Cost.unary (2 ^ F.j n)) kind lev u y

theorem MIPRE.Tailored.AnsRed.Typed.LdFamily.ldDimProg_pd (F : LdFamily) (n : ℕ) : List.length (ldDimProg.toFun (F.pd n)) = D (F.j n) * F.t n

theorem MIPRE.Tailored.AnsRed.Typed.LdFamily.exists_ldBitsV_of_toBits (F : LdFamily) (n : ℕ) {lev : ℕ} (τ : LIDT.CL.Ty) (x : Fin (D (F.j n) * F.t n) → CL.𝔽₂) : ∃ (u : Fin (D (F.j n)) → (SAT.shoupBinField (F.t n) ⋯).carrier), CL.toBits ((CL.CLFun.truncate lev (F.cl n τ)).eval x) = ldBitsV (F.j n) (F.t n) ⋯ u

noncomputable def MIPRE.Tailored.AnsRed.Typed.LdFamily.directSampler (F : LdFamily) (pp : Cost.Prog) (hpp : Cost.Prog.WellScoped 1 pp) (hruns : ∀ (n : ℕ), ∃ (t : ℕ), pp.Runs (Cost.encode n) (F.pd n) t) : CL.DirectSampler 3 LIDT.CL.Ty

The low-degree half of the answer-reduced sampler, directly answered, given a routine computing its parameters.

Equations

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