Prove the sharp n-axis monomial elimination record count.

research/n-axis-monomial-records/PROOF.md

@@ -0,0 +1,204 @@
+# Record count of one n-axis monomial elimination
+
+This is a proof about one synthesis. It is not a lower bound on every
+recipe in the selected primitive alphabet, and it does not change κ.
+
+## Normal form
+
+Use the nine-axis shape from `research/final4610-independent-admission/SPECIALIZATION.md`,
+with the axis count left free. An n-axis monomial is an invertible matrix
+`A` over `F_2`, a translation `b` in `F_2^n`, a global phase `a` modulo 4,
+linear coefficients `alpha_i` modulo 4, and off-diagonal bits `Q_ij` for
+`i < j`. The diagonal of `Q` is carried by `alpha_i mod 2` and is not a
+separate controlled-sign record. On a basis address the monomial applies
+the quadratic phase and then the affine map `x -> A x + b`.
+
+The selected-bit primitives used here are one row addition, one translation
+of a single bit, one unit phase on a single bit, one controlled sign on a
+pair of bits, and one global factor of `i`. A row swap is three row
+additions: over `F_2`,
+
+```text
+u <- u+v,    v <- v+u,    u <- u+v
+```
+
+sends `(u, v)` to `(v, u)`. Two additions do not.
+
+## Elimination
+
+Start from `M = A`. For `k = 0, ..., n-1`:
+
+1. Let `r` be the least index at least `k` with `M_{r k} = 1`.
+2. If `r != k`, swap rows `r` and `k`.
+3. For every `i != k` with `M_{i k} = 1`, add row `k` into row `i`.
+
+**Block form.** At the start of column `k` the matrix is
+
+```text
+[ I_k    B ]
+[ 0      C ]
+```
+
+with `C` of size `n-k`. Swaps are among rows `k, ..., n-1`, and those rows
+have zeros in columns `0, ..., k-1`, so a swap does not change the finished
+columns. Row `k`, once it holds the pivot, also has zeros in columns
+`0, ..., k-1`, because that row was taken from the bottom block. Adding it
+to other rows therefore does not change finished columns. Clearing column
+`k` makes that column equal to `e_k`. By induction the algorithm ends at
+`I_n` whenever every pivot exists.
+
+**Pivot existence.** The elementary steps are invertible, so `A` is
+invertible if and only if the current matrix is. In the block form that is
+equivalent to `C` being invertible. The first column of an invertible `C`
+is nonzero, so a pivot row `r >= k` exists. At `k = n-1` the only eligible
+row is `n-1`, so the last column never swaps. Thus the number of swaps is
+at most `n-1`.
+
+**Column charge.** Fix column `k`. Let `s_k` be 1 if a swap occurs and 0
+otherwise, and let `a_k` be the number of additions. There are `n-1` rows
+other than the pivot.
+
+- If `s_k = 0`, at most those `n-1` rows are cleared, so `a_k <= n-1`.
+- If `s_k = 1`, then `M_{k k} = 0` before the swap. After the swap that
+  zero lies in the row that was exchanged. That row is not cleared, so
+  `a_k <= n-2`.
+
+In both cases `a_k + s_k <= n-1`. Summing over columns,
+
+```text
+sum a_k + sum s_k <= n(n-1),    sum s_k <= n-1.
+```
+
+The address recipe replaces each swap by three additions, so its length is
+
+```text
+sum a_k + 3 sum s_k
+  = sum (a_k + s_k) + 2 sum s_k
+  <= n(n-1) + 2(n-1)
+  = (n+2)(n-1).
+```
+
+The separate ceilings `sum a_k <= n(n-1)` and `sum s_k <= n-1` are true,
+but adding them charges `3(n-1)` for the swaps on top of `n(n-1)`
+additions and produces the longer count `(n+3)(n-1)`. The column charge
+removes `n-1` from that count. For `n > 1` the two separate ceilings are
+not achieved by one matrix: a swapped column has at least one uncleared
+row. The exhaustive check for `n <= 4` records that fact. The inequality
+above does not need it.
+
+## Phase and translation
+
+These records do not depend on `A`.
+
+- `b` has at most `n` ones, one translation each.
+- Each `alpha_i` lies in `{0,1,2,3}`, so at most `3n` unit phase records.
+- At most one controlled sign for each of the `n(n-1)/2` pairs.
+- The global phase `a` needs at most three factors of `i`.
+
+Adding these ceilings to the address bound gives
+
+```text
+R(n) = (n+2)(n-1) + 4n + 3 + n(n-1)/2 = (3n^2 + 9n + 2)/2.
+```
+
+The numerator is even because `n(n+3)` is even, so `3n(n+3) + 2` is even.
+The same count is an integer recipe length for every positive integer `n`.
+
+## The bound is achieved by this synthesis
+
+For `n = 1` the matrix `(1)`, the translation `1`, `alpha_0 = 3` and global
+phase `3` emit `0 + 1 + 3 + 0 + 3 = 7 = R(1)` records.
+
+For `n >= 2` define `A` by
+
+```text
+row 0 = e_{n-1},    row i = e_0 + e_i for i = 1, ..., n-1.
+```
+
+At the start of column `k`, for `0 <= k <= n-1`,
+
+- row `i` equals `e_i + e_k` for every `i < k`,
+- row `k` equals `e_{n-1}`,
+- row `i` equals `e_k + e_i` for every `i > k`.
+
+This holds at `k = 0`. If `k < n-1`, row `k` has a zero in column `k` and
+row `k+1` has a one there, so the pivot is row `k+1`. After that swap,
+clearing column `k` adds the pivot row to the `k` rows above it and to the
+`n-k-2` rows below `k+1`, which is `n-2` additions, and produces the same
+description at column `k+1`. At column `n-1` there is no swap, and each of
+the `n-1` earlier rows has a one in the last column.
+
+Thus the algorithm swaps on exactly the first `n-1` columns, performs
+`(n-1)(n-2)` additions there and `n-1` additions on the last column, and
+the address length is
+
+```text
+(n-1)^2 + 3(n-1) = (n+2)(n-1).
+```
+
+Choose every bit of `b` equal to 1, every `alpha_i` equal to 3, every
+`Q_ij` equal to 1, and global phase 3. Then `alpha_i` is odd, so the
+stored diagonal bit is 1, and no extra controlled sign is emitted for it.
+This one monomial makes the synthesis emit exactly `R(n)` records.
+
+Reaching `I_n` also shows that this `A` is invertible. The census for
+`n <= 4` finds exactly one maximizer in each `GL(n, F_2)`, and it is this
+matrix.
+
+## Comparison with the published sufficient counts
+
+The `#4610` specialization charges at most `n(n-1)` additions and at most
+`n-1` swaps separately. That address length is `(n+3)(n-1)`, and the full
+record ceiling is
+
+```text
+L(n) = (3n^2 + 11n)/2 = R(n) + (n-1).
+```
+
+At `n = 9` this is `96 + 9 + 27 + 36 + 3 = 171`, matching the published
+line. The sharper count is `R(9) = 163`. Both are sufficient. The value
+171 is not false; it does not use the column charge.
+
+The operation list in section 6 of the `#7000` application review is
+`n(n-1)+3n` row additions, `n` affine flips, `3n` unit phases,
+`n(n-1)/2` controlled signs and three global phases. Its sum is
+
+```text
+S(n) = L(n) + 3 = R(n) + n + 2,
+```
+
+because `n(n-1)+3n` charges `n` swaps rather than `n-1`. At `n = 9` the
+sum is 174. The review then uses the still larger per-map ceiling
+`4(n+1)^2`. The gap is an integer:
+
+```text
+4(n+1)^2 - R(n) = (5n^2 + 7n + 6)/2.
+```
+
+It is positive for every positive integer `n`. At `n = 153`,
+
+```text
+R(153) = 35803,    4(154)^2 = 94864.
+```
+
+The review multiplies the square ceiling by its stated map count
+`311304` and obtains `29531542656`, which is below `2^35` and therefore
+below the stated `2^40`. The same map count times `R(153)` is
+`11145617112`, which is below `2^34`. These are comparisons of the
+integers already fixed by the formulas. They do not rederive the map
+count 311304, and they do not change the admitted κ
+`363005817/100000000000`.
+
+## What is not claimed
+
+The algorithm accepts exactly the invertible matrices: every successful run
+ends at `I_n` by invertible steps, and every invertible matrix has a pivot
+at each column. The exhaustive check for `n <= 4` matches `|GL(n, F_2)|`.
+That census is not the proof for larger `n`.
+
+`R(n)` is the exact length of this synthesis on one monomial. Another
+factorization into the same primitives might be shorter. No such search is
+claimed to be exhaustive. Assumption `precision_tape` is not discharged:
+the proof bounds the record list that the retained tape tariff multiplies.
+It does not prove the movement exponent, the storage prescription, or the
+outer threshold calculation.

