Sylver coinage

DefinitionLegal moves in Sylver Coinage#✓fully proved

For a set \(M\) of natural numbers (a position of Sylver Coinage), the set \(L(M)\) of legal moves consists of the natural numbers that are not finite sums of elements of \(M\), repetitions allowed, i.e. the natural numbers outside the additive submonoid of \(\mathbb{N}\) generated by \(M\). Since \(0\) is the empty sum, every legal move is positive.

public def sylverLegalMoves (M : Set ℕ) : Set ℕ :=
  {q | q ∉ AddSubmonoid.closure M}

Sources

• Morgan Boyers, Natalie Burton, Jeff Rushall, James Warner and Tara Zurick, On Winning Strategies in Sylver Coinage When 4 Has Been Chosen, INTEGERS 24 (2024), Article G2, Section 1 (rules of Sylver Coinage, L(M)).

Used by 12

Used bySicherman's claim on replies to 4 and an odd number · Ends of a Sylver Coinage position · The largest legal move is an end · N-positions of Sylver Coinage · Even replies to 4 and an odd number at least 5 lose · Enders with largest legal move above 1 are N-positions · Opening with 2 loses · P-positions of Sylver Coinage · The position \(\{2, 3\}\) is a P-position · In an ender, every smaller move eliminates the largest legal move · A canonical position is the minimal generating set of its semigroup · Zero is never a legal move

InductiveP-positions of Sylver Coinage#✓fully proved

A set \(M\) of natural numbers is a P-position of Sylver Coinage when \(1 \notin M\) and, for every legal move \(q\) of \(M\), the position \(M \cup \{q\}\) is an N-position. P-positions and N-positions are defined together, as a mutual inductive definition. In particular a position whose only legal move is \(1\) is a P-position (the player to move must name \(1\) and loses).

public inductive IsSylverPPosition : Set ℕ → Prop
  | intro {M : Set ℕ} (one_notMem : 1 ∉ M)
      (forall_move : ∀ q ∈ sylverLegalMoves M, IsSylverNPosition (insert q M)) :
      IsSylverPPosition M

Sources

• Morgan Boyers, Natalie Burton, Jeff Rushall, James Warner and Tara Zurick, On Winning Strategies in Sylver Coinage When 4 Has Been Chosen, INTEGERS 24 (2024), Article G2, Section 1 (P- and N-positions).

Uses 1 · Used by 8

Statement usesLegal moves in Sylver Coinage

Used byOdd numbers above 3 have a unique odd partner after 4 · Sicherman's claim on replies to 4 and an odd number · Opening with 2 loses · Four-element P-positions containing 4 · Hutchings' theorem · The position \(\{2, 3\}\) is a P-position · Conway's bounds for 4-pairs · Unique odd partner after 4

InductiveN-positions of Sylver Coinage#✓fully proved

A position \(M\) of Sylver Coinage is an N-position (the player to move wins) when either \(1 \in M\), so that the previous player named \(1\) and lost, or some legal move \(q\) of \(M\) leads to a P-position \(M \cup \{q\}\). N-positions and P-positions are defined together inductively by these rules.

public inductive IsSylverNPosition : Set ℕ → Prop
  | one_mem {M : Set ℕ} (h : 1 ∈ M) : IsSylverNPosition M
  | move {M : Set ℕ} {q : ℕ} (hq : q ∈ sylverLegalMoves M)
      (h : IsSylverPPosition (insert q M)) : IsSylverNPosition M

Sources

• Morgan Boyers, Natalie Burton, Jeff Rushall, James Warner and Tara Zurick, On Winning Strategies in Sylver Coinage When 4 Has Been Chosen, INTEGERS 24 (2024), Article G2, Section 1 (P- and N-positions).

Uses 1 · Used by 7

Statement usesLegal moves in Sylver Coinage

Used byOdd numbers above 3 have a unique odd partner after 4 · Even replies to 4 and an odd number at least 5 lose · Enders with largest legal move above 1 are N-positions · Opening with 2 loses · The position \(\{2, 3\}\) is a P-position · Conway's bounds for 4-pairs · Unique odd partner after 4

TheoremZero is never a legal move#✓fully proved

For every set \(M\) of natural numbers, \(0\) is not a legal move of the Sylver Coinage position \(M\).

public theorem zero_notMem_sylverLegalMoves (M : Set ℕ) : 0 ∉ sylverLegalMoves M

Sources

• Morgan Boyers, Natalie Burton, Jeff Rushall, James Warner and Tara Zurick, On Winning Strategies in Sylver Coinage When 4 Has Been Chosen, INTEGERS 24 (2024), Article G2, Section 1 (rules of Sylver Coinage, L(M)).

