Audit (no new kappa): the composed T488 profile is exactly PR3642's optimal packing vertex

research/t488-attains-retimed-packing-cap/README.md

@@ -0,0 +1,131 @@
+# The composed T488 profile is exactly PR #3642's optimal packing vertex
+
+**Result (exact arithmetic, scoped to the cited fixed-capacity model).** PR #3653's
+published paid profile for the T488 × retiming composition is *exactly* the
+optimal profile of PR #3642's fixed-capacity packing relaxation at `T = 488`:
+
+```
+PROFILE_488 = 4392 * {1:2437, 2:724, 3:226, 4:102, 5:20, 8:8}
+            +  488 * {1:234, 3:261/4, 5:57/4, 48:1531/4}
+```
+
+Every coefficient is an integer and every summand is quoted from the two pinned
+public receipts. The second factor is PR #3642's `ideal_idle_per_replica`, the
+feasible primal vertex of its 2,551-pattern dual. Because the local bill enters
+the moment additively and is fixed, the moment-minimising packing does not depend
+on the bill, so a construction already at that vertex stays optimal when the
+retiming changes the bill. The composition is at the vertex.
+
+Consequences, at the strength actually established:
+
+1. The T530-to-T488 packing gap of `2.4507952107748684e-8` in the moment root is
+   **closed exactly**. That number is both PR #3642's published remaining
+   headroom and PR #3653's claimed improvement over it: the entire gain is the
+   fixed-inventory headroom PR #3642 had already certified, realised by #3633's
+   T488 allocation.
+2. No packing inside the certificate's model — fixed capacities
+   `{8:672, 16:448, 32:448, 48:448}` per replica, widths
+   `{4:26, 5:2, 6:18, 7:52, 8:97, 9:213}`, retimed bill, dimension 73, live
+   `896*T` — can improve the composed κ. The next gain requires a changed word
+   or local bill, helper inventory, capacity set, or model.
+3. At `T = 488` the relaxation is integer-attained (`488 = 0 mod 4` clears the
+   quarters), so the optimum is a real child multiset, not a fractional fiction.
+
+This is a scoped ceiling statement, not a new κ, not supplier admission and not a
+selected-frontier change. The optimality of the vertex is PR #3642's dual
+certificate (re-executed, not re-proved here).
+
+```sh
+python3.12 -I -B research/t488-attains-retimed-packing-cap/verify.py
+```
+
+Expected:
+
+```text
+PASS_T488_ATTAINS_RETIMED_PACKING_CAP checks=26 controls=7 identity_exact=true cap_attained=true no_new_kappa
+```
+
+Python 3.12, standard library only. `--write` regenerates `RESULT.json`.
+
+## What is checked
+
+| # | Check | Strength |
+|---|---|---|
+| 1 | The certificate's own `ideal_profile_at_T740` equals `6660*bill + 740*ideal_idle` | convention cross-check of my reading of the model |
+| 2 | `PROFILE_488` equals `4392*bill + 488*ideal_idle` exactly | exact integer identity (the result) |
+| 3 | Rank mass `65088*488 = 31762944`; live `437248 = 896*488`; physical `437757 = live + 408 + 8 + 91 + 2` | published aggregate identities |
+| 4 | Residual `PROFILE_488 - 4392*bill = 488*ideal_idle`; idle mass `18873`; bill mass `5135`; `9*5135 + 18873 = 65088` | exact decomposition |
+| 5 | Rank-48 child count `186782 <= 448*488`; ranks 8,16,32 zero | capacity feasibility of the vertex |
+| 6 | `M(0.001730418899766071163804) < 0 < M(0.001730418899766071163805)` with 80-digit Decimal, `M' > 0` at the midpoint, straddle survives one grid step outside | independent bracket reproduction |
+| 7 | Released 70-digit string reconstructs from the lower endpoint minus `10^-46` and `10^-70`; delta over the pinned T530 floor equals the published headroom to one `10^-24` grid step | released-value audit |
+| 8 | Seven rejection controls: T530 literal is not at the vertex (two ways), pre-retiming bill fails, wrong replica count fails, one rank-1 unit breaks the bracket, swapped endpoints break it, `T = 490` is fractional | controls |
+
+`RESULT.json` is generated by the verifier and compared byte-for-byte on each run.
+
+## Sources
+
+External bytes are hash-recorded, not vendored; a reviewer fetches the named
+heads. Base `20ecf2891d80b5acf18d980b2164fb44ea7faa90`.
+
+| Source | Head | File | SHA-256 |
+|---|---|---|---|
+| PR #3642 | `6568db75adbb61437190545f6fef1534c70e91e5` | `research/staged-release-retiming-t530/packing-cap/RETIMED-PACKING-CAP.json` | `6ca9271b3813d860e9b2aa4d5cf1d6bf579ccd5ea33a60e94ddf814474a6b0f3` |
+| PR #3642 | same | `.../packing-cap/check_retimed_cap.py` | `63ae34f20507b145d13b0fbdb801a092c5018b9a4a4ed385ab12c2db1ec6a98e` |
+| PR #3642 | same | `.../packing-cap/cap-source/binomial.py` (PR3531 pin) | `03eebf2be23cab07e5f9e978980fee7b17e10847da5720c3e4e0adb243e8e4fa` |
+| PR #3642 | same | `.../packing-cap/cap-source/pr3630-check_budget.py` | `639820c9ccf72b88ae16768055ec5500a66004784f57a2fa5f218bf4d2e4ee05` |
+| PR #3653 | `607a09ff441c79b215a8127a81f4cc70021d0d9b` | `research/retimed-t488-composition/PROOF.md` | `7a010afb7a01cded37b18561e903ca580eea5d838456cab0db061a13ad5fd04b` |
+
+The published cap receipt re-runs on its own pinned inputs in 1.6 s with the same
+interpreters and prints `PASS_RETIMED_ALL_2551_FIXED_INVENTORY_PATTERNS`,
+`cap ['0.001730418899766071163804', '0.001730418899766071163805']`,
+`literal ['0.001730394391813963415120', '0.001730394391813963415121']`,
+`headroom 2.4507952107748684e-08`. That re-run is recorded evidence of the
+certificate's own bytes; it is not an independent re-derivation of its dual.
+
+## What this does not establish
+
+- **No new κ.** The selected record is unchanged; this package reports an exact
+  identity and a scoped saturation consequence.
+- **The optimality is inherited.** The 2,551-pattern dual, its 2,539 strictly
+  positive reduced costs, 12 symbolic zeros and coefficient hash are PR #3642's.
+  I re-executed its verifier on the pinned bytes and reproduced its receipt; I did
+  not re-derive the dual basis or the pattern enumeration.
+- **No construction replay.** No word, operator, owner journal, native provider,
+  admission stage or fresh-bootstrap wrapper is replayed. Nothing here admits a
+  supplier or establishes chronology or physical-family attainment, which the
+  certificate's own scope excludes.
+- **One grid step.** The published headroom rational and the difference of the two
+  published decimal floors differ by exactly `10^-24`; the package checks the
+  agreement to that grid step and reports both values rather than choosing one.
+
+## Open next questions
+
+Structured copies are in `TASK.json`.
+
+1. **Re-derive the dual independently.** Re-implement the 2,551-pattern
+   enumeration and the 10×10 rational basis inverse from PR3630's spec, then
+   check every reduced cost without importing PR #3642's script. Blocker: the
+   coefficient convention (`73*x` scaling of the binomial moment) has to be
+   cross-checked first; this package uses the certificate's convention as quoted.
+2. **Does the same vertex persist under the next bill change?** The additivity
+   argument says yes for any fixed additive bill; the open part is whether a
+   changed *inventory* (helper widths or capacity counts) moves the vertex. First
+   step: recompute `ideal_idle_per_replica` under one changed capacity row and
+   compare the root.
+3. **Chronology and physical attainment.** The certificate bounds a relaxation;
+   whether the T488 allocation's literal owner journal attains the same vertex
+   chronologically is PR #3653's own owner-audit obligation, not covered here.
+
+## Credit
+
+roger-sato's PR #3642 supplied the retiming, the fixed-capacity certificate, its
+dual basis and the published headroom; rohanarun's PR #3653 supplied the composed
+paid profile and released endpoint; hexapode's PR #3633 supplied the T488
+allocation that reaches the vertex; Ross Richardson's PR #3605 and #3630 supplied
+the staged suppliers and the exact dual basis; PR3531 supplied the
+positive-binomial interval engine. The exact identity, the bill-additivity
+observation, the T530 negative control and the seven controls here are new in
+this package.
+
+Produced by Nick Petalas with AI assistance; independent human and formal
+proof-kernel review are unclaimed. Apache-2.0.

