Research: rank-8 complex decoders are gauge-rigid; E-graph eight-term floor (no new kappa)

research/complex-rank8-decoder-rigidity/CLAIM.md

@@ -0,0 +1,37 @@
+# Local sprint claim (no pinned coordination issue exists)
+
+- Recorded: 2026-10-13T17:00Z; result recorded 2026-10-13 evening (UTC).
+- Track: 40–49, structural decoder research. Assignment seed **47**, drawn once with
+  `python3 -c "import secrets; print(secrets.randbelow(100))"` (OS randomness) at 2026-10-13T16:59:56Z.
+- Start commit: `2921874911956718fcaaaf9396fe8267b3cfa9f0` (main at 17:00Z, selected κ 0.001661960547713947, PR942,
+  complex side binds). Rebased before submission onto main `1b59b624d21924f8e3537cdc1ac52d3be6eda2fe` (selected κ 0.001672660197076918, PR1094);
+  the package is additive and its statements do not depend on the selected record.
+- Object: rank-8 decoders in PR717's E-graph-only copy-cost model (D1(a)) on P112: is every rank-8 real
+  matrix with K_ii = 4 and K_ij = 0 on orthogonal root pairs diagonally gauge-equivalent to 2G? This is the
+  step PR717 D1(b) records as ARGUED (local rigidity D1(d) plus a sampled global search), and the model
+  PR968 lists as not covered.
+- Method: pivot reduction on a live frame; D4-block / S(3,4,8) structure; propositional zero-exclusion with a
+  shipped DRUP refutation replayed by an independent RUP checker; exact algebra for the class and gluing
+  lemmas; exact rational checks of the corollary; numerical random-start probes as non-proof evidence.
+- Candidates considered and not chosen: (1) the n ≥ 9 mixed-β floor on P112 (PR717 open problem; SAT/CP-SAT
+  attempts recorded as killed; too risky for the window); (2) k = 2 labellings of punctured in-cap graphs in
+  dimension ≤ 17 (PR446 §6.2 covers only the full graph; value for the construction unclear);
+  (3) realization pricing of PR968's asymmetric centres (requires the complex word compiler; PR717 recorded
+  the price without shipping it).
+- Expected deliverable: research note / scoped structural result with a written proof and an exact
+  verifier. No κ claim.
+- Expected finish: same day (hard stop 2026-10-13 23:01 UTC).
+
+## Result
+
+- Delivered as `research/complex-rank8-decoder-rigidity/` (research note / scoped structural result, no κ claim).
+- Theorem: on P112 and P120 every rank-≤8 solution of the E-graph system is D(2G)D^{-1}. Corollary: eight
+  costly terms in the E-graph model have PR968 normal-form supports, hence cst ≥ 64 (P112) / 72 (P120).
+- Extension (same PR, second commit batch): the theorem transfers to the 336 P104 units of type (2,2,2,2)
+  (cst ≥ 56); zero exclusion holds on P111 and all 1260 P104 units; the missing proof input for the other
+  P104 types and P111 is recorded.
+- Reproduce: `python3 -I -B research/complex-rank8-decoder-rigidity/verify.py` (and `--live P120`), about 10 s CPU (up to ~30 s wall) each; 61 checks on P112, 41 on P120.
+- Overlap re-checked against the PR list (through #1210) and the discussion board before submission; the concurrent
+  #1191 (one-sided mask rigidity, any term count) and #1180 (all-pairs, both factors root-linear) are complementary,
+  not duplicates; see README.
+- Submitted: https://github.com/CrocSwap/integer-mult-bounds/pull/1212 (status: research note / scoped structural result, no κ claim).

research/complex-rank8-decoder-rigidity/SOURCES.json

@@ -0,0 +1,43 @@
+{
+  "base_commit": "1b59b624d21924f8e3537cdc1ac52d3be6eda2fe",
+  "selected_record": {
+    "path": "certificates/selected-result.json",
+    "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32",
+    "kappa": "836330098538459/500000000000000000",
+    "decimal": "0.001672660197076918",
+    "source_pr": 1094,
+    "note": "unchanged by this package; the result makes no kappa claim"
+  },
+  "pinned_files_in_main": {
+    "research/complex-frame-pair-decoders/PROOF.md": "ba53c1d8a9bc2d935d546bde46ca7341bd65f8515013e07b073296b4db2a9a74",
+    "research/complex-frame-pair-decoders/README.md": "edd848b0177dc73a6e2646d4fd82f0b2ceae37e642bf19d6af602579a041a57e",
+    "research/complex-frame-pair-decoders/verify.py": "bdf7ee497dc04dfc634ee5b7848f6a2b39b0169668fb1a60a9715111dbd15395",
+    "research/format-limits/README.md": "0fa0d6b2df96ddc06b876c41c5fa8d2335b97f36bc8f17d1371296d23199c263",
+    "research/five-port-quadratic-decoder/sources/pr446-PROOF.md": "7a8c3bab633c08e7d96297dec9f9e7ed68d6bd0e076b73310c7d6b08a16df017"
+  },
+  "pinned_files_in_open_prs": {
+    "PR717 research/format-limits-2/README.md": {
+      "head": "4a97676294f9fa413b65986e9984fddeda71e4cc",
+      "git_blob": "4e78bd5c50d037627ea2bc7505432659b3eb16c9",
+      "sha256": "fa69ebcade9150675a540150e1200045394dcb45abbe8ab9669934b0be53fadd",
+      "used_for": "rows D1(a)-(d), D2, D3: model, open problem, ARGUED status"
+    },
+    "PR717 research/format-limits-2/s5-6-decoders-spec/checks/e8model.py": {
+      "head": "4a97676294f9fa413b65986e9984fddeda71e4cc",
+      "git_blob": "489a3e2c12e58c0e824eb6c49f5168ddc6756085",
+      "sha256": "7255d13ef349e7a549c0f26addf35ef72d28c72343f3abfcbab2f5eba74834a5",
+      "used_for": "definitions cross-checked (line order, FRAME0, label pairing, pairing-rank cost); not executed"
+    },
+    "PR717 research/format-limits-2/s5-6-decoders-spec/checks/d1_decoder_floor.py": {
+      "head": "4a97676294f9fa413b65986e9984fddeda71e4cc",
+      "git_blob": "cfb61a2f77d81bc5101a74e47331abf3b2475415",
+      "sha256": "ef4b7aa039f9c259b94f92e1e2519f00256e1574556980c2490127954608db6e",
+      "used_for": "the E-graph reduction and the D1(b)/(d) computations referred to; not executed"
+    }
+  },
+  "proof_generation": {
+    "tool": "python-sat 1.9.dev15 (Glucose 4.1, with_proof=True) via make_proof.py",
+    "note": "verify.py does not depend on python-sat; it replays the DRUP files (proof-<L>.drup for the full CNF, proof-<L>-two-diag.drup for the reduced CNF with only the two-term and diagonal families) with its own RUP checker"
+  },
+  "start_commit": "2921874911956718fcaaaf9396fe8267b3cfa9f0 (main at the start of the work; the package was rebased onto main at the end)"
+}

research/complex-rank8-decoder-rigidity/make_proof.py

@@ -0,0 +1,56 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: Apache-2.0
+"""Regenerate the DRUP refutation checked by verify.py (needs python-sat; verify.py itself does not).
+
+    python3 -I -B research/complex-rank8-decoder-rigidity/make_proof.py --live P112 --out /new/proof-P112.drup
+
+The CNF is built by verify.build_zero_cnf with its deterministic variable numbering, conjoined with the
+clause "some pattern variable is true" (some entry of K[:,F] or K[F,:] vanishes on its block).  A DRUP
+proof produced by any solver can be substituted; verify.py replays it with its own RUP checker.
+"""
+import argparse
+import sys
+from pathlib import Path
+
+sys.path.insert(0, str(Path(__file__).resolve().parent))
+import verify as V  # noqa: E402
+
+
+def main():
+    ap = argparse.ArgumentParser()
+    ap.add_argument('--live', default='P112', help='P112, P120, or an extension unit name (P111, P104-44, P104-2222, P104-11111111)')
+    ap.add_argument('--out', required=True)
+    ap.add_argument('--solver', default='g4', help='pysat solver name with proof support (g4 = Glucose 4.1)')
+    ap.add_argument('--families', default=None, help='comma-separated clause families (default all: two,four,diag,trans)')
+    args = ap.parse_args()
+    from pysat.solvers import Solver
+    if args.live in ('P112', 'P120'):
+        live = V.P112 if args.live == 'P112' else V.P120
+        F = V.choose_pivot(live)
+    else:
+        units = V.extension_units()[0]
+        live, F, _desc = units[args.live]
+        F = list(F)
+        if args.families is None:
+            args.families = ','.join(V.EXPECTED['EXT']['units'][args.live]['families'])
+    rel = V.blocks_relative(F, live)
+    fams = None if args.families is None else set(args.families.split(','))
+    cnf, zvars, stats = V.build_zero_cnf(live, F, rel, options=fams)
+    clauses = [list(c) for c in cnf.clauses] + [list(zvars)]
+    with Solver(name=args.solver, bootstrap_with=clauses, with_proof=True) as s:
+        sat = s.solve()
+        proof = s.get_proof()
+    if sat:
+        print('UNEXPECTED: satisfiable; a nontrivial zero pattern exists')
+        return 1
+    out = Path(args.out)
+    if out.exists():
+        print(f'refusing to overwrite {out}')
+        return 2
+    out.write_text('\n'.join(proof) + '\n')
+    print(f'UNSAT; wrote {len(proof)} proof lines to {out} (vars {len(cnf.names)}, clauses {len(clauses)}, {stats})')
+    return 0
+
+
+if __name__ == '__main__':
+    sys.exit(main())

research/complex-rank8-decoder-rigidity/probe_numeric.py

@@ -0,0 +1,119 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: Apache-2.0
+"""Numerical probe (evidence, NOT part of the proof): random-start Levenberg-Marquardt on the rank-8
+E-graph system x_i.y_j = 0 (orthogonal live pairs), x_i.y_i = 4, and a diagonal-gauge test of every
+converged solution against 2G.  Requires numpy.  Usage:
+    python3 -I probe_numeric.py <seed> <trials> [P120|P112|P104[,...]]
+Recorded runs are listed in README.md ("Numerical probes")."""
+import itertools, sys, time
+import numpy as np
+
+def _e8_roots():
+    roots = []
+    for i, j in itertools.combinations(range(8), 2):
+        for si in (1, -1):
+            for sj in (1, -1):
+                v = [0] * 8; v[i], v[j] = 2 * si, 2 * sj; roots.append(tuple(v))
+    for s in itertools.product((1, -1), repeat=8):
+        if s.count(-1) % 2 == 0:
+            roots.append(tuple(s))
+    return roots
+_LINES = []; _seen = set()
+for _r in _e8_roots():
+    _k = _r if _r > tuple(-a for a in _r) else tuple(-a for a in _r)
+    if _k not in _seen:
+        _seen.add(_k); _LINES.append(_r)
+NL = len(_LINES)
+RV = np.array(_LINES, dtype=float) / 2.0
+G = np.rint(RV @ RV.T).astype(int)
+FRAME0 = []
+for _a in range(4):
+    for _s in (1, -1):
+        _v = [0] * 8; _v[2 * _a], _v[2 * _a + 1] = 2, 2 * _s; FRAME0.append(_LINES.index(tuple(_v)))
+_P112 = [i for i in range(NL) if i not in FRAME0]
+# PR717 D3(b)'s second punctured frame: its clique indices 9,15,24,46,52,66,94,104 are P112 positions
+# (PR968 verify.py maps them through p112[q]); as 120-line indices they are [11, 17, 28, 52, 60, 74, 102, 112].
+P104_CLIQUE = [_P112[q] for q in (9, 15, 24, 46, 52, 66, 94, 104)]
+assert all(G[a][b] == 0 for a in P104_CLIQUE for b in P104_CLIQUE if a != b) and not set(P104_CLIQUE) & set(FRAME0)
+
+def system(live):
+    L = list(live); n = len(L)
+    orth = [(a, b) for a, i in enumerate(L) for b, j in enumerate(L) if i != j and G[i, j] == 0]
+    return L, n, orth
+
+def residual(z, n, orth, oi, oj):
+    X = z[:8*n].reshape(n, 8); Y = z[8*n:].reshape(n, 8)
+    return np.concatenate([np.einsum('ij,ij->i', X[oi], Y[oj]), np.einsum('ij,ij->i', X, Y) - 4.0])
+
+def jac(z, n, orth, oi, oj):
+    X = z[:8*n].reshape(n, 8); Y = z[8*n:].reshape(n, 8)
+    m = len(orth); J = np.zeros((m + n, 16*n))
+    rows = np.arange(m)
+    for c in range(8):
+        J[rows, 8*oi + c] = Y[oj, c]
+        J[rows, 8*n + 8*oj + c] = X[oi, c]
+    for i in range(n):
+        J[m+i, 8*i:8*i+8] = Y[i]; J[m+i, 8*n+8*i:8*n+8*i+8] = X[i]
+    return J
+
+def lm(z, n, orth, oi, oj, iters=300, tol=1e-20):
+    lam = 1e-3
+    r = residual(z, n, orth, oi, oj); f = r @ r
+    for it in range(iters):
+        J = jac(z, n, orth, oi, oj)
+        A = J.T @ J; g = J.T @ r; dg = np.diag(A)
+        while True:
+            dz = -np.linalg.solve(A + lam * (np.diag(dg) + 1e-12*np.eye(A.shape[0])), g)
+            z2 = z + dz; r2 = residual(z2, n, orth, oi, oj); f2 = r2 @ r2
+            if f2 < f:
+                z, r, f = z2, r2, f2; lam = max(lam / 3, 1e-15); break
+            lam *= 4
+            if lam > 1e14: return z, f
+        if f < tol: break
+    return z, f
+
+def gauge_test(z, L, n):
+    X = z[:8*n].reshape(n, 8); Y = z[8*n:].reshape(n, 8)
+    K = X @ Y.T; Gl = G[np.ix_(L, L)]
+    odd = [(i, j) for i in range(n) for j in range(n) if abs(Gl[i, j]) == 1]
+    if min(abs(K[i, j]) for i, j in odd) < 1e-7:
+        return 'ZERO-ODD-ENTRY', None
+    # d_i/d_j = K_ij/(2G_ij) must be a consistent potential: log|.| is a coboundary and signs consistent
+    w = {(i, j): K[i, j] / (2 * Gl[i, j]) for i, j in odd}
+    pot = np.full(n, np.nan); pot[0] = 1.0; frontier = [0]
+    adj = {i: [] for i in range(n)}
+    for i, j in odd: adj[i].append(j)
+    while frontier:
+        nf = []
+        for i in frontier:
+            for j in adj[i]:
+                if np.isnan(pot[j]): pot[j] = pot[i] / w[(i, j)]; nf.append(j)
+        frontier = nf
+    err = max(abs(w[(i, j)] - pot[i] / pot[j]) / (1 + abs(pot[i] / pot[j])) for i, j in odd)
+    return ('GAUGE-EQUIV' if err < 1e-6 else 'NOT-GAUGE-EQUIV'), err
+
+if __name__ == '__main__':
+    seed = int(sys.argv[1]) if len(sys.argv) > 1 else 0
+    trials = int(sys.argv[2]) if len(sys.argv) > 2 else 8
+    rng = np.random.default_rng(seed)
+    cases = {'P120': [], 'P112': FRAME0, 'P104': FRAME0 + P104_CLIQUE}
+    if len(sys.argv) > 3:
+        cases = {k: v for k, v in cases.items() if k in sys.argv[3].split(',')}
+    for name, punct in cases.items():
+        live = [i for i in range(NL) if i not in punct]
+        L, n, orth = system(live); oi = np.array([p[0] for p in orth]); oj = np.array([p[1] for p in orth])
+        z0 = np.concatenate([(np.sqrt(2) * RV[L]).ravel()] * 2)   # coordinate solution: x_i = y_i = sqrt2 r_i -> x.y = 2<r,r> = 4
+        assert np.max(abs(residual(z0, n, orth, oi, oj))) < 1e-9
+        s = np.linalg.svd(jac(z0, n, orth, oi, oj), compute_uv=False)
+        nul = 16*n - int((s > 1e-8 * s[0]).sum())
+        print(f'{name}: live={n} orth_pairs={len(orth)} unknowns={16*n} eqs={len(orth)+n} tangent_nullity_at_coord={nul} (gauge dim 64+{n}-1={63+n})', flush=True)
+        t0 = time.time(); summary = {}
+        for t in range(trials):
+            z = rng.standard_normal(16 * n)
+            z, f = lm(z, n, orth, oi, oj)
+            if f < 1e-16:
+                tag, err = gauge_test(z, L, n)
+            else:
+                tag, err = f'NOCONV(f={f:.2e})', None
+            summary[tag] = summary.get(tag, 0) + 1
+        print(f'   {trials} random starts -> {summary}  [{time.time()-t0:.0f}s]', flush=True)