OAI/Probability/CriticalZ3/SeedTrials.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CriticalZ3.Box.bits_mono line 13
  2. theorem OAI.CriticalZ3.Box.disjoint_bits line 20
  3. theorem OAI.CriticalZ3.Box.center_mem_cube line 29
  4. theorem OAI.CriticalZ3.Box.cube_bits_card line 32
  5. def OAI.CriticalZ3.Box.relayCenter line 38
  6. def OAI.CriticalZ3.Box.seedBox line 39
  7. def OAI.CriticalZ3.Box.successBits line 41
  8. def OAI.CriticalZ3.Box.seedCard line 45
  9. def OAI.CriticalZ3.Box.successCard line 46
  10. theorem OAI.CriticalZ3.Box.crossing_not_internal line 50
  11. theorem OAI.CriticalZ3.Box.crossing_injective line 59
  12. theorem OAI.CriticalZ3.Box.seedBox_contained line 73
  13. theorem OAI.CriticalZ3.Box.successBits_card line 77
  14. theorem OAI.CriticalZ3.Box.successBits_disjoint line 88
  15. theorem OAI.CriticalZ3.LatticeGraph.successBits_disjoint_outside line 117
  16. theorem OAI.CriticalZ3.LatticeGraph.ContainsBox.mono line 127
  17. theorem OAI.CriticalZ3.LatticeGraph.success_reaches_center line 132

    Source documentation

    A successful exterior trial supplies a path for both bond and site percolation.

    theorem success_reaches_center (m : Model) (C : Box) (r : ℕ)
    (hw : ∀ i, C.lower i+r ≤ C.upper i-r) (hC : G.ContainsBox (C.expand 1))
    {ω : m.Config} {o y : G.Node} (hy : y.1 ∈ G.entrants m C ω o)
    (hs : ∀ e ∈ C.successBits r m y.1, ω e = true) :
    ∃ v : G.Node, v.1 = C.relayCenter r y.1 ∧ G.Conn m ω o v := by
…

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