OAI/Geometry/HyperbolicGroups/RelativeContact.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.selectedDart line 24
  2. def OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.rawDart line 25
  3. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.rawDart_pair line 26
  4. abbrev OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.ActualContact line 32
  5. abbrev OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.ActualRawSide line 33
  6. abbrev OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.ActualRawBoundary line 34
  7. def OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.InteriorSelection line 37

    Source documentation

    Only genuine disk-interior cells belong to a fragment.

    def InteriorSelection : Prop := ∀ F : P.Face, select F = true → ∃ k, P.faceKind F = .inl k
…
  8. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.selected_interior line 42
  9. def OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.selectedStep line 50
  10. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.selectedStep_index line 52
  11. def OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.selectedPosition line 56
  12. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.selectedPosition_eq line 58
  13. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.selectedPosition_value line 64
  14. def OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.contactLeft line 74
  15. def OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.contactRight line 76
  16. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.actual_contact_ne line 80
  17. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.actual_contact_value line 91
  18. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.actual_contact_capacity line 105
  19. theorem OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.actual_contact_bound line 143

    Source documentation

    The contact-counting estimate for the literal normalized mixed picture. Only the stochastic rank event and layer-size bounds remain here; no side capacity, radial accounting, or label-incidence premise is assumed.

    theorem actual_contact_bound {M : ℕ} {α β δ : ℝ}
    (hgood : Occurrences.GoodUpTo M α β δ (Sum.elim w d)) (hb : P.NoBigon)
    (ht : ∀ j, Fintype.card ((actualWeights n w d ell hell word c hc f P select hs hm hred hrad).TopAt j) ≤ M)
    (hf : ∀ j, Fintype.card ((actualWeights n w d ell hell word c hc f P select hs hm hred hrad).FanAt j) ≤ M)
    (hq : ∀ j, Fintype.card ((actualWeights n w d ell hell word c hc f P select hs hm hred hrad).SquareAt j) ≤ M)
    (hv : ∀ j, Fintype.card ((actualWeights n w d ell hell word c hc f P select hs hm hred hrad).SixAt j) ≤ M) :
    let W := actualWeights n w d ell hell word c hc f P select hs hm hred hrad
…

    Mentions: OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.actualWeights

  20. lemma OAI.HyperbolicObstruction.ConeSkeleton.RelDisk.actual_boundary_contacts_eq line 176