proof-lab: add erdos160 (OPEN) finite-certificate target

[ashhart]

Summary

Adds syntra proof-lab erdos160 --max-n <N> --node-limit <L>, mirroring the shipped erdos190 proof-lab path, for Erdos #160 (erdosproblems.com/160, status OPEN):

h(N) is the smallest number of colours k such that {1..N} can be k-coloured so that every four-term arithmetic progression contains at least three distinct colours.

The open question is the asymptotic growth of h(N) (known: h(N) << N^{2/3}; Hunter << N^{(log3/log22)+o(1)} ~ N^{0.355}). A finite computation cannot resolve it, so the command produces finite exact values + certificates and explicitly refuses the asymptotic.

What changed

Combinatorics kernel (Lycan/src/combinatorics.rs)

• bad_arithmetic_progression_160 / is_good_coloring_160 — the #160 predicate (a 4-AP is bad iff it has < 3 distinct colours), distinct from #190's monochromatic/rainbow predicate.
• search_coloring_160 — bounded exhaustive search, canonical colour assignment, incremental pruning of the 4-APs ending at each position.
• h160 — per-N minimum-colour search returning WITNESS (h(N) <= c), EXHAUSTION (h(N) >= c; with a c-witness gives exact h(N)=c), or INCONCLUSIVE (node limit hit -> no claim).

Proof lab (src/proof_lab.rs, CLI wiring in src/lib.rs)

• run_erdos160: per-N witness/exhaustion/inconclusive rows, finite exact + bound claims, conjectures/non-claims (monotonicity; the h(N) >= 3 for N >= 4 floor), a Lean starter file, and a proof arena. No --k flag (AP length fixed at 4).
• Load-bearing refusal: the asymptotic estimate is an explicit proof obligation asymptotic_estimate_h160 with status expert_theorem_required, plus an arena asymptotic_refusal case; every finite result is labelled finite evidence that does not resolve Erdos #160, and the command never emits an asymptotic claim.
• Monotonicity h(N) <= h(N+1) is asserted across rows; any violation is flagged in conjectures, warnings, and the arena.

Docs: CONTEXT.md (contract still passes), DEMOS.md, README.md, examples/proof-lab/README.md describe erdos160 as an OPEN target handled honestly, distinct from solved #190.

Verification (all green locally, cargo 1.95)

• cargo build --release: clean (only a pre-existing unrelated Lycan PathBuf warning).
• Full suite as CI runs it:
  • Syntra lib: 57 passed
  • Syntra CLI integration (--test-threads=1): 30 passed
  • Syntra auth_routes: 10 passed
  • Lycan lib: 261 passed
  • Lycan integration: 139 passed
  • python3 evals/repo-read/check_context_contract.py: OK
• ./target/release/syntra proof-lab erdos160 --max-n 18 --node-limit 200000 prints h(N) = 1,1,1,3,3,3,3,3,3,3,3,3,4,4,4,4,4,4 for N=1..18 (jumps at N=4 and N=13) — matches the independently verified values.

Tests reproduce the verified facts: h(1..3)=1, h(4..12)=3, h(13..18)=4; the N=22 witness [1,1,3,4,2,4,1,2,1,3,3,2,4,1,2,1,3,3,2,4,1,4] validates with 4 colours; exact h(12)=3 and h(13)=4 via witness + exhaustion; monotonicity holds; a tiny node limit reports inconclusive (not a bound).

🤖 Generated with Claude Code