From 12269a5311577c5aabbba432558e89fb12de869c Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 20 Oct 2026 20:59:48 +0100 Subject: [PATCH] feat(research): bound imbalanced negative Q8 target shapes --- research/q8-negative-shape-bound/PROOF.md | 242 +++++++++++ research/q8-negative-shape-bound/README.md | 114 ++++++ research/q8-negative-shape-bound/SOURCES.json | 36 ++ research/q8-negative-shape-bound/TASK.json | 83 ++++ research/q8-negative-shape-bound/VERIFY.json | 36 ++ research/q8-negative-shape-bound/verify.py | 375 ++++++++++++++++++ 6 files changed, 886 insertions(+) create mode 100644 research/q8-negative-shape-bound/PROOF.md create mode 100644 research/q8-negative-shape-bound/README.md create mode 100644 research/q8-negative-shape-bound/SOURCES.json create mode 100644 research/q8-negative-shape-bound/TASK.json create mode 100644 research/q8-negative-shape-bound/VERIFY.json create mode 100644 research/q8-negative-shape-bound/verify.py diff --git a/research/q8-negative-shape-bound/PROOF.md b/research/q8-negative-shape-bound/PROOF.md new file mode 100644 index 0000000000..37d58cfc34 --- /dev/null +++ b/research/q8-negative-shape-bound/PROOF.md @@ -0,0 +1,242 @@ +# A shape-sensitive lower bound for mixed negative Q8 targets + +## Model and inherited identities + +Work in the full formal algebra `F2[Q8]`, with distinct basis elements +`1,z,i,zi,j,zj,ij,zij` and relations + +```text +i^2 = j^2 = z, z^2 = 1, ji = z ij. +``` + +Every scalar role starts with independent arbitrary dirty input. Free +operations are binary scalar GL changes of basis. Each paid call has the +normalized form + +```text +D_l = I + (1 + [g_l]) u_l v_l^T, +g_l in {i,j}, u_l,v_l binary, v_l^T u_l = 1. +``` + +The endpoint is diagonal, with `t_i` copies of `[zi]`, `t_j` copies of `[zj]` +and identity on all other roles. Put `t=t_i+t_j>0` and `n=n_i+n_j`. +Every extra dirty role must restore. The role count is any finite integer. + +We use the chronological identities of Nick Petalas's PR3578 and PR3589 +as premises, rather than independently re-certifying those packages. Let +X contain call columns u_l and Y contain call rows v_l^T. Form L as the +strictly lower triangular part of the FULL-role YX before restricting X +and Y to active output and input coordinates. Group call coordinates by +label, preserving chronological order inside each group. Write + +```text +X = (X_i X_j), Y = (Y_i; Y_j), +K_i = I + L_ii, K_j = I + L_jj. +``` + +Both K_i and K_j are invertible. The first-order equations are + +```text +X_i Y_i = P_i, X_j Y_j = P_j, XY = I_t, +rank(P_i)=t_i, rank(P_j)=t_j. +``` + +The two quadratic orientations give + +```text +X_i K_i Y_i + X_j(L_ji Y_i + K_j Y_j) = 0, (Q) +X_i K_i Y_i + (X_i L_ij + X_j K_j)Y_j = 0. (Q') +``` + +These equations also hold for mixed targets: the endpoint's first-order +sum and its tau coefficient are both I_t. The derivation of Q and Q' +uses this sum, not the homogeneous extra premise X_jY_j=0. Equivalently, +they are the two equations X(I+H)Y=0 in PR3589, expanded by label blocks. +Swapping i and j gives the reverse equations. PR3589's cubic argument gives + +```text +rank(X_i), rank(Y_i), rank(X_j), rank(Y_j) >= 3t-n. (C) +``` + +The first-order equations also imply `n_g>=t_g` and the trace parities +`n_i=t_i mod 2`, `n_j=t_j mod 2`. PR3736 records those block floors and +the previous necessary-count region. All ranks here are binary ranks. + +## The new quadratic inequalities + +Set a=rank(X_j) and b=rank(Y_j). Rank-nullity for X_jY_j=P_j gives + +```text +a+b <= n_j+t_j. (1) +``` + +Since rank(X_i),rank(Y_i)>=t_i and K_i is invertible, Sylvester gives + +```text +rank(X_i K_i Y_i) >= 2t_i-n_i. +``` + +Equation Q bounds this rank by a; equation Q' bounds it by b. These +bounds remain valid when the right side is negative. Therefore + +```text +4t_i-2n_i <= a+b <= n_j+t_j, +2n_i+n_j >= 4t_i-t_j. (2) +``` + +Exchanging labels proves the companion inequality. Thus every exact word +satisfies the new pair + +```text +2n_i+n_j >= 4t_i-t_j, +n_i+2n_j >= 4t_j-t_i. (3) +``` + +For t_j=0 this recovers the homogeneous quadratic inequality of PR3578. +The new content is its mixed-target correction term and its combination +with the mixed cubic ranks. In particular, replacing n_j+t_j in (1) by +n_j would be unsound; the nonzero product P_j has to remain charged. + +## Shape-sensitive total counts + +The cubic ranks C and rank-nullity give the inherited inequalities + +```text +2n+n_i >= 6t-t_i, 2n+n_j >= 6t-t_j. (4) +``` + +Add the second inequality of (4) to the first inequality of (3), written +as `2n-n_j >= 4t_i-t_j`. This gives + +```text +4n >= 6t+4t_i-2t_j = 10t_i+4t_j. +``` + +Swapping labels and retaining PR3589's sum bound proves + +```text +n >= max(11(t_i+t_j)/5, (5t_i+2t_j)/2, (2t_i+5t_j)/2). (5) +``` + +The first term is inherited. The other terms improve it exactly when +one target multiplicity is greater than four times the other. Consequently +attainment of the real-valued 11t/5 bound requires +`t_i <= 4t_j` and `t_j <= 4t_i`. This is a restriction on the possible +equality shapes, not a construction at any of the remaining shapes. + +## Exact projection of this necessary-count region + +Consider ONLY the following arithmetic relaxation: nonnegative integer +n_i,n_j, the block floors, the two trace parities, the two inherited cubic +count inequalities (4), and the two new quadratic inequalities (3). +Its exact minimum is + +```text +N(t_i,t_j) = t + 2 max(ceil(3t/5), ceil(3t_i/4), ceil(3t_j/4)). (6) +``` + +This is not asserted to be a realizable word length. To prove (6), write + +```text +n_i=t_i+2a, n_j=t_j+2b, s=a+b, a,b nonnegative integers. +``` + +The four inequalities become + +```text +3a+2b >= t_i+2t_j, 2a+3b >= 2t_i+t_j, +2a+b >= t_i-t_j, a+2b >= t_j-t_i. +``` + +For fixed integer s, a is allowed exactly when + +```text +max(0, t_i+2t_j-2s, t_i-t_j-s) + <= a <= +min(s, 3s-2t_i-t_j, 2s+t_i-t_j). (7) +``` + +Both endpoints are integers. Comparing the three lower endpoints with +the three upper endpoints gives exactly + +```text +s >= 0, +3s >= 2t_i+t_j, 3s >= t_i+2t_j, +2s >= t_i-t_j, 2s >= t_j-t_i, +5s >= 3t, 4s >= 3t_i, 4s >= 3t_j. +``` + +The ninth comparison repeats s>=0. The last three inequalities imply +all earlier ones. For example, 5s>=3t and 4s>=3t_i imply + +```text +s >= (5/9)(3t/5) + (4/9)(3t_i/4) = (2t_i+t_j)/3. +``` + +The other three-fold bound follows by symmetry. Also +`3t_i/4 >= (t_i-t_j)/2` for nonnegative multiplicities, and likewise +after swapping labels. Hence (7) is nonempty exactly when + +```text +s >= max(ceil(3t/5), ceil(3t_i/4), ceil(3t_j/4)). +``` + +Choosing the lower endpoint in (7) explicitly supplies integer a,b in +this arithmetic relaxation. This proves both necessity and sufficiency +for that relaxation and establishes (6), including parity. + +## A strict improvement and an infinite excluded family + +At shape `(t_i,t_j)=(7,1)`, the old mixed cubic/floor/parity region +admits `(n_i,n_j)=(7,11)`, total 18. The new first quadratic inequality +would require `25>=27`, so that pair is impossible. Formula (6) gives +N(7,1)=20, attained within the relaxation by `(n_i,n_j)=(7,13)`. +An actual 20-call word is not supplied. The direct word costs 24. + +More generally, for every positive integer k, shape `(7k,k)` and counts +`(7k,11k)` satisfy every old mixed cubic/floor/parity condition, but violate +the new quadratic inequality `25k>=27k`. Also every actual word at that +shape has `n>=37k/2`; parity strengthens this to +`n>=8k+2 ceil(21k/4)`. Thus the improvement is not confined to a finite +search domain. No universal 5t/2 mixed-target bound is asserted. + +The relaxation is still insufficient: at shape (2,1), (6) gives seven, +while PR3536's separate full-algebra result gives the actual minimum nine. +That earlier minimum is cited, not independently replayed here. In +particular the four-target ten-versus-twelve questions are unchanged. + +## Evidence, limits and credit + +The proof above is a scoped mathematical argument using PR3578/PR3589's +chronological equations as inherited premises. Its new step is the +mixed quadratic rank charge, followed by the exact integer projection. +The verifier corroborates the projection by exhaustive bounded integer +enumeration and checks full formal direct words as positive controls. +Its generic binary rank fixtures test the new rank inference; they are +not endpoint realizations. The emitted receipt binds all package and +declared input bytes by SHA256. No receipt is written by hand. + +Produced by Nick Petalas. Nick Petalas's PR3570, PR3578, PR3589 and PR3736 +retain credit for the cubic identities, homogeneous method, mixed ranks +and previous count region. Their retained lineage includes PR3536 and +PR3558's chronological and cyclic methods, PR3517's normalization, +Tuafo/PR2900, ywz65/PR2587, PR3487, Aaron Wang/PR2318, Cinna Davis, +steph4n-gh and the credited Q8/register sources. Standard rank inequalities +are not claimed as new. Exact source pins appear in SOURCES.json. + +Independent human and formal proof-kernel review are unclaimed. No actual +shorter word, physical caller, scalar/routing/hosting/precision invoice, +supplier admission, multiplication theorem or new kappa is supplied. +The selected frontier is unchanged. The selected full cold replay, Lean +and Docker builds were not run because this result changes none of them. + +## Open next questions + +- Can any imbalanced shape attain (6) as a full eight-coefficient endpoint? + Start at (7,1), where the new bound is 20 and direct execution costs 24. + Count fixtures alone cannot answer this question. +- Does equality in both rank charges impose a further obstruction? Start + at the simultaneous quadratic/cubic equalities on the real boundary + t_i=4t_j, retaining the same chronological L in both orientations. +- Any formal saving still needs a matched physical caller and complete + invoice. No such caller is identified by the count theorem. diff --git a/research/q8-negative-shape-bound/README.md b/research/q8-negative-shape-bound/README.md new file mode 100644 index 0000000000..8f583087e1 --- /dev/null +++ b/research/q8-negative-shape-bound/README.md @@ -0,0 +1,114 @@ +# A shape-sensitive bound for mixed negative Q8 targets + +For t_i inverse-i targets and t_j inverse-j targets, every exact positive-Q8 +word in the retained dirty-register model satisfies + +```text +2n_i+n_j >= 4t_i-t_j, n_i+2n_j >= 4t_j-t_i, +2n >= 5t_i+2t_j, 2n >= 2t_i+5t_j. +``` + +This is a scoped proof with finite corroboration. It strengthens the inherited +11t/5 total-call bound when one target multiplicity exceeds four times the +other. At shape (7,1), the previous necessary-count region allowed 18 calls; +the new lower bound is 20. No 20-call construction is supplied. Direct +execution costs 24, so the actual minimum remains in {20,22,24}. + +The exact minimum of the strengthened INTEGER COUNT RELAXATION is + +```text +N(t_i,t_j) = t_i+t_j + + 2 max(ceil(3(t_i+t_j)/5), ceil(3t_i/4), ceil(3t_j/4)). +``` + +This projects the block floors, trace parities, inherited cubic count +inequalities and the two new quadratic inequalities. It is not an attainable +word classification. For example the relaxation permits seven at shape +(2,1), whose actual minimum nine is already established in PR3536. + +[PROOF.md](PROOF.md) gives the new mixed quadratic rank charge, the uniform +proof, the exact integer projection and the infinite excluded family +(t_i,t_j;n_i,n_j)=(7k,k;7k,11k). The argument permits any finite number +of arbitrary restored dirty spectators and arbitrary binary scalar GL mixing. +Paid calls are positive i/j rank-one idempotent calls in the full formal +F2[Q8] algebra. Extra call types, clean workspace and physical costs are +outside this model. + +## Evidence and reproduction + +From the repository root, use CPython 3.12: + +```sh +~/git/integer-mult-bounds/.venv/bin/python3.12 -B research/q8-negative-shape-bound/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/q8-negative-shape-bound +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/q8-negative-shape-bound --check-source-history +``` + +The registered normal and optimized commands enumerate every candidate +nonnegative surplus split through total target count 64, compare its exact +minimum with the formula, and construct an arithmetic witness for each shape. +They also check the new rank inference on small binary matrices, exact full +Q8 direct words with two arbitrary dirty spectators, every regular basis +column of those words, and failure controls. These finite checks corroborate +the written proof; they do not independently re-certify the predecessor +chronological identities. The verifier prints a deterministic receipt bound +to all package files and declared source bytes, and writes no files. + +[SOURCES.json](SOURCES.json) pins the inherited proofs and historical catalogue +and selected record at main `12fa8c5c844be21bfefb38a19503fbd867a11244`. +[TASK.json](TASK.json) records the changed card scope. This is a mathematical +side result for `bit-new-register-model`, not a new legal native construction. + +## Limitations + +The exact word minimum at shape (7,1), realizability of the count fixtures, +all physical scalar/routing/restoration/hosting/precision costs and supplier +admission remain unresolved. Unknown costs are not zero. No multiplication +theorem, kappa improvement or selected-frontier change is claimed. The selected +full cold replay, Lean and Docker builds are unrelated and were not run. +Independent human and formal proof-kernel review are unclaimed. + +The verifier uses Python-managed allocations, bounded by its fixed target, +binary-width and ten-role limits. This is the documented Power of Ten rule-3 +deviation: Python allocates tuples and integers during enumeration. Results +are aggregated rather than retaining candidate splits. If the bounds grow, +review the live-memory bound before widening them. Every loop has a finite +input or fixed-range bound; functions stay below 60 physical lines. Explicit +ValueError contracts remain active under optimized Python. No recursion, +dynamic code, external solver, subprocess or dependency is used by the verifier. +Warnings are treated as errors in both registered scientific commands. + +## Related open work + +- [PR3906](https://github.com/CrocSwap/integer-mult-bounds/pull/3906) checks + arbitrary-dirty restoration of the one/two-target direct construction. It + does not derive the mixed shape bound. The overlapping one/two-target + counts are exactly 3 and 6 here, matching that package and PR3697. +- [PR2444](https://github.com/CrocSwap/integer-mult-bounds/pull/2444) supplies + generic noncommutative exact-search tooling and a different GL2/S3 census. + It does not study this inverse-Q8 target-count projection; no numerical + quantity is shared. + +## Open next questions + +- Is there a full 20-call word for seven zi and one zj targets? Start with + the legal splits at n=20 and the complete eight-coefficient endpoint + equations. This decides whether the new floor is attained, but no endpoint + search or physical caller is supplied here. +- Can simultaneous equality in the new quadratic and inherited cubic rank + charges be realized at t_i=4t_j? Keep one chronological L in both + orientations. Further count fixtures cannot establish realizability. +- Can an actual caller benefit from an improved formal word after its complete + physical bill? First name that caller and its permitted layout and reads. + No such caller or full invoice is currently supplied by this package. + +## Credit + +This contribution was produced by Nick Petalas. PR3578 supplies the homogeneous +quadratic method, PR3589 the mixed cubic boundary ranks, and PR3736 the old +necessary-count comparison. All are used as credited premises, not offered +as a new verification deliverable. Their PR3570/PR3536/PR3558/PR3517, +Tuafo/PR2900, ywz65/PR2587, PR3487, Aaron Wang/PR2318, Cinna Davis, +steph4n-gh and Q8/register predecessor attribution is retained in PROOF.md. +The mixed-target correction and its exact integer projection are new here. +New work is Apache-2.0. diff --git a/research/q8-negative-shape-bound/SOURCES.json b/research/q8-negative-shape-bound/SOURCES.json new file mode 100644 index 0000000000..31df15970d --- /dev/null +++ b/research/q8-negative-shape-bound/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/q8-count-region-rank-floor/PROOF.md", + "usage": "input", + "git_blob": "d73cc9414e1205352fcd8d150bd3e80bfd922204", + "sha256": "6e07f2cdb87619b95869ff4650de1fe12b9767a6171ac68fcae7d553b7657381" + }, + { + "path": "research/q8-homogeneous-mixed-floor/PROOF.md", + "usage": "input", + "git_blob": "e35410f07b26d9edb0851b3777b3753ef181b4bf", + "sha256": "472ba6f092199d6d10450cfd38c126268aee4d071004acaabaf6b9d551ad340d" + }, + { + "path": "research/q8-mixed-boundary-rank/PROOF.md", + "usage": "input", + "git_blob": "771efad64c1a7930d6e68d55ace64357d27fdcc0", + "sha256": "331c45cd80d563bf956caa029db241014dc66235b41f6fa83833e3c7ee5f4294" + } + ] +} diff --git a/research/q8-negative-shape-bound/TASK.json b/research/q8-negative-shape-bound/TASK.json new file mode 100644 index 0000000000..abb95f2bc0 --- /dev/null +++ b/research/q8-negative-shape-bound/TASK.json @@ -0,0 +1,83 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 7, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "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": "A shape-sensitive necessary-call theorem for mixed negative Q8 targets, and the exact integer projection of its strengthened count relaxation.", + "scope_change_reason": "This extends the explicitly open sharpness question after PR3589 and the count region in PR3736. It stays in the retained formal nonabelian model rather than supplying a new native operation alphabet; the result is a scoped mathematical obstruction, not supplier admission.", + "bottleneck_link": "Mathematical side result for the nonabelian bit-register model. It rules out previously permitted imbalanced target counts; physical implementation and the binding complex supplier remain outside scope.", + "budget_minutes": 60, + "stop_rule": "Prove the mixed quadratic rank inequalities and exact count-relaxation projection, corroborate them by bounded exact enumeration and rank/direct-word controls, and stop before endpoint search or physical implementation.", + "outcome": "completed", + "evidence": "PROOF.md and deterministic hash-bound stdout receipt from verify.py; bounded exhaustive integer projection, arithmetic witnesses, binary rank fixtures, full Q8 direct words and failure controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Is a full 20-call word possible at the (7,1) inverse-target shape?", + "why_it_matters": "The new theorem leaves the actual minimum in {20,22,24}.", + "first_step": "Use the legal n=20 splits and all eight formal endpoint coefficient equations.", + "blocked_by": "No endpoint realization or exhaustive word exclusion is supplied." + }, + { + "question": "Can the quadratic and cubic equality cases be realized simultaneously at t_i=4t_j?", + "why_it_matters": "The boundary determines whether the inherited 11t/5 count can be attained at its extreme ratio.", + "first_step": "Use the same chronological L in both orientations and inspect equality in each rank charge.", + "blocked_by": "Necessary count witnesses need not lift to endpoint words." + }, + { + "question": "Can a formal word improve a matched complete physical caller bill?", + "why_it_matters": "Formal call counts alone do not imply an exponent gain.", + "first_step": "Name a caller, its source and output layout, allowed reads and all scalar and recursive costs.", + "blocked_by": "No such physical caller or complete invoice is supplied." + } + ], + "coordination": { + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19080549", + "upstream_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "priority_revision": 7, + "checked_utc": "2026-10-20T19:59:00Z", + "overlap_coverage": "Complete cached pagination: 340 open PRs and 2972 Discussion records at 2026-10-20T19:53Z. Live first 100 open PRs and latest handoff comments refreshed before commit. Relevant open PRs 3906 and 2444 have distinct scopes; historical Q8 titles and source proofs were inspected. Unpublished work and arbitrary code diffs are outside this coverage." + } +} diff --git a/research/q8-negative-shape-bound/VERIFY.json b/research/q8-negative-shape-bound/VERIFY.json new file mode 100644 index 0000000000..c5e59716db --- /dev/null +++ b/research/q8-negative-shape-bound/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/q8-count-region-rank-floor/PROOF.md", + "research/q8-homogeneous-mixed-floor/PROOF.md", + "research/q8-mixed-boundary-rank/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exhaustive bounded integer projection and constructive count witnesses; new binary rank inference; complete dirty Q8 direct words and failure controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same scientific checks under optimized Python, with explicit contracts active." + } + ] +} diff --git a/research/q8-negative-shape-bound/verify.py b/research/q8-negative-shape-bound/verify.py new file mode 100644 index 0000000000..ed414ce092 --- /dev/null +++ b/research/q8-negative-shape-bound/verify.py @@ -0,0 +1,375 @@ +#!/usr/bin/env python3 +"""Corroborate the new Q8 shape bound; emit a deterministic hash-bound receipt. + +Produced by Nick Petalas. Apache-2.0. +""" + +import hashlib +import itertools +import json +from pathlib import Path + +MAX_TARGETS = 64 +MAX_BINARY_WIDTH = 3 +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def ceil_div(value, divisor): + require(value >= 0 and divisor > 0, "invalid nonnegative ceiling") + return (value + divisor - 1) // divisor + + +def count_bound(ti, tj): + return ( + ti + + tj + + 2 * max(ceil_div(3 * (ti + tj), 5), ceil_div(3 * ti, 4), ceil_div(3 * tj, 4)) + ) + + +def allowed(ti, tj, ni, nj, strengthened): + t, n = ti + tj, ni + nj + if ni < ti or nj < tj or (ni - ti) % 2 or (nj - tj) % 2: + return False + if 2 * n + ni < 6 * t - ti or 2 * n + nj < 6 * t - tj: + return False + return not strengthened or ( + 2 * ni + nj >= 4 * ti - tj and ni + 2 * nj >= 4 * tj - ti + ) + + +def enumerate_counts(): + records, improved, candidates, feasible = [], [], 0, 0 + for t in range(1, MAX_TARGETS + 1): + for ti in range(t + 1): + tj, old_min, new_min = t - ti, None, None + for s in range(t + 1): + has_pair = False + for a in range(s + 1): + candidates += 1 + ni, nj = ti + 2 * a, tj + 2 * (s - a) + old_ok = allowed(ti, tj, ni, nj, False) + new_ok = allowed(ti, tj, ni, nj, True) + if old_ok and old_min is None: + old_min = ni + nj + if new_ok: + feasible += 1 + has_pair = True + if new_min is None: + new_min = ni + nj + require( + has_pair == (t + 2 * s >= count_bound(ti, tj)), + f"projection mismatch at {(ti, tj, s)}", + ) + require( + old_min is not None and new_min == count_bound(ti, tj), + f"minimum mismatch at {(ti, tj)}", + ) + records.append([ti, tj, old_min, new_min]) + if ti and tj and new_min > old_min: + improved.append([ti, tj, old_min, new_min]) + require([7, 1, 18, 20] in improved, "missing strict mixed improvement") + return { + "shapes": len(records), + "candidate_splits": candidates, + "feasible_splits": feasible, + "improved_mixed_shapes": len(improved), + "records_sha256": digest(records), + "first_improvements": improved[:12], + } + + +def canonical_count_witnesses(): + records = [] + for t in range(1, MAX_TARGETS + 1): + for ti in range(t + 1): + tj = t - ti + s = (count_bound(ti, tj) - t) // 2 + a = max(0, ti + 2 * tj - 2 * s, ti - tj - s) + b = s - a + require(a >= 0 and b >= 0, "negative interval witness") + require( + allowed(ti, tj, ti + 2 * a, tj + 2 * b, True), + "invalid constructive count witness", + ) + records.append([ti, tj, ti + 2 * a, tj + 2 * b]) + return {"witnesses": len(records), "sha256": digest(records)} + + +def matrix_rank(rows, width): + require(0 <= width <= MAX_BINARY_WIDTH, "binary width exceeds bound") + basis = [0] * width + rank = 0 + for original in rows: + row = original + require(0 <= row < 1 << width, "binary row outside width") + for pivot in range(width - 1, -1, -1): + if row & (1 << pivot): + if basis[pivot]: + row ^= basis[pivot] + else: + basis[pivot] = row + rank += 1 + break + return rank + + +def binary_product(left, right): + out = [] + for row in left: + value = 0 + for index, other in enumerate(right): + if row & (1 << index): + value ^= other + out.append(value) + return tuple(out) + + +def lower_units(width): + slots = [(row, col) for row in range(width) for col in range(row)] + for bits in range(1 << len(slots)): + rows = [1 << index for index in range(width)] + for index, (row, col) in enumerate(slots): + if bits & (1 << index): + rows[row] |= 1 << col + yield tuple(rows) + + +def check_new_rank_step(): + pairs, middle_units = 0, 0 + for width in range(MAX_BINARY_WIDTH + 1): + lefts = tuple(itertools.product(range(1 << width), repeat=2)) + rights = tuple(itertools.product(range(4), repeat=width)) + for left in lefts: + a = matrix_rank(left, width) + for right in rights: + pairs += 1 + b = matrix_rank(right, 2) + p = matrix_rank(binary_product(left, right), 2) + require(a + b <= width + p, "nonzero-product rank charge") + require(2 * min(a, b) <= width + p, "two-sided rank charge") + for unit in lower_units(width): + middle_units += 1 + product = binary_product(binary_product(left, unit), right) + require( + matrix_rank(product, 2) >= a + b - width, + "invertible chronological middle rank", + ) + zero_product_mutant = matrix_rank((1, 2), 2) * 2 + require(zero_product_mutant > 2, "nonzero product correction was lost") + return {"rectangular_pairs": pairs, "chronological_middle_cases": middle_units} + + +def q8_mul(left, right): + a, b, c = left & 1, (left >> 1) & 1, left >> 2 + d, e, f = right & 1, (right >> 1) & 1, right >> 2 + sign = c ^ f ^ (a & d) ^ (b & e) ^ (b & d) + return (a ^ d) | ((b ^ e) << 1) | (sign << 2) + + +def left_basis_action(group, coefficient): + result = 0 + for basis in range(8): + if coefficient & (1 << basis): + result ^= 1 << q8_mul(group, basis) + return result + + +def right_basis_action(coefficient, group): + result = 0 + for basis in range(8): + if coefficient & (1 << basis): + result ^= 1 << q8_mul(basis, group) + return result + + +def group_controls(): + require(q8_mul(1, 1) == q8_mul(2, 2) == 4, "Q8 squares") + require(q8_mul(1, 2) == 3 and q8_mul(2, 1) == 7, "Q8 noncommutation") + cases = 0 + for a, b, c in itertools.product(range(8), repeat=3): + require( + q8_mul(q8_mul(a, b), c) == q8_mul(a, q8_mul(b, c)), + "group multiplication is not associative", + ) + cases += 1 + return {"associative_triples": cases} + + +def apply_call(matrix, group, u, v): + size = len(matrix) + require(group in (1, 2), "only positive i/j calls are paid") + require( + 0 < u < 1 << size and 0 < v < 1 << size, + "call vectors outside the finite role space", + ) + require((u & v).bit_count() % 2 == 1, "non-idempotent paid call") + row_sum = [0] * size + for index, row in enumerate(matrix): + if v & (1 << index): + row_sum = [a ^ b for a, b in zip(row_sum, row, strict=True)] + increment = [value ^ left_basis_action(group, value) for value in row_sum] + return tuple( + tuple( + value ^ (increment[col] if u & (1 << row) else 0) + for col, value in enumerate(values) + ) + for row, values in enumerate(matrix) + ) + + +def identity(size): + return tuple(tuple(int(row == col) for col in range(size)) for row in range(size)) + + +def target(ti, tj, dirty): + diagonal = [1 << 5] * ti + [1 << 6] * tj + [1] * dirty + return tuple( + tuple(value if row == col else 0 for col in range(len(diagonal))) + for row, value in enumerate(diagonal) + ) + + +def full_word_controls(): + words, entries, calls, dirty_basis_columns = 0, 0, 0, 0 + for t in range(1, 9): + for ti in range(t + 1): + tj, dirty = t - ti, 2 + matrix = identity(t + dirty) + for role in range(t): + group = 1 if role < ti else 2 + for _ in range(3): + matrix = apply_call(matrix, group, 1 << role, 1 << role) + calls += 1 + require(matrix == target(ti, tj, dirty), "full dirty endpoint differs") + require(3 * t >= count_bound(ti, tj), "direct upper word violates bound") + words += 1 + entries += (t + dirty) ** 2 + for col in range(t + dirty): + for basis in range(8): + actual = tuple( + right_basis_action(row[col], basis) for row in matrix + ) + inverse = 5 if col < ti else (6 if col < t else 0) + expected = tuple( + (1 << q8_mul(inverse, basis)) if row == col else 0 + for row in range(t + dirty) + ) + require(actual == expected, "regular dirty basis column differs") + dirty_basis_columns += 1 + return { + "direct_words": words, + "formal_entries": entries, + "paid_calls_executed": calls, + "regular_basis_columns_covered": dirty_basis_columns, + } + + +def failure_controls(): + controls = [] + require(allowed(7, 1, 7, 11, False), "old comparison fixture rejected") + require(not allowed(7, 1, 7, 11, True), "new inequality missing") + controls.append("old eighteen-call fixture rejected by new inequality") + require(allowed(2, 1, 2, 5, True), "necessary-only seven-call fixture lost") + controls.append("count relaxation does not assert endpoint existence") + require(count_bound(7, 1) == 20 and count_bound(1, 7) == 20, "shape/parity control") + controls.append("label exchange and parity strengthen the real bound") + exact = target(1, 0, 2) + mutant = [list(row) for row in exact] + mutant[1][0] = 1 + require(tuple(tuple(row) for row in mutant) != exact, "dirty leak accepted") + controls.append("full matrix rejects off-diagonal dirty leakage") + try: + apply_call(identity(2), 1, 1, 2) + except ValueError: + controls.append("non-idempotent call rejected") + else: + raise ValueError("non-idempotent call accepted") + for k in range(1, 257): + require(allowed(7 * k, k, 7 * k, 11 * k, False), "old scaled fixture") + require(not allowed(7 * k, k, 7 * k, 11 * k, True), "scaled exclusion") + require( + count_bound(7 * k, k) == 8 * k + 2 * ceil_div(21 * k, 4), + "scaled parity projection", + ) + controls.append("256 scaled strict exclusions corroborate the uniform family") + return controls + + +def digest(value): + payload = json.dumps(value, sort_keys=True, separators=(",", ":")).encode() + return hashlib.sha256(payload).hexdigest() + + +def read_limited(path, limit): + with path.open("rb") as stream: + payload = stream.read(limit + 1) + require(len(payload) <= limit, "source exceeds byte bound: " + str(path)) + return payload + + +def authenticated_sources(): + payload = read_limited(PACKAGE / "SOURCES.json", 65536) + manifest = json.loads(payload) + expected = { + "docs/research/agent-task-catalog.json", + "certificates/selected-result.json", + "research/q8-count-region-rank-floor/PROOF.md", + "research/q8-homogeneous-mixed-floor/PROOF.md", + "research/q8-mixed-boundary-rank/PROOF.md", + } + require(len(manifest["files"]) == len(expected), "source inventory size changed") + require( + {row["path"] for row in manifest["files"]} == expected, + "source inventory changed", + ) + hashes = {} + for row in manifest["files"]: + if row["usage"] == "provenance": + continue + require(row["usage"] == "input", "unknown source role") + path = ROOT / row["path"] + payload = read_limited(path, 4 * 1024 * 1024) + actual = hashlib.sha256(payload).hexdigest() + require(actual == row["sha256"], "source hash mismatch: " + row["path"]) + hashes[row["path"]] = actual + for name in ( + "PROOF.md", + "README.md", + "TASK.json", + "SOURCES.json", + "VERIFY.json", + "verify.py", + ): + path = PACKAGE / name + hashes[path.relative_to(ROOT).as_posix()] = hashlib.sha256( + read_limited(path, 4 * 1024 * 1024) + ).hexdigest() + return hashes + + +def main(): + source_hashes = authenticated_sources() + result = { + "status": "PASS_Q8_NEGATIVE_SHAPE_BOUND", + "claim_type": "scoped proof with finite corroboration", + "count_projection": enumerate_counts(), + "count_witnesses": canonical_count_witnesses(), + "rank_step": check_new_rank_step(), + "q8_algebra": group_controls(), + "direct_words": full_word_controls(), + "failure_controls": failure_controls(), + "source_sha256": source_hashes, + } + result["receipt_sha256"] = digest(result) + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()