Complete dyadic helper bases without an individual unit pivot

research/dyadic-helper-basis-completion/PROOF.md

@@ -0,0 +1,77 @@
+# Complete dyadic basis construction
+
+Let D = Z[1/2]. Let a be a row and b a column in D^n, with a b = 1.
+For any index p there is an invertible R over D such that a R = e_p^T
+and R e_p = b. The compiler emits R as ordinary ADDs with coefficients
+in D and SCALEs by units of D. All operations use the same physical chart.
+This is an application of the Euclidean algorithm, not a new theorem about
+principal ideal domains. Nick Petalas used Euclidean row preparation in
+[PR5115](https://github.com/CrocSwap/integer-mult-bounds/pull/5115)
+for a single-hub shear. Here both the row and column are prescribed.
+
+First clear all denominators of a by a common power of two, d. Each
+column scaling is invertible over D. Apply the integer Euclidean algorithm
+to coordinate p and each other coordinate. An ADD and a swap perform
+one division step. The nonzero pivot becomes the gcd g of the integer
+coordinates, up to sign. Because a b = 1, every odd prime divisor of g
+would divide 1 in D. Thus g has no odd prime divisor. It is a unit in D.
+A final unit scaling gives a P = e_p^T. Each operation used to construct
+P is invertible over D. The loop terminates because each Euclidean
+remainder has smaller absolute value than its divisor.
+
+Set c = P^-1 b. Then c_p = a b = 1. The shear
+
+```text
+S = I + (c - e_p) e_p^T
+```
+
+is a product of ADDs on rows other than p. It satisfies S e_p = c and
+e_p^T S = e_p^T. Set R = P S. Then
+
+```text
+a R = e_p^T,       R e_p = b.
+```
+
+Execution order is S followed by the reverse order of the right factors
+of P. The compiler records this order explicitly. Its inverse uses the
+reverse instruction list, with negative ADD coefficients and inverse
+SCALE coefficients. No odd division, extra field, native MOVE or owned
+zero is required. Scalar coefficients remain outside the tensor power.
+Thus the identity holds for whole fields at every positive tensor width.
+
+The pinned PR5602 constructor requires some a_i to be a dyadic unit.
+That condition is sufficient but unnecessary. For example,
+
+```text
+a = (3, 5),       b = (2, -1)^T,
+R = [[2, 5], [-1, -3]],       det(R) = -1.
+```
+
+Both identities hold. Neither entry of a is a unit. More generally,
+completeness depends on the ideal generated by the row, not on any one
+entry. The supplied b proves that this ideal is D. A rational pair whose
+coefficients have odd denominators is outside this arithmetic contract.
+
+## Exact caller boundary and limits
+
+The two uses in PR5602 are the input/output helper basis and the common
+cut basis. Its handoff proof needs only the two displayed identities,
+invertibility and common charts. This compiler supplies those algebraic
+requirements for all dyadic dual pairs. It does not find the prefix/suffix
+kernels, prove that a cut exists, change a frame or add a productive target.
+The source's nine witnesses supply 18 concrete interfaces. The verifier
+checks all 18 with a separate dense matrix interpreter.
+
+An emitted ADD with a large coefficient is not free. A consumer must
+check the source's coefficient bound, total scalar allowance, prefix growth,
+operation count and fixed-tape costs before installation. This package does
+not replace the source constructor or rerun its physical caller, native
+phases, compiler or outer proof. It does not increase complete kappa or
+change the selected frontier. The five inherited assumptions stay open.
+
+The finite tests corroborate the algorithm and find implementation errors.
+The argument above establishes the all-input statement. Neither the tests
+nor this paper proof are proof-assistant or independent human acceptance.
+
+Ali Romman with substantial OpenAI Codex assistance. Apache-2.0.
+Credit the PR5599/5602 helper handoff and all retained P104 predecessors.

research/dyadic-helper-basis-completion/README.md

@@ -0,0 +1,67 @@
+# Complete the dyadic helper-basis constructor
+
+This enabling algorithm removes the unit-entry restriction in the
+[PR5602](https://github.com/CrocSwap/integer-mult-bounds/pull/5602) helper
+basis constructor. For every dyadic row a and column b with a b = 1,
+[basis.py](basis.py) emits ADD and unit SCALE operations for R with
+`a R = e_p^T` and `R e_p = b`. The pair `(3,5)` and `(2,-1)` is legal
+but has no unit row entry. The old sufficient test rejects it.
+
+The [proof](PROOF.md) gives the complete construction. The
+[replay](verify.py) uses a separate dense matrix interpreter and checks all
+18 basis interfaces from the source's nine handoffs. It also checks every
+integer dual pair in `[-5,5]^2` at both pivots: 616 compilations, including
+16 primitive pairs omitted by the old test. Another 96 presentations cover
+dimensions 1 through 12 and dyadic fractions. Five invalid-input controls
+and an operation-sign control reject their defects. [RESULT.json](RESULT.json)
+is the exact receipt. [SOURCES.json](SOURCES.json) pins all consumed inputs.
+
+This is a complete constructor for one algebraic interface. It does not
+find a new physical helper channel. Complete kappa is unchanged. Consumers
+must charge the emitted scalar operations and recheck growth, operation
+count, native maps, ownership, the physical caller and the full invoice.
+The complete selected replay was not run: orientation read the selected
+record and its promotion proof; its sparse source closure is not present.
+
+## Reproduce
+
+Python 3.12 and the standard library suffice. From the repository root:
+
+```sh
+python3 -B scripts/research_package.py --package research/dyadic-helper-basis-completion
+```
+
+Normal and optimized commands must print `PASS_DYADIC_HELPER_BASIS_COMPLETION`.
+The launcher must print `PASS_REGISTERED_RESEARCH_PACKAGE`. The scientific
+checker does not call Git or the network. Export the package with its three
+declared source files. A source hash mismatch fails before the checks.
+
+## Scope and credit
+
+Base: canonical main `d7633ce230196a1d5d061347de7a0fd8be512ed6`, priority 7.
+The three source files equal PR5602 head
+`6c224aa720203c4f4615e6538d8038a275387db8`. The
+[claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/5125#discussioncomment-19184390)
+is separate from the active different-carrier and word-reassociation searches.
+Remote overlap pagination was complete at 22:17 UTC; local notes are sparse.
+No exhaustive novelty claim is made.
+
+Ali Romman's [PR5599](https://github.com/CrocSwap/integer-mult-bounds/pull/5599)
+and PR5602 supply the helper handoff, source witnesses and compiler interface.
+Nick Petalas's [PR5115](https://github.com/CrocSwap/integer-mult-bounds/pull/5115)
+already uses Euclidean row preparation for a different single-hub shear
+contract. Its [proof](https://github.com/CrocSwap/integer-mult-bounds/blob/391355b8e537b82cedabd45af509177496e7a7a6/research/dyadic-rankone-borrowing/README.md)
+is related prior work. The present interface prescribes both a row and a
+column. It does not claim row preparation as new. The Euclidean method is standard. The P104/native/controller/compiler lineage
+retains its source credit; it is not re-proved here. New implementation,
+interface proof and checks: Ali Romman with substantial OpenAI Codex assistance.
+Apache-2.0. No independent human or formal-kernel acceptance is claimed.
+
+## Open next questions
+
+Use the complete constructor in the current cut search only after checking
+live overlap. First test whether a previously rejected dual pair gives a
+new physical target. Then charge the emitted scalar work and growth and
+rerun the complete caller. Feasibility over the dyadic ring is distinct
+from feasibility over the rational field. An exact pairing-ideal test can
+prevent searches from relying on an unavailable odd inverse.

research/dyadic-helper-basis-completion/RESULT.json

@@ -0,0 +1,124 @@
+{
+  "counterexample_operations": [
+    [
+      "SCALE",
+      1,
+      1,
+      "-1"
+    ],
+    [
+      "ADD",
+      0,
+      1,
+      "1"
+    ],
+    [
+      "ADD",
+      1,
+      0,
+      "-1"
+    ],
+    [
+      "ADD",
+      0,
+      1,
+      "1"
+    ],
+    [
+      "ADD",
+      1,
+      0,
+      "-2"
+    ],
+    [
+      "SCALE",
+      1,
+      1,
+      "-1"
+    ],
+    [
+      "ADD",
+      0,
+      1,
+      "1"
+    ],
+    [
+      "ADD",
+      1,
+      0,
+      "-1"
+    ],
+    [
+      "ADD",
+      0,
+      1,
+      "1"
+    ],
+    [
+      "ADD",
+      1,
+      0,
+      "-1"
+    ],
+    [
+      "SCALE",
+      1,
+      1,
+      "-1"
+    ],
+    [
+      "ADD",
+      0,
+      1,
+      "1"
+    ],
+    [
+      "ADD",
+      1,
+      0,
+      "-1"
+    ],
+    [
+      "ADD",
+      0,
+      1,
+      "1"
+    ],
+    [
+      "ADD",
+      1,
+      0,
+      "-1"
+    ],
+    [
+      "SCALE",
+      1,
+      1,
+      "-1"
+    ],
+    [
+      "ADD",
+      0,
+      1,
+      "1"
+    ],
+    [
+      "ADD",
+      1,
+      0,
+      "-1"
+    ],
+    [
+      "ADD",
+      0,
+      1,
+      "1"
+    ]
+  ],
+  "exhaustive_compilations": 616,
+  "larger_presentations": 96,
+  "omitted_primitive_pairs": 16,
+  "rejected_inputs": 5,
+  "sign_control": true,
+  "source_interfaces": 18
+}

research/dyadic-helper-basis-completion/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "d7633ce230196a1d5d061347de7a0fd8be512ed6",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446",
+      "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/p104-coupled-helper-bases/PROOF.md",
+      "usage": "input",
+      "git_blob": "168733f6c486d689e58de15c6c34ce1b5ae6b12d",
+      "sha256": "d9049aa75f065c3c21b0f55246c433c643584bca8969f2f382a83c425c4a2927"
+    },
+    {
+      "path": "research/p104-coupled-helper-bases/WITNESS.json",
+      "usage": "input",
+      "git_blob": "8073b3c9772a4a7c94e07d613c2f5c45b1c650fc",
+      "sha256": "e4dfc526453eb9d232772ffdb587fff1923e247341405aee031318b0fb9cb638"
+    },
+    {
+      "path": "research/p104-coupled-helper-bases/construct.py",
+      "usage": "input",
+      "git_blob": "ef5936ca89d6502d7f6af1ce6903d8500c117401",
+      "sha256": "2360066b0a1390c60a86d9788ada1504478e7e48bbfe3fcdf27a5563379fc001"
+    }
+  ]
+}