Documentation

MIPRE.Foundations.LowDegree.BinaryNonresidueLoop

Bounded auxiliary root lifting #

This is the specified program for the odd-prime auxiliary stage. It repeatedly factors f(X^q), retaining the current f once factorization returns at most one factor. Nonterminal choices are clipped to the initial seed width, ensuring a global runtime bound even on malformed inputs. The statements here establish execution and size bounds; the nonresidue and termination correctness theorems are separate algebraic obligations.

source
@[reducible, inline]
abbrev MIPRE.LowDegree.BinaryPolynomial.NonresidueState :
Type

Exponent minus one in unary, coefficient cap, done flag, and current polynomial.

Equations
Instances For
    source
    noncomputable def MIPRE.LowDegree.BinaryPolynomial.liftCandidates (s : NonresidueState) :
    List Cost.BitStr

    Factor the positive-power substitution in the current candidate.

    Equations
    Instances For
      source
      noncomputable def MIPRE.LowDegree.BinaryPolynomial.nonresidueStep (s : NonresidueState) :
      Bool → NonresidueState

      One bounded root-lifting step, retaining the old polynomial at the stopping test.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem MIPRE.LowDegree.BinaryPolynomial.nonresidueStep_done (s : NonresidueState) (b : Bool) (hs : s.2.2.1 = true) :
        nonresidueStep s b = s

        Stopping is absorbing, so padding the iteration budget is harmless.

        source
        theorem MIPRE.LowDegree.BinaryPolynomial.nonresidueStep_width (s : NonresidueState) (b : Bool) :
        (nonresidueStep s b).1 = s.1 ∧ (nonresidueStep s b).2.1 = s.2.1 ∧ List.length (nonresidueStep s b).2.2.2 ≤ max (List.length s.2.2.2) (List.length s.2.1)

        Each step retains both external parameters and respects the original width cap.

        source
        theorem MIPRE.LowDegree.BinaryPolynomial.fold_nonresidueStep_width (l : Cost.BitStr) (s : NonresidueState) :
        (List.foldl nonresidueStep s l).1 = s.1 ∧ (List.foldl nonresidueStep s l).2.1 = s.2.1 ∧ List.length (List.foldl nonresidueStep s l).2.2.2 ≤ max (List.length s.2.2.2) (List.length s.2.1)

        The complete loop retains metadata and never exceeds the initial maximum width.

        source
        noncomputable def MIPRE.LowDegree.BinaryPolynomial.isEmptyListProg :
        Cost.PolyTimeFun (List Cost.BitStr) Bool
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def MIPRE.LowDegree.BinaryPolynomial.liftCandidatesProg :
          Cost.PolyTimeFun NonresidueState (List Cost.BitStr)
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            noncomputable def MIPRE.LowDegree.BinaryPolynomial.nonresidueStepProg :
            Cost.PolyTimeFun (NonresidueState × Bool) NonresidueState
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              theorem MIPRE.LowDegree.BinaryPolynomial.nonresidueStep_bounded :
              nonresidueStepProg.FoldBounded (10 * Polynomial.X + 10)
              source
              noncomputable def MIPRE.LowDegree.BinaryPolynomial.nonresidueLoopProg :
              Cost.PolyTimeFun (Cost.BitStr × NonresidueState) NonresidueState

              Run the bounded lifting loop with explicitly supplied fuel and metadata.

              Equations
              Instances For
                source
                @[simp]
                theorem MIPRE.LowDegree.BinaryPolynomial.nonresidueLoopProg_apply (l : Cost.BitStr) (s : NonresidueState) :
                nonresidueLoopProg.toFun (l, s) = List.foldl nonresidueStep s l
                source
                noncomputable def MIPRE.LowDegree.BinaryPolynomial.nonresidueLiftStateProg :
                Cost.PolyTimeFun Cost.Unary NonresidueState

                The auxiliary root-lifting program initialized from the deterministic cyclotomic seed. The initial seed degree supplies the iteration budget, and its full width supplies the cap.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  noncomputable def MIPRE.LowDegree.BinaryPolynomial.nonresidueLiftBitsProg :
                  Cost.PolyTimeFun Cost.Unary Cost.BitStr

                  The retained binary polynomial from the bounded auxiliary construction.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For