Prove sharp two-role dyadic helper-basis conditioning (no new κ)

research/dyadic-basis-conditioning/PROOF.md

@@ -0,0 +1,125 @@
+# Optimal conditioning with a prescribed dyadic row and column
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Write D=Z[1/2]. Let a=(a_1,a_2) be a real dyadic row and b=(b_1,b_2)^T
+a real dyadic column with ab=1. A compatible completion is R in GL_2(D)
+such that aR=e_1^T and Re_1=b. Equivalently, the first column of R is b
+and the first row of R^{-1} is a. The Euclidean condition number is
+cond_2(R)=||R||_2 ||R^{-1}||_2. Set A=a_1^2+a_2^2 and B=b_1^2+b_2^2.
+Both are positive and AB>=1 by Cauchy-Schwarz.
+
+## Theorem
+
+Every compatible completion has the unique form
+
+    R_{k,s} = [ b, s 2^k (-a_2,a_1)^T ],   k in Z, s in {1,-1}.
+
+Put q_k=A 2^k+B 2^{-k}. Then
+
+    cond_2(R_{k,s}) = (q_k+sqrt(q_k^2-4))/2.
+
+The optimal exponents are exactly the integers satisfying
+
+    2^{2k-1} <= B/A <= 2^{2k+1}.
+
+There is one such integer except when B/A is an odd power of two,
+meaning 2^{2j+1} for an integer j. In that case j and j+1 both minimize.
+The sign s is free. These are all minimizers, with no hidden choice of
+another basis vector.
+
+## Proof of the classification
+
+The first-column constraint writes R=[b,z]. The other constraint says az=0.
+Since a is nonzero, the real kernel of a is the line spanned by
+(-a_2,a_1)^T, so z=t(-a_2,a_1)^T for a unique real t. Directly,
+
+    det R = t(a_1 b_1+a_2 b_2) = t.
+
+Because R is a dyadic matrix, its determinant belongs to D. Invertibility
+over D requires that determinant to be a unit. The units of D are exactly
+s 2^k: a dyadic number and its reciprocal both have power-of-two
+denominators exactly when its reduced numerator has no odd prime factor.
+Thus t=s 2^k. Conversely every displayed R has dyadic entries, unit
+determinant, first column b and aR=(1,0), so it is a compatible completion.
+This also proves the asserted inverse-row characterization.
+
+## Proof of the condition number and optimum
+
+Let the singular values be sigma_1>=sigma_2>0, and put c=sigma_1/sigma_2.
+Their squared sum is the squared Frobenius norm B+t^2 A. Their product is
+|det R|=|t|. Therefore
+
+    c+c^{-1} = (sigma_1^2+sigma_2^2)/(sigma_1 sigma_2)
+             = B/|t|+A|t| = q_k.
+
+Solving c^2-q_k c+1=0 with c>=1 proves the formula. This expression is
+strictly increasing in q>=2. Hence minimizing q suffices. Its successive
+differences have the sign of A 2^{2k+1}-B, because
+
+    q_{k+1}-q_k = A 2^k-B 2^{-k-1}.
+
+The differences are negative before their single sign change and positive
+afterward. Comparing k with its two neighbors gives precisely the two
+displayed inequalities. They cover all positive B/A, overlap only at the
+stated equality boundaries, and exclude every other exponent globally.
+This is an all-integer proof, rather than a bounded search.
+
+An exact implementation needs two candidates. Let e=floor(log_2(B/A)),
+computed by bit lengths and a rational comparison. The candidates are
+floor(e/2) and floor(e/2)+1. Comparing their rational q values retains all
+ties and requires neither logarithmic approximation nor eigenvalue rounding.
+
+## Dyadic reversibility can cost more than real completion
+
+If R is allowed to be any real invertible matrix with the same two
+constraints, its parameter t can be any nonzero real number. Arithmetic-
+geometric mean gives q(t)>=2 sqrt(AB), with equality exactly when
+|t|=sqrt(B/A). Its optimum condition number is therefore
+
+    sqrt(AB)+sqrt(AB-1).
+
+The dyadic optimum equals that real optimum exactly when sqrt(B/A) is a
+power of two. Otherwise the dyadic optimum is strictly greater. A dyadic
+matrix that is merely invertible over Q need not be invertible over D;
+allowing an odd determinant silently changes the arithmetic contract.
+
+## The source pair
+
+Ali Romman's PR5611 supplies a=(3,5), b=(2,-1)^T as a legal pair with no
+individual unit entry in a, and gives the compatible completion
+[[2,5],[-1,-3]]. That constructor and its correctness are cited, not audited.
+The new optimization has A=34, B=5. At k=-1,
+
+    R = [[2,-5/2],[-1,3/2]],    det R=1/2,    q=27,
+    cond_2(R)=(27+sqrt(725))/2.
+
+Indeed 1/8 < 5/34 < 1/2, so k=-1 is the unique optimal exponent.
+Its two determinant signs are the only optimal completions. The cited
+unit-determinant completion has q=39, so the new one is strictly better.
+The unconstrained real optimum is sqrt(170)+13 and is strictly smaller
+than the dyadic optimum, since 27^2>4*170. The example shows a genuine
+arithmetic conditioning penalty rather than a numerical eigenvalue artifact.
+
+At a=(1,0), b=(1,1)^T, B/A=2. Both k=0 and k=1 minimize, with q=3.
+This is an exact tie control for the optimizer.
+
+## Helper-interface scope
+
+The source dual-pair interface is the motivation and the compatible input
+contract. This theorem optimizes its two-role endpoint basis, without extra
+roles. For arbitrary independent complex banks of the same positive size,
+R tensor I and its inverse have these same Euclidean norms and condition
+number, because their Gram matrices tensor the corresponding scalar Gram
+matrix with I. This is a scalar bank change, not a tensor power of R.
+
+Endpoint conditioning alone does not certify intermediate scalar growth,
+componentwise rounded error, a gate-count optimum, a physically legal helper
+cut, source delivery, dirty restoration in a complete word, frames, ownership,
+stock, tape cost, compiler closure or outer funding. More workspace changes
+the optimization domain. No selected assumption, complete multiplication
+theorem, supplier admission or new kappa follows. The all-pair result is this
+written proof; the accompanying finite checker corroborates it. Classical
+two-by-two singular-value identities and dyadic-unit algebra are not claimed
+as new general tools. Independent human and formal proof-kernel review are
+unclaimed.

