LiftedDiagramSampling.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

def OAI.HyperbolicObstruction.IncidenceTemplate.finalDiagramCutoff line 20
Source documentation
A single diagonal cutoff for filling and the full LIFTED chain statement. Nothing about a future picture, action, word, or deck group is sampled later.
```
def finalDiagramCutoff (m : ℕ) : ℕ :=
…
```
def OAI.HyperbolicObstruction.IncidenceTemplate.finalDiagramStage line 26
lemma OAI.HyperbolicObstruction.IncidenceTemplate.finalDiagramStage_good line 29

theorem OAI.HyperbolicObstruction.IncidenceTemplate.finalDiagramStage_linear line 35

Source documentation

Finite-letter linear filling for the same final selected arrays.

theorem finalDiagramStage_linear (m : ℕ) :
    ∃ C : ℝ, 0 < C ∧ ∀ word : List (LetterPresentation.Alphabet (finalDiagramStage m).size),
      PresentedGroup.mk (Relator (finalDiagramStage m).size (finalDiagramStage m).master
        (finalDiagramStage m).six) (FreeGroup.mk word) = 1 →
      ∃ a, WordPictures.Homotopy (SimpleWordRelator (finalDiagramStage m).size
        (finalDiagramStage m).master (finalDiagramStage m).six) word [] a ∧
        (a : ℝ) ≤ C * word.length := by
…

Mentions: OAI.HyperbolicObstruction.LetterPresentation.Alphabet, OAI.HyperbolicObstruction.IncidenceTemplate.finalDiagramStage, OAI.HyperbolicObstruction.WordPictures.Homotopy

theorem OAI.HyperbolicObstruction.IncidenceTemplate.finalDiagramStage_lifted_chain_zero line 53

Source documentation

All lifted cellular coefficients vanish for every mapped spherical picture for the final selected arrays. Unlike projected chain sums, coefficients for different deck translates of one cell may be chosen independently.

theorem finalDiagramStage_lifted_chain_zero (m : ℕ)
    (G : Type) [Group G] (A : Type) [AddCommGroup A]
    (voltage : Dart (finalDiagramStage m).size (finalDiagramStage m).master → G)
    (hv : ∀ e, voltage (rev (finalDiagramStage m).size (finalDiagramStage m).master e) = (voltage e)⁻¹)
    (hcell : ∀ a : Cell (finalDiagramStage m).size (finalDiagramStage m).master (finalDiagramStage m).six,
      (List.ofFn (fun i => voltage (side (finalDiagramStage m).size (finalDiagramStage m).master
        (finalDiagramStage m).six a i))).prod = 1)
    (c : G → Top (finalDiagramStage m).size (finalDiagramStage m).master → MacroGraph.graph.Dart → A)
    (hc : ∀ g a e, c g a e.symm = -c g a e)
    (f : G → FrozenCell (finalDiagramStage m).size (finalDiagramStage m).master (finalDiagramStage m).six → A)
    (P : WalkPicture.{0} (liftedWalkTarget (finalDiagramStage m).size (finalDiagramStage m).master
      (finalDiagramStage m).six voltage hv hcell c hc f))
…

Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.finalDiagramStage

theorem OAI.HyperbolicObstruction.IncidenceTemplate.finalDiagramSamplingSequence line 73
theorem OAI.HyperbolicObstruction.IncidenceTemplate.finalDiagramStage_eventually_noAction line 80
Source documentation
If every selected letter group is infinite, then all sufficiently late groups admit no geometric CAT(0) action.
```
theorem finalDiagramStage_eventually_noAction
    [∀ m, Infinite (SamplingStage.LetterGroup finalDiagramStage m)] :
    ∀ᶠ m in Filter.atTop, NoGeometricCATZeroAction (SamplingStage.LetterGroup finalDiagramStage m) :=
…
```
Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.SamplingStage.LetterGroup, OAI.HyperbolicObstruction.IncidenceTemplate.finalDiagramStage, OAI.HyperbolicObstruction.NoGeometricCATZeroAction