Documentation

LeanPool.MisereGames.Misere.Blocking

Misere combinatorial games.

source
@[irreducible]
def MisereGames.Form.IsBlockedEnd {G : Type (u + 1)} [Form G] (p : Player) (g : G) :
Prop

A blocked end for player p: g is a p-end, and for every opponent move gr, either gr is again a p blocked end, or else p has a move from gr to a p blocked end. This is weaker than IsDeadEnd: every p dead end is a p blocked end (isBlockedEnd_of_isDeadEnd), but not the other way around.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem MisereGames.Form.isBlockedEnd_def {G : Type (u + 1)} [Form G] (p : Player) (g : G) :
    IsBlockedEnd p g ↔ IsEnd p g ∧ ∀ gr ∈ moves (-p) g, IsBlockedEnd p gr ∨ ∃ (grl : G) (_ : grl ∈ moves p gr), IsBlockedEnd p grl
    source
    theorem MisereGames.Form.isEnd_of_isBlockedEnd {G : Type (u + 1)} [Form G] {g : G} {p : Player} (h1 : IsBlockedEnd p g) :
    IsEnd p g
    source
    theorem MisereGames.Form.IsBlockedEnd.hereditary_def {G : Type (u + 1)} [Form G] {g : G} {p : Player} (h1 : IsBlockedEnd p g) (gr : G) :
    gr ∈ moves (-p) g → IsBlockedEnd p gr ∨ ∃ (grl : G) (_ : grl ∈ moves p gr), IsBlockedEnd p grl
    source
    @[simp]
    theorem MisereGames.Form.not_mem_moves_of_isBlockedEnd {G : Type (u + 1)} [Form G] {g gp : G} {p : Player} (h1 : IsBlockedEnd p g) :
    gp ∉ moves p g
    source
    theorem MisereGames.Form.isBlockedEnd_of_isDeadEnd {G : Type (u + 1)} [Form G] {g : G} {p : Player} (h1 : IsDeadEnd p g) :
    IsBlockedEnd p g

    A dead end is a blocked end.

    source
    theorem MisereGames.Form.IsBlockedEnd.add {G : Type (u + 1)} [Form G] {g h : G} {p : Player} (h1 : IsBlockedEnd p g) (h2 : IsBlockedEnd p h) :
    IsBlockedEnd p (g + h)
    source
    @[simp]
    theorem MisereGames.Form.IsBlockedEnd.neg_iff {G : Type (u + 1)} [Form G] {g : G} {p : Player} :
    IsBlockedEnd p (-g) ↔ IsBlockedEnd (-p) g
    source
    theorem MisereGames.Form.isBlockedEnd_zero {G : Type (u + 1)} [Form G] {p : Player} :
    IsBlockedEnd p 0
    source
    theorem MisereGames.Form.isBlockedEnd_right_natCast {G : Type (u + 1)} [Form G] (n : ℕ) :
    IsBlockedEnd Player.right ↑n
    source
    theorem MisereGames.Form.isBlockedEnd_right_nonneg_intCast {G : Type (u + 1)} [Form G] (k : ℤ) (h1 : k ≥ 0) :
    IsBlockedEnd Player.right ↑k
    source
    theorem MisereGames.Form.isBlockedEnd_left_nonpos_intCast {G : Type (u + 1)} [Form G] (k : ℤ) (h1 : k ≤ 0) :
    IsBlockedEnd Player.left ↑k
    source
    @[irreducible]
    def MisereGames.Form.IsBlocking {G : Type (u + 1)} [Form G] (g : G) :
    Prop

    A game is blocking if every end is a blocked end, hereditarily.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem MisereGames.Form.isBlockedEnd_of_isBlocking {G : Type (u + 1)} [Form G] {g : G} {p : Player} (h1 : IsBlocking g) (h2 : IsEnd p g) :
      IsBlockedEnd p g
      source
      theorem MisereGames.Form.isBlocking_of_mem_moves {G : Type (u + 1)} [Form G] {g h : G} {p : Player} (h1 : IsBlocking g) (h2 : h ∈ moves p g) :
      IsBlocking h
      source
      theorem MisereGames.Form.isBlocking_of_isOption {G : Type (u + 1)} [Form G] {g g' : G} (h1 : IsBlocking g) (h2 : IsOption g' g) :
      IsBlocking g'
      source
      theorem MisereGames.Form.isBlocking_of_isDeadEnding {G : Type (u + 1)} [Form G] {g : G} (h1 : IsDeadEnding g) :
      IsBlocking g

      Every dead-ending game is blocking.

      source
      @[simp]
      theorem MisereGames.Form.IsBlocking.add {G : Type (u + 1)} [Form G] {g h : G} (h1 : IsBlocking g) (h2 : IsBlocking h) :
      IsBlocking (g + h)
      source
      instance MisereGames.Form.instClosedUnderAddIsBlocking {G : Type (u + 1)} [Form G] :
      ClosedUnderAdd IsBlocking
      source
      instance MisereGames.Form.instClosedUnderNegIsBlocking {G : Type (u + 1)} [Form G] :
      ClosedUnderNeg IsBlocking
      source
      @[simp]
      theorem MisereGames.Form.isBlocking_zero {G : Type (u + 1)} [Form G] :
      IsBlocking 0
      source
      @[simp]
      theorem MisereGames.Form.isBlocking_natCast {G : Type (u + 1)} [Form G] (n : ℕ) :
      IsBlocking ↑n
      source
      @[simp]
      theorem MisereGames.Form.isBlocking_intCast {G : Type (u + 1)} [Form G] (k : ℤ) :
      IsBlocking ↑k
      source
      @[simp]
      theorem MisereGames.Form.isBlocking_one {G : Type (u + 1)} [Form G] :
      IsBlocking 1
      source
      structure MisereGames.Form.ShortBlocking {G : Type (u + 1)} [Form G] (g : G) :
      Prop

      The short blocking universe.

      Instances For
        source
        instance MisereGames.Form.instHereditaryShortBlocking {G : Type (u + 1)} [Form G] :
        Hereditary ShortBlocking
        source
        instance MisereGames.Form.instClosedUnderNegShortBlocking {G : Type (u + 1)} [Form G] :
        ClosedUnderNeg ShortBlocking
        source
        instance MisereGames.Form.instClosedUnderAddShortBlocking {G : Type (u + 1)} [Form G] :
        ClosedUnderAdd ShortBlocking
        source
        instance MisereGames.Form.instClosedUnderDicoticIsShortShortBlocking {G : Type (u + 1)} [Form G] :
        ClosedUnderDicotic IsShort ShortBlocking
        source
        instance MisereGames.Form.instShortUniverseShortBlocking {G : Type (u + 1)} [Form G] :
        ShortUniverse ShortBlocking
        source
        instance MisereGames.Form.instHasNatShortBlocking {G : Type (u + 1)} [Form G] :
        HasNat ShortBlocking
        source
        instance MisereGames.Form.instClosedUnderAddNatShortBlocking {G : Type (u + 1)} [Form G] :
        ClosedUnderAddNat ShortBlocking
        source
        instance MisereGames.Form.instHasIntShortBlocking {G : Type (u + 1)} [Form G] :
        HasInt ShortBlocking
        source
        instance MisereGames.GameForm.instIntegerInvertibleShortBlocking :
        IntegerInvertible Form.ShortBlocking

        This is [Davies, Miller, Milley (Lemma 4.5 on p. 26)][davies:SumsPFreeForms:2025]