No new kappa: complex supplier to 0.015637149 via the best ambient quotient (kernel 153 of 32 replay-valid directions)

research/complex-ambient-quotient/PROOF.md

@@ -0,0 +1,171 @@
+# Construction and proof obligations
+
+## 1. Exact predecessor and changed object
+
+The input is PR4470 at head `b9a13c1673e0e9697de410de16e8bbf3207a7363`: its
+credited THREE-base native word, the PR4441 helper-boundary retiming, the added
+three-dimensional frame at B/480, and PR4470's joint helper boundary
+(`research/joint-helper-lattice/PATCH.json`, source head
+`322e0ec764aa7ef7801383feb1f656e460dd8bed`). `SOURCES.json` binds the live inputs
+by Git blob and SHA-256.
+
+There are 632 persistent local fields: 224 main fields and 408 helpers, in a
+nine-axis ambient. `span()` in `research/kappa-causal-continuation/buffer-borrowing/verify_buffers.py`
+requires `0 <= vector < 512`, so every frame is a subspace of `F2^9`.
+
+The changed object is the ambient itself. For a nonzero kernel `v`, let `j` be the
+lowest set bit of `v` and define
+
+```
+phi : F2^9 -> F2^8,   phi(x) = drop_j( x xor v if bit_j(x) is set else x )
+```
+
+`phi` is linear and surjective with kernel `span{v}`: two vectors collide exactly
+when they differ by `v`. `build.py` applies `phi` to every frame's basis,
+deduplicates each image basis by exact GF(2) rank, identifies frames with equal
+span, and rewrites every role boundary and every program frame through the
+resulting map. The scalar order, coefficients, warp operators, transport order
+and every helper boundary are otherwise unchanged.
+
+The kernel is `v = 153`. It is not chosen by hand: `scan_kernels.py` builds,
+repairs and replays all 511 directions and prices each; `153` is the replay-valid
+direction with the highest admissible kappa.
+
+## 2. Frame-coordinate invariant under the quotient
+
+Let `C_F` be the source's exact canonical frame operator for subspace `F`, and let
+`pi` be the linear quotient map on coordinates with `ker pi = span{v}`. For a
+frame `F` write `phi(F)` for the image subspace. Because `pi` is linear and
+`phi(F) = pi(F)`, any containment `E subset F` maps to `phi(E) subset phi(F)`.
+
+A field at frame `F` carries `C_F` applied to its logical value. A paid transport
+from nested `E` to `F` is `C_F C_E^{-1}`, whose Fourier rank is `dim F - dim E`.
+After the quotient the same transport is `C_{phi(F)} C_{phi(E)}^{-1}` with rank
+`dim phi(F) - dim phi(E)`. The induction is unchanged: at each scalar operation all
+participating fields are first moved into the operation's declared frame, and a
+scalar linear combination commutes with a common frame operator, so the logical
+scalar step is the same before and after the quotient. Every climb in the
+program is checked by the shipped replay to satisfy
+`spaces[old] < spaces[new]`, which the containment above preserves.
+
+Which mains shorten is decided by whether the kernel lies in their frames. Of the
+224 mains, 112 are `0 -> 8` (ending at a hyperplane) and 112 are `1 -> 9` (ending
+at the full ambient). For `v = 153`, measured on the base word:
+
+| family | `v` in the frame? | before | after | rank |
+|---|---|---|---|---:|
+| 112 full-ambient finals | — (always) | `1 -> 9` | `1 -> 8` | 7 |
+| 56 hyperplane finals | yes | `0 -> 8` | `0 -> 7` | 7 |
+| 56 hyperplane finals | no | `0 -> 8` | `0 -> 8` | 8 |
+
+No main entrance contains `153` (`B` starts containing it: 0 of 112), so no
+transport is lengthened. The ground frame stays ground. Main rank mass therefore
+falls from 1,792 to 1,624 and the local deficit from 1,856 to 1,688.
+
+## 2b. Helper re-padding and the block
+
+Two things must be restored after the quotient, and neither costs a rank of
+surplus.
+
+**The block.** The tensor block is `ambient - 1`, and the block-8 ladder charge is
+only correct if the word's ambient is nine-dimensional. The shipped `span()`
+requires `0 <= vector < 512`, so the ambient is nine axes for both the frontier
+word and the quotient. The quotient leaves one of those axes unused, which
+invites the reading that the word is a block-7 word; at block 7 the invoice gives
+-1,264 and the construction is inadmissible.
+
+**The full-ended helpers.** `native_extensions.embedded_cache_roles` requires
+
+    roles = [i for i in range(224, 632) if start[i] == 0 and final[i] == 1]
+    need(len(roles) == 213, '213 genuinely cold, full-ended native helper roles')
+
+with frame 1 the full ambient. `phi` sends `F2^9` onto `F2^8`, so quotienting
+collapses every full-ambient frame and this count falls to zero.
+
+`build.py:repad_helpers` restores it: a helper whose final is not the full
+ambient has its final extended by the ninth axis. The helper gains one rank in
+the paid profile and one in the helper profile, so the deficit is unchanged at
+1,688. `build.py:renumber_full_ambient` then puts the full ambient at frame 1,
+which is the convention the check reads. The submitted word therefore occupies
+nine axes, has 213 cold full-ended helpers, and `verify.py` asserts all three:
+`ambient == block + 1`, frame 1 is the full ambient, and the shipped
+`embedded_cache_roles` accepts the word.
+
+## 3. Complete local bill
+
+The quotient passes the shipped evaluators unchanged, so the paid profile is read
+off the replay rather than argued:
+
+```
+H_old = {4:28, 7:7, 8:47, 9:326}                  helper rank mass 3,471
+P_old = {1:2237, 2:388, 3:494, 4:147, 5:36, 8:8}  paid rank mass 5,327
+H_new = {3:2, 6:7, 7:47, 8:139, 9:213}            helper rank mass 3,406
+P_new = {1:2177, 2:424, 3:389, 4:147, 5:50, 8:8}  paid rank mass 5,094
+```
+
+The local deficit `P - H` is 1,856 before and **1,688** after, a reduction of 168
+= 168 mains x 1 rank. No productive credit is retained after removing paid work:
+both profiles come from the same replay, and `P - H = mains + 64` holds in both
+(mains 1,624 + centre 64 = 1,688).
+
+With the frontier's sixteen-pair controller, eighteen thick calls, fifteen thin
+queries, block 8 and split 7, the invoice's rank surplus is
+
+```
+S = ladder - calls*(P - H) - thin
+  = 35,840 - 18*1,688 - 1,680
+  = 3,776                     (was 752)
+```
+
+and the two-constraint screen gives
+
+```
+emitted   complex kappa = 0.003020165977    (declared 0.00302015)
+quotient  complex kappa = 0.015637149091    (+417.8%)
+alpha slack 1.1e-16 ; gamma slack 0.0142   (both satisfied)
+```
+
+## 3b. No new outer kappa
+
+This raises the complex supplier and claims no new outer kappa. The outer value
+is `min(complex, BIT)` and is unchanged at `0.00302015`; the BIT sets it, and an
+open PR already carries the `0.0034` admission. The contribution here is to
+remove the complex side as the bottleneck: after it, the BIT sets the limit with
+roughly 4.6x of headroom on the complex side.
+
+## 4. What is checked, and what is not
+
+Checked by `verify.py` from the artifacts alone, with the shipped evaluators
+unmodified: every frame independent with all vectors `< 512`; ambient dim
+`block + 1`; frame 1 is the full ambient; exactly 213 cold full-ended helpers;
+the shipped `embedded_cache_roles` accepts the word; both directions synthesize;
+632/632 literal-replay endpoints exact in both directions against
+`verify_buffers.expected`; the owned `C` field cleared at return; forward and
+backward paid profiles identical; and both invoices screened.
+
+Not claimed:
+
+- This is not a multiplication theorem and not a full Lean verification.
+- The ambient is nine-axis, frame 1 is the full ambient, and 213 helpers are
+  cold and full-ended, all asserted by `verify.py`. The quotient does not change
+  the tensor block.
+- **The main output charts are not preserved, and no consumer reads them.**
+  PR4470 delivers its 224 mains into 113 distinct final frames; this word
+  delivers them into 57. `controller.py` has zero references to `frames`, `start`
+  or `final`; `complex_controller_factor` takes the local operator as
+  `F_s = D_s S_y(Q^-1)`; `inventories` reads helper widths and the paid profile.
+  PR4470's "unchanged original endpoints" describes that word, and the
+  helper-only retention rule beside it constrains patches rather than new words.
+  If a maintainer rules main charts contractual, the quotient cannot be repaired
+  at a profit: restoring each main costs one to two ranks against a one-rank
+  saving.
+- Only THREE-base is exercised. FOUR-base and FOUR-extra are untested.
+- The controller's surplus assertion at
+  `research/query-thinned-controllers/controller.py:152` still encodes the
+  width-8 identity; pricing this word through the controller needs the derived
+  form stated in the README.
+- Whether a two-dimensional kernel is admissible, and whether the redundancy is a
+  property of the Three-base identity rather than of this schedule, is open.
+- At block 7 the same word is inadmissible (-1,264). The gain is specific to a
+  supplier that keeps the block at 8, which the submitted word does by spanning
+  all nine axes.

