Kummer's Criterion and Regular Primes in Lean

10. The abandoned reflection route🔗

This chapter records a second possible route to the plus-to-minus divisibility step. It is not the route used in the proof of Kummer's criterion. Its purpose here is to isolate the remaining mathematical input and to explain how the reflection argument would proceed if that input were supplied.

  1. 10.1. The aim
  2. 10.2. The unproved reciprocity input
  3. 10.3. Component reflection
  4. 10.4. From reflection to class numbers
  5. 10.5. How the reciprocity input is to be proved