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

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Clock and observation margins for the entire filled branch trajectory.

  1. theorem OAI.ForcedComputation.Recorder.Planar.shifted_parking_bounds line 13

    Source documentation

    The parking rectangles have room for the rational initial translation.

    theorem shifted_parking_bounds {n : ℕ} {κ : ℚ} (hκ : 0 ≤ κ) (hκ' : κ ≤ 1 / 64)
    (i : Fin n) (δ : Fin 2 → ℚ)
    (hδ₀ : |(δ 0 : ℝ)| ≤ 1 / 512) (hδ₁ : |(δ 1 : ℝ)| ≤ 3 / 1024)
    {x : Plane} (hx : x ∈ (parkingBox n κ i).carrier) :
    translatedPoint δ x ∈ clockRectangle.carrier ∧ 3 / 16 ≤ translatedPoint δ x 1 := by
…
  2. theorem OAI.ForcedComputation.Recorder.Planar.horizontalPoint_vertical line 52
  3. theorem OAI.ForcedComputation.Recorder.Planar.shifted_horizontalPoint_clock line 56
  4. theorem OAI.ForcedComputation.Recorder.Planar.branch_scaledStage_mem line 96
  5. theorem OAI.ForcedComputation.Recorder.Planar.shifted_branchAnchors_clock line 107
  6. theorem OAI.ForcedComputation.Recorder.Planar.shifted_branchAnchors_safe line 137
  7. theorem OAI.ForcedComputation.Recorder.Planar.normalizedAnchors_clock line 164
  8. theorem OAI.ForcedComputation.Recorder.Planar.normalizedAnchors_safe line 171
  9. theorem OAI.ForcedComputation.Recorder.Planar.normalizedCurve_segment line 179
  10. theorem OAI.ForcedComputation.Recorder.Planar.normalizedCurve_clock line 195
  11. theorem OAI.ForcedComputation.Recorder.Planar.normalizedCurve_safe line 213