Add Erdos #160 proof-lab target

[ashhart]

Summary

Adds syntra proof-lab erdos160, a bounded finite-shadow target for Erdos Problem #160. The new target estimates finite h(N) rows: the least color count needed so every 4-term arithmetic progression in {1..N} has at least three distinct colors.

This keeps erdos190 as the solved/sanity-check target and adds #160 as the live open-problem target.

What changed

• Added Lycan combinatorics helpers for the #160 predicate:
  • detect 4-APs with fewer than three distinct colors
  • verify three-distinct 4-AP colorings
  • bounded witness / unsat / inconclusive search by N, color cap, and node limit
• Added native Lycan kernels:
  • comb.hasThreeDistinct4ApColoring(colors)
  • comb.badThreeDistinct4Ap(colors)
  • comb.threeDistinct4ApWitness(n, max_colors, node_limit)
• Added syntra proof-lab erdos160 with JSON/Markdown/Lean output support.
• Updated proof-lab docs, README, DEMOS, examples index, and CONTEXT.md so #160 is visible as the open-problem finite-shadow target.

Verification

• cargo test --release proof_lab -- --test-threads=1
• cargo test --release --manifest-path Lycan/Cargo.toml combinatorics -- --test-threads=1
• cargo test --release --manifest-path Lycan/Cargo.toml erdos160_kernels -- --test-threads=1
• ./target/release/syntra proof-lab erdos160 --max-n 22 --max-colors 4 --node-limit 100000 --format json
  • reports exact finite rows through N=22 with h(22) = 4
• python3 evals/repo-read/check_context_contract.py
• git diff --check
• cargo test --release -- --test-threads=1
• cargo test --release --manifest-path Lycan/Cargo.toml -- --test-threads=1

Warnings observed are existing unused-code/import warnings only.