OAI/MathematicalPhysics/ContinuumCoulomb/Programs/ChargePrograms.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

Actual polynomial-time stack programs for the two rounded binary-well charges. The geometric scale is unary and the number of sites is binary. The output is the pair of binary natural-number codes.

  1. def OAI.ContinuumCoulomb.ChargePrograms.parameters line 16
  2. theorem OAI.ContinuumCoulomb.ChargePrograms.parameters_encoding line 19
  3. theorem OAI.ContinuumCoulomb.ChargePrograms.parameters_length line 25
  4. def OAI.ContinuumCoulomb.ChargePrograms.intToNatProgram line 34

    Source documentation

    Clamp a signed binary integer to a natural number.

    noncomputable def intToNatProgram : Procedure intCode Nat.bits Int.toNat :=
…
  5. def OAI.ContinuumCoulomb.ChargePrograms.rationalRoundProgram line 41

    Source documentation

    Ties round upward, exactly as the manuscript's rational charge function.

    noncomputable def rationalRoundProgram : Procedure ratCode intCode (fun q => round q) :=
…
  6. def OAI.ContinuumCoulomb.ChargePrograms.scaledRoundProgram line 46
  7. def OAI.ContinuumCoulomb.ChargePrograms.rawParameters line 53
  8. def OAI.ContinuumCoulomb.ChargePrograms.dProgram line 55
  9. def OAI.ContinuumCoulomb.ChargePrograms.mProgram line 58
  10. def OAI.ContinuumCoulomb.ChargePrograms.amplificationProgram line 61
  11. def OAI.ContinuumCoulomb.ChargePrograms.dRationalProgram line 65
  12. def OAI.ContinuumCoulomb.ChargePrograms.mRationalProgram line 68
  13. def OAI.ContinuumCoulomb.ChargePrograms.fractionProgram line 71
  14. def OAI.ContinuumCoulomb.ChargePrograms.primaryRatioProgram line 77
  15. def OAI.ContinuumCoulomb.ChargePrograms.primaryRawProgram line 82
  16. def OAI.ContinuumCoulomb.ChargePrograms.secondaryRawProgram line 86
  17. def OAI.ContinuumCoulomb.ChargePrograms.naturalInputProgram line 91

    Source documentation

    Parse the actual marker bits of a binary natural number.

    noncomputable def naturalInputProgram : Procedure BinaryEncoding.natural.encode Nat.bits id :=
…
  18. def OAI.ContinuumCoulomb.ChargePrograms.inputProgram line 94
  19. def OAI.ContinuumCoulomb.ChargePrograms.naturalOutputProgram line 101
  20. def OAI.ContinuumCoulomb.ChargePrograms.output line 104
  21. def OAI.ContinuumCoulomb.ChargePrograms.primaryProgram line 107
  22. def OAI.ContinuumCoulomb.ChargePrograms.secondaryProgram line 111
  23. def OAI.ContinuumCoulomb.ChargePrograms.pairProgram line 115
  24. def OAI.ContinuumCoulomb.ChargePrograms.program line 122

    Source documentation

    Both physical charges, including rational scaling and integer rounding, are computed by a finite Boolean-stack program with a polynomial runtime.

    noncomputable def program : Procedure parameters.encode output.encode
    (fun x => (binaryPrimaryCharge x.1 x.2, binarySecondaryCharge x.1 x.2)) :=
…

    Mentions: OAI.ContinuumCoulomb.binaryPrimaryCharge, OAI.ContinuumCoulomb.binarySecondaryCharge

  25. def OAI.ContinuumCoulomb.ChargePrograms.certificate line 127
  26. theorem OAI.ContinuumCoulomb.ChargePrograms.output_length line 131
  27. theorem OAI.ContinuumCoulomb.ChargePrograms.output_length_le line 139