Rational hitting lists: the model

Noncommutative rational formulas are formulas (Cslib.Circuits.Formula) over the signature ratSignature of rational constants, addition, ordered multiplication and inversion. They are evaluated relationally in any ring with a rational structure map: an inverse node requires an actual two-sided inverse of its operand's value, so evaluation is partial. A formula is admissible if some substitution of square rational matrices of positive dimension lies in its domain, and nonzero if some such substitution yields a nonzero value. A finite list of matrix substitutions hits the formulas of node count at most s if every admissible nonzero such formula has an invertible value at some substitution on the list.

The node count of a formula, the source's size measure, counts every syntax-tree node: input leaves, constants and operations (Formula.nodeCount, the native gate count Formula.size plus the leaf count Formula.leafSize).

Main definitions

• Cslib.Circuits.Rational.ratSignature, Cslib.Circuits.Rational.Formula: the signature and the formulas, with constructors Formula.var, Formula.const, Formula.add, Formula.mul, Formula.inv and the induction principle Formula.inductionOn.
• Cslib.Circuits.Rational.Formula.nodeCount: the number of syntax-tree nodes.
• Cslib.Circuits.Rational.Formula.Eval: partial evaluation as a relation.
• Cslib.Circuits.Rational.Evaluates, Cslib.Circuits.Rational.Admissible, Cslib.Circuits.Rational.Nonzero: evaluation on rational matrices, and its domain and support.
• Cslib.Circuits.Rational.Output, Cslib.Circuits.Rational.encodeOutput: lists of matrix substitutions of a common positive dimension and their binary encoding.
• Cslib.Circuits.Rational.Hits: the hitting property.

Main results

• Cslib.Circuits.Rational.Formula.eval_add_iff and its siblings: evaluation unfolds along the constructors.

References

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

inductive Cslib.Circuits.Rational.RatOp : Type

The operation symbols of noncommutative rational formulas.

• const (q : ℚ) : RatOp

  A rational constant.

• add : RatOp

  Addition.

• mul : RatOp

  Ordered multiplication.

• inv : RatOp

  Inversion.

@[instance_reducible]

instance Cslib.Circuits.Rational.instDecidableEqRatOp : DecidableEq RatOp

def Cslib.Circuits.Rational.instDecidableEqRatOp.decEq (x✝ x✝¹ : RatOp) : Decidable (x✝ = x✝¹)

@[reducible, inline]

abbrev Cslib.Circuits.Rational.ratSignature : Signature

The signature of rational formulas: constants are nullary, addition and multiplication are binary, and inversion is unary.

@[reducible, inline]

abbrev Cslib.Circuits.Rational.Formula (n : ℕ) : Type

A noncommutative rational formula over n variables and rational constants.

@[reducible, inline]

abbrev Cslib.Circuits.Rational.Formula.var {n : ℕ} (i : Fin n) : Formula n

The input variable i.

@[reducible, inline]

abbrev Cslib.Circuits.Rational.Formula.const {n : ℕ} (q : ℚ) : Formula n

The rational constant q.

@[reducible, inline]

abbrev Cslib.Circuits.Rational.Formula.add {n : ℕ} (f g : Formula n) : Formula n

The sum of two formulas.

@[reducible, inline]

abbrev Cslib.Circuits.Rational.Formula.mul {n : ℕ} (f g : Formula n) : Formula n

The ordered product of two formulas.

@[reducible, inline]

abbrev Cslib.Circuits.Rational.Formula.inv {n : ℕ} (f : Formula n) : Formula n

The inverse of a formula.

theorem Cslib.Circuits.Rational.Formula.inductionOn {n : ℕ} {motive : Formula n → Prop} (f : Formula n) (var : ∀ (i : Fin n), motive (var i)) (const : ∀ (q : ℚ), motive (const q)) (add : ∀ (f g : Formula n), motive f → motive g → motive (f.add g)) (mul : ∀ (f g : Formula n), motive f → motive g → motive (f.mul g)) (inv : ∀ (f : Formula n), motive f → motive f.inv) : motive f

Induction on rational formulas, with one case for each constructor.

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

The number of syntax-tree nodes, counting input leaves, constants and operations alike: the operation nodes Formula.size together with the input leaves Formula.leafSize.

@[simp]

theorem Cslib.Circuits.Rational.Formula.nodeCount_var {n : ℕ} (i : Fin n) : (var i).nodeCount = 1

@[simp]

theorem Cslib.Circuits.Rational.Formula.nodeCount_const {n : ℕ} (q : ℚ) : (const q).nodeCount = 1

@[simp]

theorem Cslib.Circuits.Rational.Formula.nodeCount_add {n : ℕ} (f g : Formula n) : (f.add g).nodeCount = f.nodeCount + g.nodeCount + 1

@[simp]

theorem Cslib.Circuits.Rational.Formula.nodeCount_mul {n : ℕ} (f g : Formula n) : (f.mul g).nodeCount = f.nodeCount + g.nodeCount + 1

@[simp]

theorem Cslib.Circuits.Rational.Formula.nodeCount_inv {n : ℕ} (f : Formula n) : f.inv.nodeCount = f.nodeCount + 1

theorem Cslib.Circuits.Rational.Formula.nodeCount_pos {n : ℕ} (f : Formula n) : 0 < f.nodeCount

A formula has at least one node.

def Cslib.Circuits.Rational.Formula.Eval {n : ℕ} {R : Type u} [Ring R] (c : ℚ →+* R) (X : Fin n → R) : Formula n → R → Prop

f.Eval c X v: the formula f is defined at the substitution X in the ring R, with rational constants interpreted by c, and has the value v. An inverse node requires an actual two-sided inverse of the value of its operand, not a totalized inverse.

