Rational hitting lists: affine

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Computability/RationalHitting/Affine.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.Affine.Form (n : ℕ) : Type

A constant coefficient and one rational coefficient per variable.

Equations

• Complexity.RationalHitting.Affine.Form n = (ℚ × (Fin n → ℚ))

def Complexity.RationalHitting.Affine.constant {n : ℕ} (a : ℚ) : Form n

The affine form with the given constant and zero variable coefficients.

Equations

• Complexity.RationalHitting.Affine.constant a = (a, 0)

def Complexity.RationalHitting.Affine.varForm {n : ℕ} (i : Fin n) : Form n

The affine coordinate form for one variable.

Equations

• Complexity.RationalHitting.Affine.varForm i = (0, Pi.single i 1)

def Complexity.RationalHitting.Affine.eval {n : ℕ} {R : Type u_1} [Ring R] (c : ℚ →+* R) (X : Fin n → R) : Form n →+ R

Evaluate an affine form in a rational algebra, with coefficients on the left.

Equations

• Complexity.RationalHitting.Affine.eval c X = { toFun := fun (a : Complexity.RationalHitting.Affine.Form n) => c a.1 + ∑ i : Fin n, c (a.2 i) * X i, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Complexity.RationalHitting.Affine.eval_constant {n : ℕ} {R : Type u_1} [Ring R] (c : ℚ →+* R) (X : Fin n → R) (a : ℚ) : (eval c X) (constant a) = c a

@[simp]

theorem Complexity.RationalHitting.Affine.eval_variable {n : ℕ} {R : Type u_1} [Ring R] (c : ℚ →+* R) (X : Fin n → R) (i : Fin n) : (eval c X) (varForm i) = X i

def Complexity.RationalHitting.Affine.constMatrix {n : ℕ} {ι : Type u_2} {κ : Type u_3} (A : Matrix ι κ ℚ) : Matrix ι κ (Form n)

Regard a rational matrix as a matrix of constant affine forms.

Equations

• Complexity.RationalHitting.Affine.constMatrix A = A.map Complexity.RationalHitting.Affine.constant

@[simp]

theorem Complexity.RationalHitting.Affine.eval_constMatrix {n : ℕ} {R : Type u_1} [Ring R] {ι : Type u_2} {κ : Type u_3} (c : ℚ →+* R) (X : Fin n → R) (A : Matrix ι κ ℚ) : (constMatrix A).map ⇑(eval c X) = A.map ⇑c

@[reducible]

def Complexity.RationalHitting.Formula.Index {n : ℕ} : Formula n → Type

The finite row and column index type of the formula's linear realization.

Equations

• (Complexity.RationalHitting.Formula.var a).Index = (Unit ⊕ Unit)
• (Complexity.RationalHitting.Formula.const a).Index = (Unit ⊕ Unit)
• (f.add g).Index = (f.Index ⊕ g.Index)
• (f.mul g).Index = (f.Index ⊕ g.Index)
• f.inv.Index = (f.Index ⊕ Unit)

@[reducible]

instance Complexity.RationalHitting.Formula.indexFintype {n : ℕ} (h : Formula n) : Fintype h.Index

Equations

• (Complexity.RationalHitting.Formula.var a).indexFintype = { elems := Finset.univ.disjSum Finset.univ, complete := ⋯ }
• (Complexity.RationalHitting.Formula.const a).indexFintype = { elems := Finset.univ.disjSum Finset.univ, complete := ⋯ }
• (f.add g).indexFintype = { elems := Finset.univ.disjSum Finset.univ, complete := ⋯ }
• (f.mul g).indexFintype = { elems := Finset.univ.disjSum Finset.univ, complete := ⋯ }
• f.inv.indexFintype = { elems := Finset.univ.disjSum Finset.univ, complete := ⋯ }

@[reducible]

instance Complexity.RationalHitting.Formula.indexDecidableEq {n : ℕ} (h : Formula n) : DecidableEq h.Index

Equations

• (Complexity.RationalHitting.Formula.var a).indexDecidableEq = fun (a b : Unit ⊕ Unit) => instDecidableEqSum a b
• (Complexity.RationalHitting.Formula.const a).indexDecidableEq = fun (a b : Unit ⊕ Unit) => instDecidableEqSum a b
• (f.add g).indexDecidableEq = fun (a b : f.Index ⊕ g.Index) => instDecidableEqSum a b
• (f.mul g).indexDecidableEq = fun (a b : f.Index ⊕ g.Index) => instDecidableEqSum a b
• f.inv.indexDecidableEq = fun (a b : f.Index ⊕ Unit) => instDecidableEqSum a b

theorem Complexity.RationalHitting.Formula.card_index {n : ℕ} (f : Formula n) : Fintype.card f.Index = f.size + 1

def Complexity.RationalHitting.Formula.row {n : ℕ} (f : Formula n) : Matrix Unit f.Index ℚ

The left row of the formula's linear realization.

Equations

• (Complexity.RationalHitting.Formula.var a).row = Matrix.fromCols 1 0
• (Complexity.RationalHitting.Formula.const a).row = Matrix.fromCols 1 0
• (f.add g).row = f.row.fromCols g.row
• (f.mul g).row = f.row.fromCols 0
• f.inv.row = Matrix.fromCols 0 (-1)

def Complexity.RationalHitting.Formula.col {n : ℕ} (f : Formula n) : Matrix f.Index Unit ℚ

The right column of the formula's linear realization.

Equations

• (Complexity.RationalHitting.Formula.var a).col = Matrix.fromRows 0 1
• (Complexity.RationalHitting.Formula.const a).col = Matrix.fromRows 0 1
• (f.add g).col = f.col.fromRows g.col
• (f.mul g).col = Matrix.fromRows 0 g.col
• f.inv.col = Matrix.fromRows 0 1

def Complexity.RationalHitting.Formula.pencil {n : ℕ} (f : Formula n) : Matrix f.Index f.Index (Affine.Form n)

The affine matrix pencil built recursively from a rational formula.

Equations

• One or more equations did not get rendered due to their size.
• (f.add g).pencil = Matrix.fromBlocks f.pencil 0 0 g.pencil
• (f.mul g).pencil = Matrix.fromBlocks f.pencil (-Complexity.RationalHitting.Affine.constMatrix (f.col * g.row)) 0 g.pencil
• f.inv.pencil = Matrix.fromBlocks f.pencil (Complexity.RationalHitting.Affine.constMatrix f.col) (Complexity.RationalHitting.Affine.constMatrix f.row) 0

@[reducible, inline]

abbrev Complexity.RationalHitting.Formula.realized {n : ℕ} {R : Type u_1} [Ring R] (c : ℚ →+* R) (X : Fin n → R) (f : Formula n) : Matrix f.Index f.Index R

Evaluate all entries of the formula's affine pencil.

Equations

• Complexity.RationalHitting.Formula.realized c X f = f.pencil.map ⇑(Complexity.RationalHitting.Affine.eval c X)

@[reducible, inline]

abbrev Complexity.RationalHitting.Formula.rowR {n : ℕ} {R : Type u_1} [Ring R] (c : ℚ →+* R) (f : Formula n) : Matrix Unit f.Index R

Map the realization's rational row into the target ring.

Equations

• Complexity.RationalHitting.Formula.rowR c f = f.row.map ⇑c

@[reducible, inline]

abbrev Complexity.RationalHitting.Formula.colR {n : ℕ} {R : Type u_1} [Ring R] (c : ℚ →+* R) (f : Formula n) : Matrix f.Index Unit R

Map the realization's rational column into the target ring.

Equations

• Complexity.RationalHitting.Formula.colR c f = f.col.map ⇑c

@[reducible, inline]

abbrev Complexity.RationalHitting.Formula.scalar {R : Type u_1} [Ring R] (a : R) : Matrix Unit Unit R

Represent a scalar as a one-by-one matrix.

Equations

• Complexity.RationalHitting.Formula.scalar a = Matrix.uniqueRingEquiv.symm a

theorem Complexity.RationalHitting.Formula.realized_add {n : ℕ} {R : Type u_1} [Ring R] (c : ℚ →+* R) (X : Fin n → R) (f g : Formula n) : realized c X (f.add g) = Matrix.fromBlocks (realized c X f) 0 0 (realized c X g)

theorem Complexity.RationalHitting.Formula.realized_mul {n : ℕ} {R : Type u_1} [Ring R] (c : ℚ →+* R) (X : Fin n → R) (f g : Formula n) : realized c X (f.mul g) = Matrix.fromBlocks (realized c X f) (-colR c f * rowR c g) 0 (realized c X g)

theorem Complexity.RationalHitting.Formula.realized_inv {n : ℕ} {R : Type u_1} [Ring R] (c : ℚ →+* R) (X : Fin n → R) (f : Formula n) : realized c X f.inv = Matrix.fromBlocks (realized c X f) (colR c f) (rowR c f) 0

theorem Complexity.RationalHitting.Formula.rowR_add {n : ℕ} {R : Type u_1} [Ring R] (c : ℚ →+* R) (f g : Formula n) : rowR c (f.add g) = (rowR c f).fromCols (rowR c g)

theorem Complexity.RationalHitting.Formula.colR_add {n : ℕ} {R : Type u_1} [Ring R] (c : ℚ →+* R) (f g : Formula n) : colR c (f.add g) = (colR c f).fromRows (colR c g)

theorem Complexity.RationalHitting.Formula.rowR_mul {n : ℕ} {R : Type u_1} [Ring R] (c : ℚ →+* R) (f g : Formula n) : rowR c (f.mul g) = (rowR c f).fromCols 0

theorem Complexity.RationalHitting.Formula.colR_mul {n : ℕ} {R : Type u_1} [Ring R] (c : ℚ →+* R) (f g : Formula n) : colR c (f.mul g) = Matrix.fromRows 0 (colR c g)

theorem Complexity.RationalHitting.Formula.rowR_inv {n : ℕ} {R : Type u_1} [Ring R] (c : ℚ →+* R) (f : Formula n) : rowR c f.inv = Matrix.fromCols 0 (-1)

theorem Complexity.RationalHitting.Formula.colR_inv {n : ℕ} {R : Type u_1} [Ring R] (c : ℚ →+* R) (f : Formula n) : colR c f.inv = Matrix.fromRows 0 1

theorem Complexity.RationalHitting.Formula.leaf_realization {R : Type u_1} [Ring R] (a : R) : ∃ (M : Matrix (Unit ⊕ Unit) (Unit ⊕ Unit) R), Matrix.fromBlocks 1 (-scalar a) 0 1 * M = 1 ∧ M * Matrix.fromBlocks 1 (-scalar a) 0 1 = 1 ∧ NoncommBlocks.matMul (NoncommBlocks.matMul (Matrix.fromCols 1 0) M) (Matrix.fromRows 0 1) = scalar a

theorem Complexity.RationalHitting.Formula.Eval.realization {n : ℕ} {R : Type u_1} [Ring R] (c : ℚ →+* R) (X : Fin n → R) {f : Formula n} {a : R} (ha : Eval c X f a) : ∃ (M : Matrix f.Index f.Index R), realized c X f * M = 1 ∧ M * realized c X f = 1 ∧ rowR c f * M * colR c f = scalar a

Exact affine realization of every defined original subtree.

def Complexity.RationalHitting.Formula.inverseNodes {n : ℕ} : Formula n → List (Formula n)

The list retains occurrences, not just distinct subexpressions.

Equations

• (Complexity.RationalHitting.Formula.var a).inverseNodes = []
• (Complexity.RationalHitting.Formula.const a).inverseNodes = []
• (f.add g).inverseNodes = f.inverseNodes ++ g.inverseNodes
• (f.mul g).inverseNodes = f.inverseNodes ++ g.inverseNodes
• f.inv.inverseNodes = f.inv :: f.inverseNodes

def Complexity.RationalHitting.Formula.certificates {n : ℕ} (f : Formula n) : List (Formula n)

.inv f here denotes the root augmentation pencil, not a new counted gate.

Equations

• f.certificates = f.inverseNodes ++ [f.inv]

theorem Complexity.RationalHitting.Formula.Eval.pencil_isUnit {n : ℕ} {R : Type u_1} [Ring R] (c : ℚ →+* R) (X : Fin n → R) {f : Formula n} {a : R} (ha : Eval c X f a) : IsUnit (realized c X f)

theorem Complexity.RationalHitting.Formula.Eval.augmented_isUnit_iff {n : ℕ} {R : Type u_1} [Ring R] (c : ℚ →+* R) (X : Fin n → R) {f : Formula n} {a : R} (ha : Eval c X f a) : IsUnit (realized c X f.inv) ↔ IsUnit a

theorem Complexity.RationalHitting.Formula.Eval.inverseNodes_units {n : ℕ} {R : Type u_1} [Ring R] (c : ℚ →+* R) (X : Fin n → R) {f : Formula n} {a : R} (ha : Eval c X f a) (h : Formula n) : h ∈ f.inverseNodes → IsUnit (realized c X h)

theorem Complexity.RationalHitting.Formula.eval_of_inverseNodes_units {n : ℕ} {R : Type u_1} [Ring R] (c : ℚ →+* R) (X : Fin n → R) (f : Formula n) (hu : ∀ h ∈ f.inverseNodes, IsUnit (realized c X h)) : ∃ (a : R), Eval c X f a

theorem Complexity.RationalHitting.Formula.certificates_iff {n : ℕ} {R : Type u_1} [Ring R] (c : ℚ →+* R) (X : Fin n → R) (f : Formula n) : (∀ h ∈ f.certificates, IsUnit (realized c X h)) ↔ ∃ (a : R), Eval c X f a ∧ IsUnit a

Full original-tree definedness and invertible final value are equivalent to all affine-pencil certificates. No rational cancellation is performed.

theorem Complexity.RationalHitting.Formula.inverseNodes_length {n : ℕ} (f : Formula n) : f.inverseNodes.length ≤ f.size

theorem Complexity.RationalHitting.Formula.size_le_of_mem_inverseNodes {n : ℕ} {f h : Formula n} (hh : h ∈ f.inverseNodes) : h.size ≤ f.size

theorem Complexity.RationalHitting.Formula.certificate_bounds {n : ℕ} (f : Formula n) (s : ℕ) (hs : 1 ≤ s) (hf : f.size ≤ s) : f.certificates.length ≤ s + 1 ∧ ∀ h ∈ f.certificates, 0 < Fintype.card h.Index ∧ Fintype.card h.Index ≤ 2 * s + 1

def Complexity.RationalHitting.Affine.coeff {n : ℕ} (a : Form n) : Fin (n + 1) → ℚ

The homogeneous coefficient, with index zero reserved for the constant term.

Equations

• Complexity.RationalHitting.Affine.coeff a i = Fin.cases a.1 a.2 i

def Complexity.RationalHitting.Affine.homogeneous {n : ℕ} {R : Type u_1} [Ring R] (c : ℚ →+* R) (Z : Fin (n + 1) → R) (a : Form n) : R

Evaluate the homogeneous form on an extra constant coordinate.

Equations

• Complexity.RationalHitting.Affine.homogeneous c Z a = ∑ i : Fin (n + 1), c (Complexity.RationalHitting.Affine.coeff a i) * Z i

theorem Complexity.RationalHitting.Affine.homogeneous_one {n : ℕ} {R : Type u_1} [Ring R] (c : ℚ →+* R) (X : Fin n → R) (a : Form n) : homogeneous c (fun (i : Fin (n + 1)) => Fin.cases 1 X i) a = (eval c X) a

theorem Complexity.RationalHitting.Affine.normalized {n : ℕ} {R : Type u_1} [Ring R] [Algebra ℚ R] (Z : Fin (n + 1) → R) (u : R) (hu : Z 0 * u = 1) (a : Form n) : homogeneous (algebraMap ℚ R) Z a = Z 0 * (eval (algebraMap ℚ R) fun (i : Fin n) => u * Z i.succ) a

theorem Complexity.RationalHitting.Affine.normalized_pencil {n : ℕ} {R : Type u_1} [Ring R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Algebra ℚ R] (L : Matrix ι ι (Form n)) (Z : Fin (n + 1) → R) (u : R) (hu : Z 0 * u = 1) : L.map (homogeneous (algebraMap ℚ R) Z) = (Matrix.scalar ι) (Z 0) * L.map ⇑(eval (algebraMap ℚ R) fun (i : Fin n) => u * Z i.succ)

theorem Complexity.RationalHitting.Affine.normalized_pencil_unit {n : ℕ} {R : Type u_1} [Ring R] {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Algebra ℚ R] (L : Matrix ι ι (Form n)) (Z : Fin (n + 1) → R) (z : Rˣ) (hz : ↑z = Z 0) (hL : IsUnit (L.map (homogeneous (algebraMap ℚ R) Z))) : IsUnit (L.map ⇑(eval (algebraMap ℚ R) fun (i : Fin n) => ↑z⁻¹ * Z i.succ))

theorem Complexity.RationalHitting.Affine.eval_reindex {n : ℕ} {K : Type v_2} [Field K] [CharZero K] {ι : Type v_3} {κ : Type v_4} [Fintype κ] [DecidableEq κ] (L : Matrix ι ι (Form n)) (X : Fin n → Matrix κ κ K) {ι' : Type v_5} (e : ι ≃ ι') : ((Matrix.reindex e e) L).map ⇑(eval (algebraMap ℚ (Matrix κ κ K)) X) = (Matrix.reindex e e) (L.map ⇑(eval (algebraMap ℚ (Matrix κ κ K)) X))

Reindexing a pencil's coefficients does not alter its matrix evaluation.

theorem Complexity.RationalHitting.Affine.homogeneous_flat {n : ℕ} {K : Type v_2} [Field K] [CharZero K] {ι : Type v_3} {κ : Type v_4} [Fintype ι] [Fintype κ] [DecidableEq κ] (L : Matrix ι ι (Form n)) (Z : Fin (n + 1) → Matrix κ κ K) : (Matrix.compRingEquiv ι κ K) (L.map (homogeneous (algebraMap ℚ (Matrix κ κ K)) Z)) = fun (a b : ι × κ) => ∑ r : Fin (n + 1), (algebraMap ℚ K) (coeff (L a.1 b.1) r) * Z r a.2 b.2

Homogeneous affine coefficients give exactly the ordinary Kronecker pencil.