OAI/MathematicalPhysics/ContinuumCoulomb/ManyBody/MediatorUnaryPrimitives.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Actual unary arithmetic, projections, and a small repeated-doubling program for the fixed mediator scale constant.

  1. theorem OAI.ContinuumCoulomb.MediatorUnaryProgram.delta_as_mul line 11
  2. opaque OAI.ContinuumCoulomb.MediatorUnaryProgram.add line 16
  3. opaque OAI.ContinuumCoulomb.MediatorUnaryProgram.mul line 18
  4. opaque OAI.ContinuumCoulomb.MediatorUnaryProgram.rProgram line 21
  5. opaque OAI.ContinuumCoulomb.MediatorUnaryProgram.restProgram line 22
  6. opaque OAI.ContinuumCoulomb.MediatorUnaryProgram.wProgram line 24
  7. opaque OAI.ContinuumCoulomb.MediatorUnaryProgram.gProgram line 26
  8. opaque OAI.ContinuumCoulomb.MediatorUnaryProgram.nProgram line 28
  9. opaque OAI.ContinuumCoulomb.MediatorUnaryProgram.cube line 31
  10. opaque OAI.ContinuumCoulomb.MediatorUnaryProgram.rCube line 36
  11. opaque OAI.ContinuumCoulomb.MediatorUnaryProgram.wCube line 38
  12. opaque OAI.ContinuumCoulomb.MediatorUnaryProgram.cubicProduct line 39
  13. opaque OAI.ContinuumCoulomb.MediatorUnaryProgram.double line 41
  14. opaque OAI.ContinuumCoulomb.MediatorUnaryProgram.powerTwoStep line 47

    Source documentation

    Emit the fixed scale constant by twenty doublings. This keeps the finite machine description small instead of hardcoding a million pushes.

    noncomputable opaque powerTwoStep (k : ℕ)
    (p : Procedure envCode unaryCode (fun _ => 2 ^ k)) :
    Procedure envCode unaryCode (fun _ => 2 ^ (k + 1)) :=
…
  15. def OAI.ContinuumCoulomb.MediatorUnaryProgram.powerTwoConstant line 55
  16. opaque OAI.ContinuumCoulomb.MediatorUnaryProgram.scaleConstant line 59