The proof check's equations, as programs

Slice P4h of planning/aldous-lyons-track.md: the equations the linear values of an oracle's point answer enter in the proof check (Typed.proofEqs): the system check and the three linear assignment checks, each a field equation in the answer bits whose coefficients are read from the point and the readable value of g_O. Each is computed by fieldConsF from a program of its value at the answer bits (proofEqsF_eq); with the guard of ArLpProof they are the proof check's constraints (proofConsF_eq).

• zAt: the answer bits' field element at a position of the oracle's answer.
• pLin, pαL, pβLa, pβLb, pβL: the positions of the linear slots, after the readable ones (idxO_gLa and the rest).

Positions of the linear slots and cells of an index of O

noncomputable def MIPRE.Tailored.AnsRed.Typed.pLin {J : Type} [Cost.SizedEncoding J] (ρ : Cost.PolyTimeFun J PrfIn) (c : Cost.PolyTimeFun J Cost.Unary) : Cost.PolyTimeFun J Cost.Unary

The position R + c of the oracle's answer: c after the readable slots.

Equations

• MIPRE.Tailored.AnsRed.Typed.pLin ρ c = MIPRE.Cost.PolyTimeFun.append.ap₂ (MIPRE.Tailored.AnsRed.Typed.jRc ρ) c

noncomputable def MIPRE.Tailored.AnsRed.Typed.lB0 {J : Type} [Cost.SizedEncoding J] (ρ : Cost.PolyTimeFun J PrfIn) : Cost.PolyTimeFun J Cost.Unary

5 + ◇', the position of β_{La} after the readable slots.

Equations

• MIPRE.Tailored.AnsRed.Typed.lB0 ρ = MIPRE.Cost.PolyTimeFun.append.ap₂ (MIPRE.Tailored.AnsRed.Typed.uc 5) (MIPRE.Tailored.AnsRed.Typed.jOW ρ)

noncomputable def MIPRE.Tailored.AnsRed.Typed.pαL {J : Type} [Cost.SizedEncoding J] (ρ : Cost.PolyTimeFun J PrfIn) (i : Cost.PolyTimeFun J Cost.Unary) : Cost.PolyTimeFun J Cost.Unary

The position of α^L_i.

Equations

• MIPRE.Tailored.AnsRed.Typed.pαL ρ i = MIPRE.Tailored.AnsRed.Typed.pLin ρ (MIPRE.Cost.PolyTimeFun.append.ap₂ (MIPRE.Tailored.AnsRed.Typed.uc 5) i)

noncomputable def MIPRE.Tailored.AnsRed.Typed.pβLa {J : Type} [Cost.SizedEncoding J] (ρ : Cost.PolyTimeFun J PrfIn) (i : Cost.PolyTimeFun J Cost.Unary) : Cost.PolyTimeFun J Cost.Unary

The position of β_{La, i}.

Equations

• MIPRE.Tailored.AnsRed.Typed.pβLa ρ i = MIPRE.Tailored.AnsRed.Typed.pLin ρ (MIPRE.Cost.PolyTimeFun.append.ap₂ (MIPRE.Tailored.AnsRed.Typed.lB0 ρ) i)

noncomputable def MIPRE.Tailored.AnsRed.Typed.pβLb {J : Type} [Cost.SizedEncoding J] (ρ : Cost.PolyTimeFun J PrfIn) (i : Cost.PolyTimeFun J Cost.Unary) : Cost.PolyTimeFun J Cost.Unary

The position of β_{Lb, i}.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.pβL {J : Type} [Cost.SizedEncoding J] (ρ : Cost.PolyTimeFun J PrfIn) (k : ℕ) (i : Cost.PolyTimeFun J Cost.Unary) : Cost.PolyTimeFun J Cost.Unary

The position of β_{L, k, i}.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.cB {J : Type} [Cost.SizedEncoding J] (ρ : Cost.PolyTimeFun J PrfIn) (i : Cost.PolyTimeFun J Cost.Unary) : Cost.PolyTimeFun J Cost.Unary

The cell ℓ + i of an index of O: of the second linear answer.

Equations

• MIPRE.Tailored.AnsRed.Typed.cB ρ i = MIPRE.Cost.PolyTimeFun.append.ap₂ (MIPRE.Tailored.AnsRed.Typed.jL ρ) i

