From c4484f0242a3f85b6c822bcb2e0b7c1646496e01 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 13:37:48 +0000 Subject: [PATCH] docs(research): prove the sharp ten-call affine target minimum --- .../affine-four-target-sharp-ten/PROOF.md | 147 +++++++++ .../affine-four-target-sharp-ten/README.md | 107 ++++++ .../affine-four-target-sharp-ten/SOURCES.json | 24 ++ .../affine-four-target-sharp-ten/TASK.json | 84 +++++ .../affine-four-target-sharp-ten/VERIFY.json | 34 ++ .../affine-four-target-sharp-ten/verify.py | 306 ++++++++++++++++++ 6 files changed, 702 insertions(+) create mode 100644 research/affine-four-target-sharp-ten/PROOF.md create mode 100644 research/affine-four-target-sharp-ten/README.md create mode 100644 research/affine-four-target-sharp-ten/SOURCES.json create mode 100644 research/affine-four-target-sharp-ten/TASK.json create mode 100644 research/affine-four-target-sharp-ten/VERIFY.json create mode 100644 research/affine-four-target-sharp-ten/verify.py diff --git a/research/affine-four-target-sharp-ten/PROOF.md b/research/affine-four-target-sharp-ten/PROOF.md new file mode 100644 index 0000000000..4acbf47d90 --- /dev/null +++ b/research/affine-four-target-sharp-ten/PROOF.md @@ -0,0 +1,147 @@ +# Proof of the sharp ten-call minimum + +## Statement and boundary + +Let G=AGL_2(F2), with composition acting on the rightmost argument first. +Write points as (x0,x1) and set + +```text +a(x0,x1) = (x0+x1,x1), b(x0,x1) = (x0,x0+x1), +tx(x0,x1) = (x0+1,x1), ty(x0,x1) = (x0,x1+1), +s = aba, h = s tx, h^-1 = tx s. +``` + +For any finite R>=4, work in M_R(F2[G]). Every data and spectator role has +arbitrary initial contents. The required complete endpoint is + +```text +T = diag([h],[h^-1],[tx],[ty],1,...,1). +``` + +A paid call is D_N(g)=I+([g]+1)N, with g in {a,b,tx,ty}, N=uv^T over F2, +and v^T u=1. Arbitrary scalar GL_R(F2) maps are free and may be interleaved. +The exact minimum paid length is ten, independently of R. No other address +maps, clean allocations, singular scalar operations, COPYs, resets or residual +couplings are allowed. This is a formal algebra theorem, not a native tariff. + +The upper word and four-role target are Cinna Davis's PR #1745. The new result +is the matching lower bound, including arbitrary finite restored dirty roles. +The proof separates the two disjoint classes of paid letters. + +## At least six a/b calls + +The homomorphism G -> GL_2(F2) forgets the translation. It sends tx and ty +to the identity and sends both h and h^-1 to s. Extend it linearly to the +group algebras and entrywise to the role matrices. A putative circuit becomes +a circuit for diag([s],[s],1,...,1), with only its a/b calls remaining. +The six-call lower bound for this two-swap endpoint is already established +by commdata2338's PR #1414. The following cut restates the needed bound +without importing a predecessor executable or finite search. + +The group L=GL_2(F2) has the six distinct elements + +```text +1, a, b, ab, ba, s=aba=bab. +``` + +Use its left regular representation, and split the address basis into +H={1,a,b} and K={ab,ba,s}. Direct multiplication gives + +```text +a H = {a,1,ab}, b H = {b,ba,1}, s H = {s,ab,ba}=K. +``` + +Thus each of a and b has crossing rank one from H to K, while s has +crossing rank three. Include every scalar role in each address half. For +any represented matrix M let q(M)=rank(M[K,H]). Block multiplication gives + +```text +(AB)[K,H] = A[K,H] B[H,H] + A[K,K] B[K,H], +q(AB) <= q(A)+q(B). +``` + +A scalar role map never changes the address and has crossing block zero. +The crossing block of D_N(a) or D_N(b) is N tensor E, where E is the +one-entry crossing matrix of that letter. It has rank one. A projected +translation call is the identity. The complete endpoint has two disjoint +s blocks, hence crossing rank 3+3=6. Identity spectators contribute zero. +Subadditivity proves that the original word contains at least six a/b calls. +This argument does not bound or compress the number of roles. + +The cut-rank method is standard. Adam Gall's PR #1941 and the odd-dihedral +joint-tariff package provide related all-register cut arguments. The two-swap +minimum itself is predecessor work, not a newly claimed result here. + +## At least four translation calls + +Use the homogeneous representation + +```text +rho(A,t) = [ A t ] + [ 0 1 ]. +``` + +After applying rho entrywise and grouping all 2R coordinate rows before the +R homogeneous-coordinate rows, every represented operator has block form + +```text +M = [ L U ] + [ 0 C ]. +``` + +Here U is a 2R-by-R matrix over F2. Define tau(M)=rank(U). For two such +matrices, + +```text +U(M1 M2) = L1 U2 + U1 C2, +tau(M1 M2) <= tau(M1)+tau(M2). +``` + +This rank inequality requires no commutation or independence of intermediate +data. Scalar GL_R mixing has U=0, since it acts as B tensor I2 on coordinate +rows and as B on homogeneous rows. Calls with labels a or b also have U=0. +A translation call with nonzero vector t has + +```text +U(D_(uv^T)(t)) = (u tensor t) v^T. +``` + +Both vectors are nonzero, so this block has rank one. The dot-product +condition is required by the paid alphabet, though nonzero rank alone is +enough for this part of the lower bound. Consequently tau of the final +endpoint is at most the number of tx/ty calls. + +The four nonzero translation vectors of h,h^-1,tx,ty are, respectively, +(0,1), (1,0), (1,0), (0,1). Each occupies a different role. Thus the first +four columns of U(T) have disjoint nonempty coordinate supports, and all +other columns are zero. They are linearly independent, so tau(T)=4. +Every complete circuit therefore contains at least four tx/ty calls. + +These translation calls are disjoint from the a/b calls counted above. +The total paid length is at least 6+4=10. The two representations are used +only for necessary lower bounds. Neither is a sufficient endpoint oracle. + +## Attainment and conclusion + +Use coordinate role projectors. In chronological order execute + +```text +role 0: tx, a, b, a +role 1: a, b, a, tx +role 2: tx +role 3: ty +``` + +The first row produces s tx=h, the second produces tx s=h^-1, and the last +two produce their indicated translations. Every other role is untouched. +These are exactly the predecessor's direct ten paid factors, written in +chronological order. There is no extra scalar operation, workspace, inverse +or unpaid restoration in this upper word. It attains the lower bound. + +This closes PR #1745's eight/nine-call question negatively. Changing the +paid labels or allowing clean-only endpoints requires another argument. +For example, one unit h label would itself have charges q=3 and tau=1; +the separated unit-price proof would no longer apply. Native implementation, +physical costs, recursive interfaces and multiplication exponents are not +consequences of this formal minimum. The proof has not been checked by a +formal proof kernel or independently reviewed by a human. diff --git a/research/affine-four-target-sharp-ten/README.md b/research/affine-four-target-sharp-ten/README.md new file mode 100644 index 0000000000..68cafaff20 --- /dev/null +++ b/research/affine-four-target-sharp-ten/README.md @@ -0,0 +1,107 @@ +# Four mixed affine targets need exactly ten paid calls + +This contribution is produced by Nick Petalas. Claim type: scoped written +algebraic proof with finite exact corroboration. No new kappa. + +Cinna Davis's [PR #1745](https://github.com/CrocSwap/integer-mult-bounds/pull/1745) +left the paid minimum for `diag(h,h^-1,tx,ty)` between eight and ten calls. +The exact minimum is **ten**, even with arbitrary free binary scalar mixing +and any finite number of restored dirty spectators. Here `h=aba tx` in +AGL_2(F2), and the only paid labels are `a,b,tx,ty` with binary rank-one +idempotent role couplings. All original inputs are arbitrary. + +The [proof](PROOF.md) separates the paid alphabet. Forgetting translations +leaves two coordinate swaps, requiring six a/b calls. The homogeneous +translation block has rank four, requiring four tx/ty calls. Since these +letter classes are disjoint, the lower bounds add. The existing direct +word attains ten. The new contribution is the sharp lower bound and its +uniform dirty-workspace implication. The upper word and predecessor's +six/seven-call searches are credited, and their searches are not replayed. + +## Evidence and reproduction + +From the worktree root, using CPython 3.12 and only the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/affine-four-target-sharp-ten/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/affine-four-target-sharp-ten/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/affine-four-target-sharp-ten +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/affine-four-target-sharp-ten --check-source-history +``` + +Use another CPython 3.12 path on another machine. The direct marker is +`PASS_AFFINE_FOUR_TARGET_SHARP_TEN minimum=10 linear_floor=6 translation_floor=4`. +The checker prints a generated receipt bound to all package file hashes. +It writes no files and needs no Git, network, solver or predecessor code. +The registered manifest runs the normal and optimized commands separately. + +The checker verifies all 576 affine quotient products, all 651 binary +rank-one idempotents through five roles with each of the four paid labels, +and both endpoint bounds through eight roles. Exact row-span enumeration +corroborates elimination on all 146 matrices in the declared small domains. +Nine full formal witnesses include scalar conjugations involving dirty +spectators. A separate set-valued faithful regular-action interpreter checks +all 1,344 original input basis columns across those witnesses. All ninety +single-paid-call omissions fail. Boundary controls cover invalid couplings, +extra labels, wrong h/h^-1 order, dirty leakage, invisible representation +kernels and the different charge of an added h label. + +The universal result follows from the written rank inequalities, not from +finite circuit enumeration. Small proof representations never certify a +positive formal endpoint. The witness checker retains all 24 group-algebra +coefficients, and the second interpreter uses the faithful regular action. + +## Scope, provenance and credit + +Canonical base is `de5ec2e7a6074068452f45b1a191b5c72832df4a`, priority revision 8. +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19217827) +proposed an eight/nine-call search. The first new step supplied a direct +proof excluding both lengths, so no solver search was needed. The +`connector-alphabet-change` card is marked changed in [TASK.json](TASK.json). +This is a mechanism-screening side result for a fixed restricted alphabet, +rather than an added operation or a supplier improvement. It identifies +that this particular target has no formal paid-call sharing headroom. + +[SOURCES.json](SOURCES.json) pins the catalogue, selected record and +predecessor README as historical provenance. These are bibliographic inputs; +the standalone proof/checker consumes no predecessor executable or receipt. +No predecessor file, source archive or selected-frontier file is changed. + +Credit Cinna Davis / 1337isnot1337 for PR #1745's target, exact alphabet, +open interval and direct word; Gareth Davidson / bitplane for PR #1333's +affine register framework; commdata2338 for PR #1414's two-swap minimum; +Adam Gall for PR #1941's related cut method; and eumemic, Ali Romman, +David Govea and the contributors retained in those sources for the register +lineage. Elementary block ranks, regular representations and subadditivity +are standard tools. The new separated bound and this package are produced +by Nick Petalas. Apache-2.0. + +## Limitations and unrun obligations + +The theorem requires exact formal group-algebra equality, a fixed linear +word, binary scalar mixing, the four stated paid labels, rank-one idempotent +couplings, and full restoration of arbitrary dirty spectators. It does not +cover larger paid alphabets, clean-only boundaries, erasure, nonlinear or +adaptive programs, or specialized nonfaithful address actions. + +No native supplier, implementation tariff, frame/owner/hosting contract, +movement, stock, precision, tape bill, productive credit or complete recursive +invoice is supplied. No new multiplication exponent follows. The selected +cold replay, Lean, Docker and predecessor scientific suites were not run. +Independent human and formal proof-kernel review are unclaimed. + +The code has no recursion and caps its role domain at eight and matrix +sizes at 256. All checked loops have fixed finite domains or at most twelve +instructions per witness. Python and its exact containers allocate dynamically; +this bounded managed-runtime verifier is not a fixed-allocation program. +Callback controls have an explicit finite target list. Warning-strict normal +and optimized execution supplies interpreter diagnostics. Whole-repository +lint and static typing are outside this isolated package. + +## Open next questions + +Can a concrete native operation justify adding one label that escapes the +separated charge? Begin with one explicit additional affine label and a +complete entrance/exit, scalar, frame, restoration and recursive invoice. +The h label demonstrates the mathematical change, but its native price is +unknown. A larger fixed-alphabet search on this same target cannot beat ten. diff --git a/research/affine-four-target-sharp-ten/SOURCES.json b/research/affine-four-target-sharp-ten/SOURCES.json new file mode 100644 index 0000000000..4525e9a837 --- /dev/null +++ b/research/affine-four-target-sharp-ten/SOURCES.json @@ -0,0 +1,24 @@ +{ + "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/affine-mixed-four-targets-seed5638/README.md", + "usage": "provenance", + "git_blob": "67ccbd01b2b009263c0de7fff7b57d8d1f2c4463", + "sha256": "531944770dd4c36a5eb0c9aa29193aef13b38060fc213694e4abae55899f6e2d" + } + ] +} diff --git a/research/affine-four-target-sharp-ten/TASK.json b/research/affine-four-target-sharp-ten/TASK.json new file mode 100644 index 0000000000..0a4049f172 --- /dev/null +++ b/research/affine-four-target-sharp-ten/TASK.json @@ -0,0 +1,84 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "original_card": { + "id": "connector-alphabet-change", + "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/universal-connector-boundary/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Construct and charge a legal extra operation on a minimal instance.", + "Prove a target-specific bound after adding one specified operation family." + ], + "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free. 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", + "research/universal-connector-boundary/verify.py" + ], + "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY", + "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.", + "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.", + "allowed_variations": [ + "Choose one additional operation and a small source count for its first counterexample." + ], + "scope_change_triggers": [ + "Keeping the alphabet and only increasing the source count; record this as a changed assignment.", + "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions." + ], + "overlap_terms": [ + "universal connector", + "source-toggle", + "connector alphabet" + ] + }, + "scope_status": "changed", + "actual_scope": "Prove the exact ten-call minimum for PR1745 mixed affine targets, for every finite restored dirty workspace.", + "scope_change_reason": "Replace the broad added-alphabet experiment by the predecessor's explicitly open fixed-alphabet eight/nine-call question. The disjoint linear and translation charges resolve it without a solver.", + "bottleneck_link": "Scoped mechanism-screening side result: this fixed mixed target has no paid-call sharing headroom; changing an operation requires complete physical pricing.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified original step, the sharp ten-call lower bound. Do not extend to other targets or alphabets.", + "outcome": "completed", + "evidence": "PROOF.md gives two rank inequalities with endpoint charges 6 and 4. verify.py generates the exact finite corroboration and source-bound receipt.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a concrete native implementation justify one added affine label that escapes the separated charge?", + "why_it_matters": "The fixed four-label target has no formal paid-call sharing gain, while a changed label can have a larger representation charge.", + "first_step": "Specify one added label and price its complete entrance/exit, scalar, frame, restoration and recursive bill.", + "blocked_by": "No actual native label implementation or complete invoice is supplied." + } + ], + "claim_type": "scoped written proof with finite exact corroboration", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19217827", + "playbook": "Autonomous local run", + "overlap": { + "source": "PR #1745", + "source_author": "1337isnot1337", + "checks": "Live open PRs, latest 30 handoff comments, active Discussions, account PRs and distinctive merged/main README searches. Cached card-wide search has 470 open PRs and 5426 Discussion records with complete remote pagination; sparse local inventory is incomplete.", + "limitations": "No search proves novelty; unpublished work and arbitrary historical diffs were not searched." + }, + "local_environment": { + "python": "3.12.15", + "implementation": "CPython", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "interpreter": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12", + "diagnostics": "-I -W error, normal and -O; no assertion-dependent admission" + }, + "local_validation": { + "normal_seconds": 0.117, + "optimized_seconds": 0.119, + "timing_scope": "Whole direct verifier subprocess including startup, receipt construction and output capture; check durations only.", + "status": "Both direct commands and the registered package runner pass; hosted CI separate." + } +} diff --git a/research/affine-four-target-sharp-ten/VERIFY.json b/research/affine-four-target-sharp-ten/VERIFY.json new file mode 100644 index 0000000000..41e4ade3ee --- /dev/null +++ b/research/affine-four-target-sharp-ten/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact quotient/cut/translation factors, full formal and faithful dirty endpoints, omission and scope controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same checks with Python assertions disabled; acceptance uses explicit exceptions." + } + ] +} diff --git a/research/affine-four-target-sharp-ten/verify.py b/research/affine-four-target-sharp-ten/verify.py new file mode 100644 index 0000000000..621cefa172 --- /dev/null +++ b/research/affine-four-target-sharp-ten/verify.py @@ -0,0 +1,306 @@ +#!/usr/bin/env python3 +"""Exact corroboration of the separated linear/translation lower bound.""" +from __future__ import annotations + +import hashlib +import itertools +import json +from pathlib import Path + +IDENTITY = (0, 1, 2, 3) +LABELS = {"a": (0, 1, 3, 2), "b": (0, 3, 2, 1), + "tx": (1, 0, 3, 2), "ty": (2, 3, 0, 1)} +MAX_ROLES = 8 + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def compose(left, right): + return tuple(left[right[i]] for i in range(4)) + + +def linear_part(g): + return tuple(x ^ g[0] for x in g) + + +def rank(rows, columns): + need(0 <= columns <= 256 and len(rows) <= 256, "rank domain") + need(all(type(x) is int and 0 <= x < 1 << columns for x in rows), "rank rows") + basis = [0] * columns + answer = 0 + for original in rows: + row = original + for bit in range(columns - 1, -1, -1): + if row >> bit & 1: + if basis[bit]: + row ^= basis[bit] + else: + basis[bit] = row + answer += 1 + break + return answer + + +def parity(value): + return value.bit_count() & 1 + + +def validate_gate(roles, name, u, v): + need(type(roles) is int and 1 <= roles <= MAX_ROLES, "role domain") + need(name in LABELS, "paid alphabet") + need(type(u) is int and type(v) is int, "coupling type") + need(0 < u < 1 << roles and 0 < v < 1 << roles, "coupling range") + need(parity(u & v) == 1, "idempotent coupling") + + +def group_data(): + group = tuple(itertools.permutations(range(4))) + need(len(group) == 24 and all(linear_part(g) in group for g in group), "affine group") + linear = tuple(g for g in group if g[0] == 0) + a, b = LABELS["a"], LABELS["b"] + swap = compose(compose(a, b), a) + half = frozenset((IDENTITY, a, b)) + need(len(linear) == 6 and len(half) == 3, "regular cut") + need({compose(swap, x) for x in half} == set(linear) - half, "swap crosses all") + for g, h in itertools.product(group, repeat=2): + need(linear_part(compose(g, h)) == compose(linear_part(g), linear_part(h)), + "quotient homomorphism") + return group, linear, half, swap + + +def homogeneous(g): + origin = g[0] + col0, col1 = g[1] ^ origin, g[2] ^ origin + return (sum(((x >> 0) & 1) << j for j, x in enumerate((col0, col1, origin))), + sum(((x >> 1) & 1) << j for j, x in enumerate((col0, col1, origin))), 4) + + +def represented_factor(roles, g, u, v): + block = homogeneous(g) + rows = [1 << i for i in range(3 * roles)] + for i, j, d in itertools.product(range(roles), range(roles), range(3)): + if u >> i & v >> j & 1: + rows[3 * i + d] ^= (block[d] ^ (1 << d)) << (3 * j) + return tuple(rows) + + +def translation_block(rows, roles): + return tuple(sum(((rows[3 * i + d] >> (3 * j + 2)) & 1) << j + for j in range(roles)) for i in range(roles) for d in range(2)) + + +def crossing_factor(roles, g, u, v, linear, half): + inside = tuple(x for x in linear if x in half) + outside = tuple(x for x in linear if x not in half) + rows = [] + for i, destination in itertools.product(range(roles), outside): + row = 0 + for j, source in itertools.product(range(roles), inside): + if u >> i & v >> j & 1 and compose(g, source) == destination: + row |= 1 << (3 * j + inside.index(source)) + rows.append(row) + return tuple(rows) + + +def proof_factors(linear, half): + counts = {} + for roles in range(1, 6): + projectors = [(u, v) for u in range(1, 1 << roles) + for v in range(1, 1 << roles) if parity(u & v)] + counts[str(roles)] = len(projectors) + for (u, v), (name, g) in itertools.product(projectors, LABELS.items()): + validate_gate(roles, name, u, v) + t = rank(translation_block(represented_factor(roles, g, u, v), roles), roles) + q = rank(crossing_factor(roles, linear_part(g), u, v, linear, half), 3 * roles) + need((q, t) == ((1, 0) if name in ("a", "b") else (0, 1)), + "separated paid charges") + return counts + + +def targets(swap): + return (compose(swap, LABELS["tx"]), compose(LABELS["tx"], swap), + LABELS["tx"], LABELS["ty"]) + + +def endpoint_bounds(linear, half, wanted): + result = [] + for roles in range(4, MAX_ROLES + 1): + rows = tuple(homogeneous(g)[d] << (3 * i) + for i, g in enumerate(wanted + (IDENTITY,) * (roles - 4)) + for d in range(3)) + t = rank(translation_block(rows, roles), roles) + q = sum(rank(crossing_factor(1, linear_part(g), 1, 1, linear, half), 3) + for g in wanted) + need((q, t) == (6, 4), "endpoint lower bounds") + result.append({"roles": roles, "linear_floor": q, "translation_floor": t}) + return result + + +def direct_word(roles): + need(4 <= roles <= MAX_ROLES, "witness roles") + word = [] + # Chronological order is the reverse of each displayed group product. + for i, names in enumerate((("tx", "a", "b", "a"), + ("a", "b", "a", "tx"), ("tx",), ("ty",))): + word.extend(("paid", name, 1 << i, 1 << i) for name in names) + return word + + +def formal_apply(roles, word, group): + index = {g: i for i, g in enumerate(group)} + one = 1 << index[IDENTITY] + matrix = [[one if i == j else 0 for j in range(roles)] for i in range(roles)] + for kind, name, u, v in word: + if kind == "scalar": + need(name == "add" and 0 <= u < roles and 0 <= v < roles and u != v, + "scalar instruction") + matrix[u] = [x ^ y for x, y in zip(matrix[u], matrix[v])] + continue + need(kind == "paid", "instruction kind") + validate_gate(roles, name, u, v) + source = [0] * roles + for i in range(roles): + if v >> i & 1: + source = [x ^ y for x, y in zip(source, matrix[i])] + delta = [] + for entry in source: + translated = 0 + for k, element in enumerate(group): + if entry >> k & 1: + translated ^= 1 << index[compose(LABELS[name], element)] + delta.append(entry ^ translated) + for i in range(roles): + if u >> i & 1: + matrix[i] = [x ^ y for x, y in zip(matrix[i], delta)] + return tuple(tuple(row) for row in matrix) + + +def literal_columns(roles, word, group, wanted): + """Separate set-valued regular-action execution on every dirty input column.""" + for original_role, address in itertools.product(range(roles), group): + state = [set() for _ in range(roles)] + state[original_role] = {address} + for kind, name, u, v in word: + if kind == "scalar": + state[u] ^= state[v] + continue + validate_gate(roles, name, u, v) + source = set() + for i in range(roles): + if v >> i & 1: + source ^= state[i] + perm = LABELS[name] + delta = source ^ {tuple(perm[x] for x in element) for element in source} + for i in range(roles): + if u >> i & 1: + state[i] ^= delta + expected = [set() for _ in range(roles)] + g = wanted[original_role] if original_role < 4 else IDENTITY + expected[original_role] = {tuple(g[x] for x in address)} + need(state == expected, "literal dirty endpoint") + return roles * 24 + + +def witness_checks(group, wanted): + index = {g: i for i, g in enumerate(group)} + columns = 0 + omitted = 0 + witnesses = 0 + for roles in range(4, MAX_ROLES + 1): + word = direct_word(roles) + for mixed in range(2 if roles > 4 else 1): + actual = word + if mixed: + changed = [] + for kind, name, u, v in word: + up = u ^ ((u >> (roles - 1) & 1) << 0) + vp = v ^ ((v & 1) << (roles - 1)) + changed.append((kind, name, up, vp)) + actual = [("scalar", "add", 0, roles - 1)] + changed + actual += [("scalar", "add", 0, roles - 1)] + endpoint = formal_apply(roles, actual, group) + expected = tuple(tuple((1 << index[wanted[i] if i < 4 else IDENTITY]) + if i == j else 0 for j in range(roles)) + for i in range(roles)) + need(endpoint == expected, "full formal witness") + columns += literal_columns(roles, actual, group, wanted) + witnesses += 1 + for position, instruction in enumerate(actual): + if instruction[0] == "paid": + need(formal_apply(roles, actual[:position] + actual[position + 1:], group) + != expected, "omitted paid call accepted") + omitted += 1 + return {"witnesses": witnesses, "regular_basis_columns": columns, + "single_paid_call_omissions_rejected": omitted} + + +def rejects(function, message): + try: + function() + except ValueError: + return + raise ValueError(message) + + +def controls(group, linear, half, wanted): + rejects(lambda: validate_gate(4, "h", 1, 1), "new label accepted") + rejects(lambda: validate_gate(4, "a", 1, 2), "nilpotent accepted") + rejects(lambda: validate_gate(4, "a", 0, 1), "zero coupling accepted") + rejects(lambda: validate_gate(4, "a", 16, 1), "oversized coupling accepted") + rejects(lambda: validate_gate(True, "a", 1, 1), "boolean role count accepted") + word = direct_word(5) + [("paid", "tx", 16, 16)] + rejects(lambda: literal_columns(5, word, group, wanted), "dirty spectator leakage") + reversed_target = (wanted[1], wanted[0], wanted[2], wanted[3]) + rejects(lambda: literal_columns(4, direct_word(4), group, reversed_target), "phase order") + # The necessary representations are deliberately not endpoint certificates. + omega_h = tuple(0 for _ in range(3)) + for g in group: + omega_h = tuple(x ^ y for x, y in zip(omega_h, homogeneous(g))) + need(omega_h == (0, 0, 0), "homogeneous alias control") + need(all(sum(linear_part(g) == h for g in group) == 4 for h in linear), + "quotient alias control") + need(len(group) > 0 and len(set(group)) == 24, "formal Omega is nonzero") + # An extra affine h label has charges (3,1), rather than a unit charge. + q = rank(crossing_factor(1, linear_part(wanted[0]), 1, 1, linear, half), 3) + t = rank(translation_block(represented_factor(1, wanted[0], 1, 1), 1), 1) + need((q, t) == (3, 1), "enlarged-alphabet distinction") + return 10 + + +def rank_controls(): + checked = 0 + for nrows, ncols in ((1, 1), (2, 2), (2, 3), (3, 2)): + for rows in itertools.product(range(1 << ncols), repeat=nrows): + span = {0} + for row in rows: + span |= {x ^ row for x in span} + need(len(span) == 1 << rank(rows, ncols), "independent rank oracle") + checked += 1 + return checked + + +def main(): + group, linear, half, swap = group_data() + wanted = targets(swap) + need(wanted[0] == (2, 0, 3, 1) and wanted[1] == (1, 3, 0, 2), "target convention") + receipt = { + "claim_type": "scoped written proof with finite exact corroboration", + "minimum": 10, + "projectors_by_roles": proof_factors(linear, half), + "endpoint_bounds": endpoint_bounds(linear, half, wanted), + "witness_checks": witness_checks(group, wanted), + "boundary_controls": controls(group, linear, half, wanted), + "rank_oracle_matrices": rank_controls(), + } + root = Path(__file__).resolve().parent + receipt["source_sha256"] = {p.name: hashlib.sha256(p.read_bytes()).hexdigest() + for p in sorted(root.iterdir()) if p.is_file()} + print("PASS_AFFINE_FOUR_TARGET_SHARP_TEN minimum=10 linear_floor=6 translation_floor=4") + print(json.dumps(receipt, sort_keys=True)) + + +if __name__ == "__main__": + main()