Reduce the concrete nonunit handoff allowance to 232 (no κ)

research/p104-double-preconditioned-handoff/CODE-BOUNDS.md

@@ -0,0 +1,38 @@
+# Implementation bounds
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+The executable domain is the two fixed dual pairs, one fixed source word and
+one constructed handoff. No discovery search runs during verification.
+The two new Python files use structured control flow without recursion.
+Boundary programs have at most six events, boundary matrices have at most
+five coordinates and inverse checks have at most twelve events. All proof
+checks use explicit exceptions and remain enabled with `-O`.
+
+The complete word is bounded below 26,000 events with 744 formal coordinates,
+a fixed source-frame catalogue and eight owned slots. The retained engines
+enforce their source-specific operation, coordinate, frame and coefficient
+contracts. Boundary controls perform eleven omission checks and two order
+checks; whole-word controls perform exactly eight replays. Source inventory
+has four entries. Both registered commands have 120-second timeouts.
+
+Managed Python and `Fraction` allocate during execution. This is a documented
+deviation from fixed allocation; the finite dimensions, event counts and
+coefficient domain bound the live state. No fixed-memory implementation or
+measured peak allocation is claimed. One mutated word is replayed per control;
+the finite input sizes also bound temporary copies.
+
+Authenticated predecessor code is compiled directly from bytes into three
+explicit module names. This deliberate dynamic-loading deviation avoids stale
+bytecode reads. `completion.py` is loaded the same way. The handoff constructor's
+in-memory `basis` function is replaced once with the new explicit program.
+The four dependency hashes are checked before any predecessor code executes.
+No predecessor file, module source or receipt is changed. Their existing
+implementation choices remain source-specific dependencies, not a new claim
+of compliance or an unrelated refactoring target.
+
+Each new function is below 60 physical lines. Strong runtime contracts,
+warning-strict normal and optimized execution, source compilation and whitespace
+checks cover the touched code. Python's standard library supplies no static
+type checker; no additional installed linter or proof kernel is assumed.
+Receipts are generated on stdout and include hashes of package and input files.

research/p104-double-preconditioned-handoff/PROOF.md

