Prove sharp spectral conditioning for signed rank transport (no κ)

research/sharp-rank-conditioning/PROOF.md

@@ -0,0 +1,137 @@
+# Sharp conditioning price of signed rank transport
+
+This proof was produced by Nick Petalas. Apache-2.0.
+
+## Statement
+
+Use Jeremy Diviney's PR #836 model and signed rank potential, with a finite
+group G, W independent arbitrary-input roles, a symmetric subadditive metric
+r on G, arbitrary invertible complex scalar mixing and paid left row
+multiplications by h of price c >= r(h). A free group call has r(h)=0.
+Every prefix S is invertible in Mat_W(C[G]). Its faithful left regular matrix
+is denoted A(S), and K(S)=||A(S)||_2 ||A(S)^(-1)||_2 >= 1.
+
+For every paid call on row i, immediately before that call,
+
+    |Delta Phi| <= c (K(S)+K(S)^(-1))/2.                 (1)
+
+The constant in (1) is sharp at every real K >= 1, already for two roles
+and G=C2. Sharpness is local: it does not assert that a complete cheaper
+endpoint exists.
+
+If a complete endpoint has constant metric m_j on the formal support of
+each input column j, put M=sum_j m_j. If its paid prices sum to s>0, then
+
+    M <= sum_k c_k (K(S_k)+K(S_k)^(-1))/2.              (2)
+
+In particular, if M>s, at least one paid prefix satisfies
+
+    K(S_k) >= M/s + sqrt((M/s)^2-1).                  (3)
+
+For M=9 and eight unit-price calls, this is
+
+    K(S_k) >= (9+sqrt(17))/8 > 41/25.
+
+The rational lower comparison is strict because sqrt(17)>103/25,
+as 17*625=10625>10609=103^2. PR #836's norm-product diagnostic gives
+only K(S_k)>=9/8 through its stated K_i<=K(S_k) comparison. The new
+threshold is a necessary condition in the same finite-group formal model.
+
+## The spectral inequality
+
+For any invertible finite complex matrix A and unit vector e, put
+
+    R=e*AA*e, L=e*(AA*)^(-1)e,
+    a=sigma_min(A)^2, b=sigma_max(A)^2.
+
+Here stars mean conjugate transposes, and e* denotes the row corresponding
+to the column e. In a spectral basis, R and L are weighted averages of
+lambda and lambda^(-1) on [a,b], using the same nonnegative weights summing
+to one. Since (lambda-a)(lambda-b)<=0,
+
+    lambda+ab/lambda <= a+b,
+    R+ab L <= a+b,
+    4ab R L <= (R+ab L)^2 <= (a+b)^2.
+
+Taking square roots gives the classical Kantorovich bound
+
+    ||e*A||_2 ||A^(-1)e||_2 <= (K+K^(-1))/2.          (4)
+
+Indeed the first norm squared is R and the second is L, since
+A^(-*)A^(-1)=(AA*)^(-1). Equality for a<b requires equal spectral weight
+on the minimum and maximum eigenvalues of AA*. The scalar inequality,
+spectral theorem and Kantorovich bound are classical; the application and
+attaining formal register family below are the contribution.
+
+## Applying the inequality to the formal coefficients
+
+Write S_ij=sum_g a_ij(g)[g] and (S^(-1))_ji=sum_g b_ji(g)[g].
+PR #836 proves, for the actual formal inverse,
+
+    p_ij(g)=Re(a_ij(g)b_ji(g^(-1))),
+    sum_(j,g) p_ij(g)=1,
+    Delta Phi=sum_(j,g)(r(hg)-r(g))p_ij(g).
+
+The metric hypotheses imply |r(hg)-r(g)|<=c. Thus
+
+    |Delta Phi| <= c sum_(j,g)|a_ij(g)b_ji(g^(-1))|
+                <= c sqrt(R_i L_i),
+    R_i=sum_(j,g)|a_ij(g)|^2,
+    L_i=sum_(j,g)|b_ji(g^(-1))|^2.
+
+In the left regular representation, [g] sends e_x to e_(gx). Fix the
+address 1 and role i. The corresponding matrix row lists a_ij(x^(-1)),
+while the inverse column lists b_ji(x). Hence their squared norms are
+exactly R_i and L_i. This uses a faithful representation, with no
+identification of dependent concrete frame matrices with formal coefficients.
+Apply (4) to this matrix row and inverse column to obtain (1).
+
+PR #836 also proves that scalar mixing and metric-zero calls preserve Phi,
+that Phi(I)=0, and that the stated full endpoint has Phi=M. Sum (1) over
+the paid calls to get (2). The function (K+1/K)/2 increases on [1,infinity).
+Consequently the largest paid-prefix K has (K+1/K)/2 >= M/s. Solving the
+quadratic gives (3). The finite word has finitely many paid prefixes, so
+the maximum exists. Dirty restored columns may have m_j=0; they are still
+independent inputs in the full regular matrix.
+
+## A family attaining the local constant
+
+Let G={1,t}, t^2=1, and r(1)=0,r(t)=1. For v>=1 put
+
+    a=(v+v^(-1))/2, b=(v-v^(-1))/2,
+    B=[[a,b],[b,a]], D=diag([1],[t]),
+    S=D B D=[[a[1],b[t]],[b[t],a[1]]].
+
+This is a legal prefix: two row-t calls and one invertible scalar mixer
+produce it. All role inputs remain independent; no clean state is used.
+Its inverse has a on the diagonal and -b[t] off the diagonal, because
+a^2-b^2=1. In the faithful regular representation, D is orthogonal and
+B has positive eigenvalues v and 1/v, each repeated twice after lifting.
+Thus K(S)=v^2. Before multiplying the first row by [t], the two nonzero
+pairings on that row are a^2 at 1 and -b^2 at t. The call therefore gains
+
+    Delta Phi=a^2+b^2=(v^2+v^(-2))/2=(K+K^(-1))/2.
+
+This proves equality in (1) for every K>=1 by taking v=sqrt(K). The
+exact executable fixtures use rational v; irrational parameters belong
+to the written theorem, not the finite rational enumeration. The same
+prefix has Phi=-2b^2, and the next prefix has Phi=1. It has no promised
+full constant-rank endpoint. Neither its gain nor its conditioning is
+evidence for an eight-call solution.
+
+## Scope and predecessor credit
+
+PR #836, Jeremy Diviney, supplies the signed rank potential, its transport
+identity, endpoint normalization and original nonunitary search diagnostic.
+Those are cited inputs; this package does not replay the predecessor word
+examples or audit their counts. Nir Ailon supplies the retained
+forward/inverse-potential context. Credit eumemic #288, Swapnil Jain and
+the retained register/frame lineage; littleBro #680/#705 supplies the
+predecessor's finite Clifford context. No predecessor code is imported.
+
+The result uses finite groups, complex coefficients and full invertible
+arbitrary-input words. An infinite-group extension, restricted-input clean
+ancillas, nonfaithful concrete representations, a physical word, complete
+supplier, paid physical invoice, compiler, precision/tape, stock, analytic
+recovery and a multiplication exponent are outside scope. Independent
+human and formal proof-kernel review are unclaimed.

