From 57b4c06ddd657c85823c8a11857cd5b54bb1837e Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Mon, 2 Nov 2026 19:06:51 -0600 Subject: [PATCH 1/2] Certify the complete two-cycle incidence class with formal controls --- .../two-cycle-incidence-certificate/PROOF.md | 201 +++++++++ .../two-cycle-incidence-certificate/README.md | 77 ++++ .../RESULT.json | 190 +++++++++ .../SOURCES.json | 36 ++ .../two-cycle-incidence-certificate/TASK.json | 64 +++ .../VERIFY.json | 38 ++ .../two-cycle-incidence-certificate/verify.py | 380 ++++++++++++++++++ 7 files changed, 986 insertions(+) create mode 100644 research/two-cycle-incidence-certificate/PROOF.md create mode 100644 research/two-cycle-incidence-certificate/README.md create mode 100644 research/two-cycle-incidence-certificate/RESULT.json create mode 100644 research/two-cycle-incidence-certificate/SOURCES.json create mode 100644 research/two-cycle-incidence-certificate/TASK.json create mode 100644 research/two-cycle-incidence-certificate/VERIFY.json create mode 100644 research/two-cycle-incidence-certificate/verify.py diff --git a/research/two-cycle-incidence-certificate/PROOF.md b/research/two-cycle-incidence-certificate/PROOF.md new file mode 100644 index 0000000000..b8490d9cb0 --- /dev/null +++ b/research/two-cycle-incidence-certificate/PROOF.md @@ -0,0 +1,201 @@ +# Two-cycle incidence certificate + +## Scope and exact sources + +Use the formal model from +[PR #6012](https://github.com/CrocSwap/integer-mult-bounds/pull/6012): +two scalar roles over F2[GL_n(F2)], n>=3, with target [c]I_2. +Here c cycles address coordinates 0,1,2 and fixes all spectators. +A paid call is D(g,P)=I+([g]+[e])P, where g=I+e_i e_j^T, +i!=j, and P is a rank-one binary idempotent. Equality means equality +of every formal group coefficient. + +Free scalar maps are normalized into the projectors. Augmentation of +the target forces the remaining terminal scalar map to be I. This +normalization is inherited from the credited formal-model sources. + +The source +[two-write proof](https://github.com/CrocSwap/integer-mult-bounds/blob/7c49fe32c55de02c2c873655c804b16e4c3fef0a/research/two-write-spectator-projection/README.md) +proves that the two writer projectors of a restored coordinate are equal. +For a moved coordinate they are complementary. The moved-row conclusion +uses both the word and its inverse. Transposition gives the same rule for +reader pairs. Its selected middle labels and their g b h relabeling remain +required. We do not replace that proof by an augmented-matrix relaxation. + +PR6012 reduces a possible word shorter than twelve to five address +coordinates. At length ten, each coordinate is read and written exactly +twice. The two-write equations therefore apply to all ten reader/writer +pairs. These source results are premises; their complete original +scientific suites are not replayed here. Their exact proof files and the +related commuting-method source are authenticated by SOURCES.json. + +## 1. One ordinary 3-cycle still costs six with dirty spectators + +A coordinate CNOT changes one row by adding another. Read matrix factors +in execution order, with the rightmost factor first. Build the undirected +interaction graph in that order. A gate that joins two previously +disconnected components cannot change a diagonal entry: the source row +has no coefficient at the destination coordinate. Initially all diagonal +entries are one. + +Consider the final interaction component that contains the three target +coordinates. It contains all three, since their final cycle moves their +basis vectors among them. If this component contains s vertices, exactly +s-1 gates first join its components. Each of its three target diagonal +entries is zero at the endpoint. Each requires a gate that changes that +entry; that gate is not a join. A gate changes only one row, so at least +three other gates are required. If a spectator is in this component, +s>=4 and the component uses at least (s-1)+3>=6 gates. + +If no spectator is in the component, its action is a word in GL_3(F2). +The complete 168-state breadth-first certificate gives distance six to +each of the two coordinate 3-cycles. The independent enumeration of all +512 binary 3x3 matrices finds exactly those 168 invertible matrices. +The BFS includes all six coordinate CNOTs at every reached state, so it +excludes every shorter word in this finite base case. Gates on other +components cannot change this action. + +The usual six-gate construction on the three target coordinates attains +the bound and leaves every spectator unchanged. Thus the exact ordinary +cost is six for every n>=3. + +This argument retains the connectivity/diagonal method credited to Alan +Bu, Evan Fan and Robert Joo in +[Minimum Synthesis Cost of CNOT Circuits](https://arxiv.org/abs/2408.07898). +Their permutation-circuit result is established prior work. The present +small proof and finite certificate make this source application explicit; +they are not a claim of a new ordinary CNOT lower bound. + +## 2. Exact twelve-call minimum in the commuting two-role class + +Let P be one rank-one idempotent. A rank-one idempotent Q that commutes +with P preserves both one-dimensional spaces im(P) and ker(P). In that +basis Q is diagonal, idempotent and has rank one. Hence Q=P or Q=I+P. +This holds for all six binary rank-one projectors, and is checked on all +36 ordered pairs. + +If all call projectors commute, one fixed scalar basis puts them in the +two coordinate projections. Every call then acts in exactly one of two +scalar lanes. The complete formal endpoint is the pair of ordinary +address-group products in those lanes. The target [c]I is unchanged by +this scalar basis change, so both lane products must equal c. Section 1 +requires at least six calls in each lane. Thus at least twelve paid calls +are necessary. + +Conversely, put one six-CNOT construction in each lane. This realizes +[c]I with twelve calls in every n>=3. The bound is sharp in the stated +commuting class. It excludes neither noncommuting projectors nor larger +scalar-role models. The diagonalization method already appears in Aaron +Wang's [PR #2317](https://github.com/CrocSwap/integer-mult-bounds/pull/2317) +for a different SWAP endpoint and retains that credit. + +## 3. The incidence obstruction + +For a residual ten-call word, make one vertex per call. Join the two +writers of each address coordinate with a writer edge. Join its two +readers with a reader edge. Each vertex has one edge of each kind. +The graph is a disjoint union of alternating even cycles; parallel +writer/reader edges are allowed. + +Give an edge parity zero for a spectator coordinate and one for a target +coordinate. By the source two-write lemma, its endpoints have equal +projectors at parity zero and complementary projectors at parity one. +An odd parity sum around a component would force P=I+P, which is +impossible. If all component parities are even, one root projector +determines every projector in that component. + +In a connected graph all projectors therefore lie in one complementary +pair. Section 2 requires twelve calls, contradicting length ten. +This is JoyboyBrian's released connected-incidence reduction, now bound to +the source proofs and the complete finite certificate below. + +A disconnected consistent graph with c components has exactly 6^c +projector assignments satisfying the pair equations. Exactly 3*2^c +assignments use a single common complementary pair: choose one of the +three unordered pairs and one orientation for each component. Those +assignments are also excluded. The other assignments are possible inputs +to the unresolved full formal equations; they are not valid endpoints. + +## 4. Exact census domain and result + +Fix writer positions 2i and 2i+1 for coordinate i, i=0,...,4. A reader +assignment is a length-ten sequence in which each coordinate occurs twice +and the reader differs from the writer at every position. Enumerate all +such sequences. Every actual ten-call incidence graph maps to this +domain by relabeling call vertices to group the writers. + +This relabeling forgets chronology. It is used only for graph constraints. +It is not a legal reordering of a formal word. The counts below are +normalized assignments, not graph-isomorphism classes, chronological +programs or numbers of possible endpoints. + +| Consistent pair equations | Components | Assignments | +|---|---:|---:| +| No | 2 | 3072 | +| No | 3 | 1920 | +| No | 4 | 432 | +| No | 5 | 42 | +| Yes | 1 | 4992 | +| Yes | 2 | 2688 | +| Yes | 3 | 560 | +| Yes | 4 | 48 | +| Yes | 5 | 2 | + +All 13,756 assignments are accounted for. Pair parity rejects 5,466. +The connected obstruction rejects another 4,992. The remaining 3,298 +disconnected assignments contain 247,296 noncommuting projector assignments +that satisfy these pair equations. No claim is made that any one realizes +the target. + +Graph propagation agrees with a separate GF2 equation elimination on +every assignment. A separate coefficient-count dynamic program verifies +the total number of loop-free reader assignments. The source-domain +limits are thus explicit, and completeness has two different checks. + +## 5. Formal endpoint controls + +The released connected fixture uses labels (i,i+1 mod5), i=0,...,4, +followed by (i,i+2 mod5), i=0,...,4. Its consistent projector colors are + + 0,0,1,0,1,1,1,0,0,1. + +It passes all reader and writer pair equations. It is connected and puts +five calls in each lane. Its full formal product is not the target for +any of the six root projectors: each product has two distinct group +labels. This shows that pair parity alone is not sufficient. + +The two exact engines use binary matrices and complete permutations as +group labels. Their scalar coefficient multiplication is also separate. +They compare every formal coefficient; neither accepts only a natural +matrix image. They agree on 36 twelve-call attainers and 216 mixed-lane +fixtures. All 432 single-call deletions from the attainers fail. + +Additional controls detect a flipped incidence parity and the missing +middle-label relabeling in D(g,P)D(h,P)D(g,P). A four-term formal polynomial +with distinct labels has zero natural matrix image, which shows why that +quotient cannot replace formal equality. A five-component graph passes +the pair filter, and an explicit noncommuting pair stays outside the +commuting proof. Three copied predecessor files are changed one at a time +and each change is rejected by source authentication. + +## Limits and credit + +The unrestricted five-coordinate ten- and eleven-call cases remain open. +The next useful step is the full selected-middle/off-subgroup equations on +the disconnected noncommuting cases, with their original chronology. +This certificate does not create a native operator, physical tariff, +supplier, new kappa or selected-frontier change. + +Credit JoyboyBrian for PR6090 and +[the released incidence handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/6075#discussioncomment-19234840); +Nick Petalas for PR6012; Mihir Srivastava for the formal model; +James Reed / @jwr404 for PR5005/PR5379; Aaron Wang / @navinor for the prior +commuting reduction; and Bu, Fan and Joo for the ordinary CNOT method. +All predecessor notices and sources remain unchanged. + +The new contribution is this exact normalized incidence certificate and +source-bound completion with full formal controls. No priority is claimed +for the handoff lemma, commuting diagonalization or ordinary CNOT bound. +Independent human review, proof-kernel formalization, full source search, +selected cold replay, Lean and Docker are unrun. Prepared by Ali Romman +with substantial OpenAI Codex assistance. New work is Apache-2.0. diff --git a/research/two-cycle-incidence-certificate/README.md b/research/two-cycle-incidence-certificate/README.md new file mode 100644 index 0000000000..282ef9b542 --- /dev/null +++ b/research/two-cycle-incidence-certificate/README.md @@ -0,0 +1,77 @@ +# Exact incidence certificate for the residual two-cycle question + +**Scoped proof and finite certificate; no new kappa.** This completes +[JoyboyBrian's released handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/6075#discussioncomment-19234840) +with pinned predecessor lemmas, a complete normalized incidence census and +full formal group-algebra checks. The [proof](PROOF.md) states the exact +model, attribution, census domain and remaining obligations. + +For the two-role formal target consisting of two coordinate 3-cycles, +commuting rank-one projectors have exact cost twelve in every address +dimension, including arbitrarily many restored address spectators. +The ordinary CNOT bound and commuting reduction are credited methods. +The released connected-incidence lemma is also credited, not claimed new. + +In the residual five-coordinate ten-call domain, the exact census gives: + +| Classification | Normalized incidence assignments | +|---|---:| +| Inconsistent pair constraints | 5466 | +| Consistent connected graphs, excluded by the twelve-call bound | 4992 | +| Disconnected graphs left unresolved | 3298 | +| Total | 13756 | + +The unresolved graphs have 247,296 noncommuting projector assignments +that satisfy the pair constraints. None is certified to realize the target. +The census fixes each writer pair and enumerates loop-free reader assignments. +It forgets chronology; it is not a formal-word search or an isomorphism census. + +## Evidence and reproduction + +From the repository root, CPython 3.12 and the standard library: + +```sh +python3.12 -B scripts/research_package.py --package research/two-cycle-incidence-certificate +python3.12 -B scripts/check_research_commit.py --package research/two-cycle-incidence-certificate --check-source-history +``` + +Expected markers: `PASS_TWO_CYCLE_INCIDENCE`, +`PASS_REGISTERED_RESEARCH_PACKAGE` and `PASS_RESEARCH_COMMIT_BYTES`. +Normal and optimized modes are registered. The default verifier compares +[RESULT.json](RESULT.json) without writing it. `--output NEW_FILE` writes +a separate receipt and refuses to overwrite a file. + +Every incidence assignment agrees between graph propagation and GF2 +elimination. A separate counting dynamic program verifies the domain size. +The ordinary BFS covers all 168 invertible three-by-three binary matrices. +The matrix-label and complete-permutation-label engines agree on 36 exact +twelve-call attainers, 216 lane-decomposition fixtures and all six versions +of the handoff's connected fixture. All 432 deleted attaining calls fail. +Controls reject wrong edge parity, missing middle relabeling, acceptance +in an unfaithful natural quotient and source changes. Disconnected and +noncommuting controls remain outside the exclusion. + +All source files are authenticated against canonical main +7c49fe32c55de02c2c873655c804b16e4c3fef0a and retained in the declared input +closure. No predecessor scientific suite, selected replay, Lean, Docker, +independent human review or proof-kernel verification is claimed. +The all-dimension proof reduces to the explicit finite GL3 base certificate; +it is not an extrapolation from sampled address sizes. + +## Open next questions + +Apply the complete selected-middle and off-subgroup equations to one +bounded disconnected pattern, preserving the original chronological word +and the required g b h relabeling. The unrestricted ten- and eleven-call +questions remain open. No physical supplier, tariff, selected assumption +discharge or selected-frontier change follows from this certificate. + +## Credit + +JoyboyBrian supplied PR6090 and the released incidence lemma. Nick Petalas +supplied PR6012; Mihir Srivastava supplied the formal model; James Reed +supplied the cited small-dimension work; Aaron Wang supplied the prior +commuting reduction for a different SWAP target. Bu, Fan and Joo supplied +the ordinary CNOT connectivity method. See PROOF.md for source links and +exact scope. Sources and notices remain unchanged. Prepared by Ali Romman +with substantial OpenAI Codex assistance. New work is Apache-2.0. diff --git a/research/two-cycle-incidence-certificate/RESULT.json b/research/two-cycle-incidence-certificate/RESULT.json new file mode 100644 index 0000000000..b596afa1a0 --- /dev/null +++ b/research/two-cycle-incidence-certificate/RESULT.json @@ -0,0 +1,190 @@ +{ + "formal": { + "attainers": 36, + "connected_fixture_colors": [ + 0, + 0, + 1, + 0, + 1, + 1, + 1, + 0, + 0, + 1 + ], + "connected_formal_supports": [ + 2, + 2, + 2, + 2, + 2, + 2 + ], + "disconnected_components": 5, + "lane_decompositions": 216, + "middle_relabel_control": true, + "natural_quotient_control": true, + "noncommuting_control": true, + "omitted_attaining_calls": 432, + "parity_control": true + }, + "incidence": { + "assignment_sha256": "6dbf049b3d91e82e9f946d2f2a66bd9c75a58e1908a416d1de6d44cd7e634713", + "assignments": 13756, + "connected_rejections": 4992, + "histogram": [ + { + "components": 2, + "consistent": false, + "count": 3072 + }, + { + "components": 3, + "consistent": false, + "count": 1920 + }, + { + "components": 4, + "consistent": false, + "count": 432 + }, + { + "components": 5, + "consistent": false, + "count": 42 + }, + { + "components": 1, + "consistent": true, + "count": 4992 + }, + { + "components": 2, + "consistent": true, + "count": 2688 + }, + { + "components": 3, + "consistent": true, + "count": 560 + }, + { + "components": 4, + "consistent": true, + "count": 48 + }, + { + "components": 5, + "consistent": true, + "count": 2 + } + ], + "parity_rejections": 5466, + "unresolved_incidence_assignments": 3298, + "unresolved_noncommuting_projector_assignments": 247296 + }, + "ordinary_bfs": { + "cycle_paths": [ + [ + [ + 0, + 1 + ], + [ + 0, + 2 + ], + [ + 2, + 0 + ], + [ + 0, + 2 + ], + [ + 1, + 2 + ], + [ + 2, + 1 + ] + ], + [ + [ + 0, + 1 + ], + [ + 0, + 2 + ], + [ + 1, + 0 + ], + [ + 0, + 1 + ], + [ + 2, + 1 + ], + [ + 1, + 2 + ] + ] + ], + "distance_histogram": { + "0": 1, + "1": 6, + "2": 24, + "3": 51, + "4": 60, + "5": 24, + "6": 2 + }, + "states": 168 + }, + "projectors": { + "commuting_pairs": 12, + "component_assignments": [ + [ + 1, + 6, + 6, + 0 + ], + [ + 2, + 36, + 12, + 24 + ], + [ + 3, + 216, + 24, + 192 + ], + [ + 4, + 1296, + 48, + 1248 + ], + [ + 5, + 7776, + 96, + 7680 + ] + ] + }, + "schema_version": 1, + "source_mutation_controls": 3 +} diff --git a/research/two-cycle-incidence-certificate/SOURCES.json b/research/two-cycle-incidence-certificate/SOURCES.json new file mode 100644 index 0000000000..a7177789d7 --- /dev/null +++ b/research/two-cycle-incidence-certificate/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/fiveswap-alt13-commuting-screen/README.md", + "usage": "input", + "git_blob": "d29ed698475ef96770e09d26d891afdbb316e1c4", + "sha256": "edba3d71ad274311f3a8c2293d390a7adba38deca344662c0364cbdd192521d3" + }, + { + "path": "research/two-three-cycles-every-dimension/PROOF.md", + "usage": "input", + "git_blob": "ca692812836f82484d228d8b4eb0f250c007d7a8", + "sha256": "b7af7801ddd5ff1e8d07d50dcd6f537f052d515839b828f0c4fd040351b8bce3" + }, + { + "path": "research/two-write-spectator-projection/README.md", + "usage": "input", + "git_blob": "7eaec710199bb2e437cb6c88f6f195da3f6f153b", + "sha256": "a488e036a1ffa0b8693a1f1ad38d69a970d272a28ebdca6f3a0ef9d87a0c0374" + } + ] +} diff --git a/research/two-cycle-incidence-certificate/TASK.json b/research/two-cycle-incidence-certificate/TASK.json new file mode 100644 index 0000000000..f2f6b9c973 --- /dev/null +++ b/research/two-cycle-incidence-certificate/TASK.json @@ -0,0 +1,64 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "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": "Complete the released connected-incidence two-cycle lemma with an exact normalized incidence census and full formal controls.", + "scope_change_reason": "Use the released PR6090/PR6012 handoff; the outcome is a source-bound structural restriction, not a new physical BIT mechanism.", + "bottleneck_link": "The census removes inconsistent and connected cases from the unresolved ten-call two-cycle candidate. Remaining disconnected cases need the full chronological formal equations.", + "budget_minutes": 60, + "stop_rule": "Stop after the complete declared incidence domain, commuting-class sharp bound, exact formal controls and verification. Do not run an unrestricted ten/eleven-call search.", + "outcome": "completed", + "evidence": "PROOF.md and RESULT.json bind the source lemmas to all 13,756 normalized assignments, independent elimination/count checks and two full formal engines.", + "author": "Ali Romman", + "ai_assistance": "Substantial OpenAI Codex assistance. No independent human or proof-kernel review.", + "open_questions": [ + { + "question": "Which disconnected noncommuting incidence assignments survive the full selected-middle and off-subgroup equations in their actual chronology?", + "why_it_matters": "The pair constraints and connected exclusion leave 3,298 incidence assignments unresolved.", + "first_step": "Retain original call order and the required g b h relabeling in one bounded disconnected component pattern.", + "blocked_by": "The graph filter does not encode complete formal cancellation." + } + ] +} diff --git a/research/two-cycle-incidence-certificate/VERIFY.json b/research/two-cycle-incidence-certificate/VERIFY.json new file mode 100644 index 0000000000..f3f2f50823 --- /dev/null +++ b/research/two-cycle-incidence-certificate/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/fiveswap-alt13-commuting-screen/README.md", + "research/two-three-cycles-every-dimension/PROOF.md", + "research/two-write-spectator-projection/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete incidence census, independent GF2 elimination/count, sharp commuting construction, full formal coefficient controls and source corruption." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete incidence census, independent GF2 elimination/count, sharp commuting construction, full formal coefficient controls and source corruption." + } + ] +} diff --git a/research/two-cycle-incidence-certificate/verify.py b/research/two-cycle-incidence-certificate/verify.py new file mode 100644 index 0000000000..f491d15115 --- /dev/null +++ b/research/two-cycle-incidence-certificate/verify.py @@ -0,0 +1,380 @@ +#!/usr/bin/env python3 +"""Check the complete incidence class and exact formal endpoint controls. + +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. +JoyboyBrian supplied the released connected-incidence lemma and fixture. +""" +import argparse +from collections import Counter, deque +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path +import random +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +I2, Z2 = (1, 2), (0, 0) + + +def need(ok, why): + if not ok: + raise ValueError(why) + + +def authenticate(root): + for row in json.loads((HERE/'SOURCES.json').read_text())['files']: + if row['usage'] == 'input': + need(sha256((root/row['path']).read_bytes()).hexdigest() == row['sha256'], + 'Source mismatch: '+row['path']) + + +def identity(n): + return tuple(1 << j for j in range(n)) + + +def add(a, b): + return tuple(x ^ y for x, y in zip(a, b)) + + +def mul(a, b): + out = [] + for row in a: + value = 0 + for j, other in enumerate(b): + if row >> j & 1: + value ^= other + out.append(value) + return tuple(out) + + +def gate(n, target, source): + rows = list(identity(n)) + rows[target] ^= 1 << source + return tuple(rows) + + +PROJECTORS = [p for p in product(range(4), repeat=2) + if p not in (Z2, I2) and mul(p, p) == p] + + +def formal(word, n): + state = {identity(n): I2} + for label, p in word: + out = {} + for h, coefficient in state.items(): + for g, q in ((identity(n), add(I2, p)), (label, p)): + key = mul(h, g) + out[key] = add(out.get(key, Z2), mul(coefficient, q)) + state = {k: v for k, v in out.items() if v != Z2} + return state + + +def permutation(matrix): + return tuple(sum(((row & x).bit_count() & 1) << j + for j, row in enumerate(matrix)) + for x in range(1 << len(matrix))) + + +def independent_formal(word, n): + """Use complete permutations as group labels and dense scalar matrices.""" + zero, one = (0, 0, 0, 0), (1, 0, 0, 1) + ident = tuple(range(1 << n)) + state = {ident: one} + def dense(p): + return tuple(p[i] >> j & 1 for i in range(2) for j in range(2)) + def dot(a, b): + return tuple(sum(a[2*i+k]*b[2*k+j] for k in range(2)) % 2 + for i in range(2) for j in range(2)) + for label, projector in word: + g, p = permutation(label), dense(projector) + q = tuple(x ^ y for x, y in zip(one, p)) + out = {} + for h, a in state.items(): + for k, b in ((h, q), (tuple(h[g[x]] for x in range(len(g))), p)): + old, value = out.get(k, zero), dot(a, b) + out[k] = tuple(x ^ y for x, y in zip(old, value)) + state = {k: v for k, v in out.items() if v != zero} + return state + + +def compare_engines(word, n): + primary = formal(word, n) + converted = {permutation(k): tuple(v[i] >> j & 1 for i in range(2) for j in range(2)) + for k, v in primary.items()} + need(converted == independent_formal(word, n), 'Independent full formal coefficients') + return primary + + +def ordinary_bfs(): + ident = identity(3) + generators = [(i, j) for i in range(3) for j in range(3) if i != j] + paths, queue = {ident: []}, deque([ident]) + while queue: + h = queue.popleft() + for i, j in generators: + nxt = mul(h, gate(3, i, j)) + if nxt not in paths: + paths[nxt] = paths[h]+[(i, j)] + queue.append(nxt) + need(len(paths) == 168, 'Complete GL3') + cycles = ((2, 4, 1), (4, 1, 2)) + need(all(len(paths[c]) == 6 for c in cycles), 'Both ordinary cycle minima') + # A rank enumeration gives a separate inventory of the group. + invertible = set() + for rows in product(range(8), repeat=3): + if len({0, rows[0], rows[1], rows[2], rows[0]^rows[1], + rows[0]^rows[2], rows[1]^rows[2], rows[0]^rows[1]^rows[2]}) == 8: + invertible.add(rows) + need(invertible == set(paths), 'Independent complete group inventory') + return paths, cycles + + +def edges(labels): + need(len(labels) == 10 and all(i != j for i, j in labels), 'Ten loop-free calls') + result = [] + for side in (0, 1): + for coordinate in range(5): + positions = [j for j, pair in enumerate(labels) if pair[side] == coordinate] + need(len(positions) == 2, 'Two reads and writes per coordinate') + result.append((*positions, int(coordinate < 3))) + return result + + +def graph_check(relations): + adjacent = [[] for _ in range(10)] + for x, y, parity in relations: + adjacent[x].append((y, parity)) + adjacent[y].append((x, parity)) + need(all(len(row) == 2 for row in adjacent), 'Alternating degree two') + colors, components, ok = {}, 0, True + for root in range(10): + if root in colors: + continue + components += 1 + colors[root] = 0 + queue = [root] + while queue: + x = queue.pop() + for y, parity in adjacent[x]: + value = colors[x] ^ parity + if y in colors: + ok &= colors[y] == value + else: + colors[y] = value + queue.append(y) + return ok, components, [colors[x] for x in range(10)] + + +def linear_check(relations): + pivots, ok = {}, True + for x, y, parity in relations: + row = (1 << x) ^ (1 << y) ^ (parity << 10) + for bit in range(10): + if not row >> bit & 1: + continue + if bit in pivots: + row ^= pivots[bit] + else: + pivots[bit] = row + break + else: + if row: + ok = False + return ok, 10-len(pivots) + + +def assignments(): + remaining = [2]*5 + values = [] + def walk(): + if len(values) == 10: + yield tuple(values) + return + target = len(values)//2 + for source in range(5): + if source != target and remaining[source]: + remaining[source] -= 1 + values.append(source) + yield from walk() + values.pop() + remaining[source] += 1 + yield from walk() + + +def incidence_census(): + histogram, total, digest = Counter(), 0, sha256() + for sources in assignments(): + labels = [(j//2, source) for j, source in enumerate(sources)] + relations = edges(labels) + ok, components, _ = graph_check(relations) + need((ok, components) == linear_check(relations), 'Graph and GF2 elimination') + histogram[(ok, components)] += 1 + digest.update(bytes(sources)) + total += 1 + # Independent coefficient DP counts the loop-free reader assignments. + counts = {(0, 0, 0, 0, 0): 1} + for position in range(10): + nxt = Counter() + for state, multiplicity in counts.items(): + for source in range(5): + if source != position//2 and state[source] < 2: + changed = list(state) + changed[source] += 1 + nxt[tuple(changed)] += multiplicity + counts = nxt + need(counts == {(2, 2, 2, 2, 2): total}, 'Independent assignment count') + parity_rejections = sum(v for (ok, _), v in histogram.items() if not ok) + connected_rejections = histogram[(True, 1)] + survivors = sum(v for (ok, count), v in histogram.items() if ok and count > 1) + noncommuting = sum(v*(6**count-3*2**count) + for (ok, count), v in histogram.items() if ok) + need(total == parity_rejections+connected_rejections+survivors, 'Complete partition') + return dict(assignments=total, assignment_sha256=digest.hexdigest(), + parity_rejections=parity_rejections, connected_rejections=connected_rejections, + unresolved_incidence_assignments=survivors, + unresolved_noncommuting_projector_assignments=noncommuting, + histogram=[dict(consistent=k[0], components=k[1], count=v) + for k, v in sorted(histogram.items())]) + + +def projector_checks(): + need(len(PROJECTORS) == 6, 'All binary rank-one projectors') + pairs = 0 + for p, q in product(PROJECTORS, repeat=2): + commute = mul(p, q) == mul(q, p) + need(commute == (p == q or add(p, q) == I2), 'Common complementary pair') + pairs += int(commute) + counts = [] + for components in range(1, 6): + commuting = sum(all(mul(p, q) == mul(q, p) for p in choices for q in choices) + for choices in product(PROJECTORS, repeat=components)) + need(commuting == 3*2**components, 'Exact commuting component assignments') + counts.append([components, 6**components, commuting, 6**components-commuting]) + return dict(commuting_pairs=pairs, component_assignments=counts) + + +def formal_checks(paths, cycles): + positive = omitted = separated = 0 + rng = random.Random(60906012) + for n in (3, 4, 5): + for c in cycles: + route = paths[c] + for p in PROJECTORS: + q = add(I2, p) + word = [(gate(n, i, j), r) for r in (p, q) for i, j in route] + target = {tuple(c)+identity(n)[3:]: I2} + need(compare_engines(word, n) == target, 'Sharp twelve-call attainer') + positive += 1 + for j in range(12): + need(formal(word[:j]+word[j+1:], n) != target, 'Deleted attaining call') + omitted += 1 + for length in (0, 1, 5, 10, 11, 12): + generated = [] + lane = {p: identity(n), q: identity(n)} + for _ in range(length): + i, j = rng.sample(range(n), 2) + r = rng.choice((p, q)) + g = gate(n, i, j) + lane[r] = mul(lane[r], g) + generated.append((g, r)) + expected = {} + for r, label in lane.items(): + expected[label] = add(expected.get(label, Z2), r) + expected = {k: v for k, v in expected.items() if v != Z2} + need(compare_engines(generated, n) == expected, 'Formal lane decomposition') + separated += 1 + labels = [(i, (i+1) % 5) for i in range(5)]+[(i, (i+2) % 5) for i in range(5)] + relations = edges(labels) + ok, components, colors = graph_check(relations) + need(ok and components == 1 and Counter(colors) == {0: 5, 1: 5}, + 'Published connected fixture') + connected_colors = list(colors) + target = {tuple(cycles[0])+identity(5)[3:]: I2} + connected = [] + for p in PROJECTORS: + word = [(gate(5, i, j), p if color == 0 else add(I2, p)) + for (i, j), color in zip(labels, colors)] + result = compare_engines(word, 5) + need(result != target, 'Pair constraints are insufficient for endpoint') + connected.append(len(result)) + bad = list(relations) + x, y, parity = bad[0] + bad[0] = (x, y, 1-parity) + need(not graph_check(bad)[0] and not linear_check(bad)[0], 'Wrong edge parity') + disconnected = [(i, (i+1) % 3) for i in range(3)]+[(3, 4), (4, 3)] + disconnected = [pair for pair in disconnected for _ in range(2)] + ok, components, colors = graph_check(edges(disconnected)) + need(ok and components == 5, 'Disconnected cases survive the graph filter') + p, q = next((p, q) for p, q in product(PROJECTORS, repeat=2) if mul(p, q) != mul(q, p)) + need(formal([(gate(3, 0, 1), p), (gate(3, 1, 2), q)], 3) + != formal([(gate(3, 1, 2), q), (gate(3, 0, 1), p)], 3), + 'Do not commute noncommuting calls') + # The selected middle label must be conjugated, not only retained. + p = PROJECTORS[0] + g, h = gate(3, 2, 1), gate(3, 0, 2) + relabeled = compare_engines([(g, p), (h, p), (g, p)], 3) + need(relabeled == {identity(3): add(I2, p), mul(mul(g, h), g): p} + and relabeled != {identity(3): add(I2, p), h: p}, 'Middle label relabeling') + # A natural matrix image can vanish while four formal labels remain. + g, h = gate(4, 0, 1), gate(4, 2, 3) + labels = (identity(4), g, h, mul(g, h)) + need(len(set(labels)) == 4 and add(add(labels[0], labels[1]), + add(labels[2], labels[3])) == (0, 0, 0, 0), 'Unfaithful natural quotient control') + return dict(attainers=positive, omitted_attaining_calls=omitted, + lane_decompositions=separated, connected_fixture_colors=connected_colors, + connected_formal_supports=connected, parity_control=True, + disconnected_components=components, noncommuting_control=True, + middle_relabel_control=True, natural_quotient_control=True) + + +def source_controls(): + rows = [r for r in json.loads((HERE/'SOURCES.json').read_text())['files'] if r['usage'] == 'input'] + with tempfile.TemporaryDirectory(prefix='incidence-source-') as folder: + root = Path(folder) + for row in rows: + path = root/row['path'] + path.parent.mkdir(parents=True, exist_ok=True) + path.write_bytes((ROOT/row['path']).read_bytes()) + authenticate(root) + for row in rows: + path = root/row['path'] + original = path.read_bytes() + path.write_bytes(original+b'\nchanged\n') + try: + authenticate(root) + except ValueError as error: + need(str(error) == 'Source mismatch: '+row['path'], 'Source rejection') + else: + raise ValueError('Changed predecessor accepted') + path.write_bytes(original) + return len(rows) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--output', type=Path) + args = parser.parse_args() + authenticate(ROOT) + paths, cycles = ordinary_bfs() + result = dict(schema_version=1, + ordinary_bfs=dict(states=len(paths), + distance_histogram=dict(sorted(Counter(map(len, paths.values())).items())), + cycle_paths=[paths[c] for c in cycles]), + incidence=incidence_census(), projectors=projector_checks(), + formal=formal_checks(paths, cycles), source_mutation_controls=source_controls()) + result = json.loads(json.dumps(result)) + if args.output: + with args.output.open('x', encoding='utf-8') as stream: + json.dump(result, stream, indent=2, sort_keys=True) + stream.write('\n') + else: + need(result == json.loads((HERE/'RESULT.json').read_text()), 'Stored receipt mismatch') + print('PASS_TWO_CYCLE_INCIDENCE', result['incidence']['assignments'], + 'incidence assignments;', result['formal']['attainers'], 'formal attainers;', + result['formal']['omitted_attaining_calls'], 'deletion controls') + + +if __name__ == '__main__': + main() From c98e5b03a7d9001a155ba10bc9faad0ceb7cad68 Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Mon, 2 Nov 2026 19:24:49 -0600 Subject: [PATCH 2/2] docs: record upstream onboarding failure before incidence replay --- research/two-cycle-incidence-certificate/README.md | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/research/two-cycle-incidence-certificate/README.md b/research/two-cycle-incidence-certificate/README.md index 282ef9b542..22224472ee 100644 --- a/research/two-cycle-incidence-certificate/README.md +++ b/research/two-cycle-incidence-certificate/README.md @@ -58,6 +58,16 @@ independent human review or proof-kernel verification is claimed. The all-dimension proof reduces to the explicit finite GL3 base certificate; it is not an extrapolation from sampled address sizes. +## Hosted validation record + +The first [hosted run](https://github.com/CrocSwap/integer-mult-bounds/actions/runs/41558037028) +failed before package selection. The unchanged onboarding test +`test_success_and_malformed_reply_stop_ready_descendant` read an empty +`child-ready` file and raised `ValueError`. The package replay did not run. +GitHub rejected a job retry because the contributor lacks repository admin +rights. This record does not turn that failed run into a scientific pass. +Local normal and optimized package checks passed as stated above. + ## Open next questions Apply the complete selected-middle and off-subgroup equations to one