Audit (no κ): exact owner-fill optima on the T74 handoff line — #2374's fill is optimal over all fills; #2435's fill leaves +5.8e-10 (pattern optimum certified)

research/t74-owner-fill-optimality/README.md

@@ -0,0 +1,124 @@
+# Exact owner-fill optimality on the T74 handoff line: PR2374 is optimal; PR2435's fill leaves +5.8e-10
+
+**Audit / independent check; no κ claim.** This package certifies the exact pattern-integer optimum of the
+whole-helper owner fill for the two latest T74 claims and compares each claim's published fill with it.
+
+- **[PR2374](https://github.com/CrocSwap/integer-mult-bounds/pull/2374)** (Jeremy Kothe) claims "an exact
+  window-free-optimal owner fill" on [PR2322](https://github.com/CrocSwap/integer-mult-bounds/pull/2322)'s
+  words.
+  - **Confirmed and strengthened.** Every legal whole-helper owner fill of these words has
+    **b ≤ κ₂₃₇₄ + 10⁻¹⁵**.
+  - Its idle multiset `{1:21978, 3:8592, 5:2552, 32:1, 48:24560}` is the only one whose root exceeds
+    κ₂₃₇₄ − 10⁻¹².
+  - Owner-map work on the PR2322 words is therefore exactly exhausted. The earlier cap in
+    [PR2402](https://github.com/CrocSwap/integer-mult-bounds/pull/2402) allowed up to 8.1e-10.
+- **[PR2435](https://github.com/CrocSwap/integer-mult-bounds/pull/2435)** (Jeremy Kothe, κ = 0.0016985113437)
+  raises 24 copy-buffer entrances and adds "an exact owner fill for the new inventory", with idle
+  `{1:20824, 3:6695, 5:1, 48:25302}`.
+  - **That fill is not the pattern optimum.** The unique pattern-integer optimum has idle
+    **`{1:20822, 3:6694, 5:2, 48:25302}`**, with root **0.0016985119240, +5.80e-10 above PR2435's claimed κ**.
+  - It moves two rank-1 remainders and one rank-3 remainder into one more rank-5 remainder. Its pattern
+    counts are in the receipt; for example it uses two (32: 9,9,9) bins and 1,156 (48: 4,8,9,9,9,9) bins.
+  - Every legal fill of the PR2435 words has b ≤ that root + 10⁻¹⁵.
+  - Whether the optimum can be realized under PR2435's windows and family rules is **not** checked here.
+    It is a concrete owner-level target worth up to +5.8e-10.
+
+## Method (`owner_optimum.py`)
+
+0. **Inputs.**
+   - PR2322 words: profile and inventory recounted in PR2402.
+   - PR2435 words: recounted for this audit with the PR2387 frame-climb rule from PR2435 head `324d7d35`
+     (`BORROW-WORD-43base`, blob 7e382c2d; `BORROW-WORD-43extra`, blob 29fa1b3a). Both providers give
+     profile {1:2359, 2:632, 3:330, 4:120, 5:38, 8:8} and inventory {4:33, 5:9, 7:62, 8:90, 9:240}, equal to
+     the published report.
+   - The idle multisets and κ values are as published in each PR body.
+1. **The relaxation.** A legal fill places every helper role whole into one idle bin. The bins have ranks
+   8/16/32/48 and counts 49,728 / 33,152 / 33,152 / 33,152. So the fill's idle remainders come from an
+   integer pattern-count vector x ≥ 0 over the 1,163 width patterns, with the bin and width-inventory row
+   sums fixed (PR2387 / PR2360 relaxation, after PR1129). Windows, families and ports are dropped. That
+   makes this a relaxation of every legal fill, and the moment is linear in x.
+2. **Root check.** The PR2322 local profile (recounted in PR2402) plus PR2374's idle multiset has its root
+   certified within ±10⁻¹⁵ of the claimed κ, using 800-bit enclosures. Its rank mass equals 73·66304 − 23680.
+3. **Exact dual.** At a₀ = κ₂₃₇₄ + 10⁻¹⁵, a float simplex dual is repaired to an exact rational dual. It is
+   feasible against 800-bit lower enclosures of h(r) = (r/73)^(1−a₀) on all 1,163 patterns. Every integer
+   x then satisfies
+
+       66304·μₓ(a₀) ≥ L_loc + D + Σ_p rc_p xₚ,   rc_p ≥ 0 exact,
+
+   and if Σ rc_p xₚ ≥ T := 66304 − L_loc − D, then bₓ ≤ a₀. Here T ≈ 1.5475e-4.
+4. **Enumeration.** Every integer x with Σ rc_p xₚ < T is enumerated exactly.
+   - Only 9 basic and 7 non-basic patterns have rc < T.
+   - The 2 degenerate patterns, (32: 7,8,8,9) and (32: 7,7,9,9), are checked to swap only zero-remainder
+     patterns, so they never change the idle multiset. Their basis representation is integral, so their
+     counts never affect integrality.
+   - Any solution using them therefore maps to a count-0 representative with the same idle multiset and the
+     same Σ rc. That representative is checked to be nonnegative for every candidate combination, so the
+     sweep is complete.
+   - The other 5 have reduced costs 5.5e-5 … 1.5e-4, which allows counts ≤ 2.
+   - Basic variables are solved in exact rationals.
+5. **Search, then exclusion.**
+   - Search: at a = κ_claim, enumerate every integer solution that could beat the claim. A budget-pruned
+     DFS is exact. Rank the distinct idle multisets by certified root.
+   - Exclusion: at a₀ = (best root) + 10⁻¹⁵, zero integer survivors remain, so every fill has b ≤ a₀.
+6. **Control at (best root) − 10⁻¹²:** the optimal fill must survive, and it does.
+   - For PR2374 there are 25 survivors and for PR2435 there are 1,250. Each set is made of degenerate
+     copies of one heavy part, and all carry the optimal idle multiset.
+   - That gives the uniqueness statement.
+
+An adversarial AI reviewer reviewed the PR2374 part (the PR2435 extension came later) and found it
+**not refuted**. Using its own code
+(Decimal at 90 digits), it:
+- reproduced PR2374's root to 60 digits;
+- confirmed with a Gomory group-relaxation shortest path that the only correction within the budget is one
+  empty 32-bin;
+- ran local search over more than 48,000 exchanges of up to 4 bins without finding any improvement.
+
+Its runner-up fill, `{1:21978, 3:8591, 5:2553, 30:1, 48:24560}`, has a root 5.0e-10 below PR2374's. Its
+two wording issues are fixed here: the nonnegativity argument for the degenerate sweep, and the
+degenerate-copy count.
+
+## Reproduce
+
+From the repository root, standard library only. It needs no network, since all inputs are vendored and
+pinned.
+
+```sh
+python3 -I -B research/t74-owner-fill-optimality/owner_optimum.py     # ~45 s
+```
+
+Expected final line:
+`PASS_T74_OWNER_OPTIMUM pr2374:claim_is_optimum pr2435:optimum_gain=+5.803e-10 unique_within_1e-12 no_new_kappa`
+
+All results were run on CPython 3.14.4; the registered Python 3.12 replay was not run locally.
+
+## Scope and limits
+
+- **What is not re-checked.** Realization of the fills (windows, families, ports, admission, outer) is not
+  re-run, for either PR's fill or for the PR2435 pattern optimum. The bound covers every legal fill.
+  Attaining PR2435's optimum needs a realized owner map.
+- **What the statement covers.** It is about owner fills of the fixed PR2322 and PR2435 words, the 249/417
+  dispatch and the unchanged PR2269 bin stock. Changed words, inventories or templates are outside it; see PR2402
+  and PR2429 for those levers.
+- **Exactness.** The enumeration is exact (integer and rational), with an exact dual and enclosures. The
+  only floating-point step is the simplex that proposes the dual, and its repair is exact.
+
+## Open next questions
+
+- **Other inventories.** Do the same exact integer-optimality certificates hold for PR2312's and PR2269's
+  inventories? That would show whether every recent owner-fill PR on the T74 line was already at the
+  integer optimum. First step: run `owner_optimum.py` with their inventories and published idle
+  multisets.
+- **Recursive-interface levers.** Since packing on these words is exhausted, which word-level move is
+  cheapest to realize? Candidates are a block-53 handoff (+4.3e-8, PR2402) and cold-restoring one
+  end-climb-3 helper (+1.46e-6, PR2429). First step: attempt the PR601-style commutation test on the 64
+  end-climb-3 helpers.
+
+## Credits and licence
+
+- PR2374 / PR2349 (Jeremy Kothe) and PR2363 (mason-hale): the audited fills.
+- PR2322 (Vlado Vojdanovski): the words.
+- PR2360 (Jeremy Diviney) and PR1129 (Ali Romman): the pattern-dual relaxation.
+- PR2387 / PR2402 (this author): the LP and recount tools, vendored with pins.
+
+Prepared with substantial AI assistance (Claude Code, Anthropic, Claude Opus 5.5). An adversarial AI
+reviewer was used; no independent human review is claimed. Apache-2.0.

research/t74-owner-fill-optimality/SOURCES.json

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

research/t74-owner-fill-optimality/TASK.json

@@ -0,0 +1,65 @@
+{
+  "schema_version": 1,
+  "task_id": "independent-moment",
+  "priority_revision": 4,
+  "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2",
+  "original_card": {
+    "id": "independent-moment",
+    "question": "Does one changed supplier or assembly claim lack a source-bound independent check of a specific new implication?",
+    "starting_points": [
+      "certificates/selected-result.json"
+    ],
+    "methods": [
+      "Reconstruct the rank ledger from original operations rather than trusting its aggregate.",
+      "Implement certified moment inequalities through a different exact enclosure method."
+    ],
+    "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Record the selected certificate and complex_profile rather than taking a PR headline as input.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "List the existing independent checks for the exact selected or candidate sources. Pick a new changed input, missing binding or distinct failure mode; stop with a handoff if the proposed arithmetic check is already covered.",
+    "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.",
+    "allowed_variations": [
+      "Reconstruct either a source ledger or a numeric enclosure with a different method."
+    ],
+    "scope_change_triggers": [
+      "Importing the primary function and calling its output independent verification."
+    ],
+    "overlap_terms": [
+      "independent moment",
+      "rank histogram",
+      "exact enclosure"
+    ]
+  },
+  "scope_status": "refined",
+  "actual_scope": "Are the owner fills claimed by PR2374 (PR2322 words) and PR2435 (copy-buffer-raised words) optimal over all legal whole-helper fills (exact bin-pattern integer relaxation), and if not, what is the optimum?",
+  "scope_change_reason": "Drawn on the adversarial-audit track (seed 71). The specific new implication of PR2374 is its optimality claim, which had no independent check; the bin-pattern integer program gives one by a different method and over a larger class.",
+  "bottleneck_link": "Shows owner packing on the T74 handoff line is exactly exhausted for PR2322's words and has exactly +5.8e-10 left for PR2435's words, so further gains need word-level changes.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop once the exact dual plus integer enumeration either exhibits a better idle multiset or proves none exists above kappa_2374 + 1e-15, with a below-root control.",
+  "outcome": "completed",
+  "evidence": "owner_optimum.py: both claimed roots certified within 1e-15 of their kappa; exact dual plus pruned exact enumeration finds the pattern-integer optimum and excludes everything above it + 1e-15. PR2374: optimum = its fill (unique within 1e-12). PR2435: unique optimum idle {1:20822,3:6694,5:2,48:25302}, root 0.0016985119240 (+5.80e-10 over its claim). PR2435 words recounted (profile/inventory equal to report).",
+  "author": "Sagar Thakrar",
+  "ai_assistance": "Prepared with substantial AI assistance: Claude Code (Anthropic, Claude Opus 5.5) wrote the certificate and text; a separate Claude subagent adversarially reviewed it. No independent human review is claimed.",
+  "open_questions": [
+    {
+      "question": "Can PR2435's pattern optimum {1:20822,3:6694,5:2,48:25302} be realized as a legal owner map under its windows and families?",
+      "why_it_matters": "It is worth +5.80e-10 in kappa on the current top T74 claim and is the exact maximum for those words.",
+      "first_step": "Start from PR2435's FILL and move helpers into two extra (32: 9,9,9) bins and the (48: 4,8,9,9,9,9) bins listed in the receipt's pattern_counts, re-checking windows and family rules.",
+      "blocked_by": "Window/family feasibility is not modelled by the pattern relaxation."
+    },
+    {
+      "question": "Which word-level move on the PR2322 words is cheapest to realize now that packing is exhausted?",
+      "why_it_matters": "Owner fills cannot add more than 1e-15; word-level moves are priced at +4.3e-8 (handoff) to +1.46e-6 (cold-restoring an end-climb-3 helper).",
+      "first_step": "Attempt a PR601-style commutation test on the 64 end-climb-3 helpers (PR2429).",
+      "blocked_by": "Exact cleanup commutation semantics of the T74 words are not modelled here."
+    }
+  ]
+}

research/t74-owner-fill-optimality/VERIFY.json

@@ -0,0 +1,19 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/owner_optimum.py"
+      ],
+      "timeout_seconds": 300,
+      "checks": "For PR2374 and PR2435: certified root bracket of the published idle multiset; exact search of integer pattern solutions that could beat the claim; certified root of the best; exact dual exclusion at best + 1e-15 (no survivors); control at best - 1e-12 (optimum survives, unique idle multiset). Expect PASS_T74_OWNER_OPTIMUM."
+    }
+  ]
+}