Prove paired-stage loss at m = 4 under the chronology cut is exactly 10 (no new κ)

research/paired-stage-chronology-m4/PROOF.md

@@ -0,0 +1,101 @@
+# Exact paired-stage loss at m = 4 under the mixed chronology cut
+
+## Model
+
+This is the binary normalized paired-stage controller of
+[PR #5631](https://github.com/CrocSwap/integer-mult-bounds/pull/5631)
+(`research/paired-stage-chronology-cut`), which builds on PR #5617. Work
+over F2. There are n main fields and L = n + 2 = 2m full calls, listed in
+chronological order. Call i has a query
+
+    R_i = u_i v_i,   v_i u_i = 0,   sum_i R_i = I_n,
+
+and a rank-two idempotent P_i with P_i R_i = R_i P_i = R_i. The calls are
+partitioned into m stages of two calls each. Stage c with calls i, j has
+target derivative E_c = P_i + P_j. The targets must be idempotent and
+diagonal in one common output basis, and every stage must satisfy the mixed
+coefficient condition of PR #5631 Section 4:
+
+    [P_i, S_i] + [P_j, S_j] = 0,   S_i = sum_(l > i) R_l.          (*)
+
+Put r_c = rank E_c and D = 4m - sum_c r_c. PR #5631 proves D >= 2 for
+m >= 4 from the rank and pairing cuts, and asks whether a family of bounded
+loss can satisfy (*) at all sizes.
+
+## Theorem (finite, m = 4)
+
+At m = 4 (n = 6, L = 8), every query system, chronological order, stage
+pairing and projector choice that satisfies the conditions above has
+D >= 10. Equivalently sum_c r_c <= 6. The bound is attained.
+
+Of the 35,008 query Gram systems, 23,564 admit no assignment at all. The
+remaining 11,444 have minimum loss distributed as
+`{10: 2400, 12: 4760, 14: 3084, 16: 1200}`. The previous lower bound at
+m = 4 was D >= 2.
+
+These are necessary conditions only. The theorem is a lower bound for any
+complete word in this model. A system that passes is not a caller: the
+other word coefficients, native realization and price are not checked.
+
+## Reduction to a finite enumeration
+
+**Lemma 1 (Gram normal form).** Put U = [u_0 ... u_(L-1)] and let V have
+rows v_i. Then UV = I_n, and K = VU is an L x L idempotent of rank n with
+zero diagonal. If two systems have the same K, they are conjugate by an
+element of GL(n, F2). Proof: set G = U V'. Then G U' = U K = U and
+V G = K V' = V', and G (U' V) = U K V = I. So u_i = G u'_i and
+v'_i = v_i G, and R'_i = G^-1 R_i G. Conjugation preserves compatibility,
+ranks, commutation, idempotence and (*). Conversely every such K arises:
+take V a basis matrix of its column space and U the coordinates of its
+columns.
+
+I + K is a rank-two idempotent with all diagonal entries one. Every
+rank-two idempotent factors as XY with X of size L x 2, Y of size 2 x L
+and YX = I_2. Its diagonal is x_i . y_i. The verifier therefore enumerates
+all sequences of pairs (x_i, y_i), x_i nonzero in F2^2 and x_i . y_i = 1,
+with sum y_i x_i^T = I_2, and keeps the distinct K. There are 35,008 at
+L = 8 and 976 at L = 6. Order is part of K, so every chronology is covered.
+
+**Lemma 2 (projectors).** PR #5617 Section 2 shows that the compatible
+rank-two idempotents for call i are exactly P = u_i b + a v_i with
+v_i a = b u_i = 1 and b a = 0. The verifier enumerates all such (a, b). Each P arises from exactly two
+parameter pairs, (a, b) and (a + u_i, b + v_i), so candidates are deduplicated.
+
+**Lemma 3 (reversal).** Since sum R = I and [P_i, R_i] = 0,
+[P_i, sum_(l < i) R_l] = [P_i, sum_(l > i) R_l]. Hence reversing the call
+order and transposing every matrix maps a valid assignment to a valid one
+with the same ranks. In Gram terms this is K -> J K^T J, with J the
+reversal. The census computes one representative per orbit and weights
+it by orbit size. The m = 3 weighted census reproduces an unreduced run.
+
+**Stage algebra.** In characteristic two, (P_i + P_j)^2 = P_i + P_j exactly
+when P_i and P_j commute. A family of commuting idempotents is diagonal in a
+common basis, and the converse is immediate. For each call pair the
+verifier groups projectors by the value of [P_i, S_i], so (*) becomes
+equality of keys. It keeps all commuting pairs, records each distinct E and
+its rank, then takes the maximum of sum r_c over all 105 pairings and all
+pairwise commuting choices of E, by exhaustive branch and bound. The bound
+4 per remaining stage is exact because r_c <= 4.
+
+## Controls
+
+- m = 3: the same code finds D = 0 on 146 Gram systems, so the program is
+  not vacuous. PR #5631 reports a genuine six-query word that passes.
+- An optimal m = 4 word is rebuilt and passed to PR #5631's own
+  `chronology.mixed` routine, unchanged. It reports no defect. Exchanging
+  the first two calls makes it report a defect.
+- Reversing the call order of the witness keeps every mixed coefficient,
+  as Lemma 3 predicts.
+
+A separate implementation using NumPy and no orbit reduction reproduced the
+m = 4 histogram over all 35,008 systems. That run is local evidence and is
+not registered.
+
+## What this does and does not settle
+
+The data show (*) is strong at m = 4: the best target mass is 6 of 16.
+This does not prove that D grows with m. The m = 5 census is larger
+(n = 8 gives 2^13 projectors per call) and was not run. No asymptotic
+lemma is proved. The theorem does not cover thin calls, idle maps, coupled
+ports, characteristic other than two or other word coefficients. It changes
+no price exclusion: PR #5631 already rejects m <= 47 with D >= 2.

research/paired-stage-chronology-m4/README.md

@@ -0,0 +1,94 @@
+# Paired-stage loss at m = 4 under the chronology cut is exactly 10
+
+**Finite certificate, scoped to a necessary-condition model. No new κ.**
+
+In the binary normalized paired-stage controller of
+[PR #5631](https://github.com/CrocSwap/integer-mult-bounds/pull/5631), take
+m = 4 stages (n = 6 fields, L = 8 calls). Impose the earlier rank and pairing
+conditions together with PR #5631's mixed chronology coefficient (*). Then every
+query system, chronological order, stage pairing and compatible projector
+choice has loss
+
+    D = 4m - sum_c rank E_c >= 10,
+
+and 10 is attained. The earlier bound at this size was D >= 2. Stage targets
+can keep at most 6 of the 16 possible ranks.
+
+PR #5631 asks whether a constant-loss family can satisfy chronology at all
+sizes. This answers the first open size. It does not decide the asymptotic
+question. See [PROOF.md](PROOF.md) for the model, the reduction lemmas and the
+controls.
+
+## Census
+
+| | Gram systems |
+|---|---:|
+| all query Gram systems at L = 8 (every order) | 35,008 |
+| no assignment satisfies the conditions | 23,564 |
+| minimum D = 10 | 2,400 |
+| minimum D = 12 | 4,760 |
+| minimum D = 14 | 3,084 |
+| minimum D = 16 | 1,200 |
+
+The census is exhaustive over three things. First, it covers every Gram matrix
+K = (v_i u_j). Equal K means the systems are conjugate. Second, it covers every
+compatible rank-two projector u b + a v for each call. Third, it covers all 105
+pairings, with every pairwise-commuting choice of stage targets. A reversal
+symmetry halves the work, and the histogram is reweighted by orbit size.
+
+Controls:
+
+- At m = 3 the same code finds D = 0, so the search is not vacuous.
+- An optimal m = 4 word, with stage ranks 0, 0, 2 and 4, passes PR #5631's own
+  `chronology.mixed` routine unchanged.
+- Exchanging that word's first two calls makes the routine report a defect.
+
+Locally, a second implementation in NumPy, without the orbit reduction,
+reproduced the full histogram. A sample with (*) removed gave minimum D of
+4 to 6 on 11 of 12 random systems, so the cut is what raises the loss to 10.
+Those two runs are local evidence and are not registered.
+
+## Limits
+
+These are necessary conditions. Passing them does not make a caller: other word
+coefficients, native realization, restoration and price are unchecked. The
+model has no thin calls, no idle maps, separate ports and characteristic two.
+The result moves no price exclusion. PR #5631 already rejects m <= 47 using
+D >= 2. No m = 5 census and no all-size lemma is claimed.
+
+## Reproduce
+
+Python 3.12, standard library only, from the repository root:
+
+```sh
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/paired-stage-chronology-m4
+# or directly:
+python3.12 -B research/paired-stage-chronology-m4/verify.py                       # witness and controls, < 5 s
+python3.12 -O -B research/paired-stage-chronology-m4/verify.py --shard K --shards 7  # K = 0..6
+```
+
+Each shard checks about 2,500 orbit representatives against its histogram and SHA256
+in [RESULT.json](RESULT.json). A shard takes about 130 CPU seconds, or about
+35 s of wall time with four processes. `--jobs` sets the process count.
+The verifier imports the pinned `research/paired-stage-chronology-cut/chronology.py`
+unchanged; its hash is in [SOURCES.json](SOURCES.json).
+
+## Open next questions
+
+1. **Does the loss grow with m?** If D grows linearly, PR #5631's argument
+   excludes every paired-stage size at κ >= 0.003. The first step is an m = 5
+   census, or a paired analogue of Cinna Davis's minimum-query
+   private-projector lemma that bounds the number of rank-four stages. The
+   blocker is size: n = 8 gives 2^13 projectors per call, so pure enumeration
+   needs a structural reduction.
+2. **Why is the rank sum at most 6?** Classifying the 2,400 optimal systems
+   and their rank patterns could give a proof that generalizes.
+
+Structured versions are in [TASK.json](TASK.json).
+
+## Credit
+
+Model, mixed coefficient cut and `chronology.mixed`: Ali Romman (PR #5631),
+building on PR #5617, Cinna Davis's private-projector lemma, and the P104
+source contributors credited there. The m = 4 census, reduction lemmas and
+verifier were produced by Nick Petalas. Apache-2.0.