Rational hitting lists: quantum matrices

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

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

def Complexity.RationalHitting.HahnMatrix.mapCoeff {Γ : Type u_1} {R : Type u_2} {S : Type u_3} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] [Ring S] (φ : R →+* S) : HahnSeries Γ R →+* HahnSeries Γ S

Apply a ring homomorphism to every Hahn-series coefficient.

Equations

• Complexity.RationalHitting.HahnMatrix.mapCoeff φ = { toFun := fun (x : HahnSeries Γ R) => x.map ↑φ.toAddMonoidHom, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

theorem Complexity.RationalHitting.HahnMatrix.coeff_mul_support_superset {Γ : Type u_1} {R : Type u_2} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] (x y : HahnSeries Γ R) (a : Γ) (s t : Set Γ) (hs : s.IsPWO) (ht : t.IsPWO) (hxs : x.support ⊆ s) (hyt : y.support ⊆ t) : (x * y).coeff a = ∑ ij ∈ Finset.antidiagonal hs ht a, x.coeff ij.1 * y.coeff ij.2

def Complexity.RationalHitting.HahnMatrix.entry {Γ : Type u_1} {R : Type u_2} [LinearOrder Γ] [Ring R] {ι : Type u_4} (x : HahnSeries Γ (Matrix ι ι R)) (i j : ι) : HahnSeries Γ R

Extract one matrix entry from every Hahn-series coefficient.

Equations

• Complexity.RationalHitting.HahnMatrix.entry x i j = x.map { toFun := fun (A : Matrix ι ι R) => A i j, map_zero' := ⋯ }

@[simp]

theorem Complexity.RationalHitting.HahnMatrix.entry_coeff {Γ : Type v_1} {R : Type v_2} [LinearOrder Γ] [Ring R] {ι : Type v_4} (x : HahnSeries Γ (Matrix ι ι R)) (i j : ι) (a : Γ) : (entry x i j).coeff a = x.coeff a i j

theorem Complexity.RationalHitting.HahnMatrix.entry_support {Γ : Type v_1} {R : Type v_2} [LinearOrder Γ] [Ring R] {ι : Type v_4} (x : HahnSeries Γ (Matrix ι ι R)) (i j : ι) : (entry x i j).support ⊆ x.support

def Complexity.RationalHitting.HahnMatrix.split {Γ : Type u_1} {R : Type u_2} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] {ι : Type u_4} [Fintype ι] [DecidableEq ι] : HahnSeries Γ (Matrix ι ι R) →+* Matrix ι ι (HahnSeries Γ R)

Identify a matrix-valued Hahn series with a matrix of scalar Hahn series.

Equations

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

theorem Complexity.RationalHitting.HahnMatrix.split_injective {Γ : Type u_1} {R : Type u_2} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] [Ring R] {ι : Type u_4} [Fintype ι] [DecidableEq ι] : Function.Injective ⇑split

def Complexity.RationalHitting.HahnMatrix.scalarSeries {Γ : Type u_1} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] {ι : Type u_4} [Fintype ι] [DecidableEq ι] {K : Type u_5} [Field K] : HahnSeries Γ K →+* HahnSeries Γ (Matrix ι ι K)

Scalar series embedded as scalar matrices at each coefficient.

Equations

• Complexity.RationalHitting.HahnMatrix.scalarSeries = Complexity.RationalHitting.HahnMatrix.mapCoeff (algebraMap K (Matrix ι ι K))

theorem Complexity.RationalHitting.HahnMatrix.split_scalarSeries {Γ : Type u_1} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] {ι : Type u_4} [Fintype ι] [DecidableEq ι] {K : Type u_5} [Field K] (x : HahnSeries Γ K) : split (scalarSeries x) = (algebraMap (HahnSeries Γ K) (Matrix ι ι (HahnSeries Γ K))) x

