Conditional κ = 6.83847872497761e-4: five-level bootstrap on PR211 cascade frames

.github/workflows/cascade-frames-bit.yml

@@ -0,0 +1,42 @@
+name: Verify cascade-optimized bit frames
+on:
+  pull_request:
+    paths:
+      - 'research/cascade-frames-bit/**'
+      - 'research/source-assisted-v4/**'
+      - 'research/source-assisted/**'
+      - 'scripts/paired_cube_assembly.py'
+      - '.github/workflows/cascade-frames-bit.yml'
+  push:
+    paths:
+      - 'research/cascade-frames-bit/**'
+      - '.github/workflows/cascade-frames-bit.yml'
+  workflow_dispatch:
+permissions:
+  contents: read
+jobs:
+  full:
+    runs-on: ubuntu-24.04
+    timeout-minutes: 45
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
+        with:
+          persist-credentials: false
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
+        with:
+          repository: CrocSwap/integer-mult-bounds
+          ref: a1175449f34d39ff933d9d8ab23ced1f32b290ec
+          path: .dependencies/pr200
+          persist-credentials: false
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
+        with:
+          repository: CrocSwap/integer-mult-bounds
+          ref: 187e1010ac8b259af8e9b5166f68b64bc27b4b47
+          path: .dependencies/pr193
+          persist-credentials: false
+      - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97
+        with:
+          python-version: '3.13'
+      - run: python -m pip install -r .dependencies/pr193/research/source-assisted/requirements-round13.txt
+      - run: python -B research/cascade-frames-bit/verify.py --complex-root .dependencies/pr193 --bit-root .dependencies/pr200 --full
+      - run: git diff --exit-code

.github/workflows/packed-diagonal-bit.yml

@@ -0,0 +1,38 @@
+name: Verify packed diagonal bit supplier
+on:
+  pull_request:
+    paths:
+      - 'research/packed-diagonal-bit/**'
+      - 'research/source-assisted-v4/**'
+      - 'research/source-assisted/**'
+      - 'scripts/paired_cube_assembly.py'
+      - '.github/workflows/packed-source-assisted-bit.yml'
+  workflow_dispatch:
+permissions:
+  contents: read
+jobs:
+  full:
+    runs-on: ubuntu-24.04
+    timeout-minutes: 30
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
+        with:
+          persist-credentials: false
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
+        with:
+          repository: CrocSwap/integer-mult-bounds
+          ref: a1175449f34d39ff933d9d8ab23ced1f32b290ec
+          path: .dependencies/pr200
+          persist-credentials: false
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1
+        with:
+          repository: CrocSwap/integer-mult-bounds
+          ref: 187e1010ac8b259af8e9b5166f68b64bc27b4b47
+          path: .dependencies/pr193
+          persist-credentials: false
+      - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97
+        with:
+          python-version: '3.13'
+      - run: python -m pip install -r .dependencies/pr193/research/source-assisted/requirements-round13.txt
+      - run: python -B research/packed-diagonal-bit/verify.py --complex-root .dependencies/pr193 --bit-root .dependencies/pr200 --full
+      - run: git diff --exit-code

research/cascade-frames-bit/NOTICE

@@ -0,0 +1,4 @@
+
+
+Finite stopped-leaf extension (2026-10-10)
+This follow-up reuses PR211's cascade-optimized frame supplier (Rohan Arun, with Claude assistance) and adds two exact fixed-depth composition levels following PR185/187/210. The fourth- and fifth-level recurrences, exact certificate update, and independent audit were prepared with OpenAI Codex assistance. No authorship is claimed for PR211's frame layout, PR200's bit word/checkers, PR197's banks, PR193's complex supplier, or their inherited interfaces.

research/cascade-frames-bit/PR-STATEMENT.md

