OAI/Combinatorics/HadwigerCounterexample/RefinedPinImages.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HadwigerCounterexample.front line 14
2. theorem OAI.HadwigerCounterexample.front_rank line 16
3. theorem OAI.HadwigerCounterexample.combined_rank line 27
4. abbrev OAI.HadwigerCounterexample.Signal line 31
5. def OAI.HadwigerCounterexample.readPin line 33
6. abbrev OAI.HadwigerCounterexample.EffSeq line 36
7. def OAI.HadwigerCounterexample.entrySeq line 38
8. abbrev OAI.HadwigerCounterexample.Story line 42
9. instance OAI.HadwigerCounterexample.fintypeStory line 45
10. def OAI.HadwigerCounterexample.story line 56
11. def OAI.HadwigerCounterexample.specialLeaf line 59
12. theorem OAI.HadwigerCounterexample.storyOk line 65
13. theorem OAI.HadwigerCounterexample.story_size line 109
14. theorem OAI.HadwigerCounterexample.plan_inc_eff line 137
15. theorem OAI.HadwigerCounterexample.front_table line 146

    Source documentation

    Old contractions on admissible tables evaluate correctly when the enlarged leaf has pinned the entire front.

    theorem front_table (x y : UnitType p n N)
        {a b : Pin p n N} (s : Plan p n)
        (hf : front s≤a.sp)
        {M : Cross p n} (hx : a.agree x) (hB : tableFlag b a (reciprocal p M) y)
        (i j : Bool) (w : Profile p n) (h : w∈effective s i) :
        contract p (actual p x y) i j w=contract p M i j w := by
    …

    Mentions: OAI.HadwigerCounterexample.UnitType, OAI.HadwigerCounterexample.Pin, OAI.HadwigerCounterexample.Plan, OAI.HadwigerCounterexample.front, OAI.HadwigerCounterexample.Cross, OAI.HadwigerCounterexample.tableFlag, OAI.HadwigerCounterexample.reciprocal, OAI.HadwigerCounterexample.Profile, OAI.HadwigerCounterexample.effective, OAI.HadwigerCounterexample.contract, OAI.HadwigerCounterexample.actual

16. theorem OAI.HadwigerCounterexample.weave line 174
17. theorem OAI.HadwigerCounterexample.phase_fixed line 221