ClosedPicture.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.HyperbolicObstruction.ConeSkeleton.all_area line 22
lemma OAI.HyperbolicObstruction.ConeSkeleton.area_le_darts line 29
lemma OAI.HyperbolicObstruction.ConeSkeleton.all_boundary_zero line 35

theorem OAI.HyperbolicObstruction.ConeSkeleton.small_normal_empty line 44

Source documentation

A bounded closed normal picture has no faces. This uses the genuine rank event for its size, not an abstract incidence or link assumption.

theorem small_normal_empty {M : ℕ} {α β δ : ℝ}
    (ha : 0 < α) (hbeta : 7*α < β) (hd : 0 < δ)
    (hgood : Occurrences.GoodUpTo M α β δ (Sum.elim w d))
    (hs : P.Simple) (hm : P.FrozenMapped (walkFrozenTarget n w d c hc f))
    (hred : P.FullyReduced) (hrad : P.RadialInjective (isApex n w)) (hb : P.NoBigon)
    (hM : 8 * actualArea n w d c hc f P (fun _ => true) ≤ M) : IsEmpty P.Dart := by
…

Mentions: OAI.HyperbolicObstruction.ConeSkeleton.walkFrozenTarget, OAI.HyperbolicObstruction.ConeSkeleton.isApex, OAI.HyperbolicObstruction.ConeSkeleton.actualArea

theorem OAI.HyperbolicObstruction.ConeSkeleton.small_closed_chain_zero line 64
Source documentation
Bounded spherical-chain vanishing: the checked finite surgeries produce normal form and preserve the literal chain. No topological realization is asserted by this combinatorial statement.
```
theorem small_closed_chain_zero {M : ℕ} {α β δ : ℝ}
    (ha : 0 < α) (hbeta : 7*α < β) (hd : 0 < δ)
    (hgood : Occurrences.GoodUpTo M α β δ (Sum.elim w d))
    (hm : P.FrozenMapped (walkFrozenTarget n w d c hc f))
    (hM : 8 * Fintype.card P.Dart ≤ M) : P.chain = 0 := by
…
```
Mentions: OAI.HyperbolicObstruction.ConeSkeleton.walkFrozenTarget