LetterCover.lean`

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

def OAI.HyperbolicObstruction.ConeSkeleton.letterVoltage line 20
Source documentation
The actual original marked presentation supplies the deck labels, via fixed fan routes; the larger auxiliary polygon bouquet group is not used.
```
def letterVoltage (e : Dart n w) : LetterPresentation.Group n w d :=
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.Dart, OAI.HyperbolicObstruction.LetterPresentation.Group
lemma OAI.HyperbolicObstruction.ConeSkeleton.letterVoltage_rev line 23
lemma OAI.HyperbolicObstruction.ConeSkeleton.letterVoltage_word line 27
lemma OAI.HyperbolicObstruction.ConeSkeleton.letterVoltage_cell line 36
lemma OAI.HyperbolicObstruction.ConeSkeleton.letterVoltage_letter line 48
def OAI.HyperbolicObstruction.ConeSkeleton.letterGroupCover line 54
Source documentation
A fully constructed cover target for the actual letter quotient. Its relation equations are theorems, not assumptions of the chain conclusion.
```
def letterGroupCover := actualCellCover n w d (letterVoltage n w d)
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.actualCellCover, OAI.HyperbolicObstruction.ConeSkeleton.letterVoltage
def OAI.HyperbolicObstruction.ConeSkeleton.letterIntegralTarget line 57
def OAI.HyperbolicObstruction.ConeSkeleton.letterIntegralFrozenTarget line 60
theorem OAI.HyperbolicObstruction.ConeSkeleton.uniform_letter_integral_chain_zero line 65
Source documentation
Uniformly in every realization of the original arrays, not a scalar projection and not a conclusion conditional on cover equations.
```
theorem uniform_letter_integral_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
theorem OAI.HyperbolicObstruction.ConeSkeleton.finalDiagramStage_letter_chain_zero line 82
Source documentation
For the SAME independently sampled presentation, every spherical picture with its actual original-group lift has zero full integral cell vector. Infinitude and identification with the topological universal cover are NOT asserted by this combinatorial theorem.
```
theorem finalDiagramStage_letter_chain_zero (m : ℕ)
    (P : WalkPicture.{0} (letterIntegralTarget (finalDiagramStage m).size
      (finalDiagramStage m).master (finalDiagramStage m).six))
    (hm : P.FrozenMapped (letterIntegralFrozenTarget (finalDiagramStage m).size
      (finalDiagramStage m).master (finalDiagramStage m).six)) : P.chain = 0 :=
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.letterIntegralTarget, OAI.HyperbolicObstruction.ConeSkeleton.size, OAI.HyperbolicObstruction.ConeSkeleton.letterIntegralFrozenTarget