SpatialChunks.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.GammaFPP.CrossingBridge.spatial_chunk_decomposition line 10
Source documentation
The source first-exit decomposition of every actual finite path. Empty remainders are retained; every full chunk is nonempty.
```
theorem spatial_chunk_decomposition (b : ℝ) (k m : ℕ) (ds : List Step) :
    ∃ blocks : List (List Step), ∃ rest : List Step,
      ds=blocks.flatten++rest ∧ (∀ q ∈ blocks, FullSpatialChunk b k m q) ∧
      (∀ i ≤ rest.length, chunkInterior b k m (displacement (rest.take i))) := by
…
```
Mentions: OAI.GammaFPP.CrossingBridge.FullSpatialChunk, OAI.GammaFPP.CrossingBridge.chunkInterior

lemma OAI.GammaFPP.CrossingBridge.spatial_chunk_displacement_bound line 32

Source documentation

Each full chunk and the remainder change the longitudinal coordinate by at most 2L, giving the cut-number bound from the manuscript.

lemma spatial_chunk_displacement_bound (b : ℝ) (hb : |b| ≤ 1) (k m : ℕ)
    (blocks : List (List Step)) (rest : List Step)
    (hfull : ∀ q ∈ blocks, FullSpatialChunk b k m q)
    (hrest : ∀ i ≤ rest.length, chunkInterior b k m (displacement (rest.take i))) :
    |(displacement (blocks.flatten++rest)).1| ≤ 2*(2 : ℤ)^m*((blocks.length : ℤ)+1) := by
…

Mentions: OAI.GammaFPP.CrossingBridge.FullSpatialChunk, OAI.GammaFPP.CrossingBridge.chunkInterior

def OAI.GammaFPP.CrossingBridge.chunkIndexTail line 49
def OAI.GammaFPP.CrossingBridge.BoundedIndexSteps line 53
lemma OAI.GammaFPP.CrossingBridge.chunkIndexTail_length line 57
lemma OAI.GammaFPP.CrossingBridge.chunkIndexTail_bounded line 65
Source documentation
Every actual full-chunk itinerary obeys the bounded increment rule. The indices may repeat.
```
lemma chunkIndexTail_bounded (b : ℝ) (hb : |b| ≤ 1) (k m : ℕ) (hs : 2 ≤ (2 : ℝ)^k)
    (p : Vertex) (blocks : List (List Step))
    (hfull : ∀ q ∈ blocks, FullSpatialChunk b k m q) :
    BoundedIndexSteps (spatialChunkIndex b k m p) (chunkIndexTail b k m p blocks) := by
…
```
Mentions: OAI.GammaFPP.CrossingBridge.FullSpatialChunk, OAI.GammaFPP.CrossingBridge.BoundedIndexSteps, OAI.GammaFPP.CrossingBridge.spatialChunkIndex, OAI.GammaFPP.CrossingBridge.chunkIndexTail