Multiplication-occurrence rank budgets #
Present the nonuniform interaction-rank theorem directly in terms of the evaluated multiplication gates of an arithmetic circuit. This avoids asking clients to index a second, certificate-dependent filtered list while retaining one budget entry for every gate occurrence, including repeated semantic products.
theorem
Algebraic.Fusion.Arithmetic.Interaction.Rank.Occurrence.exists_budget_ge_ceilDiv
{count : ℕ}
(targetRank : ℕ)
(targetPositive : 0 < targetRank)
(budget : Fin count → ℕ)
(target_le_sum : targetRank ≤ ∑ index : Fin count, budget index)
:
A positive quantity bounded by a finite sum forces one summand to reach its ceiling average. Positivity also rules out an empty index type.
def
Algebraic.Fusion.Arithmetic.Interaction.Rank.Occurrence.interactionFamily
{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)
:
The interaction map created by a particular evaluated multiplication-gate occurrence.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Algebraic.Fusion.Arithmetic.Interaction.Rank.Occurrence.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 (circuitMultiplicationArguments constant problem.inputs circuit).length → ℕ)
:
Nonuniform rank budget indexed directly by evaluated multiplication-gate occurrences.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Algebraic.Fusion.Arithmetic.Interaction.Rank.Occurrence.ArgumentBound
{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 2 → U) → ℕ)
:
A semantic budget function can be checked on membership in the multiplication-occurrence list. The final sum still counts duplicate occurrences separately.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Algebraic.Fusion.Arithmetic.Interaction.Rank.Occurrence.targetFeature_mem_span
{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))
:
certificate.feature problem.target ∈ Submodule.span K (Set.range (interactionFamily certificate circuit))
The target feature is spanned by the occurrence-indexed interaction family.
theorem
Algebraic.Fusion.Arithmetic.Interaction.Rank.Occurrence.IndexedBound.of_argumentBound
{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 2 → U) → ℕ)
(bound : ArgumentBound certificate circuit budget)
:
IndexedBound certificate circuit
fun (index : Fin (circuitMultiplicationArguments constant problem.inputs circuit).length) =>
budget ((circuitMultiplicationArguments constant problem.inputs circuit).get index)
An argument-indexed semantic budget induces an occurrence-indexed budget by evaluating it at each gate's actual arguments.
theorem
Algebraic.Fusion.Arithmetic.Interaction.Rank.Occurrence.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 (circuitMultiplicationArguments constant problem.inputs circuit).length → ℕ)
(localBound : IndexedBound certificate circuit budget)
:
Target rank is at most the sum of occurrence-indexed local rank budgets.
theorem
Algebraic.Fusion.Arithmetic.Interaction.Rank.Occurrence.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 (circuitMultiplicationArguments constant problem.inputs circuit).length → ℕ)
(localBound : IndexedBound certificate circuit budget)
:
targetRank ≤ ∑ index : Fin (circuitMultiplicationArguments constant problem.inputs circuit).length, budget index
Natural-number form of the occurrence-indexed rank inequality.
theorem
Algebraic.Fusion.Arithmetic.Interaction.Rank.Occurrence.exists_occurrence_budget_ge_ceilDiv
{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 : ℕ)
(targetPositive : 0 < 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 (circuitMultiplicationArguments constant problem.inputs circuit).length → ℕ)
(localBound : IndexedBound certificate circuit budget)
:
∃ (index : Fin (circuitMultiplicationArguments constant problem.inputs circuit).length),
targetRank ⌈/⌉ (circuitMultiplicationArguments constant problem.inputs circuit).length ≤ budget index
Some actual multiplication occurrence carries at least the ceiling average of any positive certified target-rank lower bound.
theorem
Algebraic.Fusion.Arithmetic.Interaction.Rank.Occurrence.targetRank_le_sum_argumentBudget
{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 2 → U) → ℕ)
(localBound : ArgumentBound certificate circuit budget)
:
A semantic argument budget bounds target rank by its list sum over actual multiplication occurrences.