OAI/MathematicalPhysics/ContinuumCoulomb/Programs/SourceMetadataProgram.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The actual source parser computes unary polynomial bounds from the raw encoding length. No polynomial bound is supplied as an unverified oracle.

  1. def OAI.ContinuumCoulomb.SourceMetadataProgram.size line 11
  2. opaque OAI.ContinuumCoulomb.SourceMetadataProgram.sizeProgram line 13
  3. def OAI.ContinuumCoulomb.SourceMetadataProgram.boundProgram line 16
  4. opaque OAI.ContinuumCoulomb.SourceMetadataProgram.vertexCount line 22
  5. opaque OAI.ContinuumCoulomb.SourceMetadataProgram.edgeCount line 26
  6. def OAI.ContinuumCoulomb.SourceMetadataProgram.input line 31
  7. opaque OAI.ContinuumCoulomb.SourceMetadataProgram.environment line 35
  8. opaque OAI.ContinuumCoulomb.SourceMetadataProgram.inputProgram line 38
  9. def OAI.ContinuumCoulomb.SourceMetadataProgram.normalizedProgram line 41
  10. def OAI.ContinuumCoulomb.SourceMetadataProgram.certificate line 44