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 (the generic Cslib.Circuits.Formula.nodeCount, the native gate count Formula.size plus the leaf count Formula.leafSize).

Main definitions

• Cslib.Circuits.Rational.RatOp, Cslib.Circuits.Rational.ratSignature, Cslib.Circuits.Rational.Formula: the operation symbols, signature, and formulas, with constructors Formula.var, Formula.const, Formula.add, Formula.mul, Formula.inv and the induction principle Formula.inductionOn.
• Cslib.Circuits.Rational.Formula.Eval: partial evaluation as a relation.
• Cslib.Circuits.Rational.Mat, Cslib.Circuits.Rational.Tuple: square rational matrices and matrix substitutions.
• 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.encodeNat, Cslib.Circuits.Rational.encodeRat, Cslib.Circuits.Rational.encodeTuple, 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.

The generic Cslib.Circuits.Formula.nodeCount_input and Cslib.Circuits.Formula.nodeCount_gate specialized to the constructors; simp derives these from the generic lemmas, so they are not simp lemmas themselves.

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

A variable leaf has node count 1.

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

A rational constant node has node count 1.

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

The node count of add f g is f.nodeCount + g.nodeCount + 1.

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

The node count of mul f g is f.nodeCount + g.nodeCount + 1.

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

The node count of inv f is f.nodeCount + 1.

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

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

(var i).Eval c X v holds if and only if 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

(const q).Eval c X v holds if and only if 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

(add f g).Eval c X v holds if and only if f and g evaluate to a and b with 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

(mul f g).Eval c X v holds if and only if f and g evaluate to a and b with 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

(inv f).Eval c X v holds if and only if f evaluates to a two-sided inverse a of v.

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.