A uniform effective step of the binary Artin–Schreier tower

def MIPRE.LowDegree.BinaryArtinSchreier.rootVectorBits (p : Cost.BitStr) : Cost.BitStr

The canonical quotient root, computed by multiplying the encoded unit by X.

Equations

• MIPRE.LowDegree.BinaryArtinSchreier.rootVectorBits p = MIPRE.LowDegree.BinaryPolynomial.shiftReduce p (MIPRE.LowDegree.BinaryPolynomial.oneBits p)

@[simp]

theorem MIPRE.LowDegree.BinaryArtinSchreier.rootVectorBits_length (p : Cost.BitStr) : List.length (rootVectorBits p) = List.length p

theorem MIPRE.LowDegree.BinaryArtinSchreier.evalBits_rootVectorBits {R : Type u_1} [CommRing R] [CharP R 2] (z : R) (p : Cost.BitStr) (hp : p ≠ []) (hz : z ^ List.length p = BinaryPolynomial.evalBits z p) : BinaryPolynomial.evalBits z (rootVectorBits p) = z

def MIPRE.LowDegree.BinaryArtinSchreier.cubicParameterBits (p : Cost.BitStr) : Cost.BitStr

The uniform parameter α³ + α² in the supplied quotient.

Equations

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

@[simp]

theorem MIPRE.LowDegree.BinaryArtinSchreier.cubicParameterBits_length (p : Cost.BitStr) : List.length (cubicParameterBits p) = List.length p

theorem MIPRE.LowDegree.BinaryArtinSchreier.evalBits_cubicParameterBits {R : Type u_1} [CommRing R] [CharP R 2] (z : R) (p : Cost.BitStr) (hp : p ≠ []) (hz : z ^ List.length p = BinaryPolynomial.evalBits z p) : BinaryPolynomial.evalBits z (cubicParameterBits p) = z ^ 3 + z ^ 2

noncomputable def MIPRE.LowDegree.BinaryArtinSchreier.rootVectorBitsProg : Cost.PolyTimeFun Cost.BitStr Cost.BitStr

Equations

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

noncomputable def MIPRE.LowDegree.BinaryArtinSchreier.cubicParameterBitsProg : Cost.PolyTimeFun Cost.BitStr Cost.BitStr

Equations

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

@[simp]

theorem MIPRE.LowDegree.BinaryArtinSchreier.rootVectorBitsProg_apply (p : Cost.BitStr) : rootVectorBitsProg.toFun p = rootVectorBits p

@[simp]

theorem MIPRE.LowDegree.BinaryArtinSchreier.cubicParameterBitsProg_apply (p : Cost.BitStr) : cubicParameterBitsProg.toFun p = cubicParameterBits p

def MIPRE.LowDegree.BinaryArtinSchreier.towerStepBits (p : Cost.BitStr) : Cost.BitStr

Form the parameter's complete Frobenius product and substitute X² + X.

Equations

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

noncomputable def MIPRE.LowDegree.BinaryArtinSchreier.towerStepBitsProg : Cost.PolyTimeFun Cost.BitStr Cost.BitStr

A single ambient program for one tower step, valid also on malformed moduli.

Equations

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

@[simp]

theorem MIPRE.LowDegree.BinaryArtinSchreier.towerStepBitsProg_apply (p : Cost.BitStr) : towerStepBitsProg.toFun p = towerStepBits p

def MIPRE.LowDegree.BinaryArtinSchreier.parameterOrbitBits (p : Cost.BitStr) : Cost.BitStr

The coefficient list of the parameter's complete old-field Frobenius product.

Equations

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

@[simp]

theorem MIPRE.LowDegree.BinaryArtinSchreier.parameterOrbitBits_length (p : Cost.BitStr) : List.length (parameterOrbitBits p) = List.length p + 1

@[instance_reducible]

noncomputable def MIPRE.LowDegree.BinaryArtinSchreier.quotientFintype (p : Cost.BitStr) : Fintype (AdjoinRoot (polyOfBits (p ++ [true])))

Equations

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

theorem MIPRE.LowDegree.BinaryArtinSchreier.quotientFiniteDimensional (p : Cost.BitStr) : Module.Finite (ZMod 2) (AdjoinRoot (polyOfBits (p ++ [true])))

theorem MIPRE.LowDegree.BinaryArtinSchreier.quotientCharP (p : Cost.BitStr) [Fact (Irreducible (polyOfBits (p ++ [true])))] : CharP (AdjoinRoot (polyOfBits (p ++ [true]))) 2

theorem MIPRE.LowDegree.BinaryArtinSchreier.quotient_finrank (p : Cost.BitStr) : Module.finrank (ZMod 2) (AdjoinRoot (polyOfBits (p ++ [true]))) = List.length p