noncomputable def MIPRE.Tailored.AnsRed.Typed.cL {J : Type} [Cost.SizedEncoding J] (ρ : Cost.PolyTimeFun J PrfIn) (k : ℕ) (i : Cost.PolyTimeFun J Cost.Unary) : Cost.PolyTimeFun J Cost.Unary

The cell 2ℓ + k ◇ + i of an index of O: of the k-th copy.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.cSgn {J : Type} [Cost.SizedEncoding J] (ρ : Cost.PolyTimeFun J PrfIn) (k : ℕ) : Cost.PolyTimeFun J Cost.Unary

The cell 2ℓ + 3◇ + k of an index of O: of the k-th sign.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.pLin_eq {t : ℕ} {J : Type} [Cost.SizedEncoding J] {ρ : Cost.PolyTimeFun J PrfIn} {x : J} {j d : ℕ} {L : PcpDims} {e : Cost.Data} (hP : rP.toFun (ρ.toFun x) = arParams t j d L e) {c : Cost.PolyTimeFun J Cost.Unary} {k : ℕ} (hc : c.toFun x = Cost.unary k) : (pLin ρ c).toFun x = Cost.unary ((rSlots L).length + k)

theorem MIPRE.Tailored.AnsRed.Typed.pgLa_eq {t : ℕ} {J : Type} [Cost.SizedEncoding J] {ρ : Cost.PolyTimeFun J PrfIn} {x : J} {j d : ℕ} {L : PcpDims} {e : Cost.Data} (hP : rP.toFun (ρ.toFun x) = arParams t j d L e) : (pLin ρ (uc 0)).toFun x = Cost.unary (idxO Slot.gLa)

theorem MIPRE.Tailored.AnsRed.Typed.pgLb_eq {t : ℕ} {J : Type} [Cost.SizedEncoding J] {ρ : Cost.PolyTimeFun J PrfIn} {x : J} {j d : ℕ} {L : PcpDims} {e : Cost.Data} (hP : rP.toFun (ρ.toFun x) = arParams t j d L e) : (pLin ρ (uc 1)).toFun x = Cost.unary (idxO Slot.gLb)

theorem MIPRE.Tailored.AnsRed.Typed.pgL_eq {t : ℕ} {J : Type} [Cost.SizedEncoding J] {ρ : Cost.PolyTimeFun J PrfIn} {x : J} {j d : ℕ} {L : PcpDims} {e : Cost.Data} (hP : rP.toFun (ρ.toFun x) = arParams t j d L e) (k : Fin 3) : (pLin ρ (uc (2 + ↑k))).toFun x = Cost.unary (idxO (Slot.gL k))

theorem MIPRE.Tailored.AnsRed.Typed.pαL_eq {t : ℕ} {J : Type} [Cost.SizedEncoding J] {ρ : Cost.PolyTimeFun J PrfIn} {x : J} {j d : ℕ} {L : PcpDims} {e : Cost.Data} (hP : rP.toFun (ρ.toFun x) = arParams t j d L e) {i : Cost.PolyTimeFun J Cost.Unary} (a : Fin L.oW) (hi : i.toFun x = Cost.unary ↑a) : (pαL ρ i).toFun x = Cost.unary (idxO (Slot.αL a))

theorem MIPRE.Tailored.AnsRed.Typed.pβLa_eq {t : ℕ} {J : Type} [Cost.SizedEncoding J] {ρ : Cost.PolyTimeFun J PrfIn} {x : J} {j d : ℕ} {L : PcpDims} {e : Cost.Data} (hP : rP.toFun (ρ.toFun x) = arParams t j d L e) {i : Cost.PolyTimeFun J Cost.Unary} (a : Fin L.ℓ) (hi : i.toFun x = Cost.unary ↑a) : (pβLa ρ i).toFun x = Cost.unary (idxO (Slot.βLa a))

theorem MIPRE.Tailored.AnsRed.Typed.pβLb_eq {t : ℕ} {J : Type} [Cost.SizedEncoding J] {ρ : Cost.PolyTimeFun J PrfIn} {x : J} {j d : ℕ} {L : PcpDims} {e : Cost.Data} (hP : rP.toFun (ρ.toFun x) = arParams t j d L e) {i : Cost.PolyTimeFun J Cost.Unary} (a : Fin L.ℓ) (hi : i.toFun x = Cost.unary ↑a) : (pβLb ρ i).toFun x = Cost.unary (idxO (Slot.βLb a))

