Lax Lean Archive

Basic properties of Sprague–Grundy values

Lax689614.GrundyProperties · concepts/Lax689614/GrundyProperties.lean · lax-689614

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    Observation 2 and Lemma 3: every smaller value is reachable, the current value is not reachable, and a position is losing exactly when its value is zero. Lemma 4: on a disjoint union, the value is the bitwise exclusive-or of the component values. The binary formula gives the finite-family formula by iteration.

    Concept map
    3 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 4 statements. Each proof establishes one of them relative to its assumptions.

    1 disjoint_union proven

    2 losing_iff_zero proven

    3 smaller_reachable proven

    4 value_not_reachable proven

    Lean source view on GitHub

    1import Lax689614.Grundy
    2import Mathlib.Data.Nat.Bitwise
    3
    4/-!
    5---
    6title: Basic properties of Sprague–Grundy values
    7type: theorem
    8---
    9Observation 2 and Lemma 3: every smaller value is reachable, the current
    10value is not reachable, and a position is losing exactly when its value is
    11zero. Lemma 4: on a disjoint union, the value is the bitwise exclusive-or
    12of the component values. The binary formula gives the finite-family formula
    13by iteration.
    14-/
    15
    16namespace Lax689614.GrundyProperties
    17
    18open ArcKayles Grundy
    19
    20axiom smaller_reachable {V : Type} [DecidableEq V] (G : SimpleGraph V)
    21 (S : Finset V) (i : ℕ) (h : i < value G S) :
    22 ∃ u ∈ S, ∃ v ∈ S, G.Adj u v ∧ value G (remove S u v) = i
    23
    24axiom value_not_reachable {V : Type} [DecidableEq V] (G : SimpleGraph V)
    25 (S : Finset V) (u v : V) (hu : u ∈ S) (hv : v ∈ S) (he : G.Adj u v) :
    26 value G (remove S u v) ≠ value G S
    27
    28axiom losing_iff_zero {V : Type} [DecidableEq V] (G : SimpleGraph V) (S : Finset V) :
    29 ¬ Winning G S ↔ value G S = 0
    30
    31axiom disjoint_union {V : Type} [DecidableEq V] (G : SimpleGraph V)
    32 (S T : Finset V) (hd : Disjoint S T)
    33 (hn : ∀ u ∈ S, ∀ v ∈ T, ¬ G.Adj u v) :
    34 value G (S ∪ T) = Nat.xor (value G S) (value G T)
    35
    36end Lax689614.GrundyProperties
    37
    Show ProofShow ProofShow ProofShow Proof
    Builds on
    Used by

    none

    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…