Prove a moving-frame ternary COPY floor of 14 (no κ)

research/ternary-moving-frame-floor/PROOF.md

@@ -0,0 +1,165 @@
+# Four unrestricted terms cannot beat thirteen ternary lines
+
+## Statement and contract
+
+Let K be any field of characteristic zero. Let P contain the thirteen vectors
+in {-1,0,1}^3 whose first nonzero coordinate is 1, in lexicographic order.
+Let X be the 13 by 3 matrix with those rows and G = X X^T. Define the binary
+13 by 13 matrix B by
+
+```text
+B_st = 1 if s=t or p_s dot p_t=0, and 0 otherwise.
+```
+
+For an exact decomposition G = sum_j u_j v_j^T over K, set R_j = supp u_j,
+A_j = supp v_j, and charge
+
+```text
+C = sum_j rank_F2 B[R_j,A_j].
+```
+
+The factors may leave the evaluation code, use arbitrary characteristic-zero
+coefficients and cancel. Frames are unrestricted. The pairing B and the
+thirteen ports are fixed. No nonnegativity or Gram-factor constraint is
+imposed on the factors.
+
+**Theorem.** Every decomposition with at most four terms has C >= 14.
+Every decomposition with at most three terms has C >= 18. The latter bound
+is attained by the coordinate decomposition. No attainment of 14, or exact
+four-term optimum, is asserted.
+
+The below-thirteen four-term question of Aaron Wang's PR2518 is therefore
+settled negatively for its full-orthogonality pairing. This is a scoped
+mathematical obstruction, with a finite exact rank lemma. It is not a search
+failure, physical decoder construction or complete multiplication theorem.
+
+## 1. The exact restriction-rank lemma
+
+Write E = im X. For 0 <= n <= 13 define
+
+```text
+e(n) = min rank_F2 B[supp(Xa),A],
+       over nonzero a in K^3 and A subset of P with |A|=n.
+```
+
+The exact values, in increasing n, are
+
+```text
+n     0  1  2  3  4  5  6  7  8  9 10 11 12 13
+e(n)  0  1  2  3  3  4  4  5  5  6  6  6  7  7.
+```
+
+Here is a complete finite reduction, including extension fields K. The zero
+ports of Xa are the rational vectors p in P satisfying p dot a = 0.
+If there are at least two, take two distinct zero ports p,q. They are
+linearly independent, and a is a nonzero K-multiple of their rational cross
+product d = p cross q. The zero-port set is exactly that of d. Three
+independent zero ports would force a=0, which is excluded.
+
+If there is one zero port p, choose any other port q. The cross product d
+vanishes at p, so supp(Xd) is a subset of supp(Xa). If there are no zero
+ports, choose any two distinct ports. The same support containment holds.
+Deleting rows cannot increase binary rank. Consequently it suffices to
+check primitive cross products of all 78 unordered port pairs.
+
+After division by the coordinate gcd and a sign change making the first
+nonzero coordinate positive, there are exactly 25 distinct cross products
+and 25 distinct supports. Their support sizes are 9, 10 or 11. The checker
+independently reconstructs these directions from primitive vectors in
+[-2,2]^3 having at least two zero ports. This box is complete because every
+cross-product coordinate is a difference of two products in {-1,0,1}.
+Distinct ports are never proportional, so two zero ports are independent.
+
+For every one of these 25 supports and every one of the 8,192 subsets A,
+the checker computes the binary rank twice, using row elimination with high
+pivots and transposed-column elimination with low pivots. All 204,800
+comparisons agree. Minimizing by |A| gives the displayed table. The generated
+receipt includes an attaining support/subset witness for each entry.
+Every listed direction is rational and hence belongs to K, so these
+witnesses establish equality as well as the lower bounds. In particular,
+every nonzero vector in E has at least nine nonzero entries.
+
+This finite lemma is the only exhaustive premise. The argument below
+quantifies over all decompositions, rather than enumerating frames.
+
+## 2. A code side is forced at four terms
+
+The rows of X include the coordinate vectors, so X has rank three. Direct
+summation also gives X^T X = 9 I_3. Thus G has rank three over K, its column
+and row spaces equal E, and its thirteen columns are pairwise nonproportional.
+The last assertion follows from the injectivity of X and the distinct
+projective representatives p_t, since G[:,t] = X p_t.
+
+Remove every zero outer product, leaving k active terms. Necessarily k>=3.
+Write U and V for the 13 by k factor matrices, so G=UV^T. Both have rank
+at least three. When k=3 both have rank three and both column spaces equal E.
+
+When k=4, U and V cannot both have rank four: U would be injective as a map
+K^4 to K^13 and V^T would be onto K^4, making UV^T have rank four. At least
+one therefore has rank three. Its column space equals E, because it contains
+the rank-three column space of G or G^T. The symmetry of B makes the tariff
+unchanged by transposing the decomposition. We may take the code side to be U.
+
+This permits arbitrary vectors outside E on the other side. It is precisely
+why the result covers moving-frame decompositions beyond a fixed one-extra
+identity family. The rank argument is classical and is consistent with
+joaqcoo's PR1224 one-sided representation context; that general observation
+is not claimed as new.
+
+## 3. Three active terms
+
+For k=3, each nonzero v_j lies in E and has support size at least nine.
+Each u_j is also a nonzero code vector. The finite lemma therefore gives
+rank_F2 B[R_j,A_j] >= min_{9<=n<=13} e(n) = 6. Summing gives C>=18.
+
+The coordinate decomposition uses u_j=v_j=X e_j. Direct evaluation gives
+three tariff ranks of six, so it attains 18. This elementary fixture is
+constructed from the definitions; no predecessor census is replayed.
+
+## 4. Four active terms
+
+Let n_j=|A_j|. Each n_j is between 1 and 13. Each column of G needs at least
+one nonzero coefficient among the corresponding rows of V. If a column uses
+only one term, it is proportional to that term's u_j. Because the thirteen
+columns of G are pairwise nonproportional, each u_j can serve at most one
+such column. At most four columns use only one term; every other column uses
+at least two. Therefore
+
+```text
+n_1+n_2+n_3+n_4 >= 4 + 2*9 = 22.
+```
+
+The restriction-rank lemma gives C >= sum_j e(n_j). Exhausting the 13^4
+ordered size tuples, retaining those with sum at least 22, gives
+
+```text
+min sum_j e(n_j) = 14,
+```
+
+with one attaining relaxation tuple (1,1,7,13). The checker enumerates every
+tuple. This tuple is not asserted to come from an actual factorization.
+For a short direct confirmation, e(n)>=(n+1)/2 for 1<=n<=13, with equality
+only at n in {1,11,13}. A bill below 14 would be at most 13, hence would
+require sum n_j=22 and four equality sizes. Four members of {1,11,13}
+cannot sum to 22. Thus C>=14. Combining with the three-term case proves
+the theorem for every decomposition with at most four terms.
+
+## Scope and credit
+
+Aaron Wang / navinor's PR2518 poses the unrestricted four-term question,
+building on his PR2272 screen. DreamingOfClouds's PR2125, PR2228 and PR2111
+supply the dense-polar/COPY model; Cinna Davis's PR2240 supplies the narrower
+one-extra fixed-frame construction; joaqcoo's PR1224 supplies the retained
+one-sided factorization context. The source packages retain their credit.
+The new result is this complete 25-direction restriction-rank certificate
+and its application to all four-term factorizations on the thirteen ports.
+
+The fixed pairing, characteristic zero and at-most-four-term restrictions
+are essential to the proved scope. Five factors can have both factor
+matrices of rank four, so the forced-code-side argument does not extend
+automatically. Changed pairings, masked identities, shared delivery and
+physical/native/ownership/restoration/compiler/precision/stock/outer costs
+are outside this theorem. No new kappa or selected-frontier change follows.
+Independent human and formal proof-kernel review are unclaimed.
+
+This proof was produced by Nick Petalas. Apache-2.0.

