diff --git a/research/p112-two-total-rank-one-seed21/CERTIFICATE.json b/research/p112-two-total-rank-one-seed21/CERTIFICATE.json new file mode 100644 index 0000000000..36a0c0c245 --- /dev/null +++ b/research/p112-two-total-rank-one-seed21/CERTIFICATE.json @@ -0,0 +1,498 @@ +{ + "assignment_seed": 21, + "classification_counts": { + "covered": 13, + "outside_claim": 2 + }, + "controls": [ + "source-perturbation-breaks-all-pairs", + "omit-nonzero-extra-term", + "conjugation-is-not-transpose", + "rank-two-source-cannot-collapse", + "complex-rank-not-real-column-rank", + "coupled-rank-two-inside-not-classified-as-covered", + "GL2-basis-change-is-not-cost-free", + "k3-one-outside-does-not-force-source-rank-one", + "dependent-and-independent-binary-rows" + ], + "examples": [ + { + "classification": "covered", + "collapsed_cost": 64, + "disjoint_blocks": [ + { + "cost": 0, + "floor": 0, + "support": [] + }, + { + "cost": 0, + "floor": 0, + "support": [] + } + ], + "extra_terms": 2, + "identity_entries_checked": 12544, + "name": "zero-added-readers", + "ordered_costs": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 0, + 0 + ], + "quotient_rank": 0, + "reader_rank": 0, + "source_quotient_rank": 0, + "source_rank": 2, + "total_cost": 64 + }, + { + "classification": "covered", + "collapsed_cost": 64, + "disjoint_blocks": null, + "extra_terms": 2, + "identity_entries_checked": 12544, + "name": "zero-added-sources-outside", + "ordered_costs": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 0, + 0 + ], + "quotient_rank": 2, + "reader_rank": 2, + "source_quotient_rank": 0, + "source_rank": 0, + "total_cost": 64 + }, + { + "classification": "covered", + "collapsed_cost": 72, + "disjoint_blocks": null, + "extra_terms": 2, + "identity_entries_checked": 12544, + "name": "off-column-(1, 0)", + "ordered_costs": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 1 + ], + "quotient_rank": 1, + "reader_rank": 2, + "source_quotient_rank": 0, + "source_rank": 1, + "total_cost": 73 + }, + { + "classification": "covered", + "collapsed_cost": 72, + "disjoint_blocks": null, + "extra_terms": 2, + "identity_entries_checked": 12544, + "name": "off-column-(-1, 0)", + "ordered_costs": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 1 + ], + "quotient_rank": 1, + "reader_rank": 2, + "source_quotient_rank": 0, + "source_rank": 1, + "total_cost": 73 + }, + { + "classification": "covered", + "collapsed_cost": 72, + "disjoint_blocks": null, + "extra_terms": 2, + "identity_entries_checked": 12544, + "name": "off-column-(0, 1)", + "ordered_costs": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 1 + ], + "quotient_rank": 1, + "reader_rank": 2, + "source_quotient_rank": 0, + "source_rank": 1, + "total_cost": 73 + }, + { + "classification": "covered", + "collapsed_cost": 72, + "disjoint_blocks": null, + "extra_terms": 2, + "identity_entries_checked": 12544, + "name": "off-column-(1, 1)", + "ordered_costs": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 1 + ], + "quotient_rank": 1, + "reader_rank": 2, + "source_quotient_rank": 0, + "source_rank": 1, + "total_cost": 73 + }, + { + "classification": "covered", + "collapsed_cost": 64, + "disjoint_blocks": null, + "extra_terms": 2, + "identity_entries_checked": 12544, + "name": "canceling-off-column", + "ordered_costs": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 1, + 1 + ], + "quotient_rank": 1, + "reader_rank": 1, + "source_quotient_rank": 0, + "source_rank": 1, + "total_cost": 66 + }, + { + "classification": "covered", + "collapsed_cost": 72, + "disjoint_blocks": null, + "extra_terms": 2, + "identity_entries_checked": 12544, + "name": "reader-rank-one-source-rank-two", + "ordered_costs": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 1 + ], + "quotient_rank": 0, + "reader_rank": 1, + "source_quotient_rank": 1, + "source_rank": 2, + "total_cost": 73 + }, + { + "classification": "covered", + "collapsed_cost": 72, + "disjoint_blocks": null, + "extra_terms": 3, + "identity_entries_checked": 12544, + "name": "three-totals-quotient-two", + "ordered_costs": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 1, + 1, + 8 + ], + "quotient_rank": 2, + "reader_rank": 3, + "source_quotient_rank": 0, + "source_rank": 1, + "total_cost": 74 + }, + { + "classification": "covered", + "collapsed_cost": 72, + "disjoint_blocks": null, + "extra_terms": 4, + "identity_entries_checked": 12544, + "name": "four-totals-quotient-three", + "ordered_costs": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 1, + 1, + 1, + 8 + ], + "quotient_rank": 3, + "reader_rank": 4, + "source_quotient_rank": 0, + "source_rank": 1, + "total_cost": 75 + }, + { + "classification": "covered", + "collapsed_cost": null, + "disjoint_blocks": [ + { + "cost": 8, + "floor": 8, + "support": [ + 3 + ] + }, + { + "cost": 8, + "floor": 8, + "support": [ + 7 + ] + } + ], + "extra_terms": 2, + "identity_entries_checked": 12544, + "name": "rank-two-disjoint-coordinate-retirement", + "ordered_costs": [ + 8, + 8, + 8, + 0, + 8, + 8, + 8, + 0, + 8, + 8 + ], + "quotient_rank": 0, + "reader_rank": 2, + "source_quotient_rank": 0, + "source_rank": 2, + "total_cost": 64 + }, + { + "classification": "outside_claim", + "collapsed_cost": null, + "disjoint_blocks": null, + "extra_terms": 2, + "identity_entries_checked": 12544, + "name": "basis-mixed-retirement", + "ordered_costs": [ + 8, + 8, + 8, + 0, + 8, + 8, + 8, + 0, + 9, + 9 + ], + "quotient_rank": 0, + "reader_rank": 2, + "source_quotient_rank": 0, + "source_rank": 2, + "total_cost": 66 + }, + { + "classification": "covered", + "collapsed_cost": null, + "disjoint_blocks": [ + { + "cost": 25, + "floor": 16, + "support": [ + 0, + 2 + ] + }, + { + "cost": 24, + "floor": 16, + "support": [ + 4, + 6 + ] + } + ], + "extra_terms": 2, + "identity_entries_checked": 12544, + "name": "disjoint-two-complex-lifts", + "ordered_costs": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 9, + 8 + ], + "quotient_rank": 0, + "reader_rank": 2, + "source_quotient_rank": 2, + "source_rank": 2, + "total_cost": 81 + }, + { + "classification": "covered", + "collapsed_cost": null, + "disjoint_blocks": [ + { + "cost": 24, + "floor": 16, + "support": [ + 0, + 1 + ] + }, + { + "cost": 24, + "floor": 16, + "support": [ + 2, + 3 + ] + }, + { + "cost": 17, + "floor": 16, + "support": [ + 4, + 5 + ] + } + ], + "extra_terms": 3, + "identity_entries_checked": 12544, + "name": "disjoint-three-complex-lifts", + "ordered_costs": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 1 + ], + "quotient_rank": 0, + "reader_rank": 3, + "source_quotient_rank": 1, + "source_rank": 3, + "total_cost": 81 + }, + { + "classification": "outside_claim", + "collapsed_cost": null, + "disjoint_blocks": null, + "extra_terms": 2, + "identity_entries_checked": 12544, + "name": "dense-rank-two-inside-remains-open", + "ordered_costs": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8 + ], + "quotient_rank": 0, + "reader_rank": 2, + "source_quotient_rank": 0, + "source_rank": 2, + "total_cost": 80 + } + ], + "field": "Gaussian rational, algebraic transpose", + "full_identity_entries": 200704, + "k3_boundary": { + "classification": "outside_claim", + "collapsed_cost": null, + "disjoint_blocks": null, + "extra_terms": 3, + "identity_entries_checked": 12544, + "name": "k3-one-outside-insufficient", + "ordered_costs": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 1, + 1, + 8 + ], + "quotient_rank": 1, + "reader_rank": 2, + "source_quotient_rank": 0, + "source_rank": 2, + "total_cost": 74 + }, + "no_new_kappa": true, + "schema": 1, + "scope": "finite boundary fixtures for written quotient/collapse theorem" +} diff --git a/research/p112-two-total-rank-one-seed21/CLAIM.md b/research/p112-two-total-rank-one-seed21/CLAIM.md new file mode 100644 index 0000000000..3a89d03efb --- /dev/null +++ b/research/p112-two-total-rank-one-seed21/CLAIM.md @@ -0,0 +1,82 @@ +# Local sprint claim — seed 21 + +Track: complex supplier (OS draw `secrets.randbelow(100)` = **21**). +Base: `1b59b624d21924f8e3537cdc1ac52d3be6eda2fe`. +Started 2026-10-13 19:39 UTC; expected finish 20:19 UTC. + +## Exact scope + +P112 all-pairs ten-term decoders retaining the eight coordinate readers. +Test whether two extra totals whose readers leave the coordinate column +space can evade the #845/#998 single-lift copy floor. Use quotient-space +rank and support-rank subadditivity, with exact Gaussian-rational examples. +Also record the directly related k-total quotient-nullity-one corollary +and the disjoint coefficient-support composition of single-lift bounds. +Expected deliverable: a scoped obstruction, explicit boundary examples, +source pins, a deterministic certificate and a separate checker; no kappa. + +## Three candidates and selection + +1. Conjugate a selected k8 helper by dyadic scales: overlaps #1161, and + stage consolidation #1170; rejected. +2. Shorten CK coefficient lowering at fixed grid: overlaps #1118 and + #1036/#999; rejected. +3. Two-total P112 off-column cancellation: chosen. #845 and #998 cover + one total, #1133 covers scalar-field descent for that single total, + #1098 its support lemma. None covers the two-total quotient reduction. + #968/#1077 cover exactly eight terms with altered readers; different class. + +Seed 21 selects coordinate pair index 21 in lexicographic order and port21 +for boundary examples. These are diagnostics, not claimed disjoint searches. +The proof is uniform over complex coefficients. No search is reopened. + +## Source and cost gates + +Selected at base: PR1094, kappa 0.001672660197076918, on the seven-slot k8 +word, predecessor PR1087. Read the selected record, its source inventory, +assembly and community-batch1099 review; selection is context only. + +Grant preparation, source access, frames, restoration and recursive children +zero extra cost and test the necessary copy-rank saving first. If the floor +64 survives, stop physical synthesis. This is not a complete moment bound: +redistributing equal rank mass or changing other expenses remains open. + +## Coordination and overlap + +Read 786 open PR metadata entries, relevant PR bodies #1118/#1161/#1170, +#1133/#1120/#845, the review ledger, and predecessor proofs. The GitHub +pinnedIssues query returned no nodes; the only open issues were #650/#913. +The live discussion board contained start-here #1163, handoffs #1166 and +mechanisms #1167, with no comments or scoped claims at entry. Per the task's +no-coordination-issue fallback this claim is local; no reservation issue +is opened. Refresh PRs and discussions before submission. + +## Bounded work and verification + +Stop after the precise reduction is proved or falsified and finite boundary +fixtures are checked. Reserve the final quarter for adversarial proof review, +source/certificate mutation controls, optimized execution, clean relocation +and handoff. Two delegated workers stay in this scope: proof review and a +separately implemented finite checker. Both are AI assistance. + +Contributor: Philipp / @mightyOil, with substantial OpenAI Codex assistance. +Credit Mihir Srivastava (#845), @woklerx (#998), DreamingOfClouds (#717/#446), +and Joel Pulikkan / GamingPuzzled (#620). Apache-2.0. + +## DONE — one local result and handoff + +The [completed result](README.md), [proof](PROOF.md), +[exact certificate](CERTIFICATE.json), and [validation](VALIDATION.json) +exclude dependent, off-column-canceling and disjoint-support added totals +from lowering the P112 copy-rank sum. Independent overlapping coordinate +lifts with arbitrary source columns remain outside this result. + +The full package command passed, including inherited #845/#998 replay, +1,180 independent matrix identities and eight packaging controls. Final +refresh inspected 798 open PRs through #1186. Concurrent #1180 is credited +and compared explicitly: its both-factors-in-code hypothesis excludes our +outside-source fixtures. Main remains the recorded base commit. This is a +scoped negative result, with no selected frontier change or new kappa. +The one focused PR and its immutable local patch are supplied in the final +user handoff. No public coordination issue existed, so this local claim is +the only claim updated. diff --git a/research/p112-two-total-rank-one-seed21/INDEPENDENT.json b/research/p112-two-total-rank-one-seed21/INDEPENDENT.json new file mode 100644 index 0000000000..bfad31d704 --- /dev/null +++ b/research/p112-two-total-rank-one-seed21/INDEPENDENT.json @@ -0,0 +1,55 @@ +{ + "conjugate_transpose_negative_control": "rejected", + "controls": { + "rank_one_reader": 28, + "rank_one_source_outside_readers": 28, + "rank_two_dense_overlap_control": 28, + "rank_two_disjoint_axes": 28, + "rank_two_disjoint_pairs": 210, + "rejected_omitted_terms": 28, + "rejected_source_perturbations": 28, + "transposed_identities": 322 + }, + "coordinate_pairs": 28, + "disjoint_support_controls": { + "axis_pairs": 28, + "combined_cost_rule": "component_1 + component_2 - 64 >= 64", + "component_costs": [ + 64 + ], + "component_identity_count": 476, + "two_plus_two_partitions": 210 + }, + "entries_per_identity": 12544, + "full_matrix_identities": 1180, + "general_k_control": { + "k": 3, + "quotient_rank": 2, + "reader_rank": 3, + "source_rank": 1 + }, + "observed_total_costs": { + "rank_one_reader": [ + 73 + ], + "rank_one_source_outside_readers": [ + 73 + ], + "rank_two_dense_overlap_control": [ + 80 + ], + "rank_two_disjoint_axes": [ + 64 + ], + "rank_two_disjoint_pairs": [ + 64 + ] + }, + "outside_both_reductions": "rank_two_dense_overlap_control", + "outside_port": 78, + "scope": "independent exact finite fixtures; universal proof remains in PROOF.md", + "seed": 21, + "source_geometry_sha256": "4f44af368e046002553d632ee90c6470990827cea3fae41f0f54018522d7a080", + "status": "pass", + "zero_boundaries": 2 +} diff --git a/research/p112-two-total-rank-one-seed21/NOTICE.md b/research/p112-two-total-rank-one-seed21/NOTICE.md new file mode 100644 index 0000000000..5a161c1eec --- /dev/null +++ b/research/p112-two-total-rank-one-seed21/NOTICE.md @@ -0,0 +1,32 @@ +# Attribution and license + +Prepared for Philipp / **@mightyOil** with substantial **OpenAI Codex** +assistance in mathematics, implementation, tests and documentation. +The separate implementations and proof review are AI-assisted; no independent +human review or proof-assistant verification is claimed. New material is +Apache-2.0 under the repository LICENSE. + +- **Mihir Srivastava / @mihir-s-05, #845**: the real fixed-reader single-lift + floor, geometry construction and finite-premise certificate/checkers. +- **@woklerx, #998**: complex-to-real support transfer and the complex + single-lift theorem used after collapse or independently on disjoint groups. +- **DreamingOfClouds, #717**: P112 model and open mixed-rank question; + **#446**: inherited separate-total physical copy-tree interpretation. +- **Joel Pulikkan / GamingPuzzled, #620**, and predecessors: the original + coordinate cost 64, not a new value established by this contribution. +- **Adam Gall / @adamgall, #1098**: separate Gram-spectrum corroboration + of #845's support lemma; adjacent evidence, not an executable dependency. +- **Sagar Thakrar / @thakrarsagar, #1133**: concurrent rational single-lift support descent; + distinct scalar-field extension, no code or results imported. +- **@woklerx, #1180**, head `75b408646d558147a4eb250fc407d1fbfcb8df4e`: concurrent + overcomplete factor-linear floor; overlap and distinct arbitrary-source + coverage are explained in README.md. No pending code or proof is imported. +- The selected context retains **Rohan Arun #1094**, **Jeremy Kothe's + k8/slot/T16 and #1087 lineage**, **Hao Yan #858**, **Chafik Boukhalfa**, + **icekylinx**, **DreamingOfClouds #589**, **eumemic #555**, and the full + original notices. No selected-construction improvement is claimed here. + +No predecessor files are copied or modified. Their source-specific notices +remain in place and are pinned along with the consumed sources. Rank-nullity +and support/rank subadditivity are standard linear algebra; the contribution +is their explicit cost-preserving reduction and scoped P112 consequence. diff --git a/research/p112-two-total-rank-one-seed21/PROOF.md b/research/p112-two-total-rank-one-seed21/PROOF.md new file mode 100644 index 0000000000..4ec1af4cc9 --- /dev/null +++ b/research/p112-two-total-rank-one-seed21/PROOF.md @@ -0,0 +1,277 @@ +# Rank-one and disjoint-support reductions for P112 extra totals + +This is a scoped written theorem about exact finite matrix factorizations and +the inherited support-only copy-rank cost. It is not a proof-assistant +formalization or a theorem about unrestricted physical delivery programs. + +The real single-lift obstruction is due to **Mihir Srivastava +(@mihir-s-05), PR845**. Its complex extension is due to **@woklerx, PR998**. +Their proofs are retained in +[the real predecessor](../p112-single-lift/PROOF.md) and +[the complex predecessor](../p112-complex-single-lift/PROOF.md). +The P112 model comes from **DreamingOfClouds, PR717**; the coordinate value +64 belongs to **Joel Pulikkan / GamingPuzzled, PR620** and its predecessors. +The present addition is the support-subadditivity reduction for dependent +extra sources or readers, its quotient-space consequence including extra +readers outside the coordinate column space, and the direct summation of +single-lift bounds when the added readers use disjoint coordinate sets. +These reductions do not claim new priority for rank-nullity, rank +subadditivity, or summing bounds on disjoint groups. + +## Exact model and inherited premise + +Let `X` be the predecessor's real `112 x 8` matrix, with columns `x_j`, +`XX^T = 2G`, and complex column rank eight. All transposes below are +algebraic transposes: no complex conjugation occurs. Let `l_i` and `v_i` +be its fixed binary labels and dual labels. For complex vectors define + + beta(d,s) = rank_F2 (v_i dot l_u)_(i in supp(d), u in supp(s)). + +The rank of an empty matrix is zero. This cost depends only on supports; +it is neither complex matrix rank nor an estimate of physical bit width. +The complex predecessor proves that for every `a in C^8` and +`z in C^112`, + + sum_j beta(x_j, x_j - a_j z) + beta(Xa,z) >= 64. (1) + +In particular, `beta(x_j,x_j)=8` for each of the eight coordinates, +and `sum_j beta(x_j,x_j)=64`. + +For an integer `k >= 1`, consider any exact factorization on **all** +matrix entries + + XX^T = XT^T + DZ^T, (2) + +where `T` has eight columns `t_j` and `D,Z` have `k` columns `d_h,z_h`. +Every entry of `T,D,Z` may be an arbitrary complex number. The first +eight reader columns `x_j` are retained. Its separate-total cost is + + C(T,D,Z) = sum_j beta(x_j,t_j) + sum_h beta(d_h,z_h). (3) + +Zero readers and zero sources are allowed; no column is required to be +in `col_C(X)` at the outset. Write + + q = rank_C([X D]) - rank_C(X). + +Equivalently, `q` is the rank of the added readers in the quotient space +`C^112 / col_C(X)`. + +**Theorem.** Every factorization (2) satisfies `C(T,D,Z) >= 64` if at +least one of the following holds: + +1. `rank_C(Z) <= 1`; +2. `rank_C(D) <= 1`; +3. `q >= k-1`; +4. `D=XA` and the columns `a_h` of `A` have pairwise disjoint + coordinate supports `J_h = {j : a_jh != 0}`. + +Condition 3 implies condition 1 by exactness; it is useful because it +can be checked from the added readers before finding their source columns. +Condition 4 permits independent extra sources and readers. Its supports +refer to coefficients in the retained coordinate basis, not to the +112-component supports of the reader vectors `Xa_h`. + +## Support subadditivity + +For arbitrary complex vectors `u_h`, scalars `c_h`, and a fixed source +`s`, support containment and binary matrix rank give + + beta(sum_h c_h u_h, s) + <= sum_(h: c_h != 0) beta(u_h,s). (4) + +Indeed, the support of the sum is contained in the union of the supports +of the `u_h` with nonzero coefficient. Restricting a matrix to fewer rows +cannot increase rank. The binary matrix on the union of those row sets +is obtained by selecting rows from their vertical concatenation, whose +rank is at most the sum of their ranks. Repeated rows cause no problem. +The same argument using columns proves + + beta(d, sum_h c_h s_h) + <= sum_(h: c_h != 0) beta(d,s_h). (5) + +Multiplication by a nonzero complex scalar does not change support. +These statements concern ranks over `F2`; complex coefficients are used +only to determine supports. They do not require positivity, bounded +coefficients, or the vectors to belong to `col_C(X)`. + +## Collapse of rank-one sources + +If `rank_C(Z)=0`, all `z_h` vanish. Equation (2) becomes +`X(T^T-X^T)=0`; injectivity of `X` gives `T=X`. The eight retained terms +alone cost 64 and every added term costs zero. + +Otherwise `rank_C(Z)=1`, so there are a nonzero vector `z` and scalars +`c_h` with `z_h=c_h z`. Put `d=sum_h c_h d_h`. The identity becomes + + XX^T = XT^T + d z^T. (6) + +By (4), + + beta(d,z) <= sum_h beta(d_h,z_h). (7) + +For `c_h=0` both the original added term and its cost are zero; such +indices are simply omitted from (4). + +Reducing each column of (6) modulo `col_C(X)` gives +`[d] z_i=0` for every index `i`. Since `z` is nonzero, this forces +`d in col_C(X)`. Write `d=Xa`, uniquely. Substitution into (6) and +injectivity of `X` give + + T^T = X^T - a z^T, or equivalently t_j=x_j-a_j z. + +Applying (1) and then (7) proves + + C(T,D,Z) >= sum_j beta(x_j,x_j-a_j z)+beta(Xa,z) >= 64. + +This includes `d=0`. Individual `d_h` may lie outside `col_C(X)`; +their quotient components can cancel in the combination `d`. The proof +requires only the combined reader to belong to the coordinate column +space and therefore does not discard that possibility. + +## Collapse of rank-one readers + +If `rank_C(D)=0`, equation (2) again gives `T=X`, so the cost is 64. +Otherwise choose a nonzero `d` and scalars `c_h` such that `d_h=c_h d`. +Put `z=sum_h c_h z_h`. Equation (6) holds, and (5) gives + + beta(d,z) <= sum_h beta(d_h,z_h). (8) + +If `z=0`, exactness gives `T=X`; the nonnegative added costs cannot +lower 64. If `z!=0`, the same quotient and injectivity argument used +above gives `d=Xa` and `t_j=x_j-a_j z`. Equation (1) and inequality +(8) prove the required bound. No assumption on the rank of `Z` was +used in this case. + +## Quotient rank forces source dependence + +Let `pi: C^112 -> C^112 / col_C(X)` be the quotient map. Applying it +to the columns of (2) gives + + (pi D) Z^T = 0. (9) + +View `pi D` as a linear map with domain `C^k`. It has rank `q` and +kernel dimension `k-q`. Equation (9) places the image of `Z^T` in +that kernel. Hence, for every exact factorization (2), + + rank_C(Z) = rank_C(Z^T) <= k-q. (10) + +If `q>=k-1`, inequality (10) yields `rank_C(Z)<=1`, which is the +already proved first case. If `q=k`, all sources are zero. If `k=1`, +the condition `q>=k-1` is automatic and recovers the inherited +nine-term conclusion. The theorem has no `k=0` hypothesis; with no +added terms, injectivity directly gives `T=X` and cost 64. + +The numerical lower bound is sharp for the whole stated class: taking +`T=X` and `Z=0` gives cost 64. This does not assert that every individual +quotient-rank stratum attains 64. + +## Disjoint coordinate supports separate into single lifts + +Suppose `D=XA`, and write `a_h` for column `h` of `A`. Injectivity of +`X` in (2) gives + + T=X-ZA^T, so t_j=x_j-sum_h a_jh z_h. (11) + +Assume the sets `J_h={j:a_jh!=0}` are pairwise disjoint. If `j` belongs +to `J_h`, it belongs to no other such set, and therefore +`t_j=x_j-a_jh z_h`. If `j` lies outside their union `J`, then `t_j=x_j`. +Consequently the exact cost separates as + + C(T,D,Z) + = 8(8-|J|) + + sum_h [sum_(j in J_h) beta(x_j,x_j-a_jh z_h) + + beta(Xa_h,z_h)]. (12) + +Apply the inherited complex single-lift inequality (1) separately to +each pair `(a_h,z_h)`. Its `8-|J_h|` unaffected coordinate terms each +cost eight, so subtracting them gives + + sum_(j in J_h) beta(x_j,x_j-a_jh z_h)+beta(Xa_h,z_h) + >= 64-8(8-|J_h|) = 8|J_h|. (13) + +Since disjointness gives `|J|=sum_h |J_h|`, substituting (13) in (12) +proves `C(T,D,Z)>=64`. + +Empty `J_h` cause no exception: then `a_h=0`, `Xa_h=0`, and the +corresponding bracket in (12) is zero, irrespective of `z_h`. Zero +sources also cause no exception, because (1) includes them. There is +no dependence, reality, magnitude, or sign requirement on the nonzero +coefficients or sources. For `k>8`, at most eight of the disjoint sets +can be nonempty; the same argument handles all remaining zero readers. + +## Consequence for exactly two added totals + +Take `k=2`, allowing zero columns as before. If either added reader +lies outside `col_C(X)`, then `q>=1=k-1`. Consequently the cost is at +least 64. Off-column readers are not forbidden as algebraic +factorizations: they may cancel in the quotient when their sources +are dependent. That cancellation cannot lower the cost, because the +dependent-source collapse does not increase it. + +Therefore any exact ten-term factorization (2) with cost **strictly +less than 64** must satisfy all of + + d_1,d_2 in col_C(X), + rank_C(D)=2, + rank_C(Z)=2. (14) + +This is a necessary condition, not existence of such a factorization. +The first line follows because otherwise condition 3 applies. The +second and third lines follow from conditions 2 and 1, since matrices +with two columns have rank at most two. + +There is then a unique `8 x 2` complex matrix `A` with `D=XA`; +injectivity of `X` implies `rank_C(A)=2` and + + T=X-ZA^T, + XX^T=X(X-ZA^T)^T+(XA)Z^T. (15) + +Since a strict saving cannot satisfy condition 4, the coordinate +supports of these two columns must also intersect: + + supp(a_1) intersect supp(a_2) != empty. (16) + +Thus the remaining two-total question can be confined to full-rank +`A` and `Z` in (15), with overlapping coordinate supports for the +columns of `A` and arbitrary complex entries. The overlap in (16) +is a necessary condition, not evidence of a saving: it says that +at least one retained coordinate source is affected by both added +totals. Cost is not invariant under arbitrary mixing of their two +columns: such mixing can change individual supports and beta costs. +Nonzero rescalings and permutations alone preserve cost. + +## Scope and remaining obligations + +The result does **not** prove a bound for the remaining case (15) +with `rank_C(A)=rank_C(Z)=2` and overlapping column supports of `A`. +For `k>=3`, an off-column reader alone need not give `q>=k-1`; no +such stronger claim follows from (10). +Nor is a general complex-to-real support transfer for multiple totals +claimed. The inherited complex extension is used only through the +single-lift inequality, either after collapse or separately for each +disjoint coordinate group. + +The result assumes exact equality on all entries and retention of +the eight coordinate readers. It does not cover masked equality +with free correction terms, arbitrary reader changes, other +geometries, or interacting/nonlinear copy programs. Independent +nonzero rescalings of the retained coordinate readers can be absorbed +into their source columns without changing supports, but arbitrary +mixing cannot. + +Before applying this lower bound, preparation, source access, frame +changes, cleanup/restoration, hosting and recursive-child work are +all optimistically granted zero additional cost. Even under that +relaxation, the covered cases cannot lower the separate-total +copy-rank sum. Savings in other cost components or rank distribution +at equal sum are not excluded. The physical interpretation still +inherits **DreamingOfClouds' PR446** separate-total copy-tree +assumptions; no physical compiler, all-size multiplication theorem, +new supplier, kappa, or runtime improvement is supplied here. + +The general complex-parameter proof is the written argument above. +Finite exact fixtures can check identities, quotient ranks and the +claimed failure modes; they are not an exhaustive search of complex +parameters and do not replace that proof or the pinned predecessor +premises. Substantial OpenAI Codex assistance was used; delegated AI +review is not independent human review. diff --git a/research/p112-two-total-rank-one-seed21/README.md b/research/p112-two-total-rank-one-seed21/README.md new file mode 100644 index 0000000000..1124da18d4 --- /dev/null +++ b/research/p112-two-total-rank-one-seed21/README.md @@ -0,0 +1,154 @@ +# Two extra P112 totals need independent, overlapping coordinate lifts + +**Scoped negative result; no new kappa.** In an exact ten-term P112 decoder +retaining the eight coordinate readers, adding two totals cannot lower the +pairing-rank copy cost below **64** if either added matrix has rank at most +one, if either added reader leaves the coordinate column space, or if the +two coordinate coefficient supports are disjoint. + +Consequently any improvement in this model must have both added matrices +of rank two, both added readers inside `col_C(X)`, and **overlapping** +coefficient supports. The full coupled case with arbitrary source columns remains unresolved +by this package. The result +closes off-column cancellation and independent batching as ways around +Mihir Srivastava's #845 / @woklerx's #998 single-lift floor; it does not +claim a floor for every ten-term decoder. + +The [proof](PROOF.md) gives two generalizations for any number `k` of +added totals: quotient rank `rank([X D])-8 >= k-1` forces source rank at +most one, and pairwise disjoint coefficient supports cannot help even +with independent sources. These are written complex-parameter arguments, +not conclusions drawn from finite search. + +## Reproduce + +From the repository root, Python 3.10+ and the standard library: + +```sh +python3 -I -S -B research/p112-two-total-rank-one-seed21/test_package.py +``` + +Expected final status: + +```text +PASS_P112_TWO_TOTAL_PACKAGE controls=8 identities=1180 +``` + +This read-only command checks pinned inputs, replays both retained #845 +checkers and #998's primary/independent checks, reproduces the new primary +and independent receipts, and runs optimized, mutation and relocation +controls. On the recorded macOS host the recorded run took 43 seconds; +actual timing is in [VALIDATION.json](VALIDATION.json). + +For a quick new-result replay without the predecessor census: + +```sh +python3 -I -S -B research/p112-two-total-rank-one-seed21/verify.py +python3 -I -S -B research/p112-two-total-rank-one-seed21/independent_check.py +``` + +The main marker reports **15 examples, nine mathematical controls**, and +`coupled_rank_two=open`. The independent checker emits deterministic JSON, +compared in full to `INDEPENDENT.json` by the package command. The main +certificate can be regenerated with `verify.py --write /new/file.json`; +existing outputs are not overwritten. `--check PATH` compares every field. + +## Exact model and useful boundary + +Write `X` for the pinned real `112 x 8` coordinate matrix. The identity is + +```text +XX^T = XT^T + DZ^T, +D,Z have two columns; transpose is algebraic, without conjugation. +``` + +Cost is the sum of the binary label-pairing ranks of the ten reader/source +support rectangles. In the remaining case, `D=XA` uniquely and +`T=X-ZA^T`; both `A` and `Z` must have rank two. Arbitrary complex values +and zero terms are included in the theorem. + +Mixing the two added terms by an invertible basis change preserves the +matrix identity but need not preserve this cost. An exact fixture retires +two coordinates with cost **64**; the sum/difference basis of those same +two terms costs **66**. Thus normalizing `A` by arbitrary column mixing +cannot be treated as free when searching the remaining case. + +## Evidence and limits + +- Primary: 15 full P112 identities, exact Gaussian-rational rank by rational + realification, literal restricted binary-pairing ranks, rank-one + contractions, disjoint complex lifts, and boundary examples at `k=3,4`. +- Independent: no primary or predecessor Python imports; pinned geometry + JSON, rational column elimination, set-based binary elimination, **1,180 + full matrix identities** including **322 transposes** and **476 component + identities**. All 28 coordinate pairs and all 210 unordered disjoint + two-plus-two support partitions are completed. Dense overlapping controls + are explicitly outside the proved reductions. +- Mathematical controls include source perturbation, omitted terms, + conjugate transpose, improper rank-one contraction, non-free basis + change, and a `k=3,q=1` exact example showing that one off-column reader + alone does not force source rank one for three totals. +- Packaging controls reject four changed receipt fields and source drift, + preserve existing output, reproduce identical certificate bytes, and run + in a minimal offline tree whose path contains spaces. Guards survive `-O`. + +The finite examples exercise the proof boundaries. They are not an +exhaustive complex-parameter search, a formal proof, or independent human +review. The uniform statements depend on the inherited #845/#998 theorem; +its finite premises are replayed and source-bound, not claimed as new work. + +Before physical synthesis, all extra preparation, source access, frames, +restoration, hosting and recursive-child work are optimistically granted +zero cost. Even that relaxation cannot lower the copy-rank **sum** in the +covered classes, so no physical implementation is pursued. Rank distribution +at the same sum and other cost components may still improve the recursive +moment. This is not a complete moment or runtime obstruction. + +The physical interpretation retains DreamingOfClouds' #446 separate-total, +drop-free gathering/copy-tree assumptions. Masked equality, changed retained +readers, other geometries, interacting delivery programs and the coupled +rank-two case remain outside scope. All-size/compiler, mutable-source, +hosting, precision/tape, analytic-transfer and bit H1-H5 obligations are +unchanged. No selected supplier, native admission, full cold replay, Lean +multiplication theorem, hosted CI result or new exponent is claimed. + +## Provenance and overlap + +Base: `1b59b624d21924f8e3537cdc1ac52d3be6eda2fe`; OS assignment seed **21**, +complex-supplier track. The selected result at this base is Rohan Arun's +#1094, conditional kappa **0.001672660197076918**, with PR589/PR555 on the +bit side. Its selected record, source inventory, assembly and maintainer +review were followed; they are context, not runtime inputs for this result. + +[SOURCES.json](SOURCES.json) records immutable SHA-256 and Git-blob pins for +the full two predecessor packages. #845 head is +`125ce25bdae421627b56077adc14940c2d0aa52f`; #998 head is +`66b777bf2b0160ed926572ff8714ac7b7bba0859`. Both are incorporated in the base +review ledger. #1133's pending rational descent extends #998 in the scalar +field, while this result changes the number of added totals. #968/#1077 +concern exactly eight terms with changed readers; #1098 verifies a +predecessor geometry premise. No pending code is imported. + +At the final overlap check, @woklerx's **#1180**, head +`75b408646d558147a4eb250fc407d1fbfcb8df4e`, had appeared. Its written theorem +covers arbitrary term counts and punctures, but requires **both** factor +matrices to lie in the live root code. Within our `D=XA` subcase, the scopes overlap when +`Z` also lies in `col(X)` (and hence so does `T`). Our distinct coverage permits arbitrary source +columns outside that space, off-column canceling readers, and disjoint lifts +with independent outside sources. In `CERTIFICATE.json`, the disjoint complex +fixtures have `source_quotient_rank=2` and `1` respectively; #1180's hypothesis +therefore does not apply. Conversely our theorem retains eight coordinate +readers and does not subsume #1180's variable-reader result. This is a scoped +comparison of its pinned proof, not a complete independent acceptance of +#1180 or an imported dependency. Its factor-linear subcase is not claimed +as an unanswered research question here. + +[CLAIM.md](CLAIM.md) records the three candidate tasks, assignment, +zero-extra-cost screen, coordination check and stopping rule. +[VALIDATION.json](VALIDATION.json) records final overlap and executed checks. +Only this new research package changes; `upstream/`, the selected frontier, +source archives and predecessor evidence remain unchanged. + +Prepared by **Philipp / @mightyOil**, with substantial **OpenAI Codex** +assistance in analysis, proof, code, independent AI checks and writing. +See [NOTICE.md](NOTICE.md) for predecessor credit. Apache-2.0. diff --git a/research/p112-two-total-rank-one-seed21/SOURCES.json b/research/p112-two-total-rank-one-seed21/SOURCES.json new file mode 100644 index 0000000000..6e21983a19 --- /dev/null +++ b/research/p112-two-total-rank-one-seed21/SOURCES.json @@ -0,0 +1,112 @@ +{ + "base_commit": "1b59b624d21924f8e3537cdc1ac52d3be6eda2fe", + "inputs": { + "research/p112-complex-single-lift/CLAIM.md": { + "git_blob": "5cc7ea45440dd687eab3d05f9a3ae3ad1ba10f8b", + "sha256": "3f800921504dd2e96b04f64395732b06ff62e6201c7c18f418335093808764f4" + }, + "research/p112-complex-single-lift/INDEPENDENT.json": { + "git_blob": "82e026a894fa7e401e5ae71d0cc47f893c2cd1c3", + "sha256": "97a51584e58c27dda0442129767681585eff2f4899e71204775d606c02b4f53a" + }, + "research/p112-complex-single-lift/NOTICE.md": { + "git_blob": "68d68674a5cf4dbc6216751ef70a091169bb4a20", + "sha256": "d51e48f42c11a931a24ea0b6c1f8d537d03c1afaa3c2f2113ac6aea9d6529631" + }, + "research/p112-complex-single-lift/PROOF.md": { + "git_blob": "ccbd30f7bc776a88b0591c03d7020075ba3fd8a4", + "sha256": "66b16fa65af3eb105983ad995bf6b6047b305906cdb1786fe1ef18c3cad8daad" + }, + "research/p112-complex-single-lift/README.md": { + "git_blob": "2014d46ed0649d63c5dc32d944ea5227d28989ed", + "sha256": "b83e98ba58eba2ce593fc85465a84a7a9e4f0e8f210feed5b43403f6c2bca5a8" + }, + "research/p112-complex-single-lift/RESULTS.json": { + "git_blob": "69d3fd935333b015298e03a3e80cd4c570dfd63c", + "sha256": "108ada330cc1b1dee3bb261239854200606e2d7224b1aa17d978316a09aea429" + }, + "research/p112-complex-single-lift/REVIEW.md": { + "git_blob": "4d34ec60d484c092fac5750e185ed8f985bc7f6a", + "sha256": "acd719a184897a4a097cf5b6c5c144383002805ae50b2c4ddcf423ba3f10f8f1" + }, + "research/p112-complex-single-lift/SOURCES.json": { + "git_blob": "544c4e4ad68168aa96796f6dea45bfb8dd59460a", + "sha256": "145ef2c832157be6dee907fdb7ad6d314fa00f406ba1edcd5b90f8d759ea0006" + }, + "research/p112-complex-single-lift/VALIDATION.json": { + "git_blob": "610d7c6569908ca5d67a918687464a44501da401", + "sha256": "cc366215d15577dcae2657ca95fc04c230b168e2a900e55b96bd347cad4987a9" + }, + "research/p112-complex-single-lift/independent_check.py": { + "git_blob": "20e59462ff5bef81c87da62b8093ca9e7b9143cd", + "sha256": "2244bc6a4d38ae820a62d87672e3a010f33b03c870a25ce08de7b620bdfb6380" + }, + "research/p112-complex-single-lift/verify.py": { + "git_blob": "71d3471bb20cb531718aa43123228e829f6f47f6", + "sha256": "79ef22aa0a7d30e0467b50293805d6652991e60fc66e11deb97a24a4cd5bd771" + }, + "research/p112-single-lift/CLAIM.md": { + "git_blob": "018ce860b6e5a0add12c7f536c3c76569a1313b3", + "sha256": "9962399c8b4c79b801cd9b7958390c7bc250696cd86bfc897b9a062a8e4ac357" + }, + "research/p112-single-lift/NOTICE.md": { + "git_blob": "eb811ef7e601441f07c996fa3a265639b354eb8f", + "sha256": "54fcd00460fed3afecad295c0e8310cc1f44d00a21c9ac2872be8c4e3ca26dbe" + }, + "research/p112-single-lift/PROOF.md": { + "git_blob": "609a2b1f83f17523a570a1a2e1731817c87a587a", + "sha256": "02147aa2a93a449dcbd15886b42d993bd0dbb554d7c15d347a9567fbe2a442e1" + }, + "research/p112-single-lift/README.md": { + "git_blob": "41ee5713cd31f82b3a2882a178b03ed8fbede436", + "sha256": "b0aa432b38e6317661d4edfe5fa37c377cff937a527fe83a55261e7202ce2442" + }, + "research/p112-single-lift/RESULTS.json": { + "git_blob": "be204ad0bb27dda715acc3e01fbe7ad6ddc1e010", + "sha256": "0947e7380f931dc8e447751b9b33d531a1ced92a6b94225be7ea29ea57497c05" + }, + "research/p112-single-lift/SOURCES.json": { + "git_blob": "a36ad2fa75d5f2bbce60997a4caa21b0f12786c3", + "sha256": "3895e1e5d97987d760fca7ef124cccabcfe5a675ce2928c1c9b2de1f48bb7667" + }, + "research/p112-single-lift/VALIDATION.json": { + "git_blob": "b4bd7db494afdc59d536ea87c4319809ef0c589d", + "sha256": "a6a470faad34810db0cf3c9bd518b7ee8fd61be7e5dff47d865cb8732a85f2eb" + }, + "research/p112-single-lift/geometry.py": { + "git_blob": "34c1abf059d7be5fe5e5044cf01a09b843071c68", + "sha256": "3857c11ec731a602b8059d85d58fbb3b641bab687bb33016a0e54f7567752c8a" + }, + "research/p112-single-lift/independent_check.py": { + "git_blob": "dec55ff6c048c8aa2e4c9bc274345c56d8c016d6", + "sha256": "9d74b6fde539f82c31fda88074c7c2dd0465f9892ed61b8d13b5dae0fbf5d29b" + }, + "research/p112-single-lift/reference-geometry.json": { + "git_blob": "d862663d3c0ffe3c72df510e89997beb85cef640", + "sha256": "4f44af368e046002553d632ee90c6470990827cea3fae41f0f54018522d7a080" + }, + "research/p112-single-lift/reference/PR717-NOTICE.md": { + "git_blob": "481f6bf99bb19c7f2f73b0991a751b6b9187b16c", + "sha256": "7809c20cd037dcc29edb5207cbc333bed7b2bd1026cb4f1137f150de90d6866d" + }, + "research/p112-single-lift/reference/pr717_e8model.py": { + "git_blob": "489a3e2c12e58c0e824eb6c49f5168ddc6756085", + "sha256": "7255d13ef349e7a549c0f26addf35ef72d28c72343f3abfcbab2f5eba74834a5" + }, + "research/p112-single-lift/verify.py": { + "git_blob": "b7a81ad2f5beb21cd5595b93c0c07b467a3a9715", + "sha256": "8da963c33c5d09f1f23437cd89cb9c05f397ac1cddae49d3dc47b2d719555546" + } + }, + "predecessors": { + "845": "125ce25bdae421627b56077adc14940c2d0aa52f", + "998": "66b777bf2b0160ed926572ff8714ac7b7bba0859" + }, + "selected_context": { + "kappa": "836330098538459/500000000000000000", + "not_runtime_dependency": true, + "record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "review": "docs/research/community-batch1099-review.md", + "source_pr": 1094 + } +} diff --git a/research/p112-two-total-rank-one-seed21/VALIDATION.json b/research/p112-two-total-rank-one-seed21/VALIDATION.json new file mode 100644 index 0000000000..ee3345bcb1 --- /dev/null +++ b/research/p112-two-total-rank-one-seed21/VALIDATION.json @@ -0,0 +1,71 @@ +{ + "artifact_sha256": { + "CERTIFICATE.json": "2b154c9df7452d1d102dcebc0b9f1d822ba3d8e5ddbc9c17b13c17013b49dcfe", + "INDEPENDENT.json": "746b19c5e8d3b28809377c884656811e0ec093504f063c972a6e9e59db8be9ff", + "PROOF.md": "7209dd082f47dca3d096ceb30b9efd674d6332d5ca0e4decd22337b0b3b87d6f", + "independent_check.py": "25ec6df7449ee8cbe4c31f963c425da9650077cdd9c540432cbe7acb9b72c472", + "test_package.py": "0d9acaed7c0c09bcd30f3e80ab638391ce8e7c1287821ec9742a7407b5cad106", + "verify.py": "01945dbb1c57ff9130258d82c8565d1f75e8ec4322856aba81fe090fca9f6f30" + }, + "base_commit": "1b59b624d21924f8e3537cdc1ac52d3be6eda2fe", + "checked_at_utc": "2026-10-13T19:55:48.783818+00:00", + "initial_attempt": { + "resolution": "Complete all edits before the final run; unchanged guard passed. No mathematical check was weakened.", + "status": "package preservation guard rejected concurrent documentation edits" + }, + "no_new_kappa": true, + "not_run": [ + "repository-wide historical suite", + "selected supplier cold replay", + "native/global hosting admission", + "Lean", + "hosted CI" + ], + "overlap_refresh": { + "discussions_checked": [ + 1163, + 1166, + 1167 + ], + "latest_number_seen": 1186, + "main_head": "1b59b624d21924f8e3537cdc1ac52d3be6eda2fe", + "nearby_prs": { + "1133": "8301a4698152cf63d3b4992145ecc8621942a6cd", + "845": "125ce25bdae421627b56077adc14940c2d0aa52f", + "998": "66b777bf2b0160ed926572ff8714ac7b7bba0859" + }, + "nearest_concurrent": { + "author": "woklerx", + "head": "75b408646d558147a4eb250fc407d1fbfcb8df4e", + "pr": 1180, + "scope_comparison": "Both factor matrices in root code, arbitrary term counts. Our arbitrary outside-source and canceling outside-reader cases are outside that hypothesis; no pending code imported." + }, + "new_claim": "PR279 provenance reconciliation by adamgall; unrelated", + "open_pr_count": 798, + "pinned_coordination_issue": null + }, + "package_replay": { + "command": "python3 -I -S -B research/p112-two-total-rank-one-seed21/test_package.py", + "exit_code": 0, + "platform": "macOS-27.0.1-arm64-arm-64bit-Mach-O", + "python": "3.14.7", + "seconds": 43.026, + "stderr": "", + "stdout": "PASS_P112_SINGLE_LIFT: 511 support certificates; 3272 sign cases; 128 conflicting kernels; 9 negative controls; copy cost >= 64\nPASS_P112_SINGLE_LIFT_INDEPENDENT: 511 nonzero integer minors; 3272 set-rank replays; 128 incompatible kernels; 4 arithmetic controls\nPASS_P112_COMPLEX_SINGLE_LIFT_INDEPENDENT: 460 exact cases; 4140 support pairs; 460 cost vectors; 56 entrywise identities; 6 controls\nPASS_P112_COMPLEX_SINGLE_LIFT: 14 exact projections; 8 negative controls; identical term costs; floor 64\nPASS_P112_TWO_TOTAL_REDUCTION examples=15 controls=9 floor=64 coupled_rank_two=open no_new_kappa\nPASS_P112_TWO_TOTAL_PACKAGE controls=8 identities=1180\n{\"packaging_controls\": [\"reject_receipt_examples\", \"reject_receipt_assignment_seed\", \"reject_receipt_no_new_kappa\", \"reject_receipt_quotient_rank\", \"preserve_existing_output\", \"byte_identical_regeneration\", \"minimal_offline_relocation_with_spaces\", \"reject_source_drift_before_import\"]}\n" + }, + "review": { + "findings_resolved": [ + "State each inherited coordinate beta is eight explicitly", + "Qualify basis mixing: rescaling/permutation preserve cost", + "Scope PR1180 overlap by both reader and source membership" + ], + "type": "delegated AI mathematical and implementation review, not human or formal review" + }, + "selected_record_check": { + "command": "make selected-record-check", + "exit_code": 0, + "output": "PASS selected record, exact kappa, original source inventory and proof supplement: 836330098538459/500000000000000000" + }, + "source_inputs_unchanged": true, + "status": "PASS local verification" +} diff --git a/research/p112-two-total-rank-one-seed21/independent_check.py b/research/p112-two-total-rank-one-seed21/independent_check.py new file mode 100644 index 0000000000..7774fd3bb0 --- /dev/null +++ b/research/p112-two-total-rank-one-seed21/independent_check.py @@ -0,0 +1,293 @@ +#!/usr/bin/env python3 +"""Independent exact controls for rank-one and disjoint-support reductions. + +Only the pinned predecessor JSON is consumed: no primary or predecessor Python +is imported. The universal reduction and inherited floor are written proofs; +these fixtures exercise their hypotheses, identities, and scope boundaries. +Apache-2.0; substantial OpenAI Codex assistance, not human-only review. +""" + +from fractions import Fraction +from hashlib import sha256 +from itertools import combinations +import json +from pathlib import Path +import random + + +HERE = Path(__file__).resolve().parent +GEOMETRY = HERE.parent / "p112-single-lift" / "reference-geometry.json" +GEOMETRY_SHA256 = "4f44af368e046002553d632ee90c6470990827cea3fae41f0f54018522d7a080" + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def rational_rank(columns): + """Column rank by a fresh rational echelon basis; no floating point.""" + basis = {} + for column in columns: + v = list(map(Fraction, column)) + for p in sorted(basis): + if v[p]: + coefficient = v[p] + v = [a - coefficient * b for a, b in zip(v, basis[p])] + pivot = next((i for i, a in enumerate(v) if a), None) + if pivot is not None: + denominator = v[pivot] + basis[pivot] = [a / denominator for a in v] + return len(basis) + + +def binary_rank(rows): + """Rank over F2 by set symmetric difference, separate from Q arithmetic.""" + basis = {} + for row in rows: + v = set(row) + while v: + p = min(v) + if p not in basis: + basis[p] = v + break + v.symmetric_difference_update(basis[p]) + return len(basis) + + +def pair(u, v): + return (u & v).bit_count() % 2 + + +def beta(left, right, labels, duals): + target = [i for i, v in enumerate(right) if v] + return binary_rank( + {j for j in target if pair(duals[i], labels[j])} + for i, value in enumerate(left) if value + ) + + +def add(a, b): + return [u + v for u, v in zip(a, b)] + + +def subtract(a, b): + return [u - v for u, v in zip(a, b)] + + +def identity(left, right, gram): + require(len(left) == len(right), "factor count") + n = len(gram) + require(all(len(v) == n for v in left + right), "factor length") + return all(sum(d[i] * z[j] for d, z in zip(left, right)) == gram[i][j] + for i in range(n) for j in range(n)) + + +def gaussian_identity(left, right, gram, conjugate=False): + """Full matrix equality in Z[i], represented by integer coefficient pairs.""" + for i in range(len(gram)): + for j in range(len(gram)): + real = imag = 0 + for d, z in zip(left, right): + a, b = d[i] + c, e = z[j] + if conjugate: + e = -e + real += a * c - b * e + imag += a * e + b * c + if (real, imag) != (gram[i][j], 0): + return False + return True + + +def main(): + raw = GEOMETRY.read_bytes() + require(sha256(raw).hexdigest() == GEOMETRY_SHA256, "pinned geometry hash") + data = json.loads(raw) + x, labels, duals = data["X"], data["labels"], data["duals"] + n = len(x) + require(n == len(labels) == len(duals) == 112, "112 ports") + require(all(len(row) == 8 for row in x), "eight fixed coordinates") + columns = [list(c) for c in zip(*x)] + require(rational_rank(columns) == 8, "full coordinate rank") + gram = [[sum(a * b for a, b in zip(r, s)) for s in x] for r in x] + for i in range(n): + for j in range(n): + root_dot = sum(a * b for a, b in zip(data["roots"][i], data["roots"][j])) + require(root_dot % 4 == 0 and gram[i][j] * 2 == root_dot, + "exact root Gram identity") + require(pair(duals[i], labels[j]) == (1 + root_dot // 4) % 2, + "all-entry binary pairing geometry") + require([beta(c, c, labels, duals) for c in columns] == [8] * 8, + "baseline cost is 64") + + rng = random.Random(21) + pairs = list(combinations(range(8), 2)) + rng.shuffle(pairs) + port = rng.randrange(n) + unit = [int(i == port) for i in range(n)] + require(rational_rank(columns + [unit]) == 9, "chosen port outside col(X)") + zero = [0] * n + counts = {"rank_one_reader": 0, "rank_one_source_outside_readers": 0, + "rank_two_disjoint_axes": 0, "rank_two_dense_overlap_control": 0, + "rank_two_disjoint_pairs": 0, "transposed_identities": 0, + "rejected_source_perturbations": 0, "rejected_omitted_terms": 0} + observed_costs = {} + disjoint_component_costs = set() + disjoint_checks = 0 + checks = 0 + + def check_factors(name, t, d, z, ranks, quotient, merged=None): + nonlocal checks + require(rational_rank(d) == ranks[0] and rational_rank(z) == ranks[1], + name + " exact reader/source ranks") + require(rational_rank(columns + d) - 8 == quotient, + name + " quotient rank") + require(identity(columns + d, t + z, gram), name + " all-entry identity") + checks += 1 + require(identity(t + z, columns + d, gram), name + " transposed identity") + checks += 1 + counts["transposed_identities"] += 1 + original_extra = sum(beta(a, b, labels, duals) for a, b in zip(d, z)) + coordinate_cost = sum(beta(a, b, labels, duals) for a, b in zip(columns, t)) + if merged is not None: + reader, source = merged + require(identity(columns + [reader], t + [source], gram), name + " merge identity") + checks += 1 + merged_cost = beta(reader, source, labels, duals) + require(merged_cost <= original_extra, name + " beta contraction") + require(coordinate_cost + merged_cost >= 64, name + " inherited floor fixture") + total = coordinate_cost + original_extra + observed_costs.setdefault(name, set()).add(total) + counts[name] += 1 + return total + + def check_disjoint_components(supports, sources, combined_cost): + nonlocal checks, disjoint_checks + require(not set(supports[0]) & set(supports[1]), "disjoint coefficient supports") + component_costs = [] + for support, source in zip(supports, sources): + reader = [sum(columns[j][i] for j in support) for i in range(n)] + component_t = [subtract(c, source) if j in support else c + for j, c in enumerate(columns)] + require(identity(columns + [reader], component_t + [source], gram), + "single-lift component all-entry identity") + checks += 1 + cost = sum(beta(c, z, labels, duals) for c, z in zip(columns, component_t)) + cost += beta(reader, source, labels, duals) + require(cost >= 64, "single-lift component floor fixture") + component_costs.append(cost) + require(combined_cost == sum(component_costs) - 64 >= 64, + "disjoint costs combine after subtracting one baseline") + disjoint_component_costs.update(component_costs) + disjoint_checks += 1 + + for a, b in pairs: + ca, cb = columns[a], columns[b] + t = [c[:] for c in columns] + t[a] = subtract(ca, cb) + # Two independent readers whose quotient components cancel exactly. + d, z = [unit, subtract(ca, unit)], [cb, cb] + check_factors("rank_one_source_outside_readers", t, d, z, (2, 1), 1, (ca, cb)) + # Rank-one readers with individually non-coordinate source components. + check_factors("rank_one_reader", t, [ca, ca], [unit, subtract(cb, unit)], + (1, 2), 0, (ca, cb)) + # Outside rank-one collapse, but covered by disjoint coefficient supports. + inside_t = [c[:] for c in columns] + inside_t[a], inside_t[b] = zero[:], zero[:] + inside_cost = check_factors("rank_two_disjoint_axes", inside_t, [ca, cb], [ca, cb], + (2, 2), 0) + check_disjoint_components(([a], [b]), [ca, cb], inside_cost) + # a1=e_a+e_b and a2=e_a-e_b overlap in both coordinates. Both D + # and Z have rank two, quotient rank zero: outside both reductions. + dense_t = [c[:] for c in columns] + dense_t[a] = [-v for v in cb] + dense_t[b] = subtract(add(cb, cb), ca) + check_factors("rank_two_dense_overlap_control", dense_t, + [add(ca, cb), subtract(ca, cb)], [ca, cb], (2, 2), 0) + perturbed = [v[:] for v in z] + perturbed[0][(port + 1) % n] += 1 + require(not identity(columns + d, t + perturbed, gram), "reject perturbed source") + counts["rejected_source_perturbations"] += 1 + require(not identity(columns + d[:1], t + z[:1], gram), "reject omitted term") + counts["rejected_omitted_terms"] += 1 + + # All unordered 2+2 disjoint coefficient-support partitions: C(8,4)*3=210. + # Both readers use two coordinates, so these are not axis-only examples. + for four in combinations(range(8), 4): + for partner in four[1:]: + left_support = [four[0], partner] + right_support = [j for j in four if j not in left_support] + supports = [left_support, right_support] + readers = [[sum(columns[j][i] for j in support) for i in range(n)] + for support in supports] + sources = [columns[support[0]] for support in supports] + disjoint_t = [c[:] for c in columns] + for support, source in zip(supports, sources): + for j in support: + disjoint_t[j] = subtract(columns[j], source) + cost = check_factors("rank_two_disjoint_pairs", disjoint_t, readers, sources, + (2, 2), 0) + check_disjoint_components(supports, sources, cost) + require(counts["rank_two_disjoint_pairs"] == 210 and disjoint_checks == 238, + "complete finite disjoint-support fixture domain") + + # k=3 and quotient rank k-1: all three sources collapse to one. + second = next([int(i == p) for i in range(n)] for p in range(n) + if rational_rank(columns + [unit, [int(i == p) for i in range(n)]]) == 10) + a, b = pairs[0] + ca, cb = columns[a], columns[b] + t = [c[:] for c in columns] + t[a] = subtract(ca, cb) + three_d = [unit, second, subtract(subtract(ca, unit), second)] + require(rational_rank(three_d) == 3 and rational_rank(columns + three_d) - 8 == 2, + "k=3 exact quotient rank") + require(rational_rank([cb, cb, cb]) == 1 and identity(columns + three_d, t + [cb] * 3, gram), + "k=3 exact source rank and identity") + require(beta(ca, cb, labels, duals) + <= sum(beta(v, cb, labels, duals) for v in three_d), "k=3 beta contraction") + checks += 1 + + # Boundary rank zero and quotient rank two with zero sources. + require(identity(columns + [unit, second], columns + [zero, zero], gram), "zero source boundary") + require(rational_rank([zero, zero]) == 0 and rational_rank(columns + [unit, second]) == 10, + "zero source boundary ranks") + require(identity(columns + [zero, zero], columns + [unit, second], gram), "zero reader boundary") + checks += 2 + + # Scale one added reader by i and its source by -i. Bilinear transpose + # preserves the identity, whereas substituting adjoint reverses its sign. + real_vector = lambda v: [(value, 0) for value in v] + complex_left = list(map(real_vector, columns)) + [[(0, v) for v in ca], real_vector(zero)] + complex_right = list(map(real_vector, t)) + [[(0, -v) for v in cb], real_vector(zero)] + require(gaussian_identity(complex_left, complex_right, gram), "Gaussian-integer bilinear identity") + require(not gaussian_identity(complex_left, complex_right, gram, conjugate=True), + "reject conjugate-transpose substitution") + checks += 1 + print(json.dumps({ + "status": "pass", + "scope": "independent exact finite fixtures; universal proof remains in PROOF.md", + "seed": 21, + "source_geometry_sha256": GEOMETRY_SHA256, + "coordinate_pairs": len(pairs), + "outside_port": port, + "full_matrix_identities": checks, + "entries_per_identity": n * n, + "controls": counts, + "observed_total_costs": {k: sorted(v) for k, v in observed_costs.items()}, + "disjoint_support_controls": { + "axis_pairs": 28, + "two_plus_two_partitions": 210, + "component_identity_count": 2 * disjoint_checks, + "component_costs": sorted(disjoint_component_costs), + "combined_cost_rule": "component_1 + component_2 - 64 >= 64" + }, + "outside_both_reductions": "rank_two_dense_overlap_control", + "general_k_control": {"k": 3, "reader_rank": 3, "source_rank": 1, "quotient_rank": 2}, + "zero_boundaries": 2, + "conjugate_transpose_negative_control": "rejected" + }, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/p112-two-total-rank-one-seed21/test_package.py b/research/p112-two-total-rank-one-seed21/test_package.py new file mode 100644 index 0000000000..c1099c5903 --- /dev/null +++ b/research/p112-two-total-rank-one-seed21/test_package.py @@ -0,0 +1,79 @@ +#!/usr/bin/env python3 +"""Reproduce both receipts and adversarial packaging controls, stdlib only. + +Philipp / mightyOil with substantial OpenAI Codex assistance. Apache-2.0. +""" +from hashlib import sha256 +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +HERE=Path(__file__).resolve().parent +ROOT=HERE.parents[1] + + +def require(ok,message): + if not ok: + raise ValueError(message) + + +def run(script,*args,optimized=False,success=True): + cmd=[sys.executable,'-I','-S','-B']+(['-O'] if optimized else [])+[str(script),*map(str,args)] + p=subprocess.run(cmd,capture_output=True,text=True) + require((p.returncode==0)==success,'unexpected subprocess result: '+str(cmd)+'\n'+p.stdout+p.stderr) + return p + + +def main(): + before={p:sha256(p.read_bytes()).hexdigest() for p in HERE.iterdir() if p.is_file()} + main_result=run(HERE/'verify.py','--with-predecessors') + require('PASS_P112_COMPLEX_SINGLE_LIFT:' in main_result.stdout,'missing inherited replay') + require('PASS_P112_SINGLE_LIFT_INDEPENDENT:' in main_result.stdout,'missing inherited independent replay') + run(HERE/'verify.py',optimized=True) + independent=run(HERE/'independent_check.py',optimized=True) + require(json.loads(independent.stdout)==json.loads((HERE/'INDEPENDENT.json').read_text()),'independent receipt mismatch') + checks=[] + with tempfile.TemporaryDirectory(prefix='p112 two total ') as scratch: + temp=Path(scratch) + expected=json.loads((HERE/'CERTIFICATE.json').read_text()) + mutants=[] + for key,value in [('examples',expected['examples'][:-1]),('assignment_seed',22),('no_new_kappa',False)]: + m=dict(expected);m[key]=value;mutants.append((key,m)) + m=json.loads(json.dumps(expected));m['examples'][2]['quotient_rank']=0;mutants.append(('quotient_rank',m)) + for name,mutant in mutants: + target=temp/(name+'.json');target.write_text(json.dumps(mutant)) + p=run(HERE/'verify.py','--check',target,success=False) + require('certificate mismatch' in p.stderr,'wrong failure for '+name) + checks.append('reject_receipt_'+name) + output=temp/'existing.json';output.write_text('preserve me\n') + run(HERE/'verify.py','--write',output,success=False) + require(output.read_text()=='preserve me\n','output clobbered') + checks.append('preserve_existing_output') + regenerated=temp/'regenerated.json';run(HERE/'verify.py','--write',regenerated) + require(regenerated.read_bytes()==(HERE/'CERTIFICATE.json').read_bytes(),'nondeterministic regeneration') + checks.append('byte_identical_regeneration') + relocated=temp/'isolated source tree' + for directory in ('p112-single-lift','p112-complex-single-lift','p112-two-total-rank-one-seed21'): + shutil.copytree(ROOT/'research'/directory,relocated/'research'/directory, + ignore=shutil.ignore_patterns('__pycache__')) + copied=relocated/'research'/HERE.name + run(copied/'verify.py',optimized=True) + p=run(copied/'independent_check.py',optimized=True) + require(json.loads(p.stdout)==json.loads((HERE/'INDEPENDENT.json').read_text()),'relocated independent result') + checks.append('minimal_offline_relocation_with_spaces') + source=relocated/'research/p112-single-lift/geometry.py' + source.write_bytes(source.read_bytes()+b'\n# source mutation\n') + p=run(copied/'verify.py',success=False) + require('source hash:' in p.stderr,'source mutation not rejected at admission') + checks.append('reject_source_drift_before_import') + require(all(sha256(p.read_bytes()).hexdigest()==digest for p,digest in before.items()),'default checks modified package') + print(main_result.stdout.strip()) + print('PASS_P112_TWO_TOTAL_PACKAGE controls='+str(len(checks))+' identities='+str(json.loads(independent.stdout)['full_matrix_identities'])) + print(json.dumps({'packaging_controls':checks},sort_keys=True)) + + +if __name__=='__main__': + main() diff --git a/research/p112-two-total-rank-one-seed21/verify.py b/research/p112-two-total-rank-one-seed21/verify.py new file mode 100644 index 0000000000..9a53f2f6c6 --- /dev/null +++ b/research/p112-two-total-rank-one-seed21/verify.py @@ -0,0 +1,338 @@ +#!/usr/bin/env python3 +"""Exact boundary evidence for PROOF.md, not a proof of its quantifiers. + +Philipp / mightyOil, with substantial OpenAI Codex assistance. Apache-2.0. +Only the standard library is required. All guards survive -O. +""" +import argparse +from collections import Counter +from fractions import Fraction +from hashlib import sha256 +import importlib.util +from itertools import combinations +import json +from pathlib import Path +import subprocess +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SEED = 21 +ZERO = (0, 0) +ONE = (1, 0) +I = (0, 1) + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def add(a, b): + return (a[0] + b[0], a[1] + b[1]) + + +def neg(a): + return (-a[0], -a[1]) + + +def mul(a, b): + return (a[0]*b[0]-a[1]*b[1], a[0]*b[1]+a[1]*b[0]) + + +def plus(a, b): + return [add(x, y) for x, y in zip(a, b)] + + +def minus(a, b): + return plus(a, [neg(v) for v in b]) + + +def scale(a, c): + return [mul(v, c) for v in a] + + +def linear(columns, coefficients): + result = [ZERO] * len(columns[0]) + for col, c in zip(columns, coefficients): + result = plus(result, scale(col, c)) + return result + + +def rank_q(rows): + basis = {} + for original in rows: + row = list(map(Fraction, original)) + for p, pivot in sorted(basis.items()): + c = row[p] + if c: + row = [a-c*b for a, b in zip(row, pivot)] + p = next((j for j, a in enumerate(row) if a), None) + if p is not None: + basis[p] = [a/row[p] for a in row] + return len(basis) + + +def rank_c(columns): + """Exact Q-rank of realification is twice Q(i)-rank.""" + if not columns: + return 0 + rows = list(zip(*columns)) + block = [[z[0] for z in row]+[-z[1] for z in row] for row in rows] + block += [[z[1] for z in row]+[z[0] for z in row] for row in rows] + r = rank_q(block) + require(r % 2 == 0, 'odd realification rank') + return r // 2 + + +def rank_f2(rows): + pivots = {} + for row in rows: + while row: + p = row.bit_length()-1 + if p in pivots: + row ^= pivots[p] + else: + pivots[p] = row + break + return len(pivots) + + +def beta(d, z, geometry): + """Build the actual restricted pairing matrix, not a support-size proxy.""" + sources = [j for j, a in enumerate(z) if a != ZERO] + rows = [sum(((geometry['duals'][i] & geometry['labels'][j]).bit_count() % 2) << k + for k, j in enumerate(sources)) + for i, a in enumerate(d) if a != ZERO] + return rank_f2(rows) + + +def outer_sum(readers, sources): + n = len(readers[0]) + rr, ii = [[0]*n for _ in range(n)], [[0]*n for _ in range(n)] + for d, z in zip(readers, sources): + ds = [(j, a) for j, a in enumerate(d) if a != ZERO] + zs = [(j, a) for j, a in enumerate(z) if a != ZERO] + for j, a in ds: + for k, b in zs: + c = mul(a, b) + rr[j][k] += c[0] + ii[j][k] += c[1] + return rr, ii + + +def require_identity(x, t, d, z): + n = len(x[0]) + require(len(x) == len(t) == 8 and len(d) == len(z), 'term count') + require(all(len(c) == n for c in x+t+d+z), 'port count') + require(outer_sum(x+d, t+z) == outer_sum(x, x), 'all-pairs identity') + + +def collapse(columns, other): + """Collapse a rank-one column family; factors stay Gaussian rational.""" + n = len(columns[0]) + pivot = next((v for v in columns if any(a != ZERO for a in v)), None) + if pivot is None: + return [ZERO]*n, [ZERO]*n + i = next(i for i, a in enumerate(pivot) if a != ZERO) + a, b = pivot[i] + inv = (Fraction(a, a*a+b*b), Fraction(-b, a*a+b*b)) + cs = [mul(col[i], inv) for col in columns] + require(all(col == scale(pivot, c) for col, c in zip(columns, cs)), 'rank-one collapse premise') + return pivot, linear(other, cs) + + +def fixture(name, x, a, d, z, merged_z): + t = [minus(col, scale(merged_z, c)) for col, c in zip(x, a)] + return {'name': name, 'T': t, 'D': d, 'Z': z} + + +def coupled_fixture(name, x, coefficients, sources): + d = [linear(x, a) for a in coefficients] + t = [minus(col, linear(sources, [a[j] for a in coefficients])) + for j, col in enumerate(x)] + return {'name': name, 'T': t, 'D': d, 'Z': sources} + + +def examples(x): + n = len(x[0]); zero = [ZERO]*n + j, h = list(combinations(range(8), 2))[SEED % 28] + a = [ZERO]*8; a[j] = ONE + port = [ZERO]*n; port[SEED] = ONE + port2 = [ZERO]*n; port2[SEED+1] = ONE + port3 = [ZERO]*n; port3[SEED+2] = ONE + cases = [] + cases.append(fixture('zero-added-readers', x, [ZERO]*8, [zero, zero], [x[j], x[h]], zero)) + cases.append(fixture('zero-added-sources-outside', x, [ZERO]*8, [port, port2], [zero, zero], zero)) + for c in [ONE, (-1, 0), I, (1, 1)]: + # d1 + c*d2 = x_j, while both d's may be outside col(X). + d2 = port; d1 = minus(x[j], scale(port, c)) + cases.append(fixture('off-column-'+str(c), x, a, [d1, d2], [x[h], scale(x[h], c)], x[h])) + cases.append(fixture('canceling-off-column', x, [ZERO]*8, [port, scale(port,I)], + [x[h], scale(x[h],I)], zero)) + cases.append(fixture('reader-rank-one-source-rank-two', x, a, [x[j], scale(x[j],I)], + [minus(x[h],scale(port,I)), port], x[h])) + cases.append(fixture('three-totals-quotient-two', x, a, + [port, port2, minus(minus(x[j],port),port2)], [x[h]]*3, x[h])) + cases.append(fixture('four-totals-quotient-three', x, a, + [port,port2,port3,minus(minus(minus(x[j],port),port2),port3)], [x[h]]*4, x[h])) + t = [list(col) for col in x]; t[j] = zero; t[h] = zero + cases.append({'name':'rank-two-disjoint-coordinate-retirement','T':t,'D':[x[j],x[h]],'Z':[x[j],x[h]]}) + cases.append({'name':'basis-mixed-retirement','T':t, + 'D':[plus(x[j],x[h]),minus(x[j],x[h])], + 'Z':[scale(plus(x[j],x[h]),(Fraction(1,2),0)), + scale(minus(x[j],x[h]),(Fraction(1,2),0))]}) + aa = [[ONE,ZERO,I,ZERO,ZERO,ZERO,ZERO,ZERO], + [ZERO,ZERO,ZERO,ZERO,ONE,ZERO,(1,1),ZERO]] + cases.append(coupled_fixture('disjoint-two-complex-lifts',x,aa, + [plus(x[j],scale(port,I)),plus(x[h],port2)])) + aa = [[ONE,I,ZERO,ZERO,ZERO,ZERO,ZERO,ZERO], + [ZERO,ZERO,ONE,ONE,ZERO,ZERO,ZERO,ZERO], + [ZERO,ZERO,ZERO,ZERO,ONE,(0,-1),ZERO,ZERO]] + cases.append(coupled_fixture('disjoint-three-complex-lifts',x,aa,[x[j],x[h],port])) + # All four factors nontrivial; exact rank-two block is not a collapse. + t = [list(col) for col in x] + t[j] = minus(x[j], plus(x[j],x[h])); t[h] = minus(x[h], minus(x[j],x[h])) + cases.append({'name':'dense-rank-two-inside-remains-open','T':t, + 'D':[plus(x[j],x[h]),minus(x[j],x[h])], 'Z':[x[j],x[h]]}) + return cases + + +def inspect(case, x, geometry): + t,d,z = case['T'],case['D'],case['Z'] + require_identity(x,t,d,z) + rd,rz = rank_c(d),rank_c(z) + q = rank_c(x+d)-8 + require(rz <= len(d)-q, 'quotient rank inequality') + costs = [beta(v,w,geometry) for v,w in zip(x+d,t+z)] + collapse_info = None + if rz <= 1: + common, merged = collapse(z,d) + collapse_info = (merged, common) + elif rd <= 1: + collapse_info = collapse(d,z) + else: + require(q == 0 or len(d) > 2, 'two-total outside reader with independent sources') + contracted_cost = None + disjoint_blocks = None + if collapse_info is not None: + merged,common = collapse_info + require_identity(x,t,[merged],[common]) + merged_beta = beta(merged,common,geometry) + require(merged_beta <= sum(costs[8:]), 'support-rank subadditivity') + contracted_cost = sum(costs[:8])+merged_beta + require(contracted_cost >= 64, 'inherited single-lift floor on fixture') + if q == 0: + # This finite left inverse is checked, not assumed by the theorem. + require([[sum(mul(a,b)[0] for a,b in zip(u,v)) for v in x] for u in x] + == [[56*int(i==j) for j in range(8)] for i in range(8)], 'X Gram left inverse') + coefficients = [[scale([sum_gaussian(mul(a,b) for a,b in zip(v,col))], + (Fraction(1,56),0))[0] for v in x] for col in d] + require(all(linear(x,a)==col for a,col in zip(coefficients,d)), 'coordinate coefficient reconstruction') + supports = [{j for j,c in enumerate(a) if c != ZERO} for a in coefficients] + if sum(map(len,supports)) == len(set().union(*supports)): + disjoint_blocks = [] + for h,support in enumerate(supports): + cost = sum(costs[j] for j in support)+costs[8+h] + require(cost >= 8*len(support), 'disjoint single-lift block floor') + disjoint_blocks.append({'support':sorted(support),'cost':cost,'floor':8*len(support)}) + require(sum(costs)>=64,'disjoint lifts floor') + return {'name':case['name'],'extra_terms':len(d),'reader_rank':rd,'source_rank':rz, + 'quotient_rank':q,'source_quotient_rank':rank_c(x+z)-8, + 'ordered_costs':costs,'total_cost':sum(costs), + 'collapsed_cost':contracted_cost, + 'disjoint_blocks':disjoint_blocks, + 'classification':'covered' if collapse_info is not None or disjoint_blocks is not None else 'outside_claim', + 'identity_entries_checked':len(x[0])**2} + + +def sum_gaussian(values): + result = ZERO + for value in values: + result = add(result,value) + return result + + +def controls(x,g,cases): + names=[] + def rejects(name, call): + try: call() + except ValueError: names.append(name) + else: raise ValueError('control accepted: '+name) + import copy + c=copy.deepcopy(cases[2]);c['Z'][1][SEED]=add(c['Z'][1][SEED],ONE) + rejects('source-perturbation-breaks-all-pairs',lambda: require_identity(x,c['T'],c['D'],c['Z'])) + c=cases[2] + rejects('omit-nonzero-extra-term',lambda: require_identity(x,c['T'],c['D'][:1],c['Z'][:1])) + c=copy.deepcopy(cases[4]);c['Z']=[[(a,-b) for a,b in v] for v in c['Z']] + rejects('conjugation-is-not-transpose',lambda: require_identity(x,c['T'],c['D'],c['Z'])) + rejects('rank-two-source-cannot-collapse',lambda: collapse(cases[-1]['Z'],cases[-1]['D'])) + require(rank_c([x[0],scale(x[0],I)])==1, 'complex rank control') + names.append('complex-rank-not-real-column-rank') + require(inspect(cases[-1],x,g)['classification']=='outside_claim','reject overbroad two-total floor argument') + names.append('coupled-rank-two-inside-not-classified-as-covered') + by_name={case['name']:inspect(case,x,g) for case in cases + if case['name'] in ('rank-two-disjoint-coordinate-retirement','basis-mixed-retirement')} + require(by_name['rank-two-disjoint-coordinate-retirement']['total_cost']==64 + and by_name['basis-mixed-retirement']['total_cost']==66,'GL2 mixing changes separate-total cost') + names.append('GL2-basis-change-is-not-cost-free') + # k=3, q=1 still allows source rank2: an outside canceling pair plus a lift. + p=[ZERO]*112;p[SEED]=ONE + a=[ZERO]*8;a[0]=ONE + boundary=fixture('k3-one-outside-insufficient',x,a,[p,scale(p,(-1,0)),x[0]], + [x[1],x[1],x[2]],x[2]) + b=inspect(boundary,x,g) + require(b['quotient_rank']==1 and b['source_rank']==2 and b['classification']=='outside_claim', + 'k>=3 threshold boundary') + names.append('k3-one-outside-does-not-force-source-rank-one') + require(rank_f2([3,5,6])==2 and rank_f2([3,5,7])==3,'F2 rank controls') + names.append('dependent-and-independent-binary-rows') + return names,b + + +def check_sources(): + manifest=json.loads((HERE/'SOURCES.json').read_text()) + for name,record in manifest['inputs'].items(): + require(sha256((ROOT/name).read_bytes()).hexdigest()==record['sha256'],'source hash: '+name) + return manifest + + +def compute(): + check_sources() + path=ROOT/'research/p112-single-lift/geometry.py' + spec=importlib.util.spec_from_file_location('p112_retained_geometry',path) + gmod=importlib.util.module_from_spec(spec);spec.loader.exec_module(gmod) + geometry=gmod.build();gmod.check_geometry(geometry) + x=[[(row[j],0) for row in geometry['X']] for j in range(8)] + require(rank_c(x)==8,'complex X rank') + cases=examples(x) + receipts=[inspect(c,x,geometry) for c in cases] + names,boundary=controls(x,geometry,cases) + return {'schema':1,'assignment_seed':SEED,'field':'Gaussian rational, algebraic transpose', + 'scope':'finite boundary fixtures for written quotient/collapse theorem', + 'examples':receipts,'controls':names,'k3_boundary':boundary, + 'full_identity_entries':112*112*(len(cases)+1), + 'classification_counts':dict(Counter(r['classification'] for r in receipts)), + 'no_new_kappa':True} + + +def main(): + parser=argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write',type=Path) + parser.add_argument('--check',type=Path,default=HERE/'CERTIFICATE.json') + parser.add_argument('--with-predecessors',action='store_true') + args=parser.parse_args() + result=compute() + if args.with_predecessors: + # Pinned #998 driver replays both #845 checkers plus its independent checker. + subprocess.run([sys.executable,'-I','-S','-B',str(ROOT/'research/p112-complex-single-lift/verify.py')],check=True) + if args.write: + require(not args.write.exists(),'refusing to overwrite output') + args.write.write_text(json.dumps(result,indent=2,sort_keys=True)+'\n') + else: + require(result==json.loads(args.check.read_text()),'certificate mismatch') + print('PASS_P112_TWO_TOTAL_REDUCTION examples=%d controls=%d floor=64 coupled_rank_two=open no_new_kappa' + %(len(result['examples']),len(result['controls']))) + +if __name__=='__main__': + main()