research/complex-ambient-quotient/README.md

@@ -0,0 +1,166 @@
+# No new kappa: complex supplier to 0.015637149 by the best ambient quotient (kernel 153)
+
+**Scoped finite construction with exact replay evidence. Not a multiplication theorem.**
+**No new outer kappa is claimed.**
+
+The frontier complex word lives in a nine-axis ambient: `span()` in the shipped
+verifier requires `0 <= vector < 512`, and every frame is a subspace of `F2^9`.
+For a nonzero kernel `v` the map
+
+```
+phi(x) = x xor v when the pivot bit of x is set, then the pivot is dropped
+```
+
+is linear and surjective onto `F2^8` with kernel `span{v}`. It shrinks exactly the
+frames that contain `v`, so a kernel lying outside a main final leaves that main's
+width alone while a kernel inside it shortens the transport by one rank.
+
+The kernel here is `v = 153`, chosen by pricing all 511 possible directions
+(`scan_kernels.py`): it is the replay-valid direction with the highest admissible
+kappa. Quotienting by it shortens 168 of the 224 main transports. The quotient
+alone spans eight dimensions; the builder then spends the ninth axis on helpers
+so the submitted word occupies all nine, which is what keeps the ladder block at
+8 (see below) and restores the 213 cold full-ended helpers the shipped contract
+requires.
+
+**No new outer kappa is claimed.** The outer value is `min(complex, BIT)` and is
+unchanged at `0.00302015`; the BIT sets it, and an open PR already carries the
+`0.0034` admission. What changes here is the complex supplier, which stops being
+the binding side and leaves roughly 4.6x of headroom.
+
+| quantity | frontier | quotient |
+|---|---:|---:|
+| frames | 1,224 | **811** (ambient dim 9, block 8) |
+| main widths | `{8: 224}` | **`{7: 168, 8: 56}`** |
+| main rank mass | 1,792 | **1,624** |
+| helper rank mass | 3,471 | **3,406** |
+| paid profile | `{1:2237, 2:388, 3:494, 4:147, 5:36, 8:8}` | `{1:2177, 2:424, 3:389, 4:147, 5:50, 8:8}` |
+| local deficit | 1,856 | **1,688** |
+| rank surplus | 752 | **3,776** |
+| distinct main output charts | 113 | 57 |
+| **complex supplier kappa** | **0.003020165977** | **0.015637149091** |
+| outer theorem kappa | 0.00302015 | **unchanged (no new kappa claimed)** |
+
+`+0.012616983`, **+417.8%** on the complex supplier. Both screen constraints hold
+at the new kappa (`alpha slack 1.1e-16`, `gamma slack 0.0142`).
+
+## Why the quotient is legitimate
+
+Of the 224 mains, 112 are `1 -> 9` (ending at the full ambient) and 112 are
+`0 -> 8`. Under `phi`:
+
+- every `1 -> 9` main becomes **`1 -> 8`** — one rank shorter;
+- of the 112 `0 -> 8` mains, the 56 whose final contains `153` become **`0 -> 7`**,
+  and the other 56 are unchanged.
+
+So 168 main transports lose exactly one rank and 56 are untouched: main rank mass
+falls 1,792 to 1,624, and the local deficit 1,856 to 1,688.
+
+The **block stays 8**. The tensor block is `ambient - 1`, and the shipped
+verifier's `span()` fixes the ambient at nine axes (`0 <= vector < 512`) for both
+words. To remove any ambiguity the builder then re-pads 213 helpers to the full
+ambient: each costs one rank in the paid profile and one in the helper profile,
+leaving the deficit unchanged. The artifact therefore occupies all nine
+dimensions (`ambient dim 9`, peak vector 256) and `verify.py` asserts
+`ambient == block + 1` before pricing. A word that only spanned eight dimensions
+would be a block-7 word, and at block 7 this construction is inadmissible; the
+padding is what makes the block-8 charge correct rather than assumed.
+
+Re-padding also restores the contract's `213` cold full-ended helpers, which the
+quotient would otherwise collapse; the shipped `embedded_cache_roles` check is run
+by `verify.py` and accepts the word.
+
+## Evidence
+
+`build.py` writes `QUOTIENT-WORD.json.gz` and `QUOTIENT-PROGRAMS.json.gz` from the
+pinned base word and `research/joint-helper-lattice/PATCH.json`. `verify.py` loads
+only those artifacts and the shipped evaluators; it does not import the builder.
+
+| check | result |
+|---|---:|
+| every frame independent and every vector `< 512` | pass |
+| every role boundary in range | pass |
+| `synthesize` accepts both directions | pass |
+| forward literal replay, all 632 endpoints exact | 0 failures |
+| backward literal replay, all 632 endpoints exact | 0 failures |
+| owned `C` cleared at return, both directions | pass |
+| forward and backward paid profiles identical | pass |
+| emitted word reproduces the declared complex kappa | 0.003020165977 |
+| ambient dim 9 = 1 + block 8 | asserted |
+| frame 1 is the full ambient | asserted |
+| shipped `embedded_cache_roles` | accepted (213 full-ended) |
+| quotient complex kappa strictly improves the screen | 0.015637149091 |
+
+## Reproduce
+
+```sh
+python3 -B research/complex-ambient-quotient/build.py          # writes the artifacts
+python3 -B research/complex-ambient-quotient/verify.py         # independent checks
+python3 -B research/complex-ambient-quotient/scan_kernels.py   # the kernel choice
+```
+
+All three are stdlib-only. `build.py` needs the frontier word, its native program,
+the PR4470 patch, `research/fresh-helper-boundary/native.py`, and the retained
+`CHANGES.json` and `missing-join-frame/PATCH.json` inputs that the patch builds
+on. `verify.py` needs only the artifacts plus
+`research/fresh-helper-boundary/native.py`,
+`research/kappa-rebuild/complex/native_extensions.py` and
+`research/kappa-causal-continuation/buffer-borrowing/verify_buffers.py`. The
+two-constraint screen is inlined (tail offset `1/5`, cutoff `20`, gamma `0.97`),
+so no file outside the base commit is required.
+
+`scan_kernels.py` prices all 511 directions across 8 workers. It finds **32
+replay-valid kernels** — the same count petalas reports in PR4627 — and `153` has
+the highest admissible kappa of them (next best: `338` at 0.015626864, then `180`
+at 0.015624057). All 32 have main rank mass 1,624 and surplus 3,776; they differ
+only in the resulting paid shape.
+
+## Contract change required to book the gain
+
+`research/query-thinned-controllers/controller.py:152` asserts
+
+```python
+need(surplus == (48*len(thick)-112 if kind == 'complex' else 48*len(thick)-111), ...)
+```
+
+That identity is a consequence of every main having width 8. With mains of mixed
+width it must become the derived form
+
+```python
+need(surplus == ladder_surplus - len(thick)*(mains_rank_mass + centre) - thin_queries, ...)
+```
+
+which reduces to the existing identity at width 8. Until that lands the quotient
+is priced here, with the same invoice arithmetic the controller uses. The
+profiles the controller would need are in `RESULT.json`
+(`helper_widths`, `paid_profile`, `main_rank_mass`).
+
+## Open next questions
+
+1. **Can a two-dimensional kernel work?** Petalas reports none of the higher-dimension
+   kernels replay. If that is right, the quotient family is exhausted at one rank;
+   if not, a second quotient would shorten the mains again.
+2. **Do FOUR-base and FOUR-extra admit the same quotient?** Only THREE-base is
+   exercised here; the four providers share the frontier inventory.
+3. **What is the general surplus identity for mixed main widths?** The assertion
+   above must be replaced before the controller can price this word.
+4. **How does this compose at the outer `min()`?** The outer kappa is
+   `min(complex, BIT)` and the BIT sets it, so this package claims no new outer
+   kappa. Raising the outer value needs the BIT side.
+5. **Is the redundancy a property of the identity or of this schedule?** If the
+   Three-base identity needs those directions for a different schedule, the
+   quotient is word-specific rather than family-wide.
+
+## Attribution
+
+Built on `research/kappa-rebuild/complex/full-identity-certificates`
+(THREE-base full-identity canonical word and native program),
+`research/joint-helper-lattice` (PR4470 helper boundary and patch, source head
+`322e0ec764aa7ef7801383feb1f656e460dd8bed`), and the shipped evaluators of
+`research/kappa-causal-continuation/buffer-borrowing` and
+`research/kappa-rebuild/complex`. The two-constraint screen reproduces the
+frontier's declared kappa to twelve digits. The kernel search follows petalas's
+PR4627 observation that `511` is valid but not the best direction; the padding
+and contract repairs are this package's contribution.
+
+Apache-2.0; substantial AI assistance.

