From 941810a486b6f6b4701194fcf5aead6fbaa74d24 Mon Sep 17 00:00:00 2001 From: commdata2338 <199849969+commdata2338@users.noreply.github.com> Date: Sat, 17 Oct 2026 13:03:19 -0500 Subject: [PATCH] Research: obstruct two simple orders for the coupled T20 packing cap Answers a bounded part of PR #3153's smaller-replica handoff, with PR #3148's coupled inventory fixed. In the inherited source-window model a cap-attaining packing needs one width-eight role in every capacity-eight bin, taken from a call inside that bin's window. At T20, stage-major order has 11,583 eligible roles for 13,440 such bins and replica-major order 5,940, forcing at least 1,857 and 7,500 non-tight bins. Written Hall-count proofs give 78T+297 and 375T for every positive T, also under replica permutations within complete stage or replica blocks. In the inherited packing dual each non-tight capacity-eight bin costs more than 3/250, so both orders push the complete moment above one at the cap bracket's left endpoint. The shipped interleaved T74 order passes the same necessary matching for all 49,728 bins. Conditional on the pinned inventory, window model, additive bin pricing and inherited local paid profile; arbitrary interleaved T20 orders, a full allocation and native or physical admission remain open. No new kappa. Adds research/coupled-t20-window-audit/ only. Submitted by @commdata2338 with substantial AI assistance (OpenAI Codex research and implementation; packaged with Claude Code). Co-Authored-By: Claude Opus 5.5 (1M context) Claude-Session: https://claude.ai/code/session_01X86sCSXdoDd61SDFfC1PKG --- research/coupled-t20-window-audit/README.md | 196 +++++++++ research/coupled-t20-window-audit/RESULT.json | 405 ++++++++++++++++++ .../coupled-t20-window-audit/SOURCES.json | 54 +++ research/coupled-t20-window-audit/TASK.json | 122 ++++++ research/coupled-t20-window-audit/VERIFY.json | 39 ++ .../coupled-t20-window-audit/test_verify.py | 143 +++++++ research/coupled-t20-window-audit/verify.py | 328 ++++++++++++++ 7 files changed, 1287 insertions(+) create mode 100644 research/coupled-t20-window-audit/README.md create mode 100644 research/coupled-t20-window-audit/RESULT.json create mode 100644 research/coupled-t20-window-audit/SOURCES.json create mode 100644 research/coupled-t20-window-audit/TASK.json create mode 100644 research/coupled-t20-window-audit/VERIFY.json create mode 100644 research/coupled-t20-window-audit/test_verify.py create mode 100644 research/coupled-t20-window-audit/verify.py diff --git a/research/coupled-t20-window-audit/README.md b/research/coupled-t20-window-audit/README.md new file mode 100644 index 0000000000..35ccfd01f4 --- /dev/null +++ b/research/coupled-t20-window-audit/README.md @@ -0,0 +1,196 @@ +# Two simple chronologies cannot attain the coupled-carrier packing cap + +**Scoped obstruction, with exact source-bound checks; no new kappa.** +The fixed PR3148/PR3153 inventory cannot attain its packing relaxation in +stage-major or replica-major order, for **any positive number T of replicas**. +At the first cap-integral count, T20, at least **1,857** or **7,500** capacity-eight +bins, respectively, must use a non-tight pattern. This answers a bounded part +of [PR3153's smaller-replica handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/3145#discussioncomment-18996207). +It leaves interleaved T20 orders open. + +| T20 order | Required capacity-eight bins | Eligible width-eight roles in their three neighborhoods | Forced non-tight bins | +| --- | ---: | ---: | ---: | +| Stage-major | 13,440 | 11,583 | 1,857 | +| Replica-major | 13,440 | 5,940 | 7,500 | + +An exact interval matching attains each displayed role count in a relaxation +that ignores all other helper widths and same-call physical-family conflicts. +The obstruction already holds in that favorable relaxation. No actual packing +or physical program is constructed. As a positive control, all **49,728** such +bins admit a matching for the shipped, interleaved T74 order. + +## Source contract and the new implication + +Keep the inherited provider inventory per local call +`{4:26, 5:2, 6:18, 7:50, 8:99, 9:213}` and local paid profile +`{1:2433, 2:724, 3:228, 4:102, 5:20, 8:8}` fixed. Both named providers have +these counts. Each replica executes stages 0 through 8 in increasing order. +A bin belongs to a replica, idle child, and one of 112 ports. Its window is +**open at the preceding touch and closed at its final stage**. + +A forward interpretation of the frozen template's local calls and bridges +reconstructs all eighteen child types. It agrees with all **666** serialized +windows of the original T37 plan. The six capacity-eight children are: + +| Children | Physical families within an owner | Window for owner r | +| --- | --- | --- | +| 1, 3 | 2, 3 | t(r,1) < time <= t(r,2) | +| 5, 7 | 4, 5 | t(r,3) < time <= t(r,4) | +| 9, 11 | 6, 7 | t(r,5) < time <= t(r,6) | + +Each row supplies 224 distinct bins per owner. The template's historical T37 +replication field is not asserted to construct T20: only its per-replica stage +and pending-window contract is transported to the two explicitly defined orders. + +The inherited packing dual has twelve tight patterns among 2,551 legal +patterns. Its **only tight capacity-eight pattern is [8]**. The primary replay +executes PR3153's authenticated exact arithmetic module, checks the entire +primal/dual pattern certificate, and evaluates all six other capacity-eight +patterns. It does not rely on a saved PASS receipt. Each other pattern has +reduced cost strictly greater than **3/250**, uniformly on the inherited +root bracket. Thus any cap-attaining allocation must place one distinct +width-eight role in every capacity-eight bin. This implication, combined with +the source windows, is the obstruction used here. + +## Proof + +For any set S of capacity-eight bins, let N(S) be the union of their eligible +call times. A call has only 99 width-eight roles. Therefore at most +`99 * |N(S)|` bins of S can receive the tight pattern [8]. At least +`max(0, |S| - 99*|N(S)|)` bins must be non-tight. Ignoring physical-family +conflicts enlarges the feasible set, so it cannot invalidate this lower bound. +This is the necessary matching-count inequality; it assumes neither an +allocation heuristic nor native supplier admission. + +**Stage-major.** Execute all T calls of stage 0, then all T of stage 1, and so +on. For either pair of children whose window runs from stage s to stage s+1, +where s is 1, 3, or 5, take all 224T associated bins. Their windows have at most +2T-1 eligible call times: the first call of stage s is excluded, and the last +possible deadline is the last call of stage s+1. Hence each group forces + +``` +224T - 99(2T-1) = 26T + 99 +``` + +non-tight bins. The three groups are distinct, giving **78T+297** overall. +This lower bound also holds with arbitrary replica permutations within each +complete stage block. For the increasing-replica order replayed here, the +eligible union has exactly 2T-1 calls and a matching fills all those slots. +At T20 the per-group counts are 4,480, 3,861 and 619. + +**Replica-major.** Execute all nine stages of one replica before beginning +the next. Each of the three short windows contains only its upper-stage call. +It has 224 demanded bins and 99 eligible roles. The 3T disjoint groups force +**125*3T = 375T** non-tight bins. This is independent of the permutation of +whole replicas. At T20 the per-stage-pair counts are 4,480, 1,980 and 2,500. + +A useful necessary condition for any changed interleaving is +`t(r,s+1)-t(r,s) >= 3` for s in {1,3,5}: one owner's 224 required placements +need at least three calls of capacity 99. These individual inequalities are +not sufficient, as the stage-major T20 counterexample shows; subsets of owners +must also satisfy the matching-count inequality. + +**Cost consequence.** Write `H_q(b)=q*(73/q)^b`, with H_0=0, and normalize the +complete inherited bill by `73*896*T`. At a fixed b in PR3153's cap bracket, +subtracting the same dual objective from every packing leaves the sum of bin +reduced costs. All are nonnegative; every forced non-tight capacity-eight bin +contributes more than 3/250. For T20 the normalized excess over the packing +relaxation is therefore strictly greater than + +``` +stage-major: 5571/327040000 (about 0.0000170346135) +replica-major: 9/130816 (about 0.0000687989237) +``` + +The complete inherited relaxation moment at the left endpoint +`b = 17297774946785970118869 / 10^25` is also enclosed in the replay. Adding +either exact penalty gives a lower bound above one. This rejects those orders +at that endpoint; it neither optimizes their smaller attainable exponent nor +changes the selected result. The claim is conditional on the pinned inventory, +window model, additive bin pricing, and inherited local paid profile. + +**Matching evidence.** The new checker uses earliest-deadline matching on +individual unit jobs, aggregating identical intervals for efficiency. Processing +slots in time order and choosing an available job with earliest deadline is +maximum-cardinality: in any maximum matching using a different available job +at that slot, exchange it with the chosen job's later assignment, if present; +its release is already past and its deadline is no earlier. If the chosen job +was unmatched, replace the other job. This preserves cardinality. The tests +compare the implementation with a separate exhaustive subset-matching oracle +on all 5,670 multisets/supply profiles in the stated tiny domain. The T20 Hall +upper bounds and actual matching counts independently certify equality. + +## Reproduce and evidence + +Python 3.12, standard library only; no solver, native compilation or network: + +```sh +python3 -I -B research/coupled-t20-window-audit/verify.py +python3 -I -B research/coupled-t20-window-audit/test_verify.py +python3 -B scripts/research_package.py --package research/coupled-t20-window-audit +``` + +Expected primary marker: + +```text +PASS_COUPLED_T20_WINDOW_AUDIT stage_major_deficit=1857 replica_major_deficit=7500 baseline_T74_deficit=0 cap8_bad_penalty_gt=3/250 +``` + +The primary replay finishes in about one second. `--emit` prints the full +regenerated receipt; the normal command compares every field with +[RESULT.json](RESULT.json). It records exact source intervals, all six short +Hall witnesses, matching hashes, rational reduced-cost bounds and moment +bounds. [SOURCES.json](SOURCES.json) pins six live inputs to the base commit. + +Controls cover the exhaustive matching oracle; open/closed window boundaries; +job and call capacities; all serialized source windows; physical-family aliases; +missing ports; duplicate or noncausal calls; changed provider widths and primal +counts; corrupted source bytes; and the complete optimized CLI. The written +closed forms cover all positive T; finite replays at T=1,2,3,20,74 corroborate +them. The published T74 order is a positive control for this necessary matching +relaxation only. Its passing count is not a new full allocation audit. + +## Scope and decision + +The original `complex-new-helper-inventory` card is **changed** to the explicit +PR3153 follow-up. It fixes the inventory and rejects two chronological realizations; +it does not propose a new helper type. [TASK.json](TASK.json) records the single +draw, scope change, overlap and the bounded stopping decision. Scientific base: +`463113d675af7410ac91d53a4fed51ec6494eb9a`, priority revision 6. + +**Decision: stop synthesis for these two chronology families.** + +## Open next questions + +The useful next +step remains a genuinely interleaved T20 order that passes the necessary matching +conditions, followed by an integral tight-pattern assignment with physical-family +exclusion and all other widths. First enforce the three individual gap constraints +and all interval matching constraints; reject a candidate before a large allocation +solve if any fail. Passing those constraints still leaves the full assignment, +chronology/bridges, compact offsets, native frames, dirty restoration, physical +stock/prefix/outer admission and all-size/analytic obligations open. This package +performs none of that synthesis or supplier admission, and does not prove T740 +necessary. A changed inventory or source contract requires a new cost calculation. + +The stock identity `896*T+509` would count 18,429 physical families at T20; +it is inherited bookkeeping conditional on a complete construction, not a +physical space bound established by this audit. No new lowering search or +family expansion is justified by the present negative result alone. + +## Credit + +Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance. +No independent human or proof-assistant review is claimed. Apache-2.0. + +Nick Petalas's PR3153 (`c509607d1208396ec0045f0ab79f8392fce40b01`) supplies +the independent cap audit, exact arithmetic reused here, and smaller-replica +handoff. Jeremy Diviney's PR3148 (`f2927a4b8afcf0701a6b945e14f30de1d94f5176`) +supplies the cap-attaining T740 construction. dcharb78's PR3133 supplies the +coupled inventory; Gonzalo Mier's PR3143 +(`dcfaf1d1a7cfebaab22b95776a36a543bc684d50`) supplies the comparison. +Nick Petalas's PR3024/3030, Marius-Paul Dumitrean's PR2979, Tekalign's owner +checker, Arham Tahir's PR3136 audit and the retained geometry/native/owner +contributors keep their predecessor credit. Hiroki Kumazaki's old-journal +transport test in Discussion3145 is a different, already completed task. +Original source files and their notices are retained unchanged. diff --git a/research/coupled-t20-window-audit/RESULT.json b/research/coupled-t20-window-audit/RESULT.json new file mode 100644 index 0000000000..d44dd88b64 --- /dev/null +++ b/research/coupled-t20-window-audit/RESULT.json @@ -0,0 +1,405 @@ +{ + "cap_premise": { + "all_pattern_margin_lower": "472769451967935797931856521500375206616817192841927929104466592736125577061/115792089237316195423570985008687907853269984665640564039457584007913129639936", + "cap8_bad_patterns": [ + { + "counts": [ + 0, + 0, + 0, + 0, + 0, + 0 + ], + "idle": 8, + "lower": "10241861022910743384624340204391709724177520348207761262806485636188978673255/463168356949264781694283940034751631413079938662562256157830336031652518559744" + }, + { + "counts": [ + 0, + 0, + 0, + 1, + 0, + 0 + ], + "idle": 1, + "lower": "1429901924765350981948120681947909880182545252331266648543974466116555909545/115792089237316195423570985008687907853269984665640564039457584007913129639936" + }, + { + "counts": [ + 0, + 0, + 1, + 0, + 0, + 0 + ], + "idle": 2, + "lower": "645058973320429136317999536529000178466586710326147960919001780143644653147/28948022309329048855892746252171976963317496166410141009864396001978282409984" + }, + { + "counts": [ + 0, + 1, + 0, + 0, + 0, + 0 + ], + "idle": 3, + "lower": "226580104130158853692729766706476671499271715454438039329436620282868911431/7237005577332262213973186563042994240829374041602535252466099000494570602496" + }, + { + "counts": [ + 1, + 0, + 0, + 0, + 0, + 0 + ], + "idle": 4, + "lower": "1586051973073831574712442725720668616871248482770246116964774089508889125885/57896044618658097711785492504343953926634992332820282019728792003956564819968" + }, + { + "counts": [ + 2, + 0, + 0, + 0, + 0, + 0 + ], + "idle": 0, + "lower": "667037298321281618766866993290964819222531066867085798756612616617495108345/28948022309329048855892746252171976963317496166410141009864396001978282409984" + } + ], + "cap_interval": [ + "17297774946785970118869/10000000000000000000000000", + "1729777494678597011887/1000000000000000000000000" + ], + "patterns": 2551, + "relaxation_moment_at_left_lower": "37868644864171888551324654544319000461482052556176367346546078895599699752288810487/37868644864171888551324654937241293384333415785051090063464208273947909917444669440", + "tight_patterns": 12, + "uniform_bad_bin_penalty_gt": "3/250" + }, + "historical_source_windows_checked": 666, + "orders": { + "replica_major": { + "calls": 180, + "groups": [ + { + "available_width8_roles": 1980, + "children": [ + 1, + 3 + ], + "deficit": 2500, + "demand": 4480, + "neighbor_calls": [ + 2, + 11, + 20, + 29, + 38, + 47, + 56, + 65, + 74, + 83, + 92, + 101, + 110, + 119, + 128, + 137, + 146, + 155, + 164, + 173 + ] + }, + { + "available_width8_roles": 1980, + "children": [ + 5, + 7 + ], + "deficit": 2500, + "demand": 4480, + "neighbor_calls": [ + 4, + 13, + 22, + 31, + 40, + 49, + 58, + 67, + 76, + 85, + 94, + 103, + 112, + 121, + 130, + 139, + 148, + 157, + 166, + 175 + ] + }, + { + "available_width8_roles": 1980, + "children": [ + 9, + 11 + ], + "deficit": 2500, + "demand": 4480, + "neighbor_calls": [ + 6, + 15, + 24, + 33, + 42, + 51, + 60, + 69, + 78, + 87, + 96, + 105, + 114, + 123, + 132, + 141, + 150, + 159, + 168, + 177 + ] + } + ], + "matched_in_relaxation": 5940, + "moment_at_cap_left_gt": "37871250186179728165721684891481695939408751130831344259236966691239877797705709047/37868644864171888551324654937241293384333415785051090063464208273947909917444669440", + "moment_excess_over_relaxation_gt": "9/130816", + "placement_sha256": "dca3496cf23a73f13de0a044060738395b0d0601d85d6c46c3493da45c2c7877", + "replicas": 20, + "required_cap8_bins": 13440, + "unmatched": 7500 + }, + "stage_major": { + "calls": 180, + "groups": [ + { + "available_width8_roles": 3861, + "children": [ + 1, + 3 + ], + "deficit": 619, + "demand": 4480, + "neighbor_calls": [ + 21, + 22, + 23, + 24, + 25, + 26, + 27, + 28, + 29, + 30, + 31, + 32, + 33, + 34, + 35, + 36, + 37, + 38, + 39, + 40, + 41, + 42, + 43, + 44, + 45, + 46, + 47, + 48, + 49, + 50, + 51, + 52, + 53, + 54, + 55, + 56, + 57, + 58, + 59 + ] + }, + { + "available_width8_roles": 3861, + "children": [ + 5, + 7 + ], + "deficit": 619, + "demand": 4480, + "neighbor_calls": [ + 61, + 62, + 63, + 64, + 65, + 66, + 67, + 68, + 69, + 70, + 71, + 72, + 73, + 74, + 75, + 76, + 77, + 78, + 79, + 80, + 81, + 82, + 83, + 84, + 85, + 86, + 87, + 88, + 89, + 90, + 91, + 92, + 93, + 94, + 95, + 96, + 97, + 98, + 99 + ] + }, + { + "available_width8_roles": 3861, + "children": [ + 9, + 11 + ], + "deficit": 619, + "demand": 4480, + "neighbor_calls": [ + 101, + 102, + 103, + 104, + 105, + 106, + 107, + 108, + 109, + 110, + 111, + 112, + 113, + 114, + 115, + 116, + 117, + 118, + 119, + 120, + 121, + 122, + 123, + 124, + 125, + 126, + 127, + 128, + 129, + 130, + 131, + 132, + 133, + 134, + 135, + 136, + 137, + 138, + 139 + ] + } + ], + "matched_in_relaxation": 11583, + "moment_at_cap_left_gt": "4733661242737628704981169907284560482727087890407617453766042839225025979541754321307/4733580608021486068915581867155161673041676973131386257933026034243488739680583680000", + "moment_excess_over_relaxation_gt": "5571/327040000", + "placement_sha256": "8f709bbd1e66d3eda465e99dd5a8db37e9d06caef534b1634e92b6760d55a707", + "replicas": 20, + "required_cap8_bins": 13440, + "unmatched": 1857 + } + }, + "positive_T74": { + "calls": 666, + "matched_in_relaxation": 49728, + "placement_sha256": "c4c34672f620658e128103d895099923b54251429936144af22881ff31871c32", + "replicas": 74, + "required_cap8_bins": 49728, + "unmatched": 0 + }, + "scope": "Two chronology families excluded from the inherited cap; arbitrary T20 orders and supplier admission remain open.", + "source_intervals": { + "1": [ + 8, + 1, + 2, + 2 + ], + "11": [ + 8, + 5, + 6, + 7 + ], + "3": [ + 8, + 1, + 2, + 3 + ], + "5": [ + 8, + 3, + 4, + 4 + ], + "7": [ + 8, + 3, + 4, + 5 + ], + "9": [ + 8, + 5, + 6, + 6 + ] + }, + "status": "PASS_COUPLED_T20_WINDOW_AUDIT" +} diff --git a/research/coupled-t20-window-audit/SOURCES.json b/research/coupled-t20-window-audit/SOURCES.json new file mode 100644 index 0000000000..ceeca7c17c --- /dev/null +++ b/research/coupled-t20-window-audit/SOURCES.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "base_commit": "463113d675af7410ac91d53a4fed51ec6494eb9a", + "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" + }, + { + "path": "research/coupled-cap-independent/arithmetic.py", + "usage": "input", + "git_blob": "b2a6b13673256f6ae41818352aff456461b7bbe1", + "sha256": "1d9b1983e16e000f3bea75ac019356f1a30775db85ee4d6eeba409b26cc219f5" + }, + { + "path": "research/coupled-cap-independent/vendor/CAP.json", + "usage": "input", + "git_blob": "804edbf26529d259e473ec5c79b7755370001cdc", + "sha256": "e32f3ecd5e6594935583f80f643cf1930e8bc017e3c541025c335395a15cf19c" + }, + { + "path": "research/coupled-cap-independent/vendor/PROVIDERS.json", + "usage": "input", + "git_blob": "0b2343675099d0a9fe90da6e1f1e53f50235567e", + "sha256": "52eb0d85caa7b2d4a93acdf5011f52b793f61ddca86235fb03cd9a09397ad4cd" + }, + { + "path": "research/rank7-joint-endframes/allocation/ORDER.json", + "usage": "input", + "git_blob": "7409c4df1092241729739596c7648bda504e6aad", + "sha256": "519d1d5dbb997a219fcfcad34c0b03e7838bef24199784d7e964fa10090f66e1" + }, + { + "path": "research/rank7-joint-endframes/allocation/vendor/PLAN.json.gz", + "usage": "input", + "git_blob": "7a1db55a4d53ee99280be4f3ab7d29f7b2033adf", + "sha256": "d566cfb87b71639d4138e1f89b543e2dd6a7772070226a2a14c799a6835bf21e" + }, + { + "path": "research/rank7-joint-endframes/allocation/vendor/TEMPLATE.json.gz", + "usage": "input", + "git_blob": "114808c32b1799da53524bdc25cea67efb60009e", + "sha256": "21297b20f1f2dc76eb9dd8124416068c3cb096bab9df17fa4da19bc68dfe082e" + } + ] +} diff --git a/research/coupled-t20-window-audit/TASK.json b/research/coupled-t20-window-audit/TASK.json new file mode 100644 index 0000000000..edf24baa4f --- /dev/null +++ b/research/coupled-t20-window-audit/TASK.json @@ -0,0 +1,122 @@ +{ + "schema_version": 1, + "task_id": "complex-new-helper-inventory", + "priority_revision": 6, + "base_commit": "463113d675af7410ac91d53a4fed51ec6494eb9a", + "original_card": { + "id": "complex-new-helper-inventory", + "question": "Can a new local cost interface change the deficit-to-recursive-cost ratio beyond current packing?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/complex-local-word-ceiling/README.md", + "research/heterogeneous-owner-assembly/README.md", + "certificates/selected-result.json", + "research/selected-k8-unrestricted-ends/README.md" + ], + "methods": [ + "Propose a changed helper inventory and derive an optimistic exact moment.", + "Design a small completed instance and independently verify its endpoint and rank bill." + ], + "acceptance_gate": "A new physically realizable contract outside the frozen catalogue whose per-call profile, screened with ceiling.ceiling(), beats the selected word's packing ceiling; a lower cap does not establish identical circuitry or order attainable optima, and is insufficient to pass the stronger-budget target under this model. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/complex-local-word-ceiling/verify.py" + ], + "expected": "PASS_COMPLEX_LOCAL_WORD_CEILING", + "inspect": "Read the selected word's per-call local profile, its packing ceiling and the lever table; run levers.py for the ideal budget of the lever you target.", + "scope": "Positive control and planning budget only; this is not a new construction or full cold replay." + }, + "first_experiment": "Before any synthesis, write the candidate per-call local profile (and centre charge / unpaid coordinates if changed) and screen it with ceiling.ceiling(); reject it if even the ideal ceiling does not beat the selected word's by your stated margin.", + "bottleneck_link": "Packing of the selected word is capped at +0.87% (ceiling model); only a lower local excess spend or a changed coverage law raises the cap.", + "allowed_variations": [ + "Narrow to one changed boundary or helper type with explicit counts.", + "If the coverage law, template or guard changes, derive an applicable fully charged replacement bound instead of applying the incumbent ceiling outside its scope." + ], + "scope_change_triggers": [ + "Mixing only providers already inside the pinned catalogue.", + "Only changing helper terminal subspaces and monotone frames within the fixed scalar word, entrances and cleanup contract already covered by #1995/#2013.", + "Continuing a partial cost improvement while leaving the same unpriced consumer, restoration or central-readout obligation unresolved; refresh the family expansion decision first. Local product-retiming evidence has a narrow scope and is not a ban on changed graphs or contracts." + ], + "overlap_terms": [ + "helper inventory", + "heterogeneous-owner", + "mutable leaver" + ] + }, + "scope_status": "changed", + "actual_scope": "Source-bound Hall obstructions to the fixed coupled inventory at T20 in stage-major and replica-major orders; general closed forms for both order families.", + "scope_change_reason": "The chooser third suggestion exposed Discussion3145; PR3148/3153 have already completed its original T740 journal task. PR3153 explicitly asks for smaller-replica chronology. This bounded audit fixes inventory instead of inventing a new helper type.", + "bottleneck_link": "Pattern integrality at T20 is insufficient: short pending windows force non-tight bins, whose positive dual costs prevent these orders from attaining the inherited cap. Avoiding a doomed allocation synthesis is the contribution.", + "budget_minutes": 60, + "stop_rule": "Stop after rejecting the two named orders and checking the inherited cost implication. No search of arbitrary T20 interleavings or dependent native implementation.", + "outcome": "completed", + "evidence": "RESULT.json: source-bound T20 deficits 1857 and 7500; all 666 historical windows; positive T74 necessary matching; 2551 inherited packing patterns and six strict cap8 penalties; nine behavioral groups including 5670 exhaustive matching cases.", + "author": "commdata2338", + "ai_assistance": "Substantial OpenAI Codex assistance in derivation, implementation, checking and writing; no independent human review claimed.", + "open_questions": [ + { + "question": "Can a genuinely interleaved T20 order attain the same fixed-inventory cap?", + "why_it_matters": "The residue condition permits T20 but the two simplest chronology families now fail necessary source-window constraints.", + "first_step": "Enforce t(r,s+1)-t(r,s)>=3 for s=1,3,5 and the full capacity-eight interval matching conditions before attempting all-width tight-pattern allocation.", + "blocked_by": "No such chronology or all-width physical-family-compatible assignment is constructed; native/physical/prefix/outer and all-size admission remain separate." + } + ], + "selection": { + "track": "complex-mechanisms", + "nonce": "040d85d315302c1011c104d7d415cc28", + "scope_key": "5868e5281a1e63d41a22", + "chosen_suggestion": 3, + "handoff": "https://github.com/CrocSwap/integer-mult-bounds/discussions/3145#discussioncomment-18996207", + "refined_scope_key": "coupled-T20-two-orders-window-obstruction", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/3145#discussioncomment-19001819" + }, + "dependency_heads": { + "PR3153": "c509607d1208396ec0045f0ab79f8392fce40b01", + "PR3148": "f2927a4b8afcf0701a6b945e14f30de1d94f5176", + "PR3143": "dcfaf1d1a7cfebaab22b95776a36a543bc684d50" + }, + "overlap": { + "checked_main": "463113d675af7410ac91d53a4fed51ec6494eb9a", + "open_prs_fetched_at": "2026-10-17T17:04:11.636955+00:00", + "discussions_fetched_at": "2026-10-17T17:04:42.538402+00:00", + "queries": [ + "complex-new-helper-inventory", + "T20 AND coupled" + ], + "nearest": [ + "PR3148 realizes T740", + "PR3153 audits T740 and leaves smaller chronology open", + "Discussion3145 old-journal transport test is complete" + ], + "limits": "Offline cached snapshots with complete reported pagination; no arbitrary code-diff or unpublished-work coverage.", + "final_coverage": { + "open_prs": { + "fetched_at": "2026-10-17T17:26:19.594925+00:00", + "complete_pagination": true, + "records": 249 + }, + "discussions": { + "fetched_at": "2026-10-17T17:27:03.117721+00:00", + "complete_pagination": true, + "records": 2001 + } + }, + "final_limits": "Anonymous offline snapshots; complete reported pagination. Canonical main was fetched directly. Discussion3145 includes the scoped claim; no competing T20 two-order audit found." + }, + "obligation_ledger": { + "proved": "Two order-family Hall deficits and conditional positive moment penalties.", + "replayed_inherited": "Packing dual and exact source window tables.", + "unknown": "Arbitrary T20 chronology, full assignment, all physical/native/prefix/outer and all-size admission.", + "decision": "Narrow and stop; no dependent construction round." + }, + "refresh_checkpoint": { + "checked_at": "2026-10-17T17:36:47+00:00", + "base": "463113d675af7410ac91d53a4fed51ec6494eb9a", + "main": "463113d675af7410ac91d53a4fed51ec6494eb9a", + "changed_paths": [], + "priority_revision": 6, + "decision": "Continue the fixed scope; canonical main and guidance are unchanged." + } +} diff --git a/research/coupled-t20-window-audit/VERIFY.json b/research/coupled-t20-window-audit/VERIFY.json new file mode 100644 index 0000000000..7b8db4270f --- /dev/null +++ b/research/coupled-t20-window-audit/VERIFY.json @@ -0,0 +1,39 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/coupled-cap-independent/arithmetic.py", + "research/coupled-cap-independent/vendor/CAP.json", + "research/coupled-cap-independent/vendor/PROVIDERS.json", + "research/rank7-joint-endframes/allocation/ORDER.json", + "research/rank7-joint-endframes/allocation/vendor/PLAN.json.gz", + "research/rank7-joint-endframes/allocation/vendor/TEMPLATE.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-Werror", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Two T20 Hall witnesses, 666 source windows, published T74 positive relaxation, authenticated inherited packing dual and exact moment penalties." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 60, + "checks": "Nine behavioral groups including 5670 separate exhaustive matching cases, source/cost/boundary mutations and optimized CLI." + } + ] +} diff --git a/research/coupled-t20-window-audit/test_verify.py b/research/coupled-t20-window-audit/test_verify.py new file mode 100644 index 0000000000..98811314b2 --- /dev/null +++ b/research/coupled-t20-window-audit/test_verify.py @@ -0,0 +1,143 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Behavioral controls for the window obstruction, including a separate oracle.""" + +import copy +import itertools +import json +import subprocess +import sys +import tempfile +import unittest +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import verify as v + + +def subset_oracle(jobs, supplies): + """Independent exhaustive matching by reachable subsets of individual slots.""" + slots = [time for time, count in enumerate(supplies) for _ in range(count)] + states = {0} + for first, last, count, *_ in jobs: + for _ in range(count): + previous = set(states) + for state in previous: + for i, time in enumerate(slots): + if first <= time <= last and not state & (1 << i): + states.add(state | (1 << i)) + return max(map(int.bit_count, states)) + + +class WindowTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.data = v.authenticate() + cls.template = v.decoded(cls.data[v.ALLOC + "vendor/TEMPLATE.json.gz"], True) + cls.plan = v.decoded(cls.data[v.ALLOC + "vendor/PLAN.json.gz"], True) + cls.source = v.source_types(cls.template, cls.plan) + + def test_matching_exhaustive_oracle(self): + intervals = [(a, b) for a in range(3) for b in range(a, 3)] + cases = 0 + for size in range(5): + for selected in itertools.combinations_with_replacement(intervals, size): + jobs = [(a, b, 1) for a, b in selected] + for supplies in itertools.product(range(3), repeat=3): + actual, witness = v.interval_matching(jobs, supplies) + self.assertEqual(actual, subset_oracle(jobs, supplies)) + self.assertEqual(actual, v.validate_matching(jobs, supplies, witness)) + cases += 1 + self.assertEqual(cases, 5670) + + def test_boundary_and_capacity_controls(self): + jobs = [(1, 1, 2)] + self.assertEqual(v.interval_matching(jobs, [2, 1])[0], 1) + self.assertEqual(v.interval_matching([(0, 1, 2)], [2, 1])[0], 2) + with self.assertRaisesRegex(ValueError, "source window"): + v.validate_matching(jobs, [2, 1], [(0, 0, 1)]) + with self.assertRaisesRegex(ValueError, "call capacity"): + v.validate_matching(jobs, [2, 1], [(1, 0, 2)]) + with self.assertRaisesRegex(ValueError, "job capacity"): + v.validate_matching(jobs, [2, 3], [(1, 0, 2), (1, 0, 1)]) + + def test_source_cuts_and_all_plan_windows(self): + self.assertEqual(v.check_published_windows(self.source, self.plan), 666) + altered = copy.deepcopy(self.template) + event = next(e for e in altered["execution_schedule"] + if e["kind"] == "idle_cover_sweep" and e["from_level"] == 1) + event["from_level"] = 0 + with self.assertRaisesRegex(ValueError, "declared/actual"): + v.source_types(altered, self.plan) + plan = copy.deepcopy(self.plan) + plan["windows"]["0,1"][1].insert(0, 0) + with self.assertRaisesRegex(ValueError, "historical windows"): + v.check_published_windows(self.source, plan) + + def test_physical_family_and_port_binding(self): + plan = copy.deepcopy(self.plan) + plan["sides"]["3"] = plan["sides"]["1"] + with self.assertRaisesRegex(ValueError, "distinct physical families"): + v.source_types(self.template, plan) + template = copy.deepcopy(self.template) + template["idle_children"].pop() + with self.assertRaisesRegex(ValueError, "port domain"): + v.source_types(template, self.plan) + + def test_closed_forms_and_published_positive(self): + for replicas in (1, 2, 3, 20, 74): + for kind in ("stage_major", "replica_major"): + result = v.chronology_result(self.source, v.order_for(replicas, kind), kind) + expected = 3 * (26 * replicas + 99) if kind == "stage_major" else 375 * replicas + self.assertEqual(result["unmatched"], expected) + published = v.decoded(self.data[v.ALLOC + "ORDER.json"]) + self.assertEqual(v.chronology_result(self.source, published, "positive")["unmatched"], 0) + + def test_call_identity_and_causality(self): + order = v.order_for(2, "stage_major") + order[0] = order[1] + with self.assertRaisesRegex(ValueError, "unique call"): + v.times_for(order) + order = v.order_for(2, "stage_major") + order[0], order[2] = order[2], order[0] + with self.assertRaisesRegex(ValueError, "causal replica"): + v.times_for(order) + + def test_provider_and_primal_mutants(self): + data = dict(self.data) + path = v.PREDECESSOR + "vendor/PROVIDERS.json" + providers = v.decoded(data[path]) + providers["extra"]["widths"][2] = 7 + data[path] = json.dumps(providers).encode() + with self.assertRaisesRegex(ValueError, "provider widths"): + v.cap_premise(data) + data = dict(self.data) + path = v.PREDECESSOR + "vendor/CAP.json" + cap = v.decoded(data[path]) + cap["basis_patterns"][0]["count_per_replica"] = "671" + data[path] = json.dumps(cap).encode() + with self.assertRaisesRegex(ValueError, "primal conservation"): + v.cap_premise(data) + + def test_source_corruption_rejects(self): + with tempfile.TemporaryDirectory(prefix="t20-source-") as directory: + root = Path(directory) + for name, raw in self.data.items(): + target = root / name + target.parent.mkdir(parents=True, exist_ok=True) + target.write_bytes(raw) + self.assertEqual(v.authenticate(root), self.data) + target = root / (v.PREDECESSOR + "arithmetic.py") + target.write_bytes(target.read_bytes() + b"\n# changed\n") + with self.assertRaisesRegex(ValueError, "source bytes"): + v.authenticate(root) + + def test_optimized_complete_cli(self): + command = [sys.executable, "-I", "-O", "-Werror", "-B", str(v.PACKAGE / "verify.py")] + result = subprocess.run(command, capture_output=True, text=True, timeout=60) + self.assertEqual(result.returncode, 0, result.stderr) + self.assertIn("PASS_COUPLED_T20_WINDOW_AUDIT", result.stdout) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/coupled-t20-window-audit/verify.py b/research/coupled-t20-window-audit/verify.py new file mode 100644 index 0000000000..1ec6d06584 --- /dev/null +++ b/research/coupled-t20-window-audit/verify.py @@ -0,0 +1,328 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Source-window obstructions to two orders of the fixed coupled inventory. + +The combinatorial argument is new here. Authenticated PR3153 arithmetic +supplies the inherited packing-dual and interval-arithmetic premise. +Prepared for commdata2338 with substantial OpenAI Codex assistance. +""" + +import argparse +import gzip +import hashlib +import heapq +import json +import types +from collections import Counter +from fractions import Fraction +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +ALLOC = "research/rank7-joint-endframes/allocation/" +PREDECESSOR = "research/coupled-cap-independent/" +INVENTORY = {4: 26, 5: 2, 6: 18, 7: 50, 8: 99, 9: 213} +LOCAL = {1: 2433, 2: 724, 3: 228, 4: 102, 5: 20, 8: 8} +PORTS = 112 +DELTA = Fraction(3, 250) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def unique_object(pairs): + result = {} + for key, value in pairs: + require(key not in result, "duplicate JSON key") + result[key] = value + return result + + +def decoded(raw, compressed=False): + if compressed: + raw = gzip.decompress(raw) + require(len(raw) <= 32_000_000, "bounded decoded input") + return json.loads(raw, object_pairs_hook=unique_object) + + +def authenticate(root=ROOT): + manifest = decoded((PACKAGE / "SOURCES.json").read_bytes()) + data = {} + for row in manifest["files"]: + if row["usage"] != "input": + continue + path = row["path"] + require(not Path(path).is_absolute() and ".." not in Path(path).parts, + "relative source path") + target = root / path + require(target.is_file() and not target.is_symlink() and + target.stat().st_size <= 2_000_000, "bounded regular source") + raw = target.read_bytes() + require(hashlib.sha256(raw).hexdigest() == row["sha256"], + "source bytes: " + path) + data[path] = raw + require(len(data) == 6, "six live source inputs") + return data + + +def source_types(template, plan): + """Forward last-touch interpretation of the literal execution schedule.""" + capacities, port_sets = {}, {} + for entry in template["idle_children"]: + child, rank, port = entry["child"], entry["rank"], entry["port"] + require(child not in capacities or capacities[child] == rank, + "consistent child rank") + capacities[child] = rank + ports = port_sets.setdefault(child, set()) + require(port not in ports, "unique declared child port") + ports.add(port) + require(set(capacities) == set(range(18)) and + all(ports == set(range(PORTS)) for ports in port_sets.values()), + "complete eighteen-child port domain") + pairs = {e["stage"]: e["pair"] for e in template["recipe"] + if e["kind"] == "local"} + touched = dict.fromkeys(range(4)) + stage, result = None, {} + for event in template["execution_schedule"]: + kind = event["kind"] + if kind == "local_cover_sweep": + stage = event["stage"] + touched[pairs[stage]] = stage + elif kind == "bridge": + touched[event["src"]] = touched[event["dst"]] = stage + elif kind == "idle_cover_sweep": + before = touched[event["pair"]] + require(event["from_level"] == (-1 if before is None else before) + and event["to_level"] == stage, "declared/actual source cut") + for child in event["child_indices"]: + if child not in capacities: + continue + require(child not in result, "unique source interval") + require(plan["pairs"][str(child)] == event["pair"], "pair binding") + family = 2 * event["pair"] + plan["sides"][str(child)] + result[child] = (capacities[child], before, stage, family) + else: + require(kind in {"terminal_Y_translations", "terminal", + "bank_padding_cover_sweep", "translate_every_live_family"}, + "known schedule event") + require(set(result) == set(range(18)), "all source intervals recovered") + small = {c: row for c, row in result.items() if row[0] == 8} + require(small == {1: (8, 1, 2, 2), 3: (8, 1, 2, 3), + 5: (8, 3, 4, 4), 7: (8, 3, 4, 5), + 9: (8, 5, 6, 6), 11: (8, 5, 6, 7)}, + "six source-bound short intervals and distinct physical families") + return result + + +def times_for(order): + require(len(order) > 0 and len(order) % 9 == 0, "complete call count") + replicas = len(order) // 9 + times = [[None] * 9 for _ in range(replicas)] + for time, entry in enumerate(order): + require(len(entry) == 2 and all(type(x) is int for x in entry), "typed call") + stage, replica = entry + require(0 <= stage < 9 and 0 <= replica < replicas, "call domain") + require(times[replica][stage] is None, "unique call") + times[replica][stage] = time + require(all(None not in row and row == sorted(row) for row in times), + "complete causal replica order") + return times + + +def order_for(replicas, kind): + require(type(replicas) is int and 1 <= replicas <= 740, "bounded replica count") + if kind == "stage_major": + return [(s, r) for s in range(9) for r in range(replicas)] + require(kind == "replica_major", "named order") + return [(s, r) for r in range(replicas) for s in range(9)] + + +def jobs_for(source, times): + # One unit job is the required [8] placement of one physical child/port. + return [(row[before] + 1, row[after], PORTS, owner, child, family) + for owner, row in enumerate(times) + for child, (rank, before, after, family) in sorted(source.items()) + if rank == 8] + + +def check_published_windows(source, plan): + """Compare all reconstructed windows with the original T37 plan tables.""" + times = times_for(plan["order"]) + require(len(times) == plan["T"] == 37, "historical plan replication count") + expected = {} + for owner, row in enumerate(times): + for child, (rank, before, after, _) in source.items(): + left = -1 if before is None else row[before] + expected[f"{owner},{child}"] = [rank, list(range(left + 1, row[after] + 1))] + require(plan["windows"] == expected, "all reconstructed historical windows") + return len(expected) + + +def interval_matching(jobs, supplies): + """Maximum interval-to-slot matching; earliest-deadline greedy exchange.""" + require(all(type(n) is int and n >= 0 for n in supplies), "nonnegative supply") + require(all(0 <= a <= b < len(supplies) and type(n) is int and n > 0 + for a, b, n, *_ in jobs), "valid closed job interval") + releases = sorted((job[0], i) for i, job in enumerate(jobs)) + cursor, matched, heap, placements = 0, 0, [], [] + for time, supply in enumerate(supplies): + while cursor < len(releases) and releases[cursor][0] <= time: + _, i = releases[cursor] + heapq.heappush(heap, (jobs[i][1], i, jobs[i][2])) + cursor += 1 + while heap and supply: + deadline, i, left = heapq.heappop(heap) + if deadline < time: + continue + used = min(left, supply) + matched += used + supply -= used + placements.append((time, i, used)) + if left > used: + heapq.heappush(heap, (deadline, i, left - used)) + return matched, placements + + +def validate_matching(jobs, supplies, placements): + by_job, by_time = Counter(), Counter() + for time, i, count in placements: + require(type(count) is int and count > 0 and 0 <= i < len(jobs), + "positive matching entry") + require(jobs[i][0] <= time <= jobs[i][1], "matching stays inside source window") + by_job[i] += count + by_time[time] += count + require(all(n <= jobs[i][2] for i, n in by_job.items()), "job capacity") + require(all(n <= supplies[t] for t, n in by_time.items()), "call capacity") + return sum(by_job.values()) + + +def hall_witness(jobs, supplies, children): + subset = [j for j in jobs if j[4] in children] + neighbors = sorted({t for a, b, *_ in subset for t in range(a, b + 1)}) + demand = sum(j[2] for j in subset) + available = sum(supplies[t] for t in neighbors) + return {"children": list(children), "demand": demand, + "neighbor_calls": neighbors, "available_width8_roles": available, + "deficit": max(0, demand - available)} + + +def chronology_result(source, order, kind): + replicas = len(order) // 9 + jobs = jobs_for(source, times_for(order)) + supplies = [INVENTORY[8]] * len(order) + matched, placements = interval_matching(jobs, supplies) + require(validate_matching(jobs, supplies, placements) == matched, "matching witness") + groups = [hall_witness(jobs, supplies, cs) for cs in ((1, 3), (5, 7), (9, 11))] + if kind in {"stage_major", "replica_major"}: + groups_union = set().union(*(set(g["neighbor_calls"]) for g in groups)) + require(len(groups_union) == sum(len(g["neighbor_calls"]) for g in groups), + "three disjoint Hall neighborhoods") + expected = 3 * (26 * replicas + 99) if kind == "stage_major" else 375 * replicas + require(sum(g["deficit"] for g in groups) == expected, "symbolic deficit formula") + require(672 * replicas - matched == expected, "matching attains Hall upper bound") + return {"replicas": replicas, "calls": len(order), "required_cap8_bins": 672 * replicas, + "matched_in_relaxation": matched, "unmatched": 672 * replicas - matched, + "placement_sha256": hashlib.sha256(json.dumps(placements).encode()).hexdigest(), + "groups": groups} + + +def reduced_costs(module, patterns, basis, intervals): + dual = module.dual_coefficients(basis) + result = [] + for capacity, counts, idle in patterns: + if capacity != 8: + continue + coefficients = {r: Fraction(r == idle) for r in range(1, 49)} + for j, rank in enumerate((1, 3, 5, 48)): + coefficients[rank] -= sum(v * dual[i][j] + for i, v in enumerate(module.features(capacity, counts))) + if any(coefficients.values()): + lower = sum(c * intervals[r][int(c < 0)] for r, c in coefficients.items()) + require(lower > DELTA, "strict cap8 reduced-cost lower bound") + result.append({"counts": list(counts), "idle": idle, "lower": str(lower)}) + else: + require(counts == (0, 0, 0, 0, 1, 0), "only tight cap8 pattern is [8]") + require(len(result) == 6, "all six non-[8] patterns") + return result + + +def cap_premise(data): + """Replay the inherited dual, rather than assume stored PASS metadata.""" + providers = decoded(data[PREDECESSOR + "vendor/PROVIDERS.json"]) + require(set(providers) == {"extra", "gauge44"}, "both providers") + for value in providers.values(): + require(Counter(value["widths"]) == INVENTORY and len(value["widths"]) == 408, + "source-bound provider widths") + require({int(k): v for k, v in value["actual_paid_profile"].items()} == LOCAL, + "source-bound local paid profile") + module = types.ModuleType("authenticated_pr3153_arithmetic") + raw = data[PREDECESSOR + "arithmetic.py"] + exec(compile(raw, PREDECESSOR + "arithmetic.py", "exec", optimize=0), module.__dict__) + cap = decoded(data[PREDECESSOR + "vendor/CAP.json"]) + patterns, basis, amounts, rhs = module.check_primal(cap, INVENTORY, LOCAL) + lower, upper = Fraction(cap["cap_lower"]), Fraction(cap["cap_upper"]) + intervals = module.child_intervals(lower, upper) + tight, margin = module.check_dual(patterns, basis, rhs, intervals) + require([(c, ns) for c, ns in tight if c == 8] == [(8, (0, 0, 0, 0, 1, 0))], + "unique tight capacity-eight pattern") + penalties = reduced_costs(module, patterns, basis, intervals) + profile = Counter({r: 180 * n for r, n in LOCAL.items()}) + for (_, _, idle), amount in zip(basis, amounts, strict=True): + require((20 * amount).denominator == 1, "T20 integral primal") + if idle: + profile[idle] += int(20 * amount) + baseline_lower = module.moment(profile, lower, 20)[0] + return {"cap_interval": [str(lower), str(upper)], "patterns": len(patterns), + "tight_patterns": len(tight), "all_pattern_margin_lower": str(margin), + "cap8_bad_patterns": penalties, "uniform_bad_bin_penalty_gt": str(DELTA), + "relaxation_moment_at_left_lower": str(baseline_lower)} + + +def verify(data=None): + if data is None: + data = authenticate() + template = decoded(data[ALLOC + "vendor/TEMPLATE.json.gz"], True) + plan = decoded(data[ALLOC + "vendor/PLAN.json.gz"], True) + source = source_types(template, plan) + published_windows = check_published_windows(source, plan) + cap = cap_premise(data) + orders = {kind: chronology_result(source, order_for(20, kind), kind) + for kind in ("stage_major", "replica_major")} + baseline = decoded(data[ALLOC + "ORDER.json"]) + positive = chronology_result(source, baseline, "published_T74") + require(positive["replicas"] == 74 and positive["unmatched"] == 0, + "published staggered order survives necessary matching relaxation") + lp_lower = Fraction(cap["relaxation_moment_at_left_lower"]) + for result in orders.values(): + gap = result["unmatched"] * DELTA / (73 * 896 * 20) + require(lp_lower + gap > 1, "complete inherited moment exceeds one at cap left") + result["moment_excess_over_relaxation_gt"] = str(gap) + result["moment_at_cap_left_gt"] = str(lp_lower + gap) + return {"status": "PASS_COUPLED_T20_WINDOW_AUDIT", "source_intervals": + {str(k): list(v) for k, v in sorted(source.items()) if v[0] == 8}, + "historical_source_windows_checked": published_windows, + "cap_premise": cap, "orders": orders, + "positive_T74": {k: v for k, v in positive.items() if k != "groups"}, + "scope": "Two chronology families excluded from the inherited cap; " + "arbitrary T20 orders and supplier admission remain open."} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", action="store_true") + args = parser.parse_args() + result = verify() + if args.emit: + print(json.dumps(result, indent=2, sort_keys=True)) + else: + expected = decoded((PACKAGE / "RESULT.json").read_bytes()) + require(json.dumps(result, sort_keys=True) == json.dumps(expected, sort_keys=True), + "complete typed receipt equality") + print(result["status"], "stage_major_deficit=1857 replica_major_deficit=7500", + "baseline_T74_deficit=0 cap8_bad_penalty_gt=3/250") + + +if __name__ == "__main__": + main()