Uses 1

Statement usesLegal moves in Sylver Coinage

TheoremThe position \(\{2, 3\}\) is a P-position#✓fully proved

In Sylver Coinage, the position \(\{2, 3\}\) is a P-position: its only legal move is \(1\).

public theorem isSylverPPosition_two_three : IsSylverPPosition {2, 3}

Sources

• Morgan Boyers, Natalie Burton, Jeff Rushall, James Warner and Tara Zurick, On Winning Strategies in Sylver Coinage When 4 Has Been Chosen, INTEGERS 24 (2024), Article G2, Section 1 (P- and N-positions).

Uses 3 · Used by 1

Statement usesP-positions of Sylver Coinage

Proof usesN-positions of Sylver Coinage · Legal moves in Sylver Coinage

Used byOpening with 2 loses

TheoremOpening with 2 loses#✓fully proved

The position \(\{2\}\) of Sylver Coinage is an N-position: the player to move wins by naming \(3\), which leaves the P-position \(\{2, 3\}\).

public theorem isSylverNPosition_two : IsSylverNPosition {2}

Sources

• Morgan Boyers, Natalie Burton, Jeff Rushall, James Warner and Tara Zurick, On Winning Strategies in Sylver Coinage When 4 Has Been Chosen, INTEGERS 24 (2024), Article G2, Section 1 (P- and N-positions).

Uses 4

Statement usesN-positions of Sylver Coinage

Proof usesP-positions of Sylver Coinage · The position \(\{2, 3\}\) is a P-position · Legal moves in Sylver Coinage

TheoremHutchings' theorem#●ready to prove

For every prime \(p > 3\), the position \(\{p\}\) of Sylver Coinage is a P-position: a first player who opens with \(p\) wins.

public theorem_wanted isSylverPPosition_prime_opening {p : ℕ} (hp : p.Prime) (h3 : 3 < p) :
    IsSylverPPosition {p}

Sources

• Morgan Boyers, Natalie Burton, Jeff Rushall, James Warner and Tara Zurick, On Winning Strategies in Sylver Coinage When 4 Has Been Chosen, INTEGERS 24 (2024), Article G2, Theorem 1.

Uses 1

Statement usesP-positions of Sylver Coinage

DefinitionEnds of a Sylver Coinage position#✓fully proved

Let \(M\) be a position of Sylver Coinage with set of legal moves \(L(M)\). A natural number \(x\) is an end of \(M\) if \(x \in L(M)\) and every \(y \in L(M)\) with \(y \ne x\) is still a legal move of the position \(M \cup \{x\}\); that is, naming \(x\) eliminates no other legal move.

public def IsSylverEnd (M : Set ℕ) (x : ℕ) : Prop :=
  x ∈ sylverLegalMoves M ∧ ∀ y ∈ sylverLegalMoves M, y ≠ x → y ∈ sylverLegalMoves (insert x M)

Sources

• Morgan Boyers, Natalie Burton, Jeff Rushall, James Warner and Tara Zurick, On Winning Strategies in Sylver Coinage When 4 Has Been Chosen, INTEGERS 24 (2024), Article G2, Definition 2, part 6 (ends and enders).

Uses 1 · Used by 3

Statement usesLegal moves in Sylver Coinage

Used byThe largest legal move is an end · Enders with largest legal move above 1 are N-positions · In an ender, every smaller move eliminates the largest legal move

TheoremThe largest legal move is an end#✓fully proved

Let \(M\) be a position of Sylver Coinage whose set of legal moves \(L(M)\) has a greatest element \(F\). Then \(F\) is an end of \(M\).

Every other legal move \(y\) is smaller than \(F\), so a way of writing \(y\) as a sum of elements of \(M \cup \{F\}\) cannot use \(F\); hence naming \(F\) eliminates no legal move other than \(F\) itself.

public theorem isSylverEnd_of_isGreatest {M : Set ℕ} {F : ℕ}
    (hF : IsGreatest (sylverLegalMoves M) F) : IsSylverEnd M F

Sources

• Morgan Boyers, Natalie Burton, Jeff Rushall, James Warner and Tara Zurick, On Winning Strategies in Sylver Coinage When 4 Has Been Chosen, INTEGERS 24 (2024), Article G2, Definition 2, part 6 (ends and enders).

Uses 2

Statement usesEnds of a Sylver Coinage position · Legal moves in Sylver Coinage

TheoremIn an ender, every smaller move eliminates the largest legal move#●ready to prove

