From 9f4bf9b3dc7b93d5c5c57c8c4a2d2f2c6b030b0a Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 23 Oct 2026 00:45:41 +0100 Subject: [PATCH] feat(research): prove signed monotone unitriangular tariffs --- research/ut-signed-monotone-tariff/README.md | 218 ++++++++++++ .../ut-signed-monotone-tariff/SOURCES.json | 42 +++ research/ut-signed-monotone-tariff/TASK.json | 93 +++++ .../ut-signed-monotone-tariff/VERIFY.json | 34 ++ research/ut-signed-monotone-tariff/verify.py | 325 ++++++++++++++++++ 5 files changed, 712 insertions(+) create mode 100644 research/ut-signed-monotone-tariff/README.md create mode 100644 research/ut-signed-monotone-tariff/SOURCES.json create mode 100644 research/ut-signed-monotone-tariff/TASK.json create mode 100644 research/ut-signed-monotone-tariff/VERIFY.json create mode 100644 research/ut-signed-monotone-tariff/verify.py diff --git a/research/ut-signed-monotone-tariff/README.md b/research/ut-signed-monotone-tariff/README.md new file mode 100644 index 0000000000..4ad9270f73 --- /dev/null +++ b/research/ut-signed-monotone-tariff/README.md @@ -0,0 +1,218 @@ +# Exact signed monotone unitriangular call prices + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Scoped written proof with exact finite corroboration; no new kappa.** +In the full formal algebra `F2[UT_d(Z)]`, signed simple-root calls cannot +share their cost across diagonal outputs that admit sign-consistent words. +The theorem holds for every `d >= 2`, every finite number of targets and +every finite number of restored arbitrary dirty workspace roles. Free scalar +mixing is allowed. The exact minimum at arbitrary positive sign-dependent +prices is the sum of the individual positive and negative root counts below. + +For example, put `h = g1^m g2^-n`, with `m,n > 0` and `d >= 3`. The endpoint +`diag([h],[h^-1],1,...)` costs exactly `2(m+n)` unit-price calls. Every +first-superdiagonal determinant character of this endpoint is one, yet both +opposite signs have separate unavoidable bills. The price is +`m(alpha1+ + alpha1-) + n(alpha2+ + alpha2-)`. This inverse-pair family is +a new test case, not a recheck of either predecessor UT5 endpoint. + +## Model and theorem + +Let `G = UT_d(Z)` and `g_i = I + E_(i,i+1)`, for `1 <= i < d`. There are +`R >= W` roles. Paid calls are exactly + +```text +D_N(g_i^epsilon) = I_R + ([g_i^epsilon] + [1]) N, +epsilon in {+1,-1}, N = x y^T over F2, y^T x = 1. +``` + +Thus `N` is any binary rank-one idempotent. Its price is `alpha_i^epsilon > 0`. +Arbitrary `GL_R(F2)` transformations may be interleaved at zero cost in this +optimistic relaxation. No other address operation, erasure or clean workspace +is supplied. The endpoint must equal + +```text +T = diag([h_1],...,[h_W],[1],...,[1]) in Mat_R(F2[G]). +``` + +All target and workspace data start arbitrary. Formal equality requires every +workspace input to return unchanged, with no residual target coupling. The +integer address matrices are not reduced modulo two. + +Write `a_ji = (h_j)_(i,i+1)`. For **every** endpoint, every realizing program +has the separate bounds + +```text +n_i+ >= P_i = sum_j max(a_ji,0), +n_i- >= M_i = sum_j max(-a_ji,0). +``` + +Call a supplied simple-root word sign-consistent when each root `g_i` occurs +with at most one sign within that word. Signs may differ between targets. +If each `h_j` has such a word, both bounds are attained simultaneously. +Consequently its exact optimal price is + +```text +sum_i (alpha_i+ P_i + alpha_i- M_i). +``` + +The theorem permits arbitrary interleavings of root letters within each +supplied word, including noncommuting letters. Ordered products +`g_1^a1 ... g_(d-1)^a(d-1)` are one explicit subfamily. The existence of a +sign-consistent word is a hypothesis, not a decision procedure supplied here. + +## Written proof + +**1. Character projections.** For each `i`, the map +`chi_i(h) = h_(i,i+1)` is a group homomorphism from `UT_d(Z)` to `Z`. +Indeed the first-superdiagonal entry of a product is the sum of those entries; +there is no intermediate integer index strictly between `i` and `i+1`. +It sends `g_i^epsilon` to `epsilon` and every other simple-root letter to zero. +Therefore `[h] -> t^chi_i(h)` induces a ring homomorphism to +`L = F2[t,t^-1]`. Formal equality implies projected equality. No converse is +needed or asserted. + +**2. The inherited all-minor degree.** For a square Laurent matrix `A`, let +`delta(A)` be the largest degree of any nonzero square minor, over all sizes, +including the empty minor one. It is nonnegative. Cauchy--Binet gives +`delta(AB) <= delta(A) + delta(B)`: each minor is a sum of products of +equal-sized minors, and cancellation cannot increase degree. Every invertible +constant matrix and its inverse have degree zero. Applying this inequality +in both directions shows that constant invertible left or right factors +preserve `delta`. This is Adam Gall's #1911 method, also used and extended +by ywz65 in #2716; the invariant and this argument are not claimed as new. + +**3. Separate sign bills.** Since `N` is an idempotent of rank one, +`F2^R = im(N) direct-sum ker(N)`. A constant change of scalar basis puts `N` +in the form `diag(1,0,...)`. Under the `i`-th projection a call of root `i` +is therefore constant-similar to `diag(t^epsilon,1,...)`. Its `delta` is one +for `epsilon=+1` and zero for `epsilon=-1`. Calls of all other roots project +to the identity. Every free scalar transformation has `delta=0`. +Subadditivity through the entire actual word consequently bounds the endpoint +degree by `n_i+`. Replacing `t` by `t^-1` gives the separate bound by `n_i-`. +This includes every paid restoration call and every free mixing operation. + +**4. Endpoint evaluation.** The projected endpoint is diagonal with entries +`t^a_ji` and spectator entries one. Each nonzero minor of a diagonal matrix +selects a subset of its diagonal entries. Selecting precisely the positive +exponents proves `delta(T_i) = P_i`. The inverted-variable projection gives +`delta(T_i(t^-1)) = M_i`. Spectator entries contribute zero for every `R-W`. +Steps 3 and 4 prove all the separate lower bounds, without a workspace bound +and without any assumption that a target word is sign-consistent. + +**5. Attainment.** For a coordinate projector `E_j`, multiplication in the +full group algebra gives `D_Ej(g) D_Ej(h) = D_Ej(gh)`. Distinct coordinate +projectors act independently. Put the supplied word for `h_j` on role `j`. +Its signed root counts are exactly `max(a_ji,0)` and `max(-a_ji,0)` because +sign consistency forbids cancellation in `chi_i`. This realizes the complete +formal endpoint with the two bounds attained together. It uses no workspace +or scalar mixing. With left matrix actions, execute a displayed product's +letters from right to left. Positive prices now give the exact price formula. + +For the inverse-pair example, the two words are `g1^m g2^-n` and +`g2^n g1^-m`. Each is sign-consistent. Their aggregate characters cancel, +while the theorem requires `m` calls of each sign of root 1 and `n` of each +sign of root 2. This completes the example and the theorem. + +## What changes for the next search + +Cinna Davis's [#2103](https://github.com/CrocSwap/integer-mult-bounds/pull/2103) +and [#3316](https://github.com/CrocSwap/integer-mult-bounds/pull/3316) ask about +sharing calls among other diagonal UT5 targets and give target-specific +formal obstructions. The new theorem closes the sign-consistent family at +every dimension and workspace size, with heterogeneous positive prices. +A search for a saving in this alphabet must leave that family, for example +by using targets with genuine root-sign reversals. We do not replay either +predecessor census or claim their target-specific conclusions as new. + +The scalar-idempotent formal model retains the predecessor lineage of eumemic +#288 and Ali Romman #468. The proof method is credited to Adam Gall's +[#1911](https://github.com/CrocSwap/integer-mult-bounds/pull/1911) and ywz65's +[#2716](https://github.com/CrocSwap/integer-mult-bounds/pull/2716). Their +dihedral representations and tariffs are different from these integer +unitriangular character projections. Exact source bytes are pinned as +provenance in `SOURCES.json`; no predecessor executable is imported or run. +No claim of priority outside the repository is made. + +## Reproduce and evidence + +From the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/ut-signed-monotone-tariff/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/ut-signed-monotone-tariff/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/ut-signed-monotone-tariff +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/ut-signed-monotone-tariff --check-source-history +``` + +The absolute interpreter path is the original environment's CPython 3.12.15; +another CPython 3.12 installation can replace that path. Only the standard +library is needed. Expected final lines are `PASS_UT_SIGNED_MONOTONE_TARIFF`, +`PASS_REGISTERED_RESEARCH_PACKAGE` and the committed-byte/source-history pass. +The registered normal and optimized commands are separately time-bounded. + +The verifier constructs integer unitriangular products and full formal binary +coefficient matrices. It computes Laurent minors by Leibniz expansion, +separately from the written Cauchy--Binet proof. The generated report enumerates +all replay counts. It also compares formal products to a separately implemented +literal action on vectors modulo three, including every arbitrary-dirty basis +input of each sampled three-role word. That finite action corroborates the +implementation; quotient equality does not prove a formal lower bound. +The universal conclusion rests on the written proof, not finite sampling. + +Default replay writes nothing. The JSON report binds all five package files +by SHA256. Optional `--receipt /absolute/path/outside/checkout.json` creates a +fresh report and refuses an occupied path or an output inside the checkout. +There is no hand-written or committed execution receipt. + +## Limits and remaining obligations + +This is an exact paid-call result in a formal model, not a finite certificate +for a supplier or a complete multiplication theorem. The lower bounds hold +for arbitrary targets, but sharpness requires sign-consistent supplied words. +A nonidentity central commutator has every `P_i=M_i=0`, so the character +bounds do not determine arbitrary-target costs. The verifier retains that +boundary control, a noncommuting-order control, a determinant-cancellation +control, and single-call omissions of the inverse-pair constructions. + +The signed simple-root alphabet and full formal equality are essential. +Direct higher-root calls, arbitrary address maps, clean state, finite cyclic +quotient shortcuts and changed coupling alphabets are outside the theorem. +The formal attaining word has `W` dirty targets, no scratch, no free mixing +and exactly the stated paid counts. Native frames, physical XOR cost, +hosting, precision, tape movement, recursive pricing and supplier admission +are unknown. No selected construction, selected record or frozen source is +changed. Independent human and formal proof-kernel review are unclaimed. + +## Open next questions + +1. Which diagonal integer-unitriangular targets with genuine root-sign + reversals admit a saving beyond the character lower bound? This is the + first family this theorem does not exclude. Start with one explicitly + nonmonotone endpoint and a bounded exact alphabet. Higher-root information + is the missing ingredient; a zero character bill is not a construction. +2. Can one signed simple-root formal call be assigned an actual native + supplier interface and complete price? Start with its dirty-state and frame + contract and charge every scalar conversion and physical traversal. + No such bridge is supplied here, so this result alone gives no kappa gain. + +## Replay engineering + +The verifier has no recursion, dynamic code execution, subprocesses or imported +predecessor code. Group dimensions are at most six, role dimensions at most +four, the exhaustive mixed-word length is three, and literal actions use +exactly 27 addresses and three roles. The remaining fixtures have fixed loop +bounds and deterministic seeds. All functions are below 60 physical lines. +Admission checks use explicit exceptions and remain enabled under `-O`. + +Power-of-Ten rule 3 deviation: CPython allocates integers, tuples and sparse +dictionaries during arithmetic. Fixed replay dimensions, word lengths and +formal-support guards bound live data; the program is a terminating check, +not a steady service. Verification includes the complete bounded replay. +A fixed-storage implementation is a follow-up only if these bounds expand. +Rule 10 deviation: there is no compiler or configured static type checker for +this standalone standard-library package. Every registered command enables +warning errors; normal and optimized execution and explicit AST inspection +check the actual artifact. Add repository-standard static analysis if one is +adopted for these packages. These deviations make no real-time guarantee. diff --git a/research/ut-signed-monotone-tariff/SOURCES.json b/research/ut-signed-monotone-tariff/SOURCES.json new file mode 100644 index 0000000000..fac49ffa80 --- /dev/null +++ b/research/ut-signed-monotone-tariff/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/ut5-four-role-mixed-root-seede2a8/README.md", + "usage": "provenance", + "git_blob": "e2686861d72a6677204653c1fdce7762f84257b9", + "sha256": "9a8f88268f9f438abbcdac5730cab7a24eec4ea204c43312b4b7c374d1af34b0" + }, + { + "path": "research/ut5-repeated-root-height-two-20261017/README.md", + "usage": "provenance", + "git_blob": "d1c3a2cf7619e05e8fbf4e6560da1995a5e08ea2", + "sha256": "8e30cd107c46563eee0387c7328ffa519a0a588027268f47a668c518e31d577d" + }, + { + "path": "research/infinite-dihedral-register-bound/README.md", + "usage": "provenance", + "git_blob": "531ddbd1641554cbe5e84a9aec7b695353bb9cbe", + "sha256": "16a97e08710201f33c756c22de54a5073e92fe3053a795151760af456459502c" + }, + { + "path": "research/dihedral-arbitrary-couplings/README.md", + "usage": "provenance", + "git_blob": "66027d2a8856d931e7b1c8fa9811a65196d01637", + "sha256": "17bc49fd6215c155aacb0e4a8ce4a8e33e83226b8a1b937a638256a39b99f8ee" + } + ] +} diff --git a/research/ut-signed-monotone-tariff/TASK.json b/research/ut-signed-monotone-tariff/TASK.json new file mode 100644 index 0000000000..72a865f0e3 --- /dev/null +++ b/research/ut-signed-monotone-tariff/TASK.json @@ -0,0 +1,93 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "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": "refined", + "actual_scope": "Exact separate signed-simple-root call counts and positive-price optima for every sign-consistent diagonal target tuple in F2[UT_d(Z)], with arbitrary finite restored dirty workspace and free binary scalar mixing.", + "scope_change_reason": "The card permits a specified nonabelian operation family. This result changes the additive rational-frame model to integer unitriangular simple roots and establishes a uniform obstruction rather than a supplier or a new census.", + "bottleneck_link": "Closes the sign-consistent diagonal family to paid-call sharing in this formal alphabet. A supplier search must change that target premise or the alphabet; no native or recursive transfer is established.", + "budget_minutes": 60, + "stop_rule": "Stop at the first exact uniform tariff and its finite corroboration; do not extend to root-sign-reversing targets.", + "outcome": "completed", + "evidence": "README written proof and source-bound JSON generated by verify.py; normal and optimized registered finite replays.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Which diagonal integer-unitriangular targets with genuine root-sign reversals admit a saving beyond the character bound?", + "why_it_matters": "This is the first target premise outside the proved no-sharing family.", + "first_step": "Fix one nonmonotone endpoint, state a complete finite alphabet and seek higher-root information before a bounded search.", + "blocked_by": "The first-superdiagonal projections erase central commutators." + }, + { + "question": "Can one signed simple-root formal call be implemented under a native supplier contract?", + "why_it_matters": "A formal paid-call tariff alone does not price a recursive child.", + "first_step": "Specify dirty inputs, output frames and restoration, then charge scalar conversions and tape traversals.", + "blocked_by": "No native hosting, precision, recursive pricing or all-size compiler bridge is established." + } + ], + "environment": { + "python": "3.12.15", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "interpreter": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12" + }, + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19134600", + "claim_type": "scoped written proof with exact finite corroboration", + "selection": { + "seed": "9e6eeb3acfe46c3180caad0b87ca85ee", + "track": "bit-mechanisms", + "priority_revision": 7, + "baseline": "scripts/research_selected_baseline.py: PASS_RESEARCH_BASELINE_BINDINGS_ONLY; current guidance replaces historical card command", + "upstream": "624de9dc66858af0945e5f8a0942488d62280d43" + }, + "overlap": { + "checked_at": "2026-10-22T23:39:13Z", + "open_prs": 429, + "discussions": 3966, + "remote_pagination": "complete snapshots, not atomic", + "local_notes_searched": 119, + "local_note_inventory": 6319, + "local_scope": "Sparse local notes incomplete; supplemented by git grep over main READMEs, live merged searches and relevant full PR bodies. No code-diff novelty guarantee." + } +} diff --git a/research/ut-signed-monotone-tariff/VERIFY.json b/research/ut-signed-monotone-tariff/VERIFY.json new file mode 100644 index 0000000000..c908362b00 --- /dev/null +++ b/research/ut-signed-monotone-tariff/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": "All bounded formal, Laurent-minor, free-mixing, sign-consistent endpoint, literal dirty-state and boundary controls; source-bound report." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The identical complete finite corroboration with assertions disabled; admission uses explicit exceptions." + } + ] +} diff --git a/research/ut-signed-monotone-tariff/verify.py b/research/ut-signed-monotone-tariff/verify.py new file mode 100644 index 0000000000..84bd62fbf0 --- /dev/null +++ b/research/ut-signed-monotone-tariff/verify.py @@ -0,0 +1,325 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the written signed monotone UT tariff.""" +from __future__ import annotations + +import argparse +import hashlib +import itertools as it +import json +from pathlib import Path +import random + +Poly = frozenset[int] +Group = tuple[tuple[int, ...], ...] +Formal = dict[Group, int] +ZERO: Poly = frozenset() +ONE: Poly = frozenset({0}) + + +def need(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def identity(d: int) -> Group: + need(type(d) is int and 2 <= d <= 6, "dimension outside replay bound") + return tuple(tuple(int(i == j) for j in range(d)) for i in range(d)) + + +def group_mul(a: Group, b: Group) -> Group: + d = len(a) + need(len(b) == d, "group dimensions differ") + return tuple(tuple(sum(a[i][k] * b[k][j] for k in range(d)) + for j in range(d)) for i in range(d)) + + +def root(d: int, label: int, sign: int) -> Group: + a = [list(row) for row in identity(d)] + need(0 <= label < d - 1 and sign in (-1, 1), "invalid root letter") + a[label][label + 1] = sign + return tuple(tuple(row) for row in a) + + +def binary_identity(r: int) -> int: + need(type(r) is int and 1 <= r <= 4, "roles outside replay bound") + return sum(1 << (i * r + i) for i in range(r)) + + +def binary_mul(a: int, b: int, r: int) -> int: + out = 0 + for i, j in it.product(range(r), repeat=2): + value = sum(((a >> (i * r + k)) & 1) * + ((b >> (k * r + j)) & 1) for k in range(r)) & 1 + out |= value << (i * r + j) + return out + + +def projectors(r: int) -> tuple[tuple[int, int, int], ...]: + binary_identity(r) + out = [] + for x, y in it.product(range(1, 1 << r), repeat=2): + if (x & y).bit_count() % 2: + n = sum(1 << (i * r + j) for i, j in it.product(range(r), repeat=2) + if (x >> i) & (y >> j) & 1) + need(binary_mul(n, n, r) == n, "projector is not idempotent") + out.append((x, y, n)) + return tuple(out) + + +def formal_gate(g: Group, n: int, r: int) -> Formal: + e = identity(len(g)) + need(g != e, "identity is not a paid root") + return {g: n, e: binary_identity(r) ^ n} + + +def formal_mul(a: Formal, b: Formal, r: int) -> Formal: + need(len(a) <= 4096 and len(b) <= 4096, "formal support limit") + out: Formal = {} + for ga, ma in a.items(): + for gb, mb in b.items(): + coefficient = binary_mul(ma, mb, r) + if coefficient: + g = group_mul(ga, gb) + out[g] = out.get(g, 0) ^ coefficient + return {g: m for g, m in out.items() if m} + + +def poly_mul(a: Poly, b: Poly) -> Poly: + out: set[int] = set() + for x, y in it.product(a, b): + out.symmetric_difference_update({x + y}) + return frozenset(out) + + +def projection(a: Formal, r: int, label: int, sign: int = 1): + out = [[set() for _ in range(r)] for _ in range(r)] + for g, matrix in a.items(): + exponent = sign * g[label][label + 1] + for i, j in it.product(range(r), repeat=2): + if (matrix >> (i * r + j)) & 1: + out[i][j].symmetric_difference_update({exponent}) + return tuple(tuple(frozenset(p) for p in row) for row in out) + + +def delta(a) -> int: + """Leibniz determinants of every square minor, including the empty one.""" + r = len(a) + need(1 <= r <= 4, "minor dimension outside replay bound") + answer = 0 + for k in range(1, r + 1): + for rows, columns in it.product(it.combinations(range(r), k), repeat=2): + determinant = ZERO + for order in it.permutations(columns): + term = ONE + for i, j in zip(rows, order): + term = poly_mul(term, a[i][j]) + determinant = determinant.symmetric_difference(term) + if determinant: + answer = max(answer, max(determinant)) + return answer + + +def gate_checks() -> dict[str, int]: + count = total = 0 + for r in range(1, 5): + for _, _, n in projectors(r): + total += 1 + for sign in (-1, 1): + a = formal_gate(root(2, 0, sign), n, r) + need(delta(projection(a, r, 0)) == int(sign == 1), "positive gate degree") + need(delta(projection(a, r, 0, -1)) == int(sign == -1), "negative gate degree") + count += 1 + need(total == 155, "projector inventory") + return {"projectors": total, "signed_gate_checks": count} + + +def mixed_checks() -> dict[str, int]: + alphabet = [(label, sign, formal_gate(root(3, label, sign), n, 2)) + for label, sign in it.product(range(2), (-1, 1)) + for _, _, n in projectors(2)] + words = degree_checks = 0 + for letters in it.product(alphabet, repeat=3): + a = {identity(3): binary_identity(2)} + for _, _, gate in letters: + a = formal_mul(a, gate, 2) + for label, sign in it.product(range(2), (-1, 1)): + bill = sum(q == label and s == sign for q, s, _ in letters) + need(delta(projection(a, 2, label, sign)) <= bill, "mixed word exceeds bill") + degree_checks += 1 + words += 1 + need(words == 24 ** 3, "incomplete three-letter domain") + return {"mixed_three_call_words": words, "mixed_degree_checks": degree_checks} + + +def free_mixing_checks() -> dict[str, int]: + e = identity(2) + gl2 = (1 | 8, 2 | 4, 1 | 2 | 8, 1 | 4 | 8, 1 | 2 | 4, 2 | 4 | 8) + checks = 0 + for _, _, n in projectors(2): + gate = formal_gate(root(2, 0, 1), n, 2) + for left, right in it.product(gl2, repeat=2): + a = formal_mul(formal_mul({e: left}, gate, 2), {e: right}, 2) + for sign in (-1, 1): + need(delta(projection(a, 2, 0, sign)) == int(sign == 1), "free mixing changes degree") + checks += 1 + return {"free_mixing_checks": checks} + + +def endpoint(words, d: int, r: int) -> Formal: + out: Formal = {} + for role in range(r): + g = identity(d) + if role < len(words): + for label, sign in words[role]: + g = group_mul(g, root(d, label, sign)) + out[g] = out.get(g, 0) ^ (1 << (role * r + role)) + return out + + +def witness(words, d: int, r: int, omit: int = -1) -> Formal: + a = {identity(d): binary_identity(r)} + index = 0 + for role, word in enumerate(words): + for label, sign in word: + if index != omit: + gate = formal_gate(root(d, label, sign), 1 << (role * r + role), r) + a = formal_mul(a, gate, r) + index += 1 + return a + + +def monotone_checks() -> dict[str, int]: + rng = random.Random(21163316) + targets = omissions = 0 + for d, m, n, spectators in it.product(range(3, 6), range(1, 4), range(1, 4), range(3)): + a = [(0, 1)] * m + [(1, -1)] * n + b = [(1, 1)] * n + [(0, -1)] * m + words, r = [a, b], 2 + spectators + target = endpoint(words, d, r) + need(witness(words, d, r) == target, "inverse-pair formal endpoint") + ga = next(iter(endpoint([a], d, 1))) + gb = next(iter(endpoint([b], d, 1))) + need(all(ga[label][label + 1] + gb[label][label + 1] == 0 for label in range(2)), + "aggregate character should cancel") + for index in range(2 * (m + n)): + need(witness(words, d, r, index) != target, "omitted paid factor accepted") + omissions += 1 + targets += 1 + for d, r, _ in it.product(range(2, 7), range(1, 5), range(10)): + words = [] + for _role in range(r): + word = [(label, rng.choice((-1, 1)), rng.randrange(3)) for label in range(d - 1)] + letters = [(label, sign) for label, sign, count in word for _ in range(count)] + rng.shuffle(letters) + words.append(letters) + target = endpoint(words, d, r) + need(witness(words, d, r) == target, "monotone formal endpoint") + for label, sign in it.product(range(d - 1), (-1, 1)): + bill = sum(q == label and s == sign for word in words for q, s in word) + need(delta(projection(target, r, label, sign)) == bill, "endpoint tariff not sharp") + targets += 1 + return {"monotone_target_fixtures": targets, "single_omission_controls": omissions} + + +def permute_bits(value: int, g: Group, q: int) -> int: + d = len(g) + size = q ** d + need(d == 3 and q == 3 and 0 <= value < (1 << size), "literal action outside bound") + out = 0 + for index, v in enumerate(it.product(range(q), repeat=d)): + if (value >> index) & 1: + w = tuple(sum(g[i][j] * v[j] for j in range(d)) % q for i in range(d)) + target = sum(w[i] * q ** (d - i - 1) for i in range(d)) + out ^= 1 << target + return out + + +def literal_gate(state, g: Group, x: int, y: int): + total = 0 + for i, value in enumerate(state): + if (y >> i) & 1: + total ^= value + change = permute_bits(total, g, 3) ^ total + return tuple(value ^ (change if (x >> i) & 1 else 0) for i, value in enumerate(state)) + + +def formal_action(a: Formal, state): + r = len(state) + out = [0] * r + for g, matrix in a.items(): + for i, j in it.product(range(r), repeat=2): + if (matrix >> (i * r + j)) & 1: + out[i] ^= permute_bits(state[j], g, 3) + return tuple(out) + + +def literal_checks() -> dict[str, int]: + rng = random.Random(19112716) + ps = projectors(3) + basis = samples = 0 + for _case in range(16): + letters = [(rng.randrange(2), rng.choice((-1, 1)), rng.choice(ps)) for _ in range(5)] + a = {identity(3): binary_identity(3)} + for label, sign, (_, _, n) in letters: + a = formal_mul(a, formal_gate(root(3, label, sign), n, 3), 3) + states = [tuple((1 << (j % 27)) if i == j // 27 else 0 for i in range(3)) + for j in range(81)] + states += [tuple(rng.getrandbits(27) for _ in range(3)) for _ in range(20)] + for state in states: + out = state + for label, sign, (x, y, _) in reversed(letters): + out = literal_gate(out, root(3, label, sign), x, y) + need(out == formal_action(a, state), "literal arbitrary-dirty action mismatch") + basis += 81 + samples += 20 + return {"literal_basis_inputs": basis, "literal_dirty_samples": samples} + + +def controls() -> dict[str, int]: + central = [(0, 1), (1, 1), (0, -1), (1, -1)] + a = endpoint([central], 3, 1) + need(a != {identity(3): 1}, "commutator control collapsed") + need(all(delta(projection(a, 1, label, sign)) == 0 + for label, sign in it.product(range(2), (-1, 1))), "central control should be invisible") + pair = [[(0, 1), (1, -1)], [(1, 1), (0, -1)]] + wrong = [[(0, 1), (1, -1)], [(0, -1), (1, 1)]] + need(endpoint(pair, 3, 2) != endpoint(wrong, 3, 2), "noncommuting order control") + need(delta(((frozenset({2}), ZERO), (ZERO, frozenset({-2})))) == 2, + "full determinant degree substituted for all-minor degree") + invalid = 0 + for d, label, sign in ((1, 0, 1), (7, 0, 1), (3, 2, 1), (3, -1, 1), (3, 0, 0)): + try: + root(d, label, sign) + except ValueError: + invalid += 1 + need(invalid == 5, "invalid root accepted") + return {"scope_and_order_controls": 3, "invalid_input_controls": invalid} + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--receipt", type=Path, help="write a new source-bound receipt outside the checkout") + args = parser.parse_args() + package = Path(__file__).resolve().parent + if args.receipt: + destination = args.receipt.resolve() + need(package.parent.parent not in destination.parents, "receipt must be outside checkout") + need(not destination.exists(), "receipt destination already exists") + result = {} + for part in (gate_checks(), mixed_checks(), free_mixing_checks(), monotone_checks(), + literal_checks(), controls()): + result.update(part) + files = ("README.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + report = {"claim_type": "scoped written proof with finite corroboration", "checks": result, + "source_sha256": {name: hashlib.sha256((package / name).read_bytes()).hexdigest() + for name in files}} + encoded = json.dumps(report, indent=2, sort_keys=True) + "\n" + if args.receipt: + with args.receipt.open("x", encoding="utf-8") as stream: + need(stream.write(encoded) == len(encoded), "incomplete receipt write") + print(encoded, end="") + print("PASS_UT_SIGNED_MONOTONE_TARIFF no_new_kappa") + + +if __name__ == "__main__": + main()