Integer form of the regular lift

The generator's rational matrices are regular representations of matrices over the cyclotomic field CyclotomicRing.R e. Every regular-representation entry of a cyclotomic monomial is 0 or ±1, so after clearing the common denominator 2 ^ (e + 1) each lifted matrix entry is an explicit signed sum of integer monomials. This file defines that integer formula, proves it agrees with the rational lift, and bounds its entries. The integer matrices are computable and feed the executable generator.

Main definitions

• Rational.CyclotomicRing.signedEntry: the signed regular-representation coefficient of a power of the root of unity.
• Rational.IntegralTest.full, Rational.IntegralTest.padded: integer Taylor test matrices.
• Rational.IntegralLift.entry: the integer formula for a denominator-cleared lift entry.
• Rational.Generator.coordinate: the fixed row-major block coordinate.
• Rational.Generator.integerTest: the integer test matrices indexed by residues.
• Rational.Generator.integralLift: the denominator-cleared integer lift matrices.

Main results

• Rational.IntegralLift.entry_spec: the integer formula computes the scaled rational entry.
• Rational.Generator.U_cast: the integer lift is the scaled rational lift.
• Rational.Generator.U_bound: an explicit bound on the integer entries.
• Rational.Generator.tupleAt_integer: the generated tuples are normalized integer lifts.

References

• Adapted from OpenAI's formalization [OAI26a] at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a (file lean/OAI/Computability/RationalHitting/IntegralLift.lean), via the complexitylib port [Sch26d] at revision add0aca8ee0d71e68969f2cb45cf91554a50f787.

def Cslib.Circuits.Rational.CyclotomicRing.signedEntry (e : ℕ) (a : ZMod (dimension e)) (i j : Fin (degree e)) : ℤ

The signed coefficient of the cyclotomic regular representation.

def Cslib.Circuits.Rational.IntegralTest.full (M : ℕ) (a t : ℤ) : Matrix (Fin M) (Fin M) ℤ

Integer computation of the exact expanded Taylor-reversal matrix at t.

def Cslib.Circuits.Rational.IntegralTest.padded (M N : ℕ) (a t : ℤ) : Matrix (Fin M) (Fin M) ℤ

The integer Taylor test matrix with discarded columns set to zero.

theorem Cslib.Circuits.Rational.IntegralTest.coeff_bound (a : ℤ) (w M k j : ℕ) (hw : 1 ≤ w) (ha : |a| ≤ ↑w) (hk : k ≤ M) : |((Polynomial.X + Polynomial.C a) ^ k).coeff j| ≤ (2 * ↑w) ^ M

For |a| ≤ w with 1 ≤ w and k ≤ M, every coefficient of (X + C a) ^ k has absolute value at most (2 * w) ^ M.

theorem Cslib.Circuits.Rational.ThreeLift.eval_uni {K : Type u_1} [Field K] (x : Fin 3 → K) (p : Polynomial K) : (MvPolynomial.eval x) (uni p) = Polynomial.eval (x 0) p

Evaluating uni p on a three-variable tuple x evaluates p at x 0.

theorem Cslib.Circuits.Rational.ThreeLift.eval_lift {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) (R : Matrix (ZMod d) (ZMod d) (Polynomial K)) (x : Fin 3 → K) (i j : ZMod d) : (MvPolynomial.eval x) (lift χ R i j) = (↑d)⁻¹ * ∑ a : ZMod d, ∑ b : ZMod d, ∑ k : ZMod d, χ (-a * k) * Polynomial.eval (x 0) (R k (k - b)) * QuantumMatrices.weyl χ a b i j * x 1 ^ a.val * x 2 ^ b.val

Evaluating lift χ R i j at x expands to the Weyl-matrix character sum at x 0, x 1, x 2.

def Cslib.Circuits.Rational.IntegralLift.entry (e : ℕ) (T : Matrix (ZMod (CyclotomicRing.dimension e)) (ZMod (CyclotomicRing.dimension e)) ℤ) (p r : ℤ) (u v : ZMod (CyclotomicRing.dimension e)) (i j : Fin (CyclotomicRing.degree e)) : ℤ

The fixed signed-monomial integer formula for M times a regular lift entry.

