OAI/Combinatorics/HadwigerCounterexample/KeyDirections.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

Key Directions

  1. structure OAI.HadwigerCounterexample.Volley line 19

    Source documentation

    One side of the lists, with actual point inputs, indexed by the simultaneous (both units') list positions. Tags passed separately because matched across the two sides.

    structure Volley (p : Shape) (n : ℕ) (I : Type) where
…

    Mentions: OAI.HadwigerCounterexample.Shape

  2. abbrev OAI.HadwigerCounterexample.Tagging line 24
  3. abbrev OAI.HadwigerCounterexample.AtomKey line 25
  4. def OAI.HadwigerCounterexample.keyOne line 27
  5. abbrev OAI.HadwigerCounterexample.Keys line 31
  6. def OAI.HadwigerCounterexample.Volley.atomAt line 35
  7. def OAI.HadwigerCounterexample.Volley.rayAt line 36
  8. def OAI.HadwigerCounterexample.Volley.rayLoc line 37
  9. def OAI.HadwigerCounterexample.Volley.shoots line 40

    Source documentation

    List from endpoint j to endpoint k of the other unit.

    def shoots (w : I → Bool) (j k : Bool) := univ.filter (fun i => v.obj i=j ∧ w i=k)
  10. def OAI.HadwigerCounterexample.Volley.here line 41
  11. def OAI.HadwigerCounterexample.Volley.sumAt line 42
  12. def OAI.HadwigerCounterexample.Volley.keys line 45
  13. abbrev OAI.HadwigerCounterexample.Volley.visits line 48
  14. instance OAI.HadwigerCounterexample.Volley.(instance at line 49) line 49
  15. def OAI.HadwigerCounterexample.Volley.keyM line 51
  16. def OAI.HadwigerCounterexample.Volley.keyPlan line 53
  17. theorem OAI.HadwigerCounterexample.Volley.keys_loc line 56
  18. theorem OAI.HadwigerCounterexample.Volley.atom_share line 61
  19. def OAI.HadwigerCounterexample.Volley.avoids line 75

    Source documentation

    At each endpoint at most q calls, with distinct labels and no label interacting with a short vector in the pinned projections.

    def avoids (a : Plan p n) (q : ℕ) :=
…

    Mentions: OAI.HadwigerCounterexample.Plan

  20. theorem OAI.HadwigerCounterexample.point_comb line 85

    Source documentation

    Any combination of points with distinct labels has a short-ray representation on the image label set.

    theorem point_comb {p : Shape} {A : Type*} (J : Finset A) (s : A → Label p.b)
    (z : A → Base p.g n) (a : A → F) (hs : Set.InjOn s (J : Set A)) :
    ∃ u : LabVals p n, (∀ i∈J,u (s i)=a i • baseV (z i)) ∧
      ∑ i∈J,a i • point p (s i) (z i)=labcomb p n (J.image s) u := by
…

    Mentions: OAI.HadwigerCounterexample.Shape, OAI.HadwigerCounterexample.Label, OAI.HadwigerCounterexample.Base, OAI.HadwigerCounterexample.F, OAI.HadwigerCounterexample.LabVals, OAI.HadwigerCounterexample.baseV, OAI.HadwigerCounterexample.point, OAI.HadwigerCounterexample.labcomb

  21. theorem OAI.HadwigerCounterexample.Volley.key_miss line 105
  22. theorem OAI.HadwigerCounterexample.Volley.key_independent line 149