Finite BIT construction: R438 source boundary with full hosted invoice

research/bit-boundary-persistence/NOTICE.md

@@ -0,0 +1,28 @@
+# Notice
+
+New material is prepared for Ali Romman (@aliromman), with substantial
+OpenAI Codex assistance. It is supplied under Apache-2.0, the repository
+license. No independent human review is implied.
+
+The candidate starts from DreamingOfClouds's PR589 tuning of eumemic's PR555
+punctured word. The construction retains eumemic's PR543 L3 skeleton and
+interleaved scalar interface, DreamingOfClouds's PR545 punctured-star geometry,
+and the prior work identified in their source notices.
+
+The native exporter and legality checks come from Dylan Crow's PR370 lineage.
+The multi-stage column checker comes from DaysSky's PR381. The parent and
+pricing engines come from DreamingOfClouds's PR463/510 and PR315 lineage.
+Whole-residual idle hosting comes from DaysSky's PR442, with the owner and
+replica checks from chafreaky's PR443/472 lineage. The scalar interface also
+uses Zhihao Chen's PR425 work. Jacob Sussman introduced the E8 unit.
+
+These tools are used from the two unchanged packages pinned in `SOURCES.json`.
+Their source notices and licenses remain in those packages. The new builder
+and independent record replay were written for this candidate. The new driver
+uses the existing adapters and their existing supported parameters; it does
+not change the pinned exporters, checkers or pricing engines.
+
+Source inlining and early helper retirement are prior ideas. The related
+PR429/515 and PR433/437 work is acknowledged. PR953, PR980, PR997, PR1001 and PR1015
+were checked for overlap. This package claims one verified boundary and its
+complete hosted invoice, not priority for a general circuit method.

research/bit-boundary-persistence/PROOF.md

