Repository navigation
Construct complementary B/C cancellation and prove a serial-consumer cost ceiling (no new κ) - #4848
Merged
Mister-Meeseeks merged 2 commits intoOct 23, 2026
Conversation
added 2 commits
October 23, 2026 08:46
Disable command-scoped auto maintenance and GC on disposable fixture commits. Add a real-Git Trace2 regression with forced automatic work and an unguarded foreground positive control. Fixes the cleanup failure observed in registered-package run 39860907480 for PR CrocSwap#4848. Developed with substantial OpenAI Codex assistance.
Mister-Meeseeks
pushed a commit
that referenced
this pull request
Oct 23, 2026
Disable command-scoped auto maintenance and GC on disposable fixture commits. Add a real-Git Trace2 regression with forced automatic work and an unguarded foreground positive control. Fixes the cleanup failure observed in registered-package run 39860907480 for PR #4848. Developed with substantial OpenAI Codex assistance.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Change and mathematical scope
An exact typed complementary B/C consumer works, but its complete recursive bill loses. A stronger written bound excludes every positive saving for the declared serial fixed-owner model. This is a scoped construction and ceiling contribution; no new kappa or selected-frontier change is claimed.
On the 56 matched exceptional pairs, execute C1, then B2, then Y-=2X, with a shared central Q and disjoint seven-axis blocks D1,D2:
The other 56 ordinary pairs require L(-2 Q^-1), hence 56 paid rank-one query children. Replacing that correction with a scalar shear is false. All 1,040 independent persistent inputs are retained: 224 main fields and two disjoint banks of 408 helpers. Main targets are 112 rank-14 and 112 rank-15 jobs. Every inherited helper is credited once. Complete paid rank mass is 9,579 versus target mass 9,403: deficit 176.
This specifies exact typed endpoints and actual gatewise raw inverse transpose under the audited supplier/owned-temporary interfaces. It does not freshly emit or phase-check a complete 1,040-field native trace. Physical witness, positive caller moment and funded compiler/outer transfer remain separate milestones.
For n>=2 whole calls on the same 224 main owners, one shared Q and n disjoint seven-axis blocks, with only the source helpers as additional productive fields and main target ranks at most 7n+1, the optimistic target-minus-paid moment satisfies:
Cleanup and finite work are granted free only for this rejection bound. At C=0 the upper bound is 224-112n-8n_B; two C calls only tie zero. The all-exponent proof normalizes the refreshed B/C direct-price gap and checks derivative bounds 1795/7 and 1857/7, then uses strict subadditivity. It is not an extrapolation from a tested point. Changed ownership, interleaved extra productive jobs, shared producer work or different geometry lie outside this ceiling.
Task and overlap
Task complex-new-helper-inventory, priority revision 7, explicitly changed to this donor-assigned complementary consumer study. Base/current main:
624de9dc66858af0945e5f8a0942488d62280d43. Scientific package head:890fadd4683ac206fa0c39ad58ff80932bdba26b. Current additive head:d5772576a9f260768d39eea0adde36e08602e889, two commits / 17 changed files: 16 new scientific package files plus the shared test-fixture repair independently submitted in #4857. Scientific bytes are identical between those heads.Exact predecessors: #4703
4cc96829fad977aecf0018b26beb067cfd2689a5; #4712b75a27bf07f1584b20babfddf887493981cd5949; #467484cf25a580db9ed2b4b1371c40689a035711364e. Five unchanged source snapshots retain Git blob IDs and SHA256 pins. #4712's existing native endpoint/phase/cost audit is inherited, not repeated. #4674's direct-price proof method is credited; the explicit pair and the refreshed C-profile serial bound are the changed scope. #4660's older autonomous-B/A-path and #4712's dirty-helper/120-head query models are different covered rejections. #4839 is the separate actual centre-chain terminal policy.Live targeted PR bodies, related heads and bounded Discussion windows were checked. The overlap helper could not refresh remote data because gh is unavailable; sparse local coverage and lack of exhaustive Discussion pagination remain explicit in OVERLAP.json. No exhaustive novelty or task-reservation claim is made.
Validation
Python 3.12.3, Linux, standard library only:
Registered replay, exact committed-byte/source-history preflight and a Git-free optimized export with PATH=/nonexistent pass. Actual source-byte and type-sensitive receipt corruptions reject. Mathematical controls reject the wrong exceptional coefficient, omitted ordinary Q^-1 correction and forward word substituted for raw dual.
A second agent independently rederived the derivative and universal-n proof, counted the paid/target profiles without importing this verifier, and checked a separate exact rational 2x2 fixture with non-involutive Q=-2/3. It confirmed the raw-dual order and rejected the ordinary scalar-only correction. Parent also read the proof/checker, recomputed the pair identity and reran optimized verification. These are automated/agent checks, not independent human or proof-kernel acceptance.
Not freshly run: the retained native phase suite, full physical caller, finite precision, fixed-tape compiler, Lean, outer admission or selected scientific cold replay. The initial hosted run failed before package replay because detached Git maintenance raced temporary sparse-fixture cleanup. Repair #4857 is included additively; run 39863812767 completed successfully at exact additive head: all 347 helper tests pass (11 expected skips), this scientific package replays successfully, and its committed-input mutation gate passes. Local exact-head registered replay and source-history checks pass. Scalar, movement, storage and precision bills remain separate finite obligations.
Credit
Chris R / Clear1nsight with substantial OpenAI Codex assistance, delegated construction and a separate agent proof/accounting check. Apache-2.0. Credit Dugongue #4703, Cao Yifan/intqwq #4610/#4712, Cinna Davis #4674 and controller lineage, zxv, Jacob Alan Sussman, DaysSky and all retained source notices. No independent human review is claimed.
Open next questions
See PROOF.md, README.md and TASK.json. Stop enlarging this serial consumer family. A useful successor must change ownership/incidence, share actual producer work, or improve the native paid profile enough to restore a discount. Begin with one actual cross-contact word and disjoint target census, then a favourable optimistic complete bill before implementation. Canonical result #4853 and the required handoff record the scope and next task.
Merge danger
Door: two-way. Blast radius: isolated research package plus a disposable-fixture test repair. No production helper, predecessor evidence or selected result changes.