theorem MIPRE.Tailored.AnsRed.Typed.pβL_eq {t : ℕ} {J : Type} [Cost.SizedEncoding J] {ρ : Cost.PolyTimeFun J PrfIn} {x : J} {j d : ℕ} {L : PcpDims} {e : Cost.Data} (hP : rP.toFun (ρ.toFun x) = arParams t j d L e) (k : Fin 3) {i : Cost.PolyTimeFun J Cost.Unary} (a : Fin L.dm) (hi : i.toFun x = Cost.unary ↑a) : (pβL ρ (↑k) i).toFun x = Cost.unary (idxO (Slot.βL k a))

theorem MIPRE.Tailored.AnsRed.Typed.cB_eq {t : ℕ} {J : Type} [Cost.SizedEncoding J] {ρ : Cost.PolyTimeFun J PrfIn} {x : J} {j d : ℕ} {L : PcpDims} {e : Cost.Data} (hP : rP.toFun (ρ.toFun x) = arParams t j d L e) {i : Cost.PolyTimeFun J Cost.Unary} (a : Fin L.ℓ) (hi : i.toFun x = Cost.unary ↑a) : (cB ρ i).toFun x = Cost.unary ↑(L.oB a)

theorem MIPRE.Tailored.AnsRed.Typed.cL_eq {t : ℕ} {J : Type} [Cost.SizedEncoding J] {ρ : Cost.PolyTimeFun J PrfIn} {x : J} {j d : ℕ} {L : PcpDims} {e : Cost.Data} (hP : rP.toFun (ρ.toFun x) = arParams t j d L e) (k : Fin 3) {i : Cost.PolyTimeFun J Cost.Unary} (a : Fin L.dm) (hi : i.toFun x = Cost.unary ↑a) : (cL ρ (↑k) i).toFun x = Cost.unary ↑(L.oL k a)

theorem MIPRE.Tailored.AnsRed.Typed.cSgn_eq {t : ℕ} {J : Type} [Cost.SizedEncoding J] {ρ : Cost.PolyTimeFun J PrfIn} {x : J} {j d : ℕ} {L : PcpDims} {e : Cost.Data} (hP : rP.toFun (ρ.toFun x) = arParams t j d L e) (k : Fin 6) : (cSgn ρ ↑k).toFun x = Cost.unary ↑(L.oSgn k)

The answer bits at a position

noncomputable def MIPRE.Tailored.AnsRed.Typed.zAt {J : Type} [Cost.SizedEncoding J] (ρ : Cost.PolyTimeFun J PrfIn) (ζ : Cost.PolyTimeFun J Cost.BitStr) (w : Cost.PolyTimeFun J Cost.Unary) : Cost.PolyTimeFun J Cost.BitStr

The answer bits' field element at position w of the oracle's answer, at its offset o: the window at o + w t.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.zAt_eq {t : ℕ} {ht : 1 ≤ t} {J : Type} [Cost.SizedEncoding J] {ρ : Cost.PolyTimeFun J PrfIn} {ζ : Cost.PolyTimeFun J Cost.BitStr} {x : J} {j d : ℕ} {L : PcpDims} {e : Cost.Data} (hP : rP.toFun (ρ.toFun x) = arParams t j d L e) {o : ℕ} (hO : rO.toFun (ρ.toFun x) = Cost.unary o) {w : Cost.PolyTimeFun J Cost.Unary} {k : ℕ} (hw : w.toFun x = Cost.unary k) {N : ℕ} (hz : List.length (ζ.toFun x) ≤ N) : (zAt ρ ζ w).toFun x = (SAT.shoupBinField t ht).toBits ((Intro.fldAt t ht N (o + k * t)) (Intro.bitVec N (ζ.toFun x)))

The values of the equations

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.AnsRed.Typed.vρ : Cost.PolyTimeFun (PrfIn × Cost.BitStr) PrfIn

The input of an equation's value: the proof check's input and the answer bits.

Equations

• MIPRE.Tailored.AnsRed.Typed.vρ = MIPRE.Cost.PolyTimeFun.fst

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.AnsRed.Typed.vζ : Cost.PolyTimeFun (PrfIn × Cost.BitStr) Cost.BitStr

The answer bits.

Equations

• MIPRE.Tailored.AnsRed.Typed.vζ = MIPRE.Cost.PolyTimeFun.snd

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.AnsRed.Typed.tρ : Cost.PolyTimeFun (Cost.Unary × PrfIn × Cost.BitStr) PrfIn