@@ -0,0 +1,185 @@
+# Source boundary and complete cost
+
+All gate indices and original register identifiers below are zero-based.
+The object is the exact PR589 word pinned in `SOURCES.json`.
+
+## 1. The legal late read
+
+Let `x` be source77, `q` helper470, and `r` receiver444. In A, the only two
+uses of q are:
+
+```text
+A[230]  at frame79: q += x
+A[1993] at frame79: r += q
+```
+
+There is no B use of q. The copied totals do not include q. Before the second
+operation, exact replay on all independent initial columns gives
+`x = x_in` and `q = q_in + x_in` over F2. In particular, a borrowed helper is
+not treated as initially zero.
+
+Source77 begins at frame79, the line `[77]`. A[426] reads it at frame186,
+whose lines are `[33,77]` and whose rational dimension is two. Receiver444
+is still at frame0 before A[1993]. Its next gate is A[1994] at frame509,
+which contains frame186 and has dimension four. The next source77 read is
+B[35] at frame186. Thus the new gate
+
+```text
+at frame186: r += x
+```
+
+has valid entry frames, common-frame operands, and valid next frames for both
+operands. The original frame79 read of x at this time would be a descent
+from frame186 and is invalid. The new gate does not move x early.
+
+Delete A[230], replace A[1993] as above, and remove q from the physical stock.
+Subtract one from every old identifier greater than 470. Keep the E8 geometry,
+all other A gates, B, scatter and all copied totals, subject to that renaming.
+
+The rational frame check and the native legality checker give these paths:
+
+| Old register | Old path | New path |
+|---|---|---|
+| 77 | `[79,186,509,386,560,1]` | same |
+| 444 | `[0,79,509,392,513,1]` | `[0,186,509,392,513,1]` |
+| 470 | `[0,79,1]` | removed |
+
+Every other surviving register path is equal under the renaming. The complete
+lists are in `FRAME-PATHS.json`. All 636 original frames remain in the catalogue.
+
+## 2. Dirty state and literal restoration
+
+The removed read used to add both `x_in` and `q_in` to r. The new read adds
+`x_in`. Thus deletion changes a dirty-helper column; it is not a free scalar
+substitution inside the old compensated word.
+
+Rebuild D from the exact map of A, scatter and B. D contains only frame-zero
+helper-to-target operations. In this case the rebuilt D is exactly the old D
+with its 55 q operands deleted and all other identifiers renamed. It changes
+from 18,085 to 18,030 scalar ADDs. Every remaining helper contribution is paid.
+
+Rebuild C as the literal reversed list of all A/B operations that write a
+source or helper, at the full frame. Reuse of the old C would not restore the
+changed basis. C has 2,573 gates instead of 2,574. The original interleaved
+checker verifies H1-H5 and the conclusions `U_block_form`, `J_identity`,
+`C_is_U_inverse`, and `K_equals_D` on the changed word.
+
+The complete order is D, A, nine COPY/scatter/ERASE episodes, B, C, then all
+required final MOVEs. Exact F2 replay returns every source and helper to its
+initial value and maps each target `y_i` to `y_i + x_i` for every dirty column.
+The source checker also verifies the punctured-line geometry and rank-seven
+copied totals. No decoder change is used.
+
+Removing A[230] and its C inverse saves two ADDs. The compensation change saves
+55 more. The total is 57. The independent literal emitter and the unchanged
+native exporter produce the same record list for each complete word.
+
+The signed native inverse uses negated ADDs and the original unchanged center
+for reverse COPY/ERASE blocks. The existing native checkers and parent checker
+replay this inverse. The cancellation-free forward and reverse bounds remain
+49,347 and 1,113,070. Their charged precision bounds remain 93 local bits and
+177 nine-stage bits, within the inherited 104/192 allowances.
+
+## 3. Local recursive charges
+
+Deletion of q removes rank-one and rank-seven MOVEs. Moving r first to the
+rank-two frame changes its first two increments from `(1,3)` to `(2,2)`.
+No other path changes. Therefore the exact profile difference is
+
+```text
+rank 1: -2; rank 2: +2; rank 3: -1; rank 7: -1.
+```
+
+The complete profiles are:
+
+| Child rank | R439 | R438 |
+|---|---:|---:|
+| 1 | 1323 | 1321 |
+| 2 | 1342 | 1344 |
+| 3 | 79 | 78 |
+| 4 | 44 | 44 |
+| 5 | 102 | 102 |
+| 6 | 11 | 11 |
+| 7 | 19 | 18 |
+
+The paid rank mass falls from 5,129 to 5,121. It still satisfies
+`8R + 63 + 14v`, with `R=438` and `v=111`. Each local call saves two children.
+This local result alone is insufficient: the removed helper occupied an idle
+window, whose remaining child must grow.
+
+## 4. Hosting and returned idle rank
+
+Use the same nine-stage parent, four DATA pairs and 32 replicas. Expand the
+original frozen hosting plan. For each stage remove the width-eight slot for
+old helper index `470 - 222 = 248`. Group the remaining widths by idle window
+and copy, rebuild the integer pattern counts, and run the original deterministic
+expander for R438. No search or objective improvement is used.
+
+These are the nine deleted slots per replica. The last column is the old
+idle remainder before the eight units are returned.
+
+| Idle window | DATA copy | Offset | Stage | Old remainder |
+|---|---:|---:|---:|---:|
+| 2 | 82 | 16 | 0 | 4 |
+| 2 | 155 | 0 | 1 | 4 |
+| 4 | 47 | 24 | 2 | 2 |
+| 4 | 135 | 16 | 4 | 2 |
+| 4 | 185 | 32 | 5 | 2 |
+| 6 | 49 | 24 | 3 | 2 |
+| 6 | 174 | 32 | 7 | 2 |
+| 7 | 86 | 0 | 6 | 4 |
+| 8 | 31 | 0 | 8 | 6 |
+
+The expander can rename or reorder retained helper placements when it groups
+patterns. The emitted candidate, rather than the old placement names, is the
+object of the full hosting audit. That audit checks all 126,144 residual roles,
+actual source-owner windows, disjoint offsets, call orientation and restoration.
+There are no banks. Live DATA and physical stock do not increase.
+
+Per replica, the old remainder histogram is
+`{2:435, 4:444, 6:444, 7:666, 42:9}`. The new histogram is
+`{2:430, 4:441, 6:443, 7:666, 10:5, 12:3, 14:1, 42:9}`.
+The new idle children carry exactly 72 more rank units per replica. Across
+32 replicas this returns all 2,304 units removed by the 288 local words.
+The complete hosted rank mass is therefore unchanged at 1,808,352.
+
+The final paid child profile is:
+
+```text
+{1:380448, 2:400832, 3:22464, 4:26784, 5:29376,
+ 6:17344, 7:26496, 10:160, 12:96, 14:32, 42:288}
+```
+
+It contains 904,320 children, including idle remainders, instead of 904,896.
+The deficit remains `64*28416 - 1808352 = 10272`. The maximum child is 42.
+The two-level condition remains `2*42^2 = 3528 < 4096 = 64^2`.
+
+## 5. Exact supplier invoice
+
+The unchanged inherited invoice charges the emitted ADDs, bridges, COPY/ERASE
+operations, selectors, data access, restored helper stock, every recursive
+child, and the signed prefix bound. Its precision fields are:
+
+```text
+prefix:                 177 bits, charged 192
+coefficient:            177 bits
+two-level coefficient:  393 bits, charged 512
+row coefficient:        18355
+```
+
+Two independent exact moment engines accept
+
+```text
+c = 433544072119966441673 / 250000000000000000000000
+```
+
+and reject the next `10^-24` grid point
+
+```text
+1734176288479865766693 / 1000000000000000000000000.
+```
+
+These checks use the complete profile above and the inherited surcharge. They
+do not infer a supplier gain from the local ADD reduction. The smaller selected
+complex value still binds. The full-theorem assumptions listed in the README
+remain open; this is a finite conditional supplier construction.