research/t488-attains-retimed-packing-cap/RESULT.json

@@ -0,0 +1,42 @@
+{
+  "M_at_cap_lower": "-6.5209934656285285288167036837894411430540047356680669742E-17",
+  "M_at_cap_upper": "2.4654911418492912121936623595198005424154233456496942909E-17",
+  "M_prime_at_bracket_midpoint": "89864846.074778197410103660433092416854694280813095521096646577833279618245989203",
+  "audit": "t488-attains-retimed-packing-cap",
+  "audited_pr3642_head": "6568db75adbb61437190545f6fef1534c70e91e5",
+  "audited_pr3653_head": "607a09ff441c79b215a8127a81f4cc70021d0d9b",
+  "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+  "cap_root_bracket": [
+    "0.001730418899766071163804",
+    "0.001730418899766071163805"
+  ],
+  "capacity_counts_per_replica": {
+    "8": 672,
+    "16": 448,
+    "32": 448,
+    "48": 448
+  },
+  "checks": 25,
+  "controls": 7,
+  "delta_over_T530_floor": "6126988026937171/250000000000000000000000",
+  "ideal_profile_rule": "calls*bill + replicas*ideal_idle_per_replica",
+  "identity": "PROFILE_488 == 4392*bill + 488*ideal_idle_per_replica",
+  "integrality_condition": "T = 0 mod 4; T=488 satisfies it",
+  "literal_to_cap_ratio_T488": "1 (the two profiles are identical)",
+  "literal_to_cap_ratio_T530_quoted": "0.999985836983108",
+  "live": 437248,
+  "no_new_kappa": true,
+  "outcome": "PASS_T488_ATTAINS_RETIMED_PACKING_CAP",
+  "physical": 437757,
+  "published_root_headroom": "24507952107748683/1000000000000000000000000",
+  "rank_mass": 31762944,
+  "released_kappa": "0.0017304188997660711638039999999999999999999998999999999999999999999999",
+  "width_inventory_per_call": {
+    "4": 26,
+    "5": 2,
+    "6": 18,
+    "7": 52,
+    "8": 97,
+    "9": 213
+  }
+}

