OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumCrossingSelectFromSites.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The crossing selector is constructed from physical terminal indices. Every unselected edge avoids every selected pair; no matrix identity is assumed.

  1. def OAI.ContinuumCoulomb.QMARationalExchangeGraph.CrossingMatch line 14
  2. def OAI.ContinuumCoulomb.QMARationalExchangeGraph.crossingTag line 20
  3. theorem OAI.ContinuumCoulomb.QMARationalExchangeGraph.crossingTag_some line 23
  4. theorem OAI.ContinuumCoulomb.QMARationalExchangeGraph.crossingTag_none line 30
  5. def OAI.ContinuumCoulomb.QMARationalExchangeGraph.crossingSelection line 40
  6. theorem OAI.ContinuumCoulomb.QMARationalExchangeGraph.retained_no_crossing line 46