Prove exact ternary disjointness-repair rank in even dimensions

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.

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.