Fusion atoms of binary power circuits #
The implementation-independent semantic contract needed by local Fusion
arguments: every multiplication atom emitted while computing x^d produces
x^e for some e ≤ d. Polynomial degree arguments are downstream
instances of this generic arithmetic fact.
def
Algebraic.Fusion.Arithmetic.Power.MultiplicationPowerAtMost
{K R : Type}
[Mul R]
[Pow R ℕ]
(base : R)
(bound : ℕ)
(atom : Atom (Arithmetic.signature K) R)
:
A multiplication atom's result is a bounded natural power of base.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Algebraic.Fusion.Arithmetic.Power.binaryCircuit_multiplicationPowerAtMost
{K R : Type}
[Semiring R]
[One K]
(constant : K → R)
(mapsOne : constant 1 = 1)
(input : Fin 1 → R)
(exponent : ℕ)
(atom : Atom (Arithmetic.signature K) R)
(present : atom ∈ circuitAtoms (Arithmetic.Power.binaryCircuit exponent) (Arithmetic.interpretation constant) input)
:
MultiplicationPowerAtMost (input 0) exponent atom
Every multiplication atom of the shared binary-power circuit computes a power bounded by the requested exponent.