Local Fusion properties of compiled arithmetic expressions #
An expression can carry a semantic predicate that must hold at the output of every multiplication node. Tree compilation preserves this predicate at every extracted multiplication atom. This packages local gate-shape proofs independently of any particular rank measure or polynomial family.
def
Algebraic.Fusion.Arithmetic.Expression.MultiplicationProperty
{C R : Type}
{n : ℕ}
[Add R]
[Mul R]
(constant : C → R)
(input : Fin n → R)
(property : R → Prop)
:
Arithmetic.Expression C n → Prop
A semantic predicate holds at the result of every multiplication node in an arithmetic expression.
Equations
- One or more equations did not get rendered due to their size.
- Algebraic.Fusion.Arithmetic.Expression.MultiplicationProperty constant input property (Algebraic.Arithmetic.Expression.input index) = True
- Algebraic.Fusion.Arithmetic.Expression.MultiplicationProperty constant input property (Algebraic.Arithmetic.Expression.constant value) = True
Instances For
theorem
Algebraic.Fusion.Arithmetic.Expression.multiplicationProperty_of_atom
{C R : Type}
{n : ℕ}
[Add R]
[Mul R]
(constant : C → R)
(input : Fin n → R)
(property : R → Prop)
(expression : Arithmetic.Expression C n)
(holds : MultiplicationProperty constant input property expression)
(arguments : Fin 2 → R)
(present :
{ op := Arithmetic.Op.mul, arguments := arguments } ∈ circuitAtoms expression.circuit (Arithmetic.interpretation constant) input)
:
property (arguments 0 * arguments 1)
Every multiplication atom emitted by expression compilation satisfies the expression's multiplication-result predicate.