Prove sharp conditioning of the complete complex port (no new κ)

research/complex-port-sharp-conditioning/README.md

@@ -0,0 +1,212 @@
+# Sharp conditioning of the complete complex two-bank port
+
+This scoped proof replaces the bound 16 in Dugongue's
+[PR #4743](https://github.com/CrocSwap/integer-mult-bounds/pull/4743)
+by the exact Euclidean condition number
+
+\[
+ \operatorname{cond}_2 {\cal U}_f=\operatorname{cond}_2 {\cal V}_f
+ =\frac{11+3\sqrt{13}}2,\qquad f\geq1.
+\]
+
+Both the norm and inverse norm are exactly \((\sqrt{13}+3)/2\).
+The result concerns the complete two- and three-call maps on two arbitrary
+independent input banks. It does not improve their paid call count, admit a
+supplier or change the selected multiplication exponent.
+
+This contribution is produced by Nick Petalas. The shear singular-value
+calculation is classical linear algebra; the new result is its sharp
+application to these particular ports, with the exact spectrum and witness.
+Independent human and formal proof-kernel review are unclaimed.
+
+## The precise interface
+
+Use the retained letters and schedules of #4743, not a tensor power of their
+sum. Write \(G_f=G^{\otimes f}\) for each individual letter. Set
+
+\[
+ A_f=C_{0,f},\quad D_f=J_fW_fC_{0,f},\quad
+ L_f=P_f+2Q_f.
+\]
+
+The two full-input ports are
+
+\[
+ {\cal U}_f=\begin{pmatrix}A_f&0\\A_fL_fA_f&A_f\end{pmatrix},\qquad
+ {\cal V}_f=\begin{pmatrix}A_f&0\\D_fL_fA_f&D_f\end{pmatrix}.
+\]
+
+All of \(A_f,D_f,P_f,Q_f\) are unitary. Consequently each port is
+unitarily equivalent on its left and right to
+
+\[
+ {\cal S}(L_f)=\begin{pmatrix}I&0\\L_f&I\end{pmatrix}.
+\]
+
+For example \({\cal U}_f=\operatorname{diag}(I,A_f){\cal S}(L_f)
+\operatorname{diag}(A_f,I)\); replace the left \(A_f\) by \(D_f\) for
+\({\cal V}_f\). This uses both independent inputs and both outputs.
+
+## Proof of the sharp constant
+
+For any square complex matrix \(L\), its singular-value decomposition reduces the
+shear to an orthogonal sum of the two-dimensional shears
+
+\[
+ \begin{pmatrix}1&0\\s&1\end{pmatrix},
+ \qquad s\text{ a singular value of }L.
+\]
+
+The Gram matrix is \(\left(\begin{smallmatrix}1+s^2&s\\s&1
+\end{smallmatrix}\right)\). Its eigenvalues have product one and sum
+\(2+s^2\), so the corresponding singular values are
+
+\[
+ \frac{\sqrt{s^2+4}+s}{2},\qquad
+ \frac{\sqrt{s^2+4}-s}{2}.
+\]
+
+The first increases with \(s\), the second is its reciprocal. Thus both the
+shear norm and inverse norm equal the first expression at \(s=\|L\|_2\).
+
+Here \(P=SUS,\ Q=SVS\), where \(S e_x=i^{\operatorname{popcount}(x)}e_x\),
+\(U\) is CNOT from bit 0 to bit 2, and \(V\) swaps bits 0 and 1. Therefore
+
+\[
+ R=P^*Q=S^*UVS,\qquad
+ R_f=P_f^*Q_f=R^{\otimes f}.
+\]
+
+The permutation \(UV\) fixes the all-ones vector. Hence \(R_f\) fixes the
+nonzero vector \(v_f=S_f^*{\bf1}\) at every width, and
+
+\[
+ L_fv_f=P_f(I+2R_f)v_f=3P_fv_f.
+\]
+
+The triangle inequality gives \(\|L_f\|_2\leq3\), and this vector gives
+equality. Substituting \(s=3\) proves the asserted norms and condition number.
+The invariant Gram sector spanned by \((v_f,0)\) and \((0,P_fv_f)\) is exactly
+
+\[
+ \begin{pmatrix}10&3\\3&1\end{pmatrix}.
+\]
+
+Its eigenvalues are the roots of \(t^2-11t+1\), proving attainment of both
+extremes, rather than only an improved upper bound.
+
+## Complete singular spectrum
+
+For completeness, the relative permutation is
+\((0)(4)(1\ 2\ 5\ 6)(3\ 7)\). Its power traces are \(8,2,4,2\).
+Tensor traces raise these four values to the \(f\)-th power.
+The four character projectors of this order-four unitary therefore give
+multiplicities
+
+\[
+ m_+=\frac{8^f+4^f+2\,2^f}4,\quad
+ m_-=\frac{8^f+4^f-2\,2^f}4,\quad
+ m_i=m_{-i}=\frac{8^f-4^f}4.
+\]
+
+Since \(L_f^*L_f=5I+2(R_f+R_f^*)\), its squared singular values are
+9, 1 and 5 with respective multiplicities \(m_+,m_-,2m_i\).
+For each \(d\in\{1,5,9\}\), both port singular values are
+
+\[
+ \frac{\sqrt{d+4}+\sqrt d}{2},\qquad
+ \frac{\sqrt{d+4}-\sqrt d}{2},
+\]
+
+each repeated by the corresponding coupling multiplicity. This is a
+closed all-width formula, not an extrapolation of finite ranks.
+
+## Evidence and reproduction
+
+The standard-library verifier constructs the literal phase monomials
+independently at widths 1, 2 and 3. For the resulting 16-, 128- and
+1,024-row shear matrices it checks the new Gram annihilator
+
+\[
+ \prod_{d\in\{1,5,9\}}\bigl(G^2-(d+2)G+I\bigr)=0,
+ \qquad G={\cal S}(L_f)^*{\cal S}(L_f),
+\]
+
+both inverse multiplication orders and the sharp two-dimensional sector.
+Exact spectral-projector traces enumerate the squared-coupling multiplicities:
+\( (2,2,4), (18,24,22), (140,224,148) \), ordered by \(d=1,5,9\).
+Six controls reject a changed coupling coefficient, swapped multiplicities,
+the wrong inverse sign, unsupported width, invalid branch and false cap ten.
+It imports no predecessor verifier and does not replay any predecessor rank
+or endpoint certificate.
+
+From the repository root, using CPython 3.12:
+
+    /Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/complex-port-sharp-conditioning/verify.py
+    /Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/complex-port-sharp-conditioning/verify.py
+    /Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/complex-port-sharp-conditioning
+    /Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/complex-port-sharp-conditioning --check-source-history
+
+The final status is PASS_COMPLEX_PORT_SHARP_CONDITIONING. Optional
+--receipt /absolute/scratch/path.json writes a generated receipt binding all
+five package files by SHA-256. No receipt is hand-written or committed.
+
+## Scope, sources and research decision
+
+The mathematical baseline is canonical main
+624de9dc66858af0945e5f8a0942488d62280d43, priority revision 7.
+SOURCES.json pins the originating card, selected record and predecessor
+proof texts as provenance. The computation is self-contained and has no
+external live input. This changes the card's rank-shape search to a small
+precision-interface lemma. The card's historical first control was attempted
+and fails with KeyError: 'complex_profile' under the changed selected schema.
+The current source-binding control passed with
+PASS_RESEARCH_BASELINE_BINDINGS_ONLY.
+
+Credit Dugongue's #4743 for both full-input schedules and the previous
+bound 16; Yiyang / Lyy-iiis's
+[#4710](https://github.com/CrocSwap/integer-mult-bounds/pull/4710)
+for the repaired phase letters; lee-phys's
+[#4688](https://github.com/CrocSwap/integer-mult-bounds/pull/4688)
+for the two-image prefix and order-four permutation; and Jacob Alan Sussman's
+[#4628](https://github.com/CrocSwap/integer-mult-bounds/pull/4628)
+for the small-unit model, with eumemic and Swapnil Jain's predecessor
+certificate framework credited there. Their constructions and earlier
+singular-value observations are cited inputs. No predecessor credit is changed.
+
+Discovery stops at this sharper constant. The full producer/consumer bill
+remains that of #4743: paid calls, restoration, native workspace and array
+passes are inherited; numerical Gaussian implementations, compiler costs and
+complete recursive stability are separate obligations. This result does not
+price any unknown cost as zero or justify a further construction campaign.
+The proof concerns exact Euclidean endpoint conditioning. It makes no claim
+about coordinatewise rounding, internal Gaussian gate cuts, nonunitary
+encodings, a complete five-input unit or integer multiplication.
+
+Implementation inspection uses the Build the Lever and Prove It Works
+principles: the independent rerunnable Gram check is the evidence artifact.
+There is no recursion or dynamic code execution. Widths are fixed, matrices
+have at most 1,024 rows, each row at most 1,024 entries, and all functions are
+under 60 lines. Meaningful checks remain enabled under optimization.
+Managed-runtime allocation is a deviation from Power of Ten rule 3:
+Python integers, dictionaries and temporary matrices allocate during the
+finite check; the fixed dimension bounds live storage and each matrix is
+released after its width. Rule 9's indirect-call deviation is confined to
+six fixed local rejection controls. Replacing Python storage or these
+callbacks is warranted only if the verifier becomes a reusable service or
+accepts larger domains. Warning-strict ordinary and optimized commands are
+registered; no separate Python static analyzer is configured for this package.
+
+## Open next questions
+
+1. How does this sharp endpoint constant propagate through a complete
+   recursively substituted word? Start with one explicit composition of the
+   retained ports and account for the actual intervening nonunitary mixers.
+   A complete word is needed; multiplying endpoint constants blindly may lose
+   cancellation and does not establish stability.
+2. What is the sharp coordinatewise rounding-error amplification for the
+   actual native schedule? Begin with the stated monomial and paid-call error
+   channels in #4743 and retain their order. A concrete rounded Gaussian
+   implementation and its error contract remain required.
+
+The structured versions are in TASK.json. New work is Apache-2.0.

research/complex-port-sharp-conditioning/SOURCES.json

@@ -0,0 +1,42 @@
+{
+  "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/complex-prefix-native-ports/FULL-INPUT-PORT.md",
+      "usage": "provenance",
+      "git_blob": "39a461f2fbf2e009423cd784f56de121d190d842",
+      "sha256": "52b8462e28f9e87925ccfea27872630e2b2da23f19fd3d2265c2654bc016088c"
+    },
+    {
+      "path": "research/complex-prefix-native-ports/SECTOR-COMPLETION.md",
+      "usage": "provenance",
+      "git_blob": "d3fcedfa0ef8c569810cbfe3b001e509be1274aa",
+      "sha256": "2e72e19c4733213d1875f60cf87eddb733dde9266cf2581cb56393c3fabf1933"
+    },
+    {
+      "path": "research/phase-aligned-two-call-prefix/README.md",
+      "usage": "provenance",
+      "git_blob": "ef39626e0b25216d826d45371af1d181ab2754f1",
+      "sha256": "e866032429cb032f55edc9b2f3c6535ecf37680aae7cd9e8bb9b8cc21617aa64"
+    },
+    {
+      "path": "research/complex-two-image-hook-prefix/README.md",
+      "usage": "provenance",
+      "git_blob": "ac33ab36287fe1f1d9ba51b5360f44536c2ff3fc",
+      "sha256": "91d45b5af6063e30c6860a4cb46cfc44960ecd67f37c3bce9675924e30b89b4e"
+    }
+  ]
+}

research/complex-port-sharp-conditioning/TASK.json

@@ -0,0 +1,78 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 7,
+  "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+  "original_card": {
+    "id": "complex-rank-shape-decoder",
+    "question": "Can a decoder deliver the local paid mass in fewer, larger-rank children (block frame climbs instead of rank-1 to rank-3 steps)?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "research/complex-local-word-ceiling/README.md",
+      "research/complex-decoder-field-extension-seed44/README.md",
+      "research/complex-frame-pair-decoders/README.md",
+      "research/selected-k8-unrestricted-ends/README.md",
+      "research/eisenstein-reduction-copy-floor/README.md"
+    ],
+    "methods": [
+      "Find one exact small decoding identity whose frame path climbs in blocks, and price its complete per-call profile.",
+      "Bound the best effective child rank achievable for one fixed support alphabet, including copies, frames and restoration."
+    ],
+    "acceptance_gate": "A per-call local profile, with all copied information, frames and restoration counted, whose ceiling exceeds the selected word's by at least 5%; masked or overcomplete supports must change an assumption of the eight-term all-pairs bound. 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",
+        "research/complex-local-word-ceiling/verify.py"
+      ],
+      "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING",
+      "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.",
+      "scope": "Positive control and planning budget only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin. Ideal budget: rank-16 delivery is 2.31x (levers.py).",
+    "bottleneck_link": "Rank-1 children are about half of recursive cost; the selected word's effective child rank is about 3.9. Larger-rank delivery lowers recursive cost per unit of paid mass.",
+    "allowed_variations": [
+      "One masked, overcomplete or block decoder family with exact labels and supports.",
+      "A scoped lower bound on effective rank for one alphabet.",
+      "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope."
+    ],
+    "scope_change_triggers": [
+      "Repacking idle remainders of an unchanged word (covered by the packing ceiling).",
+      "Repeating the eight-term all-pairs search inside its proved scope.",
+      "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.",
+      "Searching below C=40 in the #2017 Eisenstein binary scalar-rectangle or fixed-support block-linear additive pairing model; specify a changed premise instead. This bound does not cover every complex decoder.",
+      "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts."
+    ],
+    "overlap_terms": [
+      "rank shape",
+      "block climb",
+      "masked decoder",
+      "overcomplete",
+      "effective rank"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Prove the sharp all-width Euclidean condition number and singular spectrum of the complete two- and three-call dirty-input ports from PR4743.",
+  "scope_change_reason": "The small scoped precision lemma replaces a coarse endpoint bound while preserving the predecessor schedule. It is a side result, not a new rank-shape construction.",
+  "bottleneck_link": "Exact conditioning removes slack in one local precision interface; paid child profiles and the selected exponent are unchanged.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first verified sharper all-width port bound and package it; do not extend the construction.",
+  "outcome": "completed",
+  "evidence": "Written singular-value proof; literal exact Gaussian-integer Gram checks at widths 1, 2, 3 and six rejection controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "How does the sharp endpoint constant propagate through complete recursive substitution?",
+      "why_it_matters": "A component bound alone is not a complete precision contract.",
+      "first_step": "Choose an explicit composed word and retain intervening nonunitary mixers in its norm calculation.",
+      "blocked_by": "A complete recursive word and its rounding schedule are not supplied here."
+    },
+    {
+      "question": "What is the sharp coordinatewise error amplification of the native schedule?",
+      "why_it_matters": "The Euclidean endpoint constant does not determine the error from separate rounded paid calls.",
+      "first_step": "Use the exact order of monomial updates and paid-call error injections from PR4743.",
+      "blocked_by": "An actual rounded Gaussian implementation and its error contract remain required."
+    }
+  ]
+}

research/complex-port-sharp-conditioning/VERIFY.json

@@ -0,0 +1,32 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Exact new Gram spectra, sharp invariant sector, both inverse orders and six controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-W",
+        "error",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "The same mathematical checks with Python assertions disabled."
+    }
+  ]
+}