OAI/MathematicalPhysics/ContinuumCoulomb/Programs/MediatorThreeStageProgram.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The actual finite-stack program for all three simultaneous mediator stages. It retains the first central bonds, subdivides the first spokes, then subdivides all resulting six-bond paths.

  1. opaque OAI.ContinuumCoulomb.MediatorThreeStageProgram.environment line 12
  2. opaque OAI.ContinuumCoulomb.MediatorThreeStageProgram.secondInput line 14
  3. opaque OAI.ContinuumCoulomb.MediatorThreeStageProgram.secondPaths line 18
  4. opaque OAI.ContinuumCoulomb.MediatorThreeStageProgram.thirdInput line 23
  5. def OAI.ContinuumCoulomb.MediatorThreeStageProgram.finalBonds line 29
  6. opaque OAI.ContinuumCoulomb.MediatorThreeStageProgram.bondsProgram line 38
  7. opaque OAI.ContinuumCoulomb.MediatorThreeStageProgram.verticesProgram line 43
  8. opaque OAI.ContinuumCoulomb.MediatorThreeStageProgram.boundProgram line 47
  9. def OAI.ContinuumCoulomb.MediatorThreeStageProgram.outputCode line 51
  10. opaque OAI.ContinuumCoulomb.MediatorThreeStageProgram.outputProgram line 56
  11. def OAI.ContinuumCoulomb.MediatorThreeStageProgram.certificate line 59
  12. theorem OAI.ContinuumCoulomb.MediatorThreeStageProgram.finalBonds_length line 62