Improve three-qubit Clifford Gram condition bound to 807 (no κ)

research/clifford-transvection-conditioning/ORIGIN.json

@@ -0,0 +1,25 @@
+{
+  "source_pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/6714",
+  "source_head": "f7f32a18dde54e67624a9ed9cc7e1b266d9585c0",
+  "source_author": "alephnan",
+  "files": [
+    {
+      "retained_path": "source/pr6714-result.json",
+      "original_path": "research/clifford-three-qubit-threshold/RESULT.json",
+      "sha256": "308b8dee094eb5481565ea89698ed5df69edeeecd4b63b4d78cb9cecdbe71c27",
+      "original_git_blob": "77a5c8b23b91ed215b41cd2181a245d3f7d2374e"
+    },
+    {
+      "retained_path": "source/pr6714-table.json",
+      "original_path": "research/clifford-three-qubit-threshold/table.json",
+      "sha256": "388d617a76e345774a8768f32a6a9bc6e94b87f9c8a5cf6712a95a5a3a945fcd",
+      "original_git_blob": "01f56d329aec686e49dc18f83adfea47b7fa423e"
+    }
+  ],
+  "proof_reference": {
+    "url": "https://github.com/CrocSwap/integer-mult-bounds/blob/f7f32a18dde54e67624a9ed9cc7e1b266d9585c0/research/clifford-three-qubit-threshold/PROOF.md",
+    "sha256": "d29091eb12b4ccd3f5acb389634a858af3beb0dc78865613bb7bd68c9440c6d0",
+    "retained": false
+  },
+  "scope": "Exact predecessor numerical data retained unchanged. Multiplicity decomposition and representation-theoretic premises are cited, not independently re-established."
+}

research/clifford-transvection-conditioning/PROOF.md

