The circuit function of the answer reduction

Slice P4i of planning/aldous-lyons-track.md: the circuit function of the routine, in polynomial time (arCircF). From the input verifier's programs, the index, the parameters and a seed's two questions, it computes the window describer's description of the output indicator L* at the parameters (ℓ, ◇) — the windows ℓ + 1, ℓ + 1, oW + 1, the program of L* (from a polynomial-time builder B of L*'s program at constant parameters), T = 2^K, Q = ℓ and σ', read from the parameters' data — then pads it to the gate count s. At the routine's parameters it is the circuit Params.arCirc of the honest PCPs' hypotheses (arCircF_apply); it is well formed with the PCP's inputs and s gates (arCircF_wf, arCircF_inputs, arCircF_size).

noncomputable def MIPRE.Tailored.AnsRed.Typed.arCircF (B : Cost.PolyTimeFun ((Cost.Prog × Cost.Prog) × Cost.Unary × Cost.Unary) Cost.Prog) : Cost.PolyTimeFun CircIn SAT.Circuit

The circuit function, from a builder B of the output indicator's program.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.unary_add_one (k : ℕ) : Cost.unary k ++ Cost.unary 1 = Cost.unary (k + 1)

theorem MIPRE.Tailored.AnsRed.Typed.arCircF_apply {B : Cost.PolyTimeFun ((Cost.Prog × Cost.Prog) × Cost.Unary × Cost.Unary) Cost.Prog} (hB : ∀ (L P : Cost.Prog) (p : Cost.Unary × Cost.Unary), B.toFun ((L, P), p) = lstarProg (Cost.PolyTimeFun.const p) L P) (κ : Params.ArConsts) (V : Cost.Prog × Cost.Prog × Cost.Prog) (lam mu sigma n : ℕ) (x y : Cost.BitStr) : (arCircF B).toFun (V, (lam, mu, sigma), n, arParams (Params.pTw κ lam mu sigma n) (Params.pJ κ lam mu sigma n) Params.pD (Params.pL κ lam mu sigma n) (Params.pExtra κ lam mu sigma n), x, y) = Params.arCirc κ lam mu sigma n V.2.1 V.2.2 x y

At the routine's parameters, the circuit function computes Params.arCirc.

theorem MIPRE.Tailored.AnsRed.Typed.arCircF_wf {B : Cost.PolyTimeFun ((Cost.Prog × Cost.Prog) × Cost.Unary × Cost.Unary) Cost.Prog} (inp : CircIn) : ((arCircF B).toFun inp).WellFormed

theorem MIPRE.Tailored.AnsRed.Typed.arCircF_inputs {B : Cost.PolyTimeFun ((Cost.Prog × Cost.Prog) × Cost.Unary × Cost.Unary) Cost.Prog} (hB : ∀ (L P : Cost.Prog) (p : Cost.Unary × Cost.Unary), B.toFun ((L, P), p) = lstarProg (Cost.PolyTimeFun.const p) L P) (κ : Params.ArConsts) (V : Cost.Prog × Cost.Prog × Cost.Prog) (lam mu sigma n : ℕ) (x y : Cost.BitStr) : ((arCircF B).toFun (V, (lam, mu, sigma), n, arParams (Params.pTw κ lam mu sigma n) (Params.pJ κ lam mu sigma n) Params.pD (Params.pL κ lam mu sigma n) (Params.pExtra κ lam mu sigma n), x, y)).inputs = (Params.pL κ lam mu sigma n).nIn

theorem MIPRE.Tailored.AnsRed.Typed.arCircF_size {B : Cost.PolyTimeFun ((Cost.Prog × Cost.Prog) × Cost.Unary × Cost.Unary) Cost.Prog} (hB : ∀ (L P : Cost.Prog) (p : Cost.Unary × Cost.Unary), B.toFun ((L, P), p) = lstarProg (Cost.PolyTimeFun.const p) L P) (κ : Params.ArConsts) (V : Cost.Prog × Cost.Prog × Cost.Prog) (lam mu sigma n : ℕ) (x y : Cost.BitStr) : ((arCircF B).toFun (V, (lam, mu, sigma), n, arParams (Params.pTw κ lam mu sigma n) (Params.pJ κ lam mu sigma n) Params.pD (Params.pL κ lam mu sigma n) (Params.pExtra κ lam mu sigma n), x, y)).size = (Params.pL κ lam mu sigma n).s