The bounded power-of-two constructor

The input is the requested degree in unary. The loop caps all intermediate moduli by this input degree, including on malformed states. The unbounded mathematical stage sequence below is used only to state the induction proof.

def MIPRE.LowDegree.BinaryArtinSchreier.stage : ℕ → Cost.BitStr

The mathematical sequence used to prove the bounded loop correct.

Equations

• MIPRE.LowDegree.BinaryArtinSchreier.stage 0 = [true, true]
• MIPRE.LowDegree.BinaryArtinSchreier.stage t.succ = List.dropLast (MIPRE.LowDegree.BinaryArtinSchreier.towerStepBits (MIPRE.LowDegree.BinaryArtinSchreier.stage t))

theorem MIPRE.LowDegree.BinaryArtinSchreier.stage_invariant (t : ℕ) : TowerInvariant (stage t) t

@[reducible, inline]

abbrev MIPRE.LowDegree.BinaryArtinSchreier.TowerState : Type

Target degree in unary and the current lower coefficients.

Equations

• MIPRE.LowDegree.BinaryArtinSchreier.TowerState = (MIPRE.Cost.Unary × MIPRE.Cost.BitStr)

def MIPRE.LowDegree.BinaryArtinSchreier.cappedStep (s : TowerState) : TowerState

Grow only below the target, and cap every replacement by the target width.

Equations

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

noncomputable def MIPRE.LowDegree.BinaryArtinSchreier.isEmptyUnaryProg : Cost.PolyTimeFun Cost.Unary Bool

Equations

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

noncomputable def MIPRE.LowDegree.BinaryArtinSchreier.cappedStepProg : Cost.PolyTimeFun TowerState TowerState

One uniform capped step, including its unary stopping test.

Equations

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

@[simp]

theorem MIPRE.LowDegree.BinaryArtinSchreier.cappedStepProg_apply (s : TowerState) : cappedStepProg.toFun s = cappedStep s

theorem MIPRE.LowDegree.BinaryArtinSchreier.cappedStep_width (s : TowerState) : (cappedStep s).1 = s.1 ∧ List.length (cappedStep s).2 ≤ max (List.length s.2) (List.length s.1)

theorem MIPRE.LowDegree.BinaryArtinSchreier.fold_cappedStep_width (u : Cost.Unary) (s : TowerState) : (List.foldl (fun (s : TowerState) (x : Unit) => cappedStep s) s u).1 = s.1 ∧ List.length (List.foldl (fun (s : TowerState) (x : Unit) => cappedStep s) s u).2 ≤ max (List.length s.2) (List.length s.1)

theorem MIPRE.LowDegree.BinaryArtinSchreier.cappedStep_bounded : (cappedStepProg.comp Cost.PolyTimeFun.fst).FoldBounded (6 * Polynomial.X + 6)

noncomputable def MIPRE.LowDegree.BinaryArtinSchreier.towerLoopProg : Cost.PolyTimeFun (Cost.Unary × TowerState) TowerState

Run a polynomially bounded number of capped tower steps.

Equations

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

@[simp]

theorem MIPRE.LowDegree.BinaryArtinSchreier.towerLoopProg_apply (u : Cost.Unary) (s : TowerState) : towerLoopProg.toFun (u, s) = List.foldl (fun (s : TowerState) (x : Unit) => cappedStep s) s u

theorem MIPRE.LowDegree.BinaryArtinSchreier.fold_cappedStep (u : Cost.Unary) (s : TowerState) : List.foldl (fun (s : TowerState) (x : Unit) => cappedStep s) s u = cappedStep^[List.length u] s

def MIPRE.LowDegree.BinaryArtinSchreier.powerTwoBits (u : Cost.Unary) : Cost.BitStr

Return the degree-one polynomial for unary zero or one, otherwise run the capped tower.

Equations

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

noncomputable def MIPRE.LowDegree.BinaryArtinSchreier.powerTwoBitsProg : Cost.PolyTimeFun Cost.Unary Cost.BitStr

A fixed ambient polynomial-time program on the requested degree, not its logarithm.

Equations

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

@[simp]

theorem MIPRE.LowDegree.BinaryArtinSchreier.powerTwoBitsProg_apply (u : Cost.Unary) : powerTwoBitsProg.toFun u = powerTwoBits u

theorem MIPRE.LowDegree.BinaryArtinSchreier.cappedStep_stage (u : Cost.Unary) (t : ℕ) (h : 2 ^ (t + 1 + 1) ≤ List.length u) : cappedStep (u, stage t) = (u, stage (t + 1))

theorem MIPRE.LowDegree.BinaryArtinSchreier.iterate_cappedStep_stage (u : Cost.Unary) (t : ℕ) (h : 2 ^ (t + 1) ≤ List.length u) : cappedStep^[t] (u, [true, true]) = (u, stage t)

theorem MIPRE.LowDegree.BinaryArtinSchreier.cappedStep_stage_fixed (u : Cost.Unary) (t : ℕ) (h : List.length u = 2 ^ (t + 1)) : cappedStep (u, stage t) = (u, stage t)

theorem MIPRE.LowDegree.BinaryArtinSchreier.iterate_cappedStep_finished (u : Cost.Unary) (t : ℕ) (h : List.length u = 2 ^ (t + 1)) : cappedStep^[List.length u] (u, [true, true]) = (u, stage t)

theorem MIPRE.LowDegree.BinaryArtinSchreier.powerTwoBits_succ (t : ℕ) : powerTwoBits (Cost.unary (2 ^ (t + 1))) = stage t ++ [true]

The complete constructor returns the chosen stage on every positive tower level.

theorem MIPRE.LowDegree.BinaryArtinSchreier.powerTwoBits_getLast (u : Cost.Unary) : List.getLastD (powerTwoBits u) false = true

Every output is in canonical nonzero coefficient form.

theorem MIPRE.LowDegree.BinaryArtinSchreier.powerTwoBits_correct (e : ℕ) : (polyOfBits (powerTwoBits (Cost.unary (2 ^ e)))).Monic ∧ Irreducible (polyOfBits (powerTwoBits (Cost.unary (2 ^ e)))) ∧ (polyOfBits (powerTwoBits (Cost.unary (2 ^ e)))).natDegree = 2 ^ e

The globally polynomial-time program constructs a monic irreducible binary polynomial of every requested power-of-two degree, including degree one.

theorem MIPRE.LowDegree.BinaryArtinSchreier.powerTwoBits_length (e : ℕ) : List.length (powerTwoBits (Cost.unary (2 ^ e))) = 2 ^ e + 1

The printed canonical coefficient list has the expected size.