OAI/MathematicalPhysics/ContinuumCoulomb/Programs/SquareRootProgram.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Bitwise integer square-root search and its actual polynomial-time Boolean-stack implementation. This supplies arithmetic for finite-precision geometric constants and mediator amplitudes without a real square-root oracle.

  1. abbrev OAI.ContinuumCoulomb.SquareRootProgram.State line 14
  2. def OAI.ContinuumCoulomb.SquareRootProgram.code line 16
  3. def OAI.ContinuumCoulomb.SquareRootProgram.step line 18
  4. def OAI.ContinuumCoulomb.SquareRootProgram.root line 23
  5. theorem OAI.ContinuumCoulomb.SquareRootProgram.iterate_power line 26
  6. theorem OAI.ContinuumCoulomb.SquareRootProgram.root_spec line 38

    Source documentation

    The returned integer brackets the true square root by adjacent integers.

    theorem root_spec (m : ℕ) : root m ^ 2 ≤ m ∧ m < (root m + 1) ^ 2 := by
…

    Mentions: OAI.ContinuumCoulomb.SquareRootProgram.root

  7. theorem OAI.ContinuumCoulomb.SquareRootProgram.root_le_sqrt line 42
  8. theorem OAI.ContinuumCoulomb.SquareRootProgram.sqrt_lt_root_add_one line 46
  9. def OAI.ContinuumCoulomb.SquareRootProgram.measure line 50
  10. theorem OAI.ContinuumCoulomb.SquareRootProgram.code_length line 52
  11. theorem OAI.ContinuumCoulomb.SquareRootProgram.measure_le_code line 57
  12. theorem OAI.ContinuumCoulomb.SquareRootProgram.code_le_measure line 62
  13. theorem OAI.ContinuumCoulomb.SquareRootProgram.step_measure line 67
  14. theorem OAI.ContinuumCoulomb.SquareRootProgram.iterate_half_bits line 74
  15. theorem OAI.ContinuumCoulomb.SquareRootProgram.iterate_measure line 82
  16. theorem OAI.ContinuumCoulomb.SquareRootProgram.iterate_code_bound line 93
  17. def OAI.ContinuumCoulomb.SquareRootProgram.stepProgram line 104
  18. def OAI.ContinuumCoulomb.SquareRootProgram.repeatProgram line 118
  19. def OAI.ContinuumCoulomb.SquareRootProgram.rawProgram line 122
  20. def OAI.ContinuumCoulomb.SquareRootProgram.program line 136
  21. def OAI.ContinuumCoulomb.SquareRootProgram.certificate line 139