OAI/MathematicalPhysics/ContinuumCoulomb/Programs/SourcePrograms.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Literal finite-stack decoding of every source field, including counted coordinate/edge lists and noncanonical rational pairs. The resulting registers use the existing proved machine list and rational arithmetic.

  1. def OAI.ContinuumCoulomb.SourcePrograms.equivSplitter line 14
  2. def OAI.ContinuumCoulomb.SourcePrograms.fieldInput line 18
  3. def OAI.ContinuumCoulomb.SourcePrograms.pairInput line 23
  4. def OAI.ContinuumCoulomb.SourcePrograms.rationalSplitter line 28
  5. def OAI.ContinuumCoulomb.SourcePrograms.coordinateSplitter line 32
  6. def OAI.ContinuumCoulomb.SourcePrograms.edgeSplitter line 35
  7. theorem OAI.ContinuumCoulomb.SourcePrograms.integer_length_pos line 40
  8. theorem OAI.ContinuumCoulomb.SourcePrograms.coordinate_length_pos line 43
  9. theorem OAI.ContinuumCoulomb.SourcePrograms.edge_length_pos line 49
  10. abbrev OAI.ContinuumCoulomb.SourcePrograms.Coordinate line 57
  11. def OAI.ContinuumCoulomb.SourcePrograms.coordinateCodec line 59
  12. def OAI.ContinuumCoulomb.SourcePrograms.coordinateListCodec line 61
  13. def OAI.ContinuumCoulomb.SourcePrograms.edgeListCodec line 63
  14. def OAI.ContinuumCoulomb.SourcePrograms.thresholdCodec line 65
  15. def OAI.ContinuumCoulomb.SourcePrograms.sourceTailCodec line 67
  16. def OAI.ContinuumCoulomb.SourcePrograms.sourceTupleCodec line 69
  17. def OAI.ContinuumCoulomb.SourcePrograms.coordinateListSplitter line 71
  18. def OAI.ContinuumCoulomb.SourcePrograms.edgeListSplitter line 74
  19. def OAI.ContinuumCoulomb.SourcePrograms.thresholdSplitter line 77
  20. def OAI.ContinuumCoulomb.SourcePrograms.sourceTailSplitter line 80
  21. def OAI.ContinuumCoulomb.SourcePrograms.sourceSplitter line 83
  22. def OAI.ContinuumCoulomb.SourcePrograms.rationalValue line 89

    Source documentation

    The rational denominator is parsed and reduced by the actual gcd-based machine routine, so noncanonical input fractions are handled correctly.

    noncomputable def rationalValue : Procedure binaryRationalCodec.encode ratCode BinaryRational.value := by
…

    Mentions: OAI.ContinuumCoulomb.BinaryRational.value

  23. def OAI.ContinuumCoulomb.SourcePrograms.sourceTuple line 100
  24. def OAI.ContinuumCoulomb.SourcePrograms.coordinatesRaw line 104
  25. def OAI.ContinuumCoulomb.SourcePrograms.tailRaw line 107
  26. def OAI.ContinuumCoulomb.SourcePrograms.tailTuple line 110
  27. def OAI.ContinuumCoulomb.SourcePrograms.edgesRaw line 114
  28. def OAI.ContinuumCoulomb.SourcePrograms.thresholdsRaw line 117
  29. def OAI.ContinuumCoulomb.SourcePrograms.thresholdTuple line 120
  30. def OAI.ContinuumCoulomb.SourcePrograms.coordinates line 124
  31. def OAI.ContinuumCoulomb.SourcePrograms.edges line 128
  32. def OAI.ContinuumCoulomb.SourcePrograms.lower line 132
  33. def OAI.ContinuumCoulomb.SourcePrograms.upper line 135
  34. def OAI.ContinuumCoulomb.SourcePrograms.registerCode line 138
  35. def OAI.ContinuumCoulomb.SourcePrograms.registers line 144

    Source documentation

    A concrete polynomial TM2 parser for the entire source instance.

    noncomputable def registers : Procedure binaryHeisenbergCodec.encode registerCode id :=
…

    Mentions: OAI.ContinuumCoulomb.SourcePrograms.registerCode

  36. def OAI.ContinuumCoulomb.SourcePrograms.registers_certificate line 147