@@ -0,0 +1,178 @@
+# A transvection certificate for three-qubit conditioning
+
+## Statement and inherited mathematical inputs
+
+Use the full Gaussian-dyadic three-qubit Clifford alphabet and conventions of
+[alephnan's PR6714](https://github.com/CrocSwap/integer-mult-bounds/pull/6714),
+at head `f7f32a18dde54e67624a9ed9cc7e1b266d9585c0`. For representatives
+`U_a` of its 92,897,280 projective classes, put
+
+\[
+ H_f(a,b)=\left(\operatorname{tr}(U_a^*U_b)/8\right)^f.
+\]
+
+For every integer `f >= 10`, this package proves the sufficient bounds
+
+\[
+ \boxed{\frac{2835}{131072}I\preceq H_f
+              \preceq\frac{2287845}{131072}I.}                 \tag{1}
+\]
+
+Consequently the spectral condition number is at most **807**.
+The predecessor's sufficient bounds were `945/262144` and `762615/32768`,
+with ratio 6,456. The lower bound in (1) is six times larger and the upper
+bound is three quarters as large. No optimality for the actual spectrum is claimed.
+
+The following are cited predecessor results, rather than claims reproved here.
+They are in its [PROOF.md, Sections 2 through 7](https://github.com/CrocSwap/integer-mult-bounds/blob/f7f32a18dde54e67624a9ed9cc7e1b266d9585c0/research/clifford-three-qubit-threshold/PROOF.md).
+
+1. Let `V` be the natural eight-dimensional representation, and `sigma` run
+   over the thirty irreducible characters of `Sp(6,2)`. The odd central-sector
+   irreducibles are `V tensor sigma`. Their multiplicities in `V^(tensor 9)`
+   are the nonnegative integers `m_sigma` retained in the source result.
+2. If `mu` is an even-sector irreducible relevant at width ten, then
+
+   \[
+   \overline V\otimes\mu
+       =\bigoplus_\sigma n_\sigma(V\otimes\sigma),\qquad n_\sigma\ge0.
+   \]
+
+   Write `d_sigma = dim sigma` and `d = dim mu`. Dimensions and reciprocity give
+
+   \[
+   d=\sum_\sigma n_\sigma d_\sigma,\qquad
+   m_\mu(10)=\sum_\sigma n_\sigma m_\sigma.             \tag{2}
+   \]
+
+3. There is `N` equal to 28 or 36 and an integer `a >= 1` with `d=Na`.
+   For a transvection `tau` of `Sp(6,2)`, set
+
+   \[
+    T=\sum_\sigma n_\sigma\chi_\sigma(\tau).
+   \]
+
+   Then `|T| <= 16a = 16d/N`. This follows because exactly sixteen quadratic
+   forms in either Pauli-character orbit are fixed by a transvection.
+   In the source's phase convention, the quotient-character sum differs from
+   the character of `mu` at its Clifford lift by a scalar of absolute value one.
+4. The eigenvalue on the regular matrix block of `mu` is
+
+   \[
+   \lambda_\mu(10)=\frac{92897280}{8^{10}}
+                       \frac{m_\mu(10)}{d}.             \tag{3}
+   \]
+
+   Also `H_(f+1) = H_f circ H_1`, where `circ` is the Schur product,
+   `H_1` is positive semidefinite, and its diagonal is one.
+
+The exact source numerical files are retained unchanged. Their origin and hashes
+are in [ORIGIN.json](ORIGIN.json). The published character table is due to
+Chin-Yen Lee, Wei-Hsuan Yu, Yung-Ning Peng and Ching-Jui Lai. This proof uses
+the predecessor's identification and multiplicities as inputs. It does not
+reconstruct the table, audit that identification, or rerun its decomposition.
+
+## The new finite certificate
+
+For every one of the thirty types, write `t_sigma = chi_sigma(tau)`. The
+retained data satisfy the two integer inequalities
+
+\[
+ 4m_\sigma-5d_\sigma-7t_\sigma\ge0,\qquad
+ 1345d_\sigma+1883t_\sigma-12m_\sigma\ge0.               \tag{4}
+\]
+
+These are the new supporting lines. The verifier reads the cited width-nine
+multiplicities and the transvection column, evaluates every residual in (4)
+exactly, and prints all thirty pairs. This is a finite arithmetic certificate
+for new inequalities in the predecessor data, rather than another verification
+of its threshold or multiplicity calculation.
+
+The source row numbers and the three tight data points explain the constants:
+
+| source row | `d_sigma` | `t_sigma` | `m_sigma` |
+| --- | ---: | ---: | ---: |
+| 1 | 1 | 1 | 269 |
+| 2 | 7 | -5 | 0 |
+| 9 | 56 | -24 | 28 |
+
+The lower supporting line passes through normalized rows 2 and 9. The upper
+supporting line passes through normalized rows 1 and 2. Checking only these
+three points would be insufficient; (4) is checked for **every** type.
+
+Multiply (4) by the nonnegative integers `n_sigma` and sum. By (2),
+
+\[
+ \frac54d+\frac74T\le m_\mu(10)
+        \le\frac{1345}{12}d+\frac{1883}{12}T.           \tag{5}
+\]
+
+Both slopes are positive. Applying `-16d/N <= T <= 16d/N` gives
+
+\[
+ \left(\frac54-\frac{28}{N}\right)d
+   \le m_\mu(10)
+   \le\left(\frac{1345}{12}+\frac{7532}{3N}\right)d.   \tag{6}
+\]
+
+Thus the two orbit-specific intervals for `m_mu(10)/d` are
+
+| `N` | lower bound | upper bound |
+| --- | ---: | ---: |
+| 28 | 1/4 | 807/4 |
+| 36 | 17/36 | 19637/108 |
+
+The first interval contains the second. Since
+`92897280/8^10 = 2835/32768`, (3) proves (1) at width ten.
+
+For propagation, if `alpha I <= H_f <= beta I`, Schur positivity gives
+
+\[
+ (H_f-\alpha I)\circ H_1\succeq0,\qquad
+ (\beta I-H_f)\circ H_1\succeq0.
+\]
+
+The unit diagonal means `I circ H_1=I`. Therefore the same interval holds at
+`f+1`, proving (1) for every `f >= 10`. This is a written universal implication
+from the stated representation-theoretic inputs, not a finite-width extrapolation.
+
+## What is sharp, and what is still open
+
+The two bounds in (6) are sharp for the following **relaxation only**. Assign
+arbitrary nonnegative weights `x_sigma` summing to one, retain the thirty points
+
+\[
+ (r_\sigma,c_\sigma)=(t_\sigma/d_\sigma,m_\sigma/d_\sigma),
+ \qquad \left|\sum_\sigma x_\sigma r_\sigma\right|\le16/N,
+\]
+
+and minimize or maximize `sum x_sigma c_sigma`. The following explicit mixtures
+attain all four bounds; weights refer to the indicated source rows.
+
+| `N` | extremum | nonzero weights |
+| --- | --- | --- |
+| 28 | minimum | row 2: 1/2; row 9: 1/2 |
+| 28 | maximum | row 1: 3/4; row 2: 1/4 |
+| 36 | minimum | row 2: 1/18; row 9: 17/18 |
+| 36 | maximum | row 1: 73/108; row 2: 35/108 |
+
+Together with (4), these mixtures prove the relaxed optimum, including its
+orientation at the two ends of the trace interval. The independent primal route
+in the verifier lists every simplex vertex in the trace slab and every intersection
+of a simplex edge with its two bounding hyperplanes. These cover the vertices:
+at a vertex, at most two weights can be positive since there is the sum constraint
+and at most one active trace constraint. If two trace coordinates coincide, a
+nontrivial edge interior is not a vertex. All arithmetic is rational.
+
+The relaxation discards additional representation and multiplicity constraints.
+Its attaining mixtures are not claimed to come from any actual irreducible `mu`.
+In particular **807 is a sufficient uniform bound, not the exact condition
+number**, and neither endpoint is claimed to be an actual eigenvalue.
+
+## Scope
+
+This is a scoped native-algebra conditioning theorem with exact finite
+corroboration. It does not improve the already proved threshold ten. It supplies
+no new paid-call construction, recursive invoice, physical implementation,
+selected supplier admission or multiplication exponent. All five selected
+framework assumptions retain their status. Independent human and formal
+proof-kernel review are unclaimed.

research/clifford-transvection-conditioning/README.md

@@ -0,0 +1,102 @@
+# Three-qubit Clifford Gram condition bound 807
+
+Scoped written proof with exact finite corroboration, produced by Nick Petalas.
+For the full projective three-qubit Clifford alphabet and every integer `f >= 10`,
+
+\[
+ \frac{2835}{131072} I\preceq H_f\preceq\frac{2287845}{131072} I,
+ \qquad H_f(a,b)=\left(\operatorname{tr}(U_a^*U_b)/8\right)^f.
+\]
+
+The sufficient uniform spectral condition bound is **807**. This improves the
+6,456 bound of [alephnan's PR6714](https://github.com/CrocSwap/integer-mult-bounds/pull/6714):
+the lower endpoint increases sixfold and the upper endpoint decreases by a quarter.
+It is a sufficient interval; the exact spectrum and its sharp endpoints remain open.
+
+The new step is two affine inequalities on its thirty quotient-character types.
+Summing them against an actual irreducible's nonnegative multiplicities and using
+the predecessor's transvection trace bound proves the improved interval at width
+ten. Its Schur-product argument propagates that same interval to every larger width.
+[PROOF.md](PROOF.md) gives all hypotheses, the exact rational certificate, and
+attaining mixtures for the relaxation. This contribution does not improve the
+already proved threshold ten or the selected multiplication exponent.
+
+## Reproduce
+
+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/clifford-transvection-conditioning/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/clifford-transvection-conditioning/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/clifford-transvection-conditioning
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/clifford-transvection-conditioning --check-source-history
+```
+
+Another CPython 3.12 path can replace the absolute interpreter path. The direct
+verifier prints `PASS_CLIFFORD_TRANSVECTION_CONDITIONING` inside a generated JSON
+receipt with all thirty pairs of affine residuals, both orbit-specific bounds,
+the complete relaxed-vertex results, seven rejection controls, and every package
+file's SHA256. It writes no files. The registered runner executes both normal and
+optimized commands; all checks remain active under optimization.
+
+The finite arithmetic certifies the **new supporting inequalities and optimization**.
+It does not rerun the predecessor's character extraction, width-nine decomposition,
+threshold proof or native program. Exact source data are retained unchanged under
+`source/`, with hashes and public commit links in [ORIGIN.json](ORIGIN.json).
+[VALIDATION.md](VALIDATION.md) records executed checks and replay limits.
+
+## Claims and limitations
+
+The uniform implication rests on the written proof and the cited mathematical
+inputs of PR6714, including its identification of the published character table.
+The upper and lower relaxed optima are attained by convex mixtures, which need
+not correspond to actual irreducibles. No actual spectral endpoint or exact
+condition number is claimed. The 92,897,280-square Gram matrix is not constructed.
+
+This is a native-algebra side result. No physical caller, coefficient preparation,
+dirty restoration, precision/tape bill, complete recursive invoice, selected
+supplier admission or complete multiplication theorem is supplied. All five
+selected framework assumptions retain their status. No selected cold replay,
+Lean or Docker run was needed. Independent human and formal proof-kernel review
+are unclaimed.
+
+The `formal-interface-lemma` card is explicitly changed to this written spectral
+question. Its selected-source orientation passed; its proof-assistant acceptance
+gate is not claimed. Source-bound numerical data and classical representation
+and Schur-product facts remain credited premises.
+
+## Open next questions
+
+- Determine the actual width-ten spectral endpoints. Start with the two
+  quadratic-form stabilizer representation decompositions. Their additional
+  multiplicity constraints are the missing input; the relaxed witnesses do not
+  establish actual attainment.
+- Add one more phase-correct conjugacy-class trace constraint without computing
+  the whole even-sector table. Start by counting its fixed quadratic forms.
+  The single-transvection relaxation is solved exactly here, so a stronger
+  bound needs additional representation information.
+
+The same questions and blockers are structured in [TASK.json](TASK.json).
+
+## Related open work and credit
+
+[PR6714](https://github.com/CrocSwap/integer-mult-bounds/pull/6714) studies this
+same alphabet and Gram matrix. It proves threshold ten and supplies the cited
+multiplicities, trace bound and sufficient interval. This package answers part
+of its second open question by improving the interval, without rechecking those
+results. Its threshold and all exact source quantities are retained as inputs.
+
+[PR6718](https://github.com/CrocSwap/integer-mult-bounds/pull/6718) gives a
+written review of PR6714's even-sector argument and old constants. It is
+separate review coverage and does not derive this improved certificate.
+
+Credit alephnan for PR6714's theorem and representation-theoretic reduction;
+Chin-Yen Lee, Wei-Hsuan Yu, Yung-Ning Peng and Ching-Jui Lai for the published
+character table; Ali Romman for the Clifford trace/pointwise framework; MatShep
+for the sharp one- and two-qubit results; and Nick Petalas for the earlier lower
+bound and open question cited by PR6714. Affine linear programming, tensor
+reciprocity, character bounds and Schur products are classical. The new result
+is the improved source-specific certificate and its universal conditioning
+consequence. New work is Apache-2.0.
+
+[Advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19440708).

research/clifford-transvection-conditioning/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "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"
+    }
+  ]
+}