Research: X54 mixed-T37 saturation — exhaustive local sweeps, exact Φ packing invariant and width/Φ prices (no new kappa)

research/x54-mixed-t37-saturation/README.md

@@ -0,0 +1,155 @@
+# Saturation of the X54 mixed-T37 construction (#1193/#1218)
+
+**No new κ.** This is a scoped negative result plus a screening tool for the highest open claim,
+κ = 0.001675809683500501 (#1193, #1218, #1239). It asks whether that construction can still be improved by
+(a) more width-neutral local moves on its two final words, or (b) a better packing of the same helpers.
+Within the families and the model below, the answer is no. It also gives exact prices for helper-width changes,
+so later inventory proposals can be screened before anyone builds them.
+
+> **Superseded in part during this session.** Gains appeared after the base snapshot (21:03Z), and both escape
+> the scope stated here:
+> - #1274 found a local gain on the same words outside the #1186 move families. It replaces the pivot-531 cold
+>   kernel with a helper-donor kernel, giving H1 −3, H3 +1.
+> - #1252 (Gonzalo-Mier), applied in #1268 and #1280, repartitions completely idle rank-48 children
+>   (48+48 → 45+51).
+>
+> So statement 2 below is about the **bin-remainder model**, where an idle child is a bin's unfilled remainder.
+> Idle-axis exchanges after packing are not covered by it. The sweep tallies, the Φ invariant on occupied bins
+> and the width/Φ prices remain valid for what they state. The highest open claim is now
+> 0.001676377648122875 (#1280).
+
+## Inputs
+
+These are vendored byte-for-byte from open PRs and pinned in `verify.py`:
+
+| File | Source |
+|---|---|
+| `inputs/D3-WORD.json.gz` | #1193 `vendor/pr1207/BASE-X54-WORD.json.gz`: #1148 joint entrances + #1195 fusions + X54 (125 calls) |
+| `inputs/D4-WORD.json.gz` | #1193 `data/FOUR-WORD.json.gz`: D3 + entrance group 627 (208 calls) |
+| `inputs/FLOW.json.gz`, `inputs/MIX.json` | #1193's frozen integer pattern flow and call dispatch |
+
+The #1193 head is `4e392e90`; #1218 at `0aa14797` reuses the same words, flow and dispatch. The T37 bin
+capacities are recomputed from files already on main: the retained #1042 replay archive and PR858/PR870's
+unchanged `actual_windows`.
+
+## Results
+
+### 1. No local gain is left in the toolkit's move families
+
+I used the #1186 toolkit at head `9254a3cc`, unchanged, with exact frame pricing. Both final words were swept.
+#1195 had swept only the pre-slot and seven-slot words, before X54 and the joint entrances.
+
+| Family | Candidates per word | Feasible | Gains (D3 / D4) |
+|---|---:|---:|---:|
+| Read fusion + single/pair swap repairs + full exchange (`repair.py`) | 2,238 | 969 | 0 / 0 |
+| Read-set exchange, every subset of swappable reads, 14 copy pairs | 50 | 0 | 0 / 0 |
+| Joint triangle-hybrid, ≤3 fused reads, partial swaps, both restore modes | 161 | 24 | 0 / 0 |
+
+The baseline frames are also exactly optimal: the frame-solver optimum equals the published profile. The
+per-candidate results are in `evidence/sweeps/`.
+
+### 2. The incumbent idle profile is optimal for its mix in the bin-remainder model (exact)
+
+`packing.py` uses standard-library integer arithmetic. It recounts every helper width from the two words and
+checks that the flow hosts all 159,840 helpers exactly once. The bins hold `{8:24864, 16:16576, 32:16576, 48:16576}`
+and the idle remainders are `{1:2, 48:11374}`, with mass 545,954.
+
+**Width-class invariant.** Let φ(4) = φ(8) = 0, φ(5) = 3, φ(7) = 1 and φ(9) = −1. Enumerating every multiset
+of widths gives these bounds:
+- a bin filled exactly to capacity 8, 16 or 32 has Φ ≥ 0;
+- a bin filled exactly to capacity 48 has Φ ≥ −4.
+
+Φ is additive, so its total is fixed by the helper inventory: −20,814 for 125 D3 + 208 D4.
+
+**Consequence.** The only cheaper idle histogram of the same mass is `{2:1, 48:11374}`. A histogram with fewer
+rank-48 parts is dearer by Karamata; this is checked for every j up to 11,374 at #1193's root endpoint.
+Realizing `{2:1, 48:11374}` would need exactly 5,202 occupied capacity-48 bins, one remainder-two bin and every
+other bin full. Then Φ ≥ −20,810 > −20,814, a contradiction.
+
+The incumbent is tight. Every occupied capacity-48 bin attains −4, and the two `4+9+9+9` bins give −3 each.
+**So the two leftover rank-one idle units cannot be merged into one rank-two child.** That would have been the
+only remaining helper-packing gain, about +3.3·10⁻¹⁰ in κ, for this mix. This holds even with time windows,
+ports and family rules ignored. It does not hold once the idle children themselves are reshaped (#1252).
+
+### 3. The mix is optimal among demotion counts (numerical screening)
+
+`aggregate.py` (SciPy/HiGHS, floating point) lets every call use k ∈ [−3, 3] extra four-helper entrance groups.
+Each group is taken to change the profile by `−8H1+8H2+4H3−4H4` and four widths by 4→5. Only k = 0, 1 are
+admitted words; the others are a linear extrapolation. The model ranges over all 1,163 bin patterns and relaxes
+time windows. Its integer optimum equals the incumbent objective exactly: 208 groups in total. The fractional LP
+gains only half a group, which is not integral, worth ≈2.5·10⁻¹⁰ in κ.
+
+The LP duals have an exact two-parameter structure, π_w = −λ·w − μ·φ(w), with λ = 11.731 per unit of helper
+width and μ = 25.041 per unit of Φ. The units are 10⁶ × moment × W, at the #1193 root.
+
+### Screening rule for a proposed local change
+
+Take a per-call change with paid-profile delta Δn, total helper-width delta ΔWid and Φ delta ΔΦ. Its marginal
+score is
+
+```
+score = Σ_r Δn_r · 1e6·((r/73)^(1-a) − r/73)  −  11.731·ΔWid  −  25.041·ΔΦ
+```
+
+summed over the calls that adopt it, with a = 0.0016786227. A negative score is a candidate gain.
+Δκ ≈ −1.028·10⁻¹¹ × score. The prices are marginal LP duals. An integral packing must still exist, and there is
+almost no slack (2 units), so rerun the ILP with the new variant and then admit it natively.
+
+Examples:
+- An extra entrance group scores ≈ −1, which is break-even. That is why #1193 stops where it does.
+- Shrinking one 9-wide helper to 8 earns 13.3. Turning a 9 into a 7 earns 26.6.
+- Turning a 4 into a 5 earns 86.9, but growing 7→8 costs 13.3.
+
+## Reproduce
+
+```sh
+python3 -B research/x54-mixed-t37-saturation/verify.py                        # ~2 s, stdlib
+python3 -B research/x54-mixed-t37-saturation/aggregate.py --out /tmp/agg.json  # ~25 s, SciPy
+python3 -B research/x54-mixed-t37-saturation/sweep.py --toolkit PR1186/research/exact-frame-toolkit \
+    --word D3 --out /tmp/sweeps --workers 6                                    # ~10 min per word
+```
+
+`verify.py` does the following:
+- checks the input pins;
+- replays the exact packing statement against `evidence/PACKING.json`;
+- rejects five controls: a changed call mix, a changed helper width, a non-conserving pattern, a dropped bin
+  and non-invariant φ weights;
+- recounts the stored sweep tallies.
+
+It does not rerun the sweeps or the ILP.
+
+## Scope and limitations
+
+- The sweeps cover the #1186 move families as implemented. #1274's helper-donor kernel shows that gains do exist
+  outside them, with their default limits: `repair.py` tries at most
+  40 repairs per fusion. They do not cover other delivery rewrites, entrance or end changes, or different
+  helper interfaces. A failed finite search is not an impossibility theorem.
+- The packing statements relax time windows, ports and per-call family rules, so they are upper bounds on what
+  any helper packing could achieve when an idle child is a bin's remainder. Repartitioning idle axes, as in
+  #1252, is outside that model. They assume the retained T37 bin geometry (capacities ≤ 48) and the {4,5,7,8,9}
+  width alphabet.
+- All inherited conditions of the incumbent remain conditions here: all-size compiler, common-label and
+  mutable-source realization, whole-call hosting, precision and tape, exact recovery, analytic transfer, and
+  bit H1–H5.
+
+## Open next questions
+
+1. **Can a helper-width change pass the screening rule?** For example, a 9→8 end at local cost below 13.3 units,
+   or a 4→5 entrance change below 86.9 per helper. *Why:* the packing is saturated, so only a changed inventory
+   or local word can move κ. *First step:* price candidate single-helper entrance and end changes with the
+   #1186 `harness.Pricer`, then score them with the rule above. *Blocked by:* there is no generator for
+   single-helper interface changes; #1176 found that entrance demotions need whole four-helper groups.
+2. **How do the width/Φ prices move once idle children are reshaped?** #1252/#1280 turn idle 48s into 45/51.
+   *Why:* those exchanges change the marginal value of idle mass, and so λ, and with it the break-even price of
+   an entrance group. The mix may then want more or fewer than 208 groups. *First step:* rerun `aggregate.py`
+   with an idle-cost function in which empty capacity-48 bins can pair into 45+51 at #1280's achieved rate.
+   *Blocked by:* that rate depends on #1252's per-(replica, port) commuting-axis condition, which is not
+   modelled here.
+
+## Credit
+
+The #1193 global allocation is Jeremy Diviney's; #1218 is Rohan Arun's composition. The words come from
+Thomas DiFiore's #1148, Marius-Paul Dumitrean's #1195 fusions, Jeremy Kothe's #1130 X54 and #1196/#1207's
+composition. The search toolkit is #1186, by Marius-Paul Dumitrean. The windows are from Hao Yan's PR858/PR870
+geometry. The demotion-group lead is #1111/#1176. #1240's packing-ceiling note motivated the idle-rank
+question. Prepared by Wronskode with substantial AI assistance (Anthropic Claude, via Claude Code). Apache-2.0.

research/x54-mixed-t37-saturation/RESULT.json

@@ -0,0 +1,54 @@
+{
+ "incumbent": {
+  "heads": {
+   "1193": "4e392e90e3fca8f395e35d6a23644920160a9f0f",
+   "1218": "0aa147977ad226f9d777d6a21a610ab037985b1e"
+  },
+  "kappa": "1675809683500501/1000000000000000000",
+  "prs": [
+   1193,
+   1218
+  ]
+ },
+ "status": "NO_NEW_KAPPA_SCOPED_SATURATION",
+ "sweeps": {
+  "D3": {
+   "exchange": {
+    "candidates": 50,
+    "feasible": 0,
+    "gains": 0
+   },
+   "joint": {
+    "candidates": 161,
+    "feasible": 24,
+    "gains": 0
+   },
+   "repair": {
+    "candidates": 2238,
+    "feasible": 969,
+    "gains": 0
+   }
+  },
+  "D4": {
+   "exchange": {
+    "candidates": 50,
+    "feasible": 0,
+    "gains": 0
+   },
+   "joint": {
+    "candidates": 161,
+    "feasible": 24,
+    "gains": 0
+   },
+   "repair": {
+    "candidates": 2238,
+    "feasible": 969,
+    "gains": 0
+   }
+  }
+ },
+ "toolkit": {
+  "head": "9254a3cc610a72e9c4600da089d5cdbcab996b9c",
+  "pr": 1186
+ }
+}

research/x54-mixed-t37-saturation/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "dd6403f774a0891093a006ae9716c02e371b1fdb",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11",
+      "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb",
+      "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce"
+    }
+  ]
+}

