Prove full-rank ternary disjointness repair in odd dimensions

research/ternary-disjointness-repair/PROOF.md

@@ -0,0 +1,103 @@
+# Full-rank ternary identity repair in every odd dimension
+
+Let F be any field of characteristic three. For an odd integer h >= 3,
+let A_h have rows and columns indexed by the nonempty proper subsets of [h],
+with (A_h)_{U,V} = 1 when U and V are disjoint and zero otherwise. Put
+v = 2^h-2 and B_h = I_v-A_h.
+
+**Theorem.** B_h is invertible. Thus rank_F(B_h) = 2^h-2. The minimum
+number of additive scalar rank-one terms repairing A_h to I_v is exactly
+2^h-2.
+
+This is a characteristic-three statement. Ali Romman's binary theorem in
+[#4962](https://github.com/CrocSwap/integer-mult-bounds/pull/4962) concerns
+I+A_h over F2 and has a different rank. The tensor representation and the
+need to analyze the deletion of two endpoints come from that predecessor.
+The new step here is the characteristic-three inverse and its nonsingular
+two-endpoint block.
+
+## The full tensor inverse
+
+Include the empty and full subsets, and write the resulting disjointness
+matrix as T = K tensor ... tensor K, with h factors and
+
+```text
+K   = [1 1]     K² = [2 1]     K³ = [0 2]     K⁴ = -I₂.
+      [1 0]          [1 1]          [2 1]
+```
+
+These identities hold in the prime subfield F3, hence in F. Tensor
+multiplication gives T⁴ = (-1)^h I = -I because h is odd. Consequently
+M = I-T is invertible, with
+
+```text
+R = M⁻¹ = (I+T+T²+T³)/2 = 2(I+T+T²+T³).
+```
+
+Indeed, (I-T)(I+T+T²+T³) = I-T⁴ = 2I. Both matrices are polynomials
+in T, so the same multiplication works in the other order.
+
+Let E denote the ordered two indices (empty, full). The entries of a
+tensor power at these two indices are the h-th powers of the corresponding
+local entries. Since 2^h = 2 in F3 for odd h, the principal block of R is
+
+```text
+R_EE = 2 [1+1+2^h+0   0+1+1+2^h] = [2 2].
+         [0+1+1+2^h   1+0+1+1  ]   [2 0]
+```
+
+Its determinant is -4 = 2 in F3, so it is invertible over F. Its inverse is
+
+```text
+Q = [0 2].
+    [2 1]
+```
+
+## Deleting the two endpoints
+
+Write P for the proper nonempty indices. The principal block M_PP is
+exactly B_h. Suppose B_h x = 0. Extend x to a full vector z by giving it
+zero coordinates at both endpoints. The P coordinates of Mz vanish,
+so Mz is supported on E. Write Mz = i_E t, where i_E inserts the two
+endpoint coordinates. Multiplying by R gives z = R i_E t. Taking the E
+coordinates, which are zero in z, gives R_EE t = 0. Invertibility of
+R_EE implies t = 0, hence z = 0 and x = 0. Thus B_h is invertible.
+
+The proof also gives an explicit inverse without solving another system:
+
+```text
+B_h⁻¹ = R_PP - R_PE Q R_EP.
+```
+
+To verify this formula directly on an arbitrary interior right-hand side y,
+start with z = R i_P y. Subtract R i_E Q z_E. The new vector has zero E
+coordinates, while its image under M still has P coordinates y. Its P
+coordinates therefore solve B_h x = y. This proves the formula over F.
+
+## Exact additive repair count
+
+If A_h + sum_{j=1}^ell u_j w_j^T = I_v for arbitrary input vectors, then
+the sum equals B_h. Subadditivity of rank gives v = rank(B_h) <= ell.
+Conversely, B_h = sum_{j=1}^v (B_h e_j)e_j^T supplies v nonzero rank-one
+terms because B_h is invertible. Hence the algebraic minimum is exactly v.
+
+This is an additive decomposition count. It supplies neither a physical
+realization nor permission to reuse a binary supplier's cost ledger.
+
+## Necessary hypotheses and limits
+
+Odd h is essential to this argument and to the stated conclusion as a
+uniform claim: at h=2, the proper-set repair is
+
+```text
+[ 1 -1],
+[-1  1]
+```
+
+which has rank one and kernel vector (1,1) over F3. The h=1 proper-set
+matrix is empty and is excluded. Even dimensions above two, other
+characteristics and nonadditive repairs are not settled here.
+
+The theorem is a written algebraic proof with bounded exact corroboration.
+It does not establish a complete multiplication theorem, a supplier,
+a physical COPY tariff, a new kappa or formal proof-kernel acceptance.

research/ternary-disjointness-repair/README.md

@@ -0,0 +1,101 @@
+# Ternary disjointness needs a full-rank additive identity repair
+
+For every odd h >= 3 and every field F of characteristic three, disjointness
+on the nonempty proper subsets of [h] satisfies
+
+```text
+rank_F(I-A_h) = 2^h-2.
+```
+
+Exactly 2^h-2 additive scalar rank-one terms are necessary and sufficient
+to repair A_h to the identity. This is a **scoped algebraic proof**, with an
+explicit inverse and bounded exact corroboration. It gives a maximal-rank
+obstruction to cheap additive repair in this ternary counterpart of the
+Boolean-lattice endpoint. It does not assume a ternary physical supplier.
+
+[PROOF.md](PROOF.md) derives a polynomial inverse of the full tensor matrix
+and proves that its two-endpoint block is nonsingular. Deleting those
+endpoints leaves an invertible repair. The resulting explicit inverse is
+checked literally in the finite replay. Even h is outside the theorem;
+h=2 is a counterexample to dropping the oddness hypothesis.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/ternary-disjointness-repair
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/ternary-disjointness-repair/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/ternary-disjointness-repair --check-source-history
+```
+
+The manifest runs the verifier normally and with optimization enabled. Each
+run computes the ranks at h=3,5,7,9; verifies the full polynomial inverse,
+endpoint block and corrected interior inverse at h=3,5,7; independently
+enumerates all 729 candidate kernel vectors at h=3; and checks six rejecting
+controls plus the h=2 counterexample. It prints a generated report bound to
+the hashes of all six package files, followed by
+`PASS_TERNARY_DISJOINTNESS_REPAIR`. No receipt is handwritten or required
+as a committed input. The all-h and all-field conclusions come from the
+written proof, not the finite enumeration.
+
+## Scope, provenance and credit
+
+Scientific base: `a5df48c55ea806d7952b65acc9c76d878ff09b13`, priority revision 7.
+The selected frontier remains unchanged. The `formal-interface-lemma` card
+is changed to an original characteristic-three side theorem; this is not
+a formalization or a replay of another contribution.
+
+Ali Romman's [#4962](https://github.com/CrocSwap/integer-mult-bounds/pull/4962)
+provides the binary rank theorem, tensor representation and endpoint-deletion
+approach. Its exact scientific head is
+`378275c8e1228d7cdad4888d808a8b8c6395b32e`. Its retained proof and README
+are pinned as provenance, not executed. mikey1201's
+[#172](https://github.com/CrocSwap/integer-mult-bounds/pull/172) supplies
+the earlier binary disjointness endpoint, with the icekylinx/#144 compiler
+and bookkeeping lineage credited there. No predecessor implementation or
+cost ledger is imported. The new theorem and verifier are produced by Nick Petalas.
+Independent human and formal proof-kernel review are unclaimed. Apache-2.0.
+
+Before claiming, live PRs, recent account contributions, handoffs, active
+Discussions, question-specific local reservations, and all-main README and
+merged-PR term searches were checked. The supplementary cache covered 331
+open PRs and 4,356 Discussion records; local note coverage was sparse.
+These checks do not cover arbitrary diffs or unpublished work. The
+[advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19144847)
+aimed for a first original rank statement; the odd-dimensional theorem is
+that first result, and the even-dimensional question is left open under the
+instruction to ship the first improvement.
+
+Physical coefficient preparation, paid reads/copies, dirty restoration,
+native frames, compiler/stock/precision/tape costs, actual caller integration
+and complete multiplication bounds remain unproved. No binary invoice is
+transferred to characteristic three. No selected cold replay, Lean, Docker
+or predecessor scientific verifier is run.
+
+## Verification design
+
+The checker has no recursion, external commands or input files beyond its
+six source hashes. Every matrix dimension is capped at 512. The largest
+elimination is 510 by 510, the largest dense inverse check is 128 by 128,
+and the separate kernel census has exactly 3^6 vectors. Functions stay
+below 60 lines. Explicit checks remain active under `-O`.
+
+Power of Ten rule 3 deviation: CPython allocates integers and lists during
+arithmetic. Scope is this terminating, fixed-size verifier; fixed dimension
+guards bound live storage by O(512^2) scalar slots and retained case results
+are limited to four rows. Normal/optimized replay verifies those guarded cases. A future
+larger replay must revise the explicit capacities and memory analysis.
+Warning-strict execution supplies the available interpreter diagnostics;
+there is no project-wide static analyzer requirement for this standalone
+standard-library proof check.
+
+## Open next questions
+
+- What is rank_F3(I-A_h) for even h >= 4? This would complete the ternary
+  classification. Start with the full tensor eigenspaces and the two-endpoint
+  restriction when T^4=I; the odd-dimensional inverse no longer applies.
+  Blocker: that singular full-matrix deletion calculation is not done here.
+- Can a nonadditive physical repair avoid this rank-one obstruction?
+  Start by stating an all-input ternary identity and its complete paid bill.
+  Blocker: no such physical caller or accounting contract is supplied.

research/ternary-disjointness-repair/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13",
+  "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/PROOF.txt",
+      "usage": "provenance",
+      "git_blob": "96b0e770da33660eff812df8b74302b15c557e59",
+      "sha256": "f831bc6fe5af6ad87dd028070c6db60d55f8bd1ffad052ed27092b671ab2a427"
+    },
+    {
+      "path": "research/boolean-disjointness-repair/README.md",
+      "usage": "provenance",
+      "git_blob": "5d659814e9445026ec44a64993559890dfd92a60",
+      "sha256": "b37e421642070fe7769189655c29e8fd68100000292938ffbd4d5f777a1edc11"
+    }
+  ]
+}

research/ternary-disjointness-repair/TASK.json

@@ -0,0 +1,101 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 7,
+  "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13",
+  "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 rank_F(I-A_h)=2^h-2 for every odd h>=3 over every characteristic-three field, with an explicit inverse and exact additive rank-one repair count.",
+  "scope_change_reason": "Original characteristic-three algebraic counterpart of Ali Romman PR4962; this is a written proof side result, not a proof-assistant binding or predecessor audit.",
+  "bottleneck_link": "A maximal-rank repair obstruction for a changed coefficient field; no ternary physical supplier or transferred binary ledger is assumed.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first proved original rank statement; stop at the odd-dimensional theorem and leave even dimensions and other fields open.",
+  "outcome": "completed",
+  "evidence": "PROOF.md supplies the all-odd-h argument and explicit inverse. verify.py checks exact ranks at h=3,5,7,9, literal inverses at h=3,5,7, all 729 ternary kernel vectors at h=3, six rejecting controls and the h=2 boundary counterexample.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "What is rank_F3(I-A_h) for even h>=4?",
+      "why_it_matters": "Completes the ternary additive-repair classification.",
+      "first_step": "Analyze the full tensor eigenspaces and two-endpoint restriction when T^4=I.",
+      "blocked_by": "The full inverse used here is unavailable for even h."
+    },
+    {
+      "question": "Can a nonadditive physical repair evade the rank-one obstruction?",
+      "why_it_matters": "The theorem excludes only additive scalar decompositions, not general programs.",
+      "first_step": "State an exact all-input ternary identity and complete paid bill.",
+      "blocked_by": "No physical ternary caller or accounting contract is supplied."
+    }
+  ]
+}

research/ternary-disjointness-repair/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 ternary ranks, full and corrected inverse identities, endpoint block, independent complete h=3 kernel census, invalid-domain and corrupted-inverse rejection, h=2 counterexample."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "The same complete finite replay with Python assertions disabled."
+    }
+  ]
+}