theorem Complexity.RationalHitting.HahnMatrix.scalarSeries_commute {Γ : Type u_1} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] {ι : Type u_4} [Fintype ι] [DecidableEq ι] {K : Type u_5} [Field K] (x : HahnSeries Γ K) (y : HahnSeries Γ (Matrix ι ι K)) : scalarSeries x * y = y * scalarSeries x

@[instance_reducible]

noncomputable def Complexity.RationalHitting.HahnMatrix.seriesAlgebra {Γ : Type u_1} [AddCommGroup Γ] [LinearOrder Γ] [IsOrderedAddMonoid Γ] {ι : Type u_4} [Fintype ι] [DecidableEq ι] {K : Type u_5} [Field K] : Algebra (HahnSeries Γ K) (HahnSeries Γ (Matrix ι ι K))

The natural scalar-series algebra structure, derived through an injective matrix realization rather than assuming commutative matrix coefficients.

Equations

• Complexity.RationalHitting.HahnMatrix.seriesAlgebra = Complexity.RationalHitting.HahnMatrix.scalarSeries.toAlgebra' ⋯

def Complexity.RationalHitting.QuantumMatrices.weyl {K : Type u_1} [Field K] {d : ℕ} (χ : AddChar (ZMod d) K) (a b : ZMod d) : Matrix (ZMod d) (ZMod d) K

The Weyl monomial D^a S^b.

Equations

• Complexity.RationalHitting.QuantumMatrices.weyl χ a b i j = if i = j + b then χ (a * i) else 0

@[simp]

theorem Complexity.RationalHitting.QuantumMatrices.weyl_zero {K : Type v_1} [Field K] {d : ℕ} (χ : AddChar (ZMod d) K) : weyl χ 0 0 = 1

theorem Complexity.RationalHitting.QuantumMatrices.weyl_mul {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) (a b c e : ZMod d) : weyl χ a b * weyl χ c e = χ (-c * b) • weyl χ (a + c) (b + e)

theorem Complexity.RationalHitting.QuantumMatrices.weyl_inverse_right {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) (a b : ZMod d) : weyl χ a b * χ (-a * b) • weyl χ (-a) (-b) = 1

theorem Complexity.RationalHitting.QuantumMatrices.weyl_inverse_left {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) (a b : ZMod d) : χ (-a * b) • weyl χ (-a) (-b) * weyl χ a b = 1

def Complexity.RationalHitting.QuantumMatrices.weylUnit {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) (a b : ZMod d) : (Matrix (ZMod d) (ZMod d) K)ˣ

A Weyl matrix with its explicit two-sided inverse.

Equations

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

@[simp]

theorem Complexity.RationalHitting.QuantumMatrices.weylUnit_val {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) (a b : ZMod d) : ↑(weylUnit χ a b) = weyl χ a b

@[simp]

theorem Complexity.RationalHitting.QuantumMatrices.weylUnit_zero {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) : weylUnit χ 0 0 = 1

def Complexity.RationalHitting.QuantumMatrices.fourierCoeff {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) (R : Matrix (ZMod d) (ZMod d) K) (a b : ZMod d) : K

The coefficient of a Weyl matrix in the finite Fourier expansion.

Equations

• Complexity.RationalHitting.QuantumMatrices.fourierCoeff χ R a b = (↑d)⁻¹ * ∑ j : ZMod d, χ (-a * j) * R j (j - b)

theorem Complexity.RationalHitting.QuantumMatrices.orthogonality {K : Type v_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) (hχ : χ.IsPrimitive) (x : ZMod d) : ∑ a : ZMod d, χ (a * x) = if x = 0 then ↑d else 0

theorem Complexity.RationalHitting.QuantumMatrices.fourier_reconstruction {K : Type u_1} [Field K] [CharZero K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) (hχ : χ.IsPrimitive) (R : Matrix (ZMod d) (ZMod d) K) : ∑ a : ZMod d, ∑ b : ZMod d, fourierCoeff χ R a b • weyl χ a b = R

