diff --git a/research/fixed-fourteen-basis-walk/README.md b/research/fixed-fourteen-basis-walk/README.md new file mode 100644 index 0000000000..9272f8dcce --- /dev/null +++ b/research/fixed-fourteen-basis-walk/README.md @@ -0,0 +1,175 @@ +# Sharp walk costs for the displayed fourteen-point difference basis + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Scoped proof with exact finite corroboration; no new kappa.** For the literal +six-source prefix set displayed in unpaidmoon's merged +[#4651](https://github.com/CrocSwap/integer-mult-bounds/pull/4651), + +```text +P = {0,1,2,3,4,5,6,8,16,24,32,40,48,63}, +``` + +the smallest possible maximum step weight of a fourteen-step closed walk is +four. Its minimum total number of source-map applications is twenty. Allowing +extra intermediate prefixes and arbitrarily many steps cannot lower twenty. +The fixed set therefore cannot match the generic six-source DUO construction's +sixteen source applications, even if arbitrary atomic source bundles are allowed. + +This answers the displayed-witness first step of #4651 Open next question 1. +It does not exclude a different fourteen-point basis with steps of weight at +most three. Aaron Wang's #2128 already attains the generic `(140 queries, +142 map additions)` optimum established by Tairitsu-Aya's #2156. Those results +are cited premises, not replayed here. No new generic optimum is claimed. + +## Contract + +There are six immutable source rows `x_j`, a dirty connector `z`, and 63 dirty +target rows `y_m`, with arbitrary compatible binary linear maps `B_j,A_m`. +The required update is `y_m += A_m(sum_j m_j B_j x_j)`, with sources and +connector restored. The permitted new atomic source call has a nonempty mask S: + +```text +B_S: z += sum_(j in S) B_j x_j. +``` + +It costs one root call and `|S|` source-map applications. An `A_m` readout +costs one root call and one output-map application. Outputs are read exactly +twice and are observed only after completion. No partial sums inside an atomic +call are observable. Every map application is charged, even within a bundle. +These are abstract query and application counts; physical implementation, +dispatch, source/coefficient access, frame changes and hosting are additional. + +A source prefix q describes `z = z_initial + sum_j q_j B_j x_j`. A step from +u to v has mask `u XOR v`, hence application cost its Hamming weight. Two +readouts at prefixes u,v produce mask `u XOR v` and cancel connector dirt. +This is Ross Richardson's paired-readout reduction, used as a premise. + +## Proof and attaining cycle + +Every element of `P` other than 63 has Hamming weight at most two. Therefore +its distance from 63 is at least four. Any fourteen-edge cycle visiting P +has two edges incident to 63, each costing at least four. Its other twelve +edges join distinct points and cost at least one. Thus every such cycle has +maximum edge weight at least four and total application cost at least + +```text +2*4 + 12*1 = 20. +``` + +Both bounds are attained simultaneously by + +```text +0,16,48,32,40,8,24,63,5,4,6,2,3,1,0. +``` + +The two nonsingleton edges are `24 XOR 63 = 39` and `63 XOR 5 = 58`, both of +weight four. All other edges have weight one. The six source occurrence +counts are `(4,4,2,2,4,4)`, so the connector is restored. This proves the +sharp arity and application claims without an exhaustive tour census. + +Now consider any finite closed walk visiting every point of P, with arbitrary +extra vertices, revisits, and step weights. Start at zero and retain the first +visit to each other required point, then the return to zero. Hamming distance +satisfies the triangle inequality, so replacing each intervening segment by a +single edge cannot increase its application bill. The resulting fourteen-edge +cycle visits exactly P and therefore costs at least twenty. The displayed +cycle proves equality for the larger walk class. The same lower bound holds +if only some readout boundaries are designated and extra boundaries are ignored. +This shortcut argument concerns application cost; it does not preserve an +arity restriction or root-call count. + +## Complete paired-readout word and consequence + +The verifier assigns each nonzero mask m the lexicographically first pair of +cycle boundaries with difference m. It puts the two `A_m` calls at those +boundaries. Its free-symbol replay checks all 63 endpoint identities, arbitrary +initial connector state and arbitrary initial target values. Linearity gives +the identity for all compatible source/output maps, including noncommuting +maps. The reverse query word is the inverse. + +This costs fourteen source root calls and 126 output root calls, for +`140 root queries`. Twenty source applications and 126 output applications +give `146 map applications`. The sharp fixed-set application floor is four +above the inherited generic DUO bill of 142. Changing the order, adding +intermediate vertices or allowing higher-arity bundles cannot remove that +fixed-set penalty. A different prefix set, coordinate change, output contract +or root architecture is outside the theorem. + +The decision is to stop optimizing this literal prefix set under the uniform +application tariff. The generic construction already has a lower bill. +This is a scoped obstruction to using this witness as the next construction, +not a new supplier or a universal barrier to six-source connectors. + +## Reproduction and evidence + +From the repository root, using the standard library and CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/fixed-fourteen-basis-walk +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/fixed-fourteen-basis-walk --check-source-history +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/fixed-fourteen-basis-walk/verify.py +``` + +The first and third commands also work with any installed CPython 3.12 path. +Expected direct marker: + +```text +PASS_FIXED_FOURTEEN_BASIS_WALK arity=4 source_apps=20 root_queries=140 map_apps=146 dense_cases=840 controls=163 +``` + +Normal and optimized registered commands regenerate and compare [RESULT.json](RESULT.json), +including five local file hashes. `--emit` writes the generated receipt to stdout. +A separately implemented Held--Karp recurrence over all subsets of the thirteen +nonzero terminals returns no arity-three tour and cost twenty at arities four +and six. Its finite-state counts are recorded in the receipt. It corroborates +the proof; the arbitrary-length claim rests on the written shortcut argument. + +The literal word is also replayed forward and backward on every basis input of +70 dirty rows at dimensions one, two and three, for 840 cases. Controls reject +each of the 140 single-call omissions, all twenty omitted source components, +and three malformed cycles. No predecessor census is imported or rerun. +Independent human and formal proof-kernel review are unclaimed. Lean, Docker, +selected cold replay, physical bundle admission and complete multiplication +proof obligations are unrun and outside scope. + +Python's managed allocation is a Power-of-Ten deviation. All domains are fixed: +the largest DP has 8,192 rows of thirteen costs, each transition loop has at +most thirteen iterations, and dense replay has at most 210 basis inputs per +dimension. There is no recursion, dynamic code generation or external process +in the verifier. ValueError checks remain active under optimized Python. + +## Sources and overlap + +Base canonical main is `624de9dc66858af0945e5f8a0942488d62280d43`, priority +revision 7. [TASK.json](TASK.json) records the refined card, evidence and stop +rule. [SOURCES.json](SOURCES.json) pins predecessor READMEs as historical +provenance. They are not replay inputs. The literal set above defines the new +problem. The selected record remains unchanged. + +Live open PRs, active Discussions, latest handoffs, recent account submissions, +last-hour account posts, main-tree README searches and merged-term searches +were checked before claiming. The exact displayed set appeared only in #4651 +in the main README search. The cached card scan covered 426 open PRs and 3,959 +Discussion records, with complete remote pagination; 6,196 sparse local note +paths were omitted. That scan, arbitrary unsearched diffs and unpublished work +are limits on the overlap check, not a novelty certificate. +Claim: [handoff post](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19134568). + +Credit unpaidmoon #4651 for the literal basis and explicit next question; +Ross Richardson #934/#943 for the paired-readout interface; Aaron Wang #2128 +for the generic DUO construction; Tairitsu-Aya #2156 for its generic optimum; +and Volodymyr Gavrylkiv for the known six-dimensional difference-basis value, +as credited in #2156. Cinna Davis #2201 retains the distinct one-Q4 profile +obstruction. No new priority is claimed for Hamming shortcutting or Held--Karp. +The new result is the sharp routing cost and its consequence for this literal set. + +## Open next questions + +- Can an explicitly priced coordinate change make this same abstract basis + competitive? First name its source acquisition and restoration program and + charge every application and conversion. A free coordinate change is not + covered by the literal-coordinate theorem, and no such paid program is supplied. +- For a caller with unequal source prices, can this set beat another basis + after all root costs are included? First supply an actual caller and complete + tariff table. The unit-application result alone does not settle that comparison. diff --git a/research/fixed-fourteen-basis-walk/RESULT.json b/research/fixed-fourteen-basis-walk/RESULT.json new file mode 100644 index 0000000000..d2629ef0e0 --- /dev/null +++ b/research/fixed-fourteen-basis-walk/RESULT.json @@ -0,0 +1,357 @@ +{ + "claim_type": "scoped proof with exact finite corroboration", + "cycle": [ + 0, + 16, + 48, + 32, + 40, + 8, + 24, + 63, + 5, + 4, + 6, + 2, + 3, + 1, + 0 + ], + "dense_forward_inverse_cases": 840, + "held_karp": { + "3": { + "cost": null, + "finite_states": 24114 + }, + "4": { + "cost": 20, + "finite_states": 51456 + }, + "6": { + "cost": 20, + "finite_states": 53248 + } + }, + "map_applications": 146, + "maximum_arity": 4, + "points": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 8, + 16, + 24, + 32, + 40, + 48, + 63 + ], + "readout_boundary_pairs": [ + [ + 0, + 13 + ], + [ + 0, + 11 + ], + [ + 0, + 12 + ], + [ + 0, + 9 + ], + [ + 0, + 8 + ], + [ + 0, + 10 + ], + [ + 8, + 11 + ], + [ + 0, + 5 + ], + [ + 5, + 13 + ], + [ + 5, + 11 + ], + [ + 5, + 12 + ], + [ + 5, + 9 + ], + [ + 5, + 8 + ], + [ + 5, + 10 + ], + [ + 2, + 7 + ], + [ + 0, + 1 + ], + [ + 1, + 13 + ], + [ + 1, + 11 + ], + [ + 1, + 12 + ], + [ + 1, + 9 + ], + [ + 1, + 8 + ], + [ + 1, + 10 + ], + [ + 4, + 7 + ], + [ + 0, + 6 + ], + [ + 6, + 13 + ], + [ + 6, + 11 + ], + [ + 6, + 12 + ], + [ + 6, + 9 + ], + [ + 6, + 8 + ], + [ + 6, + 10 + ], + [ + 3, + 7 + ], + [ + 0, + 3 + ], + [ + 3, + 13 + ], + [ + 3, + 11 + ], + [ + 3, + 12 + ], + [ + 3, + 9 + ], + [ + 3, + 8 + ], + [ + 3, + 10 + ], + [ + 6, + 7 + ], + [ + 0, + 4 + ], + [ + 4, + 13 + ], + [ + 4, + 11 + ], + [ + 4, + 12 + ], + [ + 4, + 9 + ], + [ + 4, + 8 + ], + [ + 4, + 10 + ], + [ + 1, + 7 + ], + [ + 0, + 2 + ], + [ + 2, + 13 + ], + [ + 2, + 11 + ], + [ + 2, + 12 + ], + [ + 2, + 9 + ], + [ + 2, + 8 + ], + [ + 2, + 10 + ], + [ + 5, + 7 + ], + [ + 1, + 4 + ], + [ + 7, + 10 + ], + [ + 7, + 8 + ], + [ + 7, + 9 + ], + [ + 7, + 12 + ], + [ + 7, + 11 + ], + [ + 7, + 13 + ], + [ + 0, + 7 + ] + ], + "rejected_controls": 163, + "root_queries": 140, + "source_applications": 20, + "source_occurrences": [ + 4, + 4, + 2, + 2, + 4, + 4 + ], + "source_sha256": { + "README.md": "766c9d1e208790e80e588b719d88549b86e793569395dc906b65906708e451cf", + "SOURCES.json": "b89f0ca41ff197d2ff295aa9226be9066ebb5d2a5f59df17ff597eb263daad30", + "TASK.json": "9c102ec8660c4b0e27158916fa8d5fe3f9031e44442031f053befd5160daf1a3", + "VERIFY.json": "d9002b245fbaf08a9945d5be5cb6cf8b04dc5d200267db195091784d9b96a3d8", + "verify.py": "f438306089983bd1ca82eca0d9fb78df17a7cfeb0f4e7a531bf25946ddf8e68a" + }, + "steps": [ + 16, + 32, + 16, + 8, + 32, + 16, + 39, + 58, + 1, + 2, + 4, + 1, + 2, + 1 + ], + "weights": [ + 1, + 1, + 1, + 1, + 1, + 1, + 4, + 4, + 1, + 1, + 1, + 1, + 1, + 1 + ] +} diff --git a/research/fixed-fourteen-basis-walk/SOURCES.json b/research/fixed-fourteen-basis-walk/SOURCES.json new file mode 100644 index 0000000000..503fbe235e --- /dev/null +++ b/research/fixed-fourteen-basis-walk/SOURCES.json @@ -0,0 +1,48 @@ +{ + "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/f2-six-difference-basis/README.md", + "usage": "provenance", + "git_blob": "71ed2d97bb74a0bdbba0ad64f71b19e9daf52487", + "sha256": "f3693dd75598a4c3baeb1f9dde4dba739d7812c106dccfb1b4a5dfb2d27e21a6" + }, + { + "path": "research/six-source-duo-add16-floor/README.md", + "usage": "provenance", + "git_blob": "a0ad8d5dd5faf384791a34feb11d767cc8d75814", + "sha256": "22a48c4a74d1687d91dd650a02456011ff0dbc5f2d6d0f5249c089b9865d8acd" + }, + { + "path": "research/connector-six-source-duo/README.md", + "usage": "provenance", + "git_blob": "9855372446ed4ecd9d91c0f7afee1932e2c2d61a", + "sha256": "f338d940075ba3782da276abf69b9578d3b1a4daaa285960cf168480d8f7c486" + }, + { + "path": "research/universal-connector-boundary/README.md", + "usage": "provenance", + "git_blob": "d277f7c5830b1f2bc42e1ff41ab86e7d7564929f", + "sha256": "23415f7829ab8d80a783142f10f7d31abbce84579362769984680af3df954476" + }, + { + "path": "research/connector-quad-six-seedde3f84/README.md", + "usage": "provenance", + "git_blob": "07910d4a19fb124869e0e057f84306c978eaa209", + "sha256": "46491c7919b5bccb25b80bbc3edb82ed45d4a57ec380f126407fbfcdb893f540" + } + ] +} diff --git a/research/fixed-fourteen-basis-walk/TASK.json b/research/fixed-fourteen-basis-walk/TASK.json new file mode 100644 index 0000000000..498459a372 --- /dev/null +++ b/research/fixed-fourteen-basis-walk/TASK.json @@ -0,0 +1,78 @@ +{ + "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": "refined", + "actual_scope": "Determine sharp maximum step arity and total source-application cost for the literal fourteen-point basis in #4651, allowing arbitrary extra intermediate vertices for the application bound.", + "scope_change_reason": "Refine the charged connector-alphabet card to the explicit fixed-witness routing question of another contributor. This does not redo a basis census or optimize over all prefix sets.", + "bottleneck_link": "The displayed set cannot attain the existing generic DUO invoice: its exact source cost is twenty, four above sixteen. This closes this fixed candidate under unit source prices and directs work to a changed set or a paid coordinate change.", + "budget_minutes": 60, + "stop_rule": "Stop at the first sharp fixed-set obstruction and attaining word. Do not optimize other bases, coordinate changes, unequal tariffs, or physical suppliers.", + "outcome": "completed", + "evidence": "Written isolated-point and shortcut proof; exact Held--Karp corroboration; full free-symbol word; dense forward/inverse cases and omission controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a paid coordinate change make this same abstract basis competitive?", + "why_it_matters": "The proved cost floor fixes the literal source coordinates.", + "first_step": "Name and price source acquisition, coordinate conversion, and restoration.", + "blocked_by": "No caller or physical conversion program is supplied." + }, + { + "question": "Does this set offer an advantage for actual unequal source tariffs?", + "why_it_matters": "Unit source applications do not order every physically priced program.", + "first_step": "Supply an actual caller and all source, output, and root costs.", + "blocked_by": "No complete caller-specific tariff table is supplied." + } + ], + "claim_type": "scoped proof with exact finite corroboration", + "environment": { + "python": "CPython 3.12.15", + "dependencies": "standard library" + }, + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19134568", + "upstream_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "priority_revision": 7 + } +} diff --git a/research/fixed-fourteen-basis-walk/VERIFY.json b/research/fixed-fourteen-basis-walk/VERIFY.json new file mode 100644 index 0000000000..c06bf19bd7 --- /dev/null +++ b/research/fixed-fourteen-basis-walk/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": 60, + "checks": "Sharp arity and application lower bounds, Held-Karp corroboration, formal dirty endpoint, dense replay, all query/component omissions, and source-bound receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Same complete check with Python assertions disabled." + } + ] +} diff --git a/research/fixed-fourteen-basis-walk/verify.py b/research/fixed-fourteen-basis-walk/verify.py new file mode 100644 index 0000000000..41cc79bcd0 --- /dev/null +++ b/research/fixed-fourteen-basis-walk/verify.py @@ -0,0 +1,198 @@ +#!/usr/bin/env python3 +"""Exact fixed-set routing and arbitrary-dirty paired-readout checks.""" + +import argparse +import hashlib +import json +from pathlib import Path + + +POINTS = (0, 1, 2, 3, 4, 5, 6, 8, 16, 24, 32, 40, 48, 63) +CYCLE = (0, 16, 48, 32, 40, 8, 24, 63, 5, 4, 6, 2, 3, 1, 0) +SOURCE_FILES = ("README.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") +PACKAGE = Path(__file__).resolve().parent + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def cycle_steps(cycle): + require(len(cycle) == 15, "fourteen edges required") + require(cycle[0] == cycle[-1] == 0, "cycle must close at zero") + require(tuple(sorted(cycle[:-1])) == POINTS, "wrong prefix set") + return tuple(a ^ b for a, b in zip(cycle, cycle[1:])) + + +def tour_optimum(cap): + """Held--Karp on the 14 terminals, with a fixed zero start.""" + require(cap in (3, 4, 6), "unsupported bounded arity") + count = len(POINTS) - 1 + infinity = 1000 # Every fourteen-edge six-bit tour costs at most 84. + costs = [[infinity] * count for _ in range(1 << count)] + for j in range(count): + weight = POINTS[j + 1].bit_count() + if weight <= cap: + costs[1 << j][j] = weight + finite_states = 0 + for mask in range(1, 1 << count): + for j in range(count): + cost = costs[mask][j] + if cost == infinity: + continue + finite_states += 1 + for k in range(count): + bit = 1 << k + weight = (POINTS[j + 1] ^ POINTS[k + 1]).bit_count() + if mask & bit == 0 and weight <= cap: + costs[mask | bit][k] = min(costs[mask | bit][k], cost + weight) + answers = [costs[-1][j] + POINTS[j + 1].bit_count() + for j in range(count) if POINTS[j + 1].bit_count() <= cap + and costs[-1][j] != infinity] + return {"cost": min(answers) if answers else None, "finite_states": finite_states} + + +def query_word(cycle): + steps = cycle_steps(cycle) + reads = [[] for _ in POINTS] + pairs = [] + for target in range(1, 64): + pair = next((i, j) for i in range(14) for j in range(i + 1, 14) + if cycle[i] ^ cycle[j] == target) + pairs.append(pair) + for boundary in pair: + reads[boundary].append(("A", target)) + word = [] + for boundary, step in enumerate(steps): + word.extend(reads[boundary]) + word.append(("B", step)) + require(len(word) == 140, "incorrect complete query count") + return tuple(word), pairs + + +def formal_endpoint(word): + """Bit 0 is A_i(z_initial), bits 1..6 are A_i B_j(x_j).""" + root = 1 + outputs = [1 << 7] * 64 # Each row's own independent initial value. + for kind, mask in word: + require(kind in ("A", "B") and 1 <= mask < 64, "invalid query") + if kind == "B": + root ^= mask << 1 + else: + outputs[mask] ^= root + return root == 1 and all(outputs[m] == (1 << 7) ^ (m << 1) + for m in range(1, 64)) + + +def matrix_rows(seed, dimension): + return tuple(((seed * (i + 1) * 7 + i * i + 3) ^ (seed >> i)) + & ((1 << dimension) - 1) for i in range(dimension)) + + +def apply_map(rows, value): + return sum(((row & value).bit_count() & 1) << i for i, row in enumerate(rows)) + + +def dense_replay(word): + cases = 0 + for dimension in (1, 2, 3): + source_maps = tuple(matrix_rows(j + 1, dimension) for j in range(6)) + target_maps = tuple(matrix_rows(j + 11, dimension) for j in range(64)) + # 70 independent rows: six sources, one connector, 63 dirty targets. + for basis in range(70 * dimension): + initial = [0] * 70 + initial[basis // dimension] = 1 << (basis % dimension) + expected = initial.copy() + for mask in range(1, 64): + value = 0 + for j in range(6): + if mask & (1 << j): + value ^= apply_map(source_maps[j], initial[j]) + expected[6 + mask] ^= apply_map(target_maps[mask], value) + actual = initial.copy() + for inverse, direction in enumerate((word, tuple(reversed(word)))): + for kind, mask in direction: + if kind == "B": + for j in range(6): + if mask & (1 << j): + actual[6] ^= apply_map(source_maps[j], actual[j]) + else: + actual[6 + mask] ^= apply_map(target_maps[mask], actual[6]) + require(actual == (initial if inverse else expected), + "dense forward/inverse endpoint mismatch") + cases += 1 + return cases + + +def controls(word): + rejected = 0 + for index in range(len(word)): + require(not formal_endpoint(word[:index] + word[index + 1:]), + "omitted query accepted") + rejected += 1 + for index, (kind, mask) in enumerate(word): + if kind == "B": + for bit in range(6): + if mask & (1 << bit): + reduced = mask ^ (1 << bit) + mutant = (word[:index] + ((kind, reduced),) + word[index + 1:] + if reduced else word[:index] + word[index + 1:]) + require(not formal_endpoint(mutant), "unpaid source component accepted") + rejected += 1 + for bad in (CYCLE[:-1], (1,) + CYCLE[1:], CYCLE[:2] + (16,) + CYCLE[3:]): + try: + cycle_steps(bad) + except ValueError: + rejected += 1 + else: + raise ValueError("invalid cycle accepted") + return rejected + + +def certificate(): + steps = cycle_steps(CYCLE) + weights = tuple(step.bit_count() for step in steps) + distances = tuple((63 ^ p).bit_count() for p in POINTS if p != 63) + require(min(distances) == 4, "isolated-point lower bound changed") + require(sum(weights) == 12 + 2 * min(distances) == 20, "sharp cost bound failed") + require(max(weights) == 4, "sharp arity witness failed") + counts = [sum(bool(step & (1 << j)) for step in steps) for j in range(6)] + require(all(count > 0 and count % 2 == 0 for count in counts), "source restoration failed") + dp = {str(cap): tour_optimum(cap) for cap in (3, 4, 6)} + require([dp[str(cap)]["cost"] for cap in (3, 4, 6)] == [None, 20, 20], + "independent routing optimum disagrees") + word, pairs = query_word(CYCLE) + require(formal_endpoint(word), "free-symbol endpoint failed") + require(formal_endpoint(tuple(reversed(word))), "free-symbol inverse failed") + return { + "claim_type": "scoped proof with exact finite corroboration", + "points": POINTS, "cycle": CYCLE, "steps": steps, "weights": weights, + "source_occurrences": counts, "maximum_arity": 4, + "source_applications": 20, "root_queries": 140, "map_applications": 146, + "held_karp": dp, "readout_boundary_pairs": pairs, + "dense_forward_inverse_cases": dense_replay(word), + "rejected_controls": controls(word), + "source_sha256": {name: hashlib.sha256((PACKAGE / name).read_bytes()).hexdigest() + for name in SOURCE_FILES}, + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", action="store_true", help="print a generated receipt") + args = parser.parse_args() + result = certificate() + if args.emit: + print(json.dumps(result, indent=2, sort_keys=True)) + else: + expected = json.loads((PACKAGE / "RESULT.json").read_text()) + require(json.loads(json.dumps(result)) == expected, "receipt or source hashes changed") + print("PASS_FIXED_FOURTEEN_BASIS_WALK arity=4 source_apps=20 " + "root_queries=140 map_apps=146 dense_cases=" + + str(result["dense_forward_inverse_cases"]) + " controls=" + + str(result["rejected_controls"])) + + +if __name__ == "__main__": + main()