Scoped negative result: no frame reassignment of the selected X4 complex word admits the next tick (exact duals, no new kappa)

research/complex-x4-frame-bound/CLAIM.md

@@ -0,0 +1,18 @@
+# Local sprint claim
+
+No pinned sprint coordination issue existed on 2026-10-13 (the only open issue was #650), so the claim is recorded here.
+
+- Track: 20–39, complex supplier. Seed **28**, drawn from the operating system's CSPRNG with Node.js `crypto.randomInt(1, 61)` at 2026-10-13T07:45:49Z (range 1–60 as instructed for this run).
+- Base commit: `f567884aeb8851b6e794af1184119a3bfbe1e631` (selected κ = 0.001661634653669567, #799 with #589 on #555; the complex side binds).
+- Object: the frame schedule of the selected complex word, PR799's X4 word (content `1e1d99ba…`), all A, B and early-cleanup gates.
+- Method: complete F₂ frame intervals, local-polytope LP and symbolic exact duals (the #557 method), with a standard-library verifier and two pinned moment engines.
+- Expected deliverable: a constructed frame improvement if the LP found one, otherwise a scoped exclusion at the next 10⁻²⁴ tick.
+- Expected finish: same day.
+
+## Candidates considered
+
+1. **Residual low-end capacity on X4.** For each helper ending at FULL, join the end-of-B frames over its inverse-row and dirt-column cones (the two cone conditions of `audit_local.py`). Result: all 216 fresh and 162 entering FULL-ending helpers have a 9-dimensional join, so no new low end exists without a scalar change. This matches the p6n note's "2 a-type units" estimate, which concerns new premix directions rather than the fixed program. Not packaged.
+2. **Joint entrance-promotion and frame search.** Every entering helper's first gate sits exactly at its entrance frame, so any promotion must raise a partner's frame. Pricing a promotion needs the owner-packing model, because freed width changes the idle profile (#850 covers only the current inventory). A rough packing-free bound, pricing all idle mass as rank-51 children, gains about 11.6 moment units (×mW) from repacking alone, roughly 17 times the X4 step (0.67), so it decides nothing. Not pursued.
+3. **Exact frame-assignment optimality of X4 (chosen).** #815 covers PR699's SW4 word with floating-point solvers and fixed tail frames, and #776 covers #626's words. The #799 review keeps the X4 frame-optimality report as a search report. No open PR claimed X4 when this work started (snapshot through #857).
+
+Overlap was refreshed again before submission; see the pull request description.

research/complex-x4-frame-bound/README.md

@@ -0,0 +1,75 @@
+# Frame reassignment cannot raise the selected X4 complex supplier
+
+**Scoped negative result. No new κ.** Base `f567884aeb8851b6e794af1184119a3bfbe1e631`, where the selected κ = 0.001661634653669567 comes from #799 with #589 on #555 and the complex side binds. Complex-supplier sprint track, OS seed 28 (see `CLAIM.md`).
+
+## Claim
+
+Fix the scalar program of the selected complex word, PR799's X4 word (decompressed content `1e1d99ba…`), which serves all 72 complex calls. Keep its gate list and order, registers, coefficients, start and end frames (so every helper width), cut, centres, target levels, precondition, FULL cleanup and the set of early-cleanup (tail) gates. Let each of its 6,364 A, B and tail gate frames be any subspace of F₂⁹ allowed by the frame contract that `research/gauge44-frames-x/independent/audit_local.py` checks:
+
+- frames are nested along every register, from its start frame to its end frame;
+- centres and targets sit at their centre frame and target level at the start of B;
+- for each of the 126 low-end helpers, every register in its inverse-row or dirt-column cone ends B inside that helper's end frame.
+
+No such assignment admits the native complex saving
+
+    b_next = 832200139425241163957/500000000000000000000000 = 0.001664400278850482327914,
+
+the next 10⁻²⁴ grid point above the selected endpoint `0.001664400278850482327913`. Every child rank is below 73, so no larger b is admitted either. The pinned outer engine (`outer.py`) requires κ < ε·q = (1−η)q/(1+q) with q = a(1−2η) (`compact_phase_layer`) and a < b (`complex_above_bit`), so κ < b/(1+b). Since b_next/(1+b_next) = 0.0016616346536695670758… lies below the next κ tick 0.001661634653669568, frame reassignment alone cannot raise the selected κ.
+
+## Proof outline
+
+1. **Domains.** Forward joins from fixed starts and start-of-B pins give a lower frame `lo`. Backward meets from fixed ends, pins and cone ceilings give an upper frame `hi`. By induction every legal frame lies in `[lo, hi]`. Here `dim(hi/lo) ≤ 3`: 5,163 gates are forced and 1,201 have 2, 5 or 16 choices (965, 206 and 30 gates). The verifier enumerates each interval and checks its size against the Gaussian-binomial count.
+2. **Cost.** A strict climb of dimension d along a register is one paid child of rank d (the `audit_local.py` rule). Climbs telescope along each register, so rank mass is fixed. The native moment then depends on the assignment only through C_d = M_d − d·M₁ with M_d = d·(73/d)^b, and C₀ = C₁ = 0.
+3. **LP.** Free gates linked along register chains form 140 components. Each component's local-polytope LP has a variable for every (gate, frame) and for every nested frame pair on each merged register edge: 9,483 rows and 12,019 columns in total. Every legal assignment is a 0/1 point.
+4. **Exact duals.** Each dual entry is a linear form in C₂…C₉ with integer coefficients. The verifier rebuilds every row, column and cost from the word, then checks every reduced cost. 8,582 are identically zero, and 3,437 are strictly positive under outward rational bounds from both pinned engines (`moment.py`, Mercator series, and `base_two_moment.py`, atanh series). In every component the dual objective equals the selected assignment's cost as an exact coefficient identity. By weak duality the selected frames minimise the local moment.
+5. **Global step.** 72 times the local profile plus the remainder {1:1, 3:1, 44:1, 48:2396} reproduces the pinned global profile. Both engines put the global moment strictly above 1 at b_next and strictly below 1 at the selected endpoint. Each call costs at least the selected word, so any reassignment, even a different one in each call, has moment above 1 at b_next.
+
+The model relaxes the centre equality at the start of B to a charged climb, and it omits native-chain conditions beyond `audit_local.py`. Both choices only enlarge the feasible set, so the bound also covers the stricter native contract.
+
+## Cross-check against the independent auditor
+
+`crosscheck.py` draws 12 random legal reassignments (40 frame changes each, seed 28), writes each into the word with the profile the model predicts, and runs the pinned `audit_local.py` unchanged. All 12 pass its exact two-orientation scalar replay and its frame, centre, target and cone checks with the predicted profile. All 12 are strictly costlier at b_next. The auditor refuses a frame below the forward join and a mismatched profile. Receipt: `data/CROSSCHECK.json`.
+
+## Reproduce
+
+Python 3.11 or newer, standard library only, assertions on, from the repository root:
+
+```sh
+python3 -B research/complex-x4-frame-bound/verify.py --controls
+```
+
+Expected final line: `PASS_X4_FRAME_ASSIGNMENT_EXCLUSION controls=6/6`, in about 5 seconds. The six controls must each be rejected: a dropped component, an inflated dual, an omitted frame choice, the accepted endpoint in place of b_next, a legal but costlier baseline, and a changed word. `RESULT.json` is the receipt of this command.
+
+Optional commands:
+
+```sh
+python3 -B research/complex-x4-frame-bound/crosscheck.py      # about 1 minute
+python3 -B research/complex-x4-frame-bound/verify.py --word /tmp/x4/jx/FULL-WORD.json.gz
+```
+
+The second form checks a freshly rebuilt word from `research/gauge44-frames-x/README.md`; the content hash must match. By default the verifier reads the retained replay archive `research/community-frontier799-audit/pr799-replay.tar.gz`, whose hash the maintainer's integration receipt records.
+
+`gen_duals.py` nominated the duals with HiGHS (highspy 1.15.1, SciPy 1.18.1, NumPy 2.5.4, Python 3.12.14). Two runs wrote byte-identical `data/DUALS.json.gz`. The generator is not part of the proof: `verify.py` imports no solver and trusts no floating-point value.
+
+Checked on Windows 11 with CPython 3.12.14 and 3.14.7.
+
+## What this leaves for the complex track
+
+Per call, 1,745 of the 2,548 rank-1 children, all 56 rank-5 children and the eight centre descents lie on register edges between forced frames. Any κ gain from this supplier needs a scalar change (read sets, gate order, tail membership), new start or end frames (entrances, low ends, widths), or a change to owners and hosting. Frame re-choice on X4 is closed at b_next.
+
+## Scope
+
+Not covered: scalar rewrites, gate reordering or read-set exchanges; moving gates into or out of the early cleanup; entrance promotions or any other start or end frame change; owners, hosting and the finite invoice; the bit supplier; other outer theorems. The exclusion holds at b_next for the fixed word. It does not replay the native construction chain. The inherited all-size compiler, common-label and mutable-source realization, whole-call hosting, precision and tape, and analytic hypotheses remain. This is a finite certificate, not a Lean proof.
+
+## Prior work
+
+- chafreaky's #557 (`research/frame-domain-ceiling`) introduced complete F₂ domains, this LP relaxation and symbolic exact duals, for the PR551 word.
+- ntedvs's #776 (open) applies the method to #626's jp8 and ck words, with tail frames outside its scope.
+- Rohansguliani's #815 (open) solves PR699's SW4 word and #626's words with floating-point LP and CP-SAT, with tail frames fixed, and rediscovers #741.
+- JointXF reported in #799 that FrameCoal's optimiser reaches the X4 profile. The #799 review keeps that as a search report. This package corroborates it with an exact certificate.
+
+This package is a new implementation for the native gauge44 word format. Unlike the earlier packages, it frees the 163 early-cleanup frames and derives the low-end cone ceilings from the exact prefix map.
+
+The X4 word is Jeremy Kothe's #799 construction on chafreaky's #741 frames, BRoute's SW4 exchange, BlockInvert's promotions, the p6n and no-triangle layers and icekylinx's #645 gauge44 factory, with the lineage recorded in `research/gauge44-frames-x/README.md` and `CONTRIBUTORS.md`.
+
+Prepared for @navinor with substantial assistance from Claude Code. Apache-2.0. No independent human review.

research/complex-x4-frame-bound/RESULT.json

@@ -0,0 +1,65 @@
+{
+  "status": "PASS_X4_FRAME_ASSIGNMENT_EXCLUSION",
+  "word": {
+    "kind": "retained PR799 replay archive",
+    "archive": "research/community-frontier799-audit/pr799-replay.tar.gz",
+    "archive_sha256": "4dff69f3509ca81ab768ebf4b39bb6313b331995e4b2a412729b541a39c8459a",
+    "member": "pr799-native-fresh/jx/FULL-WORD.json.gz",
+    "content_sha256": "1e1d99ba7aab877d6b573c41f7030ee73de9a52fee51d0a822ddaae71251999f"
+  },
+  "excluded_b": "832200139425241163957/500000000000000000000000",
+  "gates": 6364,
+  "free_gates": 1201,
+  "domain_sizes": {
+    "2": 965,
+    "5": 206,
+    "16": 30
+  },
+  "components": 140,
+  "lp_rows": 9483,
+  "lp_columns": 12019,
+  "zero_reduced_costs": 8582,
+  "positive_reduced_costs": 3437,
+  "cone_ceilings": 128,
+  "baseline_local_profile": {
+    "1": 2548,
+    "2": 338,
+    "3": 430,
+    "4": 194,
+    "5": 56,
+    "8": 8
+  },
+  "brute_forced_components": 121,
+  "brute_forced_assignments": 307,
+  "global_step": {
+    "remainder": {
+      "1": 1,
+      "3": 1,
+      "44": 1,
+      "48": 2396
+    },
+    "moment_minus_one_lower": {
+      "mercator": "31359434841007457051186662850250005479126591/13479973333575319897333507543509815336818572211270286240551805124608",
+      "base_two": "581593/250000000000000000000000000000"
+    }
+  },
+  "kappa_step": {
+    "selected_kappa": "1661634653669567/1000000000000000000",
+    "next_kappa_tick": "25963041463587/15625000000000000",
+    "outer_engine_sha256": "c1ebb52163a7219504c728a5c2b098bf1e50bf20148a2879c5a74c3cadc7c03c",
+    "b_next_over_one_plus_b_next_below_next_tick": true
+  },
+  "engines": [
+    "base_two_moment.py",
+    "moment.py"
+  ],
+  "elapsed_seconds": 1.0,
+  "controls_rejected": {
+    "drop_component": "component count",
+    "inflate_dual": "dual objective differs from the baseline",
+    "omit_label": "incomplete domain",
+    "accepted_endpoint": "baseline admitted at the excluded exponent (mercator)",
+    "worse_baseline": "dual objective differs from the baseline",
+    "wrong_word": "X4 word content hash"
+  }
+}

research/complex-x4-frame-bound/SOURCES.json

@@ -0,0 +1,56 @@
+{
+  "base_commit": "f567884aeb8851b6e794af1184119a3bfbe1e631",
+  "selected_record": {
+    "path": "certificates/selected-result.json",
+    "kappa": "1661634653669567/1000000000000000000",
+    "certificate": "research/community-frontier799-audit/ASSEMBLY.json",
+    "certificate_sha256": "65c7648a8edaeaf4e0b8de3e21eeda94fba124d0935010d45ac9f76375b72cec",
+    "complex_lower": "1664400278850482327913/1000000000000000000000000"
+  },
+  "word": {
+    "archive": "research/community-frontier799-audit/pr799-replay.tar.gz",
+    "archive_sha256": "4dff69f3509ca81ab768ebf4b39bb6313b331995e4b2a412729b541a39c8459a",
+    "archive_sha256_recorded_in": "docs/research/community-frontier799-integration.json",
+    "member": "pr799-native-fresh/jx/FULL-WORD.json.gz",
+    "content_sha256": "1e1d99ba7aab877d6b573c41f7030ee73de9a52fee51d0a822ddaae71251999f",
+    "content_sha256_recorded_in": [
+      "research/gauge44-frames-x/construction/jx/RECIPE-X4.json",
+      "research/community-frontier799-audit/INDEPENDENT-LOCAL.json"
+    ],
+    "construction": "Jeremy Kothe PR799 at 80e6463157cfc80b85af09e7e2f14748fe2dac60 (research/gauge44-frames-x)"
+  },
+  "engines": {
+    "research/complex-k492-owner-repair/vendor/multicold/engines/moment.py": "81cbc864e106418fc7854322746f72180cb8110ff39f74450a3b8d55a82c1482",
+    "research/complex-k492-owner-repair/vendor/multicold/engines/base_two_moment.py": "aee70c242a2f1d225528fabe2002e1564d1dc884797c07d28a831c7878ee9098",
+    "research/complex-k492-owner-repair/vendor/multicold/engines/outer.py": "c1ebb52163a7219504c728a5c2b098bf1e50bf20148a2879c5a74c3cadc7c03c"
+  },
+  "auditor_for_crosscheck": {
+    "path": "research/gauge44-frames-x/independent/audit_local.py",
+    "sha256": "03afcfc9da428b3f6edac81c1fee7f277ab81b64998efae78380b63498dec6cd",
+    "recorded_in": "research/gauge44-frames-x/MANIFEST.json"
+  },
+  "package_files": {
+    "model.py": "0fa808a82e12a8928e43de3131958b9018476ee8c25b1ebc841316705e4f0eff",
+    "verify.py": "85e8e526cd6526a2aa547402f8810f393ee716627c6c5cce8edebaeac52804d7",
+    "gen_duals.py": "9aac56f7cd1c497bfc50f0fb47bd5b14761033127575665d576d948ee11fc3f8",
+    "crosscheck.py": "60f4c80eec322300b6a3850813829d3530cc39c4e8e4ad6318aef410a857d352",
+    "data/DUALS.json.gz": "379b4fec4df567d8bacd47f914e4acdc7d09a5236e79db42edcdbd845805831f",
+    "data/CROSSCHECK.json": "f75464ddf95b68e3e41f46ccedef0f6178c308e23347e1954478c804db920b61",
+    "RESULT.json": "2b46c4b6308d009e2051c8231af60a798da3ecddfcef033be7431faa656a08ad"
+  },
+  "dual_generation": {
+    "script": "gen_duals.py",
+    "python": "3.12.14",
+    "highspy": "1.15.1",
+    "scipy": "1.18.1",
+    "numpy": "2.5.4",
+    "note": "Solver output only nominates the duals; verify.py checks them exactly without any solver. Two generator runs produced byte-identical data/DUALS.json.gz."
+  },
+  "predecessor_pull_requests": {
+    "557": "merged; research/frame-domain-ceiling (method)",
+    "776": "open head 8bd985fe2842c948a5a4a1554b8e090f2e371afa",
+    "815": "open head d8c8b40ab0a95b6d77389e6726d86dddb60fb53c",
+    "799": "merged; audited source head 80e6463157cfc80b85af09e7e2f14748fe2dac60",
+    "741": "merged; reviewed head e516b1463606840a15f80aac1995d64ce0092e89"
+  }
+}