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

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

The actual finite list of rational affine instructions and the fixed unit-torus geometric data for the initialized computation construction.

  1. def OAI.ForcedComputation.Recorder.geometricBranches line 15
  2. def OAI.ForcedComputation.Recorder.geometricInstruction line 18
  3. def OAI.ForcedComputation.Recorder.compiledInput line 22
  4. theorem OAI.ForcedComputation.Recorder.geometricInstruction_mem line 30
  5. theorem OAI.ForcedComputation.Recorder.geometricInstruction_factor_pos line 37
  6. theorem OAI.ForcedComputation.Recorder.geometricInstruction_source_positive line 41
  7. theorem OAI.ForcedComputation.Recorder.geometricInstruction_target_positive line 46
  8. theorem OAI.ForcedComputation.Recorder.radixDigit_bounds_rat line 51
  9. theorem OAI.ForcedComputation.Recorder.geometricInstruction_source_unit line 57
  10. theorem OAI.ForcedComputation.Recorder.geometricInstruction_target_unit line 63
  11. theorem OAI.ForcedComputation.Recorder.geometricInstruction_halfWidths line 70
  12. theorem OAI.ForcedComputation.Recorder.stateBox_bounds line 86
  13. theorem OAI.ForcedComputation.Recorder.stateBox_nonterminal_x line 111
  14. theorem OAI.ForcedComputation.Recorder.stateBox_terminal_x line 120
  15. theorem OAI.ForcedComputation.Recorder.geometricInstruction_source_bounds line 129
  16. theorem OAI.ForcedComputation.Recorder.geometricInstruction_target_bounds line 135
  17. theorem OAI.ForcedComputation.Recorder.geometricInstruction_image line 141
  18. theorem OAI.ForcedComputation.Recorder.compiledInput_basic line 161
  19. theorem OAI.ForcedComputation.Recorder.compiledInput_chartMargin line 179
  20. theorem OAI.ForcedComputation.Recorder.stateBox_separation line 192
  21. theorem OAI.ForcedComputation.Recorder.geometricInstruction_source_separation line 217
  22. theorem OAI.ForcedComputation.Recorder.geometricInstruction_target_separation line 242
  23. theorem OAI.ForcedComputation.Recorder.indexed_map_separation line 269

    Source documentation

    Transfer a separation relation through a duplicate-free finite map.

    theorem indexed_map_separation {A B : Type*} (l : List A) (F : A → B)
    (hl : l.Nodup) (P : B → B → Prop)
    (hP : ∀ a b, a ≠ b → P (F a) (F b))
    (i j : Fin (l.map F).length) (hij : i ≠ j) : P ((l.map F)[i]) ((l.map F)[j]) := by
…
  24. theorem OAI.ForcedComputation.Recorder.compiledInput_source_separation line 283
  25. theorem OAI.ForcedComputation.Recorder.compiledInput_target_separation line 291
  26. theorem OAI.ForcedComputation.Recorder.compiledInput_valid line 301

    Source documentation

    The finite machine compiler supplies every hypothesis of the full-rectangle solenoidal-shear realization theorem.

    theorem compiledInput_valid (M : Alternating.Machine) (hM : M.WellFormed) :
    ValidInput (compiledInput M hM) := by
…

    Mentions: OAI.Alternating.Machine, OAI.ForcedComputation.Recorder.compiledInput