Rational hitting lists: affine realizations

Every rational formula f has a linear realization: a square matrix Formula.pencil f of affine forms in the variables, indexed by a finite type Formula.Index f with f.nodeCount + 1 elements, together with a rational row and column. Wherever f is defined, the evaluated pencil is invertible and the row, inverse and column multiply to the value of f. Conversely, f is defined with an invertible value exactly when the pencils of its inverse nodes and of its augmented root are invertible (Formula.certificates_iff); no rational cancellation is performed.

Main definitions

• Cslib.Circuits.Rational.Affine.Form, Cslib.Circuits.Rational.Affine.eval: affine forms and their evaluation.
• Cslib.Circuits.Rational.Formula.Index, Cslib.Circuits.Rational.Formula.pencil, Cslib.Circuits.Rational.Formula.row, Cslib.Circuits.Rational.Formula.col: the realization.
• Cslib.Circuits.Rational.Formula.inverseNodes, Cslib.Circuits.Rational.Formula.certificates: the inverse occurrences of a formula, and these together with the augmented root.

Main results

• Cslib.Circuits.Rational.Formula.card_index: the realization has f.nodeCount + 1 rows.
• Cslib.Circuits.Rational.Formula.Eval.realization: exact realization of defined formulas.
• Cslib.Circuits.Rational.Formula.certificates_iff: invertible certificate pencils are equivalent to a defined invertible value.
• Cslib.Circuits.Rational.Formula.certificate_bounds: the number and sizes of the certificates.

References

• Adapted from OpenAI's formalization [OAI26a] at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a (file lean/OAI/Computability/RationalHitting/Affine.lean), via the complexitylib port [Sch26d] at revision add0aca8ee0d71e68969f2cb45cf91554a50f787.

@[reducible, inline]

abbrev Cslib.Circuits.Rational.Affine.Form (n : ℕ) : Type

A constant coefficient and one rational coefficient per variable.

def Cslib.Circuits.Rational.Affine.constant {n : ℕ} (a : ℚ) : Form n

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

def Cslib.Circuits.Rational.Affine.varForm {n : ℕ} (i : Fin n) : Form n

The affine coordinate form for one variable.

def Cslib.Circuits.Rational.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.

@[simp]

theorem Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.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.

@[simp]

theorem Cslib.Circuits.Rational.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

The realization is defined by recursion on the native constructors input and gate, so that its index type reduces to sums of the index types of the arguments args j. The proofs below therefore also proceed by induction on the native constructors.

@[reducible]

def Cslib.Circuits.Rational.Formula.Index {n : ℕ} : Formula n → Type

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

@[reducible]

instance Cslib.Circuits.Rational.Formula.indexFintype {n : ℕ} (f : Formula n) : Fintype f.Index

The index type of a realization is finite.

@[reducible]

instance Cslib.Circuits.Rational.Formula.indexDecidableEq {n : ℕ} (f : Formula n) : DecidableEq f.Index

The index type of a realization has decidable equality.

theorem Cslib.Circuits.Rational.Formula.card_index {n : ℕ} (f : Formula n) : Fintype.card f.Index = f.nodeCount + 1

The realization of a formula has one more row than the formula has nodes.

def Cslib.Circuits.Rational.Formula.row {n : ℕ} (f : Formula n) : Matrix Unit f.Index ℚ

The left row of the formula's linear realization.

def Cslib.Circuits.Rational.Formula.col {n : ℕ} (f : Formula n) : Matrix f.Index Unit ℚ

The right column of the formula's linear realization.

def Cslib.Circuits.Rational.Formula.pencil {n : ℕ} (f : Formula n) : Matrix f.Index f.Index (Affine.Form n)

The affine matrix pencil built recursively from a rational formula.

@[reducible, inline]

abbrev Cslib.Circuits.Rational.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.

@[reducible, inline]

abbrev Cslib.Circuits.Rational.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.

@[reducible, inline]

abbrev Cslib.Circuits.Rational.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.

@[reducible, inline]

abbrev Cslib.Circuits.Rational.Formula.scalar {R : Type u_1} [Ring R] (a : R) : Matrix Unit Unit R

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