Let \(M\) be a set of natural numbers whose set of legal moves \(L(M)\) has a greatest element \(F > 1\), and suppose that \(F\) is the only end of \(M\) (so \(M\) is an ender). Then for every legal move \(x\) of \(M\) with \(x < F\), the number \(F\) is not a legal move of \(M \cup \{x\}\).

public theorem_wanted sylverEnder_eliminates_largest_move {M : Set ℕ} {F : ℕ}
    (hF : IsGreatest (sylverLegalMoves M) F) (hender : ∀ x, IsSylverEnd M x → x = F)
    (hF1 : 1 < F) :
    ∀ x ∈ sylverLegalMoves M, x < F → F ∉ sylverLegalMoves (insert x M)

Sources

• Morgan Boyers, Natalie Burton, Jeff Rushall, James Warner and Tara Zurick, On Winning Strategies in Sylver Coinage When 4 Has Been Chosen, INTEGERS 24 (2024), Article G2, Proposition 1.

Uses 2

Statement usesEnds of a Sylver Coinage position · Legal moves in Sylver Coinage

TheoremEnders with largest legal move above 1 are N-positions#●ready to prove

Let \(M\) be a position of Sylver Coinage whose set of legal moves \(L(M)\) has a greatest element \(F\) with \(F > 1\). If every end of \(M\) equals \(F\) (that is, \(M\) is an ender), then \(M\) is an N-position.

public theorem_wanted isSylverNPosition_of_ender {M : Set ℕ} {F : ℕ}
    (hF : IsGreatest (sylverLegalMoves M) F) (hender : ∀ x, IsSylverEnd M x → x = F)
    (hF1 : 1 < F) :
    IsSylverNPosition M

Sources

• Morgan Boyers, Natalie Burton, Jeff Rushall, James Warner and Tara Zurick, On Winning Strategies in Sylver Coinage When 4 Has Been Chosen, INTEGERS 24 (2024), Article G2, Proposition 2.

Uses 3

Statement usesEnds of a Sylver Coinage position · N-positions of Sylver Coinage · Legal moves in Sylver Coinage

TheoremTwo-generated numerical semigroups are symmetric#●ready to prove

Let \(a\), \(b\) and \(F\) be natural numbers and let \(S = \langle a, b \rangle\) be the additive submonoid of \(\mathbb{N}\) generated by \(a\) and \(b\). If \(F \notin S\) and every natural number \(n > F\) lies in \(S\) (so \(F\) is the Frobenius number of \(S\)), then \(x \in S \iff F - x \notin S\) for every natural number \(x \le F\).

The hypotheses on \(F\) force \(\gcd(a, b) = 1\) and \(a, b \ge 2\), so these are exactly the numerical semigroups of embedding dimension \(2\) other than \(\mathbb{N}\).

public theorem_wanted numericalSemigroup_two_generated_symmetric {a b F : ℕ}
    (hF : F ∉ AddSubmonoid.closure ({a, b} : Set ℕ))
    (hF_max : ∀ n, F < n → n ∈ AddSubmonoid.closure ({a, b} : Set ℕ)) :
    ∀ x ≤ F, x ∈ AddSubmonoid.closure ({a, b} : Set ℕ) ↔
      F - x ∉ AddSubmonoid.closure ({a, b} : Set ℕ)

Sources

• Morgan Boyers, Natalie Burton, Jeff Rushall, James Warner and Tara Zurick, On Winning Strategies in Sylver Coinage When 4 Has Been Chosen, INTEGERS 24 (2024), Article G2, Proposition 3, part 1.

TheoremPseudo-symmetric semigroups of multiplicity 4 and embedding dimension 3#●ready to prove

Write \(\langle A \rangle\) for the additive submonoid of \(\mathbb{N}\) generated by a set \(A\). Let \(a\), \(b\) and \(F\) be natural numbers with \(4 < a < b\), \(a \notin \langle 4 \rangle\) and \(b \notin \langle 4, a \rangle\) (so \(\{4, a, b\}\) is the minimal generating set of \(S = \langle 4, a, b \rangle\)), and suppose that \(F \notin S\) and that every natural number \(n > F\) lies in \(S\). Then \(S\) is pseudo-symmetric, meaning that \(F\) is even and \(x \in S \iff F - x \notin S\) for every natural number \(x \le F\) with \(x \ne F / 2\), if and only if \(a\) is odd and \(b = a + 2\).

