From c7386166f445ae47bbe04e87bc08d1ccf6ae4814 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Sun, 18 Oct 2026 22:20:12 +0100 Subject: [PATCH 1/2] audit(research): compose T488 at the retimed packing vertex PR3653's published T488 x retiming paid profile is exactly PR3642's published optimal fixed-capacity packing profile at T=488: 4392*local_bill + 488*ideal_idle_per_replica, coefficient for coefficient. The local bill enters the moment additively, so the optimal packing vertex does not depend on it; the composition therefore sits at the certified vertex. The 2.4507952107748684e-8 root gap PR3642 published between its literal T530 profile and its cap is closed exactly, and no repacking inside that model can improve the composed kappa. Seven controls include the T530 literal residual (not at the vertex) and the pre-retiming bill. No new kappa, no supplier admission, no word or owner replay; the 2551-pattern dual is re-executed from its pinned bytes, not re-derived. --- .../README.md | 131 ++++++++ .../RESULT.json | 42 +++ .../SOURCES.json | 18 + .../TASK.json | 78 +++++ .../VERIFY.json | 22 ++ .../verify.py | 308 ++++++++++++++++++ 6 files changed, 599 insertions(+) create mode 100644 research/t488-attains-retimed-packing-cap/README.md create mode 100644 research/t488-attains-retimed-packing-cap/RESULT.json create mode 100644 research/t488-attains-retimed-packing-cap/SOURCES.json create mode 100644 research/t488-attains-retimed-packing-cap/TASK.json create mode 100644 research/t488-attains-retimed-packing-cap/VERIFY.json create mode 100644 research/t488-attains-retimed-packing-cap/verify.py diff --git a/research/t488-attains-retimed-packing-cap/README.md b/research/t488-attains-retimed-packing-cap/README.md new file mode 100644 index 0000000000..36e32df4fd --- /dev/null +++ b/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. diff --git a/research/t488-attains-retimed-packing-cap/RESULT.json b/research/t488-attains-retimed-packing-cap/RESULT.json new file mode 100644 index 0000000000..74029e404f --- /dev/null +++ b/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 + } +} diff --git a/research/t488-attains-retimed-packing-cap/SOURCES.json b/research/t488-attains-retimed-packing-cap/SOURCES.json new file mode 100644 index 0000000000..0839f4876a --- /dev/null +++ b/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" + } + ] +} diff --git a/research/t488-attains-retimed-packing-cap/TASK.json b/research/t488-attains-retimed-packing-cap/TASK.json new file mode 100644 index 0000000000..5905d5e0e4 --- /dev/null +++ b/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." + } + ] +} diff --git a/research/t488-attains-retimed-packing-cap/VERIFY.json b/research/t488-attains-retimed-packing-cap/VERIFY.json new file mode 100644 index 0000000000..b6989186de --- /dev/null +++ b/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" + } + ] +} diff --git a/research/t488-attains-retimed-packing-cap/verify.py b/research/t488-attains-retimed-packing-cap/verify.py new file mode 100644 index 0000000000..4b1530ab7e --- /dev/null +++ b/research/t488-attains-retimed-packing-cap/verify.py @@ -0,0 +1,308 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Does the composed T488 x retiming profile attain the T530 packing ceiling? + +Audited objects (public, exact pins and SHA-256 in README.md and SOURCES.json): + + * PR #3642, research/staged-release-retiming-t530/packing-cap at head + 6568db75adbb61437190545f6fef1534c70e91e5. Its RETIMED-PACKING-CAP.json + publishes the feasible primal idle bill per replica + {1: 234, 3: 261/4, 5: 57/4, 48: 1531/4}, + the retimed local bill per call {1:2437,2:724,3:226,4:102,5:20,8:8}, + capacities per replica {8:672,16:448,32:448,48:448}, the ideal profile at + T=740, and the fixed-inventory relaxation root bracket + (0.001730418899766071163804, 0.001730418899766071163805). + + * PR #3653, research/retimed-t488-composition at head + 607a09ff441c79b215a8127a81f4cc70021d0d9b. Its published paid profile is + {1:10817496,2:3179808,3:1024434,4:447984,5:94794,8:35136,48:186782} + at 4,392 calls and 488 replicas (9 calls per replica). + +The check is one exact integer identity plus its consequences: + + PROFILE_488 == 4392 * local_bill + 488 * ideal_idle_per_replica. + +So the composed profile is exactly the certificate's own optimal profile at +T=488 (its published T=740 ideal profile is reproduced by the same rule as a +convention cross-check). Because the local bill enters the moment additively +and is fixed, the moment-minimising packing does not depend on the bill; a +construction already at the optimal vertex stays optimal when the bill changes. +Hence the composed profile attains the fixed-capacity relaxation ceiling, the +T530-to-T488 packing headroom is closed exactly, and no repacking inside the +certificate's model can improve the composed kappa. + +Scope: this is an exact arithmetic and model-consistency audit. The optimality +of the published primal vertex is PR #3642's certificate (its 2,551-pattern +dual), cited and re-executed as recorded evidence, not re-proved here. No word, +owner journal, native provider, admission stage or selected-frontier value is +replayed. No new kappa is claimed. + +usage: verify.py [--write] + +Nick Petalas, donated research session (worker 7), with AI assistance. +Apache-2.0. +""" +from __future__ import annotations + +import json +import sys +from decimal import Decimal, getcontext +from fractions import Fraction +from pathlib import Path + +HERE = Path(__file__).resolve().parent + +# --- PR #3642 packing-cap constants (quoted from the pinned public receipt) --- +BILL = {1: 2437, 2: 724, 3: 226, 4: 102, 5: 20, 8: 8} +PRE_RETIMING_BILL = {1: 2439, 2: 726, 3: 224, 4: 102, 5: 20, 8: 8} +IDEAL_IDLE = {1: Fraction(234), 3: Fraction(261, 4), + 5: Fraction(57, 4), 48: Fraction(1531, 4)} +CAPACITY_COUNTS = {8: 672, 16: 448, 32: 448, 48: 448} +WIDTH_INVENTORY = {4: 26, 5: 2, 6: 18, 7: 52, 8: 97, 9: 213} +CAP_ROOT = (Fraction(432604724941517790951, 250000000000000000000000), + Fraction(346083779953214232761, 200000000000000000000000)) +CAP_ROOT_DECIMAL = ("0.001730418899766071163804", + "0.001730418899766071163805") +LITERAL_ROOT = (Fraction(21629929897674542689, 12500000000000000000000), + Fraction(1730394391813963415121, 1000000000000000000000000)) +LITERAL_ROOT_DECIMAL = ("0.001730394391813963415120", + "0.001730394391813963415121") +HEADROOM = Fraction(24507952107748683, 10 ** 24) +LITERAL_TO_CAP_FLOAT = "0.999985836983108" +PATTERNS, STRICT, SYMBOLIC_ZERO = 2551, 2539, 12 +IDEAL_740 = {1: 16403580, 2: 4821840, 3: 1553445, 4: 679320, + 5: 143745, 8: 53280, 48: 283235} + +# --- PR #3653 composed profile (quoted from the pinned public proof) --- +PROFILE_488 = {1: 10817496, 2: 3179808, 3: 1024434, 4: 447984, + 5: 94794, 8: 35136, 48: 186782} +CALLS_488, REPLICAS_488, CALLS_PER_REPLICA = 4392, 488, 9 +PROFILE_530 = {1: 11747920, 2: 3453480, 3: 1112042, 4: 486540, + 5: 103690, 8: 38160, 48: 202828} +CALLS_530, REPLICAS_530 = 4770, 530 +LIVE_PER_CALL, WIDTH = 896, 73 +RANK_MASS_PER_REPLICA = 65088 +PHYSICAL_488 = 437757 +RELEASED_488 = ("0.0017304188997660711638039999999999999999999998999999" + "999999999999999999") +MARGINS = (Fraction(1, 10 ** 46), Fraction(1, 10 ** 70)) + +getcontext().prec = 80 + + +def ideal_profile(replicas: int, calls: int) -> dict[int, Fraction]: + """Certificate's own construction: local bill per call + optimal idle bill.""" + profile = {r: Fraction(calls * q) for r, q in BILL.items()} + for r, q in IDEAL_IDLE.items(): + profile[r] = profile.get(r, Fraction(0)) + replicas * q + return profile + + +def as_decimal(value: Fraction, digits: int) -> str: + """Exact decimal string for a fraction whose denominator divides 10**digits.""" + assert (value * 10 ** digits).denominator == 1 + n = value.numerator * (10 ** digits // value.denominator) + sign = "-" if n < 0 else "" + n = abs(n) + return f"{sign}{n // 10 ** digits}.{n % 10 ** digits:0{digits}d}" + + +def moment(profile: dict[int, Fraction], a: Fraction, live: int) -> Decimal: + """M(a) = sum_r n_r*r^(1-a) - live*73^(1-a); root of M is the saving b.""" + assert 0 < a < 1 and live % LIVE_PER_CALL == 0 + e = Decimal(1) - Decimal(a.numerator) / Decimal(a.denominator) + total = Decimal(0) + for r, n in profile.items(): + nf = Fraction(n) + total += (Decimal(nf.numerator) / Decimal(nf.denominator)) * (Decimal(r) ** e) + total -= Decimal(live) * (Decimal(WIDTH) ** e) + return total + + +def rank_mass(profile: dict[int, Fraction]) -> Fraction: + return sum(Fraction(r) * n for r, n in profile.items()) + + +class Audit: + def __init__(self) -> None: + self.checks = 0 + self.controls = 0 + self.rows: dict[str, object] = {} + + def check(self, ok: bool, label: str) -> None: + if not ok: + raise SystemExit(f"FAIL {label}") + self.checks += 1 + + def control(self, rejected: bool, label: str) -> None: + if not rejected: + raise SystemExit(f"CONTROL NOT REJECTED {label}") + self.controls += 1 + + def record(self, key: str, value: object) -> None: + self.rows[key] = value + + +def main() -> None: + write = "--write" in sys.argv[1:] + audit = Audit() + + # 1. Convention cross-check on the certificate's own published ideal. + audit.check(CALLS_PER_REPLICA * 740 == 6660, "T740 has 6,660 calls") + audit.check(ideal_profile(740, 6660) == {r: Fraction(n) for r, n in IDEAL_740.items()}, + "T740 ideal profile follows the bill + idle rule") + audit.check(all(Fraction(n).denominator == 1 for n in ideal_profile(740, 6660).values()), + "T740 ideal profile is integral") + audit.record("ideal_profile_rule", "calls*bill + replicas*ideal_idle_per_replica") + + # 2. The composed profile is exactly the certificate's ideal at T=488. + audit.check(CALLS_488 == CALLS_PER_REPLICA * REPLICAS_488, "4,392 = 488*9 calls") + built = ideal_profile(REPLICAS_488, CALLS_488) + audit.check(built == {r: Fraction(n) for r, n in PROFILE_488.items()}, + "composed T488 profile equals the certificate's ideal at T=488") + audit.check(all(v.denominator == 1 for v in built.values()), + "T488 ideal is integer-attained (488 = 0 mod 4)") + audit.record("identity", "PROFILE_488 == 4392*bill + 488*ideal_idle_per_replica") + + # 3. Aggregate identities. + audit.check(rank_mass(built) == RANK_MASS_PER_REPLICA * REPLICAS_488, + "composed rank mass is 65088*488") + live = LIVE_PER_CALL * REPLICAS_488 + audit.check(live == 437248, "live stock is 896*488") + audit.check(PHYSICAL_488 == live + 408 + 8 + 91 + 2, + "physical 437757 = live + 408 helpers + 8 centers + 91 buffers + 2 fields") + audit.record("rank_mass", 65088 * 488) + audit.record("live", live) + audit.record("physical", PHYSICAL_488) + + # 4. Idle-bill decomposition is exact and matches the certificate. + idle = {r: PROFILE_488.get(r, 0) - CALLS_488 * BILL.get(r, 0) + for r in set(PROFILE_488) | set(BILL)} + idle = {r: Fraction(v, REPLICAS_488) for r, v in idle.items() if v} + audit.check(idle == IDEAL_IDLE, "residual equals ideal_idle_per_replica exactly") + audit.check(sum(Fraction(r) * q for r, q in idle.items()) == 18873, + "idle rank mass is 18873 per replica") + audit.check(sum(Fraction(r) * q for r, q in BILL.items()) == 5135, + "local bill rank mass is 5135 per call") + audit.check(CALLS_PER_REPLICA * 5135 + 18873 == RANK_MASS_PER_REPLICA, + "9*5135 + 18873 = 65088 per replica") + + # 5. Capacity feasibility of the ideal vertex at T=488. + for rank, cap in CAPACITY_COUNTS.items(): + count = Fraction(REPLICAS_488) * idle.get(rank, Fraction(0)) + audit.check(count <= cap * REPLICAS_488, + f"rank-{rank} child count within per-replica capacity") + audit.record("capacity_counts_per_replica", CAPACITY_COUNTS) + audit.record("width_inventory_per_call", WIDTH_INVENTORY) + + # 6. Moment bracket at the certificate's adjacent 10^-24 grid points. + lo, hi = CAP_ROOT + m_lo = moment(built, lo, live) + m_hi = moment(built, hi, live) + audit.check(m_lo < 0 < m_hi, + "composed moment straddles the certificate's cap bracket") + mid = (lo + hi) / 2 + e = Decimal(1) - Decimal(mid.numerator) / Decimal(mid.denominator) + deriv = -(sum((Decimal(Fraction(n).numerator) / Decimal(Fraction(n).denominator)) + * (Decimal(r) ** e) * Decimal(r).ln() + for r, n in built.items())) + deriv += Decimal(live) * (Decimal(WIDTH) ** e) * Decimal(WIDTH).ln() + audit.check(deriv > 0, "moment is strictly increasing at the bracket midpoint") + audit.check(moment(built, lo - Fraction(1, 10 ** 24), live) < 0 < + moment(built, hi + Fraction(1, 10 ** 24), live), + "straddle holds one grid step outside the bracket") + audit.record("M_at_cap_lower", str(m_lo)) + audit.record("M_at_cap_upper", str(m_hi)) + audit.record("M_prime_at_bracket_midpoint", str(deriv)) + + # 7. Released string, delta and headroom. + released = lo - MARGINS[0] - MARGINS[1] + audit.check(as_decimal(released, 70) == RELEASED_488, + "released decimal string reconstructs from the lower endpoint") + audit.check(released < lo < hi, "released value stays strictly below the bracket") + delta = lo - LITERAL_ROOT[0] + audit.check(delta == hi - LITERAL_ROOT[1], + "bracket shift is the same at both endpoints") + audit.check(abs(delta - HEADROOM) <= Fraction(1, 10 ** 24), + "bracket shift agrees with the published root headroom to one grid step") + audit.check(LITERAL_ROOT[0] < lo < hi and LITERAL_ROOT[1] < hi, + "the whole T530 literal bracket lies below the T488 cap bracket") + audit.record("released_kappa", RELEASED_488) + audit.record("delta_over_T530_floor", str(delta)) + audit.record("published_root_headroom", str(HEADROOM)) + audit.record("literal_to_cap_ratio_T530_quoted", LITERAL_TO_CAP_FLOAT) + audit.record("literal_to_cap_ratio_T488", "1 (the two profiles are identical)") + + # 8. Controls: the identity is not automatic. + # (a) The T530 literal is not at the ideal vertex. + t530_built = ideal_profile(REPLICAS_530, CALLS_530) + t530_diff = {r: t530_built.get(r, 0) - PROFILE_530.get(r, 0) + for r in set(t530_built) | set(PROFILE_530)} + audit.control(any(v != 0 for v in t530_diff.values()), + "T530 literal differs from the ideal profile") + t530_idle = {r: Fraction(PROFILE_530.get(r, 0) - CALLS_530 * BILL.get(r, 0), REPLICAS_530) + for r in set(PROFILE_530) | set(BILL)} + audit.control({r: v for r, v in t530_idle.items() if v} != IDEAL_IDLE, + "T530 literal residual is not the certificate's idle bill") + + # (b) Pre-retiming bill does not reconstruct the composed profile. + pre = {r: Fraction(CALLS_488 * q) for r, q in PRE_RETIMING_BILL.items()} + for r, q in IDEAL_IDLE.items(): + pre[r] = pre.get(r, Fraction(0)) + REPLICAS_488 * q + audit.control(pre != {r: Fraction(n) for r, n in PROFILE_488.items()}, + "pre-retiming local bill fails the identity") + + # (c) Wrong replica scaling fails. + wrong = {r: Fraction(CALLS_488 * q) for r, q in BILL.items()} + for r, q in IDEAL_IDLE.items(): + wrong[r] = wrong.get(r, Fraction(0)) + REPLICAS_530 * q + audit.control(wrong != {r: Fraction(n) for r, n in PROFILE_488.items()}, + "wrong replica count fails the identity") + + # (d) One rank-1 unit in the profile breaks the bracket. + mutated = dict(PROFILE_488) + mutated[1] += 1 + audit.control(not (moment(mutated, lo, live) < 0 < moment(mutated, hi, live)), + "one rank-1 unit shift breaks the certificate bracket") + + # (e) Swapped bracket endpoints are rejected by the sign straddle. + audit.control(not (moment(built, hi, live) < 0 < moment(built, lo, live)), + "swapped bracket endpoints fail the straddle") + + # (f) Integrality is load-bearing: T=490 (not a multiple of 4) is fractional. + frac = ideal_profile(490, 4410) + audit.control(any(v.denominator != 1 for v in frac.values()), + "T not divisible by 4 gives a fractional ideal profile") + audit.record("integrality_condition", "T = 0 mod 4; T=488 satisfies it") + + result = { + "audit": "t488-attains-retimed-packing-cap", + "outcome": "PASS_T488_ATTAINS_RETIMED_PACKING_CAP", + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "audited_pr3642_head": "6568db75adbb61437190545f6fef1534c70e91e5", + "audited_pr3653_head": "607a09ff441c79b215a8127a81f4cc70021d0d9b", + "identity": "PROFILE_488 = 4392*bill + 488*ideal_idle_per_replica", + "cap_root_bracket": list(CAP_ROOT_DECIMAL), + "checks": audit.checks, + "controls": audit.controls, + "no_new_kappa": True, + } + result.update(audit.rows) + if write: + (HERE / "RESULT.json").write_text( + json.dumps(result, indent=2, sort_keys=True) + "\n", encoding="utf-8") + print("wrote RESULT.json") + return + expected = json.loads((HERE / "RESULT.json").read_text(encoding="utf-8")) + if expected != json.loads(json.dumps(result)): + diff = sorted(set(expected) ^ set(result)) or [ + k for k in set(expected) & set(result) if expected[k] != result[k]] + raise SystemExit(f"FAIL RESULT.json mismatch: {diff[:6]}") + audit.check(True, "RESULT.json matches the recomputed receipt") + print("PASS_T488_ATTAINS_RETIMED_PACKING_CAP " + f"checks={audit.checks} controls={audit.controls} " + "identity_exact=true cap_attained=true no_new_kappa") + + +if __name__ == "__main__": + main() From 7f52e40c06ac9d58f44516336384a4c2ebd1213c Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Sun, 18 Oct 2026 22:24:47 +0100 Subject: [PATCH 2/2] docs(research): drop internal setup wording from the verifier header --- research/t488-attains-retimed-packing-cap/verify.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/research/t488-attains-retimed-packing-cap/verify.py b/research/t488-attains-retimed-packing-cap/verify.py index 4b1530ab7e..a641cafc0c 100644 --- a/research/t488-attains-retimed-packing-cap/verify.py +++ b/research/t488-attains-retimed-packing-cap/verify.py @@ -39,7 +39,7 @@ usage: verify.py [--write] -Nick Petalas, donated research session (worker 7), with AI assistance. +Produced by Nick Petalas with AI assistance. Apache-2.0. """ from __future__ import annotations