Circuit-local interaction-rank bounds #
The base rank certificate asks for a uniform rank bound on every possible semantic multiplication interaction. Restricted arithmetic models usually only control the products that actually occur at circuit gates.
This module provides that local interface. If every multiplication
interaction extracted from one evaluated circuit has rank at most r, while
the target feature has rank at least R, then ceil(R / r) multiplication
gates are necessary.
def
Algebraic.Fusion.Arithmetic.Interaction.Rank.Local.CircuitBound
{K : Type u}
{C : Type v}
{U : Type w}
{A : Type x}
{B : Type y}
[Field K]
[Add U]
[Mul U]
[AddCommGroup A]
[Module K A]
[AddCommGroup B]
[Module K B]
{constant : C → U}
{problem : Problem U}
(certificate : Interaction.Certificate constant problem)
(circuit : Circuit (Arithmetic.signature C) problem.inputCount 1)
(interactionRank : ℕ)
:
A local rank restriction on exactly the multiplication interactions that occur when evaluating a circuit on the problem's designated inputs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Algebraic.Fusion.Arithmetic.Interaction.Rank.Local.IndexedBound
{K : Type u}
{C : Type v}
{U : Type w}
{A : Type x}
{B : Type y}
[Field K]
[Add U]
[Mul U]
[AddCommGroup A]
[Module K A]
[AddCommGroup B]
[Module K B]
{constant : C → U}
{problem : Problem U}
(certificate : Interaction.Certificate constant problem)
(circuit : Circuit (Arithmetic.signature C) problem.inputCount 1)
(budget :
Fin (interactions certificate (circuitAtoms circuit (Arithmetic.interpretation constant) problem.inputs)).length → ℕ)
:
Nonuniform local-rank budget indexed by the actual retained interaction occurrences of an evaluated circuit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Algebraic.Fusion.Arithmetic.Interaction.Rank.Local.MultiplicationBound
{K : Type u}
{C : Type v}
{U : Type w}
{A : Type x}
{B : Type y}
[Field K]
[Add U]
[Mul U]
[AddCommGroup A]
[Module K A]
[AddCommGroup B]
[Module K B]
{constant : C → U}
{problem : Problem U}
(certificate : Interaction.Certificate constant problem)
(circuit : Circuit (Arithmetic.signature C) problem.inputCount 1)
(interactionRank : ℕ)
:
Equivalent-to-use atom-level formulation: bound the interaction created by every multiplication atom in the evaluated circuit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Algebraic.Fusion.Arithmetic.Interaction.Rank.Local.CircuitBound.of_multiplicationBound
{K : Type u}
{C : Type v}
{U : Type w}
{A : Type x}
{B : Type y}
[Field K]
[Add U]
[Mul U]
[AddCommGroup A]
[Module K A]
[AddCommGroup B]
[Module K B]
{constant : C → U}
{problem : Problem U}
(certificate : Interaction.Certificate constant problem)
(circuit : Circuit (Arithmetic.signature C) problem.inputCount 1)
(interactionRank : ℕ)
(bound : MultiplicationBound certificate circuit interactionRank)
:
CircuitBound certificate circuit interactionRank
An atom-level multiplication bound implies the filtered-list circuit bound used by the rank theorem.
theorem
Algebraic.Fusion.Arithmetic.Interaction.Rank.Local.target_rank_le_sum_indexedBudget
{K : Type u}
{C : Type v}
{U : Type w}
{A : Type x}
{B : Type y}
[Field K]
[Add U]
[Mul U]
[AddCommGroup A]
[Module K A]
[AddCommGroup B]
[Module K B]
{constant : C → U}
{problem : Problem U}
(certificate : Interaction.Certificate constant problem)
(circuit : Circuit (Arithmetic.signature C) problem.inputCount 1)
(constructs : problem.Constructs circuit (Arithmetic.interpretation constant))
(budget :
Fin (interactions certificate (circuitAtoms circuit (Arithmetic.interpretation constant) problem.inputs)).length → ℕ)
(localBound : IndexedBound certificate circuit budget)
:
(certificate.feature problem.target).rank ≤ ∑ index :
Fin (interactions certificate (circuitAtoms circuit (Arithmetic.interpretation constant) problem.inputs)).length,
↑(budget index)
The target feature rank is bounded by the sum of nonuniform local interaction-rank budgets.
theorem
Algebraic.Fusion.Arithmetic.Interaction.Rank.Local.targetRank_le_sum_indexedBudget
{K : Type u}
{C : Type v}
{U : Type w}
{A : Type x}
{B : Type y}
[Field K]
[Add U]
[Mul U]
[AddCommGroup A]
[Module K A]
[AddCommGroup B]
[Module K B]
{constant : C → U}
{problem : Problem U}
(certificate : Interaction.Certificate constant problem)
(targetRank : ℕ)
(target_rank_ge : ↑targetRank ≤ (certificate.feature problem.target).rank)
(circuit : Circuit (Arithmetic.signature C) problem.inputCount 1)
(constructs : problem.Constructs circuit (Arithmetic.interpretation constant))
(budget :
Fin (interactions certificate (circuitAtoms circuit (Arithmetic.interpretation constant) problem.inputs)).length → ℕ)
(localBound : IndexedBound certificate circuit budget)
:
targetRank ≤ ∑ index :
Fin (interactions certificate (circuitAtoms circuit (Arithmetic.interpretation constant) problem.inputs)).length,
budget index
Natural-number form of the nonuniform indexed-budget inequality.
theorem
Algebraic.Fusion.Arithmetic.Interaction.Rank.Local.target_rank_le_mul_multiplicationCost
{K : Type u}
{C : Type v}
{U : Type w}
{A : Type x}
{B : Type y}
[Field K]
[Add U]
[Mul U]
[AddCommGroup A]
[Module K A]
[AddCommGroup B]
[Module K B]
{constant : C → U}
{problem : Problem U}
(certificate : Interaction.Certificate constant problem)
(interactionRank : ℕ)
(circuit : Circuit (Arithmetic.signature C) problem.inputCount 1)
(constructs : problem.Constructs circuit (Arithmetic.interpretation constant))
(localBound : CircuitBound certificate circuit interactionRank)
:
Under a circuit-local rank bound, the target feature rank is at most the number of multiplication gates times the local bound.
theorem
Algebraic.Fusion.Arithmetic.Interaction.Rank.Local.targetRank_le_mul_multiplicationCost
{K : Type u}
{C : Type v}
{U : Type w}
{A : Type x}
{B : Type y}
[Field K]
[Add U]
[Mul U]
[AddCommGroup A]
[Module K A]
[AddCommGroup B]
[Module K B]
{constant : C → U}
{problem : Problem U}
(certificate : Interaction.Certificate constant problem)
(targetRank interactionRank : ℕ)
(target_rank_ge : ↑targetRank ≤ (certificate.feature problem.target).rank)
(circuit : Circuit (Arithmetic.signature C) problem.inputCount 1)
(constructs : problem.Constructs circuit (Arithmetic.interpretation constant))
(localBound : CircuitBound certificate circuit interactionRank)
:
Natural-number target rank is bounded by local rank times multiplication cost.
theorem
Algebraic.Fusion.Arithmetic.Interaction.Rank.Local.circuit_lowerBound
{K : Type u}
{C : Type v}
{U : Type w}
{A : Type x}
{B : Type y}
[Field K]
[Add U]
[Mul U]
[AddCommGroup A]
[Module K A]
[AddCommGroup B]
[Module K B]
{constant : C → U}
{problem : Problem U}
(certificate : Interaction.Certificate constant problem)
(targetRank interactionRank : ℕ)
(target_rank_ge : ↑targetRank ≤ (certificate.feature problem.target).rank)
(positive : 0 < interactionRank)
(circuit : Circuit (Arithmetic.signature C) problem.inputCount 1)
(constructs : problem.Constructs circuit (Arithmetic.interpretation constant))
(localBound : CircuitBound certificate circuit interactionRank)
:
Circuit-local interaction rank yields a multiplication lower bound.