@[simp]

theorem Cslib.Circuits.Rational.Formula.eval_var_iff {n : ℕ} {R : Type u} [Ring R] {c : ℚ →+* R} {X : Fin n → R} {v : R} {i : Fin n} : Eval c X (var i) v ↔ v = X i

@[simp]

theorem Cslib.Circuits.Rational.Formula.eval_const_iff {n : ℕ} {R : Type u} [Ring R] {c : ℚ →+* R} {X : Fin n → R} {v : R} {q : ℚ} : Eval c X (const q) v ↔ v = c q

@[simp]

theorem Cslib.Circuits.Rational.Formula.eval_add_iff {n : ℕ} {R : Type u} [Ring R] {c : ℚ →+* R} {X : Fin n → R} {f g : Formula n} {v : R} : Eval c X (f.add g) v ↔ ∃ (a : R) (b : R), Eval c X f a ∧ Eval c X g b ∧ v = a + b

@[simp]

theorem Cslib.Circuits.Rational.Formula.eval_mul_iff {n : ℕ} {R : Type u} [Ring R] {c : ℚ →+* R} {X : Fin n → R} {f g : Formula n} {v : R} : Eval c X (f.mul g) v ↔ ∃ (a : R) (b : R), Eval c X f a ∧ Eval c X g b ∧ v = a * b

@[simp]

theorem Cslib.Circuits.Rational.Formula.eval_inv_iff {n : ℕ} {R : Type u} [Ring R] {c : ℚ →+* R} {X : Fin n → R} {f : Formula n} {v : R} : Eval c X f.inv v ↔ ∃ (a : R), Eval c X f a ∧ a * v = 1 ∧ v * a = 1

theorem Cslib.Circuits.Rational.Formula.Eval.var {n : ℕ} {R : Type u} [Ring R] {c : ℚ →+* R} {X : Fin n → R} (i : Fin n) : Eval c X (Formula.var i) (X i)

A variable evaluates to its assigned value.

theorem Cslib.Circuits.Rational.Formula.Eval.const {n : ℕ} {R : Type u} [Ring R] {c : ℚ →+* R} {X : Fin n → R} (q : ℚ) : Eval c X (Formula.const q) (c q)

A constant evaluates through the scalar homomorphism.

theorem Cslib.Circuits.Rational.Formula.Eval.add {n : ℕ} {R : Type u} [Ring R] {c : ℚ →+* R} {X : Fin n → R} {f g : Formula n} {a b : R} (ha : Eval c X f a) (hb : Eval c X g b) : Eval c X (f.add g) (a + b)

Defined summands give a defined sum.

theorem Cslib.Circuits.Rational.Formula.Eval.mul {n : ℕ} {R : Type u} [Ring R] {c : ℚ →+* R} {X : Fin n → R} {f g : Formula n} {a b : R} (ha : Eval c X f a) (hb : Eval c X g b) : Eval c X (f.mul g) (a * b)

Defined factors give a defined ordered product.

theorem Cslib.Circuits.Rational.Formula.Eval.inv {n : ℕ} {R : Type u} [Ring R] {c : ℚ →+* R} {X : Fin n → R} {f : Formula n} {a b : R} (ha : Eval c X f a) (hab : a * b = 1) (hba : b * a = 1) : Eval c X f.inv b

An inverse node is defined at a two-sided inverse of the value of its operand.

@[reducible, inline]

abbrev Cslib.Circuits.Rational.Mat (d : ℕ) : Type

Square rational matrices of the specified dimension.

@[reducible, inline]

abbrev Cslib.Circuits.Rational.Tuple (n d : ℕ) : Type

A matrix substitution for every input variable.

def Cslib.Circuits.Rational.Evaluates {n d : ℕ} (f : Formula n) (X : Tuple n d) (v : Mat d) : Prop

Defined evaluation on a rational matrix tuple.

def Cslib.Circuits.Rational.Admissible {n : ℕ} (f : Formula n) : Prop

Some positive-dimensional rational matrix substitution is in the formula's domain.

def Cslib.Circuits.Rational.Nonzero {n : ℕ} (f : Formula n) : Prop

Some positive-dimensional rational matrix substitution has a defined nonzero value.

structure Cslib.Circuits.Rational.Output (n : ℕ) : Type

A finite list of matrix substitutions, all of one common positive dimension.

• dimension : ℕ

  Common dimension of all matrix tuples.

• dimension_pos : 0 < self.dimension

  Exclude the trivial zero-dimensional matrix ring.

• tuples : List (Tuple n self.dimension)

  The finite list of matrix substitutions, in output order.

def Cslib.Circuits.Rational.encodeNat (a : ℕ) : List Bool

Little-endian unsigned binary, prefixed by a unary bit-length and a zero terminator. This is a self-delimiting binary encoding, including zero.

def Cslib.Circuits.Rational.encodeRat (a : ℚ) : List Bool

Sign bit, binary numerator magnitude, and positive binary denominator. Rat.num and Rat.den are the canonical reduced numerator and denominator.

def Cslib.Circuits.Rational.encodeTuple {n d : ℕ} (X : Tuple n d) : List Bool

Serialize a tuple in variable, row, and column order using reduced rational encodings.

def Cslib.Circuits.Rational.encodeOutput {n : ℕ} (H : Output n) : List Bool

Encode the common dimension, tuple count, and all rational matrix entries.

def Cslib.Circuits.Rational.Hits {n : ℕ} (s : ℕ) (H : Output n) : Prop

Every admissible nonzero formula with at most s nodes has an invertible value at some substitution on the list.