Documentation

Complexitylib.Algebraic.LowerBound.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.Profile.Multiplication

Split-indexed restrictions on multiplication outputs #

This is the atom-level entry point for proving a rectangular rank profile. Different splits may use unrelated arguments to bound the same multiplication output, while the profile theorem chooses the strongest resulting ratio.

source
def Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.Profile.MultiplicationOutputRankAtMost {K C : Type} [Field K] (constant : C → K) (degree : ℕ) (degreeAtLeastTwo : 2 ≤ degree) (circuit : Circuit (Arithmetic.signature C) degree 1) (localRank : Fin (degree + 1) → ℕ) :
Prop

At every split, every evaluated multiplication output obeys the indicated rectangular catalecticant rank bound.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.Profile.localRankAtMost_of_multiplicationOutputRankAtMost {K C : Type} [Field K] (constant : C → K) (degree : ℕ) (degreeAtLeastTwo : 2 ≤ degree) (circuit : Circuit (Arithmetic.signature C) degree 1) (localRank : Fin (degree + 1) → ℕ) (bound : MultiplicationOutputRankAtMost constant degree degreeAtLeastTwo circuit localRank) :
    LocalRankAtMost constant degree degreeAtLeastTwo circuit localRank

    Atom-level bounds at every split induce the corresponding circuit-local rank profile.

    source
    theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.Profile.certifiedLowerBound_of_multiplicationOutputRankAtMost {K C : Type} [Field K] [CharZero K] (constant : C → K) (degree : ℕ) (degreeAtLeastTwo : 2 ≤ degree) (localRank : Fin (degree + 1) → ℕ) (rankPositive : ∀ (split : Fin (degree + 1)), 0 < localRank split) (circuit : Circuit (Arithmetic.signature C) degree 1) (constructs : (problem K degree).Constructs circuit (Arithmetic.interpretation fun (scalar : C) => MvPolynomial.C (constant scalar))) (bound : MultiplicationOutputRankAtMost constant degree degreeAtLeastTwo circuit localRank) :
    certifiedLowerBound degree localRank ≤ circuit.cost Arithmetic.multiplicationCost

    The optimized rectangular lower bound, stated directly from atom-level rank restrictions.