RelativeGlobalStep.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.partition_face_bound line 31

Source documentation

The protected exterior contributes at most the literal outside word length. The cut term is the number of unordered genuine interior contacts, not darts.

theorem partition_face_bound {M : ℕ} {α β δ : ℝ} (ha : 0 ≤ α)
    (hgood : Occurrences.GoodUpTo M α β δ (Sum.elim w d))
    (hs : P.Simple) (hm : P.FrozenMapped (frozen n w d ell hell word c hc f))
    (hred : P.FullyReduced) (hrad : P.RadialInjective (isApex n w)) (hb : P.NoBigon)
    (hM : ∀ i, 8 * Fintype.card {F : InteriorFace n w d ell hell word c hc f P // part F.val = i} ≤ M) :
    defectConstant α β δ * Fintype.card (InteriorFace n w d ell hell word c hc f P) ≤
      (ell : ℝ) + 2 * Fintype.card (RelativeCutContact P.pairing
        (Interior n w d ell hell word c hc f P ∘ P.faceClass) (part ∘ P.faceClass)) := by
…

Mentions: OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.frozen, OAI.HyperbolicObstruction.ConeSkeleton.isApex, OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.InteriorFace, OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.Interior

theorem OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.partition_filling_bound line 48

Source documentation

Actual relator filling with its exact fragment-cut cost. This is valid for every small partition, without assuming that a low-cut separator exists.

theorem partition_filling_bound {M : ℕ} {α β δ : ℝ} (ha : 0 ≤ α)
    (hk : 0 ≤ defectConstant α β δ)
    (hgood : Occurrences.GoodUpTo M α β δ (Sum.elim w d))
    (hs : P.Simple) (hm : P.FrozenMapped (frozen n w d ell hell word c hc f))
    (hred : P.FullyReduced) (hrad : P.RadialInjective (isApex n w)) (hb : P.NoBigon)
    (hM : ∀ i, 8 * Fintype.card {F : InteriorFace n w d ell hell word c hc f P // part F.val = i} ≤ M) :
    ∃ a, Homotopy (SimpleWordRelator n w d) (List.ofFn word) [] a ∧
      defectConstant α β δ * a ≤ 30 * ((ell : ℝ) +
        2 * Fintype.card (RelativeCutContact P.pairing
          (Interior n w d ell hell word c hc f P ∘ P.faceClass) (part ∘ P.faceClass))) := by
…