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()