From a5a8a76babad35f872545230d106984e8fa51fec Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 13:38:22 +0000 Subject: [PATCH] feat(research): prove sharp Fano cut gap for a Singer target --- research/gl3-singer-cut-gap/PROOF.md | 120 +++++++++ research/gl3-singer-cut-gap/README.md | 119 +++++++++ research/gl3-singer-cut-gap/SOURCES.json | 30 +++ research/gl3-singer-cut-gap/TASK.json | 82 ++++++ research/gl3-singer-cut-gap/VERIFY.json | 37 +++ research/gl3-singer-cut-gap/verify.py | 325 +++++++++++++++++++++++ 6 files changed, 713 insertions(+) create mode 100644 research/gl3-singer-cut-gap/PROOF.md create mode 100644 research/gl3-singer-cut-gap/README.md create mode 100644 research/gl3-singer-cut-gap/SOURCES.json create mode 100644 research/gl3-singer-cut-gap/TASK.json create mode 100644 research/gl3-singer-cut-gap/VERIFY.json create mode 100644 research/gl3-singer-cut-gap/verify.py diff --git a/research/gl3-singer-cut-gap/PROOF.md b/research/gl3-singer-cut-gap/PROOF.md new file mode 100644 index 0000000000..516bab067f --- /dev/null +++ b/research/gl3-singer-cut-gap/PROOF.md @@ -0,0 +1,120 @@ +# A sharp point-and-line cut obstruction + +This scoped proof uses a finite exact certificate on two seven-element sets. +It does not establish the optimum of a multi-target formal word. + +## Model + +Let `G=GL_3(F_2)`, with `s_ij=I+E_ij`, `i!=j`, at unit price. Matrices act +on column vectors. The ordered generator list is +`(s_01,s_02,s_10,s_12,s_20,s_21)`. Let + +```text + [1 1 1] +g = [1 0 1] binary columns (7,1,3). + [1 0 0] +``` + +In `M_R(F_2[G])`, a paid call is `I+([s_ij]+[e])uv^T`, with binary +`v^T u=1`. Any invertible scalar register mixing is free. There are `t>=1` +active roles with targets `[g]` or `[g^-1]`; every other role is an arbitrary +dirty spectator with exact identity output. All off-diagonal outputs vanish. + +Use the point set `P=F_2^3\{0}` with action `x -> A x`, or the line set +`L`, labelled by nonzero normal covectors, with action `a -> A^-T a`. +The latter convention makes incidence invariant. Modules may be arbitrary +finite direct sums of these permutation modules. A coordinate cut chooses +any subset of the basis in each summand, identically for every scalar role. + +For an address permutation `A` and cut `H`, write + +`c_H(A)=#{x in H : A x not in H}`. + +This is the rank over `F_2` of the crossing block of the permutation matrix. +The number is unchanged on replacing `A` by `A^-1` or `H` by its complement. + +## The finite certificate + +On **each** of P and L, every one of the 128 subsets satisfies + +`2 c_H(g) <= sum_(i!=j) c_H(s_ij)`. (1) + +Here is the complete slack histogram for either module. The slack is the +right-hand side minus the left-hand side, without dividing by two. + +| Slack | 0 | 2 | 4 | 6 | 8 | +|---|---:|---:|---:|---:|---:| +| Number of subsets | 34 | 46 | 34 | 10 | 4 | + +`verify.py` enumerates all subsets and checks (1) with integer arithmetic. +It constructs both actions from all 168 invertible binary matrices, checks +all their composition pairs, and checks line incidence independently of +the inverse-transpose formula. This finite enumeration is the proof of +(1), not a sampled experiment or a numerical optimization claim. + +Matching cuts make the upper bound sharp. Label points and covectors by +their binary integers 1 through 7, with coordinate zero the low bit. Take +`H_P={2,4,6}` and `H_L={2,4}`. Their exact profiles are + +| Cut | s_01 | s_02 | s_10 | s_12 | s_20 | s_21 | g | +|---|---:|---:|---:|---:|---:|---:|---:| +| H_P on P | 2 | 2 | 0 | 0 | 0 | 0 | 2 | +| H_L on L | 0 | 0 | 1 | 1 | 1 | 1 | 2 | + +Weight the first cut by 1/2 and the second by 1. Every paid generator +then has weight exactly 1, and g has weight exactly 3. Equivalently, use +one point copy and two line copies with a single coordinate cut, then +divide all ranks by two. + +## Passage to every finite module sum and role count + +For a fixed coordinate cut, crossing rank is subadditive under composition. +Indeed `(AB)_(out,in)=A_(out,in)B_(in,in)+A_(out,out)B_(out,in)`, so its +rank is at most the sum of the two crossing ranks. Free scalar register +mixing has zero crossing block. A paid factor has crossing block +`uv^T tensor (s_ij)_(out,in)`, up to the order of tensor factors. Its rank +is exactly `c_H(s_ij)`, since `uv^T` has rank one. At the required diagonal +endpoint the crossing rank is `t c_H(g)`. Every restored spectator adds zero. +This proves the inherited cut inequality for any finite dirty workspace. + +Coordinate cuts on a direct sum split across the summands. Their crossing +ranks add, so (1) continues to hold for every allowed module sum. If a +nonnegative combination of these cut inequalities has paid-generator +coefficients `b_ij<=1`, its endpoint coefficient is at most + +`(t/2) sum_(i!=j) b_ij <= 3t`. (2) + +The two matching cuts attain `3t`. Thus the complete normalized cone of +the declared coordinate-cut inequalities has **exact value 3t**, for +every t and every choice of target orientations. Taking more copies, +more coordinate cuts, or more dirty roles cannot improve this value. +No linear-program solver is needed to verify the upper or lower certificate. + +## Comparison with the direct bill + +In chronological execution order, the four labels +`s_01,s_02,s_10,s_21` have product `s_21 s_10 s_02 s_01=g`. Direct execution +on each active coordinate therefore costs `4t`, restoring all spectators. +The full group-algebra verifier checks this endpoint for t=1,2,3, including +all omitted-call controls and dirty-coupling detours. The Cayley traversal +also finds that g has distance four. The inverse has the reversed word. + +For a single target, every formal coefficient in a k-paid-call word is +supported on products of at most k paid address labels, even with free +scalar mixing and dirty roles. The coefficient `[g]` therefore requires +at least four calls. This standard support argument, already used in +JoyboyBrian's PR #4974, is not a new contribution here. The new certificate +shows that the specified point-and-line cut cone stops at three even in +this singleton case. For multiple targets, **4t is a direct upper bound**; +this package does not claim an all-workspace lower bound of 4t. + +## Limits + +Arbitrary subspace cuts, modules other than finite sums of P and L, +role-dependent cuts, nonlinear or integer-combined invariants and different +paid alphabets are outside (2). In particular the full regular module is +not a sum of these two modules as a permutation module. The theorem neither +constructs shared paid work nor excludes it. Native implementation, +compiler/hosting/precision invoices, recursive suppliers and the complete +multiplication theorem remain unproved here. No proof-kernel or independent +human review is claimed. diff --git a/research/gl3-singer-cut-gap/README.md b/research/gl3-singer-cut-gap/README.md new file mode 100644 index 0000000000..13ca08c383 --- /dev/null +++ b/research/gl3-singer-cut-gap/README.md @@ -0,0 +1,119 @@ +# Fano point and line cuts stop at three for a four-call Singer target + +For the binary GL3 target with columns `(7,1,3)`, every nonnegative +combination of coordinate-cut rank inequalities from finite sums of the +Fano point and dual-line permutation modules has normalized value at most +**three per target**. Two explicit cuts attain three. The independent +coordinate word costs four per target. + +The sharp cone value is `3t` for any number `t>=1` of targets, each either +g or its inverse, with any finite restored dirty workspace and free +invertible binary scalar mixing. This is a **scoped proof with a finite +256-cut certificate**. It rules out this particular invariant route for +closing the direct-word gap. It does not prove shared paid work or the +actual multi-target optimum. No new kappa or selected-frontier change. + +[PROOF.md](PROOF.md) defines the model, proves the passage from the finite +certificate to all finite module sums and role counts, and gives the +matching rational primal and dual certificates. Every one of the 128 +point cuts and 128 line cuts is checked exactly. The decisive inequality is +`2*c_H(g) <= sum_(i!=j) c_H(I+E_ij)`. The attaining point cut is `{2,4,6}` +with weight `1/2`; the line cut is `{2,4}` with weight `1`. + +## Reproduce + +From the repository root, Python 3.12 and the standard library only: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/gl3-singer-cut-gap/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/gl3-singer-cut-gap +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/gl3-singer-cut-gap --check-source-history +``` + +A reviewer can replace that interpreter path with any CPython 3.12 binary. +`VERIFY.json` registers warning-strict normal and optimized checks. Each +prints `PASS_GL3_SINGER_CUT_GAP` inside a generated JSON receipt that binds +all package files and both declared predecessor README inputs by SHA256. +No receipt is hand-written or accepted in place of recomputation. The +verifier writes no files and needs neither Git nor network in a source +export with its declared inputs. + +Coverage includes all 168 group elements, 56,448 action-composition checks, +1,176 point-line incidence checks, all 256 cuts, and 2,520 actual paid +crossing blocks from all 35 rank-one idempotents through three roles on +six declared cuts. Formal group-algebra controls check the direct endpoint +with one to three targets and a dirty spectator, 24 omitted calls, three +restored dirty detours and three corresponding leaks. Four malformed-input +controls remain active under optimization. These controls support the +specified finite certificate; they are not larger-register word searches. + +Both direct commands and the complete registered replay passed locally on +CPython 3.12.15, macOS arm64. Each registered command completed in under one +second. Hosted CI certification is separate from these local checks. + +## Verifier bounds + +The checker has no recursion, dynamic evaluation or subprocesses. All 21 +functions are at most 29 lines. Group enumeration considers 343 column +triples; Cayley traversal has seven rounds and at most 168 states; each +action table has 168 rows. Formal coefficients have at most 168 group +keys and four scalar roles in the controls; each word has at most 14 +factors. Rank elimination has at most 21 columns. Every rejection uses an +explicit exception, so optimization cannot disable it. + +Python necessarily allocates managed objects during these computations. +This is a deviation from fixed allocation after initialization, confined +to the stated finite domains. Fixed matrix sizes, group support and loop +bounds constrain live mathematical data; Python allocator overhead is not +statically certified. Expanding these domains requires a fresh resource +bound. Warning-strict normal and optimized execution, source compilation +and the repository package checks are the available diagnostics; no +separate Python linter is installed in the environment used here. + +## Scope and next decision + +The original `bit-new-register-model` card is changed to the quotient-based +invariant question in Josie Elliston's PR #1974, Open next question 2. +That predecessor already proves the complete two-role tariff by a word +census. Its census is cited, not replayed. This package adds the exact +point-and-line coordinate-cut cone obstruction for the specified order-seven +endpoint. A natural-representation alias alone does not prove this closure. + +Stop this certificate family for this target. Arbitrary subspaces, +other permutation modules, role-dependent cuts and nonlinear or integer +combinations are outside the proof. Native address realization, compiler, +hosting, precision, tape accounting, recursive profiles and the complete +multiplication theorem are unproved here. No human or proof-kernel review +is claimed; no predecessor engine, selected supplier, Lean or Docker replay +is run. + +## Open next questions + +- Can a coordinate cut in a different GL3 permutation module certify more + than three for this exact target? Start with one explicit finite G-set + and report its six generator crossings and target crossing. It must lie + outside the point/line direct-sum class. A stronger valid cut is missing. +- Can a noncoordinate subspace cut in a point/line module sum exceed three? + Start with one explicit binary subspace and compute all seven quotient + ranks. The present proof uses coordinate subsets and does not settle it. + +## Sources and credit + +The proof and verifier were produced by Nick Petalas. Apache-2.0. +Credit Josie Elliston's +[PR #1974](https://github.com/CrocSwap/integer-mult-bounds/pull/1974) and +Hanson Sun's seed18 package for the formal mixed-target model and written +invariant question; Adam Gall and Ross Richardson for the cut-rank method; +JoyboyBrian's [PR #4974](https://github.com/CrocSwap/integer-mult-bounds/pull/4974) +for the existing single-target support argument; and the retained eumemic, +Ali Romman and Gareth Davidson register-model lineage. The cut inequality +and single-target distance principle are inherited. The matching finite +cone certificates for this Singer endpoint are the new contribution. + +[SOURCES.json](SOURCES.json) pins the source bytes at canonical main +`de5ec2e7a6074068452f45b1a191b5c72832df4a`. The +[advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19217837) +records the exact scope. Main-tree, merged-PR, open-PR and live claim +searches found no matching Singer point/line certificate. This is search +coverage, not a guarantee about unpublished work. The existing three-cycle +cut-ceiling work has a different endpoint and is not extended here. diff --git a/research/gl3-singer-cut-gap/SOURCES.json b/research/gl3-singer-cut-gap/SOURCES.json new file mode 100644 index 0000000000..c14502ade1 --- /dev/null +++ b/research/gl3-singer-cut-gap/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/bit-gl3-mixed-targets-length10/README.md", + "usage": "input", + "git_blob": "59ac7008af69ffb41e10e6574308d68c33d44c48", + "sha256": "f1f88a618fa998baa2bb5e8bc69c225405b6106b4c0a5646d84c42166cd4aff5" + }, + { + "path": "research/bit-gl3-mixed-targets-seed18/README.md", + "usage": "input", + "git_blob": "3e5f714a9ae2113afdf00352f29c73073843d2a8", + "sha256": "885674f74ba2f40256f0d3388a8e856aae7b27063aea84b2687eda08787e101f" + } + ] +} diff --git a/research/gl3-singer-cut-gap/TASK.json b/research/gl3-singer-cut-gap/TASK.json new file mode 100644 index 0000000000..007ccdc1ea --- /dev/null +++ b/research/gl3-singer-cut-gap/TASK.json @@ -0,0 +1,82 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "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": "Prove exact normalized point/line coordinate-cut cone value 3t for t copies of the GL3 Singer target with columns (7,1,3) or its inverse, versus direct bill 4t.", + "scope_change_reason": "Take PR1974 Open next question 2 and rule out one explicit quotient-based invariant family. This is a proof-method side result, not a new register construction or a predecessor census replay.", + "bottleneck_link": "An exact obstruction prevents pursuing this cut family to prove the direct tariff; other modules or noncoordinate invariants are needed.", + "budget_minutes": 60, + "stop_rule": "Ship the first matching exact primal/dual certificate. Do not expand to other modules or targets.", + "outcome": "completed", + "evidence": "All 256 point/line cuts satisfy the exact dual inequality; two explicit cuts attain value three. A written direct-sum and cut-rank argument gives every finite module sum and dirty-role count.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can another GL3 permutation module certify more than three for this Singer target?", + "why_it_matters": "This would leave the exact closed certificate family.", + "first_step": "Give one explicit finite G-set and its six generator cuts and target cut.", + "blocked_by": "No stronger valid cut is supplied." + }, + { + "question": "Can a noncoordinate subspace cut in a point/line module sum exceed three?", + "why_it_matters": "Such a cut changes the coordinate-subset hypothesis.", + "first_step": "Provide one explicit binary subspace and compute all seven quotient ranks.", + "blocked_by": "No such subspace or upper certificate is known here." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19217837", + "question_source": { + "pr": 1974, + "author": "JosieElliston", + "question": "Open next question 2, written invariant for additive tariffs" + }, + "environment": { + "python": "3.12.15 (main, Oct 14 2026, 00:55:37) [Clang 23.1.3 ]", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "dependencies": "Python standard library only", + "receipt": "Generated on stdout from a fresh complete computation; no stored receipt accepted." + } +} diff --git a/research/gl3-singer-cut-gap/VERIFY.json b/research/gl3-singer-cut-gap/VERIFY.json new file mode 100644 index 0000000000..622f772cc2 --- /dev/null +++ b/research/gl3-singer-cut-gap/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/bit-gl3-mixed-targets-length10/README.md", + "research/bit-gl3-mixed-targets-seed18/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Complete exact point/line cut certificate, action/endpoint and rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Same complete certificate and controls with assertions disabled." + } + ] +} diff --git a/research/gl3-singer-cut-gap/verify.py b/research/gl3-singer-cut-gap/verify.py new file mode 100644 index 0000000000..b86496118b --- /dev/null +++ b/research/gl3-singer-cut-gap/verify.py @@ -0,0 +1,325 @@ +#!/usr/bin/env python3 +"""Exact certificate for the declared Fano coordinate-cut cone. + +Produced by Nick Petalas. Apache-2.0. +No solver, predecessor executable, network, Git or output file is needed. +""" + +import hashlib +import itertools +import json +from collections import Counter +from pathlib import Path + + +IDENTITY = (1, 2, 4) +TARGET = (7, 1, 3) +LABELS = tuple((i, j) for i in range(3) for j in range(3) if i != j) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def apply(matrix, vector): + value = 0 + for i in range(3): + if vector >> i & 1: + value ^= matrix[i] + return value + + +def multiply(left, right): + return tuple(apply(left, column) for column in right) + + +def generators(): + result = [] + for i, j in LABELS: + columns = list(IDENTITY) + columns[j] ^= 1 << i + result.append(tuple(columns)) + return tuple(result) + + +def point_action(matrix): + return tuple(apply(matrix, x) - 1 for x in range(1, 8)) + + +def inverse(matrix): + action = point_action(matrix) + need(sorted(action) == list(range(7)), "matrix is singular") + return tuple(action.index(x - 1) + 1 for x in IDENTITY) + + +def line_action(matrix): + inv = inverse(matrix) + return tuple(sum(((inv[k] & x).bit_count() % 2) << k + for k in range(3)) - 1 for x in range(1, 8)) + + +def crossing(action, mask): + need(0 <= mask < 128, "cut mask out of range") + return sum((mask >> x & 1) and not (mask >> action[x] & 1) + for x in range(7)) + + +def all_group_elements(gens): + group = tuple(a for a in itertools.product(range(1, 8), repeat=3) + if len({apply(a, x) for x in range(1, 8)}) == 7) + need(len(group) == 168, "wrong GL3 order") + words = {IDENTITY: ()} + frontier = [IDENTITY] + for _ in range(7): + following = [] + for matrix in frontier: + for label, gen in enumerate(gens): + product = multiply(gen, matrix) + if product not in words: + words[product] = words[matrix] + (label,) + following.append(product) + frontier = following + need(set(words) == set(group), "incomplete Cayley traversal") + need(len(words[TARGET]) == 4, "target distance changed") + power = IDENTITY + for _ in range(7): + power = multiply(TARGET, power) + need(power == IDENTITY and TARGET != IDENTITY, "target order is not seven") + return group, words[TARGET] + + +def check_actions(group): + """Compare columns to an independently evaluated row/dot-product action.""" + points = {} + lines = {} + for matrix in group: + rows = tuple(sum(((matrix[j] >> i) & 1) << j for j in range(3)) + for i in range(3)) + alternate = tuple(sum(((row & x).bit_count() % 2) << i + for i, row in enumerate(rows)) - 1 + for x in range(1, 8)) + points[matrix] = point_action(matrix) + lines[matrix] = line_action(matrix) + need(points[matrix] == alternate, "row/column action disagreement") + # Orthogonality identifies each line without a transpose convention. + for normal in range(1, 8): + members = {x - 1 for x in range(1, 8) + if (normal & x).bit_count() % 2 == 0} + image = {points[matrix][x] for x in members} + new_normal = lines[matrix][normal - 1] + 1 + expected = {x - 1 for x in range(1, 8) + if (new_normal & x).bit_count() % 2 == 0} + need(image == expected, "point/line incidence disagreement") + for left, right in itertools.product(group, repeat=2): + product = multiply(left, right) + for actions in (points, lines): + need(actions[product] == tuple(actions[left][x] + for x in actions[right]), + "action is not a homomorphism") + return points, lines + + +def cut_certificate(gens, actions): + profiles = [] + histograms = [] + for action in actions: + histogram = Counter() + for mask in range(128): + paid = tuple(crossing(action[g], mask) for g in gens) + target = crossing(action[TARGET], mask) + slack = sum(paid) - 2 * target + need(slack >= 0, "dual certificate violated") + need(crossing(action[inverse(TARGET)], mask) == target, + "inverse target changes the cut") + complement = mask ^ 127 + need(crossing(action[TARGET], complement) == target, + "complement symmetry violated") + profiles.append([mask, list(paid), target, slack]) + histogram[slack] += 1 + histograms.append(dict(sorted(histogram.items()))) + point = profiles[42] + line = profiles[128 + 10] + need(point[1:] == [[2, 2, 0, 0, 0, 0], 2, 0], "point primal changed") + need(line[1:] == [[0, 0, 1, 1, 1, 1], 2, 0], "line primal changed") + need(all(point[1][i] + 2 * line[1][i] == 2 for i in range(6)), + "primal exceeds a paid budget") + need(point[2] + 2 * line[2] == 6, "primal value is not three") + return profiles, histograms + + +def binary_rank(rows): + pivots = {} + for row in rows: + for _ in range(21): + if not row: + break + pivot = row.bit_length() - 1 + if pivot not in pivots: + pivots[pivot] = row + break + row ^= pivots[pivot] + else: + raise ValueError("rank elimination exceeded capacity") + return len(pivots) + + +def paid_block(action, mask, u, v, width): + rows = [] + for role in range(width): + for address in range(7): + if mask >> address & 1: + continue + row = 0 + for source in range(7): + if (mask >> source & 1 and action[source] == address + and u >> role & 1): + for donor in range(width): + if v >> donor & 1: + row |= 1 << (7 * donor + source) + rows.append(row) + return rows + + +def check_paid_blocks(gens, actions): + """Test actual crossing matrices, rather than only the rank formula.""" + count = 0 + projectors = 0 + for width in range(1, 4): + for u, v in itertools.product(range(1, 1 << width), repeat=2): + if (u & v).bit_count() % 2 != 1: + continue + projectors += 1 + for action in actions: + for gen in gens: + for mask in (0, 10, 42, 85, 117, 127): + rows = paid_block(action[gen], mask, u, v, width) + need(binary_rank(rows) == crossing(action[gen], mask), + "paid tensor crossing rank mismatch") + count += 1 + need(projectors == 35, "projector domain incomplete") + return count + + +def scalar_multiply(left, right, width): + rows = [] + for row in left: + output = 0 + for j in range(width): + if row >> j & 1: + output ^= right[j] + rows.append(output) + return tuple(rows) + + +def formal_multiply(left, right, width): + result = {} + for a, b in itertools.product(left, right): + product = multiply(a, b) + value = scalar_multiply(left[a], right[b], width) + previous = result.get(product, (0,) * width) + result[product] = tuple(x ^ y for x, y in zip(previous, value)) + return {a: rows for a, rows in result.items() if any(rows)} + + +def formal_word(word, width): + unit = tuple(1 << i for i in range(width)) + value = {IDENTITY: unit} + for gen, projector in word: + at_identity = tuple(x ^ y for x, y in zip(unit, projector)) + factor = {IDENTITY: at_identity, gen: projector} + value = formal_multiply(factor, value, width) + return value + + +def check_formal_endpoints(gens, word): + omissions = 0 + for targets in range(1, 4): + width = targets + 1 + circuit = [] + for role in range(targets): + projector = tuple(1 << role if i == role else 0 for i in range(width)) + circuit.extend((gens[label], projector) for label in word) + expected = {TARGET: tuple(1 << i if i < targets else 0 + for i in range(width)), + IDENTITY: tuple(1 << i if i == targets else 0 + for i in range(width))} + need(formal_word(circuit, width) == expected, "direct endpoint failed") + for omitted in range(len(circuit)): + altered = circuit[:omitted] + circuit[omitted + 1:] + need(formal_word(altered, width) != expected, "missing call accepted") + omissions += 1 + # This projector writes an arbitrary source into a dirty spectator. + dirty = tuple(1 if i in (0, targets) else 0 for i in range(width)) + detour = [(gens[0], dirty)] * 2 + need(formal_word(detour + circuit, width) == expected, + "dirty spectator not restored") + need(formal_word(detour[:1] + circuit, width) != expected, + "dirty leakage accepted") + return omissions + + +def boundary_controls(): + for mask in (-1, 128, 256): + try: + crossing(tuple(range(7)), mask) + except ValueError: + continue + raise ValueError("invalid mask accepted") + try: + inverse((1, 1, 4)) + except ValueError: + pass + else: + raise ValueError("singular inverse accepted") + return 4 + + +def source_and_package_hashes(): + package = Path(__file__).resolve().parent + root = package.parents[1] + sources = json.loads((package / "SOURCES.json").read_text()) + source_hashes = {} + for entry in sources["files"]: + if entry["usage"] != "input": + continue + digest = hashlib.sha256((root / entry["path"]).read_bytes()).hexdigest() + need(digest == entry["sha256"], "changed source: " + entry["path"]) + source_hashes[entry["path"]] = digest + package_hashes = {p.name: hashlib.sha256(p.read_bytes()).hexdigest() + for p in sorted(package.iterdir()) if p.is_file()} + return source_hashes, package_hashes + + +def main(): + sources, package = source_and_package_hashes() + gens = generators() + group, word = all_group_elements(gens) + actions = check_actions(group) + profiles, histograms = cut_certificate(gens, actions) + blocks = check_paid_blocks(gens, actions) + omissions = check_formal_endpoints(gens, word) + payload = { + "status": "PASS_GL3_SINGER_CUT_GAP", + "claim_type": "scoped proof with finite cut certificate", + "target_columns": TARGET, + "group_order": len(group), + "cut_count": len(profiles), + "cut_slack_histograms": histograms, + "cut_profiles_sha256": hashlib.sha256(json.dumps(profiles).encode()).hexdigest(), + "action_composition_checks": 2 * len(group) ** 2, + "point_line_incidence_checks": 7 * len(group), + "paid_crossing_blocks": blocks, + "direct_word": [LABELS[i] for i in word], + "direct_distance": len(word), + "cone_value_per_target": 3, + "omitted_call_controls": omissions, + "boundary_controls": boundary_controls(), + "source_sha256": sources, + "package_sha256": package, + } + print(json.dumps(payload, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()