OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Programs/FiniteLabels.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Computable state and symbol labels obtained by indexing explicit finite lists.

  1. def OAI.ForcedComputation.Recorder.controlEnumeration line 10
  2. def OAI.ForcedComputation.Recorder.symbolEnumeration line 13
  3. def OAI.ForcedComputation.Recorder.controlLabel line 16
  4. def OAI.ForcedComputation.Recorder.symbolLabel line 21
  5. def OAI.ForcedComputation.Recorder.radixBase line 26
  6. def OAI.ForcedComputation.Recorder.radixDigit line 29
  7. theorem OAI.ForcedComputation.Recorder.radixBase_gt_one line 32
  8. theorem OAI.ForcedComputation.Recorder.radixDigit_bounds line 37
  9. theorem OAI.ForcedComputation.Recorder.radixDigit_gap line 41
  10. def OAI.ForcedComputation.Recorder.bandScale line 45
  11. def OAI.ForcedComputation.Recorder.centerY line 48
  12. def OAI.ForcedComputation.Recorder.recorderHalting line 51
  13. def OAI.ForcedComputation.Recorder.stateOffset line 55
  14. theorem OAI.ForcedComputation.Recorder.bandScale_pos line 59
  15. theorem OAI.ForcedComputation.Recorder.bandScale_le line 63
  16. theorem OAI.ForcedComputation.Recorder.centerY_bounds line 69
  17. theorem OAI.ForcedComputation.Recorder.centerY_gap line 86