OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumEvenTapeGeometry.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

The literal even tape has the canonical reserved-leaf geometry, up to its explicit vertex and triple-edge ordering.

  1. def OAI.ContinuumCoulomb.QuantumEvenTapeGeometry.input line 19
  2. theorem OAI.ContinuumCoulomb.QuantumEvenTapeGeometry.input_valid line 23
  3. theorem OAI.ContinuumCoulomb.QuantumEvenTapeGeometry.count_eq line 26
  4. theorem OAI.ContinuumCoulomb.QuantumEvenTapeGeometry.bonds_length line 30
  5. def OAI.ContinuumCoulomb.QuantumEvenTapeGeometry.tripleEquiv line 33
  6. def OAI.ContinuumCoulomb.QuantumEvenTapeGeometry.vertex line 38
  7. def OAI.ContinuumCoulomb.QuantumEvenTapeGeometry.edge line 42
  8. theorem OAI.ContinuumCoulomb.QuantumEvenTapeGeometry.route_eq line 46
  9. theorem OAI.ContinuumCoulomb.QuantumEvenTapeGeometry.source_eq line 52
  10. def OAI.ContinuumCoulomb.QuantumEvenTapeGeometry.tagLeft line 61
  11. def OAI.ContinuumCoulomb.QuantumEvenTapeGeometry.tagRight line 64
  12. theorem OAI.ContinuumCoulomb.QuantumEvenTapeGeometry.fresh_val line 67
  13. theorem OAI.ContinuumCoulomb.QuantumEvenTapeGeometry.old_val line 72
  14. theorem OAI.ContinuumCoulomb.QuantumEvenTapeGeometry.tag_left line 74
  15. theorem OAI.ContinuumCoulomb.QuantumEvenTapeGeometry.tag_right line 87
  16. theorem OAI.ContinuumCoulomb.QuantumEvenTapeGeometry.entry_tag line 96
  17. theorem OAI.ContinuumCoulomb.QuantumEvenTapeGeometry.literal_left line 104
  18. theorem OAI.ContinuumCoulomb.QuantumEvenTapeGeometry.literal_right line 117
  19. theorem OAI.ContinuumCoulomb.QuantumEvenTapeGeometry.literal_work line 130
  20. def OAI.ContinuumCoulomb.QuantumEvenTapeGeometry.relabel line 144
  21. def OAI.ContinuumCoulomb.QuantumEvenTapeGeometry.embedding line 156
  22. theorem OAI.ContinuumCoulomb.QuantumEvenTapeGeometry.ofFn_cast line 160
  23. theorem OAI.ContinuumCoulomb.QuantumEvenTapeGeometry.entry_count line 165
  24. theorem OAI.ContinuumCoulomb.QuantumEvenTapeGeometry.triple_cast line 168
  25. theorem OAI.ContinuumCoulomb.QuantumEvenTapeGeometry.represents line 172
  26. theorem OAI.ContinuumCoulomb.QuantumEvenTapeGeometry.work_le line 201
  27. theorem OAI.ContinuumCoulomb.QuantumEvenTapeGeometry.embedding_bounded line 215
  28. theorem OAI.ContinuumCoulomb.QuantumEvenTapeGeometry.realizes line 220