@@ -0,0 +1,45 @@
+# Five-level finite bootstrap on the PR211 cascade-frame supplier
+
+## Result
+
+Starting from open PR211's exact conditional exponent `683847872495777/10^18`, this follow-up adds two fixed stopped-leaf levels and obtains
+
+```text
+kappa = 683847872497761/10^18
+      = 0.000683847872497761.
+```
+
+The exact gain over PR211 is `1984/10^18`. The fifth level adds the last `10^-18` grid step over the four-level version. The bit supplier still binds. The regenerated certificate stores all 47 exact positive assembly margins, and the independent audit rejects the adjacent final grid point.
+
+## Mechanism and inherited construction
+
+The finite supplier and physical frames are PR211's frozen cascade-optimized PR200 bit word: 6,191 changed operation frames, the same terminal-modified word, 1,760 compensated aliases, completed banks, and PR193 complex supplier. We do not overwrite that layout with an older frame candidate. In an explicit comparison, PR211 already uses the same first-frame minimum joins at all 17 pairs found in our prior local search, while its second frames are smaller than that earlier candidate. The stronger cascade schedule is retained intact.
+
+Let `c` be the newly priced packed bit saving and let `a_0` be the fully paid ordinary saving from the admitted PR200 word. Five fixed recurrences use
+
+```text
+a_j = (1-c)c + c a_(j-1),  j=1,2,3,4,5.
+```
+
+The exact rational verifier checks every recurrence, `a_(j-1) < a_j < c < 1-a_j`, the two-supplier paid moments, and the unchanged 47-constraint assembly with `eta=beta=10^-24` and weakening `10^-30`. The finite depth is five, independent of input size. For the fixed suppliers, the exact assembly ceiling at the unattained limit `a=c` has the same `10^-18` grid floor as the fifth level; since every finite `a_j<c` and the ceiling is increasing, no deeper fixed level can raise the reported grid value. The limiting value is only an upper-bound check, not an input supplier.
+
+## Reproduction and validation
+
+```sh
+python -B research/cascade-frames-bit/verify.py \
+  --complex-root .dependencies/pr193 \
+  --bit-root .dependencies/pr200 \
+  --full
+```
+
+The existing workflow checks out the pinned PR193 and PR200 sources, reruns the PR193 complex verifier, re-admits all PR200 frames and terminal columns, rebuilds banks, recomputes the exact certificate and independent moment audit, and compares the regenerated certificate byte for byte. The root Verify workflow also covers the repository Makefile matrix and formal jobs.
+
+The local exact-arithmetic replay used PR211's frozen admitted physical record and the byte-pinned PR193 assembly/certificate. It produced five levels, 47 positive exact assembly margins, an independent moment audit PASS, and the exact limiting-grid upper bound. At Draft creation, this follow-up's GitHub Actions runs have not yet completed; the submitted branch reruns the complete frame/source verification.
+
+## Conditions and limits
+
+The conclusion remains conditional on the inherited all-width compiler, completed weighted/restored selector, routing, prime supply, precision/recovery, fixed analytic tape, and finite bridge hypotheses. PR211's cascade search is heuristic and does not prove a frame optimum. Finite verification does not prove the inherited all-size interfaces or the multiplication theorem unconditionally; this adds no Lean proof and makes no practical-speedup claim.
+
+## Attribution
+
+The cascade frame layout and its verification belong to PR211 (Rohan Arun, with Anthropic Claude assistance). The bit word/checkers are from PR200, banks from PR197, complex supplier from PR193, and finite-composition work from PR185/187/210; their licenses and source notices are retained. The fifth-level arithmetic extension and independent audit were prepared with substantial OpenAI Codex assistance. No inherited construction is claimed as new or exclusive work.

research/cascade-frames-bit/README.md

@@ -0,0 +1,64 @@
+# Cascade-optimized frames on PR200's banked bit word
+
+Under the retained multiplication interfaces, this finite witness certifies
+
+$$
+T(n)=O\left(n(\log n)^{1-\kappa}\right),\qquad
+\kappa=\frac{683847872497761}{10^{18}}=0.000683847872497761 .
+$$
+
+That is **+0.0962%** over PR207 (`1366380910073/(2*10^15)` = 0.0006831904550365) and **+0.1152%** over PR205 (0.000683061299399923). The bit supplier still binds; PR193's complex saving `700918443859411/10^18` is unchanged. Two additional fixed finite-leaf levels raise PR211's exact κ by `1984/10^18`; the fifth level adds the final `10^-18` grid step over the four-level version.
+
+| Construction | Unpacked bit coarse | Packed bit coarse | Conditional kappa |
+|---|---:|---:|---:|
+| PR205: PR200 word + completed banks | 6.77774e-4 | 6.835282e-4 | 0.000683061299399923 |
+| PR207: 302 coordinated frames + banks | | | 0.0006831904550365 |
+| PR211: 6,191 cascade-optimized frames + three finite levels | 6.785484e-4 | 6.843158e-4 | 0.000683847872495777 |
+| Intermediate: same frames + four finite levels | 6.785484e-4 | 6.843158e-4 | 0.000683847872497760 |
+| **This: same frames + five finite levels** | **6.785484e-4** | **6.843158e-4** | **0.000683847872497761** |
+
+## What is new
+
+PR207 showed that PR200's operation frames are not optimal for the paid moment and admitted 302 rational frame changes. This package pushes the same lever much further with a different search.
+
+**Exact chain model.** Every physical chain of PR200's word (donor + recipient splices, root frames, terminal full frame) is a sequence of slots. Each operation frame is shared by its destination and source chains. A frame is feasible when it contains the operation's value span, is G-nondegenerate, and is nested between its neighbours on both chains. The cost of a chain is the sum of `t*ln(72/t)` over its rank increments `t`, the first-order paid-moment weight.
+
+**Cascading moves.** For an operation, try raising its frame to a later neighbour frame on either chain (up to four slots ahead), or to its global feasible maximum. Joining the new frame forward along every affected chain repairs nesting. Lowering mirrors this: meet backward down to the global feasible minimum. Root frames, gauge frames, start frames and alias endpoints stay fixed. A move is accepted on exact cost decrease. Single-operation moves stall almost at once; the cascades plus short annealing (T = 0.5, 1.0, 0.3) reach a deeper local optimum. Internal chain cost falls from 804,451.6 to 803,364.5 (−0.135%).
+
+**Admission by PR200's own checkers.** Frames are the only change; 6,191 operations receive new rational bases (`opframe-bases.json`). PR200's modules re-check:
+
+- every replacement frame for value span and nondegeneracy;
+- all physical chain nestings and the 1,760 alias containments;
+- the 34-sink terminal-modified word on all 1,760 source, 1,760 target and 17,114 dirty columns, over F2 and over the integers (residual bound 39,780, 24-bit packed digits);
+- Gram/prime witnesses for all 24,611 used frames, each with residual factor below 2^80;
+- the paid coarse and atom certificate.
+
+The resulting unpacked coarse saving is `135709678471459/(2*10^17)`.
+
+**Banks.** Same as PR205. Role counts, gauges and aliases are unchanged, so there are 45,842 banks, W = 56,402, deficit 5,808, maximum child 22, and at most 171 chart factors. The conservative selector-call bound is 5,368,513,266.
+
+**Composition.** The finite ordinary-leaf recurrence uses five levels from the re-certified ordinary saving. It is followed by the balanced 47-constraint assembly with eta = beta = 10^-24. The next 10^-18 grid point fails. The exact limiting grid ceiling at the coarse bit saving is also the five-level value, so deeper fixed levels cannot raise κ on this grid; the unattained limit is used only as an upper bound, not as a supplier.
+
+## Reproduce
+
+```sh
+git -C <pr193> checkout 187e1010ac8b259af8e9b5166f68b64bc27b4b47
+git -C <pr200> checkout a1175449f34d39ff933d9d8ab23ced1f32b290ec
+python -B research/cascade-frames-bit/verify.py --complex-root <pr193> --bit-root <pr200> --full
+```
+
+The full run takes about 6 minutes on two cores. It re-runs PR193's complex verifier, re-admits every frame through PR200's exact checkers, rebuilds charts and banks, and reproduces `certificate.json` byte for byte. Without `--full`, it re-derives the arithmetic from the stored physical record.
+
+## Scope
+
+This is a conditional finite supplier certificate. It inherits, without proving, the same all-size compiler, the completed weighted/restored selector, routing, precision, the fixed analytic tape, and the finite bridge hypotheses as PR193/197/200/205/207. The frame search is a heuristic local optimum with no optimality claim. The search scripts are not needed for verification: only the frozen frame list is a mathematical input.
+
+## Credits
+
+- PR200 (Chafik Boukhalfa): word and checkers.
+- PR193: complex supplier.
+- PR197 (Evan McKinney): bank packing.
+- PR185/187: finite composition.
+- PR207 (Dugongue): first showed that frame re-optimization pays and how to admit frames through PR200's checkers.
+
+Prepared by Rohan Arun with Anthropic Claude assistance. Apache-2.0.

