Dyadic fusion for arithmetic circuits

Many arithmetic complexity measures obey a maximum rule for addition and a sum rule for multiplication. Degree is the basic example. If all generators and constants have measure at most one, a value of measure at least 2 ^ n requires n successive dyadic threshold crossings.

This file realizes that argument as a genuine fusion model. Its witnesses are the thresholds 2 ^ k, for k < n. Addition and constants preserve every witness. A multiplication can violate at most one witness, since two inputs below 2 ^ k produce a result below 2 ^ (k + 1). Therefore a fusion cover contains at least n multiplication atoms, and the generic circuit-to-cover theorem gives an exact multiplicative-complexity lower bound.

structure Algebraic.Fusion.Dyadic.Measure (K : Type u) (R : Type v) [Add R] [Mul R] (constant : K → R) : Type v

A natural-valued arithmetic measure with degree-like local bounds.

• value : R → ℕ

  Complexity assigned to a semantic arithmetic value.

• add_le (left right : R) : self.value (left + right) ≤ max (self.value left) (self.value right)

  Addition is maximum-bounded.

• mul_le (left right : R) : self.value (left * right) ≤ self.value left + self.value right

  Multiplication is sum-bounded.

• constant_le_one (scalar : K) : self.value (constant scalar) ≤ 1

  Every named constant starts below the first dyadic threshold.

def Algebraic.Fusion.Dyadic.model {K : Type u} {R : Type v} [Add R] [Mul R] {constant : K → R} (measure : Measure K R constant) (problem : Problem R) (levels : ℕ) (input_le_one : ∀ (input : Fin problem.inputCount), measure.value (problem.inputs input) ≤ 1) (target_ge : 2 ^ levels ≤ measure.value problem.target) : Model Arithmetic.multiplicationCost (Arithmetic.interpretation constant) problem

Fusion model whose observations are dyadic upper bounds on an arithmetic measure.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance Algebraic.Fusion.Dyadic.witnessFintype {K : Type u} {R : Type v} [Add R] [Mul R] {constant : K → R} (measure : Measure K R constant) (problem : Problem R) (levels : ℕ) (input_le_one : ∀ (input : Fin problem.inputCount), measure.value (problem.inputs input) ≤ 1) (target_ge : 2 ^ levels ≤ measure.value problem.target) : Fintype (model measure problem levels input_le_one target_ge).Witness

The dyadic model has the canonical finite witness enumeration.

Equations

• Algebraic.Fusion.Dyadic.witnessFintype measure problem levels input_le_one target_ge = id inferInstance

@[simp]

theorem Algebraic.Fusion.Dyadic.witness_card {K : Type u} {R : Type v} [Add R] [Mul R] {constant : K → R} (measure : Measure K R constant) (problem : Problem R) (levels : ℕ) (input_le_one : ∀ (input : Fin problem.inputCount), measure.value (problem.inputs input) ≤ 1) (target_ge : 2 ^ levels ≤ measure.value problem.target) : Fintype.card (model measure problem levels input_le_one target_ge).Witness = levels

theorem Algebraic.Fusion.Dyadic.add_preserved {K : Type u} {R : Type v} [Add R] [Mul R] {constant : K → R} (measure : Measure K R constant) (problem : Problem R) (levels : ℕ) (input_le_one : ∀ (input : Fin problem.inputCount), measure.value (problem.inputs input) ≤ 1) (target_ge : 2 ^ levels ≤ measure.value problem.target) (arguments : Fin 2 → R) (level : Fin levels) : { op := Arithmetic.Op.add, arguments := arguments }.PreservedBy (model measure problem levels input_le_one target_ge) level

Addition preserves every dyadic witness.

theorem Algebraic.Fusion.Dyadic.constant_preserved {K : Type u} {R : Type v} [Add R] [Mul R] {constant : K → R} (measure : Measure K R constant) (problem : Problem R) (levels : ℕ) (input_le_one : ∀ (input : Fin problem.inputCount), measure.value (problem.inputs input) ≤ 1) (target_ge : 2 ^ levels ≤ measure.value problem.target) (scalar : K) (arguments : Fin (Arithmetic.arity (Arithmetic.Op.constant scalar)) → R) (level : Fin levels) : { op := Arithmetic.Op.constant scalar, arguments := arguments }.PreservedBy (model measure problem levels input_le_one target_ge) level

Named constants preserve every dyadic witness.

theorem Algebraic.Fusion.Dyadic.bounds_of_mul_not_preserved {K : Type u} {R : Type v} [Add R] [Mul R] {constant : K → R} (measure : Measure K R constant) (problem : Problem R) (levels : ℕ) (input_le_one : ∀ (input : Fin problem.inputCount), measure.value (problem.inputs input) ≤ 1) (target_ge : 2 ^ levels ≤ measure.value problem.target) (arguments : Fin 2 → R) (level : Fin levels) (failure : ¬{ op := Arithmetic.Op.mul, arguments := arguments }.PreservedBy (model measure problem levels input_le_one target_ge) level) : (∀ (input : Fin 2), measure.value (arguments input) ≤ 2 ^ ↑level) ∧ 2 ^ ↑level < measure.value (arguments 0 * arguments 1)

