diff --git a/research/even-ternary-disjointness-rank/PROOF.md b/research/even-ternary-disjointness-rank/PROOF.md new file mode 100644 index 0000000000..3594536c29 --- /dev/null +++ b/research/even-ternary-disjointness-rank/PROOF.md @@ -0,0 +1,189 @@ +# Exact ternary disjointness repair in every even dimension + +Let F be any field of characteristic three. For an integer h >= 2, let +A_h be the matrix indexed by the nonempty proper subsets of [h], with +entry 1 precisely when its row and column subsets are disjoint. Write +B_h = I - A_h, of size v = 2^h - 2. + +**Theorem.** For every even h >= 4, + +$$ + d_h=2^{h-2}+(-1)^{h/2}2^{h/2-1},\qquad + \dim_F\ker B_h=d_h-1, +$$ +$$ + \operatorname{rank}_F B_h + =3\cdot2^{h-2}-1-(-1)^{h/2}2^{h/2-1}. +$$ + +At h=2 the rank is 1. Consequently, the minimum number of arbitrary +additive scalar rank-one terms repairing A_h to I is the displayed rank. + +Nick Petalas's [PR #5173](https://github.com/CrocSwap/integer-mult-bounds/pull/5173) +proves the full-rank result for odd h and gives the h=2 boundary example. +This settles its explicitly open even-h >= 4 question. The tensor/deletion +approach follows Ali Romman's binary [PR #4962](https://github.com/CrocSwap/integer-mult-bounds/pull/4962). +The new work is the singular characteristic-three endpoint restriction and +the resulting exact all-even-dimensional formula. The formulas count +algebraic terms, not paid physical operations. + +## 1. Full tensor kernel + +Include the empty and full subsets, denoted 0 and f. The full disjointness +matrix and its identity repair are + +$$ + K=\begin{pmatrix}1&1\\1&0\end{pmatrix},\qquad + T=K^{\otimes h},\qquad M=I-T. +$$ + +All entries lie in F3. Rank is preserved by extension of the coefficient +field, as characterized by nonzero minors. Thus it is enough to calculate +over F9; the same rank then holds over F3 and every characteristic-three +field F, whether or not F contains F9. + +In F9 choose a root alpha of x^2-x-1. The other root is beta=1-alpha=alpha^3. +The roots are distinct, alpha^4=-1, and alpha has order eight. The two +vectors (alpha,1)^T and (beta,1)^T form an eigenbasis of K. Their tensor +products form an eigenbasis of T. A tensor with k beta factors has +eigenvalue alpha^(h+2k), and hence belongs to ker M exactly when + +$$ + h+2k\equiv0\pmod8. +$$ + +It follows, as an **integer multiplicity count**, that + +$$ + d_h=\dim\ker M + =\sum_{\substack{0\leq k\leq h\\k\equiv-h/2\ (4)}}\binom hk + \quad(h\text{ even}). +$$ + +This is not an inference from a trace reduced modulo three. For completeness, +the ordinary complex fourth-root filter evaluates this integer binomial sum. +Set h=2m and take i in C. Then + +$$ + d_h=\tfrac14\bigl(2^h+i^m(1+i)^h+(-i)^m(1-i)^h\bigr) + =2^{h-2}+(-1)^m2^{m-1}, +$$ + +because (1+i)^(2m)=2^m i^m and its conjugate has the same real contribution. +The omitted fourth term is 0^h=0. In particular d_2=0, whereas d_h>0 +for every even h>=4. + +Every tensor eigenvector of eigenvalue one has coordinate 1 at f and +coordinate alpha^(h+2k)=1 at 0. Therefore + +$$ + x_0=x_f\quad\text{for every }x\in\ker M. +$$ + +For h>=4, evaluation x -> x_0 on ker M is nonzero: any one of those +eigenvectors has value 1. Consequently the subspace of ker M vanishing +at both endpoints has dimension d_h-1. It remains to prove that it is +exactly the kernel of the interior principal block; endpoint deletion +alone does not imply this. + +## 2. Singular endpoint restriction + +The explicit local powers in characteristic three are + +$$ + K^2=\begin{pmatrix}2&1\\1&1\end{pmatrix},\qquad K^4=-I. +$$ + +For even h, T^4=I. Define two polynomial operators + +$$ + P=I+T+T^2+T^3,\qquad G=T^2-T. +$$ + +They satisfy + +$$ + MP=0,\quad P^2=P,\quad MG=GM=I-P. +$$ + +Indeed P acts as 4=1 on the eigenvalue-one subspace and as zero on +the other eigenspaces. Alternatively the identities follow by polynomial +multiplication using T^4=I and 3=0. In particular P projects onto ker M. + +Let E=(0,f). At those endpoints a tensor-power entry is the h-th power +of the corresponding local entry. As h is even, + +$$ + T_{EE}=\begin{pmatrix}1&1\\1&0\end{pmatrix},\quad + (T^2)_{EE}=\begin{pmatrix}1&1\\1&1\end{pmatrix},\quad + G_{EE}=\begin{pmatrix}0&0\\0&1\end{pmatrix}. +$$ + +Take y in ker B_h, and extend it to a full vector z with z_0=z_f=0. +The interior coordinates of Mz vanish. Choose a full-kernel eigenvector +x with x_0=x_f=1, which exists for h>=4. Since M is symmetric, + +$$ + 0=(Mx)^Tz=x^TMz=(Mz)_0+(Mz)_f. +$$ + +Thus Mz=a(e_0-e_f) for some scalar a. Apply G and the polynomial +identity to obtain + +$$ + z=aG(e_0-e_f)+Pz. +$$ + +Put w=Pz. Since w is in ker M, w_0=w_f. The two endpoint coordinates +of the last display give + +$$ + 0=w_0,\qquad 0=-a+w_f. +$$ + +Therefore a=0, and z itself belongs to ker M. Conversely any full-kernel +vector vanishing at E restricts to a vector in ker B_h. Restriction and +zero extension are inverse linear maps between these kernels, proving + +$$ + \dim\ker B_h=d_h-1. +$$ + +Subtracting from 2^h-2 proves the rank formula. The argument establishes +the deletion step without assuming that the singular full matrix has an +inverse or that a principal submatrix keeps its nullity. + +## 3. The small boundary and the repair count + +For h=2, d_h=0, so the eigenvector used in the deletion proof does not +exist. The literal interior matrix is + +$$ + B_2=\begin{pmatrix}1&-1\\-1&1\end{pmatrix}, +$$ + +of rank one. Extending the h>=4 formula to h=2 would incorrectly give +rank three for a two-by-two matrix. This boundary is retained from #5173, +not claimed as a new result. + +If A_h+sum_{j=1}^ell u_j v_j^T=I, subadditivity of rank implies +ell>=rank B_h. Conversely every rank-r matrix has a rank factorization +B_h=UV with U having r columns and V having r rows. Expanding this +product gives r rank-one summands. The factorization can be constructed +over F3 and remains valid over every F. Thus the lower bound is attained +in the stated unrestricted additive algebraic model. + +## Scope and proof status + +This is a written all-even-dimensional proof, corroborated by bounded +exact finite calculations. The finite checks do not prove the universal +quantifier; independent human review and formal proof-kernel acceptance +remain unclaimed. + +No native ternary supplier, paid COPY/read count, coefficient-preparation +method, dirty-restoration contract, frame/hosting construction, precision, +fixed-tape/compiler bound, recursive invoice or new multiplication exponent +is supplied. In particular the binary ledger in #4962 is not transferred +to characteristic three, and no nonadditive repair is excluded. + +Krzysztof Wojt, with substantial OpenAI Codex assistance. Apache-2.0. diff --git a/research/even-ternary-disjointness-rank/README.md b/research/even-ternary-disjointness-rank/README.md new file mode 100644 index 0000000000..c5c228bc57 --- /dev/null +++ b/research/even-ternary-disjointness-rank/README.md @@ -0,0 +1,121 @@ +# Exact ternary disjointness-repair rank in even dimensions + +For every even **h >= 4** and every field F of characteristic three, let +A_h be disjointness on the nonempty proper subsets of [h]. Then + +$$ +\operatorname{rank}_F(I-A_h) +=3\cdot2^{h-2}-1-(-1)^{h/2}2^{h/2-1}. +$$ + +This also counts the minimum unrestricted additive scalar rank-one terms +repairing A_h to the identity. At h=2 the rank is 1. +The [written proof](PROOF.md) resolves the explicitly open even-dimensional +question in Nick Petalas's [#5173](https://github.com/CrocSwap/integer-mult-bounds/pull/5173). +That predecessor proves odd h and supplies the h=2 control. The new step +proves that deleting both endpoints reduces the singular full tensor's +kernel dimension by exactly one, for every even h>=4. + +| h | Interior dimension | Exact rank | Kernel dimension | +|---:|---:|---:|---:| +| 2 | 2 | 1 | 1 | +| 4 | 14 | 9 | 5 | +| 6 | 62 | 51 | 11 | +| 8 | 254 | 183 | 71 | +| 10 | 1022 | 783 | 239 | + +This is a **scoped algebraic proof with finite exact corroboration**. +Independent human review and formal proof-kernel acceptance are unclaimed. +No native ternary supplier, physical COPY tariff, complete recursive bill, +new kappa or selected-frontier change is claimed. + +## Reproduce and evidence + +Python 3.12, standard library only. From the repository root: + +```sh +python3.12 -I -W error -B research/even-ternary-disjointness-rank/verify.py +python3.12 -I -O -W error -B research/even-ternary-disjointness-rank/verify.py +python3.12 -B scripts/research_package.py --package research/even-ternary-disjointness-rank +``` + +Expected marker: `PASS_EVEN_TERNARY_DISJOINTNESS_RANK`. Each direct check +took under one second on CPython 3.12.12/macOS. The verifier is read-only, +Git/network-free and uses explicit exceptions, comparing its complete finite +result with [RESULTS.json](RESULTS.json). To regenerate evidence without +overwriting it, pass `--emit-results` and redirect stdout to a new file. + +Checks cover exact bit-packed F3 ranks at h=2,4,6,8,10 and separately written +dense ranks through h=8; all 729 ternary 2-by-3 matrices compare the engines. +At h=2,4,6,8, all 340 basis columns check T^4=I, MP=0, P^2=P and +MG=GM=I-P, the endpoint blocks and projector ranks, where +P=I+T+T^2+T^3 and G=T^2-T. At h=2,4 the tensor action also agrees with the +literal disjointness predicate on every column. + +A separate complete kernel count uses two half-input syndrome tables, +without elimination. At h=4 it covers all 3^14=4,782,969 inputs, enumerating +4,374 half inputs, and finds 243 kernel vectors. The h=2 control finds three. +The integer binomial multiplicity formula is checked at 100 even dimensions +from 2 to 200. Thirteen domain, h=2, endpoint-deletion, group-inverse and +projector rejection controls pass. These checks corroborate the written +proof; they do not supply its universal quantifier. + +[independent.py](independent.py) was written by a separately tasked Luna +worker given the matrix definition and finite dimensions, without the +candidate formula or predecessor verifier code. The primary agent inspected +and reran it. This is separate implementation within AI-assisted work, +not independent human review. Its standalone output also records full-matrix +and single-endpoint-deletion ranks at h=2,4,6. + +## Scope, sources and overlap + +Scientific base: fresh canonical main +`ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c`, priority revision 7. +[Claim #5194](https://github.com/CrocSwap/integer-mult-bounds/discussions/5194) +takes the released [#5173 handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19145071). +This changes the generic `formal-interface-lemma` card to that concrete +algebraic question. It closes an infinite family left open by the predecessor; +the odd-h theorem and binary rank are cited rather than replayed as new work. + +Initial overlap covered 6,996 local notes, 312 open PRs and 4,384 Discussion +records with complete pagination at 12:12–12:13 UTC on 2026-10-23, followed +by targeted live checks before claiming. No competing even-dimensional claim +was found. Arbitrary diffs and unpublished work remain coverage limits. +The donor's excluded topics and parallel R437/projection work are outside scope. + +[SOURCES.json](SOURCES.json) pins the exact base, blobs and SHA256 of the +catalogue, selected record and predecessor documents as historical provenance. +No predecessor code or artifact is imported or modified. The checker constructs +its own matrices, so those documents are not live scientific inputs. The +registered runner checks Git provenance; the standalone checker needs no Git. + +Physical implementation, coefficient preparation, reads/copies, arbitrary +dirty restoration, frames/hosting, precision, tape, stock, compiler and +recursive/outer costs are outside scope and not treated as zero. The binary +ledger from #4962 does not transfer to F3. Nonadditive repairs are not excluded. +No predecessor scientific suite, selected cold replay, Lean or Docker run is +needed or claimed. + +## Open next questions + +Can a nonadditive ternary repair avoid this additive rank obstruction? +This matters to whether the endpoint can support a useful physical supplier. +First specify an exact all-input ternary operation and a complete favorable +paid bill, including preparation and restoration. Those contracts and costs +are missing; another parameter sweep of the solved additive rank family is +not a useful next step. No implementation expansion or follow-up is reserved. + +## Credit + +- **Nick Petalas, #5173**, head `50ee4f7069d7aabdcdfc44ebadf0456d8cf82e0c`: + odd-dimensional ternary theorem, h=2 boundary and explicit even-h question. +- **Ali Romman, #4962**: binary repair theorem and tensor/endpoint-deletion + approach, with substantial OpenAI Codex assistance. +- **mikey1201, #172**, head `427b23bc79489e7b2b7548bfd434dd9670fd5c47`: + disjointness endpoint and retained **icekylinx/#144** compiler/bookkeeping + lineage, with source-specific Cline assistance. No physical cost is assumed free. +- **Krzysztof Wojt**, with substantial **OpenAI Codex assistance**: all-even + theorem, singular endpoint argument, checker and package; the bounded Luna + fixture task is disclosed above. + +New work is Apache-2.0. Frozen sources and the selected result remain unchanged. diff --git a/research/even-ternary-disjointness-rank/RESULTS.json b/research/even-ternary-disjointness-rank/RESULTS.json new file mode 100644 index 0000000000..db67ba0059 --- /dev/null +++ b/research/even-ternary-disjointness-rank/RESULTS.json @@ -0,0 +1,98 @@ +{ + "complete_kernel_counts": { + "2": { + "covered_inputs": 9, + "enumerated_half_inputs": 6, + "kernel_vectors": 3 + }, + "4": { + "covered_inputs": 4782969, + "enumerated_half_inputs": 4374, + "kernel_vectors": 243 + } + }, + "independent_literal_ranks": { + "field": "F_3", + "full_subset_matrix_I_minus_K_tensor_h": { + "2": { + "dimension": 4, + "full_rank_mod_3": 4, + "rank_after_deleting_empty_subset": 2, + "rank_after_deleting_full_subset": 3 + }, + "4": { + "dimension": 16, + "full_rank_mod_3": 10, + "rank_after_deleting_empty_subset": 10, + "rank_after_deleting_full_subset": 10 + }, + "6": { + "dimension": 64, + "full_rank_mod_3": 52, + "rank_after_deleting_empty_subset": 52, + "rank_after_deleting_full_subset": 52 + } + }, + "proper_nonempty_subset_matrix_I_minus_A": { + "2": { + "dimension": 2, + "rank_mod_3": 1 + }, + "4": { + "dimension": 14, + "rank_mod_3": 9 + }, + "6": { + "dimension": 62, + "rank_mod_3": 51 + }, + "8": { + "dimension": 254, + "rank_mod_3": 183 + } + } + }, + "multiplicity_formula_checks": 100, + "new_kappa": null, + "packed_rank_small_matrices": 729, + "polynomial_identity_checks": { + "2": { + "columns": 4, + "projector_rank": 0 + }, + "4": { + "columns": 16, + "projector_rank": 6 + }, + "6": { + "columns": 64, + "projector_rank": 12 + }, + "8": { + "columns": 256, + "projector_rank": 72 + } + }, + "ranks": { + "10": 783, + "2": 1, + "4": 9, + "6": 51, + "8": 183 + }, + "rejection_controls": [ + "invalid_dimension_-2", + "invalid_dimension_0", + "invalid_dimension_1", + "invalid_dimension_3", + "invalid_dimension_5", + "invalid_dimension_4.0", + "invalid_dimension_True", + "omit_h2_exception", + "keep_full_kernel_nullity_after_deletion", + "delete_only_empty", + "delete_only_full", + "G_equals_T_squared_plus_T", + "scale_projector_by_two" + ] +} diff --git a/research/even-ternary-disjointness-rank/SOURCES.json b/research/even-ternary-disjointness-rank/SOURCES.json new file mode 100644 index 0000000000..e32bdbb504 --- /dev/null +++ b/research/even-ternary-disjointness-rank/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/boolean-disjointness-repair/README.md", + "usage": "provenance", + "git_blob": "5d659814e9445026ec44a64993559890dfd92a60", + "sha256": "b37e421642070fe7769189655c29e8fd68100000292938ffbd4d5f777a1edc11" + }, + { + "path": "research/ternary-disjointness-repair/PROOF.md", + "usage": "provenance", + "git_blob": "680e0adb269a3cd3420c2fe2312bea99c4b76ded", + "sha256": "43d61f2c7ea623e6a39783b486c12c8edea62197a2ae2512a4e4f9596f8920e0" + }, + { + "path": "research/ternary-disjointness-repair/README.md", + "usage": "provenance", + "git_blob": "1acd9f2e821c080a4091ef8b584d32d6201f7d07", + "sha256": "13da08bfa713096bba971539553fd3170222ce26780b66585493ddda635e3a50" + } + ] +} diff --git a/research/even-ternary-disjointness-rank/TASK.json b/research/even-ternary-disjointness-rank/TASK.json new file mode 100644 index 0000000000..e5a5eaac21 --- /dev/null +++ b/research/even-ternary-disjointness-rank/TASK.json @@ -0,0 +1,95 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove the exact characteristic-three rank of I-A_h on nonempty proper Boolean subsets for every even h >= 4, retaining the known h=2 exception, and deduce the exact additive rank-one repair count.", + "scope_change_reason": "Take the explicit open even-dimensional question in Nick Petalas PR5173 after its released handoff; this is a scoped algebraic interface proof rather than formal proof-assistant work or a repetition of the odd-dimensional inverse.", + "bottleneck_link": "The disjointness endpoint of mikey1201 PR172 requires repair. This theorem completes its characteristic-three additive rank obstruction. It supplies no native ternary realization or recursive cost improvement; all physical costs remain outside scope.", + "budget_minutes": 240, + "stop_rule": "One all-even-dimensional rank theorem with a proved endpoint-deletion step; a finite rank table alone would be insufficient. Stop after this result and its verification. Do not expand into other fields, nonadditive repairs or physical implementation. Budget includes publication.", + "outcome": "completed", + "evidence": "PROOF.md proves rank = 3*2^(h-2)-1-(-1)^(h/2)*2^(h/2-1) for all even h>=4. RESULTS.json is regenerated by verify.py: ranks at h=2,4,6,8,10; separate dense ranks through h=8; 729 small rank-engine fixtures; 340 complete polynomial-identity columns; complete h=2/4 kernel counts; 100 integer multiplicity checks; thirteen rejection controls. Normal and optimized registered commands are declared.", + "author": "Krzysztof Wojt with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance for derivation, proof, implementation and publication. A separately tasked Luna worker generated finite dense-rank fixtures without the candidate formula; the primary agent inspected and reran them. This is not independent human review.", + "open_questions": [ + { + "question": "Can a specified nonadditive ternary repair evade the additive rank obstruction?", + "why_it_matters": "A different endpoint-repair contract may change the physical supplier decision after the additive family is solved.", + "first_step": "Write one exact all-input ternary operation and a complete favorable paid bill before an implementation campaign.", + "blocked_by": "Native operation, coefficient preparation, dirty restoration, frames/hosting, precision/tape and recursive costs remain unspecified; this package does not set them to zero." + } + ] +} diff --git a/research/even-ternary-disjointness-rank/VERIFY.json b/research/even-ternary-disjointness-rank/VERIFY.json new file mode 100644 index 0000000000..868cf60859 --- /dev/null +++ b/research/even-ternary-disjointness-rank/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact ranks, complete kernel counts, polynomial endpoint identities, independent dense fixtures and thirteen rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat every scientific check with Python assertions disabled." + } + ] +} diff --git a/research/even-ternary-disjointness-rank/independent.py b/research/even-ternary-disjointness-rank/independent.py new file mode 100644 index 0000000000..ffe5693873 --- /dev/null +++ b/research/even-ternary-disjointness-rank/independent.py @@ -0,0 +1,169 @@ +#!/usr/bin/env python3 +"""Generate finite F_3 rank fixtures for Boolean disjointness matrices. + +This standalone script constructs the matrices from subset definitions and +computes ranks by modular Gaussian elimination. Its finite outputs are +fixtures only; they do not establish a formula for general h. + +Prepared for Krzysztof Wojt by a separately tasked OpenAI Codex Luna worker, +given only the matrix definition and finite dimensions, not the rank formula. +Inspected and rerun by the primary Codex agent. This is implementation +separation within AI-assisted work, not independent human review. Apache-2.0. +""" + +from __future__ import annotations + +import json + + +MODULUS = 3 +K = ((1, 1), (1, 0)) + + +def rank_mod3(matrix: list[list[int]]) -> int: + """Return the rank over F_3 by ordinary row reduction.""" + if not matrix: + return 0 + + row_count = len(matrix) + column_count = len(matrix[0]) + if any(len(row) != column_count for row in matrix): + raise ValueError("rank_mod3 requires a rectangular matrix") + + work = [[entry % MODULUS for entry in row] for row in matrix] + pivot_row = 0 + + for column in range(column_count): + selected = None + for candidate in range(pivot_row, row_count): + if work[candidate][column] != 0: + selected = candidate + break + if selected is None: + continue + + if selected != pivot_row: + work[pivot_row], work[selected] = work[selected], work[pivot_row] + + pivot_value = work[pivot_row][column] + inverse = pow(pivot_value, -1, MODULUS) + for j in range(column, column_count): + work[pivot_row][j] = (work[pivot_row][j] * inverse) % MODULUS + + for other in range(row_count): + if other == pivot_row: + continue + factor = work[other][column] + if factor == 0: + continue + for j in range(column, column_count): + work[other][j] = ( + work[other][j] - factor * work[pivot_row][j] + ) % MODULUS + + pivot_row += 1 + if pivot_row == row_count: + break + + return pivot_row + + +def proper_subset_matrices(h: int) -> tuple[list[int], list[list[int]], list[list[int]]]: + """Construct A_h and B_h=I-A_h on nonempty proper subsets of [h].""" + if h < 2: + raise ValueError("h must be at least 2 for nonempty proper subsets") + + subsets = list(range(1, (1 << h) - 1)) + adjacency = [ + [int((left & right) == 0) for right in subsets] + for left in subsets + ] + b_matrix = [ + [((1 if i == j else 0) - adjacency[i][j]) % MODULUS + for j in range(len(subsets))] + for i in range(len(subsets)) + ] + return subsets, adjacency, b_matrix + + +def kronecker_product( + left: tuple[tuple[int, ...], ...] | list[list[int]], + right: tuple[tuple[int, ...], ...] | list[list[int]], +) -> list[list[int]]: + """Form a Kronecker product with rows ordered by row-pair blocks.""" + product: list[list[int]] = [] + for left_row in left: + for right_row in right: + product.append([ + left_entry * right_entry + for left_entry in left_row + for right_entry in right_row + ]) + return product + + +def full_tensor_matrix(h: int) -> list[list[int]]: + """Construct I-K^tensor h on all subsets, reducing entries modulo 3.""" + if h < 1: + raise ValueError("h must be positive for the tensor matrix") + + tensor: list[list[int]] = [[1]] + for _ in range(h): + tensor = kronecker_product(tensor, K) + + return [ + [((1 if i == j else 0) - tensor[i][j]) % MODULUS + for j in range(len(tensor))] + for i in range(len(tensor)) + ] + + +def principal_matrix_without(matrix: list[list[int]], removed: int) -> list[list[int]]: + """Delete one indexed row and the corresponding column.""" + size = len(matrix) + if any(len(row) != size for row in matrix): + raise ValueError("principal deletion requires a square matrix") + if removed < 0 or removed >= size: + raise IndexError("deleted index is outside the matrix") + + kept = [index for index in range(size) if index != removed] + return [[matrix[i][j] for j in kept] for i in kept] + + +def collect_results() -> dict[str, object]: + proper_results: dict[str, dict[str, int]] = {} + for h in (2, 4, 6, 8): + subsets, _adjacency, b_matrix = proper_subset_matrices(h) + proper_results[str(h)] = { + "dimension": len(subsets), + "rank_mod_3": rank_mod3(b_matrix), + } + + tensor_results: dict[str, dict[str, int]] = {} + for h in (2, 4, 6): + full_matrix = full_tensor_matrix(h) + full_dimension = len(full_matrix) + tensor_results[str(h)] = { + "dimension": full_dimension, + "full_rank_mod_3": rank_mod3(full_matrix), + "rank_after_deleting_empty_subset": rank_mod3( + principal_matrix_without(full_matrix, 0) + ), + "rank_after_deleting_full_subset": rank_mod3( + principal_matrix_without(full_matrix, full_dimension - 1) + ), + } + + return { + "field": "F_3", + "proper_nonempty_subset_matrix_I_minus_A": proper_results, + "full_subset_matrix_I_minus_K_tensor_h": tensor_results, + } + + +def main() -> None: + print(json.dumps(collect_results(), indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/even-ternary-disjointness-rank/verify.py b/research/even-ternary-disjointness-rank/verify.py new file mode 100644 index 0000000000..c90cfe2632 --- /dev/null +++ b/research/even-ternary-disjointness-rank/verify.py @@ -0,0 +1,257 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of PROOF.md; no universal theorem acceptance. + +Krzysztof Wojt with substantial OpenAI Codex assistance. Apache-2.0. +Standard library only; read-only and independent of Git/network/predecessor code. +""" +from __future__ import annotations + +import argparse +from collections import Counter +from hashlib import sha256 +from itertools import product +import json +from math import comb +from pathlib import Path +import runpy + + +PACKAGE = Path(__file__).resolve().parent + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def multiplicity(h: int) -> int: + require(type(h) is int and h >= 2 and h % 2 == 0, "even integer h >= 2 required") + return 2 ** (h - 2) + (-1) ** (h // 2) * 2 ** (h // 2 - 1) + + +def claimed_rank(h: int) -> int: + d = multiplicity(h) + return 1 if h == 2 else 2 ** h - 1 - d + + +def pack(row: list[int] | tuple[int, ...]) -> tuple[int, int]: + return tuple(sum(1 << j for j, x in enumerate(row) if x % 3 == c) + for c in (1, 2)) + + +def add(a: tuple[int, int], b: tuple[int, int]) -> tuple[int, int]: + a1, a2 = a + b1, b2 = b + an, bn = a1 | a2, b1 | b2 + return ((a1 & ~bn) | (b1 & ~an) | (a2 & b2), + (a2 & ~bn) | (b2 & ~an) | (a1 & b1)) + + +def packed_rank(rows: list[tuple[int, int]]) -> int: + basis = {} + for row in rows: + require(row[0] & row[1] == 0, "overlapping ternary digit masks") + while row[0] | row[1]: + pivot = (row[0] | row[1]) & -(row[0] | row[1]) + if row[1] & pivot: + row = (row[1], row[0]) + if pivot not in basis: + basis[pivot] = row + break + b1, b2 = basis[pivot] + row = add(row, (b2, b1)) + return len(basis) + + +def interior_rows(h: int) -> list[tuple[int, int]]: + """Build I-A directly by enumerating nonzero submasks of each complement.""" + full = (1 << h) - 1 + rows = [] + for u in range(1, full): + complement = full ^ u + v, twos = complement, 0 + while v: + twos |= 1 << (v - 1) + v = (v - 1) & complement + rows.append((1 << (u - 1), twos)) + return rows + + +def tensor_action(vector: list[int], h: int) -> list[int]: + """Apply K^{tensor h} by local two-coordinate steps, in F3.""" + require(len(vector) == 1 << h, "tensor dimension mismatch") + result = vector[:] + for bit in range(h): + stride = 1 << bit + for start in range(0, len(result), 2 * stride): + for offset in range(stride): + lo, hi = start + offset, start + offset + stride + a, b = result[lo], result[hi] + result[lo], result[hi] = (a + b) % 3, a + return result + + +def sub(a: list[int], b: list[int]) -> list[int]: + return [(x - y) % 3 for x, y in zip(a, b, strict=True)] + + +def polynomial_columns(h: int) -> tuple[list[list[int]], list[list[int]]]: + """Check T^4=I, MP=0, P^2=P and MG=GM=I-P on every basis column.""" + n = 1 << h + ps, gs = [], [] + for j in range(n): + e = [int(i == j) for i in range(n)] + t = [e] + for _ in range(4): + t.append(tensor_action(t[-1], h)) + require(t[4] == e, "T^4 is not I") + p = [sum(row[i] for row in t[:4]) % 3 for i in range(n)] + g = sub(t[2], t[1]) + require(tensor_action(p, h) == p, "MP is nonzero") + # On an eigenvalue-one vector, I+T+T^2+T^3 is multiplication by 4=1. + pp = p[:] + current = p[:] + for _ in range(3): + current = tensor_action(current, h) + pp = [(x + y) % 3 for x, y in zip(pp, current, strict=True)] + require(pp == p, "P is not idempotent") + require(sub(g, tensor_action(g, h)) == sub(e, p), "MG != I-P") + me = sub(e, t[1]) + tme = tensor_action(me, h) + require(sub(tensor_action(tme, h), tme) == sub(e, p), "GM != I-P") + require(p[0] == p[-1], "full kernel projector endpoints differ") + if h <= 4: + require(t[1] == [int((i & j) == 0) for i in range(n)], + "tensor action disagrees with literal disjointness") + ps.append(p) + gs.append(g) + require([[gs[j][i] for j in (0, n - 1)] for i in (0, n - 1)] + == [[0, 0], [0, 1]], "incorrect G endpoint block") + require(all(ps[j][i] == 0 for i in (0, n - 1) for j in (0, n - 1)), + "incorrect P endpoint block") + require(packed_rank([pack(c) for c in ps]) == multiplicity(h), + "projector rank differs from integer eigenspace count") + return ps, gs + + +def kernel_count(matrix: list[list[int]]) -> tuple[int, int]: + """Count every ternary input via two complete half-input syndrome tables.""" + n = len(matrix) + columns = list(zip(*matrix, strict=True)) + + def syndromes(part: list[tuple[int, ...]]) -> Counter: + table = Counter({(0,) * n: 1}) + for col in part: + nxt = Counter() + for key, count in table.items(): + for coefficient in range(3): + nxt[tuple((x + coefficient * y) % 3 + for x, y in zip(key, col, strict=True))] += count + table = nxt + return table + + cut = n // 2 + left, right = syndromes(columns[:cut]), syndromes(columns[cut:]) + count = sum(value * right.get(tuple((-x) % 3 for x in key), 0) + for key, value in left.items()) + return count, 3 ** cut + 3 ** (n - cut) + + +def rejection_controls(independent: dict, ps: list[list[int]], gs: list[list[int]]) -> list[str]: + rejected = [] + for h in (-2, 0, 1, 3, 5, 4.0, True): + try: + claimed_rank(h) + except ValueError: + rejected.append(f"invalid_dimension_{h!r}") + else: + raise ValueError(f"invalid h accepted: {h!r}") + require(2 ** 2 - 1 - multiplicity(2) != claimed_rank(2), "h=2 control lost") + rejected.append("omit_h2_exception") + require(14 - multiplicity(4) != claimed_rank(4), "wrong nullity control lost") + rejected.append("keep_full_kernel_nullity_after_deletion") + for endpoint in ("empty", "full"): + value = independent["full_subset_matrix_I_minus_K_tensor_h"]["4"][ + f"rank_after_deleting_{endpoint}_subset"] + require(value != claimed_rank(4), "single-endpoint deletion control lost") + rejected.append(f"delete_only_{endpoint}") + # A wrong-sign G has the wrong endpoint block and violates MG=I-P. + h, n = 4, 16 + e = [int(i == 0) for i in range(n)] + t1 = tensor_action(e, h) + t2 = tensor_action(t1, h) + bad_g = [(x + y) % 3 for x, y in zip(t2, t1, strict=True)] + require(sub(bad_g, tensor_action(bad_g, h)) != sub(e, ps[0]), + "wrong-sign group inverse control lost") + rejected.append("G_equals_T_squared_plus_T") + bad_p = [(2 * x) % 3 for x in ps[0]] + require(sub(gs[0], tensor_action(gs[0], h)) != sub(e, bad_p), + "scaled projector control lost") + rejected.append("scale_projector_by_two") + return rejected + + +def verify() -> dict: + separate = runpy.run_path(str(PACKAGE / "independent.py")) + independent = separate["collect_results"]() + dense_rank = separate["rank_mod3"] + # Exhaustive small rectangular matrices test all ternary pivot coefficients. + matrices = 0 + for digits in product(range(3), repeat=6): + rows = [list(digits[:3]), list(digits[3:])] + require(packed_rank([pack(r) for r in rows]) == dense_rank(rows), + "packed rank disagrees with separate dense elimination") + matrices += 1 + ranks = {} + for h in (2, 4, 6, 8, 10): + rank = packed_rank(interior_rows(h)) + require(rank == claimed_rank(h), f"literal interior rank fails at h={h}") + ranks[str(h)] = rank + if h <= 8: + require(rank == independent["proper_nonempty_subset_matrix_I_minus_A"][str(h)]["rank_mod_3"], + "independent literal matrix rank disagrees") + multiplicities = {} + for h in range(2, 202, 2): + exact = sum(comb(h, k) for k in range(h + 1) if (h + 2 * k) % 8 == 0) + require(exact == multiplicity(h), "integer multiplicity formula fails") + multiplicities[str(h)] = exact + polys = {} + for h in (2, 4, 6, 8): + ps, gs = polynomial_columns(h) + polys[str(h)] = {"columns": 1 << h, "projector_rank": multiplicity(h)} + if h == 4: + controls = rejection_controls(independent, ps, gs) + counts = {} + for h in (2, 4): + _, _, matrix = separate["proper_subset_matrices"](h) + count, partial_inputs = kernel_count(matrix) + expected = 3 ** (len(matrix) - claimed_rank(h)) + require(count == expected, "complete kernel count disagrees") + counts[str(h)] = {"kernel_vectors": count, "covered_inputs": 3 ** len(matrix), + "enumerated_half_inputs": partial_inputs} + return {"ranks": ranks, "independent_literal_ranks": independent, + "packed_rank_small_matrices": matrices, + "multiplicity_formula_checks": len(multiplicities), + "polynomial_identity_checks": polys, "complete_kernel_counts": counts, + "rejection_controls": controls, "new_kappa": None} + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit-results", action="store_true", + help="print regenerated finite evidence; write no files") + args = parser.parse_args() + result = verify() + if args.emit_results: + print(json.dumps(result, indent=2, sort_keys=True)) + return + expected = json.loads((PACKAGE / "RESULTS.json").read_text(encoding="utf-8")) + require(result == expected, "finite evidence differs from committed RESULTS.json") + hashes = {p.name: sha256(p.read_bytes()).hexdigest() + for p in sorted(PACKAGE.iterdir()) if p.is_file()} + print(json.dumps({"checks": result, "package_sha256": hashes}, sort_keys=True)) + print("PASS_EVEN_TERNARY_DISJOINTNESS_RANK finite_corroboration_only no_new_kappa") + + +if __name__ == "__main__": + main()