From d56d43c726dddc37a97a5dabf9d13ef861394133 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 20 Oct 2026 20:59:05 +0100 Subject: [PATCH] feat(research): classify signed connector tariffs by characteristic --- .../signed-characteristic-spectrum/README.md | 228 +++++++++++++++ .../RESULT.json | 25 ++ .../SOURCES.json | 42 +++ .../signed-characteristic-spectrum/TASK.json | 68 +++++ .../VERIFY.json | 37 +++ .../signed-characteristic-spectrum/verify.py | 263 ++++++++++++++++++ 6 files changed, 663 insertions(+) create mode 100644 research/signed-characteristic-spectrum/README.md create mode 100644 research/signed-characteristic-spectrum/RESULT.json create mode 100644 research/signed-characteristic-spectrum/SOURCES.json create mode 100644 research/signed-characteristic-spectrum/TASK.json create mode 100644 research/signed-characteristic-spectrum/VERIFY.json create mode 100644 research/signed-characteristic-spectrum/verify.py diff --git a/research/signed-characteristic-spectrum/README.md b/research/signed-characteristic-spectrum/README.md new file mode 100644 index 0000000000..436a3f525a --- /dev/null +++ b/research/signed-characteristic-spectrum/README.md @@ -0,0 +1,228 @@ +# Exact signed-connector tariffs over coefficient rings + +This is a scoped proof with a finite certificate. For the canonical signed +three-source connector below, the minimum is **12 calls in characteristic two, +13 in characteristic three, and 14 in characteristic zero or at least four**. +The statement covers every nonzero unital coefficient ring, including composite +characteristics and rings with zero divisors. It is uniform over finite free +modules, arbitrary fixed linear maps and arbitrary dirty data. + +The new result transfers the characteristic-zero obstruction to every +characteristic at least four and proves the exact fixed-price envelope there. +It also lifts the characteristic-three construction from F3 to every ring of +characteristic three. The predecessor words and obstruction remain credited. +There is no new kappa, supplier admission or complete multiplication theorem. + +## Interface and theorem + +Let R be a nonzero unital ring. Use seven distinct arrays x0,x1,x2,y0,y1,y2,z +in a finite free R-module of any positive rank. The six fixed R-linear maps +Ai,Bj need not commute or be invertible. The only permitted operations are + +```text +Bj^s: z += s Bj(xj) +Ai^s: yi += s Ai(z) s = +1 or -1 +``` + +The word is independent of data and of the particular maps. Sources are immutable, +outputs are not read, and z must restore. Initial outputs and z are arbitrary. +Every complete call preserves its source and other data, restores private scratch +and returns required heads. No scalar multipliers, transfers, extra connectors, +role changes, direct products or other data operations are available. A minus +sign subtracts an increment; it does not invert Ai or Bj. + +The required final update is + +```text +M = [[1,1,1], [1,1,-1], [1,-1,0]] +yi += sum_j Mij Ai(Bj(xj)); xj and z unchanged. +``` + +A word must work for every choice of arrays and maps over R. Specialized maps +or a particular module on which R acts nonfaithfully can have cheaper words; +those are not this uniform problem. The zero ring is excluded. + +Let cF > 0 be the complete fixed price of operator F, equal for its two signs, +and let S be the sum of all six prices. Then the exact minimum query bill is + +```text +char R = 2: 2 S +char R = 3: 2 S + min_F cF +char R = 0 or >= 4: 2 S + 2 min_F cF. +``` + +Setting all prices to one gives the three call minima above. The prices include +child execution, source/coefficient access, private restoration, required routing, +frame adaptation and head returns. Admission, coefficient preparation and root +selection/control remain additional costs. If those depend on the word, this +formula is the query bill, not an optimum for the combined implementation. + +## Proof + +Write u_j = Bj(xj). After the source calls at a boundary t, + +```text +z = z_initial + sum_j q_t[j] u_j. +``` + +For output i, let d_i be the signed sum of its readouts and let +C_ij = sum over its readouts at t of s*q_t[j]. Linearity gives exactly + +```text +yi_final = yi_initial + d_i Ai(z_initial) + sum_j C_ij Ai(Bj(xj)). +``` + +Thus integer coefficient identities q_final=0, d=0, C=M, reduced in R, +are sufficient. They are also necessary for uniform correctness: use the free +rank-one module R, identity maps, isolate one initial source or z, and set +unwanted maps to zero. The map Z -> R, n -> n*1_R, has kernel zero in +characteristic zero and cZ in finite characteristic c. No division, field +hypothesis, lack of torsion elsewhere in R, or absence of zero divisors is used. + +**At least two calls per operator.** Every row and column of M is nonzero. +An absent Bj cannot contribute its column and one occurrence cannot restore z. +An absent Ai cannot update its row and one occurrence cannot cancel initial z. +All six operators therefore occur at least twice in every characteristic. + +**The 12-call obstruction transfers without modular aliasing.** In characteristic +zero or at least three, two signed calls can have signed sum zero only when their +signs are opposite. At exactly 12 calls each source therefore enters once and +leaves once, so q_t[j] is either zero or one fixed sign epsilon_j. Each Ai has +two opposite readouts, and its desired row must be a signed difference between +two visited q vectors. Every coordinate of that difference is in {-1,0,1}. +The difference from a required entry in {-1,0,1} is in {-2,-1,0,1,2}. +It vanishes in R exactly when it is the integer zero for all characteristics +zero or at least three. Consequently a 12-call word here would be a 12-call +word for the same integer target in characteristic zero. + +Ross Richardson's [PR944](https://github.com/CrocSwap/integer-mult-bounds/pull/944) +proves that no such paired path covers all three rows. This is an explicitly +used predecessor theorem, not a new obstruction census. The graph proof in +[the retained rigidity note](../nonunit-signed-connector-rigidity/PROOF.md) +is another account of that same obstruction. This transfer excludes 12 calls +in every characteristic zero or at least three. In characteristic two the two +signs coincide and the no-alias implication fails, as it should. + +**Characteristic three is the only three-occurrence exception.** Three signs +sum to one of -3,-1,1,3. This sum cannot vanish in a nonzero ring of characteristic +zero or at least four. In those characteristics every operator's count is either +two or at least four. Since all counts equal to two was excluded, some operator +has at least four calls. This proves both the 14-call lower bound and the +weighted bound 2S + 2 min_F cF for words of any length. In particular, the proof +does not assume all restoring counts are even in finite characteristic. + +martinxxx9's [PR1088](https://github.com/CrocSwap/integer-mult-bounds/pull/1088) +supplies six integer 14-call words, each repeating a chosen operator four times +and every other operator twice. Their coefficient identities hold over Z, +so they hold over every R. Choosing a cheapest operator attains the bound. +This proves the new characteristic-at-least-four result, including all composite +characteristics, without an infinite search over moduli. + +In characteristic three, the support bound and 12-call exclusion imply that +some operator pays at least one extra call. Sagar Thakrar's +[PR1349](https://github.com/CrocSwap/integer-mult-bounds/pull/1349) supplies a +13-call word with any chosen operator tripled. Its coefficient residuals are +integer multiples of three, so it works over every characteristic-three ring, +including F3[epsilon]/(epsilon^2). This proves 2S + min_F cF beyond F3 itself. +The word and the F3 optimum are predecessor results; the ring lift is the extension. + +In characteristic two the following 12-call word attains two calls of each +operator. At its positive reads the source prefixes are (1,1,0) and (1,1,1). +The required signs +1 and -1 agree in R, so these are exactly the target rows. +The first reads subtract the independent initial dirt and the final source +calls restore z. + +```text +A0- A1- A2- B0+ B1+ A2+ B2+ A0+ A1+ B0- B1- B2- +``` + +The binary support-floor phenomenon is already part of PR944/PR934. This word +makes the characteristic boundary explicit; it is not claimed as a new binary +connector construction. Together these cases prove the stated spectrum. + +## Finite evidence and reproduction + +From the repository root, use CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/signed-characteristic-spectrum/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/signed-characteristic-spectrum/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/signed-characteristic-spectrum +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/signed-characteristic-spectrum --check-source-history +``` + +Expected scientific marker: `PASS_SIGNED_CHARACTERISTIC_SPECTRUM`. +The verifier checks 238 short signed-count cases, 10,935 no-alias cases and +24 exact rational price cases. The 13 literal witnesses comprise the binary +word and the six credited repairs in each of the other cases. + +A separate dense interpreter executes 2,190 word/input cases. Each checks the +forward action, inverse action and dirty round trip on all 28 scalar basis +inputs plus two dense dirty inputs. The matrices represent two-dimensional +modules over (Z/cZ)[epsilon]/(epsilon^2), or Z[epsilon]/(epsilon^2) at c=0. +The tested characteristics are 0,2,3,4,5,6,7,8,9,10,12,15,16. The operators +include noncommuting maps. This exercises nonfield rings and independent dirty +coordinates rather than treating scalar identity maps as the only realization. + +The 199 controls consist of 84 query omissions and 84 sign flips in the six +14-call words over characteristic four, 30 uses of the six ternary words in +wrong characteristics, and the binary word incorrectly used in characteristic +three. Every control fails its named target identity. No count includes an +unexamined failure classification. + +[RESULT.json](RESULT.json) is generated from these checks and binds every +package file other than itself and all four live predecessor inputs by SHA256. +An optional `--write-receipt /new/external/path.json` generates a fresh candidate +outside the checkout and refuses overwrite. The default replay compares the +recomputed receipt with the committed one. No predecessor executable is imported. + +## Limits and implementation obligations + +The universal statement is the written scoped proof with the explicitly cited +PR944 paired-path obstruction. Executed modular cases corroborate the extension; +they do not enumerate every ring or certify a complete multiplication theorem. +Independent human and formal proof-kernel review are unclaimed. No new supplier, +selected cold replay, physical port installation, stock, precision, fixed-tape +compiler or outer analytic admission is supplied. The selected frontier is unchanged. + +The Python implementation uses dynamic allocation with finite fixed domains: +words have at most 14 queries, banks have 28 scalar coordinates, there are 30 +input banks, 13 characteristics and 13 witnesses. All loops have finite explicit +bounds or iterate authenticated, bounded package files. Each function is under +60 lines. Explicit exceptions enforce the invariants even under `-O`. +This is the managed-runtime deviation from fixed preallocation in Power of Ten; +there is no recursive execution or child process. Standard-library execution +with warnings as errors is the registered diagnostic surface. + +## Open next questions + +1. Determine the exact characteristic-dependent tariff when the two signs of + an operator have different prices. This matters because a physical interface + can price inverse calls differently. Start with the six credited repairs and + a count-vector lower bound. Additional restoring words may be needed, and + the equal-sign envelope here does not settle that problem. +2. Find a source-bound supplier seam with this exact signed 3x3 demand and all + six complete prices. Begin with one literal 14-call word and a full port, + frame, restoration and precision ledger. No compatible selected caller has + been identified here, so no downstream kappa claim follows. + +## Credit and provenance + +This extension was produced by Nick Petalas. Ross Richardson supplies PR944's +characteristic-zero target, interface and obstruction and PR934's binary +predecessor. martinxxx9 supplies PR1088's six weighted repair words. Sagar +Thakrar supplies PR1349's F3 words and minimum. Charles Bethin's retained +nonunit rigidity note supplies the cited alternate graph proof of the inherited +obstruction. +CubeJerry/PR889 and Chafik Boukhalfa/PR628 retain the signed fanout and dirty +product-commutator lineage in the predecessor notices. No predecessor credit +line or package is changed. Apache-2.0. + +The scientific base is `12fa8c5c844be21bfefb38a19503fbd867a11244`, priority +revision 7. The earlier [released characteristic handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19080030) +proposed the short signed-count observation but published no verified result. +This package completes that question and extends the coefficient domain to +unital rings. Its [claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19080558) +was posted before the proof package was developed. Sources are pinned in +[SOURCES.json](SOURCES.json); [TASK.json](TASK.json) records the scope change +from an added operation to a coefficient-domain theorem. diff --git a/research/signed-characteristic-spectrum/RESULT.json b/research/signed-characteristic-spectrum/RESULT.json new file mode 100644 index 0000000000..a0457591d4 --- /dev/null +++ b/research/signed-characteristic-spectrum/RESULT.json @@ -0,0 +1,25 @@ +{ + "counts": { + "dense_cases": 2190, + "negative_controls": 199, + "no_alias_cases": 10935, + "price_cases": 24, + "signed_count_cases": 238, + "witnesses": 13 + }, + "input_sha256": { + "research/nonunit-signed-connector-rigidity/PROOF.md": "18cd39d53dc5c27ee7777ac8a9a04c3c3300647e57860224d8cc362d0068144e", + "research/signed-connector-obstruction/CERTIFICATE.json": "2930f0ae2c77cf94eadc9f065fe8d034249e5e607b9eb4e8f581d1c60f5e763b", + "research/ternary-connector-independent-seed84/CERTIFICATE.json": "a814ec93439ea36878fd1b6ebd3c19c3151b27e474ca0edc3d0a14c290d82b7c", + "research/weighted-signed-connector-seed58/CERTIFICATE.json": "30291599facabc902e85bda418e587d7af37760875b86f88607dbf2c9f38cbeb" + }, + "payload_sha256": { + "README.md": "82a19c28f1f5e25ab1a20a04ae90ab35b825f70c1d768f40c1ebe6394953fb33", + "SOURCES.json": "230995bcff820450a61cd66afd6ae3685f7f03997356766f54b53f853da8e02d", + "TASK.json": "afe8f62caef049b88da428893da9d295b49807c91b18e54dbc172210f87c62ed", + "VERIFY.json": "c8a7f1416a8a61c0648f96b1004b2ead9b5c539dad2d8d932b6a3884f925e0e7", + "verify.py": "2ef3524aea635311b32428f1a39be09e3fe55d337b316e5a33e8f5c3d32e8294" + }, + "schema": "signed-characteristic-spectrum/v1", + "status": "PASS_SIGNED_CHARACTERISTIC_SPECTRUM" +} diff --git a/research/signed-characteristic-spectrum/SOURCES.json b/research/signed-characteristic-spectrum/SOURCES.json new file mode 100644 index 0000000000..c20cbb25a9 --- /dev/null +++ b/research/signed-characteristic-spectrum/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/nonunit-signed-connector-rigidity/PROOF.md", + "usage": "input", + "git_blob": "c4d51cb64a0a2fed2bfd3289be816f3b9a024f58", + "sha256": "18cd39d53dc5c27ee7777ac8a9a04c3c3300647e57860224d8cc362d0068144e" + }, + { + "path": "research/signed-connector-obstruction/CERTIFICATE.json", + "usage": "input", + "git_blob": "2d047548111241783bd977115318317f0ad23302", + "sha256": "2930f0ae2c77cf94eadc9f065fe8d034249e5e607b9eb4e8f581d1c60f5e763b" + }, + { + "path": "research/ternary-connector-independent-seed84/CERTIFICATE.json", + "usage": "input", + "git_blob": "6d309616c6626d50531cfb522d8227483ffbccc7", + "sha256": "a814ec93439ea36878fd1b6ebd3c19c3151b27e474ca0edc3d0a14c290d82b7c" + }, + { + "path": "research/weighted-signed-connector-seed58/CERTIFICATE.json", + "usage": "input", + "git_blob": "abaa49bf8b1724461ba11fa37aa1df5e73ddf7bf", + "sha256": "30291599facabc902e85bda418e587d7af37760875b86f88607dbf2c9f38cbeb" + } + ] +} diff --git a/research/signed-characteristic-spectrum/TASK.json b/research/signed-characteristic-spectrum/TASK.json new file mode 100644 index 0000000000..d31e5b0320 --- /dev/null +++ b/research/signed-characteristic-spectrum/TASK.json @@ -0,0 +1,68 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 7, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "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": "Exact canonical signed-connector tariff over every nonzero unital coefficient ring, with arbitrary dirty data, uniform linear maps and positive fixed prices equal between signs.", + "scope_change_reason": "The card requests a new priced operation. This side result instead changes the coefficient domain, takes the released characteristic handoff, and proves which arithmetic characteristics preserve or reduce the existing signed-query tariff.", + "bottleneck_link": "Coefficient-domain changes can alter the restoration tariff of recursive connector interfaces; this theorem prevents importing F3 savings into incompatible coefficient rings. No supplier seam or kappa gain is asserted.", + "budget_minutes": 60, + "stop_rule": "Finish the written ring-characteristic proof, its fixed-price envelope and bounded exact controls. Stop before physical supplier expansion.", + "outcome": "completed", + "evidence": "README.md proof; verify.py; generated RESULT.json", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the exact envelope for sign-dependent prices?", + "why_it_matters": "Inverse child calls can have different physical prices.", + "first_step": "Derive signed count-vector lower bounds and price the six credited repairs.", + "blocked_by": "Potential additional restoring word types beyond the equal-sign envelope." + }, + { + "question": "Where does a selected supplier expose this exact demand?", + "why_it_matters": "Abstract query savings imply no supplier or exponent improvement without a complete caller.", + "first_step": "Bind one literal word to six fixed ports and complete prices.", + "blocked_by": "No compatible source-bound caller, precision or full implementation ledger is supplied." + } + ] +} diff --git a/research/signed-characteristic-spectrum/VERIFY.json b/research/signed-characteristic-spectrum/VERIFY.json new file mode 100644 index 0000000000..1f56e3e7b5 --- /dev/null +++ b/research/signed-characteristic-spectrum/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/nonunit-signed-connector-rigidity/PROOF.md", + "research/signed-connector-obstruction/CERTIFICATE.json", + "research/ternary-connector-independent-seed84/CERTIFICATE.json", + "research/weighted-signed-connector-seed58/CERTIFICATE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Ring-characteristic count law, no modular alias, exact prices, noncommuting dual-ring dirty action/inverse, and 199 rejection controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Identical scientific checks and authenticated receipt with Python assertions disabled." + } + ] +} diff --git a/research/signed-characteristic-spectrum/verify.py b/research/signed-characteristic-spectrum/verify.py new file mode 100644 index 0000000000..177cc1e62d --- /dev/null +++ b/research/signed-characteristic-spectrum/verify.py @@ -0,0 +1,263 @@ +#!/usr/bin/env python3 +"""Finite evidence for the signed-connector ring-characteristic theorem.""" + +import argparse +import hashlib +import itertools +import json +from fractions import Fraction +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parent.parent +TARGET = ((1, 1, 1), (1, 1, -1), (1, -1, 0)) +OPERATORS = ("B0", "B1", "B2", "A0", "A1", "A2") +CHARACTERISTICS = (0, 2, 3, 4, 5, 6, 7, 8, 9, 10, 12, 15, 16) +BINARY_WORD = (("A", 0, -1), ("A", 1, -1), ("A", 2, -1), + ("B", 0, 1), ("B", 1, 1), ("A", 2, 1), + ("B", 2, 1), ("A", 0, 1), ("A", 1, 1), + ("B", 0, -1), ("B", 1, -1), ("B", 2, -1)) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def digest(data): + return hashlib.sha256(data).hexdigest() + + +def read_inputs(): + manifest = json.loads((PACKAGE / "SOURCES.json").read_text()) + inputs = {} + for entry in manifest["files"]: + if entry["usage"] == "input": + path = ROOT / entry["path"] + data = path.read_bytes() + require(digest(data) == entry["sha256"], f"source hash: {path}") + inputs[entry["path"]] = data + return inputs + + +def source_json(inputs, name): + return json.loads(inputs[f"research/{name}/CERTIFICATE.json"]) + + +def normalize(value, characteristic): + return value % characteristic if characteristic else value + + +def coefficient_action(word): + require(0 < len(word) <= 14, "word length outside finite evidence domain") + source = [0, 0, 0] + dirt = [0, 0, 0] + rows = [[0, 0, 0] for _ in range(3)] + for kind, index, sign in word: + require(kind in ("A", "B") and index in range(3), "invalid port") + require(sign in (-1, 1), "invalid query sign") + if kind == "B": + source[index] += sign + else: + dirt[index] += sign + for column in range(3): + rows[index][column] += sign * source[column] + return source, dirt, rows + + +def correct(word, characteristic): + source, dirt, rows = coefficient_action(word) + residual = source + dirt + residual += [rows[i][j] - TARGET[i][j] + for i in range(3) for j in range(3)] + return all(normalize(value, characteristic) == 0 for value in residual) + + +def occurrences(word): + return tuple(sum(kind + str(index) == name for kind, index, _ in word) + for name in OPERATORS) + + +def coefficient_checks(): + sign_cases = 0 + for characteristic in (0, *range(2, 18)): + for length in range(1, 4): + for signs in itertools.product((-1, 1), repeat=length): + zero = normalize(sum(signs), characteristic) == 0 + expected = length == 2 and ( + characteristic == 2 or sum(signs) == 0) + expected |= characteristic == 3 and abs(sum(signs)) == 3 + require(zero == expected, "short signed-count law") + sign_cases += 1 + vectors = tuple(itertools.product((-1, 0, 1), repeat=3)) + alias_cases = 0 + for characteristic in range(3, 18): + for difference in vectors: + for target in vectors: + modular_equal = all((a - b) % characteristic == 0 + for a, b in zip(difference, target)) + require(modular_equal == (difference == target), "modular alias") + alias_cases += 1 + require(normalize(1 - (-1), 2) == 0, "characteristic-two control") + return sign_cases, alias_cases + + +def collect_words(inputs): + integer = source_json(inputs, "weighted-signed-connector-seed58")["witnesses"] + ternary = source_json(inputs, "ternary-connector-independent-seed84")["canonical_words"] + require(set(integer) == set(ternary) == set(OPERATORS), "six witness keys") + words = [(2, "paired", BINARY_WORD)] + for name in OPERATORS: + for characteristic, witnesses, extra in ((0, integer, 2), (3, ternary, 1)): + word = tuple(tuple(query) for query in witnesses[name]) + require(len(word) == 12 + extra, "credited witness length") + expected = tuple(2 + (extra if op == name else 0) for op in OPERATORS) + require(occurrences(word) == expected, "credited witness counts") + require(correct(word, characteristic), "witness coefficient action") + words.append((characteristic, name, word)) + require(correct(BINARY_WORD, 2) and occurrences(BINARY_WORD) == (2,) * 6, + "characteristic-two word") + return words + + +def price_checks(words): + prices = [tuple(Fraction(1 if i == j else 5) for i in range(6)) + for j in range(6)] + prices += [tuple(Fraction(i + 1, i + 2) for i in range(6)), (Fraction(1),) * 6] + cases = 0 + for characteristic, surcharge in ((0, 2), (2, 0), (3, 1)): + candidates = [word for char, _, word in words if char == characteristic] + for tariff in prices: + bills = [sum(price * count for price, count in + zip(tariff, occurrences(word))) for word in candidates] + require(min(bills) == 2 * sum(tariff) + surcharge * min(tariff), + "fixed-price envelope") + cases += 1 + return cases + + +def add(left, right, sign, characteristic): + return tuple(normalize(a + sign * b, characteristic) for a, b in zip(left, right)) + + +def multiply(matrix, vector, characteristic): + return tuple(normalize(sum(a * b for a, b in zip(row, vector)), characteristic) + for row in matrix) + + +def dual_matrix(seed): + # Multiplication by a+b*epsilon is [[a,0],[b,a]], epsilon**2=0. + matrix = [[0] * 4 for _ in range(4)] + for i in range(2): + for j in range(2): + a = (seed + 2 * i + j) % 3 - 1 + b = (2 * seed + i + 3 * j) % 5 - 2 + matrix[2 * i][2 * j] = a + matrix[2 * i + 1][2 * j] = b + matrix[2 * i + 1][2 * j + 1] = a + return tuple(tuple(row) for row in matrix) + + +def execute(word, bank, operators, characteristic): + state = list(bank) + for kind, index, sign in word: + source, target = (index, 6) if kind == "B" else (6, 3 + index) + matrix = operators[(kind, index)] + state[target] = add(state[target], multiply(matrix, state[source], characteristic), + sign, characteristic) + return tuple(state) + + +def target_bank(bank, operators, characteristic, sign=1): + state = list(bank) + for i in range(3): + for j in range(3): + bx = multiply(operators[("B", j)], bank[j], characteristic) + abx = multiply(operators[("A", i)], bx, characteristic) + state[3 + i] = add(state[3 + i], abx, sign * TARGET[i][j], characteristic) + return tuple(state) + + +def dense_checks(words): + operators = {(kind, j): dual_matrix(1 + j + 4 * (kind == "A")) + for kind in ("A", "B") for j in range(3)} + a, b = operators[("A", 0)], operators[("B", 0)] + require(multiply(a, multiply(b, (1, 0, 0, 0), 0), 0) != + multiply(b, multiply(a, (1, 0, 0, 0), 0), 0), "noncommuting maps") + banks = [tuple(tuple(int(4 * role + k == column) for k in range(4)) + for role in range(7)) for column in range(28)] + banks += [tuple(tuple((seed + 3 * role + 2 * k) % 7 - 3 for k in range(4)) + for role in range(7)) for seed in (1, 3)] + cases = 0 + for characteristic in CHARACTERISTICS: + selected = 2 if characteristic == 2 else 3 if characteristic == 3 else 0 + for char, _, word in words: + if char != selected: + continue + inverse = tuple((kind, index, -sign) for kind, index, sign in reversed(word)) + for raw in banks: + bank = tuple(tuple(normalize(x, characteristic) for x in row) for row in raw) + output = execute(word, bank, operators, characteristic) + require(output == target_bank(bank, operators, characteristic), "dense action") + require(execute(inverse, bank, operators, characteristic) == + target_bank(bank, operators, characteristic, -1), "dense inverse") + require(execute(inverse, output, operators, characteristic) == bank, + "dirty round trip") + cases += 1 + return cases + + +def negative_checks(words): + cases = 0 + for char, _, word in words: + if char == 0: + for index in range(len(word)): + require(not correct(word[:index] + word[index + 1:], 4), "deleted query") + changed = list(word) + kind, port, sign = changed[index] + changed[index] = (kind, port, -sign) + require(not correct(changed, 4), "flipped query") + cases += 2 + if char == 3: + for wrong in (0, 4, 5, 6, 9): + require(not correct(word, wrong), "ternary-only restoration") + cases += 1 + require(not correct(BINARY_WORD, 3), "binary sign alias control") + cases += 1 + return cases + + +def receipt(): + inputs = read_inputs() + words = collect_words(inputs) + sign_cases, alias_cases = coefficient_checks() + counts = {"signed_count_cases": sign_cases, "no_alias_cases": alias_cases, + "price_cases": price_checks(words), "dense_cases": dense_checks(words), + "negative_controls": negative_checks(words), "witnesses": len(words)} + payload = {path.name: digest(path.read_bytes()) for path in sorted(PACKAGE.iterdir()) + if path.is_file() and path.name != "RESULT.json"} + return {"schema": "signed-characteristic-spectrum/v1", "counts": counts, + "payload_sha256": payload, + "input_sha256": {path: digest(data) for path, data in sorted(inputs.items())}, + "status": "PASS_SIGNED_CHARACTERISTIC_SPECTRUM"} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write-receipt", type=Path) + args = parser.parse_args() + result = receipt() + if args.write_receipt: + destination = args.write_receipt.resolve() + require(not destination.is_relative_to(ROOT), "receipt output must be outside checkout") + with destination.open("x") as stream: + json.dump(result, stream, indent=2, sort_keys=True) + stream.write("\n") + else: + expected = json.loads((PACKAGE / "RESULT.json").read_text()) + require(result == expected, "generated receipt differs") + print(result["status"], json.dumps(result["counts"], sort_keys=True)) + + +if __name__ == "__main__": + main()