theorem Cslib.Circuits.Rational.Formula.realized_add {n : ℕ} {R : Type u_1} [Ring R] (c : ℚ →+* R) (X : Fin n → R) (a : Fin (ratSignature.Arity RatOp.add) → Formula n) : realized c X (Formula.gate RatOp.add a) = Matrix.fromBlocks (realized c X (a 0)) 0 0 (realized c X (a 1))

theorem Cslib.Circuits.Rational.Formula.realized_mul {n : ℕ} {R : Type u_1} [Ring R] (c : ℚ →+* R) (X : Fin n → R) (m : Fin (ratSignature.Arity RatOp.mul) → Formula n) : realized c X (Formula.gate RatOp.mul m) = Matrix.fromBlocks (realized c X (m 0)) (-colR c (m 0) * rowR c (m 1)) 0 (realized c X (m 1))

theorem Cslib.Circuits.Rational.Formula.realized_inv {n : ℕ} {R : Type u_1} [Ring R] (c : ℚ →+* R) (X : Fin n → R) (b : Fin (ratSignature.Arity RatOp.inv) → Formula n) : realized c X (Formula.gate RatOp.inv b) = Matrix.fromBlocks (realized c X (b 0)) (colR c (b 0)) (rowR c (b 0)) 0

theorem Cslib.Circuits.Rational.Formula.rowR_add {n : ℕ} {R : Type u_1} [Ring R] (c : ℚ →+* R) (a : Fin (ratSignature.Arity RatOp.add) → Formula n) : rowR c (Formula.gate RatOp.add a) = (rowR c (a 0)).fromCols (rowR c (a 1))

theorem Cslib.Circuits.Rational.Formula.colR_add {n : ℕ} {R : Type u_1} [Ring R] (c : ℚ →+* R) (a : Fin (ratSignature.Arity RatOp.add) → Formula n) : colR c (Formula.gate RatOp.add a) = (colR c (a 0)).fromRows (colR c (a 1))

theorem Cslib.Circuits.Rational.Formula.rowR_mul {n : ℕ} {R : Type u_1} [Ring R] (c : ℚ →+* R) (m : Fin (ratSignature.Arity RatOp.mul) → Formula n) : rowR c (Formula.gate RatOp.mul m) = (rowR c (m 0)).fromCols 0

theorem Cslib.Circuits.Rational.Formula.colR_mul {n : ℕ} {R : Type u_1} [Ring R] (c : ℚ →+* R) (m : Fin (ratSignature.Arity RatOp.mul) → Formula n) : colR c (Formula.gate RatOp.mul m) = Matrix.fromRows 0 (colR c (m 1))

theorem Cslib.Circuits.Rational.Formula.rowR_inv {n : ℕ} {R : Type u_1} [Ring R] (c : ℚ →+* R) (b : Fin (ratSignature.Arity RatOp.inv) → Formula n) : rowR c (Formula.gate RatOp.inv b) = Matrix.fromCols 0 (-1)

theorem Cslib.Circuits.Rational.Formula.colR_inv {n : ℕ} {R : Type u_1} [Ring R] (c : ℚ →+* R) (b : Fin (ratSignature.Arity RatOp.inv) → Formula n) : colR c (Formula.gate RatOp.inv b) = Matrix.fromRows 0 1

theorem Cslib.Circuits.Rational.Formula.realized_input {n : ℕ} {R : Type u_1} [Ring R] (c : ℚ →+* R) (X : Fin n → R) (i : Fin n) : realized c X (Formula.input i) = Matrix.fromBlocks 1 (-scalar (X i)) 0 1

theorem Cslib.Circuits.Rational.Formula.realized_const {n : ℕ} {R : Type u_1} [Ring R] (c : ℚ →+* R) (X : Fin n → R) (q : ℚ) (args : Fin (ratSignature.Arity (RatOp.const q)) → Formula n) : realized c X (Formula.gate (RatOp.const q) args) = Matrix.fromBlocks 1 (-scalar (c q)) 0 1

theorem Cslib.Circuits.Rational.Formula.rowR_input {n : ℕ} {R : Type u_1} [Ring R] (c : ℚ →+* R) (i : Fin n) : rowR c (Formula.input i) = Matrix.fromCols 1 0

