GlobalClosedPicture.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.HyperbolicObstruction.ConeSkeleton.uniform_normal_picture_empty line 20
Source documentation
Unbounded normal spherical-picture vanishing. The size cutoff is in the rank EVENT, not in the picture: the theorem applies to every finite normal picture for that realization, without any assumed separator interface.
```
theorem uniform_normal_picture_empty {α β δ : ℝ}
    (ha : 0 < α) (hb : 7*α < β) (hd : 0 < δ) :
    ∃ K : ℕ, 0 < K ∧ ∀ (n : ℕ)
      (w : TableModel.Entry (A := Alphabet n) rowSupport → Bool)
…
```
Mentions: OAI.HyperbolicObstruction.TableModel.Entry
theorem OAI.HyperbolicObstruction.ConeSkeleton.uniform_closed_picture_chain_zero line 55
Source documentation
Every literal genus-zero closed picture carries zero chain, after the proved finite normal-form surgeries. This is not yet the topological theorem that a nonzero Hurewicz cycle admits such a picture.
```
theorem uniform_closed_picture_chain_zero {α β δ : ℝ}
    (ha : 0 < α) (hb : 7*α < β) (hd : 0 < δ) :
    ∃ M : ℕ, 0 < M ∧ ∀ (n : ℕ)
      (w : TableModel.Entry (A := Alphabet n) rowSupport → Bool)
…
```
Mentions: OAI.HyperbolicObstruction.TableModel.Entry