Critical-layer restriction for binary-compiled Waring circuits

Binary powering visits a sparse sequence of exponents rather than every intermediate exponent. The generic arithmetic power-atom theorem identifies each emitted multiplication as a bounded power; this module interprets that fact in the Waring critical layer.

theorem Algebraic.Fusion.SumOfTerms.Waring.Restriction.Binary.criticalLayerOrPower_linearForm_pow {K : Type} [Field K] (n : ℕ) (term : Term K n) (exponent : ℕ) (_bounded : exponent ≤ 2 * n) : CriticalLayerOrPower n (linearForm term ^ exponent)

Any bounded power of a Waring linear form is either outside the critical degree or is itself one charged Waring term.

theorem Algebraic.Fusion.SumOfTerms.Waring.Restriction.Binary.powerCircuit_multiplicationAtomProperty {K : Type} [Field K] (n : ℕ) (term : Term K n) (exponent : ℕ) (bounded : exponent ≤ 2 * n) (atom : Atom (Arithmetic.signature K) (MvPolynomial (Fin (2 * n)) K)) (present : atom ∈ circuitAtoms (Arithmetic.Power.binaryCircuit exponent) (Arithmetic.interpretation ⇑MvPolynomial.C) fun (x : Fin 1) => linearForm term) : MultiplicationAtomProperty n atom

Every multiplication atom in a binary power circuit is a bounded power of the input linear form, hence satisfies the critical-layer restriction.