research/t488-attains-retimed-packing-cap/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81",
+      "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5",
+      "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0"
+    }
+  ]
+}

research/t488-attains-retimed-packing-cap/TASK.json

@@ -0,0 +1,78 @@
+{
+  "schema_version": 1,
+  "task_id": "independent-moment",
+  "priority_revision": 6,
+  "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90",
+  "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",
+      "research/rank7-joint-endframes/README.md",
+      "docs/research/research-family-status.md"
+    ],
+    "methods": [
+      "Independently reconstruct a coordinated frame/circuit change and its single-change control, then derive the complete rank and physical ledger.",
+      "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": "Read #2979 joint rank-7 end-frame proposal and the revision-6 evidence status. Its claimed kappa is not selected. Compare coordinated changes with the losing single-change controls and locate the complete physical ledger; an aggregate moment alone does not validate the mechanism.",
+      "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."
+    },
+    "first_experiment": "Prioritize a bounded independent audit of #2979: reconstruct one joint group and its single-lowering control, check the declared frames/chronology, then trace changed children, idle widths and cleanup buffers into the complete invoice and both supplier caps. Choose one still-missing implication after checking existing audits. Stop with exact unresolved dependencies if full admission exceeds the session; do not launch a new lowering census on an unvalidated premise or substitute extra root digits for mechanism checking.",
+    "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.",
+      "Promoting #2979 from merged source archive to validated supplier solely from author PASS receipts or aggregate pricing."
+    ],
+    "overlap_terms": [
+      "independent moment",
+      "rank histogram",
+      "exact enclosure",
+      "2979",
+      "rank7 joint endframes",
+      "paired extraction",
+      "joint lowering"
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Independent exact-arithmetic audit of one implication of the newest composed conditional supplier: PR #3653's published T488 x retiming paid profile equals PR #3642's published ideal fixed-capacity packing profile at T=488 exactly, PROFILE_488 = 4392*local_bill + 488*ideal_idle_per_replica. Checks: reproduce the certificate's own T740 ideal as a convention control; the exact identity; aggregate identities (rank mass 65088*488, live 896*488, physical 437757); the residual decomposition; capacity feasibility; the moment bracket at the two published 10^-24 endpoints with an 80-digit engine; the released 70-digit string; the delta over the pinned T530 floor against the published headroom; seven rejection controls. Consequence stated only at certificate strength: the composition is the optimal vertex of the cited relaxation, so the 2.4507952107748684e-8 T530-to-T488 root headroom is closed exactly and no repacking inside that model can improve it. No word, owner journal, native provider, admission stage or selected-frontier value is replayed; no new kappa is claimed.",
+  "scope_change_reason": "The card's named first object is a #2979 joint rank-7 audit. This session instead closes a stated open question from the immediately preceding independent audit of the same live frontier family (PR #3740, open question 2: is the composed profile's moment margin zero against PR #3642's relaxation?). That is a direct, bounded continuation of the same claimed supplier, and the answer is an exact identity rather than another report of near-equal decimals. The card's acceptance gate - independence, source binding, positive cases and semantic failure controls - is met by the seven controls and the exact reconstruction.",
+  "bottleneck_link": "The conditional T488/T530 cluster (kappa about 0.0017304) is the most active candidate family above the selected 0.001672660197076918. Deciding whether its current value is a word-level advance or the certified packing ceiling determines where the next unit of effort goes: more repacking (exhausted) versus a changed word, bill, inventory or model.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop once the identity, the T740 convention, the aggregate identities, the bracket straddle, the released string, the headroom identity and seven controls are reproducible from the quoted constants and the published cap receipt re-runs on its pinned bytes. Do not re-derive the dual, replay the word or claim a new kappa in this session.",
+  "outcome": "completed",
+  "evidence": "RESULT.json. PROFILE_488 = 4392*bill + 488*ideal_idle holds exactly with integer coefficients; rank mass 31762944, live 437248, idle mass 18873 per replica, bill mass 5135; M(0.001730418899766071163804) = -6.5209934656285285288167036837894411430540047356680669742e-17 < 0 < 2.4654911418492912121936623595198005424154233456496942909e-17 = M(0.001730418899766071163805); M' at the midpoint about 8.9865e7; released 70-digit string reconstructs; delta over the T530 floor 2.4507952107748684e-8 equals the certificate's published headroom to one 10^-24 grid step; seven controls rejected. The published cap receipt re-ran on its pinned inputs in 1.6 s and reproduced PASS_RETIMED_ALL_2551_FIXED_INVENTORY_PATTERNS with the same bracket and headroom.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can the 2,551-pattern dual be re-derived independently of PR #3642's script?",
+      "why_it_matters": "The attainment conclusion inherits the certificate's optimality. A separate implementation would turn a re-executed receipt into an independent proof of optimality.",
+      "first_step": "Rebuild PR3630's 10x10 basis spec and the residual-rank objective from the published constants, then check every pattern's reduced cost with exact rational interval arithmetic.",
+      "blocked_by": "The certificate's coefficient convention (a 73x scaling of the binomial moment) must be matched first; this package treats it as quoted."
+    },
+    {
+      "question": "Does a changed helper inventory or capacity row move the optimal vertex?",
+      "why_it_matters": "Bill additivity keeps the vertex fixed for any additive bill, so the remaining lever is the inventory. If a changed capacity row lowers the root, the family has a real next search; if not, only the word/model remains.",
+      "first_step": "Recompute the primal idle vertex under one changed capacity row, then evaluate the resulting root with the same bracket method.",
+      "blocked_by": "Requires the dual re-derivation above or a trusted certificate variant for the changed row."
+    },
+    {
+      "question": "Does the literal T488 owner journal attain the vertex chronologically?",
+      "why_it_matters": "The certificate bounds a fractional packing; physical-family and chronology attainment are separate obligations and a gap there would weaken the attained-cap reading.",
+      "first_step": "Compare the composed package's literal owner audit output against the vertex child counts per replica.",
+      "blocked_by": "PR #3653's own owner/invoice replay; not run in this session."
+    }
+  ]
+}

research/t488-attains-retimed-packing-cap/VERIFY.json

@@ -0,0 +1,22 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "certificates/selected-result.json",
+    "docs/research/agent-task-catalog.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 600,
+      "checks": "Exact identity PROFILE_488 = 4392*local_bill + 488*ideal_idle_per_replica against PR3642's published optimal packing vertex; T740 convention cross-check; aggregate rank-mass/live/physical identities; residual decomposition and per-replica idle mass; capacity feasibility; 80-digit moment straddle at the two published 10^-24 endpoints, positive derivative and one-step-outside margin; released 70-digit string; delta over the pinned T530 floor against the published headroom to one grid step; seven rejection controls; RESULT.json byte match in read mode"
+    }
+  ]
+}