Failure of a multiplication atom supplies bounds on both arguments and a strictly larger result.

theorem Algebraic.Fusion.Dyadic.mul_failure_unique {K : Type u} {R : Type v} [Add R] [Mul R] {constant : K → R} (measure : Measure K R constant) (problem : Problem R) (levels : ℕ) (input_le_one : ∀ (input : Fin problem.inputCount), measure.value (problem.inputs input) ≤ 1) (target_ge : 2 ^ levels ≤ measure.value problem.target) (arguments : Fin 2 → R) (first second : Fin levels) (firstFailure : ¬{ op := Arithmetic.Op.mul, arguments := arguments }.PreservedBy (model measure problem levels input_le_one target_ge) first) (secondFailure : ¬{ op := Arithmetic.Op.mul, arguments := arguments }.PreservedBy (model measure problem levels input_le_one target_ge) second) : first = second

One multiplication cannot cross two distinct dyadic thresholds.

noncomputable def Algebraic.Fusion.Dyadic.failureRules {K : Type u} {R : Type v} [Add R] [Mul R] {constant : K → R} (measure : Measure K R constant) (problem : Problem R) (levels : ℕ) (input_le_one : ∀ (input : Fin problem.inputCount), measure.value (problem.inputs input) ≤ 1) (target_ge : 2 ^ levels ≤ measure.value problem.target) : Arithmetic.FailureRules (model measure problem levels input_le_one target_ge)

The dyadic local lemmas packaged for the generic bounded-failure arithmetic interface. Its capacity is exactly one threshold per multiplication.

Equations

• Algebraic.Fusion.Dyadic.failureRules measure problem levels input_le_one target_ge = { capacity := 1, add_preserved := ⋯, constant_preserved := ⋯, mul_failure_card_le := ⋯ }

@[simp]

theorem Algebraic.Fusion.Dyadic.failureRules_capacity {K : Type u} {R : Type v} [Add R] [Mul R] {constant : K → R} (measure : Measure K R constant) (problem : Problem R) (levels : ℕ) (input_le_one : ∀ (input : Fin problem.inputCount), measure.value (problem.inputs input) ≤ 1) (target_ge : 2 ^ levels ≤ measure.value problem.target) : (failureRules measure problem levels input_le_one target_ge).capacity = 1

theorem Algebraic.Fusion.Dyadic.exists_unpreserved_multiplication {K : Type u} {R : Type v} [Add R] [Mul R] {constant : K → R} (measure : Measure K R constant) (problem : Problem R) (levels : ℕ) (input_le_one : ∀ (input : Fin problem.inputCount), measure.value (problem.inputs input) ≤ 1) (target_ge : 2 ^ levels ≤ measure.value problem.target) (cover : Cover (model measure problem levels input_le_one target_ge)) (level : Fin levels) : ∃ arguments ∈ Arithmetic.multiplicationArguments cover.atoms, ¬{ op := Arithmetic.Op.mul, arguments := arguments }.PreservedBy (model measure problem levels input_le_one target_ge) level

Every dyadic witness has an unpreserved multiplication in a fusion cover.

noncomputable def Algebraic.Fusion.Dyadic.failingArguments {K : Type u} {R : Type v} [Add R] [Mul R] {constant : K → R} (measure : Measure K R constant) (problem : Problem R) (levels : ℕ) (input_le_one : ∀ (input : Fin problem.inputCount), measure.value (problem.inputs input) ≤ 1) (target_ge : 2 ^ levels ≤ measure.value problem.target) (cover : Cover (model measure problem levels input_le_one target_ge)) (level : Fin levels) : Fin 2 → R

Arguments of a multiplication selected by one dyadic witness.

Equations

• Algebraic.Fusion.Dyadic.failingArguments measure problem levels input_le_one target_ge cover level = Classical.choose ⋯

theorem Algebraic.Fusion.Dyadic.failingArguments_mem {K : Type u} {R : Type v} [Add R] [Mul R] {constant : K → R} (measure : Measure K R constant) (problem : Problem R) (levels : ℕ) (input_le_one : ∀ (input : Fin problem.inputCount), measure.value (problem.inputs input) ≤ 1) (target_ge : 2 ^ levels ≤ measure.value problem.target) (cover : Cover (model measure problem levels input_le_one target_ge)) (level : Fin levels) : failingArguments measure problem levels input_le_one target_ge cover level ∈ Arithmetic.multiplicationArguments cover.atoms

