OAI/Combinatorics/HadwigerCounterexample/ResidualCutPairs.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HadwigerCounterexample.Volley.CleanRay line 14
2. theorem OAI.HadwigerCounterexample.Volley.clean_apply line 19
3. theorem OAI.HadwigerCounterexample.Volley.clean_zero line 29
4. theorem OAI.HadwigerCounterexample.Volley.clean_proj line 35

   Source documentation

   Key coefficients cannot contribute to a short nonattack primal combination even if only the primal projection is specified.

   private theorem clean_proj {w : I → Bool} {a : Plan p n} (t : Tagging p I) {R q : ℕ}
       (hb : v.bounded w) (hv : v.avoids a q) (hr : R+14 ≤ q)
       (x : Ray p n) (z : Place p) (i : Bool) (hx : v.CleanRay i R x)
       (b : Vec (visits p t z.1)) (he : x-(IP p n i)ᵀ *ᵥ (v.keyM t z.1 *ᵥ b) ∈ sPin a z i) :
       ∀ j∈v.visitH t i z.1,b j = 0 := by
   …

   Mentions: OAI.HadwigerCounterexample.Plan, OAI.HadwigerCounterexample.Tagging, OAI.HadwigerCounterexample.Ray, OAI.HadwigerCounterexample.Place, OAI.HadwigerCounterexample.Vec, OAI.HadwigerCounterexample.Volley.visits, OAI.HadwigerCounterexample.IP, OAI.HadwigerCounterexample.sPin

5. theorem OAI.HadwigerCounterexample.Volley.clean_sPin line 71
6. theorem OAI.HadwigerCounterexample.Volley.clean_Pin line 85
7. theorem OAI.HadwigerCounterexample.orth_delta_probe line 116
8. theorem OAI.HadwigerCounterexample.Volley.clean_effective line 169