@@ -0,0 +1,135 @@
+# Ordered cancellation in the concrete dual pairs
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+The dual pairs and column-unit formula are CubeJerry's PR6322, extending
+unpaidmoon's PR6297 and Ali Romman's PR5611/5602. The new construction below
+uses their exact scalar boundary contract.
+
+## The two noncommuting preconditioners
+
+Let `p=596`, and let `e_i` be a coordinate column. Work over `Z[1/2]`.
+Retain the row and two columns
+
+```
+a = (5/16)e592^T + (5/16)e593^T + (5/8)e594^T + (3/8)e596^T,
+u = -e592 + e593 + e594 + e596,
+b = -e188 + u.
+```
+
+Both pairings `a u` and `a b` are one. These are boundary functionals and
+directions, not assumed values of dirty registers.
+
+Set
+
+```
+S1 = I + e592 e593^T,
+S2 = I + (1/2)e594 e592^T,
+S  = S2 S1.
+```
+
+Each shear fixes `e_p` and is invertible by negating its coefficient.
+They do not commute: the product of the second nilpotent part with the first
+is `(1/2)e594 e593^T`, whereas the reversed product is zero.
+
+First applying `S1` to either column cancels its 592 coordinate. Consequently
+`S2` changes no column coordinate afterward. For `d` equal to `u` or `b`,
+
+```
+d' = S d = d + e592.
+```
+
+For the row, `S1^-1` cancels coordinate 593. The next right multiplication
+by `S2^-1` cancels coordinate 592, since `(5/16) - (1/2)(5/8) = 0`.
+Therefore
+
+```
+a' = a S^-1 = (5/8)e594^T + (3/8)e596^T.
+```
+
+The pivot coordinate of `d'` is still one and `a'd'=1`. Apply PR6322's
+column-unit formula to get `R'` satisfying `a'R'=e_p^T` and `R'e_p=d'`.
+Explicitly its first operation is `x596 -= (5/8)x594`, followed by the
+unit injections from 596 to the nonpivot support of `d'`.
+
+Put `R=S^-1 R'=S1^-1 S2^-1 R'`. Then
+
+```
+a R = a' R' = e_p^T,
+R e_p = S^-1 d' = d.
+```
+
+Thus the two inverse preconditioners must execute after `R'`, in the
+order `S2^-1`, then `S1^-1`. This order is proof-relevant. Every factor is an
+invertible coordinate ADD on arbitrary inputs.
+
+## Literal programs and complete tariff
+
+The source completion is the following six ADDs at frame 3:
+
+```
+x596 -= (5/8)x594
+x188 -= x596
+x593 += x596
+x594 += x596
+x594 -= (1/2)x592
+x592 -= x593
+```
+
+The cut completion at frame 1053 omits only `x188 -= x596`.
+The inverse of either completion reverses the list and negates every
+coefficient. No SCALE, spare role, initialized register or new transport is
+needed by these completions.
+
+For a reduced dyadic `c=n/d`, the retained scalar ADD allowance is
+`A(c)=2(3+floor(log2|n|)+popcount(|n|)+log2 d)`. Hence
+
+```
+A(1) = 8,   A(1/2) = 10,   A(5/8) = 20.
+source completion = 20 + 3*8 + 10 + 8 = 62,
+cut completion    = 20 + 2*8 + 10 + 8 = 54,
+all four boundaries = 2*(62+54) = 232.
+```
+
+Inverse costs are identical because the tariff is insensitive to the sign.
+All coefficients and inverse coefficients satisfy the retained
+`|c|+1 < 2^16` bound. There are `2*(6+5)=22` ADDs. PR6322 already proves
+that count minimal for these separately completed boundary maps, with arbitrary
+ancillary roles. Its ADD lower bound is cited, not independently re-proved or
+replayed here. No weighted optimum follows from it.
+
+## Whole-word application and claim boundary
+
+Use the same historical PR5580 source, cut 13762, pivot 596 and frames
+`3 < 1053 < 127` as PR6297/6322. Let `P` and `Q` be its prefix and suffix,
+let `W=QP`, and let `R_s`, `R_c` be the new source and cut completions.
+The retained constructor checks the exact prefix/suffix equations
+`vP=a` and `Qu=b` and the availability of all cut operands before inserting
+the new programs. They give
+
+```
+e_p^T R_c^-1 P R_s = v P R_s = e_p^T,
+R_s^-1 Q R_c e_p = R_s^-1 Q u = e_p.
+```
+
+Retire the original arbitrary pivot input at the cut and continue with a
+fresh arbitrary input `z`. The output becomes
+`R_s^-1 W R_s x - e_p x_p + e_p z`.
+The source basis acts only on the independent `(3,127)` helper group, where
+`W` is identity, and commutes with the main shear. Thus this equals
+`W x - e_p x_p + e_p z`, with retired output `x_p`. Both input freedoms are
+preserved. This is the credited coupled-handoff argument applied to the new
+boundary maps, not a new general handoff theorem.
+
+The new word has 25,162 events, 736 public inputs and eight owned lifetimes
+with peak one. Complete scalar allowance is `217428+232=217660`, using the
+predecessor's source allowance as a comparison premise; both exact arithmetic
+engines freshly enumerate the new word's complete allowance and endpoints.
+They check all 744 formal columns and 553,536 coefficients. Paid profile is
+`{1:2211,2:459,3:494,4:94,5:164,6:18,7:14}` and productive helper profile is
+`{4:84,5:6,8:15,9:423}`, as in the predecessor handoff.
+
+This proves a legal scalar construction and its finite invoice, without a
+new recursive moment, kappa or selected-frontier claim. No weighted optimum,
+current-word transfer, native/caller admission, rounded precision/tape bound,
+stock or uniform compiler proof is supplied. All five selected framework
+assumptions remain. Independent human and formal proof-kernel review are unclaimed.

research/p104-double-preconditioned-handoff/README.md