theorem MIPRE.LowDegree.BinaryArtinSchreier.quotient_pow_card (p : Cost.BitStr) [Fact (Irreducible (polyOfBits (p ++ [true])))] (x : AdjoinRoot (polyOfBits (p ++ [true]))) : x ^ 2 ^ List.length p = x

theorem MIPRE.LowDegree.BinaryArtinSchreier.parameterOrbitBits_spec (p : Cost.BitStr) [Fact (Irreducible (polyOfBits (p ++ [true])))] (hp : p ≠ []) : (polyOfBits (parameterOrbitBits p)).Monic ∧ (polyOfBits (parameterOrbitBits p)).natDegree = List.length p ∧ (Polynomial.aeval (AdjoinRoot.root (polyOfBits (p ++ [true])) ^ 3 + AdjoinRoot.root (polyOfBits (p ++ [true])) ^ 2)) (polyOfBits (parameterOrbitBits p)) = 0

The descended complete orbit is monic of the old field degree and annihilates its cubic parameter; repeated conjugates cause no difficulty.

theorem MIPRE.LowDegree.BinaryArtinSchreier.towerStepBits_irreducible (p : Cost.BitStr) [Fact (Irreducible (polyOfBits (p ++ [true])))] (t : ℕ) (hd : List.length p = 2 ^ t) (hc : Irreducible (quadratic (AdjoinRoot.root (polyOfBits (p ++ [true])) ^ 3 + AdjoinRoot.root (polyOfBits (p ++ [true])) ^ 2))) : Irreducible (polyOfBits (towerStepBits p))

One valid power-of-two tower stage gives the next irreducible flat binary polynomial.

theorem MIPRE.LowDegree.BinaryArtinSchreier.towerStepBits_monic_natDegree (p : Cost.BitStr) [Fact (Irreducible (polyOfBits (p ++ [true])))] (hp : p ≠ []) : (polyOfBits (towerStepBits p)).Monic ∧ (polyOfBits (towerStepBits p)).natDegree = 2 * List.length p

The normalized step output has exactly the doubled degree plus its leading bit.

theorem MIPRE.LowDegree.BinaryArtinSchreier.towerStepBits_cubic (p : Cost.BitStr) [Fact (Irreducible (polyOfBits (p ++ [true])))] (t : ℕ) (hd : List.length p = 2 ^ t) (hc : Irreducible (quadratic (AdjoinRoot.root (polyOfBits (p ++ [true])) ^ 3 + AdjoinRoot.root (polyOfBits (p ++ [true])) ^ 2))) : have this := ⋯; Irreducible (quadratic (AdjoinRoot.root (polyOfBits (towerStepBits p)) ^ 3 + AdjoinRoot.root (polyOfBits (towerStepBits p)) ^ 2))

The effective flat step preserves the invariant for its canonical quotient root.

theorem MIPRE.LowDegree.BinaryArtinSchreier.towerStepBits_getLast (p : Cost.BitStr) [Fact (Irreducible (polyOfBits (p ++ [true])))] (hp : p ≠ []) : List.getLastD (towerStepBits p) false = true

Normalization leaves a true leading bit on every valid step output.

theorem MIPRE.LowDegree.BinaryArtinSchreier.towerStepBits_length (p : Cost.BitStr) [Fact (Irreducible (polyOfBits (p ++ [true])))] (hp : p ≠ []) : List.length (towerStepBits p) = 2 * List.length p + 1

A valid step has doubled lower-coefficient width.

theorem MIPRE.LowDegree.BinaryArtinSchreier.initial_polynomial : polyOfBits [true, true, true] = quadratic 1

The seed is the specified degree-two polynomial.

structure MIPRE.LowDegree.BinaryArtinSchreier.TowerInvariant (p : Cost.BitStr) (t : ℕ) : Prop

A valid stage records the exact power-of-two width and the cubic no-root invariant.

• width : List.length p = 2 ^ (t + 1)
• irreducible : Irreducible (polyOfBits (p ++ [true]))
• cubic : let this := ⋯; Irreducible (quadratic (AdjoinRoot.root (polyOfBits (p ++ [true])) ^ 3 + AdjoinRoot.root (polyOfBits (p ++ [true])) ^ 2))

theorem MIPRE.LowDegree.BinaryArtinSchreier.initial_invariant : TowerInvariant [true, true] 0

The initial stage satisfies the reusable tower invariant.

theorem MIPRE.LowDegree.BinaryArtinSchreier.towerStep_invariant (p : Cost.BitStr) (t : ℕ) (h : TowerInvariant p t) : TowerInvariant (List.dropLast (towerStepBits p)) (t + 1)

Dropping the normalized leading bit prepares the next supplied modulus.