diff --git a/research/seven-query-xor-floor/CERTIFICATE.json b/research/seven-query-xor-floor/CERTIFICATE.json new file mode 100644 index 0000000000..2b03f1e852 --- /dev/null +++ b/research/seven-query-xor-floor/CERTIFICATE.json @@ -0,0 +1,149 @@ +{ + "schema_version": 1, + "status": "PASS_SEVEN_QUERY_XOR_FLOOR", + "scope": "Five-source common-B mutable-source Q/R/X alphabet (PR1898). Restored straight-line words. Exact minimum source-XOR count at Q=7.", + "claim": { + "Q": 7, + "min_X": 6, + "sharp": true, + "answers_789q_oq1": "No non-path (or path) schedule at Q=7 can reach X<=2; in fact X<=5 is impossible.", + "no_new_kappa": true + }, + "component_lemma": { + "statement": "An interaction graph with c components forces at least n+c queries on n sources.", + "n": 5 + }, + "edge_bound": { + "argument": "Any interaction graph with e undirected edges on n=5 labels has c>=n-e components. For e<=2, c>=3 so Q>=n+c>=8. Census tightens X=2 to c>=4.", + "X_le_2_query_floor_from_edges": 8, + "X_le_2_query_floor_from_census": 9 + }, + "census": { + "n": 5, + "bound": 6, + "raw_half_word_counts": [ + 1, + 20, + 400, + 8000 + ], + "half_distinct_matrices": [ + 1, + 20, + 261, + 2770 + ], + "half_matrix_graph_states": [ + 1, + 20, + 270, + 3130 + ], + "last_layer_sha256": "03182f1a0a36c51ea1112ed41e3e4c3d99393dc479dc1c4c477673d0f7eeb190", + "by_length": [ + { + "length": 0, + "identity_graphs": 1, + "connected_identity_graphs": 0, + "minimum_components": 5, + "query_floor_n_plus_c": 10, + "graphs_sha256": "d0bca111f8628137adc4c16f123496dcdd1d590d06cb5d9acd68b39fe656fb97" + }, + { + "length": 1, + "identity_graphs": 0, + "connected_identity_graphs": 0, + "minimum_components": null, + "query_floor_n_plus_c": null, + "graphs_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945" + }, + { + "length": 2, + "identity_graphs": 10, + "connected_identity_graphs": 0, + "minimum_components": 4, + "query_floor_n_plus_c": 9, + "graphs_sha256": "0899bb1953bc4b09e040dbb8308c5c134c718d3cfe052d06ff64baed6062eb7f" + }, + { + "length": 3, + "identity_graphs": 0, + "connected_identity_graphs": 0, + "minimum_components": null, + "query_floor_n_plus_c": null, + "graphs_sha256": "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945" + }, + { + "length": 4, + "identity_graphs": 55, + "connected_identity_graphs": 0, + "minimum_components": 3, + "query_floor_n_plus_c": 8, + "graphs_sha256": "546640ef872e4f0d2ebda17f74c88eeea8ccff09cb9e16de7cff2ff6735cd024" + }, + { + "length": 5, + "identity_graphs": 10, + "connected_identity_graphs": 0, + "minimum_components": 3, + "query_floor_n_plus_c": 8, + "graphs_sha256": "defa9e87f9e7cc3a75d63330d451e5d1c8cd011734d1a489ec0d84af6ba68504" + }, + { + "length": 6, + "identity_graphs": 175, + "connected_identity_graphs": 0, + "minimum_components": 2, + "query_floor_n_plus_c": 7, + "graphs_sha256": "163a9c5ccd357bfc55f07c641213f247253db4894f6798c6e75c94104e2be060" + } + ] + }, + "query_floors_by_X": { + "0": 10, + "1": null, + "2": 9, + "3": null, + "4": 8, + "5": 8, + "6": 7 + }, + "attaining_witness": { + "kind": "path_lowered_even_subset", + "closed_path": [ + 0, + 1, + 2, + 6, + 12, + 24, + 16, + 0 + ], + "Q": 7, + "R": 82, + "X": 6, + "tariff_at_38_2_2": 442, + "invoice": { + "Q": 7, + "R": 82, + "X": 6, + "map_leaves": 278, + "echo_nodes": 63, + "root_dispatches": 95, + "borrowed_dirty_rows": 4, + "tariff": 442, + "complete_prices": { + "b": 38, + "a": 2, + "x": 2 + } + }, + "credit": "Path-lowered champion from mutable-source-789q-invoice lineage; PR1898 alphabet." + }, + "pr2455_crosscheck": { + "matched_graph_digests_0_through_6": true, + "note": "Open PR2455 proves X>=8 at Q=6; this package reuses the same meet-in-the-middle census through X=6 for the Q=7 floor. Per-length graph digests match that package's RESULT.json." + }, + "new_kappa": false +} diff --git a/research/seven-query-xor-floor/NOTICE.md b/research/seven-query-xor-floor/NOTICE.md new file mode 100644 index 0000000000..1a71fa7e69 --- /dev/null +++ b/research/seven-query-xor-floor/NOTICE.md @@ -0,0 +1,21 @@ +# Notice + +New material in this directory is Apache-2.0. + +Predecessor credit (do not alter historical notices elsewhere): + +- Arham Tahir / PR1898 `research/mutable-source-minimum-queries` — five-source + alphabet, minimum-query endpoint, abstract complete-call tariff. +- ywz65 / open PR2455 `research/mutable-source-six-query-xor` — component lemma + and meet-in-the-middle restored interaction-graph census at six queries; + digests for lengths 0–6 are cross-checked here. +- Arham Tahir / PR1370 — path-local shear lowering. +- TennisBowling / PR1524 — equal-price theorem and unequal-price handoff. +- Ross Richardson / PR943/934 — prefix framework. +- Fork path-lowered `research/mutable-source-789q-invoice` — champion path and + non-path OQ1 answered here; that package is not edited. +- Live pin: `research/mutable-source-shear-cost/CERTIFICATE.json` (ten-query + four-X context). + +Prepared by Wentao Li (VictorLiwentao, @Is__Victor) with substantial AI +assistance. diff --git a/research/seven-query-xor-floor/PROOF.md b/research/seven-query-xor-floor/PROOF.md new file mode 100644 index 0000000000..68dfbd7656 --- /dev/null +++ b/research/seven-query-xor-floor/PROOF.md @@ -0,0 +1,115 @@ +# Exact source-XOR floor at seven queries + +This is a scoped obstruction and sharpness statement in the five-source +common-B mutable-source alphabet of +[PR1898](https://github.com/CrocSwap/integer-mult-bounds/pull/1898). +It does not claim a new kappa, physical supplier tariff, or global unequal-price +optimum over all query counts. + +It answers open question 1 of the path-lowered +`research/mutable-source-789q-invoice` lineage: whether a non-path XOR schedule +at seven queries can reach `X≤2` with `R=82` (tariff `≤436`). The answer is +negative for a stronger reason: **every restored seven-query word needs +`X≥6`**, path or non-path. The credited path-lowered champion attains `X=6`, +so the floor is sharp. + +## Alphabet and restoration + +Retain five distinct arbitrary-dirty F₂ source rows `x₀,…,x₄`, thirty-one +distinct arbitrary-dirty outputs `y_m`, a connector `z`, and private scratch. +Complete calls are `Q_j: z += B x_j`, `R_m: y_m += A_m z`, and paid +`X_(s,t): x_t += x_s`. The exit map is + +```text +y_m += A_m B(sum_j bit_j(m) · x_j_initial), +``` + +with every source, connector and private scratch restored. Straight-line words +are data independent. Extra connectors, free copies, output mixing and +source-specific B maps are excluded. This is PR1340/PR1898's source-shear +alphabet. + +## Interaction graph and component lemma + +Build the undirected **interaction graph** on the five source labels: every +`X_(s,t)` contributes the edge `{s,t}`, including edges whose matrix effects +later cancel. Suppose the graph has `c` components `C_i` of sizes `n_i`. + +Each query increment lies in the coordinate subspace of its source's component. +Connector restoration forces the sum of increments inside each component to be +zero, so the increments that touch component `i` span a space of dimension at +most `t_i − 1` whenever that component is queried `t_i` times. Covering the +`n_i`-dimensional source space on that component therefore requires +`t_i ≥ n_i + 1`. Every component must be queried (an unqueried component cannot +contribute its sources to the AB image while restoring). Summing yields + +```text +Q = Σ t_i ≥ Σ (n_i + 1) = n + c. +``` + +Thus an interaction graph with `c` components forces at least `n + c` queries. +This lemma is the same component bound used by open +[PR2455](https://github.com/CrocSwap/integer-mult-bounds/pull/2455) at six +queries; the proof is reproduced here so the present package is freestanding. + +## Census of restored XOR words through length six + +A restored source-shear word of XOR-length `ℓ` is a product of `ℓ` elementary +shears that returns every source to its initial basis. Meet-in-the-middle on +`(source matrix, all-used-edge graph)` lists every restored interaction graph +at each length `ℓ ≤ 6` (PR2455 technique; digests match that package's +`RESULT.json` for lengths 0–6). Observed minimum component counts: + +| X length | Restored graphs | Min components | Query floor `n+c` | +|---:|---:|---:|---:| +| 0 | 1 | 5 | 10 | +| 1 | 0 | — | — | +| 2 | 10 | 4 | 9 | +| 3 | 0 | — | — | +| 4 | 55 | 3 | 8 | +| 5 | 10 | 3 | 8 | +| 6 | 175 | 2 | 7 | + +No length through six has a connected restored graph. In particular, every +restored word with `X ≤ 5` has query floor at least 8, so it cannot run at +exactly seven queries. + +A coarser edge bound already excludes the 789q OQ1 target without the census: +any graph with `e ≤ 2` edges on five labels has `c ≥ 5 − e ≥ 3`, hence +`Q ≥ 8`. The census strengthens `X = 2` to `c ≥ 4` / `Q ≥ 9` and extends the +exclusion through `X = 5`. + +## Sharpness at seven queries + +The first XOR length whose census floor is `≤ 7` is `X = 6` (minimum +components 2). Therefore every restored seven-query word satisfies `X ≥ 6`. + +The path-lowered closed prefix + +```text +(0, 1, 2, 6, 12, 24, 16, 0) +``` + +attains `7 Q / 82 R / 6 X` under even-subset readout and path-local +compute/uncompute lowering (credited champion of the 789q invoice lineage). +Dirty root and inverse identities hold for the PR1898 abstract maps. Its +abstract complete-call tariff at `(b,a,x)=(38,2,2)` is 442. Attainment shows +the XOR floor is sharp. + +## Scope limits + +- No claim that seven-query words cannot undercut tariff 436 via a **lower R** + than 82 with `X ≥ 6`. Readout minima under unrestricted non-path schedules + remain open. +- No claim about eight or nine queries beyond the inherited path-lowered floors. +- No physical common-B hosting, precision, tape or selected-supplier invoice. +- No new kappa. + +## Relation to predecessors + +| Prior | Already proves | This package adds | +|---|---|---| +| PR1898 | Min `Q = 6`, min `R = 96` at that `Q`, `8 X` construction | — | +| PR2455 (open) | `X ≥ 8` at exactly six queries | — | +| 789q invoice (fork, path-lowered) | Path-class `Q∈{7,8,9}` invoices; OQ1 asks non-path `X≤2` at `R=82` | — | +| **This** | — | **`X ≥ 6` at exactly seven queries, sharp; rejects OQ1** | diff --git a/research/seven-query-xor-floor/README.md b/research/seven-query-xor-floor/README.md new file mode 100644 index 0000000000..0f65aa7bc2 --- /dev/null +++ b/research/seven-query-xor-floor/README.md @@ -0,0 +1,98 @@ +# Seven-query source-XOR floor is exactly six + +**Scoped obstruction with sharp attainment; no new kappa.** In the five-source +common-B mutable-source alphabet of +[PR1898](https://github.com/CrocSwap/integer-mult-bounds/pull/1898), every +restored straight-line word with **exactly seven queries** needs **at least six +source XORs**. The bound is sharp: the credited path-lowered champion + +```text +(0, 1, 2, 6, 12, 24, 16, 0) +``` + +attains `7 Q / 82 R / 6 X` (abstract tariff **442** at `(b,a,x)=(38,2,2)`). + +This answers open question 1 of the path-lowered +`research/mutable-source-789q-invoice` lineage (beyond +[#2455](https://github.com/CrocSwap/integer-mult-bounds/pull/2455) / +[#1898](https://github.com/CrocSwap/integer-mult-bounds/pull/1898)): a non-path +XOR schedule at seven queries **cannot** reach `X≤2` with `R=82` (nor any `R`), +because already `X≤5` is impossible at `Q=7`. + +| X length | Min interaction components | Query floor `5+c` | Admits `Q=7`? | +|---:|---:|---:|---| +| ≤2 | ≥4 (census; edges alone give ≥3) | ≥9 | no | +| 4 or 5 | 3 | 8 | no | +| **6** | **2** | **7** | **yes (sharp)** | + +The component lemma (`Q ≥ n + c`) and the meet-in-the-middle restored-graph +census through length six are recorded in [PROOF.md](PROOF.md) and +[CERTIFICATE.json](CERTIFICATE.json). Graph digests for lengths 0–6 match open +PR2455's published `RESULT.json` (that PR proves `X≥8` at **six** queries; +this package uses the same census engine for the **seven**-query floor). + +No claim that seven-query words cannot undercut tariff 436 by lowering `R` +below 82 while keeping `X≥6`. No physical supplier invoice or new κ. + +## Reproduce + +Python **3.12**, standard library only, from the repository root: + +```sh +python3.12 -I -B research/seven-query-xor-floor/verify.py +python3.12 -I -O -B research/seven-query-xor-floor/verify.py +python3.12 -I -B research/seven-query-xor-floor/independent.py +python3.12 -I -B research/seven-query-xor-floor/test_package.py +python3.12 -B scripts/research_package.py --package research/seven-query-xor-floor +``` + +Expected: + +```text +PASS_SEVEN_QUERY_XOR_FLOOR Q=7 min_X=6 sharp X<=5 blocked answers_789q_oq1 no_new_kappa +PASS_INDEPENDENT_SEVEN_QUERY_XOR_FLOOR min_X=6 floors_block_X_le_5 ... tariff=442 controls=2 +PASS_SEVEN_QUERY_XOR_FLOOR_PACKAGE_TESTS groups=6 +PASS_REGISTERED_RESEARCH_PACKAGE research/seven-query-xor-floor outcome=completed +``` + +Default verify is read-only and compares a fresh census to +[CERTIFICATE.json](CERTIFICATE.json). Use `--write` only to regenerate that +receipt. Admission uses `need()` (not `assert`); `-O` also passes. + +## Scope and overlap + +Base commit `0b1cccf86e2f5132ed286a26ef0a681a495740ea`. Direct predecessors: +PR1898 (minimum-query endpoint), open PR2455 (six-query XOR necessity), and the +fork path-lowered 789q invoice (OQ1). Leave-alone objects through +[#2593](https://github.com/CrocSwap/integer-mult-bounds/pull/2593) and the +pending `mutable-source-789q-invoice` R-spectrum repair are not edited. + +Closest prior: PR2455 proves `X≥8` at `Q=6` and does not settle seven queries. +The 789q package prices path-lowered `Q∈{7,8,9}` bills and leaves non-path +`X≤2` open. This freestanding package closes that XOR-floor obligation at +`Q=7` for the full restored alphabet. + +## Open next questions + +1. What is the minimum readout count `R` among restored seven-query words with + `X=6`? Why it matters: tariff `38·7 + 2R + 2·6` undercuts 436 iff `R≤78`. + First step: search restored length-6 shear words whose query schedule admits + even-subset (or cheaper) coverings with `R≤78`. Blocked by: no such covering + census is claimed here. +2. Does the same component+census method give a sharp XOR floor at eight + queries? First step: extend the restored-graph census to the first length + with `n+c ≤ 8` and match an attaining word. Blocked by: larger search. + +## Credit + +Credit **Arham Tahir / PR1898** (alphabet, minimum-query endpoint, abstract +tariff), **ywz65 / PR2455** (component lemma and meet-in-the-middle restored +census at six queries; digests reused as cross-check), **PR1370** (path-local +shear lowering), the fork **789q invoice** lineage (path-class champion and +OQ1), **TennisBowling / PR1524**, **Ross Richardson / PR943**, and the retained +mutable-source lineage. Live input pin: +`research/mutable-source-shear-cost/CERTIFICATE.json` (ten-query four-X +context). Prepared by Wentao Li +([VictorLiwentao](https://github.com/VictorLiwentao), +[@Is__Victor](https://x.com/Is__Victor)) with substantial AI assistance. +Apache-2.0. No independent human review or multiplication theorem is claimed. diff --git a/research/seven-query-xor-floor/SOURCES.json b/research/seven-query-xor-floor/SOURCES.json new file mode 100644 index 0000000000..719b378cbd --- /dev/null +++ b/research/seven-query-xor-floor/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "research/mutable-source-shear-cost/CERTIFICATE.json", + "usage": "input", + "git_blob": "48958451bc819f2caa13bf3d9609423706ffb8a0", + "sha256": "665435375c025bbcf69eadf43bd9aeae44eb12fefdf12a78d5bfd66abde4ae3c" + } + ] +} diff --git a/research/seven-query-xor-floor/TASK.json b/research/seven-query-xor-floor/TASK.json new file mode 100644 index 0000000000..2c5cc6e186 --- /dev/null +++ b/research/seven-query-xor-floor/TASK.json @@ -0,0 +1,84 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "original_card": { + "id": "connector-alphabet-change", + "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?", + "starting_points": [ + "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.", + "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." + ], + "overlap_terms": [ + "universal connector", + "source-toggle", + "connector alphabet" + ] + }, + "scope_status": "changed", + "actual_scope": "Prove the exact minimum source-XOR count at seven queries in the PR1898 five-source restored Q/R/X alphabet: X>=6, sharp via the path-lowered champion; thereby reject the 789q non-path OQ1 target X<=2 at R=82.", + "scope_change_reason": "The drawn connector-alphabet card is redirected to the explicit non-path XOR open question left by the #1898/#2455/789q lineage, which is the nearest unpaid #840-style obstruction outside leave-alone tooling hosts and the in-flight 789q R-spectrum repair.", + "bottleneck_link": "A sharp seven-query XOR floor prices whether intermediate query counts can undercut the six-query endpoint via cheap shared source preparation.", + "budget_minutes": 60, + "stop_rule": "Stop after component lemma, restored-graph census through X=6, sharp attaining witness, package tests; no R-minimum search at Q=7.", + "outcome": "completed", + "evidence": "CERTIFICATE.json census digests matching PR2455 lengths 0-6, query floors blocking X<=5 at Q=7, champion 7Q/82R/6X identity and tariff 442, independent column-image census, corruption controls.", + "author": "Wentao Li", + "ai_assistance": "Substantial AI assistance for derivation, implementation, checking and writing.", + "open_questions": [ + { + "question": "What is the minimum readout count R among restored seven-query words with X=6?", + "why_it_matters": "Tariff 38*7+2R+2*6 undercuts 436 iff R<=78.", + "first_step": "Search restored length-6 shear words whose query schedule admits coverings with R<=78.", + "blocked_by": "No such covering census is claimed here." + }, + { + "question": "Does the same component+census method give a sharp XOR floor at eight queries?", + "why_it_matters": "Completes the intermediate-query XOR side of the unequal-price handoff.", + "first_step": "Extend the restored-graph census to the first length with n+c<=8 and match an attaining word.", + "blocked_by": "Larger search." + } + ], + "predecessors": [ + { + "pr": 1898, + "credit": "Arham Tahir; minimum-query endpoint and abstract tariff fixture" + }, + { + "pr": 2455, + "credit": "ywz65; component lemma and meet-in-the-middle restored census at six queries" + }, + { + "pr": 1370, + "credit": "Arham Tahir; path-local shear lowering / four-X word" + }, + { + "pr": 1524, + "credit": "TennisBowling; equal-price theorem / unequal-price handoff" + } + ] +} diff --git a/research/seven-query-xor-floor/VERIFY.json b/research/seven-query-xor-floor/VERIFY.json new file mode 100644 index 0000000000..dfde2aabd5 --- /dev/null +++ b/research/seven-query-xor-floor/VERIFY.json @@ -0,0 +1,52 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/mutable-source-shear-cost/CERTIFICATE.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Restored-graph census through X=6, component floors, PR2455 digest cross-check, champion identity, certificate match, source pins" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same admission under PYTHONOPTIMIZE via need()" + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 120, + "checks": "Separate column-image census and champion F2 replay" + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 300, + "checks": "Corruption rejection, duplicate JSON keys, -O controls" + } + ] +} diff --git a/research/seven-query-xor-floor/independent.py b/research/seven-query-xor-floor/independent.py new file mode 100644 index 0000000000..e7a6136115 --- /dev/null +++ b/research/seven-query-xor-floor/independent.py @@ -0,0 +1,172 @@ +#!/usr/bin/env python3 +"""Independent column-image check of the Q=7 XOR floor. Wentao Li + AI, Apache-2.0.""" +from __future__ import annotations + +import hashlib +import itertools +import json +import sys +from pathlib import Path + +HERE = Path(__file__).resolve().parent +CERT_PATH = HERE / "CERTIFICATE.json" + + +def need(ok, message): + if not ok: + raise SystemExit(f"FAIL_INDEPENDENT: {message}") + + +def component_count(n, graph): + labels = list(range(n)) + for k, (s, t) in enumerate(itertools.combinations(range(n), 2)): + if graph >> k & 1: + a, b = labels[s], labels[t] + labels = [a if c == b else c for c in labels] + return len(set(labels)) + + +def operators(n): + edges = list(itertools.combinations(range(n), 2)) + return [ + (s, t, 1 << edges.index(tuple(sorted((s, t))))) + for s in range(n) + for t in range(n) + if s != t + ] + + +def shear_matrix(rows, s, t): + out = [list(r) for r in rows] + for col in range(len(out[0])): + out[t][col] ^= out[s][col] + return tuple(tuple(r) for r in out) + + +def half_layers_matrix(n, depth): + """Column-image variant: track n-by-n matrices over F2 explicitly.""" + identity = tuple(tuple(1 if i == j else 0 for j in range(n)) for i in range(n)) + layers = [{identity: {0}}] + for _ in range(depth): + nxt = {} + for rows, graphs in layers[-1].items(): + for s, t, bit in operators(n): + nxt.setdefault(shear_matrix(rows, s, t), set()).update(g | bit for g in graphs) + layers.append(nxt) + return layers + + +def census_matrix(n=5, bound=6): + layers = half_layers_matrix(n, (bound + 1) // 2) + out = [] + for length in range(bound + 1): + a, b = length // 2, (length + 1) // 2 + unions = set() + for rows, left in layers[a].items(): + unions.update(x | y for x in left for y in layers[b].get(rows, ())) + comps = [component_count(n, g) for g in unions] + out.append( + { + "length": length, + "identity_graphs": len(unions), + "minimum_components": min(comps) if comps else None, + "query_floor": (n + min(comps)) if comps else None, + "graphs_sha256": hashlib.sha256( + json.dumps(sorted(unions), separators=(",", ":")).encode() + ).hexdigest(), + } + ) + return out + + +def replay_champion_columns(closed): + """Direct F2 column simulation of path-lowered word on dirty basis.""" + n = 5 + # State: each role is an F2 vector of length n (source coordinates) plus + # a free dirty bit ignored for the AB image check on outputs. + # We track source images as n-bit masks on the initial basis. + x = [1 << j for j in range(n)] + z = 0 + y = [0] * 32 + # Build path word inline + slots = list(closed[:-1]) + reads = {} + for mask in range(1, 32): + found = None + for size in range(2, len(slots) + 1, 2): + for subset in itertools.combinations(range(len(slots)), size): + value = 0 + for i in subset: + value ^= slots[i] + if value == mask: + found = subset + break + if found is not None: + break + need(found is not None, f"uncovered mask {mask}") + reads[mask] = found + x_count = 0 + q_count = 0 + r_count = 0 + for step, point in enumerate(closed): + for mask, subset in reads.items(): + if step in subset: + y[mask] ^= z + r_count += 1 + if step + 1 >= len(closed): + break + delta = point ^ closed[step + 1] + target = (delta & -delta).bit_length() - 1 + donors = [j for j in range(5) if j != target and delta >> j & 1] + for j in donors: + x[target] ^= x[j] + x_count += 1 + z ^= x[target] + q_count += 1 + for j in reversed(donors): + x[target] ^= x[j] + x_count += 1 + need(q_count == 7 and x_count == 6 and r_count == 82, "champion counts") + need(x == [1 << j for j in range(n)], "sources unrestored") + need(z == 0, "connector unrestored") + for mask in range(1, 32): + want = 0 + for j in range(n): + if mask >> j & 1: + want ^= 1 << j + need(y[mask] == want, f"output mask {mask} wrong") + return {"Q": q_count, "R": r_count, "X": x_count} + + +def main(): + need(CERT_PATH.is_file(), "missing certificate") + cert = json.loads(CERT_PATH.read_text(encoding="utf-8")) + rows = census_matrix() + for row, expected in zip(rows, cert["census"]["by_length"]): + need(row["identity_graphs"] == expected["identity_graphs"], f"count at X={row['length']}") + need(row["minimum_components"] == expected["minimum_components"], f"min_c at X={row['length']}") + need(row["graphs_sha256"] == expected["graphs_sha256"], f"digest at X={row['length']}") + floor = row["query_floor"] + need(floor == expected["query_floor_n_plus_c"], f"floor at X={row['length']}") + for x in range(6): + floor = rows[x]["query_floor"] + need(floor is None or floor >= 8, f"independent: X={x} blocks Q=7") + need(rows[6]["query_floor"] == 7, "independent: X=6 allows Q=7") + + closed = tuple(cert["attaining_witness"]["closed_path"]) + bill = replay_champion_columns(closed) + need(bill["X"] == 6, "independent champion X") + tariff = 38 * bill["Q"] + 2 * bill["R"] + 2 * bill["X"] + need(tariff == 442, "independent tariff") + + # Edge bound control: 2 edges => >=3 components on 5 labels. + need(5 - 2 >= 3, "edge arithmetic") + print( + "PASS_INDEPENDENT_SEVEN_QUERY_XOR_FLOOR " + f"min_X=6 floors_block_X_le_5 champion={bill} tariff={tariff} controls=2" + ) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/research/seven-query-xor-floor/model.py b/research/seven-query-xor-floor/model.py new file mode 100644 index 0000000000..5c3106d430 --- /dev/null +++ b/research/seven-query-xor-floor/model.py @@ -0,0 +1,248 @@ +"""Seven-query source-XOR floor for the five-source mutable-source alphabet. + +Self-contained relative to PR1898 / PR2455 / the path-lowered 789q invoice. +Wentao Li with substantial AI assistance. Apache-2.0. +""" +from __future__ import annotations + +import hashlib +import itertools +import json +from collections import Counter + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def operators(n=5): + edges = list(itertools.combinations(range(n), 2)) + return [ + (s, t, 1 << edges.index(tuple(sorted((s, t))))) + for s in range(n) + for t in range(n) + if s != t + ] + + +def component_count(n, graph): + labels = list(range(n)) + for k, (s, t) in enumerate(itertools.combinations(range(n), 2)): + if graph >> k & 1: + a, b = labels[s], labels[t] + labels = [a if c == b else c for c in labels] + return len(set(labels)) + + +def shear(rows, s, t): + out = list(rows) + out[t] ^= out[s] + return tuple(out) + + +def half_layers(n, depth): + """All (exact matrix, all-used-edge graph) states at each XOR depth.""" + layers = [{tuple(1 << j for j in range(n)): {0}}] + for _ in range(depth): + nxt = {} + for rows, graphs in layers[-1].items(): + for s, t, bit in operators(n): + nxt.setdefault(shear(rows, s, t), set()).update(g | bit for g in graphs) + layers.append(nxt) + return layers + + +def meet_census(n=5, bound=6): + """Restored interaction graphs by XOR length via meet-in-the-middle. + + A word u followed by reverse(v) restores sources exactly when M(u)=M(v); + its interaction graph is G(u) union G(v). Technique credited to PR2455. + """ + layers = half_layers(n, (bound + 1) // 2) + by_length = [] + for length in range(bound + 1): + a, b = length // 2, (length + 1) // 2 + unions = set() + for rows, left in layers[a].items(): + unions.update(x | y for x in left for y in layers[b].get(rows, ())) + components = [component_count(n, g) for g in unions] + by_length.append( + { + "length": length, + "identity_graphs": len(unions), + "connected_identity_graphs": sum(c == 1 for c in components), + "minimum_components": min(components) if components else None, + "query_floor_n_plus_c": (n + min(components)) if components else None, + "graphs_sha256": hashlib.sha256( + json.dumps(sorted(unions), separators=(",", ":")).encode() + ).hexdigest(), + } + ) + digest_rows = [[list(rows), sorted(gs)] for rows, gs in sorted(layers[-1].items())] + return { + "n": n, + "bound": bound, + "raw_half_word_counts": [(n * (n - 1)) ** k for k in range(len(layers))], + "half_distinct_matrices": [len(layer) for layer in layers], + "half_matrix_graph_states": [sum(len(gs) for gs in layer.values()) for layer in layers], + "last_layer_sha256": hashlib.sha256( + json.dumps(digest_rows, separators=(",", ":")).encode() + ).hexdigest(), + "by_length": by_length, + } + + +def min_even_subset_R(slots): + """Minimum total even-subset readout count on connector prefix slots.""" + need(type(slots) is tuple and slots and slots[0] == 0, "slots must start at 0") + n = len(slots) + best = [99] * 32 + for bits in range(1 << n): + if bits.bit_count() % 2: + continue + value = 0 + for i in range(n): + if bits >> i & 1: + value ^= slots[i] + size = bits.bit_count() + if size < best[value]: + best[value] = size + if any(best[mask] >= 99 for mask in range(1, 32)): + return None + return sum(best[1:]) + + +def even_subset_reads(slots): + n = len(slots) + reads = {} + for mask in range(1, 32): + found = None + for size in range(2, n + 1, 2): + for subset in itertools.combinations(range(n), size): + value = 0 + for i in subset: + value ^= slots[i] + if value == mask: + found = subset + break + if found is not None: + break + need(found is not None, f"mask {mask} uncovered") + reads[mask] = found + return reads + + +def path_X(closed): + total = 0 + for a, b in zip(closed, closed[1:]): + delta = a ^ b + need(delta != 0, "zero query edge") + total += 2 * (delta.bit_count() - 1) + return total + + +def path_word(closed): + need(closed[0] == closed[-1] == 0, "path is not closed") + slots = tuple(closed[:-1]) + reads = even_subset_reads(slots) + word = [] + for step, point in enumerate(closed): + word += [["R", mask] for mask, subset in reads.items() if step in subset] + if step + 1 >= len(closed): + break + delta = point ^ closed[step + 1] + need(delta != 0, "zero query edge") + target = (delta & -delta).bit_length() - 1 + donors = [j for j in range(5) if j != target and delta >> j & 1] + word += [["X", j, target] for j in donors] + word.append(["Q", target]) + word += [["X", j, target] for j in reversed(donors)] + return word + + +def root_ops(word, n=5): + out = [] + for event in word: + kind = event[0] + if kind == "Q": + out.append(["B", f"x{event[1]}", "z"]) + elif kind == "R": + out.append([f"A{event[1]}", "z", f"y{event[1]}"]) + elif kind == "X": + out.append(["", f"x{event[1]}", f"x{event[2]}"]) + else: + raise ValueError("unknown root operation") + return out + + +def roles(n=5): + return [f"x{j}" for j in range(n)] + [f"y{m}" for m in range(1, 1 << n)] + ["z"] + [ + f"w{j}" for j in range(3) + ] + + +def interpret(operations, names, initial=None): + state = {r: {(r,)} for r in names} if initial is None else {r: set(p) for r, p in initial.items()} + for coefficient, source, target in operations: + need(source in state and target in state and source != target, "invalid port") + terms = state[source] if coefficient == "" else {(coefficient,) + term for term in state[source]} + state[target].symmetric_difference_update(terms) + return state + + +def expected(n=5): + state = {r: {(r,)} for r in roles(n)} + for mask in range(1, 1 << n): + for j in range(n): + if mask >> j & 1: + state[f"y{mask}"].symmetric_difference_update({(f"A{mask}", "B", f"x{j}")}) + return state + + +def check_identity(word, n=5): + ops = root_ops(word, n) + result = interpret(ops, roles(n)) + need(result == expected(n), "dirty root map or restoration failed") + need( + interpret(ops[::-1], roles(n), result) == {r: {(r,)} for r in roles(n)}, + "root inverse failed", + ) + return Counter(event[0] for event in word) + + +def invoice(word): + counts = Counter(event[0] for event in word) + leaves = 28 * counts["Q"] + counts["R"] + nodes = 9 * counts["Q"] + dispatch = len(word) + return { + "Q": counts["Q"], + "R": counts["R"], + "X": counts["X"], + "map_leaves": leaves, + "echo_nodes": nodes, + "root_dispatches": dispatch, + "borrowed_dirty_rows": 4, + "tariff": leaves + nodes + counts["X"] + dispatch, + "complete_prices": {"b": 38, "a": 2, "x": 2}, + } + + +# Credited path-lowered champion from the 789q invoice lineage (PR1898 alphabet). +CHAMPION_7 = (0, 1, 2, 6, 12, 24, 16, 0) + +# Cross-check digests vs open PR2455 RESULT.json for lengths present there. +PR2455_GRAPH_DIGESTS = { + 0: "d0bca111f8628137adc4c16f123496dcdd1d590d06cb5d9acd68b39fe656fb97", + 1: "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + 2: "0899bb1953bc4b09e040dbb8308c5c134c718d3cfe052d06ff64baed6062eb7f", + 3: "4f53cda18c2baa0c0354bb5f9a3ecbe5ed12ab4d8e11ba873c2f11161202b945", + 4: "546640ef872e4f0d2ebda17f74c88eeea8ccff09cb9e16de7cff2ff6735cd024", + 5: "defa9e87f9e7cc3a75d63330d451e5d1c8cd011734d1a489ec0d84af6ba68504", + 6: "163a9c5ccd357bfc55f07c641213f247253db4894f6798c6e75c94104e2be060", +} + +# PR2455's published last_layer_sha256 is for half-depth 4 (bound=7). This +# package's claim only needs bound=6 (half-depth 3); per-length graph digests +# 0..6 are the load-bearing cross-check. diff --git a/research/seven-query-xor-floor/test_package.py b/research/seven-query-xor-floor/test_package.py new file mode 100644 index 0000000000..e917e8a8d1 --- /dev/null +++ b/research/seven-query-xor-floor/test_package.py @@ -0,0 +1,101 @@ +#!/usr/bin/env python3 +"""Package fault controls for the seven-query XOR floor. Wentao Li + AI, Apache-2.0.""" +from __future__ import annotations + +import json +import shutil +import subprocess +import sys +import tempfile +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PKG_NAME = "seven-query-xor-floor" + + +def need(ok, message): + if not ok: + raise SystemExit(f"FAIL_TEST: {message}") + + +def run(args, cwd=None): + return subprocess.run(args, cwd=cwd or ROOT, text=True, capture_output=True) + + +def main(): + # 1) Default read-only verify. + proc = run([sys.executable, "-I", "-B", str(HERE / "verify.py")]) + need(proc.returncode == 0, proc.stderr + proc.stdout) + need("PASS_SEVEN_QUERY_XOR_FLOOR" in proc.stdout, proc.stdout) + + # 2) -O admission via need(). + proc = run([sys.executable, "-I", "-O", "-B", str(HERE / "verify.py")]) + need(proc.returncode == 0, proc.stderr + proc.stdout) + need("PASS_SEVEN_QUERY_XOR_FLOOR" in proc.stdout, proc.stdout) + + # 3) Certificate corruption rejection on a temp checkout layout. + with tempfile.TemporaryDirectory() as tmp: + tmp_path = Path(tmp) + research = tmp_path / "research" / PKG_NAME + shutil.copytree(HERE, research) + pinned = tmp_path / "research" / "mutable-source-shear-cost" + pinned.mkdir(parents=True) + shutil.copy2( + ROOT / "research" / "mutable-source-shear-cost" / "CERTIFICATE.json", + pinned / "CERTIFICATE.json", + ) + cert = research / "CERTIFICATE.json" + data = json.loads(cert.read_text(encoding="utf-8")) + data["claim"]["min_X"] = 0 + cert.write_text(json.dumps(data, indent=2) + "\n", encoding="utf-8") + proc = run([sys.executable, "-I", "-B", str(research / "verify.py")], cwd=tmp_path) + need(proc.returncode != 0, "corrupted certificate should fail") + + # 4) Source pin corruption rejection. + with tempfile.TemporaryDirectory() as tmp: + tmp_path = Path(tmp) + research = tmp_path / "research" / PKG_NAME + shutil.copytree(HERE, research) + pinned = tmp_path / "research" / "mutable-source-shear-cost" + pinned.mkdir(parents=True) + src = ROOT / "research" / "mutable-source-shear-cost" / "CERTIFICATE.json" + (pinned / "CERTIFICATE.json").write_bytes(src.read_bytes() + b"\n") + proc = run([sys.executable, "-I", "-B", str(research / "verify.py")], cwd=tmp_path) + need(proc.returncode != 0, "source drift should fail") + + # 5) Independent checker. + proc = run([sys.executable, "-I", "-B", str(HERE / "independent.py")]) + need(proc.returncode == 0, proc.stderr + proc.stdout) + need("PASS_INDEPENDENT_SEVEN_QUERY_XOR_FLOOR" in proc.stdout, proc.stdout) + + # 6) Duplicate JSON key rejection. + with tempfile.TemporaryDirectory() as tmp: + tmp_path = Path(tmp) + research = tmp_path / "research" / PKG_NAME + shutil.copytree(HERE, research) + pinned = tmp_path / "research" / "mutable-source-shear-cost" + pinned.mkdir(parents=True) + shutil.copy2( + ROOT / "research" / "mutable-source-shear-cost" / "CERTIFICATE.json", + pinned / "CERTIFICATE.json", + ) + cert = research / "CERTIFICATE.json" + raw = cert.read_text(encoding="utf-8") + # Inject a duplicate top-level key after the opening brace content. + corrupted = raw.replace( + '"schema_version": 1,', + '"schema_version": 1,\n "schema_version": 2,', + 1, + ) + need(corrupted != raw, "failed to inject duplicate key") + cert.write_text(corrupted, encoding="utf-8") + proc = run([sys.executable, "-I", "-B", str(research / "verify.py")], cwd=tmp_path) + need(proc.returncode != 0, "duplicate JSON key should fail") + + print("PASS_SEVEN_QUERY_XOR_FLOOR_PACKAGE_TESTS groups=6") + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/research/seven-query-xor-floor/verify.py b/research/seven-query-xor-floor/verify.py new file mode 100644 index 0000000000..8fc4b51501 --- /dev/null +++ b/research/seven-query-xor-floor/verify.py @@ -0,0 +1,186 @@ +#!/usr/bin/env python3 +"""Exact seven-query source-XOR floor; read-only default. Wentao Li + AI, Apache-2.0.""" +from __future__ import annotations + +import argparse +import hashlib +import json +import sys +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(HERE)) +from model import ( # noqa: E402 + CHAMPION_7, + PR2455_GRAPH_DIGESTS, + check_identity, + invoice, + meet_census, + min_even_subset_R, + path_X, + path_word, +) + +CERT_PATH = HERE / "CERTIFICATE.json" +SOURCES_PATH = HERE / "SOURCES.json" + + +def need(ok, message): + if not ok: + raise SystemExit(f"FAIL: {message}") + + +def sha256(path: Path) -> str: + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def load_json_reject_duplicates(path: Path): + text = path.read_text(encoding="utf-8") + + def _hook(pairs): + out = {} + for key, value in pairs: + if key in out: + raise ValueError(f"duplicate JSON key {key!r} in {path}") + out[key] = value + return out + + return json.loads(text, object_pairs_hook=_hook) + + +def check_source_pins(): + sources = load_json_reject_duplicates(SOURCES_PATH) + for rec in sources["files"]: + if rec["usage"] != "input": + continue + live = ROOT / rec["path"] + need(live.is_file(), f"missing input {rec['path']}") + need(sha256(live) == rec["sha256"], f"source bytes mismatch: {rec['path']}") + + +def build_certificate(): + census = meet_census(n=5, bound=6) + for row in census["by_length"]: + length = row["length"] + need(row["graphs_sha256"] == PR2455_GRAPH_DIGESTS[length], f"digest drift at X={length}") + need(row["connected_identity_graphs"] == 0, f"unexpected connected restore at X={length}") + + # Component+census floors: first X with query_floor <= 7 is X=6. + # String keys so JSON round-trips compare equal. + floors = {str(row["length"]): row["query_floor_n_plus_c"] for row in census["by_length"]} + need(floors["0"] == 10, "X=0 floor") + need(floors["2"] == 9, "X=2 floor") + need(floors["4"] == 8, "X=4 floor") + need(floors["5"] == 8, "X=5 floor") + need(floors["6"] == 7, "X=6 floor") + need(floors["1"] is None and floors["3"] is None, "odd-length restores should be empty") + for x in range(6): + floor = floors[str(x)] + need(floor is None or floor >= 8, f"X={x} must not admit Q=7") + need(floors["6"] == 7, "X=6 admits Q=7 via c=2") + + # Attaining path-lowered witness at X=6 (credited 789q champion). + closed = CHAMPION_7 + need(path_X(closed) == 6, "champion path_X") + slots = tuple(closed[:-1]) + r_total = min_even_subset_R(slots) + need(r_total == 82, "champion even-subset R") + word = path_word(closed) + counts = check_identity(word) + need(counts["Q"] == 7 and counts["X"] == 6 and counts["R"] == 82, "champion bill") + bill = invoice(word) + need(bill["tariff"] == 442, "champion tariff") + + # Edge-count soft bound: X<=2 simple edges => c>=3 => Q>=8 (independent of census). + # Census strengthens X=2 to c>=4 / Q>=9 and excludes X<=5 for Q=7. + edge_bound = { + "argument": "Any interaction graph with e undirected edges on n=5 labels has c>=n-e components. For e<=2, c>=3 so Q>=n+c>=8. Census tightens X=2 to c>=4.", + "X_le_2_query_floor_from_edges": 8, + "X_le_2_query_floor_from_census": 9, + } + + return { + "schema_version": 1, + "status": "PASS_SEVEN_QUERY_XOR_FLOOR", + "scope": ( + "Five-source common-B mutable-source Q/R/X alphabet (PR1898). " + "Restored straight-line words. Exact minimum source-XOR count at Q=7." + ), + "claim": { + "Q": 7, + "min_X": 6, + "sharp": True, + "answers_789q_oq1": "No non-path (or path) schedule at Q=7 can reach X<=2; in fact X<=5 is impossible.", + "no_new_kappa": True, + }, + "component_lemma": { + "statement": "An interaction graph with c components forces at least n+c queries on n sources.", + "n": 5, + }, + "edge_bound": edge_bound, + "census": census, + "query_floors_by_X": floors, + "attaining_witness": { + "kind": "path_lowered_even_subset", + "closed_path": list(closed), + "Q": 7, + "R": 82, + "X": 6, + "tariff_at_38_2_2": bill["tariff"], + "invoice": bill, + "credit": "Path-lowered champion from mutable-source-789q-invoice lineage; PR1898 alphabet.", + }, + "pr2455_crosscheck": { + "matched_graph_digests_0_through_6": True, + "note": "Open PR2455 proves X>=8 at Q=6; this package reuses the same meet-in-the-middle census through X=6 for the Q=7 floor. Per-length graph digests match that package's RESULT.json.", + }, + "new_kappa": False, + } + + +def compare_cert(fresh, committed): + need(committed.get("status") == "PASS_SEVEN_QUERY_XOR_FLOOR", "bad certificate status") + need(fresh["claim"] == committed["claim"], "claim drift") + need(fresh["query_floors_by_X"] == committed["query_floors_by_X"], "floor drift") + need(fresh["census"]["by_length"] == committed["census"]["by_length"], "census drift") + need( + fresh["census"]["last_layer_sha256"] == committed["census"]["last_layer_sha256"], + "layer digest drift", + ) + need(fresh["attaining_witness"]["X"] == committed["attaining_witness"]["X"], "witness X drift") + need( + fresh["attaining_witness"]["tariff_at_38_2_2"] + == committed["attaining_witness"]["tariff_at_38_2_2"], + "witness tariff drift", + ) + + +def main(argv=None): + ap = argparse.ArgumentParser(description=__doc__) + ap.add_argument("--write", action="store_true", help="regenerate CERTIFICATE.json") + args = ap.parse_args(argv) + + check_source_pins() + fresh = build_certificate() + + if args.write: + CERT_PATH.write_text(json.dumps(fresh, indent=2) + "\n", encoding="utf-8") + print("WROTE_CERTIFICATE", CERT_PATH) + else: + need(CERT_PATH.is_file(), "missing CERTIFICATE.json; author with --write") + committed = load_json_reject_duplicates(CERT_PATH) + compare_cert(fresh, committed) + + print( + "PASS_SEVEN_QUERY_XOR_FLOOR " + "Q=7 min_X=6 sharp " + "X<=5 blocked " + "answers_789q_oq1 " + "no_new_kappa" + ) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main())