OAI/Geometry/HyperbolicGroups/LiftedClosedPicture.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HyperbolicObstruction.ConeSkeleton.indexingTarget line 19

   Source documentation

   Zero coefficients specify the base indexing target only: the cover has arbitrary independent weights for each lifted step.

   def indexingTarget (n : ℕ) (w : TableModel.Entry (A := Alphabet n) rowSupport → Bool)
   …

   Mentions: OAI.HyperbolicObstruction.TableModel.Entry

2. def OAI.HyperbolicObstruction.ConeSkeleton.indexingFrozenTarget line 23
3. theorem OAI.HyperbolicObstruction.ConeSkeleton.uniform_lifted_picture_chain_zero line 30

   Source documentation

   Normal-form vanishing holds in every regular voltage cover, with each signed lifted cell retained separately. This is stronger than vanishing of the projected base-cell chain.

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