Prove the BIT COPY floor for closed snapshot paths

research/bit-copy-path/NOTICE.md

@@ -0,0 +1,10 @@
+# Notice
+
+Prepared for Ross Richardson with substantial OpenAI Codex assistance in
+mathematical derivation, implementation, exact checks, and independent
+agent review. No human or formal-kernel review is claimed.
+
+This research contribution is provided under the repository's Apache-2.0
+license. Preserved source excerpts retain their original authorship and
+provenance; see `RELATED-WORK.md`, `PREDECESSOR.json`, and the component
+source manifests.

research/bit-copy-path/PREDECESSOR.json

@@ -0,0 +1,55 @@
+{
+  "commit": "b4ec15cbdb017776c04b0bf369a807f2278113cd",
+  "files": {
+    "WORD.json.gz": {
+      "source": "/Users/ross/git/math/.research-automation/runs/bit-full-caller-20261020T1028Z/release/bit-full-caller/inputs/consumer/inputs/retained/boundary/inputs/WORD.json.gz",
+      "old_relative": "inputs/consumer/inputs/retained/boundary/inputs/WORD.json.gz",
+      "sha256": "c46ccd7d3eedabc6a7efbb1a91ec13f2928bad8ee0bac57c6e593a092d13d96c"
+    },
+    "GEOMETRY.json.gz": {
+      "source": "/Users/ross/git/math/.research-automation/runs/bit-full-caller-20261020T1028Z/release/bit-full-caller/inputs/consumer/inputs/retained/boundary/inputs/GEOMETRY.json.gz",
+      "old_relative": "inputs/consumer/inputs/retained/boundary/inputs/GEOMETRY.json.gz",
+      "sha256": "a353999bceac4ac957f540adfd3e5f8768297138b27132eeb83332e2ea4b1022"
+    },
+    "TERMINAL-CHARTS.json": {
+      "source": "/Users/ross/git/math/.research-automation/runs/bit-full-caller-20261020T1028Z/release/bit-full-caller/inputs/consumer/inputs/retained/boundary/inputs/TERMINAL-CHARTS.json",
+      "old_relative": "inputs/consumer/inputs/retained/boundary/inputs/TERMINAL-CHARTS.json",
+      "sha256": "489216ea25f47f061675ab7b7e4a17289a531bce6fe77cca166a13265bfcbb17"
+    },
+    "global_k.py.txt": {
+      "source": "/Users/ross/git/math/.research-automation/runs/bit-full-caller-20261020T1028Z/release/bit-full-caller/inputs/consumer/inputs/retained/source-context/global_k.py",
+      "old_relative": "inputs/consumer/inputs/retained/source-context/global_k.py",
+      "sha256": "6368196a393ac25bb2918880e4c4bd31ed733b762c27b6873ab391cbc0c5c3c8"
+    },
+    "FULL-CALLER-PROOF.md": {
+      "source": "/Users/ross/git/math/.research-automation/runs/bit-full-caller-20261020T1028Z/release/bit-full-caller/bounds/PROOF.md",
+      "old_relative": "bounds/PROOF.md",
+      "sha256": "ebdd9283a7762e01f84ee9dde8885d4ba05cc6c93a4430296ff0a71ea7205832"
+    },
+    "FULL-CALLER-README.md": {
+      "source": "/Users/ross/git/math/.research-automation/runs/bit-full-caller-20261020T1028Z/release/bit-full-caller/README.md",
+      "old_relative": "README.md",
+      "sha256": "d8ea32275410a0fc13e3e1a67f3dba134679a67912b4ffc893b88b2ced967823"
+    },
+    "full-check-screens.py.txt": {
+      "source": "/Users/ross/git/math/.research-automation/runs/bit-full-caller-20261020T1028Z/release/bit-full-caller/bounds/check_screens.py",
+      "old_relative": "bounds/check_screens.py",
+      "sha256": "c07d15a1e5edcbbab584fd77b26c2e6787c2baa4ef013de72dbfd52f5d2960e6"
+    },
+    "full-exact-interval.py.txt": {
+      "source": "/Users/ross/git/math/.research-automation/runs/bit-full-caller-20261020T1028Z/release/bit-full-caller/bounds/exact_interval.py",
+      "old_relative": "bounds/exact_interval.py",
+      "sha256": "d8a78c2a2f87a5cf9fff0367d70f21dcdb712a509ba365879aee134b18c4c25d"
+    },
+    "full-schedule-witness.json": {
+      "source": "/Users/ross/git/math/.research-automation/runs/bit-full-caller-20261020T1028Z/release/bit-full-caller/schedule/WITNESS.json",
+      "old_relative": "schedule/WITNESS.json",
+      "sha256": "8420b5c57fd033f05675c7a1d72a1ba1a07c19542042698028b300019295a94b"
+    },
+    "full-invoices.json": {
+      "source": "/Users/ross/git/math/.research-automation/runs/bit-full-caller-20261020T1028Z/release/bit-full-caller/bounds/INVOICES.json",
+      "old_relative": "bounds/INVOICES.json",
+      "sha256": "d0877305ca03e88622586fd76622fc9e2e2da0484de3b112577467c82f386a92"
+    }
+  }
+}