research/dyadic-basis-conditioning/README.md

@@ -0,0 +1,136 @@
+# Sharp conditioning of two-role dyadic helper completion
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+For every dyadic row a and column b of length two with ab=1, the least
+Euclidean condition number of a compatible invertible dyadic basis has an
+exact formula. Write A=||a||_2^2 and B=||b||_2^2. Choose every integer k with
+
+    2^(2k-1) <= B/A <= 2^(2k+1).
+
+Then q=A*2^k+B*2^(-k), and the optimum is
+
+    cond_2(R) = (q+sqrt(q^2-4))/2,
+    R = [b, ±2^k*(-a_2,a_1)^T].
+
+There are at most two optimal exponents. The optimizer finds them by two
+exact rational comparisons, without numerical logarithms or eigenvalues.
+[PROOF.md](PROOF.md) classifies every compatible completion and proves
+global optimality over all integer exponents, including ties.
+
+This is a scoped mathematical proof with exact finite corroboration.
+It builds on the dual-pair interface of Ali Romman's merged
+[PR #5611](https://github.com/CrocSwap/integer-mult-bounds/pull/5611).
+That source constructs legal completions and leaves their growth and
+precision costs payable. Its constructor is cited, not audited or replayed.
+The new result optimizes endpoint conditioning in the two-role contract.
+
+For its pair a=(3,5), b=(2,-1)^T, the unique optimal determinant magnitude
+is 1/2, with R=[[2,-5/2],[-1,3/2]]. The condition number is exactly
+(27+sqrt(725))/2. The cited unit-determinant completion has q=39; the new
+one has q=27, hence strictly smaller condition number. Real completions
+without the dyadic inverse requirement reach sqrt(170)+13, strictly below
+the dyadic optimum. Thus arithmetic reversibility can impose a genuine
+conditioning penalty. At a=(1,0), b=(1,1)^T, both k=0 and k=1 are optimal.
+
+## Reproduce
+
+From the repository root, with CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/dyadic-basis-conditioning/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/dyadic-basis-conditioning/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/dyadic-basis-conditioning
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/dyadic-basis-conditioning --check-source-history
+```
+
+Other hosts may substitute their CPython 3.12 interpreter. The last command
+checks the committed publication. Normal and optimized scientific commands
+print `PASS_DYADIC_BASIS_CONDITIONING` and a generated SHA256-bound receipt.
+The launcher prints `PASS_REGISTERED_RESEARCH_PACKAGE`. No receipt is
+handwritten. The scientific verifier writes no files, imports no predecessor
+code, and runs without Git or the network, including from a standalone export.
+
+The finite domain contains all 308 integer dual pairs with each coordinate
+in [-5,5], with seven reciprocal dyadic rescalings per pair. These 2,156
+presentations are compared against 71,148 directly constructed exponent
+matrices. Both determinant signs give 4,760 checked optimal representatives;
+224 presentations have tied exponents. A separate second-column oracle
+enumerates 56,628 literal matrices over 52 smaller dual pairs, finding 488
+compatible grid matrices and the same optima. Four size-boundary pairs and
+14 rejection controls cover malformed inputs, odd denominators, size limits,
+bad duality, a nonunit determinant, wrong endpoints, exponents and spectral
+proxies. All checks remain active under Python optimization. These finite
+counts corroborate the proof and do not replace its universal argument.
+
+## Scope and credit
+
+Scientific base is canonical main
+19fdb086ea96af9a9f87936a2b888e10af4ed810, priorities revision 8. The current
+selected-source binding check passed after sparse inputs were materialized.
+The originating card is explicitly changed from a physical helper-inventory
+construction to this endpoint precision-interface theorem. It supplies no
+new productive targets or favorable complete signed moment. Discovery stopped
+at this first result. [TASK.json](TASK.json) records the scope change and
+[SOURCES.json](SOURCES.json) pins provenance; there are no live source inputs.
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19228475)
+preceded substantive work.
+
+Credit Ali Romman #5611 for the completed dual-pair interface, its explicit
+nonunit-entry pair and open growth/precision obligation; #5602 and #5599 for
+the helper-splitting context and their retained P104/native/controller/compiler
+lineage. Nick Petalas #5115 supplies earlier row preparation in a different
+single-hub interface. The dyadic-unit classification, Cauchy-Schwarz and
+two-by-two singular-value identities are classical. Their application to this
+exact constrained optimum and the optimizer are the new contribution.
+Predecessor files and credit lines are unchanged. Independent human and
+formal proof-kernel review are unclaimed.
+
+Live PR lists and bodies, recent account work, handoffs, local reservations,
+merged searches and distinctive all-main README searches were checked.
+The cached card search had complete remote pagination but sparse local notes;
+direct Git-tree searches supplemented that limit. These are bounded overlap
+checks, not proof of novelty or coverage of unpublished work.
+
+The theorem fixes exactly two roles, real dyadic scalar coefficients,
+the prescribed row and column, dyadic invertibility and the Euclidean norm.
+It also applies to the same scalar basis tensored with an identity on banks.
+It does not optimize extra workspace, scalar instructions, intermediate growth
+or rounded error. No physical cut, frames, ownership/restoration, source access,
+stock, tape, native costs, compiler, supplier admission, complete multiplication
+theorem or new kappa is claimed. Lean, Docker and the selected complete cold
+replay are unrun. The selected frontier is unchanged.
+
+## Open next questions
+
+- Can one actual helper cut use this optimal basis while keeping intermediate
+  scalar growth and the full paid/target invoice favorable? Start with its
+  exact two-role pair and emit a chronological scalar schedule. Physical
+  compatibility, rounding, restoration and the complete bill are blockers.
+- What is the exact optimum with at least three prescribed helper roles?
+  Start with one three-coordinate dual pair. The complementary basis is no
+  longer a single scalar parameter, so the dyadic determinant restriction
+  alone does not solve the problem. No higher-dimensional optimum is claimed.
+
+## Executable bounds
+
+Build the Lever led to the reusable exact optimizer. Prove It Works led to
+the separate direct-column oracle and dense Gram/inverse checks. Foundational
+Thinking kept the endpoint contract as a row/column pair and separated it
+from physical schedules. Power of Ten inspection covers the two new Python
+files. There is no recursion, generated code, network, subprocess or callback
+dispatch. Functions have at most 28 physical lines. External coordinates are
+integers or Fractions with at most 64 numerator bits and 64 denominator bits
+after the binary point. The optimizer's loops have at most two entries and
+its powers are bounded by 260 in magnitude. The finite oracle uses fixed
+domains, including at most 261 candidate exponents, 1,089 second columns
+and 308 stored integer pairs. Package hashing reads seven files of at most
+256 KiB each.
+
+Python allocation is a rule 3 managed-runtime deviation confined to this
+bounded offline command. The fixed coordinate, matrix and enumeration limits
+bound live data; no steady service is supplied. A lower-level runtime would
+need fixed storage before widening these limits. Warning-strict normal and
+optimized execution plus in-memory compilation provide local diagnostics;
+no separate Python linter is available on PATH. No shared configuration or
+predecessor code is changed.

research/dyadic-basis-conditioning/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/dyadic-helper-basis-completion/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "8c51201534aaab80b2cefe1ef12c3a1048ce3f36",
+      "sha256": "a909d7b909edffb5babec3e937a3d13052aeaf87852ec73a37dac9802b6d9734"
+    },
+    {
+      "path": "research/dyadic-helper-basis-completion/README.md",
+      "usage": "provenance",
+      "git_blob": "595d586859ca22e488a675bb1b78985fa8157d36",
+      "sha256": "6eec44155e30cf8b100cfd2e6378d0dd60da1cdf496e3b88251a40018fe9bcb3"
+    }
+  ]
+}