From 9ad4c47068f900fa1619191292539adcced0d638 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Krzysztof=20W=C3=B3jt?= <97155365+krzysztofwojt@users.noreply.github.com> Date: Fri, 23 Oct 2026 09:38:48 +0200 Subject: [PATCH] Prove a uniform spectral ceiling for three-cycle permutation cuts --- research/three-cycle-cut-ceiling/README.md | 278 ++++++++++ research/three-cycle-cut-ceiling/SOURCES.json | 42 ++ research/three-cycle-cut-ceiling/TASK.json | 70 +++ research/three-cycle-cut-ceiling/VERIFY.json | 40 ++ .../three-cycle-cut-ceiling/independent.py | 501 ++++++++++++++++++ .../three-cycle-cut-ceiling/test_controls.py | 57 ++ research/three-cycle-cut-ceiling/verify.py | 215 ++++++++ 7 files changed, 1203 insertions(+) create mode 100644 research/three-cycle-cut-ceiling/README.md create mode 100644 research/three-cycle-cut-ceiling/SOURCES.json create mode 100644 research/three-cycle-cut-ceiling/TASK.json create mode 100644 research/three-cycle-cut-ceiling/VERIFY.json create mode 100644 research/three-cycle-cut-ceiling/independent.py create mode 100644 research/three-cycle-cut-ceiling/test_controls.py create mode 100644 research/three-cycle-cut-ceiling/verify.py diff --git a/research/three-cycle-cut-ceiling/README.md b/research/three-cycle-cut-ceiling/README.md new file mode 100644 index 0000000000..888c2c19b9 --- /dev/null +++ b/research/three-cycle-cut-ceiling/README.md @@ -0,0 +1,278 @@ +# A uniform ceiling for three-cycle permutation-cut certificates + +**Computer-assisted proof-method obstruction; no new kappa.** In the formal +coordinate-CNOT model of #4939/#4950/#4968, let `t` target registers carry +coordinate three-cycles, on arbitrary triples and in either orientation. +All other registers are dirty and restored; scalar register mixing is free. +For every finite address dimension `n >= 3` and register count `R >= t`, +every nonnegative combination of register-independent permutation cuts has +normalized target value at most + +\[ +\beta t,\qquad \beta=\frac{27+9\sqrt2}{7}=5.675417\ldots<\frac{23}{4}<6. +\] + +This includes **every subset of the regular representation**, every finite +permutation action, and mixtures of different actions. Consequently that +linear cut relaxation, followed by rounding up its final value, cannot prove +the direct `6t` tariff when `t >= 4`: its rounded value is at most `6t-1`. +This does **not** construct a word shorter than `6t` or exclude stronger uses +of integer call-count constraints. + +The constant is **sharp for the real quadratic domination used below**. +The optimum over Boolean cuts can be smaller and is **not determined here**. +In particular, this is not an exact certification of #4968's exploratory +approximately 3.51 cut value. + +## Delta and model + +James Reed's [#4968](https://github.com/CrocSwap/integer-mult-bounds/pull/4968) +proves mixed-transposition cut bounds and reports restricted order-pattern +optima, leaving arbitrary permutation cuts open. JoyboyBrian's +[#4974](https://github.com/CrocSwap/integer-mult-bounds/pull/4974) proves the +single-three-cycle word floor by formal support. James Reed's +[#5005](https://github.com/CrocSwap/integer-mult-bounds/pull/5005) proves two +three-cycles cost twelve at `n=3,R=2` by an exact word search. Those word +minima are not recomputed. The new result is a certified ceiling on the +**whole linear cut cone**, with a uniform lift beyond the 168-element group. + +Work in `M_R(F2[GL_n(F2)])`. A paid factor is +`D_N(g)=I+([g]+[e])N`, where `g=I+E_ij`, `i!=j`, and +`N=u v^T`, `v^T u=1`. Every such rank-one factor costs one. Scalar +`GL_R(F2)` maps are free. The endpoint is diagonal, with one coordinate +three-cycle in each of `t` roles and identity in all other roles. Equality +is formal, on arbitrary dirty inputs; no clean workspace or free address +map is introduced. + +For a finite permutation action on a set `Omega` and `A subset Omega`, write +`out_A(g)=|{x in A: gx not in A}|`. The cut in the register representation +is `A tensor F2^R`; the **same** `A` is used for every register. Its binary +cross-block rank `q_A` satisfies + +\[ +q_A(UV)\le q_A(U)+q_A(V),\quad q_A(\text{free scalar})=0, +\quad q_A(D_N(g))=\operatorname{out}_A(g), +\quad q_A(T)=\sum_{r=1}^t\operatorname{out}_A(c_r). +\] + +The product inequality follows by expanding its off-diagonal block. The +paid block is a partial permutation matrix tensored with a rank-one matrix; +the target blocks are separate direct summands. These are the credited +#4950/#4968 cut formulas. Subsequent real quadratic forms concern these +**integer crossing counts**; they do not lift formal binary endpoint +equalities to characteristic zero. + +## 1. The finite integer certificate + +In the integral group algebra of `H=GL3(F2)`, let `S` be its six coordinate +CNOTs, let `c:(x0,x1,x2)->(x1,x2,x0)`, and put + +\[ +\ell=6e-\sum_{s\in S}s,\qquad b=2e-c-c^2. +\] + +The exact coefficient identity is `p(ell)b=0`, where + +\[ +\begin{split} +p(X)={}&(X^2-6X+7)(X^2-14X+42)\\ + &\cdot(X-5)(X-6)(X-7)(X-9). +\end{split} +\] + +For an auditable expanded form, its coefficients from constant to leading +term are + +```text +555660, -1006362, 741006, -295897, 70871, -10494, 942, -47, 1. +``` + +[verify.py](verify.py) enumerates the 168 invertible three-row binary +matrices and evaluates this expression by exact integer convolution. Every +one of the 168 coefficients is zero. This is the finite computer-assisted +premise. Independently, [independent.py](independent.py) generates the group +as permutations of the seven nonzero vectors and checks the operator on +**all 168 basis columns**, with no imports from the primary implementation. +The regular representation is faithful, so the coefficient identity is an +identity in `Z[H]`, not only a numerical spectral observation. + +## 2. Quadratic domination, and its sharpness + +Apply any finite-dimensional real orthogonal representation of `H` to the +certificate and call the images `L` and `B`. Every CNOT is an involution, +so `L=sum_s(I-U_s)` is self-adjoint and positive semidefinite. Also +`B=2I-U_c-U_c^2` is self-adjoint, `B^2=3B`, and `LB=BL`: conjugation by `c` +permutes the six CNOTs. Thus `B/3` is an orthogonal projection. + +On `im B`, `p(L)=0`. The roots of `p` are + +```text +3-sqrt(2), 3+sqrt(2), 7-sqrt(7), 7+sqrt(7), 5, 6, 7, 9. +``` + +The smallest is `alpha=3-sqrt(2)>0`. Decompose `f=f0+f1`, with +`f0 in ker B` and `f1 in im B`. The spectral theorem and commutation give + +\[ +\langle f,Lf\rangle\ge\alpha\|f_1\|^2,\qquad +\langle f,(B/2)f\rangle=\tfrac32\|f_1\|^2. +\] + +Consequently + +\[ +6\langle f,(B/2)f\rangle\le +\frac9{3-\sqrt2}\langle f,Lf\rangle +=\beta\langle f,Lf\rangle.\tag{1} +\] + +Here is an exact witness that this **real quadratic** constant is optimal. +Let `q=p/(X^2-6X+7)` and, in the regular representation, set +`v=q(L)B delta_e`, `w=(L-3I)v`. Both verifiers check + +```text +(L-3I)w = 2v, Bv = 3v, +||v||^2 = 117151272, ||w||^2 = 234302544, + = -165676896, v,w each have 165 nonzero entries. +``` + +Then `a=v-w/sqrt(2)` is a nonzero vector with `La=alpha*a`, `Ba=3a`. +It is nonzero because nonzero rational vectors `v,w` cannot satisfy +`w=sqrt(2)*v`. It attains equality in (1). This real vector is not claimed +to be a Boolean cut; spectral sharpness does not settle the cut optimum. + +## 3. All cuts, all address dimensions, and all register counts + +For any permutation action, substitute `f=1_A` in (1). Permutations have +equally many entries into and exits from a subset, so + +\[ +\langle1_A,(I-U_s)1_A\rangle=\operatorname{out}_A(s),\qquad +\langle1_A,(B/2)1_A\rangle=\operatorname{out}_A(c). +\] + +The latter also uses `out_A(c)=out_A(c^-1)`. Hence every subset satisfies + +\[ +6\operatorname{out}_A(c)\le +\beta\sum_{s\in S}\operatorname{out}_A(s).\tag{2} +\] + +For `n>=3`, restrict any permutation action of `GL_n(F2)` to the embedded +`GL3(F2)` on a target's three coordinates. It is still an orthogonal +representation of that subgroup, so (2) holds for its six internal CNOTs. +All other coordinates are untouched by those six operators. No projection +from `GL_n` to `GL3`, clean-ancilla specialization, or bound on spectator +writes is needed. In the regular action this can equivalently be seen by +partitioning into orbits `H x` and summing the same inequality on each. +Coordinate relabelling and `c <-> c^-1` cover every target triple/orientation. + +Now choose arbitrary nonnegative cut weights, possibly on different finite +permutation actions. Let `C_g` be the resulting paid cost for a coordinate +CNOT `g`, and `D_r` the resulting crossing value of target `c_r`. Set +`M=max_g C_g`, taking the maximum over **all** paid address labels. Summing +(2) with the weights, for the six-label set `S_r` of target `r`, gives + +\[ +D_r\le\frac\beta6\sum_{g\in S_r}C_g\le\beta M, +\qquad Q(T)=\sum_rD_r\le\beta t M.\tag{3} +\] + +If `M=0`, the target value is zero and this combination supplies no bound. +Otherwise its ordinary subadditivity certificate is `calls >= Q(T)/M`, +and (3) bounds that certificate by `beta*t`. Weights can depend on `n,R,t`; +the argument does not. Extra dirty registers and dense scalar mixing do not +change the paid cross-block rank-one calculation. + +Finally `beta<23/4` follows from `36sqrt(2)<53`, or `2592<2809`. For `t>=4`, + +\[ +\beta t<6t-t/4\le6t-1, +\quad\text{so}\quad \lceil Q(T)/M\rceil\le6t-1. +\] + +This statement concerns nonnegative linear combinations and their final +rounding. It does not bound an integer program retaining every individual +label count, nonlinear combinations, non-coordinate subspace cuts, or the +actual word length. Direct concatenation still supplies the familiar `6t` +upper bound; whether calls can be shared remains a separate question. + +## Evidence and reproduction + +Python 3.12, standard library only; no numerical solver in verification: + +```sh +python3.12 -B scripts/research_package.py --package research/three-cycle-cut-ceiling +python3.12 -I -W error -B research/three-cycle-cut-ceiling/verify.py +python3.12 -I -O -W error -B research/three-cycle-cut-ceiling/independent.py +``` + +The registered replay runs both implementations normally and with `-O`. +The primary recomputes the group-algebra identity and sharpness vectors, +checks 144 literal binary paid cross-block ranks and four dirty endpoints, +and exhausts all 32,768 cuts of the natural 15-point `GL4` action with a +spectator coordinate. Those finite model checks corroborate (not replace) +the written lift. Altering the polynomial, omitting a CNOT, using an +order-two/identity target, assuming a rank-two paid factor has rank-one cost, +omitting a dirty-role restoration, and claiming a six-to-one crossing ratio +are distinct controls. The independent engine checks all 168 columns and +requires all corrupted operators to fail; its acceptance logic is also +tested on deliberately corrupted reports. +Actual CLI mutation tests reject twelve corrupted runs across normal and +optimized interpreters; reversing the cycle is accepted in both modes. +The complete registered replay passed locally on macOS arm64 / Python 3.12.12. + +Numerical exploration suggested the polynomial. A 45-second MILP probe did +not certify a Boolean-cut optimum; neither it nor floating eigensolutions +are acceptance evidence. Exact polynomial evaluation and the written +spectral argument are the evidence retained here. No predecessor word +census, full selected cold replay, Lean, Docker, or physical supplier run +is required or claimed. The selected-source metadata baseline passed; +that check is not scientific admission. + +## Scope and stopping decision + +This is a side result on a lower-bound proof method, with a changed +`bit-new-register-model` scope. It prevents an unrestricted permutation-cut +LP campaign from certifying `6t` by the stated linear mechanism for `t>=4`. +It establishes no supplier, compiler/stock/precision bill, actual sharing, +complete multiplication theorem, or new kappa. Selected `60403/20000000` +is unchanged. Stop at this certificate rather than enlarge the word search. + +## Open next questions + +1. **What is the Boolean-cut optimum at n=3?** It is at most `beta`, and can + be smaller. Start from an explicit cut/weight witness and a separately + certified global upper bound. The 2^168 cut domain and missing exact + optimization certificate remain the obstacle. More floating digits of + a feasible cut are not a solution. +2. **Can a different invariant prove multi-cycle additivity?** Target one + new obstruction, such as register interactions or constrained integer + label counts, beyond these nonnegative permutation-cut combinations. + Begin with a precise statement for four targets; neither this ceiling + nor the single-target support lemma supplies the needed additive bound. + +## Coordination and credit + +Canonical [claim and status](https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-19140523). +Fresh clone: `f259dabc7d70e0db8d6d36bfda888f008bbfecc1`; before claiming, +refreshed to the scientific base `4c0a359d88f22f05189d51f48387750b801a45d4`. +Priority revision 7 and governing guidance were unchanged. Entry overlap +covered complete pagination of 303 open PRs and 4,153 Discussion records, +plus 6,710 local notes, followed by live topic checks. This is bounded +overlap evidence, not a novelty guarantee. The claim began at fixed GL3; +the written representation restriction proves the all-dimension extension. +Exact predecessor bytes, selected record and task card are provenance pins +in [SOURCES.json](SOURCES.json), not live runtime dependencies. + +Credit James Reed / jwr404 (#4950, #4968, #5005) for the cut model and open +question; Mihir Srivastava (#4939) for the spectator model; JoyboyBrian +(#4974) for the formal-support theorem; Ross Richardson (#1989 and GL2 +corollary), commdata2338 (#1414/#1495), Gareth Davidson (#1333), #1541, and +their retained predecessor attribution. Their packages remain unchanged. + +Prepared by Krzysztof Wojt / krzysztofwojt with substantial OpenAI Codex +assistance. A Luna supporting agent supplied the independently represented +matrix checker; the primary agent reviewed it and owns the proof and +integration. These are same-session AI-assisted checks, not independent +human review or formal-kernel acceptance. Apache-2.0. diff --git a/research/three-cycle-cut-ceiling/SOURCES.json b/research/three-cycle-cut-ceiling/SOURCES.json new file mode 100644 index 0000000000..b1b097609b --- /dev/null +++ b/research/three-cycle-cut-ceiling/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "4c0a359d88f22f05189d51f48387750b801a45d4", + "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/swap-component-cut/README.md", + "usage": "provenance", + "git_blob": "19eaadc4ea40e312d202c917e2f1914d98ca224a", + "sha256": "7fe7efcb948a71af664d8f7828c8f4a056de3c6c3aa2cb82e420ec6ae7bd0106" + }, + { + "path": "research/swap-row-order-cut/README.md", + "usage": "provenance", + "git_blob": "941c1eb4f2301023757c45bbe1bb767962065cd1", + "sha256": "a5e9661f5ffa504cafee1c9481f0a1072b98341f98a031a2b4d18bb8c4a9ef7c" + }, + { + "path": "research/three-cycle-address-floor/README.md", + "usage": "provenance", + "git_blob": "6a65c91f29e5b226cebd32d0c1d6963a60a98761", + "sha256": "a63c4ea4c874cac1fb064e1aff07f8ef791391eb795aec22a2154eb44a8fa81e" + }, + { + "path": "research/two-three-cycle-additivity/README.md", + "usage": "provenance", + "git_blob": "6bbd51f92adebdf1e5ca8141251cc35f5990af7c", + "sha256": "b292e40966b928f26b407ae5c59b4ed9b8d4687d28076efbc759a8afdf62cdfb" + } + ] +} diff --git a/research/three-cycle-cut-ceiling/TASK.json b/research/three-cycle-cut-ceiling/TASK.json new file mode 100644 index 0000000000..4b8322d22d --- /dev/null +++ b/research/three-cycle-cut-ceiling/TASK.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 7, + "base_commit": "4c0a359d88f22f05189d51f48387750b801a45d4", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Certified ceiling beta*t, beta=(27+9*sqrt(2))/7, on every nonnegative permutation-cut combination for t coordinate-three-cycle targets, all finite address dimensions and register counts; sharp real quadratic domination, not the Boolean-cut optimum or word optimum.", + "scope_change_reason": "Take the explicit all-permutation-cut boundary left by PR4968 and PR4974 instead of repeating the GL3 word census or searching a larger register model. The initial fixed-GL3 certificate lifts to all finite dimensions by restriction to each target's embedded subgroup.", + "bottleneck_link": "Side result on a proof method: rules out this entire linear cut relaxation plus final rounding as a way to certify the full 6t tariff for t>=4. It directs any additivity proof to a stronger invariant, without asserting shared paid work or a supplier improvement.", + "budget_minutes": 240, + "stop_rule": "Stop after the exact group-algebra certificate, written uniform implication and bounded checks; no larger word census or Boolean-cut optimization campaign.", + "outcome": "partial", + "evidence": "Written cut-cone theorem from exact integer p(L)B=0, verified coefficientwise and independently on all 168 regular basis columns. Exact sharpness vectors, 144 binary paid cross-block checks, four dirty endpoints, all 32768 natural GL4 cuts, rejection controls and normal/optimized replay. No word optimum, Boolean-cut optimum, supplier admission, human or formal-kernel acceptance.", + "author": "Krzysztof Wojt / krzysztofwojt with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance. A Luna worker checked recent claims and implemented an independent seven-point-permutation matrix checker; the primary reviewed and integrated it and owns the written proof. Same-session AI assistance, not independent human review. Numerical exploration proposed the identity but is not acceptance evidence.", + "open_questions": [ + { + "question": "What is the exact Boolean-cut optimum for the GL3 three-cycle?", + "why_it_matters": "The sharp real quadratic ceiling can exceed the optimal nonnegative cut bound.", + "first_step": "Supply an explicit feasible cut/weight witness and an independently certified global upper bound, rather than more floating digits.", + "blocked_by": "The 2^168-cut domain and the absence of an exact global optimization certificate." + }, + { + "question": "Can an invariant beyond nonnegative permutation-cut combinations prove multi-cycle additivity?", + "why_it_matters": "The true 6t word tariff is separate from the ceiling on this proof method.", + "first_step": "State a precise stronger invariant for four targets, for example one retaining register interactions or integer label counts.", + "blocked_by": "No such additive invariant is supplied; the single-target support floor is not additive." + } + ] +} diff --git a/research/three-cycle-cut-ceiling/VERIFY.json b/research/three-cycle-cut-ceiling/VERIFY.json new file mode 100644 index 0000000000..845717e04c --- /dev/null +++ b/research/three-cycle-cut-ceiling/VERIFY.json @@ -0,0 +1,40 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact integer group-algebra identity, sharpness vectors, crossing-rank model binding, all natural GL4 cuts and rejecting controls." + }, + { + "argv": ["{python}", "-I", "-O", "-W", "error", "-B", "{package}/verify.py"], + "timeout_seconds": 60, + "checks": "Same certificate and controls with Python optimization enabled." + }, + { + "argv": ["{python}", "-I", "-W", "error", "-B", "{package}/independent.py"], + "timeout_seconds": 60, + "checks": "Independent seven-point permutation group and exact operators on all 168 basis columns, vector and corrupted-report checks." + }, + { + "argv": ["{python}", "-I", "-O", "-W", "error", "-B", "{package}/independent.py"], + "timeout_seconds": 60, + "checks": "Independent implementation and rejection controls with Python optimization enabled." + }, + { + "argv": ["{python}", "-I", "-W", "error", "-B", "{package}/test_controls.py"], + "timeout_seconds": 60, + "checks": "Actual CLI corruption rejections in normal and optimized interpreters, and inverse-cycle positive control." + } + ] +} diff --git a/research/three-cycle-cut-ceiling/independent.py b/research/three-cycle-cut-ceiling/independent.py new file mode 100644 index 0000000000..6bd4bc46b6 --- /dev/null +++ b/research/three-cycle-cut-ceiling/independent.py @@ -0,0 +1,501 @@ +#!/usr/bin/env python3 +"""Independent exact regular-representation check for GL(3, F_2). + +Group elements are literal permutations of the seven nonzero vectors. No +matrix package or parent scratch implementation is used. +Prepared by Krzysztof Wojt with substantial OpenAI Codex and Luna assistance. +Apache-2.0. This is same-session implementation corroboration, not human review. +""" + +from __future__ import annotations + +import json +from copy import deepcopy +from math import isqrt +from typing import Callable, Dict, List, Sequence, Tuple + + +Perm = Tuple[int, ...] +Vector = List[int] +POINTS: Tuple[int, ...] = tuple(range(1, 8)) +IDENTITY_PERM: Perm = POINTS + + +def compose(a: Perm, b: Perm) -> Perm: + """Return a after b, using image tuples on points 1 through 7.""" + return tuple(a[b[x - 1] - 1] for x in POINTS) + + +def cnot_permutation(target: int, source: int) -> Perm: + """Permutation induced by y_target=x_target XOR x_source.""" + if target == source or target not in range(3) or source not in range(3): + raise ValueError("CNOT coordinates must be distinct members of 0,1,2") + return tuple(x ^ (((x >> source) & 1) << target) for x in POINTS) + + +def cycle_permutation() -> Perm: + """Return (x0,x1,x2) -> (x1,x2,x0).""" + def rotate(x: int) -> int: + x0, x1, x2 = x & 1, (x >> 1) & 1, (x >> 2) & 1 + return x1 | (x2 << 1) | (x0 << 2) + + return tuple(rotate(x) for x in POINTS) + + +def make_generators() -> List[Perm]: + return [ + cnot_permutation(target, source) + for target in range(3) + for source in range(3) + if target != source + ] + + +def closure(generators: Sequence[Perm]) -> List[Perm]: + """BFS closure from identity, adjoining each literal permutation on left.""" + group = [IDENTITY_PERM] + seen = {IDENTITY_PERM} + cursor = 0 + while cursor < len(group): + current = group[cursor] + cursor += 1 + for generator in generators: + product = compose(generator, current) + if product not in seen: + seen.add(product) + group.append(product) + return group + + +def poly_mul(a: Sequence[int], b: Sequence[int]) -> List[int]: + result = [0] * (len(a) + len(b) - 1) + for i, x in enumerate(a): + for j, y in enumerate(b): + result[i + j] += x * y + return result + + +def make_polynomials() -> Tuple[List[int], List[int]]: + factors = [ + [7, -6, 1], + [42, -14, 1], + [-5, 1], + [-6, 1], + [-7, 1], + [-9, 1], + ] + p = [1] + for factor in factors: + p = poly_mul(p, factor) + q = [1] + for factor in factors[1:]: + q = poly_mul(q, factor) + if poly_mul(factors[0], q) != p: + raise RuntimeError("quotient construction does not reproduce p") + return p, q + + +class RegularOperators: + """Integer operators on coordinates indexed by the generated group.""" + + def __init__(self, group: Sequence[Perm], generators: Sequence[Perm]): + self.group = list(group) + self.index = {g: i for i, g in enumerate(self.group)} + self.size = len(self.group) + self.product = [ + [self.index[compose(g, h)] for h in self.group] + for g in self.group + ] + self.generator_indices = [self.index[g] for g in generators] + + def apply_p(self, g: int, vector: Sequence[int]) -> Vector: + result = [0] * self.size + row_for_column = self.product[g] + for column, value in enumerate(vector): + if value: + result[row_for_column[column]] += value + return result + + def apply_l( + self, + vector: Sequence[int], + generator_indices: Sequence[int] | None = None, + diagonal: int = 6, + ) -> Vector: + if generator_indices is None: + generator_indices = self.generator_indices + result = [diagonal * value for value in vector] + for generator in generator_indices: + row_for_column = self.product[generator] + for column, value in enumerate(vector): + if value: + result[row_for_column[column]] -= value + return result + + def apply_b(self, vector: Sequence[int], target: int) -> Vector: + target2 = self.product[target][target] + result = [2 * value for value in vector] + target_rows = self.product[target] + target2_rows = self.product[target2] + for column, value in enumerate(vector): + if value: + result[target_rows[column]] -= value + result[target2_rows[column]] -= value + return result + + +def apply_polynomial( + coefficients: Sequence[int], + vector: Sequence[int], + apply_l: Callable[[Sequence[int]], Vector], +) -> Vector: + """Horner evaluation with coefficients listed from constant upward.""" + result = [coefficients[-1] * value for value in vector] + for coefficient in reversed(coefficients[:-1]): + result = apply_l(result) + result = [value + coefficient * base for value, base in zip(result, vector)] + return result + + +def first_nonzero(vector: Sequence[int]) -> int | None: + return next((i for i, value in enumerate(vector) if value), None) + + +def check_annihilation( + operators: RegularOperators, + polynomial: Sequence[int], + target: int, + generator_indices: Sequence[int] | None = None, + diagonal: int = 6, +) -> Dict[str, object]: + def selected_l(vector: Sequence[int]) -> Vector: + return operators.apply_l(vector, generator_indices, diagonal) + + failing_columns = 0 + first_failure = None + for column in range(operators.size): + basis = [0] * operators.size + basis[column] = 1 + residual = apply_polynomial( + polynomial, operators.apply_b(basis, target), selected_l + ) + row = first_nonzero(residual) + if row is not None: + failing_columns += 1 + if first_failure is None: + first_failure = { + "column_index": column, + "column_permutation": list(operators.group[column]), + "row_index": row, + "row_permutation": list(operators.group[row]), + "value": residual[row], + } + return { + "basis_columns_checked": operators.size, + "failing_columns": failing_columns, + "first_failure": first_failure, + "zero_on_all_basis_columns": failing_columns == 0, + } + + +def vector_summary(vector: Sequence[int]) -> Dict[str, object]: + l2_squared = sum(value * value for value in vector) + root = isqrt(l2_squared) + return { + "l2_norm_exact": str(root) if root * root == l2_squared else "sqrt(" + str(l2_squared) + ")", + "l2_squared": l2_squared, + "nonzero_entries": sum(value != 0 for value in vector), + "l1": sum(abs(value) for value in vector), + } + + +def target_order(operators: RegularOperators, target: int) -> int: + power = target + order = 1 + while power != 0: + power = operators.product[target][power] + order += 1 + if order > 1000: + raise AssertionError("finite permutation unexpectedly has large order") + return order + + +def run_check() -> Dict[str, object]: + generators = make_generators() + group = closure(generators) + operators = RegularOperators(group, generators) + group_index = operators.index + + target_perm = cycle_permutation() + target = group_index[target_perm] + target2 = operators.product[target][target] + p, q = make_polynomials() + + annihilation = check_annihilation(operators, p, target) + + identity_basis = [0] * operators.size + identity_basis[group_index[IDENTITY_PERM]] = 1 + b_identity = operators.apply_b(identity_basis, target) + v = apply_polynomial(q, b_identity, operators.apply_l) + lv = operators.apply_l(v) + w = [value - 3 * base for value, base in zip(lv, v)] + lw = operators.apply_l(w) + shifted_w = [value - 3 * base for value, base in zip(lw, w)] + bv = operators.apply_b(v, target) + twice_v = [2 * value for value in v] + thrice_v = [3 * value for value in v] + + v_summary = vector_summary(v) + w_summary = vector_summary(w) + dot_vw = sum(x * y for x, y in zip(v, w)) + main_vectors = { + "v_nonzero": any(v), + "w_nonzero": any(w), + "(L_minus_3I)w_equals_2v": shifted_w == twice_v, + "Bv_equals_3v": bv == thrice_v, + "v": v_summary, + "w": w_summary, + "v_dot_w": dot_vw, + } + + altered_p = list(p) + altered_p[0] += 1 + altered_constant = check_annihilation(operators, altered_p, target) + + omitted_generator = 0 + remaining_generator_indices = operators.generator_indices[1:] + missing_generator = check_annihilation( + operators, + p, + target, + generator_indices=remaining_generator_indices, + diagonal=5, + ) + missing_generator["omitted_permutation"] = list(generators[omitted_generator]) + + identity_target = group_index[IDENTITY_PERM] + identity_b = operators.apply_b(identity_basis, identity_target) + identity_v = apply_polynomial(q, identity_b, operators.apply_l) + identity_w = [ + value - 3 * base + for value, base in zip(operators.apply_l(identity_v), identity_v) + ] + + incorrect_target = operators.generator_indices[0] + incorrect_order = target_order(operators, incorrect_target) + incorrect_target_annihilation = check_annihilation( + operators, p, incorrect_target + ) + incorrect_b_identity = operators.apply_b(identity_basis, incorrect_target) + incorrect_v = apply_polynomial(q, incorrect_b_identity, operators.apply_l) + incorrect_w = [ + value - 3 * base + for value, base in zip(operators.apply_l(incorrect_v), incorrect_v) + ] + + return { + "schema": "regular-gl3-f2-spectral-check/v1", + "representation": "literal permutations of the seven nonzero 3-bit vectors", + "group_order": operators.size, + "generator_count": len(generators), + "target_permutation": list(target_perm), + "target_order": target_order(operators, target), + "polynomial_coefficients_low_to_high": p, + "quotient_coefficients_low_to_high": q, + "p_of_l_times_b": annihilation, + "vectors": main_vectors, + "controls": { + "altered_polynomial_constant_plus_one": altered_constant, + "one_cnot_generator_omitted": missing_generator, + "identity_target": { + "b_on_identity_is_zero": not any(identity_b), + "v_nonzero_expected_but_actual": any(identity_v), + "w_nonzero_expected_but_actual": any(identity_w), + "v": vector_summary(identity_v), + "w": vector_summary(identity_w), + }, + "incorrect_order_two_target": { + "target_permutation": list(generators[0]), + "target_order": incorrect_order, + "p_of_l_times_b": incorrect_target_annihilation, + "v_nonzero": any(incorrect_v), + "w_nonzero": any(incorrect_w), + "v": vector_summary(incorrect_v), + "w": vector_summary(incorrect_w), + }, + }, + "interpretation_limit": "finite implementation check only; the abstract regular-group-algebra implication requires a separate written proof", + } + + +def validate_report(report: Dict[str, object]) -> None: + """Fail closed unless the computed report matches every required check.""" + if not isinstance(report, dict): + raise RuntimeError("report must be a JSON object") + + expected = { + "schema": "regular-gl3-f2-spectral-check/v1", + "group_order": 168, + "generator_count": 6, + "target_permutation": [4, 1, 5, 2, 6, 3, 7], + "target_order": 3, + "polynomial_coefficients_low_to_high": [ + 555660, -1006362, 741006, -295897, 70871, -10494, 942, -47, 1 + ], + "quotient_coefficients_low_to_high": [79380, -75726, 29610, -6073, 689, -41, 1], + } + for key, value in expected.items(): + if report.get(key) != value: + raise RuntimeError(f"unexpected report field {key}: {report.get(key)!r}") + + annihilation = report.get("p_of_l_times_b") + if not isinstance(annihilation, dict): + raise RuntimeError("missing p(L)B result") + if annihilation.get("basis_columns_checked") != 168: + raise RuntimeError("p(L)B did not check all 168 basis columns") + if annihilation.get("failing_columns") != 0: + raise RuntimeError("p(L)B failed on one or more basis columns") + if annihilation.get("zero_on_all_basis_columns") is not True: + raise RuntimeError("p(L)B zero status is false") + if annihilation.get("first_failure") is not None: + raise RuntimeError("p(L)B unexpectedly reports a failing column") + + vectors = report.get("vectors") + if not isinstance(vectors, dict): + raise RuntimeError("missing vector checks") + for key in ( + "v_nonzero", + "w_nonzero", + "(L_minus_3I)w_equals_2v", + "Bv_equals_3v", + ): + if vectors.get(key) is not True: + raise RuntimeError(f"required vector check failed: {key}") + + expected_v = { + "l2_norm_exact": "sqrt(117151272)", + "l2_squared": 117151272, + "nonzero_entries": 165, + "l1": 108360, + } + expected_w = { + "l2_norm_exact": "sqrt(234302544)", + "l2_squared": 234302544, + "nonzero_entries": 165, + "l1": 153216, + } + for label, values in (("v", expected_v), ("w", expected_w)): + summary = vectors.get(label) + if not isinstance(summary, dict): + raise RuntimeError(f"missing {label} summary") + for key, value in values.items(): + if summary.get(key) != value: + raise RuntimeError(f"unexpected {label}.{key}: {summary.get(key)!r}") + if vectors.get("v_dot_w") != -165676896: + raise RuntimeError("unexpected v dot w") + + controls = report.get("controls") + if not isinstance(controls, dict): + raise RuntimeError("missing controls") + for key in ( + "altered_polynomial_constant_plus_one", + "one_cnot_generator_omitted", + ): + control = controls.get(key) + if not isinstance(control, dict): + raise RuntimeError(f"missing control {key}") + if control.get("basis_columns_checked") != 168: + raise RuntimeError(f"control {key} did not check all columns") + if control.get("failing_columns") != 168: + raise RuntimeError(f"control {key} did not reject every column") + if control.get("zero_on_all_basis_columns") is not False: + raise RuntimeError(f"control {key} reports unexpected annihilation") + if control.get("first_failure") is None: + raise RuntimeError(f"control {key} lacks a failure witness") + + identity = controls.get("identity_target") + if not isinstance(identity, dict): + raise RuntimeError("missing identity-target control") + if identity.get("b_on_identity_is_zero") is not True: + raise RuntimeError("identity target did not make B zero") + if identity.get("v_nonzero_expected_but_actual") is not False: + raise RuntimeError("identity-target v control is not zero") + if identity.get("w_nonzero_expected_but_actual") is not False: + raise RuntimeError("identity-target w control is not zero") + zero_summary = { + "l2_norm_exact": "0", + "l2_squared": 0, + "nonzero_entries": 0, + "l1": 0, + } + for label in ("v", "w"): + if identity.get(label) != zero_summary: + raise RuntimeError(f"identity-target {label} is not the zero vector") + + incorrect = controls.get("incorrect_order_two_target") + if not isinstance(incorrect, dict): + raise RuntimeError("missing incorrect-target control") + if incorrect.get("target_order") != 2: + raise RuntimeError("incorrect-target control is not order two") + incorrect_annihilation = incorrect.get("p_of_l_times_b") + if not isinstance(incorrect_annihilation, dict): + raise RuntimeError("missing incorrect-target annihilation result") + if incorrect_annihilation.get("basis_columns_checked") != 168: + raise RuntimeError("incorrect-target control did not check all columns") + if incorrect_annihilation.get("failing_columns") != 168: + raise RuntimeError("incorrect-target control did not reject every column") + if incorrect_annihilation.get("zero_on_all_basis_columns") is not False: + raise RuntimeError("incorrect-target control reports unexpected annihilation") + if incorrect_annihilation.get("first_failure") is None: + raise RuntimeError("incorrect-target control lacks a failure witness") + + +def run_validator_self_tests(report: Dict[str, object]) -> int: + """Prove key report corruptions are rejected without mutating report.""" + cases = [] + + corrupt = deepcopy(report) + corrupt["controls"]["identity_target"]["b_on_identity_is_zero"] = False + cases.append(("identity status", corrupt)) + + corrupt = deepcopy(report) + corrupt["group_order"] = 167 + cases.append(("group order", corrupt)) + + corrupt = deepcopy(report) + corrupt["vectors"]["v"]["l2_squared"] += 1 + cases.append(("norm", corrupt)) + + for control_name in ( + "altered_polynomial_constant_plus_one", + "one_cnot_generator_omitted", + ): + corrupt = deepcopy(report) + corrupt["controls"][control_name]["failing_columns"] = 0 + cases.append((control_name, corrupt)) + + corrupt = deepcopy(report) + corrupt["controls"]["incorrect_order_two_target"]["p_of_l_times_b"][ + "failing_columns" + ] = 0 + cases.append(("incorrect order-two target", corrupt)) + + for name, corrupted_report in cases: + try: + validate_report(corrupted_report) + except RuntimeError: + continue + raise RuntimeError(f"validator self-test failed to reject {name}") + return len(cases) + + +def main() -> None: + report = run_check() + validate_report(report) + self_tests_passed = run_validator_self_tests(report) + report["validator_self_tests_passed"] = self_tests_passed + print(json.dumps(report, sort_keys=True, separators=(",", ":"))) + + +if __name__ == "__main__": + main() diff --git a/research/three-cycle-cut-ceiling/test_controls.py b/research/three-cycle-cut-ceiling/test_controls.py new file mode 100644 index 0000000000..b43f0e2cc1 --- /dev/null +++ b/research/three-cycle-cut-ceiling/test_controls.py @@ -0,0 +1,57 @@ +#!/usr/bin/env python3 +"""Exercise real verifier entry points on private, deliberately changed copies. + +Krzysztof Wojt with OpenAI Codex assistance. Apache-2.0. +""" +import json +from pathlib import Path +import subprocess +import sys +import tempfile + + +PACKAGE = Path(__file__).resolve().parent + + +def run_source(source, optimized, directory): + path = directory / "mutant.py" + path.write_text(source, encoding="utf-8") + command = [sys.executable, "-I", "-W", "error", "-B"] + if optimized: + command.append("-O") + return subprocess.run(command + [str(path)], text=True, capture_output=True, timeout=20) + + +def main(): + source = (PACKAGE / "verify.py").read_text(encoding="utf-8") + independent = (PACKAGE / "independent.py").read_text(encoding="utf-8") + cases = [ + (source, "C = (2, 4, 1)", "C = (1, 2, 4)", "cycle order"), + (source, "FACTORS = ((7, -6, 1)", "FACTORS = ((8, -6, 1)", "expanded polynomial"), + (source, "ell = {E: 6,", "ell = {E: 5,", "p(L)B=0"), + (source, "b = {E: 2, C: -1, c2: -1}", "b = {E: 2, C: -1, c2: 1}", "B^2=3B"), + (source, "excess * excess <= 162 *", "excess * excess <= 225 *", "six-to-one"), + (independent, "[7, -6, 1],", "[8, -6, 1],", "RuntimeError"), + ] + rejected = 0 + with tempfile.TemporaryDirectory(prefix="three-cycle-cut-controls-") as name: + directory = Path(name) + for original, before, after, expected in cases: + if original.count(before) != 1: + raise ValueError(f"mutation anchor is not unique: {before}") + for optimized in (False, True): + result = run_source(original.replace(before, after), optimized, directory) + if result.returncode == 0 or expected not in result.stderr: + raise ValueError(f"corruption accepted or wrong failure: {before}, O={optimized}: {result.stderr}") + rejected += 1 + # Reversing the same three-cycle is legal and must not be rejected. + for optimized in (False, True): + result = run_source(source.replace("C = (2, 4, 1)", "C = (4, 1, 2)"), optimized, directory) + if result.returncode or json.loads(result.stdout)["status"] != "PASS_THREE_CYCLE_CUT_CEILING": + raise ValueError(f"inverse-cycle positive control failed: {result.stderr}") + print(json.dumps({"status": "PASS_CLI_CONTROLS", "rejected_corruptions": rejected, + "inverse_cycle_positive_runs": 2}, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/three-cycle-cut-ceiling/verify.py b/research/three-cycle-cut-ceiling/verify.py new file mode 100644 index 0000000000..76b7fdcf1c --- /dev/null +++ b/research/three-cycle-cut-ceiling/verify.py @@ -0,0 +1,215 @@ +#!/usr/bin/env python3 +"""Exact integer group-algebra certificate; Python 3.12, standard library only. + +Krzysztof Wojt, with substantial OpenAI Codex assistance. Apache-2.0. +The quantified implications are proved in README.md, not by sampling cuts. +""" +from itertools import permutations, product +import json + + +E = (1, 2, 4) +C = (2, 4, 1) +FACTORS = ((7, -6, 1), (42, -14, 1), (-5, 1), (-6, 1), (-7, 1), (-9, 1)) +EXPECTED_P = (555660, -1006362, 741006, -295897, 70871, -10494, 942, -47, 1) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def rank2(rows): + basis = {} + for row in rows: + while row: + pivot = row.bit_length() - 1 + if pivot in basis: + row ^= basis[pivot] + else: + basis[pivot] = row + break + return len(basis) + + +def multiply(a, b): + """Rows of a*b, acting on column addresses; no permutation representation.""" + return tuple((b[0] if r & 1 else 0) ^ (b[1] if r & 2 else 0) + ^ (b[2] if r & 4 else 0) for r in a) + + +def add(a, b, scale=1): + result = dict(a) + for g, coefficient in b.items(): + result[g] = result.get(g, 0) + scale * coefficient + if not result[g]: + del result[g] + return result + + +def convolution(a, b): + result = {} + for g, x in a.items(): + for h, y in b.items(): + k = multiply(g, h) + result[k] = result.get(k, 0) + x * y + return {g: x for g, x in result.items() if x} + + +def poly_product(factors): + result = [1] + for factor in factors: + out = [0] * (len(result) + len(factor) - 1) + for i, x in enumerate(result): + for j, y in enumerate(factor): + out[i + j] += x * y + result = out + return result + + +def evaluate(coefficients, operator, vector): + out = {} + for coefficient in reversed(coefficients): + out = add(convolution(operator, out), vector, coefficient) + return out + + +def below_ceiling(out_c, sum_out_g): + """6*out(c) <= ((27+9*sqrt(2))/7) * sum_g out(g), exactly.""" + need(out_c >= 0 and sum_out_g >= 0, "negative crossing count") + excess = 42 * out_c - 27 * sum_out_g + return excess <= 0 or excess * excess <= 162 * sum_out_g * sum_out_g + + +def cross_rank(action, cut, scalar_rows): + """Literal binary cross-block rank of P_action tensor scalar_rows.""" + size = len(scalar_rows) + rows = {} + for x in cut: + y = action[x] + if y in cut: + continue + for r, scalar_row in enumerate(scalar_rows): + rows[(y, r)] = rows.get((y, r), 0) ^ (scalar_row << (size * x)) + return rank2(rows.values()) + + +def model_checks(group, gates): + index = {g: i for i, g in enumerate(group)} + action = lambda g: [index[multiply(g, h)] for h in group] + cuts = [{index[E]}, {i for i, g in enumerate(group) if g[0] < g[1]}, + {i for i in range(168) if i % 5 < 2}, set(range(84))] + projectors = [] + for u, v in product(range(1, 4), repeat=2): + if (u & v).bit_count() % 2: + projectors.append([v if (u >> r) & 1 else 0 for r in range(2)]) + need(len(projectors) == 6, "rank-one projector inventory") + checked = 0 + for cut in cuts: + for g in gates: + perm = action(g) + crossing = sum(perm[x] not in cut for x in cut) + for projector in projectors: + need(cross_rank(perm, cut, projector) == crossing, "paid rank/crossing binding") + checked += 1 + forward, inverse = action(C), action(multiply(C, C)) + out_c = sum(forward[x] not in cut for x in cut) + need(out_c == sum(inverse[x] not in cut for x in cut), "inverse orientation") + target_rows = [0] * (3 * 168) + for x in cut: + for role, perm in enumerate((forward, inverse, list(range(168)))): + y = perm[x] + if y not in cut: + target_rows[3 * y + role] ^= 1 << (3 * x + role) + need(rank2(target_rows) == 2 * out_c, "two targets plus restored dirty role") + counts = [sum(action(g)[x] not in cut for x in cut) for g in gates] + need(below_ceiling(out_c, sum(counts)), "regular cut bound") + one = {index[E]} + need(cross_rank(action(gates[0]), one, [1, 2]) == 2, "rank-two control") + need(cross_rank(action(C), one, [1, 2, 4]) == 3, "unrestored third-role control") + return {"paid_cross_block_checks": checked, "dirty_endpoint_checks": len(cuts), + "rank_two_and_unrestored_role_controls": 2} + + +def spectator_action_checks(gates): + """Every cut in the 15-point natural GL4 action, with axis 3 a spectator.""" + points = range(1, 16) + + def perm(g): + return [sum(((row & x).bit_count() & 1) << i for i, row in enumerate(g)) + + (x & 8) - 1 for x in points] + + actions = [perm(g) for g in gates] + [perm(C)] + images = [] + for action in actions: + table = [0] * (1 << 15) + for cut in range(1, 1 << 15): + bit = cut & -cut + table[cut] = table[cut ^ bit] | (1 << action[bit.bit_length() - 1]) + images.append(table) + for cut in range(1 << 15): + counts = [(table[cut] & ~cut).bit_count() for table in images] + need(below_ceiling(counts[-1], sum(counts[:-1])), "spectator permutation cut") + return 1 << 15 + + +def verify(): + group = [g for g in product(range(1, 8), repeat=3) if rank2(g) == 3] + need(len(group) == 168 and len(set(group)) == 168, "GL3 enumeration") + gates = [] + for i, j in permutations(range(3), 2): + rows = list(E) + rows[i] ^= rows[j] + gates.append(tuple(rows)) + c2 = multiply(C, C) + need(multiply(c2, C) == E and C != E, "cycle order") + need(all(multiply(g, g) == E for g in gates), "CNOT involutions") + need({multiply(multiply(C, g), c2) for g in gates} == set(gates), "cyclic conjugation") + need(all(multiply(g, h) in set(group) for g in gates for h in group), "regular permutations") + ell = {E: 6, **{g: -1 for g in gates}} + b = {E: 2, C: -1, c2: -1} + need(convolution(ell, b) == convolution(b, ell), "L and B commute") + need(convolution(b, b) == {g: 3 * x for g, x in b.items()}, "B^2=3B") + p = poly_product(FACTORS) + q = poly_product(FACTORS[1:]) + need(tuple(p) == EXPECTED_P, "expanded polynomial") + need(not evaluate(p, ell, b), "integer group-algebra identity p(L)B=0") + v = evaluate(q, ell, b) + shifted = add(ell, {E: 1}, -3) + w = convolution(shifted, v) + need(v and w, "nonzero sharpness vectors") + need(convolution(shifted, w) == {g: 2 * x for g, x in v.items()}, "(L-3)w=2v") + need(convolution(b, v) == {g: 3 * x for g, x in v.items()}, "Bv=3v") + vv = sum(x * x for x in v.values()) + ww = sum(x * x for x in w.values()) + vw = sum(x * w.get(g, 0) for g, x in v.items()) + need((len(v), len(w), vv, ww, vw) == (165, 165, 117151272, 234302544, -165676896), + "sharpness vector receipt") + # Exact root separation and beta < 23/4: 3>sqrt(2), sqrt(7)<3, 36sqrt(2)<53. + need(9 > 2 and 9 > 7 and 36 * 36 * 2 < 53 * 53, "algebraic root bounds") + altered_p = list(p) + altered_p[0] += 1 + need(evaluate(altered_p, ell, b), "altered polynomial must fail") + missing_gate = add(add(ell, {gates[0]: 1}), {E: 1}, -1) + need(evaluate(p, missing_gate, b), "missing CNOT must fail") + wrong_b = {E: 1, gates[0]: -1} + need(evaluate(p, ell, wrong_b), "order-two target must fail") + need(not evaluate(q, ell, {}), "identity target cannot witness sharpness") + need(not below_ceiling(1, 1), "a claimed six-to-one crossing ratio must fail") + return { + "status": "PASS_THREE_CYCLE_CUT_CEILING", + "group_order": len(group), "integer_identity_coefficients": len(group), + "p_low_to_high": p, "q_low_to_high": q, + "sharp_spectral_ceiling": "(27+9*sqrt(2))/7", + "boolean_cut_optimum": "not determined", + "v_nonzero_coefficients": len(v), "w_nonzero_coefficients": len(w), + "v_norm_squared": vv, "w_norm_squared": ww, "v_dot_w": vw, + "coefficient_and_budget_controls": 5, + "source_model": model_checks(group, gates), + "natural_GL4_cuts": spectator_action_checks(gates), + "scope": "Exact finite algebra certificate for the written all-dimension cut-cone theorem; no word optimum or new kappa.", + } + + +if __name__ == "__main__": + print(json.dumps(verify(), indent=2, sort_keys=True))