research/cascade-frames-bit/SOURCE.json

@@ -0,0 +1,24 @@
+{
+  "bit_commit": "a1175449f34d39ff933d9d8ab23ced1f32b290ec",
+  "bit_files": {
+    "research/paired-cube-diagonal-bit-168/arithmetic/interval_moment.py": "9d3d1d28bfb3375958995205179b171fb65c70a3792cf9f7a21ef5ee54f5460b",
+    "research/paired-cube-diagonal-bit-168/certificate.json": "853afa75980e11ce16b333c28311c4f635e84065867c049fda9916c2419091ed",
+    "research/paired-cube-diagonal-bit-168/selected/bit/frames_p12.json": "aec2f09df5b42165a353a9233d9c8549bf091167915f6b044689c4bfb189d406",
+    "research/paired-cube-diagonal-bit-168/selected/bit/sinks.json": "c00ff70c564829d4b97740f92796fc6ce14fbcd5ca519663828650552b80249d",
+    "research/paired-cube-diagonal-bit-168/selected/bit/word_p12.json": "0728ed1c7320430a87709b1034485cbabefec85d532b48897f74136cf3954218"
+  },
+  "bit_manifest_sha256": "015abe3342d08d08a9c4a764f103cafc1be1fe7f23d7a72471bd87412c57c2df",
+  "comparison": {
+    "pr197": "Evan McKinney, packing on PR187",
+    "pr202": "Chafik Boukhalfa, kappa = 6768823/10^10",
+    "pr204": "maxime-fleury, modelled 6.83061299e-4"
+  },
+  "complex_commit": "187e1010ac8b259af8e9b5166f68b64bc27b4b47",
+  "complex_files": {
+    "research/source-assisted-v4/SOURCE.json": "99024e5c8296ad03b6e499c3c4e1e9e879bf6a5954d8558cc39abd557edf79d6",
+    "research/source-assisted-v4/certificate.json": "d84406d2fcc6990deba2b135509e6d86600e57123d88f9b21f7b7240e1aeb513",
+    "research/source-assisted/global/FINITE_BRIDGE.txt": "66d8f4ea8752abd89952d6674a636575a0db16e18b1c16e293f48f64242f0c46",
+    "scripts/paired_cube_assembly.py": "c1ebb52163a7219504c728a5c2b098bf1e50bf20148a2879c5a74c3cadc7c03c"
+  },
+  "frames_sha256": "56b2ed0f6b867e8cafdc32ac70419cfda36d02838844572098b3fc77f8026e58"
+}