From 0c1d7ff68dfe3bf34cafed38ad1220058aa10717 Mon Sep 17 00:00:00 2001 From: ToikY <27568617+ToikY@users.noreply.github.com> Date: Thu, 5 Nov 2026 17:05:53 -0800 Subject: [PATCH] Review settlement DP and anchored attaining header --- .../settlement-header-word-review/LICENSE | 201 +++++++++ research/settlement-header-word-review/NOTICE | 18 + .../settlement-header-word-review/README.md | 20 + .../RECORD-ASSEMBLED-REVIEW.md | 41 ++ .../RECORD-ASSEMBLED-SEAL.json | 17 + .../RECORD-CODE-DRAFT-SEAL.json | 28 ++ .../RECORD-CODE-DRAFT.md | 130 ++++++ .../RECORD-CROSS-DERIVATION.md | 47 ++ .../RECORD-CROSS-SEAL.json | 46 ++ .../RECORD-DERIVATION-DRAFT.md | 116 +++++ .../RECORD-DERIVATION-SEAL.json | 16 + .../settlement-header-word-review/REVIEW.md | 81 ++++ .../SOURCE-PINS.json | 185 ++++++++ .../SOURCES.json | 66 +++ .../settlement-header-word-review/TASK.json | 135 ++++++ .../inputs/ALGORITHM.md | 34 ++ .../inputs/LICENSE | 201 +++++++++ .../inputs/NOTICE | 12 + .../inputs/PROOF.md | 63 +++ .../inputs/README.md | 34 ++ .../inputs/ROOT-NOTICE | 415 ++++++++++++++++++ .../inputs/certificates.py.txt | 142 ++++++ .../inputs/example_check.py.txt | 66 +++ .../inputs/literal.py.txt | 61 +++ .../inputs/monomial.py.txt | 45 ++ .../inputs/settlement.py.txt | 100 +++++ .../inputs/source/6710-NOTICE | 10 + .../inputs/source/LICENSE | 201 +++++++++ .../inputs/source/finite.py.txt | 68 +++ .../inputs/verify.py.txt | 92 ++++ 30 files changed, 2691 insertions(+) create mode 100644 research/settlement-header-word-review/LICENSE create mode 100644 research/settlement-header-word-review/NOTICE create mode 100644 research/settlement-header-word-review/README.md create mode 100644 research/settlement-header-word-review/RECORD-ASSEMBLED-REVIEW.md create mode 100644 research/settlement-header-word-review/RECORD-ASSEMBLED-SEAL.json create mode 100644 research/settlement-header-word-review/RECORD-CODE-DRAFT-SEAL.json create mode 100644 research/settlement-header-word-review/RECORD-CODE-DRAFT.md create mode 100644 research/settlement-header-word-review/RECORD-CROSS-DERIVATION.md create mode 100644 research/settlement-header-word-review/RECORD-CROSS-SEAL.json create mode 100644 research/settlement-header-word-review/RECORD-DERIVATION-DRAFT.md create mode 100644 research/settlement-header-word-review/RECORD-DERIVATION-SEAL.json create mode 100644 research/settlement-header-word-review/REVIEW.md create mode 100644 research/settlement-header-word-review/SOURCE-PINS.json create mode 100644 research/settlement-header-word-review/SOURCES.json create mode 100644 research/settlement-header-word-review/TASK.json create mode 100644 research/settlement-header-word-review/inputs/ALGORITHM.md create mode 100644 research/settlement-header-word-review/inputs/LICENSE create mode 100644 research/settlement-header-word-review/inputs/NOTICE create mode 100644 research/settlement-header-word-review/inputs/PROOF.md create mode 100644 research/settlement-header-word-review/inputs/README.md create mode 100644 research/settlement-header-word-review/inputs/ROOT-NOTICE create mode 100644 research/settlement-header-word-review/inputs/certificates.py.txt create mode 100644 research/settlement-header-word-review/inputs/example_check.py.txt create mode 100644 research/settlement-header-word-review/inputs/literal.py.txt create mode 100644 research/settlement-header-word-review/inputs/monomial.py.txt create mode 100644 research/settlement-header-word-review/inputs/settlement.py.txt create mode 100644 research/settlement-header-word-review/inputs/source/6710-NOTICE create mode 100644 research/settlement-header-word-review/inputs/source/LICENSE create mode 100644 research/settlement-header-word-review/inputs/source/finite.py.txt create mode 100644 research/settlement-header-word-review/inputs/verify.py.txt diff --git a/research/settlement-header-word-review/LICENSE b/research/settlement-header-word-review/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/settlement-header-word-review/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/settlement-header-word-review/NOTICE b/research/settlement-header-word-review/NOTICE new file mode 100644 index 0000000000..ee6a7044b2 --- /dev/null +++ b/research/settlement-header-word-review/NOTICE @@ -0,0 +1,18 @@ +Settlement/header-word external written review + +New external review prepared by ToikY with substantial OpenAI Codex assistance +through separate target-known abstract, source-aware code and metadata roles. +Apache-2.0. Source-aware AI agreement is not human or proof-kernel acceptance. + +SHIN09-git authored PR6712 monomial guard settlement, its central theorem, +implementation and original evidence, with substantial OpenAI Codex assistance. +Determinant identities, elementary row operations and debt-partition ideas have +earlier sources. PR6710 supplied retained exact finite-field arithmetic. ToikY +provided the predecessor binary complete-header/all-field pair-sign extension; +Nick Petalas authored the marginal/common-covector pair law. None is recounted +as a new theorem, construction, count or test in this review. + +Exact source notices are retained in inputs/NOTICE, inputs/source/6710-NOTICE +and inputs/ROOT-NOTICE. Apache licenses are retained as LICENSE, inputs/LICENSE +and inputs/source/LICENSE. Original attributions and limitations remain intact. +This inert subset is not the original runnable suite; no endorsement is implied. diff --git a/research/settlement-header-word-review/README.md b/research/settlement-header-word-review/README.md new file mode 100644 index 0000000000..b31a66e3c4 --- /dev/null +++ b/research/settlement-header-word-review/README.md @@ -0,0 +1,20 @@ +# Settlement/header-word source review + +This is an external **written** review of SHIN09-git [PR6712](https://github.com/CrocSwap/integer-mult-bounds/pull/6712), frozen at `03caa7f6cb5bd21c834024e9d81f6b43eb325b91`. It covers the central zero-target h−Z settlement/partition argument, the actual constructed row-addition word and the anchored full-prefix/proper-minor implication. The exact statement and limitations are in [REVIEW.md](REVIEW.md). + +Separately sealed abstract and source-aware code roles found no material gap within that scope, followed by source/peer reconciliation. This is a qualified written outcome, not a new central theorem or implementation, proof-kernel acceptance, or a fresh replay of existing source checks. Historical predecessor familiarity and source exposure are disclosed in the retained notes/seals. Commit/export/publication/CI status belongs to separate later receipts. + +The source valid exact-field/value domain, full-family and anchor hypotheses remain essential. Generic mathematical helpers operate on their stated generated-data domain; they are not an arbitrary hostile certificate-packet parser. The anchored gate replay already exists upstream and was not executed here. The later source binary/ternary/envelope/orbit/pricing classifications are **UNREVIEWED** here; numerical DP outputs remain unreplayed; source eight commands,20faults and finite counts were not rerun. + +[Source pins](SOURCE-PINS.json) bind15 exact inert inputs/90418bytes:13 foreign-head objects and2 canonical root license/notice objects. [Canonical provenance](SOURCES.json) has the eight current-main guidance pins plus LICENSE/NOTICE; it makes no claim that foreign pending source objects are canonical ancestors. Source code copies have `.txt` suffixes. This curated subset is not the original47-file runnable suite, and there is no scientific `VERIFY.json` or scientific command in this package. + +[TASK.json](TASK.json) retains the complete original formal-interface card and records the narrowed written scope. Its formal/kernel gate remains unmet. [NOTICE](NOTICE), [LICENSE](LICENSE) and the retained source notices preserve credit: SHIN09-git owns the source theorem/code/evidence; classical determinant/elementary-row/debt-partition methods, PR6710 finite-field arithmetic, ToikY's predecessor header/pair-sign extension and Nick Petalas's marginal/common-covector pair law are not new results here. This review uses substantial source-aware OpenAI Codex assistance. + +No native or physical invoice, supplier, all-five-assumptions discharge, multiplication theorem, κ/frontier change, adoption or merge follows. Maintainer edits and auto-merge must remain disabled if published; actual settings require a separate live receipt. + +## Open next questions + +- Formalize the typed exact-field/value domain, allowed operation alphabet, generated word and full-family/anchor implication in a proof kernel. +- Specify and independently audit any hostile-packet parser or physical primitive invoice separately. The current mathematical interface does not provide either contract. + +Read the preserved [abstract first draft](RECORD-DERIVATION-DRAFT.md), [code first draft](RECORD-CODE-DRAFT.md), [source cross-binding](RECORD-CROSS-DERIVATION.md) and [exact-version assessment](RECORD-ASSEMBLED-REVIEW.md), with their adjacent seals. diff --git a/research/settlement-header-word-review/RECORD-ASSEMBLED-REVIEW.md b/research/settlement-header-word-review/RECORD-ASSEMBLED-REVIEW.md new file mode 100644 index 0000000000..627f5fb9aa --- /dev/null +++ b/research/settlement-header-word-review/RECORD-ASSEMBLED-REVIEW.md @@ -0,0 +1,41 @@ +# Exact assembled-version review of the settlement audit + +**Qualified PASS. No correction requested for this exact assembled version.** Reviewed `research/settlement-header-word-review/REVIEW.md`, 12,550 bytes, SHA256 `f623123e4f1ea937d0e1976f7c750338633ef2aba4c14e4e8fc451dfc95898c5`, against the actual source text, my first code note, the primary derivation and its source cross-review. + +The first-note hashes remain: primary `8befc623ef765523ab9ac6ec6ec29de003f482724e1340c166e4917236d36a78`, code `7bf994a3a42da5f0f0c5f14744b3245429c883ea9cbf2074e027c0da931bb184`, source cross `9e2f4c41fc824c590853cb5d85de9d594cdbf9abd124740dac2d572ce90af189`. Their metadata hashes were checked; originals/seals were not edited. No source/new scientific program, field constructor, import, DP, matrix/minor search, witness, enumeration, fault, numerical experiment or kernel was executed. This is exact-version written review, not a third independent derivation or a source replay. + +## Central scope and complete-family quantifiers + +The assembled text correctly confines acceptance to h-Z slope settlement, actual zero-target `partition`/`add_row`/`witness` and the anchored full-proper-minor endpoint. It expressly excludes the binary dummy branch, ternary prices/envelope, NP-completeness, orbits and other later statements despite exposure. Existing source claims, eight commands, multiple routes, twenty faults and finite outcomes retain source credit and are not newly accepted execution results. + +The guard derivation uses all affine parameters and every proper prefix. A nonzero slope prefix has a field-linear parameter functional onto the scalar field, so some parameter fails that prefix. The assembled clarification that this failing parameter may depend on the prefix is correct; it does not require one parameter to fail at all prefixes. Total W*u=0 supplies the final coordinate when subtracting consecutive proper prefixes. The full determinant is excluded, and first-pivot or arbitrary-subfamily predicates are not substituted. + +The F3 singleton-subfamily hand control is valid: b=(0,0,1) passes the identity's proper prefixes for parameter zero, while W=(1,-1,0) has a nonzero first charge and the complete family supplies a failing parameter. It is labeled as a changed-premise deduction, not a new source case or numerical result. + +## Lower bound, DP and actual word + +The two-charge conservation has the correct inverse-dual orientation. Free monomial normalization preserves the settlement objective and paid length, without claiming all free permutations preserve the full guard event. The component lower bound retains zero-charge helpers and includes repeated/ineffective paid operations; it does not rely on the false principle that a step can remove at most one active charge. A component's active labels form a zero-sum block, and its connectivity bound remains valid if the scalar anchor is used as a helper by a competing word. + +The recurrence interprets the actual labeled subset sums as maximum zero cumulative-prefix boundaries. Its two-way connection to block partitions and the nested-mask backtracking proof justify Z. Repeated equal charge values remain distinct labels; the empty prefix is not counted. The source's final count check is correctly described as association, not a substitute for maximality proof. + +The donor proof uses the nonzero u component, not a donor charge/W component. The target index has not yet been eliminated, the donor is never targeted, and blocks are disjoint, so every emitted field coefficient is legal. Even a hypothetical intermediate zero collector charge would not create division by zero. The update copies values and uses each old target row entry before changing the source entry. No ordinary-integer inverse is smuggled into finite-field code. + +The witness-return distinction is accurate: returned gates and metadata are not themselves transformed fields. `example_check.example` really does replay the gates through `add_row` on b and w, then enumerates the complete flat and checks a positive literal proper-minor order count against the subset counter. `certificates.constructions` merely storing the dictionary is separately identified. These source paths were read, not run. Their small examples are not used to infer the universal proof. + +## Anchor, field closure and physical frame + +The anchored scalar carrier is inactive for slope settlement and untouched by the attaining word. Its scalar support and normalization therefore survive; placing it last makes every proper scalar and slope prefix zero. The argument proves the required header, not restoration of original u/b/W coordinates or a physical dirty-owner service. An unanchored input cannot borrow this scalar conclusion. + +The F2 unanchored hand control is valid: with u=(1,1,1,0), b=(1,1,1,0), W=(0,0,0,1), scalar normalization and zero slope charges hold. Under free monomials the three scalar ones and one zero only permute, and the first one necessarily occurs at a proper prefix, causing a failed determinant. This correctly demonstrates a missing-anchor premise, not a source theorem counterexample. + +The code's retained arithmetic closure is stated as only q in{2,3,4,5,7,8,9}; the abstract field calculation is not presented as an all-prime-power constructor. Valid field operations, encoded labels, equal widths and valid indices are explicit helper premises. The review does not claim a new arithmetic-table/irreducibility audit, complete hostile packet validation or execution of the larger import closure. + +Input-dependent coefficients and free permutation/diagonal choices belong to the source operation metric. Selection, coefficient generation/precision, routing, storage, inverse/return and physical restored-frame costs remain separate. The conclusion is not a universal minimum in another gate alphabet or caller model, and is distinct from prior fixed486 or complete-uniform-header counts. + +## Evidence, exposure and credit + +Eight abstract and nine code controls are correctly described as overlapping UNEXECUTED deductions, not seventeen experiments. Source control intentions retain their original provenance. The assembled exposure chronology distinguishes target-known abstract derivation before current source/peer from the source-aware code role's earlier scout exposure, followed by sealed cross-review. No blind, human or formal-kernel acceptance is implied. + +SHIN09-git6712 keeps the theorem, witnesses, prices and broader source results;6710, ToikY/Nick Petalas prior header results and classical determinant/row-operation/debt-partition methods retain their scopes. No new DP result, full-field constructor, later price theorem, physical caller/native supplier, kappa, selected-frontier, adoption, merge or follow-on reservation is claimed. The formal/kernel task gate and all five selected framework assumptions remain unmet in the stated sense. + +This PASS binds only the exact reviewed hash above. Complete publication/source custody, commit/mode/export readback and hosted helper CI are separate evidence and were not independently repeated by this note. diff --git a/research/settlement-header-word-review/RECORD-ASSEMBLED-SEAL.json b/research/settlement-header-word-review/RECORD-ASSEMBLED-SEAL.json new file mode 100644 index 0000000000..11a9e54d4c --- /dev/null +++ b/research/settlement-header-word-review/RECORD-ASSEMBLED-SEAL.json @@ -0,0 +1,17 @@ +{ + "artifact": { + "bytes": 7122, + "path": "/private/tmp/contribution-batch-b13-20261105T2038Z/session-08/SETTLEMENT-ASSEMBLED-REVIEW.md", + "sha256": "6c8de9914e17d1d24d1621682b80b813dbd6f9fcd0f0b4b5f3827ef38a227546" + }, + "reviewed_assembled": { + "bytes": 12550, + "path": "/private/tmp/crocswap-b9/research/settlement-header-word-review/REVIEW.md", + "sha256": "f623123e4f1ea937d0e1976f7c750338633ef2aba4c14e4e8fc451dfc95898c5" + }, + "schema_version": 1, + "scientific_execution": false, + "sealed_at_utc": "2026-11-06T01:02:48.777522+00:00", + "sealed_originals_edited": false, + "verdict": "Qualified PASS for exact assembled central-scope written review; no correction requested" +} diff --git a/research/settlement-header-word-review/RECORD-CODE-DRAFT-SEAL.json b/research/settlement-header-word-review/RECORD-CODE-DRAFT-SEAL.json new file mode 100644 index 0000000000..b0a47134ed --- /dev/null +++ b/research/settlement-header-word-review/RECORD-CODE-DRAFT-SEAL.json @@ -0,0 +1,28 @@ +{ + "artifact": { + "bytes": 17081, + "path": "/private/tmp/contribution-batch-b13-20261105T2038Z/session-08/SETTLEMENT-CODE-DRAFT.md", + "sha256": "7bf994a3a42da5f0f0c5f14744b3245429c883ea9cbf2074e027c0da931bb184" + }, + "historical_scout_exposure_disclosed": true, + "peer_draft_read_before_seal": false, + "schema_version": 1, + "scientific_execution_by_author": false, + "scope": "h-Z separation proof plus partition/add_row/witness and anchored replay association only; no binary dummy/ternary envelope/NP/orbit or new counts", + "sealed_at_utc": "2026-11-06T00:54:59.195538+00:00", + "source_aware": true, + "source_blobs": { + "ALGORITHM.md": "f855486175dd7c85c86fe410e85038636bed55aa", + "PROOF.md": "234bbba4812a8a5ca774679451ba17a8072d6b56", + "certificates.py": "e753a14ac687c0d2826a0bb42db9999bdbc4d89f", + "example_check.py": "311863c06845ac005292e25c47338dc6cde83ad6", + "literal.py": "bef3d242ad16109eabf27a41cf0c34b47ad76c6d", + "monomial.py": "3b68a6d1a59b8407f4b54706eeaad78dfa397e21", + "settlement.py": "74df4fb3154fc62775850fcf54136a46faa33989", + "source/finite.py": "b88d32f8ef386f3debd589d6eaf72d5501ab1132", + "verify.py": "ddfade70fb213da5a493f6c244aef3943bc1a482" + }, + "source_head": "03caa7f6cb5bd21c834024e9d81f6b43eb325b91", + "source_pr": 6712, + "verdict": "Qualified PASS for central zero-target settlement and anchored proper-minor implication under valid exact-field/value domain" +} diff --git a/research/settlement-header-word-review/RECORD-CODE-DRAFT.md b/research/settlement-header-word-review/RECORD-CODE-DRAFT.md new file mode 100644 index 0000000000..90b7f63ba0 --- /dev/null +++ b/research/settlement-header-word-review/RECORD-CODE-DRAFT.md @@ -0,0 +1,130 @@ +# Source-aware audit of settlement and its anchored attaining word + +## Verdict and scope + +**Qualified PASS for the central h-Z slope-separation theorem, the actual zero-target partition/addition/witness path, and the anchored full-proper-minor implication. No material discrepancy was found.** The source already owns this theorem, its prices and witnesses. This note is an external written proof-to-code audit, not a new optimum, finite result or actual execution. + +Exact source: SHIN09-git PR6712 head `03caa7f6cb5bd21c834024e9d81f6b43eb325b91`, `research/monomial-guard-settlement/`. The proof, algorithms and settlement implementation were exposed in the earlier bounded scout; this is not a fresh blind role. More source/caller text was read for this assignment. No current peer draft was read before sealing. No source/new scientific program, import, DP, enumeration, matching, literal-minor search, fault, NumPy/native operation or proof kernel was executed. + +The selected path is `witness(...,target_value=None)`. The binary dummy branch, ternary scalar/envelope theorems, NP-completeness, orbit classifications and later claims were visible in source context but are **outside this audit**. The source's eight registered commands, multiple computational routes, twenty faults and extensive reported finite certificates remain source evidence; none is rerun, missing or newly established here. + +Inspected exact source bindings: + +| Path | Git blob | +| --- | --- | +| PROOF.md | `234bbba4812a8a5ca774679451ba17a8072d6b56` | +| ALGORITHM.md | `f855486175dd7c85c86fe410e85038636bed55aa` | +| settlement.py | `74df4fb3154fc62775850fcf54136a46faa33989` | +| source/finite.py | `b88d32f8ef386f3debd589d6eaf72d5501ab1132` | +| literal.py | `bef3d242ad16109eabf27a41cf0c34b47ad76c6d` | +| monomial.py | `3b68a6d1a59b8407f4b54706eeaad78dfa397e21` | +| example_check.py | `311863c06845ac005292e25c47338dc6cde83ad6` | +| certificates.py | `e753a14ac687c0d2826a0bb42db9999bdbc4d89f` | +| verify.py | `ddfade70fb213da5a493f6c244aef3943bc1a482` | + +Only the relevant constructor/consumer predicates are accepted below; importing one of these files would pull additional source outside this narrow claim, and no import occurred here. + +## 1. Exact model and arithmetic assumptions + +Work in a finite field K with valid exact addition, multiplication, negation, inversion of nonzero elements and zero encoded by0. Let u in K^m be nonzero, b a row with b*u=1, and W a matrix of slope rows with W*u=0. The full affine guard family is `b+lambda W` for **every** lambda in K^d. Guards test every proper leading principal minor of the corank-one complements after the same coordinate header. + +Permutations and invertible diagonal coordinate scalings are free. A paid step is an elementary row addition `R_i <- R_i+a R_j`, with i!=j and a!=0. Header dimension is fixed; known-input-dependent coefficient/word choice is allowed. This is a specified algebraic operation metric, not a universal circuit minimum, restored-input service or physical tariff. + +Slope charges are labeled vectors y_i=u_i*W_:i, with total sum zero. Initially zero charges are discarded for the list defining h and Z; h is the number of nonzero charges, and Z is the maximum number of nonempty zero-sum blocks partitioning those h labels. For h=0, Z=0. Labels matter even if two vector values agree. + +The abstract theorem works over any field satisfying these operations. The actual retained `Field` constructor implements only q in{2,3,4,5,7,8,9}, using prime-field or polynomial-basis lookup tables. It is not an all-prime-power constructor. This review reads that closure and relies on its valid-field arithmetic contract; it does not newly certify every arithmetic table/irreducible polynomial or advertise hostile field-object admission. Actual inputs must have equal vector widths, valid field labels and valid coordinate indices. Generic helper signatures do not independently validate every such shape/type condition. + +## 2. Full guards force slope separation + +For a prefix, let X be the scalar charge sum and Y its slope-vector sum. The determinant lemma makes the guard for parameter lambda equal to `1-X-lambda Y`. If Y!=0, the linear map lambda->lambda Y is onto K, so one parameter in the **complete** affine family makes the determinant zero. Hence passing every guard forces every proper Y prefix to vanish. The full slope sum also vanishes by W*u=0. Consecutive differences therefore force every coordinate charge y_i to vanish, including the final coordinate. + +Conversely y_i=0 makes all slope prefixes vanish, but leaves the scalar prefix requirement X!=1. Separation alone is not the full unanchored guard condition. A named proper subfamily can also fail the necessity argument because it may omit the offending parameter. These are hypotheses of the exact price transfer, not optional interpretations. + +The actual `flat_rows` enumerates all d-tuples of field parameters and combines each with b and the slope rows. `literal.identity_pass` forms the actual complements and tests orders1,...,m-1; `literal_orders` checks corresponding proper subsets along every labeled order. The full determinant is correctly excluded. No literal predicate or parameter enumeration was executed by this review. + +## 3. Actual dual row update and conserved component charges + +The source `add_row(field,u,rows,target,source,a)` rejects equal target/source or zero a. It updates + + u_i <- u_i+a*u_j, + row_j <- row_j-a*row_i + +for every supplied dual row, where i is target and j is source. Other u components and other row entries remain unchanged. It makes copies and uses each old target-row entry when updating that row's source entry. This is exactly u->T*u, row->row*T^-1 for T=I+a E_(i,j); it is not the opposite dual orientation. + +For slope columns, only the two vector charges change: + + y_i <- y_i+a*u_j*W_:i, + y_j <- y_j-a*u_j*W_:i. + +Their sum is conserved. This identity does not require the transferred vector to equal either current whole charge in an arbitrary word. It applies even when initially zero-charge coordinates are used as helpers. All row pairings with u are preserved by the dual action, so the normalized affine family remains the same family under the accumulated header. + +## 4. Lower bound includes free monomials and zero-charge helpers + +A monomial matrix normalizes elementary transvections: conjugating one by a permutation/diagonal gives another valid transvection with relabeled distinct indices and a nonzero scalar. Therefore every allowed word can be rewritten with the same number of paid steps and all free monomials at the end. A diagonal cancels from each product u_i*W_:i; a permutation only relabels the charges. The zero-charge objective is invariant under this final monomial, although the full guard event itself is NOT invariant under arbitrary coordinate permutations. + +For the remaining paid word, put an edge between the two fixed labels of every paid step, counting repeated operations in the total cost. By the preceding conservation identity, the sum of initial charges in each connected component equals the sum of final charges there. At a separated endpoint this is zero. Components containing initially active labels thus induce a partition of all active labels into nonempty zero-sum blocks. If there are C such components, C<=Z. + +A component containing k active labels and any number of initially zero helpers has at least k vertices and needs at least k-1 connecting edges. Repeated edges or extra zero-helper vertices cannot lower that connectivity requirement. Summing over active components gives at least + + sum_components(k-1) = h-C >= h-Z + +paid operations. Components containing only initially zero charges contribute no negative cost and can be ignored. This proves the advertised lower bound for arbitrary allowed successful words, not just for the attaining constructor. A full guard requires separation by Section2, so it shares this lower bound. + +## 5. The actual DP finds Z, including its backtracking + +`subset_sums` starts with the empty sum and, for each labeled value, appends the old subset sums plus that value. The right-hand list is built before extension, so its indices correspond to masks with the next label bit set. Under equal widths and field addition these are precisely all labeled subset sums, not merely value multisets. + +For any ordering of a subset S, count its nonempty prefixes whose sum is zero. Maximizing this quantity obeys + + P(empty)=0, + P(S)=1_(sum(S)=0)+max_(i in S) P(S without i). + +The final element i has no influence on earlier prefixes, and the last prefix is zero exactly when the full subset sum is zero. This is the recurrence implemented by `score[mask]` and `last[mask]`, not a greedy choice of arbitrary zero blocks. Each predecessor mask is strictly smaller, so the numeric mask loop has already computed it. + +For the selected full active list the total is zero. Any ordering's zero-prefix boundaries partition that list into zero-sum blocks, so its boundary count is at most Z. Conversely concatenate any zero-sum block partition in any within-block order; its block ends supply at least that many zero prefixes. Maximizing over orders therefore gives exactly Z. + +Backtracking repeatedly removes the stored last bit. Starting with an end mask of zero total, whenever the remaining mask also has zero total, their nonempty set difference is a zero-sum block. The current end is then replaced by that remaining mask. Successive blocks are disjoint and cover the entire list by the final empty mask; the stored predecessor choices attain `score[-1]`. The source's final block-count equality checks this reconstruction association. It does not by itself replace the DP proof of maximality, supplied above. Empty input immediately returns the correct empty partition. + +## 6. The attaining word has a legal nonzero donor at every step + +For the selected zero-target path, `witness` filters to the initially nonzero vector charges and calls `partition`. There is no appended dummy. Each resulting block is nonempty, contains only real active labels, and has total zero. In each block the code chooses its last real label as donor/root j, then visits every other real i once. + +An active vector charge implies u_i!=0. The donor u_j is nonzero initially and never changes: each addition targets i, not j. Distinct blocks use disjoint labels, and previous operations in the block change only the donor's dual column, not an unvisited target's u component. Thus at every visit both u_i and u_j are nonzero and + + a=-u_i/u_j + +is a legal nonzero field coefficient. The actual table expression `mul[neg[u[i]]][inv[u[root]]]` implements this field quotient without ordinary-integer division or an inverse-of-zero call. + +The addition makes u_i zero. Its dual update adds that target's whole current charge to the donor charge. Repeating leaves all visited charges zero and the donor charge equal to the initial block sum, hence zero. A block of size k uses k-1 gates. Summed over Z blocks this is h-Z, meeting Section4's lower bound. Labels initially of zero charge remain untouched by this construction. + +The source final charge and gate-count checks associate the generated internal result with the partition. Its returned dictionary contains gate tuples and certificate metadata, **not** the transformed u/rows. A caller must replay those gates on the original complete data if it wants an actual header result; merely storing the dictionary is not that replay. The all-input word argument establishes the implication without claiming that this review ran a witness. + +## 7. Anchored carrier makes this the full proper-minor price + +Assume b is supported at a single carrier c, u_c*b_c=1 and W_:c=0. Its slope charge is zero, so c is not an active label and the attaining word never uses it as target or donor. On every gate both targeted noncarrier b entries are zero; the dual update keeps them zero. Hence b remains supported at c, u_c is unchanged, and the carrier remains normalized. Its slope column also remains zero. + +After settlement all coordinate slope charges vanish. A free final permutation placing c last makes every proper scalar prefix zero, so every original affine guard has determinant one at every proper prefix. This proves the all-input anchored attaining implication. It is a coordinate-header operation: u and other dual coordinates may change, and no restoration of the original input vector or physical caller frame is asserted. + +There is a real source consumer for this bridge. In `example_check.collect`, the anchored examples obtain gates from the slope-only witness. `example_check.example` then replays each gate via `add_row` on BOTH b and w, constructs the complete flat rows, and requires a positive literal order count agreeing with the subset order counter. This is distinct from `certificates.constructions`, whose anchored entries just store witness dictionaries. The source's replay already exists; it was not performed by this review, and its finite examples do not replace the all-input argument above. + +## 8. Written weakening controls — all UNEXECUTED + +1. **Wrong dual orientation/sign.** Updating the target entry of a row instead of the source entry, or using+a there, need not implement T^-1 and destroys the displayed two-charge conservation. A gate name alone does not establish the inverse-dual action. +2. **A donor that changes.** If the accumulator were also targeted by the settlement step or an earlier block, its u component could become zero and the displayed division would be illegal. The actual disjoint-block/source-only donor invariant is required. +3. **Drop free-monomial normalization.** Applying a fixed-label component argument while arbitrary free permutations are interleaved needs justification. Monomial conjugation supplies that normal form; arbitrary extra free linear mixing would not. +4. **Ignore zero-charge helpers in a lower bound.** They can have nonzero u or dual columns and participate in transfers. The component graph must include their labels; the bound then survives because adding vertices cannot reduce k-1 required connections among k active labels. +5. **Use any greedy zero-sum subset.** A locally found block need not maximize the eventual block count. The DP optimizes all labeled orders and backtracks an attaining partition; counting one partition proves an upper word, not its minimality. +6. **Retain only a named proper affine subfamily.** A nonzero slope prefix might not hit one for any retained parameter. The separation necessity uses the complete parameter family; applying its lower bound to an arbitrary smaller list would change the theorem. +7. **Use an unanchored scalar row.** Zero slopes alone do not ensure all scalar prefixes avoid one. The anchored carrier, its untouched support and final carrier-last permutation are the extra full-guard argument. An arbitrary free permutation can fail it. +8. **Skip the last proper prefix or check only zero charges.** The actual predicate is all orders1 throughm-1, never just a first pivot or the full determinant. Word metadata or a separation summary does not itself execute this predicate; replay on b+W and the actual complement checks are the source's separate route. +9. **Treat helper signatures as hostile packet validation.** Malformed widths/labels/negative indices, an unsupported Field constructor input or an altered target_value branch are not admitted by the stated generated path. A field representation or physical gate alphabet change requires its own proof; no all-q code-constructor or arbitrary circuit minimum is inferred. + +These are proof challenges to weakened claims or operations, not source defects, new observations or seventeen experiments when combined with a peer's overlapping list. Source extensive controls retain their own provenance. + +## Conclusion, credit and remaining scope + +The central proof, recurrence/backtracking and actual dual word are consistent. The active partition supplies both a lower bound against every allowed word and a legal attaining sequence; the anchored carrier supplies the separate all-proper-minor endpoint. No source code change is requested. + +SHIN09-git6712 retains the finite-field guard realization, exact prices, witnesses, sharp ternary and other package results. Classical debt-clearing/zero-sum partition methods and subspace/header predecessors keep their attribution;6710 and ToikY/Nick Petalas complete-header work are not repriced by this note. The imported exact arithmetic retains its original source/license and known supported domain. Substantial Codex/source-aware review exposure is disclosed. + +No new DP result, witness execution, matrix/raw/orbit census, field-law table certification, binary dummy/ternary envelope/NP result, restored physical input/output service, movement/precision/selection/return invoice, native supplier, human/formal acceptance, kappa, selected-frontier or adoption change follows from this audit. All selected framework assumptions remain in their prior state. diff --git a/research/settlement-header-word-review/RECORD-CROSS-DERIVATION.md b/research/settlement-header-word-review/RECORD-CROSS-DERIVATION.md new file mode 100644 index 0000000000..b317c677d4 --- /dev/null +++ b/research/settlement-header-word-review/RECORD-CROSS-DERIVATION.md @@ -0,0 +1,47 @@ +# Post-seal binding of the settlement derivation + +Cross-reviewed 2026-11-06 around01:00UTC, after both first drafts were sealed. This is a source-aware cross-review, not a new independent derivation. No source/new scientific program, Field constructor, DP, witness, literal minors, permutation/raw-state search, test, experiment, import, compilation or kernel was executed. Only inert source/prose and metadata hash/time operations were read. No earlier note, seal or package file was edited. + +## Exact objects and verdict + +Source6712 head `03caa7f6cb5bd21c834024e9d81f6b43eb325b91`, directory `research/monomial-guard-settlement/`. Relevant byte bindings read after release: + +- settlement.py Git74df4fb3154fc62775850fcf54136a46faa33989, local SHA256 `2667a15111b7d0dc8c887ea2813c8340e07f7f33385f35cb3e956100f25039e4`. +- literal.py Gitbef3d242ad16109eabf27a41cf0c34b47ad76c6d, SHA256 `479b78c3f4f0ca21294d84685c0d6177acdac96ae974d29b192516ab9ecd4391`. +- monomial.py Git3b68a6d1a59b8407f4b54706eeaad78dfa397e21, SHA256 `57f870433d7cc005b875527f83c85be21ee620cb3310f61a7b557a1cbd8cbd72`. +- example_check.py Git311863c06845ac005292e25c47338dc6cde83ad6, SHA256 `9e18439050d137e8e7a6a4774e927f0f1b614a2707863fd3cac73a467a813a05`. +- Peer SETTLEMENT-CODE-DRAFT.md SHA256 `7bf994a3a42da5f0f0c5f14744b3245429c883ea9cbf2074e027c0da931bb184`. + +I also read the relevant central PROOF sections and the retained exact-arithmetic helper as inert text. Later proof sections appeared in that source excerpt, but binary-dummy, ternary, complexity/orbit and other later claims are not reviewed here. + +**Qualified PASS** for the zero-target settlement path and anchored full-family implication, under valid exact-field and shape/label premises. No mathematical correction to my first draft is required. Its source-proof-unexposed timestamp/hash remains accurately historical: first draft `8befc623ef765523ab9ac6ec6ec29de003f482724e1340c166e4917236d36a78` is unchanged. No new h-Z/source numeric result is claimed. + +## Actual dual orientation and attainable word + +The source's target=i, source=j convention is exactly `u_i+=a*u_j` and, for EVERY supplied dual row, `row_j-=a*row_i`. It is the coupled inverse right action required by my charge formula, not its transpose or a plus-sign variant. Each row's old target entry is used and copies are made, so the source's value semantics agree with the algebra. + +On `witness(...,target_value=None)`, active values are precisely nonzero vector charges. There is no dummy. A block's chosen root is its last real label; it need not be the label last removed by DP backtracking. Any donor in a zero-sum block works. The actual coefficient `mul[neg[u[i]]][inv[u[root]]]` is exactly -u_i/u_j, using field inversion rather than integer division. The donor u_j stays nonzero, each unvisited target u_i stays at its original nonzero value, and different blocks have disjoint labels. Thus every emitted coefficient is legal; intermediate cancellation of the donor CHARGE does not invalidate its nonzero u component. + +The code returns gates/certificate metadata, not transformed u/rows. My abstract claim was that those gates form an attaining word, not that the dictionary itself executes a header. A consumer must replay the gates on the full desired dual data, including b when appropriate. The source already has that consumer in example_check; it is not a missing step newly identified here. + +## DP mask order and literal backtracking + +`subset_sums` evaluates its appended list from the old list before extension; its order is the ordinary labeled binary-mask order. Every vector has the same width in this certified domain. For a mask and any present low bit, `mask^bit0, let Z be the maximum number of blocks in a partition of the LABELED active set A into nonempty zero-sum subsets. Such a partition exists because sum_A y_i=0. For h=0 use the empty partition and Z=0. A single nonzero charge cannot have total zero, so h=1 does not occur under these premises. Repeated equal vector values are still distinct labels. + +The settlement objective is to make every individual charge zero. The count-law/header-passing objective needs the extra affine/anchor conditions in Section5; it must not be silently identified with settlement for an arbitrary family. + +## 2. Local conservation and a lower bound including zero helpers + +For a paid addition i←i+a*j, the updates are + + u_i'=u_i+a*u_j, W_j'=W_j-a*W_i, + +with u_j and W_i unchanged and all other components unchanged. Therefore + + y_i'=y_i+a*u_j*W_i, + y_j'=y_j-a*u_j*W_i. + +Only those two charges can change, and their vector sum is conserved. This remains true when either initial/current charge is zero. In particular a zero-charge helper can acquire a nonzero charge; ignoring such slots in the lower bound would be invalid. + +Trace labeled strands through every free permutation; free diagonal scaling leaves each charge unchanged. Equivalently, conjugating a transvection by a monomial matrix merely changes its distinct indices and nonzero coefficient, so one may track/normalize free monomial actions without granting additional mixing. Draw an undirected edge between the tracked labels for each paid primitive. Multiple/ineffective edges still cost; they do not weaken the bound. + +Within any connected component of this paid-operation graph, its final charge sum equals its initial sum. If all final charges are zero, each component containing active labels therefore determines a nonempty zero-sum subset of the initial A. Those subsets partition A. Let their number be C. Then C<=Z. + +A component with a active labels and any additional zero-charge helpers needs at least a-1 edges: a connected graph on all its vertices needs at least vertices-1, which is no smaller. Sum over the C active components; ignore components with no initial active label. Any settling word of length L satisfies + + L>=sum_components(a-1)=h-C>=h-Z. + +This covers arbitrary intermediate charge creation/cancellation, initial zero helpers, repeated charges, and free monomial normalization. It is not merely a statement that one operation can remove at most one nonzero charge; an operation can remove two opposite charges at once, and the component/zero-sum partition is what accounts for that. + +## 3. A legal attaining word with a nonzero donor component + +Take a partition into Z zero-sum blocks. In each block B choose one collector/donor j. Since its INITIAL charge is nonzero, u_j!=0. For each i in B except j, apply + + i <- i - (u_i/u_j)*j. + +The coefficient is nonzero: before its elimination, that u_i is its unchanged initial nonzero value, and u_j stays nonzero. The operation sets u_i to0 and transfers its entire current charge to j: + + y_i' =0, y_j'=y_j+y_i. + +The collector's u_j is never changed by these operations. Even if its CHARGE happens to cancel at an intermediate stage, u_j remains nonzero and the next division is still legal. No assumption that its W_j or charge stays nonzero is needed. + +After |B|-1 operations all charges of B are zero because its initial sum was zero. Other blocks and all initial zero-charge helpers were untouched. Thus h-Z legal row additions settle every charge, matching the lower bound. This is an algebraic operation count under the full nonzero-field coefficient alphabet, not a bit/arithmetic/route/storage tariff. The chronological header product uses the same coupled W inverse at every step; it is not permissible to update u alone. + +## 4. Zero-prefix subset DP and partition backtracking + +For S subset of A let Y(S)=sum_(i in S)y_i. Define D(empty)=0 and, for nonempty S, + + D(S)=max_(i in S) D(S\{i}) + indicator[Y(S)=0]. + +Interpret D(S) as the maximum number of NONEMPTY zero-sum cumulative prefixes along an ordering of S. This interpretation follows by the last-element recurrence: all earlier prefixes form an ordering of S\{i}, and the new final prefix contributes precisely the displayed indicator. It does not require Y(S)=0 at intermediate subsets. + +For an ordering of the full A, its total sum is zero. Cut at every nonempty zero-prefix endpoint, including the last. Differences of two zero cumulative sums give nonempty consecutive zero-sum blocks covering A. Hence its number of counted endpoints is at most Z. + +Conversely order the blocks of any Z-block zero-sum partition, with their labels in any within-block order. Every block end is a zero-prefix endpoint, so the maximum is at least Z. Together these observations prove D(A)=Z. They also explain why maximizing the count, rather than minimizing it, gives the least settlement price h-D(A). + +Store one actual maximizing last-label choice at each subset. Backtrack from A to empty and reverse the removed-label sequence. Its zero-prefix boundaries give an actual labeled partition; the star-donor construction of Section3 then supplies an attaining word. No numerical field/DP enumeration is needed for this proof. If a code instead deduplicates equal charge values, counts the empty prefix, changes zero tests to approximate tests or reconstructs labels in the wrong direction, it no longer follows this association. The exponential subset state space is a source implementation consideration, not a practical scalability claim proved here. + +## 5. Full affine-family guards: necessity and anchored sufficiency + +Now let b be a row with b*u=1, assume W*u=0, and consider the FULL affine family + + v_lambda = b + lambda*W, lambda in E^*, + +where all coefficient rows are available, not an arbitrary subset. Under a header transform u,b,W together. For prefix j put + + s_j=sum_(i<=j)b_i*u_i, z_j=sum_(i<=j)u_i*W_i. + +The rank-one determinant identity gives the complement's leading minor as + + 1-s_j-lambda*z_j. + +For z_j!=0, the map lambda↦lambda*z_j is onto K (choose a nonzero coordinate and solve). Thus some family member has a zero minor at that prefix. If ALL members pass ALL proper prefixes, necessarily z_j=0 for j=1,...,m-1, and also s_j!=1. Since z_0=z_m=0, differences force every individual charge y_i=0, including the final one. Therefore any passing header pays at least the settlement lower bound. The lambda that fails can depend on j; no single lambda failing every prefix is required. + +Settlement alone does not automatically satisfy the scalar prefix conditions s_j!=1. For an attaining upper bound assume an ANCHORED scalar carrier c: + + u_c!=0, W_c=0, + b_i=0 for i!=c, b_c*u_c=1. + +The anchor is not active. The attaining word in Section3 uses only initially active indices, hence avoids c, preserves u_c and W_c, and preserves b because its transvection targets have b_i=0. All charges become zero with exactly h-Z paid operations while the scalar carrier survives. A final free permutation places c last. Every proper prefix then has z_j=0 and s_j=0, so every full-family proper minor equals1. This proves the same price for the anchored full-family passing problem, without an extra paid scalar-settlement step. + +The lower bound allowed arbitrary paid words, including use of zero helpers or the anchor. The upper construction preserves the anchor. Thus allowing additional such words cannot beat the lower bound, and no restriction that all hypothetical words preserve the anchor was needed. Conversely without the anchor premise this upper construction does not establish the same guard price. + +## 6. Written weakening controls — UNEXECUTED + +1. **Forget zero helpers in the lower bound.** A paid move can create a charge at an initially zero slot while moving it from another. Track every paid edge/label, including those helpers; only then do connected components conserve their initial sums and bound the operation count. A proof based only on the number of currently nonzero slots is insufficient. +2. **Lose the coupled inverse.** Update u by a row addition but leave W fixed. The displayed two-charge transfer and component conservation no longer hold. A charge can then disappear for reasons outside this header model. +3. **Permit arbitrary free GL.** A free general basis change can align a nonzero u with the last coordinate; W*u=0 then puts its last image column at zero and settles all charges for free. Restricting free headers to monomial matrices is essential to the h-Z price. +4. **Restrict the paid alphabet silently.** The attaining coefficient is -u_i/u_j. If a fixed language disallows that field element, or charges for its arithmetic/precision, h-Z is not automatically its operation price. The theorem uses all nonzero field coefficients at unit abstract cost. +5. **Confuse charge zero with donor component zero.** The collector's charge may cancel before all transfers, but u_j remains nonzero. Stopping on that charge, or dividing by a W component instead of u_j, can wrongly reject a legal attaining construction. +6. **Deduplicate labels or count the empty DP prefix.** Repeated equal nonzero charges are separate input slots (for example four identical charges over F2 can split into two opposite-in-characteristic-two pairs). Empty-prefix counting would shift D by one and falsely reduce the predicted paid price. Zero-prefix endpoints must reconstruct nonempty blocks covering all active labels. +7. **Replace full family by a subfamily.** Over F3, take m=3,u=(1,1,1), W=(1,-1,0), b=(0,0,1). The singleton lambda=0 passes every proper prefix at the identity although charges are not settled. The full affine family includes a member failing a prefix. Necessity of settlement is a quantified all-lambda statement, not a statement for arbitrary named guard subfamilies. +8. **Drop the scalar anchor.** Over F2, take m=4,u=(1,1,1,0), b=(1,1,1,0), W=(0,0,0,1). Then b*u=1, W*u=0 and all charges are zero, so settlement costs0. But scalar products b_i*u_i are three ones and one zero. Under any free monomial header they merely permute, so the first one occurs at a proper prefix and gives a failed minor. Thus the unanchored full-family guard price is not automatically h-Z. This is a changed-premise hand control, not a counterexample to the anchored source claim. + +These are mathematical deductions, not executed tests, new source fields or observed source failures. No DP value, h/Z statistic, header census or physical cost was computed by a program. + +## Credit and remaining source binding + +The source6712 owns h-Z and its stated applications/certificates. Zero-sum partitioning, component bounds, row elimination and rank-one determinant arguments are classical principles; this review does not claim their invention. Prior common-image family/row-dependency work remains distinct. Substantial OpenAI Codex assistance produced this target-known note without a blind/human/kernel claim. + +Post-seal review must bind the actual source definition of active charges, free/paid alphabet, anchor, DP and returned header convention to these hypotheses. The note supplies no arbitrary-subfamily/unanchored price theorem, physical coefficient/route/owner/tape/retained restoration invoice, selected assumption discharge, new count or kappa/frontier/adoption change. diff --git a/research/settlement-header-word-review/RECORD-DERIVATION-SEAL.json b/research/settlement-header-word-review/RECORD-DERIVATION-SEAL.json new file mode 100644 index 0000000000..e29138844f --- /dev/null +++ b/research/settlement-header-word-review/RECORD-DERIVATION-SEAL.json @@ -0,0 +1,16 @@ +{ + "current6712_proof_or_code_read_before_seal": false, + "current_peer_or_coordinator_draft_read_before_seal": false, + "draft": { + "bytes": 13198, + "path": "/private/tmp/contribution-batch-b13-20261105T2038Z/session-08/SETTLEMENT-DERIVATION-DRAFT.md", + "sha256": "8befc623ef765523ab9ac6ec6ec29de003f482724e1340c166e4917236d36a78" + }, + "historical_context": "Prior common-image/count-law review context is known; source-proof-unexposed for this assignment, not blind discovery.", + "limits": "No source/new program import, compilation, constructor, DP, field test, census, numerical experiment or kernel. Only written mathematics and metadata hash/time.", + "role": "target-known abstract charge-settlement and anchored affine-family derivation", + "schema_version": 1, + "scientific_execution": false, + "sealed_at_utc": "2026-11-06T00:55:59.805057+00:00", + "target": "PR6712 h-Z charge settlement under coupled monomial/free and full-field paid row-add alphabet, subset DP, anchored full affine guard family" +} diff --git a/research/settlement-header-word-review/REVIEW.md b/research/settlement-header-word-review/REVIEW.md new file mode 100644 index 0000000000..de5afbb0c9 --- /dev/null +++ b/research/settlement-header-word-review/REVIEW.md @@ -0,0 +1,81 @@ +# Settlement price and its actual attaining header + +## Result and exact scope + +Qualified written PASS: SHIN09-git [PR6712](https://github.com/CrocSwap/integer-mult-bounds/pull/6712), head `03caa7f6cb5bd21c834024e9d81f6b43eb325b91`, already proves the central h−Z slope-settlement price. This external review binds its lower bound, subset-DP/backtracking and actual `witness(..., target_value=None)` row word to the anchored complete-affine-family proper-minor endpoint. No material discrepancy was found on that domain; no code change is requested. + +This is a new source-bound review, not a new theorem, optimum, witness execution, count or physical tariff. The source owns h−Z, its original eight commands, multiple routes, twenty faults and all reported finite outcomes. None was executed here. The binary dummy target branch, ternary scalar/envelope/extra-step claims, NP-completeness, orbit classifications and later sections are outside this review, including where retained source context exposes their text. + +`PROOF.md` blob `234bbba4812a8a5ca774679451ba17a8072d6b56`, `ALGORITHM.md` `f855486175dd7c85c86fe410e85038636bed55aa` and `settlement.py` `74df4fb3154fc62775850fcf54136a46faa33989` are the central inputs. The exact additional consumer/arithmetic texts and source custody are listed in SOURCE-PINS.json. Python files are inert `.py.txt`; this subset is not a runnable original suite. Remote source custody is checked separately from canonical-main provenance; no pending foreign object is represented as a main ancestor. + +## Model and quantified endpoint + +Let K be a field, u a fixed-dimensional column, b a row with bu=1, and W a matrix with Wu=0. The guard family contains **every** row b+λW, λ∈K^d. A header transforms u→Tu and each dual row r→rT⁻¹. Permutations and invertible diagonal matrices are free; every transvection T=I+aEᵢⱼ with i≠j, a≠0 costs one. Input-dependent choice is allowed. This is a coordinate-header metric; original coordinates need not be restored. No restricted instruction alphabet, coefficient bit cost, physical gate realization or free general linear mixing is inferred. + +Define labeled vector charges yᵢ=uᵢW_:ᵢ, active set A={i:yᵢ≠0}, h=|A|. Their total is zero. Let Z be the largest number of nonempty zero-sum blocks in a partition of A. For h=0 set Z=0. Equal charge values retain distinct labels. + +For any proper prefix put X=Σbᵢuᵢ and Y=ΣuᵢW_:ᵢ over that prefix. Its rank-one-complement determinant is 1−X−λY. If Y≠0, the scalar map λ↦λY is surjective, so some member of the **complete** family fails that minor. Passing every member at every proper prefix forces all such Y to zero. Consecutive differences, together with total Wu=0, force every individual yᵢ=0. The failing λ may depend on the prefix; a common failing parameter is unnecessary. + +Thus successful full-family headers must settle the slope charges. The converse also needs scalar prefixes to avoid one; settlement alone is insufficient. The attaining full-guard statement below uses a scalar anchor and makes all proper determinants exactly one. + +## Lower bound against every allowed word + +For the paid step i←i+a·j, the actual dual update is W_:ⱼ←W_:ⱼ−aW_:ᵢ while uᵢ←uᵢ+auⱼ. Hence + + yᵢ′ = yᵢ + auⱼW_:ᵢ, + yⱼ′ = yⱼ − auⱼW_:ᵢ. + +Only two charges change and their vector sum is conserved. This holds for initially zero-charge helpers too; a helper can acquire charge and cannot simply be discarded from a lower-bound proof. + +Monomial matrices normalize transvections. Move free operations to the end by conjugation, preserving paid length and legal nonzero coefficients, or equivalently track labeled strands through free permutations. Diagonal factors leave each charge unchanged and terminal permutations only relabel the settled objective. This normalization is for charge settlement, not a claim that arbitrary permutations preserve the guard event. + +Draw an undirected edge for each paid step between its tracked labels. At a settled endpoint, each connected component's initial charge sum is zero. Components containing active labels induce C nonempty zero-sum blocks partitioning A, so C≤Z. A component containing k active labels and any zero helpers needs at least k−1 edges. Counting all paid edges, including repetitions or ineffective operations, gives + + L ≥ Σ(k−1) = h−C ≥ h−Z. + +Components with no initially active label contribute no negative cost. This covers intermediate cancellation/creation and all allowed words, including ones using the scalar anchor. A heuristic that each step removes at most one active charge would not suffice: a step can remove two opposite charges. + +## Why the actual subset recurrence and backtracking attain Z + +`subset_sums` doubles the old list by adding the next labeled vector. Under equal widths and exact valid field labels, numeric indices are the intended bitmask sums. `partition` rejects a nonzero total and uses + + D(∅)=0, + D(S)=maxᵢ∈S D(S\{i}) + [Σᵢ∈S yᵢ=0]. + +This maximizes the number of nonempty zero cumulative prefixes along an ordering of S, by choosing its last label. Every predecessor mask is numerically smaller. At full A, cut an ordering at all zero-prefix boundaries: those cuts form nonempty zero-sum blocks covering A. Conversely concatenate a maximum zero-sum partition; its block ends are zero prefixes. Therefore D(A)=Z. + +The stored `last[mask]` is an actual maximizing removed bit. Backtracking starts with zero-total `end=A`; whenever the nested remaining mask has zero total, `end ^ mask` is a nonempty zero-sum set difference, then `end` becomes that remaining mask. Successive differences are disjoint and cover A upon reaching empty. Their number is D(A); the source checks that association. Empty input returns the empty partition. Repeated vector values are never deduplicated. The check alone does not establish maximality; the preceding recurrence interpretation does. + +No DP value or finite partition was computed by this review. Exponential state space is not a scalability endorsement. + +## Legal attaining word and the literal code orientation + +In each optimal block choose its final real label j as collector. Initially active yⱼ implies uⱼ≠0. For every other i in that block use a=−uᵢ/uⱼ and target i, source j. Unvisited uᵢ retains its initial nonzero value and uⱼ never changes; disjoint blocks cannot affect it. Thus every coefficient is legal and nonzero, even if the collector's **charge** cancels before the final transfer. Each step sets uᵢ to zero and transfers its entire current charge into j. At the end the collector charge is the original block sum, zero. This uses |block|−1 steps per block, hence h−Z total. + +`add_row` first copies u and each row. It rejects target==source or zero a, sets `u[target] += a*u[source]`, then sets each copied `row[source] -= a*row[target]`. Distinct indices mean the target entry used for that dual update is its old value. The expression `mul[neg[u[i]]][inv[u[root]]]` is precisely the field quotient above; no ordinary-integer division or inverse of zero is needed. The zero-target witness filters active labels, partitions them without a dummy, records the tuples, applies this update, and checks no remaining nonzero charges and gate count h−number_of_blocks. + +Its returned dictionary contains gate tuples/certificate metadata, **not** transformed u and dual rows. Replaying these tuples on all original rows is a separate consumer obligation; storing the dictionary alone does not execute a header. + +## Anchored full proper-minor bridge and existing consumer + +Assume b is supported at c, u_c b_c=1 and W_:c=0. Then c is inactive and the attaining word never touches it. Every target/donor is outside c, so both corresponding b entries stay zero under the inverse-dual update. The anchor's b, u and slope column are preserved. After slope settlement, a free permutation puts c last. All proper scalar prefixes are zero and all proper slope prefixes are zero, so every original full-family proper determinant is one. The lower bound allowed arbitrary words, including use of c; the attaining word avoids it. No unanchored price theorem follows. + +There is already a real source consumer. `example_check.collect()` obtains the anchored slope-only gates. `example_check.example()` replays them through `add_row` on BOTH b and w, calls `flat_rows` to enumerate the complete parameter family, and compares a positive `literal_orders` result against `passing_permutations`. `literal_orders` builds actual complements and principal submatrices for every proper size 1,...,m−1 along labeled orders; it excludes the full corank-one determinant. `certificates.constructions()` merely retaining witness dictionaries is a different use. The finite replay and lower-depth search already belong to the source; neither ran here. The uniform argument above supplies the all-input implication, conditional on the model, rather than extrapolating from those examples. + +## Code domain and written weakening controls + +The retained exact `Field` implements q∈{2,3,4,5,7,8,9}. The abstract field theorem is broader; this review does not certify every arithmetic table/irreducible polynomial or claim an all-prime-power code constructor. Field validity, equal row/vector widths, valid labels and coordinate indices are premises. Generic helpers do not independently admit arbitrary malformed/hostile packets. + +The sealed abstract/code roles contain eight and nine overlapping **UNEXECUTED** weakening controls, not seventeen experiments. They challenge the coupled inverse sign/orientation, zero helpers, free-monomial normalization, legal coefficient alphabet, collector component vs charge, labeled optimal DP vs greedy blocks, complete parameters, scalar anchor, every proper prefix and generated valid-input domain. + +Two explicit hand controls delimit the endpoint. Over F₃, u=(1,1,1), W=(1,−1,0), b=(0,0,1): the singleton λ=0 passes identity proper prefixes despite nonzero slope charges; the complete family supplies the failing parameter. Over F₂, u=(1,1,1,0), b=(1,1,1,0), W=(0,0,0,1): bu=1, Wu=0, h=0, yet three scalar ones cannot avoid a proper prefix sum of one under free monomials. Thus unanchored guard success is not implied by zero slope cost. These are changed-premise mathematical deductions, not observed source failures or new field searches. + +## Review process, credit and obligations + +The coordinator read the prior scout/source body and had informal preclaim algebraic reasoning. The code role had earlier source proof/code/later-section exposure. The target-known abstract role sealed before current6712 proof/code/peer reading; historical context is not excluded. First drafts and seals are retained unchanged, followed by a source/peer cross and an exact-version assembled review. AI role separation supplies inspectable arguments, not blind discovery, human independence or proof-kernel acceptance. No scientific source import, DP, field computation, constructor, matrix/minor search, census, mutant or kernel ran. + +The original formal-interface task card is retained with explicit CHANGED written-review scope; its formal/kernel gate remains unmet. Reviewers can inspect this argument against exact inert texts and sealed roles without a replay hook. There is no scientific VERIFY registration and no claim of replaying the source's eight commands. Hosted repository-helper CI is reported separately if run. + +SHIN09-git6712 retains the law, prices, original witnesses and subsequent classifications, with its disclosed Codex assistance. Credit6710 finite-field/context work, ToikY's distinct binary/all-field pair and prior header work, Nick Petalas's marginal/pair/header predecessors, all original NOTICE/license contributors and classical determinant, row-operation, connected-component/debt-clearing/zero-sum partition methods. This review was produced by ToikY with substantial OpenAI Codex assistance and separate abstract/code/metadata/byte roles; no predecessor endorsement is asserted. + +Actual physical header selection, coefficient implementation, placement/movement, restoration/inverse, tape/precision, stock/owner cleanup, sampling, native/all-column supplier, compiler and full tariff remain open. All five selected framework assumptions remain in their prior state. No κ/frontier/adoption change, merge, physical multiplication result, new numerical optimum or reservation of follow-on work follows. diff --git a/research/settlement-header-word-review/SOURCE-PINS.json b/research/settlement-header-word-review/SOURCE-PINS.json new file mode 100644 index 0000000000..98c5017e53 --- /dev/null +++ b/research/settlement-header-word-review/SOURCE-PINS.json @@ -0,0 +1,185 @@ +{ + "schema_version": 1, + "files": [ + { + "local_path": "inputs/ALGORITHM.md", + "repository": "SHIN09-git/integer-mult-bounds", + "commit": "03caa7f6cb5bd21c834024e9d81f6b43eb325b91", + "path": "research/monomial-guard-settlement/ALGORITHM.md", + "git_blob": "f855486175dd7c85c86fe410e85038636bed55aa", + "sha256": "50a6b09914858a786eac7112f46cc40f854dcd1fe4eab85416bc8c3e2096039b", + "bytes": 5130, + "original_pr": 6712, + "original_head": "03caa7f6cb5bd21c834024e9d81f6b43eb325b91", + "usage": "inert exact written-review source; Python copies .txt; no scientific execution; subset not original runnable suite" + }, + { + "local_path": "inputs/LICENSE", + "repository": "CrocSwap/integer-mult-bounds", + "commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "path": "LICENSE", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "bytes": 11357, + "original_pr": null, + "original_head": null, + "usage": "inert exact written-review source; Python copies .txt; no scientific execution; subset not original runnable suite" + }, + { + "local_path": "inputs/NOTICE", + "repository": "SHIN09-git/integer-mult-bounds", + "commit": "03caa7f6cb5bd21c834024e9d81f6b43eb325b91", + "path": "research/monomial-guard-settlement/NOTICE", + "git_blob": "cb8d1d358fb2a34159b0a0590d9d406b6f41495f", + "sha256": "a1dbffd855be85d5228ffeb7d1eea68b19b8ed708c17a51684b8e1373ff59c63", + "bytes": 714, + "original_pr": 6712, + "original_head": "03caa7f6cb5bd21c834024e9d81f6b43eb325b91", + "usage": "inert exact written-review source; Python copies .txt; no scientific execution; subset not original runnable suite" + }, + { + "local_path": "inputs/PROOF.md", + "repository": "SHIN09-git/integer-mult-bounds", + "commit": "03caa7f6cb5bd21c834024e9d81f6b43eb325b91", + "path": "research/monomial-guard-settlement/PROOF.md", + "git_blob": "234bbba4812a8a5ca774679451ba17a8072d6b56", + "sha256": "23ccd896bc8bc20f3e6171d45eb41648ed512b16b0719a099f437719004141e7", + "bytes": 9863, + "original_pr": 6712, + "original_head": "03caa7f6cb5bd21c834024e9d81f6b43eb325b91", + "usage": "inert exact written-review source; Python copies .txt; no scientific execution; subset not original runnable suite" + }, + { + "local_path": "inputs/README.md", + "repository": "SHIN09-git/integer-mult-bounds", + "commit": "03caa7f6cb5bd21c834024e9d81f6b43eb325b91", + "path": "research/monomial-guard-settlement/README.md", + "git_blob": "1ed2b1058a5eeae64efb55d53bf3df297c51f61d", + "sha256": "fa282b62b11938c7cfe3606203945d5ced6a323347d6d6fa149275f76aee510e", + "bytes": 4209, + "original_pr": 6712, + "original_head": "03caa7f6cb5bd21c834024e9d81f6b43eb325b91", + "usage": "inert exact written-review source; Python copies .txt; no scientific execution; subset not original runnable suite" + }, + { + "local_path": "inputs/ROOT-NOTICE", + "repository": "CrocSwap/integer-mult-bounds", + "commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "path": "NOTICE", + "git_blob": "59d8e0cf3102e15bd11db430838365531e2d7f18", + "sha256": "b49022cb4104d90b182e4c335f670faf45529025b15db77bf0291835083c28bd", + "bytes": 24973, + "original_pr": null, + "original_head": null, + "usage": "inert exact written-review source; Python copies .txt; no scientific execution; subset not original runnable suite" + }, + { + "local_path": "inputs/certificates.py.txt", + "repository": "SHIN09-git/integer-mult-bounds", + "commit": "03caa7f6cb5bd21c834024e9d81f6b43eb325b91", + "path": "research/monomial-guard-settlement/certificates.py", + "git_blob": "e753a14ac687c0d2826a0bb42db9999bdbc4d89f", + "sha256": "5489a7a9e075d0a9f0e4f05450601d9467d3cbfb345f730cd01704bb5d99ccc7", + "bytes": 5747, + "original_pr": 6712, + "original_head": "03caa7f6cb5bd21c834024e9d81f6b43eb325b91", + "usage": "inert exact written-review source; Python copies .txt; no scientific execution; subset not original runnable suite" + }, + { + "local_path": "inputs/example_check.py.txt", + "repository": "SHIN09-git/integer-mult-bounds", + "commit": "03caa7f6cb5bd21c834024e9d81f6b43eb325b91", + "path": "research/monomial-guard-settlement/example_check.py", + "git_blob": "311863c06845ac005292e25c47338dc6cde83ad6", + "sha256": "9e18439050d137e8e7a6a4774e927f0f1b614a2707863fd3cac73a467a813a05", + "bytes": 2545, + "original_pr": 6712, + "original_head": "03caa7f6cb5bd21c834024e9d81f6b43eb325b91", + "usage": "inert exact written-review source; Python copies .txt; no scientific execution; subset not original runnable suite" + }, + { + "local_path": "inputs/literal.py.txt", + "repository": "SHIN09-git/integer-mult-bounds", + "commit": "03caa7f6cb5bd21c834024e9d81f6b43eb325b91", + "path": "research/monomial-guard-settlement/literal.py", + "git_blob": "bef3d242ad16109eabf27a41cf0c34b47ad76c6d", + "sha256": "479b78c3f4f0ca21294d84685c0d6177acdac96ae974d29b192516ab9ecd4391", + "bytes": 2113, + "original_pr": 6712, + "original_head": "03caa7f6cb5bd21c834024e9d81f6b43eb325b91", + "usage": "inert exact written-review source; Python copies .txt; no scientific execution; subset not original runnable suite" + }, + { + "local_path": "inputs/monomial.py.txt", + "repository": "SHIN09-git/integer-mult-bounds", + "commit": "03caa7f6cb5bd21c834024e9d81f6b43eb325b91", + "path": "research/monomial-guard-settlement/monomial.py", + "git_blob": "3b68a6d1a59b8407f4b54706eeaad78dfa397e21", + "sha256": "57f870433d7cc005b875527f83c85be21ee620cb3310f61a7b557a1cbd8cbd72", + "bytes": 1355, + "original_pr": 6712, + "original_head": "03caa7f6cb5bd21c834024e9d81f6b43eb325b91", + "usage": "inert exact written-review source; Python copies .txt; no scientific execution; subset not original runnable suite" + }, + { + "local_path": "inputs/settlement.py.txt", + "repository": "SHIN09-git/integer-mult-bounds", + "commit": "03caa7f6cb5bd21c834024e9d81f6b43eb325b91", + "path": "research/monomial-guard-settlement/settlement.py", + "git_blob": "74df4fb3154fc62775850fcf54136a46faa33989", + "sha256": "2667a15111b7d0dc8c887ea2813c8340e07f7f33385f35cb3e956100f25039e4", + "bytes": 3618, + "original_pr": 6712, + "original_head": "03caa7f6cb5bd21c834024e9d81f6b43eb325b91", + "usage": "inert exact written-review source; Python copies .txt; no scientific execution; subset not original runnable suite" + }, + { + "local_path": "inputs/source/6710-NOTICE", + "repository": "SHIN09-git/integer-mult-bounds", + "commit": "03caa7f6cb5bd21c834024e9d81f6b43eb325b91", + "path": "research/monomial-guard-settlement/source/6710-NOTICE", + "git_blob": "c799eae7d615d1ab50a0636362d41afb54e03f7d", + "sha256": "73c84c39fce771bc67decaf259fbde4ef3a36186e69bae8f010e641bd606c854", + "bytes": 630, + "original_pr": 6712, + "original_head": "03caa7f6cb5bd21c834024e9d81f6b43eb325b91", + "usage": "inert exact written-review source; Python copies .txt; no scientific execution; subset not original runnable suite" + }, + { + "local_path": "inputs/source/LICENSE", + "repository": "SHIN09-git/integer-mult-bounds", + "commit": "03caa7f6cb5bd21c834024e9d81f6b43eb325b91", + "path": "research/monomial-guard-settlement/source/LICENSE", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "bytes": 11357, + "original_pr": 6712, + "original_head": "03caa7f6cb5bd21c834024e9d81f6b43eb325b91", + "usage": "inert exact written-review source; Python copies .txt; no scientific execution; subset not original runnable suite" + }, + { + "local_path": "inputs/source/finite.py.txt", + "repository": "SHIN09-git/integer-mult-bounds", + "commit": "03caa7f6cb5bd21c834024e9d81f6b43eb325b91", + "path": "research/monomial-guard-settlement/source/finite.py", + "git_blob": "b88d32f8ef386f3debd589d6eaf72d5501ab1132", + "sha256": "506c96e92759a2f4aab5e0f88a340506ab900db99a924d3d21547752eeeacfd6", + "bytes": 2599, + "original_pr": 6712, + "original_head": "03caa7f6cb5bd21c834024e9d81f6b43eb325b91", + "usage": "inert exact written-review source; Python copies .txt; no scientific execution; subset not original runnable suite" + }, + { + "local_path": "inputs/verify.py.txt", + "repository": "SHIN09-git/integer-mult-bounds", + "commit": "03caa7f6cb5bd21c834024e9d81f6b43eb325b91", + "path": "research/monomial-guard-settlement/verify.py", + "git_blob": "ddfade70fb213da5a493f6c244aef3943bc1a482", + "sha256": "d1d8b1de08f690e7ff68f15fc3860509d677b94b0c7781d3a779730a6735116f", + "bytes": 4208, + "original_pr": 6712, + "original_head": "03caa7f6cb5bd21c834024e9d81f6b43eb325b91", + "usage": "inert exact written-review source; Python copies .txt; no scientific execution; subset not original runnable suite" + } + ] +} diff --git a/research/settlement-header-word-review/SOURCES.json b/research/settlement-header-word-review/SOURCES.json new file mode 100644 index 0000000000..eb62d04aab --- /dev/null +++ b/research/settlement-header-word-review/SOURCES.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "AGENTS.md", + "usage": "provenance", + "git_blob": "fa006ceb6b6b9d6c0e799f210963f4587ecfb162", + "sha256": "fbee67ab9e0ae4629a35fd9dba69c8f7e29e4a15392eb2d0f75d8768ffb65f40" + }, + { + "path": "autoresearch.md", + "usage": "provenance", + "git_blob": "2fe84a7b30b1e26e60ce0ec4775894eb1831c5d6", + "sha256": "d16f0d3bb4d4b213d06c128db6d6460b0fe9ec1ac5a6c1ea1febf1db40e7b60d" + }, + { + "path": "CONTRIBUTING.md", + "usage": "provenance", + "git_blob": "5185786f2ec00f215019fb5777d70979429690a9", + "sha256": "fcd1a8d0e52342a23b8ffa9e905e85ccc539fb084145ef016dfc93cedfb3d924" + }, + { + "path": "docs/research/current-priorities.md", + "usage": "provenance", + "git_blob": "6f5d40d13d8f3bdc12ce7954c8c3eb4ab1f8be91", + "sha256": "70f61c8d140ae6e892f2b8f065bba4eae3e76f7a8f55f632fd4e2f9f34039bdc" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-procedure.md", + "usage": "provenance", + "git_blob": "06b35b9805b5c15d1623edfb20560266a4bbfdfc", + "sha256": "8367063f9f2d48543415451e026f83224ea962b28801bea6904e6e425ed023e4" + }, + { + "path": "docs/research/research-family-status.md", + "usage": "provenance", + "git_blob": "3c19b18ef7225b47f0abcd9d51ae7c83d0cdfd15", + "sha256": "92c8010dfd9fc33e921f70526231f8689e06ea784f1b1387d895344b227f36d7" + }, + { + "path": "LICENSE", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "usage": "provenance" + }, + { + "path": "NOTICE", + "git_blob": "59d8e0cf3102e15bd11db430838365531e2d7f18", + "sha256": "b49022cb4104d90b182e4c335f670faf45529025b15db77bf0291835083c28bd", + "usage": "provenance" + } + ] +} diff --git a/research/settlement-header-word-review/TASK.json b/research/settlement-header-word-review/TASK.json new file mode 100644 index 0000000000..96eb006e8e --- /dev/null +++ b/research/settlement-header-word-review/TASK.json @@ -0,0 +1,135 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "External written source-bound review of PR6712 central zero-target h-Z settlement, debt partition and constructed row-addition word, plus anchored full-prefix/proper-minor binding. Source theorem, implementation and finite counts remain predecessor results.", + "scope_change_reason": "Formal-interface card narrowed to a written algebra-to-source and anchored-family review; original formal/kernel gate remains unmet.", + "scope_key": "settlement-header-word-review:03caa7f6:central-h-minus-Z-and-anchored-prefix", + "seed": "813e0000000000000000000000000008", + "time_budget_minutes": 60, + "question": "Under the source valid exact-field/value domain and stated full-family/anchor hypotheses, do central settlement and the actual generated word/anchored-prefix association satisfy the stated contract?", + "success_rule": "Separately sealed written abstract and code reviews, source/peer reconciliation and explicit hypotheses/weakening controls, or an actionable gap.", + "stop_rule": "Freeze scientific work by2026-11-06T01:32:50Z; reserve at least15minutes for verification before01:47:50Z. No source/scientific imports, original tests, census, numerical experiment, new verifier or proof-kernel/native execution.", + "method": "Target-known abstract draft sealed before current source proof/code/peer; separate source-aware code draft sealed before peer; then source/peer reconciliation. Prior6710/common-image familiarity disclosed. No blind, human or proof-kernel acceptance claim.", + "bottleneck_link": "A mathematical charge-settlement identity needs its exact allowed operations, source-generated word and anchored full-family hypotheses; generic mathematical code is not a hostile certificate-packet parser.", + "family_decision": "External written review of existing central settlement/actual-word and anchored-prefix interfaces. Existing source gate replay, ternary/envelope/orbit/DP evidence and20fault outcomes are not new or rerun.", + "outcome": "partial", + "scientific_status": "WRITTEN_SETTLEMENT_WORD_REVIEW_NO_GAP_FOUND", + "author": "ToikY", + "ai_assistance": "Substantial OpenAI Codex with separate target-known abstract/source-aware code/metadata/finalbyte roles; code6712 prior scout and root priorbody/preclaim reasoning disclosed, historical6710/common-image familiarity notexcluded; first drafts sealed before current peer cross-reading.", + "credit": "SHIN09-git owns PR6712 central theorem, word/code and existing evidence, with substantial OpenAI Codex assistance. Classical determinant identities, elementary row operations and debt partition; PR6710 retained finite-field arithmetic and notices; ToikY binary complete-header/all-field pair-sign extension; Nick Petalas predecessor marginal/common-covector pair law. ToikY/OpenAI Codex external written review.", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19429938", + "overlap": { + "at": "2026-11-06T01:00:00Z", + "live_open_prs": 702, + "complete_pages": [ + 100, + 100, + 100, + 100, + 100, + 100, + 100, + 2 + ], + "source_head": "03caa7f6cb5bd21c834024e9d81f6b43eb325b91", + "queries": "Coordinator liveHub/index/all-state and exact6712/package coverage; prepublication refresh found only unrelated6752 archive delta, source comments0/head unchanged.", + "limits": "This records coordinator overlap receipts, not an exhaustive absence or novelty proof; hidden/unindexed/unpublished work UNKNOWN.", + "excluded": "99 priorresults andB13sessions1-7; source6712 theorem/code/counts/gate replay,6710,ToikY/Nick predecessors are not new/recounted." + }, + "remaining_obligations": [ + "Original formal/kernel acceptance gate unmet; source-aware AI review is not human or kernel acceptance.", + "Exact valid field/value domain, full family, anchor and generated-data hypotheses remain essential; generic helpers are not an arbitrary hostile packet parser.", + "Source47files not all reviewed; curated15inputs/90418B are an inert subset, not original runnable closure. Original eightcommands/20faults and all source finite counts were not executed.", + "Later binary/ternary/envelope/DP/orbit/price claims outside this central/anchored review are UNREVIEWED here.", + "No native/physical cost, supplier, full multiplication theorem, allfive selectedassumptions, kappa/frontier change, adoption or merge." + ], + "open_questions": [ + { + "question": "Can the exact central settlement, allowed row word and anchored full-family hypotheses be formalized in a proof kernel?", + "why_it_matters": "Written source-aware roles do not meet formal acceptance.", + "first_step": "State the typed exact-field/value domain and allowed operation alphabet, then bind the generated word and anchored family.", + "blocked_by": "No kernel development or separately budgeted formal build in this session." + }, + { + "question": "Which stronger parser or physical implementation contracts can be established separately?", + "why_it_matters": "The current generic mathematical routines and word identities do not establish hostile-packet validation or physical billing.", + "first_step": "Specify a concrete typed parser/caller and primitive invoice before claiming admission.", + "blocked_by": "Outside this written central/anchored interface review." + } + ], + "evidence": "Abstract draft13198B SHA8befc623ef765523ab9ac6ec6ec29de003f482724e1340c166e4917236d36a78 sealed00:55:59.805057UTC before currentproof/code/peer; source-aware code17081B SHA7bf994a3a42da5f0f0c5f14744b3245429c883ea9cbf2074e027c0da931bb184 sealed00:54:59.195538UTC beforepeer. Qualified written PASS/no materialgap reported with full-family/anchor/validField/generic-not-packet-parser limits; cross and REVIEW retained separately. Actual source anchored gate replay already existed and was not executed here. Source15/90418B,13foreign+2canonicalroot copies; remote commit/root/research/package/source path/mode/blob/size custody and full originalcard/canonical10provenance checked by metadata role. Zero scientific commands. Assembled, committed, export, public and CI evidence separate. Sourcecross SHA9e2f4c41fc824c590853cb5d85de9d594cdbf9abd124740dac2d572ce90af189; exactassembled SHA6c8de9914e17d1d24d1621682b80b813dbd6f9fcd0f0b4b5f3827ef38a227546 bindsREVIEW12550B SHAf623123e4f1ea937d0e1976f7c750338633ef2aba4c14e4e8fc451dfc95898c5; qualifiedPASS/no corrections. Eight+nine overlapping UNEXECUTED controls, not17experiments." +} diff --git a/research/settlement-header-word-review/inputs/ALGORITHM.md b/research/settlement-header-word-review/inputs/ALGORITHM.md new file mode 100644 index 0000000000..f855486175 --- /dev/null +++ b/research/settlement-header-word-review/inputs/ALGORITHM.md @@ -0,0 +1,34 @@ +# Computing and certifying the price + +## Exact algorithms + +For the list of $h$ nonzero charges (or the augmented binary list), precompute $\Sigma(S)$ for every labeled subset. Any order of a zero-total list cuts into zero-sum blocks at its zero prefix sums. Conversely, concatenating any zero-sum partition yields at least that many boundaries. Thus the maximum number of zero-sum blocks is given by + +~~~text +P(empty) = 0 +P(S) = [sum(S)=0] + max_{i in S} P(S without i). +~~~ + +Store an attaining predecessor, recover the order, then cut at its zero sums. The comparison and reconstruction are independent of the cost of constructing the actual row additions. PROOF.md supplies those additions. For vectors of width $d$, the labeled DP uses $O((h+d)2^h)$ field/index operations and $O((d+1)2^h)$ stored entries, plus the explicit gates. With $t$ fixed charge types of multiplicities $n_i$, use a count vector instead of a subset. This needs at most $\prod_i(n_i+1)$ states and $O((t+d)\prod_i(n_i+1))$ operations. For fixed field and fixed slope dimension this is polynomial in the number of labeled coordinates. A minimizing word is easy to check by actual multiplication once its partition is known. + +## Small scalar fields + +An inverse pair $x,-x$ can always be placed together in a maximizing partition. If they were in different blocks, extract the pair and unite the two remainders, whose total is zero. If they were together in a larger block, splitting the pair off gives an additional block. Thus canceling all existing inverse pairs is safe. Arbitrary choices of larger zero-sum subsets need not preserve the maximum. + +For scalar slope charges of total zero, the following give $Z$, before charging $h-Z$ additions. + +* Over $\mathbb F_2$, $Z=h/2$. +* Over $\mathbb F_3$, let $A,B$ be the counts of $+1,-1$. Pair opposite signs and make triples from the remaining equal charges. This gives $Z=\min(A,B)+|A-B|/3$. +* Over $\mathbb F_4$, the three nonzero elements sum to zero, and all three multiplicities have the same parity. Pair identical elements. If the three counts are odd, the remaining three elements form one block. This attains $Z=\lfloor h/2\rfloor$ since every block needs at least two entries. +* Over $\mathbb F_5$, remove inverse pairs and count them separately. At most two types remain. After multiplication by a unit and possibly exchanging them, these are $1,2$ with counts $A,B$ (a single type makes blocks of five). The remaining maximum is + $\min((A+2B)/5,(3A+B)/5)$. Both terms are integers. For the first upper bound give an entry of type one weight one and an entry of type two weight two. Every zero block has total weight at least five. For the second bound use weights three and one, respectively. These are also related by doubling modulo five. If $B\ge2A$, take $A$ blocks $(1,2,2)$ and split the remaining twos into groups of five. If $B\le2A$, start with $(A+2B)/5$ blocks of weight five. Allocate the $B$ twos to the blocks, at most two per block, and use ones to fill each remaining weight. This attains the respective smaller bound. + +For example the charges $(1,1,1,2,4,4,4,3)$ over $\mathbb F_5$ split into four inverse pairs. Greedily taking the first four labels instead leaves two indivisible blocks of four. The resulting six additions exceed the attainable four. + +## Complexity with a variable prime field + +Consider the anchored full-pencil decision problem, with a supplied prime field, one slope row, and a budget $L$. This problem is strongly NP-complete. Membership in NP follows from the partition theorem (or from a word of at most $h-1$ additions and polynomial-time row operations). This statement concerns variable field order. The fixed-alphabet algorithm above has different parameters. + +Use the bounded-integer 3-PARTITION problem. Its $3n$ positive integers $a_i$ satisfy $B/4nB$ of polynomial size. Bertrand's postulate allows a prime at most $2nB$ when $nB>1$. On the strongly NP-hard bounded-integer restriction, trial division across this interval is polynomial. Small trivial inputs can be decided directly. Use $3n$ positive charges $a_i$ and $n$ charges $-B$ in $\mathbb F_p$, plus an additional zero-slope carrier. Set every $u_i=1$, take $b$ to select the carrier, and use those charges as the slope row. The normalized full pencil has exactly the required form. [Garey and Johnson, 1975](https://doi.org/10.1137/0204035) + +Each block has integer sum between $-nB$ and $nB$, so modular zero means integer zero. Every nonempty zero block must include a negative entry. Thus $Z\le n$, with equality precisely when each block uses one $-B$ and positive entries summing to $B$. The strict size conditions require exactly three positives. The price $4n-Z$ is at most $3n$ precisely for yes-instances. Even explicitly listing all $p$ guards takes only polynomial space on this restriction. This transfers a classical debt-clearing obstruction to a priced finite-field header. The classical transaction problem and its hardness have earlier literature. [Pătcaș and Bartha, 2019](https://doi.org/10.2478/ausi-2019-0010) diff --git a/research/settlement-header-word-review/inputs/LICENSE b/research/settlement-header-word-review/inputs/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/settlement-header-word-review/inputs/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/settlement-header-word-review/inputs/NOTICE b/research/settlement-header-word-review/inputs/NOTICE new file mode 100644 index 0000000000..cb8d1d358f --- /dev/null +++ b/research/settlement-header-word-review/inputs/NOTICE @@ -0,0 +1,12 @@ +Monomial guard settlement +New proofs, source and finite evidence prepared by SHIN09-git with +substantial OpenAI Codex assistance. Apache-2.0. + +source/finite.py is the unchanged small-field arithmetic from PR6710; +source/6710-PROOF.md, source/6710-TASK.json and source/6710-NOTICE retain +that package's exact bytes and disclosures. The binary complete-header +extension and all-field pair-sign corollary are due to ToikY. Nick Petalas +authored the predecessor marginal and common-covector pair law. The +determinant identity, elementary row operations and debt-partition idea +have earlier sources; see the proof and SOURCES.json. The different +computational checks in this package share the same assisted authorship. diff --git a/research/settlement-header-word-review/inputs/PROOF.md b/research/settlement-header-word-review/inputs/PROOF.md new file mode 100644 index 0000000000..234bbba481 --- /dev/null +++ b/research/settlement-header-word-review/inputs/PROOF.md @@ -0,0 +1,63 @@ +# Paying to separate the coordinates of a guard family + +Work over a finite field $K$ of order $q$. A nonzero column $u$ and a row $v$ satisfy $vu=1$. Its guard tests all leading principal minors of orders $1$ through $m-1$ of the corank-one complement $G(I-uv)G^{-1}$. The full determinant is always zero. PR6710 treats a complete uniform header $G$ and asks what remains under monomial headers. We count free permutations and nonzero coordinate scalings, and charge one unit for each elementary addition $R_i\gets R_i+aR_j$, $i\ne j$, $a\ne0$. Choices may depend on the known input. This is a finite-field operation metric. Data movement, precision, inverses, selection and restoration in a physical caller are unpriced. [PR #6710](https://github.com/CrocSwap/integer-mult-bounds/pull/6710) + +## What can a permutation alone accomplish? + +The state transforms by $u\mapsto Gu,\ v\mapsto vG^{-1}$. On positions $S$ in a prefix, the principal determinant is $1-\sum_{i\in S}u_iv_i$, by the rank-one determinant identity. A diagonal change cancels in every product $u_i v_i$. Thus a uniform monomial header induces exactly a uniform permutation of the labeled coordinates. For any named subfamily, mark a proper subset $S$ allowed when none of its row sums is one. Set $F(\varnothing)=1$ and compute + +~~~text +F(S) = [S is allowed] sum_{i in S} F(S without i). +~~~ + +The full set is always allowed in this recurrence because its minor is not tested. Each term fixes the last coordinate of an order. The exact joint probability is $F([m])/m!$. An empty named subfamily has probability one. In particular the identities and the coordinate order matter here, even when the complete general-linear orbits agree. + +For example take $m=2,\ u=(1,1)^T,\ v_a=(1-a,a)$ for all $a\in K$. Guards $a=0,1$ pass on opposite orders. Each has marginal $1/2$ and their joint probability is zero. All other directions pass both orders. Conjugate this same family by the matrix with rows $(1,-1),(0,1)$. The new image vector is $(0,1)^T$ and the rows become $(1-a,1)$. Every guard now passes on the very same one of the two orders. The joint probability for the full pencil is $1/2$, above the product $2^{-q}$. This disagreement already occurs over the binary field, despite the positive complete-header theorem. + +## The separation distance + +For the full affine family take $v_\lambda=b+\lambda W$ for all $\lambda\in K^d$, with $bu=1,\ Wu=0$. The $d$ rows of $W$ may be chosen independent. The case $d=1$ is the full pencil. Write $x_i=u_i b_i$ and $y_i=u_i W_{:i}\in K^d$. The slope charges $y_i$ sum to zero and the scalar charges $x_i$ sum to one. At a proper prefix, if its vector slope sum $Y$ is nonzero, the parameter $\lambda$ can make $X+\lambda Y$ equal one. If $Y=0$, every direction passes exactly when $X\ne1$. Therefore all the guards can pass only if every proper slope prefix vanishes. The final slope sum vanishes too, so subtracting successive prefixes forces **every individual $y_i$ to vanish**. Conversely, when all $y_i$ vanish, what remains is precisely the single-row scalar prefix test. This necessity uses the full parameter family. + +Discard initially zero slope charges. Write $h$ for the number left, and $Z$ for the largest number of nonempty disjoint zero-sum blocks partitioning those $h$ labeled charges. Set $Z=0$ for the empty list. The **exact minimum number of paid row additions making all slope charges zero** is + +~~~text +distance to separation = h - Z . +~~~ + +The proof works for vectors in arbitrary dimension. Under $R_i\gets R_i+aR_j$, the column component $u_i$ increases by $a u_j$ and column $W_{:j}$ decreases by $aW_{:i}$. Consequently the only charge changes are +$y_i\gets y_i+a u_j W_{:i}$ and $y_j\gets y_j-a u_j W_{:i}$. A monomial conjugates an elementary addition into another such addition, with relabeled indices and a nonzero scalar. Thus free operations may all be moved to the end, where they only permute the charges. + +For any successful word, connect the two labels involved in each paid addition. The initial charge sum on each connected component is conserved and must be zero. The components containing initially nonzero charges partition those charges into at most $Z$ blocks. A component containing $k$ active labels needs at least $k-1$ edges, including when initially zero labels are used as helpers. Repeated edges are still charged operations. Summing yields the lower bound $h-Z$. + +For the reverse bound, choose a maximizing partition. In each block keep one initially active coordinate $j$ and visit the other labels $i$ in any order. Add row $j$ to row $i$ with coefficient $-u_i/u_j$. This sets $u_i$ to zero and transfers its whole charge to $j$ in the dual rows. The accumulator's $u_j$ never changes. Its final charge is the block sum, zero. Each block of size $k$ costs $k-1$. These legal elementary matrices supply the missing realization step in transferring the classical zero-sum partition idea to constrained row operations. [Csaba Pătcaș, *The debts’ clearing problem: a new approach*](https://acta.sapientia.ro/content/docs/the-debts-clearing-problem-a-new-approac.pdf) + +## When the separation price is the full guard price + +Call a scalar carrier **anchored** if $b$ is supported at a single coordinate $c$, $u_c b_c=1$ and $W_{:c}=0$. The construction above never touches $c$ since $y_c=0$. It preserves $b$, and a free permutation puts $c$ last. Every proper scalar prefix is then zero. Thus for an anchored full flat, $h-Z$ is also the exact minimum price of a header passing **all the original minors**. A full guard requires separation regardless of whether the carrier is anchored. + +For instance over $K=\mathbb F_5$ take $u=(1,1,1,1,1)^T,\ b=(0,0,0,0,1)$ and a single slope. For $(1,4,2,3,0)$ two opposite pairs settle in two additions. For $(1,1,1,2,0)$ only the whole active block sums to zero, so three additions are necessary and sufficient. Both lists have four active labels, yet their optimal costs differ. WITNESSES.json supplies every coefficient and EXAMPLES.json checks all raw states at every smaller cost plus an actual attaining word. + +## Arbitrary binary families + +Now take any nonempty ordered list of normalized rows $V$, possibly repeated or dependent. Set $z_i=u_i V_{:i}$ and $t=(1,\ldots,1)$. In the binary field a proper prefix passes every guard if and only if its sum is **the zero vector**. Thus success after a free permutation means the charges vanish off one coordinate, whose charge is $t$. Write $h$ for the number of nonzero $z_i$, and append a single labeled dummy charge $-t$ to those $h$ charges. If $Z_*$ is the maximum zero-sum block count of this augmented list, then + +~~~text +minimum paid additions passing an arbitrary binary family = h - Z_* . +~~~ + +In a successful word, append the dummy to the component of the final carrier. This component has initial total $t$. All other components have initial total zero. This gives the same edge lower bound. Conversely, settle every block as above, consolidating only the real charges of the dummy's block onto one accumulator. That block contains at least one real charge. Its final value is $t$, and a free permutation puts it last. The dummy is a bookkeeping device and never a row or usable workspace. The same formula computes the distance to a single charge in any field, which suffices for guarding but need not be necessary outside the binary case. + +Even when slope separation is free, the remaining price can grow without bound. Over the binary field choose $2n+1$ coordinates with $u_i=b_i=1$, and a separate zero-$u$ coordinate supporting $W$. Every active charge for the full pencil is the same all-ones vector. After adjoining the dummy there are $2n+2$ identical charges, so $Z_*=n+1$ and the exact full guard price is $n$. All slope charges were already zero. A prior separation test alone cannot price this input. + +## Ternary flats whose slopes are already separated + +Suppose $q=3$ and every $y_i=0$. Write $A$ for the number of scalar charges $+1$ and $B$ for those equal to $-1$. Thus $D=A-B\equiv1\pmod3$ and $n=A+B>0$. In reverse order the guard passes if and only if every nonempty scalar prefix in that reverse order has nonzero sum (the full sum is one). Starting with zero, the first charge must be nonzero. After zeros are removed the prefix states alternate between $+1$ and $-1$, finishing at $+1$. For odd $n$ this requires $D=1$, and for even $n$ it requires $D=-2$. Each allowed case has exactly one sign pattern. It starts with $+1$ for odd $n$ and $-1$ for even $n$, after which the next nonzero step is forced. Conditional on the first coordinate being nonzero, the relative order of the nonzero labels is uniform. The passing probability under a uniform monomial header is therefore + +~~~text +n/[m binom(n,A)] if D is 1 or -2; otherwise 0 . +~~~ + +More strongly, with row additions allowed the exact full guard price here is +$\min(|D-1|,|D+2|)/3$. One paid addition changes at most two scalar charges, preserving their total in the field. Their signed integer sum can change only by zero or by three in absolute value. This gives the lower bound even when the intermediate slope charges are unrestricted. When $D>1$, merge two $+1$ charges into one $-1$ and one zero. The previously separated slopes on those active coordinates remain zero. Each such merge decreases $D$ by three. When $D<-2$, pair two negative charges instead. In either direction there are enough same-sign pairs, and the resulting scalar list has the required ordering. In particular $s$ active coordinates alone do not determine either the probability or the minimum price. + +For arbitrary odd fields with an unanchored carrier we supply an exact order-counting algorithm and a separation lower bound. The anchored and already-separated hypotheses identify the statements that give a full paid distance here. diff --git a/research/settlement-header-word-review/inputs/README.md b/research/settlement-header-word-review/inputs/README.md new file mode 100644 index 0000000000..1ed2b1058a --- /dev/null +++ b/research/settlement-header-word-review/inputs/README.md @@ -0,0 +1,34 @@ +# Paying row additions for a common-image guard header + +Permuting coordinates and scaling them by nonzero elements can change which proper leading minors pass, even for two representatives of the same complete general-linear orbit. Here a mixing operation adds a nonzero multiple of one row to another. This follows the restricted-header question in [PR #6710](https://github.com/CrocSwap/integer-mult-bounds/pull/6710). + +**A five-element example.** Four nonzero coordinate charges must be made zero. With charges `1,4,2,3`, two opposite pairs cost **two** additions. With `1,1,1,2`, only the whole list sums to zero, so **three** are necessary. A separate normalized carrier ensures that both prices give genuinely passing headers. All lower-cost states fail the literal principal-minor tests. [Explicit words and depth counts](EXAMPLES.json) + +| Question | Result | +| --- | --- | +| What can a uniform monomial header do? | A labeled subset recurrence counts the exact joint probability. The same complete orbit can have zero joint probability on one input and one half on another. [Counting proof](PROOF.md) | +| How much does coordinatewise slope separation cost? | For $h$ nonzero charges and at most $Z$ disjoint zero-sum blocks, the optimum is $h-Z$. The graph bound and actual row additions match. It is also the full guard cost for an anchored carrier. [Proof](PROOF.md) · [Witnesses](WITNESSES.json) | +| What if the carrier is arbitrary? | In the binary field, adjoining one dummy charge gives the exact full price for every nonempty normalized list. In the ternary field let $S$ be the separation price and $L$ the isolated scalar price. The full price always lies between $\max(S,L)$ and $2S+L$. Both endpoints are attained for **every** choice of $S,L$ across dimensions. [Sharp envelope](GAP.md) | +| Can the two requirements interact? | Even the sum $S+L$ may underestimate the optimum by an arbitrarily large amount. Five is the first ternary dimension with any strict gap above the larger single bound. [Free-orbit census](ORBITS.md) | +| How hard is the optimization? | A labeled subset algorithm produces a word and its matching partition bound. For fixed alphabet, multiplicity compression is polynomial in the number of coordinates. With variable prime field, even the anchored pencil budget decision is strongly NP-complete. [Algorithms and reduction](ALGORITHM.md) | + +This is an exact arithmetic and operation-count result in a specified header model. Free scalings/permutations and a unit price for every addition are modeling choices. It supplies neither physical caller prices nor a changed bound for integer multiplication. + +## Reproduce + +From the repository root with Python 3.12: + +```sh +python3.12 -B scripts/research_package.py --package research/monomial-guard-settlement +``` + +For just the two displayed examples and the ternary controls, run `python3.12 -I -W error -B example_check.py` inside the package directory. The [validation notes](VALIDATION.md) distinguish literal matrices, raw tuple searches, orbit-weighted coverage and the optional larger census. [Sources](SOURCES.json) pin original bytes and [overlap notes](OVERLAP.json) compare neighboring work. + +## Open next questions + +1. For an unanchored ternary pencil, is the optimal price already determined by the multiset of scalar/slope charge pairs? The free-orbit graph retains additional information at zero image coordinates. Search for two such orbits with equal charges and different prices, or prove a path-lifting argument. +2. What sharp price envelope replaces $2S+L$ in the five-element field? Begin with the cost of arranging already-separated scalar charges. The ternary alternation of the two nonzero residues does not extend directly. + +## Attribution + +Prepared by SHIN09-git with substantial OpenAI Codex assistance. The retained field-arithmetic table and the precursor disclosures are from PR6710. ToikY and Nick Petalas retain credit for their earlier complete-header work. The abstract debt-partition principle and debt-clearing complexity have prior literature. The contribution here is the finite-field guard realization, its sharp paid distances and restricted-header certificates. [NOTICE](NOTICE) diff --git a/research/settlement-header-word-review/inputs/ROOT-NOTICE b/research/settlement-header-word-review/inputs/ROOT-NOTICE new file mode 100644 index 0000000000..59d8e0cf31 --- /dev/null +++ b/research/settlement-header-word-review/inputs/ROOT-NOTICE @@ -0,0 +1,415 @@ +A sharper exponent for integer multiplication +Copyright 2026 Douglas Colkitt + +This project includes unmodified source files from OpenAI's manuscript +"Integer multiplication below n log n" and its accompanying repository: +https://github.com/openai/math +Commit: adc7f1241b42e322a6451854ab7e4b4c146bf78a + +The original manuscript identifies OpenAI as its author. Its Apache-2.0 +license is retained at upstream/LICENSE. The exact source URLs and hashes +are recorded in upstream/manifest.json. Proposed modifications are supplied +as separate files under patches/; upstream source files remain unchanged. + +The original local research note, scripts, certificates, patches, and +documentation were prepared by Douglas Colkitt with assistance from OpenAI +Codex. The community release incorporates work by the contributors identified +in the notices below; it is not solely Douglas Colkitt's work. +This project is not an official OpenAI release or an OpenAI endorsement. + +Related contributions (not imported in this checkpoint): +Zhihao Chen (jacklightChen), PR #7, supplied an earlier ternary five-subset +motif, finite-alphabet transfer and a different compressed producer: +https://github.com/CrocSwap/integer-mult-bounds/pull/7 +The present checkpoint claims no priority for that motif. Related compressed +complex-network work was submitted by eumemic in PR #3: +https://github.com/CrocSwap/integer-mult-bounds/pull/3 +The pending contributions and their stronger bounds require their own review; +this notice does not represent adoption or verification of their claims. + +Additional community work, including parallel and superseded submissions, is +acknowledged in CONTRIBUTORS.md, with pinned submission metadata in +docs/research/contribution-snapshot.json. These acknowledgements do not imply +joint authorship of the checkpoint, incorporation of pending code, or verification +of submitted mathematical claims. Original source-specific notices remain in force. + +Community release (accepted by conditional maintainer audit): +The following original contributor notices apply to the imported PR #39 chain. +The preceding non-import statements describe the preserved 2^-30 checkpoint. + +Ternary five-subset construction and common-four-point resynthesis +Copyright 2026 Zhihao Chen (jacklightChen) + +This is Zhihao Chen's first submission of this specific construction to this +repository. Research, proof development, code and verification were prepared +with substantial assistance from GPT-6 Astra (OpenAI Codex), as identified by +the contributor. This is not independent review or an OpenAI endorsement. +Future research building on this contribution should explicitly acknowledge +Zhihao Chen (jacklightChen), cite the accompanying note and pull request, and +retain the preceding contributors' attribution. This notice records research +provenance; the repository's Apache-2.0 license remains unchanged. + +Dependencies retained from eumemic's Claude-assisted PRs #3 and #5: +https://github.com/CrocSwap/integer-mult-bounds/pull/3 +https://github.com/CrocSwap/integer-mult-bounds/pull/5 +PR #5 commit: d3d370c34937503bd3fa63c83d505a05e8e50893 +These include complex_circuit.py, complex_network.py, fast_gaussian.py, +their generators, construction notes and certificates. The Gaussian input +scaling proof is corrected in this derivative; see the modification notice below. +Aligned pairing also appears in Bortlesboat's PR #2. Retained totals and bank +sharing appear in dleen's PR #4 and cheaper retained centers in eumemic's PR #6. +Their results and ideas are credited separately from this new construction. + +Bulk recursion and controlled tensor basis, 8 October 2026 +Copyright 2026 icekylinx + +The new projector batching, controlled simultaneous basis, mixed-width tape +recursions, whole-residual complex recursion, and dependency-path precision +guard in the batched-23 proof package are contributed by icekylinx, developed +with substantial OpenAI GPT-6 Astra assistance. Review corrections and +repository integration were prepared with OpenAI Codex assistance. They build on the retained +PR #7 finite producers and the preceding contributions credited above. +The new package retains the repository's Apache-2.0 license and the original +authors' attribution. It is not an official OpenAI release or endorsement. + +Modification notice, 8 October 2026 (icekylinx): the retained fast Gaussian +proof now bounds shifted approximation error by F=2^ceil(1.14 alpha^2). +The P=34p precision budget and asymptotic exponent are unchanged. New batching +checks are integrated into make verify. Existing attribution and licenses +are retained. + +Partial-swap extension, 8 October 2026 +Copyright 2026 icekylinx + +The partial-swap framing, binary retained-total triple construction, +dependency-preserving positive labels and carrier reuse, unequal (25,23,57) +common basis, improved complex batching, and exact assembly are contributed +by icekylinx with substantial OpenAI GPT-6 Astra and Codex assistance. +This extension directly inherits PR #10, commit +62691e395a0458ce089a1c7b5d89e74291e95e29. The portable producer adapters +modify the retained paired-exclusion and shared-point implementations credited +above. The original licenses, attribution, and Gaussian correction are retained. + +Endpoint-gauge extension, 8 October 2026 +Copyright 2026 icekylinx + +The complementary auxiliary endpoint gauges, (32,30,40) controlled basis, +general nondegenerate binary phase residuals, retained-center complex producer, +updated path guard and exact assembly are contributed by icekylinx with +substantial OpenAI GPT-6 Astra and Codex assistance. This extension inherits +f2ab41aebad47861caf6316282c1793e5513845e and its PR #10 ancestry. New portable +adapters retain the paired-exclusion and shared-point contributions credited +above. Original licenses, notices and the Gaussian correction are retained. + +Structured-basis and semantic-bulk extension, 8 October 2026 +Copyright 2026 icekylinx + +The selected (32,30,36) bit construction, A1/A5 block refinements, fixed +middle-axis I+J profiles with bounded-minor CRT certificates, mixed dyadic +complex centers, complete data-front batching and circuit-specific assembly +are contributed by icekylinx with substantial OpenAI GPT-6 Astra and Codex +assistance. The immediate parent is ed90fd940279c336ebc45968631bdebfb087b505. + +The semantic/bulk compatibility argument, literal scalar charge, product row +stock and parameterization adapt Zhihao Chen (jacklightChen)'s PR #23, +commit 661ebabc1076c9f525d7ce4967c876b203fa9827. Translated complex endpoints +are adopted from the same contributor's PR #21, +commit 5ba6cf0bfb68f2be8d15610e7972207c50254d6a, following eumemic's source-frame +work and the earlier nested-basis contributions. + +Completed-child semantic precision, arbitrary-coordinate routing, phase-cell +Gaussian inversion and bulk tape transfer are credited to the RaD project +(hipotures), commit 45d9b60355872041f9275f77c057514def0d45bc, exposed through +PR #20 at 4f8d6c8272b5ff307a0da51df545ec3cd96a8b6e. Their selected proof +sources retain their separate CC0 license and original NOTICE under +references/semantic-bulk/rad20. The PR #23 source retains its recorded OpenAI +Codex assistance; RaD retains its recorded Codex and GPT-6.1-Sol Ultra +assistance. These are source attributions, not claims about this session's +runtime model. Related contributions by Rohan Arun and Aurel Prosz remain +acknowledged in the imported notices. No exclusive priority or additional +license condition is asserted. + +Copied retained-center extension, 8 October 2026 +Copyright 2026 icekylinx + +The copied retained-center schedule in both orientations, its complex-phase +transfer, the Wm-N+L rank budget, and the selected (25,23)/(28,28) composition +are contributed by icekylinx with substantial OpenAI GPT-6 Astra and Codex +assistance. This extension inherits PR #32 at +0ef3aeb61f55cc0b321ce6a0ef00acee25cefe52 and the preceding PR #10/#18/#24 work. + +The two-stage topology and paid copied-stream endpoint correction are due +to Aurel Prosz (Paureel), c82d09eb4781b68435e3fa3eb6beea72fa900fab, +through Zhihao Chen (jacklightChen)'s PR #29 unequal-axis composition, +9d963275075fa98f1da821e27757b238dafd6b3c. That source also credits Swapnil +Jain's two-stage development at ae405eb474d1486b2d8aef90139869f927f4836a. + +The contiguous corner method, incidence factorization and exact partition +certificates are due to Rohan Arun (PR #31), method commit +02f68f95369c39955c5ffcfddbd75cd83e26b305. The selected (25,23) certificate +specializes Dominik Scholz's parameterization (PR #33), +a499a345c040aa15b68e984a0904eadc485c7a7e. Their source notices and proof +snapshots are preserved in references/copied-centers. Historical OpenAI +Codex, GPT-6 Astra and Anthropic Claude Opus 5.5 assistance is credited to +the respective imported sources. Existing PR #21/#23 and RaD attribution, +licenses and the Gaussian correction remain in force. + +Copied centers with reversed (23,25) data corners, 2026-10-08 +Rohan Arun with substantial OpenAI Codex assistance supplies the composition, +exact dimension23 controls and cost/assembly integration. James Chang's PR34 +supplies the reversed boundary family; icekylinx's PR36 supplies copied retained +centers and the selected complex graph. The balanced assembly remains attributed +to RaD/hipotures and its PR34 specialization. Retain Dominik Scholz PR33, Rohan +Arun PR31, Zhihao Chen PR29/21/23, Paureel/Aurel Prosz, Swapnil Jain, icekylinx, +eumemic, Douglas Colkitt, OpenAI and all earlier notices and hypotheses. +This is not a claim of formal verification, new foundational rank identities, +global optimality or measured runtime speedup. + +Fixed middle basis with copied reversed corners (2026-10-08): +Rohan Arun, with substantial OpenAI Codex assistance. Composition and +simultaneous-basis proof retain icekylinx PR32/36, James Chang PR34, +Dominik Scholz PR35/38, Zhihao Chen, Paureel, Swapnil Jain, RaD/hipotures, +eumemic and all preceding attribution and licenses. See research/copied-fixed-reversed. + +Changed-graph composition with copied centers and fixed bases, 8 October 2026 +Prepared with OpenAI Codex assistance. +The new composition uses icekylinx PR36 copied centers and PR32 fixed-I+J +projectors/profiler, Dominik Scholz PR35 two fixed factors and CRT argument, +Zhihao Chen (jacklightChen) PR29/23 interfaces, Aurel Prosz (Paureel) and +Swapnil Jain's two-stage development, Rohan Arun PR25/31 corner methods, +Dominik Scholz PR33/38 dimension/composition work; James Chang (jamesyc) +PR34 reversed geometry and balanced transfer; Rohan Arun PR37/39/40 +reversed integration, modular data tests and both-fixed baseline; +RaD (hipotures) PR41 changed scalar DAGs, alternating point order and +independent role compiler; RaD balanced routing/bulk interfaces, and all +retained predecessors. +Complete attribution and the conditional proof boundary are recorded in +research/copied-fixed/PROOF.md; imported originals and source pins are retained. +Original Apache-2.0 and CC0 notices remain applicable. + +Community follow-up integration (PRs #49, #45 and #26), 8 October 2026: +Rohan Arun contributes weighted carrier matching and climbed summand/leave-one-out +orders (PRs #44/#47/#49), with Anthropic Claude assistance. The final construction +composes Chafik Boukhalfa's changed-graph checks, exact rational data recovery and +reordered exclusion sums (PRs #43/#46/#48, OpenAI Codex assistance) with RaD / +hipotures's alternating pair order and independent physical role compiler (#41). +All predecessor attribution and conditional proof interfaces remain in force. + +Alejandro Zarzuelo Urdiales contributes Gaussian parity and canonical arithmetic +proofs, finite tensor execution, profile precision accounting and mixed-center +reference checks (#45), with substantial OpenAI Codex assistance. See +research/gaussian-parity-synthesis/PROVENANCE.md for his full attribution. +Ryan S / princezuda contributes historical Lean certificate arithmetic, algebraic +frame/movement/guard lemmas and independent paired-circuit checks (#26). Original +source notices and historical snapshots are preserved. Neither formal package +claims a full formal proof of the multiplication algorithm or a new kappa. + +Joint frame compilation of skip-prefix strips + +The local compiler and exact finite witnesses were prepared by eumemic with +substantial OpenAI Codex assistance. Avi Eisenberg / ikeboy with Anthropic +Claude assistance supplied the unmodified PR #53 skip-prefix producer. +The pinned PR #48 pipeline is Chafik Boukhalfa's contribution, incorporating +Rohan Arun, RaD / hipotures, icekylinx, Dominik Scholz, James Chang, +Zhihao Chen, Aurel Prosz / Paureel, Swapnil Jain, eumemic, Douglas Colkitt, +OpenAI, David Harvey, Joris van der Hoeven and the earlier contributors +credited in the retained sources. See references/frame-compiler/pr48/NOTICE +and references/frame-compiler/pr53/NOTICE for their original attribution. +No authorship or review by those predecessors is claimed for this compiler. + +Joint dual-skip/frame-compiler composition (2026-10-08) +--------------------------------------------------- +Rohan Gupta / gupt1156 with Anthropic Claude assistance: PR55 dual-skip +scalar graph; original LICENSE and NOTICE are retained under +references/frame-compiler/pr55. eumemic with substantial OpenAI Codex +assistance: PR57 joint reversible frame compiler, serialized physical-word +replay and profile reconstruction. Chafik Boukhalfa with OpenAI Codex +assistance: this composition, independent integration and exact certificate. +Avi Eisenberg / ikeboy, Rohan Arun, RaD / hipotures, icekylinx, and all +predecessor authors retain the notices above and in pinned source files. +No original copyright or Apache-2.0 notice is removed. + +Ranked reclamation after the PR58 joint-dual composition (2026-10-08) +---------------------------------------------------------------- +Chafik Boukhalfa with OpenAI Codex assistance: prioritize retired physical +slots by descending current frame rank, retaining slot ID as the tie-breaker; +complete replay, exact profiles, comparison and adversarial controls. +The dedicated joint_dual_reclaim_compiler.py is derived from eumemic's PR57 +compiler. Its original shared compiler remains byte-identical. The PR55 +producer and all preceding attribution remain unchanged. The complete PR58 +comparison certificate and its original source/proof provenance are retained +under references/frame-compiler/pr58. + +Skip-prefix strip producer, 8 October 2026 +By Avi Eisenberg (ikeboy), with Anthropic Claude (Claude Opus 5.5) +assistance. The skip-prefix leave-one-out strip layout in +research/skip-strips/skip_graph.py is new. Everything else reuses Chafik +Boukhalfa's PR #43/#46/#48 research/copied-fixed pipeline, its verification +code, exact data recovery and support-order sorting, together with: +- Rohan Arun's PR #44 weighted carrier matching optimizer; +- RaD (hipotures) PR #41 alternating point order; +- every predecessor credited above. +Complete attribution and the conditional proof boundary are recorded in +research/skip-strips/PROOF.md. Original Apache-2.0 and CC0 notices remain +applicable. + +Local split-pair skip-prefix research continuation (2026-10-08) +Prepared with substantial OpenAI Codex assistance at the user's request. +New contribution: singleton/pair recursive partition refinement, finite summand +order and moment search, and verified composition with inherited paid clones. +Avi Eisenberg/ikeboy with Anthropic Claude assistance: PR53 skip-prefix strips. +Chafik Boukhalfa with OpenAI Codex assistance: PR54 original-envelope clone +specialization and PR43/46/48 checking interfaces. RaD/hipotures: PR51 +whole-chain/source-partition cloning and earlier producer/interfaces. +Rohan Arun: PR44 weighted matching and earlier fixed/reversed work, with all +stated historical AI assistance. All predecessor notices remain applicable. + +Original-envelope whole-chain clones on skip-prefix strips (research/skip-clones): +Chafik Boukhalfa, prepared with OpenAI Codex assistance. The complete-chain +source-partition clone operation is adapted from RaD / hipotures, PR #51, +with original envelopes retained here. The scalar base is Avi Eisenberg's +PR #53 skip-prefix layout, prepared with Anthropic Claude assistance. +All credited PR #43/#46/#48, PR #44 and earlier code/proof notices remain +in force. This extension is provided under the repository's Apache-2.0 terms. + +Community review checkpoint #50–#61, 8 October 2026 +Maintainer integration and independent arithmetic: Douglas Colkitt, with OpenAI Codex. +Avi Eisenberg / ikeboy: skip-prefix strip framework (#53), with Anthropic Claude. +Rohan Gupta / gupt1156: parallel order search (#50, stated Antigravity assistance) +and dual-suffix strips (#55, Anthropic Claude assistance). +Eumemic: equal-frame joint compilation and paid signal reclamation (#57), with Codex. +Chafik Boukhalfa: original-envelope paid clones (#54), composition (#58) and ranked +reclamation (#60), with Codex. Rohan Arun: order search (#52) and positive-frame +composition (#56), with Anthropic Claude and stated Codex validation assistance. +RaD / hipotures: enlarged frames, source partitions and paid whole-chain clones +(#51), with Codex. Rohan Garg / rohangar1: singleton/pair recursion and paid-clone +composition (#59), with Codex. Alejandro Zarzuelo Urdiales: exact parameter +refinement, scoped Lean arithmetic, matrix/parity and search tools (#61), with +his disclosed multi-tool and Codex assistance. +Parallel #50/#52 records are reviewed and credited without replacing the earlier +climbed-48 implementation; their exact commit history is retained. The separate +#51 witness is retained as research; its source-graph/negative-basis data proof +has not received the same full replay as #56's consumed compiler machinery. +See docs/research/community-round2-review.md for precise validation boundaries. +All earlier licenses, contributions and notices remain applicable. + +Interval strips and core-aware pair assembly + +The interval leave-one-out strips and the core-aware group-pair assembly in +research/pair-assembly were prepared by Avi Eisenberg / ikeboy with Anthropic +Claude assistance. They build on PR #53's skip-prefix pipeline and its +inherited PR #48 sources. The stacked witness in research/pair-assembly/frame +uses eumemic's PR #57 joint frame compiler unchanged; its driver and verifier +are adaptations of PR #57's skip_frame_compiler.py, skip_frame_compose.py and +verify_skip_frame.py. Original notices are retained. + +Stopped product-ring extension, 9 October 2026 +Copyright 2026 icekylinx + +The opposite-bank generic projector factorization, componentwise atom-ring +adapters, stopped recurrence and outer ordinary-interchange conversion, +aligned pair-star producer with rational centers, exact denominator-21 +grid and selected (23,23)/(24,24) composition are contributed by icekylinx +with substantial OpenAI GPT-6 Astra and Codex assistance. This extension +builds on merged PR #36, 11817ccacb564bb7f98789c20dc11d3fece207e3, and is +integrated on upstream main 56b66d58297deca1d7dd130247d720e960f77a37. + +The retained ordinary leaf uses the preceding projector, corner and +copied-center proofs. The selected two-stage topology retains Aurel Prosz +(Paureel), Swapnil Jain and Zhihao Chen's credits; the semantic assembly +retains PR #21/#23 and RaD's attribution. Paired producers, carrier matching, +original source notices and each imported license remain unchanged. + +Partial-gauge extension, 9 October 2026 +Copyright 2026 icekylinx + +The pair-first cube assembly, compatible backward frame enlargement, +partial source-gauge schedule and stopped whole-projector composition are +contributed by icekylinx with substantial OpenAI GPT-6 Astra and Codex +assistance, extending PR #104 at 948ce1510df750f4c18b96bdaef436a86f8bf834. + +The physical deferred bit word, reflected event accounting, fan-order +clarification and signed two-stage endpoint are adopted from Zhihao Chen +(jacklightChen), PR #97, e15350b66e4bf796153a68c240a6cc1b788abe3e, with +Codex assistance. Its deferred readouts, V leaves, lifted frames and frozen +witness originate in Swapnil Jain's 741e7aa078392553815df7926ee17ac5e25a8c38, +with the original Claude disclosure retained. Cyclic interval and core-aware +pair primitives build on Avi Eisenberg (ikeboy), PR #62, +ad0f25ff7b23cff7f08ad237c2254e6ecf74257e, with Anthropic Claude assistance. +Prior two-stage, copied-center, ordinary-leaf, semantic/bulk, routing and +precision credits remain in force. Imported source notices and licenses +are preserved under references/partial-gauge/; see SOURCES.json. + +Three-stage cover extension, 9 October 2026 +Copyright 2026 icekylinx + +The arbitrary-subspace Clifford frame theorem, three-stage Cayley geometry, +weighted q-adic GL cover, unit-lower weighted compiler, charged local-ring +fallback, uniform batching, internal row borrowing and exact composition +are contributed by icekylinx with substantial OpenAI GPT-6 Astra assistance. This +repository integration uses Codex assistance and extends +PR #115, cf60442983c153a3a0f5272ea4713f99eba13c86. + +The selected local complex DAG and support/label replay are adopted from +Copyright 2026 eumemic, PR #117, cbb05ce504d571546d9b7794c186a613c659c3bf, +with its original Apache-2.0 terms and Claude assistance disclosure. +The unchanged bit physical word retains Zhihao Chen (jacklightChen), +PR #97, and Swapnil Jain's underlying witness and assistance notices. +The prior opposite-bank, stopped ordinary-leaf, copied-center, topology, +semantic/bulk, precision and analytic credits remain applicable. +Original source notices and license bytes are preserved in +references/three-stage-cover/pr117/ and references/partial-gauge/. + +Paired-cube and shared-core extension, 9 October 2026 +Copyright 2026 icekylinx + +The paired-coordinate triple-cube identity, signed overlap channels, +original-source involution, coordinate-star centers, concrete frame/carrier +compiler, chronological source gauges, PR97 gauge-subset selection, +orthogonal cross-stage routing and exact supplier/assembly integration +are contributed by icekylinx with substantial OpenAI GPT-6 Astra assistance. +Repository integration uses Codex assistance and extends PR #130 at +6a9970a530119174507904e23592fd59ede19a5d. + +The substantial completed-core workspace-sharing principle is credited to +an664, PR #128, 530588a019b4a74f09180680c9e3961bf649ec89, with its reported +OpenAI Codex assistance. No source code, partition or serialized witness +from that PR is imported. The new routing and paired-motif integration +are described separately and claim no exclusive priority for broad sharing, +paired-coordinate, Fourier or carrier-matching ideas. + +Selected coarse queries restrict the retained eumemic PR #117 positive DAG; +its original Apache-2.0 and Claude assistance notices remain unchanged. +The bit word and original frames retain Zhihao Chen's PR #97 and Swapnil +Jain's frozen witness, notices and historical assistance disclosures. +Earlier generalized Clifford, three-stage, uniform weighted recursion, +ordinary-leaf, semantic/bulk, precision and analytic credits remain in force. +Source-specific license bytes are preserved under references/. + +October 9 recycled-bit integration: +DaysSky (#150), William Porter/hpst3r (#147), Thomas Marchand/Th0rgal (#146), +Rohan Gupta/gupt1156 (#148), James Chang/jamesyc (#124), SovereignSteak (#122). +The original notices and assistance disclosures are retained under research/, +including research/recycled-bit-integration/NOTICE. Andrew Barnes/Bortlesboat +(#101) repairs shared verifiers using rfu08's #64 counterexample. rfu08's +scoped finite and formal-transfer packages are included separately; they do +not establish the full multiplication theorem. Earlier and parallel credits +remain applicable. Douglas Colkitt integrated these with OpenAI Codex assistance. + +SovereignSteak PR151 independently supplies the matching gauge/recycling +composition and the selected 473/10^6 atom refinement; its original package +and assistance disclosure are retained under research/gauge-recycling/. + +October 9 coordinated-frame and completed-entrance-bank integration: +Dugongue PR186, 166a34d75e853e933855f0f7e940fe77c4bb6b8d, builds on +Chafik Boukhalfa/chafreaky's PR181, 7fb2194801e3a10f54772c7f0d5505035a4fc0ad, +and eumemic's PR168 v4, 4a3c769e5c5430e7114c4d3e099ff34664677f17. +The frozen package and prerequisite archive preserve all author, source-license +and assistance notices, including PR175's compiler optimization. DaysSky's +carrier closure, James Chang's terminal substitution and balanced assembly, +geckods' stopping refinements and all preceding framework credits remain. +Rohan Arun's PR185 bootstrap and chafreaky's PR182 bit refinement are reviewed +parallel contributions; their gains are not added to the selected witness. +Douglas Colkitt integrated the package and supplied the bank scheduling +supplement with OpenAI Codex assistance, under Apache-2.0. The all-size +interfaces remain conditional; finite verification is not full formalization. diff --git a/research/settlement-header-word-review/inputs/certificates.py.txt b/research/settlement-header-word-review/inputs/certificates.py.txt new file mode 100644 index 0000000000..e753a14ac6 --- /dev/null +++ b/research/settlement-header-word-review/inputs/certificates.py.txt @@ -0,0 +1,142 @@ +"""Zero-block, raw-order and closed-form finite certificates.""" +from collections import Counter +from fractions import Fraction +from functools import lru_cache +from itertools import combinations, combinations_with_replacement +from math import factorial + +from algorithms import frequency_blocks, scalar_small_field +from literal import identity_pass, literal_orders +from monomial import flat_rows, passing_permutations, separated_ternary_probability +from settlement import Field, partition, ternary_extra, witness + + +def need(condition, name): + if not condition: + raise ValueError(name) + + +def block_oracle(f, values): + """List admissible blocks directly; then cover by disjoint zero blocks.""" + values = tuple(values) + zero_masks = [] + for k in range(1,len(values)+1): + for indices in combinations(range(len(values)),k): + total = [0]*len(values[0]) + for i in indices: + total = [f.add[a][b] for a,b in zip(total,values[i])] + if not any(total): + zero_masks.append(sum(1 << i for i in indices)) + @lru_cache(None) + def best(mask): + if not mask: + return 0 + pivot = mask & -mask + return 1+max(best(mask ^ block) for block in zero_masks + if pivot & block and mask & block == block) + return best((1 << len(values))-1) + + +def partitions_report(): + result = [] + for q in (2,3,4,5,7,8,9): + f = Field(q) + cases = 0 + closed = 0 + edges = Counter() + for h in range(1,8): + for items in combinations_with_replacement(range(1,q),h): + total = 0 + for x in items: + total=f.add[total][x] + if total: + continue + values=[(x,) for x in items] + a=partition(f,values) + expected=block_oracle(f,values) + need(len(a)==expected==frequency_blocks(f,values),"labeled/frequency/disjoint partitions") + if q <= 5: + need(expected==scalar_small_field(f,items),"small-field exact block count") + closed+=1 + cases+=1 + edges[h-expected]+=1 + result.append(dict(q=q,scalar_cases=cases,small_field_cases=closed, + optimal_cost_histogram=dict(sorted(edges.items())))) + return result + + +def permutation_reports(): + result=[] + for q in (2,3,4,5,7,8,9): + f=Field(q) + u=(1,1); b=(1,0); w=(f.neg[1],1) + u2=(0,1); b2=(1,1); w2=(f.neg[1],0) + for label,image,base,slope in [("exclusive",u,b,w),("identical",u2,b2,w2)]: + rows=flat_rows(f,base,[slope]) + nums=[] + for mask in range(1 << q): + fixed=[row for i,row in enumerate(rows) if mask & (1 << i)] + a=passing_permutations(f,image,fixed) + # In dimension two the sole determinant is its literal diagonal entry. + literal=sum(all(1 != f.mul[image[j]][v[j]] for v in fixed) for j in range(2)) + need(a==literal,"two-coordinate named order counts") + nums.append(a) + expected=0 if label=="exclusive" else 1 + need(nums[-1]==expected,"monomial orbit contrast") + result.append(dict(q=q,model=label,named_subsets=len(nums), + joint_numerator=nums[-1],single_numerators=[nums[1<0)==(ternary_extra(values)==0) and d%3==1,"ternary zero-cost criterion") + tested+=1 + report.append(dict(m=m,tested=tested)) + return report + + +def constructions(): + f=Field(5) + anchor=[] + for w in [(1,4,2,3,0),(1,1,1,2,0),(1,1,1,2,4,4,4,3,0)]: + p=witness(f,(1,)*len(w),[w]) + anchor.append(dict(field=5,w=w,certificate=p)) + binary=[] + f=Field(2) + for n in range(6): + h=2*n+1 + u=(1,)*h+(0,); b=u; w=(0,)*h+(1,) + pencil=flat_rows(f,b,[w]) + cert=witness(f,u,pencil,target_value=(1,1)) + need(cert["distance"]==n and witness(f,u,[w])["distance"]==0,"binary unbounded gap") + binary.append(dict(n=n,certificate=cert)) + return dict(anchored=anchor,binary=binary) + + +def controls(): + f=Field(5) + need(witness(f,(1,)*5,[(1,4,2,3,0)])["distance"]==2,"cancelling pairs anchor") + need(witness(f,(1,)*5,[(1,1,1,2,0)])["distance"]==3,"indivisible block anchor") + f2=Field(2) + rows=[(1,0),(0,1)] + need(witness(f2,(1,1),rows,target_value=(1,1))["distance"]==1,"binary dummy anchor") + need(passing_permutations(f2,(1,1),rows)==0 and passing_permutations(f2,(0,1),[(1,1),(0,1)])==1, + "monomial order anchor") + vals=(1,1,1,2) + need(frequency_blocks(f,[(x,) for x in vals])==scalar_small_field(f,vals)==1,"small field anchor") + need(ternary_extra((1,1,1,1,0))==1 and separated_ternary_probability((2,2,0))==Fraction(2,3), + "ternary scalar anchor") + need(identity_pass(f2,(0,1),[(1,1)]) and not identity_pass(f2,(1,0),[(1,1)]),"literal minor anchor") diff --git a/research/settlement-header-word-review/inputs/example_check.py.txt b/research/settlement-header-word-review/inputs/example_check.py.txt new file mode 100644 index 0000000000..311863c068 --- /dev/null +++ b/research/settlement-header-word-review/inputs/example_check.py.txt @@ -0,0 +1,66 @@ +"""Reachability and explicit attaining headers for the sharp examples.""" +from pathlib import Path +import json,sys + +HERE = Path(__file__).resolve().parent +sys.path.insert(0,str(HERE)) +from literal import literal_orders +from monomial import flat_rows, passing_permutations +from settlement import Field, add_row, witness +from state_oracle import neighbors + + +def orders(f, state, m): + return literal_orders(f,state[:m],flat_rows(f,state[m:2*m],[state[2*m:]])) + + +def smaller_levels(f, initial, m, distance): + """Every distinct raw state at every smaller shortest distance.""" + level = {initial} + seen = set(level) + records = [] + for step in range(distance): + passing = sum(orders(f,s,m)>0 for s in level) + records.append(dict(cost=step, unique_states=len(level), passing=passing)) + if passing: + raise ValueError("found a cheaper actual passing header") + if step+1 < distance: + new = {p for s in level for p in neighbors(f,s,m,2)} - seen + seen.update(new) + level = new + return records + + +def example(q,u,b,w,gates): + f = Field(q) + levels = smaller_levels(f,u+b+w,len(u),len(gates)) + u1,rows = u,(b,w) + for i,j,a in gates: + u1,rows = add_row(f,u1,rows,i,j,a) + named = flat_rows(f,rows[0],[rows[1]]) + actual = literal_orders(f,u1,named) + if not actual or actual != passing_permutations(f,u1,named): + raise ValueError("word fails actual proper minors") + return dict(q=q,u=u,b=b,w=w,minimum=len(gates),gates=gates,cheaper_levels=levels, + final_u=u1,final_b=rows[0],final_w=rows[1],passing_final_orders=actual) + + +def collect(): + records=[] + for w in ((1,4,2,3,0),(1,1,1,2,0)): + u,b=(1,)*5,(0,0,0,0,1) + proof=witness(Field(5),u,[w]) + records.append(example(5,u,b,w,proof["gates"])) + records.append(example(3,(1,)*6,(0,0,1,1,1,1),(1,2,0,0,0,0), + [(0,1,2),(2,3,2)])) + records.append(example(3,(1,1,1,1,0),(1,1,1,1,0),(0,0,0,0,1),[(0,1,2)])) + records.append(example(3,(1,)*5,(2,2,1,1,1),(1,2,0,0,0),[(0,1,2),(2,3,2)])) + return records + + +if __name__=="__main__": + rows=collect() + if json.loads(json.dumps(rows)) != json.loads((HERE/"EXAMPLES.json").read_text(encoding="utf8")): + raise ValueError("frozen depth search") + print(json.dumps(dict(status="PASS_SETTLEMENT_SHORTEST_EXAMPLES", minima=[r["minimum"] for r in rows], + cheaper_states=sum(t["unique_states"] for r in rows for t in r["cheaper_levels"])))) diff --git a/research/settlement-header-word-review/inputs/literal.py.txt b/research/settlement-header-word-review/inputs/literal.py.txt new file mode 100644 index 0000000000..bef3d242ad --- /dev/null +++ b/research/settlement-header-word-review/inputs/literal.py.txt @@ -0,0 +1,61 @@ +"""Ordinary matrix minors and a brute-force labeled-order oracle.""" +from itertools import combinations, permutations + + +def reduce_matrix(f, square, inverse=False): + n = len(square) + a = [list(row) + ([int(i == j) for j in range(n)] if inverse else []) + for i, row in enumerate(square)] + det = 1 + for j in range(n): + pivot = next((i for i in range(j, n) if a[i][j]), None) + if pivot is None: + return 0, () + if pivot != j: + a[j], a[pivot] = a[pivot], a[j] + det = f.neg[det] + factor = a[j][j] + det = f.mul[det][factor] + a[j] = [f.mul[f.inv[factor]][x] for x in a[j]] + for i in range(n): + if i != j and a[i][j]: + scalar = f.neg[a[i][j]] + a[i] = [f.add[x][f.mul[scalar][y]] for x,y in zip(a[i], a[j])] + inv = tuple(tuple(row[n:]) for row in a) if inverse else () + return det, inv + + +def complement(f, u, row): + return tuple(tuple(f.add[int(i == j)][f.neg[f.mul[x][y]]] for j,y in enumerate(row)) + for i,x in enumerate(u)) + + +def pass_subset(f, matrices, indices): + for matrix in matrices: + minor = [[matrix[i][j] for j in indices] for i in indices] + if reduce_matrix(f, minor)[0] == 0: + return False + return True + + +def identity_pass(f, u, rows): + matrices = [complement(f, u, row) for row in rows] + return all(pass_subset(f, matrices, range(length)) for length in range(1, len(u))) + + +def literal_orders(f, u, rows): + """Build actual principal submatrices; list every full labeled order.""" + m = len(u) + matrices = [complement(f, u, row) for row in rows] + admissible = set() + for length in range(1, m): + for sub in combinations(range(m), length): + if pass_subset(f, matrices, sub): + admissible.add(frozenset(sub)) + return sum(all(frozenset(order[:j]) in admissible for j in range(1, m)) + for order in permutations(range(m))) + + +def product(f, a, b): + columns = list(zip(*b)) + return tuple(tuple(f.dot(row, col) for col in columns) for row in a) diff --git a/research/settlement-header-word-review/inputs/monomial.py.txt b/research/settlement-header-word-review/inputs/monomial.py.txt new file mode 100644 index 0000000000..3b68a6d1a5 --- /dev/null +++ b/research/settlement-header-word-review/inputs/monomial.py.txt @@ -0,0 +1,45 @@ +"""Counts for uniformly permuted coordinate contributions.""" +from fractions import Fraction +from math import comb, factorial + +from settlement import charges, subset_sums + + +def passing_permutations(field, u, rows): + """Count compatible labeled orders of the proper-prefix chain.""" + m = len(u) + if not rows: + return factorial(m) + if any(field.dot(row, u) != 1 for row in rows): + raise ValueError("unnormalized guard") + sums = subset_sums(field, charges(field, u, rows)) + ways = [1] + [0]*((1 << m) - 1) + for mask in range(1, len(ways)): + if mask != len(ways) - 1 and 1 in sums[mask]: + continue + bits = mask + while bits: + bit = bits & -bits + ways[mask] += ways[mask ^ bit] + bits ^= bit + return ways[-1] + + +def flat_rows(field, b, slopes): + rows = [] + for lam in field.vectors(len(slopes)): + row = tuple(b) + for a, w in zip(lam, slopes): + row = field.axpy(row, a, w) + rows.append(row) + return rows + + +def separated_ternary_probability(values): + plus, minus = values.count(1), values.count(2) + n = plus + minus + if (plus - minus) % 3 != 1: + raise ValueError("unnormalized ternary flat") + if plus - minus not in (1, -2): + return Fraction(0) + return Fraction(n, len(values)*comb(n, plus)) diff --git a/research/settlement-header-word-review/inputs/settlement.py.txt b/research/settlement-header-word-review/inputs/settlement.py.txt new file mode 100644 index 0000000000..74df4fb315 --- /dev/null +++ b/research/settlement-header-word-review/inputs/settlement.py.txt @@ -0,0 +1,100 @@ +"""Exact zero-sum block certificates and legal row-addition witnesses.""" +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE/"source")) +from finite import Field # exact arithmetic retained from PR6710 + + +def subset_sums(field, values): + width = len(values[0]) if values else 0 + sums = [(0,)*width] + for v in values: + sums += [tuple(field.add[a][b] for a, b in zip(s, v)) for s in sums] + return sums + + +def partition(field, values): + """Maximum zero boundaries along a permutation and an attaining partition.""" + if not values: + return [] + sums = subset_sums(field, values) + if any(sums[-1]): + raise ValueError("nonzero partition total") + score = [0]*len(sums) + last = [0]*len(sums) + for mask in range(1, len(sums)): + bits = mask + best = -1 + while bits: + bit = bits & -bits + prior = score[mask ^ bit] + if prior > best: + best, last[mask] = prior, bit + bits ^= bit + score[mask] = best + int(not any(sums[mask])) + mask = len(sums) - 1 + end = mask + blocks = [] + while mask: + mask ^= last[mask] + if not any(sums[mask]): + block = end ^ mask + blocks.append([i for i in range(len(values)) if block & (1 << i)]) + end = mask + if len(blocks) != score[-1]: + raise ValueError("partition backtracking") + return blocks + + +def charges(field, u, rows): + return [tuple(field.mul[weight][row[i]] for row in rows) for i, weight in enumerate(u)] + + +def add_row(field, u, rows, target, source, a): + """Left transvection on u and inverse right transvection on every row.""" + if target == source or not a: + raise ValueError("illegal paid row addition") + u = list(u) + u[target] = field.add[u[target]][field.mul[a][u[source]]] + out = [] + for initial in rows: + row = list(initial) + row[source] = field.add[row[source]][field.mul[field.neg[a]][row[target]]] + out.append(tuple(row)) + return tuple(u), tuple(out) + + +def witness(field, u, rows, target_value=None): + """Settle to zero, or consolidate to one location using a dummy charge.""" + active = [(i, z) for i, z in enumerate(charges(field, u, rows)) if any(z)] + values = [z for _, z in active] + dummy = len(active) + if target_value is not None: + if not any(target_value): + raise ValueError("dummy target must be nonzero") + values.append(tuple(field.neg[z] for z in target_value)) + blocks = partition(field, values) + gates = [] + for block in blocks: + real = [active[i][0] for i in block if i < dummy] + root = real[-1] + for i in real[:-1]: + a = field.mul[field.neg[u[i]]][field.inv[u[root]]] + gates.append((i, root, a)) + u, rows = add_row(field, u, rows, i, root, a) + remaining = [v for v in charges(field, u, rows) if any(v)] + expected = [] if target_value is None else [tuple(target_value)] + if remaining != expected or len(gates) != len(active) - len(blocks): + raise ValueError("settlement witness") + indexed = [[active[i][0] if i < dummy else "target" for i in block] for block in blocks] + return dict(active=len(active), blocks=indexed, distance=len(gates), gates=gates) + + +def ternary_extra(values): + """Paid cost to make a separated full flat pass, for F3.""" + imbalance = values.count(1) - values.count(2) + if imbalance % 3 != 1: + raise ValueError("ternary total is not one") + return min(abs(imbalance - 1), abs(imbalance + 2))//3 diff --git a/research/settlement-header-word-review/inputs/source/6710-NOTICE b/research/settlement-header-word-review/inputs/source/6710-NOTICE new file mode 100644 index 0000000000..c799eae7d6 --- /dev/null +++ b/research/settlement-header-word-review/inputs/source/6710-NOTICE @@ -0,0 +1,10 @@ +Common-image guard pencils +New derivations, programs and finite evidence prepared by SHIN09-git with +substantial OpenAI Codex assistance. Licensed under Apache-2.0. + +ToikY authored the PR6701 binary independent-family extension and the PR6703 +all-field pair-sign corollary. Nick Petalas authored the credited predecessor +marginal, pair counting law and binary sign. Prior author-specific disclosures +appear in source/6701-NOTICE, source/6703-NOTICE and the retained proofs. +Exact original heads, Git objects, retained paths and SHA256 hashes appear in +SOURCES.json. The package includes a copy of the upstream Apache-2.0 license. diff --git a/research/settlement-header-word-review/inputs/source/LICENSE b/research/settlement-header-word-review/inputs/source/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/settlement-header-word-review/inputs/source/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/settlement-header-word-review/inputs/source/finite.py.txt b/research/settlement-header-word-review/inputs/source/finite.py.txt new file mode 100644 index 0000000000..b88d32f8ef --- /dev/null +++ b/research/settlement-header-word-review/inputs/source/finite.py.txt @@ -0,0 +1,68 @@ +"""Small explicit finite fields and exact row operations used by finite replays.""" +from itertools import product + + +class Field: + """Polynomial-basis digit encoding; field order and characteristic differ.""" + def __init__(self, q): + extensions = {4: (2, (1, 1)), 8: (2, (1, 1, 0)), 9: (3, (1, 0))} + if q in extensions: + p, modulus = extensions[q] + elif q in (2, 3, 5, 7): + p, modulus = q, (0,) + else: + raise ValueError("unimplemented arithmetic field") + self.q = q + degree = len(modulus) + coeff = [tuple((a // p**i) % p for i in range(degree)) for a in range(q)] + + def encode(values): + return sum((value % p)*p**i for i, value in enumerate(values)) + + def multiply(a, b): + word = [0] * (2*degree - 1) + for i in range(degree): + for j in range(degree): + word[i + j] += coeff[a][i] * coeff[b][j] + for i in range(len(word) - 1, degree - 1, -1): + for j, value in enumerate(modulus): + word[i - degree + j] -= word[i]*value + return encode(word[:degree]) + + self.add = [[encode([x + y for x, y in zip(coeff[a], coeff[b])]) + for b in range(q)] for a in range(q)] + self.mul = [[multiply(a, b) for b in range(q)] for a in range(q)] + self.neg = [self.add[a].index(0) for a in range(q)] + self.inv = [0] + [self.mul[a].index(1) for a in range(1, q)] + + def dot(self, a, b): + value = 0 + for x, y in zip(a, b): + value = self.add[value][self.mul[x][y]] + return value + + def vectors(self, width): + return product(range(self.q), repeat=width) + + def axpy(self, a, x, b): + return tuple(self.add[u][self.mul[x][v]] for u, v in zip(a, b)) + + def basis(self, rows): + """Canonical nonzero RREF rows, valid for the zero-dimensional quotient.""" + a = [list(row) for row in rows if any(row)] + if not a: + return () + i = 0 + for j in range(len(a[0])): + pivot = next((k for k in range(i, len(a)) if a[k][j]), None) + if pivot is None: + continue + a[i], a[pivot] = a[pivot], a[i] + a[i] = [self.mul[self.inv[a[i][j]]][v] for v in a[i]] + for k in range(len(a)): + if k != i and a[k][j]: + a[k] = list(self.axpy(a[k], self.neg[a[k][j]], a[i])) + i += 1 + if i == len(a): + break + return tuple(tuple(row) for row in a[:i]) diff --git a/research/settlement-header-word-review/inputs/verify.py.txt b/research/settlement-header-word-review/inputs/verify.py.txt new file mode 100644 index 0000000000..ddfade70fb --- /dev/null +++ b/research/settlement-header-word-review/inputs/verify.py.txt @@ -0,0 +1,92 @@ +"""Registered source, partition, price and shortest-example replay.""" +import hashlib,json,sys +from pathlib import Path + +HERE=Path(__file__).resolve().parent +sys.path.insert(0,str(HERE)) +from algorithms import frequency_blocks, scalar_small_field +from certificates import (constructions, controls, need, partitions_report, + permutation_reports, ternary_cases) +from example_check import collect as examples +from families import collect as family_certificates, endpoint +from literal import identity_pass, reduce_matrix +from monomial import flat_rows +from named_masks import collect as named_masks +from orbit_oracle import normalize, orbit_weight +from reduction import collect as reduction +from settlement import Field, add_row, partition, ternary_extra + + +def frozen(name, obj): + need(json.loads(json.dumps(obj))==json.loads((HERE/name).read_text(encoding="utf8")), + "frozen certificate: "+name) + + +def sources(): + meta=json.loads((HERE/"SOURCES.json").read_text(encoding="utf8")) + kept=[r for r in meta["files"] if "vendored_as" in r] + for r in kept: + data=(HERE/r["vendored_as"]).read_bytes() + blob=hashlib.sha1(b"blob "+str(len(data)).encode()+b"\0"+data).hexdigest() + need(r["git_blob"]==blob and r["sha256"]==hashlib.sha256(data).hexdigest(), + "retained source bytes") + if "upstream_origin" in r: + origin=r["upstream_origin"] + need(origin["commit"]=="465a0060fbd236a5e202619de4a45a694d44970a" + and origin["git_blob"]==blob and r["pin"]=="head:59457846216d7c5173fbeb4179ca120d0b32c2d3:"+r["path"], + "pending source identity") + need(len(kept)==5,"retained source count") + return len(kept) + + +def smoke(): + controls() + f=Field(5) + u,rows=add_row(f,(2,3),[(1,1)],0,1,1) + need(u==(0,3) and rows==((1,0),),"dual inverse sign") + need(len(partition(f,[(1,),(4,),(2,),(3,)]))==2,"two disjoint blocks") + need(frequency_blocks(f,[(1,),(4,),(2,),(3,)])==2,"frequency boundary") + need(scalar_small_field(f,(1,2,2,2,2,2,2,2))==2,"five-element normal form") + f3=Field(3) + need(normalize(f3,(0,2,1))==(0,1,2) and normalize(f3,(2,2,1))==(1,1,2),"projective types") + need(orbit_weight((0,2),2)==4,"free orbit weight") + need(reduce_matrix(f3,[(0,1),(1,0)])[0]==2,"literal determinant sign") + need(endpoint(1,0,True)["cost"]==2 and endpoint(1,0,False)["cost"]==1,"sharp endpoint anchors") + need(endpoint(1,1,False)["cost"]==1,"shared improvement") + need(ternary_extra((2,2))==0,"negative ternary ordering") + need(flat_rows(f3,(1,0),[(0,1)])==[(1,0),(1,1),(1,2)],"parameter coverage") + examples_on_disk=json.loads((HERE/"EXAMPLES.json").read_text(encoding="utf8")) + need([v["minimum"] for v in examples_on_disk]==[2,3,2,1,2],"small word fixture anchors") + + +def main(): + count=sources() + if sys.argv[1:]==["--controls"]: + smoke() + print(json.dumps(dict(status="PASS_SETTLEMENT_CONTROLS",sources=count))) + return + if sys.argv[1:]: + raise ValueError("unrecognized verification mode") + smoke() + reports=partitions_report() + orders=permutation_reports() + ternary=ternary_cases() + endpoints=family_certificates() + decisions=reduction() + shortest=examples() + masks=named_masks() + for name,value in [("PARTITIONS.json",reports),("ORDERS.json",orders),("TERNARY.json",ternary), + ("WITNESSES.json",constructions()),("PRICE-ENVELOPE.json",endpoints), + ("REDUCTION.json",decisions),("EXAMPLES.json",shortest)]: + frozen(name,value) + frozen("PERMUTATION-MASKS.json",masks) + print(json.dumps(dict(status="PASS_MONOMIAL_GUARD_SETTLEMENT",sources=count, + zero_sums=sum(r["scalar_cases"] for r in reports), + order_subsets=sum(r["named_subsets"] for r in orders), + higher_dim_subsets=sum(r["named_subsets"] for r in masks), + shortest_examples=[r["minimum"] for r in shortest],envelope_cases=len(endpoints), + reduction_cases=sum(r["no"]+r["yes"] for r in decisions)))) + + +if __name__=="__main__": + main()