Repository navigation
Prove P104 transport floor with arbitrary added storage - #2127
Merged
Mister-Meeseeks merged 1 commit intoOct 15, 2026
Merged
Conversation
This was referenced Oct 14, 2026
commdata2338
added a commit
to commdata2338/integer-mult-bounds
that referenced
this pull request
Oct 15, 2026
…acts Adds docs/research/p104-helper-lifetime-scope-map.md, a narrower successor to PR CrocSwap#2133's scope map. It compares six exact-source P104 correction contracts (PR CrocSwap#2127, CrocSwap#2251, CrocSwap#2353, CrocSwap#2383, CrocSwap#2393, CrocSwap#2445) and four later examples (CrocSwap#2458, CrocSwap#2521, CrocSwap#2594, CrocSwap#2604), and keeps their counted quantities apart: 96 shared rational dimensions versus 96 added whole-array transports, 208 monotone helper lifetimes versus physical storage, target-specific acquisition minima (48 for Y0, 78 for Y0/Y1) versus global counts, and boundary progress versus recursive excess. The six core registered replays pass at their pinned heads. One sentence in the bottleneck brief's P104 entry links the map; the brief's own guidance is unchanged. Navigation only: no new bound, supplier or kappa. Submitted by @commdata2338 with substantial AI assistance (OpenAI Codex research and implementation; packaged with Claude Code). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01X86sCSXdoDd61SDFfC1PKG
Mister-Meeseeks
pushed a commit
that referenced
this pull request
Oct 15, 2026
Machine-checks the chronological step behind the P104 transport floors of PR #2127 and #2148, as requested in PR #2163's handoff. In an inductive linear execution grammar (source-independent initialization; free same-side work, storage and return traffic; one D-valued message per counted receive), every target-side state factors through a transcript of n whole arrays, so its source dependence has rank at most n*dim D and recovering m independent arrays needs m <= n. The 96-transport and 48-rank floors follow as conditional corollaries. Lean 4.21.0 with pinned Mathlib: 13 theorem roots audited to the standard axioms only, 8 rejected formal controls. A Python binder reconstructs the PR #1972 witness and regenerates SourceCut.lean's finite facts, which the kernel checks by decide. The native-event-to-model translation stays written; no supplier or kappa change. Adds research/lean-transport-cut/ and its path-filtered workflow .github/workflows/lean-transport-cut.yml. Submitted by @commdata2338 with substantial AI assistance (OpenAI Codex research and implementation; packaged with Claude Code). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01X86sCSXdoDd61SDFfC1PKG
Mister-Meeseeks
pushed a commit
that referenced
this pull request
Oct 15, 2026
Code-disjoint check of the finite premises behind #2082, #2090, #2113 and #2127 (and the budget line summarized in #2133), from the hash-pinned PR1972 witness only. Every checked premise reproduces exactly: - frozen chronology: max-flow = min vertex cut = 8, certified by weak duality (feasible flow plus separating cut); extremal min cuts are Q7..Q0 (cuts 1570-1597) and C#0..C#7 after their descents (2464-2524); the #2090 query cut and cones at cut 2429 reproduce; - union graph: the eight private descents separate; each reopens 52; - frame graph: 222/222 over 444 frames; - exact replay: rank 8, M^2 = 13M, (I-M)(I-M/12) = I, minor 1/256; - budget-line constants re-derived from the witness (328/9 slack). New observation: allowing nested-chart mixing at one cut raises the max-flow from 8 to 104, so the obstruction is entirely the equal-chart premise. No new kappa, supplier or selected-frontier change. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A2DF8QgsTwrE4t3793qQUx
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
2 participants
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.
The P104 side correction still needs at least 96 additional whole-array transports when arbitrary source-independent workspace lifetimes and arbitrary valid retiming are allowed, provided the original transport occurrences are retained and every cross-frame information transfer is counted.
This extends Jeremy Diviney's PR2113 static-lifetime/retiming cut and David Arias's PR2082 local-excursion floor. Two independently implemented graph checkers collapse every occurrence of the same canonical frame, including separate private lifetimes: all 444 frames partition into 222 source-reachable and 222 target-coreachable frames after removing the same eight original descents. The written factorization proof covers every finite linear program in the stated added-storage model; the certificate checks its exact finite premise.
Additional transport count is not automatically excess recursive cost. The package includes a concrete monotone helper path illustrating productive endpoint progress. The inherited
M(0) >= 7659/7592 > 1comparison is explicitly conditional on unchanged old idle requirements and no new creditable progress. Replacement/fusion of original transports, free cross-chart operations and a changed coverage contract remain outside this result. No attaining correction, admitted supplier or new kappa is claimed.Only
research/p104-storage-cut/is added. The README contains the model/proof, cost boundary, predecessor credit and next questions; task/source metadata pins the exact base and inputs;RESULT.jsoncontains the complete partition. The scientific base is0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2, priority revision 4. Contribution commit:befebf0f4ae7a3f69fe9c5e136262559dcac125f. Submission overlap covered 381 open PRs and 789 Discussion records with complete pagination and no warnings, 20:09-20:11 UTC; text matching is not a novelty guarantee. Canonical discussion: #2123.Validation on CPython 3.12.12:
-O, including actual separation-guard removal, count-preserving partition corruption, equivalent bases, missing/corrupt source and receipt, exclusive output, and read-only source-export replay.Reproduce:
No fresh full 280-column scalar identity, native Clifford/phase replay, global owner construction, precision/all-size/outer proof or selected cold replay was run. The frozen native channel is inherited. Hosted CI is separate from these local checks.
Credit Jeremy Diviney/PR2113, David Arias/PR2082, Adam Gall/PR2090/2083/1940, Rohan Arun/PR1972, Chafik Boukhalfa/PR1991 and the geometry/coverage lineage detailed in the README. Discussion2121's replacement joint-side producer remains outside this retained-occurrence theorem. Prepared for Ross Richardson with substantial OpenAI Codex assistance in mathematics, implementation, verification and prose; Apache-2.0.