A frame-layout ceiling for #200's bit word: coarse < 6.964e-4 under the banked ledger, so κ < 6.959e-4 on #205–#207's word (no new κ)

.github/workflows/bit-frame-ceiling.yml

@@ -0,0 +1,25 @@
+name: bit-frame-ceiling
+
+on:
+  pull_request:
+    paths:
+      - 'research/bit-frame-ceiling-200/**'
+      - '.github/workflows/bit-frame-ceiling.yml'
+  push:
+    paths:
+      - 'research/bit-frame-ceiling-200/**'
+      - '.github/workflows/bit-frame-ceiling.yml'
+
+jobs:
+  ceiling:
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        python-version: ['3.11', '3.14']
+    steps:
+      - uses: actions/checkout@v4
+      - uses: actions/setup-python@v5
+        with:
+          python-version: ${{ matrix.python-version }}
+      - name: Bit frame-layout ceiling of #200's word, compared with expected.json
+        run: python3 research/bit-frame-ceiling-200/ceiling.py --check

research/bit-frame-ceiling-200/NOTICE

@@ -0,0 +1,28 @@
+Prepared by Chafik Boukhalfa with substantial Anthropic Claude assistance.
+Apache-2.0. Inherited files retain their original notices and assistance
+disclosures. This package claims no exclusive priority over concurrent work
+and reports no new exponent.
+
+Method and lineage:
+- DaysSky: PR192 (research/kappa-ceiling), the frame-layout ceiling of #168's
+  complex word: the moment-root bound a < D/C, the subadditive chain bound,
+  joint frame bounds through both registers of an operation, the exact
+  per-slot dynamic programme and the Lagrangian coupling. ceiling.py carries
+  that method, with the same structure and rigorous arithmetic, to the physical
+  bit word; the rational logarithm bounds and the archive/pin layout follow
+  PR192 directly. PR201 supplies the design ceiling cited in README.md.
+- romainhedouin: PR183, the closed-form acceptance ceiling of the assembly.
+- icekylinx PR144 and eumemic PR117/155/157/161/168: the paired-cube bit word,
+  its exact integer checker check_paired_cube_bit.py (pinned here byte for
+  byte from PR200's vendored copy of PR168 v4) and the physical ledger whose
+  chains ceiling.py mirrors.
+- jamesyc / James Chang: PR166 terminal-output accumulation, whose bit form in
+  PR200 (bit/terminal.py) fixes the sink substitution used here.
+- The word itself: Chafik Boukhalfa, PR200 at
+  a1175449f34d39ff933d9d8ab23ced1f32b290ec (research/paired-cube-diagonal-bit-168),
+  with Anthropic Claude and OpenAI Codex assistance. The eight files read are
+  pinned in SOURCE.json and carried in baseline-pr200.tar.gz.
+- The banked ledger priced alongside is the completed-entrance-bank accounting
+  of Dugongue PR186, Evan McKinney PR197, Rohan Arun PR205, EcmaXp PR206 and
+  Dugongue PR207 on this word; their bank constructions are not re-verified
+  here and the ceiling does not depend on them.

research/bit-frame-ceiling-200/PROOF.md

@@ -0,0 +1,131 @@
+# A frame-layout ceiling for #200's physical bit word
+
+This note proves an upper bound on the coarse bit saving, and hence on κ, that any choice of operation frames for
+the physical bit word of #200 can certify, and applies it to the two ledgers in use on that word: #200's own and the
+completed-entrance-bank ledger of #205, #206 and #207. It makes no κ claim and changes no existing file. The method
+is DaysSky's #192 (`research/kappa-ceiling`), carried from #168's complex word to this bit word; the facts below
+restate #192's with the bit ledger in place of the complex one. `ceiling.py` evaluates every bound with exact
+integers and checks its own model against #200's certified ledger child for child.
+
+## Setting
+
+A shared-core bit supplier is described per group vertex by `W` roles, `m = 3h`, and a multiset of children: `n_r`
+children of width `r`, `0 < r < m`. Its rank mass telescopes, `Σ_r r·n_r = W·m − D` with `D = 2v − 3ℓ`
+(`v` ports, `ℓ` the copied-centre loss). Write `f(r) = r·ln(m/r)` and `C = Σ_r n_r·f(r)`. The repository certifies a
+coarse saving `a` when an exact upper bound on the paid moment `Σ n_r·(r/(W·m))·(m/r)^a` plus the positive bad-class
+term is below 1 (`bit/prove.py`, `arithmetic/interval_moment.py` in #200). So a certified `a` satisfies
+
+    Σ_r n_r·r·(m/r)^a < W·m.                                                     (∗)
+
+**Fact 1 (moment root, #192 Lemma 1).** If (∗) holds then `a < D/C`, since `(m/r)^a ≥ 1 + a·ln(m/r)`. On #200 the
+certified coarse saving lies 0.088% below `D/C` (`ceiling.py`, fact 1).
+
+**Fact 2 (assembly and bootstrap).** #183 (romainhedouin) gives the balanced assembly's acceptance region in closed
+form: κ below `G_η(a) = a(1−2η)(1−η)/(1 + a(1−2η))`, increasing in `a` and decreasing in `η`, so `κ < a/(1+a)` for
+every `η > 0`. The ordinary-leaf wrapper gives `A_B = (1−θ)·a + θ·a_old < a`. The finite stopped-leaf bootstrap of
+#185/#197/#207 produces `a_j = (1−c)·c + c·a_{j−1} < c` at every level from the coarse saving `c`. Hence every κ
+built on this word by any of these assemblies satisfies `κ < G(min(bit, complex)) < G(bit coarse) ≤ G(D/C)` with the
+bit ledger's `D` and `C`.
+
+**Fact 3 (chains, #192 Lemma 3).** `f` is strictly subadditive on `(0, m)`, so a chain of steps of total width `t`
+costs at least `f(t)`; splitting a frame climb into more steps only costs more.
+
+## Fact 4: the frame floor of the fixed word
+
+The certified bit ledger (`scripts/paired_cube_bit_physical.py` of PR168 v4, re-counted by #200's `bit/word.py` and
+`bit/terminal.py`) consists of, per vertex:
+
+- three times the steps of every physical slot's frame chain, where a slot starts at 0, at its source line `⟨χ_S⟩`
+  or at its gauge `σ`, passes the frame of each of its operations in execution order, its root frame if it is a root,
+  and ends at the full space; a recipient continues its donor's slot through the exact step into its gauge;
+- three times the source-injection children of width 1 and the copied-centre children (width `dim` of the centre);
+- three times the partner-chain (source data) steps, fixed by the partner chronology `kchron`;
+- three times the target-chain steps, fixed by the gauges' targets and read order, the side-root frames and the
+  partner deliveries;
+- one child of width `3·dim σ` per gauged first occupant that is not a recipient (the entrance tails);
+- `2v` children of width 2.
+
+`ceiling.py` rebuilds this multiset from the word with #200's own operation frames and checks that it equals
+`overridden_profile.child_histogram` of #200's certificate exactly (W 20,668; rank 1,486,160), and that subtracting
+the terminal record gives `profile.child_histogram`.
+
+Fix the word: its DAG, operations and execution order, sources and source frames, gauges and read chronology, reuse
+pairs, partner chronology, root frames and terminal sinks. The free choice is the frame `F_i` of each operation. An
+admissible layout satisfies, as checked by the retained physical checker before the terminal record is applied:
+`span(x_i) ⊆ F_i`; both registers of operation `i` are at `F_i` while it runs; every slot's frames nest along its
+chain; a donor's last frame lies inside its recipient's gauge; a root is read at its root frame.
+
+**Lemma 4a (joint bounds).** Every admissible layout has `L_i ⊆ F_i ⊆ U_i`, where `L_i = span(x_i) + L_prev(a) +
+L_prev(b)` runs forward in execution order from the registers' entrance frames and `U_i = U_next(a) ∩ U_next(b)` runs
+backward from root frames, recipients' gauges (for donors) and the full space. *Proof.* Both registers sit at `F_i`,
+so `F_i` contains everything below either register's previous frame and lies inside everything above either
+register's next frame; the ends of every chain are fixed. ∎ Values only move between registers through operations,
+whose shared frame links both chains, so this backward pass already carries every root constraint reachable from
+`x_i`. `ceiling.py` checks that #200's layout, and #207's 302-frame layout when given, satisfy every bound.
+
+**Lemma 4b (slot floor).** For each slot, take the minimum of `Σ f(steps)` over nondecreasing dimension sequences with
+`d_i ∈ [dim(cumulative L), dim(cumulative U)]` at each event; exact events (gauge of a recipient, root frame) are
+fixed; the sequence starts at the entrance dimension and ends at `h`. The sum over slots is at most the slots' cost in
+every admissible layout. *Proof.* As in #192: only the coupling between the two registers of an operation and the
+subspace structure are dropped. ∎
+
+**Lemma 4c (coupling).** For any integer prices `λ_i`, adding `+λ_i·d` to the destination register's cost and `−λ_i·d`
+to the control register's cost at operation `i` keeps the sum of per-slot minima a lower bound, since both registers
+share `d = dim F_i` in any admissible layout. ∎ `ceiling.py` runs subgradient rounds on the prices, keeps the best
+round and asserts every round's total lies below #200's own layout cost.
+
+**The terminal record.** #200's `bit/terminal.py` (the bit form of #166) deletes each sink register and copies its
+rank increments to a pivot target; the certified substitution removes, per sink and stage, exactly the sink's last
+step (root frame to full space, width `h − dim root = 3`, present in every layout since the root frame is fixed) and
+one target child of width 21 (the pivot's cap read, fixed by the gauges and roots), and keeps every other step
+charged. `ceiling.py` checks this against the certificate's `child_delta` (−102 of width 3, −102 of width 21) and the
+pre/post target histograms, so the floor of the terminal ledger is the pre-sink floor minus this fixed cost. #207
+audits the same −102/−102 substitution on its layout.
+
+**The two ledgers.** `C_own` includes the entrance tails `3·dim σ`; `C_banked` omits them, which is the only ledger
+change the completed-entrance-bank construction of #205/#206/#207 makes to the children (their `W` changes do not
+enter `D/C`). Both floors share the slot floor and the fixed parts. Hence, for every admissible frame layout of this
+word,
+
+    coarse_own < D / C_own,floor      and      coarse_banked < D / C_banked,floor,
+
+and `κ < G(·)` of each.
+
+**Arithmetic.** Every logarithm is a rational lower bound (partial sums of `2·atanh`, nonnegative terms, truncation
+below `3^-80`), every `f(r)` is rounded down on the grid `2^-64`, and all sums, the dynamic programme and the prices
+are exact integers. The printed ceilings are rounded up on the `10^-7` grid.
+
+## Result
+
+`ceiling.py --check` (1,200 Lagrangian rounds, about 2.5 minutes, stdlib only) on the pinned files of #200 gives:
+
+| Ledger | Floor on C | Coarse saving ceiling | κ ceiling | Certified layout |
+|---|---:|---:|---:|---|
+| #200's own (entrance tails charged) | 2,804,210 | **6.904e-4** | 6.900e-4 | #200's coarse 6.7777e-4 is 98.2% of the ceiling |
+| completed entrance banks (#205/#206/#207) | 2,780,144 | **6.964e-4** | **6.959e-4** | #207's bit coarse 6.8366e-4 (D/C 6.8427e-4) is 98.2% of it |
+| without coupling the two registers of an operation | | 7.056e-4 / 7.118e-4 | | |
+
+The deficit is `D = 2v − 3ℓ = 1,936` (`v = 1,760`, `ℓ = 528`, `h = 24`, `m = 72`); the word has 41,288 operations,
+18,908 roles, 1,760 reuse pairs and 34 sinks. `--overrides` on #207's `frames/opframe-bases.json` confirms that its
+302-frame layout lies inside every joint bound and above the floor.
+
+Consequences.
+
+- Every frame refinement still possible on this word is worth at most +1.8% on the bit side under either ledger.
+- The complex supplier used with this word (#202's source-assisted word, coarse 7.00918e-4, itself within 0.01% of
+  #192's 7.010e-4 ceiling for its own frames) can never become the binding branch: the bit ceiling 6.964e-4 lies below
+  it. So every κ assembled from this bit word and any complex word at or below that ceiling stays below 6.959e-4, no
+  matter how the bit frames are chosen. Going further needs a different bit word (circuit, reuse, gauges or sinks),
+  a bank construction that removes other children, or a different design (DaysSky's #201 bounds the design at
+  2.5592e-3).
+
+
+## Scope and limits
+
+- The ceiling covers one word: the DAG, operations, sources, gauges, reuse pairs, partner chronology and 34 sinks of
+  #200 at `a1175449`. #205, #206 and #207 keep all of these (#207 changes 302 operation frames), so it covers their
+  rows. It does not bound constructions that change the word, the pairs, the gauges or the sinks, nor a different
+  bank construction that removes other children.
+- Fact 2 uses only that every retained assembly accepts κ below `a/(1+a)` of the binding supplier and that the
+  bootstrap stays below its coarse saving. It does not re-verify any assembly or bank construction.
+- The proofs are elementary and not machine-checked beyond the script's exact arithmetic and self-tests.

research/bit-frame-ceiling-200/README.md

@@ -0,0 +1,42 @@
+# bit-frame-ceiling-200
+
+A rigorous ceiling on the bit coarse saving, and hence on κ, for every operation-frame layout of #200's physical bit
+word, the word shared by #200, #205, #206 and #207. **No new κ; no existing file changes.** The method is DaysSky's
+#192 (`research/kappa-ceiling`), carried from #168's complex word to this bit word.
+
+## Result
+
+For every admissible choice of operation frames on this word (its DAG, operations, sources, gauges, 1,760 reuse pairs,
+partner chronology and 34 sinks fixed, as in #200, #205, #206 and #207):
+
+    bit coarse saving < 6.904e-4  under #200's own ledger,
+    bit coarse saving < 6.964e-4  under the completed-entrance-bank ledger of #205/#206/#207,
+
+and hence κ < 6.900e-4, respectively κ < 6.959e-4, for any assembly built on it. #207's bit side (coarse 6.8366e-4,
+κ = 6.8319e-4) is 98.2% of its ceiling, so frame work on this word is worth at most +1.8% more. The ceiling sits
+below the complex supplier those PRs use (7.009e-4), so that complex word can never become the binding branch on
+this bit word. Going further needs a different bit word, a bank construction that removes other children, or a
+different design. [PROOF.md](PROOF.md) has the statements, proofs and the full table.
+
+
+## Verify
+
+    python3 research/bit-frame-ceiling-200/ceiling.py --check        # stdlib only, about 2.5 minutes; -O is refused
+
+The script rebuilds the eight pinned files of #200 it reads (frozen physical bit word, frames, partner chronology,
+graph, profile, sinks, certificate and the retained PR168-v4 exact integer checker) in a temporary directory from
+`baseline-pr200.tar.gz` after checking the archive's and every file's sha256 against `SOURCE.json`, whose hashes are
+those of commit `a1175449`. Reviewers can confirm the pins with `git show a1175449:<path> | sha256sum`, or rebuild
+the archive byte for byte with `git archive --format=tar a1175449 <paths> | gzip -n -9`. A tampered archive is
+rejected. `--tree PATH` runs on a checkout of #200 instead. `--overrides FILE` prices another layout of the same
+word, for instance #207's `frames/opframe-bases.json`, and checks it against the bounds and the floor.
+
+Self-tests: #200's layout lies inside every derived frame bound; its slot chains reproduce #200's certified pre-sink
+ledger child for child and the terminal substitution; every per-slot floor and every Lagrangian round lies below the
+actual cost. All bounds use exact integers with rounded-down logarithms, so the printed ceilings are upper bounds.
+
+## Files
+
+- `ceiling.py`: the computation; `PROOF.md`: statements and proofs; `expected.json`: the results `--check` compares.
+- `SOURCE.json`, `baseline-pr200.tar.gz`: the pinned inputs.
+- `.github/workflows/bit-frame-ceiling.yml` runs `--check` on Python 3.11 and 3.14.

research/bit-frame-ceiling-200/SOURCE.json

@@ -0,0 +1,18 @@
+{
+ "archive": "baseline-pr200.tar.gz",
+ "archive_sha256": "316aa6942a7a027112a8c38c472c59db025c964021abf2d8b3d8fd0e90b7b075",
+ "commit": "a1175449f34d39ff933d9d8ab23ced1f32b290ec",
+ "files": {
+  "research/paired-cube-diagonal-bit-168/certificate.json": "853afa75980e11ce16b333c28311c4f635e84065867c049fda9916c2419091ed",
+  "research/paired-cube-diagonal-bit-168/references/pr168-v4/research/paired-cube-bit/check_paired_cube_bit.py": "4d7c86cd999a1519e0dfb6dcf33a8f26e442a353c3665a0f06881216a260fbf3",
+  "research/paired-cube-diagonal-bit-168/selected/bit/frames_p12.json.gz": "ad8e2705652b68476713d7647a8592505e222f2b3ccd1728dedce153aac6d462",
+  "research/paired-cube-diagonal-bit-168/selected/bit/graph_p12.json": "31a09a55920e64c8bfbac8b845dc01754c112aa6e207812e2fd1f4939d8f64cb",
+  "research/paired-cube-diagonal-bit-168/selected/bit/kchron_p12.json": "0fab548e84cf5ca7c04e8bd19b5810850463f36e0f92180efe73aeff17105e39",
+  "research/paired-cube-diagonal-bit-168/selected/bit/profile_p12.json": "c44ef8640cbcbcc9bac3a30e13373bd79efddde55d7cea514354ca2cdb60d66d",
+  "research/paired-cube-diagonal-bit-168/selected/bit/sinks.json": "c00ff70c564829d4b97740f92796fc6ce14fbcd5ca519663828650552b80249d",
+  "research/paired-cube-diagonal-bit-168/selected/bit/word_p12.json.gz": "1cb7e8ed45cf542e304fddc4b12247dbb248a0dc84dedbd832f336b2d172793a"
+ },
+ "note": "The exact files of #200 that ceiling.py reads (the frozen physical bit word, frames, partner chronology, graph, profile, terminal sinks, certificate and the retained PR168-v4 exact integer checker), byte for byte from commit a1175449; reproducible with: git archive --format=tar a1175449 <paths> | gzip -n -9",
+ "pr": 200,
+ "repository": "CrocSwap/integer-mult-bounds"
+}