@@ -0,0 +1,86 @@
+# A 232-unit nonunit helper handoff
+
+Two ordered preconditioners reduce the concrete PR6322 handoff to **22 ADDs
+and scalar allowance 232**. This saves 40 allowance units against its
+26-ADD, 272-unit alternative, and 48 against its 22-ADD, 280-unit construction.
+The complete new local word has 25,162 events and allowance 217,660.
+
+Claim type: scoped algebraic construction with exact finite corroboration.
+The 22-ADD count matches the predecessor's proved minimum for four separately
+completed boundaries. No weighted optimum or new kappa is claimed.
+
+The change answers [PR6322](https://github.com/CrocSwap/integer-mult-bounds/pull/6322)
+Open next question 2 for its exact historical dual pairs. Its elementary
+column-unit formula is a premise. The new step is the ordered pair of
+preconditioners, their cheaper explicit completion and its whole-word use.
+See [PROOF.md](PROOF.md) and [completion.py](completion.py).
+
+## Scope and evidence
+
+The constructor retains 736 independent public inputs, eight owned lifetimes,
+peak owned storage one, the rank-9 to rank-5-plus-rank-4 split and the complete
+paid profile. Two retained arithmetic engines check the **new** word on all
+744 formal columns, including 553,536 endpoint coefficients. One uses rational
+sparse rows and the other integer rows with binary denominators. Both are
+checks using credited predecessor implementations.
+
+The verifier checks both boundary equations and their full inverses. It rejects
+all eleven single forward-boundary gate omissions, both reversals of the
+preconditioner order and eight whole-word coefficient, chart, ownership or
+boundary faults. Its computed stdout receipt includes all source and package
+hashes plus the deterministic candidate-word hash. It writes no receipt or
+word into the checkout.
+
+[SOURCES.json](SOURCES.json) pins the four live inputs at canonical main
+`7c49fe32c55de02c2c873655c804b16e4c3fef0a`. This includes the original PR5580
+word, Ali Romman's handoff constructor and primary scalar checker, and
+CubeJerry's second arithmetic implementation. No predecessor scientific suite
+is replayed as the deliverable. The bounded discovery search stopped when this
+first reduction appeared; no exhaustive search conclusion is asserted.
+
+The selected record and all five framework assumptions remain unchanged.
+This is a historical scalar boundary improvement. Native phase/implementation,
+complete physical caller, stock, rounded precision/tape, compiler closure and
+outer admission are unrun or inherited. The recursive paid and target profiles
+are unchanged, so the scalar saving supplies no exponent gain. There is no
+complete multiplication theorem or independent human or proof-kernel review.
+
+## Reproduce
+
+From the contribution checkout root, with Python 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/p104-double-preconditioned-handoff/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/p104-double-preconditioned-handoff/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p104-double-preconditioned-handoff
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p104-double-preconditioned-handoff --check-source-history --check-modes
+```
+
+Another CPython 3.12 executable can replace the local interpreter path.
+Expected markers are `PASS_P104_ORDERED_HANDOFF inserted_events=22
+inserted_allowance=232`, `PASS_REGISTERED_RESEARCH_PACKAGE` and
+`PASS_RESEARCH_COMMIT_BYTES`. Registered normal and optimized commands have
+120-second bounds. [CODE-BOUNDS.md](CODE-BOUNDS.md) records implementation limits.
+
+## Open next questions
+
+Can allowance fall below 232 under these same boundary equations? A
+coefficient-sensitive lower bound, including both inverses, would decide whether
+this construction is optimal. The existing ADD-count bound does not do so.
+
+Does a current source word retain a compatible nonunit handoff? First extract
+its exact prefix/suffix pair and available charts. Changed helper boundaries
+and the complete native/caller bill block transfer of this historical saving.
+Structured questions and the narrowed card scope are in [TASK.json](TASK.json).
+
+## Credit
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+CubeJerry PR6322 supplies the dual pairs, column-unit construction, ADD-count
+minimum, lower-allowance alternative and separate arithmetic checker.
+unpaidmoon PR6297 supplies the original concrete nonunit split. Ali Romman
+PR5611/5602 supplies dyadic completion and the coupled handoff contract.
+The retained source word and checker credit David Arias, Cinna Davis,
+Gareth Davidson, Ali Romman and their P104/native/controller predecessors.
+Their files and credit lines are unchanged. Elementary shears and the
+rank-one handoff identity are classical or credited predecessor work.

research/p104-double-preconditioned-handoff/SOURCES.json

@@ -0,0 +1,60 @@
+{
+  "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/p104-coupled-helper-bases/construct.py",
+      "usage": "input",
+      "git_blob": "ef5936ca89d6502d7f6af1ce6903d8500c117401",
+      "sha256": "2360066b0a1390c60a86d9788ada1504478e7e48bbfe3fcdf27a5563379fc001"
+    },
+    {
+      "path": "research/p104-coupled-helper-bases/inputs/pr5580-WORD.json.gz",
+      "usage": "input",
+      "git_blob": "9434855e7dad0d0236d23210b3e71a2b83a9ae64",
+      "sha256": "b2a98c4bd0dbe86c09e9d15ee060dcf1aab09dbef90aa1e2127676f4039f406b"
+    },
+    {
+      "path": "research/p104-coupled-helper-bases/local.py",
+      "usage": "input",
+      "git_blob": "9556e86744e18efdd76263a36664830c695f1c0f",
+      "sha256": "5f0678c768544517780d3511995faf0d7062748e7e780c0adb5c4d9c2749a925"
+    },
+    {
+      "path": "research/p104-unit-column-handoff/ALTERNATIVE-PROOF.md",
+      "usage": "provenance",
+      "git_blob": "c6eeb859855b06137ce3a5e85328ad33f7f54e99",
+      "sha256": "ee7a4afdefa422e0eaf541e5142022657dcc33b1c7789260d8c5bcd420d1aba6"
+    },
+    {
+      "path": "research/p104-unit-column-handoff/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "ab3c84e294623fae18b82e7812cc54d0d31c546f",
+      "sha256": "3ed7f534b6e557597529b076ca683a689bf12439338fb5d06f3d27171dad5da7"
+    },
+    {
+      "path": "research/p104-unit-column-handoff/README.md",
+      "usage": "provenance",
+      "git_blob": "cae720d43e04c223dbddc459f8652df5fe6d6467",
+      "sha256": "4013fecd9229678970fb759a0e14f4467c585801be51ebfbe0f1e1c3b8a712e9"
+    },
+    {
+      "path": "research/p104-unit-column-handoff/independent.py",
+      "usage": "input",
+      "git_blob": "3bc5528b21fa65a51243c3260caebbcfae188fb4",
+      "sha256": "f7a76321beb92dbd1151e59092b17e2240d7a3037bc6e90f10b8ba2b31ee5b6a"
+    }
+  ]
+}