v1.0-r179 — L(n) = o(n): manuscript + Lean tier-1 kernel check

L(n) = o(n) — manuscript + Lean 4 kernel check

First tagged release of the research record for Erdős Problem 872: the divisor-antichain game on {2,…,n} has guaranteed length L(n) = o(n) — the game cannot be guaranteed to last εn moves for any fixed ε > 0.

What this release contains

• Theorem writeup: erdos-872/researcher-R179-lean-verified-manuscript.md — the final self-contained manuscript (robust envelope game → K-dense/rough-tag decomposition → laminar root cones → adaptive sweep → density recursion c_b ≤ ½·c_{b+1}).
• Lean 4 formalization: erdos-872/lean/r177_verification — Erdos872.main : Tendsto (originalRatio L) atTop (nhds 0), ~12,000 lines, zero sorry. Kernel-checked axiom report: [propext, Classical.choice, Erdos872.A3_exceptional_set_estimate, Quot.sound] — exactly one problem-specific axiom, A3 = Lemma 2.3 (exceptional-set density estimate, proved in the manuscript via Selberg sieve + Rankin's method, not yet formalized).
• Full research record: 179 rounds of dispatches, prompts, adversarial audits, refutations, and the verification chain, as immutable round docs with a compiled state view.

Verification status: independent rebuild + #print axioms kernel check recorded in erdos-872/verify-lean-R179-fable-kernel-check.md.

Licensing: code MIT, research artifacts CC-BY 4.0 (see LICENSE).