Compfiles: Catalog Of Math Problems Formalized In Lean

Usa1994P2

module

public import Mathlib.Algebra.Field.ZMod
public import Mathlib.Tactic.Ring

public section


/-!
# USA Mathematical Olympiad 1994, Problem 2

The sequence a₁, a₂, ... , a₉₉ has a₁ = a₃ = a₅ = ... = a₉₇ = 1,
a₂ = a₄ = a₆ = ... = a₉₈ = 2, and a₉₉ = 3. We interpret subscripts greater
than 99 by subtracting 99, so that a₁₀₀ means a₁ etc. An allowed move is to
change the value of any one of the aₙ to another member of {1, 2, 3}
different from its two neighbors, aₙ₋₁ and aₙ₊₁. Is there a sequence of
allowed moves which results in aₘ = aₘ₊₂ = ... = aₘ₊₉₆ = 1,
aₘ₊₁ = aₘ₊₃ = ... = aₘ₊₉₅ = 2, aₘ₊₉₇ = 3, aₘ₊₉₈ = 2 for some m?
[So if m = 1, we have just interchanged the values of a₉₈ and a₉₉.]

The answer is "no": the cyclic-weight sum below is an invariant of allowed
moves, it equals 3 for the initial configuration and -3 for every target
configuration.
-/

namespace Usa1994P2

/-- The three values that may appear in the sequence. We identify the values
1, 2, 3 of the problem statement with 0, 1, 2 in `ZMod 3`; the cyclic
successor map `x ↦ x + 1` then sends 1 → 2 → 3 → 1. -/
abbrev Val := ZMod 3

/-- A configuration of the sequence, indexed by `ZMod 99` (indices are
interpreted modulo 99, as in the problem statement). Index `i` corresponds
to the problem's aᵢ₊₁. -/
abbrev Config := ZMod 99 → Val

/-- The initial configuration: 1, 2, 1, 2, ..., 1, 2, 3. -/
def initial : Config := fun i ↦
  if i.val = 98 then 2 else if i.val % 2 = 0 then 0 else 1

/-- The alternating pattern underlying the target configurations:
`targetPat k` is the value at offset `k` (with `0 ≤ k ≤ 98`) from the base
index, namely 1 at even offsets `≤ 96`, 2 at odd offsets `≤ 95`, 3 at
offset 97 and 2 at offset 98. -/
def targetPat (k : ℕ) : Val :=
  if k = 97 then 2 else if k = 98 then 1 else if k % 2 = 0 then 0 else 1

/-- The target configuration with base index `m`: the value at index `i`
depends only on the offset `i - m`, exactly as in the problem statement
where index `m + k` carries the `k`-th value of the pattern. -/
def target (m : ZMod 99) : Config := fun i ↦ targetPat (i - m).val

/-- An allowed move: change the value at some index `n` to another value `v`
that differs from both neighbors. -/
def Move (a b : Config) : Prop :=
  ∃ n v, v ≠ a n ∧ v ≠ a (n - 1) ∧ v ≠ a (n + 1) ∧ b = Function.update a n v

/-- The answer to the question "is there a sequence of allowed moves to a
target configuration?" is no. -/
/- determine -/ abbrev does_exist : Bool := sorry

theorem usa1994_p2 :
    if does_exist then
      ∃ m : ZMod 99, Relation.ReflTransGen Move initial (target m)
    else
      ¬ ∃ m : ZMod 99, Relation.ReflTransGen Move initial (target m) := sorry

end Usa1994P2

File author(s): Kimi K3

This problem has a complete formalized solution.