Documentation

MIPRE.TM.CookLevin.ExactPadding

Exact-size padded succinct descriptions #

The common input width is a power of two, and the number of input and gate variables is a second power of two. Circuit construction consumes a unary gate budget: the target size can be polynomial in the value of Q and σ, so printing it is not polynomial in their binary encodings alone. The PCP view will supply this budget. Parameter computation is a separate obligation.

source
noncomputable def MIPRE.TM.CookLevin.Pad.outerDim (n T Q σ : ℕ) :
ℕ

The outer power-of-two variable count, including enough spare gates.

Equations
Instances For
    source
    noncomputable def MIPRE.TM.CookLevin.Pad.gateCount (n T Q σ : ℕ) :
    ℕ

    The exact number of gates.

    Equations
    Instances For
      source
      theorem MIPRE.TM.CookLevin.Pad.outerDim_isPow (n T Q σ : ℕ) :
      ∃ (j : ℕ), outerDim n T Q σ = 2 ^ j
      source
      theorem MIPRE.TM.CookLevin.Pad.innerDim_add_bound_le_gateCount (n T Q σ : ℕ) :
      innerDim T σ + Desc.roundUp gatePoly n T Q σ ≤ gateCount n T Q σ
      source
      theorem MIPRE.TM.CookLevin.Pad.inputs_add_gateCount (n T Q σ : ℕ) :
      5 * innerDim T σ + 5 + gateCount n T Q σ = outerDim n T Q σ
      source
      theorem MIPRE.TM.CookLevin.Pad.outerDim_polynomial :
      ∃ (P : Polynomial ℕ), ∀ (n T Q σ : ℕ), outerDim n T Q σ ≤ Polynomial.eval (Desc.LOf n T Q σ) P

      Both dimensions have a polynomial bound in the source runtime parameter.

      source
      noncomputable def MIPRE.TM.CookLevin.Pad.describeExact :
      Cost.PolyTimeFun (SAT.DescInput × Cost.Unary) SAT.Circuit

      Add gates up to the supplied budget. A too-small budget leaves the circuit unchanged; it never triggers an unbounded unary expansion.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem MIPRE.TM.CookLevin.Pad.describeExact_apply (p : SAT.DescInput) (u : Cost.Unary) :
        describeExact.toFun (p, u) = (describe.toFun p).padGates (List.length u - (describe.toFun p).size)
        source
        theorem MIPRE.TM.CookLevin.Pad.describeExact_wellFormed (p : SAT.DescInput) (u : Cost.Unary) :
        (describeExact.toFun (p, u)).WellFormed
        source
        theorem MIPRE.TM.CookLevin.Pad.describeExact_size (p : SAT.DescInput) (u : Cost.Unary) (h : (describe.toFun p).size ≤ List.length u) :
        (describeExact.toFun (p, u)).size = List.length u
        source
        theorem MIPRE.TM.CookLevin.Pad.describeExact_inputs (p : SAT.DescInput) (u : Cost.Unary) :
        (describeExact.toFun (p, u)).inputs = 5 * innerDim p.1.2.2.1 p.1.2.2.2.2 + 5
        source
        theorem MIPRE.TM.CookLevin.Pad.describeExact_formula5 (p : SAT.DescInput) (u : Cost.Unary) (ℓ r : ℕ) :
        (describeExact.toFun (p, u)).formula5 ℓ r = (describe.toFun p).formula5 ℓ r
        source
        theorem MIPRE.TM.CookLevin.Pad.describeExact_describes (D : Decider) (n T Q σ : ℕ) (x y : Cost.BitStr) (hV : SAT.Valid D.prog n T Q σ x y) (u : Cost.Unary) :
        (describeExact.toFun (((D.prog, n, T, Q, σ), x, y), u)).DescribesDecider (innerDim T σ) (innerDim T σ) D n x y T

        The exact-size circuit describes the same accepting answer prefixes.

        source
        theorem MIPRE.TM.CookLevin.Pad.describeExact_gateCount (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) (hV : SAT.Valid D n T Q σ x y) (u : Cost.Unary) (hu : List.length u = gateCount n T Q σ) :
        (describeExact.toFun (((D, n, T, Q, σ), x, y), u)).size = gateCount n T Q σ

        The intended budget yields exactly the advertised gate count.

        source
        theorem MIPRE.TM.CookLevin.Pad.describeExact_variables (D : Cost.Prog) (n T Q σ : ℕ) (x y : Cost.BitStr) (hV : SAT.Valid D n T Q σ x y) (u : Cost.Unary) (hu : List.length u = gateCount n T Q σ) :
        (describeExact.toFun (((D, n, T, Q, σ), x, y), u)).inputs + (describeExact.toFun (((D, n, T, Q, σ), x, y), u)).size = outerDim n T Q σ

        Input and gate variables together have the exact outer power-of-two count.