diff --git a/research/signed-prime-connector/README.md b/research/signed-prime-connector/README.md new file mode 100644 index 0000000000..c14a7eaab9 --- /dev/null +++ b/research/signed-prime-connector/README.md @@ -0,0 +1,252 @@ +# Exact signed two-source connector over odd prime fields + +For every odd prime p, the signed dirty connector with two immutable sources +and all p^2 - 1 nonzero coefficient rows over F_p has exact unit-call optimum + +```text +OPT_signed(p, 2) = 2p^2 + 2p - 4. +``` + +In particular, the optimum is **56 calls over F5**. The construction uses +eight source calls and two readouts for each of the 24 nonzero rows. The +lower bound permits arbitrary extra readouts, so it is an all-word optimum +within the specified alphabet. + +This is a **scoped proof with finite corroboration**, produced by Nick +Petalas. The new step is an exact full-coefficient signed optimum and a +short-path deficit argument. The prefix/difference method is predecessor +work. No new kappa or complete multiplication theorem is claimed. + +## Interface + +There are two read-only sources x_0,x_1, one borrowed dirty connector z and +distinct dirty outputs y_v indexed by every nonzero v in F_p^2. For arbitrary +compatible F_p-linear maps, the required action is + +```text +y_v += v_0 A_v B_0 x_0 + v_1 A_v B_1 x_1; +x_0, x_1 and z unchanged. +``` + +Maps may be singular and need not commute. The only operations are signed +complete calls, each with unit price: + +```text ++B_j: z += B_j x_j -B_j: z -= B_j x_j ++A_v: y_v += A_v z -A_v: y_v -= A_v z +``` + +The negative letters subtract a map application; they do not invert its +matrix. Calls preserve every other row and restore their own private scratch +and entry heads. The word is independent of data and map entries. Outputs +are observed only after completion and cannot serve as workspace. There is +no scalar-multiple source letter beyond the two signs, no source mutation, +extra connector, free copy, direct A_v B_j call or frame change. + +This retains Ross Richardson's #943/#934 complete-call boundary and uses +signed letters as in conorholds's #2208. Full coefficient demand differs from +binary-mask demand. The GF4 scalar-source alphabet of #2266 permits nonunit +coefficients in a source call and is a different model. + +## Prefix identity + +Project any legal word onto its b source calls. Let q_t in F_p^2 be their +signed prefix-count vector at boundary t, with q_0=q_b=0. At that boundary, + +```text +z = z_initial + (q_t)_0 B_0 x_0 + (q_t)_1 B_1 x_1. +``` + +Readouts of A_v with signs epsilon_s at boundaries t_s add + +```text +(sum_s epsilon_s) A_v z_initial + + sum_j (sum_s epsilon_s (q_t_s)_j) A_v B_j x_j. +``` + +Thus correctness is equivalent to cancellation of connector dirt and the +required two coefficients, together with q_b=0. Sufficiency uses linearity +only and keeps A_v on the left. Necessity follows by specializing all maps +to scalar identities and independently varying x_0,x_1,z_initial. + +Every nonzero output needs at least two readouts. A single signed readout +cannot cancel arbitrary incoming dirt in odd characteristic. With exactly +two readouts the signs must be opposite, since p is odd. Such an output is +therefore available exactly when v is a difference q_s-q_t of two prefixes. + +## Attaining construction + +Put h=(p-1)/2 and use the integer-restoring source word + +```text +(+B_0)^h (+B_1)^h (-B_0)^h (-B_1)^h. +``` + +Its 4h=2(p-1) events visit every integer boundary point of the square +[0,h]^2. Every row v has a unique representative (a,b) in [-h,h]^2. It is a +difference P-Q of two square-perimeter points: + +- For a>=0,b>=0, take P=(a,h), Q=(0,h-b). +- For a>=0,b<0, take P=(a,0), Q=(0,-b). +- For a<0, apply one of these rules to (-a,-b) and swap P,Q. + +Read +A_v at P and -A_v at Q. Both points occur on the path; their +chronological order is irrelevant because readouts preserve z. The two +calls cancel A_v z_initial and give exactly the required row. All output +pairs can be interleaved in boundary order in one word. + +There are p-1 source calls per source and two readouts per nonzero row, so +the full count is + +```text +2(p-1) + 2(p^2-1) = 2p^2 + 2p - 4. +``` + +## Lower bound allowing extra readouts + +Let M=p^2-1 and let b_j count source j's occurrences, regardless of sign. +Every legal word costs at least b+2M, where b=b_0+b_1. If b>=2(p-1), this +already proves the proposed bound. + +Suppose b<2(p-1). One coordinate j has b_j<=p-2. Its signed displacement +is zero modulo p, and its absolute value is at most b_j 2M + 2(p-1). +``` + +Thus shorter source paths are strictly more expensive even after buying +extra readouts. Combined with the construction, this proves the exact +optimum for every odd prime. No census is a premise of this proof. + +## Evidence and reproduction + +From the repository root, using CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/signed-prime-connector/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/signed-prime-connector/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/signed-prime-connector +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/signed-prime-connector --check-source-history +``` + +Any CPython 3.12 executable can replace the absolute interpreter path. The +verifier prints a generated JSON receipt bound to SHA256 hashes of all five +package files, then + +```text +PASS_SIGNED_PRIME_CONNECTOR p5_calls=56 primes=5 dense_cases=10 controls=10 +``` + +It checks the closed-form readout compiler, an independently enumerated +perimeter difference set and the full literal dirty coefficient action: + +| p | Nonzero rows | Source calls | Full calls | +|---:|---:|---:|---:| +| 3 | 8 | 4 | 20 | +| 5 | 24 | 8 | 56 | +| 7 | 48 | 12 | 108 | +| 11 | 120 | 20 | 260 | +| 13 | 168 | 24 | 360 | + +The lower-bound census visits every signed source word of length less than +four at p=3, and less than eight at p=5. It visits 85 and 21,845 words, +respectively. Among them 9 and 641 close modulo p, including the empty +word. Their smallest missing-row counts are 6 and 10, exactly 2p. Every +closed path is checked for the integer-range lemma and the final excess +inequality. No equivalence quotient or heuristic pruning is used. + +Ten dense executions cover each listed prime in dimensions two and three, +with dirty connectors and outputs, singular source maps and explicit checks +that readout/source maps do not commute. Ten rejection controls cover +dropped and sign-flipped source/readout calls, an output misroute, a missing +output pair, the F5 word interpreted over F7, and three invalid moduli. +All contracts remain enabled under optimized Python. + +The card's first working control passed with 945 pairings, maximum coverage +31, 74 queries and 182 leaves. The selected-source metadata baseline passed +separately. These are orientation checks, not new results or selected cold +replays. Predecessor results are cited rather than reverified here. + +## Bounds and implementation limits + +The written theorem is uniform in p and in compatible map dimensions. The +executable domain is bounded to odd primes at most 31, with registered +fixtures at the five listed primes and exhaustive short paths only at 3,5. +It has no recursion, subprocess, network access or file writes. The maximum +source path is 60 events, the maximum full word is 1,980 events, and package +hash reads are capped at 1 MiB per file. Every function is below 60 lines. + +Python requires dynamic allocation during computation, a Power of Ten rule 3 +deviation in this bounded offline verifier. Fixed prime, path, word and +matrix-dimension limits bound live storage; the registered timeout is 60 +seconds. The verifier is run with warnings treated as errors. No separate +project Python linter or type checker is configured or available locally. +Reconsider fixed-capacity storage only if this code enters an online caller. + +The unit call count is proved. For unequal complete prices, the same word +has the constructive bill + +```text +h sum_(j=0,1) (c_(+B_j) + c_(-B_j)) + + sum_(v!=0) (c_(+A_v) + c_(-A_v)). +``` + +Its optimality for unequal prices is unknown. Admission, map preparation, +word storage, dispatch, physical routing, frames, stock, precision and tape +costs remain additional and unknown. There is no identified recursive +consumer for full F_p^2 demand and no complete supplier budget. The family +decision is to finish this local exact result and stop construction work. + +No formal proof-kernel build, independent human review, selected cold +replay, physical supplier admission or outer multiplication proof is +supplied. The selected frontier and all frozen predecessors are unchanged. + +## Open next questions + +1. What is the exact cost with unequal complete source/readout prices? + Start at p=5 with the short-path deficit and explicitly price a source + saving against extra readouts. The unit-price proof does not compare + those weighted trades. +2. What changes for composite characteristic or a field extension? Start + by specifying the coefficient set and permitted scalar letters. The + theorem here assumes prime-field coefficients and only two signs. +3. Does an actual recursive caller need all F_p^2 coefficient rows? Pin one + before another construction round, then price admission, every signed + primitive, dispatch and dirty return. No such caller is provided here. + +## Credit and source scope + +This contribution was produced by Nick Petalas. Ross Richardson's +[#943/#934 lineage](../universal-connector-boundary/README.md) supplies the +complete-call boundary and paired-prefix criterion. conorholds's +[#2208](../bidirectional-connector/README.md) supplies signed dirty-connector +context and all-word query-model methods. Riquelme Soares's +[#4189](https://github.com/CrocSwap/integer-mult-bounds/pull/4189) supplies the +unsigned F3 one-source predecessor. The distinct full GF4 two-source problem +and charged nonunit scalar letters are from 1337isnot1337's +[#2266](https://github.com/CrocSwap/integer-mult-bounds/pull/2266). Nick +Petalas's #4256 treats all coefficient rows with unsigned calls, a different +alphabet. No priority is claimed for elementary lattice differences or the +prefix identity. + +[SOURCES.json](SOURCES.json) pins historical provenance at public base +624de9dc66858af0945e5f8a0942488d62280d43. There are no executable predecessor +dependencies. The catalogue scope is explicitly changed from a general +alphabet extension to this two-source full-coefficient exact side result. +The new step is the square construction together with an all-word lower +bound that rules out cheaper source/readout trades. Independent human and +formal proof-kernel review are unclaimed. Apache-2.0. diff --git a/research/signed-prime-connector/SOURCES.json b/research/signed-prime-connector/SOURCES.json new file mode 100644 index 0000000000..d4706ac35b --- /dev/null +++ b/research/signed-prime-connector/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/universal-connector-boundary/README.md", + "usage": "provenance", + "git_blob": "d277f7c5830b1f2bc42e1ff41ab86e7d7564929f", + "sha256": "23415f7829ab8d80a783142f10f7d31abbce84579362769984680af3df954476" + }, + { + "path": "research/bidirectional-connector/README.md", + "usage": "provenance", + "git_blob": "b2beaf30eaa0692211c939ef417dbf8ff849f6ed", + "sha256": "a41f6e79e7df54ea51d563f7007970a4e01ed8c2d1b45d1fefb1f927fee97172" + }, + { + "path": "research/gf4-scalar-source-connector-seeda472dd8c/README.md", + "usage": "provenance", + "git_blob": "2fb5391b274a9959fc26495405387a7983a1d108", + "sha256": "37f55b37d63bd90a9c601f97179f399d53e0965db795561044c1879be5351dbf" + }, + { + "path": "research/full-coefficient-connector/README.md", + "usage": "provenance", + "git_blob": "38b6c86d832683f9613126ccca113998f3e7df10", + "sha256": "ee4394deee2d92ed2df74a10830a6df2124b89e7995aab00b77a7ec7af66ee3e" + } + ] +} diff --git a/research/signed-prime-connector/TASK.json b/research/signed-prime-connector/TASK.json new file mode 100644 index 0000000000..d8f6b7ba9c --- /dev/null +++ b/research/signed-prime-connector/TASK.json @@ -0,0 +1,110 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "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 unit-call optimum 2p^2+2p-4 for every odd prime p, two immutable sources, all nonzero F_p^2 coefficient rows, one dirty restored connector, and only signed source/readout complete calls.", + "scope_change_reason": "Changes binary-mask demand to full prime-field coefficient demand and permits signed letters. This is a local exact side result, not a claim of a completed supplier budget.", + "bottleneck_link": "Signed source/readout calls are a concrete priced alphabet change at the generic connector boundary. This theorem supplies an exact local bill; a recursive full-coefficient consumer and all physical costs remain unknown.", + "budget_minutes": 60, + "stop_rule": "Stop research at the first verified original result. Package the square construction and all-word lower bound; do not pursue composite characteristics, additional sources or weighted optima.", + "outcome": "completed", + "evidence": "Written uniform proof; exact constructions at p=3,5,7,11,13; complete short-source censuses of 85 and 21845 words at p=3,5; ten dense dirty noncommuting fixtures; ten rejection controls. A generated stdout receipt binds all five package files.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the exact optimum with unequal complete call prices?", + "why_it_matters": "A physical caller may have source and readout prices that favor more readouts.", + "first_step": "At p=5 compare explicitly priced short source words against their missing-row readout costs.", + "blocked_by": "The unit-price lower bound does not solve weighted trades." + }, + { + "question": "What changes for composite characteristic or extension-field coefficients?", + "why_it_matters": "The prime-field result does not classify other coefficient alphabets.", + "first_step": "Specify the coefficient set and legal scalar letters before extending the lattice argument.", + "blocked_by": "No theorem outside odd prime fields is supplied." + }, + { + "question": "Which recursive caller needs every nonzero coefficient row in F_p^2?", + "why_it_matters": "Only a complete physical consumer can turn this call count into a supplier saving.", + "first_step": "Pin one caller and price admission, signed primitives, dispatch and dirty return.", + "blocked_by": "Caller, stock, precision and physical cost obligations are unknown." + } + ], + "claim_type": "scoped proof with finite corroboration", + "result": "OPT_signed(p,2)=2p^2+2p-4 for every odd prime p. In particular OPT_signed(5,2)=56, with eight source calls and 48 readouts.", + "predecessors": [ + { + "pr": 943, + "author": "Ross Richardson", + "role": "complete-call dirty connector and paired-prefix criterion; citation only" + }, + { + "pr": 934, + "author": "Ross Richardson", + "role": "generic connector lineage; citation only" + }, + { + "pr": 2208, + "author": "conorholds", + "role": "signed dirty-connector context and all-word query methods; canonical retained README is pinned separately" + }, + { + "pr": 4189, + "head": "5fb3936dfc8082f438f21c72dd6ca49ff4366ae7", + "author": "Riquelme Soares", + "role": "unsigned F3 one-source context; citation only" + }, + { + "pr": 2266, + "head": "9382f0d9796cd58831f876943162c536fa14cfd5", + "author": "1337isnot1337", + "role": "full GF4 two-source demand with a different scalar-source alphabet; citation only" + }, + { + "pr": 4256, + "author": "Nick Petalas", + "role": "full coefficient demand with unsigned calls; citation only" + } + ] +} diff --git a/research/signed-prime-connector/VERIFY.json b/research/signed-prime-connector/VERIFY.json new file mode 100644 index 0000000000..b8a6fdb7b7 --- /dev/null +++ b/research/signed-prime-connector/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Closed-form signed words and independent difference coverage; literal dirty coefficient ledger; complete p=3,5 short-path censuses; ten dense singular noncommuting fixtures and ten rejection controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "The same scientific checks with optimization enabled; contracts use explicit exceptions." + } + ] +} diff --git a/research/signed-prime-connector/verify.py b/research/signed-prime-connector/verify.py new file mode 100644 index 0000000000..0d97ace28f --- /dev/null +++ b/research/signed-prime-connector/verify.py @@ -0,0 +1,268 @@ +#!/usr/bin/env python3 +"""Exact signed two-source full-coefficient connector checks. + +Produced by Nick Petalas. Apache-2.0. +""" + +import hashlib +import itertools +import json +from pathlib import Path +import random +import sys + + +PRIMES = (3, 5, 7, 11, 13) +MAX_PRIME = 31 +PACKAGE_FILES = ("README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def check_prime(p): + require(isinstance(p, int) and 3 <= p <= MAX_PRIME and p % 2 == 1, + "prime outside executable odd-prime domain") + require(all(p % d for d in range(2, p)), "composite modulus") + + +def source_path(p): + check_prime(p) + h = (p - 1) // 2 + return [("B", 0, 1)] * h + [("B", 1, 1)] * h + [ + ("B", 0, -1)] * h + [("B", 1, -1)] * h + + +def vertices(path): + require(len(path) <= 2 * MAX_PRIME, "source path too long") + result = [(0, 0)] + q = [0, 0] + for kind, j, sign in path: + require(kind == "B" and j in (0, 1) and sign in (-1, 1), "bad source event") + q[j] += sign + result.append(tuple(q)) + return result + + +def rows(p): + check_prime(p) + return [v for v in itertools.product(range(p), repeat=2) if v != (0, 0)] + + +def readout_pair(v, p): + """Return perimeter points P,Q with P-Q congruent to v, without a search.""" + h = (p - 1) // 2 + a, b = (x if x <= h else x - p for x in v) + reverse = a < 0 + if reverse: + a, b = -a, -b + if b >= 0: + positive, negative = (a, h), (0, h - b) + else: + positive, negative = (a, 0), (0, -b) + if reverse: + positive, negative = negative, positive + require(tuple((x - y) % p for x, y in zip(positive, negative)) == v, + "closed-form pair has wrong coefficient") + return positive, negative + + +def compile_word(p): + path = source_path(p) + palette = vertices(path) + first = {} + for t, point in enumerate(palette): + if point not in first: + first[point] = t + slots = [[] for _ in palette] + targets = rows(p) + for index, v in enumerate(targets): + positive, negative = readout_pair(v, p) + require(positive in first and negative in first, "readout point off perimeter") + slots[first[positive]].append(("A", index, 1)) + slots[first[negative]].append(("A", index, -1)) + word = [] + for t, calls in enumerate(slots): + word.extend(calls) + if t < len(path): + word.append(path[t]) + require(palette[-1] == (0, 0), "connector not restored as an integer path") + require(len(word) == 2 * p * p + 2 * p - 4, "incorrect full call count") + return targets, word + + +def symbolic_replay(p, targets, word): + """Track dirt, B0*x0 and B1*x1, with the distinct A_v always on the left.""" + check_prime(p) + require(0 < len(targets) < MAX_PRIME ** 2, "target capacity exceeded") + require(len(word) <= 2 * MAX_PRIME ** 2 + 2 * MAX_PRIME, + "word capacity exceeded") + q = [1, 0, 0] + out = [[0, 0, 0] for _ in targets] + for kind, j, sign in word: + require(sign in (-1, 1), "invalid sign") + if kind == "B": + require(j in (0, 1), "invalid source") + q[j + 1] = (q[j + 1] + sign) % p + else: + require(kind == "A" and 0 <= j < len(targets), "invalid readout") + out[j] = [(x + sign * y) % p for x, y in zip(out[j], q)] + require(q == [1, 0, 0], "connector restoration failed") + require(out == [[0, *v] for v in targets], "dirty target action failed") + + +def difference_set(points, p): + return {((x[0] - y[0]) % p, (x[1] - y[1]) % p) + for x in points for y in points} + + +def check_constructions(): + report = [] + for p in PRIMES: + targets, word = compile_word(p) + symbolic_replay(p, targets, word) + points = vertices(source_path(p)) + require(len(difference_set(points, p)) == p * p, "incomplete difference set") + source_counts = [sum(kind == "B" and j == k for kind, j, _ in word) + for k in (0, 1)] + require(source_counts == [p - 1, p - 1], "wrong source counts") + report.append({"p": p, "targets": len(targets), "calls": len(word), + "source_calls": sum(source_counts)}) + return report + + +def check_short_paths(p): + """Census every signed source word shorter than the proposed source optimum.""" + require(p in (3, 5), "census domain is p=3,5") + letters = (("B", 0, 1), ("B", 0, -1), ("B", 1, 1), ("B", 1, -1)) + visited, closed, smallest_missing = 0, 0, p * p + for length in range(2 * (p - 1)): + for path in itertools.product(letters, repeat=length): + visited += 1 + points = vertices(path) + if any(x % p for x in points[-1]): + continue + closed += 1 + counts = [sum(event[1] == j for event in path) for j in (0, 1)] + j = 0 if counts[0] <= counts[1] else 1 + require(counts[j] <= p - 2 and counts[j] % 2 == 0, + "short coordinate count lemma failed") + values = [q[j] for q in points] + require(2 * (max(values) - min(values)) <= counts[j], + "closed integer walk range lemma failed") + missing = p * p - len(difference_set(points, p)) + require(missing >= 2 * p, "paired-readout deficit lemma failed") + require(length + missing > 2 * (p - 1), "all-word excess bound failed") + smallest_missing = min(smallest_missing, missing) + expected_visited = sum(4 ** k for k in range(2 * (p - 1))) + require(visited == expected_visited, "census incomplete") + return {"p": p, "visited": visited, "closed": closed, + "smallest_missing": smallest_missing} + + +def matvec(matrix, vector, p): + return [sum(a * b for a, b in zip(row, vector)) % p for row in matrix] + + +def matmul(a, b, p): + return [[sum(x * y for x, y in zip(row, column)) % p + for column in zip(*b)] for row in a] + + +def dense_case(p, dimension): + require(p in PRIMES and dimension in (2, 3), "dense fixture outside bounds") + targets, word = compile_word(p) + rng = random.Random(100 * p + dimension) + b = [[[int(r == 0 and c == 1) for c in range(dimension)] + for r in range(dimension)], + [[int(r == 1 and c == 0) for c in range(dimension)] + for r in range(dimension)]] + a = [[[rng.randrange(p) for _ in range(dimension)] + for _ in range(dimension)] for _ in targets] + require(any(matmul(matrix, b[0], p) != matmul(b[0], matrix, p) for matrix in a), + "fixture lacks noncommuting maps") + x = [[rng.randrange(p) for _ in range(dimension)] for _ in (0, 1)] + z0 = [1] + [rng.randrange(p) for _ in range(dimension - 1)] + incoming = [[rng.randrange(p) for _ in range(dimension)] for _ in targets] + bx = [matvec(matrix, value, p) for matrix, value in zip(b, x)] + z, out = list(z0), [list(value) for value in incoming] + for kind, j, sign in word: + if kind == "B": + z = [(old + sign * value) % p for old, value in zip(z, bx[j])] + else: + out[j] = [(old + sign * value) % p + for old, value in zip(out[j], matvec(a[j], z, p))] + require(z == z0, "dense dirty connector not restored") + for index, v in enumerate(targets): + required = [(v[0] * u + v[1] * w) % p for u, w in zip(*bx)] + expected = [(old + value) % p for old, value in + zip(incoming[index], matvec(a[index], required, p))] + require(out[index] == expected, "dense noncommuting target mismatch") + + +def check_controls(): + targets, word = compile_word(5) + first_a = next(i for i, event in enumerate(word) if event[0] == "A") + first_b = next(i for i, event in enumerate(word) if event[0] == "B") + mutants = [] + for position in (first_a, first_b): + mutants.append((5, word[:position] + word[position + 1:])) + changed = list(word) + kind, j, sign = changed[position] + changed[position] = kind, j, -sign + mutants.append((5, changed)) + changed = list(word) + kind, j, sign = changed[first_a] + changed[first_a] = kind, (j + 1) % len(targets), sign + mutants.append((5, changed)) + mutants.append((5, [event for event in word if event[:2] != ("A", 0)])) + mutants.append((7, word)) + rejected = 0 + for modulus, mutant in mutants: + try: + symbolic_replay(modulus, targets, mutant) + except ValueError: + rejected += 1 + else: + raise ValueError("semantic mutant accepted") + for invalid in (2, 9, 33): + try: + source_path(invalid) + except ValueError: + rejected += 1 + else: + raise ValueError("invalid modulus accepted") + require(rejected == 10, "control inventory changed") + return rejected + + +def file_hashes(): + package = Path(__file__).resolve().parent + result = {} + for name in PACKAGE_FILES: + path = package / name + require(path.is_file() and path.stat().st_size <= 1024 * 1024, + "missing or oversized package file") + result[name] = hashlib.sha256(path.read_bytes()).hexdigest() + return result + + +def main(): + constructions = check_constructions() + census = [check_short_paths(p) for p in (3, 5)] + for p in PRIMES: + for dimension in (2, 3): + dense_case(p, dimension) + controls = check_controls() + receipt = {"claim_type": "scoped proof with finite corroboration", + "constructions": constructions, "short_path_census": census, + "dense_cases": 2 * len(PRIMES), "rejected_controls": controls, + "python": sys.version.split()[0], "sha256": file_hashes()} + print(json.dumps(receipt, sort_keys=True)) + print("PASS_SIGNED_PRIME_CONNECTOR p5_calls=56 primes=5 dense_cases=10 controls=10") + + +if __name__ == "__main__": + main()