From e18ca76987f5945c6a4b5b6bebbe73cdab3c4561 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 14 Oct 2026 23:24:43 +0100 Subject: [PATCH] feat(research): certify the QQ16 third-moment transcript floor --- research/qq16-third-moment-capacity/PROOF.md | 208 +++++++++++++++ research/qq16-third-moment-capacity/README.md | 125 +++++++++ .../qq16-third-moment-capacity/RESULT.json | 32 +++ .../qq16-third-moment-capacity/SOURCES.json | 42 +++ research/qq16-third-moment-capacity/TASK.json | 120 +++++++++ .../qq16-third-moment-capacity/VERIFY.json | 34 +++ .../qq16-third-moment-capacity/test_verify.py | 112 ++++++++ research/qq16-third-moment-capacity/verify.py | 248 ++++++++++++++++++ 8 files changed, 921 insertions(+) create mode 100644 research/qq16-third-moment-capacity/PROOF.md create mode 100644 research/qq16-third-moment-capacity/README.md create mode 100644 research/qq16-third-moment-capacity/RESULT.json create mode 100644 research/qq16-third-moment-capacity/SOURCES.json create mode 100644 research/qq16-third-moment-capacity/TASK.json create mode 100644 research/qq16-third-moment-capacity/VERIFY.json create mode 100644 research/qq16-third-moment-capacity/test_verify.py create mode 100644 research/qq16-third-moment-capacity/verify.py diff --git a/research/qq16-third-moment-capacity/PROOF.md b/research/qq16-third-moment-capacity/PROOF.md new file mode 100644 index 0000000000..3667d35512 --- /dev/null +++ b/research/qq16-third-moment-capacity/PROOF.md @@ -0,0 +1,208 @@ +# A third-moment lower bound for the QQ16 transcript + +Fix the conserved F0/B_1_2 maps and ordinary tail of Ali Romman's +[PR1969](https://github.com/CrocSwap/integer-mult-bounds/pull/1969), retained +in `research/joint-query`. Let G be a finite group of actual owner routes, +acting regularly, and write N=|G|. Use cover-dependent fields constant in +every payload block. Payload translations then act trivially, but the +owner action remains regular. No nonfaithful quotient identifies routes. + +Under the inherited erased-family observation contract, an additional +read-only rational-linear record of rank at most d leaves at least + +```text +max(0, ceil(176N/13) - d) +``` + +original selected A/T dimensions invisible. In particular, thirteen +rational scalars per owner leave at least ceil(7N/13) invisible dimensions. +Fourteen is necessary, not proved sufficient or a sharp minimum. + +The two-moment method is Ross Richardson's PR2104. The joint A/T defect +identity is commdata2338's PR2153. This contribution supplies the third +moment and the spectral polynomial that strengthen their bound. + +## 1. Exact route premise + +Write B_s=R_s iota_U for s=0,1,2. The ordinary set U has 96 ports. +For each p in U let r_p be its eight-component integer query column and +let g_s(p) be its owner route. The frozen packet gives + +```text +g_0(p)=1, ||r_p||^2=4, +sum_p r_p r_p^T=48 I_8. +``` + +Each g_s(p), s=1,2, swaps an ordered orthonormal eight-frame C_p in the +first nine binary axes with eight external axes E_s. The external axis +sets are disjoint: E_1 uses axes 9 through 16, E_2 uses 17 through 24. +Each route fixes the unused external block and the remaining 48 axes. +The 96 ordinary ordered frames C_p are distinct. + +These are finite source facts, checked on the literal F1/F2 alignment +maps and rebound to the current and future alignments in B_1_2. The +verifier checks both the complete ordered-product sets and an independent +chart-swap reconstruction. It does not execute the native local words. + +The swap description proves + +```text +{g_1(p)g_1(q): p,q in U} intersect +{g_2(r)g_2(t): r,t in U} = {1}. +``` + +Indeed, a stage-2 product fixes E_1 pointwise. If a stage-1 product also +fixes E_1, then g_1(q)e_i=C_q,i must equal g_1(p)^-1 e_i=C_p,i for every +external basis vector e_i. Distinctness of the ordered frames forces p=q. +The same argument gives r=t. Thus identity products have only diagonal +port pairs. The independent full census gives 9,216 ordered pairs and +9,121 distinct products per stage, with exactly one common product. + +The relative routes g_s(p)g_t(p)^-1 are also distinct over the 96 ports +for each s=tr(p(T)). The exact moments imply + +```text +rank([B0;B1;B2]) = rank(T) + >= [(85/39)24 - (248/169)28 + (48/169)(109/3)] N + = (280/13)N. +``` + +This improves the two-moment bound (144/7)N. It is still a lower bound, +not an exact rank calculation. Rational and real matrix ranks agree. + +## 4. Transfer to the selected-input defect + +This is PR2153's defect argument, restated to identify the inherited +contract. Write P_(s,A), P_(s,T) and ell_(s,A), ell_(s,T) for the +ordered selected sections and their two-sided inverses. For h in ker B1 +put only pair 0 nonzero and set + +```text +X_U=h, Y_U=0, +X_A=-P_(0,A)B0h-P_(2,A)B2h, Y_A=-X_A, +X_T=P_(0,T)ell_(0,A)P_(2,A)B2h, Y_T=-X_T. +``` + +The original selected defect J(h)=(X_A,X_T) determines both queries: + +```text +B0h=-ell_(0,A)X_A-ell_(0,T)X_T, +B2h=ell_(2,A)P_(0,A)ell_(0,T)X_T. +``` + +Conversely, the two queries determine J(h). Since rank(B1)=8N, + +```text +dim J(ker B1)=rank([B0;B1;B2])-8N >= ceil(176N/13). +``` + +The ordered F0 query is zero. After F0 the ordinary fields are X_U=Y_U=h, +the selected A fields are opposite P_(2,A)B2h, and both T fields are zero. +At B_1_2 the future query is zero, the logger clears its A output, +and the current query is B1h=0. Only Y_(0,U)=h remains. + +The retained witness proof and independent rational review establish +that the ordinary tail moves h into the former-Y hole. All selected +values after B1, completed-X descendants and five forward histories +are zero. Later homogeneous selected-only controls preserve zero. +The formal-h tail is inherited evidence, not rerun by this package. +There is no separately retained transient F0 A output or free read +of the former-Y hole in this observation contract. + +Restrict an additional rational-linear record to this family, obtaining +C of rank at most d. Linear algebra gives + +```text +dim J(ker C) >= dim J(ker B1) - rank(C). +``` + +A complement of ker C has dimension rank(C), so its image can account +for at most that many defect dimensions. A positive residual supplies +an input with zero observations but nonzero required selected output. +No decoder, even nonlinear, can distinguish it from zero. Fixed offsets +and common arbitrary dirty baselines do not change this comparison. + +For q scalars per owner, capacity is at most qN on this subspace. +At q=13 the residual is at least ceil(7N/13)>0. An eight-coordinate +record, including the full original R2 X query, leaves at least +ceil(72N/13) invisible dimensions. Extra independent payload storage +must count in d. These are information dimensions, not paid ranks. + +## 5. Limits + +The finite route facts and exact arithmetic are checked by the new +verifier. The spectral and defect implications are written proofs, +not proof-assistant formalizations. The global erased-family trajectory +and local packet-to-native binding remain inherited from PR1969. + +Records of width fourteen or fifteen remain unresolved. PR2174's +sixteen-coordinate logical recovery also grants selected values at +the B1 cut and does not supply a final-only physical controller. +Changed first pairs or schedules, nonlinear record encoders and a +complete native invoice lie outside this result. No supplier admission, +recursive precision bound or multiplication exponent change follows. diff --git a/research/qq16-third-moment-capacity/README.md b/research/qq16-third-moment-capacity/README.md new file mode 100644 index 0000000000..57e9359f93 --- /dev/null +++ b/research/qq16-third-moment-capacity/README.md @@ -0,0 +1,125 @@ +# QQ16 third-moment transcript capacity + +Thirteen rational query coordinates per regular-cover owner cannot repair +the fixed QQ16 selected-input loss under the retained erased-family +observation contract. The new certificate gives + +```text +rank([B0;B1;B2]) >= 280|G|/13, +selected A/T defect >= ceil(176|G|/13), +residual after a width-13 record >= ceil(7|G|/13). +``` + +Fourteen coordinates are necessary, not proved sufficient or optimal. +These are information dimensions, not paid recursive ranks. The selected +frontier and all frozen packages remain unchanged. No new supplier or κ. + +## What changed + +Ross Richardson's [PR2104](https://github.com/CrocSwap/integer-mult-bounds/pull/2104) +uses two exact moments to obtain rank at least 144|G|/7. +commdata2338's [PR2153](https://github.com/CrocSwap/integer-mult-bounds/pull/2153) +transfers that bound to the joint A/T defect and excludes records with at +most twelve coordinates per owner. + +This package adds the third moment, `tr(T^3)=(109/3)|G|`, for +`T=sum_s B_s*B_s/48`, and an exact cubic spectral certificate. It improves +their defect lower bound by 88|G|/91 and excludes width thirteen. +[PROOF.md](PROOF.md) includes the ordered route and defect arguments. + +Two different checks establish the new finite premise. A complete census +of 18,432 ordered route products finds that the stage-1 and stage-2 +product sets intersect only at identity. A chart-swap reconstruction +checks the same implication using disjoint external axes and 96 distinct +ordinary frames. Their identity triple coefficient is exactly 6,144. +No predecessor executable is imported. + +## Reproduce + +Python 3.12, standard library only, from the repository root: + +```sh +python3.12 -I -B scripts/research_package.py --package research/qq16-third-moment-capacity +python3.12 -I -O -B research/qq16-third-moment-capacity/verify.py +python3.12 -I -O -B research/qq16-third-moment-capacity/test_verify.py +``` + +Expected verifier line: + +```text +PASS_QQ16_THIRD_MOMENT_CAPACITY rank>=280|G|/13 defect>=176|G|/13 width>=14 no_new_kappa +``` + +Normal and optimized registered replay pass on Linux with CPython 3.12.15. +The direct normal/optimized verifier runs also pass under a 512 MiB +address-space cap, with a measured peak child RSS of 114,672 KiB. The Git +provenance launcher ran without that cap because Git maps a larger existing +packfile. All 65 research-workflow tests and selected-record integrity pass. + +The read-only verifier checks live source hashes and exact equality with +[RESULT.json](RESULT.json). Three semantic controls reject a changed query +coefficient, collapsed stage routes and a duplicate chart. Seven behavior +and arithmetic tests include source and receipt corruption through the CLI. +Validation stays enabled under `-O`. + +Source commits, Git blobs and hashes are in [SOURCES.json](SOURCES.json). +[TASK.json](TASK.json) records the central-handoff override, overlap, +predecessor heads, scope and final freshness check. The generic launcher +also authenticates historical task and selected-record provenance. + +## Verification limits + +This is author-checked exact finite source evidence plus a written proof. +It has no independent human or formal-kernel review. The retained QQ16 +witness supplies the global erased-family trajectory; this package does +not rerun it, the native local words or the full selected cold replay. + +Records of width fourteen and fifteen, nonlinear encoders and changed +trajectories remain outside the exclusion. Native access, retention, +cleanup, ownership, tape, recursive precision and supplier adoption remain +open. PR2174's adjacent sixteen-coordinate recovery grants the B1-cut +selected values; it is not a final-only controller or paid-cost invoice. + +## Implementation bounds + +The verifier has no recursion or dynamic code evaluation. Its route +products have exactly 96² iterations per stage; binary application has +at most 25 iterations. The 48 spectator axes must remain fixed. Packet +input is at most 1 MiB compressed and 16 MiB decompressed, and every +proof-relevant collection comes from fixed, hash-bound source bytes. +Functions stay below 60 physical lines and all semantic guards remain +active under optimization. Each test subprocess has a 30-second timeout. + +Power-of-ten rule 3 has a managed-runtime deviation in `verify.py` and +`test_verify.py`: Python allocates parsed objects, integers and census +tuples during checking. The fixed source dimensions, input caps and +18,432-product limit bound this batch workload. Replay under a memory cap +checks the compensating control. A fixed-capacity native implementation +would only be needed if this certificate becomes a larger search tool. +The diagnostics are `-Wall` compilation and normal/optimized tests. No +additional Python static analyzer was run. + +## Open next questions + +1. Can a higher-moment certificate exclude width fourteen or fifteen? + The exact stack rank determines the remaining information gap. First + compute another identity trace with all route products counted, then + bound the spectral indicator on [0,3]. The cover is too large for naive + matrix expansion, and additional moments may still not decide the gap. +2. Can a proposed width-fourteen or width-fifteen record recover the + selected inputs under the complete observation operator? Test its + kernel against all required selected rows before native costing. + No such record or final-only controller has been supplied. The + sixteen-coordinate result in PR2174 is a useful upper description + under its explicitly granted B1-cut observations. + +## Credit + +Nick Petalas. New work is Apache-2.0; retained notices are unchanged. +Ali Romman and the PR1969 contributors supplied the conserved maps, +selected sections, route packet and erased witness. Ross Richardson +supplied the two-moment method in PR2104. commdata2338 supplied the joint +A/T capacity argument in PR2153 and the adjacent recovery in PR2174. +Cinna Davis's PR2079/PR2122 and Adam Gall's PR2086/PR2093 supplied the +preceding query and logger investigations. The inherited supplier lineage +includes Rohan Arun, Jeremy Kothe, Hao Yan and Zhihao Chen. diff --git a/research/qq16-third-moment-capacity/RESULT.json b/research/qq16-third-moment-capacity/RESULT.json new file mode 100644 index 0000000000..af9794e8d3 --- /dev/null +++ b/research/qq16-third-moment-capacity/RESULT.json @@ -0,0 +1,32 @@ +{ + "route_census": { + "ordered_pairs_per_stage": 9216, + "distinct_products_per_stage": [ + 9121, + 9121 + ], + "intersection_size": 1, + "identity_pairs_per_stage": 96 + }, + "independent_distinct_swap_charts": 96, + "cross_trace_coefficient": 1536, + "triple_trace_coefficient": 6144, + "projector_moments_per_owner": [ + "24", + "28", + "109/3" + ], + "spectral_polynomial_coefficients": [ + "0", + "85/39", + "-248/169", + "48/169" + ], + "stacked_rank_lower_per_owner": "280/13", + "selected_defect_lower_per_owner": "176/13", + "width_thirteen_residual_lower_per_owner": "7/13", + "necessary_integer_record_width": 14, + "semantic_controls_rejected": 3, + "status": "PASS_QQ16_THIRD_MOMENT_CAPACITY", + "scope": "Regular-cover information dimension; inherited erased-family contract; no native invoice or new kappa." +} diff --git a/research/qq16-third-moment-capacity/SOURCES.json b/research/qq16-third-moment-capacity/SOURCES.json new file mode 100644 index 0000000000..9ae7ec4eaf --- /dev/null +++ b/research/qq16-third-moment-capacity/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "e8870e5917057d59b730eb14721a778639eca050", + "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7" + }, + { + "path": "research/joint-query/certificate.json.gz", + "usage": "input", + "git_blob": "c6e876d8b48d768214deee265ade428f8983b566", + "sha256": "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7" + }, + { + "path": "research/joint-query/evidence/QQ16-RATIONAL-OBSERVATION-REVIEW.md", + "usage": "input", + "git_blob": "c6ecf75654a084a9cc001bd62663f341976bae7a", + "sha256": "9a06ff40830ef80d3566fce77c78639cb64d519d487a0a7f57d543c3146e2c49" + }, + { + "path": "research/joint-query/evidence/QQ16-SELECTED-WITNESS.json", + "usage": "input", + "git_blob": "5082d791d0b993492cbc5bf61ac3b69e82c96f3f", + "sha256": "e35e5868a1322e406191079c0675975b139692ba50b1e2e5fb8a40b6480519f4" + }, + { + "path": "research/joint-query/evidence/QQ16-SELECTED-WITNESS.md", + "usage": "input", + "git_blob": "307650f45e37c28d14fe913958efa4fb429242b7", + "sha256": "52f2ee565320f05282c637aa79eee100606c24240b1b5866f0c8d62e7913c9fc" + } + ] +} diff --git a/research/qq16-third-moment-capacity/TASK.json b/research/qq16-third-moment-capacity/TASK.json new file mode 100644 index 0000000000..f053e0ab81 --- /dev/null +++ b/research/qq16-third-moment-capacity/TASK.json @@ -0,0 +1,120 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "joint-query-controller", + "question": "Can one explicitly changed QQ16 interface recover the missing chart query and close a two-call controller within a favorable full budget?", + "starting_points": [ + "research/joint-query/README.md", + "research/joint-query/evidence/QQ16-SELECTED-WITNESS.md", + "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Add one explicitly priced ordinary-to-selected observation and derive the ordered two-call map and inverse.", + "Change the first local pair or retained state, then test the existing lost-observation witness and price all new operations." + ], + "acceptance_gate": "Name the changed premise of the fixed F0/B1 observation obstruction. Show exactly which query is recovered, legal native reads and restoration, and a full favorable budget including cover maps, helpers and endpoints. Local inverse identities alone do not close the global controller.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the fixed-first-pair QQ16 witness before designing a controller. The checked #1969 local words do not evade that witness or supply global placement.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "Apply the existing witness to one proposed extra observation or changed first pair. If it still loses the required record, stop. Otherwise derive one ordered two-call identity and charge the added read, chart maps and restoration before extending to more stages.", + "bottleneck_link": "The native local words exist; retained query information and its physical access are the missing link to a composed recursive interface.", + "allowed_variations": [ + "One paid query, one changed first pair, or one precisely specified affine helper state.", + "A counterexample or lower bound for that exact proposed repair." + ], + "scope_change_triggers": [ + "Retaining the fixed first pair and ordinary schedule while allowing only homogeneous selected-only control, already excluded by the witness.", + "Treating cover-map counts as zero-cost physical address operations." + ], + "overlap_terms": [ + "QQ16", + "joint-query", + "changing-chart controller", + "selected observation", + "1969" + ] + }, + "scope_status": "refined", + "actual_scope": "Exclude every additional read-only rational-linear record of at most thirteen scalars per owner at the fixed QQ16 F0/B_1_2 erased-family cut, using an exact third-moment stacked-query rank bound.", + "scope_change_reason": "This takes PR2153's explicit sharper-rank handoff and narrows the card's allowed lower-bound variation to width-thirteen observations. It supplies an information obstruction, not the card's complete controller or favorable native-budget gate.", + "bottleneck_link": "Query retention and physical access are the missing controller interface. A stronger information bound rejects under-width linear repairs before implementation; it is not a paid-rank bound or supplier gain.", + "budget_minutes": 60, + "stop_rule": "Stop after the exact third moment, two different finite route checks, spectral proof, source bindings and failure controls. Do not expand to higher moments, controller synthesis or native costing in this session.", + "outcome": "negative-result", + "evidence": "PROOF.md proves rank >= 280|G|/13 and defect >= 176|G|/13. RESULT.json binds the complete 18432-product census, independent chart proof and exact arithmetic. Seven tests check the CLI and meaningful controls.", + "author": "Nick Petalas", + "ai_assistance": "Not recorded under account publication rules.", + "selection_seed": "84be42293ad21b2afb9d3364a81f6be3", + "initial_track": "incumbent-optimization", + "assignment_override": "Current central sharper-rank handoff preferred after live overlap showed generic scalar/packing cards were covered. No chooser reroll.", + "actual_scope_key": "QQ16-fixed-F0-B12/three-query-third-moment/transcript-capacity-q13", + "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2074#discussioncomment-18935134", + "predecessors": [ + {"pr": 1969, "author": "Ali Romman", "head": "a6e6ad3936f67b8f63b5b68c5e75d540610a65e7", "credit": "Conserved maps, exact route packet and erased-family witness; consumed from main."}, + {"pr": 2104, "author": "Ross Richardson", "head": "4bdc574da394a39f955e8cf4637075649c43a632", "credit": "Two-moment stacked-query rank method; no executable imported."}, + {"pr": 2153, "author": "commdata2338", "head": "5646398dcdc01769df83b939c6b3eb5ecb4d5ebd", "credit": "Joint A/T defect and transcript-capacity argument; restated with credit, no executable imported."}, + {"pr": 2174, "author": "commdata2338", "head": "f79470a7931f3943360c10d15b428e0e4e479c22", "credit": "Adjacent sixteen-coordinate logical recovery with granted B1-cut observations; not adopted as a supplier."} + ], + "entry_overlap": { + "open_prs": 425, + "pr_snapshot_at": "2026-10-14T22:09:27.054726+00:00", + "discussion_records": 857, + "discussion_snapshot_at": "2026-10-14T22:10:57.879794+00:00", + "complete_pagination": true, + "terms": ["QQ16", "QQ16 third moment", "third-moment", "fourteen coordinates", "transcript width"], + "result": "Exact third-moment terms matched only the existing sharper-rank handoff; generic QQ16 results were inspected for adjacent scope.", + "limits": "PR titles/bodies, Discussion records and local notes, not every code diff. No novelty certificate." + }, + "submission_freshness": { + "upstream_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "priority_revision": 4, + "upstream_checked_at": "2026-10-14T22:19:41Z", + "open_prs": 426, + "pr_snapshot_at": "2026-10-14T22:19:55.132854+00:00", + "discussion_records": 859, + "discussion_snapshot_at": "2026-10-14T22:21:22.365559+00:00", + "complete_pagination": true, + "warnings": [], + "result": "Exact terms matched this package and its claim, plus the predecessor's released sharper-rank handoff. PR2104, PR2153 and PR2174 heads remain unchanged and open. No competing third-moment scope found within stated coverage." + }, + "validation": { + "environment": "Linux x86_64, CPython 3.12.15, standard library only", + "commands": [ + "python3.12 -I -B scripts/research_package.py --package research/qq16-third-moment-capacity", + "python3.12 -I -O -B scripts/research_package.py --package research/qq16-third-moment-capacity", + "python3.12 -I -O -B research/qq16-third-moment-capacity/test_verify.py", + "python3.12 -Wall -m py_compile research/qq16-third-moment-capacity/verify.py research/qq16-third-moment-capacity/test_verify.py", + "python3.12 -B -m unittest discover -s tests -p 'test_research_*.py'", + "make selected-record-check", + "git diff --check" + ], + "results": "Normal and optimized registered replays pass; seven focused tests pass normally and optimized; all 65 research workflow tests pass; diagnostics, metadata pins and selected-record integrity pass. Direct normal/optimized verifier runs pass under a 512 MiB address-space cap with measured peak child RSS 114672 KiB and combined elapsed time 1.381 seconds.", + "verification_setup_failures": "The external /usr/bin/time binary is unavailable. Applying the 512 MiB cap to the generic launcher prevented Git from mapping this checkout's large existing packfile, before any proof check ran. Registered replay then passed without that cap; direct proof computation was separately checked under the cap.", + "not_run": "Global erased-family tail replay, native local-word replay, complete selected cold replay, proof-assistant verification and independent human review." + }, + "open_questions": [ + { + "question": "Can a higher-moment spectral certificate exclude width fourteen or fifteen?", + "why_it_matters": "It would narrow the remaining record-capacity gap before native implementation.", + "first_step": "Compute another exact identity trace with complete route-product coverage, then bound the rank indicator on [0,3].", + "blocked_by": "The regular cover is too large for naive matrix expansion; higher moments may still not settle the gap." + }, + { + "question": "Can a width-fourteen or width-fifteen record recover the required selected inputs under the complete observation operator?", + "why_it_matters": "Necessary record width alone does not supply a usable controller or favorable invoice.", + "first_step": "Propose a precise linear record and check its full observation kernel against all required selected rows before pricing it.", + "blocked_by": "No such record or final-only controller is supplied; PR2174 grants additional B1-cut observations." + } + ] +} diff --git a/research/qq16-third-moment-capacity/VERIFY.json b/research/qq16-third-moment-capacity/VERIFY.json new file mode 100644 index 0000000000..7006e8d72e --- /dev/null +++ b/research/qq16-third-moment-capacity/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/joint-query/certificate.json.gz", + "research/joint-query/evidence/QQ16-RATIONAL-OBSERVATION-REVIEW.md", + "research/joint-query/evidence/QQ16-SELECTED-WITNESS.json", + "research/joint-query/evidence/QQ16-SELECTED-WITNESS.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact source pins, complete ordered route census, independent chart-swap certificate, third moment, rational spectral bound and three semantic rejection controls." + }, + { + "argv": ["{python}", "-I", "-O", "-B", "{package}/verify.py"], + "timeout_seconds": 60, + "checks": "Same source-bound certificate and controls with optimization enabled; guards must remain active." + }, + { + "argv": ["{python}", "-I", "-B", "{package}/test_verify.py"], + "timeout_seconds": 120, + "checks": "Seven arithmetic and CLI behavior groups, including source and receipt corruption under optimization." + } + ] +} diff --git a/research/qq16-third-moment-capacity/test_verify.py b/research/qq16-third-moment-capacity/test_verify.py new file mode 100644 index 0000000000..f5e2b8fa65 --- /dev/null +++ b/research/qq16-third-moment-capacity/test_verify.py @@ -0,0 +1,112 @@ +#!/usr/bin/env python3 +"""Behavior and exact-arithmetic controls for the QQ16 certificate.""" +from fractions import Fraction as Q +import importlib.util +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent +SPEC = importlib.util.spec_from_file_location("qq16_moment", HERE / "verify.py") +if SPEC is None or SPEC.loader is None: + raise RuntimeError("Verifier import is unavailable") +verifier = importlib.util.module_from_spec(SPEC) +SPEC.loader.exec_module(verifier) + + +def polynomial(x): + return Q(85, 39)*x - Q(248, 169)*x*x + Q(48, 169)*x*x*x + + +def multiply(a, b): + return [[sum(a[i][k]*b[k][j] for k in range(2)) + for j in range(2)] for i in range(2)] + + +class CertificateTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.actual = verifier.report(verifier.ROOT) + + def test_literal_source_receipt(self): + expected = json.loads((HERE / "RESULT.json").read_bytes()) + self.assertEqual(self.actual, expected) + self.assertEqual(self.actual["projector_moments_per_owner"], + ["24", "28", "109/3"]) + self.assertEqual(self.actual["necessary_integer_record_width"], 14) + self.assertEqual(self.actual["semantic_controls_rejected"], 3) + + def test_factored_spectral_polynomial(self): + self.assertEqual([polynomial(Q(x)) for x in (0, 1, 3)], + [Q(0), Q(505, 507), Q(1)]) + self.assertEqual(polynomial(Q(13, 12)), 1) + for numerator in range(301): + x = Q(numerator, 100) + self.assertEqual(1-polynomial(x), + (1-Q(12, 13)*x)**2*(1-x/3)) + self.assertLessEqual(polynomial(x), 1) + + def test_sum_of_three_literal_projections(self): + vectors = ((Q(1), Q(0)), (Q(0), Q(1)), (Q(3, 5), Q(4, 5))) + matrix = [[sum(v[i]*v[j] for v in vectors) + for j in range(2)] for i in range(2)] + square = multiply(matrix, matrix) + cube = multiply(square, matrix) + moments = [sum(a[i][i] for i in range(2)) + for a in (matrix, square, cube)] + self.assertEqual(moments, [Q(3), Q(5), Q(9)]) + bound = Q(85, 39)*moments[0] - Q(248, 169)*moments[1] + Q(48, 169)*moments[2] + self.assertEqual(bound, Q(297, 169)) + self.assertLessEqual(bound, 2) # The two coordinate vectors span Q^2. + + def test_capacity_delta(self): + bound = Q(self.actual["selected_defect_lower_per_owner"]) + self.assertEqual(bound, Q(176, 13)) + self.assertEqual(bound-Q(88, 7), Q(88, 91)) + self.assertEqual(bound-13, Q(7, 13)) + self.assertLess(bound-14, 0) # No exclusion of width fourteen. + + def test_cli_positive(self): + completed = subprocess.run( + [sys.executable, "-I", "-B", str(HERE / "verify.py")], + text=True, capture_output=True, timeout=30, check=False) + self.assertEqual(completed.returncode, 0, completed.stderr) + self.assertEqual(completed.stdout.strip(), verifier.MARKER + + " rank>=280|G|/13 defect>=176|G|/13 width>=14 no_new_kappa") + + def test_cli_rejects_changed_source(self): + with tempfile.TemporaryDirectory() as name: + root = Path(name) + path = root / verifier.PACKET + path.parent.mkdir(parents=True) + path.write_bytes(b"not the pinned packet") + completed = subprocess.run( + [sys.executable, "-I", "-O", "-B", str(HERE / "verify.py"), + "--repo", str(root)], text=True, capture_output=True, + timeout=30, check=False) + self.assertNotEqual(completed.returncode, 0) + self.assertIn("source pin:", completed.stderr) + self.assertNotIn(verifier.MARKER, completed.stdout) + + def test_cli_rejects_changed_receipt(self): + with tempfile.TemporaryDirectory() as name: + root = Path(name) + shutil.copyfile(HERE / "verify.py", root / "verify.py") + bad = dict(self.actual) + bad["necessary_integer_record_width"] = 15 + (root / "RESULT.json").write_text(json.dumps(bad), encoding="utf-8") + completed = subprocess.run( + [sys.executable, "-I", "-O", "-B", str(root / "verify.py"), + "--repo", str(verifier.ROOT)], text=True, capture_output=True, + timeout=30, check=False) + self.assertNotEqual(completed.returncode, 0) + self.assertIn("receipt mismatch", completed.stderr) + self.assertNotIn(verifier.MARKER, completed.stdout) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/qq16-third-moment-capacity/verify.py b/research/qq16-third-moment-capacity/verify.py new file mode 100644 index 0000000000..c44eb3215a --- /dev/null +++ b/research/qq16-third-moment-capacity/verify.py @@ -0,0 +1,248 @@ +#!/usr/bin/env python3 +"""Source-bound QQ16 third-moment certificate. Apache-2.0.""" +import argparse +from fractions import Fraction as Q +import gzip +import hashlib +import io +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PACKET = "research/joint-query/certificate.json.gz" +PINS = { + PACKET: "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7", + "research/joint-query/evidence/QQ16-SELECTED-WITNESS.md": + "52f2ee565320f05282c637aa79eee100606c24240b1b5866f0c8d62e7913c9fc", + "research/joint-query/evidence/QQ16-SELECTED-WITNESS.json": + "e35e5868a1322e406191079c0675975b139692ba50b1e2e5fb8a40b6480519f4", + "research/joint-query/evidence/QQ16-RATIONAL-OBSERVATION-REVIEW.md": + "9a06ff40830ef80d3566fce77c78639cb64d519d487a0a7f57d543c3146e2c49", +} +A = (0, 7, 20, 27, 36, 46, 57, 111) +T = (21, 37, 47, 76, 81, 87, 92, 110) +U = tuple(p for p in range(112) if p not in A + T) +IDENTITY = tuple(1 << i for i in range(25)) +MARKER = "PASS_QQ16_THIRD_MOMENT_CAPACITY" + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def load_packet(repo): + raw_packet = None + for name, expected in PINS.items(): + path = repo / name + need(path.is_file() and path.stat().st_size <= 1_048_576, + "source size: " + name) + raw = path.read_bytes() + need(hashlib.sha256(raw).hexdigest() == expected, "source pin: " + name) + if name == PACKET: + raw_packet = raw + need(raw_packet is not None, "missing packet") + with gzip.GzipFile(fileobj=io.BytesIO(raw_packet)) as stream: + payload = stream.read(16_777_217) + need(len(payload) <= 16_777_216, "decompressed packet size") + return json.loads(payload) + + +def apply(columns, vector): + result = 0 + # Every vector is in the validated 25-axis space. + for _ in range(25): + if not vector: + return result + bit = vector & -vector + result ^= columns[bit.bit_length() - 1] + vector ^= bit + need(vector == 0, "binary vector bound") + return result + + +def compose(left, right): + return tuple(apply(left, c) for c in right) + + +def route(packet, event): + need(event[0] == "cover_map", "cover map event") + columns = packet["map_registry"][event[2]]["owner_right_matrix_columns"] + need(len(columns) == 73 and all(type(c) is int for c in columns), + "73 integer route columns") + need(all(0 < c < 1 << 25 for c in columns[:25]), "active route axes") + need(columns[25:] == [1 << i for i in range(25, 73)], + "route must fix all 48 spectator axes") + return tuple(columns[:25]) + + +def packet_data(packet): + need((tuple(packet["A_ports"]), tuple(packet["T_ports"]), + tuple(packet["U_ports"])) == (A, T, U), "selected partition") + need(len(packet["R_rows"]) == 8, "eight query rows") + R = [[Q(row.get(str(p), 0)) for p in range(112)] + for row in packet["R_rows"]] + need(all(x.denominator == 1 for row in R for x in row), "integer query") + R = [[int(x) for x in row] for row in R] + routes = [[IDENTITY] * 112] + for stage in (1, 2): + word = packet["programs"][f"F_{stage}"] + need(word[113][:2] == ["cover_sweep", "X_A_fused_query"], + "forward alignment cut") + events = word[1:113] + need([e[1] for e in events] == [["L", p] for p in range(112)], + "forward port order") + routes.append([route(packet, e) for e in events]) + need(packet["programs"]["F_0"][1][:2] == + ["cover_sweep", "X_A_fused_query"], "stage-zero identity cut") + word = packet["programs"]["B_1_2"] + need(len(word) <= 40_000, "backward event bound") + future = next(i for i, e in enumerate(word) + if e[:2] == ["cover_sweep", "future_E_t"]) + current = next(i for i, e in enumerate(word) + if e[:2] == ["cover_sweep", "Y_U_from_X_T"]) + for stage, events in ((2, word[future - 112:future]), + (1, word[current - 120:current - 8])): + need([e[1] for e in events] == [["L", 112+p] for p in range(112)], + "backward port order") + need([route(packet, e) for e in events] == routes[stage], + "forward/backward route binding") + return R, routes + + +def dot(left, right): + return sum(x*y for x, y in zip(left, right)) + + +def check_grams(R): + for ports, scale in ((U, 48), (A, 4), (T, 4)): + matrix = [[sum(R[i][p]*R[j][p] for p in ports) + for j in range(8)] for i in range(8)] + need(matrix == [[scale*int(i == j) for j in range(8)] + for i in range(8)], "query Gram") + need([sum(R[i][p]**2 for i in range(8)) for p in U] == [4]*96, + "ordinary column norms") + + +def check_swap_charts(routes): + """A separate certificate: chart swaps and disjoint external axes.""" + charts = [] + for p in U: + chart = tuple(routes[1][p][9+i] for i in range(8)) + need(all(0 < c < 512 for c in chart), "nine-axis chart") + need(all((x & y).bit_count() % 2 == int(i == j) + for i, x in enumerate(chart) for j, y in enumerate(chart)), + "orthonormal chart") + for stage, start in ((1, 9), (2, 17)): + need(tuple(routes[stage][p][start+i] for i in range(8)) == chart, + "common stage chart") + normals = tuple(chart[i] ^ (1 << (start+i)) for i in range(8)) + rebuilt = [] + for axis in range(25): + x, out = 1 << axis, 1 << axis + for n in normals: + if (x & n).bit_count() % 2: + out ^= n + rebuilt.append(out) + need(tuple(rebuilt) == routes[stage][p], "literal chart swap") + need(compose(routes[stage][p], routes[stage][p]) == IDENTITY, + "route involution") + charts.append(chart) + need(len(set(charts)) == 96, "distinct ordinary charts") + return len(set(charts)) + + +def pair_products(routes): + products = [] + for stage in (1, 2): + grouped = {} + for p in U: + for q in U: + key = compose(routes[stage][p], routes[stage][q]) + grouped.setdefault(key, []).append((p, q)) + need(len(grouped) == 9121, "ordered product census") + products.append(grouped) + common = set(products[0]) & set(products[1]) + need(common == {IDENTITY}, "stage-product intersection") + diagonal = [(p, p) for p in U] + need(products[0][IDENTITY] == products[1][IDENTITY] == diagonal, + "identity product fibres") + return {"ordered_pairs_per_stage": 9216, + "distinct_products_per_stage": [len(g) for g in products], + "intersection_size": len(common), "identity_pairs_per_stage": 96} + + +def moment_certificate(R, routes): + check_grams(R) + chart_count = check_swap_charts(routes) + census = pair_products(routes) + columns = {p: tuple(R[i][p] for i in range(8)) for p in U} + for s, t in ((0, 1), (0, 2), (1, 2)): + relative = {compose(routes[s][p], routes[t][p]) for p in U} + need(len(relative) == 96, "distinct relative routes") + cross = sum(dot(columns[p], columns[p])**2 for p in U) + triple = sum(dot(columns[p], columns[p])**3 for p in U) + need((cross, triple) == (1536, 6144), "identity coefficients") + moments = (Q(24), Q(24) + 6*Q(cross, 48**2), + Q(24) + 18*Q(cross, 48**2) + 6*Q(triple, 48**3)) + need(moments == (Q(24), Q(28), Q(109, 3)), "projector moments") + m1, m2, m3 = moments + bound = Q(85, 39)*m1 - Q(248, 169)*m2 + Q(48, 169)*m3 + need(bound == Q(280, 13), "cubic rank bound") + need(bound - 8 - 13 == Q(7, 13), "positive width-thirteen residual") + return {"route_census": census, "independent_distinct_swap_charts": chart_count, + "cross_trace_coefficient": cross, "triple_trace_coefficient": triple, + "projector_moments_per_owner": list(map(str, moments)), + "spectral_polynomial_coefficients": ["0", "85/39", "-248/169", "48/169"], + "stacked_rank_lower_per_owner": str(bound), + "selected_defect_lower_per_owner": str(bound - 8), + "width_thirteen_residual_lower_per_owner": str(bound - 21), + "necessary_integer_record_width": 14} + + +def rejected_mutations(R, routes): + count = 0 + bad_R = [row.copy() for row in R] + bad_R[0][U[0]] += 1 + try: + check_grams(bad_R) + except ValueError: + count += 1 + collapsed = [routes[0], routes[1], routes[1]] + try: + pair_products(collapsed) + except ValueError: + count += 1 + duplicate = [row.copy() for row in routes] + duplicate[1][U[1]] = duplicate[1][U[0]] + duplicate[2][U[1]] = duplicate[2][U[0]] + try: + check_swap_charts(duplicate) + except ValueError: + count += 1 + need(count == 3, "semantic mutation controls") + return count + + +def report(repo): + R, routes = packet_data(load_packet(repo)) + result = moment_certificate(R, routes) + result["semantic_controls_rejected"] = rejected_mutations(R, routes) + result["status"] = MARKER + result["scope"] = "Regular-cover information dimension; inherited erased-family contract; no native invoice or new kappa." + return result + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--repo", type=Path, default=ROOT) + args = parser.parse_args() + actual = report(args.repo) + expected = json.loads((HERE / "RESULT.json").read_bytes()) + need(actual == expected, "receipt mismatch") + print(MARKER + " rank>=280|G|/13 defect>=176|G|/13 width>=14 no_new_kappa") + + +if __name__ == "__main__": + main()