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.

theorem Cslib.Circuits.Rational.CyclotomicRing.root_degree (e : ℕ) : AdjoinRoot.root (modulus e) ^ degree e = -1

theorem Cslib.Circuits.Rational.CyclotomicRing.root_pow_reduce (e k : ℕ) : AdjoinRoot.root (modulus e) ^ k = (-1) ^ (k / degree e) * (basis e) ⟨k % degree e, ⋯⟩

theorem Cslib.Circuits.Rational.CyclotomicRing.rho_root_pow (e k : ℕ) (i j : Fin (degree e)) : (rho e) (AdjoinRoot.root (modulus e) ^ k) i j = if (k + ↑j) % degree e = ↑i then (-1) ^ ((k + ↑j) / degree e) else 0

Every regular-representation entry of a cyclotomic monomial is 0 or ±1. This also gives an explicit integral computation with a division and remainder.

theorem Cslib.Circuits.Rational.CyclotomicRing.rho_character (e : ℕ) (a : ZMod (dimension e)) (i j : Fin (degree e)) : (rho e) ((character e) a) i j = if (a.val + ↑j) % degree e = ↑i then (-1) ^ ((a.val + ↑j) / degree e) else 0

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

The signed coefficient of the cyclotomic regular representation.

theorem Cslib.Circuits.Rational.CyclotomicRing.rho_character_integral (e : ℕ) (a : ZMod (dimension e)) (i j : Fin (degree e)) : (rho e) ((character e) a) i j = ↑(signedEntry e a i j)

theorem Cslib.Circuits.Rational.CyclotomicRing.signedEntry_abs (e : ℕ) (a : ZMod (dimension e)) (i j : Fin (degree e)) : |signedEntry e a i j| ≤ 1

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

theorem Cslib.Circuits.Rational.IntegralTest.full_bound (M : ℕ) (a t : ℤ) (w H : ℕ) (hw : 1 ≤ w) (hH : 1 ≤ H) (ha : |a| ≤ ↑w) (ht : |t| ≤ ↑H) (i j : Fin M) : |full M a t i j| ≤ ↑M * (2 * ↑w) ^ (2 * M) * ↑H ^ M

theorem Cslib.Circuits.Rational.IntegralTest.padded_bound (M N : ℕ) (a t : ℤ) (w H : ℕ) (hw : 1 ≤ w) (hH : 1 ≤ H) (ha : |a| ≤ ↑w) (ht : |t| ≤ ↑H) (i j : Fin M) : |padded M N a t i j| ≤ ↑M * (2 * ↑w) ^ (2 * M) * ↑H ^ M

theorem Cslib.Circuits.Rational.IntegralTest.full_cast {K : Type u_1} [Field K] (M : ℕ) (a t : ℤ) (i j : Fin M) : Polynomial.eval (↑t) (TestPolynomial.full M (↑a) i j) = ↑(full M a t i j)

theorem Cslib.Circuits.Rational.IntegralTest.padded_cast {K : Type u_1} [Field K] (M N : ℕ) (a t : ℤ) (i j : Fin M) : Polynomial.eval (↑t) (TestPolynomial.padded M N (↑a) i j) = ↑(padded M N a t i j)

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

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

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_bound (e : ℕ) (T : Matrix (ZMod (CyclotomicRing.dimension e)) (ZMod (CyclotomicRing.dimension e)) ℤ) (p r : ℤ) (A H : ℕ) (hT : ∀ (i j : ZMod (CyclotomicRing.dimension e)), |T i j| ≤ ↑A) (hH : 1 ≤ H) (hp : |p| ≤ ↑H) (hr : |r| ≤ ↑H) (u v : ZMod (CyclotomicRing.dimension e)) (i j : Fin (CyclotomicRing.degree e)) : |entry e T p r u v i j| ≤ ↑(CyclotomicRing.dimension e) ^ 3 * ↑A * ↑H ^ (2 * CyclotomicRing.dimension e)

theorem Cslib.Circuits.Rational.IntegralLift.rho_rat_mul (e : ℕ) (q : ℚ) (z : CyclotomicRing.R e) (i j : Fin (CyclotomicRing.degree e)) : (CyclotomicRing.rho e) ((algebraMap ℚ (CyclotomicRing.R e)) q * z) i j = q * (CyclotomicRing.rho e) z i j

theorem Cslib.Circuits.Rational.IntegralLift.rho_div_nat (e : ℕ) (z : CyclotomicRing.R e) (i j : Fin (CyclotomicRing.degree e)) : ↑(CyclotomicRing.dimension e) * (CyclotomicRing.rho e) ((↑(CyclotomicRing.dimension e))⁻¹ * z) i j = (CyclotomicRing.rho e) z i j

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

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

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

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)

theorem Cslib.Circuits.Rational.Generator.scaled_normalization {d : ℕ} (A B : Mat d) (hA : Matrix.det A ≠ 0) (c : ℚ) (hc : c ≠ 0) : (c • A)⁻¹ * c • B = A⁻¹ * B

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 ℚ)

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