public theorem_wanted numericalSemigroup_four_pseudoSymmetric_iff {a b F : ℕ} (ha : 4 < a)
    (hab : a < b) (ha_min : a ∉ AddSubmonoid.closure ({4} : Set ℕ))
    (hb_min : b ∉ AddSubmonoid.closure ({4, a} : Set ℕ))
    (hF : F ∉ AddSubmonoid.closure ({4, a, b} : Set ℕ))
    (hF_max : ∀ n, F < n → n ∈ AddSubmonoid.closure ({4, a, b} : Set ℕ)) :
    (Even F ∧ ∀ x ≤ F, x ≠ F / 2 →
        (x ∈ AddSubmonoid.closure ({4, a, b} : Set ℕ) ↔
          F - x ∉ AddSubmonoid.closure ({4, a, b} : Set ℕ))) ↔
      Odd a ∧ b = a + 2

Sources

• Morgan Boyers, Natalie Burton, Jeff Rushall, James Warner and Tara Zurick, On Winning Strategies in Sylver Coinage When 4 Has Been Chosen, INTEGERS 24 (2024), Article G2, Proposition 3, part 2.

TheoremA canonical position is the minimal generating set of its semigroup#●ready to prove

Let \(M\) be a finite set of natural numbers whose set of legal moves \(L(M)\) is finite, and suppose that removing any element changes the legal moves: \(L(M \setminus \{a\}) \ne L(M)\) for every \(a \in M\). Let \(S\) be the additive submonoid of \(\mathbb{N}\) generated by \(M\). Then \(M\) is the set of nonzero elements \(s \in S\) such that whenever \(s = a + b\) with \(a, b \in S\), one of \(a\) and \(b\) is \(0\); that is, \(M\) is the minimal system of generators of \(S\).

public theorem_wanted sylverPosition_canonical_eq_minimalGenerators (M : Finset ℕ)
    (hcanon : ∀ a ∈ M, sylverLegalMoves ((M.erase a : Finset ℕ) : Set ℕ) ≠
      sylverLegalMoves (M : Set ℕ))
    (hfin : (sylverLegalMoves (M : Set ℕ)).Finite) :
    (M : Set ℕ) = {s | s ∈ AddSubmonoid.closure (M : Set ℕ) ∧ s ≠ 0 ∧
      ∀ a ∈ AddSubmonoid.closure (M : Set ℕ), ∀ b ∈ AddSubmonoid.closure (M : Set ℕ),
        a + b = s → a = 0 ∨ b = 0}

Sources

• Morgan Boyers, Natalie Burton, Jeff Rushall, James Warner and Tara Zurick, On Winning Strategies in Sylver Coinage When 4 Has Been Chosen, INTEGERS 24 (2024), Article G2, Proposition 4, part 1.

Uses 1

Statement usesLegal moves in Sylver Coinage

TheoremEven replies to 4 and an odd number at least 5 lose#●ready to prove

Let \(x \ge 5\) be an odd natural number. For every even legal move \(b\) of the position \(\{4, x\}\), the position \(\{4, x, b\}\) is an N-position.

public theorem_wanted isSylverNPosition_four_odd_even {x b : ℕ} (hx : 5 ≤ x) (hxo : Odd x)
    (hb : Even b) (hbL : b ∈ sylverLegalMoves {4, x}) :
    IsSylverNPosition {4, x, b}

Sources

• Morgan Boyers, Natalie Burton, Jeff Rushall, James Warner and Tara Zurick, On Winning Strategies in Sylver Coinage When 4 Has Been Chosen, INTEGERS 24 (2024), Article G2, Proposition 5.

Uses 2

Statement usesN-positions of Sylver Coinage · Legal moves in Sylver Coinage

TheoremSicherman's claim on replies to 4 and an odd number#●ready to prove

For every odd natural number \(x \ge 5\) there is exactly one legal move \(q\) of the position \(\{4, x\}\) such that \(\{4, x, q\}\) is a P-position, and every legal move \(q\) of \(\{4, x\}\) with \(\{4, x, q\}\) a P-position satisfies \(q \equiv x - 2 \pmod 4\).

public theorem_wanted existsUnique_sylver_response_four_odd {x : ℕ} (hx : 5 ≤ x) (hxo : Odd x) :
    (∃! q, q ∈ sylverLegalMoves {4, x} ∧ IsSylverPPosition {4, x, q}) ∧
      ∀ q ∈ sylverLegalMoves {4, x}, IsSylverPPosition {4, x, q} → q ≡ x - 2 [MOD 4]

Sources

• Morgan Boyers, Natalie Burton, Jeff Rushall, James Warner and Tara Zurick, On Winning Strategies in Sylver Coinage When 4 Has Been Chosen, INTEGERS 24 (2024), Article G2, Proposition 6.

Uses 2

Statement usesP-positions of Sylver Coinage · Legal moves in Sylver Coinage

TheoremOdd numbers above 3 have a unique odd partner after 4#●ready to prove

