OAI/Probability/CriticalZ3/EntryLayers.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CriticalZ3.step_ge line 12
  2. theorem OAI.CriticalZ3.step_direction_injective line 15
  3. theorem OAI.CriticalZ3.step_no_reverse line 22
  4. theorem OAI.CriticalZ3.incidence_unique line 29
  5. def OAI.CriticalZ3.neighborBond line 45
  6. theorem OAI.CriticalZ3.neighborBond_incidence line 48
  7. theorem OAI.CriticalZ3.neighborBond_eq line 53
  8. def OAI.CriticalZ3.Box.Exterior line 58
  9. def OAI.CriticalZ3.Box.entry line 61
  10. theorem OAI.CriticalZ3.Box.entry_spec line 64
  11. theorem OAI.CriticalZ3.Box.entry_eq line 69
  12. def OAI.CriticalZ3.Box.entryBit line 74
  13. theorem OAI.CriticalZ3.Box.exterior_expand line 78
  14. theorem OAI.CriticalZ3.Box.entryBit_internal line 86
  15. def OAI.CriticalZ3.LatticeGraph.OutsideAdj line 99
  16. def OAI.CriticalZ3.LatticeGraph.OutsideReach line 102
  17. def OAI.CriticalZ3.LatticeGraph.entrants line 105
  18. theorem OAI.CriticalZ3.LatticeGraph.mem_entrants line 109
  19. theorem OAI.CriticalZ3.LatticeGraph.outsideReach_conn line 114
  20. theorem OAI.CriticalZ3.LatticeGraph.first_entry line 118
  21. theorem OAI.CriticalZ3.LatticeGraph.meets_entrants_nonempty line 138
  22. theorem OAI.CriticalZ3.LatticeGraph.entryBit_open line 145
  23. def OAI.CriticalZ3.LatticeGraph.entryBits line 154
  24. def OAI.CriticalZ3.LatticeGraph.Blocked line 157
  25. theorem OAI.CriticalZ3.LatticeGraph.entryBits_card line 160
  26. theorem OAI.CriticalZ3.LatticeGraph.blocked_not_meets line 163
  27. theorem OAI.CriticalZ3.LatticeGraph.blocked_earlier_entrants line 175

    Source documentation

    The shell blocking events are disjoint for the actual induced-outside paths. This is the pathwise argument, not a probabilistic assumption.

    theorem blocked_earlier_entrants (m : Model) {B : Box} {i j : ℕ} (hij : i < j)
    {ω : m.Config} {o : G.Node} (ho : ¬(B.expand j).Contains o.1)
    (hb : G.Blocked m (B.expand j) ω o) : G.entrants m (B.expand i) ω o = ∅ := by
…

    Mentions: OAI.CriticalZ3.Model, OAI.CriticalZ3.Box

  28. def OAI.CriticalZ3.LatticeGraph.outsideBits line 195
  29. theorem OAI.CriticalZ3.LatticeGraph.outsideAdj_determined line 199
  30. theorem OAI.CriticalZ3.LatticeGraph.outsideReach_determined line 219
  31. theorem OAI.CriticalZ3.LatticeGraph.entrants_determined line 233
  32. theorem OAI.CriticalZ3.LatticeGraph.entryBits_determined line 239
  33. theorem OAI.CriticalZ3.LatticeGraph.outsideBits_disjoint_inside line 244
  34. theorem OAI.CriticalZ3.LatticeGraph.entryBit_not_outside line 252
  35. theorem OAI.CriticalZ3.LatticeGraph.entryBits_disjoint_outside line 264