The proof check's input, under an index.

Equations

• MIPRE.Tailored.AnsRed.Typed.tρ = MIPRE.Cost.PolyTimeFun.fst.comp MIPRE.Cost.PolyTimeFun.snd

@[reducible, inline]

noncomputable abbrev MIPRE.Tailored.AnsRed.Typed.tζ : Cost.PolyTimeFun (Cost.Unary × PrfIn × Cost.BitStr) Cost.BitStr

The answer bits, under an index.

Equations

• MIPRE.Tailored.AnsRed.Typed.tζ = MIPRE.Cost.PolyTimeFun.snd.comp MIPRE.Cost.PolyTimeFun.snd

noncomputable def MIPRE.Tailored.AnsRed.Typed.eqTermF (wire pos : Cost.PolyTimeFun (Cost.Unary × PrfIn × Cost.BitStr) Cost.Unary) : Cost.PolyTimeFun (Cost.Unary × PrfIn × Cost.BitStr) Cost.BitStr

A term x_w (1 - x_w) v_p of an equation: the point's coordinate at the wire of the index and the linear value at the position of the index.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.asgEqF (g : Cost.PolyTimeFun (PrfIn × Cost.BitStr) Cost.Unary) (term : Cost.PolyTimeFun (Cost.Unary × PrfIn × Cost.BitStr) Cost.BitStr) (k : Cost.PolyTimeFun (PrfIn × Cost.BitStr) Cost.Unary) : Cost.PolyTimeFun (PrfIn × Cost.BitStr) Cost.BitStr

The value of an assignment equation g (1 - g) - ∑_{i < k} x_{e_i} (1 - x_{e_i}) β_i, in characteristic 2 a sum.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.asgAEqF : Cost.PolyTimeFun (PrfIn × Cost.BitStr) Cost.BitStr

The assignment equation of g_{La}.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.asgBEqF : Cost.PolyTimeFun (PrfIn × Cost.BitStr) Cost.BitStr

The assignment equation of g_{Lb}.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.asgLEqF (k : ℕ) : Cost.PolyTimeFun (PrfIn × Cost.BitStr) Cost.BitStr

The assignment equation of g_{L,k}.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.sgnCoefF {J : Type} [Cost.SizedEncoding J] (ρ : Cost.PolyTimeFun J PrfIn) (k : ℕ) : Cost.PolyTimeFun J Cost.BitStr

w_O x_{σ_k}, the coefficient of a sign: the readable value of g_O times the point's coordinate at the k-th sign of the index of O.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.sysEqF : Cost.PolyTimeFun (PrfIn × Cost.BitStr) Cost.BitStr

The value of the system equation ∑_{k < 5} w_O x_{σ_k} v_{c_k} - ∑_X x_X (1 - x_X) α^L_X, the c_k being g_{La}, g_{Lb} and the three g_{L,k}.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.proofEqsF : Cost.PolyTimeFun PrfIn (List Cost.BitStr)

The proof check's equations, as constraints: those of the system equation, then those of the five assignment equations.

Equations

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

Correctness

theorem MIPRE.Tailored.AnsRed.Typed.eqsCons_cons {t : ℕ} {ht : 1 ≤ t} {N : ℕ} (a : ((Fin N → ZMod 2) →ₗ[ZMod 2] Fq t ht) × Fq t ht) (l : List (((Fin N → ZMod 2) →ₗ[ZMod 2] Fq t ht) × Fq t ht)) : eqsCons t ht (a :: l) = List.map Intro.LinCheck.toCon (Intro.fieldChecks t ht a.1 a.2) ++ eqsCons t ht l

theorem MIPRE.Tailored.AnsRed.Typed.asg_apply {t : ℕ} {ht : 1 ≤ t} {N : ℕ} {S : Type} (v : S → (Fin N → ZMod 2) →ₗ[ZMod 2] Fq t ht) (g : S) {n : ℕ} (c : Fin n → Fq t ht) (β : Fin n → S) (w : Fin N → ZMod 2) : (certLin ∘ₗ v g - ∑ i : Fin n, mulL (c i) ∘ₗ v (β i)) w = (v g) w * (1 - (v g) w) + ∑ i : Fin n, c i * (v (β i)) w

The value of an assignment equation's linear map.