research/n-axis-monomial-records/README.md

@@ -0,0 +1,139 @@
+# An n-axis monomial elimination uses at most (3n^2+9n+2)/2 records
+
+**Proof, with an exhaustive census for n <= 4. No new κ.** The selected
+conditional value stays `363005817/100000000000`.
+
+## Result
+
+Fix the monomial normal form used for nine axes in the `#4610`
+specialization, and let the axis count be any positive integer `n`.
+Eliminate the invertible binary address matrix by the pivot rule below,
+replace each row swap by three `F_2` row additions, and emit one record
+for each translation bit, each unit of a mod-4 linear phase, each
+off-diagonal controlled sign, and each global factor of `i`.
+
+**Theorem.** This synthesis emits at most
+
+```text
+R(n) = (3n^2 + 9n + 2)/2
+```
+
+elementary records, and there is a monomial for which it emits exactly
+`R(n)`. The argument is in [PROOF.md](PROOF.md).
+
+The column charge is the new step. On column `k`, if `a_k` is the number
+of eliminations and `s_k` is 1 when a swap occurs, then `a_k + s_k <= n-1`.
+Summing and replacing each swap by three additions gives the address
+length `(n+2)(n-1)`. Charging at most `n(n-1)` additions and `n-1` swaps
+separately gives the longer address length `(n+3)(n-1)`.
+
+At `n = 9` the separate-maxima count is the published
+
+```text
+96 + 9 + 27 + 36 + 3 = 171,
+```
+
+while `R(9) = 163`. The value 171 remains a correct sufficient count. It
+does not use the column charge. The operation list in section 6 of the
+`#7000` application review sums to `R(n) + n + 2`, which is 174 at
+`n = 9`, and the review then uses `4(n+1)^2`. At `n = 153` that square is
+`94864` and `R(153) = 35803`. With the review's own map count `311304`,
+the square product `29531542656` is below `2^35`, and the sharp product
+`11145617112` is below `2^34`. The review's comparison `< 2^40` remains
+true. None of these integers changes the admitted κ.
+
+Assumption `precision_tape` is the interface being bounded: the record
+list is the fixed finite template that the retained tape tariff multiplies.
+The assumption is not discharged. The caller is this elimination, which is
+the grammar specialized at `n = 9` and invoked for general `n` by that
+application review. `frontier7000-verify` was not run.
+
+## Evidence classes
+
+The column charge, the closed form, the witness family, and the comparison
+with 171 and with `4(n+1)^2` are a proof for every positive integer `n`.
+The witness check through `n = 64` in the verifier is finite corroboration
+of that one family, not the proof.
+
+Separately, for every matrix in `M_n(F_2)` with `n <= 4`, the algorithm
+accepts a matrix if and only if it lies in `GL(n, F_2)`, never swaps the
+last column, obeys the column charge, attains `n(n-1)` additions on some
+matrix, attains `n-1` swaps on some matrix, and attains the address bound
+on exactly one matrix. That statement is an exhaustive finite census.
+Its domain is finite, the enumeration runs through every bit mask, and the
+acceptance count is checked against the product formula for `|GL(n, F_2)|`.
+It is not a proof for `n > 4`. A failed search is not used anywhere in
+this package.
+
+`R(n)` is exact for this synthesis. It is not proved to be a lower bound
+on every other recipe built from the same primitives.
+
+## Scope and evidence
+
+Catalogue card `formal-interface-lemma`, priority revision 8, base commit
+`e54523517d0f03e58352e647c403a5af3e525a57`. Scope status: **changed**.
+The card asks for a formalized interface lemma. This package does not
+start a proof-assistant development. It answers the all-size request for
+one assumption id, one caller, and one proved proposition: the record
+count above, under `precision_tape`.
+
+Ordered eligible list for this session, after dropping every unpaidmoon
+pull request and fork `cursor/*` branch named in the session brief. The
+revision-8 next-decision table comes first. Catalogue cards that the table
+does not name by id follow, in catalogue order.
+
+1. Complex helpers (`p104-side-correction`, `coverage-law-change`).
+2. BIT helper contract (`bit-helper-contract`).
+3. New decoders and interfaces.
+4. Supplier audit.
+5. All-size audit and formalization.
+6. Verification tooling.
+7. `bit-new-register-model`.
+8. `r437-carrier-integration`.
+9. `complex-rank-shape-decoder`.
+10. `complex-new-helper-inventory`.
+
+Item 5 is this package. It is not a register-model, paired-star, G20, or
+conditional-κ continuation. The original card is copied in
+[TASK.json](TASK.json). Pins are in [SOURCES.json](SOURCES.json).
+
+## Reproduce
+
+Python 3.12, standard library only, from the repository root:
+
+```sh
+python3 -B research/n-axis-monomial-records/verify.py
+python3 -O -B research/n-axis-monomial-records/verify.py
+python3 -B scripts/research_package.py --package research/n-axis-monomial-records --check-only
+python3 -B scripts/research_package.py --package research/n-axis-monomial-records
+```
+
+The verifier prints `PASS_N_AXIS_MONOMIAL_RECORDS`. Checks raise
+`SystemExit`, so optimized mode does not drop them. Not run: Lean, Docker,
+a physical caller, and `make frontier7000-verify`.
+`scripts/research_selected_baseline.py` returned
+`PASS_RESEARCH_BASELINE_BINDINGS_ONLY` and is not a scientific replay.
+
+## Open next questions
+
+- Is `R(n)` a lower bound on every selected-primitive recipe of some
+  monomial, or only the exact length of this elimination? The tariff uses
+  a sufficient count. A matching lower bound would show that this alphabet
+  cannot price that monomial more cheaply. The first step is the `n = 2`
+  witness, whose sharp recipe has 16 records. The selected rewrite system
+  is not a finite search here.
+- Does replacing the review's per-map `94864` by `R(153) = 35803` lower a
+  cutoff integer in section 6 without changing the admitted κ? The review
+  already says those finite constants leave the rank and exponent
+  inequalities unchanged. No isolated cutoff checker is included, and the
+  full admission replay was not run.
+
+## Credit
+
+The nine-axis normal form and the count 171 are Cao Yifan / intqwq,
+PR `#4610`, as recorded in
+`research/final4610-independent-admission/SPECIALIZATION.md`. The loose
+general list and the map count `311304` are the `#7000` application
+review, section 6. The package scaffold is Douglas Colkitt's. Prepared by
+unpaidmoon with substantial Cursor Grok assistance. New work is
+Apache-2.0. No independent human or formal-kernel review is claimed.

research/n-axis-monomial-records/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "input",
+      "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8",
+      "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "docs/research/pr-intake-evidence/pr7000-application/PROOF-REVIEW.md",
+      "usage": "input",
+      "git_blob": "3dd1af2285e597676725e85ad4f65e7ad326d695",
+      "sha256": "4501502c2ceb9759b20372435fe4beb51082c5a5e2910c1fd5dbe6edca415055"
+    },
+    {
+      "path": "research/final4610-independent-admission/SPECIALIZATION.md",
+      "usage": "input",
+      "git_blob": "7ee84b30892f7354e1c36611f1a5e9b082dc6147",
+      "sha256": "70430114f744108223bc1d44b98bc25b696c4b408b7b044c2a8bbdfdb434ac5c"
+    }
+  ]
+}