NormalizedSuspensionRouting.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The finite geometric exclusion condition implies the exact one-period material trajectory of the normalized stationary suspension.

theorem OAI.ForcedComputation.Recorder.Planar.normalized_branch_suspension_in line 15

Source documentation

The pulse schedule, spatial clearance, ODE, endpoints and clock bounds all come from the finite compiler.

theorem normalized_branch_suspension_in (I : Alternating.MachineInput)
    (hI : Alternating.ValidInput I)
    (b : Branch (finiteMachine (freshMachine I.1) (freshInput_valid hI).1))
    {x : Plane} (hx : x ∈ (instruction (freshMachine I.1) (freshInput_valid hI).1 b).source.carrier)
    {Φ : ℝ → Space → Space}
    (hΦ : IsMaterialFlow 1 (fun y =>
      SpatialExpression.suspensionField (normalizedHamiltonian I hI) y.2) Φ)
    {S : Set Plane} (hS : S ⊆ clockRectangle.carrier)
    (hp : ∀ k, normalizedAnchors I hI b x k ∈ S)
    (hcurve : ∀ k t, normalizedCurve I hI b x k t ∈ S) :
    Φ 1 (atHeight (normalizedAnchors I hI b x 0) 0) =
        atHeight (normalizedAnchors I hI b x 8) 1 ∧
…

theorem OAI.ForcedComputation.Recorder.Planar.normalized_branch_suspension line 39
theorem OAI.ForcedComputation.Recorder.Planar.normalized_branch_suspension_safe line 53