From 1e1af1a8f97f6eee21946cd1ff832e3d61269d33 Mon Sep 17 00:00:00 2001 From: Cinna Davis <1337isnot1337@users.noreply.github.com> Date: Wed, 14 Oct 2026 01:41:32 -0500 Subject: [PATCH] research: apply selected cut-rank bound to centre phase --- .../EXPECTED.json | 40 ++ .../selected-centre-cutrank-seed52/LICENSE | 201 +++++++++ .../selected-centre-cutrank-seed52/README.md | 140 +++++++ .../SOURCES.json | 101 +++++ .../selected-centre-cutrank-seed52/TASK.json | 94 +++++ .../VERIFY.json | 35 ++ .../selected-centre-cutrank-seed52/verify.py | 383 ++++++++++++++++++ 7 files changed, 994 insertions(+) create mode 100644 research/selected-centre-cutrank-seed52/EXPECTED.json create mode 100644 research/selected-centre-cutrank-seed52/LICENSE create mode 100644 research/selected-centre-cutrank-seed52/README.md create mode 100644 research/selected-centre-cutrank-seed52/SOURCES.json create mode 100644 research/selected-centre-cutrank-seed52/TASK.json create mode 100644 research/selected-centre-cutrank-seed52/VERIFY.json create mode 100644 research/selected-centre-cutrank-seed52/verify.py diff --git a/research/selected-centre-cutrank-seed52/EXPECTED.json b/research/selected-centre-cutrank-seed52/EXPECTED.json new file mode 100644 index 0000000000..ddf20cafda --- /dev/null +++ b/research/selected-centre-cutrank-seed52/EXPECTED.json @@ -0,0 +1,40 @@ +{ + "status": "PASS_SELECTED_CENTRE_CUTRANK_APPLICATION", + "selected_pr1094_head": "0fc329d0bec93ca7cd288eaea1295172e8789810", + "provider": "gauge44; 480 helpers; local forward program", + "centres": [ + 92, + 57, + 81, + 224, + 11, + 240, + 9, + 256 + ], + "targets": 88, + "ordinary_entry_coordinates": 704, + "ordinary_entry_rank_Q": 704, + "entry_coordinates": 96, + "entry_rank_Q": 96, + "scatter_edges": 176, + "scatter_rank_Q": 8, + "carrier_height_q": 8, + "host_endpoint_term": 0, + "conditional_transport_floor": 64, + "observed_transport_mass": 64, + "phase_event_count_excluding_marker": 208, + "scratch_registers_zero_at_both_boundaries": 8, + "selected_archive_sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6", + "canonical_word_gzip_sha256": "16bc0ebb04b4be6c0ade74badc6a0c0cdba4215eda86e4ff9f13abf8ecebd219", + "local_programs_gzip_sha256": "241fde27d4e43f5a9cb6b128f9f76c5131a53d09f0371676163f914d0b0fef3a", + "negative_controls": [ + "missing_scatter_edge", + "wrong_source_frame", + "nonzero_target_level", + "missing_scratch_clear", + "omitted_carrier_column", + "dependent_entry_rejected", + "Q_rank_not_inferred_from_F2" + ] +} diff --git a/research/selected-centre-cutrank-seed52/LICENSE b/research/selected-centre-cutrank-seed52/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/selected-centre-cutrank-seed52/LICENSE @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/research/selected-centre-cutrank-seed52/README.md b/research/selected-centre-cutrank-seed52/README.md new file mode 100644 index 0000000000..f302ad80a9 --- /dev/null +++ b/research/selected-centre-cutrank-seed52/README.md @@ -0,0 +1,140 @@ +# Selected centre phase under the scalar cut-rank bound + +This package gives an independent, finite application of the conditional +dirty-host cut-rank inequality from [PR #1664](https://github.com/CrocSwap/integer-mult-bounds/pull/1664) +to one exact stage in the accepted PR #1094 word. It fills the narrower gap +that PR #1664 explicitly left open: it did not replay the selected rank-8/64 +boundary. The method is a source-to-interface audit, distinct from +[PR #1643](https://github.com/CrocSwap/integer-mult-bounds/pull/1643), which +audits the selected centre geometry over F2 in a nested-tree relaxation. + +The overlap check also screened [PR #717](https://github.com/CrocSwap/integer-mult-bounds/pull/717), +whose Y1/Y2 centre/cut claims use a rebuilt #656 492-helper gauge44 word. +Its source manifest is pinned in TASK.json and SOURCES.json. That is related +frame/cut work, but it is a different source from this selected #1094 +480-helper emitted phase and does not apply PR #1664's scalar boundary +inequality to it; this package does not rely on it. + +After the seed-52 claim, [PR #1453](https://github.com/CrocSwap/integer-mult-bounds/pull/1453) +merged an obstruction for omitted final helper climbs through the fixed +R480 cleanup, on the same selected supplier. Its theorem fixes a later +full-frame cleanup boundary and treats private centre inputs separately. +This audit instead prices the earlier centre copy/descend/scatter/clear +phase, derives its 88-by-8 rational scatter rank, and applies PR #1664's +bound to that complete interval. It adds no helper-cleanup claim; exact +overlap pins are in TASK.json and SOURCES.json. + +The exact selected provider has eight carrier registers +`[92, 57, 81, 224, 11, 240, 9, 256]`. Its 176 emitted scatter edges touch 88 +distinct target registers, disjoint from the carriers. The verifier replays +the full pre-centre scalar prefix on all 704 ordinary registers and obtains +rank 704 over Q; the selected 96 carrier/target coordinates therefore have +rank 96. Each carrier is at a frame of height 8 and every served target is in +the zero frame. The exact 88-by-8 matrix has entries in `{−1/4, +1/4}` and +rank 8 over Q. The verifier computes this rank directly; it does not infer a +rational rank from the separate binary frame geometry. + +The emitted centre phase includes the complete private-work interval for all +eight carriers: clear a private copy at height 8, copy the carrier, move that +copy to height 0, apply its 22 rational target updates, then clear the copy at +height 0. All eight private copies are zero at entry and exit. The original +carriers remain unchanged, all 88 targets receive exactly `Y + S X`, and no +ordinary register changes frame during the phase. There is no dirty-host +credit in this scope, so the endpoint term is zero. The PR #1664 conditional +formula gives + +```text +transport mass >= H_end + q * rank_Q(S) = 0 + 8 * 8 = 64. +``` + +The exact emitted transport mass is also 64: eight height-eight descents. +Thus this source-bound interface is tight for the inherited inequality. The +phase contains 176 target ADDs and the private-copy setup/cleanup as well; +the reported 64 is specifically the frame-transport component, not the full +ADD/NEG invoice. The result does not identify transport slack that could be +removed from the selected word. + +## Reproduce + +From the repository root, with Python 3.12 and the standard library: + +```sh +python3 -B research/selected-centre-cutrank-seed52/verify.py +python3 -I -O -B research/selected-centre-cutrank-seed52/verify.py +``` + +Expected output: + +```text +PASS_SELECTED_CENTRE_CUTRANK_APPLICATION centres=8 targets=88 entry_rank_Q=96 rank_Q=8 floor=64 transport=64 controls=7 +``` + +The registered check is: + +```sh +python3.12 -B scripts/research_package.py --package research/selected-centre-cutrank-seed52 +``` + +The optimized isolated command must emit the same marker and exact receipt. + +The verifier authenticates the selected replay archive and its two compressed +provider members, interprets exact rational scalar operations, checks the +complete source/target/private boundary, and compares its output to +[EXPECTED.json](EXPECTED.json). Seven controls cover a missing edge, wrong +source frame, nonzero target level, omitted scratch cleanup, missing source +column, dependent entry data, and the difference between Q-rank and F2-rank. +The controls are finite replay checks, not a proof of the universal lemma. + +## Pins, scope and limits + +The exact base is main commit +`418e40eb2572d930b58c1cf9b82b41c0fc7ee08d`. The accepted selected record at +that base is `836330098538459/500000000000000000` (approximately +`0.001672660197076918`), still complex-binding. The selected PR #1094 source +head is `0fc329d0bec93ca7cd288eaea1295172e8789810`. Archive/member SHA-256 +pins, the exact selected source inventory, and immutable predecessor head and +blob pins are recorded in [SOURCES.json](SOURCES.json). + +This is an independent application of PR #1664's written inequality, not a +machine-checked proof of that inequality. It assumes the scalar common-frame +transport contract and its price rule from that audit. It checks only the +selected PR #1094 centre phase. It does not modify the centre schedule, +change a paid supplier profile, verify a dirty-host credit, establish +production admission, rerun the complete selected construction, alter the +accepted record, or prove a multiplication theorem. No new kappa is claimed. + +The scope was narrowed after overlap review: the broad batching/restoration +route overlaps the read-free/composable-family result in +[PR #1155](https://github.com/CrocSwap/integer-mult-bounds/pull/1155), and +the remaining two-root restoring-pass question overlaps the immediately +preceding [PR #1675](https://github.com/CrocSwap/integer-mult-bounds/pull/1675) +and [PR #1651](https://github.com/CrocSwap/integer-mult-bounds/pull/1651) +work. The selected centre application instead checks the explicit unfilled +scalar-boundary interface. The +[seed-52 claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1516#discussioncomment-18917138) +was posted on the coordination discussion; it will be updated with this +result after the final overlap refresh. + +## Open next questions + +Applying the same inequality to a changed centre implementation would require +an exact Q scatter map and the complete typed boundary, including any +nonzero dirty-host endpoint gauges and all preparation and cleanup. That +could reveal whether a new implementation avoids compulsory transport, but +this package includes no such candidate. The first step is a source-pinned +interface replay for one changed local program; physical/production +admission, wrapper pricing, and selected supplier integration remain +separate blockers. + +## Credit + +Credit Rohan Arun and the selected PR #1094 construction lineage for the +provider and emitted word; DreamingOfClouds' related legacy centre/cut work +in PR #717; Ali Romman and the disclosed Codex-assisted work in PR #1453 for +the adjacent fixed-cleanup obstruction; Dennis (@antunishdPursuit) for the +complementary selected-word F2 tree audit in PR #1643; and Andrey Mas for +the conditional scalar cut-rank proof in PR #1664. Prepared by Cinna Davis +(@1337isnot1337) with substantial OpenAI Codex assistance in scope selection, +exact replay code, source handling and exposition. No independent human +review or proof-assistant verification is claimed. New work is Apache-2.0; +the pinned predecessor sources and notices are unchanged. diff --git a/research/selected-centre-cutrank-seed52/SOURCES.json b/research/selected-centre-cutrank-seed52/SOURCES.json new file mode 100644 index 0000000000..087cd61a73 --- /dev/null +++ b/research/selected-centre-cutrank-seed52/SOURCES.json @@ -0,0 +1,101 @@ +{ + "schema_version": 1, + "base_commit": "418e40eb2572d930b58c1cf9b82b41c0fc7ee08d", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "docs/research/community-batch1099-review.md", + "usage": "input", + "git_blob": "6cb6ec061a071a06a2d18cd4dc3e9a2b05d28099", + "sha256": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb" + }, + { + "path": "research/community-frontier1094-audit/ASSEMBLY.json", + "usage": "input", + "git_blob": "5fd676df060f3b450782fdf5ff5f6beb63a5eeb0", + "sha256": "1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045" + }, + { + "path": "research/community-frontier1094-audit/INDEPENDENT1094.json", + "usage": "input", + "git_blob": "009a385e26858058a18188364078d162aa6f9519", + "sha256": "301fb8a0e4ab7e3c383ff974c54c08178283b2a3453c5282757f692a3c7a4bfd" + }, + { + "path": "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "usage": "input", + "git_blob": "6a75493790b4eff9c4a98051ef8b01d6aad0d5a8", + "sha256": "79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b" + }, + { + "path": "research/community-frontier1094-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "c24daf067f9c543421d89ca2eeaa4eb78a57fb6f", + "sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6" + } + ], + "selected_provider": { + "repository": "CrocSwap/integer-mult-bounds", + "selected_pr": 1094, + "selected_pr_head": "0fc329d0bec93ca7cd288eaea1295172e8789810", + "base_archive": "research/community-frontier1094-audit/selected-replay.tar.gz", + "archive_sha256": "f1da80610bf33c58527f18ad63b4350d0b864e1d4486141ee17ac9bed4d529d6", + "archive_members": [ + { + "path": "candidate/strict/global/base/providers/gauge44/CANONICAL-WORD.json.gz", + "sha256": "16bc0ebb04b4be6c0ade74badc6a0c0cdba4215eda86e4ff9f13abf8ecebd219" + }, + { + "path": "candidate/strict/global/base/providers/gauge44/LOCAL-PROGRAMS.json.gz", + "sha256": "241fde27d4e43f5a9cb6b128f9f76c5131a53d09f0371676163f914d0b0fef3a" + } + ] + }, + "predecessor_pins": [ + { + "pr": 1643, + "head": "362086ed05870c793b4698f8843fba6720fa30cb", + "path": "research/centre-descent-tree-audit/EXPECTED.json", + "git_blob": "7d1946207dda6b963ac2a287bff2854334084e11", + "sha256": "b8352ee1a568f6237ca93f462227ee912ac0d82086575177c39f99218783f328", + "role": "selected-word F2 tree geometry; not relied on to infer Q rank" + }, + { + "pr": 1664, + "head": "f6d5ccf4c94e52c761aa6e00f862d6e72e697b23", + "path": "research/dirty-host-cutrank-audit/PROOF.md", + "git_blob": "042fc663f14f0aff985984f201a1cdf89997d594", + "sha256": "2921c2c741ab5086a87c53340f18180ecc55675ca7dadc49579da32aba71d2f5", + "role": "inherited conditional scalar common-frame cut-rank inequality" + } + ], + "overlap_pins": [ + { + "pr": 717, + "head": "4a97676294f9fa413b65986e9984fddeda71e4cc", + "path": "research/format-limits-2/s3-4-census-gauges/SOURCES.part.json", + "git_blob": "8bd76fb8dc5b0d42023fb73b36cde506320eb42b", + "sha256": "8946ca7980cf3dd0bbb6e120407844ebb6b81f08582d39df06987f099e77b8c6", + "role": "screened as related but distinct: legacy #656 492-helper source, not the selected #1094 480-helper scalar phase" + }, + { + "pr": 1453, + "head": "3bceac90599a02a96e9b744736b3feeb00171504", + "path": "research/r480-source-independent-cleanup/README.md", + "git_blob": "69dc6cc1dc59c30c457c1a606965032cfe2561b3", + "sha256": "dca563fa47da7667c15159bfaf904a1f2a871ec610da6a76c52518209fa64ce1", + "role": "same selected supplier, but fixed full-frame cleanup/final-helper boundary; distinct from the centre-phase scatter/transport application here" + } + ] +} diff --git a/research/selected-centre-cutrank-seed52/TASK.json b/research/selected-centre-cutrank-seed52/TASK.json new file mode 100644 index 0000000000..5cdb53a5c9 --- /dev/null +++ b/research/selected-centre-cutrank-seed52/TASK.json @@ -0,0 +1,94 @@ +{ + "schema_version": 1, + "task_id": "persistent-boundary", + "priority_revision": 3, + "base_commit": "418e40eb2572d930b58c1cf9b82b41c0fc7ee08d", + "original_card": { + "id": "persistent-boundary", + "question": "Can a specified pair of consecutive calls eliminate a restoration that the next call reconstructs?", + "starting_points": [ + "research/heterogeneous-owner-assembly/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Write typed entry/exit contracts and a contracting multitype recurrence.", + "Derive a lower bound for the compulsory transitions of one proposed typed interface." + ], + "acceptance_gate": "Show actual eliminated work and legal composition; changing a scalar recurrence into a matrix is insufficient.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Find a concrete consecutive-call boundary in the selected review and list its entry/exit obligations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Specify two call types and one operation actually removed by composition; derive the normalized recurrence.", + "bottleneck_link": "Eliminating compulsory boundary work can lower recursive cost beyond packing gains.", + "allowed_variations": [ + "A two-type pilot or one explicit deferred restoration." + ], + "scope_change_triggers": [ + "Rewriting the old scalar recurrence as a matrix without eliminating work." + ], + "overlap_terms": [ + "persistent boundary", + "deferred restoration", + "multitype" + ] + }, + "scope_status": "changed", + "actual_scope": "Independent source-bound application of the scalar dirty-host cut-rank inequality to the exact eight-centre phase in selected PR1094: reconstruct the rational scatter map, verify its full typed boundary and compare the conditional rank floor with the emitted transport mass.", + "scope_change_reason": "The broad read-free batching/restoration route overlaps the completed PR1155 interface result, while the remaining two-root restoring-pass question overlaps this sprint predecessor PR1675 and its PR1651 witness. I also screened PR717: its centre/cut analysis is pinned to the older #656 492-helper gauge44 word, not the selected #1094 480-helper local emission. The card permits deriving a lower bound for compulsory transitions of one typed interface; I chose the unfilled selected-source application gap explicitly left by PR1664. This is a scoped audit, not a new composition or kappa result. After the claim was posted, PR1453 merged an R480 fixed-cleanup obstruction for the same selected supplier. I screened its exact scope: it prices final helper-climb edits across the fixed cleanup and notes the private centres separately; this package audits the earlier copy/descend/scatter/clear centre phase and derives its Q scatter rank and 64 transport floor. The evidence and theorem scope are disjoint.", + "bottleneck_link": "The scalar cut-rank term measures compulsory frame-transport mass across a chosen supplier boundary. Binding it to the selected centre phase tests whether the asserted 64-unit interface cost survives exact source, target, scratch and cleanup accounting.", + "budget_minutes": 60, + "stop_rule": "Stop after the exact selected PR1094 centre phase, its entry-rank and rational scatter replay, and semantic controls. Do not synthesize a changed centre/decoder, claim that this interface is a global supplier optimum, or infer any new kappa. If a boundary obligation fails, report only that scoped failure.", + "outcome": "completed", + "evidence": "EXPECTED.json records the exact application. verify.py replays the pinned 480-helper source, verifies entry_rank_Q=96, scatter_rank_Q=8, the zero-private-work boundary, complete copy/descent/scatter/clear interval, and the equality 64=64 with seven semantic/field controls.", + "author": "Cinna Davis (@1337isnot1337)", + "ai_assistance": "Substantial OpenAI Codex assistance: selected the scope, wrote and ran the exact verifier, and drafted the exposition. No human review or proof-assistant verification is claimed; the universal cut-rank lemma is inherited from the separately pinned PR1664 audit.", + "open_questions": [ + { + "question": "Can this boundary audit be extended to a changed centre implementation that claims nonzero dirty-host credit?", + "why_it_matters": "Only a changed, fully priced implementation could test whether the selected supplier avoids any of the compulsory 64 transport units.", + "first_step": "For one exact changed implementation, derive its Q scatter matrix and record carrier, target, host and private endpoints through the complete preparation and cleanup interval.", + "blocked_by": "No such implementation is included here; physical/production admission, full wrapper pricing and selected supplier integration remain separate obligations." + } + ], + "assignment_seed": 52, + "track": "recursive-interfaces", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1516#discussioncomment-18917138", + "candidate_selection": [ + { + "object": "General restoration coalescing across a read-free heterogeneous owner batch", + "overlap": "PR1155 and its claimed read-free/composable-family boundary result", + "decision": "not selected; too broad and directly covered" + }, + { + "object": "Remaining restoring-pass classification for the two-root bidirectional transfer fixture", + "overlap": "this run predecessor PR1675 and constructive witness PR1651", + "decision": "not selected; directly overlaps the just-completed seed50 work" + }, + { + "object": "Exact selected PR1094 eight-centre stage under the scalar dirty-host cut-rank inequality", + "overlap": "PR1664 proves the abstract conditional lemma; PR1643 covers the separate F2 tree relaxation; neither claims the selected Q scatter/boundary replay", + "decision": "selected; source-derived method and boundary application are distinct" + } + ], + "related_overlap_review": { + "pr717_head": "4a97676294f9fa413b65986e9984fddeda71e4cc", + "source_manifest": "research/format-limits-2/s3-4-census-gauges/SOURCES.part.json", + "git_blob": "8bd76fb8dc5b0d42023fb73b36cde506320eb42b", + "sha256": "8946ca7980cf3dd0bbb6e120407844ebb6b81f08582d39df06987f099e77b8c6", + "finding": "PR717 Y1/Y2 concerns a rebuilt #656 492-helper gauge44 word; related centre/cut work, but not the selected #1094 480-helper rational emitted phase or PR1664 boundary application.", + "pr1453": { + "head": "3bceac90599a02a96e9b744736b3feeb00171504", + "path": "research/r480-source-independent-cleanup/README.md", + "git_blob": "69dc6cc1dc59c30c457c1a606965032cfe2561b3", + "sha256": "dca563fa47da7667c15159bfaf904a1f2a871ec610da6a76c52518209fa64ce1", + "finding": "PR1453 fixes the selected R480 full-frame helper cleanup and proves an obstruction for omitted final helper climbs. It identifies private centres separately; it does not price the earlier centre phase or report its selected Q scatter rank." + } + } +} diff --git a/research/selected-centre-cutrank-seed52/VERIFY.json b/research/selected-centre-cutrank-seed52/VERIFY.json new file mode 100644 index 0000000000..efd1691a30 --- /dev/null +++ b/research/selected-centre-cutrank-seed52/VERIFY.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "docs/research/community-batch1099-review.md", + "research/community-frontier1094-audit/ASSEMBLY.json", + "research/community-frontier1094-audit/INDEPENDENT1094.json", + "research/community-frontier1094-audit/SELECTED-SOURCE.json", + "research/community-frontier1094-audit/selected-replay.tar.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Replays the pinned selected source members, exact Q-ranks, full centre scratch lifecycle, 64 transport mass and seven semantic controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Optimized isolated replay; must produce the same exact success marker and receipt." + } + ] +} diff --git a/research/selected-centre-cutrank-seed52/verify.py b/research/selected-centre-cutrank-seed52/verify.py new file mode 100644 index 0000000000..0e524c4970 --- /dev/null +++ b/research/selected-centre-cutrank-seed52/verify.py @@ -0,0 +1,383 @@ +#!/usr/bin/env python3 +"""Replay the selected #1094 centre block against the scalar cut-rank bound.""" +from copy import deepcopy +from fractions import Fraction +import gzip +import hashlib +import io +import json +from pathlib import Path +import tarfile + + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = Path(__file__).resolve().parent +ARCHIVE = "research/community-frontier1094-audit/selected-replay.tar.gz" +WORD_MEMBER = "candidate/strict/global/base/providers/gauge44/CANONICAL-WORD.json.gz" +PROGRAM_MEMBER = "candidate/strict/global/base/providers/gauge44/LOCAL-PROGRAMS.json.gz" +WORD_GZ_SHA256 = "16bc0ebb04b4be6c0ade74badc6a0c0cdba4215eda86e4ff9f13abf8ecebd219" +PROGRAM_GZ_SHA256 = "241fde27d4e43f5a9cb6b128f9f76c5131a53d09f0371676163f914d0b0fef3a" + + +class AuditError(ValueError): + pass + + +def require(test, message): + if not test: + raise AuditError(message) + + +def sha256(data): + return hashlib.sha256(data).hexdigest() + + +def exact_rank(matrix): + """Sparse exact Gaussian elimination over Q.""" + pivots = {} + for source in matrix: + row = {i: Fraction(x) for i, x in enumerate(source) if x} + while row: + pivot = min(row) + base = pivots.get(pivot) + if base is None: + scale = row[pivot] + pivots[pivot] = {i: x / scale for i, x in row.items()} + break + scale = row[pivot] + for i, x in base.items(): + value = row.get(i, Fraction(0)) - scale * x + if value: + row[i] = value + else: + row.pop(i, None) + return len(pivots) + + +def exact_sparse_rank(rows): + pivots = {} + for source in rows: + row = {i: Fraction(x) for i, x in source.items() if x} + while row: + pivot = min(row) + base = pivots.get(pivot) + if base is None: + scale = row[pivot] + pivots[pivot] = {i: x / scale for i, x in row.items()} + break + scale = row[pivot] + for i, x in base.items(): + value = row.get(i, Fraction(0)) - scale * x + if value: + row[i] = value + else: + row.pop(i, None) + return len(pivots) + + +def checked_entry_rank(rows, expected): + rank = exact_sparse_rank(rows) + require(rank == expected, "selected source and target values are not independent at entry") + return rank + + +def rank_f2(matrix): + """Separate frame-field diagnostic; never used for the Q scatter rank.""" + if not matrix: + return 0 + rows = [sum((int(x) & 1) << j for j, x in enumerate(row)) for row in matrix] + rank = 0 + for col in range(len(matrix[0])): + pivot = next((i for i in range(rank, len(rows)) if (rows[i] >> col) & 1), None) + if pivot is None: + continue + rows[rank], rows[pivot] = rows[pivot], rows[rank] + for i in range(len(rows)): + if i != rank and ((rows[i] >> col) & 1): + rows[i] ^= rows[rank] + rank += 1 + return rank + + +def extract(archive_bytes): + with tarfile.open(fileobj=io.BytesIO(archive_bytes), mode="r:gz") as archive: + members = {} + for name, pin in ((WORD_MEMBER, WORD_GZ_SHA256), (PROGRAM_MEMBER, PROGRAM_GZ_SHA256)): + member = archive.extractfile(name) + require(member is not None, "missing selected provider member: " + name) + raw = member.read() + require(sha256(raw) == pin, "selected provider member hash mismatch: " + name) + members[name] = json.loads(gzip.decompress(raw)) + return members[WORD_MEMBER], members[PROGRAM_MEMBER]["forward"] + + +def apply_scalar(op, rows, private): + tag, destination = op[0], op[1] + dkind, dindex = destination + target = rows if dkind == "L" else private + get_row = lambda container, index: container[index] if isinstance(container, list) else container.get(index, {}) + if tag == "clear": + target[dindex] = {} + elif tag == "copy": + skind, sindex = op[2] + source = rows if skind == "L" else private + target[dindex] = dict(get_row(source, sindex)) + elif tag == "scale": + factor = Fraction(op[2], op[3]) + target[dindex] = {i: x * factor for i, x in get_row(target, dindex).items() if x * factor} + elif tag == "add": + skind, sindex = op[2] + source = rows if skind == "L" else private + factor = Fraction(op[3], op[4]) + out = dict(get_row(target, dindex)) + for i, x in get_row(source, sindex).items(): + value = out.get(i, Fraction(0)) + factor * x + if value: + out[i] = value + else: + out.pop(i, None) + target[dindex] = out + else: + raise AuditError("unsupported scalar operation " + repr(tag)) + + +def event_state(op, rows, private): + apply_scalar(op, rows, private) + + +def read_prefix_rows(word, program): + """Replay the exact pre-centre scalar prefix on all 704 independent L rows.""" + version = 2 * word["v"] + word["R"] + rows = [{i: Fraction(1)} for i in range(version)] + private = {} + frames = list(word["start"]) + center_index = next((i for i, e in enumerate(program) if e == ["phase", "centers"]), None) + require(center_index is not None, "missing emitted centres phase") + for event in program[:center_index]: + if event[0] == "scalar": + event_state(event[1], rows, private) + elif event[0] == "climb": + _, _part, register, old, new, cost = event + require(frames[register] == old, "pre-centre frame trace has a broken edge") + require(cost >= 0, "negative frame-transition price") + frames[register] = new + elif event[0] == "adapter": + _, _kind, register, frame = event + require(frames[register] == frame, "adapter is assigned to the wrong logical frame") + elif event[0] == "residual_adapter": + _, _kind, register, frame, *_ = event + require(frames[register] == frame, "residual adapter is assigned to the wrong logical frame") + return rows, private, frames, center_index + + +def make_scatter(word, centers, targets): + col = {register: i for i, register in enumerate(centers)} + row = {register: i for i, register in enumerate(targets)} + matrix = [[Fraction(0) for _ in centers] for _ in targets] + for event in word["cut"]: + require(event[0] == "add" and event[2] in col and event[1] in row, + "unexpected canonical scatter event") + matrix[row[event[1]]][col[event[2]]] += Fraction(event[3], event[4]) + return matrix + + +def simulate_centres(word, program, centers, targets, scatter): + start = next(i for i, e in enumerate(program) if e == ["phase", "centers"]) + stop = next(i for i in range(start + 1, len(program)) if program[i] == ["phase", "B"]) + phase = program[start + 1:stop] + rows = [{("L", i): Fraction(1)} for i in range(2 * word["v"] + word["R"])] + private = {} + center_events = [e for e in phase if e[0] == "center"] + require(len(center_events) == len(centers), "wrong number of private centre transports") + require(not any(e[0] == "climb" for e in phase), "unexpected ordinary-register frame change in centre interval") + cursor = 0 + observed_mass = 0 + for k, carrier in enumerate(centers): + frame = word["center_frames"][k] + require(phase[cursor] == ["scalar", ["clear", ["C", k]], frame], "scratch preparation is missing or misplaced") + event_state(phase[cursor][1], rows, private) + cursor += 1 + require(phase[cursor] == ["scalar", ["copy", ["C", k], ["L", carrier]], frame], "carrier copy or frame is wrong") + event_state(phase[cursor][1], rows, private) + cursor += 1 + move = phase[cursor] + require(move == ["center", k, frame, 0, 8], "centre scratch does not descend to the clean target frame") + require(len(word["frames"][frame]) == 8 and len(word["frames"][0]) == 0, + "frame heights do not match the emitted 8-to-0 move") + observed_mass += move[4] + cursor += 1 + seen = [] + while cursor < len(phase) and phase[cursor][0] == "scalar" and phase[cursor][1][0] == "add": + event = phase[cursor] + op, level = event[1], event[2] + require(op[1][0] == "L" and op[2] == ["C", k] and level == 0, + "scatter edge is not a clean-frame target from this scratch") + event_state(op, rows, private) + seen.append((op[1][1], Fraction(op[3], op[4]))) + cursor += 1 + expected = [(e[1], Fraction(e[3], e[4])) for e in word["cut"] if e[2] == carrier] + require(sorted(seen) == sorted(expected), "emitted rational scatter differs from the canonical selected word") + require(len(seen) == 22 and len({r for r, _ in seen}) == 22, + "selected carrier does not serve exactly 22 distinct targets") + require(phase[cursor] == ["scalar", ["clear", ["C", k]], 0], "scratch is not cleared after its complete scatter") + event_state(phase[cursor][1], rows, private) + cursor += 1 + require(cursor == len(phase), "unaccounted operation in the centre interval") + require(all(not row for row in private.values()), "private centre scratch is dirty at exit") + require(observed_mass == 64, "unexpected emitted centre transport mass") + for target_i, target in enumerate(targets): + expected = {("L", target): Fraction(1)} + for j, carrier in enumerate(centers): + coefficient = scatter[target_i][j] + if coefficient: + expected[("L", carrier)] = coefficient + require(rows[target] == expected, "centre phase output does not equal Y + S X") + for carrier in centers: + require(rows[carrier] == {("L", carrier): Fraction(1)}, "centre carrier is altered by its scatter block") + return observed_mass, len(phase) + + +def analyze(word, program): + centers = list(word["centers"]) + targets = sorted({e[1] for e in word["cut"]}) + require(len(centers) == 8 and len(set(centers)) == 8, "selected centre roster changed") + require(len(targets) == 88 and not (set(centers) & set(targets)), "source and target boundary roles overlap") + require(word["v"] == 112 and word["R"] == 480, "not the selected 480-helper provider") + require(not word.get("target_levels", {}), "selected target levels are not all the zero frame") + require(len(word["cut"]) == 176, "selected scatter no longer has 176 edges") + for carrier in centers: + terms = [e for e in word["cut"] if e[2] == carrier] + require(len(terms) == 22 and len({e[1] for e in terms}) == 22, "scatter cardinality changed") + require({Fraction(e[3], e[4]) for e in terms} <= {Fraction(-1, 4), Fraction(1, 4)}, + "unexpected rational scatter coefficient") + + prefix_rows, prefix_private, frames, _phase_start = read_prefix_rows(word, program) + require(not prefix_private, "private scratch exists before the selected centre phase") + complete_entry_rank = exact_sparse_rank(prefix_rows) + require(complete_entry_rank == 2 * word["v"] + word["R"], + "pre-centre ordinary register state is not an invertible Q-coordinate system") + for k, carrier in enumerate(centers): + require(frames[carrier] == word["center_frames"][k], "carrier is not at its selected source frame") + require(len(word["frames"][frames[carrier]]) == 8, "carrier source frame is not height eight") + for target in targets: + require(frames[target] == 0, "target is not in the zero frame at centre-phase entry") + entry_registers = centers + targets + require(len(set(entry_registers)) == 96, "entry-boundary register selection overlaps") + entry_rank = checked_entry_rank([prefix_rows[r] for r in entry_registers], 96) + + scatter = make_scatter(word, centers, targets) + scatter_rank = exact_rank(scatter) + require(scatter_rank == 8, "selected rational scatter does not have full column rank") + transport_mass, phase_events = simulate_centres(word, program, centers, targets, scatter) + q = 8 + floor = q * scatter_rank + require(transport_mass >= floor, "emitted transport mass violates the conditional bound") + return { + "status": "PASS_SELECTED_CENTRE_CUTRANK_APPLICATION", + "selected_pr1094_head": "0fc329d0bec93ca7cd288eaea1295172e8789810", + "provider": "gauge44; 480 helpers; local forward program", + "centres": centers, + "targets": len(targets), + "ordinary_entry_coordinates": 2 * word["v"] + word["R"], + "ordinary_entry_rank_Q": complete_entry_rank, + "entry_coordinates": len(entry_registers), + "entry_rank_Q": entry_rank, + "scatter_edges": len(word["cut"]), + "scatter_rank_Q": scatter_rank, + "carrier_height_q": q, + "host_endpoint_term": 0, + "conditional_transport_floor": floor, + "observed_transport_mass": transport_mass, + "phase_event_count_excluding_marker": phase_events, + "scratch_registers_zero_at_both_boundaries": 8, + } + + +def rejected(name, action): + try: + action() + except (AuditError, KeyError, IndexError, ZeroDivisionError): + return name + raise AuditError("negative control escaped: " + name) + + +def run_controls(word, program): + names = [] + + def missing_scatter_edge(): + bad = deepcopy(word) + bad["cut"].pop() + analyze(bad, program) + + names.append(rejected("missing_scatter_edge", missing_scatter_edge)) + + def wrong_source_frame(): + bad = deepcopy(word) + bad["center_frames"][0] = 0 + analyze(bad, program) + + names.append(rejected("wrong_source_frame", wrong_source_frame)) + + def nonzero_target_level(): + bad = deepcopy(word) + target = next(e[1] for e in bad["cut"]) + bad["target_levels"] = {str(target - bad["v"]): 1} + analyze(bad, program) + + names.append(rejected("nonzero_target_level", nonzero_target_level)) + + def missing_scratch_clear(): + bad = deepcopy(program) + start = next(i for i, e in enumerate(bad) if e == ["phase", "centers"]) + stop = next(i for i in range(start + 1, len(bad)) if bad[i] == ["phase", "B"]) + clear = next(i for i in range(stop - 1, start, -1) + if bad[i][0] == "scalar" and bad[i][1][0] == "clear") + del bad[clear] + analyze(word, bad) + + names.append(rejected("missing_scratch_clear", missing_scratch_clear)) + + def omitted_carrier_column(): + bad = deepcopy(word) + carrier = bad["centers"][0] + bad["cut"] = [e for e in bad["cut"] if e[2] != carrier] + matrix = make_scatter(bad, bad["centers"], sorted({e[1] for e in bad["cut"]})) + require(exact_rank(matrix) == 7, "omitting a complete source column did not lower Q rank") + analyze(bad, program) + + names.append(rejected("omitted_carrier_column", omitted_carrier_column)) + + dependent = [{i: Fraction(1)} for i in range(96)] + dependent[-1] = dict(dependent[-2]) + names.append(rejected("dependent_entry_rejected", lambda: checked_entry_rank(dependent, 96))) + + field_witness = [[1, 1], [1, -1]] + require(exact_rank(field_witness) == 2 and rank_f2(field_witness) == 1, + "field-separation control failed") + names.append("Q_rank_not_inferred_from_F2") + return names + + +def main(): + sources = json.loads((PACKAGE / "SOURCES.json").read_text(encoding="utf-8")) + archive_path = ROOT / ARCHIVE + archive_bytes = archive_path.read_bytes() + pinned_archive = next(x["sha256"] for x in sources["files"] if x["path"] == ARCHIVE) + require(sha256(archive_bytes) == pinned_archive, "selected replay archive differs from base pin") + word, program = extract(archive_bytes) + result = analyze(word, program) + result["selected_archive_sha256"] = sha256(archive_bytes) + result["canonical_word_gzip_sha256"] = WORD_GZ_SHA256 + result["local_programs_gzip_sha256"] = PROGRAM_GZ_SHA256 + result["negative_controls"] = run_controls(word, program) + expected = json.loads((PACKAGE / "EXPECTED.json").read_text(encoding="utf-8")) + require(result == expected, "computed application differs from the committed exact receipt") + print("PASS_SELECTED_CENTRE_CUTRANK_APPLICATION " + f"centres={len(result['centres'])} targets={result['targets']} " + f"entry_rank_Q={result['entry_rank_Q']} rank_Q={result['scatter_rank_Q']} " + f"floor={result['conditional_transport_floor']} transport={result['observed_transport_mass']} " + f"controls={len(result['negative_controls'])}") + + +if __name__ == "__main__": + main()