theorem MIPRE.Tailored.AnsRed.Typed.eqTermF_eq {t : ℕ} {ht : 1 ≤ t} {j d : ℕ} {L : PcpDims} {e : Cost.Data} {inp : PrfIn} (hP : rP.toFun inp = arParams t j d L e) {o N : ℕ} (hO : rO.toFun inp = Cost.unary o) {q : Fin L.m → Fq t ht} (hpts : ∀ (X : Fin L.m), (rPts.toFun inp).getD ↑X [] = (SAT.shoupBinField t ht).toBits (q X)) {z : Cost.BitStr} (hz : List.length z ≤ N) {wire pos : Cost.PolyTimeFun (Cost.Unary × PrfIn × Cost.BitStr) Cost.Unary} (i : ℕ) (X : Fin L.m) (hw : wire.toFun (Cost.unary i, inp, z) = Cost.unary ↑X) (s : Slot L) (hp : pos.toFun (Cost.unary i, inp, z) = Cost.unary (idxO s)) : (eqTermF wire pos).toFun (Cost.unary i, inp, z) = (SAT.shoupBinField t ht).toBits (q X * (1 - q X) * (Intro.fldAt t ht N (o + idxO s * t)) (Intro.bitVec N z))

theorem MIPRE.Tailored.AnsRed.Typed.asgEqF_eq {t : ℕ} {ht : 1 ≤ t} {j d : ℕ} {L : PcpDims} {e : Cost.Data} {inp : PrfIn} (hP : rP.toFun inp = arParams t j d L e) {o N : ℕ} (hO : rO.toFun inp = Cost.unary o) {q : Fin L.m → Fq t ht} (hpts : ∀ (X : Fin L.m), (rPts.toFun inp).getD ↑X [] = (SAT.shoupBinField t ht).toBits (q X)) {z : Cost.BitStr} (hz : List.length z ≤ N) {g : Cost.PolyTimeFun (PrfIn × Cost.BitStr) Cost.Unary} (gs : Slot L) (hg : g.toFun (inp, z) = Cost.unary (idxO gs)) {wire pos : Cost.PolyTimeFun (Cost.Unary × PrfIn × Cost.BitStr) Cost.Unary} {k : Cost.PolyTimeFun (PrfIn × Cost.BitStr) Cost.Unary} {n : ℕ} (hk : k.toFun (inp, z) = Cost.unary n) (we : Fin n → Fin L.m) (β : Fin n → Slot L) (hw : ∀ (i : Fin n), wire.toFun (Cost.unary ↑i, inp, z) = Cost.unary ↑(we i)) (hp : ∀ (i : Fin n), pos.toFun (Cost.unary ↑i, inp, z) = Cost.unary (idxO (β i))) : (asgEqF g (eqTermF wire pos) k).toFun (inp, z) = (SAT.shoupBinField t ht).toBits ((certLin ∘ₗ Intro.fldAt t ht N (o + idxO gs * t) - ∑ i : Fin n, mulL (q (we i) * (1 - q (we i))) ∘ₗ Intro.fldAt t ht N (o + idxO (β i) * t)) (Intro.bitVec N z))

theorem MIPRE.Tailored.AnsRed.Typed.sgnCoefF_eq {t : ℕ} {ht : 1 ≤ t} {j d : ℕ} {L : PcpDims} {e : Cost.Data} {inp : PrfIn} (hP : rP.toFun inp = arParams t j d L e) {o : ℕ} (hO : rO.toFun inp = Cost.unary o) {q : Fin L.m → Fq t ht} (hpts : ∀ (X : Fin L.m), (rPts.toFun inp).getD ↑X [] = (SAT.shoupBinField t ht).toBits (q X)) {J : Type} [Cost.SizedEncoding J] {ρ : Cost.PolyTimeFun J PrfIn} {x : J} (hx : ρ.toFun x = inp) (k : Fin 6) : (sgnCoefF ρ ↑k).toFun x = (SAT.shoupBinField t ht).toBits (vals t ht j d L (rA.toFun inp) Slot.gO * q (L.vO (L.oSgn k)))

noncomputable def MIPRE.Tailored.AnsRed.Typed.asgLin {t : ℕ} {ht : 1 ≤ t} (L : PcpDims) (N o : ℕ) (q : Fin L.m → Fq t ht) {n : ℕ} (we : Fin n → Fin L.m) (g : Slot L) (β : Fin n → Slot L) : (Fin N → ZMod 2) →ₗ[ZMod 2] Fq t ht

