OAI/Geometry/HyperbolicGroups/ActualLiftedChain.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.ConeSkeleton.liftedWalkTarget line 24
2. def OAI.HyperbolicObstruction.ConeSkeleton.liftedFrozenTarget line 29
3. theorem OAI.HyperbolicObstruction.ConeSkeleton.uniform_actual_lifted_chain_zero line 40

   Source documentation

   Source closed-picture conclusion with independent signed coefficients for EACH lift of every elementary cone triangle and frozen cell, and actual prefix-product and cone-route coordinates. The cutoff is selected before the realization, deck group, voltage and coefficients.

   theorem uniform_actual_lifted_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