Conditional κ = 0.00308595 (+7.4120e-7 raw over #5565)

research/p104-coupled-frame-step/CHANGES.json

@@ -0,0 +1,50 @@
+{
+  "frames": [
+    [
+      30,
+      44,
+      459
+    ]
+  ],
+  "changes": [
+    {
+      "event": 14374,
+      "old": [
+        "ADD",
+        319,
+        85,
+        "1",
+        728
+      ],
+      "new_frame": 1089
+    },
+    {
+      "event": 14399,
+      "old": [
+        "ADD",
+        507,
+        319,
+        "1",
+        728
+      ],
+      "new_frame": 1089
+    },
+    {
+      "event": 16628,
+      "old": [
+        "ADD",
+        307,
+        85,
+        "-1",
+        236
+      ],
+      "new_frame": 235
+    },
+    {
+      "endpoint": "final",
+      "register": 307,
+      "old_frame": 236,
+      "new_frame": 235
+    }
+  ]
+}

research/p104-coupled-frame-step/DISCOVERY.md

@@ -0,0 +1,37 @@
+# Discovery and source credit
+
+The construction uses DreamingOfClouds's event-lattice model from PR5568,
+exact commit `47a347ff70044615e7be6581d275d12f5df38295`. That package
+reports a small retiming gain on PR5561. Its model and reported gain are
+prior work, not a discovery claimed here.
+
+A first composition on PR5580 passed the complete registered checks at
+kappa .00308191. Before publication, a fresh PR check found Pierre-Loic
+Doulcet's larger PR5565 cascade. The first candidate was preserved locally;
+it is not the contribution submitted here. The search was transferred to
+PR5565 at `9af814164b9dfc21f19ec737959d67cb71488c95` without changing
+its scalar order.
+
+The new run used OR-Tools 9.14.6206 on CPython 3.12.13, four solver workers,
+90 seconds, neighbor radius two and all intermediate subspaces in anchor
+quotients of dimension at most three. Its command structure was:
+
+```sh
+HEAVY_THREADS=4 python3.12 -B evlat.py PR5565-WORD.json.gz witness.json.gz 90 2 3
+```
+
+The status was `FEASIBLE`. The fast legality check passed and the re-price
+was about 0.003085951751. The solver was not an optimality proof, and its
+parallel output is not promised to be deterministic.
+
+The output changed 26 event/endpoint nodes in 20 independent components.
+Only one component changed the moment: three ADD charts and helper 307's
+final chart. The submitted construction retains exactly that component.
+CHANGES.json fixes its four source sites and the new three-dimensional
+frame. No solver is needed to reconstruct or verify it.
+
+Earlier scratch, compensated-scalar, fixed-order and commuting-ADD screens
+found no paid-profile gain. Those searches are not submitted as exhaustive
+obstructions. In particular, the independent owned-holder obstruction
+belongs to PR5579. The submitted claim is this explicit frame step on the
+newer cascade, its written chart proof and its complete exact certificate.

research/p104-coupled-frame-step/HANDOFF.md

@@ -0,0 +1,33 @@
+# Composition with the independent helper splits
+
+[PR #5599](https://github.com/CrocSwap/integer-mult-bounds/pull/5599), exact
+head `0644592d421b375c221045954fdf13932575ffa8`, reports conditional kappa
+.00309839 on a different word with 750 public inputs and 542 helpers.
+Its source is PR5580. This package instead consumes both stages of PR5565
+and changes three contacts plus helper 307. No combined gain is claimed.
+
+The published fifteen-split witness was read at that exact head. None of
+registers 85, 307, 319 or 507 occurs in its a, b, c or d basis-operation
+supports. This is a useful compatibility screen, not a proof of composition.
+The supports do include registers 648, 649, 650, 652 and 198, which occur
+in PR5565 Stage A. Some split witnesses use frame 597, whose contacts that
+stage removes. Do not apply the complete cascade without rechecking cuts.
+
+A bounded next test is:
+
+1. Start from the exact PR5599 word. Authenticate its source and retain
+   its larger input inventory, owned-register indices and compiler stock.
+2. Test PR5565 Stage B separately from Stage A. It supplies the source
+   frame paths needed by this package. Check its commuting interval against
+   every inserted basis operation and repeat all split-interface checks.
+3. Match this package's three ADDs by their source operands and surrounding
+   accesses. Add U = `[30,44,459]`, move the first two contacts to U, and
+   move the last contact and helper 307 exit to frame 235.
+4. Reconstruct every transport, then replay all original inputs and the
+   transpose, every native map, physical caller, both complete moment
+   engines, compiler and outer inequalities. Count every helper target and
+   scalar/basis operation. Publish a combined kappa only after those pass.
+
+Credit Ali Romman's PR5599 independent-helper construction, Pierre-Loic
+Doulcet's PR5565 cascade, DreamingOfClouds's event-lattice method and all
+retained P104 sources. This handoff reserves no further search.

research/p104-coupled-frame-step/LITERAL-CHANGES.diff

@@ -0,0 +1,13 @@
+--- PR5565/pricing.py
++++ pricing.py
+@@ -14,2 +14,2 @@
+-KAPPA, TESTED = Q('.00308520'), Q('.0030852005')
+-PREVIOUS = Q('.00308189')
++KAPPA, TESTED = Q('.00308595'), Q('.0030859505')
++PREVIOUS = Q('.00308520')
+@@ -64 +64 @@
+-    L.need(sum(targets.values()) == 12814 and sum(paid.values()) == 66726, 'Complete field and call counts')
++    L.need(sum(targets.values()) == 12814 and sum(paid.values()) == 66708, 'Complete field and call counts')
+@@ -142 +142 @@
+-    return encode({'kappa':KAPPA,'kappa_decimal':'.00308520','previous_open_pr5580':PREVIOUS,'gain':KAPPA-PREVIOUS,
++    return encode({'kappa':KAPPA,'kappa_decimal':'.00308595','previous_open_pr5565':PREVIOUS,'gain':KAPPA-PREVIOUS,

research/p104-coupled-frame-step/PROOF.md

@@ -0,0 +1,183 @@
+# Three coupled contacts improve the PR5565 P104 cascade
+
+## Source and statement
+
+The input is the exact PR5565 word at
+`9af814164b9dfc21f19ec737959d67cb71488c95`, by Pierre-Loic Doulcet
+(hexapode). It includes both stages of the commuting-contact cascade.
+[SOURCES.json](SOURCES.json) pins this word and the retained price engine.
+The event-lattice search from DreamingOfClouds's PR5568 supplied the
+construction method. This package supplies the new four-site frame step
+and its complete certificate on the later word.
+
+The construction preserves every scalar instruction, coefficient and
+position in the scalar sequence. It preserves all 208 main endpoints,
+all helper starts, all owned lifetimes and all 104 literal ports. It
+changes three ADD charts and the final frame of helper 307.
+[CHANGES.json](CHANGES.json) gives these four declarations. All event
+indices below refer to the zero-based PR5565 source program.
+
+At each of 18 local calls, the paid change is
+
+```text
+-2 H2 + 2 H3 - 2 H4 + H5.
+```
+
+The target change is `H4 - H5`. The complete conditional claim is
+kappa = 0.00308595, tested at 0.0030859505. The five framework assumptions
+and the source helper-endpoint conditions remain inherited. The selected
+record is unchanged.
+
+## Exact chart geometry
+
+The new frame U has basis `[30,44,459]` and dimension three. It is frame
+1089 in the new word. The source has 1089 frames, indexed 0 through 1088.
+The following identities use complete binary spans, not basis-list equality:
+
+```text
+U = span(frame 345 union frame 355)
+  = frame 728 intersection frame 235.
+```
+
+The relevant source frames are:
+
+| Frame | Basis | Dimension |
+| --- | --- | --- |
+| 3 | `[]` | 0 |
+| 345 | `[30,487]` | 2 |
+| 355 | `[30,44]` | 2 |
+| 728 | `[30,44,76,391]` | 4 |
+| 235 | `[30,44,74,385]` | 4 |
+| 236 | `[6,24,42,74,385]` | 5 |
+| 775 | `[7,25,43,75,139,267]` | 6 |
+| 795 | `[12,18,32,64,391]` | 5 |
+| 127 | standard nine-axis basis | 9 |
+
+The changed contacts are:
+
+| Event | Scalar instruction | Old frame | New frame |
+| --- | --- | --- | --- |
+| 14374 | `ADD 319 += 85` | 728 | U |
+| 14399 | `ADD 507 += 319` | 728 | U |
+| 16628 | `ADD 307 -= 85` | 236 | 235 |
+
+The new first two contacts let register 85 bypass frame 728. It can then
+meet helper 307 at frame 235. Helper 307 no longer needs its last rank-one
+transport and can finish at dimension four. This is a coupled change:
+the last contact cannot move down to frame 235 while 85 retains frame 728.
+
+The exact paths between unchanged accesses are:
+
+| Register | Old path | New path |
+| --- | --- | --- |
+| 85 | `345 -> 728 -> 236 -> 127` | `345 -> U -> 235 -> 127` |
+| 319 | `355 -> 728 -> 775` | `355 -> U -> 775` |
+| 507 | `3 -> 728 -> 795` | `3 -> U -> 795` |
+| 307 | `235 -> 236` | stays at `235` |
+
+All arrows are strict subspace inclusions. Every unchanged intervening
+register access is retained. The constructor checks the four source
+values, changes their charts, and replaces transports only in gaps with
+a changed endpoint. It removes eight transports and inserts seven. The
+result has 25,132 events and the same 21,686 scalar/owned events.
+
+## Arbitrary-input identity and native interfaces
+
+Let C_F be the native chart for frame F. Write a physical field as C_F z,
+where z is its abstract row. A transport from A to B applies C_B C_A^-1
+and leaves z unchanged. An ADD at one common chart forms the same abstract
+row sum. A SCALE has the same property. Thus each legal changed itinerary
+implements the same abstract scalar word.
+
+The exact replay checks a common chart at every scalar contact and strict
+nesting at every public transport. It checks all 743 original input
+coefficients in every output. Every helper row returns its own arbitrary
+input, and the main shears remain unchanged. A separate dense dyadic
+transpose replay checks the reverse operator.
+
+Helper 307 starts at frame 3 in both words. Its target changes from the
+rank-five map C_236 to the rank-four map C_235. Its input stays independent
+of all other inputs. No helper input is set to zero or discarded. Every
+other productive target stays fixed.
+
+The native replay checks every paid map, helper target and main adapter:
+rank, signed Pauli images and absolute phase. The factorwise tensor rule
+gives the same chart identity at every positive width under the retained
+native framework. These checks do not, by themselves, prove the full
+multiplication theorem or provide independent acceptance of the framework.
+
+## Complete paid and target change
+
+The four register changes give these local paid deltas:
+
+| Register | Paid delta |
+| --- | --- |
+| 85 | `H1 - H2 - H4 + H5` |
+| 319 | `H1 - 2H2 + H3` |
+| 507 | `-H1 + H2 + H3 - H4` |
+| 307 | `-H1` |
+
+Their sum is `-2H2 + 2H3 - 2H4 + H5`. The local paid rank mass and target
+rank mass both decrease by one. The complete rank-mass surplus remains
+760. Paid jobs decrease by 18, from 66,726 to 66,708. The 12,814 productive
+fields remain independent.
+
+Write h_r(k) = r^(1-k), with h_0(k) = 0. If M is target moment minus paid
+moment, then
+
+```text
+M_new(k) - M_parent(k)
+  = 18 * (2 h_2(k) - 2 h_3(k) + 3 h_4(k) - 2 h_5(k)).
+```
+
+For 0 < k < 1, this is strictly positive. To see this, the decreasing
+vector `(5,5,3,3,0)` has partial sums `(5,10,13,16,16)`, and
+`(4,4,4,2,2)` has partial sums `(4,8,12,14,16)`. The first vector
+majorizes the second. Strict concavity of x^(1-k) therefore gives
+`2 h_5 + 2 h_3 < 3 h_4 + 2 h_2`. The zero term is used only in this
+proof; it is not an uncharged job in the construction.
+
+The predecessor raw crossing is in
+`(0.00308521055201, 0.00308521055202)`. The new crossing is in `(0.00308595175070, 0.00308595175071)`.
+The raw gain is between 7.4119868e-7 and 7.4119870e-7. The raw headroom
+above the claimed endpoint is between 1.75070e-9 and 1.75071e-9. The verifier reconstructs both
+predecessor histograms from the new bill and the declared deltas, then
+checks the predecessor crossing again. Two rational moment engines check
+the new tested endpoint.
+
+The derivative certificate proves that the complete new moment is strictly
+decreasing on `[0,0.0034]`. Its upper crossing endpoint is the raw funding
+ceiling for this fixed invoice on the retained BIT band. No ceiling for
+other words or suppliers is claimed.
+
+## Full caller, verification and limits
+
+The unchanged caller has 18 forward local calls, 15 query shears and
+3,120 whole idle jobs. The physical replay checks the actual 104 ports,
+main routes, central squares, output ranks and whole-idle maps. The price
+code derives the invoice from those events and checks it again from the
+controller paths. It includes helper targets, normalizers, main adapters,
+all routes, scalar operations, owned copies and erasures.
+
+The retained price engine changes only claim, predecessor-comparison and
+exact paid-count declarations. LITERAL-CHANGES.diff records every change.
+No source checker is weakened or patched at runtime. The PR5545 source
+capsule and all 33 payload files are authenticated before import.
+
+The compiler checks all three tail ratios, completion, splitting, the
+integer threshold, retained BIT stock and all 54 strict plus four
+functional outer predicates. New negative controls reject a missing
+transport, a wrong scalar coefficient, an old contact frame, an old helper
+exit, a wrong intermediate subspace and an unchanged word presented as an
+improvement. Source controls also reject a wrong native phase, insufficient
+BIT saving and an old cutoff.
+
+The five inherited assumptions remain: native all-column implementation,
+owned erasure, uniform compiler closure, precision/fixed-tape costs and
+analytic recovery. The helper-endpoint contract retains its source review
+status. The uniform word and complete rounded multiplier are not
+materialized. The same assistant performed discovery and verification;
+this is not independent scientific review or proof-kernel acceptance.
+
+Ali Romman with substantial OpenAI Codex assistance. Apache-2.0.
+All retained source notices and predecessor credit remain in the package.