OAI/NumberTheory/Ostmann/Arithmetic/MovingFrequencyFormulaGate.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The original formula gate in frequency and internal-prime coordinates

  1. theorem OAI.Ostmann.movingNodeGuard_signed_values line 10
  2. theorem OAI.Ostmann.movingNodeGuard_residue_of_signedIntegral line 31
  3. theorem OAI.Ostmann.movingSignedFrequencyUnits_local line 65
  4. theorem OAI.Ostmann.MovingSlotData.formulaNodes_residue_of_signedIntegral line 72
  5. theorem OAI.Ostmann.moving_formula_residue_frequency_internal_iff line 114