Solve the exact mixed UT4 coefficient relaxation (no new κ)

research/ut4-mixed-relaxation-optimum/PROOF.md

@@ -0,0 +1,139 @@
+# Exact mixed middle-factor optimum
+
+Work over F2. Let S,T,H be diagonal r by r matrices. Every diagonal triple
+(s_i,t_i,h_i) is either zero or one of the seven nonzero binary triples.
+Let E be the coordinate subspace on the d nonzero triples, and let k count
+the pure-central triples (0,0,1). Consider finite n and matrices
+
+    X,U : F2^n -> F2^r,       Y,V : F2^r -> F2^n
+
+with all X columns and all Y rows nonzero, E contained in im X and in the
+row space of Y, and
+
+    XY=0, UY=S, XV=T, UV=H.                         (1)
+
+The exact minimum is
+
+    n_min = 2d+k+[d=k=1].                          (2)
+
+For d=0 the empty factorization attains zero. The written theorem permits
+all finite r and d. The executable constructor is deliberately bounded to
+64 active roles and two additional dirty identity roles.
+
+This is an exact necessary coefficient relaxation. A column gives a nonzero
+rank-one middle coupling x_j y_j^T, but U and V need not come from preceding
+and following paid chronological paths. No formal group-algebra word follows.
+
+## Lower bound, credited premise restated
+
+This is the mixed quotient argument from Nick Petalas #2175, using the
+mixed active-span constraints from Gareth Davidson #2027 and ToikY #1662's
+central quotient method. It is restated to specify the solved optimization,
+not claimed as a new lower bound.
+
+Let pi delete output coordinates where S has a one. Restrict the input to
+ker T. Since XV=T, V(ker T) lies in ker X. Since UY=S, pi U annihilates
+im Y. Since XY=0, im Y is contained in ker X. Therefore pi H restricted
+to ker T factors through ker X/im Y. Its rank is exactly k, as the only
+surviving diagonal ones have s=t=0 and h=1. Thus
+
+    k <= n-rank X-rank Y <= n-2d.
+
+At d=k=1, n=3 would force both ranks to equal one. Over F2 all nonzero
+X columns are the same vector x and all nonzero Y rows the same row y.
+Then XY=3xy=xy is nonzero, a contradiction. Thus n>=4 in that case.
+This binary exceptional case is inherited from ToikY #1662.
+
+## New step: mixed blocks attain the lower bound
+
+Direct sums preserve all four equations, nonzero columns and rows, and the
+active-span constraints. The task is therefore to allocate small blocks
+without paying a four-column singleton for an isolated pure-central role.
+
+For a single noncentral triple (s,t,h), use X=Y^T=(1,1). Choose two-entry
+binary rows U and V^T with sums s and t and dot product h. Such rows exist
+whenever (s,t) differs from (0,0): if s=1 choose U=(1,0) and V=(h,t+h);
+if s=0,t=1 choose V=(1,0) and U=(h,h). This costs two columns.
+
+The following new five-column blocks pair one pure-central coordinate with
+any one of the six noncentral coordinates. Encode a two-vector (a,b) by
+a+2b. In every row of this table set
+
+    X columns = (1,1,1,2,3), Y rows = (1,1,2,2,2).
+
+The targets are S=diag(0,s), T=diag(0,t), H=diag(1,h).
+
+| (s,t,h) | U columns | V rows |
+| --- | --- | --- |
+| (0,1,0) | (0,0,1,0,1) | (0,1,0,3,1) |
+| (0,1,1) | (0,0,1,2,3) | (0,1,0,3,1) |
+| (1,0,0) | (0,0,1,0,3) | (0,1,1,0,0) |
+| (1,0,1) | (0,0,1,0,3) | (0,1,3,2,2) |
+| (1,1,0) | (0,0,1,0,3) | (0,1,1,2,0) |
+| (1,1,1) | (0,0,1,0,3) | (0,1,3,0,2) |
+
+Each equality in (1) follows by adding the five outer products over F2.
+Both X and Y have rank two and no zero column or row. This is a finite
+algebraic table, not a search failure or a chronological witness. #2175's
+single z/uz fixture already establishes one member's attainability. We use
+its X and Y and supply a uniform table for all six partner labels. Neither
+that existing special case nor its lower bound is new credit here.
+
+For completeness the pure blocks below are ToikY #1662's construction.
+For two pure-central coordinates take X=Y^T with columns
+(1,1,2,2,3,3). For three take columns (1,2,3,4,5,6,7,1,1).
+In both cases XX^T=0, X has full row rank q, and n=3q. The q-dimensional
+quotient ker X/im X^T has a basis. Take representatives as the columns of V,
+and take U to be their dual functionals, vanishing on im X^T and extended
+to the ambient space. Then (1) holds with S=T=0 and H=I_q.
+The executable independently constructs representatives and duals by bounded
+binary elimination. It does not import or run a predecessor program.
+
+Now allocate the roles. If k=0, use noncentral singletons. If k>=2, write
+k as a sum of twos and threes, use the inherited pure blocks, and use
+noncentral singletons for the rest. This costs 3k+2(d-k)=2d+k.
+If k=1 and d>=2, use one new five-column mixed block and d-2 noncentral
+singletons, for 5+2(d-2)=2d+1 columns. If d=k=1, the inherited four-column
+fixture is X=Y^T=(1,1,1,1), U=(1,0,0,1), V=(1,0,1,0)^T.
+Zero-padding and simultaneous coordinate permutation place every block on
+its original coordinates and preserve arbitrary identity-role coordinates.
+This proves (2) for every finite diagonal target family.
+
+## Consequence and limits
+
+No strengthened mixed-root lower bound can follow from precisely (1), these
+two span constraints, and the nonzero coupling restrictions alone. They are
+already attained at 2d+k except for the inherited one-role exception. Any
+stronger formal-word bound must retain further chronological or coefficient
+information, or another constraint omitted from this relaxation. This does
+not exclude stronger methods and does not decide any remaining UT4 word cost.
+
+The pure-central endpoint, quotient/spans and single mixed fixture are
+predecessor work. The contribution is the six-partner mixed construction
+and its uniform allocation theorem, closing the general mixed relaxation.
+No literature-priority claim is made for rank-nullity, direct sums or dual bases.
+
+## Verification and code bounds
+
+The checker multiplies the four binary matrices directly, checks all nonzero
+couplings, both exact active spans, the formula and every zero-padded coordinate.
+It exhausts all seven-label sequences through four active roles, then covers
+larger mixed multiplicities and the 64-role boundary. A separate scalar census
+enumerates every U,V through four columns to recover all seven scalar minima.
+Semantic controls alter a mixed coefficient, delete a column and exchange the
+target coordinates. Invalid labels, Boolean integers and out-of-range requests
+reject. Normal and optimized execution use explicit exceptions, not assertions.
+
+All loops have finite bounds. The largest construction has at most 192 columns
+and 66 role coordinates. Pure-block searches enumerate at most 512 vectors;
+the exhaustive family domain is fixed at d<=4. Functions remain below 60 lines.
+Python and its standard library allocate dynamically; this is a documented
+managed-runtime deviation from fixed allocation. Bounded input dimensions bound
+the live mathematical arrays. No recursion, generated code or network is used.
+Strict Python warnings are enabled in registered commands. No separate static
+analyzer or proof kernel is claimed.
+
+This contribution is produced by Nick Petalas. Credit ToikY, Gareth Davidson,
+Nick Petalas, Aaron Wang, Josie Elliston, steph4n-gh, Arham Tahir, Hanson Sun,
+and the retained formal register-model lineage in the pinned sources.
+Apache-2.0. Independent human and formal proof-kernel review are unclaimed.

