Rational hitting lists: integral lift

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/RationalHitting/IntegralLift.lean

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical arguments are retained.

theorem Complexity.RationalHitting.CyclotomicRing.root_degree (e : ℕ) : AdjoinRoot.root (modulus e) ^ degree e = -1

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

theorem Complexity.RationalHitting.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 Complexity.RationalHitting.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 Complexity.RationalHitting.CyclotomicRing.signedEntry (e : ℕ) (a : ZMod (dimension e)) (i j : Fin (degree e)) : ℤ

The signed coefficient of the cyclotomic regular representation.

Equations

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

theorem Complexity.RationalHitting.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 Complexity.RationalHitting.CyclotomicRing.signedEntry_abs (e : ℕ) (a : ZMod (dimension e)) (i j : Fin (degree e)) : |signedEntry e a i j| ≤ 1

def Complexity.RationalHitting.IntegralTest.full (M : ℕ) (a t : ℤ) : Matrix (Fin M) (Fin M) ℤ

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

Equations

• Complexity.RationalHitting.IntegralTest.full M a t i j = ∑ r : Fin M, (-a) ^ (↑r.rev - ↑i) * ↑((↑r.rev).choose ↑i) * (a ^ (↑j - ↑r) * ↑((↑j).choose ↑r)) * t ^ ↑r

def Complexity.RationalHitting.IntegralTest.padded (M N : ℕ) (a t : ℤ) : Matrix (Fin M) (Fin M) ℤ

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

Equations

• Complexity.RationalHitting.IntegralTest.padded M N a t i j = if ↑j < N then Complexity.RationalHitting.IntegralTest.full M a t i j else 0

theorem Complexity.RationalHitting.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 Complexity.RationalHitting.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 Complexity.RationalHitting.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 Complexity.RationalHitting.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 Complexity.RationalHitting.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 Complexity.RationalHitting.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 Complexity.RationalHitting.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 Complexity.RationalHitting.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.

Equations

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

theorem Complexity.RationalHitting.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 Complexity.RationalHitting.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 Complexity.RationalHitting.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 Complexity.RationalHitting.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 Complexity.RationalHitting.Generator.coordinate (e : ℕ) : ZMod (CyclotomicRing.dimension e) × Fin (CyclotomicRing.degree e) ≃ Fin (matrixDimension e)

Fixed row-major block coordinate.

Equations

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

theorem Complexity.RationalHitting.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 Complexity.RationalHitting.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.

Equations

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

def Complexity.RationalHitting.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.

Equations

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

theorem Complexity.RationalHitting.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 Complexity.RationalHitting.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 Complexity.RationalHitting.Generator.scaled_normalization {d : ℕ} (A B : Mat d) (hA : Matrix.det A ≠ 0) (c : ℚ) (hc : c ≠ 0) : (c • A)⁻¹ * c • B = A⁻¹ * B

theorem Complexity.RationalHitting.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 Complexity.RationalHitting.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