OAI/MathematicalPhysics/ContinuumCoulomb/Quantum/QuantumRebitLocal.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The exact scalar core of a lifted term with one active reference qubit. Spectator reference bits are zero in the local core and contribute identities.

  1. def OAI.ContinuumCoulomb.QuantumAlgebraicHistory.referenceState line 15
  2. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.referenceState_eq_iff line 18
  3. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.reference_identity line 26
  4. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.localY_referenceState line 30
  5. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.lift_extend line 44
  6. def OAI.ContinuumCoulomb.QuantumAlgebraicHistory.oneReference line 64
  7. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.rebit_entry_of_references line 68
  8. theorem OAI.ContinuumCoulomb.QuantumAlgebraicHistory.rebit_lift_entry line 76