PulsePlateau.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Exact local motion on the open plateau surrounding a pulse rectangle. The explicit collar allows source neighborhoods, rather than only the closed source rectangles, to follow the same affine motion.

theorem OAI.ForcedComputation.PlanarHamiltonian.rectangleCutoff_one_near_plateau line 14
theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.spatial_on_plateau line 20
theorem OAI.ForcedComputation.PlanarHamiltonian.Pulse.curve_ode_plateau line 25
theorem OAI.ForcedComputation.PlanarHamiltonian.rectanglePlateau_of_dist_lt line 34
Source documentation
A perturbation smaller than the rational collar remains on the exact polynomial plateau. The norm here is the coordinate maximum norm.
```
theorem rectanglePlateau_of_dist_lt {R : RationalBox 2} {δ : ℚ}
    {x y : Plane} (hx : x ∈ R.carrier) (hxy : dist y x < (δ : ℝ)) :
    y ∈ rectanglePlateau R δ := by
…
```
Mentions: OAI.ForcedComputation.PlanarHamiltonian.rectanglePlateau

theorem OAI.ForcedComputation.PlanarHamiltonian.notMem_collar_of_dist_lt line 44

Source documentation

Endpoint-gap separation survives a controlled perturbation.

theorem notMem_collar_of_dist_lt {R S : RationalBox 2} {gap δ ε : ℚ}
    (hgap : PlanarRouting.EndpointGap gap R S) (hsmall : 2 * δ + ε ≤ gap)
    {x y : Plane} (hx : x ∈ S.carrier) (hxy : dist y x < (ε : ℝ)) :
    y ∉ (rectangleCollar R δ).carrier := by
…

Mentions: OAI.ForcedComputation.PlanarRouting.EndpointGap, OAI.ForcedComputation.PlanarHamiltonian.rectangleCollar