diff --git a/research/ternary-disjointness-repair/PROOF.md b/research/ternary-disjointness-repair/PROOF.md new file mode 100644 index 0000000000..680e0adb26 --- /dev/null +++ b/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. diff --git a/research/ternary-disjointness-repair/README.md b/research/ternary-disjointness-repair/README.md new file mode 100644 index 0000000000..1acd9f2e82 --- /dev/null +++ b/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. diff --git a/research/ternary-disjointness-repair/SOURCES.json b/research/ternary-disjointness-repair/SOURCES.json new file mode 100644 index 0000000000..88875d8c7b --- /dev/null +++ b/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" + } + ] +} diff --git a/research/ternary-disjointness-repair/TASK.json b/research/ternary-disjointness-repair/TASK.json new file mode 100644 index 0000000000..8a778b0ffc --- /dev/null +++ b/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." + } + ] +} diff --git a/research/ternary-disjointness-repair/VERIFY.json b/research/ternary-disjointness-repair/VERIFY.json new file mode 100644 index 0000000000..3706f8cdbd --- /dev/null +++ b/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." + } + ] +} diff --git a/research/ternary-disjointness-repair/verify.py b/research/ternary-disjointness-repair/verify.py new file mode 100644 index 0000000000..8fa559b719 --- /dev/null +++ b/research/ternary-disjointness-repair/verify.py @@ -0,0 +1,171 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the odd-dimensional ternary repair theorem.""" + +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path +import platform + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def identity(n): + require(0 < n <= 512, "matrix dimension outside replay bound") + return [[int(i == j) for j in range(n)] for i in range(n)] + + +def multiply(a, b): + n, inner, width = len(a), len(b), len(b[0]) + require(0 < n <= 512 and 0 < inner <= 512 and 0 < width <= 512, + "matrix dimension outside replay bound") + require(all(len(row) == inner for row in a), "left matrix shape") + require(all(len(row) == width for row in b), "right matrix shape") + out = [[0] * width for _ in range(n)] + for i in range(n): + for k in range(inner): + if a[i][k]: + for j in range(width): + out[i][j] += a[i][k] * b[k][j] + out[i] = [x % 3 for x in out[i]] + return out + + +def rank_mod_three(matrix): + require(0 < len(matrix) <= 512, "rank dimension outside replay bound") + width = len(matrix[0]) + require(0 < width <= 512 and all(len(r) == width for r in matrix), + "rank matrix shape") + a = [[x % 3 for x in row] for row in matrix] + rank = 0 + for col in range(width): + pivot = next((i for i in range(rank, len(a)) if a[i][col]), None) + if pivot is None: + continue + a[rank], a[pivot] = a[pivot], a[rank] + inverse = pow(a[rank][col], -1, 3) + a[rank] = [(x * inverse) % 3 for x in a[rank]] + for i in range(rank + 1, len(a)): + if a[i][col]: + scale = a[i][col] + a[i] = [(x - scale * y) % 3 for x, y in zip(a[i], a[rank])] + rank += 1 + if rank == len(a): + break + return rank + + +def tensor_entry(local, u, v, h): + value = 1 + for bit in range(h): + value = value * local[(u >> bit) & 1][(v >> bit) & 1] % 3 + return value + + +def polynomial_inverse(h): + require(type(h) is int and 3 <= h <= 9 and h % 2 == 1, + "replay requires odd integer h in 3..9") + local_powers = ( + ((1, 0), (0, 1)), ((1, 1), (1, 0)), + ((2, 1), (1, 1)), ((0, 2), (2, 1)), + ) + n = 1 << h + return [[2 * sum(tensor_entry(k, u, v, h) for k in local_powers) % 3 + for v in range(n)] for u in range(n)] + + +def repair_matrix(h): + require(type(h) is int and 2 <= h <= 9, "repair replay h outside 2..9") + proper = range(1, (1 << h) - 1) + # This literal set predicate is independent of the tensor-entry evaluator. + return [[(int(u == v) - int(u & v == 0)) % 3 for v in proper] + for u in proper] + + +def corrected_inverse(r): + boundary = (0, len(r) - 1) + inverse_boundary = ((0, 2), (2, 1)) + interior = range(1, len(r) - 1) + return [[(r[u][v] - sum(r[u][boundary[i]] * inverse_boundary[i][j] + * r[boundary[j]][v] + for i in range(2) for j in range(2))) % 3 + for v in interior] for u in interior] + + +def require_inverse(a, candidate): + require(multiply(a, candidate) == identity(len(a)), "inverse identity failed") + + +def rejecting_controls(r, b): + rejected = 0 + for bad in (True, 2, 4, 10): + try: + polynomial_inverse(bad) + except ValueError: + rejected += 1 + raw = [row[1:-1] for row in r[1:-1]] + correct = corrected_inverse(r) + wrong_sign = [[(2 * raw[i][j] - correct[i][j]) % 3 + for j in range(len(b))] for i in range(len(b))] + for candidate in (raw, wrong_sign): + try: + require_inverse(b, candidate) + except ValueError: + rejected += 1 + require(rejected == 6, "a negative control was not rejected") + even = repair_matrix(2) + require(rank_mod_three(even) == 1, "even-dimension counterexample lost") + require(multiply(even, [[1], [1]]) == [[0], [0]], "even kernel witness") + return rejected + + +def main(): + k = [[1, 1], [1, 0]] + k2 = multiply(k, k) + k3 = multiply(k2, k) + require(k2 == [[2, 1], [1, 1]], "K squared") + require(k3 == [[0, 2], [2, 1]], "K cubed") + require(multiply(k3, k) == [[2, 0], [0, 2]], "K fourth power") + cases = [] + for h in (3, 5, 7): + n = 1 << h + r = polynomial_inverse(h) + m = [[(int(u == v) - int(u & v == 0)) % 3 for v in range(n)] + for u in range(n)] + require_inverse(m, r) + boundary = [[r[u][v] for v in (0, n - 1)] for u in (0, n - 1)] + require(boundary == [[2, 2], [2, 0]], "endpoint inverse block") + b = repair_matrix(h) + actual_rank = rank_mod_three(b) + require(actual_rank == n - 2, "odd repair is not full rank") + require_inverse(b, corrected_inverse(r)) + cases.append({"h": h, "dimension": n - 2, "rank": actual_rank}) + b = repair_matrix(9) + actual_rank = rank_mod_three(b) + require(actual_rank == 510, "h=9 repair is not full rank") + cases.append({"h": 9, "dimension": 510, "rank": actual_rank}) + b = repair_matrix(3) + kernel_size = 0 + for x in product(range(3), repeat=6): + if all(sum(a * c for a, c in zip(row, x)) % 3 == 0 for row in b): + kernel_size += 1 + require(kernel_size == 1, "independent full kernel census") + controls = rejecting_controls(polynomial_inverse(3), b) + package = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", + "VERIFY.json", "verify.py") + hashes = {name: sha256((package / name).read_bytes()).hexdigest() for name in names} + report = {"schema": "ternary-disjointness-repair-replay/1", + "python": platform.python_version(), "cases": cases, + "kernel_vectors": 3 ** 6, "kernel_size": kernel_size, + "rejected_controls": controls, "even_counterexample_h": 2, + "source_sha256": hashes} + print(json.dumps(report, sort_keys=True, indent=2)) + print("PASS_TERNARY_DISJOINTNESS_REPAIR odd_h=3,5,7,9 no_new_kappa") + + +if __name__ == "__main__": + main()