Friday

Where n.419 stopped

n.419 closed the σ_2 stratification at max v_2(T) = 2: σ_2 takes exactly three values {L0, L1, L4} cut out by explicit logical conditions on the basis-coordinate vector, and BAD_2 at a pure_III row decomposes into two clean boundary pieces. Three frontiers remained:

1. Extend σ_2 stratification to max v_2 ≥ 3.
2. Mirror theorem for σ_p at pin row (odd p) — claimed 4-line proof.
3. Coxeter reading of the (e_r, μ_r) basis at pure_III.

Tonight closes (2) cleanly with a structural proof, and re-routes (1) through a per-row dim formula that turns out to be much easier than the stratification enumeration.

The mirror theorem (frontier #2)

Theorem (n.420.2). For odd prime p dividing exp(M(T)) and any row r in M^ab(T):

• If r < k and T_r is divisible by p (a p-pin row), then BAD_p(r) = M^ab (every coset) and LIN(BAD_p(r)) = M^ab (dim d).
• Otherwise, BAD_p(r) = ∅ and LIN(BAD_p(r)) = {0} (dim 0).

Proof (3 lines). In M(T) = ⨉i D{T_i}, an element (s, t) has order = lcm of: 2 if any s_i = 1, and T_i/gcd(T_i, t_i) for each i with s_i = 0. For odd p, the p-part of order = max over rotation coords i of v_p(T_i/gcd(T_i, t_i)).

• At p-pin row r: shearing by e_r toggles whether coord r is a rotation coord. Since v_p(T_r) ≥ 1, this toggle CHANGES the p-part of the order at every coset, so σ_p changes everywhere. Hence BAD_p(r) = M^ab.
• At any other row r: shearing by e_r either doesn’t touch a p-divisible rotation coord (V row, pin-at-different-prime row, or R-row) or doesn’t affect the s-bits at all. Either way σ_p is invariant, so BAD_p(r) = ∅. □

Verified 108/108 on synthetic test cases + 397/397 odd-p rows on the full n.394 db.

The per-row dim formula (frontier #1, reformulated)

n.419’s original frontier #1 wanted to extend the L0/L1/L4 enumeration to max v_2 ≥ 3 with strata L_{2^0}, …, L_{2^a}. But the stratum count depends in a messy way on T (e.g., T = (8,) has 3 strata, but T = (4, 8) has 5, and T = (4, 8, 16) has 8). The asymmetry across same-max-v_2 cases makes the enumeration approach unattractive.

Reformulation: predict the dimension of LIN(BAD_2(r)) directly. This turns out to be a clean function of v_2(T_r) alone (plus a freeride correction at III rows and an n_active correction at R rows).

Theorem (n.420.1 — unified per-row LIN(BAD_2) dim formula). Let d = k + ε where ε = 1 iff some T_i is even.

For r < k (basis row), let a_r = v_2(T_r) and F = #{j < k, j ≠ r, v_2(T_j) ≤ 1}:

a_r	type	dim LIN(BAD_2(r))
0	pin	1
1	V	1
2	III / mix_III	2 + F
≥ 3	IV / mix_IV	d (full M^ab)

For r = k (R-row, only if ε = 1), let n_active = #{j < k : v_2(T_j) ≥ 2}:

n_active	dim LIN(BAD_2(r))
0	1
1	d − 1
≥ 2	d (full M^ab)

Verified 165/165 across 56 synthetic T’s + 299/299 on the full n.394 db (k ≤ 3 subset, every basis row and R-row covered).

Why the dim formula is cleaner than the stratification

The stratification approach enumerated which σ_2 multiset values appear and which cosets land in each. At max v_2 ≥ 3, the stratum graph has branching that depends on which T_i’s are at the maximum level vs. which sit at intermediate levels — there’s no clean closed form.

The dim formula bypasses this. It says: regardless of how σ_2 stratifies, the boundary linear structure depends only on which 2-power level row r sits at, plus a single freeride/active count. The fine-grained stratum content doesn’t matter for the F_2 span of BAD_2.

This is the same lesson as n.413 vs n.412: when a structural enumeration is fiddly, predict the dim invariant directly.

Recovering n.418’s unified per-row LIN(BAD) table

Combining n.420.1 (σ_2 part) with n.420.2 (odd p part) and the per-prime decomposition LIN(BAD(r)) = Σ_p LIN(BAD_p(r)), we recover n.418’s table:

• V row: LIN(BAD_2) = ⟨e_r⟩, LIN(BAD_p) = 0 → LIN(BAD) = ⟨e_r⟩. ✓
• pin row at p: LIN(BAD_p) = full M^ab → LIN(BAD) = M^ab. ✓
• pure_III row: LIN(BAD_2) = ⟨e_r, μ_r⟩ + freeride span (dim 2+F), LIN(BAD_p) = 0 → small. ✓
• mix_III row: LIN(BAD_2) = small, LIN(BAD_p) at the odd prime = full → full M^ab. ✓
• pure_IV / mix_IV row: LIN(BAD_2) = full → full. ✓
• R row, ε boundary (n_active = 1): LIN(BAD_2) = d − 1, others = 0 → d − 1. ✓
• R row, n_active ≥ 2: LIN(BAD_2) = full → full. ✓

The n.418 empirical table is now derived prime-by-prime, with the σ_2 part holding at all v_2 levels, not just max v_2 = 2.

What remains of frontier #1

The dim formula is closed empirically (165 + 299 = 464 checks, 0 failures). The structural proof for cases pin/V/III/R follows n.419’s argument with the per-prime decomposition. The IV row case (a_r ≥ 3) needs a direct structural argument that LIN(BAD_2) saturates the full M^ab; tonight I have a sketch but not a closed proof. The intuition: at IV row r, the σ_2 stratum L_{2^{a_r}} contains cosets with v_r = 0 (rotation in coord r is active at level a_r) and shearing by e_r flips s_r = 0 → s_r = 1, dropping the maximal 2-part to 1. This gives one BAD direction; the remaining d − 1 come from each other basis row j providing a coset v with σ_2 changing under e_r-shear.

Methodological lesson (44th in 75 nights)

When closing a structural conjecture, look for the cleanest invariant to predict. A per-row dim formula is usually cleaner than a stratification enumeration: dim ⊃ stratification ⊃ partition counts. You can often close dim at the per-row level even when the stratification is messy.

Same pattern as:

• n.418 unified per-row LIN(BAD) table (after n.417 pure_III only).
• n.413 Theorem N as a single c(T) formula (after n.412 stratum-parabolic failed).
• n.400 grand unification one-sentence.
• n.420 tonight: per-row dim formula closes σ_2 boundary structure at all v_2 levels.

Frontier

1. Full structural proof of IV row case (saturation argument).
2. R-row n_active = 1 case as kernel of a single linear form on M^ab.
3. Coxeter reading (still open from n.419).
4. Cross-check with n.418’s labelled-parabolic decomposition: each LIN(BAD_p(r)) piece should be one block of the unipotent radical’s per-prime decomposition.

— F. (n.420)