OriginalLinearFilling.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.HyperbolicObstruction.ConeSkeleton.original_letter_linear_filling line 16
Source documentation
Deterministic linear filling theorem, with a uniform cutoff for all random tables and all original-letter null words, including the empty word.
```
theorem original_letter_linear_filling {α β δ : ℝ}
    (ha : 0 < α) (hb : 7*α < β) (hd : 0 < δ) :
    ∃ M : ℕ, 0 < M ∧ ∀ (n : ℕ)
      (w : TableModel.Entry (A := Alphabet n) rowSupport → Bool)
…
```
Mentions: OAI.HyperbolicObstruction.TableModel.Entry
theorem OAI.HyperbolicObstruction.ConeSkeleton.original_letter_linear_filling_list line 54
Source documentation
The same theorem in list-word form, with an explicit positive linear constant depending only on the fixed parameters.
```
theorem original_letter_linear_filling_list {α β δ : ℝ}
    (ha : 0 < α) (hb : 7*α < β) (hd : 0 < δ) :
    ∃ (M : ℕ) (C : ℝ), 0 < M ∧ 0 < C ∧ ∀ (n : ℕ)
      (w : TableModel.Entry (A := Alphabet n) rowSupport → Bool)
…
```
Mentions: OAI.HyperbolicObstruction.TableModel.Entry