research/bit-boundary-persistence/README.md

@@ -0,0 +1,127 @@
+# R438 bit supplier from a legal source boundary
+
+This finite construction removes one helper from the selected PR589 R439 bit
+word. At one late read, source77 is still unchanged and is available at
+frame186. Receiver444 can enter that frame before its next operation.
+The word reads source77 directly, removes helper470, and rebuilds the literal
+cleanup and dirty-target compensation.
+
+The complete nine-stage hosted invoice improves bit `c` from
+`0.001733427039589844234749` to **`0.001734176288479865766692`**.
+This package does not claim a new kappa. The selected PR942 complex value
+`0.001664727258740678855772` is smaller than both bit values. The selected
+conditional kappa remains `0.001661960547713947` at the research base.
+
+| Complete charge | PR589 R439 | This R438 word |
+|---|---:|---:|
+| Local helper registers | 439 | 438 |
+| Local native ADDs, including D and C | 24,305 | 24,248 |
+| Local native records | 27,234 | 27,175 |
+| Local paid rank mass | 5,129 | 5,121 |
+| Hosted residual roles, nine stages and 32 replicas | 126,432 | 126,144 |
+| Paid recursive children, including idle remainders | 904,896 | 904,320 |
+| Emitted local records across all 288 calls | 7,843,392 | 7,826,400 |
+| Hosted paid rank mass | 1,808,352 | 1,808,352 |
+| Live DATA / physical registers | 28,416 / 28,425 | 28,416 / 28,425 |
+| Prefix bits / charged bits | 177 / 192 | 177 / 192 |
+| Two-level coefficient bits / charged bits | 393 / 512 | 393 / 512 |
+
+The same upstream word is used on both sides. No local circuit saving from
+another PR is included. The source path is unchanged. The only surviving
+register whose path changes is receiver444:
+`[0,79,509,392,513,1]` becomes `[0,186,509,392,513,1]`.
+The removed helper had path `[0,79,1]`.
+
+## Reproduce
+
+Use Python 3.11 or later with NumPy, SymPy and SciPy, a C++17 compiler, and
+Boost headers. These are the inherited native pipeline requirements.
+From the repository root, run the following command. The output directory
+must not exist. Set `BOOST_INCLUDE` if the headers are outside `/usr/include`.
+
+```sh
+BOOST_INCLUDE=/opt/homebrew/include python3 -I -B research/bit-boundary-persistence/verify.py --output /tmp/r438-source-boundary
+```
+
+The last line is:
+
+```text
+PASS_R438_SOURCE_BOUNDARY R=439->438 ADDs=24305->24248 paid_calls=904896->904320 c=0.001734176288479865766692 controls=6 no_new_kappa
+```
+
+The command uses one worker. It rebuilds both words, checks all source pins,
+compiles and runs the original native checkers, emits both complete hosted
+schedules, audits them, and computes both invoices. It compares the new
+certificate with `CERTIFICATE.json`. It retains the generated words, native
+records, schedules, exact receipts, command list and logs in the output
+directory. It does not run a hosting search.
+
+`SOURCES.json` pins the two complete dependency packages and two selected
+context records at base `8bddbee377e2f3ce1f1247196c4b290d55767d20`.
+The packages include source notices and unused historical controls. The selected
+bit head is `a5afc8c6169ea61ba7c51dfd3cade02cc7b13b46` (PR589).
+Regenerated words are compared by canonical JSON, not gzip container bytes.
+`FRAME-PATHS.json` gives each physical register path in register order.
+
+The recorded run used macOS 26.6.1 arm64, Python 3.14.7, NumPy 2.5.4,
+SymPy 1.14.0 and SciPy 1.18.1. The command records the compiler command and
+Boost version-header hash in `RESULT.json`. Remote CI is not claimed.
+
+## Verification and scope
+
+The local checker covers every arbitrary dirty input column: 661 before the
+change and 660 after it. The original checker accepts H1-H5, the interleaved
+interface, all nine rank-seven copied totals, and the exact full-frame inverse.
+An independent literal record builder agrees with the original exporter.
+The native C++ checker covers 5, 9 and 11 stages on both words; all 96 omitted
+bridge controls reject. Each nine-stage parent audit rejects 17 mutations.
+Each whole-residual hosting audit rejects 16 mutations.
+
+Six new controls reject a changed source77, another carrier use, the late
+source read in frame79, omitted restoration, omitted compensation, and a
+missing returned idle charge. A neutral ADD pair passes and is charged twice.
+The [proof](PROOF.md) gives the boundary and complete invoice derivation.
+
+The caller uses a compressed exact cover schedule. It does not enumerate the
+astronomical address cover. The all-size bit/Gaussian compiler, common labels,
+mutable-source realization, whole-call correlated-helper hosting, common grid,
+tape, precision and analytic contracts remain inherited assumptions. Finite
+checks do not prove the full multiplication theorem or a practical speedup.
+
+The inherited `assemble9.py` also checks its historical PR548 outer arithmetic
+against a cited complex receipt. This is not a replay of the selected PR942
+complex construction or its full outer assembly. The selected record is only
+used for the stated comparison. The eleven-stage native scalar check is run;
+an eleven-stage hosted invoice is not claimed.
+
+## Relation to other work
+
+The initial candidate was to retain a helper basis between adjacent native
+calls. The selected caller alternates the DATA roles and advances to other
+hosted slices. A scalar cancellation does not establish a legal retained
+source and owner boundary there. This package instead changes one intra-call
+source access. It makes no repeated-call cancellation claim.
+
+[PR953](https://github.com/CrocSwap/integer-mult-bounds/pull/953) batches dyadic
+queries with a shared unchanged source and target. It does not provide this
+selected caller boundary. [PR997](https://github.com/CrocSwap/integer-mult-bounds/pull/997)
+has a signed Hadamard recursive interface. Its batch is not composed here.
+[PR980](https://github.com/CrocSwap/integer-mult-bounds/pull/980), head
+`ba1cf68bef0c97dfb120add04304e2de0db6f29c`, retains R439 and all frame paths.
+[PR1001](https://github.com/CrocSwap/integer-mult-bounds/pull/1001), head
+`fbf54e6c95c47a3891eb7e8ed063b5198e920f3f`, changes B at frame506. This word
+leaves B unchanged after register renaming and changes helper stock and a
+source-access frame. Their savings are not added to this result.
+[PR1015](https://github.com/CrocSwap/integer-mult-bounds/pull/1015), head
+`7588c797f4a4e9f2b9fc663cfa6e35afcac05e06`, changes all ten phase-B blocks
+and their literal cleanup. Its pinned `candidate_word` changes B and C only.
+It retains R439, A, D and the paid recursive profile. This candidate changes
+A, C, D, one path and R, while it preserves every B gate under renaming.
+No composition of the two words is tested or claimed.
+
+The full-frame obstruction in PR827 fixes A/scatter/B. The closed class in
+PR933 fixes the helper stock and cleanup structure. This construction changes
+those restrictions. Source inlining and early helper retirement are prior
+ideas; PR429/515 and PR433/437 contain related work. No general mechanism
+priority, circuit optimum, or absence of other valid boundaries is claimed.
+See [NOTICE.md](NOTICE.md) for contributor credit and AI disclosure.