From 828a1df15d5f5256f80e61c8d22b822846b76ae7 Mon Sep 17 00:00:00 2001 From: Cinna Davis <1337isnot1337@users.noreply.github.com> Date: Wed, 14 Oct 2026 02:47:01 -0500 Subject: [PATCH 1/2] Record exact S4 two-target register bound --- .../CERTIFICATE.json | 76 ++++ .../s4-two-target-cycle-seed6e525/CLAIM.md | 47 +++ .../s4-two-target-cycle-seed6e525/README.md | 111 ++++++ .../SOURCES.json | 54 +++ .../s4-two-target-cycle-seed6e525/TASK.json | 107 ++++++ .../s4-two-target-cycle-seed6e525/VERIFY.json | 24 ++ .../s4-two-target-cycle-seed6e525/verify.py | 325 ++++++++++++++++++ 7 files changed, 744 insertions(+) create mode 100644 research/s4-two-target-cycle-seed6e525/CERTIFICATE.json create mode 100644 research/s4-two-target-cycle-seed6e525/CLAIM.md create mode 100644 research/s4-two-target-cycle-seed6e525/README.md create mode 100644 research/s4-two-target-cycle-seed6e525/SOURCES.json create mode 100644 research/s4-two-target-cycle-seed6e525/TASK.json create mode 100644 research/s4-two-target-cycle-seed6e525/VERIFY.json create mode 100644 research/s4-two-target-cycle-seed6e525/verify.py diff --git a/research/s4-two-target-cycle-seed6e525/CERTIFICATE.json b/research/s4-two-target-cycle-seed6e525/CERTIFICATE.json new file mode 100644 index 0000000000..773e1941dd --- /dev/null +++ b/research/s4-two-target-cycle-seed6e525/CERTIFICATE.json @@ -0,0 +1,76 @@ +{ + "schema_version": 1, + "status": "PASS_S4_TWO_TARGET_CYCLE", + "outcome": "NO_WORD_THROUGH_FIVE_MINIMUM_SIX", + "group": "S4", + "group_order": 24, + "address_generators": [ + "s1=(12)", + "s2=(23)", + "s3=(34)" + ], + "scalar_registers": 3, + "rank_one_idempotents": 28, + "paid_generator_count": 84, + "target": "diag([s1*s2*s3],[s1*s2*s3],[e])", + "radius_left": 2, + "radius_right": 3, + "left_layer_counts": [ + 1, + 84, + 4697 + ], + "right_layer_counts": [ + 1, + 84, + 4697, + 232692 + ], + "left_state_count": 4782, + "right_state_count": 237474, + "intersection_count": 0, + "direct_call_count": 6, + "direct_word": [ + { + "address": "s1", + "u": 1, + "v": 1 + }, + { + "address": "s2", + "u": 1, + "v": 1 + }, + { + "address": "s3", + "u": 1, + "v": 1 + }, + { + "address": "s1", + "u": 2, + "v": 2 + }, + { + "address": "s2", + "u": 2, + "v": 2 + }, + { + "address": "s3", + "u": 2, + "v": 2 + } + ], + "witness_call_count": null, + "witness": null, + "semantic_controls": { + "all_paid_factors_literal_square_to_identity": true, + "single_call_omissions_rejected": 6, + "changed_third_role_rejected": true + }, + "complete_domain": "all ordered words of length <=5 over the 84 paid involutive factors; proved by radius-2/radius-3 exact meet", + "time_cap_seconds": 110, + "rss_cap_bytes": 1073741824, + "selected_kappa_claimed": false +} diff --git a/research/s4-two-target-cycle-seed6e525/CLAIM.md b/research/s4-two-target-cycle-seed6e525/CLAIM.md new file mode 100644 index 0000000000..c64cff6bf4 --- /dev/null +++ b/research/s4-two-target-cycle-seed6e525/CLAIM.md @@ -0,0 +1,47 @@ +LOCAL CLAIM AND RESULT — GitHub Discussion posting unavailable + +Track `bit-mechanisms`; OS seed `6e5256110feb8b034f6afef8802f497c`; task +`bit-new-register-model`; scope key `74c418ed2b3f8f8a98e2`; priority revision 3; +exact base `0b1cccf86e2f5132ed286a26ef0a681a495740ea`; selected-record SHA256 +`10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32`. +Local advisory expiry: `2026-10-14T09:37:35Z`. + +Question: in exact `F2[S4]` formal algebra, with three arbitrary dirty scalar +roles, can the target `diag([s1*s2*s3],[s1*s2*s3],[e])` be realized in at most +five calls `I+([s]+[e])N`? Here `s1=(12), s2=(23), s3=(34)` are each paid at +one call, `N` ranges over all 28 rank-one idempotents of `M3(F2)`, arbitrary +free scalar `GL3(F2)` mixing is normalized into the paid factors, and the +third role must be restored. The direct bill is six calls; a candidate saving +would be one call (16.7%). The model optimistically assigns no additional +hosting price to the third role or free scalar mixing and does not claim +physical compilation. + +Method/domain: exact `F2[S4]` coefficient matrices and all 84 paid factors. +A complete radius-two ball from identity and radius-three ball from target +covers every word of length at most five because every factor is an +involution. Stop at 110 seconds or 1 GiB RSS; report incomplete coverage if +capped. The actual run completed in 2.29 seconds at 60,576 KiB RSS on Python +3.12.3. + +Final overlap check: 405 open PR records were fetched over REST during +07:40–07:43Z; no exact S4/adjacent-transposition/four-cycle match appeared. +Nearest scopes are PR #1478 (UT3 central targets, r=2,3), PR #1705 (four GL2 +coordinate-SWAP targets at r=4), and PR #1711 (two AGL2 affine targets at r=2). +The cached complete discussion pagination has 351 records fetched at 07:28Z; +direct reads of #1167 and #1317 reached 07:22Z and 07:31Z and contain no S4 +claim. A fresh complete Discussion refresh failed with GitHub's GraphQL rate +limit error; REST GET succeeds, but this installation returns 404 for +Discussion comment create/update, so this claim was kept local. + +FINDING: the exact radius-two/radius-three meet has layer counts `[1,84,4697]` +and `[1,84,4697,232692]`, state totals 4,782 and 237,474, and zero meetings. +The direct six-call word passes. Literal convolution confirms all 84 factors +square to identity; six direct-word omissions and a changed-third-role endpoint +are rejected. Thus the declared S4 target has exact minimum six; the tested +one-call saving does not exist. This closes only the specified finite model. +No selected-supplier occurrence, recursive moment change, physical compiler +saving, or new κ is claimed. The selected binding-only baseline currently +reports the complex primitive as binding. + +Full package and deterministic receipt: `README.md`, `TASK.json`, +`CERTIFICATE.json`, `SOURCES.json`, `VERIFY.json`, and `verify.py`. diff --git a/research/s4-two-target-cycle-seed6e525/README.md b/research/s4-two-target-cycle-seed6e525/README.md new file mode 100644 index 0000000000..82a449f4a7 --- /dev/null +++ b/research/s4-two-target-cycle-seed6e525/README.md @@ -0,0 +1,111 @@ +# S4 two-target cycle mechanism — seed 6e525611 + +**Bounded bit-mechanism construction attempt; no new κ claimed.** + +## Scope and cost screen + +This is a changed `bit-new-register-model` assignment: the address group is +`S4`, the paid letters are the adjacent transpositions `s1=(12)`, `s2=(23)` +and `s3=(34)`, and each letter costs one call. There are three scalar roles +over `F2`; each call is `I + ([s]+[e])N` for one of the 28 rank-one +idempotents `N=uv^T`, `v^T u=1`. The target is +`diag([c],[c],[e])`, where `c=s1*s2*s3` is a 4-cycle. Every input role is +arbitrary and dirty, and all roles must be restored exactly. + +Free scalar `GL3(F2)` changes between paid calls are included: move each +change through the adjacent paid factors by conjugating its rank-one +idempotent, which preserves the set of all 28 idempotents. Augmentation +`[g] -> 1` makes every paid factor the identity and forces any final free +scalar map to be the identity as well. + +The direct word costs six calls, three for each copy of `c`. A useful local +construction must use at most five, saving at least one of the six paid +transpositions (16.7%). This bill counts every address letter, while granting +free `GL3(F2)` scalar mixing and the third role with no separate hosting or +allocation charge. Those are explicit optimistic assumptions. The endpoint +restores the dirty third role; no clean state, uncharged undo or extra address +letter is allowed. This screen is local only: it has not identified an +occurrence in the selected bit supplier, whose current selected baseline is +complex-primitive-bound. No recursive moment or selected κ change follows. + +The selected accepted record is `κ=836330098538459/500000000000000000` +(`certificates/selected-result.json`, SHA256 +`10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32`). Its +review is `docs/research/community-batch1099-review.md`, source manifest is +`research/community-frontier1094-audit/SELECTED-SOURCE.json`, certificate is +`research/community-frontier1094-audit/ASSEMBLY.json` (SHA256 +`1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045`), and +reproduction command is `make frontier1094-verify`. The selected-record +binding-only baseline was checked with the pinned `scripts/research_baseline.py`. + +## Exact result + +No word of at most five calls realizes this target. The direct six-call word +therefore has exact minimum six in the declared model. The search enumerates +the complete radius-two ball from the identity and radius-three ball from the +target using all 84 involutive factors. The shell counts are `[1,84,4697]` and +`[1,84,4697,232692]`, for 4,782 and 237,474 states; their intersection is +empty. Every coefficient is an exact 24-bit element of `F2[S4]`, not a test +under one representation of the address group. + +Completeness follows by splitting any word of length at most five as `A B` +with `|A|≤2` and `|B|≤3`. Every factor squares to identity, so `A=T B^-1` +for target `T`; a shorter word would put the same state in both enumerated +balls. A separate literal group-algebra matrix multiplier checks every factor +is involutive, verifies the six-call direct construction, rejects all six +single-call omissions, and rejects a changed third-role target. The optimized +meet uses byte-packed coefficients and exact right-convolution tables. + +The complete search took 2.29 seconds and peaked at 60,576 KiB RSS under +Python 3.12.3, well inside the 110-second/1-GiB implementation limits. No +partial search is used in the result. The full seed, base, catalogue and +selected-record pins are in [TASK.json](TASK.json) and [SOURCES.json](SOURCES.json). + +## Reproduce + +From the repository root: + +```sh +python3.12 -I -B research/s4-two-target-cycle-seed6e525/verify.py +python3.12 scripts/research_package.py --package research/s4-two-target-cycle-seed6e525 --check-only +python3.12 scripts/research_package.py --package research/s4-two-target-cycle-seed6e525 +``` + +To regenerate the deterministic receipt before replay, use +`python3.12 -I -B research/s4-two-target-cycle-seed6e525/verify.py --write`. +The direct word is the positive control; six omitted-call words and the +changed endpoint are semantic negative controls. The checker is an exact +bounded proof for this finite alphabet, not a proof assistant result. + +## Live overlap and coordination + +The final open-PR census covered 405 PR records via REST at 2026-10-14 +07:40–07:43Z. The nearest scopes were PR #1478 (the UT3 two-central-commutator +endpoint at two or three roles), PR #1705 (four coordinate-SWAP targets in +`F2[GL2(F2)]` at four roles), and PR #1711 (two affine targets in +`F2[AGL2(F2)]` at two roles). Discussion #1317 contains current AGL2 claims; +the cached complete discussion scan (351 records, fetched 07:28Z), plus direct +current reads of #1167 (through 07:22Z) and #1317 (through 07:31Z), showed no +S4/adjacent-transposition claim. +The S4 group, 4-cycle target, three-role dirty endpoint and adjacent- +transposition alphabet are distinct from those scopes. A current fresh +Discussion fetch and new claim post are unavailable: +GitHub GraphQL reports the account rate limit exceeded, and the installed REST +API has no create/update endpoint for Discussion comments. This local claim +card and package are being used while that limitation holds. + +## Open next questions + +No immediate next question is justified: the complete six-call minimum closes +the proposed S4 endpoint and removes the candidate saving. Searching another +target tuple or alphabet requires a new mechanism, separate overlap check and +fresh cost screen. + +## Credit + +The formal rational three-register bound and UT3 central-commutator study are +the immediate predecessors. Their changed alphabets and endpoints are pinned +in [SOURCES.json](SOURCES.json); live nearby PR heads are recorded in +[TASK.json](TASK.json). Prepared by Cinna Davis with substantial OpenAI Codex +assistance in scoping, exact search, verification and exposition. New work is +Apache-2.0. diff --git a/research/s4-two-target-cycle-seed6e525/SOURCES.json b/research/s4-two-target-cycle-seed6e525/SOURCES.json new file mode 100644 index 0000000000..4cdd32b69e --- /dev/null +++ b/research/s4-two-target-cycle-seed6e525/SOURCES.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "docs/research/community-batch1099-review.md", + "usage": "provenance", + "git_blob": "6cb6ec061a071a06a2d18cd4dc3e9a2b05d28099", + "sha256": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb" + }, + { + "path": "research/bit-dihedral-commutator/README.md", + "usage": "input", + "git_blob": "b7619a5d56f32daf7f48d6cc3a0e260c5a333510", + "sha256": "4f3f9df6d6d96a26ccb0fcd2ef947cce5d53b0d992da22e866f1e025be4c0492" + }, + { + "path": "research/bit-three-register-lower-bound/README.md", + "usage": "input", + "git_blob": "25e41c370c101a33a6deb978de08b03ed7539b79", + "sha256": "c12b33ef388deece0cbf891505a2ce2c0779a0c3a6cf1f0f7f7039bab59cbebd" + }, + { + "path": "research/community-frontier1094-audit/ASSEMBLY.json", + "usage": "provenance", + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" + }, + { + "path": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "usage": "provenance", + "git_blob": "6a75493790b4eff9c4a98051ef8b01d6aad0d5a8", + "sha256": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b" + }, + { + "path": "scripts/research_baseline.py", + "usage": "input", + "git_blob": "6b607b36eefd65718120ade3c8187681f11bf879", + "sha256": "59d9b04dc33e1bb3f81506d187243435de4902138a038b935e36ebaa5f37db67" + } + ] +} diff --git a/research/s4-two-target-cycle-seed6e525/TASK.json b/research/s4-two-target-cycle-seed6e525/TASK.json new file mode 100644 index 0000000000..4f8b5f957c --- /dev/null +++ b/research/s4-two-target-cycle-seed6e525/TASK.json @@ -0,0 +1,107 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json" + ], + "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.", + "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": "Write a complete operation alphabet outside one named premise and price a baseline before searching identities.", + "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." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "F2[S4] register word with three binary scalar roles; only paid address letters are adjacent transpositions s1=(12), s2=(23), s3=(34), at one call each; rank-one idempotent scalar mixers N=uv^T over F2 with v^Tu=1; target diag([c],[c],[e]) for c=s1*s2*s3 (a 4-cycle), with arbitrary dirty inputs; test whether any exact word uses at most five calls, versus the direct six-call word.", + "scope_change_reason": "The suggested nonabelian/new-register track is refined to a new address group and paid alphabet: adjacent transpositions in S4, three scalar roles, and two repeated 4-cycle targets. Recent live work already covers the same UT3 commutator target at r=2,3 (PR1478), coordinate-SWAP targets over GL2 at r=4 (PR1705), two affine targets over AGL2 (PR1711), and four-register rational frame relations (Discussion1700). The S4 target and alphabet do not duplicate those scopes.", + "bottleneck_link": "This attempt tests whether a new bit-register address alphabet offers a local cost reduction; the current selected binding-only screen reports the complex primitive as binding. The proposed S4 saving did not occur: exact minimum is six, so this mechanism yields no paid-call reduction or recursive-moment change.", + "budget_minutes": 60, + "stop_rule": "Completed: exact radius-2/radius-3 meet enumerated all words through length five. No word is found; six-call direct word verified. Search would stop and report incomplete if the 110-second code cap or 1-GiB RSS cap were reached. No widening to other targets or groups.", + "outcome": "negative-result", + "evidence": "Exact F2[S4] search over all 84 paid involutions. Identity-side layers [1,84,4697] (4782 states); target-side layers [1,84,4697,232692] (237474 states); intersection empty. Literal convolution checks all 84 generators square to identity, verifies the six-call direct word, rejects six single-call omissions and rejects the changed-third-role endpoint. Reproduced in 2.29 seconds at 60576 KiB RSS on Python 3.12.3; certificate is CERTIFICATE.json. This is a scoped exact minimum six in the declared model, not a physical supplier or kappa result.", + "author": "Cinna Davis", + "ai_assistance": "Substantial OpenAI Codex assistance in task refinement, exact group-algebra model, search implementation, verification and exposition.", + "open_questions": [], + "seed": "6e5256110feb8b034f6afef8802f497c", + "track": "bit-mechanisms", + "catalog_assessed_on": "2026-10-13", + "catalog_sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "discarded_excluded_draws": [], + "scope_key": "74c418ed2b3f8f8a98e2", + "predecessors": [ + { + "reference": "https://github.com/CrocSwap/integer-mult-bounds/pull/1478", + "head": "b30fdba48f3db70e3589ba740b0782b56ec0ba2e", + "base": "410026dc5513b87db92ae98571d1d5984c69a983", + "relationship": "Exact UT3 central-commutator minimum at two or three roles; different group from this S4 4-cycle target." + }, + { + "reference": "https://github.com/CrocSwap/integer-mult-bounds/pull/1705", + "head": "ad6b7d641b3e8576a95add7981fa75b6a8278fbc", + "base": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "relationship": "Four coordinate-SWAP targets in F2[GL2(F2)] at four roles; different address group and endpoint." + }, + { + "reference": "https://github.com/CrocSwap/integer-mult-bounds/pull/1711", + "head": "c2527419aa030fb71985d99f99e915d192e388bd", + "base": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "relationship": "Two affine targets in F2[AGL2(F2)] at two roles; different group, target and register count." + }, + { + "reference": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1700", + "relationship": "Active four-register rational frame mechanism claim; different algebra and endpoint." + }, + { + "reference": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1317#discussioncomment-18918291", + "relationship": "Active three-register AGL2 claim; different alphabet and target." + } + ], + "live_overlap": { + "open_pr_records": 405, + "open_pr_census_utc": "2026-10-14T07:40-07:43Z", + "discussion_cache_records": 351, + "discussion_cache_fetched_utc": "2026-10-14T07:28:35Z", + "discussion_search": "The cached complete pagination remains 351 records at 07:28:35Z; current REST reads of Discussions 1167 and 1317 reached 07:22:14Z and 07:31:14Z respectively. No S4/adjacent-transposition target claim found. GraphQL refresh is still rate-limited.", + "write_limit": "GitHub GraphQL returned API rate limit exceeded; REST GET is available but installed REST has no Discussion comment create/update route." + }, + "certificate_sha256": "ea12f262c8e1079a0be4f2e830a073221981e0617e830e95bb4af3ec699988c0", + "selected_record": { + "kappa": "836330098538459/500000000000000000", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "review": "docs/research/community-batch1099-review.md", + "source_manifest": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "certificate": "research/community-frontier1094-audit/ASSEMBLY.json", + "certificate_sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045", + "reproduce": "make frontier1094-verify" + }, + "no_open_questions_reason": "The exact six-call minimum closes the stated S4 target/alphabet. A different S4 target or address group would be a new mechanism and needs a separate cost screen; no narrow next experiment is justified from this bounded result." +} diff --git a/research/s4-two-target-cycle-seed6e525/VERIFY.json b/research/s4-two-target-cycle-seed6e525/VERIFY.json new file mode 100644 index 0000000000..f81c83b0f2 --- /dev/null +++ b/research/s4-two-target-cycle-seed6e525/VERIFY.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "research/bit-dihedral-commutator/README.md", + "research/bit-three-register-lower-bound/README.md", + "scripts/research_baseline.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Rebuild the complete exact S4 three-register radius-2/radius-3 meet over all 84 factors; verify all factors are involutions, the direct six-call target, empty intersection and six omission plus changed-endpoint controls; compare the deterministic certificate." + } + ] +} diff --git a/research/s4-two-target-cycle-seed6e525/verify.py b/research/s4-two-target-cycle-seed6e525/verify.py new file mode 100644 index 0000000000..232f5be388 --- /dev/null +++ b/research/s4-two-target-cycle-seed6e525/verify.py @@ -0,0 +1,325 @@ +"""Exact bounded S4 three-register paid-word search. Apache-2.0.""" +from __future__ import annotations + +import hashlib +import itertools +import json +import resource +import sys +import time +from pathlib import Path + + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +MAX_SECONDS = 110 +MAX_RSS_BYTES = 1024**3 +START = time.monotonic() + + +def need(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def check_budget() -> None: + elapsed = time.monotonic() - START + raw = resource.getrusage(resource.RUSAGE_SELF).ru_maxrss + rss = raw * (1024 if sys.platform.startswith("linux") else 1) + need(elapsed <= MAX_SECONDS, f"search time cap reached at {elapsed:.1f}s") + need(rss <= MAX_RSS_BYTES, f"search RSS cap reached at {rss} bytes") + + +# S4 is represented by permutations of four points. Multiplication composes +# functions right-to-left: (a*b)(i)=a(b(i)). +GROUP = tuple(itertools.permutations(range(4))) +GID = {g: i for i, g in enumerate(GROUP)} +IDENTITY_PERM = GID[tuple(range(4))] + + +def compose(a: tuple[int, ...], b: tuple[int, ...]) -> tuple[int, ...]: + return tuple(a[b[i]] for i in range(4)) + + +MUL = tuple( + tuple(GID[compose(a, b)] for b in GROUP) + for a in GROUP +) + + +def adjacent_swap(i: int) -> int: + p = list(range(4)) + p[i], p[i + 1] = p[i + 1], p[i] + return GID[tuple(p)] + + +SIMPLE = (adjacent_swap(0), adjacent_swap(1), adjacent_swap(2)) +CYCLE = MUL[MUL[SIMPLE[0]][SIMPLE[1]]][SIMPLE[2]] +E_BIT = 1 << IDENTITY_PERM +C_BIT = 1 << CYCLE + + +def make_translations() -> tuple[tuple[tuple[int, ...], ...], ...]: + """Lookup tables for right multiplication of F2[S4] coefficient masks.""" + all_tables = [] + for g in range(len(GROUP)): + chunks = [] + for chunk in range(3): + lookup = [] + for small in range(256): + out = 0 + for j in range(8): + if (small >> j) & 1: + old = chunk * 8 + j + if old < len(GROUP): + out ^= 1 << MUL[old][g] + lookup.append(out) + chunks.append(tuple(lookup)) + all_tables.append(tuple(chunks)) + return tuple(all_tables) + + +TRANSLATE_CHUNKS = make_translations() + + +def translate(mask: int, g: int) -> int: + t = TRANSLATE_CHUNKS[g] + return t[0][mask & 255] ^ t[1][(mask >> 8) & 255] ^ t[2][(mask >> 16) & 255] + + +def encode(cells: list[int] | tuple[int, ...]) -> bytes: + out = bytearray(27) # nine cells, each a 24-bit group-algebra element + for i, v in enumerate(cells): + out[3 * i] = v & 255 + out[3 * i + 1] = (v >> 8) & 255 + out[3 * i + 2] = (v >> 16) & 255 + return bytes(out) + + +def decode(state: bytes) -> list[int]: + return [state[i] | (state[i + 1] << 8) | (state[i + 2] << 16) for i in range(0, 27, 3)] + + +IDENTITY = encode([E_BIT, 0, 0, 0, E_BIT, 0, 0, 0, E_BIT]) +TARGET = encode([C_BIT, 0, 0, 0, C_BIT, 0, 0, 0, E_BIT]) + + +def rank_one_idempotents() -> tuple[tuple[int, int], ...]: + pairs = [] + for u in range(1, 8): + for v in range(1, 8): + if (u & v).bit_count() & 1: + pairs.append((u, v)) + return tuple(pairs) + + +PROJECTORS = rank_one_idempotents() +GENERATORS = tuple((g, u, v) for g in SIMPLE for u, v in PROJECTORS) +GENERATOR_ID = {gen: i for i, gen in enumerate(GENERATORS)} + + +def step(state: bytes, gen: tuple[int, int, int]) -> bytes: + """Right multiply exactly by I+([g]+[e])uv^T over F2[S4].""" + g, u, v = gen + cells = decode(state) + for row in range(3): + signal = 0 + base = 3 * row + for k in range(3): + if (u >> k) & 1: + signal ^= cells[base + k] + delta = signal ^ translate(signal, g) + if delta: + for col in range(3): + if (v >> col) & 1: + cells[base + col] ^= delta + return encode(cells) + + +def coeff_product(left: int, right: int) -> int: + """Independent, literal convolution in F2[S4].""" + out = 0 + a = left + while a: + abit = a & -a + i = abit.bit_length() - 1 + a ^= abit + b = right + while b: + bbit = b & -b + j = bbit.bit_length() - 1 + b ^= bbit + out ^= 1 << MUL[i][j] + return out + + +def matrix_product(a: tuple[int, ...], b: tuple[int, ...]) -> tuple[int, ...]: + out = [0] * 9 + for i in range(3): + for j in range(3): + value = 0 + for k in range(3): + value ^= coeff_product(a[3 * i + k], b[3 * k + j]) + out[3 * i + j] = value + return tuple(out) + + +def factor_matrix(gen: tuple[int, int, int]) -> tuple[int, ...]: + g, u, v = gen + out = [E_BIT if i == j else 0 for i in range(3) for j in range(3)] + t = E_BIT ^ (1 << g) + for i in range(3): + if (u >> i) & 1: + for j in range(3): + if (v >> j) & 1: + out[3 * i + j] ^= t + return tuple(out) + + +def multiply_word(word: tuple[int, ...] | list[int]) -> bytes: + result = tuple(decode(IDENTITY)) + for gi in word: + result = matrix_product(result, factor_matrix(GENERATORS[gi])) + return encode(result) + + +def ball(root: bytes, radius: int) -> tuple[dict[bytes, tuple[bytes, int] | None], list[int]]: + """Enumerate all exact states within a paid-call radius; retain parents.""" + seen: dict[bytes, tuple[bytes, int] | None] = {root: None} + frontier = [root] + layer_counts = [1] + for _depth in range(1, radius + 1): + following: list[bytes] = [] + for state_no, state in enumerate(frontier): + if (state_no & 1023) == 0: + check_budget() + for gi, gen in enumerate(GENERATORS): + nxt = step(state, gen) + if nxt not in seen: + seen[nxt] = (state, gi) + following.append(nxt) + layer_counts.append(len(following)) + frontier = following + if not frontier: + break + check_budget() + return seen, layer_counts + + +def reconstruct(parents: dict[bytes, tuple[bytes, int] | None], state: bytes) -> list[int]: + reverse_path = [] + while parents[state] is not None: + previous, gi = parents[state] # type: ignore[misc] + reverse_path.append(gi) + state = previous + reverse_path.reverse() + return reverse_path + + +def labels(word: list[int]) -> list[dict[str, int | str]]: + names = {g: f"s{i + 1}" for i, g in enumerate(SIMPLE)} + return [ + {"address": names[GENERATORS[i][0]], "u": GENERATORS[i][1], "v": GENERATORS[i][2]} + for i in word + ] + + +def direct_word() -> list[int]: + out = [] + for role in (1, 2): + for g in SIMPLE: + out.append(GENERATOR_ID[(g, role, role)]) + return out + + +def run() -> dict[str, object]: + need(len(GROUP) == 24 and len(PROJECTORS) == 28 and len(GENERATORS) == 84, "alphabet cardinality") + current = IDENTITY_PERM + for _ in range(4): + current = MUL[current][CYCLE] + need(current == IDENTITY_PERM, "the selected address product does not have order four") + need(CYCLE not in (IDENTITY_PERM, *SIMPLE), "the selected three-letter product is not a 4-cycle") + + # Each simple transposition has order two. Verify each paid factor is an + # involution by literal F2[S4] matrix multiplication before the symmetric + # meet-in-the-middle argument uses inverse balls. + for gen in GENERATORS: + m = factor_matrix(gen) + need(matrix_product(m, m) == tuple(decode(IDENTITY)), "paid generator is not involutive") + + direct = direct_word() + need(len(direct) == 6 and multiply_word(direct) == TARGET, "six-call direct construction") + deletion_controls = 0 + for omitted in range(len(direct)): + shortened = direct[:omitted] + direct[omitted + 1 :] + need(multiply_word(shortened) != TARGET, "single-call omission control") + deletion_controls += 1 + + left, left_layers = ball(IDENTITY, 2) + right, right_layers = ball(TARGET, 3) + meetings = [state for state in left if state in right] + witness = None + if meetings: + state = min(meetings) + a = reconstruct(left, state) + target_path = reconstruct(right, state) + candidate = a + list(reversed(target_path)) + need(len(candidate) <= 5 and multiply_word(candidate) == TARGET, "meeting did not yield a formal word") + witness = candidate + else: + need(not meetings, "empty intersection control") + + # A one-sided endpoint change is a semantic negative control. + changed = encode([C_BIT, 0, 0, 0, C_BIT, 0, 0, 0, C_BIT]) + need(changed != TARGET and multiply_word(direct) != changed, "changed-third-role control") + + outcome = "FIVE_CALL_WORD_FOUND" if witness is not None else "NO_WORD_THROUGH_FIVE_MINIMUM_SIX" + return { + "schema_version": 1, + "status": "PASS_S4_TWO_TARGET_CYCLE", + "outcome": outcome, + "group": "S4", + "group_order": 24, + "address_generators": ["s1=(12)", "s2=(23)", "s3=(34)"], + "scalar_registers": 3, + "rank_one_idempotents": len(PROJECTORS), + "paid_generator_count": len(GENERATORS), + "target": "diag([s1*s2*s3],[s1*s2*s3],[e])", + "radius_left": 2, + "radius_right": 3, + "left_layer_counts": left_layers, + "right_layer_counts": right_layers, + "left_state_count": len(left), + "right_state_count": len(right), + "intersection_count": len(meetings), + "direct_call_count": len(direct), + "direct_word": labels(direct), + "witness_call_count": None if witness is None else len(witness), + "witness": None if witness is None else labels(witness), + "semantic_controls": { + "all_paid_factors_literal_square_to_identity": True, + "single_call_omissions_rejected": deletion_controls, + "changed_third_role_rejected": True, + }, + "complete_domain": "all ordered words of length <=5 over the 84 paid involutive factors; proved by radius-2/radius-3 exact meet", + "time_cap_seconds": MAX_SECONDS, + "rss_cap_bytes": MAX_RSS_BYTES, + "selected_kappa_claimed": False, + } + + +if __name__ == "__main__": + receipt = run() + path = HERE / "CERTIFICATE.json" + if "--write" in sys.argv: + path.write_text(json.dumps(receipt, indent=2) + "\n") + else: + need(path.is_file(), "missing committed certificate; run verify.py --write once") + need(receipt == json.loads(path.read_text()), "certificate mismatch") + print( + receipt["status"], + receipt["outcome"], + "layers=" + str(receipt["left_layer_counts"]) + "/" + str(receipt["right_layer_counts"]), + "states=" + str(receipt["left_state_count"]) + "/" + str(receipt["right_state_count"]), + "meetings=" + str(receipt["intersection_count"]), + ) From edb4a289a5f32c8209140144e384dcd3fa8cbfd1 Mon Sep 17 00:00:00 2001 From: Cinna Davis <1337isnot1337@users.noreply.github.com> Date: Wed, 14 Oct 2026 02:47:50 -0500 Subject: [PATCH 2/2] Record S4 result PR handoff --- research/s4-two-target-cycle-seed6e525/CLAIM.md | 2 ++ research/s4-two-target-cycle-seed6e525/README.md | 3 ++- research/s4-two-target-cycle-seed6e525/TASK.json | 9 ++++++++- 3 files changed, 12 insertions(+), 2 deletions(-) diff --git a/research/s4-two-target-cycle-seed6e525/CLAIM.md b/research/s4-two-target-cycle-seed6e525/CLAIM.md index c64cff6bf4..e1b58cfbe3 100644 --- a/research/s4-two-target-cycle-seed6e525/CLAIM.md +++ b/research/s4-two-target-cycle-seed6e525/CLAIM.md @@ -45,3 +45,5 @@ reports the complex primitive as binding. Full package and deterministic receipt: `README.md`, `TASK.json`, `CERTIFICATE.json`, `SOURCES.json`, `VERIFY.json`, and `verify.py`. + +SUBMITTED: [PR #1720](https://github.com/CrocSwap/integer-mult-bounds/pull/1720), head `828a1df15d5f5256f80e61c8d22b822846b76ae7`. It is open; no merge or frontier change is claimed. diff --git a/research/s4-two-target-cycle-seed6e525/README.md b/research/s4-two-target-cycle-seed6e525/README.md index 82a449f4a7..4325212c74 100644 --- a/research/s4-two-target-cycle-seed6e525/README.md +++ b/research/s4-two-target-cycle-seed6e525/README.md @@ -92,7 +92,8 @@ transposition alphabet are distinct from those scopes. A current fresh Discussion fetch and new claim post are unavailable: GitHub GraphQL reports the account rate limit exceeded, and the installed REST API has no create/update endpoint for Discussion comments. This local claim -card and package are being used while that limitation holds. +card and package are being used while that limitation holds. The result is +submitted in [PR #1720](https://github.com/CrocSwap/integer-mult-bounds/pull/1720). ## Open next questions diff --git a/research/s4-two-target-cycle-seed6e525/TASK.json b/research/s4-two-target-cycle-seed6e525/TASK.json index 4f8b5f957c..6fdce80bf1 100644 --- a/research/s4-two-target-cycle-seed6e525/TASK.json +++ b/research/s4-two-target-cycle-seed6e525/TASK.json @@ -103,5 +103,12 @@ "certificate_sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045", "reproduce": "make frontier1094-verify" }, - "no_open_questions_reason": "The exact six-call minimum closes the stated S4 target/alphabet. A different S4 target or address group would be a new mechanism and needs a separate cost screen; no narrow next experiment is justified from this bounded result." + "no_open_questions_reason": "The exact six-call minimum closes the stated S4 target/alphabet. A different S4 target or address group would be a new mechanism and needs a separate cost screen; no narrow next experiment is justified from this bounded result.", + "submission": { + "kind": "pull_request", + "number": 1720, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1720", + "head_commit": "828a1df15d5f5256f80e61c8d22b822846b76ae7", + "status": "open" + } }