Remove 60 native maps and 42 more ADDs after PR5350; kappa unchanged

research/native-gauge-cancellation/PROOF.md

@@ -0,0 +1,105 @@
+# Exact native-map cancellation on the fixed source word
+
+## 1. Scope
+
+The input is the final PR4610 word after the credited PR5350 constructor.
+All 632 persistent inputs are arbitrary. C0 is owned and returns zero.
+The output is a new scalar/native word with the same physical endpoints,
+frame contacts and recursive invoice. This proof does not establish a higher
+kappa, a practical speedup, or an optimum among linear circuits.
+
+## 2. Normalize each field before comparing ADDs
+
+Write the current value in field r as
+
+    y_r = c_r G_r z_r,
+
+where c_r is a nonzero rational scalar and G_r is a word in native maps and
+their inverses. Initially c_r=1 and G_r is empty. A SCALE changes c_r. A warp
+W changes G_r to W G_r. Adjacent inverse letters reduce in the free group.
+Only this exact inverse rule is used; no finite-column coincidence is assumed.
+
+An ADD y_r += a y_s acts on the normalized values as
+
+    z_r += (a c_s/c_r) G_r^-1 G_s z_s.
+
+For r distinct from s, two such ADDs on the same ordered pair commute and
+combine by coefficient addition when their normalized native words agree.
+Two ADDs on pairs (r,s) and (u,v) commute if r differs from v and u differs
+from s. This follows by multiplying their elementary block matrices: both
+cross terms vanish. It holds for noncommuting operator coefficients.
+
+The constructor scans back only across this commuting relation. A source
+write or target read stops the scan. A CLEAR or COPY stops it on each of its
+operands. Thus it does not move an ADD through an overwrite or a dependent
+operation. When it combines two coefficients at the later contact, it converts
+the sum back to that contact's actual scalar factor. A zero sum deletes both
+ADDs. A nonzero sum replaces the later scalar coefficient. Every intermediate
+native map and SCALE remains in place at this step.
+
+Consequently the changed logical word is an exact identity in the free
+operator algebra. It holds for any representation of the native maps,
+including their actual absolute phases and every allowed column multiplicity.
+This algebraic statement does not discharge the inherited all-size native
+implementation assumption.
+
+## 3. Remove native maps with no remaining contact
+
+For each field, the second pass tracks native maps between scalar contacts.
+A scalar read, write, COPY or CLEAR ends that interval. SCALE commutes with a
+native linear map. Within one interval, adjacent inverse letters cancel.
+This includes letters separated by operations on other fields.
+
+Climbs are coordinate changes in the logical frame representation. The
+constructor keeps every paid climb record. After the logical simplification,
+both retained native interpreters check the actual input frame of every
+warp, the common frame of every scalar contact, each paid transition, every
+persistent output, and the owned return. This is necessary: logical equality
+alone would not prove that the changed record list has legal physical frames.
+
+For a legal framed word, substitute the frame map at each contact. Each
+internal frame map cancels its inverse at the next operation. The physical
+endpoint is therefore the final frame map, followed by the logical word,
+followed by the inverse initial frame map. Since the initial and final maps
+and the logical operator are unchanged, the physical endpoint is unchanged.
+All paid edges and all surviving warps have the original exact phase recipes.
+No new edge or monomial operator is introduced. The historical recipe proofs
+are reused; this replay does not run their full phase-lowering suite again.
+
+## 4. Exact effect on the complete bill
+
+The pass follows the PR5350 compressor. Per orientation, it removes 42 scalar
+ADD records and 60 of its 240 warp records. The source scalar allowance uses
+coefficient size; it is not a flat price per ADD. The extra allowance saving
+is exactly 236. Including PR5350, the reduction from PR4610 is 193 scalar
+records, 60 warps and 1452 scalar allowance units per call.
+
+Both orientations retain every PR5350 paid record in its chronological order.
+They also retain the original PR4610 role/frame/rank transition census. The
+paid profile is
+
+    {1:2201, 2:412, 3:510, 4:127, 5:40, 8:8}.
+
+The main and helper endpoints and all helper inputs are unchanged. Hence all
+productive jobs are unchanged. For every exponent t, both sums of r^t in the
+complete controller invoice are identical to their previous values. The
+recursive moment and kappa do not improve. If the same word is used in all
+18 full calls of the retained p16 controller, the local count differences
+multiply by 18; that statement is arithmetic, not a new whole-controller run.
+
+## 5. Evidence and limits
+
+The deterministic receipt contains both retained all-column interpreter
+results, the generated program hashes and source-event patch. Dense rational
+controls check dependency barriers and scalar normalization. An actual scalar
+sign mutation fails both native interpreters in both orientations. The source
+files are pinned by bytes and Git blob.
+
+There is no new independent native interpreter, cold selected replay, uniform
+compiler, BIT supplier, precision/tape implementation, analytic recovery,
+formal-kernel proof or end-to-end integer-multiplication check. The five
+selected framework assumptions remain. Independent human review is open.
+
+Credit Cao Yifan, Cinna Davis, ahrazzle, Chrisbryan17, Dugongue, zxv, Jacob
+Alan Sussman, and all retained source authors. Ali Romman with substantial
+OpenAI Codex assistance. Apache-2.0.