research/ternary-moving-frame-floor/README.md

@@ -0,0 +1,132 @@
+# A moving-frame COPY floor for thirteen ternary lines
+
+Every exact factorization of the Gram matrix on the thirteen projective
+nonzero lines of {-1,0,1}^3 into at most four scalar outer products has
+full-orthogonality binary COPY cost at least **14**. This settles the
+below-thirteen question in Aaron Wang / navinor's
+[PR2518](https://github.com/CrocSwap/integer-mult-bounds/pull/2518), Open next
+question 2. Factors may move freely, leave the evaluation code on one side,
+and use arbitrary coefficients over any characteristic-zero field.
+
+Claim type: scoped written mathematical proof with an exact finite rank
+certificate. The minimum with at most four terms lies between 14 and 18; no claim
+of sharpness at 14 is made. Three terms have sharp cost 18. No new kappa,
+physical decoder, supplier admission or selected-frontier change is claimed.
+This contribution was produced by Nick Petalas. Independent human and formal
+proof-kernel review are unclaimed. Apache-2.0.
+
+[PROOF.md](PROOF.md) gives the full contract and argument. At four terms,
+rank forces one factor side into the three-dimensional evaluation code.
+All code supports reduce to 25 rational intersection directions. Their
+complete restriction-rank envelope, combined with the thirteen pairwise
+nonproportional Gram columns, forces the lower bound. No predecessor
+census or scientific verifier is executed.
+
+## Reproduce
+
+Run from the repository root with the standard library only:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/ternary-moving-frame-floor/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/ternary-moving-frame-floor/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/ternary-moving-frame-floor
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/ternary-moving-frame-floor --check-source-history
+```
+
+Any CPython 3.12 interpreter can replace the absolute local path. The direct
+verifier reads only these six package files, writes nothing and prints a
+generated receipt binding their SHA256 hashes, followed by
+
+```text
+PASS_TERNARY_MOVING_FRAME_FLOOR four_term_cost>=14 three_term_cost>=18
+```
+
+The checker reconstructs the thirteen ports and independently enumerates the
+25 intersection directions. It compares row and transposed-column binary
+elimination on all 25*8192 restrictions. It then enumerates all 13^4 ordered
+support-size tuples. Exact new factorization fixtures include three examples
+whose non-code side has rank four, together with their transposes. The
+coordinate fixture attains the three-term bill 18. Seven rejection controls
+cover a zero direction, rank capacity, omitted direction, changed pairing,
+underpriced envelope, failed scalar identity and excess term count. A
+separate fixture distinguishes characteristic-zero scalar rank from binary
+tariff rank. No enumeration of all coefficient tuples is claimed or needed.
+
+Both normal and optimized registered commands use explicit exceptions, so
+optimization does not disable the checks. The generic runner checks metadata
+and source pins separately. The source-history preflight requires the
+retained Git history; direct mathematical replay needs no Git or network.
+
+## Scope and implementation bounds
+
+The exact pairing has unit diagonal and off-diagonal one precisely when the
+original port vectors are orthogonal. Changed pairings, masked exactness,
+shared-copy prices, other geometries, positive characteristic and five or
+more active factors are not covered. The support relaxation's attaining
+size tuple is not asserted to be a realizable factorization.
+
+The written reduction is a proof over all stated fields and decompositions.
+The finite replay certifies its restriction-rank premise and corroborates
+the algebraic fixtures. It is not a complete multiplication theorem or
+independent human/proof-kernel acceptance. Physical acquisition, delivery,
+native realization, arbitrary dirty-helper restoration, ownership, routing,
+compiler closure, precision, stock, BIT compatibility and the outer bill
+remain unpriced. No selected cold replay, Lean or Docker run was performed.
+
+The standalone verifier has no recursion, subprocesses, network access,
+writes or mutable global cache. Each function is below sixty physical lines.
+Its main exact loop is bounded by 25 directions and 8192 subsets. The size
+loop has 28561 tuples. Matrices have at most 13 rows and 13 columns; factor
+fixtures have at most four terms. The registered command timeout is 120
+seconds. Power of Ten rule 3 has a managed-runtime deviation: CPython
+allocates integer, Fraction and collection objects while running. Live
+mathematical state is bounded by these fixed dimensions, with one current
+restriction retained at a time. Fixed-capacity storage would be required
+for a native steady-operation implementation. The rejection helper has seven fixed local callable targets, a bounded
+Power of Ten rule 9 deviation used only for failure controls.
+Warnings-as-errors execution is the applicable diagnostic check; no external static analyzer is claimed.
+
+## Sources, overlap and family decision
+
+Base main is `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8,
+selected PR6030. [SOURCES.json](SOURCES.json) pins the question README,
+catalogue and selected record as historical provenance. There are no live
+external mathematical inputs. [TASK.json](TASK.json) retains the complete
+card and explains the changed scope. The selected binding baseline passed
+as orientation, without a supplier replay.
+
+The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19362906)
+followed checks of live handoffs, local reservations, open and recent-account
+PRs, all-main README object/formula searches, merged/general-form searches
+and the cached card report. The cached scan covered 406 open PRs and 6355
+Discussion records but only 111 local note records of 8917 HEAD notes.
+Explicit Git searches covered all main README paths for the distinctive
+object and formula terms. Sparse notes, arbitrary historical diffs and
+unpublished work remain coverage limits. This is bounded overlap evidence,
+not a novelty certificate or a literature-priority claim.
+
+Credit Aaron Wang / navinor's PR2518 and PR2272 for the exact open question
+and fixed dense-polar contract; DreamingOfClouds's PR2125, PR2228, PR2111,
+PR446, PR595 and PR1590 for the retained COPY/polar-law model; Cinna Davis /
+1337isnot1337's PR2240 for the fixed-frame one-extra family; and joaqcoo's
+PR1224 for the one-sided factorization context. Rank factorization,
+projective intersections and binary elimination are classical. The new step
+is the complete restriction-rank lemma and its all-moving-frame four-term
+consequence on these thirteen ports. Predecessor results and credit lines
+remain unchanged.
+
+The family decision is to stop this below-thirteen four-term route at its
+algebraic cost gate. An exact cheaper decoder under a changed term count,
+pairing or delivery contract would reopen a different question. A new
+physical construction campaign is not justified by this negative result.
+
+## Open next questions
+
+1. What is the exact minimum with at most four terms, between 14 and 18? First seek a
+   complete exact factorization costing 14 through 17, allowing the other
+   factor side to leave the code. The support-size relaxation alone need
+   not be realizable.
+2. Can five terms beat thirteen with this pairing? First specify the two
+   rank-four factor spaces and enforce a rank-three product. Neither side
+   must then equal the evaluation code, so the present reduction is not a
+   five-term exclusion.

research/ternary-moving-frame-floor/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/polar-law-t7-overcomplete-screen/README.md",
+      "usage": "provenance",
+      "git_blob": "3d7a42855310f5251452bdb003300275b538efc3",
+      "sha256": "ed9c61d8616fa4bc86a9d28d66f49aa774ef25fe56a4e3c895b69bf784e7880f"
+    }
+  ]
+}