Documentation

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

Rectangular catalecticant rank profiles #

A single arithmetic circuit can have very different local interaction ranks at different catalecticant splits. This module records those bounds as a profile rₖ and packages the strongest lower bound certified by any split:

maxₖ ceil(choose d k / rₖ) ≤ multiplication cost.

Keeping the profile separate from any particular source of local rank bounds lets decomposition, restriction, and future shifted-flattening arguments share the same comparison layer.

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

A split-indexed family of local interaction-rank bounds for one circuit.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    def Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.Profile.certifiedLowerBound (degree : ℕ) (localRank : Fin (degree + 1) → ℕ) :
    ℕ

    The strongest cost lower bound supplied by a rectangular rank profile.

    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.split_le_certifiedLowerBound (degree : ℕ) (localRank : Fin (degree + 1) → ℕ) (split : Fin (degree + 1)) :
      degree.choose ↑split ⌈/⌉ localRank split ≤ certifiedLowerBound degree localRank

      Every individual split contributes a lower bound no larger than the best profile bound.

      source
      theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.Profile.certifiedLowerBound_const_eq_middle (degree interactionRank : ℕ) (rankPositive : 0 < interactionRank) :
      (certifiedLowerBound degree fun (x : Fin (degree + 1)) => interactionRank) = degree.choose (degree / 2) ⌈/⌉ interactionRank

      For a positive constant local-rank bound, optimizing over all rectangular splits is exactly the middle-layer bound.

      source
      @[simp]
      theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.Profile.certifiedLowerBound_one (degree : ℕ) :
      (certifiedLowerBound degree fun (x : Fin (degree + 1)) => 1) = degree.choose (degree / 2)

      Rank-one profiles recover the raw middle binomial coefficient.

      source
      theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.Profile.split_lowerBound {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))) (profile : LocalRankAtMost constant degree degreeAtLeastTwo circuit localRank) (split : Fin (degree + 1)) :
      degree.choose ↑split ⌈/⌉ localRank split ≤ circuit.cost Arithmetic.multiplicationCost

      A profile hypothesis recovers the rectangular Fusion lower bound at each chosen split.

      source
      theorem Algebraic.Fusion.Arithmetic.Interaction.Polynomial.Catalecticant.Rectangular.Profile.certifiedLowerBound_le_multiplicationCost {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))) (profile : LocalRankAtMost constant degree degreeAtLeastTwo circuit localRank) :
      certifiedLowerBound degree localRank ≤ circuit.cost Arithmetic.multiplicationCost

      The maximum over all rectangular splits is a certified multiplication-cost lower bound.