Rational hitting lists: evaluation

Basic properties of the partial evaluation of rational formulas: values are unique, they are transported along ring homomorphisms, and they lift back along homomorphisms reflecting units.

Main results

• Cslib.Circuits.Rational.Formula.Eval.unique: a formula has at most one value.
• Cslib.Circuits.Rational.Formula.Eval.map: values are mapped by ring homomorphisms.
• Cslib.Circuits.Rational.Formula.Eval.lift: values lift along homomorphisms reflecting units.
• Cslib.Circuits.Rational.Formula.Eval.unit_of_division_lift: a nonzero value mapped out of a division ring is a unit.

References

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

theorem Cslib.Circuits.Rational.Formula.Eval.unique {n : ℕ} {R : Type u_1} [Ring R] {c : ℚ →+* R} {X : Fin n → R} {h : Formula n} {a b : R} (ha : Eval c X h a) (hb : Eval c X h b) : a = b

A formula has at most one value at a substitution.

theorem Cslib.Circuits.Rational.Formula.Eval.map {n : ℕ} {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] {c : ℚ →+* R} {X : Fin n → R} {h : Formula n} {a : R} (ha : Eval c X h a) (f : R →+* S) : Eval (f.comp c) (fun (i : Fin n) => f (X i)) h (f a)

A ring homomorphism maps a value of a formula to a value at the mapped substitution.

theorem Cslib.Circuits.Rational.Formula.Eval.lift {n : ℕ} {R : Type u_1} {S : Type u_2} [Ring R] [Ring S] (f : R →+* S) (hf : ∀ (x : R), IsUnit (f x) → IsUnit x) {c : ℚ →+* R} {X : Fin n → R} {h : Formula n} {a : S} (ha : Eval (f.comp c) (fun (i : Fin n) => f (X i)) h a) : ∃ (b : R), Eval c X h b ∧ f b = a

Defined evaluations lift through a homomorphism reflecting units. In particular this handles every inverse occurrence before considering the root.

theorem Cslib.Circuits.Rational.Formula.Eval.unit_of_division_lift {n : ℕ} {R : Type u_1} [Ring R] {D : Type u_3} [DivisionRing D] [Nontrivial R] (f : D →+* R) {c : ℚ →+* D} {X : Fin n → D} {h : Formula n} {a : R} (ha : Eval (f.comp c) (fun (i : Fin n) => f (X i)) h a) (ha0 : a ≠ 0) : IsUnit a

Mapping a defined nonzero value out of a division ring makes it a unit. This is used after the partial-specialization domain proof, not instead of it.