theorem Cslib.Circuits.Rational.Formula.colR_input {n : ℕ} {R : Type u_1} [Ring R] (c : ℚ →+* R) (i : Fin n) : colR c (Formula.input i) = Matrix.fromRows 0 1

theorem Cslib.Circuits.Rational.Formula.rowR_const {n : ℕ} {R : Type u_1} [Ring R] (c : ℚ →+* R) (q : ℚ) (args : Fin (ratSignature.Arity (RatOp.const q)) → Formula n) : rowR c (Formula.gate (RatOp.const q) args) = Matrix.fromCols 1 0

theorem Cslib.Circuits.Rational.Formula.colR_const {n : ℕ} {R : Type u_1} [Ring R] (c : ℚ →+* R) (q : ℚ) (args : Fin (ratSignature.Arity (RatOp.const q)) → Formula n) : colR c (Formula.gate (RatOp.const q) args) = Matrix.fromRows 0 1

theorem Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.Formula.Eval.realization {n : ℕ} {R : Type u_1} [Ring R] (c : ℚ →+* R) (X : Fin n → R) {f : Formula n} {v : R} (hv : Eval c X f v) : ∃ (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 v

Exact affine realization of every defined formula: the evaluated pencil is invertible, and the row, its inverse and the column multiply to the value.

def Cslib.Circuits.Rational.Formula.inverseNodes {n : ℕ} : Formula n → List (Formula n)

The inverse nodes of a formula, as a list retaining occurrences rather than distinct subexpressions.

@[simp]

theorem Cslib.Circuits.Rational.Formula.inverseNodes_var {n : ℕ} (i : Fin n) : (var i).inverseNodes = []

@[simp]

theorem Cslib.Circuits.Rational.Formula.inverseNodes_const {n : ℕ} (q : ℚ) : (const q).inverseNodes = []

@[simp]

theorem Cslib.Circuits.Rational.Formula.inverseNodes_add {n : ℕ} (f g : Formula n) : (f.add g).inverseNodes = f.inverseNodes ++ g.inverseNodes

@[simp]

theorem Cslib.Circuits.Rational.Formula.inverseNodes_mul {n : ℕ} (f g : Formula n) : (f.mul g).inverseNodes = f.inverseNodes ++ g.inverseNodes

@[simp]

theorem Cslib.Circuits.Rational.Formula.inverseNodes_inv {n : ℕ} (f : Formula n) : f.inv.inverseNodes = f.inv :: f.inverseNodes

def Cslib.Circuits.Rational.Formula.certificates {n : ℕ} (f : Formula n) : List (Formula n)

The inverse nodes together with the augmented root inv f, which is a certificate pencil and not a new counted gate.

theorem Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.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

At a defined point, the augmented pencil is invertible exactly when the value is.

theorem Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.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 invertibility of all affine-pencil certificates. No rational cancellation is performed.

theorem Cslib.Circuits.Rational.Formula.inverseNodes_length {n : ℕ} (f : Formula n) : f.inverseNodes.length ≤ f.nodeCount

theorem Cslib.Circuits.Rational.Formula.nodeCount_le_of_mem_inverseNodes {n : ℕ} {f h : Formula n} (hh : h ∈ f.inverseNodes) : h.nodeCount ≤ f.nodeCount

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

A formula with at most s nodes has at most s + 1 certificates, each of dimension at most 2 * s + 1.

def Cslib.Circuits.Rational.Affine.coeff {n : ℕ} (a : Form n) : Fin (n + 1) → ℚ

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

def Cslib.Circuits.Rational.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.

theorem Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.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 Cslib.Circuits.Rational.Affine.eval_reindex {n : ℕ} {K : Type u_2} [Field K] [CharZero K] {ι : Type u_3} {ι' : Type u_4} {κ : Type u_5} [Fintype κ] [DecidableEq κ] (L : Matrix ι ι (Form n)) (X : Fin n → Matrix κ κ K) (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 Cslib.Circuits.Rational.Affine.homogeneous_flat {n : ℕ} {K : Type u_2} [Field K] [CharZero K] {ι : Type u_3} {κ : Type u_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.