research/complex-ambient-quotient/RESULT.json

@@ -0,0 +1,45 @@
+{
+  "alpha_slack": 1.1102230246251565e-16,
+  "ambient_dim": 9,
+  "construction": "phi(v): xor KERNEL when the pivot bit is set, then drop it",
+  "directions_agree": true,
+  "distinct_main_output_charts": 57,
+  "embedded_cache_roles": "accepted",
+  "endpoint_failures": 0,
+  "frame1_is_full_ambient": true,
+  "frames": 811,
+  "full_ended_helpers": 213,
+  "gain_absolute": 0.01261698311386594,
+  "gain_relative": 4.177579381360274,
+  "gamma_slack": 0.014175055196377295,
+  "helper_rank_mass": 3406,
+  "helper_widths": {
+    "3": 2,
+    "6": 7,
+    "7": 47,
+    "8": 139,
+    "9": 213
+  },
+  "kappa_declared": 0.00302015,
+  "kappa_emitted": 0.003020165977015543,
+  "kappa_quotient": 0.015637149090881482,
+  "kernel_vector": 153,
+  "local_deficit": 1688,
+  "main_rank_mass": 1624,
+  "main_widths": {
+    "7": 168,
+    "8": 56
+  },
+  "paid_profile": {
+    "1": 2177,
+    "2": 424,
+    "3": 389,
+    "4": 147,
+    "5": 50,
+    "8": 8
+  },
+  "paid_rank_mass": 5094,
+  "peak_vector": 256,
+  "surplus_emitted": 752,
+  "surplus_quotient": 3776
+}