From 0e5f24d033eba7a36e6fc990d7263dc4c2ee9183 Mon Sep 17 00:00:00 2001 From: Wentao Li Date: Thu, 15 Oct 2026 16:56:12 +0000 Subject: [PATCH] Research: prove even-subset R floor 82 among X=6 at seven queries Answers #2643 OQ1 in the PR1898 alphabet: covering Q=7 walks have R in {82,88,96}, so min R among X=6 is exactly 82 (sharp via champion). Repeated prefixes cannot undercut; tariff floor 442 does not beat 436. Prepared by Wentao Li with substantial AI assistance. --- research/seven-query-r-floor/CERTIFICATE.json | 160 +++++++++ research/seven-query-r-floor/NOTICE.md | 21 ++ research/seven-query-r-floor/PROOF.md | 96 +++++ research/seven-query-r-floor/README.md | 95 +++++ research/seven-query-r-floor/SOURCES.json | 24 ++ research/seven-query-r-floor/TASK.json | 88 +++++ research/seven-query-r-floor/VERIFY.json | 52 +++ research/seven-query-r-floor/independent.py | 223 ++++++++++++ research/seven-query-r-floor/model.py | 333 ++++++++++++++++++ research/seven-query-r-floor/test_package.py | 100 ++++++ research/seven-query-r-floor/verify.py | 233 ++++++++++++ 11 files changed, 1425 insertions(+) create mode 100644 research/seven-query-r-floor/CERTIFICATE.json create mode 100644 research/seven-query-r-floor/NOTICE.md create mode 100644 research/seven-query-r-floor/PROOF.md create mode 100644 research/seven-query-r-floor/README.md create mode 100644 research/seven-query-r-floor/SOURCES.json create mode 100644 research/seven-query-r-floor/TASK.json create mode 100644 research/seven-query-r-floor/VERIFY.json create mode 100644 research/seven-query-r-floor/independent.py create mode 100644 research/seven-query-r-floor/model.py create mode 100644 research/seven-query-r-floor/test_package.py create mode 100644 research/seven-query-r-floor/verify.py diff --git a/research/seven-query-r-floor/CERTIFICATE.json b/research/seven-query-r-floor/CERTIFICATE.json new file mode 100644 index 0000000000..1beb9f97b6 --- /dev/null +++ b/research/seven-query-r-floor/CERTIFICATE.json @@ -0,0 +1,160 @@ +{ + "schema_version": 1, + "status": "PASS_SEVEN_QUERY_R_FLOOR", + "scope": "Five-source common-B mutable-source Q/R/X alphabet (PR1898). Even-subset readout on connector states of restored straight-line words with exactly seven queries. Exact minimum R among words with X=6.", + "claim": { + "Q": 7, + "min_R_among_X_eq_6": 82, + "min_R_even_subset_all_walks": 82, + "sharp": true, + "answers_7qxor_oq1": "Minimum even-subset R among restored seven-query words with X=6 is exactly 82; R<=78 is impossible in this readout class, so the abstract tariff cannot undercut 436 via lower R at X=6.", + "no_new_kappa": true + }, + "classification": { + "distinct_six_nonzero": { + "covering_sets": 583296, + "attainable_R": [ + 82, + 88 + ], + "histogram": { + "82": 97216, + "88": 486080 + }, + "first_witnesses": { + "82": [ + 0, + 1, + 2, + 4, + 8, + 15, + 16 + ], + "88": [ + 0, + 1, + 2, + 3, + 4, + 8, + 16 + ] + }, + "min_R": 82 + }, + "one_repeat_spanning_five": { + "kind": "one_repeat_on_standard_basis", + "covering_walks": 1680, + "attainable_R": [ + 96 + ], + "histogram": { + "96": 1680 + }, + "min_R": 96, + "first_witness": [ + 0, + 1, + 0, + 2, + 4, + 8, + 16 + ], + "argument": "GL(5) reduces every spanning 5-set one-repeat covering walk to this basis census; R totals are invariant. Only R=96 occurs." + }, + "span_obstruction_samples": [ + { + "labels": [ + 1, + 2, + 4, + 8 + ], + "rank": 4, + "best_even_subset_image_size": 16, + "covers_all_31": false, + "note": "rank4_omit_16" + }, + { + "labels": [ + 1, + 2, + 3, + 4, + 5 + ], + "rank": 3, + "best_even_subset_image_size": 8, + "covers_all_31": false, + "note": "rank3_dependent_five" + }, + { + "labels": [ + 1, + 2, + 4, + 8, + 3 + ], + "rank": 4, + "best_even_subset_image_size": 16, + "covers_all_31": false, + "note": "rank4_five_with_sum" + } + ], + "argument": "A covering even-subset slot list of length 7 must span F2^5, so it uses at least five linearly independent nonzero labels. With six intermediate slots after the leading 0, the covering cases are: (i) six distinct nonzero labels (Hamilton walks; R in {82,88}); (ii) five spanning nonzero labels with exactly one repeated vertex (R=96 on the GL(5) basis census). Fewer independent labels cannot cover. Therefore min R = 82." + }, + "xor_floor_citation": { + "object": "research/seven-query-xor-floor (CrocSwap #2643)", + "statement": "Every restored seven-query word needs X>=6; sharp via the same champion.", + "use_here": "Together with min even-subset R=82, every X=6 word has R>=82.", + "not_reopened": true + }, + "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 / seven-query-xor-floor lineage; PR1898 alphabet." + }, + "tariff": { + "complete_prices": { + "b": 38, + "a": 2, + "x": 2 + }, + "six_query_endpoint": 436, + "beat_436_at_Q7_X6_requires_R_le": 78, + "min_tariff_at_Q7_X6": 442, + "undercuts_436": false + }, + "new_kappa": false +} diff --git a/research/seven-query-r-floor/NOTICE.md b/research/seven-query-r-floor/NOTICE.md new file mode 100644 index 0000000000..f30cb8402a --- /dev/null +++ b/research/seven-query-r-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 restored interaction-graph census at six queries. +- 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` — distinct-slot + `R ∈ {82,88}` spectrum and champion path; that package is not edited. +- Open #2643 `research/seven-query-xor-floor` — restored `X ≥ 6` at `Q = 7` + and OQ1 answered here; that package is not edited. +- Live pin: `research/mutable-source-shear-cost/CERTIFICATE.json`. + +Prepared by Wentao Li (VictorLiwentao, @Is__Victor) with substantial AI +assistance. diff --git a/research/seven-query-r-floor/PROOF.md b/research/seven-query-r-floor/PROOF.md new file mode 100644 index 0000000000..1774ff169b --- /dev/null +++ b/research/seven-query-r-floor/PROOF.md @@ -0,0 +1,96 @@ +# Exact even-subset readout floor at seven queries among X = 6 + +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 readout optimum +outside the even-subset connector-state class. + +It answers open question 1 of +[CrocSwap/integer-mult-bounds#2643](https://github.com/CrocSwap/integer-mult-bounds/pull/2643) +(`research/seven-query-xor-floor`): what is the minimum readout count `R` +among restored seven-query words with `X = 6`? Under even-subset readout on +connector states, the answer is **exactly 82**. + +## Setup + +Retain five distinct arbitrary-dirty F₂ source rows, thirty-one outputs, a +connector, and private scratch. Complete calls are `Q_j`, `R_m`, and paid +`X_(s,t)` as in PR1898. Straight-line words are data-independent; sources and +connector restore. + +Each query contributes an effective F₂⁵ mask (the current linear form of the +queried source). Connector restoration forces those seven masks to sum to +zero, so the connector state follows a **closed walk of length 7** in F₂⁵. +Even-subset readout prices a slot list `(s₀,…,s₆)` with `s₀ = 0` by + +```text +R = Σ_{m=1}^{31} min{|T| : T ⊂ {0,…,6}, |T| even, ⊕_{i∈T} s_i = m}. +``` + +Zero query edges are forbidden, so consecutive slots differ and the return +edge to 0 is present (`s₆ ≠ 0`). + +## Classification of covering walks + +A covering slot list must realize every nonzero mask, so the F₂-span of its +slot values is all of F₂⁵. Hence it uses at least five linearly independent +nonzero labels. With only six slots after the leading 0, the covering cases +are: + +1. **Six distinct nonzero labels.** The intermediate slots are a permutation + of those labels (Hamilton walks on `{0} ∪ S`). Exhaustive even-subset + census over all `C(31,6)` choices yields covering sets only, with + attainable totals **`R ∈ {82, 88}`** (histogram `97216` / `486080`). +2. **Five spanning nonzero labels with exactly one repeated vertex.** Any + such spanning 5-set is `GL(5)`-equivalent to the standard basis + `{1,2,4,8,16}`, and the even-subset total `R` is `GL(5)`-invariant. + The basis census of valid one-repeat walks (extra visit to `0`, or one + basis vector doubled) covers in every case with **`R = 96` only** + (`1680` walks). +3. **Fewer than five independent nonzero labels.** The even-subset image lies + in a proper subspace, so some masks are missed. Explicit dependent samples + stay at image size `≤ 16`. + +Therefore every covering Q=7 even-subset schedule has `R ∈ {82, 88, 96}`, and +the global minimum is **82**. + +## Minimum R among X = 6 + +Open [#2643](https://github.com/CrocSwap/integer-mult-bounds/pull/2643) proves +that every restored seven-query word needs `X ≥ 6` (sharp). Combined with +`R ≥ 82` in the even-subset class, every restored seven-query word with +`X = 6` has even-subset `R ≥ 82`. + +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)`). +Dirty root and inverse identities hold. Thus the minimum is **exactly 82**. + +## Tariff consequence + +At `Q = 7` and `X = 6`, tariff `38·7 + 2R + 2·6 = 278 + 2R` undercuts the +six-query endpoint **436** iff `R ≤ 78`. The floor `R = 82` gives tariff +**442** and blocks that undercut inside the even-subset class. + +## Scope limits + +- No claim about readout alphabets cheaper than even-subset connector-state + combinations (odd-cardinality schedules, output mixing, extra connectors). +- Leave-alone objects through #2643 (including #2593 triadic and the XOR + floor package) and pending `mutable-source-789q-invoice` are not edited. +- No physical common-B hosting, precision, tape, or new kappa. + +## Relation to predecessors + +| Prior | Already proves | This package adds | +|---|---|---| +| PR1898 | Min `Q = 6`, endpoint tariff 436 | — | +| PR2455 (open) | `X ≥ 8` at `Q = 6` | — | +| 789q invoice (fork) | Path-class distinct-slot `R ∈ {82,88}` at `Q = 7` | — | +| #2643 seven-query XOR floor | `X ≥ 6` at `Q = 7`, sharp; OQ1 asks min `R` at `X = 6` | — | +| **This** | — | **Min even-subset `R` at `Q = 7` is 82 even with repeats; hence min `R` among `X = 6` is 82** | diff --git a/research/seven-query-r-floor/README.md b/research/seven-query-r-floor/README.md new file mode 100644 index 0000000000..2a53a5eb0b --- /dev/null +++ b/research/seven-query-r-floor/README.md @@ -0,0 +1,95 @@ +# Seven-query even-subset R floor among X = 6 is exactly 82 + +**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** and even-subset +connector-state readout needs **at least 82 readouts**. Among words with +**`X = 6`**, that floor is sharp: the 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 +[#2643](https://github.com/CrocSwap/integer-mult-bounds/pull/2643) +(`research/seven-query-xor-floor`): the minimum `R` among restored seven-query +words with `X = 6` is **exactly 82** in the even-subset class. In particular +`R ≤ 78` is impossible, so tariff `38·7 + 2R + 2·6` cannot undercut the +six-query endpoint **436** by lowering `R` at `X = 6`. + +| Covering walk class | Distinct nonzero labels | Attainable even-subset R | +|---|---:|---| +| Hamilton (distinct slots) | 6 | **{82, 88}** | +| One repeated vertex (GL basis census) | 5 spanning | **{96}** | +| Rank `< 5` label sets | ≤4 independent | none (image ≤16) | + +The distinct-slot spectrum matches the path-lowered 789q invoice. Allowing +repeated prefixes cannot beat 82: the only additional covering layer is +`R = 96`. Combined with #2643's restored XOR floor `X ≥ 6`, every `X = 6` +word has `R ≥ 82`. + +## Reproduce + +Python **3.12**, standard library only, from the repository root: + +```sh +python3.12 -I -B research/seven-query-r-floor/verify.py +python3.12 -I -O -B research/seven-query-r-floor/verify.py +python3.12 -I -B research/seven-query-r-floor/independent.py +python3.12 -I -B research/seven-query-r-floor/test_package.py +python3.12 -B scripts/research_package.py --package research/seven-query-r-floor +``` + +Expected: + +```text +PASS_SEVEN_QUERY_R_FLOOR Q=7 min_R_among_X=6 is 82 sharp repeat_layer_R=96 answers_7qxor_oq1 tariff_floor=442 no_new_kappa +PASS_INDEPENDENT_SEVEN_QUERY_R_FLOOR min_R=82 ... tariff=442 answers_7qxor_oq1 +PASS_SEVEN_QUERY_R_FLOOR_PACKAGE_TESTS groups=6 +PASS_REGISTERED_RESEARCH_PACKAGE research/seven-query-r-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, open PR2455, fork path-lowered `mutable-source-789q-invoice` (distinct +slot spectrum; not edited), and open #2643 seven-query XOR floor (OQ1; leave +alone). Leave-alone through #2643 including #2593 triadic is respected. + +Closest prior: 789q prices path-class distinct-slot `R ∈ {82,88}` but does not +classify repeated-prefix coverings; #2643 proves `X ≥ 6` and leaves min `R` at +`X = 6` open. This freestanding package closes that readout obligation. + +## Open next questions + +1. Can a readout alphabet strictly cheaper than even-subset connector-state + combinations reach `R ≤ 78` at `Q = 7` with `X = 6`? + Why it matters: only then could seven queries undercut tariff 436 at the + #2643 XOR floor. First step: define one priced odd-cardinality or + multi-connector readout model and re-run the walk census. Blocked by: no + cheaper covering witness is known. +2. Does the same walk classification give an exact min `R` at eight queries + with the #2643-style XOR floor? + Why it matters: completes the intermediate-query unequal-price handoff. + First step: extend covering censuses to length-8 walks (including repeats). + Blocked by: larger search. + +## Credit + +Credit **Arham Tahir / PR1898** (alphabet, minimum-query endpoint, abstract +tariff), **ywz65 / PR2455** (six-query XOR necessity), **PR1370** (path-local +shear lowering), the fork **789q invoice** lineage (distinct-slot spectrum and +champion), open **#2643** (XOR floor; OQ1 answered here; not edited), +**TennisBowling / PR1524**, **Ross Richardson / PR943**, and the retained +mutable-source lineage. Live input pin: +`research/mutable-source-shear-cost/CERTIFICATE.json`. 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-r-floor/SOURCES.json b/research/seven-query-r-floor/SOURCES.json new file mode 100644 index 0000000000..719b378cbd --- /dev/null +++ b/research/seven-query-r-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-r-floor/TASK.json b/research/seven-query-r-floor/TASK.json new file mode 100644 index 0000000000..e703e5ffb5 --- /dev/null +++ b/research/seven-query-r-floor/TASK.json @@ -0,0 +1,88 @@ +{ + "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 even-subset readout count R among restored seven-query words with X=6 in the PR1898 five-source alphabet: R=82 sharp; classify repeated-prefix coverings at R=96; answer #2643 OQ1 and block tariff undercut via R<=78.", + "scope_change_reason": "The drawn connector-alphabet card is redirected to the explicit unpaid min-R-at-X=6 open question left by #2643 / the #1898/#2455/789q lineage, which is the nearest priced obstruction outside leave-alone tooling hosts and the in-flight leave-alones through #2643.", + "bottleneck_link": "A sharp seven-query R floor at the #2643 XOR minimum prices whether intermediate query counts can undercut the six-query endpoint by cheaper readout.", + "budget_minutes": 60, + "stop_rule": "Stop after walk classification (distinct-6 + one-repeat + span obstruction), champion sharpness, tariff consequence, package tests; no cheaper-than-even-subset readout search.", + "outcome": "completed", + "evidence": "CERTIFICATE.json distinct-6 histogram {82:97216,88:486080}, one-repeat basis census R=96 only (1680 walks), dependent-span image samples, champion 7Q/82R/6X identity and tariff 442, independent checker, corruption controls.", + "author": "Wentao Li", + "ai_assistance": "Substantial AI assistance for derivation, implementation, checking and writing.", + "open_questions": [ + { + "question": "Can a readout alphabet strictly cheaper than even-subset connector-state combinations reach R<=78 at Q=7 with X=6?", + "why_it_matters": "Only then could seven queries undercut tariff 436 at the #2643 XOR floor.", + "first_step": "Define one priced odd-cardinality or multi-connector readout model and re-run the walk census.", + "blocked_by": "No cheaper covering witness is known." + }, + { + "question": "Does the same walk classification give an exact min R at eight queries with the #2643-style XOR floor?", + "why_it_matters": "Completes the intermediate-query unequal-price handoff.", + "first_step": "Extend covering censuses to length-8 walks including repeats.", + "blocked_by": "Larger search." + } + ], + "predecessors": [ + { + "pr": 1898, + "credit": "Arham Tahir; minimum-query endpoint and abstract tariff fixture" + }, + { + "pr": 2455, + "credit": "ywz65; six-query XOR necessity" + }, + { + "pr": 2643, + "credit": "Wentao Li; seven-query XOR floor X>=6 and OQ1 answered here" + }, + { + "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-r-floor/VERIFY.json b/research/seven-query-r-floor/VERIFY.json new file mode 100644 index 0000000000..cd68b14dda --- /dev/null +++ b/research/seven-query-r-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": 300, + "checks": "Distinct-6 R spectrum, one-repeat GL basis census, span obstruction samples, champion identity, certificate match, source pins" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Same admission under PYTHONOPTIMIZE via need()" + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 300, + "checks": "Separate distinct-6 and repeat censuses, champion F2 replay, tariff arithmetic" + }, + { + "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-r-floor/independent.py b/research/seven-query-r-floor/independent.py new file mode 100644 index 0000000000..81861a313e --- /dev/null +++ b/research/seven-query-r-floor/independent.py @@ -0,0 +1,223 @@ +#!/usr/bin/env python3 +"""Independent Q=7 even-subset R classification and champion replay. + +Does not import model.py or verify.py. Prepared by Wentao Li with substantial +AI assistance. Apache-2.0. +""" +from __future__ import annotations + +import json +from collections import Counter +from itertools import combinations, combinations_with_replacement, permutations +from pathlib import Path + +HERE = Path(__file__).resolve().parent +CERT_PATH = HERE / "CERTIFICATE.json" +CHAMPION = (0, 1, 2, 6, 12, 24, 16, 0) +BASIS = (1, 2, 4, 8, 16) + + +def fail(message): + raise SystemExit(f"FAIL_INDEPENDENT: {message}") + + +def even_R(slots): + 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_image(slots): + n = len(slots) + image = set() + 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] + image.add(value) + return image + + +def tariff(q, r, x): + return (28 * q + r) + (9 * q) + x + (q + r + x) + + +def distinct6_spectrum(): + hist = Counter() + covering = 0 + for nonzero in combinations(range(1, 32), 6): + total = even_R((0,) + nonzero) + if total is None: + continue + covering += 1 + hist[total] += 1 + if sorted(hist) != [82, 88]: + fail(f"spectrum {sorted(hist)}") + if dict(hist) != {82: 97216, 88: 486080}: + fail(f"histogram {dict(hist)}") + if covering != 583296: + fail(f"covering {covering}") + return dict(hist) + + +def one_repeat_basis(): + hist = Counter() + covering = 0 + # Extra 0 + for j in range(1, 6): + rest = [i for i in range(1, 7) if i != j] + for perm in permutations(BASIS): + slots = [0] * 7 + slots[j] = 0 + for pos, val in zip(rest, perm): + slots[pos] = val + if any(slots[i] == slots[i + 1] for i in range(6)) or slots[6] == 0: + continue + total = even_R(tuple(slots)) + if total is None: + continue + covering += 1 + hist[total] += 1 + # Doubled basis vector + for dbl_idx in range(5): + others = [BASIS[i] for i in range(5) if i != dbl_idx] + for p1, p2 in combinations(range(1, 7), 2): + rest_pos = [i for i in range(1, 7) if i not in (p1, p2)] + for perm in permutations(others): + slots = [0] * 7 + slots[p1] = slots[p2] = BASIS[dbl_idx] + for pos, val in zip(rest_pos, perm): + slots[pos] = val + if any(slots[i] == slots[i + 1] for i in range(6)) or slots[6] == 0: + continue + total = even_R(tuple(slots)) + if total is None: + continue + covering += 1 + hist[total] += 1 + if sorted(hist) != [96]: + fail(f"repeat spectrum {sorted(hist)}") + if covering != 1680: + fail(f"repeat covering {covering}") + return covering, dict(hist) + + +def rank_obstruction(): + labels = (1, 2, 3, 4, 5) + best = 0 + for multi in combinations_with_replacement((0,) + labels, 6): + best = max(best, len(even_image((0,) + multi))) + if best >= 32: + fail(f"dependent set covered with image {best}") + return best + + +def path_x(closed): + total = 0 + for a, b in zip(closed, closed[1:]): + delta = a ^ b + if delta == 0: + fail("zero edge") + total += 2 * (delta.bit_count() - 1) + return total + + +def replay_champion(): + """Direct F2 column simulation of the path-lowered champion.""" + slots = list(CHAMPION[:-1]) + if even_R(tuple(slots)) != 82: + fail("champion R") + if path_x(CHAMPION) != 6: + fail("champion X") + # Connector walk + even-subset reads + path-local shears on formal AB image. + x = [1 << j for j in range(5)] + z = 0 + y = [0] * 32 + reads = {} + for mask in range(1, 32): + found = None + for size in range(2, len(slots) + 1, 2): + for subset in 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 + if found is None: + fail(f"uncovered {mask}") + reads[mask] = found + for step, point in enumerate(CHAMPION): + for mask, subset in reads.items(): + if step in subset: + y[mask] ^= z + if step + 1 >= len(CHAMPION): + break + delta = point ^ CHAMPION[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] + z ^= x[target] + for j in reversed(donors): + x[target] ^= x[j] + if x != [1 << j for j in range(5)] or z != 0: + fail("sources/connector not restored") + for mask in range(1, 32): + expected = 0 + for j in range(5): + if mask >> j & 1: + expected ^= 1 << j + # y holds connector snapshots; with B=id on masks, image should match mask bits. + if y[mask] != expected: + fail(f"output image mask {mask}: {y[mask]} != {expected}") + return 82, 6 + + +def main(): + hist = distinct6_spectrum() + cov, rh = one_repeat_basis() + img = rank_obstruction() + r, x = replay_champion() + if tariff(7, 82, 6) != 442: + fail("tariff") + if tariff(7, 78, 6) >= 436: + fail("R=78 threshold") + committed = json.loads(CERT_PATH.read_text(encoding="utf-8")) + if committed["claim"]["min_R_among_X_eq_6"] != 82: + fail("certificate claim") + if committed["classification"]["distinct_six_nonzero"]["histogram"] != { + str(k): v for k, v in hist.items() + }: + # hist keys are ints; certificate uses string keys + cert_hist = committed["classification"]["distinct_six_nonzero"]["histogram"] + if cert_hist != {str(k): v for k, v in hist.items()}: + fail("cert distinct hist mismatch") + print( + "PASS_INDEPENDENT_SEVEN_QUERY_R_FLOOR " + f"min_R=82 repeat_covering={cov} repeat_hist={rh} " + f"dep_image={img} champion_R={r} champion_X={x} tariff=442 " + "answers_7qxor_oq1" + ) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/research/seven-query-r-floor/model.py b/research/seven-query-r-floor/model.py new file mode 100644 index 0000000000..11343fbcee --- /dev/null +++ b/research/seven-query-r-floor/model.py @@ -0,0 +1,333 @@ +"""Seven-query even-subset readout floor for the five-source mutable-source alphabet. + +Self-contained relative to PR1898 / PR2455 / the path-lowered 789q invoice / +the seven-query XOR floor (#2643). Prepared by Wentao Li with substantial AI +assistance. Apache-2.0. +""" +from __future__ import annotations + +import itertools +from collections import Counter +from itertools import combinations, permutations + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def min_even_subset_R(slots): + """Minimum total even-subset readout count on connector prefix slots. + + ``slots[0]`` must be 0. The final restored 0 is identified with slot 0, so + ``slots`` lists the Q connector states before the closing query edge. + """ + 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_image(slots): + n = len(slots) + image = set() + 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] + image.add(value) + return image + + +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 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): + """Paid source-XOR count under path-local compute/uncompute lowering.""" + 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 rank_f2(vectors, dim=5): + mat = list(vectors) + rank = 0 + for bit in range(dim): + pivot = next((i for i in range(rank, len(mat)) if mat[i] >> bit & 1), None) + if pivot is None: + continue + mat[rank], mat[pivot] = mat[pivot], mat[rank] + for i in range(len(mat)): + if i != rank and mat[i] >> bit & 1: + mat[i] ^= mat[rank] + rank += 1 + return rank + + +def rank_increments(closed): + return rank_f2([closed[i] ^ closed[i + 1] for i in range(len(closed) - 1)]) + + +def valid_walk_slots(slots): + """Closed Q=7 walk: start at 0, no zero edges, return edge to 0 present.""" + if type(slots) is not tuple or len(slots) != 7 or slots[0] != 0: + return False + if slots[-1] == 0: + return False + if any(slots[i] == slots[i + 1] for i in range(6)): + return False + return True + + +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}, + } + + +def tariff_qrx(q, r, x): + """Abstract complete-call tariff at (b,a,x)=(38,2,2).""" + leaves = 28 * q + r + nodes = 9 * q + dispatch = q + r + x + return leaves + nodes + x + dispatch + + +def enumerate_distinct6_R_spectrum(): + """Exhaust all distinct nonzero 6-slot sets; return covering R spectrum.""" + histogram = Counter() + covering = 0 + witnesses = {} + for nonzero in combinations(range(1, 32), 6): + slots = (0,) + nonzero + total = min_even_subset_R(slots) + if total is None: + continue + covering += 1 + histogram[total] += 1 + witnesses.setdefault(total, slots) + attainable = sorted(histogram) + return { + "covering_sets": covering, + "attainable_R": attainable, + "histogram": {str(r): histogram[r] for r in attainable}, + "first_witnesses": {str(r): list(witnesses[r]) for r in attainable}, + "min_R": attainable[0] if attainable else None, + } + + +def repeat_layer_basis_census(): + """Valid Q=7 walks on the standard basis with exactly one repeated vertex. + + Any covering walk whose distinct nonzero slots form a spanning 5-set is + GL(5)-equivalent to a walk on {0,1,2,4,8,16} with the same multiplicity + pattern; even-subset total R is GL-invariant. Dependent 5-sets cannot + span F2^5, so their even-subset image misses masks. + """ + labels = (1, 2, 4, 8, 16) + hist = Counter() + covering = 0 + best = None + witness = None + + # Extra visit to 0 (second 0 in slots[1..5]); each basis vector once. + for j in range(1, 6): + rest = [i for i in range(1, 7) if i != j] + for perm in permutations(labels): + slots = [0] * 7 + slots[j] = 0 + for pos, val in zip(rest, perm): + slots[pos] = val + slots_t = tuple(slots) + if not valid_walk_slots(slots_t): + continue + total = min_even_subset_R(slots_t) + if total is None: + continue + covering += 1 + hist[total] += 1 + if best is None or total < best: + best = total + witness = slots_t + + # One basis vector doubled; others once; 0 only at the start. + for dbl_idx in range(5): + others = [labels[i] for i in range(5) if i != dbl_idx] + for p1, p2 in combinations(range(1, 7), 2): + rest_pos = [i for i in range(1, 7) if i not in (p1, p2)] + for perm in permutations(others): + slots = [0] * 7 + slots[p1] = slots[p2] = labels[dbl_idx] + for pos, val in zip(rest_pos, perm): + slots[pos] = val + slots_t = tuple(slots) + if not valid_walk_slots(slots_t): + continue + total = min_even_subset_R(slots_t) + if total is None: + continue + covering += 1 + hist[total] += 1 + if best is None or total < best: + best = total + witness = slots_t + + attainable = sorted(hist) + return { + "kind": "one_repeat_on_standard_basis", + "covering_walks": covering, + "attainable_R": attainable, + "histogram": {str(r): hist[r] for r in attainable}, + "min_R": best, + "first_witness": list(witness) if witness is not None else None, + "argument": ( + "GL(5) reduces every spanning 5-set one-repeat covering walk to this " + "basis census; R totals are invariant. Only R=96 occurs." + ), + } + + +def span_obstruction_samples(): + """Dependent nonzero sets cannot cover: even-subset image stays in a proper subspace.""" + samples = [] + # Rank-4 (omit one basis vector) and a rank-3 dependent 5-set. + for labels, note in ( + ((1, 2, 4, 8), "rank4_omit_16"), + ((1, 2, 3, 4, 5), "rank3_dependent_five"), + ((1, 2, 4, 8, 3), "rank4_five_with_sum"), + ): + best_image = 0 + alphabet = (0,) + tuple(labels) + for multi in itertools.combinations_with_replacement(alphabet, 6): + image = even_subset_image((0,) + multi) + best_image = max(best_image, len(image)) + samples.append( + { + "labels": list(labels), + "rank": rank_f2(labels), + "best_even_subset_image_size": best_image, + "covers_all_31": best_image >= 32, + "note": note, + } + ) + return samples + + +# Credited path-lowered champion from the 789q / #2643 lineage. +CHAMPION_7 = (0, 1, 2, 6, 12, 24, 16, 0) diff --git a/research/seven-query-r-floor/test_package.py b/research/seven-query-r-floor/test_package.py new file mode 100644 index 0000000000..7a434049c8 --- /dev/null +++ b/research/seven-query-r-floor/test_package.py @@ -0,0 +1,100 @@ +#!/usr/bin/env python3 +"""Package fault controls for the seven-query R 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-r-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_R_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_R_FLOOR" in proc.stdout, proc.stdout) + + # 3) Certificate 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) + 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_R_among_X_eq_6"] = 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_R_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") + 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_R_FLOOR_PACKAGE_TESTS groups=6") + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/research/seven-query-r-floor/verify.py b/research/seven-query-r-floor/verify.py new file mode 100644 index 0000000000..a49ae45451 --- /dev/null +++ b/research/seven-query-r-floor/verify.py @@ -0,0 +1,233 @@ +#!/usr/bin/env python3 +"""Exact seven-query even-subset R floor among X=6; read-only default. + +Prepared by Wentao Li with substantial AI assistance. 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, + check_identity, + enumerate_distinct6_R_spectrum, + invoice, + min_even_subset_R, + path_X, + path_word, + repeat_layer_basis_census, + span_obstruction_samples, + tariff_qrx, + valid_walk_slots, +) + +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(): + # Layer A: distinct 6-nonzero slot sets (Hamiltonian connector walks). + distinct = enumerate_distinct6_R_spectrum() + need(distinct["min_R"] == 82, "unexpected distinct-6 min R") + need(distinct["attainable_R"] == [82, 88], f"unexpected spectrum {distinct['attainable_R']}") + need( + distinct["histogram"] == {"82": 97216, "88": 486080}, + f"unexpected histogram {distinct['histogram']}", + ) + need(distinct["covering_sets"] == 583296, "unexpected covering count") + + # Layer B: one-repeat walks on a spanning 5-set (GL-reduced to the basis). + repeats = repeat_layer_basis_census() + need(repeats["min_R"] == 96, "unexpected one-repeat min R") + need(repeats["attainable_R"] == [96], f"unexpected repeat spectrum {repeats['attainable_R']}") + need(repeats["covering_walks"] == 1680, f"unexpected repeat covering {repeats['covering_walks']}") + need(valid_walk_slots(tuple(repeats["first_witness"])), "repeat witness not a valid walk") + + # Layer C: fewer than five independent nonzero labels cannot span F2^5. + samples = span_obstruction_samples() + for row in samples: + need(row["rank"] < 5, f"sample {row['note']} should be dependent") + need(not row["covers_all_31"], f"sample {row['note']} should not cover") + need(row["best_even_subset_image_size"] <= 16, f"sample {row['note']} image too large") + + # Classification: every covering Q=7 even-subset slot list has either + # six distinct nonzero labels (R in {82,88}) or a one-repeat spanning + # five-set (R=96). Hence global min R is 82. + min_R = 82 + need(min(distinct["min_R"], repeats["min_R"]) == min_R, "global min R") + + # Sharpness at X=6: credited champion attains R=82 with path-local X=6. + # Combined with the #2643 restored XOR floor X>=6 at Q=7 (cited; not reopened), + # every restored seven-query word with X=6 has R>=82, and 82 is attained. + closed = CHAMPION_7 + need(path_X(closed) == 6, "champion path_X") + slots = tuple(closed[:-1]) + need(valid_walk_slots(slots), "champion slots") + need(min_even_subset_R(slots) == 82, "champion R") + word = path_word(closed) + counts = check_identity(word) + need(dict(counts) == {"Q": 7, "R": 82, "X": 6}, f"champion counts {counts}") + bill = invoice(word) + need(bill["tariff"] == 442, f"champion tariff {bill}") + need(tariff_qrx(7, 82, 6) == 442, "tariff arithmetic") + need(tariff_qrx(7, 78, 6) == 434, "undercut threshold arithmetic") + need(434 < 436 < 442, "R<=78 would undercut 436; R=82 cannot") + + return { + "schema_version": 1, + "status": "PASS_SEVEN_QUERY_R_FLOOR", + "scope": ( + "Five-source common-B mutable-source Q/R/X alphabet (PR1898). " + "Even-subset readout on connector states of restored straight-line " + "words with exactly seven queries. Exact minimum R among words with X=6." + ), + "claim": { + "Q": 7, + "min_R_among_X_eq_6": 82, + "min_R_even_subset_all_walks": 82, + "sharp": True, + "answers_7qxor_oq1": ( + "Minimum even-subset R among restored seven-query words with X=6 " + "is exactly 82; R<=78 is impossible in this readout class, so the " + "abstract tariff cannot undercut 436 via lower R at X=6." + ), + "no_new_kappa": True, + }, + "classification": { + "distinct_six_nonzero": distinct, + "one_repeat_spanning_five": repeats, + "span_obstruction_samples": samples, + "argument": ( + "A covering even-subset slot list of length 7 must span F2^5, so it " + "uses at least five linearly independent nonzero labels. With six " + "intermediate slots after the leading 0, the covering cases are: " + "(i) six distinct nonzero labels (Hamilton walks; R in {82,88}); " + "(ii) five spanning nonzero labels with exactly one repeated vertex " + "(R=96 on the GL(5) basis census). Fewer independent labels cannot " + "cover. Therefore min R = 82." + ), + }, + "xor_floor_citation": { + "object": "research/seven-query-xor-floor (CrocSwap #2643)", + "statement": "Every restored seven-query word needs X>=6; sharp via the same champion.", + "use_here": "Together with min even-subset R=82, every X=6 word has R>=82.", + "not_reopened": True, + }, + "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 / " + "seven-query-xor-floor lineage; PR1898 alphabet." + ), + }, + "tariff": { + "complete_prices": {"b": 38, "a": 2, "x": 2}, + "six_query_endpoint": 436, + "beat_436_at_Q7_X6_requires_R_le": 78, + "min_tariff_at_Q7_X6": 442, + "undercuts_436": False, + }, + "new_kappa": False, + } + + +def compare_cert(fresh, committed): + need(committed.get("status") == "PASS_SEVEN_QUERY_R_FLOOR", "bad certificate status") + need(fresh["claim"] == committed["claim"], "claim drift") + need( + fresh["classification"]["distinct_six_nonzero"]["histogram"] + == committed["classification"]["distinct_six_nonzero"]["histogram"], + "distinct histogram drift", + ) + need( + fresh["classification"]["one_repeat_spanning_five"]["histogram"] + == committed["classification"]["one_repeat_spanning_five"]["histogram"], + "repeat histogram drift", + ) + need( + fresh["attaining_witness"]["R"] == committed["attaining_witness"]["R"], + "witness R drift", + ) + need( + fresh["attaining_witness"]["tariff_at_38_2_2"] + == committed["attaining_witness"]["tariff_at_38_2_2"], + "witness tariff drift", + ) + need(fresh["tariff"] == committed["tariff"], "tariff block 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_R_FLOOR " + "Q=7 min_R_among_X=6 is 82 sharp " + "repeat_layer_R=96 " + "answers_7qxor_oq1 " + "tariff_floor=442 " + "no_new_kappa" + ) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main())