Fourier inversion on each cyclic matrix diagonal.

@[reducible, inline]

abbrev Complexity.RationalHitting.QuantumLift.Exponents : Type

Lexicographically ordered pairs of integer exponents.

Equations

• Complexity.RationalHitting.QuantumLift.Exponents = Lex (ℤ × ℤ)

@[reducible, inline]

abbrev Complexity.RationalHitting.QuantumLift.Ambient {K : Type u_1} [Field K] {d : ℕ} : Type u_1

Hahn series with matrix coefficients and two integer exponents.

Equations

• Complexity.RationalHitting.QuantumLift.Ambient = HahnSeries Complexity.RationalHitting.QuantumLift.Exponents (Matrix (ZMod d) (ZMod d) K)

def Complexity.RationalHitting.QuantumLift.monomialUnit {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) (g : Exponents) : (Matrix (ZMod d) (ZMod d) K)ˣ

The Weyl unit assigned to an exponent pair.

Equations

• Complexity.RationalHitting.QuantumLift.monomialUnit χ g = Complexity.RationalHitting.QuantumMatrices.weylUnit χ ↑(ofLex g).1 ↑(ofLex g).2

theorem Complexity.RationalHitting.QuantumLift.monomialUnit_zero {K : Type v_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) : monomialUnit χ 0 = 1

theorem Complexity.RationalHitting.QuantumLift.monomialUnit_mul {K : Type v_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) (g h : Exponents) : ∃ (c : K), ↑(monomialUnit χ g) * ↑(monomialUnit χ h) = c • ↑(monomialUnit χ (g + h))

@[reducible, inline]

abbrev Complexity.RationalHitting.QuantumLift.divisionSubring {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) : Subring (HahnSeries Exponents (Matrix (ZMod d) (ZMod d) K))

The Hahn-series subring whose coefficients lie on the Weyl monomial lines.

Equations

• Complexity.RationalHitting.QuantumLift.divisionSubring χ = Complexity.RationalHitting.QuantumSeries.coefficientRing (Complexity.RationalHitting.QuantumLift.monomialUnit χ) ⋯ ⋯

@[instance_reducible]

noncomputable instance Complexity.RationalHitting.QuantumLift.instDivisionRingSubtypeHahnSeriesExponentsMatrixZModMemSubringDivisionSubring {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) : DivisionRing ↥(divisionSubring χ)

Equations

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

noncomputable def Complexity.RationalHitting.QuantumLift.lift {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) (R : Matrix (ZMod d) (ZMod d) K) : Ambient

The Fourier lift as a finite Hahn series.

Equations

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

theorem Complexity.RationalHitting.QuantumLift.lift_mem {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) (R : Matrix (ZMod d) (ZMod d) K) : lift χ R ∈ divisionSubring χ

noncomputable def Complexity.RationalHitting.QuantumLift.liftD {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) (R : Matrix (ZMod d) (ZMod d) K) : ↥(divisionSubring χ)

The finite Fourier lift as an element of the division subring.

Equations

• Complexity.RationalHitting.QuantumLift.liftD χ R = ⟨Complexity.RationalHitting.QuantumLift.lift χ R, ⋯⟩

noncomputable def Complexity.RationalHitting.QuantumLift.representation {K : Type u_1} [Field K] {d : ℕ} [NeZero d] (χ : AddChar (ZMod d) K) : ↥(divisionSubring χ) →+* Matrix (ZMod d) (ZMod d) (HahnSeries Exponents K)

The representation used in the rank-gap argument. Its coefficient field is a commutative Hahn field; all inversion takes place inside the division subring, never by adjoining arbitrary matrix-field scalars.

Equations

• Complexity.RationalHitting.QuantumLift.representation χ = Complexity.RationalHitting.HahnMatrix.split.comp (Complexity.RationalHitting.QuantumLift.divisionSubring χ).subtype