DiagramSampling.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.HyperbolicObstruction.IncidenceTemplate.diagramCutoff line 18
Source documentation
One cutoff simultaneously enforces the original-letter linear filling and unbounded closed-picture chain vanishing. It is selected before each alphabet and realization.
```
def diagramCutoff (m : ℕ) : ℕ :=
…
```
def OAI.HyperbolicObstruction.IncidenceTemplate.diagramSelectedStage line 26

theorem OAI.HyperbolicObstruction.IncidenceTemplate.diagramSelectedStage_linear line 31

Source documentation

Every selected realization has an actual finite-letter linear Dehn bound, not a radius-limited or surrogate-picture estimate.

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

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

theorem OAI.HyperbolicObstruction.IncidenceTemplate.diagramSelectedStage_chain_zero line 49

Source documentation

The SAME selected arrays have vanishing chain for every closed mapped picture and every abelian coefficient group. No bound on picture size remains. This does NOT assert their topological asphericity.

theorem diagramSelectedStage_chain_zero (m : ℕ)
    (A : Type) [AddCommGroup A]
    (c : Top (diagramSelectedStage m).size (diagramSelectedStage m).master →
      MacroGraph.graph.Dart → A)
    (hc : ∀ a e, c a e.symm = -c a e)
    (f : FrozenCell (diagramSelectedStage m).size (diagramSelectedStage m).master
      (diagramSelectedStage m).six → A)
    (P : WalkPicture.{0} (walkTarget (diagramSelectedStage m).size (diagramSelectedStage m).master
      (diagramSelectedStage m).six c hc f))
    (hm : P.FrozenMapped (walkFrozenTarget (diagramSelectedStage m).size
      (diagramSelectedStage m).master (diagramSelectedStage m).six c hc f)) : P.chain = 0 := by
…

Mentions: OAI.HyperbolicObstruction.IncidenceTemplate.diagramSelectedStage

theorem OAI.HyperbolicObstruction.IncidenceTemplate.diagramSamplingSequence line 69
Source documentation
The selected sequence retains ALL the probabilistic conditional sampling laws used in the obstruction argument; no new sampling hypothesis is required.
```
theorem diagramSamplingSequence : SamplingSequence Field Admissible
    (SamplingStage.Alphabet diagramSelectedStage) (SamplingStage.Matches diagramSelectedStage)
    (SamplingStage.label diagramSelectedStage) :=
…
```
Mentions: OAI.HyperbolicObstruction.SamplingSequence, OAI.HyperbolicObstruction.IncidenceTemplate.Field, OAI.HyperbolicObstruction.IncidenceTemplate.Admissible, OAI.HyperbolicObstruction.IncidenceTemplate.SamplingStage.Alphabet, OAI.HyperbolicObstruction.IncidenceTemplate.diagramSelectedStage, OAI.HyperbolicObstruction.IncidenceTemplate.SamplingStage.Matches, OAI.HyperbolicObstruction.IncidenceTemplate.SamplingStage.label