Documentation

Complexitylib.Algebraic.LowerBound.Fusion.SumOfTerms.Waring.Rectangular.Restriction.Binary

Critical layers of rectangular binary Waring gadgets #

Interpret the generic bounded-power atom theorem in the degree-d homogeneous layer. For d ≥ 2, coefficient-times-variable products and proper powers are invisible, while a full power is one rectangular Waring term.

source
def Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Restriction.Binary.CriticalLayerOrPower {K : Type} [Field K] (degree : ℕ) (polynomial : MvPolynomial (Fin degree) K) :
Prop

A polynomial's degree-d component is zero or one rectangular Waring term.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Restriction.Binary.criticalLayerOrPower_of_isHomogeneous_ne {K : Type} [Field K] (degree visibleDegree : ℕ) (polynomial : MvPolynomial (Fin degree) K) (homogeneous : polynomial.IsHomogeneous visibleDegree) (notCritical : visibleDegree ≠ degree) :
    CriticalLayerOrPower degree polynomial
    source
    theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Restriction.Binary.criticalLayerOrPower_termValue {K : Type} {degree : ℕ} [Field K] (term : Term K degree) :
    CriticalLayerOrPower degree (termValue term)
    source
    theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Restriction.Binary.criticalLayerOrPower_linearForm_pow {K : Type} [Field K] (degree : ℕ) (term : Term K degree) (exponent : ℕ) (_bounded : exponent ≤ degree) :
    CriticalLayerOrPower degree (linearForm term ^ exponent)
    source
    def Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Restriction.Binary.MultiplicationAtomProperty {K : Type} [Field K] (degree : ℕ) (atom : Atom (Arithmetic.signature K) (MvPolynomial (Fin degree) K)) :
    Prop

    Atom-local form of the rectangular critical-layer property.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Restriction.Binary.multiplicationProperty_expressionSum {K : Type} [Field K] (degree : ℕ) (expressions : List (Arithmetic.Expression K degree)) (each : ∀ expression ∈ expressions, Arithmetic.Expression.MultiplicationProperty (⇑MvPolynomial.C) MvPolynomial.X (CriticalLayerOrPower degree) expression) :
      Arithmetic.Expression.MultiplicationProperty (⇑MvPolynomial.C) MvPolynomial.X (CriticalLayerOrPower degree) (Translation.expressionSum expressions)

      Multiplication-property closure under the expression sum used for a linear form.

      source
      theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Restriction.Binary.multiplicationProperty_coefficientVariable {K : Type} [Field K] (degree : ℕ) (degreeAtLeastTwo : 2 ≤ degree) (coefficient : K) (index : Fin degree) :
      Arithmetic.Expression.MultiplicationProperty (⇑MvPolynomial.C) MvPolynomial.X (CriticalLayerOrPower degree) ((Arithmetic.Expression.constant coefficient).mul (Arithmetic.Expression.input index))
      source
      theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Restriction.Binary.multiplicationProperty_linearFormExpression {K : Type} [Field K] (degree : ℕ) (degreeAtLeastTwo : 2 ≤ degree) (term : Term K degree) :
      Arithmetic.Expression.MultiplicationProperty (⇑MvPolynomial.C) MvPolynomial.X (CriticalLayerOrPower degree) (Translation.Binary.linearFormExpression term)
      source
      theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Restriction.Binary.multiplicationProperty_scaleExpression {K : Type} [Field K] (degree : ℕ) (term : Term K degree) :
      Arithmetic.Expression.MultiplicationProperty (⇑MvPolynomial.C) (fun (x : Fin 1) => linearForm term ^ degree) (CriticalLayerOrPower degree) (Translation.Binary.scaleExpression term.scale)
      source
      theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Restriction.Binary.powerCircuit_multiplicationAtomProperty {K : Type} [Field K] (degree : ℕ) (term : Term K degree) (exponent : ℕ) (bounded : exponent ≤ degree) (atom : Atom (Arithmetic.signature K) (MvPolynomial (Fin degree) K)) (present : atom ∈ circuitAtoms (Arithmetic.Power.binaryCircuit exponent) (Arithmetic.interpretation ⇑MvPolynomial.C) fun (x : Fin 1) => linearForm term) :
      MultiplicationAtomProperty degree atom

      Generic arithmetic binary-power atoms become rectangular critical-layer atoms when the base is the Waring linear form.

      source
      theorem Algebraic.Fusion.SumOfTerms.Waring.Rectangular.Restriction.Binary.termCircuit_multiplicationAtomProperty {K : Type} [Field K] (degree : ℕ) (degreeAtLeastTwo : 2 ≤ degree) (term : Term K degree) (atom : Atom (Arithmetic.signature K) (MvPolynomial (Fin degree) K)) (present : atom ∈ circuitAtoms (Translation.Binary.termCircuit term) (Arithmetic.interpretation ⇑MvPolynomial.C) MvPolynomial.X) :
      MultiplicationAtomProperty degree atom

      Every multiplication in a complete rectangular binary term gadget obeys the critical-layer property.