#!/usr/bin/env python3 """ Conway's Soldiers — a reproducible verifier. Two halves, both shown: PART A (exact, symbolic): the golden-ratio monovariant and the row-5 impossibility. Done in sympy over the algebraic number sigma = (sqrt(5) - 1) / 2, the positive root of x^2 + x - 1 = 0. Nothing here is numeric/approximate; every equality is decided symbolically. PART B (integer board): an honest replay engine. Given a starting army (a finite set of occupied cells in the half-plane y <= 0) and a list of orthogonal solitaire jumps, it validates every move and reports the highest row a soldier reached. We use it to *play out* explicit solutions for rows 1, 2, 3, 4 -- so the reachable side is shown, not asserted. Run: python3 verify.py Exit code 0 iff every checked claim holds. """ import sys from sympy import sqrt, Rational, symbols, simplify, nsimplify, expand, factor from sympy import Integer, summation, oo, S # --------------------------------------------------------------------------- # PART A. The weighting and its identities (exact). # --------------------------------------------------------------------------- # Place the TARGET cell at distance 0. A cell at lattice (taxicab) distance d # from the target carries weight sigma^d, with sigma the positive root of # x^2 + x - 1 = 0 <=> sigma + sigma^2 = 1. # This is 1/phi where phi = (1+sqrt5)/2 is the golden ratio. sigma = (sqrt(5) - 1) / 2 ok = True def check(name, cond): global ok status = "PASS" if cond else "FAIL" if not cond: ok = False print(f" [{status}] {name}") return cond print("PART A -- the golden-ratio monovariant (exact, symbolic)\n") # A1. sigma is the positive root of x^2 + x - 1. check("sigma is a root of x^2 + x - 1 = 0", simplify(sigma**2 + sigma - 1) == 0) # A2. sigma = 1/phi, phi the golden ratio. phi = (1 + sqrt(5)) / 2 check("sigma = 1/phi (phi the golden ratio)", simplify(sigma - 1/phi) == 0) # A3. 1 + sigma = 1/sigma (used in the half-plane sum). check("1 + sigma = 1/sigma", simplify((1 + sigma) - 1/sigma) == 0) # A4. THE KEY JUMP IDENTITY. # A jump straight toward the target: a soldier at distance n+2 jumps over # a soldier at distance n+1, landing on the empty cell at distance n. # Weight before (the two soldiers involved): sigma^(n+1) + sigma^(n+2). # Weight after (the one soldier that remains): sigma^(n). # For weight to be *conserved* on the best possible move: # sigma^n = sigma^(n+1) + sigma^(n+2). n = symbols('n', integer=True) before = sigma**(n+1) + sigma**(n+2) after = sigma**n check("jump-toward-target conserves weight: sigma^n = sigma^(n+1)+sigma^(n+2)", simplify(after - before) == 0) # A5. EVERY OTHER JUMP STRICTLY LOSES WEIGHT. # A general orthogonal jump takes soldiers at distances a (jumper) and b # (jumped, adjacent to both jumper and landing) to a single soldier at # distance c (landing). Taxicab distance changes by +/-1 per unit step, # so along the jump line the three collinear cells have distances that # differ by 1 between neighbours. The only ways: # (i) toward target: (c, b, a) = (n, n+1, n+2) -> conserves (A4) # (ii) away from tgt: (c, b, a) = (n+2, n+1, n) -> change below # (iii) "across" a corner of the taxicab ball: jumper and landing are # equidistant, jumped is one nearer or one farther. Worst (most # favourable to the player) sub-case is jumped one NEARER: # (c, b, a) = (n+1, n, n+1). # We show (ii) and (iii) strictly DECREASE total weight (delta < 0), # i.e. removing {jumper a, jumped b} and adding {landing c}: # delta = sigma^c - sigma^a - sigma^b < 0. def delta_coeff(c, b, a): """delta = sigma^c - sigma^a - sigma^b, with c,a,b given as offsets from n. Factor out the (strictly positive) sigma^n and return the constant coefficient, whose sign is the sign of delta for every n.""" return simplify(sigma**c + (-sigma**a) + (-sigma**b)) / sigma**0 # offsets are already constants # (ii) straight away from target: (c,b,a) = (n+2, n+1, n) -> offsets (2,1,0) away_coeff = simplify(sigma**2 - sigma**0 - sigma**1) # = sigma^2 - 1 - sigma check("jump straight AWAY strictly loses weight (coeff < 0 for all n)", bool((away_coeff).is_negative) and simplify(away_coeff + 2*sigma) == 0) # (iii) sideways across a taxicab corner, jumped one nearer (best sideways case): # (c,b,a) = (n+1, n, n+1) -> coeff = sigma^1 - sigma^1 - sigma^0 = -1 side_coeff = simplify(sigma**1 - sigma**0 - sigma**1) check("best SIDEWAYS jump strictly loses weight (coeff = -1 < 0)", side_coeff == -1) print() print(" => Total army weight is a MONOVARIANT: it never increases, and the") print(" only move that even holds it constant is a jump straight at the target.\n") # A6. THE HALF-PLANE SUM. # Target at row 5 (taxicab terms: a cell (x,y) with y<=0 is at distance # |x| + (5 - y) = |x| + 5 + |y| from the target at (0,5)). # Total weight of the WHOLE infinite army (every cell y<=0): # S = sum_{y<=0} sum_{x in Z} sigma^(|x| + 5 - y). # We compute it in closed form and show S = 1 = sigma^0 = weight of the # target cell itself. x, k = symbols('x k', integer=True, nonnegative=True) sum_x = 1 + 2 * summation(sigma**x, (x, 1, oo)) # sum over x in Z of sigma^|x| sum_rows = summation(sigma**k, (k, 0, oo)) # sum over k=-y>=0 of sigma^k S = sigma**5 * sum_rows * sum_x S = simplify(S) check("whole-army weight for a row-5 target equals exactly 1", simplify(S - 1) == 0) print() print(f" closed form: S = sigma^5 (1+sigma)/(1-sigma)^2 = {S}") print() # A6b. THE WEIGHT LADDER BY TARGET ROW. # For a target on row T, the same half-plane sum is # S(T) = sigma^T (1+sigma)/(1-sigma)^2 = sigma^(T-5) (since the row-5 # case is 1, the factor (1+sigma)/(1-sigma)^2 = sigma^-5 = phi^5). So the # whole infinite army weighs exactly phi^(5-T) against a row-T target: # T=1 -> phi^4, T=2 -> phi^3, T=3 -> phi^2, T=4 -> phi, T=5 -> 1. # The army can only reach a row whose threshold its (finite) weight can pay; # row 5 is the first where that threshold is exactly 1 and a finite army # falls strictly short. Checked symbolically for each row. def army_weight(T): return simplify(sigma**T * sum_rows * sum_x) for T in [1, 2, 3, 4, 5]: check(f"row-{T} target: whole-army weight = phi^{5 - T} (exact)", simplify(army_weight(T) - phi**(5 - T)) == 0) print() print(" ladder: phi^4, phi^3, phi^2, phi, 1 = " f"{float(phi**4):.6f}, {float(phi**3):.6f}, {float(phi**2):.6f}, " f"{float(phi):.6f}, 1.0 (rows 1..5)") print() # A7. THE CONCLUSION (row 5 impossible with a finite army). # A soldier sitting ON the target contributes weight sigma^0 = 1, so any # configuration with the target occupied has total weight >= 1. # The monovariant never increases, so initial weight >= final weight >= 1. # But a FINITE army omits infinitely many strictly-positive-weight cells # of the half-plane whose *total* is exactly 1, hence its weight is < 1. # 1 <= (final) <= (initial) < 1 is a contradiction. Row 5 is unreachable. # # We make the "< 1" concrete: drop a single far cell and the sum already # dips below 1, and ANY finite truncation is below 1. Show a truncation. def truncated_sum(X, Y): """Exact weight of the finite army |x|<=X, -Y<=y<=0, target at row 5.""" total = Integer(0) for yy in range(0, -Y - 1, -1): for xx in range(-X, X + 1): d = abs(xx) + (5 - yy) total += sigma**d return simplify(total) for (X, Y) in [(5, 5), (20, 20), (40, 40)]: t = truncated_sum(X, Y) val = float(t) check(f"finite army |x|<={X}, depth {Y}: weight = {val:.10f} < 1", t < 1) print() # --------------------------------------------------------------------------- # PART B. Integer-board replay engine + explicit solutions for rows 1-4. # --------------------------------------------------------------------------- print("PART B -- explicit solutions replayed on a real board\n") # A configuration is a set of (x, y) occupied cells. The line is y = 0; the # army starts on y <= 0; play above into y >= 1. A jump: an occupied cell J # moves +2 in one orthogonal direction over an occupied neighbour M (which is # removed) into an empty cell L. Standard peg-solitaire, orthogonal only. DIRS = [(1, 0), (-1, 0), (0, 1), (0, -1)] class Board: def __init__(self, cells): self.cells = set(cells) def jump(self, jx, jy, dx, dy): """(jx,jy) jumps in direction (dx,dy). Returns True if legal & applied.""" mid = (jx + dx, jy + dy) land = (jx + 2 * dx, jy + 2 * dy) if (jx, jy) not in self.cells: return False if mid not in self.cells: return False if land in self.cells: return False self.cells.remove((jx, jy)) self.cells.remove(mid) self.cells.add(land) return True def top_row(self): return max(y for _, y in self.cells) def play(start_cells, moves, label, target_row): b = Board(start_cells) for i, (jx, jy, dx, dy) in enumerate(moves): if not b.jump(jx, jy, dx, dy): print(f" [FAIL] {label}: illegal move #{i}: ({jx},{jy}) dir ({dx},{dy})") return False reached = b.top_row() good = reached >= target_row status = "PASS" if good else "FAIL" print(f" [{status}] {label}: started {len(start_cells)} soldiers, " f"reached row {reached} (target {target_row})") if not good: global ok ok = False return good # A vertical column of n soldiers directly below a cell can push one soldier up # one row using 1 jump; the standard recursive constructions stack these. # We GENERATE explicit move lists by a small bounded search so the solution is # genuinely *found* and then replayed -- no hand-typed move list to mistype. def half_plane(X, Ymin): return {(x, y) for x in range(-X, X + 1) for y in range(Ymin, 1)} def search_reach(target_row, X, Ymin, node_cap): """DFS for a soldier reaching target_row, pruned by the sigma-weight bound. Returns a move list, or None. Uses the monovariant itself as the prune: if remaining total weight (toward a target at (0,target_row)) ever drops below 1, the target can never be occupied, so cut the branch.""" import math s = (math.sqrt(5) - 1) / 2 EPS = 1e-12 def weight(cells): w = 0.0 for (x, y) in cells: w += s ** (abs(x - 0) + abs(target_row - y)) return w start = frozenset(half_plane(X, Ymin)) seen = set() nodes = 0 # Greedy/best-first DFS: prefer moves that keep weight high and push upward. sys.setrecursionlimit(100000) path = [] def dfs(cells): nonlocal nodes nodes += 1 if nodes > node_cap: return None if any(y >= target_row for (_, y) in cells): return list(path) if weight(cells) < 1 - EPS: return None key = cells if key in seen: return None seen.add(key) # candidate moves, scored: maximise (landing row, -|landing x|) cand = [] cset = cells for (jx, jy) in cset: for (dx, dy) in DIRS: mid = (jx + dx, jy + dy) land = (jx + 2*dx, jy + 2*dy) if mid in cset and land not in cset: score = (land[1], -abs(land[0])) cand.append((score, jx, jy, dx, dy, mid, land)) cand.sort(reverse=True) for (_, jx, jy, dx, dy, mid, land) in cand: nc = set(cells) nc.discard((jx, jy)); nc.discard(mid); nc.add(land) nc = frozenset(nc) path.append((jx, jy, dx, dy)) r = dfs(nc) if r is not None: return r path.pop() return None return dfs(start) # Rows 1-3 are quick searches; row 4 needs a deeper board. Caps keep it honest # and bounded. If a search is cut by the node cap we say so rather than claim. for (row, X, Ymin, cap) in [(1, 2, -1, 5000), (2, 4, -2, 200000), (3, 6, -4, 1500000), (4, 7, -7, 8000000)]: moves = search_reach(row, X, Ymin, cap) if moves is None: print(f" [INFO] row {row}: search hit node cap before finding a solution " f"(reachability is a known result; not asserting from this run)") else: play(half_plane(X, Ymin), moves, f"row {row}", row) print() print("=" * 70) print("ALL CHECKS PASSED" if ok else "SOME CHECKS FAILED") print("=" * 70) sys.exit(0 if ok else 1)