Deterministic binary polynomial gcd

Euclidean division decreases the canonical divisor width. The original divisor list supplies the iteration budget, and a zero-divisor state is absorbing. The same width bound holds for malformed states, so the ambient program has a global polynomial bound rather than a promise only on well-formed inputs.

@[reducible, inline]

abbrev MIPRE.LowDegree.BinaryPolynomial.GCDState : Type

Two successive remainders in the Euclidean algorithm.

Equations

• MIPRE.LowDegree.BinaryPolynomial.GCDState = (MIPRE.Cost.BitStr × MIPRE.Cost.BitStr)

def MIPRE.LowDegree.BinaryPolynomial.gcdStep (s : GCDState) : Bool → GCDState

One bounded Euclidean iteration; its second input serves only as fuel.

Equations

• MIPRE.LowDegree.BinaryPolynomial.gcdStep s x✝ = if List.isEmpty s.2 = true then s else (s.2, (MIPRE.LowDegree.BinaryPolynomial.divModBits (List.dropLast s.2) s.1).2)

theorem MIPRE.LowDegree.BinaryPolynomial.gcdStep_second_length (s : GCDState) (b : Bool) : List.length (gcdStep s b).2 ≤ List.length s.2 - 1

The divisor width decreases on every nonterminal step, even on malformed states.

theorem MIPRE.LowDegree.BinaryPolynomial.gcdStep_width (s : GCDState) (b : Bool) : max (List.length (gcdStep s b).1) (List.length (gcdStep s b).2) ≤ max (List.length s.1) (List.length s.2)

Both state components stay within the original maximum width.

theorem MIPRE.LowDegree.BinaryPolynomial.fold_gcdStep_width (l : Cost.BitStr) (s : GCDState) : max (List.length (List.foldl gcdStep s l).1) (List.length (List.foldl gcdStep s l).2) ≤ max (List.length s.1) (List.length s.2)

An entire bounded loop retains the original width bound.

theorem MIPRE.LowDegree.BinaryPolynomial.fold_gcdStep_second_length (l : Cost.BitStr) (s : GCDState) : List.length (List.foldl gcdStep s l).2 ≤ List.length s.2 - List.length l

Each fuel bit removes one possible remaining divisor coefficient.

theorem MIPRE.LowDegree.BinaryPolynomial.normalize_polyOfBits (a : Cost.BitStr) : normalize (polyOfBits a) = polyOfBits a

Binary polynomials are already normalized as elements of the gcd monoid.

theorem MIPRE.LowDegree.BinaryPolynomial.gcdStep_correct (s : GCDState) (b : Bool) (hs : s.2 = [] ∨ List.getLastD s.2 false = true) : gcd (polyOfBits (gcdStep s b).1) (polyOfBits (gcdStep s b).2) = gcd (polyOfBits s.1) (polyOfBits s.2) ∧ ((gcdStep s b).2 = [] ∨ List.getLastD (gcdStep s b).2 false = true)

Each division step preserves the polynomial gcd and the canonical-divisor invariant.

theorem MIPRE.LowDegree.BinaryPolynomial.fold_gcdStep_correct (l : Cost.BitStr) (s : GCDState) (hs : s.2 = [] ∨ List.getLastD s.2 false = true) : gcd (polyOfBits (List.foldl gcdStep s l).1) (polyOfBits (List.foldl gcdStep s l).2) = gcd (polyOfBits s.1) (polyOfBits s.2)

The complete Euclidean loop preserves the polynomial gcd.

def MIPRE.LowDegree.BinaryPolynomial.gcdBits (a b : Cost.BitStr) : Cost.BitStr

The binary Euclidean algorithm uses one iteration per original divisor bit.

Equations

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

theorem MIPRE.LowDegree.BinaryPolynomial.polyOfBits_gcdBits (a b : Cost.BitStr) : polyOfBits (gcdBits a b) = gcd (polyOfBits a) (polyOfBits b)

The executable algorithm computes Mathlib's normalized polynomial gcd.

theorem MIPRE.LowDegree.BinaryPolynomial.fold_gcdStep_canonical (l : Cost.BitStr) (s : GCDState) (ha : s.1 = [] ∨ List.getLastD s.1 false = true) (hb : s.2 = [] ∨ List.getLastD s.2 false = true) : ((List.foldl gcdStep s l).1 = [] ∨ List.getLastD (List.foldl gcdStep s l).1 false = true) ∧ ((List.foldl gcdStep s l).2 = [] ∨ List.getLastD (List.foldl gcdStep s l).2 false = true)

Both Euclidean state entries retain a canonical binary representation.

theorem MIPRE.LowDegree.BinaryPolynomial.gcdBits_canonical (a b : Cost.BitStr) : gcdBits a b = [] ∨ List.getLastD (gcdBits a b) false = true

The gcd output has no trailing zero coefficient.

theorem MIPRE.LowDegree.BinaryPolynomial.gcdBits_width (a b : Cost.BitStr) : List.length (gcdBits a b) ≤ max (List.length a) (List.length b)

Output width is bounded by the larger input representation.

noncomputable def MIPRE.LowDegree.BinaryPolynomial.isEmptyRemProg : Cost.PolyTimeFun Cost.BitStr Bool

Equations

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

noncomputable def MIPRE.LowDegree.BinaryPolynomial.tailBitsProg : Cost.PolyTimeFun Cost.BitStr Cost.BitStr

Equations

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

noncomputable def MIPRE.LowDegree.BinaryPolynomial.dropLastBitsProg : Cost.PolyTimeFun Cost.BitStr Cost.BitStr

Remove the implicit leading coefficient before passing a canonical divisor to division.

Equations

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

@[simp]

theorem MIPRE.LowDegree.BinaryPolynomial.dropLastBitsProg_apply (a : Cost.BitStr) : dropLastBitsProg.toFun a = List.dropLast a

noncomputable def MIPRE.LowDegree.BinaryPolynomial.gcdStepProg : Cost.PolyTimeFun (GCDState × Bool) GCDState

Equations

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

theorem MIPRE.LowDegree.BinaryPolynomial.gcdStep_bounded : gcdStepProg.FoldBounded (10 * Polynomial.X + 10)

noncomputable def MIPRE.LowDegree.BinaryPolynomial.gcdBitsProg : Cost.PolyTimeFun (Cost.BitStr × Cost.BitStr) Cost.BitStr

A fixed deterministic ambient program for binary polynomial gcd.

Equations

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

@[simp]

theorem MIPRE.LowDegree.BinaryPolynomial.gcdBitsProg_apply (a b : Cost.BitStr) : gcdBitsProg.toFun (a, b) = gcdBits a b