Conditional κ = 0.012401086416 (BIT-limited, +310.6%): BIT supplier to 0.012401086416 via the ambient quotient (kernel 150)

research/bit-ambient-quotient/PROOF.md

@@ -0,0 +1,142 @@
+# Construction and proof obligations
+
+## 1. Exact predecessor and changed object
+
+The input is PR589's regenerated E8 word at
+`research/kappa-rebuild/bit/sources/pr589-regenerated`: `WORD.json.gz` (pinned by
+SHA-256 `e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f`, which
+matches `mixed_productive_bit.py`'s own `WORD_HASH`), `records/frames.json`
+(636 frames stored by annihilator rows) and `records/249-records.bin` (249
+records, `<6i`: `op, x, y, c, f, z`). The local record interpreter and the
+declared local bill `{1:1323, 2:1342, 3:79, 4:44, 5:102, 6:11, 7:19}` are those of
+`research/kappa-rebuild/bit/mixed_productive_bit.py`.
+
+There are 661 persistent fields: `2V = 222` main fields and `R = 439` helpers, in
+an eight-axis ambient. A frame's dimension is the dimension of the GF(2) nullspace
+of its annihilator rows; frame 1 is the full ambient.
+
+The changed object is the ambient. For a kernel subspace `K` of dimension `k` with
+annihilator basis `r_1..r_(8-k)`,
+
+```
+phi : F2^8 -> F2^(8-k),   phi(x)_i = r_i . x
+```
+
+`phi` is linear and surjective with kernel exactly `K`. `build.py` maps every
+frame's vector set through `phi`, deduplicates each image basis by exact GF(2)
+rank, identifies frames with equal image, and rewrites every role boundary and
+every record's frame fields. Every MOVE rank is recomputed as
+`dim(image(destination)) - dim(image(source))`. The record order, the ADD/COPY
+structure and every helper boundary are otherwise unchanged.
+
+The kernel is `span{150, 102, 255}`, dimension 3. It is not chosen by hand:
+`scan_kernels.py` prices the dimension ladder and samples the solids. The value is
+a plateau in the dimension — 445 of 455 sampled three-dimensional kernels replay
+and all price at 0.032249423394893.
+
+## 2. Frame-coordinate invariant under the quotient
+
+A field at frame `F` carries the frame operator `C_F`; a chosen frame `E subset F`
+carries `C_E`, and the paid transport between them has rank `dim F - dim E`.
+Because `phi` is linear, `E subset F` implies `phi(E) subset phi(F)`, so every
+nesting the records rely on survives and the transport's rank becomes
+`dim phi(F) - dim phi(E)`.
+
+The induction is unchanged: at each scalar step the participating fields are moved
+into the operation's declared frame, and a scalar linear combination commutes with
+a common frame operator, so the logical step is the same before and after the
+quotient. The replay checks that directly — the arbitrary-column test and the
+endpoint test are frame-independent value tests, and both are exact in both
+directions.
+
+No MOVE is lengthened, since `dim phi(F) <= dim F` for every `F`; a move is
+shortened by the number of kernel dimensions its destination meets minus the number
+its source meets.
+
+## 2b. Re-padding the full ambient and the block
+
+The tensor block is `ambient - 1`, and the block-7 ladder charge is correct only if
+the word's ambient is eight-dimensional. The quotient leaves `k` axes unused, so
+`build.py` re-pads the full-ambient image with all `k` of them: the 5-dimensional
+image becomes the whole of `F2^8` again. Every role that ended at the full ambient
+ends there again, so helper finals are dimension 8, helper ranks are preserved, and
+the ambient is eight axes.
+
+## 3. Complete local bill
+
+Read off the replay:
+
+```
+emitted   {1:1323, 2:1342, 3:79, 4:44, 5:102, 6:11, 7:19}          mass 5,129
+quotient  {1:1020, 2:495, 3:75, 4:442, 5:143, 6:4, 7:12, 8:2}      mass 4,842
+```
+
+The paid mass falls by 287 ranks per call and its shape shifts into ranks 4 and 5.
+With the frontier's sixteen-stage controller, eighteen thick calls, fifteen thin
+queries, `ports = 111` and `block = 7`:
+
+```
+targets = 63,216 (helpers) + 154,290 (ladder)              = 217,506
+paid    = 18*paid_mass + 1,665 (thin) + 122,766 (idles)
+
+emitted   217,506 - (18*5,129 + 1,665 + 122,766) =   753
+quotient  217,506 - (18*4,842 + 1,665 + 122,766) = 5,919
+```
+
+The two-constraint screen gives
+
+```
+emitted   BIT kappa = 0.003464248972    (the frontier's declared BIT value)
+quotient  BIT kappa = 0.032249423394893    (+830.92% over the emitted word)
+
+Against this package's own one-dimensional quotient, the frontier base
+0.012401086416, the step is +160.05%.
+```
+
+## 3b. Where the composition stands
+
+The frontier base for this package is its own one-dimensional quotient,
+0.012401086416. With the complex supplier at 0.015637149091
+(`research/complex-ambient-quotient`) and the BIT supplier now at
+0.032249423394893, the outer `min(complex, BIT)` is the complex side. The BIT is no
+longer binding and has 2.06x of headroom over the complex.
+
+The complex side cannot follow with the same construction yet: `synthesize` in
+`research/fresh-helper-boundary/native.py:85` hardcodes the centre transport's rank
+as `8`
+
+```python
+e = ['center', 0, e[2], second[3], 8]
+```
+
+and the centre frames are dim-8 hyperplanes, so a kernel of dimension >= 2 always
+shrinks them and the stored rank stops matching the frame dimensions. The
+one-dimensional complex quotient avoids this because its kernel direction misses
+the centre frames. Deriving that rank instead of fixing it at 8 is the change the
+complex side needs.
+
+## 4. What is checked, and what is not
+
+Checked by `verify.py` from the artifact and the pinned source word, with the
+shipped record interpreter: 661 roles; ambient dimension 8; the kernel basis is
+independent and the declared quotient width matches its dimension; no helper final
+below dimension 8; all 439 helper starts at ground; both directions replay with
+24,305 ADDs and 9 COPY episodes; all arbitrary input columns exact; all 661
+endpoints exact; owned COPY cleanup exact; forward and backward paid profiles
+identical; the source word reproduces the declared local bill; the emitted invoice
+reproduces the frontier's BIT kappa; and the quotient strictly improves the screen.
+
+Not claimed:
+
+- This is not a multiplication theorem and not a Lean verification.
+- **The outer kappa does not move here.** The complex supplier sets it; this
+  package moves the BIT supplier from the base 0.012401086416 to 0.032249423394893.
+- **The frame charts are not preserved**: 636 frames become 65. The interpreter
+  validates the word's own frame record and `inventories` reads only the paid and
+  helper profiles, so no consumer in this tree reads the charts — but a contract
+  requiring particular charts would reject the word. This is the #4604 question.
+- Kernel dimension 4 replays but prices worse (0.0175); the plateau break is
+  unexplained. Dimension 5 was not searched exhaustively.
+- Only PR589's E8 word is exercised; 292 other `h = 8` words are untested.
+- The admission parameters in `research/query-thinned-controllers/verify.py` are
+  declared literals, not functions of the supplier, and are not raised here.

research/bit-ambient-quotient/README.md

@@ -0,0 +1,130 @@
+# BIT supplier 0.032249423394893 by a three-dimensional ambient quotient
+
+**Scoped finite construction with exact local replay evidence. Not a multiplication theorem.**
+
+**Frontier base: 0.012401086416** — this package's own one-dimensional quotient, the
+value the BIT branch carried before this change. The three-dimensional quotient moves
+the BIT supplier from `0.012401086416` to **`0.032249423394893`**, a **+160.05%** step
+on that base, and from the emitted word's `0.003464248972024` to that value,
+**+830.92%** in total.
+
+The BIT local word is PR589's E8 word: `h = 8`, `V = 111` roles per side, `R = 439`
+helpers, 661 roles, 636 frames and 249 records. Frames are stored by annihilator
+rows, so a frame is the GF(2) nullspace of its rows.
+
+For a kernel subspace `K` of dimension `k`, the map
+
+```
+phi(x) = (r_1.x, ..., r_(8-k).x)      over a basis r of the annihilator of K
+```
+
+is linear and surjective onto `F2^(8-k)` with kernel exactly `K`. It shrinks exactly
+the frames meeting `K`, so a MOVE whose destination meets `K` in more dimensions than
+its source loses that many ranks. Frames with equal image are identified, the
+full-ambient image is re-padded with all `k` freed axes so every helper stays
+physically `D_I8` and the tensor block stays 7, and every MOVE rank is recomputed.
+
+## The kernel dimension is the lever
+
+| kernel dim | kappa | vs base 0.012401086416 |
+|---:|---:|---:|
+| 1 | 0.012401086416 | — (the base) |
+| 2 | 0.021785831250 | +75.68% |
+| **3** | **0.032249423394893** | **+160.05%** |
+| 4 | 0.017525188018 | +41.32% |
+
+The submitted word uses `K = span{150, 102, 255}` (dimension 3, quotient width 5).
+Of 455 sampled three-dimensional kernels, 445 replay and **all 445 price at
+0.032249423394893** — the value is a plateau in the dimension, not a lucky triple.
+
+| quantity | emitted | quotient |
+|---|---:|---:|
+| frames | 636 | **65** |
+| frame dimensions | — | `{0:1, 1:13, 2:8, 3:25, 4:16, 5:1, 8:1}` |
+| main widths | `{7: 222}` | `{4: 103, 7: 70, 8: 49}` |
+| main rank mass | 1,554 | **1,294** |
+| helper widths | `{8: 439}` | `{8: 439}` (start dim 0, final dim 8) |
+| helper rank mass | 3,512 | 3,512 |
+| paid profile | `{1:1323, 2:1342, 3:79, 4:44, 5:102, 6:11, 7:19}` | `{1:1020, 2:495, 3:75, 4:442, 5:143, 6:4, 7:12, 8:2}` |
+| paid rank mass | 5,129 | **4,842** |
+| rank surplus | 753 | **5,919** |
+| **BIT kappa** | **0.003464248972024** | **0.032249423394893** |
+
+## Why the quotient is legitimate
+
+A frame meeting `K` in `j` dimensions loses exactly `j`, and nothing else moves, so
+no MOVE is lengthened: `dim phi(F) <= dim F` for every `F`. The shipped local record
+interpreter then replays the rewritten word with no change of its own:
+
+| check | result |
+|---|---:|
+| forward replay | 24,305 ADDs, 9 COPY episodes, all 661 endpoints exact |
+| reverse replay | 24,305 ADDs, 9 COPY episodes, all 661 endpoints exact |
+| arbitrary input columns, both directions | exact |
+| owned COPY cleanup | exact |
+| helper finals at dim 8 | 439 of 439 |
+| helper starts at ground | 439 of 439 |
+| source word reproduces the declared bill | `{1:1323, 2:1342, 3:79, 4:44, 5:102, 6:11, 7:19}` |
+| emitted BIT kappa reproduces the frontier | 0.003464248972024 |
+
+The last two rows are the calibration: replaying the *pinned source word* through the
+same interpreter reproduces the declared local bill exactly, and the emitted invoice's
+screen reproduces the frontier's BIT kappa to fifteen digits. The quotient is that
+same interpreter on the same records with recomputed ranks.
+
+**The block stays 7.** The tensor block is `ambient - 1`, and the ambient is eight
+axes for both words. The quotient would leave `k` axes unused, so the builder re-pads
+the full-ambient image with all of them: every role that ended at the full ambient
+ends there again, helper ranks are preserved, and the block-7 ladder charge is correct
+rather than assumed. `verify.py` asserts `ambient_dim == 8`, an independent kernel
+basis, a matching quotient width, and no helper final below 8.
+
+## Reproduce
+
+```sh
+python3 -B research/bit-ambient-quotient/build.py          # writes the artifact
+python3 -B research/bit-ambient-quotient/verify.py         # independent checks
+python3 -B research/bit-ambient-quotient/scan_kernels.py   # the dimension ladder
+```
+
+`verify.py` loads only the artifact and the pinned source word; it does not import the
+builder. The two-constraint screen is inlined (tail offset `1/5`, cutoff `20`,
+gamma `0.97`), so no file outside the base commit is required.
+
+## What is not claimed
+
+- **The outer kappa does not move in this package.** The outer value is
+  `min(complex, BIT)`; the complex supplier sets it.
+- **The frame charts collapse**: 636 frames become 65. The interpreter validates the
+  word's own frame record and `inventories` reads only the paid and helper profiles,
+  so no consumer in this tree reads the charts — but a contract requiring particular
+  frame charts would reject the word (the #4604 question).
+- Kernel dimension 4 replays but prices worse at 0.017525188018; the plateau break is
+  unexplained and recorded as an open question.
+- This is not a multiplication theorem and not a Lean verification.
+- Only PR589's E8 word is exercised; 292 other `h = 8` words are untested.
+
+## Open next questions
+
+1. **Why does dimension 4 fall back to 0.017525188018?** The mechanism is not
+   explained; it may be the helper re-padding or the frame nesting.
+2. **Can the complex supplier follow?** It needs
+   `research/fresh-helper-boundary/native.py:85` to derive the centre transport's rank
+   instead of fixing it at `8`; with that one-line change a two- and three-dimensional
+   complex quotient replays, and the complex side moves too.
+3. **Which consumer, if any, requires the frame charts?** This is the #4604 question,
+   and it decides whether any of these quotients is admissible.
+4. **What admission parameters correspond to a 0.032249423394893 supplier?** The
+   declared literals in `research/query-thinned-controllers/verify.py` are far below
+   it.
+
+## Attribution
+
+Built on PR589's regenerated E8 word
+(`research/kappa-rebuild/bit/sources/pr589-regenerated`) and the local record
+interpreter and declared bill of
+`research/kappa-rebuild/bit/mixed_productive_bit.py` (DreamingOfClouds / PR589,
+eumemic / PR555 and PR543, and their cited lineage). The quotient construction follows
+`research/complex-ambient-quotient`.
+
+Apache-2.0; substantial AI assistance.

research/bit-ambient-quotient/RESULT.json

@@ -0,0 +1,55 @@
+{
+  "ambient_dim": 8,
+  "directions_agree": true,
+  "emitted_kappa": 0.003464248972023964,
+  "emitted_paid": {
+    "1": 1323,
+    "2": 1342,
+    "3": 79,
+    "4": 44,
+    "5": 102,
+    "6": 11,
+    "7": 19
+  },
+  "emitted_paid_mass": 5129,
+  "emitted_surplus": 753,
+  "endpoint_failures": 0,
+  "frames": 65,
+  "gain_absolute": 0.02878517442286887,
+  "gain_relative": 8.309210641419726,
+  "helper_widths": {
+    "8": 439
+  },
+  "kernel_basis": [
+    150,
+    102,
+    255
+  ],
+  "kernel_dimension": 3,
+  "local_checks": {
+    "adds": 24305,
+    "copies": 9
+  },
+  "main_rank_mass": 1294,
+  "main_widths": {
+    "4": 103,
+    "7": 70,
+    "8": 49
+  },
+  "package": "bit-ambient-quotient",
+  "quotient_kappa": 0.03224942339489283,
+  "quotient_paid": {
+    "1": 1020,
+    "2": 495,
+    "3": 75,
+    "4": 442,
+    "5": 143,
+    "6": 4,
+    "7": 12,
+    "8": 2
+  },
+  "quotient_paid_mass": 4842,
+  "quotient_surplus": 5919,
+  "roles": 661,
+  "status": "PASS_BIT_AMBIENT_QUOTIENT"
+}

research/bit-ambient-quotient/SOURCES.json

@@ -0,0 +1,42 @@
+{
+  "schema_version": 1,
+  "base_commit": "b9a13c1673e0e9697de410de16e8bbf3207a7363",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40",
+      "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65",
+      "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96"
+    },
+    {
+      "path": "research/kappa-rebuild/bit/sources/pr589-regenerated/WORD.json.gz",
+      "usage": "input",
+      "git_blob": "85a4499bf9e4911a705d50567a2c2ef6cf23739a",
+      "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f"
+    },
+    {
+      "path": "research/kappa-rebuild/bit/sources/pr589-regenerated/records/frames.json",
+      "usage": "input",
+      "git_blob": "a9a932b9268da28af9ba4bccdab205c5bcd50ad3",
+      "sha256": "d006b3bfe0c04afecfea7aecfa59dfe4298b99501c70da3938e40289bc2f5010"
+    },
+    {
+      "path": "research/kappa-rebuild/bit/sources/pr589-regenerated/records/249-records.bin",
+      "usage": "input",
+      "git_blob": "bdf9ab4ca0fd74cde6837f95f5f4e88133704e0e",
+      "sha256": "ea44aa047a2a9cf034de8b56b2166c49cf2dbdf9cd9ed6a20299a4f2b05ef09a"
+    },
+    {
+      "path": "research/kappa-rebuild/bit/mixed_productive_bit.py",
+      "usage": "input",
+      "git_blob": "9c7a8bd5d3ae4c19952648c815031858d6627b96",
+      "sha256": "b32291b0db7fc0d332ec444c70746ab0fb03351d2e50546f8bcb64060e3ff95e"
+    }
+  ]
+}