OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Detector/ExpandingFiniteGates.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Finite parallel translation gates. Separation is required for the whole address table, so the selected computation is never used to define which gates are present.

  1. theorem OAI.ForcedComputation.ExpandingDetector.translationGate_eq_zero line 15
  2. theorem OAI.ForcedComputation.ExpandingDetector.other_gate_eq_zero line 21
  3. def OAI.ForcedComputation.ExpandingDetector.parallelGate line 37
  4. theorem OAI.ForcedComputation.ExpandingDetector.parallelGate_smooth line 41
  5. theorem OAI.ForcedComputation.ExpandingDetector.parallelGate_properties line 45
  6. theorem OAI.ForcedComputation.ExpandingDetector.parallelGate_plateau line 77