OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumOrderedLabelBlocks.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Literal fixed-size programs for the triple partition and YY/private blocks. The branch tests inspect only the stored support labels.

  1. opaque OAI.ContinuumCoulomb.QuantumOrderedLabelData.entryProgram line 13
  2. opaque OAI.ContinuumCoulomb.QuantumOrderedLabelData.labelTest line 17
  3. opaque OAI.ContinuumCoulomb.QuantumOrderedLabelData.lengthTest line 21
  4. def OAI.ContinuumCoulomb.QuantumOrderedLabelData.selected line 27
  5. def OAI.ContinuumCoulomb.QuantumOrderedLabelData.selectedProgram line 29
  6. def OAI.ContinuumCoulomb.QuantumOrderedLabelData.partitionLookup line 34
  7. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelData.partitionLookup_eq line 43
  8. opaque OAI.ContinuumCoulomb.QuantumOrderedLabelData.partitionProgram line 57
  9. opaque OAI.ContinuumCoulomb.QuantumOrderedLabelData.pairLabelsProgram line 69
  10. opaque OAI.ContinuumCoulomb.QuantumOrderedLabelData.realLabelsProgram line 72
  11. opaque OAI.ContinuumCoulomb.QuantumOrderedLabelData.thirdMediatorProgram line 75
  12. opaque OAI.ContinuumCoulomb.QuantumOrderedLabelData.thirdBlockProgram line 79
  13. opaque OAI.ContinuumCoulomb.QuantumOrderedLabelData.zerosProgram line 103
  14. def OAI.ContinuumCoulomb.QuantumOrderedLabelData.yyLookup line 107
  15. theorem OAI.ContinuumCoulomb.QuantumOrderedLabelData.yyLookup_eq line 112
  16. def OAI.ContinuumCoulomb.QuantumOrderedLabelData.relabelProgram line 123
  17. def OAI.ContinuumCoulomb.QuantumOrderedLabelData.crossedProgram line 127
  18. opaque OAI.ContinuumCoulomb.QuantumOrderedLabelData.yyFactorsProgram line 131
  19. opaque OAI.ContinuumCoulomb.QuantumOrderedLabelData.yyBlockProgram line 142
  20. opaque OAI.ContinuumCoulomb.QuantumOrderedLabelData.privateBlockProgram line 158