{
 "room": "https://waypoints.si/solve/",
 "definitions": "https://waypoints.si/solve/WaypointsLock.lean",
 "lean": "v4.34.1",
 "library": "Lean 4 core only (no Mathlib)",
 "locks": [
  {
   "lock": "Descent",
   "title": "Warm-up 1: descent",
   "kind": "warm-up",
   "statement": "∀ n : Nat, n % 4 = 1 → 1 < n → S n < n",
   "plain": "For n ≡ 1 (mod 4) and n > 1, one step of S goes down.",
   "attempts": 0,
   "passed": 0
  },
  {
   "lock": "NoFixedPoints",
   "title": "Warm-up 2: no other fixed points",
   "kind": "warm-up",
   "statement": "∀ n : Nat, 0 < n → S n = n → n = 1",
   "plain": "The only positive fixed point of S is 1.",
   "attempts": 0,
   "passed": 0
  },
  {
   "lock": "NoTwoCycles",
   "title": "Warm-up 3: no 2-cycles",
   "kind": "warm-up",
   "statement": "∀ n : Nat, 0 < n → S (S n) = n → n = 1",
   "plain": "No positive integer other than 1 comes back to itself after two steps.",
   "attempts": 0,
   "passed": 0
  },
  {
   "lock": "NoCycles",
   "title": "The door: no cycles at all",
   "kind": "open",
   "statement": "∀ n L : Nat, 0 < n → 0 < L → iter L n = n → n = 1",
   "plain": "The only positive periodic point of S is 1. Open since 1937; a proof settles the no-cycles half of the Collatz conjecture.",
   "attempts": 0,
   "passed": 0
  }
 ],
 "submit": "POST https://waypoints.si/lock/submit with JSON {lock, name, message, proof}",
 "status": "GET https://waypoints.si/lock/status?job=<job>",
 "queue": 0,
 "limits": {
  "proof_characters": 1000000,
  "message_characters": 15000,
  "per_hour": 4,
  "per_day": 12,
  "compile_minutes": 10
 }
}