From c33d673cb7e913f0e013c55111558297473d0ce8 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 09:12:57 +0000 Subject: [PATCH] feat(research): prove asymmetric UT3 tariff gap --- .../ut3-asymmetric-monotone-gap/README.md | 218 +++++++++++++ .../ut3-asymmetric-monotone-gap/RESULT.json | 37 +++ .../ut3-asymmetric-monotone-gap/SOURCES.json | 36 +++ .../ut3-asymmetric-monotone-gap/TASK.json | 73 +++++ .../ut3-asymmetric-monotone-gap/VERIFY.json | 34 +++ .../ut3-asymmetric-monotone-gap/verify.py | 288 ++++++++++++++++++ 6 files changed, 686 insertions(+) create mode 100644 research/ut3-asymmetric-monotone-gap/README.md create mode 100644 research/ut3-asymmetric-monotone-gap/RESULT.json create mode 100644 research/ut3-asymmetric-monotone-gap/SOURCES.json create mode 100644 research/ut3-asymmetric-monotone-gap/TASK.json create mode 100644 research/ut3-asymmetric-monotone-gap/VERIFY.json create mode 100644 research/ut3-asymmetric-monotone-gap/verify.py diff --git a/research/ut3-asymmetric-monotone-gap/README.md b/research/ut3-asymmetric-monotone-gap/README.md new file mode 100644 index 0000000000..74c7496b36 --- /dev/null +++ b/research/ut3-asymmetric-monotone-gap/README.md @@ -0,0 +1,218 @@ +# Separate monotone UT3 price minima need not compose + +For three central UT3(F2) targets with scalar rank cap three, set the complete +positive-rank prices to `a(d)=5+d^2` and `b(d)=10+d`. The exact full formal bill +is **54**, although the two independent partition minima sum to **53**. +Arbitrarily many restored dirty roles and non-idempotent scalar couplings +cannot attain that separate lower bill. + +Claim type: **scoped algebraic proof with exact finite corroboration**. +This answers the nonproportional-price question in +[PR4846](https://github.com/CrocSwap/integer-mult-bounds/pull/4846) negatively. +The new step is a chronological cut obstruction. The predecessor's common-price +theorem remains applicable to its stated hypothesis. No physical supplier, +recursive moment gain, new kappa or complete multiplication theorem is supplied. + +This package was produced by Nick Petalas. Independent human and formal +proof-kernel review are unclaimed. Apache-2.0. + +## Model and theorem + +Use Arham Tahir's [PR1919](https://github.com/CrocSwap/integer-mult-bounds/pull/1919) +rank-capped alphabet. Write `G=UT3(F2)` as + +```text +(x,y,z)(u,v,w) = (x+u, y+v, z+w+xv), +a=(1,0,0), b=(0,1,0), c=abab=(0,0,1). +``` + +Group coordinates use binary arithmetic. For any finite `r>=3`, a paid call +in `Mat_r(F2[G])` is `D_N(g)=I+([g]+[1])N`, where `g` is `a` or `b` and +`1<=rank_F2(N)<=3`. Matrices `N` need not be idempotent. Every call is an +involution because `([g]+[1])^2=0`. Scalar invertible binary maps are free +in this formal model. Conjugation normalizes them into the paid matrices; +augmentation forces the remaining scalar map to be identity, as in PR1919. + +Require the entire formal endpoint + +```text +T = diag([c],[c],[c],[1],...,[1]). +``` + +Every input is arbitrary, including every spectator. There are no clean +ancillas, free address maps, central-letter calls, COPY, ERASE or uncharged +inverse calls. All restoration calls are charged. + +Define the two nonnegative nondecreasing prices, with value zero at rank zero, +by `a(1..3)=(6,9,14)` and `b(1..3)=(11,12,13)`. + +**Theorem.** The exact minimum bill for T is 54 for every finite r>=3. +The independent rank-partition lower bounds are 27 for a and 26 for b, but +no single legal word attains both. Four rank-three calls attain 54 without +extra roles. + +## Proof + +PR1919's coefficient-span lemma gives total rank at least six for each +letter, for every legal full endpoint and arbitrary restored dirty workspace. +Its rank argument builds on steph4n-gh #1573, Arham Tahir #1589 and Hanson Sun +#1607. The present proof uses that lemma. No predecessor executable is imported +or replayed. + +For ranks d=1,2,3, the exact rational dual bounds are + +```text +a(d) >= (9/2)d, with equality only at d=2; +b(d) >= (13/3)d, with equality only at d=3. +``` + +Consequently every word costs at least `27+26=53`. Equality requires total +rank exactly six for each letter, exactly three rank-two a calls and exactly +two rank-three b calls. These are the unique equality rank lists. They also +attain each independent partition minimum separately. + +We now exclude their simultaneous occurrence. Use the inherited quotient + +```text +Q = F2 / (X^2,Y^2, all words of length at least three), +phi([x,y,z]) = 1+xX+yY+zXY+(z+xy)YX. +``` + +The group law makes phi an algebra homomorphism. It sends a calls to `I+NX` +and b calls to `I+NY`. Put `P=diag(1,1,1,0,...,0)`. The full endpoint has +zero X and Y coefficients and has both XY and YX coefficients equal to P. +This quotient supplies necessary conditions, not a sufficient endpoint test. + +Consider any realizing word with exactly two b calls. Their scalar matrices +are equal, say N, because the Y coefficient is zero. Let L, M and R be the +sums of a-call matrices before the first b, between the two b calls and after +the second b. Vanishing of the X coefficient gives `L+M+R=0`. Expanding the +two mixed coefficients in their actual order gives + +```text +XY: L N + (L+M)N = M N = P, +YX: N(M+R) + N R = N M = P. +``` + +Thus `rank M>=3`. Also `M=L+R`, so the a calls outside the interval have +rank sum at least three. The a calls inside the interval likewise have rank +sum at least three. If every a call has rank two, at least two must lie +inside and at least two outside. There cannot be only three a calls. +The argument permits arbitrary noncommuting matrices and every finite number +of restored dirty spectators. + +This excludes bill 53. Every call price is an integer, so the bill is at +least 54. For attainment, execute `D_P(a),D_P(b),D_P(a),D_P(b)`. Each target +sees `abab=c`; every spectator sees identity. Its complete price is +`2*14+2*13=54`. This proves the theorem. + +The result does not contradict the earlier asymmetric concave theorem in +[PR2129](https://github.com/CrocSwap/integer-mult-bounds/pull/2129). The a +price here is nonconcave. The common monotone theorem of #4846 also remains +unchanged. The failed implication is that arbitrary separate monotone +partition optima always compose into one legal word. + +## Exact evidence + +[verify.py](verify.py) is a new standard-library implementation. +[RESULT.json](RESULT.json) is generated by replay and binds all five source +and metadata files by SHA256. It records: + +- The two exact price duals and their equality cases, all seven rank-count + partitions of six with parts at most three, and all ten a/b order patterns + with three a calls and two b calls. +- All 3,840 choices of nonzero two-by-two N and arbitrary L,M, with R=L+M, + evaluated in the full formal group algebra. Their mixed coefficients equal + MN and NM in every case. Sixteen choices give the full two-target endpoint. + These are cut-identity fixtures, not a census of three-target words. +- Thirty-six complete endpoint fixtures on three through six roles. Eight + are the two orientations of the optimal word. Twenty-eight are six-call + rank-two comparison words under seven target-basis frames. A separate + literal three-by-three address-matrix implementation checks all 1,296 + faithful regular-action basis columns, including every dirty spectator. +- Thirty-two deleted-call controls and three semantic controls reject: + a changed dirty spectator, a nonzero formal perturbation invisible to the + quotient, and an unrestored first-order coefficient. The quotient-kernel + perturbation is a diagnostic operator, not an asserted paid word. + +The all-workspace lower bound is the written proof. Finite tests corroborate +its equations and the attaining boundary; they do not replace it. No previous +contributor's reported count is rechecked as this package's deliverable. + +## Reproduction + +From the repository root with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/ut3-asymmetric-monotone-gap +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/ut3-asymmetric-monotone-gap/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/ut3-asymmetric-monotone-gap/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/ut3-asymmetric-monotone-gap --check-source-history +``` + +Elsewhere replace the interpreter path with CPython 3.12. The direct marker is +`PASS_UT3_ASYMMETRIC_MONOTONE_GAP separate=53 exact=54 no_new_kappa`. +Normal replay writes nothing. `verify.py --emit` prints a freshly computed +receipt to standard output. Both registered commands have 120-second limits. + +## Scope, sources and credit + +Scientific base is canonical main `de5ec2e7a6074068452f45b1a191b5c72832df4a`, +priority revision 8, selected conditional kappa .00310045. The selected +source-binding orientation passes; it is not a scientific replay. +[SOURCES.json](SOURCES.json) pins the exact predecessor READMEs, selected +record and catalogue as historical provenance. There are no live external +inputs. [TASK.json](TASK.json) records the changed card scope and structured +next questions. The +[advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19213517) +names this exact pricing question. + +Credit Arham Tahir #1919 for the rank-capped alphabet, rank-volume lemma and +nonlinear-pricing question; Nick Petalas #2129 for asymmetric concave pricing +and #4846 for common monotone pricing and the explicit open question; and +steph4n-gh #1573, Arham Tahir #1589, Hanson Sun #1607 and Josie Elliston #1792 +for the retained coefficient-span and model lineage. Retain juper997 #1478, +woklerx #1443, Gareth Davidson / bitplane #1333 and their credited predecessors. +Their files and credit lines are unchanged. + +Entry overlap included 405 open PRs and 5,286 Discussion records with complete +remote pagination. Sparse local coverage was incomplete. Separate all-main +README searches, merged PR searches and the relevant UT3 pricing PR bodies +found the explicit unresolved question but no delivered asymmetric monotone +gap. Arbitrary nested files, unindexed literature and unpublished work are +outside that coverage; global literature priority is unclaimed. + +Physical scalar mixing, native address implementation, recursive-child rank +identification, hosting, precision/tape costs, compiler admission and analytic +transfer are outside scope. No selected cold replay, Lean or Docker run was +performed. The selected frontier is unchanged. + +## Open next questions + +Can one characterize when separate monotone partition minima are compatible? +Start with exactly two b calls and classify a-rank partitions that can supply +rank three on both sides of the interval cut. This would improve interface +pricing, but the cut alone need not suffice for arbitrary noncommuting words. + +Can a native complete UT3 interface realize useful asymmetric prices? First +specify one literal producer/consumer pair and charge scalar mixing, frames, +preparation, dirty restoration, hosting and precision. Physical realization +and the interpretation of scalar rank as recursive child rank are missing. + +## Implementation bounds + +The verifier has no recursion, subprocesses, network access or write path. +Formal matrices have at most six roles and eight group coefficients per cell; +words have at most sixteen factors. The cut sweep has exactly 3,840 cases, +the partition scan has 343 count vectors, and kernel scanning has 255 masks. +The literal check covers at most 48 basis inputs per fixture. Source and +receipt reads reject files exceeding 128 KiB. Every function is below sixty +physical lines. Exceptions keep all checks active under optimized Python. + +Power-of-Ten rule 3 has a managed-runtime deviation. Python allocates bounded +lists, tuples and integers during replay; allocator internals are not +instrumented and no allocation-free execution is claimed. Raw-pointer and +preprocessor restrictions have no direct Python equivalent. Calls are direct +apart from fixed standard-library iteration and JSON serialization. Warning- +strict normal and optimized replay plus AST/function-length inspection are +the available diagnostics; no separate static type checker is configured. diff --git a/research/ut3-asymmetric-monotone-gap/RESULT.json b/research/ut3-asymmetric-monotone-gap/RESULT.json new file mode 100644 index 0000000000..98df4546f8 --- /dev/null +++ b/research/ut3-asymmetric-monotone-gap/RESULT.json @@ -0,0 +1,37 @@ +{ + "claim_type": "scoped algebraic proof", + "cut_cases": 3840, + "deleted_call_controls": 32, + "endpoint_fixtures": 36, + "full_two_target_cases": 16, + "no_new_kappa": true, + "prices": { + "a_prices": [ + 0, + 6, + 9, + 14 + ], + "b_prices": [ + 0, + 11, + 12, + 13 + ], + "full_minimum": 54, + "letter_orders": 10, + "partitions": 7, + "separate_minimum": 53 + }, + "regular_basis_columns": 1296, + "schema_version": 1, + "semantic_controls": 3, + "shadow_kernel_masks": 7, + "source_sha256": { + "README.md": "83b933b256e70499121efd9d9cc2e1d8d64c8c939b460dccd28d7fd9c5d68146", + "SOURCES.json": "a3977e9c8c0cc85acb2c9f784ce097ea6a24022353aa1ca7e6232ad5b9745011", + "TASK.json": "9a06aa1f61f18f15964ad6a3b4128b0f054dcf247d0557ceae036560169829f3", + "VERIFY.json": "de21ebd18023186f98fe1ce427b779b29297a670ee76af95230de8c3fdb667c6", + "verify.py": "5422cd563779273783583e687d438982cf8fe910aa28c71c78222a70cac48062" + } +} diff --git a/research/ut3-asymmetric-monotone-gap/SOURCES.json b/research/ut3-asymmetric-monotone-gap/SOURCES.json new file mode 100644 index 0000000000..cf37779a4c --- /dev/null +++ b/research/ut3-asymmetric-monotone-gap/SOURCES.json @@ -0,0 +1,36 @@ +{ + "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/ut3-rank-bounded-block-calls/README.md", + "usage": "provenance", + "git_blob": "dc0d1bac91fcebecc9fed4e8c3d26a11acca3ef5", + "sha256": "822574c7040b5571d729960951425a1ad9742ae8541a2af2882733f952975b5d" + }, + { + "path": "research/ut3-concave-rank-tariff/README.md", + "usage": "provenance", + "git_blob": "28526ec86ed833f345247c67718fa151fe2a039f", + "sha256": "33244a1263261475f549c57e5714921e97eba29fc3c7ab0eaaccacb18cc16fa1" + }, + { + "path": "research/ut3-monotone-rank-tariff/README.md", + "usage": "provenance", + "git_blob": "ac6dd3ff8e5b79071adb79660f9e9c43e9f9809b", + "sha256": "977b84a16161b413f232a4b563c801ecbca22e9b41bf931a4f8c5cf25a4f892f" + } + ] +} diff --git a/research/ut3-asymmetric-monotone-gap/TASK.json b/research/ut3-asymmetric-monotone-gap/TASK.json new file mode 100644 index 0000000000..0b0313a884 --- /dev/null +++ b/research/ut3-asymmetric-monotone-gap/TASK.json @@ -0,0 +1,73 @@ +{ + "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": "A sharp asymmetric monotone tariff gap for three central UT3(F2) block targets, rank cap three and arbitrary restored dirty workspace.", + "scope_change_reason": "Take the explicit nonproportional-price question in merged PR4846. The card asks for a new mechanism; this is a formal pricing obstruction for the existing PR1919 alphabet, with no native implementation or supplier gain.", + "bottleneck_link": "Independent letter optimizers need not compose into a chronological word. The exact 54-versus-53 gap supplies a necessary interface-pricing check; scalar coupling rank is not an admitted recursive child rank.", + "budget_minutes": 60, + "stop_rule": "Stop after the first exact asymmetric gap, its all-workspace cut proof and one attaining full endpoint. Leave general asymmetric optimization and physical realization open.", + "outcome": "completed", + "evidence": "Written all-workspace proof of exact minimum 54 versus separate lower bill 53; 3840 interval identities, 36 full endpoint fixtures, 1296 faithful regular basis columns and 35 semantic/deletion controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What exact compatibility criterion lets two arbitrary monotone letter tariffs attain both independent partition minima?", + "why_it_matters": "The explicit 53 lower bill is unattainable, so separate dynamic programs do not suffice for asymmetric interfaces.", + "first_step": "Classify feasible a-rank partitions when exactly two b calls are optimal, using the inside/outside full-rank cut.", + "blocked_by": "The cut is only a necessary condition for general noncommuting words." + }, + { + "question": "Can a native UT3 block interface realize an asymmetric complete price with a useful recursive gain?", + "why_it_matters": "A formal price gap does not change the selected multiplication bound.", + "first_step": "Specify one literal producer and consumer, then charge preparation, scalar mixing, frames, restoration, hosting and precision.", + "blocked_by": "No physical realization or identification of scalar coupling rank with recursive child rank is supplied." + } + ], + "claim_type": "scoped algebraic proof", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19213517", + "upstream_checked_at": "2026-10-27T09:04:32Z" +} diff --git a/research/ut3-asymmetric-monotone-gap/VERIFY.json b/research/ut3-asymmetric-monotone-gap/VERIFY.json new file mode 100644 index 0000000000..ea18c0de06 --- /dev/null +++ b/research/ut3-asymmetric-monotone-gap/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 price duals and equality cases, all two-role cut identities, full dirty endpoints, separate faithful regular action, source-bound receipt and rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact price duals and equality cases, all two-role cut identities, full dirty endpoints, separate faithful regular action, source-bound receipt and rejection controls." + } + ] +} diff --git a/research/ut3-asymmetric-monotone-gap/verify.py b/research/ut3-asymmetric-monotone-gap/verify.py new file mode 100644 index 0000000000..a9fdc984f8 --- /dev/null +++ b/research/ut3-asymmetric-monotone-gap/verify.py @@ -0,0 +1,288 @@ +#!/usr/bin/env python3 +"""Exact corroboration of the asymmetric UT3 tariff gap. Apache-2.0.""" + +import hashlib +import itertools +import json +from pathlib import Path +import sys + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def identity(r): + require(1 <= r <= 6, "matrix dimension outside 1..6") + return tuple(1 << i for i in range(r)) + + +def add(a, b): + return tuple(x ^ y for x, y in zip(a, b, strict=True)) + + +def multiply(a, b): + r = len(a) + require(len(b) == r and 1 <= r <= 6, "matrix shape") + rows = [] + for row in a: + out = 0 + for j in range(r): + if row >> j & 1: + out ^= b[j] + rows.append(out) + return tuple(rows) + + +def rank(a): + rows = list(a) + r = len(rows) + pivots = 0 + for j in range(r): + candidates = [i for i in range(pivots, r) if rows[i] >> j & 1] + if candidates: + i = candidates[0] + rows[pivots], rows[i] = rows[i], rows[pivots] + for h in range(pivots + 1, r): + if rows[h] >> j & 1: + rows[h] ^= rows[pivots] + pivots += 1 + return pivots + + +def group_product(g, h): + x, y, z = g & 1, g >> 1 & 1, g >> 2 & 1 + u, v, w = h & 1, h >> 1 & 1, h >> 2 & 1 + return (x ^ u) | ((y ^ v) << 1) | ((z ^ w ^ (x & v)) << 2) + + +def literal_product(g, h): + a = ((1, g & 1, g >> 2 & 1), (0, 1, g >> 1 & 1), (0, 0, 1)) + b = ((1, h & 1, h >> 2 & 1), (0, 1, h >> 1 & 1), (0, 0, 1)) + c = [[sum(a[i][k] * b[k][j] for k in range(3)) % 2 + for j in range(3)] for i in range(3)] + return c[0][1] | (c[1][2] << 1) | (c[0][2] << 2) + + +def algebra_product(a, b): + out = 0 + for g in range(8): + if a >> g & 1: + for h in range(8): + if b >> h & 1: + out ^= 1 << group_product(g, h) + return out + + +def formal_identity(r): + return tuple(tuple(int(i == j) for j in range(r)) for i in range(r)) + + +def formal_word(word, r): + require(0 <= len(word) <= 16, "word bound") + op = formal_identity(r) + for g, n in word: + require(g in (1, 2) and len(n) == r, "illegal call") + require(all(0 <= row < 1 << r for row in n), "nonbinary matrix") + factor = tuple(tuple(int(i == j) ^ (((1 << g) ^ 1) if n[i] >> j & 1 else 0) + for j in range(r)) for i in range(r)) + nxt = [] + for i in range(r): + row = [] + for j in range(r): + entry = 0 + for k in range(r): + entry ^= algebra_product(op[i][k], factor[k][j]) + row.append(entry) + nxt.append(tuple(row)) + op = tuple(nxt) + return op + + +def shadow(op, coefficient): + require(coefficient in range(4), "unknown coefficient") + rows = [] + for row in op: + out = 0 + for j, cell in enumerate(row): + parity = 0 + for g in range(8): + x, y, z = g & 1, g >> 1 & 1, g >> 2 & 1 + value = (x, y, z, z ^ (x & y))[coefficient] + parity ^= (cell >> g & 1) & value + out |= parity << j + rows.append(out) + return tuple(rows) + + +def expected(r, w=3): + return tuple(tuple((1 << 4 if i < w else 1) if i == j else 0 + for j in range(r)) for i in range(r)) + + +def literal_check(word, op, r): + columns = 0 + for source in range(r): + for address in range(8): + payload = [0] * r + payload[source] = 1 << address + for g, n in reversed(word): + delta = [0] * r + for i in range(r): + for j in range(r): + if n[i] >> j & 1: + for h in range(8): + if payload[j] >> h & 1: + delta[i] ^= (1 << h) ^ (1 << literal_product(g, h)) + payload = [x ^ y for x, y in zip(payload, delta, strict=True)] + want = [] + for i in range(r): + cell = 0 + for g in range(8): + if op[i][source] >> g & 1: + cell ^= 1 << literal_product(g, address) + want.append(cell) + require(payload == want, "literal regular action disagrees") + columns += 1 + return columns + + +def price_checks(): + a, b = (0, 6, 9, 14), (0, 11, 12, 13) + require(all(2 * a[d] >= 9 * d for d in range(1, 4)), "a dual") + require(all(3 * b[d] >= 13 * d for d in range(1, 4)), "b dual") + require([d for d in range(1, 4) if 2 * a[d] == 9 * d] == [2], "a equality") + require([d for d in range(1, 4) if 3 * b[d] == 13 * d] == [3], "b equality") + lists = [] + for counts in itertools.product(range(7), repeat=3): + if sum(d * counts[d - 1] for d in range(1, 4)) == 6: + lists.append(counts) + costs = [[sum(table[d] * c[d - 1] for d in range(1, 4)) for c in lists] + for table in (a, b)] + require(min(costs[0]) == 27 and min(costs[1]) == 26, "separate optima") + orders = list(itertools.combinations(range(5), 2)) + for left, right in orders: + inside = right - left - 1 + require(2 * inside < 3 or 2 * (3 - inside) < 3, "cut exclusion") + return {"a_prices": a, "b_prices": b, "separate_minimum": 53, + "full_minimum": 54, "partitions": len(lists), "letter_orders": len(orders)} + + +def cut_checks(): + matrices = list(itertools.product(range(4), repeat=2)) + zero = (0, 0) + cases = 0 + full_targets = 0 + for n in matrices[1:]: + for left in matrices: + for middle in matrices: + right = add(left, middle) + word = [(1, left), (2, n), (1, middle), (2, n), (1, right)] + op = formal_word(word, 2) + require(shadow(op, 0) == zero and shadow(op, 1) == zero, "linear closure") + require(shadow(op, 2) == multiply(middle, n), "XY interval") + require(shadow(op, 3) == multiply(n, middle), "YX interval") + if op == expected(2, 2): + require(rank(middle) >= 2 and rank(add(left, right)) >= 2, + "full target violates cut") + full_targets += 1 + cases += 1 + require(cases == 3840 and full_targets > 0, "cut coverage") + return {"cut_cases": cases, "full_two_target_cases": full_targets} + + +def witness_checks(): + fixtures = 0 + columns = 0 + controls = 0 + for r in range(3, 7): + q = tuple(1 << i if i < 3 else 0 for i in range(r)) + for letters in ((1, 2, 1, 2), (2, 1, 2, 1)): + word = [(g, q) for g in letters] + op = formal_word(word, r) + require(op == expected(r), "optimal full endpoint") + require(sum((5 + rank(n) ** 2 if g == 1 else 10 + rank(n)) + for g, n in word) == 54, "attaining bill") + columns += literal_check(word, op, r) + fixtures += 1 + for deleted in range(4): + require(formal_word(word[:deleted] + word[deleted + 1:], r) != expected(r), + "deleted paid call accepted") + controls += 1 + frames = [identity(r)] + for i, j in itertools.permutations(range(3), 2): + s = list(identity(r)) + s[i] ^= 1 << j + frames.append(tuple(s)) + for s in frames: + word = [] + for omitted in range(3): + p = tuple(1 << i if i < 3 and i != omitted else 0 for i in range(r)) + n = multiply(multiply(s, p), s) + require(rank(n) == 2, "comparison rank") + word.extend(((1, n), (2, n))) + op = formal_word(word, r) + require(op == expected(r), "conjugated comparison endpoint") + columns += literal_check(word, op, r) + fixtures += 1 + return {"endpoint_fixtures": fixtures, "regular_basis_columns": columns, + "deleted_call_controls": controls} + + +def semantic_controls(): + q = (1, 2, 4, 0) + word = [(g, q) for g in (1, 2, 1, 2)] + bad = word + [(1, (0, 0, 0, 8))] + require(formal_word(bad, 4) != expected(4), "dirty spectator accepted") + base = formal_word(word, 4) + kernel = [] + for cell in range(1, 256): + op = ((cell,),) + if all(shadow(op, i) == (0,) for i in range(4)) and cell.bit_count() % 2 == 0: + kernel.append(cell) + require(kernel, "missing shadow kernel control") + mutant = [list(row) for row in base] + mutant[3][3] ^= kernel[0] + mutant = tuple(tuple(row) for row in mutant) + require(mutant != base and all(shadow(mutant, i) == shadow(base, i) for i in range(4)), + "quotient-only endpoint control") + a, b = (2, 0), (0, 1) + require(multiply(a, b) != multiply(b, a), "noncommuting matrix fixture") + op = formal_word([(1, a), (2, b), (1, a)], 2) + require(shadow(op, 1) != (0, 0), "unrestored first-order control") + return {"semantic_controls": 3, "shadow_kernel_masks": len(kernel)} + + +def source_hashes(): + package = Path(__file__).resolve().parent + hashes = {} + for name in ("README.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py"): + with (package / name).open("rb") as stream: + data = stream.read(131073) + require(len(data) <= 131072, "source file size bound") + hashes[name] = hashlib.sha256(data).hexdigest() + return hashes + + +def main(): + require(sys.argv[1:] in ([], ["--emit"]), "usage: verify.py [--emit]") + require(all(group_product(g, h) == literal_product(g, h) + for g in range(8) for h in range(8)), "literal group law") + report = {"schema_version": 1, "claim_type": "scoped algebraic proof", + "no_new_kappa": True, "prices": price_checks(), **cut_checks(), + **witness_checks(), **semantic_controls(), "source_sha256": source_hashes()} + if sys.argv[1:] == ["--emit"]: + print(json.dumps(report, indent=2, sort_keys=True)) + else: + path = Path(__file__).resolve().parent / "RESULT.json" + with path.open("rb") as stream: + raw = stream.read(131073) + require(len(raw) <= 131072, "receipt size bound") + require(json.loads(raw) == json.loads(json.dumps(report)), "receipt differs from replay") + print("PASS_UT3_ASYMMETRIC_MONOTONE_GAP separate=53 exact=54 no_new_kappa") + print(json.dumps(report, sort_keys=True)) + + +if __name__ == "__main__": + main()