OAI/NumberTheory/Ostmann/Arithmetic/ArithmeticSpectatorHistory.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

From reconstructed integer histories to the spectator tree

The realization conditions record the two child products and the terminal modulus. They allow composite inserted pivots: division by the compensation unit gives the giant used by the rational tree. No prime law is assigned to that composite integer.

  1. def OAI.Ostmann.spectatorHistoryLeaf line 18
  2. def OAI.Ostmann.spectatorHistoryCutoff line 22
  3. def OAI.Ostmann.spectatorHistoryWeight line 26
  4. def OAI.Ostmann.SpectatorHistoryRealizes line 32
  5. theorem OAI.Ostmann.spectatorHistoryWeight_eq_tree line 53