research/native-gauge-cancellation/README.md

@@ -0,0 +1,95 @@
+# Remove 60 native maps after the final Cao scalar compressor
+
+This exact circuit change removes **60 native-map records and 42 more scalar
+ADD records per native call**, after the 151-ADD reduction in
+[PR #5350](https://github.com/CrocSwap/integer-mult-bounds/pull/5350).
+The new scalar allowance saving is 236 per call. The total reduction from
+Cao Yifan's final PR4610 word is 193 scalar records, 60 native maps, and 1452
+scalar allowance units per call. The native-map count falls from 240 to 180.
+These are circuit counts, not measured running times.
+
+**Kappa does not change. This is not the requested bottleneck breakthrough.**
+The complete paid Gaussian profile and all 408 productive helper boundaries
+are unchanged. Thus the complete recursive moment is identical for every
+exponent. The selected conditional kappa at the base is 0.0030217758. The
+binding main-transform cost is unchanged. No selected record is edited.
+
+| Orientation | PR4610 scalar allowance | PR5350 allowance | New allowance |
+| --- | ---: | ---: | ---: |
+| Forward | 158120 | 156904 | 156668 |
+| Backward | 158168 | 156952 | 156716 |
+
+The new pass tracks each field's scalar factor and formal native-map word.
+It combines exact equal ADD operators across commuting instructions. It then
+removes native maps that have become an unused inverse pair. It preserves
+noncommuting dependencies and reset barriers. [PROOF.md](PROOF.md) states the
+algebra and the physical-frame argument. [RESULT.json](RESULT.json) gives the
+source-event patch, generated word hashes, both native receipts, complete
+local invoices, and failure controls.
+
+The base is canonical main `1ec1119972c9aefe42525172d07b332fcff81cb4`.
+[SOURCES.json](SOURCES.json) pins all ten consumed files by SHA256 and Git
+blob. The original native payload has decompressed SHA256
+`cfcd36b40326d7a5815e1db5313444379b3fb756b27d5201c561574c085cc0dd`.
+The source constructor, archives, receipts and selected supplier are not edited.
+
+## Verification
+
+Use Python 3.12 and the standard library. From the repository root:
+
+```sh
+python3 -B scripts/research_package.py --package research/native-gauge-cancellation
+```
+
+The scientific command ends with:
+
+```text
+PASS_NATIVE_GAUGE_CANCELLATION_NO_KAPPA_CHANGE
+```
+
+The verifier rebuilds both orientations. Two retained source interpreters
+check all 632 arbitrary persistent columns, arbitrary owned entry state,
+exact scalar frames, native-map words, and zero return of the owned field.
+Every paid record from PR5350 is retained. Every original role/frame/rank
+transition is retained. The complete paid profile remains
+`{1:2201,2:412,3:510,4:127,5:40,8:8}` with 3298 jobs and rank mass 5327.
+The formal prefix bounds remain 457 forward and 169 backward.
+
+Exact dense controls check source writes, target reads, scalar-weight changes
+and resets. A distinct native-map word cannot be cancelled. Both native
+interpreters reject a changed scalar sign in the actual emitted word.
+The default replay compares the deterministic receipt without writing it;
+`--write` is the explicit receipt-generation command.
+
+[VALIDATION.md](VALIDATION.md) records executed checks. No new phase recipe is
+needed: the paid records are unchanged and each retained warp is an original
+frame-bound warp. Their existing absolute-phase lowering is reused, not
+rerun. No complete controller, compiler, BIT, outer-ledger, cold-supplier,
+formal-kernel or end-to-end integer-multiplication replay is claimed. Native
+all-column, ownership, uniform compiler, precision/tape and analytic-recovery
+assumptions remain inherited. Independent human review remains open.
+
+## Open next questions
+
+This result does not justify another search with the same recursive bill.
+A kappa claim needs a changed paid or productive profile and full admission.
+The present package makes no claim about the best possible scalar circuit.
+
+## Credit
+
+Cao Yifan supplies the final native word in
+[PR #4610](https://github.com/CrocSwap/integer-mult-bounds/pull/4610).
+Cinna Davis supplies the commuting and triangle rewrites in
+[PR #4692](https://github.com/CrocSwap/integer-mult-bounds/pull/4692).
+ahrazzle supplies their paid-profile-safe final-word composition in
+[PR #5350](https://github.com/CrocSwap/integer-mult-bounds/pull/5350).
+Chrisbryan17 supplies the earlier bounded inverse-pair check in
+[PR #5265](https://github.com/CrocSwap/integer-mult-bounds/pull/5265).
+This package imports the prior constructor and both retained interpreters;
+they are not new independent implementations. It adds scalar/native-map
+normalization and the resulting cancellations.
+
+Credit Cinna Davis's controller/helper lineage, Dugongue's native maps, zxv,
+Jacob Alan Sussman, and all retained scalar, Clifford, geometry, compiler,
+precision and analytic authors. Source notices remain unchanged. New work by
+Ali Romman with substantial OpenAI Codex assistance; no subagents. Apache-2.0.