From f177c4f27e63dfa2e886033bb6a4e2dcd91f40b6 Mon Sep 17 00:00:00 2001 From: CubeJerry <80299683+CubeJerry@users.noreply.github.com> Date: Sat, 7 Nov 2026 15:14:42 +0800 Subject: [PATCH] Prove sharp zero-edge image bound four and universal rank-three bound six Prepared for @CubeJerry with substantial OpenAI assistance. Retains predecessor attribution and scope. No new kappa. --- research/bit-zero-edge-image-bound/LICENSE | 201 +++++++++++ research/bit-zero-edge-image-bound/NOTICE | 15 + .../bit-zero-edge-image-bound/ORIGINS.json | 18 + research/bit-zero-edge-image-bound/PROOF.md | 272 ++++++++++++++ research/bit-zero-edge-image-bound/README.md | 70 ++++ .../bit-zero-edge-image-bound/RESULT.json | 165 +++++++++ research/bit-zero-edge-image-bound/REVIEW.md | 18 + .../bit-zero-edge-image-bound/SOURCES.json | 30 ++ research/bit-zero-edge-image-bound/TASK.json | 70 ++++ .../bit-zero-edge-image-bound/VERIFY.json | 28 ++ .../bit-zero-edge-image-bound/WITNESSES.json | 191 ++++++++++ .../sources/pr6782-PROOF.md | 287 +++++++++++++++ research/bit-zero-edge-image-bound/verify.py | 337 ++++++++++++++++++ 13 files changed, 1702 insertions(+) create mode 100644 research/bit-zero-edge-image-bound/LICENSE create mode 100644 research/bit-zero-edge-image-bound/NOTICE create mode 100644 research/bit-zero-edge-image-bound/ORIGINS.json create mode 100644 research/bit-zero-edge-image-bound/PROOF.md create mode 100644 research/bit-zero-edge-image-bound/README.md create mode 100644 research/bit-zero-edge-image-bound/RESULT.json create mode 100644 research/bit-zero-edge-image-bound/REVIEW.md create mode 100644 research/bit-zero-edge-image-bound/SOURCES.json create mode 100644 research/bit-zero-edge-image-bound/TASK.json create mode 100644 research/bit-zero-edge-image-bound/VERIFY.json create mode 100644 research/bit-zero-edge-image-bound/WITNESSES.json create mode 100644 research/bit-zero-edge-image-bound/sources/pr6782-PROOF.md create mode 100644 research/bit-zero-edge-image-bound/verify.py diff --git a/research/bit-zero-edge-image-bound/LICENSE b/research/bit-zero-edge-image-bound/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/bit-zero-edge-image-bound/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/bit-zero-edge-image-bound/NOTICE b/research/bit-zero-edge-image-bound/NOTICE new file mode 100644 index 0000000000..8c194925cc --- /dev/null +++ b/research/bit-zero-edge-image-bound/NOTICE @@ -0,0 +1,15 @@ +Sharp image bounds for three binary pattern dimensions +Prepared for @CubeJerry with substantial OpenAI assistance. Apache-2.0. + +New work: the intersecting-diagonal-dependency argument, sharp no-edge +joint-image bound four at three pattern dimensions, its even-parity +attaining complete pool, and the resulting sharp universal maximum six. + +Nick Petalas's CrocSwap/integer-mult-bounds#5921 supplies the inherited +fiber/cardinality theorem and originating sharp-image question. +CrocSwap/integer-mult-bounds#6782 supplies the inherited edge-quotient +bound and edge-containing examples. Its exact PROOF.md is retained as +sources/pr6782-PROOF.md with original attribution and Apache-2.0 notice. +ORIGINS.json pins those bytes. No predecessor code is imported. + +Independent human acceptance and proof-assistant verification are unclaimed. diff --git a/research/bit-zero-edge-image-bound/ORIGINS.json b/research/bit-zero-edge-image-bound/ORIGINS.json new file mode 100644 index 0000000000..44fe687dec --- /dev/null +++ b/research/bit-zero-edge-image-bound/ORIGINS.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "files": [ + { + "path": "sources/pr6782-PROOF.md", + "repository": "CrocSwap/integer-mult-bounds", + "pull_request": 6782, + "commit": "685457252b51b9c7932ece363365bdf0b12c9c31", + "upstream_path": "research/bit-three-relation-core/PROOF.md", + "status_at_initial_read": "open", + "git_blob": "5e9b0aa91c5cd7fd552eaf1dfcc51b32c165e859", + "sha256": "1fad3fa92b26bcd290b179ee3b714c3d25017bc63fa2439124e2e10ddb2c374c", + "license": "Apache-2.0", + "credit": "Prepared for @CubeJerry with substantial OpenAI assistance; exact original attribution retained.", + "role": "Inherited edge-quotient proof and disjoint-edge attaining example; exact bytes retained for Git-free provenance review. No predecessor code is imported." + } + ] +} diff --git a/research/bit-zero-edge-image-bound/PROOF.md b/research/bit-zero-edge-image-bound/PROOF.md new file mode 100644 index 0000000000..2a9c238937 --- /dev/null +++ b/research/bit-zero-edge-image-bound/PROOF.md @@ -0,0 +1,272 @@ +# Sharp joint-image bounds for three binary pattern dimensions + +Prepared for **@CubeJerry** with substantial OpenAI assistance. New work is +Apache-2.0. This is a written, all-width linear-algebra proof, accompanied by +finite exact corroboration. **No new κ.** + +## 1. Statement and relation to earlier work + +Work over the binary field F2. For a matrix N, write off(N) for the matrix +obtained by deleting its diagonal. Let P be a linear subspace of the +zero-diagonal W-by-W matrices, and define the **complete noncoordinate pool** + + C(P) = {N = x y^T : y^T x = 1, off(N) in P, off(N) != 0}. + +The condition y^T x=1 makes N a rank-one idempotent. Put + + V(P) = sum_{N in C(P)} im(N), + +and let e(P) be the number of matrix units E_ab, a!=b, contained in P. +Coordinate projectors E_aa are excluded, even though their zero patterns +belong to every P. + +**Theorem 1 (no-edge bound).** If dim P<=3 and e(P)=0, then + + dim V(P) <= 4. + +For dim P=3 the bound is sharp, already at W=5. The transpose statement +also holds: the span of the covectors y has dimension at most four. +Neither statement assumes that the pool acts irreducibly on its joint image. + +**Theorem 2 (sharp universal rank-three bound).** Among all three-dimensional +binary pattern spaces and all widths, the maximum of dim V(P) is exactly six. +More precisely, the following bounds hold: + +| e(P) | Joint-image bound | Source of the bound | +| --- | ---: | --- | +| 0 | 4, sharp | Theorem 1 below | +| 1 | 5 | The edge-quotient argument in #6782 | +| 2 | 5, sharp | #6782, including an irreducible attaining example | +| 3 | 6, sharp | #6782; three disjoint directed edges attain six | + +The new result is the sharp no-edge bound four, replacing the previous +seven-projector upper bound. Combining it with the inherited edge-containing +bounds establishes the sharp universal maximum six. We do not claim the +one-edge bound is sharp, or a new classification of irreducible pools. + +The question originates in Nick Petalas's #5921, +`research/pattern-pool-cardinality/PROOF.md` and its README. That contribution +proved the fiber and cardinality theorem and explicitly left sharp joint-image +dimension as a follow-up. The later #6782, +`research/bit-three-relation-core/PROOF.md`, established the edge-quotient +bound and identified the zero-edge case as outside its sharp classification. +Its exact proof is retained in `sources/pr6782-PROOF.md`; this package's +argument is self-contained and does not import predecessor code. + +## 2. The inherited fiber lemma + +We recall and credit the following lemma to Nick Petalas, #5921. + +**Fiber lemma.** A realized nonzero off-diagonal pattern has exactly one +binary rank-one-idempotent lift, except a matrix unit E_ab. That pattern has +exactly the two lifts + + e_a(e_a+e_b)^T, (e_a+e_b)e_b^T. + +Here is the short proof, to make the mathematical dependencies reviewable. +If distinct projectors N=xy^T and M=uv^T have the same pattern, their sum D +is nonzero and diagonal. Its rank is at most two and its trace is zero, since +both projectors have trace one. Over F2, D therefore has exactly two nonzero +diagonal entries, at a,b. Its image is contained in span(x,u), so this span +equals span(e_a,e_b). Applying the same argument to the transposes puts y,v +in that coordinate plane too. The six rank-one idempotents on F2^2 are + + [[1,0],[0,0]], [[0,0],[0,1]], + [[1,1],[0,0]], [[0,1],[0,1]], + [[0,1],[0,1]]^T, [[1,1],[0,0]]^T. + +Their only repeated nonzero patterns are the two single directed edges. +This also excludes a third lift. In particular, when e(P)=0, different pool +projectors have different nonzero patterns. + +## 3. Intersecting diagonal dependencies + +The key new observation is about image independence; it does **not** require +the covectors to be independent. + +**Lemma 3.** Let N_i=x_i y_i^T, 1<=i<=5, have linearly independent nonzero +image vectors x_1,...,x_5 over F2 and nonzero covectors y_i. Suppose + + D = N_1+N_2+N_3, F = N_1+N_4+N_5 + +are diagonal. Then N_1 is a coordinate projector. + +**Proof.** Take any coordinate j with (y_1)_j=1. The j-th column of D is + + x_1 + (y_2)_j x_2 + (y_3)_j x_3. + +It is nonzero, since x_1,x_2,x_3 are independent. As D is diagonal, this +column must equal e_j. The same reasoning for F puts e_j in both +span(x_1,x_2,x_3) and span(x_1,x_4,x_5). Independence of all five image +vectors makes the intersection exactly span(x_1). Consequently x_1=e_j. +Every coordinate in the support of y_1 must satisfy this same equality, +so y_1=e_j too. Hence N_1=E_jj. This proof does not need the idempotence +hypothesis separately. ∎ + +The independence assumption is essential. In the sharp construction in +Section 5, five projectors can have both displayed diagonal sums while +their common projector is noncoordinate; their image rank is four. The +verifier retains this as a failure control. + +**Lemma 4 (five points in the binary three-space).** Any five distinct +nonzero vectors of F2^3 contain two three-element zero-sum subsets meeting +in exactly one element. + +**Proof.** Let a,b be the two omitted nonzero vectors and put p=a+b. The +vector p is present. Addition by p partitions the other six nonzero +vectors into three pairs. One pair is {a,b}; the two remaining pairs are +present, and each, together with p, is a zero-sum triple. These triples +meet exactly at p. ∎ + +There are 21 five-element subsets; the verifier checks every one. The +four-point set {001,010,100,111} has no zero-sum triple, so this particular +argument does not reduce the upper bound from four to three. + +## 4. Proof of the no-edge theorem + +Assume for contradiction dim V(P)>=5. Choose five pool projectors with +independent images. By the fiber lemma their patterns are five distinct +nonzero elements of P. Their existence forces dim P=3, since a space of +dimension at most two has at most three nonzero elements. + +Lemma 4 supplies two zero-sum pattern triples with exactly one common +pattern. Uniqueness of each lift makes the triples share exactly one +projector. Relabeling the five projectors gives the two triples in +Lemma 3. A zero sum of patterns means that each corresponding sum of +projectors is diagonal. Lemma 3 then makes their shared projector +coordinate, contradicting its membership in C(P). Thus dim V(P)<=4. + +Apply the same result to P^T to obtain the covector-span bound. This is an +all-width argument; no finite census is used to establish its quantifiers. + +## 5. A complete no-edge pool attaining four + +Use coordinates 0,1,2,3,4. Let U be the even-parity subspace on coordinates +1 through 4, viewed as a subspace of F2^5 with coordinate 0 equal to zero. +It has dimension three and no weight-one vector. Set + + P = {u e_0^T : u in U}. + +This is a three-dimensional zero-diagonal pattern space with no matrix +unit. For each nonzero u in U, the matrix + + N_u = (e_0+u)e_0^T + +is a rank-one idempotent with pattern u e_0^T. All seven nonzero patterns +are realized, and each has a unique lift by the fiber lemma. Thus these +seven projectors are the **complete** pool. + +Their images lie in span(e_0) direct-sum U. For distinct nonzero u,v in U, +the three vectors e_0+u, e_0+v and e_0+u+v sum to e_0. Therefore e_0 is +in V(P), and then every u is too. Hence + + V(P) = span(e_0) direct-sum U, dim V(P)=4. + +For literal reproduction, use bit i for coordinate i. A basis of U has +masks 6,10,18, and its nonzero masks are 6,10,12,18,20,24,30. The seven +projector factors (x,y) are (1+u,1). This example is reducible: U is its +common kernel. Sharpness here is for **total joint image**, not irreducible +core dimension. + +## 6. The inherited edge-quotient argument and the universal maximum + +For clarity we give the argument from #6782 in full and claim no novelty +for it. Let e=e(P), let P_0 be the span of all e matrix units in P, and +let E be the coordinate span of their endpoints. Distinct matrix units +are independent, so dim P_0=e and e<=dim P. Both lifts of every edge +belong to the complete pool, and their images span its two endpoints. +Consequently E is contained in V(P). + +A noncoordinate rank-one idempotent whose pattern is supported in the +E-by-E block has image in E. Indeed, an outside coordinate i with x_i=1 +would force y=e_i from its off-diagonal row. The outside column i then +forces x=e_i, contradicting noncoordinate status. In particular, the +zero coset P_0 contributes no joint-image dimension modulo E. + +Fix a nonzero coset of P/P_0 and two projectors N=xy^T and M=uv^T whose +patterns belong to it. Their off-diagonal difference is supported in +E-by-E. Suppose x and u have independent images modulo E. Their outside +rows and inside columns give + + (x mod E)(y|E)^T = (u mod E)(v|E)^T, + +forcing y|E=v|E=0. Both inside blocks then vanish, so the full patterns +of N and M agree. They are distinct projectors, and the fiber lemma +makes this common pattern a single edge. Its two lifts have covectors +vanishing on E only if both edge endpoints lie outside E. This +contradicts the definition of E using **all** edges in P. + +Thus the image classes in each nonzero coset are pairwise dependent; +over F2 their span has dimension at most one. Therefore + + dim V(P) <= dim E + 2^(dim P-e) - 1 + <= 2e + 2^(dim P-e) - 1. + +For dim P=3 and e=1,2,3 this gives respectively 5,5,6. For e=0 use the +new upper bound four instead of seven. All cases have joint image at +most six. + +The old attaining example consists of three disjoint directed edges: + + P = span(E_01,E_23,E_45) in M_6(F2). + +Their six lifts have factor masks + + (1,3), (3,2), (4,12), (12,8), (16,48), (48,32). + +They span all six coordinate directions. A sum of two or more disjoint +edges is not realizable: the two required entries force a forbidden +cross entry in a rank-one matrix. Hence the displayed pool is complete. +This proves the sharp universal maximum six, with attainment credited +to #6782. + +## 7. Relevance, scope and remaining obligations + +The all-width reduction cuts the largest previously unclassified +three-dimensional no-edge joint image from seven to four. This is a +structural restriction on the binary scalar pool. In the relation-based +word framework of #6777 and #6782 it can be used after their hypotheses +have legitimately reduced the occurring pattern span to at most three +and dealt with coordinate calls. We do not reprove those word-reduction +hypotheses or assert that an arbitrary three-relation word satisfies +the required split. + +V(P) is invariant under every projector in C(P), since the image of +every such projector lies in V(P). The quotient action is zero for the +projectors and identity for factors I+(z^A-1)N. This elementary fact does +not license free physical basis changes, discard coordinate calls, or +prove a paid/target rank inequality. Coordinate projectors have zero +pattern and can enlarge the joint image without bound; excluding them +is essential. Four-dimensional pattern spaces also fall outside the +theorem: the same parity construction in width six has joint image +five, and is a retained scope control. + +This package proves no rational-address realization, native primitive, +dirty-input compiler, recursive invoice, supplier admission, full +multiplication improvement, formal proof-kernel result, or human +acceptance. The selected frontier is unchanged. + +## Open next questions + +1. **Irreducible no-edge bound.** Can a complete three-dimensional no-edge + pool act irreducibly on a four-dimensional joint image, or is the + irreducible bound three? The sharp example above is reducible, so it + does not decide this. Start by classifying four independent image + projectors and their remaining patterns. A new all-width argument or + explicit example is required; a failed finite search would not settle it. +2. **Word consequences after a valid split.** Does the reduced at-most-four + scalar alphabet satisfy the required three-relation paid-rank + obstruction, or admit a rank-saving word? First state and check the + exact relation/cube-span and coordinate-call hypotheses from #6777 + and #6782, then derive the full endpoint and paid-rank accounting. + This pool theorem alone supplies neither conclusion. + +## Source and attribution record + +Scientific base: `7c49fe32c55de02c2c873655c804b16e4c3fef0a`. +Retained #6782 proof: head `685457252b51b9c7932ece363365bdf0b12c9c31`, +with exact content hashes in `ORIGINS.json`. Credit Nick Petalas for +#5921's fiber/cardinality theorem; @CubeJerry and the credited researchers +in #6782 for its edge-quotient bound and attaining edge examples. The +relation-word context is inherited from #6777 and the sources it credits; +it is context, not a proof dependency of Theorems 1 or 2. diff --git a/research/bit-zero-edge-image-bound/README.md b/research/bit-zero-edge-image-bound/README.md new file mode 100644 index 0000000000..89b4cc00d5 --- /dev/null +++ b/research/bit-zero-edge-image-bound/README.md @@ -0,0 +1,70 @@ +# Sharp image bounds for three binary pattern dimensions + +**A complete noncoordinate binary projector pool in a three-dimensional pattern space containing no single-edge pattern has joint-image dimension at most four, and four is attained.** This replaces the previous upper bound seven for the missing zero-edge case. Combined with the credited edge-quotient theorem of #6782, it establishes that the exact maximum total joint-image dimension among **all** three-dimensional pattern spaces is six. **No new κ.** + +Claim type: written all-width mathematical proof with finite exact corroboration. [PROOF.md](PROOF.md) includes all inherited lemmas needed for the corollary. Independent algebraic review is recorded in [REVIEW.md](REVIEW.md); it is not formal proof-kernel verification or independent human acceptance. + +## What is new + +Nick Petalas's #5921, `research/pattern-pool-cardinality`, gave a sharp pool cardinality theorem and left sharp joint-image dimension as an explicit question. #6782, `research/bit-three-relation-core`, subsequently proved the edge-quotient bound and treated the edge-containing rank-three cases; its zero-edge upper bound was seven. This package settles precisely that remaining total-image case. + +Among any five distinct nonzero patterns in a binary three-space, there are two zero-sum triples meeting once. If their five image vectors were independent, the corresponding diagonal matrix sums would force the common projector to be coordinate, contradicting the pool definition. An even-parity construction gives a complete seven-projector pool whose images span four dimensions. This sharp example is reducible; it does not settle the irreducible no-edge maximum. + +The universal maximum six combines the new result with #6782's existing edge-quotient argument and disjoint-edge example. Their predecessor credit is retained. + +## Reproduce + +From the repository root, using CPython 3.12: + +```sh +python3.12 -B scripts/research_package.py --package research/bit-zero-edge-image-bound +``` + +Expected: two `PASS_ZERO_EDGE_IMAGE_BOUND` reports followed by `PASS_REGISTERED_RESEARCH_PACKAGE research/bit-zero-edge-image-bound outcome=completed`. The manifest runs identical coverage normally and with `-O`; validation uses explicit exceptions, not Python assertions. There are no third-party dependencies or external runtime inputs. + +For a package-only replay without Git or network: + +```sh +python3.12 -I -B research/bit-zero-edge-image-bound/verify.py +``` + +[RESULT.json](RESULT.json) is the generated deterministic report. The optional `--json-output /path/outside/the/package.json` writes a fresh report after every check passes. `--integrity-only` checks retained-source bytes only and is explicitly not a mathematical replay. + +## Verification coverage and failure controls + +The verifier imports no predecessor implementation. It checks all 21 five-point subsets of F2^3, all binary rank-one-idempotent fibers at widths one through seven, and complete pools for four witnesses: + +| Witness | Pattern dimension | Edge count | Pool size | Joint-image dimension | +| --- | ---: | ---: | ---: | ---: | +| New sharp parity-code pool | 3 | 0 | 7 | 4 | +| Inherited three disjoint edges | 3 | 3 | 6 | 6 | +| Inherited two-edge scope control | 3 | 2 | 5 | 5 | +| Rank-four parity-code scope control | 4 | 0 | 15 | 5 | + +The finite census enumerates every space generated by three independent **realized nonedge patterns** at each width, deduplicates spaces, then discards those containing an edge. It does not enumerate every three-space in the full off-diagonal ambient vector space. + +| Width | Distinct generated spaces | Zero-edge spaces checked | Largest joint image | +| --- | ---: | ---: | ---: | +| 3 | 202 | 112 | 3 | +| 4 | 104,657 | 98,997 | 4 | + +This domain contains every possible counterexample at these widths: if the realized patterns span at most two dimensions, fiber uniqueness bounds the pool size by three. Finite coverage is corroboration; the all-width result rests on the proof. Enumeration is deterministic, has no random seed, and stops only after its stated domain is exhausted. + +Nine controls reject: a false cap three; an omitted complete-pool member; a nonidempotent factor; an admitted coordinate projector; the two-edge example used outside the no-edge hypothesis; the rank-four example used outside the dimension hypothesis; dependent images in the intersection lemma; nondiagonal dependency sums; and actual retained-source byte corruption in a temporary copy. The dependent-image control really has both diagonal sums and a shared noncoordinate projector, demonstrating why independence matters. + +## Sources and scope + +Scientific base: `7c49fe32c55de02c2c873655c804b16e4c3fef0a`. [SOURCES.json](SOURCES.json) pins the originating catalogue, selected record and #5921 proof/question source as historical provenance. [ORIGINS.json](ORIGINS.json) pins the exact retained #6782 proof at `685457252b51b9c7932ece363365bdf0b12c9c31`, including Git-blob and SHA256 hashes. Retaining these bytes avoids a dependency on pending branch history for cold replay. + +The lead assigned the precise zero-edge question after a bounded archive and overlap review; incomplete coverage is not a proof of novelty. [TASK.json](TASK.json) records the changed scope from the register-model catalogue card. + +The theorem assumes F2, rank-one idempotents, nonzero patterns, at most three pattern dimensions and no matrix units. Coordinate projectors can enlarge the image without bound. Applying the scalar reduction to words requires the exact relation and coordinate-call hypotheses of the relevant predecessor framework. Rational addresses, native implementation, restoration, full recursive accounting and κ improvement remain unproved. The selected construction and frontier are unchanged. + +## Open next questions + +- Can a complete no-edge pool be irreducible on a four-dimensional joint image? Start by classifying four independent image projectors and the remaining patterns. A universal argument or an explicit example is needed; the reducible sharp example here does not decide it. +- After a valid relation/cube-span and coordinate-call split, what paid-rank statement holds for the at-most-four-dimensional no-edge alphabet? First verify those inherited hypotheses, then derive the full endpoint and paid/target invoice. The scalar dimension bound supplies neither a saving nor a general word obstruction. + +## Credit + +Prepared for **@CubeJerry** with substantial OpenAI assistance in research, proof drafting, implementation and adversarial review. New work is Apache-2.0. Credit **Nick Petalas** and #5921 for the fiber/cardinality theorem and sharp-image question; credit **@CubeJerry** and the researchers credited in #6782 for its edge-quotient bound, two-edge example and disjoint-edge attainment. #6777 and its cited lineage supply relation-word context; their entire scientific suites were not replayed here. diff --git a/research/bit-zero-edge-image-bound/RESULT.json b/research/bit-zero-edge-image-bound/RESULT.json new file mode 100644 index 0000000000..6450597597 --- /dev/null +++ b/research/bit-zero-edge-image-bound/RESULT.json @@ -0,0 +1,165 @@ +{ + "all_width_proof": "PROOF.md; not established by finite replay", + "census": { + "3": { + "generated_spaces": 202, + "image_dimension/pool_size": { + "1/4": 1, + "2/3": 53, + "3/3": 48, + "3/4": 7, + "3/5": 3 + }, + "zero_edge_spaces": 112 + }, + "4": { + "generated_spaces": 104657, + "image_dimension/pool_size": { + "1/4": 52, + "2/3": 18012, + "2/4": 1450, + "2/5": 100, + "3/3": 72676, + "3/4": 5468, + "3/5": 168, + "4/4": 987, + "4/5": 84 + }, + "zero_edge_spaces": 98997 + } + }, + "claim": "finite corroboration of written all-width no-edge image bound four; universal rank-three bound six", + "fano": { + "five_point_subsets": 21, + "four_point_cap": [ + 1, + 2, + 4, + 7 + ] + }, + "fibers": [ + { + "edge_patterns": 0, + "idempotents": 1, + "realized_nonzero_patterns": 0, + "width": 1 + }, + { + "edge_patterns": 2, + "idempotents": 6, + "realized_nonzero_patterns": 2, + "width": 2 + }, + { + "edge_patterns": 6, + "idempotents": 28, + "realized_nonzero_patterns": 19, + "width": 3 + }, + { + "edge_patterns": 12, + "idempotents": 120, + "realized_nonzero_patterns": 104, + "width": 4 + }, + { + "edge_patterns": 20, + "idempotents": 496, + "realized_nonzero_patterns": 471, + "width": 5 + }, + { + "edge_patterns": 30, + "idempotents": 2016, + "realized_nonzero_patterns": 1980, + "width": 6 + }, + { + "edge_patterns": 42, + "idempotents": 8128, + "realized_nonzero_patterns": 8079, + "width": 7 + } + ], + "negative_controls": [ + { + "control": "false no-edge cap three", + "rejection": "claimed joint-image bound" + }, + { + "control": "incomplete seven-projector pool", + "rejection": "pool is complete" + }, + { + "control": "nonidempotent factor mutation", + "rejection": "projector is idempotent" + }, + { + "control": "coordinate-call admission", + "rejection": "projector is noncoordinate" + }, + { + "control": "two-edge dimension-five scope witness", + "rejection": "no-edge theorem excludes matrix units" + }, + { + "control": "rank-four parity-code scope witness", + "rejection": "no-edge theorem pattern dimension at most three" + }, + { + "control": "dependent images invalidate intersection lemma", + "rejection": "dependency images are independent" + }, + { + "control": "nondiagonal sums invalidate intersection lemma", + "rejection": "dependency sum is diagonal" + }, + { + "control": "retained-source byte corruption", + "rejection": "source SHA256 mismatch" + } + ], + "new_kappa": false, + "sources": [ + { + "bytes": 15385, + "path": "sources/pr6782-PROOF.md", + "sha256": "1fad3fa92b26bcd290b179ee3b714c3d25017bc63fa2439124e2e10ddb2c374c" + } + ], + "witnesses": { + "rank_four_scope_control": { + "covector_dimension": 1, + "edge_count": 0, + "joint_image_dimension": 5, + "pattern_dimension": 4, + "pool_size": 15, + "width": 6 + }, + "three_edge_sharp": { + "covector_dimension": 6, + "edge_count": 3, + "joint_image_dimension": 6, + "pattern_dimension": 3, + "pool_size": 6, + "width": 6 + }, + "two_edge_scope_control": { + "covector_dimension": 5, + "edge_count": 2, + "joint_image_dimension": 5, + "pattern_dimension": 3, + "pool_size": 5, + "width": 5 + }, + "zero_edge_sharp": { + "covector_dimension": 1, + "edge_count": 0, + "joint_image_dimension": 4, + "pattern_dimension": 3, + "pool_size": 7, + "width": 5 + } + } +} diff --git a/research/bit-zero-edge-image-bound/REVIEW.md b/research/bit-zero-edge-image-bound/REVIEW.md new file mode 100644 index 0000000000..c8bc557cee --- /dev/null +++ b/research/bit-zero-edge-image-bound/REVIEW.md @@ -0,0 +1,18 @@ +# Independent algebraic review + +Reviewer: lead research orchestrator, a separate OpenAI agent from the +proof author, acting for @CubeJerry. Review date: 2026-11-07 UTC. + +The reviewer independently read the entire PROOF.md and checked the +intersecting diagonal triples, the parity-code sharp example, and the +reproduced edge-quotient argument. The reviewer found the all-width bound +proof sound, including the fact that covector independence is unnecessary. + +This was an algebraic review of the actual proof, not merely a rerun of +the author's finite checker. The reviewer required the stated distinction +between total joint-image sharpness and irreducibility, and retention of +the word-reduction and coordinate-call hypotheses. Those limitations are +explicit in the proof and README. + +This is AI-assisted independent review within one coordinated session. +It is not independent human acceptance or formal proof-kernel verification. diff --git a/research/bit-zero-edge-image-bound/SOURCES.json b/research/bit-zero-edge-image-bound/SOURCES.json new file mode 100644 index 0000000000..b7b6beb77f --- /dev/null +++ b/research/bit-zero-edge-image-bound/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/pattern-pool-cardinality/PROOF.md", + "usage": "provenance", + "git_blob": "4fce5d3b6a9c810cfd4d298b209dbd51cefa173c", + "sha256": "47ebe562180c7276bbf0636e9ba3aa1a84f8962ff8b60b3b2fb30cee4514e989" + }, + { + "path": "research/pattern-pool-cardinality/README.md", + "usage": "provenance", + "git_blob": "ae404ea1d8a65f3c48b9817e7664c17abc4bf736", + "sha256": "f677bf62dc68c67c267a60c625e4555e428b9fc290fda4033cd9eb0cb06ae3b0" + } + ] +} diff --git a/research/bit-zero-edge-image-bound/TASK.json b/research/bit-zero-edge-image-bound/TASK.json new file mode 100644 index 0000000000..a75d560f05 --- /dev/null +++ b/research/bit-zero-edge-image-bound/TASK.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "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": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Prove a sharp all-width joint-image bound for complete binary noncoordinate rank-one-idempotent pools in three-dimensional zero-edge pattern spaces; combine with credited edge-quotient bounds.", + "scope_change_reason": "The lead assigned the exact unresolved zero-edge case from #5921 and #6782 after canonical landscape and overlap review. This is structural alphabet reduction before a word search, not another expansion of an already-excluded three-register word family.", + "bottleneck_link": "Three relation dimensions can lead to three-dimensional binary pattern spaces under the exact inherited word hypotheses. The new sharp bound reduces the missing zero-edge joint-image case from seven to four and closes the universal rank-three total-image maximum at six; it does not establish paid-rank savings or supplier admission.", + "budget_minutes": 80, + "stop_rule": "Stop once an all-width proof and attaining complete pool are obtained and independently reviewed, or after the assigned research cutoff. Finite corroboration exhausts widths 3 and 4 spaces generated by realized nonedge patterns, all five-point subsets of F2^3, and literal witness completions up to width 6; no stochastic search or time-based early truncation.", + "outcome": "completed", + "evidence": "PROOF.md proves the sharp no-edge bound four and universal rank-three bound six. verify.py checks exact fibers at widths 1..7, all 21 Fano five-point sets, four complete fixtures, a defined finite census and nine negative controls. RESULT.json records the replay.", + "author": "@CubeJerry", + "ai_assistance": "Substantial OpenAI assistance for research, proof drafting, exact verification code, and adversarial review. No independent human or formal proof-kernel acceptance claimed.", + "open_questions": [ + { + "question": "Can an irreducible complete three-dimensional no-edge pool have joint-image dimension four?", + "why_it_matters": "The sharp total-image example has a common kernel; a smaller irreducible bound could further reduce the word alphabet.", + "first_step": "Classify four independent image projectors and the possible remaining patterns using the intersecting-dependency constraint.", + "blocked_by": "No all-width classification or attaining irreducible example is established here; finite absence is not impossibility." + }, + { + "question": "What paid-rank statement holds for valid three-relation words whose reduced no-edge scalar pool has at most four active dimensions?", + "why_it_matters": "A scalar dimension reduction changes the search domain but does not itself change the BIT supplier or overall kappa.", + "first_step": "Verify the exact cube-span and coordinate-call split hypotheses from #6777/#6782, then derive complete endpoint and paid/target accounting for the restricted word.", + "blocked_by": "Coordinate calls, rational-address realization, native conversion and a complete paid-rank proof remain outside this package." + } + ] +} diff --git a/research/bit-zero-edge-image-bound/VERIFY.json b/research/bit-zero-edge-image-bound/VERIFY.json new file mode 100644 index 0000000000..9caf259c4f --- /dev/null +++ b/research/bit-zero-edge-image-bound/VERIFY.json @@ -0,0 +1,28 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact fibers; all 21 Fano five-point sets; complete sharp and scope fixtures; deterministic width-3/4 census; nine mathematical and source-corruption controls." + }, + { + "argv": [ + "{python}", + "-B", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The identical proof-relevant coverage and negative controls with Python assertions disabled." + } + ] +} diff --git a/research/bit-zero-edge-image-bound/WITNESSES.json b/research/bit-zero-edge-image-bound/WITNESSES.json new file mode 100644 index 0000000000..ff7c04974b --- /dev/null +++ b/research/bit-zero-edge-image-bound/WITNESSES.json @@ -0,0 +1,191 @@ +{ + "schema_version": 1, + "encoding": "Vector bit i denotes coordinate i; matrix bit W*i+j denotes row i, column j.", + "cases": { + "zero_edge_sharp": { + "width": 5, + "pattern_dimension": 3, + "pattern_basis": [ + 1056, + 32800, + 1048608 + ], + "pool": [ + [ + 7, + 1 + ], + [ + 11, + 1 + ], + [ + 13, + 1 + ], + [ + 19, + 1 + ], + [ + 21, + 1 + ], + [ + 25, + 1 + ], + [ + 31, + 1 + ] + ], + "edge_count": 0, + "joint_image_dimension": 4 + }, + "three_edge_sharp": { + "width": 6, + "pattern_dimension": 3, + "pattern_basis": [ + 2, + 32768, + 536870912 + ], + "pool": [ + [ + 1, + 3 + ], + [ + 3, + 2 + ], + [ + 4, + 12 + ], + [ + 12, + 8 + ], + [ + 16, + 48 + ], + [ + 48, + 32 + ] + ], + "edge_count": 3, + "joint_image_dimension": 6 + }, + "two_edge_scope_control": { + "width": 5, + "pattern_dimension": 3, + "pattern_basis": [ + 2, + 8192, + 5931680 + ], + "pool": [ + [ + 1, + 3 + ], + [ + 3, + 2 + ], + [ + 4, + 12 + ], + [ + 12, + 8 + ], + [ + 26, + 21 + ] + ], + "edge_count": 2, + "joint_image_dimension": 5 + }, + "rank_four_scope_control": { + "width": 6, + "pattern_dimension": 4, + "pattern_basis": [ + 4160, + 262208, + 16777280, + 1073741888 + ], + "pool": [ + [ + 7, + 1 + ], + [ + 11, + 1 + ], + [ + 13, + 1 + ], + [ + 19, + 1 + ], + [ + 21, + 1 + ], + [ + 25, + 1 + ], + [ + 31, + 1 + ], + [ + 35, + 1 + ], + [ + 37, + 1 + ], + [ + 41, + 1 + ], + [ + 47, + 1 + ], + [ + 49, + 1 + ], + [ + 55, + 1 + ], + [ + 59, + 1 + ], + [ + 61, + 1 + ] + ], + "edge_count": 0, + "joint_image_dimension": 5 + } + } +} diff --git a/research/bit-zero-edge-image-bound/sources/pr6782-PROOF.md b/research/bit-zero-edge-image-bound/sources/pr6782-PROOF.md new file mode 100644 index 0000000000..5e9b0aa91c --- /dev/null +++ b/research/bit-zero-edge-image-bound/sources/pr6782-PROOF.md @@ -0,0 +1,287 @@ +# The five-dimensional two-edge core at three pattern dimensions + +Prepared for **@CubeJerry** with substantial OpenAI assistance. New work is +Apache-2.0. This is a scoped written proof, with finite corroboration. It does +not settle the three-relation paid-rank question or improve kappa. + +## 1. Exact statement + +Work over F2. For an r-dimensional space P of zero-diagonal W-by-W matrices, +let C(P) be **all** noncoordinate rank-one idempotents N=xy^T with +`off(N) in P`. Thus x,y are nonzero, y^T x=1, and off(N)!=0. Let e(P) count +the matrix units E_ab (a!=b) in P. Let V be the joint image of C(P). + +**Theorem (three-dimensional spaces containing two edges).** Suppose r=3. + +1. If e(P)=2, let E be the coordinate span of the endpoints of those two + directed edges. Then `dim V <= dim E + 1 <= 5`. If the edges share an + endpoint, the bound is at most four. +2. If e(P)=2, dim V=5, and the restrictions of the complete pool C(P) to V + act irreducibly, the edges have disjoint endpoints. There is a binary + basis of V in which the **set of restricted projectors** is exactly + `{E11,E22,E33,E44,J5}`, where J5 is the five-by-five all-ones matrix. + This normal form is irreducible. +3. If e(P)=3, the pool is a direct sum over the connected components of + the undirected graph of the three edges. Each nontrivial component + uses at most four coordinates. In particular, every irreducible + constituent has dimension at most four, although the total joint + image can have dimension six. + +Both the bound five in part 1 and the irreducible exception in part 2 +are attained. Therefore a reduction of all rank-three noncoordinate +pattern pools to irreducible scalar cores of dimension at most four is +false. The theorem does **not** assert that a rank-saving diagonal word +exists on the five-dimensional exception. + +There cannot be more than three matrix units in P: distinct matrix units +are linearly independent. The general corollary in Section 3 also bounds the one-edge case by five. +The irreducible classification is specific to two edges; the zero-edge +case and the one-edge irreducible classification remain outside it. + +## 2. Inherited fiber lemma and a new quotient observation + +We use Nick Petalas's #5921 fiber lemma: a realized nonzero binary pattern +has one rank-one-idempotent lift, except E_ab, whose two lifts are +`e_a(e_a+e_b)^T` and `(e_a+e_b)e_b^T`. The proof follows by subtracting two +lifts: their diagonal difference has rank at most two and even trace, so +is supported on two coordinates; the resulting binary 2-by-2 list gives +the stated pair. This lemma and its credit are inherited. + +**Quotient observation.** Let U be a coordinate subspace, and let N=xy^T +and M=uv^T be noncoordinate binary rank-one idempotents such that +`off(N)+off(M)` is supported within the U-by-U block. If x and u have +linearly independent images modulo U, then N and M have the same +single-edge pattern, and both endpoints of this edge lie outside U. + +Indeed, the outside-U rows and inside-U columns give +`(x mod U)(y|U)^T=(u mod U)(v|U)^T`. Independence forces y|U=v|U=0. +Consequently the entire inside-U block vanishes in both matrices, so +their full off-diagonal patterns are equal. The projectors differ, since +their image classes are independent. The fiber lemma makes that common +pattern a single edge. In its two lifts both covectors vanish on U only +when both endpoints lie outside U. This proves the observation. + +Also, a noncoordinate rank-one idempotent with its entire off-diagonal +pattern supported inside U has its image in U. Otherwise choose an +outside coordinate i with x_i=1. Its off-diagonal row forces y=e_i; the +remaining outside-block entries then force x=e_i, making the projector +coordinate, a contradiction. + +## 3. Sharp joint-image bound + +Assume e(P)=2. Let p,q be the two edge patterns, let P0=span(p,q), and let +E be their endpoint space. Every pool projector whose pattern belongs +to P0 has image in E by the preceding observation. Moreover the two lifts +of each edge belong to the **complete** pool and their images span its +two endpoints. Thus E is contained in V. + +There is just one nonzero coset P/P0. For any two projectors with patterns +in that coset, their off-diagonal difference is supported inside E. +If their image classes modulo E were independent, the quotient observation +would produce a third single-edge pattern in P, with endpoints outside E. +This contradicts e(P)=2. Hence their image classes are pairwise dependent. +Over F2 all nonzero such classes are equal; their span has dimension at +most one. Therefore V/E has dimension at most one. This proves part 1 +at every ambient width, without a word-length or address-rank assumption. + +**General edge-quotient bound.** More generally, let P have dimension r, +let e=e(P), and let E be the coordinate span of the endpoints of +**all** e edge patterns. +Let P0 be their span, of dimension e. The same proof gives + + dim V <= dim E + 2^(r-e) - 1. + +The zero coset contributes only images inside E, while each of the +2^(r-e)-1 nonzero cosets contributes at most one quotient-image dimension. +Otherwise the quotient observation would produce an additional edge with +endpoints outside E, contrary to its definition. This also holds at e=0 +with E=0. For r=3 and e=1 it gives dim V<=5. For e=0 it gives only the +seven-projector bound; no five-dimensional reduction is asserted there. +This resolves an edge-containing slice of #5921's explicit open question +about sharp joint-image dimension, whose general cardinality estimate +gives the coarser bound 2^r+r-1 (ten at r=3). The e=2 normal form is the +new sharp irreducible case. + +Since dim E<=2e and the function 2e+2^(r-e)-1 is convex in e, its +maximum on 0<=e<=r occurs at an endpoint. Consequently every complete +noncoordinate pool satisfies + + dim V <= max(2^r-1, 2r). + +In particular, all three-dimensional pattern pools have joint image at +most seven. This is an upper bound, not an attainment claim. The precise +r=3 conclusions supplied here are: + +| Number e of edge patterns | Joint-image bound | Additional conclusion | +| --- | ---: | --- | +| 0 | 7 | No sharpness or irreducible classification proved | +| 1 | 5 | No sharpness or irreducible classification proved | +| 2 | 5 | Irreducibly sharp; unique five-dimensional restriction | +| 3 | 6 | Coordinate components have dimension at most four | + +## 4. The unique irreducible five-dimensional restriction + +Suppose dim V=5 and the restricted pool is irreducible. Part 1 makes +E four-dimensional, so the edges are disjoint. Order their endpoints +as (1,2),(3,4), with edge patterns E12 and E34. Choose w in V supported +outside E, so `V=E direct-sum F2*w`. + +The two lifts of each edge restrict to their usual two-by-two block and +annihilate w. Conjugating by +`S=(I+E12)(I+E34)` makes those four lifts E11,E22,E33,E44. This change of +basis acts only on E. + +The sum E12+E34 is unrealizable: its entries (1,2) and (3,4) +would force the unwanted cross entry (1,4) in a rank-one matrix. Thus +the four edge lifts exhaust the nonzero realized patterns in P0. +All remaining projectors have patterns in the single coset P/P0. Before +or after this shear, the E-to-w and w-to-E blocks of their restrictions +are identical: their differences have zero off-block entries in the +original coordinates. More explicitly, a difference has its off-diagonal +support inside E; on E its outside component is zero, and on w its E +component is zero because w has no E coordinates. Both projectors +preserve V, so the remaining outside component is a scalar multiple of w. + +Write the common off-block column and row as a and b^T. If a=0, the line +F2*w is invariant under every restricted projector. If b=0, E is +invariant. Irreducibility therefore makes both a and b nonzero. + +Write any remaining rank-one restriction as +`(alpha,epsilon)(beta^T,eta)` in the basis E,w. Its off-blocks give +`alpha*eta=a` and `epsilon*beta=b`. Over F2, nonzero a,b force +`epsilon=eta=1`, alpha=a and beta=b. Thus there is **one** remaining +restricted projector, namely `(a,1)(b^T,1)`. + +With the four coordinate projectors present, irreducibility forces all +four entries of a and b to be one. If a_i=0, the hyperplane with coordinate +i zero is invariant; if b_i=0, the line F2*e_i is invariant. Conversely, +when a=b=(1,1,1,1), the remaining projector is J5 and the family is +irreducible: for a nonzero invariant subspace U, either some vector has +one of its first four coordinates nonzero, so Eii puts e_i in U and J5 +puts the all-ones vector in U; or U initially contains e5, and J5 again +puts the all-ones vector in U. Applying E11,...,E44 then gives e1,...,e4, +and adding them to the all-ones vector gives e5. Thus U=F2^5. + +This proves both uniqueness and irreducibility of the normal form. +It is an assertion about the set of restrictions; different original +projectors need not be distinguished if their restrictions coincide. + +## 5. Explicit sharp pool + +Use five coordinates numbered 0 through 4. An integer mask lists the +support of a binary vector, with bit i representing coordinate i. Take + +| Projector | x mask | y mask | +| --- | ---: | ---: | +| P | 1 | 3 | +| Q | 3 | 2 | +| R | 4 | 12 | +| T | 12 | 8 | +| B | 26 | 21 | + +Here B=(e1+e3+e4)(e0+e2+e4)^T. Each y^T x is one. Let +`P*=span(E01,E23,off(B))`. These three patterns are independent and the +only matrix units in P* are E01 and E23. The complete noncoordinate +pool C(P*) is exactly the five projectors in the table. + +For the last completeness assertion, the outside coordinate 4 has +B_44=1. Every pattern in off(B)+span(E01,E23) has the same nonzero +row-4 and column-4 off-diagonal entries. Any rank-one idempotent lift +therefore has x4=y4=1, fixing all other x and y entries and hence fixing +B itself. Among span(E01,E23), only the individual edges are realized: +their sum has two disjoint edges and cannot be a rank-one off-diagonal +pattern. Its four lifts are P,Q,R,T. + +The shear S=(I+E01)(I+E23), with S^-1=S, sends these five projectors to +E00,E11,E22,E33,J5. Section 4 proves irreducibility without enumeration. +The verifier independently checks all 496 binary rank-one idempotents +at width five, all 372 nonzero proper subspaces, and the conjugation. +This is a counterexample to a four-dimensional **pool** compression, +not to the two-relation rank theorem or to any paid-rank inequality. + +## 6. The three-edge case + +If e(P)=3, those three matrix units form a basis of P. Every realized +pattern is supported on their graph. The undirected support graph of a +noncoordinate rank-one idempotent is connected on its nonzero rows and +columns: the supports of x and y meet (their dot product is one), and +a common support coordinate connects all the others. Its support is +therefore contained in one connected component of the three-edge graph. +There are no extra isolated diagonal coordinates in a noncoordinate +rank-one lift. Thus every projector is supported in one component. +A connected component with at most three distinct edges has at most four +vertices. This proves part 3. Three disjoint edges attain total image +dimension six, showing why part 3 must discuss components instead of +claiming a total image bound five. + +## 7. Exact word relevance and its limits + +In the binary scalar-idempotent word model, let L be the saturated +integral lattice of exponent relations, with rank three. The first-order +augmentation argument from #720/#6777 puts the span of off-diagonal +coefficient vectors inside L/2L. Thus the occurring pattern span has +dimension at most three. The new theorem concerns the **dimension-three** +case whose complete pattern space contains at least two single edges. +It does not cover smaller pattern dimensions with three relations. +The one-edge case has the general joint-image bound five, but no unique +irreducible normal form is proved here. The zero-edge case has only the +general bound seven. + +Coordinate calls cannot simply be discarded. Here is a sufficient exact +split, which also explains the relevance of the complete pool. Let L0 be +the saturated rational span of all cube relations (entries in {-1,0,1}). +If rank L0<=2, the cube-fiber lift preserves the full endpoint and the +inherited #6777 theorem already gives the disjoint-subset rank bound. +Otherwise L0=L. If the occurring pattern span has dimension three, its +first-order coefficient vectors span all of L/2L. At a coordinate-call +index every such coefficient is zero, so every lattice vector has an even +entry there. A cube relation must then have entry zero there. Since cube +relations rationally span L, **every** relation has zero entry at every +coordinate-call index. The exponent group consequently splits as the +noncoordinate group plus the independent coordinate-call generators. + +Projecting away those free generators removes coordinate calls while +preserving a diagonal monomial endpoint. Apply the joint-image theorem +to the complete noncoordinate pool. Its joint image is invariant and its +quotient action is the identity. As in #6777, a diagonal monomial endpoint +preserving a binary subspace decomposes that subspace by equal monomial +labels: independence of the group-algebra monomials makes each coordinate +label projection preserve the subspace. An adapted binary basis therefore +keeps the endpoint diagonal. Nonidentity quotient labels cannot occur. + +In the one-edge or two-edge case this reduces the noncoordinate word to +at most five active scalar dimensions. The following uniqueness conclusion +is restricted to the two-edge case. If the five-dimensional complete-pool +restriction is irreducible, Section 4 gives its unique alphabet. If it +is reducible, an invariant flag gives block-upper-triangular subquotient blocks of +dimensions at most four. Adapt the binary basis to the equal-monomial +label decomposition at every flag term to retain a diagonal endpoint. +Each rank-one idempotent has exactly one active diagonal block. +The three-edge case already has coordinate blocks of size at most four. + +The shear to {E11,...,E44,J5} need **not** preserve a diagonal endpoint: +it can introduce the two edge positions. It is a proof normal form, not +a license to assume a diagonal endpoint in the sheared coordinates or to +insert free address transformations. The independent coordinate-call +generators removed above must also be restored to their original target +labels. No saving follows from +this scalar reduction. Exact rank-three diagonal identities, rational +rank-one address realizations and a complete paid/target invoice remain +unproved. + +## 8. Provenance and scope + +Scientific base: 7c49fe32c55de02c2c873655c804b16e4c3fef0a. The inherited +all-width two-relation theorem is #6777, exact head + e62a9d0d4143e11c190fcb4d81d83dc1662da782. Credit Nick Petalas/#5921 for the +fiber and cardinality theorem; David Govea/#720 and Ali Romman/#468 for +the relation and augmentation framework; woklerx/#1456 and #1846 for +the common-pattern and historical two-plane reductions; and eumemic/#288 +for the formal model. The new contribution is the quotient observation, +general edge-quotient bound, sharp two-edge bound, unique five-dimensional +irreducible normal form, +and its explicit obstruction to four-dimensional pool compression. + +No physical supplier, native implementation, dirty-input compiler, recursive +invoice, admitted BIT improvement, selected-frontier change, new kappa, +independent human acceptance, or proof-assistant formalization is claimed. diff --git a/research/bit-zero-edge-image-bound/verify.py b/research/bit-zero-edge-image-bound/verify.py new file mode 100644 index 0000000000..389007f0ca --- /dev/null +++ b/research/bit-zero-edge-image-bound/verify.py @@ -0,0 +1,337 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the written all-width zero-edge proof. + +Prepared for @CubeJerry with substantial OpenAI assistance. Apache-2.0. +Standard library only; no Git, predecessor-code imports or network required. +Finite checks do not prove the all-width theorem by enumeration. +""" + +import argparse +import copy +import hashlib +import itertools +import json +from pathlib import Path +import tempfile + +HERE = Path(__file__).resolve().parent + + +class VerificationError(ValueError): + """A proof-relevant fixture or replay obligation failed.""" + + +def need(condition, message): + if not condition: + raise VerificationError(message) + + +def rank(vectors): + pivots = {} + for value in vectors: + while value: + lead = value.bit_length() - 1 + if lead in pivots: + value ^= pivots[lead] + else: + pivots[lead] = value + break + return len(pivots) + + +def span(vectors): + result = {0} + for value in vectors: + result |= {entry ^ value for entry in result} + return result + + +def matrix(x, y, width): + """Row-major bit packing, including the diagonal.""" + return sum(y << (width * row) for row in range(width) if x >> row & 1) + + +def diagonal_mask(width): + return sum(1 << (row * width + row) for row in range(width)) + + +def off_matrix(value, width): + return value & ~diagonal_mask(width) + + +def pattern(x, y, width): + return off_matrix(matrix(x, y, width), width) + + +def catalogue(width): + """All binary rank-one idempotents, by their literal off-diagonal matrix.""" + result = {} + for x in range(1, 1 << width): + for y in range(1, 1 << width): + if (x & y).bit_count() % 2: + result.setdefault(pattern(x, y, width), []).append((x, y)) + return result + + +def source_integrity(directory): + origins = json.loads((directory / 'ORIGINS.json').read_text()) + need(len(origins['files']) == 1, 'source inventory count') + rows = [] + for entry in origins['files']: + raw = (directory / entry['path']).read_bytes() + sha256 = hashlib.sha256(raw).hexdigest() + git_blob = hashlib.sha1(b'blob ' + str(len(raw)).encode() + b'\0' + raw).hexdigest() + need(sha256 == entry['sha256'], 'source SHA256 mismatch') + need(git_blob == entry['git_blob'], 'source Git-blob mismatch') + rows.append({'path': entry['path'], 'sha256': sha256, 'bytes': len(raw)}) + return rows + + +def check_fibers(catalogues): + result = [] + for width, by_pattern in catalogues.items(): + total = sum(map(len, by_pattern.values())) + need(total == ((1 << width) - 1) * (1 << (width - 1)), 'idempotent census') + need(set(by_pattern.get(0, [])) == {(1 << i, 1 << i) for i in range(width)}, + 'zero-pattern coordinate fiber') + edges = 0 + for value, lifts in by_pattern.items(): + if value == 0: + continue + if value.bit_count() == 1: + edges += 1 + position = value.bit_length() - 1 + a, b = divmod(position, width) + need(a != b, 'edge is off diagonal') + expected = {(1 << a, (1 << a) | (1 << b)), + ((1 << a) | (1 << b), 1 << b)} + need(set(lifts) == expected, 'edge fiber has its exact two lifts') + else: + need(len(lifts) == 1, 'nonedge fiber is unique') + need(edges == width * (width - 1), 'complete directed-edge count') + result.append({'width': width, 'idempotents': total, + 'realized_nonzero_patterns': len(by_pattern) - 1, + 'edge_patterns': edges}) + return result + + +def check_fano(): + checked = 0 + for subset in itertools.combinations(range(1, 8), 5): + triangles = [set(triple) for triple in itertools.combinations(subset, 3) + if triple[0] ^ triple[1] ^ triple[2] == 0] + need(len(triangles) == 2, 'five-point set has two zero-sum triples') + need(len(triangles[0] & triangles[1]) == 1, 'triple intersection is one point') + need(triangles[0] | triangles[1] == set(subset), 'triple union is the five points') + a, b = sorted(set(range(1, 8)) - set(subset)) + need(triangles[0] & triangles[1] == {a ^ b}, 'constructive Fano center') + checked += 1 + need(checked == 21, 'all five-point subsets checked') + cap = (1, 2, 4, 7) + need(all(a ^ b ^ c != 0 for a, b, c in itertools.combinations(cap, 3)), + 'four-point cap has no zero-sum triple') + return {'five_point_subsets': checked, 'four_point_cap': list(cap)} + + +def check_case(case, catalogues): + width = case['width'] + basis = case['pattern_basis'] + need(1 <= width <= 7, 'fixture width in finite replay domain') + need(all(isinstance(p, int) and 0 < p < (1 << (width * width)) for p in basis), + 'pattern-basis range') + need(all(off_matrix(p, width) == p for p in basis), 'pattern basis is zero diagonal') + need(rank(basis) == case['pattern_dimension'], 'declared pattern dimension') + patterns = span(basis) + need(len(patterns) == 1 << case['pattern_dimension'], 'pattern-space size') + given = [] + for raw in case['pool']: + need(len(raw) == 2, 'projector factor pair') + x, y = raw + need(0 < x < (1 << width) and 0 < y < (1 << width), 'projector factor range') + need((x & y).bit_count() % 2 == 1, 'projector is idempotent') + value = pattern(x, y, width) + need(value != 0, 'projector is noncoordinate') + need(value in patterns, 'projector pattern belongs to P') + given.append((x, y)) + need(len(given) == len(set(given)), 'pool has no duplicates') + complete = {lift for value in patterns - {0} + for lift in catalogues[width].get(value, [])} + need(set(given) == complete, 'pool is complete') + image_dimension = rank(x for x, _ in complete) + covector_dimension = rank(y for _, y in complete) + need(image_dimension == case['joint_image_dimension'], 'declared joint-image dimension') + need(image_dimension <= case.get('joint_image_bound', image_dimension), + 'claimed joint-image bound') + edges = sum(value.bit_count() == 1 for value in patterns) + need(edges == case['edge_count'], 'declared edge count') + return {'width': width, 'pattern_dimension': case['pattern_dimension'], + 'edge_count': edges, 'pool_size': len(complete), + 'joint_image_dimension': image_dimension, 'covector_dimension': covector_dimension} + + +def require_noedge_theorem_scope(case): + need(case['pattern_dimension'] <= 3, 'no-edge theorem pattern dimension at most three') + need(case['edge_count'] == 0, 'no-edge theorem excludes matrix units') + + +def check_dependency_configuration(pairs, width): + need(len(pairs) == 5, 'dependency configuration size') + need(all(x and y for x, y in pairs), 'dependency factors are nonzero') + need(rank(x for x, _ in pairs) == 5, 'dependency images are independent') + for indices in ((0, 1, 2), (0, 3, 4)): + value = 0 + for index in indices: + value ^= matrix(*pairs[index], width) + need(off_matrix(value, width) == 0, 'dependency sum is diagonal') + x, y = pairs[0] + need(x == y and x.bit_count() == 1, 'shared projector is coordinate') + + +def expect_rejection(label, action, reason, observed): + try: + action() + except VerificationError as error: + need(reason in str(error), label + ': rejected for the wrong reason: ' + str(error)) + observed.append({'control': label, 'rejection': str(error)}) + else: + raise VerificationError(label + ': invalid input was accepted') + + +def check_controls(cases, catalogues): + observed = [] + sharp = cases['zero_edge_sharp'] + forged = copy.deepcopy(sharp) + forged['joint_image_bound'] = 3 + expect_rejection('false no-edge cap three', lambda: check_case(forged, catalogues), + 'claimed joint-image bound', observed) + omitted = copy.deepcopy(sharp) + omitted['pool'].pop() + expect_rejection('incomplete seven-projector pool', lambda: check_case(omitted, catalogues), + 'pool is complete', observed) + nonidempotent = copy.deepcopy(sharp) + nonidempotent['pool'][0][0] ^= 1 + expect_rejection('nonidempotent factor mutation', lambda: check_case(nonidempotent, catalogues), + 'projector is idempotent', observed) + coordinate = copy.deepcopy(sharp) + coordinate['pool'].append([1, 1]) + expect_rejection('coordinate-call admission', lambda: check_case(coordinate, catalogues), + 'projector is noncoordinate', observed) + expect_rejection('two-edge dimension-five scope witness', + lambda: require_noedge_theorem_scope(cases['two_edge_scope_control']), + 'excludes matrix units', observed) + expect_rejection('rank-four parity-code scope witness', + lambda: require_noedge_theorem_scope(cases['rank_four_scope_control']), + 'dimension at most three', observed) + coordinate_five = [(1 << i, 1 << i) for i in range(5)] + check_dependency_configuration(coordinate_five, 6) + # Labels u1,u2,u1+u2,u3,u1+u3 give both required sums E_00. + dependent = [(1 | u, 1) for u in (6, 10, 12, 18, 20)] + for indices in ((0, 1, 2), (0, 3, 4)): + value = 0 + for index in indices: + value ^= matrix(*dependent[index], 5) + need(value == 1, 'dependent control really has both diagonal sums E_00') + need(rank(x for x, _ in dependent) == 4, 'dependent control has image rank four') + need(pattern(*dependent[0], 5) != 0, 'dependent control shared projector is noncoordinate') + expect_rejection('dependent images invalidate intersection lemma', + lambda: check_dependency_configuration(dependent, 5), + 'images are independent', observed) + nondiagonal = coordinate_five.copy() + nondiagonal[0] = (1, 33) + expect_rejection('nondiagonal sums invalidate intersection lemma', + lambda: check_dependency_configuration(nondiagonal, 6), + 'sum is diagonal', observed) + # Run the actual hash checker on changed retained bytes outside this package. + with tempfile.TemporaryDirectory(prefix='zero-edge-source-control-') as temporary: + destination = Path(temporary) + (destination / 'ORIGINS.json').write_bytes((HERE / 'ORIGINS.json').read_bytes()) + for entry in json.loads((HERE / 'ORIGINS.json').read_text())['files']: + target = destination / entry['path'] + target.parent.mkdir(parents=True, exist_ok=True) + target.write_bytes((HERE / entry['path']).read_bytes() + b'\ncorrupted\n') + expect_rejection('retained-source byte corruption', lambda: source_integrity(destination), + 'source SHA256 mismatch', observed) + return observed + + +EXPECTED_CENSUS = { + 3: {'generated_spaces': 202, 'zero_edge_spaces': 112, + 'image_dimension/pool_size': {'1/4': 1, '2/3': 53, '3/3': 48, '3/4': 7, '3/5': 3}}, + 4: {'generated_spaces': 104657, 'zero_edge_spaces': 98997, + 'image_dimension/pool_size': {'1/4': 52, '2/3': 18012, '2/4': 1450, + '2/5': 100, '3/3': 72676, '3/4': 5468, + '3/5': 168, '4/4': 987, '4/5': 84}} +} + + +def check_census(width, by_pattern): + """All 3-spaces generated by three realized nonedge patterns at this width. + + This does not enumerate arbitrary subspaces of the full off-diagonal + ambient space. If the realized patterns span less than three dimensions, + fiber uniqueness already bounds the image dimension by three. + """ + lifts = {p: values[0] for p, values in by_pattern.items() if p.bit_count() > 1} + need(all(len(by_pattern[p]) == 1 for p in lifts), 'census unique nonedge lifts') + seen = set() + histogram = {} + for a, b, c in itertools.combinations(sorted(lifts), 3): + if c == a ^ b: + continue + nonzero = tuple(sorted((a, b, c, a ^ b, a ^ c, b ^ c, a ^ b ^ c))) + if nonzero in seen: + continue + seen.add(nonzero) + if any(p.bit_count() == 1 for p in nonzero): + continue + pool = [lifts[p] for p in nonzero if p in lifts] + dimension = rank(x for x, _ in pool) + need(dimension <= 4, 'finite no-edge image bound') + need(rank(y for _, y in pool) <= 4, 'finite transposed no-edge image bound') + key = str(dimension) + '/' + str(len(pool)) + histogram[key] = histogram.get(key, 0) + 1 + result = {'generated_spaces': len(seen), 'zero_edge_spaces': sum(histogram.values()), + 'image_dimension/pool_size': dict(sorted(histogram.items()))} + need(result == EXPECTED_CENSUS[width], 'frozen exact census at width ' + str(width)) + return result + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--json-output', type=Path, + help='write the completed deterministic report after every check passes') + parser.add_argument('--integrity-only', action='store_true', + help='check retained provenance bytes only; not a mathematical replay') + args = parser.parse_args() + sources = source_integrity(HERE) + if args.integrity_only: + print('PASS_ZERO_EDGE_SOURCE_BYTES ' + json.dumps(sources, sort_keys=True)) + return + catalogues = {width: catalogue(width) for width in range(1, 8)} + cases = json.loads((HERE / 'WITNESSES.json').read_text())['cases'] + witnesses = {name: check_case(case, catalogues) for name, case in cases.items()} + require_noedge_theorem_scope(cases['zero_edge_sharp']) + report = { + 'claim': 'finite corroboration of written all-width no-edge image bound four; universal rank-three bound six', + 'all_width_proof': 'PROOF.md; not established by finite replay', + 'new_kappa': False, + 'sources': sources, + 'fibers': check_fibers(catalogues), + 'fano': check_fano(), + 'witnesses': witnesses, + 'census': {str(width): check_census(width, catalogues[width]) for width in (3, 4)}, + 'negative_controls': check_controls(cases, catalogues), + } + need(json.loads((HERE / 'RESULT.json').read_text()) == report, + 'committed deterministic report matches the completed replay') + payload = json.dumps(report, sort_keys=True, indent=2) + '\n' + if args.json_output: + args.json_output.write_text(payload) + print('PASS_ZERO_EDGE_IMAGE_BOUND ' + json.dumps(report, sort_keys=True)) + + +if __name__ == '__main__': + try: + main() + except (VerificationError, OSError, KeyError, TypeError, json.JSONDecodeError) as error: + raise SystemExit('FAIL_ZERO_EDGE_IMAGE_BOUND: ' + str(error)) from error