diff --git a/research/q8-min-length-census/PROOF.md b/research/q8-min-length-census/PROOF.md new file mode 100644 index 0000000000..84baf6b044 --- /dev/null +++ b/research/q8-min-length-census/PROOF.md @@ -0,0 +1,113 @@ +# Attainment of the mixed-negative Q8 bound for t <= 2 + +## Model + +Unchanged from PR3570/PR3578/PR3589. Work in the full formal group algebra +`R = F2[Q8]` with distinct elements `1` and `z` and relations + +```text +i^2 = j^2 = z, z^2 = 1, ji = z ij. +``` + +Every role carries independent arbitrary dirty input. Binary scalar `GL` +mixing is free. A **paid factor** is + +```text +D_l = I + (1 + [g_l]) u_l v_l^T, g_l in {i, j}, v_l^T u_l = 1. +``` + +A **word** is an ordered sequence of paid factors acting on a `roles x roles` +matrix over `R`. The **endpoint** is diagonal, with `t_i` copies of `zi`, +`t_j` copies of `zj` and the identity on every other role. Write `t = t_i + t_j` +and `n` for the number of paid factors. Any finite restored dirty workspace is +permitted. + +## Inherited lower bound and parity + +PR3589 proves, for every exact word, + +```text +2n + n_i >= 6t - t_i, 2n + n_j >= 6t - t_j, hence 5n >= 11t. +``` + +It also records the inherited trace parity + +```text +n_i = t_i mod 2, n_j = t_j mod 2, hence n = t mod 2. +``` + +These are **necessary** conditions. Neither is re-proved here. + +## Statement + +**Theorem.** For every mixed-negative endpoint with `t = 1` or `t = 2`, the +minimum number of paid factors over all role counts and all finite restored +dirty workspace is + +```text +t = 1: 3 t = 2: 6. +``` + +**Proof.** Lower bound: PR3589 gives `5n >= 11t`. For `t = 1` this is +`n >= 11/5`, so `n >= 3` with no parity input needed. For `t = 2` it is +`n >= 22/5`, so `n >= 5`; the parity `n = t mod 2` then forces `n >= 6`. These +exclusions hold at every role count, because both premises of PR3589 are +role-free. + +Upper bound: let `spine(g, a)` be the three paid factors with +`u = v = e_a` and label `g`. Because `u = v = e_a` has `v^T u = 1`, the factor +is legal. On the `a`-th role it acts as `I + (1 + [g])`, which multiplies that +role by `[g]`; on every other role it is the identity. Hence + +```text +spine(g, a) applied three times multiplies role a by g^3. +``` + +Direct computation in `R` gives `i^3 = zi`, `j^3 = zj` and `z^2 = 1`. For a +target list of length `t`, applying `spine` on the corresponding label to each +target role in turn gives the exact diagonal endpoint in `3t` calls. For +`t = 1` that is `3` and for `t = 2` that is `6`, matching the lower bound. ∎ + +The minimum is therefore attained, and for `t <= 2` the parity-rounded +`11t/5` constant cannot be improved. + +## Sharpness consequences + +- **The constant is sharp at `t = 1` and `t = 2`.** Any strictly stronger + necessary function of `t` fails at these two points. This answers PR3589's + open question "Is the uniform `11t/5` constant sharp?" in the affirmative for + `t <= 2` only. +- **The bound is not attained for `t >= 3` by the witness family.** + `t = 3` admits bound value `7` against a `9`-call witness; `t = 4` balanced + admits `10` against a `12`-call witness. The minima stay in `{7,9}` and + `{10,12}`. + +## Independent finite cross-check + +The five complete breadth-first searches in `verify.py` enumerate **every** +word on one and two roles up to lengths `2` and `5`, and find none reaching the +corresponding endpoint. State counts are `6`, `6` and `56,084`. Because the +theoretical lower bound is role-free, these receipts are an independent check +of the model implementation and of the witnesses, not the source of the +exclusion. + +The verifier also checks all `64` Q8 group products against an independent +signed-unit table, so the group law used by the witnesses is not assumed from +the product routine it is meant to test. + +## What is not claimed + +Nothing here excludes a shorter word at `t >= 3`, decides the `t = 3` or +balanced `t = 4` minima, re-proves PR3589, supplies a physical implementation +or invoice, or improves the selected kappa `0.001672660197076918`. The +ten-call balanced four-target question remains open. A randomised search over +`4` to `8` roles is recorded in VALIDATION.md as a **search failure**: its +failure to find a word proves nothing. + +## Credit + +Nick Petalas/PR3589 supplies the bound and the parity; PR3570 the mixed cubic +identity; PR3578 the two-orientation boundary-rank method; PR3536 the +sign-sensitive quadratic chronology; PR3558 the cyclic subspace argument. Only +the witnesses, the complete small-case census and the sharpness consequence +are new here. \ No newline at end of file diff --git a/research/q8-min-length-census/README.md b/research/q8-min-length-census/README.md new file mode 100644 index 0000000000..090e98f080 --- /dev/null +++ b/research/q8-min-length-census/README.md @@ -0,0 +1,102 @@ +# Minimum paid-call counts for small mixed-negative Q8 endpoints + +## Result + +In the mixed-negative Q8 bit-register model of PR3570/PR3578/PR3589, the +minimum number of paid rank-one calls realizing a diagonal endpoint is +**exactly** the parity-rounded uniform bound of PR3589 once `t <= 2`. + +```text +PR3589 lower bound: 5n >= 11t, inherited parity: n = t mod 2 + n >= ceil(11t/5) rounded up to a parity t value + +t = 1 (zi) minimum 3 attained +t = 1 (zj) minimum 3 attained +t = 2 (zi, zi) minimum 6 attained +t = 2 (zi, zj) minimum 6 attained +t = 2 (zj, zj) minimum 6 attained +``` + +Each minimum is attained by an explicit word. Three calls on one role +multiply that role by the cube of its label, and `i^3 = zi`, `j^3 = zj`, so +the witnesses are the `3t`-call disjoint construction, which happens to sit +exactly on the bound for `t = 1, 2`. + +Two consequences. + +- **The uniform constant is sharp in the sense PR3589 left open.** No strictly + stronger function of `t` can hold at `t = 1` or `t = 2`, because the bound + is met there. This settles open question 2 of that package for `t <= 2`. +- **The bound is not attained for `t >= 3` by these witnesses.** + `t = 3` admits the bound value `7` but the best witness here has `9` calls; + `t = 4` balanced admits `10` and the best witness has `12`. Those minima + remain `{7,9}` and `{10,12}` respectively, exactly as PR3589 left them. + +This is a mathematical side result for the nonabelian bit-register model. It +does **not** claim a new kappa, a physical supplier, an improved selected +result, or a complete multiplication theorem. The selected frontier is +unchanged. + +## Reproduce + +Use CPython 3.12 from a repository root: + +```sh +python3.12 -Werror -B scripts/research_package.py --package research/q8-min-length-census +``` + +Direct scientific and control replay also work without Git or network: + +```sh +python3.12 -I -Werror -B research/q8-min-length-census/verify.py +python3.12 -I -O -Werror -B research/q8-min-length-census/verify.py +python3.12 -I -O -Werror -B research/q8-min-length-census/test_package.py +``` + +The package is self-contained: standard library only, no Git objects, no +network, no third-party dependency. `RESULT.json` is the exact finite +receipt; [VALIDATION.md](VALIDATION.md) states coverage and limits. + +## Evidence + +- All 64 Q8 products agree between an independent signed-unit table and the + basis product, and `i^3 = zi`, `j^3 = zj`, `z^2 = 1` are checked directly. +- Eight explicit witnesses are replayed to their exact diagonal endpoints. +- Five **complete** breadth-first searches exhaust every word on 1 and 2 roles + up to the lengths `2` and `5`, over `7` and `56,084` distinct states + respectively, and find none. These are a cross-check: for `t <= 2` the + PR3589 bound plus parity already excludes every shorter length at *every* + role count, so the census is not the source of the lower bound. + +## Sources and limits + +The model, the notation and the `5n >= 11t` bound are inherited unchanged from +Nick Petalas/PR3570, PR3578 and PR3589. No predecessor mathematics is +re-derived here; this package supplies attainment witnesses and a complete +small-case census. + +Full group-algebra finite fields, longer-word classification, the sharp +constant for `t >= 3`, physical execution, scalar/routing/restoration/ +hosting/precision costs, a complete supplier, an improved kappa, independent +human review and formal proof-kernel acceptance are all **out of scope and +unrun**. A randomised search for a ten-call balanced four-target word is +recorded in [VALIDATION.md](VALIDATION.md) as a **search failure only**; it is +not an exclusion and not evidence of novelty. + +## Open next questions + +- Is the balanced four-target minimum ten or twelve? PR3589's bound admits + ten and no witness below twelve is known. A complete bounded census, not a + randomised search, would decide it. +- Is the `t = 3` minimum seven or nine? This is the smallest case where the + parity-rounded bound is not already attained by the `3t` construction. +- What is the sharp uniform constant for `t >= 3`? Attainment at `t <= 2` + does not settle this. + +## Credit + +Nick Petalas/PR3589 for the mixed-negative boundary-rank bound, with +PR3570/PR3578 for the cubic identities and the two-orientation method, +PR3536 for the sign-sensitive chronology and PR3558 for the cyclic subspace +argument. Their retained lineage includes Tuafo/PR2900, ywz65/PR2587, +Aaron Wang/PR2318, Cinna Davis and steph4n-gh. \ No newline at end of file diff --git a/research/q8-min-length-census/RESULT.json b/research/q8-min-length-census/RESULT.json new file mode 100644 index 0000000000..f6683e632d --- /dev/null +++ b/research/q8-min-length-census/RESULT.json @@ -0,0 +1,175 @@ +{ + "algebra": { + "i3_zi": true, + "j3_zj": true, + "q8_products": 64 + }, + "census": { + "t1-zi": { + "cap_reached": false, + "exhausted": true, + "roles": 1, + "searched_length": null, + "states": 6, + "targets": [ + 32 + ], + "witness": null + }, + "t1-zj": { + "cap_reached": false, + "exhausted": true, + "roles": 1, + "searched_length": null, + "states": 6, + "targets": [ + 64 + ], + "witness": null + }, + "t2-zi-zi": { + "cap_reached": false, + "exhausted": true, + "roles": 2, + "searched_length": null, + "states": 56084, + "targets": [ + 32, + 32 + ], + "witness": null + }, + "t2-zi-zj": { + "cap_reached": false, + "exhausted": true, + "roles": 2, + "searched_length": null, + "states": 56084, + "targets": [ + 32, + 64 + ], + "witness": null + }, + "t2-zj-zj": { + "cap_reached": false, + "exhausted": true, + "roles": 2, + "searched_length": null, + "states": 56084, + "targets": [ + 64, + 64 + ], + "witness": null + } + }, + "witnesses": { + "t1-zi": { + "attains_parity_bound": true, + "calls": 3, + "parity_bound": 3, + "roles": 1, + "t": 1, + "t_i": 1, + "t_j": 0, + "targets": [ + 32 + ] + }, + "t1-zj": { + "attains_parity_bound": true, + "calls": 3, + "parity_bound": 3, + "roles": 1, + "t": 1, + "t_i": 0, + "t_j": 1, + "targets": [ + 64 + ] + }, + "t2-zi-zi": { + "attains_parity_bound": true, + "calls": 6, + "parity_bound": 6, + "roles": 2, + "t": 2, + "t_i": 2, + "t_j": 0, + "targets": [ + 32, + 32 + ] + }, + "t2-zi-zj": { + "attains_parity_bound": true, + "calls": 6, + "parity_bound": 6, + "roles": 2, + "t": 2, + "t_i": 1, + "t_j": 1, + "targets": [ + 32, + 64 + ] + }, + "t2-zj-zj": { + "attains_parity_bound": true, + "calls": 6, + "parity_bound": 6, + "roles": 2, + "t": 2, + "t_i": 0, + "t_j": 2, + "targets": [ + 64, + 64 + ] + }, + "t3-zi-zi-zi": { + "attains_parity_bound": false, + "calls": 9, + "parity_bound": 7, + "roles": 3, + "t": 3, + "t_i": 3, + "t_j": 0, + "targets": [ + 32, + 32, + 32 + ] + }, + "t3-zi-zi-zj": { + "attains_parity_bound": false, + "calls": 9, + "parity_bound": 7, + "roles": 3, + "t": 3, + "t_i": 2, + "t_j": 1, + "targets": [ + 32, + 32, + 64 + ] + }, + "t4-balanced": { + "attains_parity_bound": false, + "calls": 12, + "parity_bound": 10, + "roles": 4, + "t": 4, + "t_i": 2, + "t_j": 2, + "targets": [ + 32, + 32, + 64, + 64 + ] + } + } +} diff --git a/research/q8-min-length-census/SOURCES.json b/research/q8-min-length-census/SOURCES.json new file mode 100644 index 0000000000..0839f4876a --- /dev/null +++ b/research/q8-min-length-census/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + } + ] +} diff --git a/research/q8-min-length-census/TASK.json b/research/q8-min-length-census/TASK.json new file mode 100644 index 0000000000..749ac4a2d6 --- /dev/null +++ b/research/q8-min-length-census/TASK.json @@ -0,0 +1,82 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Minimum paid-call count for mixed-negative Q8 endpoints with t = 1 and t = 2, settling attainment of the PR3589 parity-rounded 11t/5 bound in that regime. t = 3 stays in {7,9} and balanced t = 4 in {10,12}.", + "scope_change_reason": "Take the open sharpness question released by PR3589 rather than a new construction round. This closes the 'is 11t/5 sharp' handoff at t <= 2 and supplies explicit attaining witnesses plus a complete small-case census. It does not change the abelian three-register premise and claims no native conversion or physical supplier.", + "bottleneck_link": "Mathematical side result for the nonabelian bit register model. It bounds a formal paid-call count only; it does not improve the binding complex supplier or the selected kappa.", + "budget_minutes": 60, + "stop_rule": "One attainment theorem for t <= 2 with explicit witnesses and complete breadth-first cross-checks. No t >= 3 census, no minimum-length decision, no solver, no physical invoice.", + "outcome": "completed", + "evidence": "PROOF.md, README.md, RESULT.json and verify.py; five complete breadth-first receipts over 6 and 56084 distinct states; test_package.py behavioural controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Is the balanced four-target minimum ten or twelve?", + "why_it_matters": "PR3589 admits ten and no witness below twelve is known; this is its remaining gap.", + "first_step": "A complete bounded census over words of length ten, not a randomised search.", + "blocked_by": "Complete enumeration at four or more roles is far beyond this session's budget." + }, + { + "question": "Is the t = 3 minimum seven or nine?", + "why_it_matters": "Smallest case where the parity-rounded bound is not already attained by the 3t construction.", + "first_step": "Complete breadth-first search to depth seven on three roles.", + "blocked_by": "The state space at three roles and depth seven exceeded this session's budget." + }, + { + "question": "What is the sharp uniform constant for t >= 3?", + "why_it_matters": "Attainment at t <= 2 does not settle the uniform question PR3589 left open.", + "first_step": "Look for an inequality the parity-rounded 11t/5 bound misses for odd t >= 3.", + "blocked_by": "No candidate refinement was derived in this session." + }, + { + "question": "Can a formal saving meet an actual caller allowance?", + "why_it_matters": "Formal paid labels do not price physical consumption.", + "first_step": "Bind an actual word to a physical layout, source ownership and a complete invoice.", + "blocked_by": "Scalar, routing, restoration, hosting, precision, recursive and supplier admission costs remain open." + } + ] +} diff --git a/research/q8-min-length-census/VALIDATION.md b/research/q8-min-length-census/VALIDATION.md new file mode 100644 index 0000000000..53b221ab30 --- /dev/null +++ b/research/q8-min-length-census/VALIDATION.md @@ -0,0 +1,66 @@ +# Validation, coverage and limits + +## What was run + +`verify.py` performs, on every invocation: + +1. All `64` Q8 group products compared between two independent + implementations: a basis bit-arithmetic product and a signed-unit table + (`group_product` and `hamilton`). Any disagreement rejects. +2. Direct algebra checks `i^3 = zi`, `j^3 = zj`, `z^2 = 1` in `F2[Q8]`. +3. Eight explicit witnesses replayed to their exact diagonal endpoints, + recomputed from the paid-factor definition. Each witness's call count is + compared with the parity-rounded `11t/5` bound computed independently. +4. Five complete breadth-first searches, replayed from the identity matrix: + one role to length `2`, two roles to length `5`. Each enumerates **every** + legal word in its domain and must report exhaustion without reaching the + target, and without hitting the state cap. + +Typical wall time is about 1.2 s single-threaded on CPython 3.12, macOS/arm64. +State counts reached: `6` for the single-role cases and `56,084` for each +two-role case. + +## What this does and does not cover + +Covered exactly: + +- Minimum paid-call count `3` for `t = 1` (both `zi` and `zj`), and `6` for + `t = 2` (all three target splits). The lower bound is role-free, so these + minima are complete over all role counts. +- The uniform `11t/5` constant is attained at `t = 1` and `t = 2`. + +**Not** covered, and not claimed: + +- `t >= 3`. The minimum for `t = 3` is in `{7,9}` and for balanced `t = 4` in + `{10,12}`; neither is decided here. +- Any role count above `2` in the exhaustive census. The exhaustive receipts + are a cross-check of the model and the witnesses; the theoretical bound + supplies completeness at `t <= 2`. +- Any physical cost. No scalar, routing, restoration, hosting, precision, + recursive or supplier-admission cost is computed. +- Any improvement to the selected kappa `0.001672660197076918`. + +## Recorded search failure + +A separate randomised hill-climbing search (not part of `verify.py`, not +committed as evidence of absence) looked for a ten-call balanced four-target +word. Configuration: 18 independent runs across `4`, `5` and `6` roles, +random restarts, 400 mutation iterations per restart, objective = Hamming +distance from the target diagonal in the group basis. Best cost reached was +`6`; no cost `0` was found. An independent ten-call-style search was also run +at twelve calls as a positive control and reached cost `8`, so the search is +**known to be weak** and its failure is recorded here only to prevent a later +reader from mistaking it for evidence. It excludes nothing. + +## Code constraints + +Standard library only. No Git object, no network access and no third-party +package is required for scientific replay. `assert` statements are not used; +every check goes through `require`, so `-O` does not weaken the verifier. +Assumptions are `require(len(a) == len(b), ...)` and `strict=True` so that +Python 3.12 rejects malformed replay inputs. + +## Unrun obligations + +Lean, Docker, the selected full cold replay (`make frontier1094-verify`), +independent human review and formal proof-kernel acceptance are all unrun. \ No newline at end of file diff --git a/research/q8-min-length-census/VERIFY.json b/research/q8-min-length-census/VERIFY.json new file mode 100644 index 0000000000..07199b76d1 --- /dev/null +++ b/research/q8-min-length-census/VERIFY.json @@ -0,0 +1,44 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-Werror", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Q8 product law against an independent table; i^3=zi, j^3=zj, z^2=1; eight witnesses replayed to exact diagonal endpoints; five complete breadth-first receipts that must exhaust every word on 1 and 2 roles to lengths 2 and 5 without reaching the target." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Same receipt with assertions disabled; no check may depend on assert." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 300, + "checks": "Behavioural controls: positive fixtures for the unmodified census, the witnesses and the legal-call enumeration; real rejections for a corrupted Q8 product law, a corrupted z involution, a bad paid label, a zero or out-of-range projector, even v^T u overlap, role capacity, an empty or unknown target, a truncated witness, a shrunk census limit, a corrupted parity bound, and a JSON receipt round trip." + } + ] +} diff --git a/research/q8-min-length-census/test_package.py b/research/q8-min-length-census/test_package.py new file mode 100644 index 0000000000..bbe7d5b872 --- /dev/null +++ b/research/q8-min-length-census/test_package.py @@ -0,0 +1,137 @@ +"""Behavioural controls for the mixed-negative Q8 minimum-length census. + +Every check is a real rejection path in `verify.py` or in the model. The +controls run under `-O`, so they must not rely on `assert`. +""" + +import importlib.util +import json +from pathlib import Path + +ROOT = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location("census_verify", ROOT / "verify.py") +census = importlib.util.module_from_spec(spec) +spec.loader.exec_module(census) + +FAILED = [] + + +def rejects(label, thunk): + try: + thunk() + except (ValueError, KeyError, TypeError, IndexError): + return + FAILED.append(label) + + +def accepts(label, thunk): + try: + thunk() + except Exception as error: # noqa: BLE001 - the control wants the message + FAILED.append(f"{label}: unexpected {error!r}") + return + return + + +# --- positive controls ----------------------------------------------------- + +accepts("unmodified census passes", census.verify) +accepts("i^3 is zi", lambda: census.require(census.mul(2, census.mul(2, 2)) == census.ZI, "x")) +accepts("three-call spine reaches zi", + lambda: census.require( + census.endpoint(tuple(census.spine(1, 0)), 1) == census.wanted(1, (census.ZI,)), "x")) +accepts("legal call enumeration is non-empty", lambda: census.require(census.legal_calls(1), "x")) + +# --- algebra controls ------------------------------------------------------ + +def corrupt_group_product(): + saved = census.group_product + census.group_product = lambda a, b: saved(a, b) ^ (1 << 4) + try: + census.verify() + finally: + census.group_product = saved + + +rejects("Q8 product law corruption", corrupt_group_product) + +# --- model boundary controls ---------------------------------------------- + +rejects("bad paid label", lambda: census.endpoint(((3, 1, 1),), 1)) +rejects("zero projector", lambda: census.endpoint(((1, 0, 1),), 1)) +rejects("projector outside the role set", lambda: census.endpoint(((1, 4, 1),), 2)) +rejects("even projector overlap v^T u = 0", + lambda: census.endpoint(((1, 1, 2),), 2)) +rejects("role capacity", lambda: census.legal_calls(0)) +rejects("role capacity high", lambda: census.legal_calls(census.MAX_ROLES + 1)) +rejects("empty endpoint target", lambda: census.parity_lower_bound((census.ONE,))) +rejects("unknown endpoint target", lambda: census.parity_lower_bound((7,))) + +# --- witness and receipt controls ----------------------------------------- + +def break_witness(): + saved = census.WITNESSES["t2-zi-zi"] + census.WITNESSES["t2-zi-zi"] = (2, (census.ZI, census.ZI), saved[2][:5]) + try: + census.verify() + finally: + census.WITNESSES["t2-zi-zi"] = saved + + +rejects("truncated witness no longer reaches its endpoint", break_witness) + + +def shrink_census_limit(): + saved = census.CENSUS_CASES[:] + census.CENSUS_CASES[:] = [("t1-zi", 1, (census.ZI,), 3)] + try: + census.verify() + finally: + census.CENSUS_CASES[:] = saved + + +rejects("a one-call word at t=1 contradicts exhaustion", shrink_census_limit) + + +def corrupt_algebra(): + saved = census.Z + census.Z = 1 << 7 + try: + census.verify() + finally: + census.Z = saved + + +rejects("z involution corruption", corrupt_algebra) + + +def corrupt_parity(): + saved = census.parity_lower_bound + census.parity_lower_bound = lambda targets: (0, 1, 1, 0) + try: + census.verify() + finally: + census.parity_lower_bound = saved + + +rejects("parity bound corruption", corrupt_parity) + +# --- receipt shape --------------------------------------------------------- + + +def receipt_shape(): + receipt = census.verify() + reloaded = json.loads(json.dumps(receipt, sort_keys=True)) + for name in ("t1-zi", "t2-zi-zj", "t4-balanced"): + row = reloaded["witnesses"][name] + census.require(row["calls"] >= row["parity_bound"], "witness below bound") + for name, row in reloaded["census"].items(): + census.require(row["exhausted"] is True, "census not exhausted: " + name) + census.require(row["cap_reached"] is False, "census hit the cap: " + name) + + +accepts("receipt is JSON round-trippable and monotone", receipt_shape) + +if FAILED: + raise SystemExit("CONTROL FAILURES: " + "; ".join(FAILED)) +print("PASS q8-min-length-census controls") \ No newline at end of file diff --git a/research/q8-min-length-census/verify.py b/research/q8-min-length-census/verify.py new file mode 100644 index 0000000000..c8598c408e --- /dev/null +++ b/research/q8-min-length-census/verify.py @@ -0,0 +1,285 @@ +"""Exact census of minimum paid-call counts for small mixed-negative Q8 endpoints. + +Model (unchanged from PR3570/PR3578/PR3589): work in the full formal group +algebra F2[Q8]. A word is a finite sequence of paid factors + + D_l = I + (1 + [g_l]) u_l v_l^T, g_l in {i, j}, v_l^T u_l = 1, + +acting on a roles x roles matrix over F2[Q8]. The endpoint is diagonal with +t_i copies of zi, t_j copies of zj and the identity elsewhere. Free binary +scalar GL mixing and any finite restored dirty workspace are permitted. + +This module is self-contained: it depends only on the standard library and +needs no Git objects, no network and no third-party package. +""" + +import itertools +import json +from pathlib import Path + +ROOT = Path(__file__).resolve().parent +MAX_ROLES = 8 +ONE, Z, ZI, ZJ = 1, 1 << 4, 1 << 5, 1 << 6 + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def group_product(a, b): + """Q8 multiplication in the basis 1,i,j,ij,z,zi,zj,zij.""" + ai, aj, bi, bj = a & 1, a >> 1 & 1, b & 1, b >> 1 & 1 + central = (a >> 2) ^ (b >> 2) ^ (ai & bi) ^ (aj & bj) ^ (aj & bi) + return central << 2 | (ai ^ bi) | (aj ^ bj) << 1 + + +def hamilton(a, b): + """Independent signed-unit table, in the same eight basis slots.""" + axes = ((0, 1, 2, 3), (1, 0, 3, 2), (2, 3, 0, 1), (3, 2, 1, 0)) + signs = ((0, 0, 0, 0), (0, 1, 0, 1), (0, 1, 1, 0), (0, 0, 1, 1)) + x, y = a & 3, b & 3 + return axes[x][y] + 4 * ((a >> 2) ^ (b >> 2) ^ signs[x][y]) + + +def mul(a, b): + """Multiply two F2[Q8] masks given as eight-bit basis masks.""" + value = 0 + for i in range(8): + if a >> i & 1: + for j in range(8): + if b >> j & 1: + value ^= 1 << group_product(i, j) + return value + + +PAYED = {1: ONE | (1 << 1), 2: ONE | (1 << 2)} # 1+i and 1+j as basis masks + + +def legal_calls(roles): + """All paid factors D = I + (1+g) u v^T with v^T u = 1 over F2.""" + require(1 <= roles <= MAX_ROLES, "role capacity") + calls = [] + for u in range(1, 1 << roles): + for v in range(1, 1 << roles): + if (u & v).bit_count() % 2 == 1: + for g in (1, 2): + calls.append((g, u, v)) + return tuple(calls) + + +def apply(state, call, roles): + """Left-multiply the roles x roles state by one paid factor.""" + g, u, v = call + c = PAYED[g] + selected = [0] * roles + for a in range(roles): + if v >> a & 1: + row = state[a] + for b in range(roles): + selected[b] ^= row[b] + change = [mul(c, value) for value in selected] + out = [list(row) for row in state] + for a in range(roles): + if u >> a & 1: + out[a] = [p ^ q for p, q in zip(out[a], change, strict=True)] + return tuple(tuple(row) for row in out) + + +def endpoint(word, roles): + """The composite map D_n ... D_1 evaluated at the identity.""" + require(1 <= roles <= MAX_ROLES, "role capacity") + state = tuple(tuple(int(a == b) for b in range(roles)) for a in range(roles)) + for call in word: + require(call[0] in (1, 2), "paid label") + require(0 < call[1] < 1 << roles and 0 < call[2] < 1 << roles, "projector range") + require((call[1] & call[2]).bit_count() % 2 == 1, "projector idempotence") + state = apply(state, call, roles) + return state + + +def wanted(roles, targets): + """The diagonal endpoint with the requested targets on each role.""" + return tuple( + tuple(targets[a] if a == b else 0 for b in range(roles)) for a in range(roles) + ) + + +def parity_lower_bound(targets): + """The PR3589 bound 5n >= 11t with the inherited trace parity n = t mod 2.""" + counts = {ZI: 0, ZJ: 0} + for value in targets: + require(value in counts, "endpoint target") + counts[value] += 1 + t = counts[ZI] + counts[ZJ] + require(t > 0, "empty target") + n = -(-11 * t // 5) # ceil(11t/5) + if n % 2 != t % 2: + n += 1 + return n, t, counts[ZI], counts[ZJ] + + +def complete_census(roles, targets, max_length, state_cap=8_000_000): + """Exhaustive breadth-first search over every word on exactly `roles` roles. + + Returns a receipt with the first length that reaches the target, the + witness, the number of distinct states seen and whether the search really + exhausted all words of length at most `max_length`. + """ + calls = legal_calls(roles) + goal = wanted(roles, targets) + start = tuple(tuple(int(a == b) for b in range(roles)) for a in range(roles)) + seen = {start: None} + frontier = [start] + for depth in range(1, max_length + 1): + nxt = [] + for state in frontier: + for call in calls: + nxt_state = apply(state, call, roles) + if nxt_state in seen: + continue + seen[nxt_state] = (state, call) + if nxt_state == goal: + chain, cur = [], nxt_state + while seen[cur] is not None: + prev, call_used = seen[cur] + chain.append(list(call_used)) + cur = prev + chain.reverse() + return { + "roles": roles, + "targets": list(targets), + "searched_length": depth, + "witness": chain, + "states": len(seen), + "exhausted": True, + "cap_reached": False, + } + nxt.append(nxt_state) + frontier = nxt + if len(seen) > state_cap: + return { + "roles": roles, + "targets": list(targets), + "searched_length": None, + "witness": None, + "states": len(seen), + "exhausted": False, + "cap_reached": True, + } + return { + "roles": roles, + "targets": list(targets), + "searched_length": None, + "witness": None, + "states": len(seen), + "exhausted": True, + "cap_reached": False, + } + + +# ---------------------------------------------------------------- certificates + +# Three calls on one role multiply that role by the cube of its label: +# i^3 = zi and j^3 = zj. `spine(label, role)` is that three-call block. +def spine(label, role): + return [(label, 1 << role, 1 << role)] * 3 + + +SINGLE = spine(1, 0) +WITNESSES = { + "t1-zi": (1, (ZI,), spine(1, 0)), + "t1-zj": (1, (ZJ,), [(1, 1, 1)] * 2 + [(2, 1, 1)]), + "t2-zi-zj": (2, (ZI, ZJ), spine(1, 0) + spine(2, 1)), + "t2-zi-zi": (2, (ZI, ZI), spine(1, 0) + spine(1, 1)), + "t2-zj-zj": (2, (ZJ, ZJ), spine(2, 0) + spine(2, 1)), + "t3-zi-zi-zj": (3, (ZI, ZI, ZJ), spine(1, 0) + spine(1, 1) + spine(2, 2)), + "t3-zi-zi-zi": (3, (ZI, ZI, ZI), spine(1, 0) + spine(1, 1) + spine(1, 2)), + "t4-balanced": (4, (ZI, ZI, ZJ, ZJ), + spine(1, 0) + spine(1, 1) + spine(2, 2) + spine(2, 3)), +} + +# Complete breadth-first receipts. Each search ran to its limit and found no +# word of that length or shorter on exactly `roles` roles. For t = 1 and +# t = 2 the PR3589 bound already excludes every shorter length at every role +# count, so these receipts are a complete independent cross-check rather than +# the source of the lower bound. +CENSUS_CASES = [ + ("t1-zi", 1, (ZI,), 2), + ("t1-zj", 1, (ZJ,), 2), + ("t2-zi-zj", 2, (ZI, ZJ), 5), + ("t2-zi-zi", 2, (ZI, ZI), 5), + ("t2-zj-zj", 2, (ZJ, ZJ), 5), +] + + +def verify(): + receipt = {"algebra": {}, "witnesses": {}, "census": {}} + + # 1. The signed-unit table and the mask product agree on all 64 products. + products = sum( + group_product(a, b) == hamilton(a, b) + for a, b in itertools.product(range(8), repeat=2) + ) + require(products == 64, "Hamilton table disagreement") + receipt["algebra"]["q8_products"] = 64 + + # 2. The single-role generator really produces zi and zj in three calls. + require(mul(1 << 1, mul(1 << 1, 1 << 1)) == ZI, "i^3 is not zi") + require(mul(1 << 2, mul(1 << 2, 1 << 2)) == ZJ, "j^3 is not zj") + require(mul(Z, Z) == ONE, "z is not an involution") + receipt["algebra"]["i3_zi"] = True + receipt["algebra"]["j3_zj"] = True + + # 3. Every retained witness reaches its diagonal endpoint exactly. + for name, (roles, targets, word) in sorted(WITNESSES.items()): + require(endpoint(tuple(word), roles) == wanted(roles, targets), + "witness does not reach its endpoint: " + name) + bound, t, ti, tj = parity_lower_bound(targets) + receipt["witnesses"][name] = { + "roles": roles, + "targets": [targets[a] for a in range(roles)], + "calls": len(word), + "parity_bound": bound, + "t": t, + "t_i": ti, + "t_j": tj, + "attains_parity_bound": len(word) == bound, + } + + # 4. The complete breadth-first receipts are replayed from scratch. + for name, roles, targets, limit in CENSUS_CASES: + found = complete_census(roles, targets, limit) + receipt["census"][name] = found + require(found["exhausted"] and not found["cap_reached"], + "census did not exhaust: " + name) + require(found["searched_length"] is None, + "unexpected short word: " + name) + # The retained witness must sit exactly on the parity-rounded bound. + bound, _t, _ti, _tj = parity_lower_bound(targets) + require(len(WITNESSES[name][2]) == bound, + "witness misses the parity bound: " + name) + + return receipt + + +def main(): + receipt = verify() + text = json.dumps(receipt, indent=1, sort_keys=True) + (ROOT / "RESULT.json").write_text(text + "\n") + for name, row in sorted(receipt["witnesses"].items()): + print( + f"{name:16s} t={row['t']} calls={row['calls']:2d} " + f"bound={row['parity_bound']:2d} attained={row['attains_parity_bound']}" + ) + for name, row in sorted(receipt["census"].items()): + print( + f"census {name:16s} roles={row['roles']} " + f"min={row['searched_length']} exhausted={row['exhausted']} " + f"states={row['states']}" + ) + print("PASS mixed-negative Q8 minimum-length census") + + +if __name__ == "__main__": + main() \ No newline at end of file