theorem Algebraic.Fusion.Dyadic.failingArguments_spec {K : Type u} {R : Type v} [Add R] [Mul R] {constant : K → R} (measure : Measure K R constant) (problem : Problem R) (levels : ℕ) (input_le_one : ∀ (input : Fin problem.inputCount), measure.value (problem.inputs input) ≤ 1) (target_ge : 2 ^ levels ≤ measure.value problem.target) (cover : Cover (model measure problem levels input_le_one target_ge)) (level : Fin levels) : ¬{ op := Arithmetic.Op.mul, arguments := failingArguments measure problem levels input_le_one target_ge cover level }.PreservedBy (model measure problem levels input_le_one target_ge) level

noncomputable def Algebraic.Fusion.Dyadic.failingMultiplication {K : Type u} {R : Type v} [Add R] [Mul R] {constant : K → R} (measure : Measure K R constant) (problem : Problem R) (levels : ℕ) (input_le_one : ∀ (input : Fin problem.inputCount), measure.value (problem.inputs input) ≤ 1) (target_ge : 2 ^ levels ≤ measure.value problem.target) (cover : Cover (model measure problem levels input_le_one target_ge)) (level : Fin levels) : Fin (Arithmetic.multiplicationArguments cover.atoms).length

Index of the multiplication selected by one dyadic witness.

Equations

• Algebraic.Fusion.Dyadic.failingMultiplication measure problem levels input_le_one target_ge cover level = Classical.choose ⋯

theorem Algebraic.Fusion.Dyadic.get_failingMultiplication {K : Type u} {R : Type v} [Add R] [Mul R] {constant : K → R} (measure : Measure K R constant) (problem : Problem R) (levels : ℕ) (input_le_one : ∀ (input : Fin problem.inputCount), measure.value (problem.inputs input) ≤ 1) (target_ge : 2 ^ levels ≤ measure.value problem.target) (cover : Cover (model measure problem levels input_le_one target_ge)) (level : Fin levels) : (Arithmetic.multiplicationArguments cover.atoms).get (failingMultiplication measure problem levels input_le_one target_ge cover level) = failingArguments measure problem levels input_le_one target_ge cover level

theorem Algebraic.Fusion.Dyadic.failingMultiplication_spec {K : Type u} {R : Type v} [Add R] [Mul R] {constant : K → R} (measure : Measure K R constant) (problem : Problem R) (levels : ℕ) (input_le_one : ∀ (input : Fin problem.inputCount), measure.value (problem.inputs input) ≤ 1) (target_ge : 2 ^ levels ≤ measure.value problem.target) (cover : Cover (model measure problem levels input_le_one target_ge)) (level : Fin levels) : ¬{ op := Arithmetic.Op.mul, arguments := (Arithmetic.multiplicationArguments cover.atoms).get (failingMultiplication measure problem levels input_le_one target_ge cover level) }.PreservedBy (model measure problem levels input_le_one target_ge) level

The selected multiplication really fails its witness.

theorem Algebraic.Fusion.Dyadic.failingMultiplication_injective {K : Type u} {R : Type v} [Add R] [Mul R] {constant : K → R} (measure : Measure K R constant) (problem : Problem R) (levels : ℕ) (input_le_one : ∀ (input : Fin problem.inputCount), measure.value (problem.inputs input) ≤ 1) (target_ge : 2 ^ levels ≤ measure.value problem.target) (cover : Cover (model measure problem levels input_le_one target_ge)) : Function.Injective (failingMultiplication measure problem levels input_le_one target_ge cover)

Distinct thresholds select distinct multiplication atoms.

theorem Algebraic.Fusion.Dyadic.cover_cost_lowerBound {K : Type u} {R : Type v} [Add R] [Mul R] {constant : K → R} (measure : Measure K R constant) (problem : Problem R) (levels : ℕ) (input_le_one : ∀ (input : Fin problem.inputCount), measure.value (problem.inputs input) ≤ 1) (target_ge : 2 ^ levels ≤ measure.value problem.target) (cover : Cover (model measure problem levels input_le_one target_ge)) : levels ≤ cover.cost

Every fusion cover pays one multiplication for every dyadic threshold.

theorem Algebraic.Fusion.Dyadic.circuit_multiplication_lowerBound {K : Type u} {R : Type v} [Add R] [Mul R] {constant : K → R} (measure : Measure K R constant) (problem : Problem R) (levels : ℕ) (input_le_one : ∀ (input : Fin problem.inputCount), measure.value (problem.inputs input) ≤ 1) (target_ge : 2 ^ levels ≤ measure.value problem.target) (circuit : Circuit (Arithmetic.signature K) problem.inputCount 1) (constructs : problem.Constructs circuit (Arithmetic.interpretation constant)) : levels ≤ circuit.cost Arithmetic.multiplicationCost

A dyadic measure lower bound transfers to every arithmetic circuit constructing the target.