research/bit-copy-path/README.md

@@ -0,0 +1,173 @@
+# The BIT COPY floor for closed snapshot paths
+
+**Scoped obstruction and complete planning budgets; no new supplier or κ.**
+
+This investigation changes the proposed query word, rather than applying the
+preceding fixed-word allocation ceiling to a different construction. It finds
+a stronger obstruction to replacing one of the nine actual centre copies.
+It also tests the existing 429-helper coded word in the actual recursive
+caller. Neither route supplies a κ improvement.
+
+## Main result: closed snapshot paths cannot cheapen a centre COPY
+
+Each retained centre has a seven-dimensional frame \(F_j\). Its required
+scatter column \(k_j\), reconstructed from the literal R438 word, reaches
+port roots spanning all eight dimensions.
+
+Allow any finite number of independent copies of the **same unchanged
+centre total**. Copy \(i\) may start in any subframe of \(F_j\), costing
+\(r_i\), and follow an arbitrary closed path of nested private frame moves,
+costing \(m_i\) in both directions. It may add into any compatible public
+register during the continuation after the last original COPY. Public
+frames remain monotone and the continuation contains no further COPY.
+Scalar additions, legal public retiming, and other cleanup are granted free
+for this necessary bound. The private copies must be restored for their
+guarded ERASEs.
+
+The written geometric argument proves
+
+\[
+   \sum_i\left(r_i+\frac{m_i}{2}\right)\geq 7.
+\]
+
+Consequently the replacement cannot reduce either the total paid query rank or
+its recursive moment
+\(\sum_\ell 64^\beta r_\ell^{\,1-\beta}\), for \(0\leq\beta<1\).
+For a single copy of rank \(r<7\), the complete rank cost is at least
+\(14-r\geq8\).
+
+This includes moving the private copy outside the original centre frame.
+For example, a rank-one COPY followed by a rank-one promotion and its
+rank-one inverse is a valid local transport costing three. It still cannot
+deliver the complete actual scatter column. A private slot starts and ends
+zero; no arbitrary private dirt is discarded.
+
+See [the proof](construction/PROOF.md) and
+[independent review](independent/REVIEW.md). The argument quantifies over
+the stated continuous frame class; its application to these nine centres
+uses exact finite source and rational/real geometry checks. It is not a formal-kernel
+proof, or a bound on mixtures of different totals, changed public queries,
+or a rebuilt factory.
+
+## Earlier cuts and the recoded caller
+
+Two finite screens test ways around the late-continuation premise.
+
+- Source acquisitions at all existing common-frame cuts in the actual
+  factory cannot replace any deleted centre scatter. Even relaxing the
+  five partial-helper terminal conditions leaves exact binary separators.
+- Copying each completed centre earlier at **COPY rank at most four**,
+  before the remaining centre copies, fails across all **254** eligible
+  cuts. The screen includes the
+  unchanged downstream COPYs and allows an arbitrary real intermediate
+  frame separately for each receiver. It does not cover a changed
+  incomplete total or a changed factory graph.
+
+The existing R429 source-code construction has a real local saving, but
+its unmodified substitution into the nine-stage caller fails. The complete
+888-column scalar defect has rank 63. An integral ADDRESS impulse in the
+last pair produces a nonzero TAIL component that no invertible terminal
+decoder made solely of scalar mixing and separate HEAD/TAIL routes can
+erase. Restoring the scalar source code locally does not remove the
+mismatch between successive fresh blocks.
+
+[The caller proof](composition/PROOF.md) binds this failure to the actual
+order-28 code and native charts. Its priced repair floors cover two
+specified interfaces: a minimum nine-reader common-cap repair costs at
+least 63 rank units per local call; the previous one-snapshot-per-repaired-row
+interface needs all 111 rows. Shared or differently routed repairs remain
+outside those floors.
+
+[The private-transport and wrapper appendix](composition/PRIVATE-MOVE-PROOF.md)
+also prices an explicit correction around each coded call. Cancelling and
+commuting its full-bank sweeps, while keeping both the calls and individual
+code factors in their fixed chronological order, leaves at least nine
+sweeps: 999 rank-one requests. That exceeds the allowance below 526 per
+nine-call block. Reordering code factors or replacing these sweeps by other
+routed queries is outside this particular cancellation argument.
+
+## Complete budget consequence
+
+The comparison uses the existing \(m=64\), \(W=28416\), 288-call controller
+and includes returned helper-owner obligations and the inherited child
+surcharge. The target is the necessary BIT endpoint for a 10% gain over
+the selected κ, under the retained outer relation:
+
+\[
+ c_*=\frac{9199631083923049}{4990800368916076951}.
+\]
+
+| Proposal | Remaining allowance at \(c_*\) |
+|---|---:|
+| Delete one COPY7 in every local call | Less than 4.978 tariff units per call for its replacement |
+| Use the existing coded R429 word | Less than 58.383 per call for all added repair children |
+
+The second row returns all 72 owner rank units per call from the nine
+deleted helpers. Its complete rank saving before decoding is 60 per call.
+These are planning allowances under the declared owner relaxation, not
+constructed chronological schedules.
+
+The historical P111 label-decoder mass floor of 63 is **prior work**.
+Even granting the most favorable direct-reader histogram consistent with
+that floor, \(4e_6+e_7+4e_8\), the complete optimistic BIT endpoint is below
+`0.001743442083496`. Under the retained outer relation its possible gain
+over the selected κ is below **4.050289853587%**. This consequence applies
+only to that direct-reader class. It is not a global upper bound on BIT
+algorithms.
+
+[The budget proof](bounds/PROOF.md) and
+[exact receipt](bounds/BUDGET.json) give rational intervals, the complete
+histograms, and adjacent rejection/pass tests. A separate positive-binomial
+calculation checks the numerical signs. The selected complex endpoint
+remains binding, so a BIT-only saving would not by itself change the
+selected κ.
+
+## Reproduce
+
+The package is self-contained and uses only the CPython standard library.
+From a checkout or a Git-free export:
+
+```sh
+python3.12 -I -B research/bit-copy-path/verify.py --output /tmp/bit-copy-path-check.json
+```
+
+The runner authenticates every packaged source, runs the declared checks
+in ordinary and optimized Python modes, compares their exact receipts,
+and writes all logs and generated evidence outside the package. See
+[REPLAY.json](REPLAY.json) for the command inventory. It does not reexecute
+the predecessor's complete historical suite.
+The [validation record](VALIDATION.md) separates the retained mathematical
+replays, publication review and hosted CI.
+
+## Open next questions
+
+A successful construction must change something excluded by the proved
+class: the queried totals, their factory or public query events, the
+restoration contract, or a shared routed caller repair. It must emit the
+complete arbitrary-input word and pay its native queries, helpers,
+chronological owners, rounding, storage, and outer costs. Merely moving
+the same completed snapshot later, or treating a source code as a free
+terminal decoder, does not meet those requirements.
+
+Two concrete questions remain:
+
+- **Can different queried totals share a paid path?** This changes the
+  unchanged-total premise of the theorem. Start with one complete changed
+  factory/query word, check every dirty-input column and restoration, and
+  price its full child histogram and returned helper owners. The blocker is
+  the absence of a favorable literal candidate.
+- **Can a shared routed correction repair the coded caller cheaply?** This
+  lies outside the direct-reader and fixed-order wrapper bounds. Start with
+  one complete nine-call operator correction, charging every native query
+  and source observation against the stated repair allowance. The blocker
+  is the absence of a complete legal correction; scalar endpoint agreement
+  alone does not establish native caller compatibility.
+
+The source and attribution record is in [RELATED-WORK.md](RELATED-WORK.md),
+[PREDECESSOR.json](PREDECESSOR.json), and [SOURCES.json](SOURCES.json).
+The changed word is not installed as a physical supplier. Selected
+certificates are unchanged. Local verification is distinct from hosted CI,
+human review, formal proof, and the full multiplication theorem.
+
+Apache-2.0. Prepared for Ross Richardson with substantial OpenAI Codex
+assistance, including separate construction and independent review agents.

