Effective parameters for exact succinct padding

Both dimensions and the exact gate count are computed from binary parameters in polynomial time in their bit lengths. Only the logarithmically bounded inner dimension is expanded to unary; the much larger gate count stays binary.

@[reducible, inline]

abbrev MIPRE.TM.CookLevin.Pad.ParamInput : Type

Equations

• MIPRE.TM.CookLevin.Pad.ParamInput = (ℕ × ℕ × ℕ × ℕ)

noncomputable def MIPRE.TM.CookLevin.Pad.innerDimParamsU : Cost.PolyTimeFun ParamInput Cost.Unary

Compute the common input width in unary from the four binary parameters.

Equations

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

theorem MIPRE.TM.CookLevin.Pad.innerDimParamsU_length (p : ParamInput) : List.length (innerDimParamsU.toFun p) = innerDim p.2.1 p.2.2.2

noncomputable def MIPRE.TM.CookLevin.Pad.outerDimProg : Cost.PolyTimeFun ParamInput ℕ

Binary computation of the outer power-of-two dimension.

Equations

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

theorem MIPRE.TM.CookLevin.Pad.outerDimProg_apply (p : ParamInput) : outerDimProg.toFun p = outerDim p.1 p.2.1 p.2.2.1 p.2.2.2

noncomputable def MIPRE.TM.CookLevin.Pad.gateCountProg : Cost.PolyTimeFun ParamInput ℕ

Binary computation of the exact gate count.

Equations

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

theorem MIPRE.TM.CookLevin.Pad.gateCountProg_apply (p : ParamInput) : gateCountProg.toFun p = gateCount p.1 p.2.1 p.2.2.1 p.2.2.2

noncomputable def MIPRE.TM.CookLevin.Pad.paddingParams : Cost.PolyTimeFun ParamInput (ℕ × ℕ)

The two padded-describer parameters, with an ambient polynomial-time program.

Equations

• MIPRE.TM.CookLevin.Pad.paddingParams = (MIPRE.Cost.PolyTimeFun.unaryToBin.comp MIPRE.TM.CookLevin.Pad.innerDimParamsU).pair MIPRE.TM.CookLevin.Pad.gateCountProg

theorem MIPRE.TM.CookLevin.Pad.paddingParams_apply (p : ParamInput) : paddingParams.toFun p = (innerDim p.2.1 p.2.2.2, gateCount p.1 p.2.1 p.2.2.1 p.2.2.2)