Canonical quotient-feature Fusion

Quotient the semantic vector space by the linear span of every free input and named constant. The quotient map is then a canonical linear feature that annihilates all zero-cost data. Addition cannot create a new quotient direction, while each multiplication can create at most one.

Consequently, the dimension of the requested outputs modulo free data is a multiplication lower bound. No hand-designed feature coordinates are needed.

def Algebraic.Fusion.Arithmetic.Interaction.Linear.Quotient.freeSubmodule {C : Type v} {U : Type w} (K : Type u) [Semiring K] [AddCommMonoid U] [Module K U] (constant : C → U) (problem : Problem U) : Submodule K U

Linear span of all semantic values available without a multiplication or addition gate: free problem inputs and named scalar constants.

Equations

• Algebraic.Fusion.Arithmetic.Interaction.Linear.Quotient.freeSubmodule K constant problem = Submodule.span K (Set.range problem.inputs ∪ Set.range constant)

theorem Algebraic.Fusion.Arithmetic.Interaction.Linear.Quotient.input_mem_freeSubmodule {K : Type u} {C : Type v} {U : Type w} [Semiring K] [AddCommMonoid U] [Module K U] (constant : C → U) (problem : Problem U) (input : Fin problem.inputCount) : problem.inputs input ∈ freeSubmodule K constant problem

Every free input belongs to the free-data submodule.

theorem Algebraic.Fusion.Arithmetic.Interaction.Linear.Quotient.constant_mem_freeSubmodule {K : Type u} {C : Type v} {U : Type w} [Semiring K] [AddCommMonoid U] [Module K U] (constant : C → U) (problem : Problem U) (scalar : C) : constant scalar ∈ freeSubmodule K constant problem

Every named constant belongs to the free-data submodule.

def Algebraic.Fusion.Arithmetic.Interaction.Linear.Quotient.certificate {K : Type u} {C : Type v} {U : Type w} [Field K] [AddCommGroup U] [Module K U] [Mul U] (constant : C → U) (problem : Problem U) : Certificate constant problem

Canonical interaction certificate obtained from quotienting by all free semantic data.

Equations

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

noncomputable def Algebraic.Fusion.Arithmetic.Interaction.Linear.Quotient.outputRank {K : Type u} {C : Type v} {U : Type w} {m : ℕ} [Field K] [AddCommGroup U] [Module K U] (constant : C → U) (problem : Problem U) (targets : Fin m → U) : ℕ

Dimension of the span of requested outputs modulo free inputs and named constants.

Equations

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

theorem Algebraic.Fusion.Arithmetic.Interaction.Linear.Quotient.outputRank_le_multiplicationCost {K : Type u} {C : Type v} {U : Type w} {m : ℕ} [Field K] [AddCommGroup U] [Module K U] [Mul U] (constant : C → U) (problem : Problem U) (targets : Fin m → U) (circuit : Circuit (Arithmetic.signature C) problem.inputCount m) (constructs : Multiple.Constructs problem targets circuit) : outputRank constant problem targets ≤ circuit.cost Arithmetic.multiplicationCost

Canonical quotient-output rank lower-bounds multiplication cost.

theorem Algebraic.Fusion.Arithmetic.Interaction.Linear.Quotient.circuit_multiplication_lowerBound_of_quotientIndependent {K : Type u} {C : Type v} {U : Type w} {m : ℕ} [Field K] [AddCommGroup U] [Module K U] [Mul U] (constant : C → U) (problem : Problem U) (targets : Fin m → U) (independent : LinearIndependent K (⇑(freeSubmodule K constant problem).mkQ ∘ targets)) (circuit : Circuit (Arithmetic.signature C) problem.inputCount m) (constructs : Multiple.Constructs problem targets circuit) : m ≤ circuit.cost Arithmetic.multiplicationCost

Linear independence modulo free data forces one multiplication per requested output.

theorem Algebraic.Fusion.Arithmetic.Interaction.Linear.Quotient.outputRank_le_gateCost {K : Type u} {C : Type v} {U : Type w} {m : ℕ} [Field K] [AddCommGroup U] [Module K U] [Mul U] (constant : C → U) (problem : Problem U) (targets : Fin m → U) (circuit : Circuit (Arithmetic.signature C) problem.inputCount m) (constructs : Multiple.Constructs problem targets circuit) : outputRank constant problem targets ≤ circuit.cost Arithmetic.gateCost

Canonical quotient-output rank lower-bounds total nonconstant gate cost.

theorem Algebraic.Fusion.Arithmetic.Interaction.Linear.Quotient.outputRank_le_size {K : Type u} {C : Type v} {U : Type w} {m : ℕ} [Field K] [AddCommGroup U] [Module K U] [Mul U] (constant : C → U) (problem : Problem U) (targets : Fin m → U) (circuit : Circuit (Arithmetic.signature C) problem.inputCount m) (constructs : Multiple.Constructs problem targets circuit) : outputRank constant problem targets ≤ circuit.size

Canonical quotient-output rank lower-bounds raw circuit size.