OAI/Computability/SpaceSimulation/Register/Scale.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Uniform bounds pulled along index sets. Add 1 to the reference function so that constant-size data and empty histories never require a separate positivity premise. Used also with restrictions of runs to sets of promise instances.

  1. def OAI.Fifths.Scaled line 14

    Source documentation

    Scaled S f = f is at most a constant multiple of S+1 at every argument.

    def Scaled {I : Type} (S f : I → ℕ) : Prop :=
…
  2. def OAI.Fifths.Fits line 19

    Source documentation

    Bit length bound (all instances, same constant); not by itself a computability assertion.

    def Fits {I : Type} (S f : I → ℕ) : Prop :=
…
  3. theorem OAI.Fifths.Scaled.pull line 25
  4. theorem OAI.Fifths.Scaled.of_le line 30
  5. theorem OAI.Fifths.Scaled.congr line 34
  6. theorem OAI.Fifths.Scaled.const line 37
  7. theorem OAI.Fifths.Scaled.refl line 40
  8. theorem OAI.Fifths.Scaled.add line 43
  9. theorem OAI.Fifths.Scaled.mulConst line 49
  10. theorem OAI.Fifths.Scaled.mulFamily line 55
  11. theorem OAI.Fifths.Scaled.trans line 65
  12. theorem OAI.Fifths.Fits.pull line 74
  13. theorem OAI.Fifths.Fits.mono line 78
  14. theorem OAI.Fifths.Fits.congr line 81
  15. theorem OAI.Fifths.Fits.const line 83
  16. theorem OAI.Fifths.Fits.of_scaled line 86
  17. theorem OAI.Fifths.Fits.up line 89
  18. theorem OAI.Fifths.Fits.add line 92
  19. theorem OAI.Fifths.Fits.mul line 97
  20. theorem OAI.Fifths.Fits.pow line 100
  21. theorem OAI.Fifths.Fits.pair line 104
  22. theorem OAI.Fifths.Fits.pair_left line 109
  23. theorem OAI.Fifths.Fits.pair_right line 115