A polynomial-time square root in the binary cyclic group algebra

For an odd-length coefficient vector, reading the doubled indices means reading the even positions followed by the odd positions. Splitting those two lists and appending them is polynomial-time in the ambient cost model. This implements the square-root step of self-dualization; it does not compute the inverse Gram element or the initial normal basis.

def MIPRE.LowDegree.splitParity {α : Type u_1} : List α → List α × List α

Split a list into its even-position and odd-position subsequences.

Equations

• MIPRE.LowDegree.splitParity [] = ([], [])
• MIPRE.LowDegree.splitParity (a :: l) = (a :: (MIPRE.LowDegree.splitParity l).2, (MIPRE.LowDegree.splitParity l).1)

theorem MIPRE.LowDegree.splitParity_eq_foldr {α : Type u_1} (l : List α) : splitParity l = List.foldr (fun (a : α) (s : List α × List α) => (a :: s.2, s.1)) ([], []) l

theorem MIPRE.LowDegree.length_splitParity {α : Type u_1} (l : List α) : (splitParity l).1.length = (l.length + 1) / 2 ∧ (splitParity l).2.length = l.length / 2

theorem MIPRE.LowDegree.getD_splitParity {α : Type u_1} (l : List α) (fallback : α) (n : ℕ) : (splitParity l).1.getD n fallback = l.getD (2 * n) fallback ∧ (splitParity l).2.getD n fallback = l.getD (2 * n + 1) fallback

def MIPRE.LowDegree.rootBits {α : Type u_1} (l : List α) : List α

The doubled-index permutation for an odd-length coefficient vector.

Equations

• MIPRE.LowDegree.rootBits l = (MIPRE.LowDegree.splitParity l).1 ++ (MIPRE.LowDegree.splitParity l).2

@[simp]

theorem MIPRE.LowDegree.length_rootBits {α : Type u_1} (l : List α) : (rootBits l).length = l.length

theorem MIPRE.LowDegree.getD_rootBits {α : Type u_1} (l : List α) (fallback : α) (hodd : Odd l.length) {i : ℕ} (hi : i < l.length) : (rootBits l).getD i fallback = l.getD ((i + i) % l.length) fallback

noncomputable def MIPRE.LowDegree.splitParityStep {α : Type u_1} [Cost.SizedEncoding α] : Cost.PolyTimeFun ((List α × List α) × α) (List α × List α)

Equations

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

theorem MIPRE.LowDegree.splitParityStep_size {α : Type u_1} [Cost.SizedEncoding α] (s : List α × List α) (a : α) : Cost.esize (splitParityStep.toFun (s, a)) ≤ Cost.esize s + Polynomial.eval (Cost.esize a) (Polynomial.X + 1)

noncomputable def MIPRE.LowDegree.splitParityProg {α : Type u_1} [Cost.SizedEncoding α] : Cost.PolyTimeFun (List α) (List α × List α)

The parity split, with an ambient program and polynomial cost proof.

Equations

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

@[simp]

theorem MIPRE.LowDegree.splitParityProg_apply {α : Type u_1} [Cost.SizedEncoding α] (l : List α) : splitParityProg.toFun l = splitParity l

noncomputable def MIPRE.LowDegree.rootBitsProg {α : Type u_1} [Cost.SizedEncoding α] : Cost.PolyTimeFun (List α) (List α)

The coefficient square-root permutation, in polynomial time.

Equations

• MIPRE.LowDegree.rootBitsProg = MIPRE.Cost.PolyTimeFun.append.comp MIPRE.LowDegree.splitParityProg

@[simp]

theorem MIPRE.LowDegree.rootBitsProg_apply {α : Type u_1} [Cost.SizedEncoding α] (l : List α) : rootBitsProg.toFun l = rootBits l

theorem MIPRE.LowDegree.rootBitsProg_time_le : ∃ (R : Polynomial ℕ), ∀ (l : Cost.BitStr), ∃ t ≤ Polynomial.eval (List.length l) R, rootBitsProg.code.Runs (Cost.encode l) (Cost.encode (rootBits l)) t

On bit vectors, the ambient running time is polynomial in the vector length.

noncomputable def MIPRE.LowDegree.groupOfBits {k : ℕ} [NeZero k] (l : Cost.BitStr) : AddMonoidAlgebra (ZMod 2) (ZMod k)

A binary coefficient list interpreted in the cyclic group algebra.

Equations

• MIPRE.LowDegree.groupOfBits l = AddMonoidAlgebra.ofCoeff (Finsupp.onFinset Finset.univ (fun (i : ZMod k) => MIPRE.LowDegree.ofBool (List.getD l i.val false)) ⋯)

@[simp]

theorem MIPRE.LowDegree.coeff_groupOfBits {k : ℕ} [NeZero k] (l : Cost.BitStr) (i : ZMod k) : (groupOfBits l).coeff i = ofBool (List.getD l i.val false)

theorem MIPRE.LowDegree.groupOfBits_rootBits {k : ℕ} [NeZero k] (l : Cost.BitStr) (hlen : List.length l = k) (hk : Odd k) : groupOfBits (rootBits l) = binarySquareRoot (groupOfBits l)

The implemented permutation agrees with the algebraic square-root formula.

theorem MIPRE.LowDegree.rootBitsProg_square {k : ℕ} [NeZero k] (l : Cost.BitStr) (hlen : List.length l = k) (hk : Odd k) : groupOfBits (rootBitsProg.toFun l) * groupOfBits (rootBitsProg.toFun l) = groupOfBits l

Correctness of the polynomial-time square-root program on odd-length vectors.