theorem Cslib.Circuits.Rational.IntegralLift.entry_spec (e : ℕ) (P : Matrix (ZMod (CyclotomicRing.dimension e)) (ZMod (CyclotomicRing.dimension e)) (Polynomial (CyclotomicRing.R e))) (T : Matrix (ZMod (CyclotomicRing.dimension e)) (ZMod (CyclotomicRing.dimension e)) ℤ) (t p r : ℤ) (hT : ∀ (u v : ZMod (CyclotomicRing.dimension e)), Polynomial.eval (↑t) (P u v) = ↑(T u v)) (u v : ZMod (CyclotomicRing.dimension e)) (i j : Fin (CyclotomicRing.degree e)) : ↑(entry e T p r u v i j) = ↑(CyclotomicRing.dimension e) * (CyclotomicRing.rho e) ((MvPolynomial.eval ![↑t, ↑p, ↑r]) (ThreeLift.lift (CyclotomicRing.character e) P u v)) i j

The integer formula entry e T p r u v i j equals dimension e times the (i, j) regular representation entry of ThreeLift.lift (character e) P u v at (t, p, r).

def Cslib.Circuits.Rational.Generator.coordinate (e : ℕ) : ZMod (CyclotomicRing.dimension e) × Fin (CyclotomicRing.degree e) ≃ Fin (matrixDimension e)

Fixed row-major block coordinate.

theorem Cslib.Circuits.Rational.Generator.regular_apply (e : ℕ) (A : Matrix (ZMod (CyclotomicRing.dimension e)) (ZMod (CyclotomicRing.dimension e)) (CyclotomicRing.R e)) (i j : Fin (matrixDimension e)) : (regular e) A i j = (CyclotomicRing.rho e) (A ((coordinate e).symm i).1 ((coordinate e).symm j).1) ((coordinate e).symm i).2 ((coordinate e).symm j).2

The (i, j) entry of regular e A is the corresponding entry of CyclotomicRing.rho e under coordinate e.

def Cslib.Circuits.Rational.Generator.integerTest (N e : ℕ) (a t : ℤ) : Matrix (ZMod (CyclotomicRing.dimension e)) (ZMod (CyclotomicRing.dimension e)) ℤ

Exact integer Taylor matrices, with the same fixed order of residues.

def Cslib.Circuits.Rational.Generator.integralLift (n N e : ℕ) (x : Fin 3 → ℕ) (a : Fin (n + 1)) : Matrix (Fin (matrixDimension e)) (Fin (matrixDimension e)) ℤ

The common-denominator-cleared regular matrices used in exact arithmetic.

theorem Cslib.Circuits.Rational.Generator.U_cast (n N e : ℕ) (x : Fin 3 → ℕ) (a : Fin (n + 1)) : (integralLift n N e x a).map ⇑(Int.castRingHom ℚ) = ↑(CyclotomicRing.dimension e) • rationalLift n N e x a

Casting integralLift n N e x a to ℚ equals CyclotomicRing.dimension e times rationalLift n N e x a.

theorem Cslib.Circuits.Rational.Generator.U_bound (n N e H : ℕ) (x : Fin 3 → ℕ) (hH : 1 ≤ H) (hx : ∀ (l : Fin 3), x l ≤ H) (a : Fin (n + 1)) (i j : Fin (matrixDimension e)) : |integralLift n N e x a i j| ≤ ↑(CyclotomicRing.dimension e) ^ 4 * (2 * (↑n + 1)) ^ (2 * CyclotomicRing.dimension e) * ↑H ^ (3 * CyclotomicRing.dimension e)

For grid points bounded by H ≥ 1, every entry of integralLift n N e x a has absolute value at most M ^ 4 * (2 * (n + 1)) ^ (2 * M) * H ^ (3 * M), where M = CyclotomicRing.dimension e.

theorem Cslib.Circuits.Rational.Generator.tupleAt_integer (n N e : ℕ) (x : Fin 3 → ℕ) (hz : Matrix.det (rationalLift n N e x 0) ≠ 0) (a : Fin n) : tupleAt n N e x a = ((integralLift n N e x 0).map ⇑(Int.castRingHom ℚ))⁻¹ * (integralLift n N e x a.succ).map ⇑(Int.castRingHom ℚ)

When (rationalLift n N e x 0).det ≠ 0, the normalized matrix tupleAt n N e x a is the ratio (integralLift n N e x 0)⁻¹ * integralLift n N e x a.succ over ℚ.

theorem Cslib.Circuits.Rational.Generator.U_det_ne_zero (n N e : ℕ) (x : Fin 3 → ℕ) (hz : Matrix.det (rationalLift n N e x 0) ≠ 0) : (integralLift n N e x 0).det ≠ 0

If (rationalLift n N e x 0).det ≠ 0, then (integralLift n N e x 0).det ≠ 0.