OAI/Computability/SpaceSimulation/Evaluation/Field.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

Any characteristic works with the unambiguous selectors below; use a prime field with a uniform binary computation of its modulus. Supplies a bit-space certificate for field arithmetic and folds that retain only residues.

  1. structure OAI.Fifths.Modulus line 13
  2. instance OAI.Fifths.Modulus.(instance at line 19) line 19
  3. abbrev OAI.Fifths.Modulus.K line 21
  4. theorem OAI.Fifths.Modulus.bound line 22
  5. theorem OAI.Fifths.Modulus.pos line 23
  6. def OAI.Fifths.Modulus.weight line 25
  7. def OAI.Fifths.Modulus.divisorsOK line 29

    Source comment

    Need a uniform computation yielding a modulus with Δ < p-1.
    def divisorsOK (p : ℕ) (m : ℕ) : Bool :=
…
  8. def OAI.Fifths.Modulus.isPrime line 32
  9. theorem OAI.Fifths.Modulus.isPrime_iff line 34
  10. def OAI.Fifths.Modulus.rangeSize line 45
  11. def OAI.Fifths.Modulus.accepted line 46
  12. theorem OAI.Fifths.Modulus.found line 48
  13. def OAI.Fifths.Modulus.chosen line 54
  14. theorem OAI.Fifths.Modulus.chosen_large line 57
  15. theorem OAI.Fifths.Modulus.chosen_small line 61
  16. theorem OAI.Fifths.Comp.primality line 68
  17. theorem OAI.Fifths.Comp.chosenN line 76
  18. theorem OAI.Fifths.Comp.fitElement line 89
  19. theorem OAI.Fifths.Comp.valCast line 93
  20. theorem OAI.Fifths.Comp.valZero line 97
  21. theorem OAI.Fifths.Comp.valOne line 100
  22. theorem OAI.Fifths.Comp.fieldAdd line 104
  23. theorem OAI.Fifths.Comp.fieldNeg line 109
  24. theorem OAI.Fifths.Comp.fieldSub line 121
  25. theorem OAI.Fifths.Comp.fieldMul line 126
  26. theorem OAI.Fifths.Comp.fieldPow line 131
  27. theorem OAI.Fifths.Comp.fieldSum line 146
  28. theorem OAI.Fifths.Comp.fieldProd line 161