OAI/MathematicalPhysics/ContinuumCoulomb/Programs/MediatorProgram.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

Actual polynomial-time arithmetic for the explicitly scaled rational mediator stage. Edge count, weight bound and inverse-error bound are unary; the entering coefficient and emitted spoke are canonical binary rationals.

  1. abbrev OAI.ContinuumCoulomb.MediatorProgram.Input line 13
  2. def OAI.ContinuumCoulomb.MediatorProgram.rawCode line 15
  3. def OAI.ContinuumCoulomb.MediatorProgram.rProgram line 18
  4. def OAI.ContinuumCoulomb.MediatorProgram.wProgram line 21
  5. def OAI.ContinuumCoulomb.MediatorProgram.gProgram line 25
  6. def OAI.ContinuumCoulomb.MediatorProgram.jProgram line 30
  7. def OAI.ContinuumCoulomb.MediatorProgram.cubeProgram line 35
  8. def OAI.ContinuumCoulomb.MediatorProgram.rCubeProgram line 39
  9. def OAI.ContinuumCoulomb.MediatorProgram.wCubeProgram line 43
  10. def OAI.ContinuumCoulomb.MediatorProgram.cubicProductProgram line 46
  11. def OAI.ContinuumCoulomb.MediatorProgram.scaleProgram line 50
  12. def OAI.ContinuumCoulomb.MediatorProgram.deltaProgram line 60
  13. def OAI.ContinuumCoulomb.MediatorProgram.precisionProgram line 65
  14. def OAI.ContinuumCoulomb.MediatorProgram.absoluteProgram line 70
  15. def OAI.ContinuumCoulomb.MediatorProgram.deltaRationalProgram line 80
  16. def OAI.ContinuumCoulomb.MediatorProgram.radicandProgram line 84
  17. def OAI.ContinuumCoulomb.MediatorProgram.numeratorProgram line 93
  18. def OAI.ContinuumCoulomb.MediatorProgram.denominatorProgram line 97
  19. def OAI.ContinuumCoulomb.MediatorProgram.rootInputProgram line 101
  20. def OAI.ContinuumCoulomb.MediatorProgram.spokeProgram line 107
  21. def OAI.ContinuumCoulomb.MediatorProgram.rationalCodec line 111
  22. def OAI.ContinuumCoulomb.MediatorProgram.rationalInput line 120
  23. def OAI.ContinuumCoulomb.MediatorProgram.rationalOutput line 129
  24. def OAI.ContinuumCoulomb.MediatorProgram.tailCodec line 132
  25. def OAI.ContinuumCoulomb.MediatorProgram.middleCodec line 135
  26. def OAI.ContinuumCoulomb.MediatorProgram.parameters line 138
  27. def OAI.ContinuumCoulomb.MediatorProgram.inputR line 141
  28. def OAI.ContinuumCoulomb.MediatorProgram.inputW line 144
  29. def OAI.ContinuumCoulomb.MediatorProgram.inputG line 149
  30. def OAI.ContinuumCoulomb.MediatorProgram.inputJ line 155
  31. def OAI.ContinuumCoulomb.MediatorProgram.inputProgram line 161
  32. def OAI.ContinuumCoulomb.MediatorProgram.publicDelta line 164
  33. def OAI.ContinuumCoulomb.MediatorProgram.publicSpoke line 168
  34. def OAI.ContinuumCoulomb.MediatorProgram.output line 172
  35. def OAI.ContinuumCoulomb.MediatorProgram.pairedProgram line 174
  36. def OAI.ContinuumCoulomb.MediatorProgram.certificate line 181

    Source documentation

    The actual finite machine, including rational normalization and square root search, has polynomial runtime in the explicit unary/binary inputs.

    noncomputable def certificate :
    Turing.TM2ComputableInPolyTime parameters.encode output.encode
      (fun x => (MediatorParameters.delta x.1 x.2.1 x.2.2.1,
        MediatorParameters.spoke x.1 x.2.1 x.2.2.1 x.2.2.2)) :=
…

    Mentions: OAI.ContinuumCoulomb.MediatorParameters.delta, OAI.ContinuumCoulomb.MediatorParameters.spoke

  37. theorem OAI.ContinuumCoulomb.MediatorProgram.parameters_length line 187
  38. theorem OAI.ContinuumCoulomb.MediatorProgram.output_polynomial_size line 196

    Source documentation

    The emitted coefficient code has a polynomial length bound obtained from the actual finite machine, including the square-root computation.

    theorem output_polynomial_size : ∃ p : Polynomial ℕ, ∀ x : Input,
    (output.encode (MediatorParameters.delta x.1 x.2.1 x.2.2.1,
      MediatorParameters.spoke x.1 x.2.1 x.2.2.1 x.2.2.2)).length ≤
        p.eval (parameters.encode x).length := by
…

    Mentions: OAI.ContinuumCoulomb.MediatorProgram.Input, OAI.ContinuumCoulomb.MediatorParameters.delta, OAI.ContinuumCoulomb.MediatorParameters.spoke