diff --git a/research/clifford-transvection-conditioning/ORIGIN.json b/research/clifford-transvection-conditioning/ORIGIN.json new file mode 100644 index 0000000000..6715142c4c --- /dev/null +++ b/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." +} diff --git a/research/clifford-transvection-conditioning/PROOF.md b/research/clifford-transvection-conditioning/PROOF.md new file mode 100644 index 0000000000..60a16b0578 --- /dev/null +++ b/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. diff --git a/research/clifford-transvection-conditioning/README.md b/research/clifford-transvection-conditioning/README.md new file mode 100644 index 0000000000..4d212aee94 --- /dev/null +++ b/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). diff --git a/research/clifford-transvection-conditioning/SOURCES.json b/research/clifford-transvection-conditioning/SOURCES.json new file mode 100644 index 0000000000..594089b9c7 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/clifford-transvection-conditioning/TASK.json b/research/clifford-transvection-conditioning/TASK.json new file mode 100644 index 0000000000..dee0707beb --- /dev/null +++ b/research/clifford-transvection-conditioning/TASK.json @@ -0,0 +1,113 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "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": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Improve the sufficient full three-qubit Clifford tensor-Gram interval at every width f >= 10 using a transvection-constrained multiplicity optimization.", + "scope_change_reason": "Take PR6714 open question 2 as a native-algebra side problem. This is a written conditioning proof with exact rational corroboration, not proof-assistant formalization or a discharge of a selected assumption.", + "bottleneck_link": "Quantitative native-alphabet conditioning controls coefficient recovery and identity tests. A physical caller, preparation/restoration prices and the complete signed supplier invoice remain separate; no kappa gain is inferred.", + "budget_minutes": 60, + "stop_rule": "Ship the first strict spectral improvement after an exact affine certificate and primal/dual verification; do not seek additional character constraints.", + "outcome": "completed", + "evidence": "PROOF.md; all thirty affine inequality pairs, both trace-slab optima and seven rejection controls in verify.py. The generated receipt binds every package file.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What are the actual sharp spectral endpoints of the width-ten three-qubit Gram matrix?", + "why_it_matters": "The new interval is sharp only for a one-trace relaxation; its extremal mixtures need not be actual irreducible decompositions.", + "first_step": "Obtain the two quadratic-form stabilizer representation decompositions and compare their multiplicity ratios with the new interval.", + "blocked_by": "The even-sector multiplicity constraints are not part of the retained thirty-point data." + }, + { + "question": "Can a second conjugacy-class trace bound improve the width-ten interval without a complete even-sector table?", + "why_it_matters": "The current one-transvection relaxation is now exactly solved, so an improvement within this approach needs additional information.", + "first_step": "Count fixed quadratic forms for one additional class and derive its phase-correct trace constraint.", + "blocked_by": "A rigorous source-compatible character bound for that class is needed before optimizing." + } + ], + "predecessor": { + "pr": 6714, + "author": "alephnan", + "head": "f7f32a18dde54e67624a9ed9cc7e1b266d9585c0", + "question": 2 + }, + "freshness": { + "canonical_main": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "priority_revision": 8, + "checked_utc": "2026-11-06T13:14:59.115235+00:00", + "overlap_limits": "Complete cached open-PR and Discussion pagination; targeted canonical README and merged-PR searches. Local sparse coverage incomplete; arbitrary diffs and unpublished work not covered." + } +} diff --git a/research/clifford-transvection-conditioning/VALIDATION.md b/research/clifford-transvection-conditioning/VALIDATION.md new file mode 100644 index 0000000000..0169c97b63 --- /dev/null +++ b/research/clifford-transvection-conditioning/VALIDATION.md @@ -0,0 +1,50 @@ +# Validation + +## Executed checks + +CPython 3.12.15, macOS 27.0.1 arm64, standard library only. Both declared +`VERIFY.json` commands passed locally with warnings treated as errors, in normal +and optimized modes. Measured direct times were 0.024 and 0.021 seconds, +respectively; these measurements establish the replay budget, not a speedup. +The registered launcher also passed both commands. + +Every run checks thirty lower and thirty upper affine residuals, and lists all +86 and 138 vertices of the two relaxed trace polytopes. The primal minima/maxima +match the dual affine bounds exactly. The seven semantic rejection controls +change a tight source row, omit the missing constituent, strengthen either +supporting line, reverse the transvection sign, or substitute an inadmissible +orbit size. All seven reject in normal and optimized modes. + +Two additional private-copy controls appended a space to each retained input, +one at a time. Both optimized runs rejected at the source hash gate, before +using mathematical data. Normal and optimized receipts agree byte for byte. +Receipts are generated from the actual execution and include all ten package +file hashes; there is no hand-written saved receipt. + +AST parsing/compilation and direct inspection cover the only new executable, +`verify.py`. Its largest function has 34 physical lines. It has no recursion, +dynamic code generation, subprocess or network use. There are two retained +scientific files, at most 30 character types, 435 unordered type pairs and two +trace boundary values per pair. Every read is capped at 262,144 bytes and the +receipt hashes a fixed ten-file list. Python's dynamic allocation is a declared +managed-runtime deviation from fixed-capacity allocation. The bounded inputs, +at most 900 candidate vertices per orbit, and sequential file reads bound live +data; interpreter and standard-library allocation are not instrumented. + +## Proof and review limits + +The proof was checked against its exact arithmetic certificate. Self-review +covered the use of quotient degrees, the sign and normalization of the trace +constraint, the two orbit sizes, both affine slopes, the Schur propagation, and +the distinction between relaxed and actual spectral attainment. No independent +human, external reviewer or proof kernel is claimed. + +No predecessor numerical engine or scientific verifier ran. The threshold, +multiplicity decomposition, group identification and Pauli-orbit trace argument +are cited mathematical premises from PR6714. Hash binding authenticates the +retained data, not the correctness of those inherited premises. + +The selected-source orientation passed. No selected cold replay, physical +native execution, full supplier invoice, Lean or Docker build was run. The five +selected framework assumptions remain. Hosted CI is pending; publication-byte, +source-history and export results are reported in the PR body after committing. diff --git a/research/clifford-transvection-conditioning/VERIFY.json b/research/clifford-transvection-conditioning/VERIFY.json new file mode 100644 index 0000000000..ffab3c8952 --- /dev/null +++ b/research/clifford-transvection-conditioning/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact retained input hashes; thirty lower/upper affine pairs; complete rational vertex optimization for N=28 and N=36; strict interval improvement; seven rejecting mutations; generated receipt bound to all package hashes." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact retained input hashes; thirty lower/upper affine pairs; complete rational vertex optimization for N=28 and N=36; strict interval improvement; seven rejecting mutations; generated receipt bound to all package hashes." + } + ] +} diff --git a/research/clifford-transvection-conditioning/source/pr6714-result.json b/research/clifford-transvection-conditioning/source/pr6714-result.json new file mode 100644 index 0000000000..77a5c8b23b --- /dev/null +++ b/research/clifford-transvection-conditioning/source/pr6714-result.json @@ -0,0 +1,494 @@ +{ + "status": "PASS_THREE_QUBIT_CLIFFORD_THRESHOLD_TEN", + "source_pins": 4, + "projective_order": 92897280, + "symplectic_order": 1451520, + "quotient_source_rows": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8, + 9, + 12, + 13, + 14, + 15, + 16, + 17, + 18, + 19, + 20, + 21, + 22, + 23, + 24, + 25, + 26, + 29, + 32, + 33, + 36, + 37, + 38 + ], + "quotient_source_classes": [ + [ + 1, + 2 + ], + [ + 3 + ], + [ + 4 + ], + [ + 5, + 6, + 7, + 8 + ], + [ + 9, + 10 + ], + [ + 11, + 12, + 13 + ], + [ + 14, + 15, + 16 + ], + [ + 17, + 18 + ], + [ + 19, + 20, + 21 + ], + [ + 22, + 23, + 24 + ], + [ + 25, + 26 + ], + [ + 27, + 28 + ], + [ + 29, + 30 + ], + [ + 31, + 32, + 33 + ], + [ + 34, + 35 + ], + [ + 36, + 37, + 38, + 39 + ], + [ + 40, + 41 + ], + [ + 42, + 43 + ], + [ + 44 + ], + [ + 45 + ], + [ + 46, + 47 + ], + [ + 48, + 49 + ], + [ + 50, + 51 + ], + [ + 52, + 53, + 54 + ], + [ + 55, + 56 + ], + [ + 57, + 58, + 59, + 60 + ], + [ + 61 + ], + [ + 62, + 63, + 64 + ], + [ + 65, + 66 + ], + [ + 67 + ] + ], + "quotient_class_sizes": [ + 1, + 2240, + 161280, + 945, + 672, + 7560, + 30240, + 60480, + 7560, + 315, + 10080, + 13440, + 40320, + 63, + 40320, + 3780, + 120960, + 3780, + 20160, + 120960, + 48384, + 145152, + 90720, + 11340, + 90720, + 45360, + 96768, + 10080, + 60480, + 207360 + ], + "fixed_dimensions": [ + 6, + 0, + 0, + 4, + 4, + 3, + 2, + 1, + 3, + 4, + 2, + 2, + 2, + 5, + 1, + 3, + 1, + 2, + 0, + 0, + 2, + 1, + 1, + 2, + 1, + 2, + 0, + 3, + 1, + 0 + ], + "transvection_column_one_based": 14, + "odd_tensor_multiplicities": { + "1": [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "3": [ + 0, + 1, + 1, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "5": [ + 0, + 5, + 5, + 10, + 0, + 0, + 0, + 0, + 4, + 0, + 1, + 5, + 0, + 0, + 0, + 0, + 5, + 6, + 0, + 0, + 0, + 4, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "7": [ + 30, + 0, + 1, + 0, + 28, + 104, + 105, + 0, + 0, + 0, + 35, + 0, + 70, + 35, + 120, + 126, + 7, + 0, + 42, + 140, + 35, + 20, + 140, + 0, + 0, + 28, + 21, + 90, + 70, + 64 + ], + "9": [ + 269, + 0, + 85, + 35, + 840, + 1890, + 1975, + 175, + 28, + 350, + 1407, + 210, + 2625, + 1575, + 3900, + 4410, + 945, + 567, + 2835, + 5250, + 2625, + 1728, + 5600, + 1400, + 1575, + 2940, + 2835, + 6075, + 5250, + 5440 + ], + "11": [ + 155, + 17204, + 23001, + 40953, + 5236, + 6138, + 11935, + 32725, + 86020, + 65450, + 60775, + 140250, + 45815, + 71995, + 41140, + 75922, + 207009, + 227205, + 106029, + 91630, + 137445, + 201960, + 157080, + 261800, + 294525, + 267036, + 318087, + 227205, + 274890, + 371008 + ], + "13": [ + 18383, + 632060, + 1008865, + 1640925, + 620620, + 721370, + 1098175, + 1884025, + 3918772, + 3768050, + 3861143, + 6782490, + 3878875, + 4765475, + 3989700, + 6250530, + 10927345, + 11530233, + 7912905, + 7757750, + 9420125, + 11454872, + 11525800, + 15072200, + 16956225, + 16579420, + 19217055, + 16956225, + 18840250, + 24115520 + ] + }, + "odd_tensor_ranks": { + "1": 64, + "3": 45760, + "5": 8961920, + "7": 77913472, + "9": 92894144, + "11": 92897280, + "13": 92897280 + }, + "width_nine_nullity": 3136, + "sharp_threshold": 10, + "quadratic_orbit_sizes": [ + 36, + 28 + ], + "transvection_fixtures": 63, + "remaining_degree_fractions": [ + "17/108", + "1/12" + ], + "uniform_spectral_bounds_from_ten": [ + "945/262144", + "762615/32768" + ], + "uniform_condition_upper_bound": 6456, + "negative_controls": [ + "changed table cell", + "wrong adjoint identification", + "discarded native fourth-power sign", + "omitted Pauli average", + "false width-nine independence", + "overfunded transvection trace", + "omitted odd-Arf orbit", + "even width through odd-sector formula" + ], + "scope": "Exact arithmetic supporting PROOF.md; the published character identification is a cited input, not reconstructed." +} diff --git a/research/clifford-transvection-conditioning/source/pr6714-table.json b/research/clifford-transvection-conditioning/source/pr6714-table.json new file mode 100644 index 0000000000..01f56d329a --- /dev/null +++ b/research/clifford-transvection-conditioning/source/pr6714-table.json @@ -0,0 +1,4649 @@ +{ + "schema": "published-character-table/v1", + "source": { + "title": "On character table of Clifford groups", + "authors": [ + "Chin-Yen Lee", + "Wei-Hsuan Yu", + "Yung-Ning Peng", + "Ching-Jui Lai" + ], + "arxiv": "2309.14850v2", + "url": "https://arxiv.org/html/2309.14850v2", + "section": "6.3", + "retrieved_utc": "2026-11-04", + "html_sha256": "02e0adebe50fcb4ff3cb1112600094d77c9457c45707df041486cbb4491c2a2e", + "description": "Numerical mathematical table entries extracted from six HTML panels, in published character and conjugacy-class order. No article prose is redistributed." + }, + "order": 92897280, + "adjoint_character_rows": [ + 1, + 10 + ], + "pauli_nonidentity_class": 2, + "characters": [ + [ + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + [ + 7, + 7, + -2, + 1, + 3, + 3, + 3, + 3, + 4, + 4, + -3, + -3, + -3, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + -1, + -1, + -1, + 2, + 2, + 1, + 1, + -1, + -1, + -5, + -5, + -5, + 1, + 1, + -1, + -1, + -1, + -1, + -1, + -1, + 3, + 3, + 2, + 0, + 2, + 2, + 0, + 0, + -1, + -1, + -1, + -1, + -1, + 1, + 1, + 1, + 1, + 1, + 1, + -1, + -2, + -2, + -2, + -2, + -2, + 0 + ], + [ + 15, + 15, + -3, + 0, + 3, + 3, + 3, + 3, + 0, + 0, + 1, + 1, + 1, + 0, + 0, + 0, + -2, + -2, + -3, + -3, + -3, + 7, + 7, + 7, + -2, + -2, + 3, + 3, + 1, + 1, + -5, + -5, + -5, + 1, + 1, + -1, + -1, + -1, + -1, + -1, + -1, + -1, + -1, + 1, + -1, + 0, + 0, + 0, + 0, + 1, + 1, + 3, + 3, + 3, + -1, + -1, + 1, + 1, + 1, + 1, + 0, + -2, + -2, + -2, + 0, + 0, + 1 + ], + [ + 21, + 21, + 3, + 0, + 5, + 5, + 5, + 5, + 6, + 6, + -3, + -3, + -3, + 2, + 2, + 2, + 0, + 0, + -3, + -3, + -3, + 5, + 5, + 5, + 2, + 2, + 0, + 0, + 2, + 2, + -11, + -11, + -11, + -2, + -2, + -3, + -3, + -3, + -3, + 0, + 0, + 1, + 1, + -1, + 1, + 1, + 1, + -1, + -1, + -1, + -1, + 1, + 1, + 1, + -1, + -1, + 1, + 1, + 1, + 1, + 1, + -2, + -2, + -2, + 0, + 0, + 0 + ], + [ + 21, + 21, + 3, + 0, + 1, + 1, + 1, + 1, + 6, + 6, + 3, + 3, + 3, + -2, + -2, + -2, + 0, + 0, + -1, + -1, + -1, + -3, + -3, + -3, + 0, + 0, + 0, + 0, + 0, + 0, + 9, + 9, + 9, + 0, + 0, + -3, + -3, + -3, + -3, + 0, + 0, + 5, + 5, + 3, + -1, + 1, + 1, + -1, + -1, + -1, + -1, + 1, + 1, + 1, + 1, + 1, + -1, + -1, + -1, + -1, + 1, + 0, + 0, + 0, + 2, + 2, + 0 + ], + [ + 27, + 27, + 0, + 0, + 7, + 7, + 7, + 7, + 9, + 9, + 5, + 5, + 5, + 1, + 1, + 1, + -1, + -1, + 1, + 1, + 1, + 3, + 3, + 3, + 3, + 3, + 0, + 0, + 0, + 0, + 15, + 15, + 15, + 0, + 0, + 3, + 3, + 3, + 3, + 0, + 0, + 3, + 3, + 0, + 0, + 2, + 2, + 0, + 0, + 1, + 1, + -1, + -1, + -1, + -1, + -1, + 1, + 1, + 1, + 1, + -1, + 3, + 3, + 3, + 1, + 1, + -1 + ], + [ + 35, + 35, + -1, + -1, + 7, + 7, + 7, + 7, + 5, + 5, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 5, + 5, + 5, + 11, + 11, + 11, + -1, + -1, + 2, + 2, + 2, + 2, + 15, + 15, + 15, + 0, + 0, + 3, + 3, + 3, + 3, + 0, + 0, + -1, + -1, + -1, + -1, + 0, + 0, + 0, + 0, + -1, + -1, + 3, + 3, + 3, + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 3, + 3, + 3, + -1, + -1, + 0 + ], + [ + 35, + 35, + -1, + -1, + -5, + -5, + -5, + -5, + 5, + 5, + -1, + -1, + -1, + 1, + 1, + 1, + -1, + -1, + -1, + -1, + -1, + 3, + 3, + 3, + -3, + -3, + 2, + 2, + 0, + 0, + -5, + -5, + -5, + -2, + -2, + 3, + 3, + 3, + 3, + 0, + 0, + 7, + 7, + 3, + 1, + 0, + 0, + 0, + 0, + 1, + 1, + -1, + -1, + -1, + 1, + 1, + -1, + -1, + -1, + -1, + 0, + 1, + 1, + 1, + -1, + -1, + 0 + ], + [ + 56, + 56, + 2, + -1, + 8, + 8, + 8, + 8, + 11, + 11, + -4, + -4, + -4, + -1, + -1, + -1, + -1, + -1, + 4, + 4, + 4, + -8, + -8, + -8, + 1, + 1, + 2, + 2, + -2, + -2, + -24, + -24, + -24, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -2, + 0, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + -3, + -3, + -3, + 1, + 1, + 0 + ], + [ + 63, + -1, + 0, + 0, + -1, + -1, + -1, + 15, + -1, + 15, + -1, + -1, + 7, + 3, + -1, + -1, + -1, + 1, + -1, + -1, + 7, + -1, + 15, + -1, + -1, + 3, + 3, + -1, + -1, + 3, + -1, + 31, + -1, + -1, + 1, + -1, + 7, + -1, + -1, + -1, + 1, + 3, + -1, + 0, + 0, + -1, + 3, + 1, + -1, + 1, + -1, + 3, + -1, + -1, + -1, + 1, + -1, + 3, + -1, + -1, + 0, + -1, + -1, + 7, + 1, + -1, + 0 + ], + [ + 63, + -1, + 0, + 0, + -1, + -5, + 3, + 11, + -1, + 15, + 1, + 1, + -7, + -1, + -1, + 3, + 1, + -1, + 1, + -3, + 5, + -1, + -9, + 7, + -1, + 3, + 3, + -1, + 1, + -3, + -1, + -29, + 3, + -1, + 1, + -1, + -1, + 3, + -5, + 1, + -1, + 3, + -1, + 0, + 0, + -1, + 3, + 1, + -1, + -1, + 1, + -1, + -1, + 3, + -1, + 1, + 1, + 1, + 1, + -3, + 0, + -1, + 3, + -5, + -1, + 1, + 0 + ], + [ + 70, + 70, + 7, + 1, + 6, + 6, + 6, + 6, + -5, + -5, + 2, + 2, + 2, + 3, + 3, + 3, + -1, + -1, + 2, + 2, + 2, + -10, + -10, + -10, + -1, + -1, + 1, + 1, + -1, + -1, + -10, + -10, + -10, + -1, + -1, + -2, + -2, + -2, + -2, + 1, + 1, + 2, + 2, + -1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 2, + 2, + 2, + 0, + 0, + -2, + -2, + -2, + -2, + 0, + -1, + -1, + -1, + -1, + -1, + 0 + ], + [ + 84, + 84, + 3, + 0, + 4, + 4, + 4, + 4, + -6, + -6, + 0, + 0, + 0, + -2, + -2, + -2, + 0, + 0, + 0, + 0, + 0, + 20, + 20, + 20, + 2, + 2, + 3, + 3, + -1, + -1, + 4, + 4, + 4, + 1, + 1, + 4, + 4, + 4, + 4, + 1, + 1, + 4, + 4, + -1, + 1, + -1, + -1, + -1, + -1, + 0, + 0, + 4, + 4, + 4, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + -2, + -2, + -2, + 0, + 0, + 0 + ], + [ + 105, + 105, + -3, + 0, + 5, + 5, + 5, + 5, + 15, + 15, + -5, + -5, + -5, + -1, + -1, + -1, + 1, + 1, + -1, + -1, + -1, + 1, + 1, + 1, + 1, + 1, + -3, + -3, + 1, + 1, + -35, + -35, + -35, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 5, + 5, + 1, + -1, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + -1, + -1, + -1, + -1, + -1, + -1, + 0, + 1, + 1, + 1, + -1, + -1, + 0 + ], + [ + 105, + 105, + 6, + 0, + 9, + 9, + 9, + 9, + 0, + 0, + -3, + -3, + -3, + 0, + 0, + 0, + 0, + 0, + -3, + -3, + -3, + -7, + -7, + -7, + -4, + -4, + 3, + 3, + -1, + -1, + 25, + 25, + 25, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + -3, + -3, + 2, + 0, + 0, + 0, + 0, + 0, + -1, + -1, + -3, + -3, + -3, + -1, + -1, + 1, + 1, + 1, + 1, + 0, + 4, + 4, + 4, + 0, + 0, + 0 + ], + [ + 105, + 105, + 6, + 0, + -3, + -3, + -3, + -3, + 0, + 0, + -1, + -1, + -1, + 0, + 0, + 0, + 2, + 2, + 3, + 3, + 3, + 17, + 17, + 17, + 2, + 2, + 3, + 3, + -1, + -1, + 5, + 5, + 5, + -1, + -1, + -7, + -7, + -7, + -7, + -1, + -1, + -3, + -3, + 2, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + -1, + -1, + -1, + -1, + -1, + -1, + 0, + 2, + 2, + 2, + 0, + 0, + 0 + ], + [ + 120, + 120, + -6, + 0, + 8, + 8, + 8, + 8, + 15, + 15, + 4, + 4, + 4, + -1, + -1, + -1, + 1, + 1, + -4, + -4, + -4, + -8, + -8, + -8, + 1, + 1, + 0, + 0, + -2, + -2, + 40, + 40, + 40, + -2, + -2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + -1, + -1, + 1 + ], + [ + 168, + 168, + 6, + 0, + 8, + 8, + 8, + 8, + 6, + 6, + 0, + 0, + 0, + 2, + 2, + 2, + 0, + 0, + 0, + 0, + 0, + 8, + 8, + 8, + 2, + 2, + -3, + -3, + -1, + -1, + 40, + 40, + 40, + 1, + 1, + 8, + 8, + 8, + 8, + -1, + -1, + 0, + 0, + 2, + 0, + -2, + -2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + -2, + -2, + -2, + 0, + 0, + 0 + ], + [ + 189, + 189, + 0, + 0, + 1, + 1, + 1, + 1, + 9, + 9, + -1, + -1, + -1, + 1, + 1, + 1, + -1, + -1, + -5, + -5, + -5, + 21, + 21, + 21, + 3, + 3, + 0, + 0, + 0, + 0, + -39, + -39, + -39, + 0, + 0, + -3, + -3, + -3, + -3, + 0, + 0, + -3, + -3, + 0, + 0, + -1, + -1, + 1, + 1, + -1, + -1, + 1, + 1, + 1, + 1, + 1, + -1, + -1, + -1, + -1, + -1, + 3, + 3, + 3, + 1, + 1, + 0 + ], + [ + 189, + 189, + 0, + 0, + 13, + 13, + 13, + 13, + 9, + 9, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + -3, + -3, + -3, + -3, + -3, + 0, + 0, + 0, + 0, + -51, + -51, + -51, + 0, + 0, + -3, + -3, + -3, + -3, + 0, + 0, + -3, + -3, + 0, + 0, + -1, + -1, + -1, + -1, + 1, + 1, + -3, + -3, + -3, + 1, + 1, + 1, + 1, + 1, + 1, + -1, + -3, + -3, + -3, + 1, + 1, + 0 + ], + [ + 189, + 189, + 0, + 0, + -11, + -11, + -11, + -11, + 9, + 9, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + 1, + -3, + -3, + -3, + -3, + -3, + 0, + 0, + 0, + 0, + 21, + 21, + 21, + 0, + 0, + -3, + -3, + -3, + -3, + 0, + 0, + 9, + 9, + 0, + 0, + -1, + -1, + 1, + 1, + -1, + -1, + 1, + 1, + 1, + -1, + -1, + 1, + 1, + 1, + 1, + -1, + -3, + -3, + -3, + 1, + 1, + 0 + ], + [ + 210, + 210, + 3, + 0, + 2, + 2, + 2, + 2, + 15, + 15, + 2, + 2, + 2, + -1, + -1, + -1, + -1, + -1, + 2, + 2, + 2, + 2, + 2, + 2, + -1, + -1, + 0, + 0, + 2, + 2, + 50, + 50, + 50, + 2, + 2, + -6, + -6, + -6, + -6, + 0, + 0, + -2, + -2, + -1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + -2, + -2, + -2, + 0, + 0, + -2, + -2, + -2, + -2, + 0, + -1, + -1, + -1, + -1, + -1, + 0 + ], + [ + 210, + 210, + -6, + 0, + 10, + 10, + 10, + 10, + -15, + -15, + -2, + -2, + -2, + 1, + 1, + 1, + 1, + 1, + -2, + -2, + -2, + -14, + -14, + -14, + 1, + 1, + 3, + 3, + 1, + 1, + 10, + 10, + 10, + 1, + 1, + 2, + 2, + 2, + 2, + -1, + -1, + 6, + 6, + -2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -2, + -2, + -2, + 0, + 0, + -2, + -2, + -2, + -2, + 0, + 1, + 1, + 1, + 1, + 1, + 0 + ], + [ + 216, + 216, + 0, + 0, + 8, + 8, + 8, + 8, + -9, + -9, + 4, + 4, + 4, + -1, + -1, + -1, + 1, + 1, + -4, + -4, + -4, + 24, + 24, + 24, + -3, + -3, + 0, + 0, + 0, + 0, + -24, + -24, + -24, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + -3, + -3, + -3, + -1, + -1, + -1 + ], + [ + 280, + 280, + -8, + 1, + 8, + 8, + 8, + 8, + -5, + -5, + -4, + -4, + -4, + -1, + -1, + -1, + -1, + -1, + 4, + 4, + 4, + 24, + 24, + 24, + -3, + -3, + -2, + -2, + 0, + 0, + 40, + 40, + 40, + -2, + -2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 1, + 1, + 1, + 0 + ], + [ + 280, + 280, + 10, + 1, + -8, + -8, + -8, + -8, + 10, + 10, + 0, + 0, + 0, + -2, + -2, + -2, + 0, + 0, + 0, + 0, + 0, + -8, + -8, + -8, + -2, + -2, + 1, + 1, + 1, + 1, + -40, + -40, + -40, + -1, + -1, + 8, + 8, + 8, + 8, + -1, + -1, + 0, + 0, + -2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2, + 2, + 2, + 0, + 0, + 0 + ], + [ + 315, + -5, + 0, + 0, + -5, + -5, + 11, + 11, + -2, + 30, + 3, + -1, + -9, + 2, + -2, + 2, + 0, + 0, + 3, + -1, + -9, + -5, + 27, + 11, + -2, + 6, + -3, + 1, + -1, + 3, + -5, + -85, + 11, + 1, + -1, + 3, + -5, + 3, + -13, + -1, + 1, + 3, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + 1, + 3, + -1, + -1, + 1, + -1, + 3, + -1, + -1, + -1, + 0, + -2, + 2, + 2, + 0, + 0, + 0 + ], + [ + 315, + -5, + 0, + 0, + -5, + 7, + -1, + 23, + -2, + 30, + -3, + 1, + 9, + 2, + -2, + 2, + 0, + 0, + -3, + 5, + -3, + -5, + 3, + 19, + -2, + 6, + -3, + 1, + 1, + -3, + -5, + 95, + -1, + 1, + -1, + -5, + 11, + -1, + 7, + 1, + -1, + 3, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + -1, + -1, + -1, + 3, + 1, + -1, + 1, + 1, + -3, + 1, + 0, + -2, + 2, + 2, + 0, + 0, + 0 + ], + [ + 315, + 315, + -9, + 0, + 3, + 3, + 3, + 3, + 0, + 0, + 3, + 3, + 3, + 0, + 0, + 0, + 0, + 0, + 3, + 3, + 3, + -21, + -21, + -21, + 0, + 0, + 0, + 0, + 0, + 0, + -45, + -45, + -45, + 0, + 0, + 3, + 3, + 3, + 3, + 0, + 0, + -5, + -5, + 3, + 1, + 0, + 0, + 0, + 0, + -1, + -1, + 3, + 3, + 3, + -1, + -1, + -1, + -1, + -1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 315, + -5, + 0, + 0, + -5, + -1, + 7, + 15, + 1, + -15, + 1, + -3, + 5, + -3, + 1, + 1, + 1, + -1, + 1, + 1, + -7, + -5, + 51, + 3, + 1, + -3, + 6, + -2, + 0, + 0, + -5, + -25, + 7, + -2, + 2, + 3, + 3, + -1, + -9, + 0, + 0, + 3, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + -1, + 7, + -1, + -5, + 1, + -1, + 1, + 1, + -3, + 1, + 0, + 1, + 1, + -7, + -1, + 1, + 0 + ], + [ + 315, + -5, + 0, + 0, + -5, + 3, + 3, + 19, + 1, + -15, + -1, + 3, + -5, + 1, + 1, + -3, + -1, + 1, + -1, + 3, + -5, + -5, + -21, + 27, + 1, + -3, + 6, + -2, + 0, + 0, + -5, + 35, + 3, + -2, + 2, + -5, + 3, + 3, + 3, + 0, + 0, + 3, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + 1, + -5, + -1, + 7, + 1, + -1, + 3, + -1, + -1, + -1, + 0, + 1, + -3, + 5, + 1, + -1, + 0 + ], + [ + 336, + 336, + -6, + 0, + -16, + -16, + -16, + -16, + 6, + 6, + 0, + 0, + 0, + 2, + 2, + 2, + 0, + 0, + 0, + 0, + 0, + 16, + 16, + 16, + -2, + -2, + 0, + 0, + -2, + -2, + -16, + -16, + -16, + 2, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -2, + 0, + 1, + 1, + -1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 2, + 2, + 2, + 0, + 0, + 0 + ], + [ + 378, + 378, + 0, + 0, + 2, + 2, + 2, + 2, + -9, + -9, + 2, + 2, + 2, + -1, + -1, + -1, + -1, + -1, + 2, + 2, + 2, + -6, + -6, + -6, + 3, + 3, + 0, + 0, + 0, + 0, + -30, + -30, + -30, + 0, + 0, + -6, + -6, + -6, + -6, + 0, + 0, + 6, + 6, + 0, + 0, + -2, + -2, + 0, + 0, + 0, + 0, + -2, + -2, + -2, + 0, + 0, + 2, + 2, + 2, + 2, + 1, + 3, + 3, + 3, + -1, + -1, + 0 + ], + [ + 378, + -6, + 0, + 0, + -2, + 2, + -6, + 34, + -3, + 45, + 2, + 2, + -14, + 1, + 1, + -3, + -1, + 1, + -2, + 2, + 2, + 2, + -6, + -6, + -1, + 3, + 0, + 0, + 0, + 0, + 6, + -126, + 2, + 0, + 0, + 2, + -6, + -2, + 6, + 0, + 0, + 6, + -2, + 0, + 0, + -1, + 3, + -1, + 1, + 0, + 0, + -2, + 2, + -2, + 0, + 0, + -2, + 2, + -2, + 2, + 0, + 3, + -1, + -9, + -1, + 1, + 0 + ], + [ + 378, + -6, + 0, + 0, + -2, + -14, + 10, + 18, + -3, + 45, + -2, + -2, + 14, + -3, + 1, + 1, + 1, + -1, + 2, + -2, + -2, + 2, + -6, + -6, + -1, + 3, + 0, + 0, + 0, + 0, + 6, + 114, + -14, + 0, + 0, + 2, + -6, + -2, + 6, + 0, + 0, + 6, + -2, + 0, + 0, + -1, + 3, + -1, + 1, + 0, + 0, + -2, + 2, + -2, + 0, + 0, + 2, + -2, + 2, + -2, + 0, + 3, + -5, + 3, + 1, + -1, + 0 + ], + [ + 405, + 405, + 0, + 0, + -3, + -3, + -3, + -3, + 0, + 0, + -3, + -3, + -3, + 0, + 0, + 0, + 0, + 0, + -3, + -3, + -3, + -27, + -27, + -27, + 0, + 0, + 0, + 0, + 0, + 0, + 45, + 45, + 45, + 0, + 0, + -3, + -3, + -3, + -3, + 0, + 0, + -3, + -3, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + 5, + 5, + 5, + 1, + 1, + 1, + 1, + 1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + -1 + ], + [ + 420, + 420, + -3, + 0, + -12, + -12, + -12, + -12, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 4, + 4, + 4, + 4, + 4, + 3, + 3, + 1, + 1, + 20, + 20, + 20, + -1, + -1, + 4, + 4, + 4, + 4, + 1, + 1, + -4, + -4, + 1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + -4, + -4, + -4, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -4, + -4, + -4, + 0, + 0, + 0 + ], + [ + 512, + 512, + 8, + -1, + 0, + 0, + 0, + 0, + -16, + -16, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -4, + -4, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + 0, + 0, + 0, + 0, + 0, + 1 + ], + [ + 567, + -9, + 0, + 0, + -9, + -1, + 15, + 15, + 0, + 0, + 3, + -5, + 3, + 0, + 0, + 0, + 0, + 0, + 3, + -5, + 3, + -9, + -9, + 39, + 0, + 0, + 0, + 0, + 0, + 0, + -9, + -81, + 15, + 0, + 0, + -1, + -9, + 7, + -9, + 0, + 0, + 3, + -1, + 0, + 0, + 1, + -3, + -1, + 1, + 1, + -1, + -5, + -1, + 7, + -1, + 1, + -1, + 3, + -1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 567, + -9, + 0, + 0, + -9, + 11, + 3, + 27, + 0, + 0, + -3, + 5, + -3, + 0, + 0, + 0, + 0, + 0, + -3, + 1, + 9, + -9, + 63, + 15, + 0, + 0, + 0, + 0, + 0, + 0, + -9, + 99, + 3, + 0, + 0, + -1, + 15, + -5, + 3, + 0, + 0, + 3, + -1, + 0, + 0, + 1, + -3, + -1, + 1, + -1, + 1, + 7, + -1, + -5, + -1, + 1, + 1, + 1, + 1, + -3, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 630, + -10, + 0, + 0, + 2, + -2, + -10, + 30, + -1, + 15, + -2, + 2, + 2, + 3, + -1, + -1, + 1, + -1, + 2, + 2, + -14, + -2, + 54, + -10, + 1, + -3, + 3, + -1, + -1, + 3, + 10, + -130, + -2, + 1, + -1, + -2, + -10, + 2, + 10, + 1, + -1, + -6, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2, + -2, + 2, + 0, + 0, + -2, + 2, + 2, + -2, + 0, + 1, + 1, + -7, + 1, + -1, + 0 + ], + [ + 630, + -10, + 0, + 0, + 2, + -2, + -10, + 30, + -1, + 15, + -2, + 2, + 2, + 3, + -1, + -1, + 1, + -1, + 2, + -6, + 10, + -2, + -42, + 22, + 1, + -3, + 3, + -1, + 1, + -3, + 10, + -130, + -2, + 1, + -1, + 6, + -2, + -6, + 2, + -1, + 1, + -6, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2, + -2, + 2, + 0, + 0, + 2, + -2, + -2, + 2, + 0, + 1, + 1, + -7, + 1, + -1, + 0 + ], + [ + 630, + -10, + 0, + 0, + -10, + 14, + 14, + -18, + -1, + 15, + 2, + -2, + -2, + 3, + -1, + -1, + -1, + 1, + 2, + -2, + -2, + -10, + 54, + 22, + -1, + 3, + 3, + -1, + 1, + -3, + -10, + -50, + 14, + -1, + 1, + 6, + -10, + -2, + -2, + 1, + -1, + -6, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2, + 2, + -6, + 0, + 0, + -2, + -2, + 2, + 2, + 0, + -1, + -1, + 7, + 1, + -1, + 0 + ], + [ + 630, + -10, + 0, + 0, + 2, + -18, + 6, + 14, + -1, + 15, + 2, + -2, + -2, + -1, + -1, + 3, + -1, + 1, + -2, + -2, + 14, + -2, + 54, + -10, + 1, + -3, + 3, + -1, + -1, + 3, + 10, + 110, + -18, + 1, + -1, + -2, + -10, + 2, + 10, + 1, + -1, + -6, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2, + -2, + 2, + 0, + 0, + 2, + -2, + -2, + 2, + 0, + 1, + -3, + 5, + -1, + 1, + 0 + ], + [ + 630, + -10, + 0, + 0, + 2, + -18, + 6, + 14, + -1, + 15, + 2, + -2, + -2, + -1, + -1, + 3, + -1, + 1, + -2, + 6, + -10, + -2, + -42, + 22, + 1, + -3, + 3, + -1, + 1, + -3, + 10, + 110, + -18, + 1, + -1, + 6, + -2, + -6, + 2, + -1, + 1, + -6, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2, + -2, + 2, + 0, + 0, + -2, + 2, + 2, + -2, + 0, + 1, + -3, + 5, + -1, + 1, + 0 + ], + [ + 630, + -10, + 0, + 0, + -10, + 22, + 6, + -10, + -1, + 15, + -2, + 2, + 2, + -1, + -1, + 3, + 1, + -1, + -2, + 2, + 2, + -10, + 6, + 38, + -1, + 3, + 3, + -1, + -1, + 3, + -10, + 70, + 6, + -1, + 1, + -2, + -2, + -2, + 14, + -1, + 1, + -6, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -6, + 2, + 2, + 0, + 0, + -2, + -2, + 2, + 2, + 0, + -1, + 3, + -5, + -1, + 1, + 0 + ], + [ + 945, + -15, + 0, + 0, + 1, + 1, + -15, + 49, + -3, + 45, + 1, + -3, + 5, + 1, + 1, + -3, + 1, + -1, + 1, + -3, + 5, + 1, + 33, + -15, + 1, + -3, + 0, + 0, + 0, + 0, + -15, + 225, + 1, + 0, + 0, + 1, + 9, + 1, + -15, + 0, + 0, + -3, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + 1, + -3, + 1, + 1, + 1, + -1, + -3, + 1, + 1, + 1, + 0, + -3, + 1, + 9, + -1, + 1, + 0 + ], + [ + 945, + -15, + 0, + 0, + 1, + -7, + 9, + -23, + -3, + 45, + 1, + 1, + -7, + 1, + 1, + -3, + 1, + -1, + 1, + 1, + -7, + 1, + 33, + -15, + 1, + -3, + 0, + 0, + 0, + 0, + -15, + -135, + 25, + 0, + 0, + 1, + 9, + -7, + 9, + 0, + 0, + 9, + -3, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + -1, + 1, + -3, + 5, + -1, + 1, + 1, + -3, + 1, + 1, + 0, + -3, + 1, + 9, + -1, + 1, + 0 + ], + [ + 945, + -15, + 0, + 0, + 1, + -27, + 13, + 21, + -3, + 45, + -1, + 3, + -5, + -3, + 1, + 1, + -1, + 1, + -1, + -1, + 7, + 1, + -39, + 9, + 1, + -3, + 0, + 0, + 0, + 0, + -15, + -195, + 29, + 0, + 0, + -7, + 9, + 5, + -3, + 0, + 0, + -3, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + -1, + 1, + 1, + -3, + 1, + -1, + -1, + -1, + 3, + -1, + 0, + -3, + 5, + -3, + 1, + -1, + 0 + ], + [ + 945, + -15, + 0, + 0, + 1, + 13, + -11, + -3, + -3, + 45, + -1, + -1, + 7, + -3, + 1, + 1, + -1, + 1, + -1, + 3, + -5, + 1, + -39, + 9, + 1, + -3, + 0, + 0, + 0, + 0, + -15, + 165, + 5, + 0, + 0, + 1, + -15, + 5, + -3, + 0, + 0, + 9, + -3, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + 1, + 5, + -3, + 1, + -1, + 1, + -1, + -1, + -1, + 3, + 0, + -3, + 5, + -3, + 1, + -1, + 0 + ], + [ + 1008, + -16, + 0, + 0, + -16, + 16, + 16, + 16, + 2, + -30, + 0, + 0, + 0, + -2, + 2, + -2, + 0, + 0, + 0, + 0, + 0, + -16, + 48, + 48, + 2, + -6, + -6, + 2, + 0, + 0, + -16, + 16, + 16, + 2, + -2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + 3, + 1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2, + -2, + -2, + 0, + 0, + 0 + ], + [ + 1260, + -20, + 0, + 0, + 4, + 12, + -4, + -52, + -2, + 30, + 0, + 0, + 0, + 2, + -2, + 2, + 0, + 0, + 0, + 0, + 0, + -4, + 12, + 12, + 2, + -6, + 6, + -2, + 0, + 0, + 20, + -20, + -20, + 2, + -2, + -4, + 12, + 4, + -12, + 0, + 0, + 12, + -4, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -4, + 4, + -4, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 2, + -2, + -2, + 0, + 0, + 0 + ], + [ + 1512, + -24, + 0, + 0, + -8, + -8, + 24, + -8, + -3, + 45, + -4, + 4, + 4, + 1, + 1, + -3, + -1, + 1, + 4, + -4, + -4, + 8, + -24, + -24, + -1, + 3, + 0, + 0, + 0, + 0, + 24, + 216, + -40, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + -3, + 1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 3, + -1, + -9, + -1, + 1, + 0 + ], + [ + 1512, + -24, + 0, + 0, + -8, + 24, + -8, + 24, + -3, + 45, + 4, + -4, + -4, + -3, + 1, + 1, + 1, + -1, + -4, + 4, + 4, + 8, + -24, + -24, + -1, + 3, + 0, + 0, + 0, + 0, + 24, + -264, + -8, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + -3, + 1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 3, + -5, + 3, + 1, + -1, + 0 + ], + [ + 1890, + -30, + 0, + 0, + -10, + 10, + 2, + 42, + 3, + -45, + 2, + -6, + 10, + 3, + -1, + -1, + -1, + 1, + -2, + 2, + 2, + 10, + -30, + -30, + 1, + -3, + 0, + 0, + 0, + 0, + 30, + -150, + -22, + 0, + 0, + 2, + -6, + -2, + 6, + 0, + 0, + 6, + -2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -2, + 2, + -2, + 0, + 0, + 2, + -2, + 2, + -2, + 0, + -3, + 5, + -3, + -1, + 1, + 0 + ], + [ + 1890, + -30, + 0, + 0, + 2, + -14, + 2, + 18, + 3, + -45, + -2, + 2, + 2, + 3, + -1, + -1, + 1, + -1, + -2, + 2, + 2, + 2, + -78, + 18, + -1, + 3, + 0, + 0, + 0, + 0, + -30, + -30, + 34, + 0, + 0, + -6, + -6, + 10, + -6, + 0, + 0, + 6, + -2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 6, + -2, + -2, + 0, + 0, + -2, + -2, + 2, + 2, + 0, + 3, + -5, + 3, + -1, + 1, + 0 + ], + [ + 1890, + -30, + 0, + 0, + -10, + -6, + 18, + 26, + 3, + -45, + -2, + 6, + -10, + -1, + -1, + 3, + 1, + -1, + 2, + -2, + -2, + 10, + -30, + -30, + 1, + -3, + 0, + 0, + 0, + 0, + 30, + 90, + -38, + 0, + 0, + 2, + -6, + -2, + 6, + 0, + 0, + 6, + -2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -2, + 2, + -2, + 0, + 0, + -2, + 2, + -2, + 2, + 0, + -3, + 1, + 9, + 1, + -1, + 0 + ], + [ + 1890, + -30, + 0, + 0, + 2, + -6, + -6, + 26, + 3, + -45, + 2, + -2, + -2, + -1, + -1, + 3, + -1, + 1, + 2, + -2, + -2, + 2, + 66, + -30, + -1, + 3, + 0, + 0, + 0, + 0, + -30, + 90, + 26, + 0, + 0, + 2, + 18, + -6, + -6, + 0, + 0, + 6, + -2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -2, + -2, + 6, + 0, + 0, + -2, + -2, + 2, + 2, + 0, + 3, + -1, + -9, + 1, + -1, + 0 + ], + [ + 2268, + -36, + 0, + 0, + -12, + 28, + 12, + -36, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 12, + -36, + -36, + 0, + 0, + 0, + 0, + 0, + 0, + 36, + -36, + -36, + 0, + 0, + -4, + 12, + 4, + -12, + 0, + 0, + -12, + 4, + 0, + 0, + -1, + 3, + -1, + 1, + 0, + 0, + 4, + -4, + 4, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 2520, + -40, + 0, + 0, + 8, + -24, + 8, + -24, + -1, + 15, + 4, + -4, + -4, + 3, + -1, + -1, + 1, + -1, + -4, + 4, + 4, + -8, + 24, + 24, + 1, + -3, + -6, + 2, + 0, + 0, + 40, + 200, + -56, + -2, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + 1, + -7, + 1, + -1, + 0 + ], + [ + 2520, + -40, + 0, + 0, + 8, + 8, + -24, + 8, + -1, + 15, + -4, + 4, + 4, + -1, + -1, + 3, + -1, + 1, + 4, + -4, + -4, + -8, + 24, + 24, + 1, + -3, + -6, + 2, + 0, + 0, + 40, + -280, + -24, + -2, + 2, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + -3, + 5, + -1, + 1, + 0 + ], + [ + 2520, + -40, + 0, + 0, + 8, + -8, + -8, + -8, + 2, + -30, + 0, + 0, + 0, + -2, + 2, + -2, + 0, + 0, + 0, + 0, + 0, + -8, + -72, + 56, + -2, + 6, + 3, + -1, + -1, + 3, + 40, + -40, + -40, + 1, + -1, + 8, + 8, + -8, + -8, + 1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -2, + 2, + 2, + 0, + 0, + 0 + ], + [ + 2520, + -40, + 0, + 0, + 8, + -8, + -8, + -8, + 2, + -30, + 0, + 0, + 0, + -2, + 2, + -2, + 0, + 0, + 0, + 0, + 0, + -8, + 120, + -8, + -2, + 6, + 3, + -1, + 1, + -3, + 40, + -40, + -40, + 1, + -1, + -8, + -8, + 8, + 8, + -1, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -2, + 2, + 2, + 0, + 0, + 0 + ], + [ + 2835, + -45, + 0, + 0, + 3, + -25, + 15, + -9, + 0, + 0, + -3, + 1, + 9, + 0, + 0, + 0, + 0, + 0, + -3, + 5, + -3, + 3, + 27, + -21, + 0, + 0, + 0, + 0, + 0, + 0, + -45, + -225, + 63, + 0, + 0, + 3, + 3, + -1, + -9, + 0, + 0, + -9, + 3, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + 1, + -5, + 3, + -1, + -1, + 1, + 1, + 1, + -3, + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 2835, + -45, + 0, + 0, + 3, + 11, + -21, + 27, + 0, + 0, + 3, + -1, + -9, + 0, + 0, + 0, + 0, + 0, + 3, + -1, + -9, + 3, + -45, + 3, + 0, + 0, + 0, + 0, + 0, + 0, + -45, + 315, + 27, + 0, + 0, + -5, + 3, + 3, + 3, + 0, + 0, + -9, + 3, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + -1, + -1, + 3, + -5, + -1, + 1, + 3, + -1, + -1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 2835, + -45, + 0, + 0, + 3, + 15, + -9, + -33, + 0, + 0, + -3, + 5, + -3, + 0, + 0, + 0, + 0, + 0, + -3, + 1, + 9, + 3, + 27, + -21, + 0, + 0, + 0, + 0, + 0, + 0, + -45, + 135, + 39, + 0, + 0, + 11, + -21, + -1, + -9, + 0, + 0, + 3, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 1, + -1, + -1, + -1, + 3, + 1, + -1, + 1, + 1, + 1, + -3, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + [ + 2835, + -45, + 0, + 0, + 3, + 3, + 3, + -45, + 0, + 0, + 3, + -5, + 3, + 0, + 0, + 0, + 0, + 0, + 3, + -5, + 3, + 3, + -45, + 3, + 0, + 0, + 0, + 0, + 0, + 0, + -45, + -45, + 51, + 0, + 0, + -5, + 3, + -5, + 27, + 0, + 0, + 3, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + 1, + 3, + -1, + -1, + 1, + -1, + -1, + 3, + -1, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ] + ] +} diff --git a/research/clifford-transvection-conditioning/verify.py b/research/clifford-transvection-conditioning/verify.py new file mode 100644 index 0000000000..0e215ba32c --- /dev/null +++ b/research/clifford-transvection-conditioning/verify.py @@ -0,0 +1,201 @@ +"""Exact affine certificates for the cited three-qubit multiplicity data. + +This reads predecessor data, never its verifier or character-decomposition code. +All acceptance checks remain enabled under optimized Python. +""" + +from fractions import Fraction +from hashlib import sha256 +from itertools import combinations +import json +from pathlib import Path + + +HERE = Path(__file__).resolve().parent +SOURCE_DIGESTS = { + "pr6714-result.json": "308b8dee094eb5481565ea89698ed5df69edeeecd4b63b4d78cb9cecdbe71c27", + "pr6714-table.json": "388d617a76e345774a8768f32a6a9bc6e94b87f9c8a5cf6712a95a5a3a945fcd", +} +MAX_FILE_BYTES = 262144 +PACKAGE_FILES = ( + "README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", + "ORIGIN.json", "VALIDATION.md", "verify.py", "source/pr6714-result.json", + "source/pr6714-table.json", +) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def bounded_bytes(path): + with path.open("rb") as stream: + payload = stream.read(MAX_FILE_BYTES + 1) + require(len(payload) <= MAX_FILE_BYTES, "file exceeds declared replay bound") + return payload + + +def source_points(): + sources = {} + for name, digest in SOURCE_DIGESTS.items(): + payload = bounded_bytes(HERE / "source" / name) + require(sha256(payload).hexdigest() == digest, "source hash: " + name) + sources[name] = json.loads(payload) + result = sources["pr6714-result.json"] + table = sources["pr6714-table.json"]["characters"] + indices = result["quotient_source_rows"] + multiplicities = result["odd_tensor_multiplicities"]["9"] + require(len(indices) == len(multiplicities) == 30, "thirty cited types") + require(len(set(indices)) == 30, "distinct source row indices") + column = result["transvection_column_one_based"] - 1 + fibre = result["quotient_source_classes"][column] + require(fibre == [31, 32, 33], "cited transvection fibre") + require(len(table) == 67, "cited table row count") + points = [] + for index, multiplicity in zip(indices, multiplicities): + require(type(index) is int and 1 <= index <= 67, "source row index") + row = table[index - 1] + require(len(row) == 67, "cited table column count") + degree, trace = row[0], row[fibre[0] - 1] + require(all(row[j - 1] == trace for j in fibre), "fibre identification") + points.append((index, degree, trace, multiplicity)) + validate_points(points) + require(result["projective_order"] == 92897280, "cited group order") + return tuple(points), Fraction(result["projective_order"], 8**10) + + +def validate_points(points): + require(len(points) == 30, "complete cited type list") + for index, degree, trace, multiplicity in points: + require(all(type(x) is int for x in (index, degree, trace, multiplicity)), + "integer character data") + require(degree > 0 and multiplicity >= 0, "positive degree and multiplicity") + require(abs(trace) <= degree, "character trace bound") + + +def affine_slacks(points, lower=(Fraction(5, 4), Fraction(7, 4)), + upper=(Fraction(1345, 12), Fraction(1883, 12))): + """An affine inequality at every type holds for every nonnegative mixture.""" + validate_points(points) + answer = [] + for index, degree, trace, multiplicity in points: + low = multiplicity - lower[0] * degree - lower[1] * trace + high = upper[0] * degree + upper[1] * trace - multiplicity + require(low >= 0, "lower affine certificate at row " + str(index)) + require(high >= 0, "upper affine certificate at row " + str(index)) + answer.append((index, str(low), str(high))) + return answer + + +def vertices(points, orbit_size): + """Enumerate all vertices of simplex intersected with one trace slab.""" + require(orbit_size in (28, 36), "the two cited Pauli orbit sizes") + cap = Fraction(16, orbit_size) + values = [] + for index, degree, trace, multiplicity in points: + if abs(Fraction(trace, degree)) <= cap: + values.append((Fraction(multiplicity, degree), index, index, + Fraction(1), Fraction(trace, degree))) + for first, second in combinations(points, 2): + i, degree_i, trace_i, multiplicity_i = first + j, degree_j, trace_j, multiplicity_j = second + x_i, x_j = Fraction(trace_i, degree_i), Fraction(trace_j, degree_j) + if x_i == x_j: + continue + for endpoint in (-cap, cap): + weight = (endpoint - x_j) / (x_i - x_j) + if 0 <= weight <= 1: + objective = (weight * Fraction(multiplicity_i, degree_i) + + (1 - weight) * Fraction(multiplicity_j, degree_j)) + values.append((objective, i, j, weight, endpoint)) + require(bool(values), "nonempty relaxed feasible region") + return values + + +def bounds(points, normalization): + expected = {28: (Fraction(1, 4), Fraction(807, 4)), + 36: (Fraction(17, 36), Fraction(19637, 108))} + answer = [] + for orbit_size in (28, 36): + cap = Fraction(16, orbit_size) + lower = Fraction(5, 4) - Fraction(7, 4) * cap + upper = Fraction(1345, 12) + Fraction(1883, 12) * cap + candidates = vertices(points, orbit_size) + minimum, maximum = min(candidates), max(candidates) + require((lower, upper) == expected[orbit_size], "derived orbit bounds") + require((minimum[0], maximum[0]) == (lower, upper), "primal/dual equality") + answer.append({"orbit": orbit_size, "vertices": len(candidates), + "multiplicity_bounds": [str(lower), str(upper)], + "gram_bounds": [str(normalization * lower), + str(normalization * upper)], + "minimizer": [str(x) for x in minimum[1:]], + "maximizer": [str(x) for x in maximum[1:]]}) + low, high = normalization / 4, normalization * Fraction(807, 4) + require(low == Fraction(2835, 131072), "uniform lower bound") + require(high == Fraction(2287845, 131072), "uniform upper bound") + require(high / low == 807, "uniform condition bound") + require(low == 6 * Fraction(945, 262144), "strict lower improvement") + require(high == Fraction(3, 4) * Fraction(762615, 32768), + "strict upper improvement") + return answer + + +def rejection_controls(points): + """Change a tight row or certificate; acceptance must fail at the real gate.""" + rejected = [] + for kind in ("low-row", "high-row", "missing-row", "low-line", "high-line", + "wrong-trace", "invalid-orbit"): + altered = list(points) + lower = (Fraction(5, 4), Fraction(7, 4)) + upper = (Fraction(1345, 12), Fraction(1883, 12)) + if kind == "low-row": + pos = next(i for i, row in enumerate(altered) if row[0] == 9) + index, degree, trace, multiplicity = altered[pos] + altered[pos] = (index, degree, trace, multiplicity - 1) + elif kind == "high-row": + index, degree, trace, multiplicity = altered[0] + altered[0] = (index, degree, trace, multiplicity + 1) + elif kind == "missing-row": + altered = [row for row in altered if row[0] != 2] + elif kind == "low-line": + lower = (lower[0] + Fraction(1, 10000), lower[1]) + elif kind == "high-line": + upper = (upper[0] - Fraction(1, 10000), upper[1]) + elif kind == "wrong-trace": + index, degree, trace, multiplicity = altered[1] + altered[1] = (index, degree, -trace, multiplicity) + try: + if kind == "invalid-orbit": + vertices(altered, 64) + else: + affine_slacks(altered, lower, upper) + except ValueError: + rejected.append(kind) + else: + raise ValueError("accepted mathematical mutation: " + kind) + return rejected + + +def package_hashes(): + return {name: sha256(bounded_bytes(HERE / name)).hexdigest() + for name in PACKAGE_FILES} + + +def main(): + points, normalization = source_points() + slacks = affine_slacks(points) + orbit_bounds = bounds(points, normalization) + controls = rejection_controls(points) + receipt = {"status": "PASS_CLIFFORD_TRANSVECTION_CONDITIONING", + "claim_type": "scoped proof with exact finite corroboration", + "type_count": len(points), "affine_slacks": slacks, + "orbit_bounds": orbit_bounds, "normalization": str(normalization), + "uniform_gram_bounds": ["2835/131072", "2287845/131072"], + "uniform_condition_bound": 807, "rejected_controls": controls, + "package_sha256": package_hashes()} + print(json.dumps(receipt, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()