diff --git a/research/gf8-two-source-optimum/README.md b/research/gf8-two-source-optimum/README.md new file mode 100644 index 0000000000..1fa6ce8548 --- /dev/null +++ b/research/gf8-two-source-optimum/README.md @@ -0,0 +1,224 @@ +# Exact 140-call two-source GF(8) connector + +This contribution was produced by Nick Petalas. It is a scoped mathematical +proof with a finite explicit construction. The two-source scalar-update dirty +connector over GF(8), requesting all 63 nonzero coefficient pairs, has exact +unit complete-call optimum **140**. The lower bound allows arbitrary readout +counts, rather than assuming paired readouts. The explicit axis comparator +uses 142 calls. No supplier admission or new kappa is claimed. + +The new step groups Aaron Wang's PR2128 binary walk into two field coordinates, +then transfers the existing all-word tariff argument of Tairitsu-Aya PR2156 +and Cinna Davis PR2249 to this field-linear contract. The walk and that counting +argument are credited predecessor work. Unpaidmoon's PR4651 exclusion of +twelve- and thirteen-point difference bases is a cited mathematical dependency, +not a result reverified by this package. + +## Contract + +Write K=GF(8)=F2[t]/(t^3+t+1). An integer a from 0 through 7 encodes the +coefficients of 1,t,t^2 in its three bits. There are two immutable sources +x0,x1, one borrowed arbitrarily dirty connector z, and 63 distinct arbitrarily +dirty outputs y_v, for v=(u,w) in K^2 other than zero. For arbitrary compatible +K-linear maps B0,B1,A_v, the requested endpoint is + +```text +y_v += A_v(u B0 x0 + w B1 x1) +x0, x1 and z unchanged +``` + +Only these atomic complete calls are allowed: + +```text +S(j,a): z += a Bj xj j in {0,1}, a in K minus {0} +R(v): y_v += A_v z +``` + +Calls preserve every other row and restore their private scratch and required +entry/exit heads. Each scaled S call has its own complete price, including +scalar preparation and multiplication. Readouts have coefficient one. The word +is independent of data and map entries. Outputs cannot be read or used as +workspace. There is no connector scaling, source mutation, additional root, +direct A_v Bj call, free conversion or combined readout. The 140 optimum assigns +unit price to every complete call. Unequal physical prices are separate. + +This extends Cinna Davis's PR2266 GF(4) scalar-source interface to a different +field and full coefficient demand. It is not the binary six-independent-source +DUO contract: the three basis components of each field source share one Bj. + +## Construction and arbitrary-dirt identity + +Interpret a six-bit mask as its low three bits u and high three bits w. The +source steps and nonterminal prefixes are Aaron Wang's PR2128 word: + +```text +steps 2 16 8 16 1 4 48 4 3 4 32 8 4 16 +prefixes 0 2 18 26 10 11 15 63 59 56 60 28 20 16 +``` + +Every step lies wholly in one three-bit group, including 3 and 48. Thus every +step is one legal S(j,a), rather than a bundle of distinct map applications. +There are seven calls to each Bj. The final prefix is zero. The 91 unordered +pairs of distinct nonterminal prefixes contain all 63 nonzero differences. +The verifier enumerates those 91 pairs and emits the first boundary pair for +each mask in its generated receipt. + +At prefix q=(q0,q1), the connector is exactly +`z_initial + q0 B0 x0 + q1 B1 x1`. For each v choose prefix boundaries s,t +with q_s+q_t=v, and call R(v) at both. Their incoming dirt terms cancel in +characteristic two. Linearity leaves exactly the specified output update, +with A_v on the left of each Bj. Different readouts preserve z and have +distinct targets, so all pairs can be interleaved in chronological boundary +order. This proves the identity for every row length and every allowed map, +including singular and noncommuting maps. It uses fourteen source calls and +126 readouts, totaling 140. Each elementary update is an involution; reversing +the program restores the full initial state. + +For comparison, traverse the reflected three-bit Gray cycle on the first +coordinate, then on the second: + +```text +source-0 coefficients 1 2 1 4 1 2 1 4 +source-1 coefficients 1 2 1 4 1 2 1 4 +``` + +Its prefixes contain both complete coordinate axes. Every (u,w) is a difference +of two axis points, giving the same 126 paired readouts with sixteen source +calls and 142 total calls. The new verifier constructs and checks this +comparator directly, without running a predecessor program. + +## All-word lower bound + +Specialize to scalar identity maps and independently variable x0,x1,z_initial. +Any correct word must have zero final source prefix and an even number of +readouts for every output. Each nonzero output needs at least two readouts. +With exactly two, its requested vector is a difference of two source prefixes. +A vector absent from that difference set therefore requires at least four. +This reasoning allows repeated boundary readouts and arbitrarily many calls. + +Let b be the source-call count. A closed b-step word has at most b distinct +nonterminal prefixes. Let m be the number of nonzero vectors absent from their +pairwise differences. Every word costs at least `b + 126 + 2m`. + +- If b>=14, the bound is already 140. +- If b=12 or 13, PR4651's cited theorem says no set of at most thirteen + points covers K^2=F2^6 by differences. A smaller set can be enlarged, so the + theorem covers repeated-prefix paths as well. Hence m>=1. The bills are + at least 140 and 141, respectively. +- If 0<=b<=11, there are at most b(b-1)/2 nonzero differences. Thus + `b+126+2m >= b+126+2(63-b(b-1)/2)`. The minimum of these twelve integer + expressions is 153, attained at b=11. + +This is the PR2156/PR2249 counting argument applied to the additive coefficient +group of the field-linear contract. The construction attains 140. The claim depends +on the cited PR4651 set exclusion. Its census and historical suites are not +executed here. Finite construction checks do not independently certify that +dependency or the universal written argument. + +## Complete price and storage boundary + +Let c_(j,a) be the complete scaled source-call price and r_v the complete +readout price. Let I pay admission and program construction, P pay external +coefficient preparation, and D pay instruction storage/access/dispatch. The +displayed construction has the explicit bill + +```text +C = I + P + D + + c_(0,1) + c_(0,2) + c_(0,3) + 4 c_(0,4) + + 2 c_(1,1) + 3 c_(1,2) + c_(1,4) + c_(1,6) + + 2 sum_(v != 0) r_v. +``` + +No nonunit scalar is free. A tag bit, one source bit and three coefficient +bits encode each S; a tag bit and six target bits encode each R. The actual +140-event stream needs 952 bits, versus 962 for the axis stream, before +framing or external interpreter storage. Boundary order is encoded by the +stream. No runtime pair-lookup oracle is assumed. There are 66 length-L data +rows, or 198L field-data bits, plus each child's separately charged private +scratch and control storage. No extra full row is introduced. + +At equal complete call prices the construction saves two calls. It need not +beat the axis word for unequal c_(j,a). Coefficient acquisition, physical +scaled-map services, frames, stock, precision and tape costs are unknown at a +selected supplier. There is no identified real consumer or complete supplier +invoice. The family decision is to finish this local result and stop. + +## Reproduction and coverage + +From the repository root, using CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/gf8-two-source-optimum/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/gf8-two-source-optimum/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/gf8-two-source-optimum +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/gf8-two-source-optimum --check-source-history --check-modes +``` + +An installed CPython 3.12 can replace that interpreter path. The verifier writes +no files. It prints a generated JSON receipt bound to all five package hashes, +the full boundary-pair certificate and the marker + +```text +PASS_GF8_TWO_SOURCE_OPTIMUM calls=140 sources=14 readouts=126 dense=399 controls=283 cited_lower_bound=PR4651 +``` + +Checks include all 64 products under two GF(8) multiplication implementations, +1,024 associativity/distributivity instances, seven inverse counts, free +noncommutative map endpoints in both directions and the axis comparator. Dense +replay uses separate polynomial arithmetic, all 396 basis columns and three +mixed dirty states across dimensions one, two and three. It checks forward and +inverse endpoints for all 399 inputs. All 140 call omissions, fourteen changed +source coefficients, 126 changed readout destinations and three malformed +source words must be rejected. Checks remain active under Python -O. + +The code has no recursion or subprocesses. Every loop is bounded by the fixed +field, at most 142 calls, 66 roles, matrix dimension at most three or five +package files of at most 200 KB. Every function is below sixty lines. +Python-managed allocation is a Power of Ten rule 3 deviation. Symbolic live +storage has at most four terms per output; dense row storage has at most 198 +field entries per state. The declared limits and sixty-second replay timeout +bound this offline verifier. Fixed-capacity storage should be reconsidered if +it becomes an online service. Warning-strict normal and optimized execution +are the available diagnostics; no project Python linter/type checker is +configured for this package. + +## Sources, scope and credit + +Produced by Nick Petalas. Aaron Wang / navinor PR2128 supplies the fourteen-step +walk. Tairitsu-Aya PR2156 and Cinna Davis PR2249 supply the existing all-readout +counting argument in the binary-source model. Cinna Davis / 1337isnot1337 +PR2266 supplies the paid single-source scalar +interface over GF(4). Unpaidmoon PR4651 supplies the cited difference-basis +exclusion and credits Volodymyr Gavrylkiv for the known set-level value. Ross +Richardson PR934/PR943 supplies the dirty-connector and prefix-readout lineage; +Aaron Wang's DUO work retains that lineage. All predecessor credit remains +unchanged. The new field grouping, exact field-linear tariff consequence, price +expression and verifier are the contribution here; the underlying binary walk, +counting argument and difference-basis value are not claimed as new. + +SOURCES.json pins the four predecessor READMEs, catalogue and selected-record +context at main e54523517d0f03e58352e647c403a5af3e525a57. The selected result is +#7000, conditional kappa 0.00363005817 under five retained assumptions. The +catalogue's revision-8 assessment predates that selection. This package changes +none of those inputs. TASK.json records the changed card scope and advance +[claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19540626). + +The card's historical orientation control passed with 945 pairings, maximum +coverage 31 and 74 calls. It is not the contribution or a dependency replay. +No other predecessor scientific suite, proof-kernel build, independent human review, +native/supplier replay, physical tape implementation, selected cold replay or +complete multiplication theorem is supplied. Hosted CI is separate from local +checks. Independent human and formal proof-kernel review are unclaimed. +Apache-2.0. + +## Open next questions + +- Does a source-pinned recursive caller expose this GF(8)-linear boundary at a + favorable full invoice? First identify the maps and price every scaled source + event, readout, admission, preparation, dispatch and dirty return. No such + caller or scalar service is known here. +- What is the optimum with unequal complete scaled-event prices? Begin with a + real tariff and the displayed fourteen-step and sixteen-step words. The + unit-call theorem does not settle this comparison. + +The questions, relevance, first steps and blockers are also in TASK.json. diff --git a/research/gf8-two-source-optimum/SOURCES.json b/research/gf8-two-source-optimum/SOURCES.json new file mode 100644 index 0000000000..4a3b45dded --- /dev/null +++ b/research/gf8-two-source-optimum/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/connector-six-source-duo/README.md", + "usage": "input", + "git_blob": "9855372446ed4ecd9d91c0f7afee1932e2c2d61a", + "sha256": "f338d940075ba3782da276abf69b9578d3b1a4daaa285960cf168480d8f7c486" + }, + { + "path": "research/f2-six-difference-basis/README.md", + "usage": "input", + "git_blob": "71ed2d97bb74a0bdbba0ad64f71b19e9daf52487", + "sha256": "f3693dd75598a4c3baeb1f9dde4dba739d7812c106dccfb1b4a5dfb2d27e21a6" + }, + { + "path": "research/gf4-scalar-source-connector-seeda472dd8c/README.md", + "usage": "input", + "git_blob": "2fb5391b274a9959fc26495405387a7983a1d108", + "sha256": "37f55b37d63bd90a9c601f97179f399d53e0965db795561044c1879be5351dbf" + }, + { + "path": "research/six-source-duo-add16-floor/README.md", + "usage": "input", + "git_blob": "a0ad8d5dd5faf384791a34feb11d767cc8d75814", + "sha256": "22a48c4a74d1687d91dd650a02456011ff0dbc5f2d6d0f5249c089b9865d8acd" + } + ] +} diff --git a/research/gf8-two-source-optimum/TASK.json b/research/gf8-two-source-optimum/TASK.json new file mode 100644 index 0000000000..172d9cf332 --- /dev/null +++ b/research/gf8-two-source-optimum/TASK.json @@ -0,0 +1,73 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "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 all-word unit-call optimum for the GF(8) two-source scalar-update dirty connector with all 63 nonzero coefficient rows.", + "scope_change_reason": "The added scalar source family of PR2266 is interpreted over GF(8), with full coefficient demand; this is a local interface theorem rather than supplier admission.", + "bottleneck_link": "A field-linear caller could save two complete source calls relative to an axis walk. No such selected supplier seam or complete physical bill is supplied.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified 140-call word and matching all-word lower bound. Do not extend to larger fields or suppliers.", + "outcome": "completed", + "evidence": "Free noncommutative GF(8) endpoints; separate polynomial-product dense forward/inverse replay; omitted-call and changed-call controls. PR4651 lower bound is cited, not recertified. Tairitsu-Aya PR2156 and Cinna Davis PR2249 already give the binary all-readout counting argument; only its transfer to the field-linear contract is used.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does a source-pinned recursive caller expose this GF(8)-linear two-source interface at favorable complete prices?", + "why_it_matters": "Only a compatible caller can convert the two-call saving into a recursive invoice change.", + "first_step": "Specify the two source maps and 63 readout maps, then price all scaled source events, admission, preparation, dispatch and dirty restoration.", + "blocked_by": "No such physical caller or native scalar service has been supplied." + }, + { + "question": "What is the optimum with unequal complete prices for individual scaled source events?", + "why_it_matters": "Unit-call optimality does not compare scalar preparation and routing charges.", + "first_step": "Supply a concrete tariff and compare the displayed fourteen-step word with the explicit sixteen-step axis word, including readout and descriptor charges.", + "blocked_by": "Meaningful physical prices are unknown." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19540626", + "question_source": "original", + "predecessor_author": "navinor", + "first_working_example": "Selected metadata baseline PASS_RESEARCH_BASELINE_BINDINGS_ONLY; the historical card orientation control passed with pairings=945 max_coverage=31 queries=74 leaves=182. This is orientation, not the contribution.", + "claim_type": "scoped proof with finite construction" +} diff --git a/research/gf8-two-source-optimum/VERIFY.json b/research/gf8-two-source-optimum/VERIFY.json new file mode 100644 index 0000000000..b992aeca82 --- /dev/null +++ b/research/gf8-two-source-optimum/VERIFY.json @@ -0,0 +1,39 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/connector-six-source-duo/README.md", + "research/f2-six-difference-basis/README.md", + "research/gf4-scalar-source-connector-seeda472dd8c/README.md", + "research/six-source-duo-add16-floor/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact GF(8) construction, free-map forward/inverse endpoints, dense basis and dirty cases, axis comparator, all omission/change controls and generated hash receipt. The PR4651 lower bound is cited only." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Repeat every check with interpreter assertions disabled." + } + ] +} diff --git a/research/gf8-two-source-optimum/verify.py b/research/gf8-two-source-optimum/verify.py new file mode 100644 index 0000000000..826158e15e --- /dev/null +++ b/research/gf8-two-source-optimum/verify.py @@ -0,0 +1,253 @@ +"""Exact GF(8) connector construction, produced by Nick Petalas. Apache-2.0.""" + +import hashlib +import json +import platform +from pathlib import Path + + +# Group bits 0,1,2 and 3,4,5 of Aaron Wang's PR2128 word separately. +STEPS = (2, 16, 8, 16, 1, 4, 48, 4, 3, 4, 32, 8, 4, 16) +PACKAGE = Path(__file__).resolve().parent + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def multiply(a, b): + """Polynomial basis 1,t,t^2, with t^3=t+1; inputs are field encodings.""" + need(0 <= a < 8 and 0 <= b < 8, "invalid field element") + result = 0 + for _ in range(3): + if b & 1: + result ^= a + b >>= 1 + a <<= 1 + if a & 8: + a ^= 11 + return result + + +def reference_multiply(a, b): + result = 0 + for i in range(3): + for j in range(3): + result ^= ((a >> i & 1) & (b >> j & 1)) << (i + j) + for degree in (4, 3): + if result >> degree & 1: + result ^= 11 << (degree - 3) + return result + + +def field_checks(): + for a in range(8): + for b in range(8): + need(multiply(a, b) == reference_multiply(a, b), "field product") + for c in range(8): + need(multiply(multiply(a, b), c) == multiply(a, multiply(b, c)), + "field associativity") + need(multiply(a, b ^ c) == multiply(a, b) ^ multiply(a, c), + "field distributivity") + for a in range(1, 8): + need(sum(multiply(a, b) == 1 for b in range(1, 8)) == 1, "field inverse") + return 64, 1024, 7 + + +def source_events(steps): + need(len(steps) <= 16, "source word limit") + events = [] + for step in steps: + need(0 < step < 64, "invalid source step") + low, high = step & 7, step >> 3 + need(bool(low) != bool(high), "a source call changes two coordinates") + events.append(("B", int(bool(high)), high or low)) + return events + + +def compile_word(steps): + sources = source_events(steps) + prefixes = [0] + for step in steps: + prefixes.append(prefixes[-1] ^ step) + need(prefixes[-1] == 0, "connector not restored") + pairs = {} + for s in range(len(steps)): + for t in range(s + 1, len(steps)): + mask = prefixes[s] ^ prefixes[t] + if mask: + pairs.setdefault(mask, (s, t)) + need(set(pairs) == set(range(1, 64)), "missing coefficient row") + program = [] + for boundary in range(len(steps) + 1): + for mask in range(1, 64): + if boundary in pairs[mask]: + program.append(("A", mask, 1)) + if boundary < len(sources): + program.append(sources[boundary]) + need(len(program) <= 142, "program limit") + return tuple(program), prefixes, pairs + + +def add_expression(target, source, coefficient, operator): + for (word, origin), value in source.items(): + key = ((operator,) + word, origin) + new = target.get(key, 0) ^ multiply(coefficient, value) + if new: + target[key] = new + else: + target.pop(key, None) + + +def symbolic_endpoint(program): + """Free, noncommutative map words on 66 independent incoming roles.""" + need(len(program) <= 142, "symbolic program limit") + state = [{((), role): 1} for role in range(66)] + for kind, role, coefficient in program: + if kind == "B": + add_expression(state[2], state[role], coefficient, ("B", role)) + else: + need(kind == "A" and 1 <= role <= 63, "invalid readout") + add_expression(state[role + 2], state[2], coefficient, ("A", role)) + expected = [{((), role): 1} for role in range(66)] + for mask in range(1, 64): + for source, coefficient in enumerate((mask & 7, mask >> 3)): + if coefficient: + key = ((("A", mask), ("B", source)), source) + expected[mask + 2][key] = coefficient + return state == expected + + +def apply_matrix(matrix, vector): + result = [] + for row in matrix: + value = 0 + for coefficient, entry in zip(row, vector, strict=True): + value ^= reference_multiply(coefficient, entry) + result.append(value) + return result + + +def dense_program(program, initial, sources, readers): + state = [row[:] for row in initial] + for kind, role, coefficient in program: + if kind == "B": + value = apply_matrix(sources[role], state[role]) + destination = 2 + else: + value = apply_matrix(readers[role - 1], state[2]) + destination = role + 2 + for i in range(len(value)): + state[destination][i] ^= reference_multiply(coefficient, value[i]) + return state + + +def dense_expected(initial, sources, readers): + result = [row[:] for row in initial] + values = [apply_matrix(sources[j], initial[j]) for j in range(2)] + for mask in range(1, 64): + combination = [reference_multiply(mask & 7, a) + ^ reference_multiply(mask >> 3, b) + for a, b in zip(*values, strict=True)] + update = apply_matrix(readers[mask - 1], combination) + result[mask + 2] = [a ^ b for a, b in + zip(initial[mask + 2], update, strict=True)] + return result + + +def dense_checks(program): + count = 0 + for dimension in (1, 2, 3): + sources = [[[int(i == j) ^ int(i == 0 and j == dimension - 1) + for j in range(dimension)] for i in range(dimension)], + [[int(i == j) ^ int(i == dimension - 1 and j == 0) + for j in range(dimension)] for i in range(dimension)]] + readers = [[[(mask * (i + 1) + j * j + 3 * j) % 8 + for j in range(dimension)] for i in range(dimension)] + for mask in range(1, 64)] + for column in range(66 * dimension + 1): + initial = [[0] * dimension for _ in range(66)] + if column < 66 * dimension: + initial[column // dimension][column % dimension] = 1 + else: + initial = [[(role * 5 + i * 3 + 7) % 8 + for i in range(dimension)] for role in range(66)] + expected = dense_expected(initial, sources, readers) + actual = dense_program(program, initial, sources, readers) + need(actual == expected, "dense forward endpoint") + need(dense_program(tuple(reversed(program)), actual, sources, readers) + == initial, "dense inverse endpoint") + count += 1 + return count + + +def mutation_checks(program): + count = 0 + for index, (kind, role, coefficient) in enumerate(program): + need(not symbolic_endpoint(program[:index] + program[index + 1:]), + "undetected omitted call") + count += 1 + replacement = ((kind, role, coefficient % 7 + 1) if kind == "B" + else (kind, role % 63 + 1, coefficient)) + mutant = program[:index] + (replacement,) + program[index + 1:] + need(not symbolic_endpoint(mutant), "undetected changed call") + count += 1 + for steps in (STEPS[:-1], STEPS + (9,), (1,) * 14): + try: + compile_word(steps) + except ValueError: + count += 1 + else: + raise ValueError("undetected malformed source word") + return count + + +def hashes(): + result = {} + for name in ("README.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py"): + with (PACKAGE / name).open("rb") as stream: + data = stream.read(200_001) + need(len(data) <= 200_000, "package file size limit") + result[name] = hashlib.sha256(data).hexdigest() + return result + + +def main(): + products, laws, inverses = field_checks() + program, prefixes, pairs = compile_word(STEPS) + need(len(program) == 140 and len(set(prefixes[:-1])) == 14, "word shape") + need(symbolic_endpoint(program), "free-map endpoint") + need(symbolic_endpoint(tuple(reversed(program))), "free-map inverse") + gray = (1, 2, 1, 4, 1, 2, 1, 4) + baseline, _, _ = compile_word(gray + tuple(8 * step for step in gray)) + need(len(baseline) == 142 and symbolic_endpoint(baseline), "axis comparator") + # Transfer PR2156/PR2249's counting argument to the field contract. + # PR4651's no-12/no-13 theorem is CITED; its census is not executed. + short_bounds = [b + 126 + 2 * max(0, 63 - b * (b - 1) // 2) + for b in range(12)] + need(min(short_bounds) == 153, "short-word arithmetic") + need(12 + 126 + 2 == 140 and 13 + 126 + 2 == 141, "cited-bound arithmetic") + receipt = {"claim_type": "scoped proof with finite construction", + "dependency": "PR4651 difference-basis exclusion, cited only", + "field_products": products, "field_laws": laws, + "field_inverses": inverses, "source_calls": 14, + "source_calls_by_role": [sum(e[:2] == ("B", j) for e in program) + for j in range(2)], + "readouts": 126, "complete_calls": len(program), + "axis_comparator_calls": len(baseline), + "descriptor_bits": sum(5 if e[0] == "B" else 7 for e in program), + "axis_descriptor_bits": sum(5 if e[0] == "B" else 7 + for e in baseline), + "prefixes": prefixes, "pairs": pairs, + "dense_forward_inverse_cases": dense_checks(program), + "rejected_mutations": mutation_checks(program), + "python": platform.python_version(), "sha256": hashes()} + print(json.dumps(receipt, sort_keys=True)) + print("PASS_GF8_TWO_SOURCE_OPTIMUM calls=140 sources=14 readouts=126 " + f"dense={receipt['dense_forward_inverse_cases']} " + f"controls={receipt['rejected_mutations']} cited_lower_bound=PR4651") + + +if __name__ == "__main__": + main()