Rational hitting lists: block division

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

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

@[reducible, inline]

abbrev Complexity.RationalHitting.PolynomialHahn.Exponents : Type

Lexicographically ordered integer exponents for two-variable monomials.

Equations

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

def Complexity.RationalHitting.PolynomialHahn.exponent (m : Fin 2 →₀ ℕ) : Exponents

Embed a two-variable natural exponent vector into the ordered exponent group.

Equations

• Complexity.RationalHitting.PolynomialHahn.exponent m = toLex (↑(m 0), ↑(m 1))

theorem Complexity.RationalHitting.PolynomialHahn.exponent_injective : Function.Injective exponent

noncomputable def Complexity.RationalHitting.PolynomialHahn.variableSeries {K : Type u_1} [Field K] (i : Fin 2) : HahnSeries Exponents K

The Hahn monomial corresponding to a polynomial variable.

Equations

• Complexity.RationalHitting.PolynomialHahn.variableSeries i = (HahnSeries.single (if i = 0 then toLex (1, 0) else toLex (0, 1))) 1

noncomputable def Complexity.RationalHitting.PolynomialHahn.embed {K : Type u_1} [Field K] : MvPolynomial (Fin 2) K →+* HahnSeries Exponents K

Embed bivariate polynomials into the Hahn-series ring.

Equations

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

theorem Complexity.RationalHitting.PolynomialHahn.embed_monomial {K : Type u_1} [Field K] (m : Fin 2 →₀ ℕ) (a : K) : embed ((MvPolynomial.monomial m) a) = (HahnSeries.single (exponent m)) a

theorem Complexity.RationalHitting.PolynomialHahn.embed_coeff {K : Type u_1} [Field K] (p : MvPolynomial (Fin 2) K) (m : Fin 2 →₀ ℕ) : (embed p).coeff (exponent m) = p.coeff m

theorem Complexity.RationalHitting.PolynomialHahn.embed_injective {K : Type u_1} [Field K] : Function.Injective ⇑embed

def Complexity.RationalHitting.BlockDivision.blockEmbedding {D : Type u_1} {E : Type u_2} [DivisionRing D] [Field E] {m : Type u_3} {κ : Type u_4} [Fintype m] [DecidableEq m] [Fintype κ] [DecidableEq κ] (φ : D →+* Matrix κ κ E) : Matrix m m D →+* Matrix (m × κ) (m × κ) E

Extend a matrix representation entrywise to block matrices.

Equations

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

theorem Complexity.RationalHitting.BlockDivision.unit_of_vecMul_injective {D : Type u_1} [DivisionRing D] {m : Type u_3} [Fintype m] [DecidableEq m] (A : Matrix m m D) (hA : Function.Injective ⇑A.vecMulLinear) : IsUnit A

def Complexity.RationalHitting.BlockDivision.kernelRows {D : Type u_1} {E : Type u_2} [DivisionRing D] [Field E] {m : Type u_3} {κ : Type u_4} [Fintype κ] [DecidableEq κ] (φ : D →+* Matrix κ κ E) (v : m → D) : (κ → E) →ₗ[E] m × κ → E

A nonzero row of a division-ring kernel expands into d independent ordinary kernel rows after a faithful d-dimensional representation.

Equations

• Complexity.RationalHitting.BlockDivision.kernelRows φ v = { toFun := fun (x : κ → E) (j : m × κ) => Matrix.vecMul x (φ (v j.1)) j.2, map_add' := ⋯, map_smul' := ⋯ }

theorem Complexity.RationalHitting.BlockDivision.kernelRows_injective {D : Type v_1} {E : Type v_2} [DivisionRing D] [Field E] {m : Type v_3} {κ : Type v_4} [Fintype κ] [DecidableEq κ] (φ : D →+* Matrix κ κ E) (v : m → D) (hv : v ≠ 0) : Function.Injective ⇑(kernelRows φ v)

theorem Complexity.RationalHitting.BlockDivision.kernelRows_mem {D : Type u_1} {E : Type u_2} [DivisionRing D] [Field E] {m : Type u_3} {κ : Type u_4} [Fintype m] [DecidableEq m] [Fintype κ] [DecidableEq κ] (φ : D →+* Matrix κ κ E) (A : Matrix m m D) (v : m → D) (hv : Matrix.vecMul v A = 0) (x : κ → E) : (kernelRows φ v) x ∈ ((blockEmbedding φ) A).vecMulLinear.ker

theorem Complexity.RationalHitting.BlockDivision.rank_gap {D : Type u_1} {E : Type u_2} [DivisionRing D] [Field E] {m : Type u_3} {κ : Type u_4} [Fintype m] [DecidableEq m] [Fintype κ] [DecidableEq κ] (φ : D →+* Matrix κ κ E) (A : Matrix m m D) : IsUnit ((blockEmbedding φ) A) ∨ ((blockEmbedding φ) A).rank + Fintype.card κ ≤ Fintype.card m * Fintype.card κ

The rank gap obtained by block elimination over a division ring.

theorem Complexity.RationalHitting.BlockDivision.isUnit_of_rank_gt {D : Type u_1} {E : Type u_2} [DivisionRing D] [Field E] {m : Type u_3} {κ : Type u_4} [Fintype m] [DecidableEq m] [Fintype κ] [DecidableEq κ] (φ : D →+* Matrix κ κ E) (A : Matrix m m D) (hq : 1 ≤ Fintype.card m) (h : (Fintype.card m - 1) * Fintype.card κ < ((blockEmbedding φ) A).rank) : IsUnit ((blockEmbedding φ) A)

theorem Complexity.RationalHitting.RankSpecialization.rank_le {K : Type u_1} {P : Type u_2} {E : Type u_3} {ι : Type u_4} [Field K] [CommRing P] [Field E] [Algebra K P] [Fintype ι] [DecidableEq ι] (ev : P →ₐ[K] K) (inclusion : P →+* E) (hinj : Function.Injective ⇑inclusion) (A : Matrix ι ι P) : (ev.mapMatrix A).rank ≤ (inclusion.mapMatrix A).rank

Specialization cannot raise the generic rank. This version requires no unstated minor criterion: a rank normal form supplies a nonzero minor after constant row and column changes.