From 2f4add4b548b7eb0ae38abb61fa5dc15d5a2a857 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 3 Nov 2026 21:21:00 +0000 Subject: [PATCH] feat(research): price the eight-query mutable-source row exactly In the path-lowered even-subset class of mutable-source-789q-invoice, eight-query words need R >= 74 and X >= 4, and one closed walk attains both, so the row is exact and price-independent: tariff 460 at (38,2,2). Adds exhaustive X-floor layers at Q = 6..10, the walk spectra, and an attained Q = 9 value of 486. --- .../eight-query-path-lowered-tariff/README.md | 198 +++++++++++ .../SOURCES.json | 24 ++ .../eight-query-path-lowered-tariff/TASK.json | 68 ++++ .../VERIFY.json | 20 ++ .../eight-query-path-lowered-tariff/verify.py | 318 ++++++++++++++++++ 5 files changed, 628 insertions(+) create mode 100644 research/eight-query-path-lowered-tariff/README.md create mode 100644 research/eight-query-path-lowered-tariff/SOURCES.json create mode 100644 research/eight-query-path-lowered-tariff/TASK.json create mode 100644 research/eight-query-path-lowered-tariff/VERIFY.json create mode 100644 research/eight-query-path-lowered-tariff/verify.py diff --git a/research/eight-query-path-lowered-tariff/README.md b/research/eight-query-path-lowered-tariff/README.md new file mode 100644 index 0000000000..8929afca2d --- /dev/null +++ b/research/eight-query-path-lowered-tariff/README.md @@ -0,0 +1,198 @@ +# Eight-query path-lowered words: readouts 74 and source XORs 4 are attained together + +**Scoped exact finite computation, in the PR1898 abstract tariff. No new κ.** In the +path-lowered even-subset class of +[PR2677](https://github.com/CrocSwap/integer-mult-bounds/pull/2677) +(`research/mutable-source-789q-invoice`), every eight-query word needs at least +74 readouts `R` and at least 4 source XORs `X`, and one closed walk attains both. +Both floors are known. The new fact is that they are attained together. The +eight-query row of PR2677's table was a lower bound (`R >= 74`, `X >= 0`, tariff +`>= 452`). It is now exact: + +```text +min over eight-query words of b*Q + a*R + x*X = 8b + 74a + 4x for all b, a, x > 0 +tariff at (b, a, x) = (38, 2, 2): 38*8 + 2*74 + 2*4 = 460 (24 above the six-query endpoint 436) +``` + +Witness, a closed prefix walk with 74 readouts and 4 source XORs (replayed on +arbitrary dirty formal rows by the pinned model): + +```text +(0, 1, 3, 2, 6, 14, 30, 20, 0) also (0, 4, 20, 24, 9, 1, 3, 2, 0) +``` + +| Q | readout floor | XOR floor | attained together | tariff at (38,2,2) | vs 436 | +|--:|--:|--:|---|--:|--:| +| 6 | 96 | 8 | yes (PR1898 word) | **436** exact | 0 | +| 7 | 82 | 6 | yes (PR2677 champion) | **442** exact | +6 | +| 8 | 74 | 4 | **yes (this package)** | **460** exact | +24 | +| 9 | 62 | 2 | open; best found `R=70` at `X=2` | between 470 and 486 | at least +34 | +| >= 10 | 62 | 0 | not claimed | above 460 from `38Q` and `R >= 62` | | + +The Q = 6 and Q = 7 rows are the existing values; the census and replays here +reproduce them. New here: the attaining Q = 8 word, which makes that row exact and +price-independent; the exact walk spectra; the attained Q = 9 value 486; and the +sharpness of the XOR floor at eight queries (below). The XOR floor itself is not +claimed: it is the connector consequence recorded in PR5935 (below). + +## Model + +The model, cost formulas and word builder are those of PR2677's `model.py`, which +the verifier imports as a pinned live input after a SHA256 check. A path-lowered +word is a closed connector walk `0 = w_0, w_1, ..., w_Q = 0` in `F2^5` with every +edge `w_i xor w_(i+1)` nonzero. Values and zero revisits may repeat. Then + +- `X = sum over edges of 2*(weight(edge) - 1)`, the path-local compute and uncompute + source XORs; +- `R` is the total even-subset readout count over the slot values: mask `m` costs + the least even number of slots whose XOR is `m`; +- the tariff is `38Q + 2R + 2X`, the PR1898 fixture. + +A walk covers when every nonzero mask is read, which forces its visited values to +span `F2^5`. Only covering walks are words. + +## Source-XOR floor + +For arbitrary restored source-XOR words, PR5935 +(`research/connected-xor-word-floor`, this author's earlier package) proves +`X >= 2(n - c)` for an interaction graph with `c` components. With the component +inequality `Q >= n + c` of PR2455 this gives `X >= 2(2n - Q)`, so at five sources +`X >= 2(10 - Q)` for `Q <= 10`. PR5935 records this: `X >= 4` at `Q = 8` and +`X >= 2` at `Q = 9`. This package does not re-prove it. + +For self-containment, here is a direct proof in the path-local cost model. A +covering closed walk with `Q` edges has `X >= 2*max(0, 10 - Q)`, `X = 2Q mod 4`, and +equality at the floor holds exactly when every coordinate lies in exactly two edges. + +*Proof.* The visited values are partial sums of the edges, so the edges span +`F2^5` and every coordinate occurs in some edge. The edges sum to zero, so each +coordinate occurs in an even number of edges, at least two. The weight total is the +sum of these five counts: even and at least 10. Then +`X = 2*(total - Q) >= 2*(10 - Q)`, with equality iff the counts are `2,2,2,2,2`. +For `Q <= 5` no covering walk exists, since six edges are needed to span `F2^5`. ∎ + +**Sharpness.** Each X-floor layer below contains covering walks for `Q = 6..10`, so +the floor `2(10 - Q)` is attained there by a path-lowered word, which is a restored +word. At `Q = 8` this makes the XOR floor 4 sharp for arbitrary restored words, given +PR5935's lower bound. That is the sharp eight-query XOR floor asked for in Open next +question 2 of `research/seven-query-xor-floor`. + +## Eight queries + +1. **Readout floor, repeats allowed.** A walk with eight edges visits at most seven + distinct nonzero values. The census over every set of five, six or seven values + (3,535,767 sets, 3,097,024 covering) gives the spectra + + | distinct nonzero values | `R` values (number of sets) | + |--:|---| + | 5 | 96 (83,328) | + | 6 | 82 (97,216), 88 (486,080) | + | 7 | 74 (416,640), 80 (1,180,480), 84 (833,280) | + + So `R >= 74` for every eight-query word. Repeated prefix values or zero revisits + leave at most six distinct values and force `R >= 82`. This answers Open next + question 2 of PR2677 inside the class: the exact minimum is 74, attained only + with seven distinct nonzero values. This is also the readout half of Open next + question 2 of PR2686, repeats included. Its XOR half is the sharp floor 4 above. +2. **XOR floor.** `X >= 4`, from PR5935 for every restored word and from the parity proof above in this class. +3. **Attainment.** The exhaustive layer of closed eight-edge walks with every + coordinate in exactly two edges has 730,800 walks, the count given by + inclusion-exclusion. Of these, 30,240 cover with `R = 74` and `X = 4`. Its full + spectrum is `74: 30,240`, `80: 172,800`, `82: 8,640`, `84: 161,280`, + `88: 248,640`, `96: 84,000` and 25,200 non-covering walks. + +Both floors hold for every word and one walk attains both. The Pareto frontier at +`Q = 8` is the single point `(R, X) = (74, 4)`, so the optimum does not depend on +the prices. The same argument gives single-point frontiers `(96, 8)` at `Q = 6` +and `(82, 6)` at `Q = 7`. + +## Price crossovers among Q = 6, 7, 8 + +With the three exact rows `f6 = 6b + 96a + 8x`, `f7 = 7b + 82a + 6x` and +`f8 = 8b + 74a + 4x`: + +```text +f8 < f7 iff b < 8a + 2x f7 < f6 iff b < 14a + 2x f8 < f6 iff b < 11a + 2x +``` + +At `(38, 2, 2)` all three fail, so the six-query endpoint stays optimal among +`Q <= 8`. The verifier checks the equivalences on a grid of prices. + +## Nine and ten queries + +At `Q = 9` the XOR floor is 2 and the readout floor is at least 62. The X-floor +layer has 453,600 walks and its least readout count is 70, so tariff 486 is +attained. The exact minimum lies between 470 and 486. The next layer (weight total +12, `X = 6`) is not enumerated. + +At `Q = 10` the `X = 0` layer has 113,400 walks and least `R = 64`, with no +`R = 62` walk. That reproduces the read-only ten-query repair with 64 readouts and +no source XOR recorded in `research/mutable-source-connector`, and it agrees with +the four-XOR requirement of `research/mutable-source-shear-cost` for 62 readouts. +No Q = 10 claim is made. + +## Reproduce + +Python 3.12, standard library only, from the repository root: + +```sh +python3.12 -B research/eight-query-path-lowered-tariff/verify.py +python3.12 -B scripts/research_package.py --package research/eight-query-path-lowered-tariff +``` + +Expected marker: + +```text +PASS_EIGHT_QUERY_PATH_LOWERED_TARIFF Q8=(R74,X4) tariff=460 floors_attained_Q6_Q7_Q8 Q9_in_470_486 no_new_kappa +``` + +The verifier takes about a minute. It checks: + +- the readout census above and its set counts; +- the path-local XOR floor exhaustively on 638,832 covering walks in `F2^2`, `F2^3` and + `F2^4`, including attainment of the floor at every `Q` from `n + 1` to `2n`; +- every X-floor layer at `Q = 6..10`, with walk counts equal to the closed-form + count `sum_i (-1)^i C(Q,i) C(Q-i,2)^5` and the spectra quoted here; +- literal dirty-row replays with the pinned model of the two `Q = 8` witnesses, + the `Q = 7` champion `(0,1,2,6,12,24,16,0)`, the six-query word, the `Q = 9` + witness `(0,1,3,2,6,14,10,26,16,0)` and the ten-query paths; +- the three crossover equivalences on prices `b` in 1..39 and `a`, `x` in 1..7; +- 6,000 seeded random walks, repeats and zero revisits included, comparing the + set-based readout and edge-cost formulas with the pinned model. + +[SOURCES.json](SOURCES.json) pins the model. The exhaustive search that found the +witnesses was a separate, unpackaged program. Every number above is recomputed by +`verify.py` itself. + +## Scope and limits + +- The exact row is for path-lowered even-subset words: one closed connector walk, + path-local compute and uncompute source XORs, and PR2677's tariff. The readout and + walk-spectrum claims are not checked for arbitrary XOR-interleaved restored words. + Only the XOR floor, and its sharpness at eight queries, is stated for those, and + its lower bound is PR5935's, not re-proved here. +- The tariff is the abstract complete-call fixture. No physical supplier, hosting, + precision or kappa claim is made. Independent human and formal proof-kernel review + are unclaimed. +- Nine queries are not settled. Ten queries are cross-checked only. + +## Open next questions + +1. What is the exact tariff at nine queries (between 470 and 486)? Enumerate the + `X = 6` layer at `Q = 9` and compare its least readout count with 70. The layer is + larger than the ones here. No obstruction is known. +2. Does the readout floor 74 hold for arbitrary XOR-interleaved restored words at + eight queries, with non-path source XORs? The census uses only the set of + connector values, so the first step is to check that a restored word's connector + values obey the same even-subset readout constraint. + +## Credit + +This contribution was produced by Nick Petalas. It builds on Wentao Li's PR2677 +(`research/mutable-source-789q-invoice`: model, invoice table and the open +question), PR2686 (`research/seven-query-r-floor`) and PR2643 +(`research/seven-query-xor-floor`); on Arham Tahir's PR1898 (the alphabet and the +six-query word); and on PR1370 and Ross Richardson's PR943 for the ten-query +cross-check. The XOR floor `2(10 - Q)` is the connector consequence of PR5935 +(Nick Petalas) with ywz65's PR2455 component inequality; PR2455 also proves the +six-query XOR bound. Predecessor files and notices are unchanged. Apache-2.0. diff --git a/research/eight-query-path-lowered-tariff/SOURCES.json b/research/eight-query-path-lowered-tariff/SOURCES.json new file mode 100644 index 0000000000..a4f72f3a9f --- /dev/null +++ b/research/eight-query-path-lowered-tariff/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/mutable-source-789q-invoice/model.py", + "usage": "input", + "git_blob": "8ce90c48df0a2f9eba9847f3dfe71ce6677897d1", + "sha256": "6696b01837e526f365576c6e35367fa8a1494f5bd3f49af7fe38c52366668c13" + } + ] +} diff --git a/research/eight-query-path-lowered-tariff/TASK.json b/research/eight-query-path-lowered-tariff/TASK.json new file mode 100644 index 0000000000..8c5973a15e --- /dev/null +++ b/research/eight-query-path-lowered-tariff/TASK.json @@ -0,0 +1,68 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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 eight-query row of the path-lowered even-subset mutable-source invoice (PR2677) at every positive price (b,a,x): the readout floor 74 and the source-XOR floor 4 are attained by one closed walk. Exhaustive X-floor layers at Q = 6..10; sharpness of the XOR floor at eight queries for arbitrary restored words, with its lower bound taken from PR5935. Answers Open next question 2 of PR2677, and of PR2686 and PR2643 at eight queries within these classes.", + "scope_change_reason": "The card asks for a new connector operation. This keeps the PR1898 alphabet and the PR2677 path-lowered schedule class unchanged and closes the unpriced eight-query row of an existing invoice table, a side result in the same abstract tariff.", + "bottleneck_link": "Side result. It settles the intermediate-query unequal-price handoff of the five-source common-B mutable-source connector for eight queries; it does not change a supplier or kappa.", + "budget_minutes": 60, + "stop_rule": "Stop once the eight-query row is exact and the floor layers are enumerated; leave the Q = 9 exact minimum and non-path restored readout words open.", + "outcome": "completed", + "evidence": "verify.py: readout census over all 3,535,767 value sets of size 5, 6 and 7 (3,097,024 cover every mask; spectra {96}, {82,88}, {74,80,84}); parity-lemma controls on 638,832 covering walks in F2^2..F2^4; exhaustive X-floor layers at Q = 6..10 matching closed-form walk counts; literal dirty-row replays of the Q = 8 witnesses (R=74, X=4, tariff 460), the Q = 7 champion, the Q = 6 endpoint and the Q = 9 witness (tariff 486); 6,000 seeded random walks against the pinned model.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the exact minimum tariff at nine queries (floor 470, attained 486 at X = 2, R = 70)?", + "why_it_matters": "It completes the exact rows of the path-lowered invoice table between the six-query endpoint and the ten-query repairs.", + "first_step": "Enumerate the X = 6 layer (weight total 12, each coordinate in two or four edges) at Q = 9 and compare its least readout count with 70.", + "blocked_by": "A larger layer than the X-floor layers enumerated here; no obstruction known." + }, + { + "question": "Does the readout floor 74 hold for arbitrary XOR-interleaved restored words at eight queries?", + "why_it_matters": "It would extend the exact eight-query row from path-lowered words to every restored five-source word with even-subset readouts.", + "first_step": "Check that the connector values of a restored word obey the same even-subset readout constraint, so that the census over value sets applies unchanged.", + "blocked_by": "The constraint is argued for path-lowered words only; no general proof is written here." + } + ] +} diff --git a/research/eight-query-path-lowered-tariff/VERIFY.json b/research/eight-query-path-lowered-tariff/VERIFY.json new file mode 100644 index 0000000000..95e9ab9c79 --- /dev/null +++ b/research/eight-query-path-lowered-tariff/VERIFY.json @@ -0,0 +1,20 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/mutable-source-789q-invoice/model.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Readout census over all 5-, 6- and 7-value sets, XOR parity lemma controls, exhaustive X-floor layers at Q = 6..10, literal dirty-row replays of the Q = 8, 7, 6 and 9 words, tariff crossovers, and 6,000 seeded random walks against the pinned model." + } + ] +} diff --git a/research/eight-query-path-lowered-tariff/verify.py b/research/eight-query-path-lowered-tariff/verify.py new file mode 100644 index 0000000000..5e7ad89d61 --- /dev/null +++ b/research/eight-query-path-lowered-tariff/verify.py @@ -0,0 +1,318 @@ +"""Exact eight-query row of the mutable-source invoice (path-lowered even-subset class). + +Model, tariff and word builder come from research/mutable-source-789q-invoice/model.py, +a pinned live input (Wentao Li; alphabet of PR1898). A path-lowered word is a closed +connector prefix walk 0 = w_0, w_1, ..., w_Q = 0 in F2^5 with nonzero edges, even-subset +readouts R over its slot values, and X = sum over edges of 2 * (weight(edge) - 1). +Tariff (b, a, x) = (38, 2, 2): 38 Q + 2 R + 2 X. + +Checks, all standard library: + 1. R census over every set of 5, 6 or 7 nonzero connector values (readout floors). + 2. XOR parity lemma X >= 2 * max(0, 10 - Q), exhaustive controls in F2^2, F2^3, F2^4. + 3. Exhaustive X-floor layers at Q = 6..10 (each coordinate in exactly two edges); the + Q = 10 layer is a cross-check against the earlier ten-query results, not a new claim. + 4. Literal dirty-row replay of the witness words with the pinned model. + 5. Set-based readout and edge-cost formulas against the pinned model on random walks. +""" +from __future__ import annotations + +import hashlib +import importlib.util +import random +import sys +from collections import Counter +from itertools import combinations, product +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +MODEL_PATH = ROOT / "research" / "mutable-source-789q-invoice" / "model.py" +MODEL_SHA256 = "6696b01837e526f365576c6e35367fa8a1494f5bd3f49af7fe38c52366668c13" +FULL = 32 +INF = 99 +ENDPOINT = 436 # six-query endpoint tariff at (b, a, x) = (38, 2, 2) + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def load_model(): + data = MODEL_PATH.read_bytes() + need(hashlib.sha256(data).hexdigest() == MODEL_SHA256, "pinned model.py bytes changed") + spec = importlib.util.spec_from_file_location("mutable_source_789q_model", MODEL_PATH) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def weight(x): + return x.bit_count() + + +def readout(values): + """Total even-subset readout count for the nonzero connector values (zero slot is free). + + s[m] is the least number of distinct values with XOR m; the zero slot repairs parity, + so mask m costs 2 * ceil(s[m] / 2). None when some mask is uncovered. + """ + s = [INF] * FULL + s[0] = 0 + for v in values: + new = s[:] + for m in range(FULL): + if s[m] < INF and new[m ^ v] > s[m] + 1: + new[m ^ v] = s[m] + 1 + s = new + total = 0 + for m in range(1, FULL): + if s[m] >= INF: + return None + total += 2 * ((s[m] + 1) // 2) + return total + + +def walk_x(closed): + return sum(2 * (weight(a ^ b) - 1) for a, b in zip(closed, closed[1:])) + + +def walk_r(closed): + return readout(sorted({v for v in closed if v})) + + +def census(k): + """Spectrum of R over all k-subsets of nonzero F2^5 values that cover every mask.""" + spectrum = Counter() + for values in combinations(range(1, FULL), k): + r = readout(values) + if r is not None: + spectrum[r] += 1 + return spectrum + + +def x_floor(q): + return 2 * max(0, 10 - q) + + +def check_parity_lemma_small(): + """Exhaustive control of the generic lemma X >= 2 * max(0, 2n - Q) in F2^n. + + A walk covers when its visited values span F2^n. Equality must be attained at + every Q from n + 1 to 2n, and the walk cost must be even-congruent as stated. + """ + checked = 0 + for n, qmax in ((2, 6), (3, 7), (4, 6)): + size = 1 << n + for q in range(n + 1, qmax + 1): + best = None + for tail in product(range(size), repeat=q - 1): + closed = (0,) + tail + (0,) + if any(a == b for a, b in zip(closed, closed[1:])): + continue + span = {0} + for v in closed: + span |= {s ^ v for s in span} + if len(span) != size: + continue + x = sum(2 * (weight(a ^ b) - 1) for a, b in zip(closed, closed[1:])) + floor = 2 * max(0, 2 * n - q) + need(x >= floor, f"parity lemma fails n={n} q={q} walk={closed}") + need(x % 4 == (2 * q) % 4, f"parity class fails n={n} q={q} walk={closed}") + best = x if best is None else min(best, x) + checked += 1 + if q <= 2 * n: + need(best == 2 * (2 * n - q), f"floor not attained n={n} q={q}: {best}") + else: + # Beyond Q = 2n the weight total must be even and at least Q, so X >= 2 (Q mod 2). + need(best == 2 * (q % 2), f"parity floor not attained n={n} q={q}: {best}") + return checked + + +def layer(q): + """Every closed q-edge walk whose edges are nonzero and use each coordinate exactly twice. + + These are exactly the walks with X = 2 * (10 - q). Returns (walks, spectrum, example) + where the spectrum counts walks by R (None: the visited values do not cover) and + example maps R to the first walk found in depth-first order. + """ + spectrum = Counter() + example = {} + cache = {} + counts = [0] * 5 + walk = [0] + total = 0 + + def rec(position, current, visited, used): + nonlocal total + if position == q: + need(current == 0 and all(c == 2 for c in counts), "layer closure invariant") + total += 1 + key = frozenset(visited) + if key not in cache: + cache[key] = readout(sorted(key)) + r = cache[key] + spectrum[r] += 1 + example.setdefault(r, tuple(walk)) + return + remaining = q - position - 1 + for d in range(1, FULL): + if any(d >> j & 1 and counts[j] == 2 for j in range(5)): + continue + new_used = used + weight(d) + if new_used + remaining > 10 or new_used + 5 * remaining < 10: + continue + for j in range(5): + if d >> j & 1: + counts[j] += 1 + nxt = current ^ d + added = nxt != 0 and nxt not in visited + if added: + visited.add(nxt) + walk.append(nxt) + rec(position + 1, nxt, visited, new_used) + walk.pop() + if added: + visited.discard(nxt) + for j in range(5): + if d >> j & 1: + counts[j] -= 1 + + rec(0, 0, set(), 0) + return total, spectrum, example + + +def layer_walk_count(q): + """Closed-form count of layer walks: 5 coordinates choose position pairs covering all q edges.""" + from math import comb + + return sum((-1) ** i * comb(q, i) * comb(q - i, 2) ** 5 for i in range(q + 1)) + + +def check_model_agreement(model, rng): + """Set-based readout and edge-cost formulas against the pinned model.""" + checked = 0 + for q in (6, 7, 8, 9): + for _ in range(1500): + while True: + mid = [rng.randrange(FULL) for _ in range(q - 1)] + closed = [0] + mid + [0] + if all(a != b for a, b in zip(closed, closed[1:])): + break + slots = tuple(closed[:-1]) + expected = model.min_even_subset_R(slots) + need(walk_r(closed) == expected, f"readout formula differs on {closed}") + need(walk_x(closed) == model.path_X(closed), f"edge cost differs on {closed}") + checked += 1 + return checked + + +def replay(model, closed): + """Literal dirty-row replay of the path-lowered word; returns (Q, R, X, tariff).""" + word = model.path_word(list(closed)) + counts = model.check_identity(word) + inv = model.invoice(word) + need(inv["Q"] == counts["Q"] and inv["R"] == counts["R"] and inv["X"] == counts["X"], "invoice counts") + need(inv["tariff"] == 38 * inv["Q"] + 2 * inv["R"] + 2 * inv["X"], "tariff formula") + need(model.rank_increments(list(closed)) == 5, "increments do not span") + return inv["Q"], inv["R"], inv["X"], inv["tariff"] + + +def main(): + model = load_model() + out = [] + + # 1. Readout census over all connector-value sets of size 5, 6 and 7. + spectra = {k: census(k) for k in (5, 6, 7)} + need(dict(spectra[5]) == {96: 83328}, f"size-5 spectrum {dict(spectra[5])}") + need(dict(spectra[6]) == {82: 97216, 88: 486080}, f"size-6 spectrum {dict(spectra[6])}") + need(dict(spectra[7]) == {74: 416640, 80: 1180480, 84: 833280}, f"size-7 spectrum {dict(spectra[7])}") + need(sum(spectra[7].values()) == 2430400 and sum(spectra[6].values()) == 583296, "set counts") + out.append("census R: size5 {96}, size6 {82,88}, size7 {74,80,84}; sets 83328/583296/2430400") + + # 2. Parity lemma controls. + checked = check_parity_lemma_small() + out.append(f"parity lemma controls: {checked} covering walks in F2^2..F2^4") + + # 3. Exhaustive X-floor layers. + layers = {} + for q in range(6, 11): + walks, spectrum, example = layer(q) + need(walks == layer_walk_count(q) == sum(spectrum.values()), f"layer count q={q}") + layers[q] = (walks, spectrum, example) + expect_min = {6: 96, 7: 82, 8: 74, 9: 70, 10: 64} + for q, (walks, spectrum, example) in layers.items(): + covering = [r for r in spectrum if r is not None] + need(min(covering) == expect_min[q], f"layer minimum q={q}: {min(covering)}") + out.append( + f"layer Q={q} X={x_floor(q)}: walks={walks} min R={min(covering)} " + f"at {spectrum[min(covering)]} walks; example {example[min(covering)]}" + ) + need(layers[8][1][74] == 30240 and layers[7][1][82] == 40320 and layers[6][1][96] == 155520, "attaining counts") + need(layers[10][1][64] == 2640 and layers[9][1][70] == 28080, "attaining counts q=9,10") + need(62 not in layers[10][1], "R=62 occurs in the X=0 layer at Q=10") + + # 4. Floors are attained simultaneously at Q = 6, 7, 8. + floors = {6: (96, 8), 7: (82, 6), 8: (74, 4)} + for q, (r_floor, x_floor_q) in floors.items(): + need(x_floor(q) == x_floor_q, f"X floor q={q}") + need(min(r for r in layers[q][1] if r is not None) == r_floor, f"R floor attained q={q}") + # Walks with repeated prefix values or zero revisits cannot reach R = 74. + need(min(spectra[6]) == 82 and min(spectra[5]) == 96, "repeated-value layers") + + # 5. Replays with the pinned model. + witness8 = layers[8][2][74] + need(replay(model, witness8) == (8, 74, 4, 460), f"witness8 replay {witness8}") + fixed8 = (0, 4, 20, 24, 9, 1, 3, 2, 0) + need(replay(model, fixed8) == (8, 74, 4, 460), "fixed witness replay") + champion7 = (0, 1, 2, 6, 12, 24, 16, 0) + need(replay(model, champion7) == (7, 82, 6, 442), "seven-query champion replay") + word6 = model.minimum_word_6q() + inv6 = model.invoice(word6) + need((inv6["Q"], inv6["R"], inv6["X"], inv6["tariff"]) == (6, 96, 8, ENDPOINT), "six-query endpoint") + need(model.check_identity(word6)["Q"] == 6, "six-query word replay") + witness9 = layers[9][2][70] + need(replay(model, witness9) == (9, 70, 2, 486), f"Q=9 X-floor witness {witness9}") + # Cross-check at ten queries: the read-only repair (64 readouts, no source XOR) of the earlier + # lineage is the X = 0 layer, and R = 62 does not occur there, so it needs X >= 4 (the four-X path). + witness10 = layers[10][2][64] + need(replay(model, witness10) == (10, 64, 0, 508), f"X=0 walk at Q=10 {witness10}") + ten = [0, 4, 5, 1, 3, 7, 6, 14, 28, 16, 0] + need(replay(model, ten)[:3] == (10, 62, 4), "four-X ten-query path") + out.append( + f"replays: Q=8 {witness8} and {fixed8} -> R=74 X=4 tariff 460; " + f"Q=7 champion 442; Q=6 endpoint 436; Q=9 {witness9} -> R=70 X=2 tariff 486" + ) + out.append( + f"cross-check Q=10: X=0 layer minimum R=64 ({witness10}, tariff 508), R=62 absent from that " + "layer, four-X path (R=62, X=4, tariff 512) replays" + ) + + # 6. Tariff table and exact crossovers. + def f(q, r, x, b=38, a=2, c=2): + return b * q + a * r + c * x + + need(f(8, 74, 4) == 460 and f(7, 82, 6) == 442 and f(6, 96, 8) == 436, "tariff table") + need(f(9, 62, 2) == 470 and f(9, 70, 2) == 486, "Q=9 floor and attained value") + need(f(10, 64, 0) == 508 and f(10, 62, 4) == 512, "Q=10 cross-check values") + need(f(8, 74, 4) - ENDPOINT == 24, "gap to the endpoint") + # f8 < f7 iff b < 8a + 2x; f7 < f6 iff b < 14a + 2x; f8 < f6 iff b < 11a + 2x. + for b, a, c in product(range(1, 40), range(1, 8), range(1, 8)): + need((f(8, 74, 4, b, a, c) < f(7, 82, 6, b, a, c)) == (b < 8 * a + 2 * c), "f8 vs f7") + need((f(7, 82, 6, b, a, c) < f(6, 96, 8, b, a, c)) == (b < 14 * a + 2 * c), "f7 vs f6") + need((f(8, 74, 4, b, a, c) < f(6, 96, 8, b, a, c)) == (b < 11 * a + 2 * c), "f8 vs f6") + out.append("tariff (38,2,2): Q=6 436, Q=7 442, Q=8 460 (exact); Q=9 in [470, 486]; Q>=10 > 460") + + # 7. Pinned model agreement on random walks (seeded). + checked = check_model_agreement(model, random.Random(20261103)) + out.append(f"model agreement: {checked} seeded random walks (readout and edge cost)") + + for line in out: + print(line) + print( + "PASS_EIGHT_QUERY_PATH_LOWERED_TARIFF Q8=(R74,X4) tariff=460 " + "floors_attained_Q6_Q7_Q8 Q9_in_470_486 no_new_kappa" + ) + + +if __name__ == "__main__": + main()