SpatialBadPathCover.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

def OAI.GammaFPP.CrossingBridge.SpatialBadPath line 11
Source documentation
The manuscript's bad simple-path event at a fixed scale. The path starts at the origin; the exact first-exit conditions and empty remainder are kept.
```
def SpatialBadPath (w : Edge → ℝ) (b m₀ a η : ℝ) (k m N : ℕ) : Prop :=
…
```

theorem OAI.GammaFPP.CrossingBridge.spatial_bad_path_cover line 20

Source documentation

Every bad actual path is covered by one itinerary and one weak composition. No choice of individual witnessing paths is included in the finite count.

theorem spatial_bad_path_cover (w : Edge → ℝ) (hw : ∀ e, 0 ≤ w e)
    (b m₀ am ap K η : ℝ) (hb : |b| ≤ 1) (ha : am ≤ ap) (hη : 0 < η)
    (hgap : 4*η ≤ (ap-am)/2) (k m : ℕ) (hs : 2 ≤ (2 : ℝ)^k)
    (hstep : max |m₀-((am+ap)/2)*b| |(am+ap)/2| ≤ η*(2 : ℝ)^k)
    (hscale₁ : η*(2 : ℝ)^k < 2*m₀*(2 : ℝ)^m-|((am+ap)/2)| *((2 : ℝ)^k+1))
    (hscale₂ : 3*η*(2 : ℝ)^k+2*|((am+ap)/2)| *((2 : ℝ)^k+1) < K*(2 : ℝ)^k)
    (N : ℕ) (hN : 4 ≤ N) (hbad : SpatialBadPath w b m₀ ((am+ap)/2) η k m N) :
    ∃ is ∈ spatialItineraries 0 N, ∃ ns ∈ compositionCover N (N/16),
      (0::is).length=ns.length ∧
      GammaFPP.BK.StrictDisjointPaths (spatialListSupport b k m (witnessLabels ns (0::is)))
        ((witnessLabels ns (0::is)).map (spatialWitnessFamily b m₀ am ap K η k m)) w := by
…

Mentions: OAI.GammaFPP.CrossingBridge.SpatialBadPath, OAI.GammaFPP.CrossingBridge.spatialItineraries, OAI.GammaFPP.CrossingBridge.compositionCover, OAI.GammaFPP.BK.StrictDisjointPaths, OAI.GammaFPP.CrossingBridge.spatialListSupport, OAI.GammaFPP.CrossingBridge.witnessLabels, OAI.GammaFPP.CrossingBridge.spatialWitnessFamily