# 1D and 2D Conway Checkers: Auto-monovariance in Lean

**Status (2026-05-25 evening swing):** 12 tracked theorems sorry-free,
axiom-free in `lean-status.json`.

## What was new in this swing

The earlier `f38948904` commit proved the 1D row-2 obstruction with a
*certificate-passing* `LegalJump1D` — the potential-non-increase property
was a field of the relation, supplied by whoever constructed the jump. That
mirrors the existing 2D modules (`Soldiers.lean`, `Diagonal.lean`) but is a
formalization shortcut: the certificate is the conclusion of the structural
lemma, so requiring it as a hypothesis is circular at the mathematical level.

This swing closed that gap.

### Layer 1: row-n generalization in 1D

`conway_soldiers_1d_row_n_unreachable n hn` proves unreachability for every
`n ≥ 2`. The n=2 case is the sharp Bruda-Cooper case (`potential1D 2 < 1`
strictly via the half-line argument). For `n ≥ 3` the loose ideal-half-line
bound `phi^(n-2) ≤ phi < 1` suffices. This is the full Eriksson-Lindström
d=1 bound `nM ≤ 1` mechanized.

### Layer 2: 1D auto-monovariance

Pointwise triangle inequality, proved by case analysis on sign of `a`:

```
phi^|a+2| ≤ phi^|a| + phi^|a+1|  for every integer a.
```

- `a ≥ 0`: phi^(a+2) = phi^a · phi^2 ≤ phi^a · 1 ≤ phi^a + phi^(a+1).
- `a = -1`: phi ≤ phi + 1.
- `a ≤ -2`: writes `a = -(b+2)` with `b ≥ 0`; RHS = phi^b · (phi^2 + phi) =
  phi^b · 1 = phi^b = LHS. **Equality.**

The equality case is the mathematical content of Bruda-Cooper Lemma 4.4's
integer-floor sharpness: the energy bound is tight when the army hugs the
target axis from behind.

This pointwise fact is then lifted to board-level monotonicity in
`rawJump1D_monovariant`, and `rawJump1D_imp_legalJump1D` shows the
certificate field of `LegalJump1D` is mathematically redundant.

### Layer 3: 2D back-port for orthogonal jumps

The 2D orthogonal weight factors as `phi^|Δx| · phi^|Δy|`. For an x-axis
jump, `|Δy|` is unchanged across `{src, mid, dst}`, so factoring it out
reduces the 2D pointwise inequality to the 1D inequality on the x-coordinate.
Symmetrically for y-axis.

Result: `orthogonalRawJump_monovariant_x` and
`orthogonalRawJump_monovariant_y` produce the certificate automatically from
geometry, for any orthogonal raw jump. Users of `Conway.Soldiers.LegalJump`
can now construct the certificate field without manual proof.

## What this is not

Still not a solution to an open problem. The deepest open problems in this
realm (Conway row-4 min army 19 vs 20, fully-diagonal row-4 7 vs 8, ...)
remain untouched. Twenty years of focused effort have not closed them; one
evening of formalization will not either.

## What this is

A real structural cleanup of the Lean formalization. The 1D and 2D
orthogonal cases now match the mathematical content honestly. The 8-direction
diagonal jumps in `Conway.Diagonal` still use the certificate-passing
shortcut — generalizing to that case requires fresh content (the Chebyshev
metric does not factor cleanly into independent axes) and is left for future
work.

## Tracked theorems (all sorry-free, axiom-free)

| Theorem | Module | Layer |
|---|---|---|
| `conway_soldiers_row5_unreachable` | Soldiers | 2D orth |
| `conway_soldiers_diagonal_row9_unreachable` | Diagonal | 2D diag |
| `goldenRatio_mul_fib_odd` | FibPredicate | Fib id |
| `neg_goldenConj_pow_odd` | FibPredicate | psi id |
| `conway_soldiers_1d_row2_unreachable` | OneDim | 1D sharp |
| `conway_soldiers_1d_row_n_unreachable` | OneDim | 1D row-n ≥ 2 |
| `phi_weight_triangle_forward` | OneDim | 1D pointwise |
| `phi_weight_triangle_backward` | OneDim | 1D pointwise |
| `rawJump1D_monovariant` | OneDim | 1D auto |
| `rawJump1D_imp_legalJump1D` | OneDim | 1D cert-free |
| `orthogonalRawJump_monovariant_x` | AutoMono | 2D orth auto, x |
| `orthogonalRawJump_monovariant_y` | AutoMono | 2D orth auto, y |

## Honest novelty score

~5/10. All math is known (1995-2025 published). The mechanization is novel
(no prior Lean formalization of any of this), and the certificate-removal is
a structural improvement worth keeping. The path forward to the open
problems is opened by an additional layer: the diagonal-jump 8-direction
case, then per-cell multiplicity m. Both feasible in a focused multi-session
push, neither a one-evening artifact.