From f2206e608167995b9b96b7e340b3558f2b578490 Mon Sep 17 00:00:00 2001 From: ToikY <27568617+ToikY@users.noreply.github.com> Date: Wed, 11 Nov 2026 01:57:57 -0800 Subject: [PATCH 1/2] Reuse selected replay navigation for hosted checks Reuse the exact documentation blob carried by #7161 at bb36fc65ee0b161229169505f4840c436c5ca2b9, following #7147 and #7156. --- docs/ci-verification.md | 19 ++++++++++++++++++- 1 file changed, 18 insertions(+), 1 deletion(-) diff --git a/docs/ci-verification.md b/docs/ci-verification.md index 63ba3e9aa8..52b62d0481 100644 --- a/docs/ci-verification.md +++ b/docs/ci-verification.md @@ -1,8 +1,25 @@ # CI verification -## Current selected-family replay: #6030 +## Current selected-family replay: #7000 with #7001 The [selected record](../certificates/selected-result.json) binds conditional +κ = 0.00363005817 to the [application review](research/pr-intake-evidence/pr7000-application/PROOF-REVIEW.md), +[validation receipts](research/pr-intake-evidence/pr7000-application/VALIDATION.json), +and [explicit source closure](../certificates/frontier7000-source.json). +`make frontier7000-verify` follows that exact-source selected replay. The review +reuses eleven authenticated preceding executions and records seven fresh serial +application, scalar and complete native-catalogue executions. The earlier +monolithic timeout is retained separately and is not completed coverage. +Consult the receipts for exact commands, source heads and limits. + +The five inherited framework assumptions remain. No complete uniform word, +literal multiplier execution, independent human proof or formal-kernel proof +is asserted. Routine research submissions do not need to rerun this +selected-family replay. The sections below preserve historical checkpoints. + +## Historical selected-family replay: #6030 + +The [historical checkpoint](../certificates/checkpoints/frontier6030.json) binds conditional κ = 0.003125804 to the [proof review](research/pr-intake-evidence/pr6030-audit/PROOF-REVIEW.md), [validation receipts](research/pr-intake-evidence/pr6030-audit/VALIDATION.json), and [explicit source closure](../certificates/frontier6030-source.json). From 08f41734863055b42b3975c0d434ecf2ca4fcaf8 Mon Sep 17 00:00:00 2001 From: ToikY <27568617+ToikY@users.noreply.github.com> Date: Wed, 11 Nov 2026 02:25:05 -0800 Subject: [PATCH 2/2] Exclude cached strict-prefix BIT donors for eight retags --- research/bit-strict-prefix-envelope/CERT.json | 542 ++++++++++++++++++ research/bit-strict-prefix-envelope/PROOF.md | 21 + research/bit-strict-prefix-envelope/README.md | 23 + .../bit-strict-prefix-envelope/RESULT.json | 36 ++ .../bit-strict-prefix-envelope/SOURCES.json | 36 ++ research/bit-strict-prefix-envelope/TASK.json | 77 +++ .../bit-strict-prefix-envelope/VERIFY.json | 23 + research/bit-strict-prefix-envelope/retag.py | 67 +++ research/bit-strict-prefix-envelope/verify.py | 224 ++++++++ 9 files changed, 1049 insertions(+) create mode 100644 research/bit-strict-prefix-envelope/CERT.json create mode 100644 research/bit-strict-prefix-envelope/PROOF.md create mode 100644 research/bit-strict-prefix-envelope/README.md create mode 100644 research/bit-strict-prefix-envelope/RESULT.json create mode 100644 research/bit-strict-prefix-envelope/SOURCES.json create mode 100644 research/bit-strict-prefix-envelope/TASK.json create mode 100644 research/bit-strict-prefix-envelope/VERIFY.json create mode 100644 research/bit-strict-prefix-envelope/retag.py create mode 100644 research/bit-strict-prefix-envelope/verify.py diff --git a/research/bit-strict-prefix-envelope/CERT.json b/research/bit-strict-prefix-envelope/CERT.json new file mode 100644 index 0000000000..b5a715a31c --- /dev/null +++ b/research/bit-strict-prefix-envelope/CERT.json @@ -0,0 +1,542 @@ +{ + "explicit": [ + [32929,344,[0]], + [32929,345,[0]], + [32929,346,[0]], + [32929,266,[0]], + [32929,269,[0]], + [32929,271,[0]], + [32929,273,[0]], + [32929,275,[0]], + [32929,276,[0]], + [32929,506,[0]], + [32929,113,[0]], + [32929,114,[0]], + [32929,115,[0]], + [32929,116,[0]], + [32929,117,[0]], + [32929,118,[0]], + [32929,119,[0]], + [32929,120,[0]], + [32929,121,[0]], + [32929,122,[0]], + [32929,123,[0]], + [32929,124,[0]], + [32929,127,[0]], + [32929,139,[0]], + [32929,145,[0]], + [32929,146,[0]], + [32929,157,[0]], + [32929,169,[0]], + [32929,175,[0]], + [32929,176,[0]], + [32929,190,[0]], + [32929,194,[0]], + [32929,205,[0]], + [32929,211,[0]], + [32929,212,[0]], + [32929,223,[0]], + [32929,229,[0]], + [32929,230,[0]], + [32929,241,[0]], + [32929,247,[0]], + [32929,248,[0]], + [32929,259,[0]], + [32929,265,[0]], + [32929,8,[0]], + [32929,11,[0]], + [32929,12,[0]], + [32929,13,[0]], + [32929,14,[0]], + [32929,15,[0]], + [32929,48,[0]], + [32929,49,[0]], + [32929,50,[0]], + [32929,51,[0]], + [32929,52,[0]], + [32929,53,[0]], + [32929,54,[0]], + [32929,55,[0]], + [32929,56,[0]], + [32929,57,[0]], + [32929,58,[0]], + [32929,59,[0]], + [32929,60,[0]], + [32929,75,[0]], + [32929,76,[0]], + [32929,77,[0]], + [32929,78,[0]], + [32929,79,[0]], + [32929,80,[0]], + [32929,81,[0]], + [32929,82,[0]], + [32929,83,[0]], + [32929,84,[0]], + [32929,85,[0]], + [32929,86,[0]], + [32929,87,[0]], + [32929,88,[0]], + [32929,89,[0]], + [32929,90,[0]], + [32929,91,[0]], + [32929,92,[0]], + [32929,93,[0]], + [32929,94,[0]], + [32929,95,[0]], + [32929,96,[0]], + [32929,97,[0]], + [32929,98,[0]], + [32929,99,[0]], + [32929,100,[0]], + [32929,101,[0]], + [32929,102,[0]], + [32929,103,[0]], + [32929,104,[0]], + [32981,326,[0]], + [32981,329,[1]], + [32981,330,[0]], + [32981,266,[0]], + [32981,267,[1]], + [32981,272,[1]], + [32981,273,[0]], + [32981,274,[1]], + [32981,275,[0]], + [32981,507,[1]], + [32981,114,[0]], + [32981,125,[1]], + [32981,126,[1]], + [32981,127,[0]], + [32981,128,[0]], + [32981,129,[0]], + [32981,130,[0]], + [32981,131,[0]], + [32981,132,[0]], + [32981,133,[0]], + [32981,139,[0]], + [32981,140,[0]], + [32981,151,[0]], + [32981,157,[0]], + [32981,158,[0]], + [32981,163,[0]], + [32981,169,[0]], + [32981,170,[0]], + [32981,181,[0]], + [32981,185,[0]], + [32981,193,[0]], + [32981,194,[0]], + [32981,200,[0]], + [32981,206,[0]], + [32981,212,[0]], + [32981,223,[0]], + [32981,229,[0]], + [32981,230,[0]], + [32981,241,[0]], + [32981,247,[0]], + [32981,248,[0]], + [32981,254,[0]], + [32981,260,[0]], + [32981,11,[0,5]], + [32981,12,[0]], + [32981,13,[0]], + [32981,14,[0]], + [32981,15,[0]], + [32981,32,[0]], + [32981,33,[0]], + [32981,34,[0]], + [32981,35,[0]], + [32981,36,[0]], + [32981,37,[0]], + [32981,38,[0]], + [32981,39,[0]], + [32981,40,[0]], + [32981,41,[0]], + [32981,42,[0]], + [32981,43,[0]], + [32981,44,[0]], + [32981,45,[0]], + [32981,46,[0]], + [32981,47,[0]], + [32981,61,[0]], + [32981,62,[0]], + [32981,63,[0]], + [32981,64,[0]], + [32981,65,[0]], + [32981,66,[0]], + [32981,67,[0]], + [32981,68,[0]], + [32981,69,[0]], + [32981,70,[0]], + [32981,71,[0]], + [32981,72,[0]], + [32981,73,[0]], + [32981,74,[0]], + [32981,90,[0]], + [32981,91,[0]], + [32981,92,[0]], + [32981,93,[0]], + [32981,94,[0]], + [32981,95,[0]], + [32981,96,[0]], + [32981,97,[0]], + [32981,98,[0]], + [32981,99,[0]], + [32981,100,[0]], + [32981,101,[0]], + [32981,102,[0]], + [32981,103,[0]], + [32981,104,[0]], + [33032,345,[9]], + [33032,347,[3]], + [33032,349,[3]], + [33032,267,[0,3]], + [33032,269,[5]], + [33032,270,[3]], + [33032,272,[3]], + [33032,275,[6]], + [33032,277,[0,3]], + [33032,506,[0,3]], + [33032,113,[3]], + [33032,114,[3]], + [33032,115,[3]], + [33032,116,[3]], + [33032,117,[3]], + [33032,118,[3]], + [33032,119,[3]], + [33032,120,[3]], + [33032,121,[3]], + [33032,122,[3]], + [33032,123,[3]], + [33032,124,[3]], + [33032,125,[5]], + [33032,134,[3]], + [33032,145,[3]], + [33032,151,[3]], + [33032,157,[3]], + [33032,158,[3]], + [33032,163,[3]], + [33032,164,[3]], + [33032,175,[3]], + [33032,181,[3]], + [33032,185,[3]], + [33032,193,[3]], + [33032,199,[3]], + [33032,200,[3]], + [33032,211,[3]], + [33032,217,[3]], + [33032,223,[3]], + [33032,224,[3]], + [33032,235,[3]], + [33032,236,[3]], + [33032,247,[3]], + [33032,253,[3]], + [33032,259,[3]], + [33032,260,[3]], + [33032,8,[3]], + [33032,11,[0,3]], + [33032,16,[3]], + [33032,17,[3]], + [33032,22,[3]], + [33032,23,[3]], + [33032,25,[3]], + [33032,27,[3]], + [33032,28,[3]], + [33032,30,[3]], + [33032,34,[3]], + [33032,35,[3]], + [33032,36,[3]], + [33032,37,[3]], + [33032,40,[3]], + [33032,42,[3]], + [33032,45,[3]], + [33032,47,[3]], + [33032,48,[3]], + [33032,49,[3]], + [33032,50,[3]], + [33032,54,[3]], + [33032,56,[3]], + [33032,58,[3]], + [33032,60,[3]], + [33032,61,[3]], + [33032,62,[3]], + [33032,66,[3]], + [33032,67,[3]], + [33032,68,[3]], + [33032,69,[3]], + [33032,72,[3]], + [33032,73,[3]], + [33032,77,[3]], + [33032,78,[3]], + [33032,81,[3]], + [33032,82,[3]], + [33032,83,[3]], + [33032,84,[3]], + [33032,86,[3]], + [33032,88,[3]], + [33032,90,[3]], + [33032,91,[3]], + [33032,94,[3]], + [33032,95,[3]], + [33032,99,[3]], + [33032,101,[3]], + [33032,103,[3]], + [33032,105,[0,3]], + [33032,106,[3]], + [33032,107,[3]], + [33032,108,[0,3]], + [33032,109,[0,3]], + [33032,110,[0,3]], + [33032,111,[0,3]], + [33032,112,[3]], + [33041,488,[12]], + [33041,491,[0]], + [33041,492,[0]], + [33041,277,[10]], + [33041,289,[0]], + [33041,301,[0]], + [33041,305,[0]], + [33041,310,[0]], + [33041,320,[0]], + [33041,521,[0]], + [33041,113,[0]], + [33041,119,[0]], + [33041,125,[5]], + [33041,130,[0]], + [33041,136,[0]], + [33041,143,[0]], + [33041,149,[0]], + [33041,155,[0]], + [33041,161,[0]], + [33041,166,[0]], + [33041,173,[0]], + [33041,179,[0]], + [33041,184,[0]], + [33041,187,[0]], + [33041,194,[0]], + [33041,195,[0]], + [33041,196,[0]], + [33041,197,[0]], + [33041,198,[0]], + [33041,199,[0]], + [33041,200,[0]], + [33041,201,[0]], + [33041,202,[0]], + [33041,203,[0]], + [33041,204,[0]], + [33041,205,[0]], + [33041,206,[0]], + [33041,207,[0]], + [33041,208,[0]], + [33041,209,[0]], + [33041,210,[0]], + [33041,211,[0]], + [33041,217,[0]], + [33041,218,[0]], + [33041,229,[0]], + [33041,235,[0]], + [33041,236,[0]], + [33041,247,[0]], + [33041,249,[0]], + [33041,250,[0]], + [33041,253,[0]], + [33041,8,[0]], + [33041,12,[0]], + [33041,15,[0]], + [33041,16,[0]], + [33041,17,[0]], + [33041,22,[0]], + [33041,23,[0]], + [33041,24,[0]], + [33041,26,[0]], + [33041,29,[0]], + [33041,31,[0]], + [33041,34,[0]], + [33041,35,[0]], + [33041,36,[0]], + [33041,37,[0]], + [33041,41,[0]], + [33041,43,[0]], + [33041,44,[0]], + [33041,46,[0]], + [33041,48,[0]], + [33041,49,[0]], + [33041,50,[0]], + [33041,55,[0]], + [33041,57,[0]], + [33041,59,[0]], + [33041,61,[0]], + [33041,62,[0]], + [33041,66,[0]], + [33041,67,[0]], + [33041,70,[0]], + [33041,71,[0]], + [33041,74,[0]], + [33041,77,[0]], + [33041,78,[0]], + [33041,81,[0]], + [33041,82,[0]], + [33041,85,[0]], + [33041,87,[0]], + [33041,89,[0]], + [33041,90,[0]], + [33041,91,[0]], + [33041,94,[0]], + [33041,95,[0]], + [33041,98,[0]], + [33041,100,[0]], + [33041,102,[0]], + [33041,104,[0]], + [33041,105,[0,1]], + [33041,106,[0]], + [33041,107,[0]], + [33041,108,[0,1]], + [33041,109,[0,8]], + [33041,110,[0,1]], + [33041,111,[0,1]], + [33041,112,[0]], + [33837,471,[2]], + [33837,473,[1]], + [33837,475,[2,4]], + [33837,266,[2,4]], + [33837,278,[1]], + [33837,300,[7]], + [33837,306,[1]], + [33837,309,[1]], + [33837,323,[2]], + [33837,522,[2]], + [33837,118,[1]], + [33837,119,[1]], + [33837,130,[1]], + [33837,131,[1]], + [33837,135,[1]], + [33837,144,[1]], + [33837,150,[1]], + [33837,153,[1]], + [33837,159,[1]], + [33837,165,[1]], + [33837,174,[1]], + [33837,180,[1]], + [33837,183,[1]], + [33837,186,[1]], + [33837,191,[1]], + [33837,194,[1]], + [33837,205,[1]], + [33837,211,[1]], + [33837,212,[2]], + [33837,213,[2]], + [33837,214,[2]], + [33837,215,[1]], + [33837,216,[1]], + [33837,217,[1]], + [33837,218,[1]], + [33837,219,[1]], + [33837,220,[1]], + [33837,221,[1]], + [33837,222,[1]], + [33837,223,[1]], + [33837,224,[1]], + [33837,225,[1]], + [33837,226,[1]], + [33837,227,[1]], + [33837,228,[1]], + [33837,229,[1]], + [33837,230,[1]], + [33837,232,[1]], + [33837,234,[1]], + [33837,248,[1]], + [33837,254,[1]], + [33837,260,[1]], + [33837,11,[0,1]], + [33837,12,[1]], + [33837,13,[1]], + [33837,14,[1]], + [33837,15,[1]], + [33837,17,[0,1]], + [33837,19,[1]], + [33837,21,[1]], + [33837,23,[1]], + [33837,26,[1]], + [33837,27,[1]], + [33837,30,[1]], + [33837,31,[1]], + [33837,33,[0,1]], + [33837,35,[0,1]], + [33837,37,[2]], + [33837,39,[0,1]], + [33837,42,[1]], + [33837,43,[1]], + [33837,46,[0,1]], + [33837,47,[2]], + [33837,49,[1]], + [33837,50,[0,1]], + [33837,52,[1,5]], + [33837,55,[1]], + [33837,56,[0,1]], + [33837,57,[1,5]], + [33837,58,[1]], + [33837,62,[1]], + [33837,63,[1]], + [33837,65,[1,5]], + [33837,67,[0,1]], + [33837,71,[1]], + [33837,72,[1]], + [33837,73,[1]], + [33837,74,[1]], + [33837,76,[1]], + [33837,78,[1]], + [33837,79,[2]], + [33837,81,[2]], + [33837,84,[1]], + [33837,85,[0,1]], + [33837,86,[1]], + [33837,87,[1]], + [33837,91,[2]], + [33837,93,[1]], + [33837,94,[2]], + [33837,96,[1]], + [33837,100,[1]], + [33837,101,[1]], + [33837,102,[1]], + [33837,103,[1]], + [33837,108,[0,1]], + [33837,110,[0,1]], + [33837,111,[0,1]], + [33860,453,[8]], + [33860,455,[4]], + [33860,457,[7]], + [33860,266,[1,7]], + [33860,278,[2]], + [33860,300,[4]], + [33860,303,[2]], + [33860,312,[2]], + [33860,322,[4]], + [33860,523,[7]], + [33860,118,[2]], + [33860,119,[2]] + ], + "aggregate": [ + [33860,[0,3,5,106,116,125,127,129,131,138,142,144,148,152,155,156,159,161,167,170,173,175,178,179,184,200,203,205]], + [33876,[17,24,30,108,113,125,127,132,138,150,162,164,176,180,186,189,191,192,196,197,199,200,201]], + [33883,[0,3,14,22,109,119,134,135,137,140,142,145,148,153,156,165,181,188,193,208,209,211]], + [19154,[0]], + [19155,[0]], + [19201,[3]], + [19202,[3]], + [19235,[5]], + [19236,[5]], + [19153,[0]], + [19167,[1]], + [19168,[1]], + [19180,[2]], + [19181,[2]], + [19200,[3]], + [19214,[4]], + [19215,[4]], + [19233,[5]], + [19234,[5]], + [19277,[7]], + [19278,[7]], + [19289,[8]], + [19290,[8]], + [19291,[8]] + ] +} diff --git a/research/bit-strict-prefix-envelope/PROOF.md b/research/bit-strict-prefix-envelope/PROOF.md new file mode 100644 index 0000000000..d1b84f77bf --- /dev/null +++ b/research/bit-strict-prefix-envelope/PROOF.md @@ -0,0 +1,21 @@ +# Exact full-prefix separation + +## Retained word and edit + +Use the canonical [#7001 package](https://github.com/CrocSwap/integer-mult-bounds/tree/e54523517d0f03e58352e647c403a5af3e525a57/research/paired-query-only-bit) at e54523517d0f03e58352e647c403a5af3e525a57. The eight first chronological source backups are ports 0, 1, 2, 3, 4, 5, 7 and 8. Retag their initial copies and same-chart ADD blocks to chart zero, drop the old helper ingresses, extend the literal egresses from chart zero, and merge the two late consumer ascents around the backup read. The backup is cleared in chart zero. The immutable source and retag generator determine every old event index. Replaying both words checks all 659 normalized outputs and final charts, and both retain peak 237 owned fields and 237 erasures. The retag is a local checked schedule. + +## Why the dual is decisive + +In the retained split gauge, a nested MOVE acts as identity on the normalized coefficient row, equal-chart ADD acts as XOR, SWAP exchanges rows, INIT supplies zero, and CLEAR removes the row. This gauge uses the retained projector action. It is a change of coordinates for reasoning. Let H be the target chart of an adjusted MOVE from zero. A rank credit from strict-prefix reuse requires a chart G of positive rank strictly below H with G contained in H, and the target normalized row must already be obtainable in G by the unchanged due cut. For such G the remaining MOVE would cost rank dim(H)−dim(G). Exact rational row reduction validates each chart's A/B complement and identifies identical projectors. Orthogonality to the target complement tests strict containment. + +Grant free copies of all nonzero normalized rows in G that occur anywhere in the retained retag prefix through the first subsequent contact with the recipient. The state can change only at a touched role. The checker records each row's earliest cut from the literal schedule, so earlier availability cannot be missed. This includes a hypothetical cache established before the receiver's quiet window and allows the recipient's own earlier rows in G. A new address map or newly routed cache is outside the declared retained-prefix premise. + +A dual evaluates to zero on every row in that cache and to one on the required row. It therefore rules out obtaining that row by any XOR combination. Because the inputs are independent binary fields, even address-dependent scalar choices within the common chart cannot span the required coefficient vector at any address. For an untested chart, a dual for the union over several pending charts implies a dual for each constituent chart. The same overgrant does not assert availability of a physical cross-chart XOR. + +All 35 target deadlines are covered. There are 973 strict-chart/recipient combinations in the retained frame inventory. The first deterministic cap of 512 nonempty cases yielded 512 exact duals. Exactly 79 cases have empty prefixes. At the second gate 24 recipient-wide duals cover the 382 remaining cases, with no pending or positive chart. Certificate keys are unique and all are consumed. The replay checks each dual directly on observed rows using a literal timeline distinct from the interval-history discovery. Its controls reject a newly present contaminating row and a dual that fails to pair with the target. No donated rounds, Git objects outside this checkout, temporary pointers or third-party Python libraries are required by the verifier. + +## Directed price and scope + +For `H_r = r^(1−κ)`, the recounted paid delta is `−48H_1 + 21H_2 − 6H_3 + 6H_4 − 8H_6 + 8H_7`. At raw trial 0.004008162992724 it costs about 7.737987275061839 per native invocation. Under the proposed wrapper accounting of 18 changed calls and ideal full removed QUERY credit 111, the per-call allowance is `(111 + sum(T_r H_r) − sum(P_r H_r))/18`, using the exact old #7001 caller profiles. Its directed upper is about 2.814112181981564. Strict-prefix reuse removes zero from that bill. The directed excess is strictly positive with all new ordinary work granted free. The allowance is conditional on that proposed wrapper interface, which is not a new admitted caller. + +The result excludes a retained single strict chart as the source for any one revised delivery under this fixed chronology. It does not cover physical multi-chart synthesis, new paid cache formation, altered contacts, nonnested transport, or the 103 other ports. No new all-size supplier, compiler, tape result or κ is claimed. diff --git a/research/bit-strict-prefix-envelope/README.md b/research/bit-strict-prefix-envelope/README.md new file mode 100644 index 0000000000..d592f542ff --- /dev/null +++ b/research/bit-strict-prefix-envelope/README.md @@ -0,0 +1,23 @@ +# Exclude cached strict-prefix donors for eight BIT retags + +**κ change 0%.** On eight literal source-chart retags of the #7001 BIT native word, all 35 adjusted deliveries lack a supporting retained strict-subchart donor. The result grants a free cache of every normalized row observed in the chart before the delivery's literal deadline. The full raw paid excess remains about **4.923875093080274** per changed native call at the stated trial, even with free cache, routing and restoration. + +[Proof and scope](PROOF.md) · [Directed receipt](RESULT.json) + +## Clean replay + +From a clean checkout, use CPython 3.12 with assertions: + +```sh +python3.12 -B scripts/research_package.py --package research/bit-strict-prefix-envelope +``` + +The replay authenticates the canonical retained native word, caller invoice and independent interval implementation. It reconstructs the literal eight-port retag and visits the old and new schedules. It checks every public normalized endpoint, nested MOVE, owned lifetime and the old native paid bill. It verifies 512 chart duals and 24 recipient-wide duals for the remaining 382 nonempty charts. Another 79 charts have no eligible retained row. The exact receipt records the recomputed paid delta and directed conditional allowance. + +## Open next questions + +A distinct route can change the native address action or construct new cache rows. Start with one explicitly charged nonnested or oblique donor and show its complete signed action and return. Extending the same quiet-window census cannot change the exhausted strict-prefix result. The other 103 ports, a new paid cache, cross-chart physical combinations, and whole-application verification remain open. + +## Credit + +CubeJerry's #7001 supplies the retained native word, paid caller and independent arithmetic. Credit #6726/#6834/#6980 and the delayed-cover authors for its native/projector lineage, and the Round 12–15 #7111 work for the retag, exact bound and prior quiet-window checks. The formal #7177 caller supplies the QUERY deletion and proposed raw credit. The #7198 scalar cache construction has a different premise, a common query stream. Related #7188/#7190 bounds concern paired IDLE operations. OpenAI Codex and subagents materially assisted. Apache-2.0. diff --git a/research/bit-strict-prefix-envelope/RESULT.json b/research/bit-strict-prefix-envelope/RESULT.json new file mode 100644 index 0000000000..0ee22d2823 --- /dev/null +++ b/research/bit-strict-prefix-envelope/RESULT.json @@ -0,0 +1,36 @@ +{ + "available_strict_donor_credit": [ + 0, + 0 + ], + "price": { + "conditional_allowance": [ + "281411218198156414791311154346389473473343547227920423823042722374305928296696589/100000000000000000000000000000000000000000000000000000000000000000000000000000000", + "70352804549539103697827788586597368368335886806980105955760680593576482074713429/25000000000000000000000000000000000000000000000000000000000000000000000000000000" + ], + "cost": [ + "193449681876545962645076978666954946721353727892988976730678547723250536954598169/25000000000000000000000000000000000000000000000000000000000000000000000000000000", + "193449681876545962645076978666954946721353727892988976730678547723250536954601923/25000000000000000000000000000000000000000000000000000000000000000000000000000000" + ], + "delta": { + "1": -48, + "2": 21, + "3": -6, + "4": 6, + "6": -8, + "7": 8 + }, + "excess": [ + "6154843866350342947362459504017878917650892054300443538745893356483702743994237/1250000000000000000000000000000000000000000000000000000000000000000000000000000", + "492387509308027435788996760321430313412071364344035483099671468518696219521711103/100000000000000000000000000000000000000000000000000000000000000000000000000000000" + ], + "trial": "1002040748181/250000000000000" + }, + "sites": 35, + "support": { + "aggregate_cases": 382, + "aggregate_recipients": 24, + "empty": 79, + "explicit": 512 + } +} diff --git a/research/bit-strict-prefix-envelope/SOURCES.json b/research/bit-strict-prefix-envelope/SOURCES.json new file mode 100644 index 0000000000..975c35da6e --- /dev/null +++ b/research/bit-strict-prefix-envelope/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/paired-query-only-bit/EFREE-RESULT.json", + "usage": "input", + "git_blob": "575f76487f9999ecc3e7b1b70f9f71bc582ef8a8", + "sha256": "a46b6c6040f75184cab5467656811ad988c216e3bc8e44d595a5015b6e49620b" + }, + { + "path": "research/paired-query-only-bit/independent/interval_gate.py", + "usage": "input", + "git_blob": "6d5a751dde7554b2bb3ccb9a958a3508d74ea155", + "sha256": "8dc2bc4c64cba3f83c664373984a075f1a14b4d53958084091345c8cab189dec" + }, + { + "path": "research/paired-query-only-bit/retained/inputs/BIT-NATIVE-WORD.json.gz", + "usage": "input", + "git_blob": "b718d6b2848215ad785022106dfa9f871a3d1c0c", + "sha256": "51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78" + } + ] +} diff --git a/research/bit-strict-prefix-envelope/TASK.json b/research/bit-strict-prefix-envelope/TASK.json new file mode 100644 index 0000000000..db0c5dbbbe --- /dev/null +++ b/research/bit-strict-prefix-envelope/TASK.json @@ -0,0 +1,77 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "bit-helper-contract", + "question": "Can a changed G20 helper path or independent-target split improve the complete BIT moment without losing its physical endpoint?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "research/g20-helper-split/README.md", + "research/g20-conjugation-admission/README.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient. 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_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "First read #5679/#5708 and their audits as pending component proposals. Choose one uncovered helper group/cut on an exact word; compare arbitrary-input native action, targets, owned storage, both orientations and full signed bill. Stop if the gain is only a scalar count or repaid by lost targets. Do not rerun the frozen #5609 common-frame domain without changing its hypothesis.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "G20", + "helper split", + "5679", + "5708", + "independent target" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Whole-prefix cached strict-subchart donors on the exact eight-port #7001 retag, all 35 adjusted deliveries.", + "scope_change_reason": "Test retained normalized support and the directed cost of the altered BIT path before a new physical helper is built.", + "bottleneck_link": "Saving the removed QUERY cannot fund this retag when every eligible cached strict-prefix donor has zero removable paid credit.", + "budget_minutes": 60, + "stop_rule": "Scan at most 512 nonempty strict charts, then test at most 35 recipient unions as an exact overgrant. Stop on an excluded directed price or retain pending cases.", + "outcome": "negative-result", + "evidence": "All 35 deliveries, 79 empty charts, 512 explicit chart duals, 382 cases discharged by 24 unions, exact recounted paid bill and directed price.", + "author": "ToikY", + "ai_assistance": "OpenAI Codex and subagents materially assisted the proof, implementation and independent replay.", + "open_questions": [ + { + "question": "Can an altered physical address action or a newly created cache lower the whole BIT price?", + "why_it_matters": "The certified exclusion uses rows that exist on the literal retag and one retained strict donor chart per receiver.", + "first_step": "Construct one explicit paid nonnested/oblique donor for the exact target row, charge its cache formation and restoration, and test the signed arbitrary-field action.", + "blocked_by": "A retained compatible source is unavailable in this envelope. Ownership, physical routing, precision/tape and the complete application must be proved for any changed route." + } + ] +} diff --git a/research/bit-strict-prefix-envelope/VERIFY.json b/research/bit-strict-prefix-envelope/VERIFY.json new file mode 100644 index 0000000000..b59e3ea6eb --- /dev/null +++ b/research/bit-strict-prefix-envelope/VERIFY.json @@ -0,0 +1,23 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/paired-query-only-bit/EFREE-RESULT.json", + "research/paired-query-only-bit/independent/interval_gate.py", + "research/paired-query-only-bit/retained/inputs/BIT-NATIVE-WORD.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Reconstruct the original and retag word and check all explicit and recipient-wide dual certificates, ownership, normalized endpoints and directed price." + } + ] +} diff --git a/research/bit-strict-prefix-envelope/retag.py b/research/bit-strict-prefix-envelope/retag.py new file mode 100644 index 0000000000..28ea7898d5 --- /dev/null +++ b/research/bit-strict-prefix-envelope/retag.py @@ -0,0 +1,67 @@ +"""The eight frozen #7001 backup retags from the Round 13 experiment.""" + +import copy + +def touched(event): + return event[1:3] if event[0] in ('ADD', 'SWAP') else event[1:2] + + +def modules(word): + program = word['program'] + selected = [] + edited_indices = set() + for start, (event, next_) in enumerate(zip(program, program[1:])): + if not (event[0] == 'INIT' and next_[0] == 'ADD' and event[1] == next_[1] + and next_[2] < 111 and event[2] == word['start'][next_[2]]): + continue + _, backup, source = event + port = next_[2] + body = start + 2 + while program[body][0] == 'MOVE' and program[body][2:] == [0, source]: + body += 1 + ingress = list(range(start + 2, body)) + roles = {port} | {program[i][1] for i in ingress} + assert len(roles) == len(ingress) + 1 + end_add = body + while program[end_add][0] == 'ADD' and program[end_add][3] == source and set(touched(program[end_add])) <= roles: + end_add += 1 + end = end_add + len(roles) + exits = list(range(end_add, end)) + assert {program[i][1] for i in exits} == roles + assert all(program[i][0] == 'MOVE' and program[i][2] == source for i in exits) + init, copied, late, clear = (i for i in range(start, len(program)) if backup in touched(program[i])) + assert (init, copied) == (start, start + 1) + consumer = program[late][1] + assert program[late - 1:late + 1] == [['MOVE', consumer, 0, source], ['ADD', consumer, backup, source]] + assert program[late + 1][:3] == ['MOVE', consumer, source] + assert program[clear] == ['CLEAR', backup, source] + changes = set(range(start, end)) | {late - 1, late, late + 1, clear} + assert not edited_indices & changes + edited_indices.update(changes) + selected.append({'port': port, 'backup': backup, 'source': source, 'init': start, + 'first_add': body, 'exits': exits, 'ingress': ingress, 'late_add': late, + 'late_consumer': consumer, 'clear': clear}) + if len(selected) == 8: + break + assert [m['port'] for m in selected] == [0, 1, 2, 3, 4, 5, 7, 8] + return selected + + +def retag(word, selected): + changed = copy.deepcopy(word) + program = changed['program'] + drop, adjusted = set(), {} + for m in selected: + port, start, late, clear = (m[k] for k in ('port', 'init', 'late_add', 'clear')) + changed['start'][port] = 0 + program[start][-1] = program[start + 1][-1] = program[clear][-1] = 0 + for j in range(m['first_add'], m['exits'][0]): + program[j][-1] = 0 + for j in (*m['exits'], late + 1): + program[j][2] = 0 + adjusted[j] = port + program[late][-1] = 0 + drop.update([*m['ingress'], late - 1]) + origin = [i for i in range(len(program)) if i not in drop] + changed['program'] = [program[i] for i in origin] + return changed, origin, adjusted, sorted(drop) diff --git a/research/bit-strict-prefix-envelope/verify.py b/research/bit-strict-prefix-envelope/verify.py new file mode 100644 index 0000000000..3e67a33688 --- /dev/null +++ b/research/bit-strict-prefix-envelope/verify.py @@ -0,0 +1,224 @@ +"""Check retained strict-prefix separation on the literal eight-port BIT retag.""" +from collections import Counter, defaultdict +from fractions import Fraction +import gzip +from hashlib import sha256 +from importlib.util import module_from_spec, spec_from_file_location +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +BIT = ROOT / "research/paired-query-only-bit" +PINS = { + "retained/inputs/BIT-NATIVE-WORD.json.gz": "51203e7fc75ba10bd3ac3f8e675759f47e13d262bea66b6600d1e515095cad78", + "EFREE-RESULT.json": "a46b6c6040f75184cab5467656811ad988c216e3bc8e44d595a5015b6e49620b", + "independent/interval_gate.py": "8dc2bc4c64cba3f83c664373984a075f1a14b4d53958084091345c8cab189dec", +} +TRIAL = Fraction("0.004008162992724") + + +def checked(path, expected): + raw = path.read_bytes() + if sha256(raw).hexdigest() != expected: + raise ValueError(f"SHA-256 mismatch: {path}") + return raw + + +def load(path): + spec = spec_from_file_location(path.stem, path) + module = module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def eliminate(rows): + pivots = {} + for vector in rows: + row = list(map(Fraction, vector)) + for pivot, previous in sorted(pivots.items()): + factor = row[pivot] + row = [a - factor * b for a, b in zip(row, previous, strict=True)] + pivot = next((i for i, x in enumerate(row) if x), None) + if pivot is not None: + pivots[pivot] = tuple(x / row[pivot] for x in row) + for pivot, row in sorted(pivots.items(), reverse=True): + for earlier in (i for i in pivots if i < pivot): + previous = pivots[earlier] + pivots[earlier] = tuple(a - previous[pivot] * b for a, b in zip(previous, row, strict=True)) + return tuple(row for _, row in sorted(pivots.items())) + + +def geometry(word): + frames = {} + ranks = {} + canonical = {} + names = {} + for f, entry in sorted((int(k), v) for k, v in word["frames"].items()): + head = eliminate(entry["B"]) + tail = eliminate(entry["A"]) + rank = entry["dim"] + assert len(head) == rank and len(tail) == 8 - rank + assert all(len(x) == 8 for x in head + tail) + assert all(sum(a * b for a, b in zip(x, y, strict=True)) == 0 for x in head for y in tail) + ranks[f], frames[f] = rank, (head, tail) + canonical[f] = names.setdefault(head, f) + return frames, ranks, canonical + + +def trace(word, origin, adjusted, frames, ranks, canonical): + public, owned = word["public"], word["owned_fields"] + charts = [*word["start"], *([None] * owned)] + rows = [*(1 << i for i in range(public)), *([0] * owned)] + cache = defaultdict(dict) + sites, pending = [], {} + paid, nesting = Counter(), {} + active = peak = erasures = 0 + + def observe(role, cut): + chart, row = charts[role], rows[role] + if chart is not None and row: + cache[canonical[chart]].setdefault(row, cut) + + for role in range(len(rows)): + observe(role, 0) + for cut, (old_event, event) in enumerate(zip(origin, word["program"], strict=True)): + op, role, *args = event + touched = event[1:3] if op in ("ADD", "SWAP") else event[1:2] + for owner in touched: + if owner in pending: + pending.pop(owner)["due"] = cut + if op == "ADD": + donor, chart = args + assert charts[role] == charts[donor] == chart + rows[role] ^= rows[donor] + elif op == "SWAP": + other, = args + charts[role], charts[other] = charts[other], charts[role] + rows[role], rows[other] = rows[other], rows[role] + observe(other, cut + 1) + elif op == "INIT": + assert role >= public and charts[role] is None and not rows[role] + charts[role] = args[0] + active += 1 + peak = max(peak, active) + elif op == "CLEAR": + assert role >= public and charts[role] == args[0] + charts[role], rows[role] = None, 0 + active -= 1 + erasures += 1 + else: + source, target = args + assert op == "MOVE" and charts[role] == source + smaller, larger = sorted(args, key=ranks.__getitem__) + if (smaller, larger) not in nesting: + nesting[smaller, larger] = all( + sum(a * b for a, b in zip(x, y, strict=True)) == 0 + for x in frames[smaller][0] for y in frames[larger][1]) + delta = ranks[larger] - ranks[smaller] + assert delta > 0 and nesting[smaller, larger] + paid[delta] += 1 + if old_event in adjusted: + assert source == 0 and rows[role] + site = {"event": old_event, "target_chart": canonical[target], + "target_row": rows[role], "due": len(origin)} + sites.append(site) + pending[role] = site + charts[role] = target + observe(role, cut + 1) + assert charts == [*word["final"], *([None] * owned)] and active == 0 + assert rows[:public] == [(1 << i) ^ ((1 << (i - 111)) if 111 <= i < 222 else 0) for i in range(public)] + assert (peak, erasures) == (237, 237) + return paid, sites, cache + + +def decode_duals(entries): + result = {} + for *ids, coordinates in entries: + key = tuple(ids) + assert key not in result + assert coordinates == sorted(set(coordinates)) and all(0 <= j < 659 for j in coordinates) + result[key] = sum(1 << j for j in coordinates) + return result + + +def separates(dual, target, rows): + return (dual & target).bit_count() % 2 == 1 and all((dual & row).bit_count() % 2 == 0 for row in rows) + + +def support_check(sites, cache, frames, ranks, canonical, certificate): + explicit = decode_duals(certificate["explicit"]) + aggregate = decode_duals(certificate["aggregate"]) + checked = Counter() + for site in sites: + event, target, due, target_row = (site[k] for k in ("event", "target_chart", "due", "target_row")) + for chart, rep in canonical.items(): + if chart != rep or not 0 < ranks[chart] < ranks[target]: + continue + if not all(sum(a * b for a, b in zip(x, y, strict=True)) == 0 + for x in frames[chart][0] for y in frames[target][1]): + continue + rows = [row for row, cut in cache[chart].items() if cut <= due] + if not rows: + checked["empty"] += 1 + continue + key = (event, chart) + if key in explicit: + dual = explicit.pop(key) + checked["explicit"] += 1 + else: + dual = aggregate[event,] + checked["aggregate_cases"] += 1 + checked[event] += 1 + if not separates(dual, target_row, rows): + raise ValueError(f"Invalid separator for event {event}, chart {chart}") + assert not explicit and set(aggregate) == {(event,) for event in checked if isinstance(event, int)} + assert {k: checked[k] for k in ("empty", "explicit", "aggregate_cases")} == { + "empty": 79, "explicit": 512, "aggregate_cases": 382} + assert len(aggregate) == 24 + return {"empty": 79, "explicit": 512, "aggregate_cases": 382, "aggregate_recipients": 24} + + +def price(gate, invoice, old, new): + assert old == {int(r): n for r, n in invoice["native_paid"].items()} + delta = {r: new[r] - old[r] for r in new.keys() | old.keys() if new[r] != old[r]} + assert delta == {1: -48, 2: 21, 3: -6, 4: 6, 6: -8, 7: 8} + paid = {int(r): n for r, n in invoice["paid"].items()} + targets = {int(r): n for r, n in invoice["targets"].items()} + raw_allowance = gate.add(gate.exact(111), gate.sub(gate.moment(targets, TRIAL), gate.moment(paid, TRIAL))) + cost = gate.moment(delta, TRIAL) + allowance = gate.div(raw_allowance, gate.exact(18)) + excess = gate.sub(cost, allowance) + assert excess[0] > 0 + return {"trial": str(TRIAL), "delta": delta, "cost": gate.show(cost), + "conditional_allowance": gate.show(allowance), "excess": gate.show(excess)} + + +def main(): + if not __debug__: + raise RuntimeError("Run with assertions enabled") + assert separates(4, 5, [1, 2]) and not separates(4, 5, [1, 2, 4]) + assert not separates(1, 2, [4]) + data = {k: checked(BIT / k, digest) for k, digest in PINS.items()} + word = json.loads(gzip.decompress(data["retained/inputs/BIT-NATIVE-WORD.json.gz"])) + invoice = json.loads(data["EFREE-RESULT.json"]) + gate = load(BIT / "independent/interval_gate.py") + rewrite = load(HERE / "retag.py") + certificate = json.loads((HERE / "CERT.json").read_text(encoding="utf-8")) + frames, ranks, canonical = geometry(word) + changed, origin, adjusted, _ = rewrite.retag(word, rewrite.modules(word)) + old_paid, _, _ = trace(word, range(len(word["program"])), {}, frames, ranks, canonical) + new_paid, sites, cache = trace(changed, origin, adjusted, frames, ranks, canonical) + assert len(sites) == len(adjusted) == 35 + assert next(row for row in sites if row["event"] == 19234)["target_row"] == (1 << 5) | (1 << 235) + support = support_check(sites, cache, frames, ranks, canonical, certificate) + receipt = {"support": support, "sites": 35, "available_strict_donor_credit": [0, 0], + "price": price(gate, invoice, old_paid, new_paid)} + expected = HERE / "RESULT.json" + assert json.loads(expected.read_text(encoding="utf-8")) == json.loads(json.dumps(receipt)) + print(json.dumps(receipt, sort_keys=True, indent=2)) + print("PASS_BIT_STRICT_PREFIX_ENVELOPE sites=35 explicit=512 aggregate=382 no_new_kappa") + + +if __name__ == "__main__": + main()