The linear map of an assignment equation at offset o of N answer bits: g (1 - g) minus the sum of x_{e_i} (1 - x_{e_i}) β_i.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.sysLin {t : ℕ} {ht : 1 ≤ t} (L : PcpDims) (N o : ℕ) (q : Fin L.m → Fq t ht) (wO : Fq t ht) : (Fin N → ZMod 2) →ₗ[ZMod 2] Fq t ht

The linear map of the system equation at offset o of N answer bits.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.proofEqs_eq {t : ℕ} {ht : 1 ≤ t} {L : PcpDims} (N o : ℕ) (wO : Fq t ht) (q : Fin L.m → Fq t ht) : proofEqs L N o wO q = [(sysLin L N o q wO, wO * q (L.vO (L.oSgn 5))), (asgLin L N o q (L.vO ∘ L.oA) Slot.gLa Slot.βLa, 0), (asgLin L N o q (L.vO ∘ L.oB) Slot.gLb Slot.βLb, 0), (asgLin L N o q (L.vO ∘ L.oL 0) (Slot.gL 0) (Slot.βL 0), 0), (asgLin L N o q (L.vO ∘ L.oL 1) (Slot.gL 1) (Slot.βL 1), 0), (asgLin L N o q (L.vO ∘ L.oL 2) (Slot.gL 2) (Slot.βL 2), 0)]

The proof check's equations, listed.

theorem MIPRE.Tailored.AnsRed.Typed.sysEqF_eq {t : ℕ} {ht : 1 ≤ t} {j d : ℕ} {L : PcpDims} {e : Cost.Data} {inp : PrfIn} (hP : rP.toFun inp = arParams t j d L e) {o N : ℕ} (hO : rO.toFun inp = Cost.unary o) {q : Fin L.m → Fq t ht} (hpts : ∀ (X : Fin L.m), (rPts.toFun inp).getD ↑X [] = (SAT.shoupBinField t ht).toBits (q X)) {z : Cost.BitStr} (hz : List.length z ≤ N) : sysEqF.toFun (inp, z) = (SAT.shoupBinField t ht).toBits ((sysLin L N o q (vals t ht j d L (rA.toFun inp) Slot.gO)) (Intro.bitVec N z))

The system equation's program computes its value.

theorem MIPRE.Tailored.AnsRed.Typed.proofEqsF_eq {t : ℕ} {ht : 1 ≤ t} {j d : ℕ} {L : PcpDims} {e : Cost.Data} {inp : PrfIn} (hP : rP.toFun inp = arParams t j d L e) {o N : ℕ} (hO : rO.toFun inp = Cost.unary o) (hN : rN.toFun inp = Cost.unary N) {q : Fin L.m → Fq t ht} (hpts : ∀ (X : Fin L.m), (rPts.toFun inp).getD ↑X [] = (SAT.shoupBinField t ht).toBits (q X)) : proofEqsF.toFun inp = eqsCons t ht (proofEqs L N o (vals t ht j d L (rA.toFun inp) Slot.gO) q)

The proof check's equations, as a program.

noncomputable def MIPRE.Tailored.AnsRed.Typed.proofConsF : Cost.PolyTimeFun PrfIn (List Cost.BitStr)

The proof check, as a program: the readable checks as a guard, then the equations.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.proofConsF_eq {t : ℕ} {ht : 1 ≤ t} {j d : ℕ} {L : PcpDims} {e : Cost.Data} {inp : PrfIn} (hP : rP.toFun inp = arParams t j d L e) {o N : ℕ} (hO : rO.toFun inp = Cost.unary o) (hN : rN.toFun inp = Cost.unary N) {q : Fin L.m → Fq t ht} (hpts : ∀ (X : Fin L.m), (rPts.toFun inp).getD ↑X [] = (SAT.shoupBinField t ht).toBits (q X)) (C : SAT.Circuit) (hC : C.WellFormed) (hm : C.inputs + C.size = L.m) (hin : C.inputs = L.nIn) (hs : C.size = L.s) (hG : rG.toFun inp = C.gates) {hLM : L.m ≤ 2 ^ j} {p : Fin (2 ^ j) → Fq t ht} (hq : ptm L hLM p = q) : proofConsF.toFun inp = proofCons j d L hLM N o ((MvPolynomial.rename (Fin.cast hm)) C.finiteArith) p (rA.toFun inp)

The proof check's program computes proofCons, at the oracle's point answer at offset o of N answer bits, for a well-formed circuit with the PCP's numbers of inputs and gates.