From 1ac2f221a987b2cd0a5154e762ecad03b854eb60 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 23 Oct 2026 09:14:01 +0100 Subject: [PATCH] feat(research): tighten the three-cycle cut ceiling to 17/3 --- .../three-cycle-boolean-rounding/README.md | 191 ++++++++++++++++++ .../three-cycle-boolean-rounding/SOURCES.json | 24 +++ .../three-cycle-boolean-rounding/TASK.json | 89 ++++++++ .../three-cycle-boolean-rounding/VERIFY.json | 34 ++++ .../three-cycle-boolean-rounding/verify.py | 151 ++++++++++++++ 5 files changed, 489 insertions(+) create mode 100644 research/three-cycle-boolean-rounding/README.md create mode 100644 research/three-cycle-boolean-rounding/SOURCES.json create mode 100644 research/three-cycle-boolean-rounding/TASK.json create mode 100644 research/three-cycle-boolean-rounding/VERIFY.json create mode 100644 research/three-cycle-boolean-rounding/verify.py diff --git a/research/three-cycle-boolean-rounding/README.md b/research/three-cycle-boolean-rounding/README.md new file mode 100644 index 0000000000..322197ad3b --- /dev/null +++ b/research/three-cycle-boolean-rounding/README.md @@ -0,0 +1,191 @@ +# Boolean integrality lowers the three-cycle cut ceiling to 17/3 + +This is a **scoped proof conditional on a cited spectral theorem**, with an +exact finite certificate for the new arithmetic step. Every nonnegative +combination of register-independent permutation cuts has normalized value at +most `17t/3` for `t` coordinate-three-cycle target registers. Therefore final +rounding certifies at most 17 calls for three targets. It cannot certify the +direct `6t` tariff for any `t >= 3`. + +Krzysztof Wojt's [PR #5063](https://github.com/CrocSwap/integer-mult-bounds/pull/5063), +head `9ad4c47068f900fa1619191292539adcced0d638`, proves the preceding ceiling +`beta*t`, where `beta = (27 + 9*sqrt(2))/7`. Its obstruction to proving `6t` +starts at `t = 4`. This package adds Boolean integrality and moves that threshold +to three. It takes that spectral inequality as a mathematical premise; it does +not replay or independently validate the predecessor's certificate. + +The exact Boolean-cut optimum and actual multi-target word minimum remain +open. No shorter word, complete supplier, new kappa or selected-frontier change +is claimed. + +## Model and cited premise + +Use the formal coordinate-CNOT model of James Reed's +[#4968](https://github.com/CrocSwap/integer-mult-bounds/pull/4968) and its +credited predecessors. Work in `M_R(F2[GL_n(F2)])`, with `n >= 3` and `R >= t`. +A paid factor is `I + ([s]+[e]) N`, where `s = I+E_ij`, `i != j`, and `N` +is a rank-one idempotent. Scalar register mixing is free. Target roles carry +coordinate three-cycles, on possibly different triples and in either +orientation. Every other dirty register and address coordinate is restored. + +For a finite permutation action and a subset `A`, let +`out_A(g) = |{x in A : gx not in A}|`. Each cut uses the same `A` in every +register. The credited crossing-rank formulas give paid cost `out_A(s)` and +target value equal to the sum of its role crossing counts. + +The external spectral premise for the new rounding step is PR5063 equation (2). +For the six coordinate CNOTs `S` of any embedded `H = GL3(F2)` and either coordinate +three-cycle `c`, every finite permutation action satisfies + + 6 out_A(c) <= beta sum_{s in S} out_A(s). + +See its [pinned proof](https://github.com/CrocSwap/integer-mult-bounds/blob/9ad4c47068f900fa1619191292539adcced0d638/research/three-cycle-cut-ceiling/README.md). +That pending theorem is cited, not copied or checked here. The new verifier +has no runtime dependency on the pending branch. Its local PASS establishes +the new rounding and lifting facts, not the truth of that external premise. + +## 1. The regular-action integer constraints + +The group `H` has `7*6*4 = 168` elements. For any subset `B` in its regular +left action put + + k = out_B(c), d = sum_{s in S} out_B(s). + +The order-three permutation `c` has 56 disjoint three-cycles. Each cycle +contributes at most one exit, so `0 <= k <= 56`. + +Each CNOT is a fixed-point-free involution. Its regular-action edges form a +perfect matching. The six matchings form a loop-free 6-regular multigraph +with 504 edges. Counting degrees inside `B` gives + + d = 6 |B| - 2 e(B). + +Thus `d` is even and `0 <= d <= 504`. Multiplicities cause no problem for +this degree identity. When `d = 0`, the cited inequality implies `k = 0`. +For `d > 0`, the cited inequality gives `6k/d <= beta`. + +## 2. The new rational-gap lemma + +Suppose `k,d` satisfy those constraints and `6k/d > 17/3`. Write `d = 2m`. +Then `9k > 17m`. Since `k <= 56`, we have `17m < 504`, hence `m <= 29`. +Integrality now gives `9k >= 17m+1`, and therefore + + 6k/d = 3k/m >= 17/3 + 1/(3m) >= 17/3 + 1/87 = 494/87. + +But `beta < 494/87`. After moving the rational part and squaring positive +quantities, this is exactly + + 1109^2 - 162*87^2 = 3703 > 0. + +This contradicts the cited spectral inequality. Consequently + + 6k <= (17/3)d. + +The bounded verifier independently enumerates all 57 choices of `k` and all +252 positive even choices of `d`. It compares the spectral inequality by +integer squares, with no floating arithmetic. The maximum admissible ratio +is `17/3`, achieved among these scalar pairs exactly at `(17,18)`, `(34,36)` +and `(51,54)`. These are arithmetic witnesses, **not asserted realizable cuts**. +Thus `17/3` is sharp for these scalar constraints only. + +The hypotheses matter. Allowing odd `d` admits the scalar pair `(52,55)`; +allowing `k` up to 87 admits `(87,92)`. Both obey the spectral inequality but +exceed `17/3`. They are counterexamples to the weakened arithmetic statements, +not group-action constructions. + +## 3. Every finite action, dimension and dirty-register count + +Consider one `H`-orbit `O` of an arbitrary finite permutation action. Choose +`omega in O` and lift `A intersect O` to + + B = {g in H : g omega in A}. + +The map `g -> g omega` intertwines left multiplication with the given action, +and each fiber has the same size `h = |Stab_H(omega)|`. For every label `u`, + + out_B(u) = h out_{A intersect O}(u). + +Apply the new regular-action inequality, divide by the positive integer `h`, +and sum over the finitely many orbits. This proves + + 6 out_A(c) <= (17/3) sum_{s in S} out_A(s) + +for every finite `H` action. In `GL_n(F2)`, restrict to the subgroup on a +target's three coordinates. This restriction remains a finite permutation +action regardless of address spectators. Coordinate relabelling and inverse +cycles cover every target triple and orientation. + +Now take arbitrary nonnegative cut weights, including mixtures of finite +actions. Let `C_s` be the aggregate crossing cost of paid label `s`, and let +`M = max_s C_s`, over all paid coordinate-CNOT labels. For each target role +`r`, its aggregate value `D_r` satisfies + + D_r <= (17/18) sum_{s in S_r} C_s <= (17/3) M. + +If `M = 0`, all target values vanish. Otherwise summing over targets and +dividing by `M` bounds the normalized cut value by `17t/3`. Free scalar +register mixing and arbitrary restored dirty registers do not change these +credited cut formulas. Since `17t/3 <= 6t-1` for `t >= 3`, rounding the final +relaxation value up cannot prove `6t` for those target counts. + +## Evidence and reproduction + +From the repository root, use CPython 3.12 with no third-party dependencies: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/three-cycle-boolean-rounding +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/three-cycle-boolean-rounding/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/three-cycle-boolean-rounding --check-source-history +``` + +The registered replay also runs the verifier with `-O`. The arithmetic check +covers all 14,364 bounded scalar pairs. The lifting calibration enumerates all +128 subsets of the seven-point natural action and their regular lifts. It +checks equal-size fibers, every six-label crossing count, boundary parity and +the crossing cap. It does not recompute the predecessor's spectral identity +or any word minimum. Three controls reject a smaller asserted ceiling, an +omitted parity hypothesis and an omitted crossing cap. A generated stdout +report binds the checked package files with SHA-256 hashes. + +The mathematical result remains dependent on PR5063. No independent human +review, formal proof-kernel review, exact cut optimization, three-target word +search, native conversion, compiler/precision/storage admission, or selected +construction cold replay is supplied. There is no physical consumer or saving +claim requiring an expansion of this formal-model investigation. + +## Verifier resource bounds + +Power of Ten rule 3 has a managed-runtime deviation in `verify.py`: Python +allocates integers, fractions and collections during the check. The arithmetic +scan streams exactly 14,364 pairs. The orbit check retains 168 group elements +and seven maps of 168 entries, and streams 128 subsets. All loop bounds come +from these fixed fixtures; the verifier accepts no external parameters. The +registered warning-as-error normal and optimized runs verify the same bounds +and explicit failure controls. A fixed-allocation rewrite would require a +separate runtime and is deferred unless this small exact replay becomes a +resource bottleneck. All functions remain below 60 physical lines. No source +or output file is written by the verifier. + +## Open next questions + +1. Determine the exact Boolean-cut optimum on the 168-element regular action. + Start with a rigorous cut-cone primal/dual pair and a complete optimality + argument. No attaining cut or global optimization certificate is provided. +2. Decide three-target word additivity with an invariant beyond this cut cone. + Start with a nonlinear or integer label-count constraint that distinguishes + the three-target endpoint. No such invariant or complete word census is + provided here. + +The structured questions and blockers are also in [TASK.json](TASK.json). +Neither follow-up is reserved by this package. + +## Credit + +This contribution was produced by Nick Petalas. Krzysztof Wojt supplied the +spectral cut inequality and its all-action scope in PR5063. James Reed supplied +the cut-model formulas and preceding open question in PR4968, with the +single-target and two-target word results due to JoyboyBrian and James Reed in +PR4974 and PR5005. Credit also Mihir Srivastava, Ross Richardson, +commdata2338, Gareth Davidson, PR1541 and the retained register-model lineage. +Those results are cited and not claimed as new or independently reverified. +Independent human and formal proof-kernel review are unclaimed. Apache-2.0. diff --git a/research/three-cycle-boolean-rounding/SOURCES.json b/research/three-cycle-boolean-rounding/SOURCES.json new file mode 100644 index 0000000000..1bbbb0f7f6 --- /dev/null +++ b/research/three-cycle-boolean-rounding/SOURCES.json @@ -0,0 +1,24 @@ +{ + "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" + } + ] +} diff --git a/research/three-cycle-boolean-rounding/TASK.json b/research/three-cycle-boolean-rounding/TASK.json new file mode 100644 index 0000000000..47e4a56dbd --- /dev/null +++ b/research/three-cycle-boolean-rounding/TASK.json @@ -0,0 +1,89 @@ +{ + "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": "Boolean-integrality refinement of the three-cycle permutation-cut ceiling to 17/3 per target, conditional on the cited PR5063 spectral inequality.", + "scope_change_reason": "The live open question is the Boolean-cut ceiling in the coordinate-CNOT formal model. This derives a stronger obstruction for that proof method, rather than searching for a new native word.", + "bottleneck_link": "Three coordinate-three-cycle targets cannot have their direct 18-call tariff certified by the register-independent permutation-cut cone and final rounding. A stronger invariant is needed already at three targets.", + "budget_minutes": 60, + "stop_rule": "Stop at the first strict improvement of the cited cut ceiling; do not search for the exact cut optimum or a shorter word.", + "outcome": "negative-result", + "evidence": "README.md gives the orbit-lift, even-boundary, crossing-cap and rational-gap proof. verify.py checks every scalar pair in the declared bounded domain, all 128 seven-point subsets and their regular lifts, and three hypothesis-removal controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the exact Boolean-cut optimum for a coordinate three-cycle in the regular GL3(F2) action?", + "why_it_matters": "The 17/3 ceiling is sharp only for the retained scalar constraints, not known to be attained by a cut.", + "first_step": "Produce a rigorously certified cut-cone primal/dual pair on the 168-element regular action, with a complete optimality argument.", + "blocked_by": "No attaining Boolean cut or exact global Boolean optimization certificate is supplied." + }, + { + "question": "What invariant can decide three-target word additivity beyond the permutation-cut cone?", + "why_it_matters": "The direct three-target tariff is 18, while this cone with final rounding certifies at most 17.", + "first_step": "Identify a nonlinear or integer label-count constraint not implied by nonnegative permutation cuts; test it on the three-target endpoint.", + "blocked_by": "No new word invariant or complete three-target word census is supplied." + } + ], + "predecessor": { + "pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/5063", + "head": "9ad4c47068f900fa1619191292539adcced0d638", + "use": "Cited spectral inequality only; external mathematical dependency, not a replay input or a reverified result." + }, + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19141357", + "upstream_checked_at": "2026-10-23T08:12:09.171225+00:00", + "open_pr_snapshot": "2026-10-23T08:05:13.776187+00:00", + "discussion_snapshot": "2026-10-23T08:06:05.053211+00:00", + "coverage_limit": "Sparse local notes; main-tree grep and merged searches supplement, but do not guarantee novelty." + }, + "environment": { + "python": "3.12.15", + "interpreter": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12", + "system": "Darwin", + "release": "27.0.0", + "machine": "arm64" + } +} diff --git a/research/three-cycle-boolean-rounding/VERIFY.json b/research/three-cycle-boolean-rounding/VERIFY.json new file mode 100644 index 0000000000..56ba1d87b8 --- /dev/null +++ b/research/three-cycle-boolean-rounding/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 bounded integer-pair certificate, rational gap, regular-action orbit lifts, essential-hypothesis controls and source-bound report." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same complete new-step checks with assertions disabled." + } + ] +} diff --git a/research/three-cycle-boolean-rounding/verify.py b/research/three-cycle-boolean-rounding/verify.py new file mode 100644 index 0000000000..f6ba8300d5 --- /dev/null +++ b/research/three-cycle-boolean-rounding/verify.py @@ -0,0 +1,151 @@ +#!/usr/bin/env python3 +"""Check the new Boolean rounding step; the cited spectral premise is not replayed.""" + +import hashlib +import json +from fractions import Fraction +from pathlib import Path + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def spectral_scalar_pair(k: int, d: int) -> bool: + """Decide 6k/d <= (27+9 sqrt(2))/7 by integer arithmetic.""" + require(k >= 0 and d > 0, "invalid scalar pair") + rational_part = 42 * k - 27 * d + return rational_part <= 0 or rational_part**2 <= 162 * d**2 + + +def scalar_certificate() -> dict: + best = Fraction(0) + maximizers = [] + admitted = 0 + for k in range(57): + for d in range(2, 505, 2): + if not spectral_scalar_pair(k, d): + continue + admitted += 1 + ratio = Fraction(6 * k, d) + if ratio > best: + best = ratio + maximizers = [(k, d)] + elif ratio == best: + maximizers.append((k, d)) + require(best == Fraction(17, 3), "wrong arithmetic maximum") + require(maximizers == [(17, 18), (34, 36), (51, 54)], "wrong witnesses") + gap = 1109**2 - 162 * 87**2 + require(gap == 3703 and gap > 0, "invalid rational-gap proof") + require(Fraction(17, 3) + Fraction(1, 87) == Fraction(494, 87), "gap") + return {"pairs_checked": 57 * 252, "admitted_pairs": admitted, + "maximum": str(best), "maximizers": maximizers, "gap": gap} + + +def groups_and_labels() -> tuple: + group = tuple((a, b, c) for a in range(1, 8) for b in range(1, 8) + if b != a for c in range(1, 8) if c not in (a, b, a ^ b)) + require(len(group) == len(set(group)) == 168, "GL3 inventory") + labels = tuple((i, j) for i in range(3) for j in range(3) if i != j) + return group, labels + + +def natural_image(matrix: tuple, vector: int) -> int: + return sum(((row & vector).bit_count() & 1) << i + for i, row in enumerate(matrix)) + + +def cnot_matrix(matrix: tuple, i: int, j: int) -> tuple: + result = list(matrix) + result[i] ^= result[j] + return tuple(result) + + +def cnot_vector(vector: int, i: int, j: int) -> int: + return vector ^ (((vector >> j) & 1) << i) + + +def cycle_matrix(matrix: tuple) -> tuple: + return matrix[1], matrix[2], matrix[0] + + +def cycle_vector(vector: int) -> int: + return ((vector >> 1) & 1) | (((vector >> 2) & 1) << 1) | ((vector & 1) << 2) + + +def crossing(subset: set, permutation: dict) -> int: + return sum(permutation[x] not in subset for x in subset) + + +def orbit_lift_certificate() -> dict: + group, labels = groups_and_labels() + group_set = set(group) + paid = tuple({g: cnot_matrix(g, i, j) for g in group} for i, j in labels) + cycle = {g: cycle_matrix(g) for g in group} + require(all(set(p.values()) == group_set for p in paid), "paid bijections") + require(set(cycle.values()) == group_set, "cycle bijection") + require(all(p[p[g]] == g and p[g] != g for p in paid for g in group), + "regular matchings must be fixed-point-free involutions") + require(all(cycle[cycle[cycle[g]]] == g and cycle[g] != g for g in group), + "regular cycle must have order three and no fixed point") + fibers = [sum(natural_image(g, 1) == x for g in group) for x in range(1, 8)] + require(fibers == [24] * 7, "orbit fibers") + for mask in range(128): + subset = {x for x in range(1, 8) if (mask >> (x - 1)) & 1} + lift = {g for g in group if natural_image(g, 1) in subset} + boundary = 0 + for label_index, (i, j) in enumerate(labels): + natural = sum(cnot_vector(x, i, j) not in subset for x in subset) + lifted = crossing(lift, paid[label_index]) + require(lifted == 24 * natural, "paid crossing does not lift") + boundary += lifted + natural_k = sum(cycle_vector(x) not in subset for x in subset) + k = crossing(lift, cycle) + require(k == 24 * natural_k, "cycle crossing does not lift") + internal_twice = sum(p[g] in lift for p in paid for g in lift) + require(internal_twice % 2 == 0, "internal matching-edge parity") + require(boundary == 6 * len(lift) - internal_twice, "degree identity") + require(boundary % 2 == 0 and boundary <= 504, "boundary constraints") + require(k <= 56, "order-three crossing cap") + return {"group_order": len(group), "natural_subsets": 128, + "regular_lifts": 128, "fiber_size": 24} + + +def enforce_scalar_bound(k: int, d: int, bound: Fraction) -> None: + require(spectral_scalar_pair(k, d), "control must obey spectral premise") + require(Fraction(6 * k, d) <= bound, "proposed bound is false") + + +def hypothesis_controls() -> list: + controls = ((17, 18, Fraction(28, 5), "smaller ceiling"), + (52, 55, Fraction(17, 3), "parity omitted"), + (87, 92, Fraction(17, 3), "crossing cap omitted")) + rejected = [] + for k, d, bound, name in controls: + require(spectral_scalar_pair(k, d), "invalid negative-control premise") + try: + enforce_scalar_bound(k, d, bound) + except ValueError as error: + require(str(error) == "proposed bound is false", "wrong failure") + rejected.append(name) + else: + raise ValueError("negative control accepted: " + name) + require(len(rejected) == 3, "missing controls") + return rejected + + +def main() -> None: + report = {"status": "PASS_THREE_CYCLE_BOOLEAN_ROUNDING", + "scope": "New rounding/lifting step only; PR5063 spectral premise is cited.", + "scalar": scalar_certificate(), "lift": orbit_lift_certificate(), + "rejected_controls": hypothesis_controls()} + package = Path(__file__).resolve().parent + files = ("README.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + report["source_sha256"] = { + name: hashlib.sha256((package / name).read_bytes()).hexdigest() for name in files} + print(json.dumps(report, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()