For every odd natural number \(q > 3\) there is exactly one odd natural number \(x\) such that \(\{4, x\}\) is an N-position and \(\{4, x, q\}\) is a P-position.

public theorem_wanted existsUnique_sylver_four_odd_partner {q : ℕ} (hq : 3 < q) (hqo : Odd q) :
    ∃! x, Odd x ∧ IsSylverNPosition {4, x} ∧ IsSylverPPosition {4, x, q}

Sources

• Morgan Boyers, Natalie Burton, Jeff Rushall, James Warner and Tara Zurick, On Winning Strategies in Sylver Coinage When 4 Has Been Chosen, INTEGERS 24 (2024), Article G2, Proposition 7.

Uses 2

Statement usesN-positions of Sylver Coinage · P-positions of Sylver Coinage

TheoremUnique odd partner after 4#●ready to prove

Let \(q > 3\) be an odd natural number. Then \(\{4, q\}\) is an N-position of Sylver Coinage, and there is a unique odd natural number \(x_q\) such that \(\{4, x_q\}\) is an N-position and \(\{4, q, x_q\}\) is a P-position.

When \(q < x_q\), the pair \((q, x_q)\) is a 4-pair.

public theorem_wanted sylver_four_pair_existsUnique {q : ℕ} (hq : 3 < q) (hqo : Odd q) :
    IsSylverNPosition {4, q} ∧
      ∃! x, Odd x ∧ IsSylverNPosition {4, x} ∧ IsSylverPPosition {4, q, x}

Sources

• Morgan Boyers, Natalie Burton, Jeff Rushall, James Warner and Tara Zurick, On Winning Strategies in Sylver Coinage When 4 Has Been Chosen, INTEGERS 24 (2024), Article G2, Corollary 1.

Uses 2

Statement usesN-positions of Sylver Coinage · P-positions of Sylver Coinage

TheoremConway's bounds for 4-pairs#●ready to prove

Let \(q\) and \(x\) be odd natural numbers with \(7 < q < x\) such that \(\{4, x\}\) is an N-position and \(\{4, x, q\}\) is a P-position of Sylver Coinage. Then \(2q < x < 3q\).

By the characterization of Proposition 7, such pairs \((q, x)\) are the 4-pairs of the source.

public theorem_wanted sylver_four_pair_bounds {q x : ℕ} (hqo : Odd q) (hxo : Odd x) (hq : 7 < q)
    (hqx : q < x) (hN : IsSylverNPosition {4, x}) (hP : IsSylverPPosition {4, x, q}) :
    2 * q < x ∧ x < 3 * q

Sources

• Morgan Boyers, Natalie Burton, Jeff Rushall, James Warner and Tara Zurick, On Winning Strategies in Sylver Coinage When 4 Has Been Chosen, INTEGERS 24 (2024), Article G2, Theorem 4.

Uses 2

Statement usesN-positions of Sylver Coinage · P-positions of Sylver Coinage

TheoremFour-element P-positions containing 4#●ready to prove

Let \(x > 1\) be a natural number. If \(x \equiv 1 \pmod 4\), then \(\{4, x, x + 2, 6\}\) is a P-position; if \(x \equiv 7 \pmod 8\), then \(\{4, x, x + 2, 10\}\) is a P-position; if \(x \equiv 5 \pmod 8\), then \(\{4, x, x + 6, 10\}\) is a P-position; and if \(x \equiv 1 \pmod 8\), then \(\{4, x, x + 6, 14\}\) is a P-position.

In each case \(x\) is odd. The analogous claim that \(\{4, x, x - 2, 14\}\) is a P-position for \(x \equiv 5 \pmod 8\) is false: for \(x = 13\), \(\{4, 11, 13, 14\}\) is an N-position, since naming \(5\) wins.

public theorem_wanted isSylverPPosition_four_odd_pair_even {x : ℕ} (hx : 1 < x) :
    (x % 4 = 1 → IsSylverPPosition {4, x, x + 2, 6}) ∧
      (x % 8 = 7 → IsSylverPPosition {4, x, x + 2, 10}) ∧
      (x % 8 = 5 → IsSylverPPosition {4, x, x + 6, 10}) ∧
      (x % 8 = 1 → IsSylverPPosition {4, x, x + 6, 14})

Sources

• Morgan Boyers, Natalie Burton, Jeff Rushall, James Warner and Tara Zurick, On Winning Strategies in Sylver Coinage When 4 Has Been Chosen, INTEGERS 24 (2024), Article G2, Proposition 8.

Uses 1

Statement usesP-positions of Sylver Coinage

8 fully proved12 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.