research/ut4-mixed-relaxation-optimum/README.md

@@ -0,0 +1,81 @@
+# Exact mixed-root UT4 middle-factor relaxation
+
+A scoped all-size proof determines the exact necessary coefficient-relaxation
+minimum for every diagonal mixture of UT4 u/v/z targets:
+
+    n_min = 2d+k+[d=k=1],
+
+where d counts active coordinates and k counts pure-central coordinates.
+The new step pairs a lone pure-central coordinate with any noncentral partner
+in five columns. Together with credited predecessor blocks, this attains the
+mixed lower bound uniformly. The full statement and six explicit blocks are
+in [PROOF.md](PROOF.md).
+
+This is a sharp limit of the declared four-matrix relaxation, not a paid
+chronological word. Stronger word bounds need further coefficient or chronology
+information. No physical supplier, new kappa or selected-frontier change is claimed.
+
+## Credit and relation to earlier work
+
+This contribution is produced by Nick Petalas. ToikY's
+[PR1662](https://github.com/CrocSwap/integer-mult-bounds/pull/1662) already solves
+the pure-central relaxation. Gareth Davidson's
+[PR2027](https://github.com/CrocSwap/integer-mult-bounds/pull/2027) supplies the
+mixed-root span unions and asks about mixed pure-central targets. Nick Petalas's
+[PR2175](https://github.com/CrocSwap/integer-mult-bounds/pull/2175) supplies the
+mixed 2d+k lower bound and one z/uz fixture. Those results are credited premises,
+not replay or audit deliverables. The new result uniformly attains the mixed
+relaxation, including every one-pure-central partner type.
+
+The pinned proofs retain the complete register-model lineage. Apache-2.0.
+Independent human and formal proof-kernel review are unclaimed.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/ut4-mixed-relaxation-optimum/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/ut4-mixed-relaxation-optimum/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/ut4-mixed-relaxation-optimum
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/ut4-mixed-relaxation-optimum --check-source-history
+```
+
+Any CPython 3.12 path may replace the local interpreter path. Normal execution
+is read-only and prints `PASS_UT4_MIXED_RELAXATION_OPTIMUM`. The registered hook
+runs both normal and optimized checks. RESULT.json is generated from scientific
+outputs and SHA256 hashes of package files and pinned live proofs. Explicit
+`--emit NEW_PATH` writes an external receipt and refuses an occupied path.
+
+Local exact checks cover 5,602 exhaustive mixed/padded fixtures through four
+active roles, 1,098 larger fixtures through 64 roles, all seven scalar minima,
+15 independently multiplied block templates with 176 entries, and eight
+rejection controls. The universal statement rests on the written proof.
+
+The generic card's historical first command, `scripts/research_baseline.py`,
+fails at `KeyError: 'bit_lower'` on the selected record. This unrelated source
+orientation failure was recorded; no shared code or selected record was changed.
+The selected review and source manifest were read directly.
+
+## Limitations
+
+The proof is quantified over every finite diagonal family and dirty identity
+extension. The executable constructor supports at most 64 active roles and two
+dirty coordinates. All four equations and active-span restrictions are necessary
+conditions, so an attaining fixture is not a formal operator construction.
+Physical address realization, native/compiler, hosting, precision/tape, actual
+paid paths and outer transfer remain unrun obligations. No selected cold replay,
+Lean build, independent human acceptance or formal verification is claimed.
+
+## Open next questions
+
+1. Which additional chronological equation gives a stronger mixed-family bound?
+   Start with one pure-central and one u target, impose actual prefix/suffix
+   paths on the five-column table, and charge all outer calls. The present
+   relaxation deliberately omits these paths.
+2. Can the larger mixed families' complete paid tariffs be characterized?
+   Start with a named target outside the existing z/uz weighted region, retaining
+   all formal coefficients and arbitrary dirty restoration. Relaxation attainment
+   alone does not establish an upper word or its tariff.
+
+Structured questions and exact source pins are in TASK.json and SOURCES.json.

research/ut4-mixed-relaxation-optimum/RESULT.json

@@ -0,0 +1,18 @@
+{
+  "columns_in_exhaustive_fixtures": 46022,
+  "dense_entries": 176,
+  "dense_templates": 15,
+  "exhaustive_mixed_fixtures": 5602,
+  "larger_fixtures": 1098,
+  "rejection_controls": 8,
+  "scalar_labels": 7,
+  "source_sha256": {
+    "PROOF.md": "04c4c2b99aee384e6c02626eb794eaf15b735bb5046a5d62cd1d92fad8583952",
+    "README.md": "5fdff565b3483aa121ee112efcd2699362708c4af00ad5cb5f9a33676bd26089",
+    "SOURCES.json": "f47516a3aa1ecc43109611aa403a7fdce1fff4aa4f094ad7f1a6edada1b99b52",
+    "TASK.json": "ead7f0289c238bf0fa1093b103f8e4987134ef700e3f731cf2287cb53feca136",
+    "VERIFY.json": "0c5d313f390291aa442be22a5fb73aefffc9c5ea81a37497cb6dfd43ac049316",
+    "verify.py": "da320b4bcd3ef9393d27d585b77ab5565ce0fc3533f8a807546ac76a31b9a5cd"
+  },
+  "transcript_sha256": "6fbda0ece976154c38094411f2256ef868f49ba7b7dbdca3252824da84ca4b6a"
+}

research/ut4-mixed-relaxation-optimum/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/ut4-central-tariff-relaxation/PROOF.md",
+      "usage": "input",
+      "git_blob": "8137274359979a786568da60bc802eeba2728e7f",
+      "sha256": "4820f0771cc6d5828492bf8cb0bacda2a74d3f00b58a02b8df056ab1db040f21"
+    },
+    {
+      "path": "research/ut4-mixed-central-middle/PROOF.md",
+      "usage": "input",
+      "git_blob": "e6a7c24d20c7718989a2b00e97ef9638f7804226",
+      "sha256": "34a5dc532b9010b5e8afd67273a9d4b1cf17e1362f5f432c4b433581cc7784d5"
+    },
+    {
+      "path": "research/ut4-mixed-root-tariffs/PROOF.md",
+      "usage": "input",
+      "git_blob": "633a7d5137ad13fafe719cc042099977ad1f96e5",
+      "sha256": "c0def58338a69a57ac95f1d32a744993aa07656c46eba88a99354b276917bd8e"
+    }
+  ]
+}