research/bit-copy-path/RELATED-WORK.md

@@ -0,0 +1,119 @@
+# Source attribution and the new scope
+
+The checkout base is `12fa8c5c844be21bfefb38a19503fbd867a11244`,
+with research priority revision 7. This package continues the local
+full-caller investigation at
+`b4ec15cbdb017776c04b0bf369a807f2278113cd`. The exact ten-file dependency
+slice is pinned in `PREDECESSOR.json`; the predecessor's full suite is
+not claimed as freshly rerun here.
+
+## Preserved construction and caller premises
+
+- DreamingOfClouds's PR589 supplier and PR446 Theorem C supply the underlying
+  BIT word and COPY pricing model. The R438 transport, five partial rank-four
+  terminals, and their independent geometry checks are retained source
+  constructions, not discoveries here. Their word and geometry bytes are
+  copied without alteration. Credit Ali Romman's R438/PR1043 construction
+  and boundary-persistence work, Sagar Thakrar's transport/rehosting work,
+  and the DreamingOfClouds/eumemic/PR589/PR555 lineage retained by those sources.
+- Ross Richardson's [PR3645](https://github.com/CrocSwap/integer-mult-bounds/pull/3645),
+  `research/bit-r438-source-code`, supplies the existing
+  three-pivot repair and 429-helper source-code word. Its scientific source
+  pin is `20ecf2891d80b5acf18d980b2164fb44ea7faa90`. The local 132-unit
+  saving and 72-unit owner return were already established there.
+- The C511 mutable-source boundary package already distinguishes scalar
+  closure from physical native closure, and includes the actual order-28
+  R429 code and the failed fresh-chart alignment. The frozen source
+  references and full E8 geometry are in `composition/inputs`. No
+  order-511 conclusion is transferred to the order-28 code.
+- The preceding local full-caller package supplies the complete controller,
+  ordinary owner inventory, allocation proof, and existing chronological
+  comparator. Its fixed-word ceiling is not applied to a changed local
+  histogram.
+
+The present caller contribution is the actual nine-stage last-pair impulse,
+the all-column endpoint audit, and the explicitly bounded paid repair
+screens. The general warning about physical noncommutation is prior work.
+
+## Closest later interface and budget results
+
+The publication overlap check also inspected Ross Richardson's
+[PR4033](https://github.com/CrocSwap/integer-mult-bounds/pull/4033),
+[PR4039](https://github.com/CrocSwap/integer-mult-bounds/pull/4039),
+[PR4051](https://github.com/CrocSwap/integer-mult-bounds/pull/4051), and
+[PR4054](https://github.com/CrocSwap/integer-mult-bounds/pull/4054). They cover,
+respectively, binary cold-factor/separate-reader floors, a FULL-target
+interface and its caller invoice, the older C511 mutable-source interface,
+and kernel encoding at actual native cuts. Their premises and results are
+retained. The present main theorem instead fixes one actual completed total
+and allows arbitrarily many independent snapshots with paid closed private
+frame walks through the monotone continuation. None of those earlier interface
+results is claimed as new here.
+
+Sagar Thakrar's
+[PR3948](https://github.com/CrocSwap/integer-mult-bounds/pull/3948) prices
+target-scale centre-sharing and BIT levers against the selected PR589
+invoice. The present planning comparisons use the explicitly reconstructed
+R438/five-partial-terminal inventory and the predecessor's fractional
+owner relaxation, or the separately stated full-helper coded inventory.
+Their numerical thresholds belong to those different inventories and
+relaxations; they do not correct or replace PR3948's fixed-invoice result.
+Both analyses leave the selected complex supplier binding and establish
+no new κ.
+
+## Prior direct-decoder floor
+
+Russell Seligmann's [PR757](https://github.com/CrocSwap/integer-mult-bounds/pull/757)
+(head `e2ec7d7`) and Cody Harris's
+[PR761](https://github.com/CrocSwap/integer-mult-bounds/pull/761)
+(head `2877587`) established the P111 label-decoder floor of 63.
+Joel Pulikkan / GamingPuzzled's
+[PR620](https://github.com/CrocSwap/integer-mult-bounds/pull/620)
+identified the pairing model and orthogonal-pair opportunities.
+`research/bit-orthogonal-pair-decoders` records these premises, the
+arbitrary-term floor, other punctures, and the excluded off-pattern class.
+Its README is frozen in `bounds/inputs/DIRECT-FLOOR-PRIOR-README.md`.
+
+The present finite support and basis calculations rebind that floor to
+the actual local word. They are a reproduction, not a new decoder-optimality
+claim. The new budget consequence is the complete best-histogram
+comparison, including returned owners, exact child moments, and its
+restricted endpoint ceiling.
+
+## Actual query changes tested here
+
+The main new written argument concerns immutable same-total snapshots
+following closed private frame paths during a monotone public
+continuation. It does not assume one catalogue frame or one private copy.
+Exact rank-eight target supports and rank-seven projected supports bind
+the argument to all nine actual retained totals.
+
+The source-acquisition and completed-centre factory-cut screens are
+different finite classes. Their exact separators include the actual
+downstream scalar dependencies and COPY events. They do not establish
+impossibility for altered incomplete totals or a rebuilt factory.
+
+The entry overlap refresh read all 308 open PRs, 2703 discussion records,
+and 5234 local records, with no pagination warnings, as well as discussion
+hubs 1163, 1166 and 1167. This is an overlap search, not a novelty proof:
+it is not a census of closed remote PRs or every code diff. No public
+research claim, discussion post, or PR was made during that original
+local-only investigation.
+
+Before publication, a fresh snapshot on 2026-10-20 covered 314 open PRs,
+3540 closed/merged PRs, 2713 discussion records and 5234 local records.
+All three remote corpora reported complete pagination and no warnings.
+The search included titles, bodies, discussion replies and local package
+metadata; it did not inspect every code diff or establish global novelty.
+The canonical discussion and submission record are linked from the PR.
+
+## Evidence boundaries
+
+The finite independent implementation uses separate binary state and
+rational arithmetic code. The continuous frame result is a written
+linear-algebra proof checked by separate agents, not a formal-kernel
+certificate or independent human review. There is no new physical
+compiler, rounded supplier admission, whole-owner construction, or joint
+κ claim.
+
+Apache-2.0. Substantial OpenAI Codex assistance.