research/sharp-rank-conditioning/README.md

@@ -0,0 +1,117 @@
+# Sharp spectral conditioning for signed rank transport
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+**Claim type: scoped written proof, with exact finite corroboration.** In
+Jeremy Diviney's [PR #836](https://github.com/CrocSwap/integer-mult-bounds/pull/836)
+formal register model over a finite group, a paid row call of price c has
+
+    |Delta Phi| <= c (K+1/K)/2,
+
+where K is the spectral condition number of the faithful regular prefix.
+The constant is sharp for every K>=1, already on two roles over C2.
+The new step applies the classical Kantorovich inequality to the actual
+coefficient row and inverse column, then constructs a legal equality family.
+
+For the complete rank-nine endpoint with eight unit-price calls, at least
+one paid prefix must consequently have
+
+    K >= (9+sqrt(17))/8 > 1.64,
+
+strengthening the predecessor's stated necessary 9/8 spectral bound.
+The complete weighted price condition is in [PROOF.md](PROOF.md).
+Neither local equality nor this necessary condition constructs the cheaper
+endpoint. No new kappa, physical supplier or selected-frontier change follows.
+
+## Evidence and reproduction
+
+From the repository root, with CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/sharp-rank-conditioning/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/sharp-rank-conditioning
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/sharp-rank-conditioning --check-source-history
+```
+
+Other machines can substitute their CPython 3.12 executable. Both normal and
+optimized commands are registered. The direct check prints
+`PASS_SHARP_RANK_CONDITIONING` in a generated JSON receipt binding every
+package file and the cited source proof by SHA256. It writes no files and
+works in the official Git-free export with its declared proof input.
+No receipt is handwritten.
+
+The finite check covers all 80 distinct rational parameters v=p/q with
+1<=q<=p<=16. Each equality witness has its full four-dimensional regular
+inverse checked by rational elimination and both two-dimensional Fourier
+blocks checked separately. A complete orthogonal eigenbasis certifies its
+exact spectral condition number. Literal row permutation and inversion
+give the new increment, including its negative starting potential. The
+unitary boundary v=1 is also checked separately.
+
+Another 64 rational matrices in dimensions one through eight have prescribed
+singular values and independent rational inverses. All 288 row/inverse-column
+inequalities pass; eight scalar-dimension rows attain equality. Nine rejection
+controls cover invalid bounds, parameters, capacity, singularity and replacing
+the inverse by the transpose. Four semantic checks separate a false unitary
+bound, a squared-condition substitution, the old threshold and the strict
+rational comparison. These are finite real-rational fixtures; the complex,
+all-dimension theorem rests on the written spectral argument.
+
+## Scope and credit
+
+Credit Jeremy Diviney #836 for the signed rank potential, exact transport,
+endpoint law and nonunitary search question; Nir Ailon for the retained
+forward/inverse-potential context; eumemic #288, Swapnil Jain and the retained
+register/frame lineage; littleBro #680/#705 for the predecessor's finite
+Clifford context. The Kantorovich inequality and spectral theorem are
+classical. The contribution is this sharp application and its attaining
+formal family, without a claim of general literature priority.
+
+The predecessor proof is cited and source-bound; no predecessor executable,
+example or count is replayed. The original `bit-new-register-model` card is
+explicitly changed to this complex conditioning side result in
+[TASK.json](TASK.json). Base main is
+`19fdb086ea96af9a9f87936a2b888e10af4ed810`, priority revision 8.
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19220081)
+records the scope before substantial work. Published PRs, recent account
+submissions, claims and distinctive main/merged searches were inspected.
+The cached card scan reported 324 open PRs and 5,489 Discussion records,
+with complete remote pagination, but only 224 of 8,136 main note paths
+materialized locally. Searches do not prove novelty or cover unpublished work.
+
+The theorem requires finite groups and the full invertible independent-input
+boundary. Infinite groups, clean restricted inputs, nonfaithful concrete
+representations and a complete eight-call construction are outside scope.
+Physical costs, native realization, compiler, stock, precision/tape, analytic
+recovery and the multiplication theorem remain unrun obligations. No selected
+cold replay, Lean, Docker, independent human or formal proof-kernel review is
+claimed. All five selected framework assumptions retain their status.
+
+## Open next questions
+
+Can a complete rank-nine endpoint with eight unit calls attain this necessary
+conditioning floor? Start with one fixed formal word and track exact endpoint
+equations together with every signed gain. The local equality family does not
+supply the full endpoint; this is the main blocker to an attainment claim.
+The structured question and its relevance are in TASK.json.
+
+## Implementation bounds
+
+The verifier has no recursion, subprocesses, network, dynamic code evaluation
+or shared mutable state. Numerical loops have fixed finite domains: dimensions
+at most eight, 80 witness parameters, 64 matrices, at most 24 rotations per
+matrix and nine invalid-input cases. All functions fit within 60 physical
+lines. Explicit exceptions keep every invariant active under optimization.
+Six package files and one proof input are each capped at 256 KiB.
+
+Power of Ten rule 3 deviation: CPython and Fraction allocate during the bounded
+offline calculation. Live matrices have at most 8-by-8 entries; rational
+rotations have denominators 5 or 13 and at most 24 factors, singular values
+are integers 1..4, and witness numerators/denominators are at most 16.
+These fixed capacities bound live storage and coefficient heights; runtime
+allocation itself is not instrumented. A native implementation would need
+fixed storage before claiming that property. Rule 9 deviation: eight local
+zero-argument callbacks encode the bounded invalid-input controls; production
+mathematical paths use direct calls. Rule 10 diagnostics are warning-strict
+normal/optimized replay and AST inspection; no separate static type analyzer
+is configured or run for this isolated package.

research/sharp-rank-conditioning/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "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/signed-rank-transport/PROOF.md",
+      "usage": "input",
+      "git_blob": "4b51a0eb6610201715803a7f63abc5a8bb220f13",
+      "sha256": "ba756060ce6ae6445bfb5917523081b6c370292d4acecfbd19437b30b1d1d941"
+    }
+  ]
+}

research/sharp-rank-conditioning/TASK.json

@@ -0,0 +1,84 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-new-register-model",
+  "priority_revision": 8,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "original_card": {
+    "id": "bit-new-register-model",
+    "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/bit-three-register-lower-bound/README.md",
+      "certificates/selected-result.json",
+      "research/bit-gl3-mixed-targets-length10/README.md",
+      "docs/research/community-efficient1000-review.md"
+    ],
+    "methods": [
+      "Construct the smallest exact identity in a newly specified legal operation alphabet.",
+      "Derive a target-specific relaxation bound for that same explicit alphabet."
+    ],
+    "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.",
+      "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse."
+    },
+    "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.",
+    "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.",
+    "allowed_variations": [
+      "Choose a fixed larger register count or a specified nonabelian operation family."
+    ],
+    "scope_change_triggers": [
+      "Remaining inside the already-excluded three-register abelian model.",
+      "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result."
+    ],
+    "overlap_terms": [
+      "three-register",
+      "nonabelian",
+      "group algebra"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Sharp paid rank-potential increment at a specified faithful regular spectral condition number, with a stronger necessary prefix condition and attaining two-role C2 family.",
+  "scope_change_reason": "The card asks for a larger binary register mechanism; this is a complex formal-model conditioning obstruction extending the explicit nonunitary search question of PR836.",
+  "bottleneck_link": "The current supplier bottleneck is distinct. A sharp conditioning obstruction screens formal nonunitary register searches before physical and recursive-cost work; it does not alter the selected construction.",
+  "budget_minutes": 60,
+  "stop_rule": "Package the first verified strict conditioning refinement; do not search for an eight-call word or expand the group family.",
+  "outcome": "completed",
+  "evidence": "PROOF.md proves the sharp Kantorovich application. verify.py checks 80 rational local equality witnesses, 64 rational matrices and 288 row inequalities, nine rejection controls and four semantic comparisons.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can a full rank-nine endpoint with eight unit calls attain the new necessary conditioning floor?",
+      "why_it_matters": "Local sharpness need not survive the cancellations needed for a complete endpoint. A further obstruction or a complete word would change the search.",
+      "first_step": "Track signed gains and exact full endpoint equations together for one fixed eight-call formal word, allowing nonunitary scalar mixers.",
+      "blocked_by": "The present equality family has no complete rank-nine endpoint and supplies no physical implementation."
+    }
+  ],
+  "claim_type": "scoped proof",
+  "predecessors": [
+    {
+      "pr": 836,
+      "author": "Jeremy Diviney",
+      "login": "jeremydiviney",
+      "source_commit": "7ae9124f59694bb1e5acf2ae99c65e63c115b2f4"
+    }
+  ],
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19220081",
+  "preserved_checkout": {
+    "branch": null,
+    "state": "detached HEAD",
+    "commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810"
+  },
+  "upstream_refresh": {
+    "commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+    "priority_revision": 8,
+    "checked_at": "2026-10-27T15:12:20Z"
+  }
+}