From cc43a233ad989e717c8d46c6398ee50f97f5c0b9 Mon Sep 17 00:00:00 2001 From: Adam Gall Date: Wed, 14 Oct 2026 09:46:54 -0400 Subject: [PATCH] Certify composed scalar centre source maps for selected call pair --- .../README.md | 205 ++ .../RESULT.json | 1863 +++++++++++++++++ .../SOURCES.json | 24 + .../TASK.json | 86 + .../VERIFY.json | 22 + .../verify.py | 239 +++ 6 files changed, 2439 insertions(+) create mode 100644 research/selected-centre-composed-source-rank/README.md create mode 100644 research/selected-centre-composed-source-rank/RESULT.json create mode 100644 research/selected-centre-composed-source-rank/SOURCES.json create mode 100644 research/selected-centre-composed-source-rank/TASK.json create mode 100644 research/selected-centre-composed-source-rank/VERIFY.json create mode 100644 research/selected-centre-composed-source-rank/verify.py diff --git a/research/selected-centre-composed-source-rank/README.md b/research/selected-centre-composed-source-rank/README.md new file mode 100644 index 0000000000..0e3c819eb2 --- /dev/null +++ b/research/selected-centre-composed-source-rank/README.md @@ -0,0 +1,205 @@ +# Exact composed scalar source rank for two selected centre calls + +**Finite scalar-projection certificate; not a native centre-path obstruction, +new supplier, or improved κ.** The selected record and all frozen sources are +unchanged. This package computes the centre source maps of selected forward +calls **time 0 / time 1, stage 0, replicas 0 / 8**, composing the complete first +scalar call before the second. It does not assume that different physical owner +IDs imply independent values at later execution cuts. + +## Result + +The two calls each use 704 local owner roles. Their owner sets overlap on **30 +hosted physical families**, giving **1,378** formal input coordinates jointly. +The exact projection retains all scalar operations but treats frame transports, +ordinary adapters and residual adapters as identity. Physical owners are one +scalar coordinate each: their native chart/address structure is not modeled. +This is a precisely defined projection, not an assertion of native equivalence. + +`verify.py` propagates every ordinary input column through both complete scalar +programs, snapshots the eight source rows at each `centers` boundary, checks +all ordinary endpoints and private-centre clearing, then proves over Q: + +| Quantity | Exact value | +|---|---:| +| Rank of stacked sixteen centre-source maps | 16 | +| Rank of their two 88-row scatter-output maps | 16 | +| Source rank restricted to the 224 initial source-data owners | 16 | +| Shared physical owners | 30 | +| Source maps of call 1 changed by completed call 0 | no | + +The source-data-only nonsingular minor has columns +`0,1,2,3,4,5,6,12,7168,7169,7170,7171,7172,7173,7174,7180`. +Thus the computed independence does not rely on extra information in hosted +helper dirt. Each call's eight source support sizes are +`111,106,110,107,104,105,103,106`; these are actual propagated maps, not eight +coordinate selectors. `RESULT.json` records every rational coefficient. + +An additional exact witness is obtained by solving this minor for source +values `(e0,-e0)`. All eight pairwise pooled source sums vanish, while the demanded +scatter output is nonzero. The verifier directly evaluates both assertions; +`pooled_sum_kernel_witness` records the nonzero initial data coordinates. +Explicitly, on owners `(0,1,2,3,4,5,6,12)` set +`(3,-1,2,-1,-1,-1,-1,-1)/4`, and on the corresponding owners plus 7168 +set its negative; set every other owner to zero. + +## Scoped information lemma + +Let `x` be the initial scalar owner vector. Let `P x` and `Q x` be the two +recorded source maps, and `T x` the recorded scatter increments on the two +separate output panels. Consider a **linear boundary replacement** whose sole +source-dependent transcript to its output computations is `z=E x`, with `d` +scalar components. Fix the same initial target and host dirt in two runs. +If their output differences must equal `T x`, then `T=R E` for the decoder's +linear map `R`, so + +``` +d >= rank(T). +``` + +Conversely, at the purely linear-information level, a basis of the row space +of `T` is a sufficient transcript; this says nothing about its frame legality +or cost. For this explicit projected pair the verified rank is 16, ruling out +an **eight-scalar-total-only** transcript. This is not a lower bound on the +number of arbitrary native recursive calls. + +Arbitrary initial target dirt cannot furnish missing source information because +it is fixed when taking differences. Restored host dirt cannot help unless the +replacement exposes additional source-dependent observations along the way; +such observations are additional transcript components and must be counted. +We do **not** infer a general cyclic/mixed transport inequality from this lemma. +A history-dependent native argument would need the complete boundary and +hosting-credit hypotheses of [PR1664](https://github.com/CrocSwap/integer-mult-bounds/pull/1664). + +Equal source maps have stacked rank eight. Distinct source maps can also have +rank eight: the verifier reverses the order of the second eight maps and checks +this example. Consequently, map inequality alone is not the obstruction; +the joint demanded information is. A rank-eight transcript does not alone +license a physical shared path when centre maps/charts differ. + +## Complete unchanged centre-phase invoice + +For this pair the literal phases contain: + +| Operation | Both calls | +|---|---:| +| Rank-8 transport children | 16 | +| Source COPY | 16 | +| Initial and final CLEAR | 32 | +| Scatter ADD | 352 | +| Total listed macros | 416 | +| Sum of recursive transport ranks | 128 | + +The full scalar continuations, including helper restoration, are checked for +both calls. All 30 overlapping host variables are shared in the composition; +none is cloned for free. Every centre COPY, CLEAR and scatter ADD is charged. +Initial centre clears are counted from the emitted program; the verifier's +private rows start absent, so it does not independently certify arbitrary +native private-centre dirt. Ordinary helper/target dirt **is** fully symbolic. + +This is an **unchanged baseline invoice**, not a new globally admitted cost. +There is no proposed routing, hosting or precision rewrite, hence no changed +moment or justified charge saving to submit to `ceiling.ceiling`. The scalar +transcript exclusion must not be restated as a native minimum of 128. Original +word hosting, precision and full supplier admission remain inherited, not +reverified here. + +## Native limitation and useful handoff + +The exact source cuts occur at different times. The interpreter intentionally +ignores `climb`, `adapter`, `residual_adapter` and centre frame operators while +keeping their scalar event order and centre transport invoice. It follows the +style of the inherited emitter's scalar algebra check, not a native frame +checker. In particular it is not established that identity-projected rank is +a lower bound for the true 512-address operator rank. + +The missing implication is an injective lift of the displayed source-data +minor through the actual frame operators and owner charts, with the 30 shared +host families and complete first-call continuation. Without that lemma this +result remains a reproducible source-map handoff, not an obstruction to native +centre sharing. No arbitrary-pair census, retiming exclusion, all-size theorem, +Lean proof, or independent human proof review is claimed. + +## Replay and controls + +Python 3.12, standard library only: + +```sh +python3.12 scripts/research_package.py --package research/selected-centre-composed-source-rank +python3.12 -I -O -B research/selected-centre-composed-source-rank/verify.py +``` + +Expected direct output: + +```text +PASS_SELECTED_PAIR_SCALAR_SOURCE_RANK source_rank=16 scatter_rank=16 data_rank=16 shared_owners=30 rank_mass=128 controls=5 +``` + +`verify.py --write` regenerates `RESULT.json`; ordinary replay recomputes and +compares every receipt field without writing. The five semantic controls check +equal maps, distinct dependent maps, pooled-sum loss of a nonzero output, +omission of a scatter ADD, and omission of the final centre clear. The latter +two must fail for the corresponding endpoint/private-state reason. All checks +use explicit exceptions and remain active under `-O`. + +Observed final verification: CPython **3.12.12**, Darwin arm64. Receipt +generation, registered replay and isolated optimized smoke all passed in +**2.77 seconds combined**. The registered launcher reported +`PASS_REGISTERED_RESEARCH_PACKAGE ... outcome=completed`. No full repository +suite, native frame replay or supplier cold replay was run. + +The required starting example was executed before refinement: +`research/complex-local-word-ceiling/verify.py` reported +`PASS_COMPLEX_LOCAL_WORD_CEILING`, with `a_ceiling=0.00169005410908900006`. +`levers.py` reported the ideal shared-two relaxation `a_cap≈0.003213`, factor +`1.90`, `kappa_cap≈0.003203`. Those are favorable planning numbers only and are +not this package's result. + +## Sources, overlap and attribution + +Base: `0b1cccf86e2f5132ed286a26ef0a681a495740ea`. `SOURCES.json` binds Git +provenance and live source bytes; `verify.py` additionally pins the selected +replay archive and its global-template, emitted-program and canonical-word +members. No pending PR code is imported. The selected 480-helper emitted word +is used, not the 492-helper historical evidence directories. + +Closest predecessors, with exact heads in `TASK.json`: + +- [PR1708](https://github.com/CrocSwap/integer-mult-bounds/pull/1708), Cinna Davis + (`1337isnot1337`): forward shared-source fanout. +- [PR1748](https://github.com/CrocSwap/integer-mult-bounds/pull/1748), ToikY: + shared reverse centre phase and precision guard. +- [PR1664](https://github.com/CrocSwap/integer-mult-bounds/pull/1664), Andrey Mas + (`an664`): conditional dirty-host history-span inequality. +- [PR1684](https://github.com/CrocSwap/integer-mult-bounds/pull/1684): selected + single-call scalar cut-rank application. +- [PR1829](https://github.com/CrocSwap/integer-mult-bounds/pull/1829): adjacent + selected owner/chart identity census. This package adds propagated composed + source maps and a collision witness for **one pair**, not a wider census. + +The general linear rank lemma is standard and is not claimed as new. Credit +ctoth's [discussion1516](https://github.com/CrocSwap/integer-mult-bounds/discussions/1516), +Rohan Arun's selected #1094 owner placement, Jeremy Kothe's retained word, +and the inherited compiler/emitter lineage (including icekylinx and +DreamingOfClouds). The precise new artifact is the selected paired scalar +computation on shared physical-owner variables. + +Coordination: [discussion1884](https://github.com/CrocSwap/integer-mult-bounds/discussions/1884). +Overlap search used the complete cached 539-open-PR/524-discussion snapshot +from 2026-10-14 13:09–13:10Z, including bodies/comments, and targeted predecessor +head checks before publication. Arbitrary diffs and every closed submission +were not searched; this is not a novelty guarantee. + +Prepared by Adam Gall with substantial OpenAI Codex assistance in mathematical +scoping, implementation, experiments and packaging. Apache-2.0. + +## Open next questions + +1. **Native lift:** propagate the sixteen displayed pivot columns through the + actual 512-address native prefixes and first-call continuation. This matters + because scalar projection rank alone is insufficient. The blocker is the + missing operator/frame independence lemma. +2. **Priced additional information:** specify any proposed side-channel, + noncoincident readout or cyclic hosting interface and its complete bill. + First bind its endpoint/continuation to PR1664's hypotheses. No such changed + interface is supplied here. Structured details are in `TASK.json`. diff --git a/research/selected-centre-composed-source-rank/RESULT.json b/research/selected-centre-composed-source-rank/RESULT.json new file mode 100644 index 0000000000..e53349fed1 --- /dev/null +++ b/research/selected-centre-composed-source-rank/RESULT.json @@ -0,0 +1,1863 @@ +{ + "call1_source_changed_by_complete_call0": false, + "centre_phase_bill": { + "add": 352, + "clear": 32, + "copy": 16, + "rank8": 16 + }, + "controls": [ + "equal_maps_rank8", + "distinct_permuted_maps_rank8", + "pooled_sum_loses_nonzero_output", + "omitted_scatter_rejected", + "omitted_final_clear_rejected" + ], + "distinct_permuted_map_rank": 8, + "equal_map_rank": 8, + "paid_rank_mass": 128, + "physical_owner_union": 1378, + "pivot_owner_ids": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 12, + 1344, + 1345, + 1348, + 1350, + 1356, + 1357, + 1368, + 1400 + ], + "pooled_sum_kernel_witness": { + "0": "3/4", + "1": "-1/4", + "12": "-1/4", + "2": "1/2", + "3": "-1/4", + "4": "-1/4", + "5": "-1/4", + "6": "-1/4", + "7168": "-3/4", + "7169": "1/4", + "7170": "-1/2", + "7171": "1/4", + "7172": "1/4", + "7173": "1/4", + "7174": "1/4", + "7180": "1/4" + }, + "pooled_sum_source_values": [ + 1, + 0, + 0, + 0, + 0, + 0, + 0, + 0, + -1, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "rank_restricted_to_224_source_data_owners": 16, + "replicas": [ + 0, + 8 + ], + "scatter_rank": 16, + "scope": "Scalar common-frame projection only; adapters and frame moves are not native replayed.", + "shared_owner_count": 30, + "source_data_pivot_owner_ids": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 12, + 7168, + 7169, + 7170, + 7171, + 7172, + 7173, + 7174, + 7180 + ], + "source_maps": [ + { + "0": "1", + "10": "1", + "100": "1", + "101": "1", + "102": "1", + "103": "1", + "107": "1", + "108": "1", + "109": "1", + "11": "1", + "12": "1", + "12993": "1", + "12995": "2", + "12996": "-1", + "12997": "1", + "13000": "1", + "13001": "1", + "13003": "2", + "13004": "-1", + "13005": "1", + "17": "1", + "18": "1", + "19": "1", + "2": "1", + "22": "1", + "23": "1", + "24": "1", + "25": "1", + "27": "1", + "31": "1", + "32": "1", + "33": "1", + "34": "1", + "35": "1", + "38": "1", + "39": "1", + "40": "1", + "448": "1", + "449": "-2", + "45": "1", + "450": "1", + "453": "2", + "455": "-1", + "457": "1", + "459": "1", + "460": "-2", + "461": "1", + "464": "2", + "466": "-1", + "469": "1", + "471": "1", + "472": "-2", + "473": "1", + "476": "2", + "478": "-1", + "48": "1", + "481": "1", + "483": "1", + "485": "1", + "486": "1", + "488": "2", + "489": "-1", + "49": "1", + "490": "1", + "493": "1", + "494": "1", + "496": "2", + "497": "1", + "498": "1", + "499": "1", + "50": "1", + "501": "1", + "502": "1", + "504": "2", + "505": "-1", + "506": "1", + "509": "1", + "54": "1", + "55": "1", + "56": "1", + "57": "1", + "61": "1", + "62": "1", + "63": "1", + "6763": "1", + "7": "1", + "70": "1", + "71": "1", + "72": "1", + "76": "1", + "77": "1", + "79": "1", + "81": "1", + "8452": "-1", + "8453": "1", + "8456": "2", + "8460": "1", + "85": "1", + "8512": "1", + "8514": "2", + "8515": "1", + "8516": "1", + "8517": "1", + "87": "1", + "89": "1", + "9": "1", + "90": "1", + "91": "1", + "92": "1", + "94": "1", + "98": "1" + }, + { + "0": "1", + "1": "1", + "10": "-1", + "11": "-1", + "1225": "-1", + "1226": "1", + "1229": "2", + "1234": "1", + "1236": "1", + "1237": "-1", + "1238": "1", + "1241": "2", + "1246": "1", + "1248": "1", + "1249": "-1", + "1250": "1", + "1253": "2", + "1258": "1", + "12993": "-1", + "12996": "-1", + "12997": "-1", + "13000": "1", + "13001": "1", + "13004": "1", + "13005": "-1", + "13006": "2", + "2": "1", + "25": "1", + "26": "1", + "27": "1", + "28": "1", + "29": "1", + "3": "1", + "30": "1", + "4": "1", + "484": "-2", + "485": "1", + "486": "-1", + "489": "-1", + "490": "-1", + "493": "1", + "494": "1", + "497": "1", + "498": "-1", + "499": "1", + "5": "1", + "500": "-2", + "501": "1", + "502": "-1", + "505": "-1", + "506": "-1", + "509": "1", + "57": "-1", + "58": "1", + "59": "1", + "6": "1", + "60": "1", + "61": "-1", + "62": "-1", + "63": "-1", + "64": "1", + "65": "1", + "66": "1", + "67": "1", + "6763": "1", + "68": "1", + "69": "1", + "7": "-1", + "70": "1", + "71": "1", + "72": "1", + "73": "1", + "74": "1", + "75": "1", + "76": "1", + "79": "-1", + "8": "1", + "80": "1", + "81": "-1", + "82": "1", + "83": "1", + "84": "1", + "8439": "1", + "8440": "-1", + "8441": "1", + "8444": "2", + "8449": "1", + "8451": "1", + "8512": "1", + "8515": "1", + "8516": "-1", + "8517": "1", + "8518": "-2", + "86": "1", + "87": "1", + "88": "1", + "89": "1", + "9": "-1", + "90": "1", + "91": "1", + "92": "-1", + "93": "1", + "94": "-1", + "95": "1", + "96": "1", + "97": "1" + }, + { + "0": "1", + "1": "1", + "100": "1", + "101": "1", + "102": "1", + "103": "-1", + "104": "1", + "105": "1", + "106": "1", + "1194": "1", + "1195": "1", + "1197": "2", + "1198": "-1", + "1199": "1", + "12": "1", + "1202": "1", + "1203": "1", + "1205": "2", + "1206": "-1", + "1207": "1", + "1208": "1", + "1210": "1", + "1211": "1", + "1213": "2", + "1214": "-1", + "1215": "1", + "1218": "1", + "1219": "1", + "1221": "2", + "1222": "-1", + "1223": "1", + "1224": "1", + "1249": "-1", + "1250": "1", + "1253": "-2", + "1258": "1", + "12993": "-1", + "12996": "1", + "12997": "1", + "13": "1", + "13000": "-1", + "13001": "-1", + "13003": "2", + "13004": "-1", + "13005": "-1", + "13006": "2", + "14": "1", + "15": "1", + "16": "1", + "17": "-1", + "18": "-1", + "19": "-1", + "27": "-1", + "28": "-1", + "29": "-1", + "30": "-1", + "31": "1", + "38": "-1", + "39": "-1", + "40": "-1", + "41": "1", + "42": "1", + "43": "1", + "44": "1", + "460": "-2", + "461": "1", + "464": "-2", + "466": "-1", + "469": "1", + "471": "1", + "472": "-2", + "473": "1", + "476": "-2", + "478": "-1", + "481": "1", + "483": "1", + "51": "1", + "52": "1", + "53": "1", + "54": "1", + "55": "1", + "56": "1", + "57": "1", + "58": "-1", + "59": "-1", + "6": "1", + "60": "-1", + "6763": "-1", + "7": "-1", + "73": "1", + "74": "1", + "75": "1", + "76": "1", + "77": "-1", + "78": "1", + "81": "-1", + "82": "1", + "83": "1", + "84": "1", + "8439": "1", + "8440": "-1", + "8441": "1", + "8444": "-2", + "8449": "1", + "8451": "1", + "86": "-1", + "87": "-1", + "92": "1", + "93": "-1", + "99": "1" + }, + { + "0": "1", + "104": "-1", + "105": "-1", + "106": "-1", + "107": "-1", + "108": "-1", + "109": "-1", + "1193": "-2", + "1194": "1", + "1195": "-1", + "1198": "-1", + "1199": "-1", + "1202": "1", + "1203": "1", + "1206": "1", + "1207": "-1", + "1208": "1", + "1209": "-2", + "1210": "1", + "1211": "-1", + "1214": "-1", + "1215": "-1", + "1218": "1", + "1219": "1", + "1222": "1", + "1223": "-1", + "1224": "1", + "1225": "-1", + "1226": "1", + "1229": "-2", + "1234": "1", + "1236": "1", + "1237": "-1", + "1238": "1", + "1241": "-2", + "1246": "1", + "1248": "1", + "12993": "1", + "12995": "-2", + "12996": "1", + "12997": "1", + "13": "1", + "13000": "-1", + "13001": "1", + "13004": "-1", + "13005": "1", + "14": "1", + "15": "1", + "16": "-1", + "22": "-1", + "23": "-1", + "24": "-1", + "26": "-1", + "27": "-1", + "3": "1", + "32": "1", + "33": "1", + "34": "1", + "35": "-1", + "4": "1", + "41": "-1", + "42": "-1", + "43": "-1", + "44": "-1", + "448": "1", + "449": "-2", + "45": "-1", + "450": "1", + "453": "-2", + "455": "-1", + "457": "1", + "459": "1", + "48": "1", + "49": "1", + "5": "1", + "50": "1", + "51": "1", + "52": "1", + "53": "1", + "57": "-1", + "64": "-1", + "65": "-1", + "66": "-1", + "67": "1", + "6763": "1", + "68": "1", + "69": "1", + "7": "1", + "76": "-1", + "78": "1", + "8": "-1", + "80": "1", + "81": "-1", + "8452": "-1", + "8453": "1", + "8456": "-2", + "8460": "1", + "85": "1", + "8518": "-2", + "87": "1", + "88": "1", + "92": "1", + "95": "-1", + "96": "-1", + "97": "-1", + "98": "1", + "99": "1" + }, + { + "1": "-1", + "10": "-1", + "100": "1", + "103": "1", + "105": "-1", + "106": "-1", + "107": "1", + "11": "-1", + "110": "1", + "111": "1", + "1178": "1", + "1179": "1", + "1181": "2", + "1182": "-1", + "1183": "1", + "1186": "1", + "1187": "1", + "1189": "2", + "1190": "-1", + "1191": "1", + "12": "1", + "1210": "-1", + "1211": "-1", + "1214": "1", + "1215": "1", + "1218": "-1", + "1219": "-1", + "1221": "2", + "1222": "-1", + "1223": "-1", + "1224": "1", + "1237": "-1", + "1238": "-1", + "1246": "-1", + "1248": "1", + "14": "1", + "15": "1", + "17": "1", + "20": "1", + "21": "1", + "24": "-1", + "26": "-1", + "28": "-1", + "3": "-1", + "31": "-1", + "32": "-1", + "35": "-1", + "36": "1", + "37": "1", + "38": "-1", + "41": "1", + "42": "1", + "449": "-2", + "45": "1", + "450": "-1", + "455": "-1", + "457": "-1", + "459": "1", + "46": "1", + "47": "1", + "472": "-2", + "473": "-1", + "478": "-1", + "48": "1", + "481": "-1", + "483": "1", + "501": "-1", + "502": "-1", + "505": "1", + "506": "1", + "509": "-1", + "52": "-1", + "53": "-1", + "56": "-1", + "58": "1", + "6": "1", + "62": "1", + "63": "1", + "66": "-1", + "67": "1", + "70": "1", + "71": "1", + "75": "-1", + "77": "-1", + "8": "1", + "80": "1", + "82": "1", + "8440": "-1", + "8441": "-1", + "8449": "-1", + "8451": "1", + "85": "-1", + "8512": "-1", + "8514": "2", + "8515": "1", + "8516": "-1", + "8517": "1", + "86": "-1", + "88": "-1", + "90": "-1", + "91": "-1", + "93": "1", + "95": "1", + "98": "1" + }, + { + "10": "1", + "101": "1", + "102": "-1", + "105": "1", + "106": "-1", + "108": "1", + "109": "-1", + "11": "-1", + "110": "-1", + "111": "1", + "1177": "-2", + "1178": "1", + "1179": "-1", + "1182": "-1", + "1183": "-1", + "1186": "1", + "1187": "1", + "1190": "1", + "1191": "-1", + "1192": "2", + "1209": "-2", + "1210": "1", + "1211": "1", + "1213": "-2", + "1214": "1", + "1215": "1", + "1218": "-1", + "1219": "1", + "1222": "-1", + "1223": "1", + "1224": "1", + "1225": "-1", + "1226": "-1", + "1234": "-1", + "1236": "1", + "1249": "-1", + "1250": "-1", + "1258": "-1", + "14": "-1", + "15": "1", + "18": "1", + "19": "-1", + "20": "-1", + "21": "1", + "22": "1", + "23": "-1", + "29": "-1", + "30": "1", + "33": "-1", + "34": "1", + "36": "1", + "37": "-1", + "39": "-1", + "4": "-1", + "40": "1", + "41": "1", + "42": "-1", + "448": "1", + "46": "-1", + "460": "-2", + "461": "-1", + "466": "-1", + "469": "-1", + "47": "1", + "471": "1", + "49": "1", + "5": "1", + "50": "-1", + "500": "-2", + "501": "1", + "502": "1", + "504": "-2", + "505": "1", + "506": "1", + "509": "-1", + "52": "1", + "53": "-1", + "54": "1", + "55": "-1", + "59": "1", + "60": "-1", + "62": "-1", + "63": "1", + "64": "1", + "65": "-1", + "68": "1", + "69": "-1", + "70": "1", + "71": "-1", + "73": "1", + "74": "-1", + "83": "1", + "84": "-1", + "8439": "1", + "8452": "-1", + "8453": "-1", + "8460": "-1", + "8512": "1", + "8515": "-1", + "8516": "1", + "8517": "1", + "90": "1", + "91": "-1", + "96": "1", + "97": "-1" + }, + { + "100": "-1", + "103": "1", + "104": "-1", + "108": "1", + "109": "1", + "110": "-1", + "111": "-1", + "1178": "-1", + "1179": "-1", + "1182": "1", + "1183": "1", + "1186": "-1", + "1187": "-1", + "1189": "2", + "1190": "-1", + "1191": "-1", + "1192": "2", + "1194": "-1", + "1195": "-1", + "1198": "1", + "1199": "1", + "12": "1", + "1202": "-1", + "1203": "-1", + "1205": "2", + "1206": "-1", + "1207": "-1", + "1208": "1", + "1237": "-3", + "1238": "1", + "1246": "1", + "1248": "-1", + "1249": "-3", + "1250": "1", + "1258": "1", + "13": "1", + "16": "1", + "17": "-1", + "2": "1", + "20": "1", + "21": "1", + "22": "-1", + "23": "-1", + "25": "-1", + "26": "-1", + "29": "-1", + "3": "1", + "30": "-1", + "31": "-1", + "33": "-1", + "34": "-1", + "36": "1", + "37": "1", + "38": "1", + "43": "1", + "44": "-1", + "448": "-1", + "46": "-1", + "47": "-1", + "472": "-2", + "473": "1", + "478": "1", + "481": "1", + "483": "-1", + "485": "-1", + "486": "-1", + "489": "1", + "49": "1", + "490": "1", + "493": "-1", + "494": "-1", + "496": "2", + "497": "1", + "498": "-1", + "499": "1", + "50": "1", + "51": "-1", + "56": "1", + "59": "1", + "60": "1", + "61": "1", + "66": "1", + "67": "-1", + "72": "1", + "73": "-1", + "74": "-1", + "77": "-1", + "78": "1", + "79": "-1", + "8": "1", + "80": "1", + "83": "1", + "84": "1", + "8439": "-1", + "8452": "-3", + "8453": "1", + "8460": "1", + "88": "-1", + "89": "-1", + "9": "-1", + "94": "1", + "95": "-1", + "99": "-1" + }, + { + "1": "-1", + "101": "1", + "102": "1", + "104": "-1", + "107": "-1", + "110": "-1", + "111": "-1", + "1177": "-2", + "1178": "1", + "1179": "1", + "1181": "-2", + "1182": "1", + "1183": "1", + "1186": "-1", + "1187": "1", + "1190": "-1", + "1191": "1", + "1193": "-2", + "1194": "1", + "1195": "1", + "1197": "-2", + "1198": "1", + "1199": "1", + "1202": "-1", + "1203": "1", + "1206": "-1", + "1207": "1", + "1208": "1", + "1225": "-3", + "1226": "1", + "1234": "1", + "1236": "-1", + "13": "1", + "16": "-1", + "18": "1", + "19": "1", + "2": "-1", + "20": "-1", + "21": "-1", + "24": "1", + "25": "1", + "28": "1", + "32": "1", + "35": "-1", + "36": "1", + "37": "1", + "39": "-1", + "4": "-1", + "40": "-1", + "43": "1", + "44": "1", + "449": "-2", + "45": "1", + "450": "1", + "455": "1", + "457": "1", + "459": "-1", + "46": "1", + "460": "-2", + "461": "1", + "466": "1", + "469": "1", + "47": "1", + "471": "-1", + "48": "-1", + "484": "-2", + "485": "1", + "486": "1", + "488": "-2", + "489": "1", + "490": "1", + "493": "-1", + "494": "1", + "497": "-1", + "498": "1", + "499": "1", + "5": "-1", + "51": "-1", + "54": "-1", + "55": "-1", + "58": "-1", + "6": "1", + "61": "1", + "64": "-1", + "65": "-1", + "68": "1", + "69": "1", + "72": "1", + "75": "1", + "78": "-1", + "79": "1", + "82": "-1", + "8440": "-3", + "8441": "1", + "8449": "1", + "8451": "-1", + "85": "-1", + "86": "-1", + "89": "-1", + "9": "-1", + "93": "1", + "94": "-1", + "96": "1", + "97": "1", + "98": "1", + "99": "1" + }, + { + "1344": "-2", + "1345": "1", + "1348": "2", + "1350": "-1", + "1353": "1", + "1355": "1", + "1356": "-2", + "1357": "1", + "1360": "2", + "1362": "-1", + "1365": "1", + "1367": "1", + "1369": "1", + "1370": "1", + "1372": "2", + "1373": "-1", + "1374": "1", + "1377": "1", + "1378": "1", + "1380": "2", + "1381": "1", + "1382": "1", + "1383": "1", + "1385": "1", + "1386": "1", + "1388": "2", + "1389": "-1", + "1390": "1", + "1393": "1", + "1394": "1", + "1396": "2", + "1397": "1", + "1398": "1", + "1399": "1", + "1401": "1", + "1402": "1", + "1404": "2", + "1405": "-1", + "1406": "1", + "1409": "1", + "1410": "1", + "1412": "2", + "1413": "-1", + "1414": "1", + "7168": "1", + "7170": "1", + "7175": "1", + "7177": "1", + "7178": "1", + "7179": "1", + "7180": "1", + "7185": "1", + "7186": "1", + "7187": "1", + "7190": "1", + "7191": "1", + "7192": "1", + "7193": "1", + "7195": "1", + "7199": "1", + "7200": "1", + "7201": "1", + "7202": "1", + "7203": "1", + "7206": "1", + "7207": "1", + "7208": "1", + "7213": "1", + "7216": "1", + "7217": "1", + "7218": "1", + "7222": "1", + "7223": "1", + "7224": "1", + "7225": "1", + "7229": "1", + "7230": "1", + "7231": "1", + "7238": "1", + "7239": "1", + "7240": "1", + "7244": "1", + "7245": "1", + "7247": "1", + "7249": "1", + "7253": "1", + "7255": "1", + "7257": "1", + "7258": "1", + "7259": "1", + "7260": "1", + "7262": "1", + "7266": "1", + "7268": "1", + "7269": "1", + "7270": "1", + "7271": "1", + "7275": "1", + "7276": "1", + "7277": "1", + "7625": "-1", + "7626": "1", + "7629": "2", + "7633": "1", + "7635": "1", + "7636": "-2", + "7637": "1", + "7640": "2", + "7648": "-1", + "7650": "1", + "7652": "1" + }, + { + "1368": "-2", + "1369": "1", + "1370": "-1", + "1373": "-1", + "1374": "-1", + "13746": "-1", + "13747": "1", + "13750": "2", + "13755": "1", + "13757": "1", + "13758": "-1", + "13759": "1", + "13762": "2", + "13767": "1", + "13769": "1", + "1377": "1", + "13770": "-1", + "13771": "1", + "13774": "2", + "13779": "1", + "1378": "1", + "13781": "1", + "13782": "-1", + "13783": "1", + "1381": "1", + "1382": "-1", + "1383": "1", + "1384": "-2", + "1385": "1", + "1386": "-1", + "1389": "-1", + "1390": "-1", + "1393": "1", + "1394": "1", + "1397": "1", + "1398": "-1", + "1399": "1", + "1400": "-2", + "1401": "1", + "1402": "-1", + "1405": "-1", + "1406": "-1", + "1409": "1", + "1410": "1", + "1413": "1", + "1414": "-1", + "1415": "2", + "7168": "1", + "7169": "1", + "7170": "1", + "7171": "1", + "7172": "1", + "7173": "1", + "7174": "1", + "7175": "-1", + "7176": "1", + "7177": "-1", + "7178": "-1", + "7179": "-1", + "7193": "1", + "7194": "1", + "7195": "1", + "7196": "1", + "7197": "1", + "7198": "1", + "7225": "-1", + "7226": "1", + "7227": "1", + "7228": "1", + "7229": "-1", + "7230": "-1", + "7231": "-1", + "7232": "1", + "7233": "1", + "7234": "1", + "7235": "1", + "7236": "1", + "7237": "1", + "7238": "1", + "7239": "1", + "7240": "1", + "7241": "1", + "7242": "1", + "7243": "1", + "7244": "1", + "7247": "-1", + "7248": "1", + "7249": "-1", + "7250": "1", + "7251": "1", + "7252": "1", + "7254": "1", + "7255": "1", + "7256": "1", + "7257": "1", + "7258": "1", + "7259": "1", + "7260": "-1", + "7261": "1", + "7262": "-1", + "7263": "1", + "7264": "1", + "7265": "1", + "7617": "2", + "7622": "1", + "7624": "1" + }, + { + "1344": "-2", + "1345": "1", + "1348": "-2", + "1350": "-1", + "1353": "1", + "1355": "1", + "1356": "-2", + "1357": "1", + "1360": "-2", + "1362": "-1", + "1365": "1", + "1367": "1", + "13734": "2", + "13735": "-1", + "13736": "1", + "13739": "1", + "13740": "1", + "13742": "2", + "13743": "-1", + "13744": "1", + "13745": "1", + "13770": "-1", + "13771": "1", + "13774": "-2", + "13779": "1", + "13781": "1", + "13782": "-1", + "13783": "1", + "1401": "-1", + "1402": "-1", + "1405": "1", + "1406": "1", + "1409": "-1", + "1410": "-1", + "1412": "2", + "1413": "-1", + "1414": "-1", + "1415": "2", + "7168": "1", + "7169": "1", + "7174": "1", + "7175": "-1", + "7180": "1", + "7181": "1", + "7182": "1", + "7183": "1", + "7184": "1", + "7185": "-1", + "7186": "-1", + "7187": "-1", + "7195": "-1", + "7196": "-1", + "7197": "-1", + "7198": "-1", + "7199": "1", + "7206": "-1", + "7207": "-1", + "7208": "-1", + "7209": "1", + "7210": "1", + "7211": "1", + "7212": "1", + "7219": "1", + "7220": "1", + "7221": "1", + "7222": "1", + "7223": "1", + "7224": "1", + "7225": "1", + "7226": "-1", + "7227": "-1", + "7228": "-1", + "7241": "1", + "7242": "1", + "7243": "1", + "7244": "1", + "7245": "-1", + "7246": "1", + "7249": "-1", + "7250": "1", + "7251": "1", + "7252": "1", + "7254": "-1", + "7255": "-1", + "7260": "1", + "7261": "-1", + "7267": "1", + "7268": "1", + "7269": "1", + "7270": "1", + "7271": "-1", + "7272": "1", + "7273": "1", + "7274": "1", + "7617": "-2", + "7622": "1", + "7624": "1", + "9355": "1", + "9356": "1", + "9358": "2", + "9359": "-1", + "9360": "1", + "9363": "1", + "9364": "1", + "9366": "2", + "9367": "-1", + "9368": "1", + "9369": "1", + "9371": "1", + "9372": "1" + }, + { + "13735": "-1", + "13736": "-1", + "13739": "1", + "13740": "1", + "13743": "1", + "13744": "-1", + "13745": "1", + "13746": "-1", + "13747": "1", + "13750": "-2", + "13755": "1", + "13757": "1", + "13758": "-1", + "13759": "1", + "13762": "-2", + "13767": "1", + "13769": "1", + "1400": "-2", + "1401": "1", + "1402": "1", + "1404": "-2", + "1405": "1", + "1406": "1", + "1409": "-1", + "1410": "1", + "1413": "-1", + "1414": "1", + "7168": "1", + "7171": "1", + "7172": "1", + "7173": "1", + "7175": "1", + "7176": "-1", + "7181": "1", + "7182": "1", + "7183": "1", + "7184": "-1", + "7190": "-1", + "7191": "-1", + "7192": "-1", + "7194": "-1", + "7195": "-1", + "7200": "1", + "7201": "1", + "7202": "1", + "7203": "-1", + "7209": "-1", + "7210": "-1", + "7211": "-1", + "7212": "-1", + "7213": "-1", + "7216": "1", + "7217": "1", + "7218": "1", + "7219": "1", + "7220": "1", + "7221": "1", + "7225": "-1", + "7232": "-1", + "7233": "-1", + "7234": "-1", + "7235": "1", + "7236": "1", + "7237": "1", + "7244": "-1", + "7246": "1", + "7248": "1", + "7249": "-1", + "7253": "1", + "7255": "1", + "7256": "1", + "7260": "1", + "7263": "-1", + "7264": "-1", + "7265": "-1", + "7266": "1", + "7267": "1", + "7272": "-1", + "7273": "-1", + "7274": "-1", + "7275": "-1", + "7276": "-1", + "7277": "-1", + "7625": "-1", + "7626": "1", + "7629": "-2", + "7633": "1", + "7635": "1", + "7636": "-2", + "7637": "1", + "7640": "-2", + "7648": "-1", + "7650": "1", + "7652": "1", + "9354": "-2", + "9355": "1", + "9356": "-1", + "9359": "-1", + "9360": "-1", + "9363": "1", + "9364": "1", + "9367": "1", + "9368": "-1", + "9369": "1", + "9370": "-2", + "9371": "1", + "9372": "-1" + }, + { + "1356": "-2", + "1357": "-1", + "1362": "-1", + "1365": "-1", + "1367": "1", + "13735": "1", + "13736": "1", + "13739": "-1", + "13740": "-1", + "13742": "2", + "13743": "-1", + "13744": "-1", + "13745": "1", + "13758": "-1", + "13759": "-1", + "13767": "-1", + "13769": "1", + "13782": "-1", + "13783": "-1", + "1385": "-1", + "1386": "-1", + "1389": "1", + "1390": "1", + "1393": "-1", + "1394": "-1", + "1396": "2", + "1397": "1", + "1398": "-1", + "1399": "1", + "7169": "-1", + "7171": "-1", + "7174": "1", + "7176": "1", + "7178": "-1", + "7179": "-1", + "7180": "1", + "7182": "1", + "7183": "1", + "7185": "1", + "7188": "1", + "7189": "1", + "7192": "-1", + "7194": "-1", + "7196": "-1", + "7199": "-1", + "7200": "-1", + "7203": "-1", + "7204": "1", + "7205": "1", + "7206": "-1", + "7209": "1", + "7210": "1", + "7213": "1", + "7214": "1", + "7215": "1", + "7216": "1", + "7220": "-1", + "7221": "-1", + "7224": "-1", + "7226": "1", + "7230": "1", + "7231": "1", + "7234": "-1", + "7235": "1", + "7238": "1", + "7239": "1", + "7243": "-1", + "7245": "-1", + "7248": "1", + "7250": "1", + "7253": "-1", + "7254": "-1", + "7256": "-1", + "7258": "-1", + "7259": "-1", + "7261": "1", + "7263": "1", + "7266": "1", + "7268": "1", + "7271": "1", + "7273": "-1", + "7274": "-1", + "7275": "1", + "7278": "1", + "7279": "1", + "7622": "-1", + "7624": "1", + "7636": "-2", + "7637": "-1", + "7648": "-1", + "7650": "-1", + "7652": "1", + "9339": "1", + "9340": "1", + "9342": "2", + "9343": "-1", + "9344": "1", + "9347": "1", + "9348": "1", + "9350": "2", + "9351": "-1", + "9352": "1", + "9371": "-1", + "9372": "-1" + }, + { + "1344": "-2", + "1345": "-1", + "1350": "-1", + "1353": "-1", + "1355": "1", + "13734": "-2", + "13735": "1", + "13736": "1", + "13739": "-1", + "13740": "1", + "13743": "-1", + "13744": "1", + "13745": "1", + "13746": "-1", + "13747": "-1", + "13755": "-1", + "13757": "1", + "13770": "-1", + "13771": "-1", + "13779": "-1", + "13781": "1", + "1384": "-2", + "1385": "1", + "1386": "1", + "1388": "-2", + "1389": "1", + "1390": "1", + "1393": "-1", + "1394": "1", + "1397": "-1", + "1398": "1", + "1399": "1", + "7172": "-1", + "7173": "1", + "7178": "1", + "7179": "-1", + "7182": "-1", + "7183": "1", + "7186": "1", + "7187": "-1", + "7188": "-1", + "7189": "1", + "7190": "1", + "7191": "-1", + "7197": "-1", + "7198": "1", + "7201": "-1", + "7202": "1", + "7204": "1", + "7205": "-1", + "7207": "-1", + "7208": "1", + "7209": "1", + "7210": "-1", + "7214": "-1", + "7215": "1", + "7217": "1", + "7218": "-1", + "7220": "1", + "7221": "-1", + "7222": "1", + "7223": "-1", + "7227": "1", + "7228": "-1", + "7230": "-1", + "7231": "1", + "7232": "1", + "7233": "-1", + "7236": "1", + "7237": "-1", + "7238": "1", + "7239": "-1", + "7241": "1", + "7242": "-1", + "7251": "1", + "7252": "-1", + "7258": "1", + "7259": "-1", + "7264": "1", + "7265": "-1", + "7269": "1", + "7270": "-1", + "7273": "1", + "7274": "-1", + "7276": "1", + "7277": "-1", + "7278": "-1", + "7279": "1", + "7625": "-1", + "7626": "-1", + "7633": "-1", + "7635": "1", + "9338": "-2", + "9339": "1", + "9340": "-1", + "9343": "-1", + "9344": "-1", + "9347": "1", + "9348": "1", + "9351": "1", + "9352": "-1", + "9353": "2", + "9370": "-2", + "9371": "1", + "9372": "1" + }, + { + "1356": "-2", + "1357": "1", + "1362": "1", + "1365": "1", + "1367": "-1", + "1369": "-1", + "1370": "-1", + "1373": "1", + "1374": "1", + "13758": "-3", + "13759": "1", + "13767": "1", + "13769": "-1", + "1377": "-1", + "13770": "-3", + "13771": "1", + "13779": "1", + "1378": "-1", + "13781": "-1", + "1380": "2", + "1381": "1", + "1382": "-1", + "1383": "1", + "7170": "1", + "7171": "1", + "7176": "1", + "7177": "-1", + "7180": "1", + "7181": "1", + "7184": "1", + "7185": "-1", + "7188": "1", + "7189": "1", + "7190": "-1", + "7191": "-1", + "7193": "-1", + "7194": "-1", + "7197": "-1", + "7198": "-1", + "7199": "-1", + "7201": "-1", + "7202": "-1", + "7204": "1", + "7205": "1", + "7206": "1", + "7211": "1", + "7212": "-1", + "7214": "-1", + "7215": "-1", + "7217": "1", + "7218": "1", + "7219": "-1", + "7224": "1", + "7227": "1", + "7228": "1", + "7229": "1", + "7234": "1", + "7235": "-1", + "7240": "1", + "7241": "-1", + "7242": "-1", + "7245": "-1", + "7246": "1", + "7247": "-1", + "7248": "1", + "7251": "1", + "7252": "1", + "7256": "-1", + "7257": "-1", + "7262": "1", + "7263": "-1", + "7267": "-1", + "7268": "-1", + "7271": "1", + "7272": "-1", + "7276": "1", + "7277": "1", + "7278": "-1", + "7279": "-1", + "7625": "-3", + "7626": "1", + "7633": "1", + "7635": "-1", + "9339": "-1", + "9340": "-1", + "9343": "1", + "9344": "1", + "9347": "-1", + "9348": "-1", + "9350": "2", + "9351": "-1", + "9352": "-1", + "9353": "2", + "9355": "-1", + "9356": "-1", + "9359": "1", + "9360": "1", + "9363": "-1", + "9364": "-1", + "9366": "2", + "9367": "-1", + "9368": "-1", + "9369": "1" + }, + { + "1344": "-2", + "1345": "1", + "1350": "1", + "1353": "1", + "1355": "-1", + "1368": "-2", + "1369": "1", + "1370": "1", + "1372": "-2", + "1373": "1", + "1374": "1", + "13746": "-3", + "13747": "1", + "13755": "1", + "13757": "-1", + "1377": "-1", + "1378": "1", + "13782": "-3", + "13783": "1", + "1381": "-1", + "1382": "1", + "1383": "1", + "7169": "-1", + "7170": "-1", + "7172": "-1", + "7173": "-1", + "7174": "1", + "7177": "-1", + "7181": "1", + "7184": "-1", + "7186": "1", + "7187": "1", + "7188": "-1", + "7189": "-1", + "7192": "1", + "7193": "1", + "7196": "1", + "7200": "1", + "7203": "-1", + "7204": "1", + "7205": "1", + "7207": "-1", + "7208": "-1", + "7211": "1", + "7212": "1", + "7213": "1", + "7214": "1", + "7215": "1", + "7216": "-1", + "7219": "-1", + "7222": "-1", + "7223": "-1", + "7226": "-1", + "7229": "1", + "7232": "-1", + "7233": "-1", + "7236": "1", + "7237": "1", + "7240": "1", + "7243": "1", + "7246": "-1", + "7247": "1", + "7250": "-1", + "7253": "-1", + "7254": "-1", + "7257": "-1", + "7261": "1", + "7262": "-1", + "7264": "1", + "7265": "1", + "7266": "1", + "7267": "1", + "7269": "1", + "7270": "1", + "7272": "-1", + "7275": "-1", + "7278": "-1", + "7279": "-1", + "7622": "1", + "7624": "-1", + "7636": "-2", + "7637": "1", + "7648": "1", + "7650": "1", + "7652": "-1", + "9338": "-2", + "9339": "1", + "9340": "1", + "9342": "-2", + "9343": "1", + "9344": "1", + "9347": "-1", + "9348": "1", + "9351": "-1", + "9352": "1", + "9354": "-2", + "9355": "1", + "9356": "1", + "9358": "-2", + "9359": "1", + "9360": "1", + "9363": "-1", + "9364": "1", + "9367": "-1", + "9368": "1", + "9369": "1" + } + ], + "source_rank": 16, + "source_support_sizes": [ + 111, + 106, + 110, + 107, + 104, + 105, + 103, + 106, + 111, + 106, + 110, + 107, + 104, + 105, + 103, + 106 + ], + "status": "PASS_SELECTED_PAIR_SCALAR_SOURCE_RANK", + "times": [ + 0, + 1 + ], + "unproved": "Lift scalar source-map rank to native 512-address charted frame maps at the two noncoincident cuts, with transport/hosting/precision and complete-call continuation." +} diff --git a/research/selected-centre-composed-source-rank/SOURCES.json b/research/selected-centre-composed-source-rank/SOURCES.json new file mode 100644 index 0000000000..925aecef04 --- /dev/null +++ b/research/selected-centre-composed-source-rank/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "research/community-frontier1094-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "c24daf067f9c543421d89ca2eeaa4eb78a57fb6f", + "sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6" + } + ] +} diff --git a/research/selected-centre-composed-source-rank/TASK.json b/research/selected-centre-composed-source-rank/TASK.json new file mode 100644 index 0000000000..8884749b4e --- /dev/null +++ b/research/selected-centre-composed-source-rank/TASK.json @@ -0,0 +1,86 @@ +{ + "schema_version": 1, + "task_id": "centre-path-sharing", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "original_card": { + "id": "centre-path-sharing", + "question": "Can the 64-per-call centre path (eight rank-8 COPY/ERASE totals through the private temporary) be shared across calls or shrunk?", + "starting_points": [ + "research/complex-local-word-ceiling/README.md", + "research/split-centres-global/proofs/PR386-BIT-GEOMETRY.txt", + "certificates/selected-result.json" + ], + "methods": [ + "Derive a fully charged favorable relaxation for sharing one centre path across k calls, including restoration, hosting and precision.", + "Prove a lower bound on copied information per call for the selected decoder contract." + ], + "acceptance_gate": "Show the changed centre charge and copy profile per call with every added restoration or hosting cost charged, and its ceiling via ceiling.ceiling(centre=...).", + "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": "Write the per-call centre charge and copy children for sharing across k = 2 calls, charge the sharing overhead, and screen it; stop this route if even the ideal sharing gains under 10%. Ideal budgets: free 2.80x, shared by two 1.90x (levers.py).", + "bottleneck_link": "The centre path consumes 64 of about 99.6 unpaid coordinates per call, i.e. about 64% of the raw deficit.", + "allowed_variations": [ + "One sharing pattern across a fixed number of calls.", + "One reduced copied-total contract for the existing decoder.", + "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": [ + "Removing copies without a replacement contract for the decoder's copied totals." + ], + "overlap_terms": [ + "centre path", + "copied totals", + "private temporary", + "shared centre", + "batching" + ] + }, + "scope_status": "refined", + "actual_scope": "Exact scalar projection of selected calls time0/time1 on their actual shared physical owner variables; composed eight-source maps, data-only joint rank16 and pooled-total collision witness. Not native frame transport.", + "scope_change_reason": "Equal-source fanout, reverse return and owner-identity census already exist in PR1708/1748/1829. Compute source-map dependence across an actual composed pair instead of assuming unequal owner IDs imply independent values. Native lifting is explicitly left open.", + "bottleneck_link": "Determines whether one concrete paired centre source interface can convey both scalar scatter outputs through eight totals without additional source information. No centre-charge improvement or supplier admission is claimed.", + "budget_minutes": 60, + "stop_rule": "Stop after the pinned time0/time1 composed scalar maps, exact minor/collision witness, full scalar restoration and phase bill; do not infer a native bound.", + "outcome": "completed", + "evidence": "RESULT.json stores sixteen exact source maps, data minor, pooled-sum collision, phase invoice and controls; verify.py recomputes them from the selected replay.", + "author": "Adam Gall with OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance with scoping, source inspection, mathematical argument, implementation, exact experiments and packaging; no independent human proof review claimed.", + "coordination": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1884", + "overlap": { + "open_prs": 539, + "discussions": 524, + "fetched_at": ["2026-10-14T13:09:44.369135+00:00", "2026-10-14T13:10:59.319576+00:00"], + "complete_pagination": true, + "limitations": "Cached bodies/comments and local notes; not every diff or closed submission. Relevant exact heads rechecked before publication; no novelty guarantee.", + "predecessor_heads": { + "1708": "4d163c04c0980c5b0e9092fbd5864c7cfadc125d", + "1748": "ea14f191752c9901bf6684763534d2d248fb2ad2", + "1664": "f6d5ccf4c94e52c761aa6e00f862d6e72e697b23", + "1684": "1e1af1a8f97f6eee21946cd1ff832e3d61269d33", + "1829": "e150e7ed8fa33f0be769926535eeacd076c6bd13" + } + }, + "open_questions": [ + { + "question": "Does the source-data minor lift injectively through the native 512-address frame maps and owner charts?", + "why_it_matters": "Only a native lift could turn this scalar obstruction into a statement about the actual supplier interface.", + "first_step": "Propagate the sixteen displayed data pivot columns through both native prefixes and the complete first-call continuation, retaining chart/phase operators.", + "blocked_by": "This package deliberately projects frame moves and adapters to identity; no native independence lemma is established." + }, + { + "question": "Can a changed shared interface use additional source-dependent side channels within a beneficial complete cost?", + "why_it_matters": "The transcript rank bound only excludes eight-total-only linear information transfer, not arbitrary retiming or cyclic hosting.", + "first_step": "Specify every side channel, host endpoint and continuation; apply the explicit boundary hypotheses of PR1664 and price all precision/restoration work.", + "blocked_by": "No changed physical interface or eligible fully charged schedule is supplied here." + } + ] +} diff --git a/research/selected-centre-composed-source-rank/VERIFY.json b/research/selected-centre-composed-source-rank/VERIFY.json new file mode 100644 index 0000000000..221e6ec4d7 --- /dev/null +++ b/research/selected-centre-composed-source-rank/VERIFY.json @@ -0,0 +1,22 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "research/community-frontier1094-audit/selected-replay.tar.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact composed scalar source maps, rank16 source-data minor, pooled-total collision, full dirty-helper scalar restoration, phase invoice, five controls and committed receipt equality" + } + ] +} diff --git a/research/selected-centre-composed-source-rank/verify.py b/research/selected-centre-composed-source-rank/verify.py new file mode 100644 index 0000000000..a05e796132 --- /dev/null +++ b/research/selected-centre-composed-source-rank/verify.py @@ -0,0 +1,239 @@ +#!/usr/bin/env python3 +"""Selected time0/time1 scalar projection only; not native frame admission.""" +import argparse +import gzip +import hashlib +import json +import tarfile +from collections import Counter +from fractions import Fraction as Q +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent + +ARCHIVE = 'research/community-frontier1094-audit/selected-replay.tar.gz' +PINS = { + ARCHIVE: 'f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6', + 'certificates/selected-result.json': '10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32', +} +MEMBERS = { + 'global': ('candidate/strict/global/hosted/GLOBAL-TEMPLATE.json.gz', '2acf02b418078e37090495c601fe550448751d4f35912757b13a1f778efc7760'), + 'program': ('candidate/strict/global/base/providers/gauge44/LOCAL-PROGRAMS.json.gz', '241fde27d4e43f5a9cb6b128f9f76c5131a53d09f0371676163f914d0b0fef3a'), + 'word': ('candidate/strict/global/base/providers/gauge44/CANONICAL-WORD.json.gz', '16bc0ebb04b4be6c0ade74badc6a0c0cdba4215eda86e4ff9f13abf8ecebd219'), +} + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def add(row, source, q): + for key, value in list(source.items()): + new = row.get(key, Q(0)) + q * value + if new: + row[key] = new + else: + row.pop(key, None) + + +def rank(rows): + pivots = {} + for original in rows: + row = dict(original) + while row: + col = min(row) + if col not in pivots: + q = row[col] + pivots[col] = {k: v / q for k, v in row.items()} + break + add(row, pivots[col], -row[col]) + return len(pivots), sorted(pivots) + + +def replay(program, call, physical, source_roles, stop_at_cut=False): + owners = [entry[0] for entry in call['owners']] + require(len(owners) == len(set(owners)) == 704, 'noninjective local owner map') + state = {('L', i): dict(physical[owner]) for i, owner in enumerate(owners)} + sources = None + bill = Counter() + phase = None + for event in program: + tag = event[0] + if tag == 'phase': + phase = event[1] + if phase == 'centers': + sources = [dict(state['L', i]) for i in source_roles] + if stop_at_cut: + return sources, bill + continue + if tag == 'scalar': + op = event[1] + name, dest = op[0], tuple(op[1]) + if phase == 'centers': + bill[name] += 1 + if name == 'clear': + state[dest] = {} + elif name == 'copy': + state[dest] = dict(state[tuple(op[2])]) + elif name == 'scale': + q = Q(op[2], op[3]) + require(q != 0, 'singular scale') + state[dest] = {k: q*v for k, v in state[dest].items()} + elif name == 'add': + add(state[dest], state[tuple(op[2])], Q(op[3], op[4])) + else: + raise ValueError('unknown scalar operation') + elif tag == 'center': + require(phase == 'centers' and event[4] == 8, 'unexpected centre') + bill['rank8'] += 1 + else: + # This is the declared projection, not an implementation of these maps. + require(tag in ('climb', 'adapter', 'residual_adapter'), 'unknown event') + require(sources is not None, 'missing source cut') + require(all(not row for key, row in state.items() if key[0] == 'C'), 'dirty private exit') + before = {i: dict(physical[owner]) for i, owner in enumerate(owners)} + for i, owner in enumerate(owners): + expected = dict(before[i]) + if 112 <= i < 224: + add(expected, before[i-112], Q(1)) + require(state['L', i] == expected, f'full scalar endpoint mismatch on role {i}') + physical[owner] = state['L', i] + return sources, bill + + +def solve_minor(rows, columns, target): + """Exact Gauss-Jordan solve; returned witness is checked by direct evaluation.""" + matrix = [[row.get(col, Q(0)) for col in columns] + [Q(value)] + for row, value in zip(rows, target)] + n = len(columns) + for col in range(n): + pivot = next((i for i in range(col, n) if matrix[i][col]), None) + require(pivot is not None, 'singular source-data minor') + matrix[col], matrix[pivot] = matrix[pivot], matrix[col] + divisor = matrix[col][col] + matrix[col] = [value / divisor for value in matrix[col]] + for i in range(n): + if i != col: + q = matrix[i][col] + matrix[i] = [x - q*y for x, y in zip(matrix[i], matrix[col])] + return {column: matrix[i][-1] for i, column in enumerate(columns) if matrix[i][-1]} + + +def evaluate(row, values): + return sum((q * values.get(col, Q(0)) for col, q in row.items()), Q(0)) + + +def check_semantic_controls(program, call, owners, source_roles): + start = program.index(['phase', 'centers']) + end = program.index(['phase', 'B']) + scatter = next(i for i in range(start, end) + if program[i][0] == 'scalar' and program[i][1][0] == 'add') + final_clear = end - 1 + require(program[final_clear][1][0] == 'clear', 'final centre clear position') + for label, omitted in [('omitted_scatter', scatter), ('omitted_final_clear', final_clear)]: + state = {owner: {owner: Q(1)} for owner in owners} + try: + replay(program[:omitted] + program[omitted+1:], call, state, source_roles) + except ValueError as error: + expected = 'endpoint mismatch' if label == 'omitted_scatter' else 'dirty private exit' + require(expected in str(error), 'control failed for an unrelated reason') + else: + raise ValueError(f'accepted {label}') + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--root', type=Path, default=PACKAGE.parents[1]) + parser.add_argument('--write', action='store_true', help='regenerate the exact result receipt') + args = parser.parse_args() + for path, digest in PINS.items(): + require(hashlib.sha256((args.root/path).read_bytes()).hexdigest() == digest, path) + data = {} + with tarfile.open(args.root/ARCHIVE, 'r:gz') as archive: + for key, (path, digest) in MEMBERS.items(): + raw = archive.extractfile(path).read() + require(hashlib.sha256(raw).hexdigest() == digest, path) + data[key] = json.loads(gzip.decompress(raw)) + calls = sorted(data['global']['calls'], key=lambda c: c['time'])[:2] + require([(c['time'], c['stage'], c['replica'], c['orientation']) for c in calls] + == [(0, 0, 0, 'forward'), (1, 0, 8, 'forward')], 'selected pair drift') + program = data['program']['forward'] + digest = hashlib.sha256(json.dumps(program, sort_keys=True, separators=(',', ':')).encode()).hexdigest() + require(all(c['local_program_sha256'] == digest for c in calls), 'program binding') + source_roles = data['word']['centers'] + require(source_roles == [92, 57, 81, 224, 11, 240, 9, 256], 'source role drift') + owner_sets = [{entry[0] for entry in c['owners']} for c in calls] + sweeps = [e for e in data['global']['execution_schedule'] if e.get('kind') == 'local_cover_sweep'] + require(len(sweeps) >= 2, 'missing scheduled sweeps') + for call, sweep in zip(calls, sweeps[:2]): + require(all(call[key] == sweep[key] for key in ('time', 'replica', 'stage', 'provider_id')), + 'call order differs from scheduled sweeps') + physical = {owner: {owner: Q(1)} for owner in set.union(*owner_sets)} + source_a, bill_a = replay(program, calls[0], physical, source_roles) + source_b, bill_b = replay(program, calls[1], physical, source_roles) + # Independent initialization is a control, not the main experiment. + independent = {owner: {owner: Q(1)} for owner in owner_sets[1]} + source_b_independent, _ = replay(program, calls[1], independent, source_roles, True) + rows = source_a + source_b + joint_rank, pivots = rank(rows) + data_owners = {entry[0] for c in calls for entry in c['owners'][:112]} + require(len(data_owners) == 224, 'source-data owner count changed') + clean_rows = [{k: v for k, v in row.items() if k in data_owners} for row in rows] + clean_rank, clean_pivots = rank(clean_rows) + scatter = [] + for offset in (0, 8): + for target in sorted({edge[1] for edge in data['word']['cut']}): + row = {} + for edge in data['word']['cut']: + if edge[1] == target: + index = offset + source_roles.index(edge[2]) + add(row, rows[index], Q(edge[3], edge[4])) + scatter.append(row) + scatter_rank, _ = rank(scatter) + require(joint_rank == scatter_rank == 16, 'joint source or output rank differs from16') + require(rank(source_a + source_a)[0] == 8, 'equal-source control') + require(rank(source_a + list(reversed(source_a)))[0] == 8, 'distinct-dependent control') + require(rank([{k:v for k,v in row.items() if k in pivots} for row in rows])[0] == 16, + 'pivot-minor certificate') + require(clean_rank == 16, 'source-data-only rank changed') + desired = [1] + [0]*7 + [-1] + [0]*7 + witness = solve_minor(rows, clean_pivots, desired) + values = [evaluate(row, witness) for row in rows] + require(values == desired, 'direct source witness check failed') + require(all(values[i] + values[i+8] == 0 for i in range(8)), 'pooled sums not zero') + require(any(evaluate(row, witness) for row in scatter), 'pooled witness has no output error') + check_semantic_controls(program, calls[0], owner_sets[0], source_roles) + bill = dict(bill_a + bill_b) + require(bill == {'clear':32, 'copy':16, 'rank8':16, 'add':352}, 'phase invoice') + result = { + 'status': 'PASS_SELECTED_PAIR_SCALAR_SOURCE_RANK', + 'scope': 'Scalar common-frame projection only; adapters and frame moves are not native replayed.', + 'times': [0,1], 'replicas': [0,8], + 'physical_owner_union': len(physical), 'shared_owner_count': len(owner_sets[0] & owner_sets[1]), + 'source_support_sizes': [len(row) for row in rows], + 'source_rank': joint_rank, 'scatter_rank': scatter_rank, + 'rank_restricted_to_224_source_data_owners': clean_rank, + 'pivot_owner_ids': pivots, 'source_data_pivot_owner_ids': clean_pivots, + 'call1_source_changed_by_complete_call0': source_b != source_b_independent, + 'equal_map_rank':8, 'distinct_permuted_map_rank':8, + 'centre_phase_bill': bill, 'paid_rank_mass':128, + 'source_maps': [{str(k): str(v) for k,v in sorted(row.items())} for row in rows], + 'pooled_sum_kernel_witness': {str(k): str(v) for k, v in sorted(witness.items())}, + 'pooled_sum_source_values': desired, + 'controls': ['equal_maps_rank8', 'distinct_permuted_maps_rank8', + 'pooled_sum_loses_nonzero_output', 'omitted_scatter_rejected', + 'omitted_final_clear_rejected'], + 'unproved': 'Lift scalar source-map rank to native 512-address charted frame maps at the two noncoincident cuts, with transport/hosting/precision and complete-call continuation.' + } + receipt = PACKAGE / 'RESULT.json' + if args.write: + receipt.write_text(json.dumps(result, sort_keys=True, indent=2) + '\n', encoding='utf-8') + else: + require(result == json.loads(receipt.read_text(encoding='utf-8')), 'result receipt differs') + print('PASS_SELECTED_PAIR_SCALAR_SOURCE_RANK source_rank=16 scatter_rank=16 ' + 'data_rank=16 shared_owners=30 rank_mass=128 controls=5') + + +if __name__ == '__main__': + main()