OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumFiniteMembership.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Literal membership tests for the finite geometry tables used by the 140-candidate planar route selector. The Boolean fold has constant-size state.

  1. theorem OAI.ContinuumCoulomb.QuantumFiniteMembership.fold_or line 15
  2. opaque OAI.ContinuumCoulomb.QuantumFiniteMembership.anyProgram line 24
  3. def OAI.ContinuumCoulomb.QuantumFiniteMembership.memberProgram line 34
  4. opaque OAI.ContinuumCoulomb.QuantumFiniteMembership.pairEqProgram line 44
  5. opaque OAI.ContinuumCoulomb.QuantumFiniteMembership.pairMemberProgram line 47