OAI/Geometry/HyperbolicGroups/FanApex.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.HyperbolicObstruction.FanLink.Mark line 15
  2. def OAI.HyperbolicObstruction.FanLink.Mark.plain line 21
  3. def OAI.HyperbolicObstruction.FanLink.Mark.color line 26
  4. lemma OAI.HyperbolicObstruction.FanLink.Mark.color_active line 31
  5. lemma OAI.HyperbolicObstruction.FanLink.Mark.color_f line 37
  6. lemma OAI.HyperbolicObstruction.FanLink.Mark.color_turn line 43
  7. structure OAI.HyperbolicObstruction.FanLink.FanData line 55

    Source documentation

    Combinatorial data at ONE fan occurrence in a fragment of a normalized picture. S indexes all selected top faces whose occurrence has this fan slot, including top faces that do not actually turn at this fan. The injectivity condition is that a simple macro polygon turns at a fan at most once.

    structure FanData (r S o : ℕ) where
…
  8. def OAI.HyperbolicObstruction.FanLink.FanData.state line 76
  9. def OAI.HyperbolicObstruction.FanLink.FanData.colored line 77
  10. def OAI.HyperbolicObstruction.FanLink.FanData.triangles line 79
  11. def OAI.HyperbolicObstruction.FanLink.FanData.turns line 80
  12. def OAI.HyperbolicObstruction.FanLink.FanData.payments line 81
  13. def OAI.HyperbolicObstruction.FanLink.FanData.boundary line 82
  14. def OAI.HyperbolicObstruction.FanLink.FanData.isPartial line 83
  15. instance OAI.HyperbolicObstruction.FanLink.FanData.partialDecidable line 84
  16. def OAI.HyperbolicObstruction.FanLink.FanData.partialCount line 85
  17. def OAI.HyperbolicObstruction.FanLink.FanData.multiplicity line 87
  18. def OAI.HyperbolicObstruction.FanLink.FanData.maxMultiplicity line 88
  19. def OAI.HyperbolicObstruction.FanLink.FanData.weight line 89
  20. lemma OAI.HyperbolicObstruction.FanLink.FanData.count_le line 91
  21. lemma OAI.HyperbolicObstruction.FanLink.FanData.turns_le line 123
  22. lemma OAI.HyperbolicObstruction.FanLink.FanData.color_counts line 133
  23. lemma OAI.HyperbolicObstruction.FanLink.FanData.other_count_le line 143
  24. lemma OAI.HyperbolicObstruction.FanLink.FanData.multiplicity_le line 157
  25. lemma OAI.HyperbolicObstruction.FanLink.FanData.color_Q line 161
  26. lemma OAI.HyperbolicObstruction.FanLink.FanData.color_P line 165
  27. lemma OAI.HyperbolicObstruction.FanLink.FanData.color_B line 170
  28. lemma OAI.HyperbolicObstruction.FanLink.FanData.state_full line 177
  29. lemma OAI.HyperbolicObstruction.FanLink.FanData.boundary_le line 182
  30. lemma OAI.HyperbolicObstruction.FanLink.FanData.partial_le_boundary line 188
  31. lemma OAI.HyperbolicObstruction.FanLink.FanData.one_instance_bound line 201
  32. lemma OAI.HyperbolicObstruction.FanLink.FanData.r_case_bound line 222
  33. lemma OAI.HyperbolicObstruction.FanLink.FanData.dominant_bound line 232
  34. theorem OAI.HyperbolicObstruction.FanLink.FanData.apex_bound line 261

    Source documentation

    Full source per-fan apex inequality, including omission of the fan by some selected top faces and shared dominant occurrences. It follows from the actual cyclic-link/side conditions and the simple-polygon injection above.

    theorem apex_bound :
    (L.turns:ℝ) + 2 * ((L.weight:ℝ) - S) ≤
      ((L.triangles:ℝ) + L.payments) / 2 + 2 * L.partialCount := by
…
  35. lemma OAI.HyperbolicObstruction.FanLink.FanData.triangles_le line 294