Documentation

MIPRE.Foundations.LowDegree.BinaryDegreeFactors

Prime-power degree decomposition #

This list is used only in the proof of the all-degrees constructor. The executable constructor computes the same prime-power factors by bounded unary arithmetic. Indices outside the prime support contribute the neutral factor one.

source
def MIPRE.LowDegree.BinaryDegreeFactors.degreeFactors (n : ℕ) :
List ℕ

Prime-power degree factors in ascending base order, including neutral factors.

Equations
Instances For
    source
    theorem MIPRE.LowDegree.BinaryDegreeFactors.degreeFactors_prod (n : ℕ) (hn : 0 < n) :
    (degreeFactors n).prod = n

    The complete bounded list reconstructs every positive input degree.

    source
    theorem MIPRE.LowDegree.BinaryDegreeFactors.degreeFactors_pairwise (n : ℕ) :
    List.Pairwise Nat.Coprime (degreeFactors n)

    Distinct prime indices contribute coprime powers; all other indices contribute one.

    source
    theorem MIPRE.LowDegree.BinaryDegreeFactors.degreeFactors_dvd (n : ℕ) (hn : 0 < n) {d : ℕ} (hd : d ∈ degreeFactors n) :
    d ∣ n

    Every listed factor divides the requested degree.

    source
    theorem MIPRE.LowDegree.BinaryDegreeFactors.degreeFactors_pos (n : ℕ) (hn : 0 < n) {d : ℕ} (hd : d ∈ degreeFactors n) :
    0 < d

    Every listed factor is positive, including neutral factors.

    source
    theorem MIPRE.LowDegree.BinaryDegreeFactors.degreeFactors_le (n : ℕ) (hn : 0 < n) {d : ℕ} (hd : d ∈ degreeFactors n) :
    d ≤ n

    The degree cap applies to every listed prime power.

    source
    theorem MIPRE.LowDegree.BinaryDegreeFactors.prefix_prod_dvd (n : ℕ) (hn : 0 < n) (pre post : List ℕ) (h : degreeFactors n = pre ++ post) :
    pre.prod ∣ n

    Each prefix product remains a divisor of the requested degree.