Documentation

Complexity.Algorithms.WordRAM.PrimeTrial

Charged native trial division #

This is a finite instruction program, not an invocation of Lean's primality decision procedure. The Chan–He prime table will call it only on candidates at least two.

Main definitions #

Main results #

source
@[reducible, inline]
abbrev Cslib.Algorithms.WordRAM.PrimeTrial.arg :
Fin 6

Candidate, preserved.

Instances For
    source
    @[reducible, inline]
    abbrev Cslib.Algorithms.WordRAM.PrimeTrial.divisor :
    Fin 6

    Current trial divisor.

    Instances For
      source
      @[reducible, inline]
      abbrev Cslib.Algorithms.WordRAM.PrimeTrial.flag :
      Fin 6

      Primality flag.

      Instances For
        source
        @[reducible, inline]
        abbrev Cslib.Algorithms.WordRAM.PrimeTrial.remainder :
        Fin 6

        Remainder scratch.

        Instances For
          source
          @[reducible, inline]
          abbrev Cslib.Algorithms.WordRAM.PrimeTrial.one :
          Fin 6

          Constant one.

          Instances For
            source
            @[reducible, inline]
            abbrev Cslib.Algorithms.WordRAM.PrimeTrial.zero :
            Fin 6

            Constant zero.

            Instances For
              source
              def Cslib.Algorithms.WordRAM.PrimeTrial.body :
              WordRAM.Code WordRAM.Basis.standard 6

              Test one trial divisor and advance. The conditional also charges its control instructions.

              Instances For
                source
                def Cslib.Algorithms.WordRAM.PrimeTrial.program :
                WordRAM.Code WordRAM.Basis.standard 6

                Initialize and test every divisor strictly between one and the candidate.

                Instances For
                  source
                  theorem Cslib.Algorithms.WordRAM.PrimeTrial.exec {w : ℕ} (x : WordRAM.Data 6) (hp : 2 ≤ x.regs arg) (hfit : WordRAM.Fits w (x.regs arg + 2)) :
                  ∃ (y : WordRAM.Data 6), WordRAM.ExecWithin w program x y (7 * (x.regs arg - 2) + 6) ∧ (y.regs flag = if Nat.Prime (x.regs arg) then 1 else 0) ∧ y.regs arg = x.regs arg ∧ y.mem = x.mem

                  Test a candidate at least two in at most 7(p-2)+6 native instructions. All divisors are actual register values; the native remainder instruction is charged.