research/x54-mixed-t37-saturation/TASK.json

@@ -0,0 +1,66 @@
+{
+  "schema_version": 1,
+  "task_id": "selected-packing",
+  "priority_revision": 2,
+  "base_commit": "dd6403f774a0891093a006ae9716c02e371b1fdb",
+  "original_card": {
+    "id": "selected-packing",
+    "question": "Is there a genuinely unsearched, explicitly bounded improvement to the selected packing?",
+    "starting_points": [
+      "certificates/selected-result.json",
+      "research/heterogeneous-owner-assembly/README.md"
+    ],
+    "methods": [
+      "Search a named unclaimed canonical candidate domain with a reproducible partition.",
+      "Prove a stronger scoped relaxation or exact optimum for one named residual subproblem."
+    ],
+    "acceptance_gate": "Check live PR overlap first, price both suppliers and distinguish a search best from an optimum.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Locate the selected packing source in the review and check live PRs for the same residual problem.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Define an unclaimed canonical domain and a favorable bound before starting a new search.",
+    "bottleneck_link": "An actual paid-profile gain can improve the frontier up to the other supplier cap.",
+    "allowed_variations": [
+      "One bounded residual packing instance or exact relaxation."
+    ],
+    "scope_change_triggers": [
+      "Rerunning an existing search with only a different seed as a separate mathematical contribution."
+    ],
+    "overlap_terms": [
+      "T16",
+      "owner exchange",
+      "packing"
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Is there an unsearched width-neutral local move or packing improvement for the highest open claim (#1193/#1218 X54 mixed-T37, kappa 0.001675809683500501), rather than the selected #1094 packing?",
+  "scope_change_reason": "The selected #1094 packing is superseded by open claims on the same lineage; the bounded residual question that matters is whether the strongest open construction still has local or packing headroom.",
+  "bottleneck_link": "The complex supplier binds; on this line every recent gain came from width-neutral local moves or packing. This bounds both for the incumbent words/mix and prices the inventory changes that could still help.",
+  "budget_minutes": 120,
+  "stop_rule": "Stop after exhaustive toolkit sweeps on both final words and an exact or ILP packing bound; build an admitted construction only if a gain appears.",
+  "outcome": "negative-result",
+  "evidence": "evidence/sweeps (0 gains in 2x(2238+50+161) candidates), evidence/PACKING.json (exact Phi invariant and idle optimum), evidence/AGGREGATE.json (ILP = incumbent; dual prices). Superseded in part by #1274 (local gain outside the #1186 families) and #1252/#1268/#1280 (idle-axis repartition outside the bin-remainder model).",
+  "author": "Wronskode",
+  "ai_assistance": "Substantial assistance from Anthropic Claude (Claude Code): search runs, analysis, code and text.",
+  "open_questions": [
+    {
+      "question": "Is there a single-helper entrance/end change whose local frame cost passes the width/Phi screening rule (e.g. 9->8 below 13.3 units, 4->5 below 86.9 per helper)?",
+      "why_it_matters": "Packing and width-neutral moves are saturated for the incumbent; only a changed helper inventory or new local word can move kappa on this line.",
+      "first_step": "Price candidate single-helper interface changes with the #1186 Pricer and apply the README score; rerun aggregate.py with the new variant.",
+      "blocked_by": "No generator for single-helper interface changes; #1176 reports demotions need whole four-helper groups."
+    },
+    {
+      "question": "How do the width/Phi shadow prices and the optimal demotion-group count change once idle rank-48 children can be repartitioned (48+48 -> 45+51, #1252/#1280)?",
+      "why_it_matters": "Idle reshaping changes the marginal value of idle mass, hence lambda and the break-even of an entrance group; the 208-group mix may no longer be optimal.",
+      "first_step": "Rerun aggregate.py with an idle-cost function allowing empty capacity-48 bins to pair into 45+51 at the rate #1280 achieves.",
+      "blocked_by": "The achievable pairing rate depends on #1252's per-(replica, port) commuting-axis condition, which is not modelled here."
+    }
+  ]
+}

research/x54-mixed-t37-saturation/VERIFY.json

@@ -0,0 +1,21 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/community-frontier1042-audit/selected-replay.tar.gz",
+    "research/complex-t21-owners/vendor/pr870/t16/build_parent.py"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "input pins; exact width recount, flow conservation, Phi lemma and idle optimum vs evidence/PACKING.json; five rejected mutation controls; sweep tally recount; aggregate ILP receipt."
+    }
+  ]
+}