OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Flow/PlanarDormantMargin.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Quantitative clearance for unused pulses. The enlarged rational collar leaves room for perturbing an entire source rectangle by a positive radius.

  1. theorem OAI.ForcedComputation.Recorder.Planar.routingCollar_four_small line 14
  2. theorem OAI.ForcedComputation.Recorder.Planar.ordered_source_four_gap line 25
  3. theorem OAI.ForcedComputation.Recorder.Planar.ordered_target_four_gap line 42
  4. theorem OAI.ForcedComputation.Recorder.Planar.extractHorizontal_sparse_four_zero line 62
  5. theorem OAI.ForcedComputation.Recorder.Planar.extractVertical_sparse_four_zero line 116
  6. theorem OAI.ForcedComputation.Recorder.Planar.scale_sparse_four_zero line 168
  7. theorem OAI.ForcedComputation.Recorder.Planar.insertVertical_sparse_four_zero line 221
  8. theorem OAI.ForcedComputation.Recorder.Planar.insertHorizontal_sparse_four_zero line 272
  9. theorem OAI.ForcedComputation.Recorder.Planar.action_sparseAnchor_notMem_four_collar line 324
  10. theorem OAI.ForcedComputation.Recorder.Planar.sparseAnchor_notMem_four_collar line 338
  11. theorem OAI.ForcedComputation.PlanarHamiltonian.notMem_collar_of_notMem_four line 355

    Source documentation

    Exclusion from the enlarged closed collar persists under a small displacement.

    theorem notMem_collar_of_notMem_four {R : RationalBox 2} {δ : ℚ}
    (hδ : 0 < δ) {x y : Plane}
    (hx : x ∉ (rectangleCollar R (4 * δ)).carrier)
    (hxy : dist y x < (δ : ℝ)) : y ∉ (rectangleCollar R δ).carrier := by
…

    Mentions: OAI.ForcedComputation.PlanarHamiltonian.rectangleCollar

  12. theorem OAI.ForcedComputation.Recorder.Planar.sparseAnchor_near_notMem_collar line 378

    Source documentation

    An unused pulse remains zero on a full neighborhood of the current anchor.

    theorem sparseAnchor_near_notMem_collar (M : Alternating.Machine) (hM : M.WellFormed)
    (b : Branch (finiteMachine M hM)) {x y : Plane}
    (hx : x ∈ (instruction M hM b).source.carrier)
    (i : Fin (actions M hM).length)
    (hi : ∀ k, (branchIndices M hM b k).val ≠ i.val)
    (hxy : dist y (sparseAnchor (branchIndices M hM b) (branchAnchors M hM b x) i.val) <
      (routingCollar M hM : ℝ)) :
    y ∉ (rectangleCollar (compiledPulse M hM i).rectangle (compiledPulse M hM i).collar).carrier := by
…

    Mentions: OAI.Alternating.Machine, OAI.ForcedComputation.Recorder.Branch, OAI.ForcedComputation.Recorder.finiteMachine, OAI.ForcedComputation.Recorder.Planar.instruction, OAI.ForcedComputation.Recorder.Planar.actions, OAI.ForcedComputation.Recorder.Planar.branchIndices, OAI.ForcedComputation.Recorder.Planar.branchAnchors, OAI.ForcedComputation.Recorder.Planar.routingCollar, OAI.ForcedComputation.Recorder.Planar.compiledPulse