diff --git a/research/local-corank-one-cost/PROOF.md b/research/local-corank-one-cost/PROOF.md new file mode 100644 index 0000000000..00e3b03ad6 --- /dev/null +++ b/research/local-corank-one-cost/PROOF.md @@ -0,0 +1,123 @@ +# Residue corank one attains the column bound + +This contribution was produced by Nick Petalas. The result is a scoped +algebraic proof in the formal right-vector alphabet. No new κ is claimed. + +Let K be a field contained in the centre of an associative unital local +K-algebra R. Its nonunits form its Jacobson radical J, and D=R/J is a +division algebra. Neither finite dimension, commutativity, split residue +nor nilpotence of J is assumed. Matrices act on columns on the left. + +A paid factor is I+u y^T, where u is in R^n and y is in K^n. All GL_n(K) +maps are free anywhere in a word. Singular paid factors are allowed. +Write cost(M) for the minimum number of paid factors, or infinity when no +word exists, and define + + delta(M) = min_{T in GL_n(K)} dim_K ((MT-I)K^n). + +The alphabet and column bound are from Wentao Li's #4099, following #2513, +and Nick Petalas's #4243. The two-role local unit-entry theorem is #4276. +The arbitrary-role invertible local theorem is #4787, head +4b58e8cd5690bd35cf01b0018eefa2c39a298920. ToikY's #4334 explicitly leaves +singular targets outside its field-product theorem. The new theorem below +handles singular local endpoints of arbitrary role count and residue corank +one. The arguments below are self-contained and do not replay those results. +Basis extension, Gaussian elimination, Schur complements and local-ring unit +lifting are classical facts, not claimed as new here. + +## The theorem + +For every n>=1 and every M in M_n(R) whose residue has rank n-1 over D, + + cost(M) = delta(M) = n - dim_K M(E) <= n, + E = {v in K^n : Mv belongs to K^n}. + +Here M(E) is a K-linear subspace of K^n. In particular, the zero images in E +must not be counted as fixed directions. The formula n-dim_K(E) used for +invertible targets would be wrong for singular targets. For example, +M=diag(1,...,1,0) has E=K^n but cost(M)=delta(M)=1. + +## 1. The column lower bound and its singular-target form + +Move free maps to the right by conjugation. Each conjugate of a paid factor +is again paid because K is central. A word with t paid factors is P S, +where S is free and P is their product. Expanding P-I successively writes +it as a sum of t terms v_i y_i^T with y_i in K^n. Therefore its image on +K^n has K-dimension at most t. Taking T=S^{-1} proves delta(M)<=cost(M), +including singular words. + +Delta is invariant under free maps on either side. For G,H free, put +T=H^{-1} U G^{-1}. Then + + (GMH T-I)K^n = G(MU-I)K^n. + +Hence the minima agree. Set k=dim_K M(E). For any free T, the fixed subspace +W=ker_K(MT-I) satisfies TW contained in E and M(TW)=W, so dim_K W<=k. +Rank-nullity gives delta(M)>=n-k. + +Conversely choose v_1,...,v_k in E whose images w_i=Mv_i form a basis of +M(E). The v_i are K-linearly independent, since their images are. Extend +both lists to K-bases. Let H have first k columns v_i, and let X have first +k columns w_i. Then N=X^{-1} M H has first k columns e_1,...,e_k, so +(N-I)K^n has dimension at most n-k. Free invariance proves + + delta(M)=n-k. + +This identity holds over every central K-algebra, even if M is unreachable. +The upper bound on cost in the next steps uses the local and residue-rank +hypotheses. + +## 2. Unit pivots before the last column + +In the charts just chosen, write + + N = [[I_k, B], [0, A]], t=n-k. + +The first k residue columns are D-independent. Since rank_D(bar M)=n-1, +rank_D(bar A)=t-1. In particular k<=n-1 and t>=1. + +Gaussian elimination with complete row and column pivoting on bar A +produces t-1 nonzero pivots. Make the same row and column permutations in +N, only among its last t coordinates. Each lifted pivot in the corresponding +Schur complement is outside J, hence is a unit. Eliminating a unit pivot +reduces residue rank by exactly one. Thus the first n-1 leading square +blocks of the resulting N' are invertible over R. The first k columns +remain e_1,...,e_k. No assertion is made about invertibility of N' itself. + +For completeness, the induction uses the block factorization of a matrix +[[a,b],[c,F]] with unit a into invertible triangular factors and diagonal +blocks a and F-ca^{-1}b. It works without commuting any coefficients. +At each stage of a residual block of rank s-1 and size s>=2, there is a +nonzero residue entry. Permuting it into the pivot position preserves +previous leading blocks. This supplies the next unit pivot. At s=1 no +pivot or inverse is needed. + +## 3. An attaining literal word + +Let C_j be the matrix with its first j columns equal to those of N' and +its remaining columns equal to the corresponding identity columns. +Then C_k=I and C_n=N'. For k<=j len(result): + result.append(column) + require(len(result) == n, "basis extension") + return from_columns(result) + + +def scalar_charts(m, r): + n, inputs, outputs = len(m), [], [] + for v in product(range(r.p), repeat=n): + image = tuple(row[0] for row in mm(m, tuple((x,) for x in v), r)) + if all(x < r.p for x in image) and prime_rank(outputs + [image], r.p) > len(outputs): + inputs.append(v) + outputs.append(image) + h, x = extend(inputs, n, r.p), extend(outputs, n, r.p) + return h, x, len(outputs) + + +def pivot_charts(a, r): + n, rows, cols = len(a), list(range(len(a))), list(range(len(a))) + work = [list(row) for row in a] + for j in range(n - 1): + pivot = next(((i, c) for i in range(j, n) for c in range(j, n) + if r.res[work[i][c]]), None) + require(pivot is not None, "insufficient residue rank") + i, c = pivot + rows[j], rows[i] = rows[i], rows[j] + work[j], work[i] = work[i], work[j] + cols[j], cols[c] = cols[c], cols[j] + for row in work: + row[j], row[c] = row[c], row[j] + for i in range(j + 1, n): + multiplier = r.mul[work[i][j]][r.inv[work[j][j]]] + work[i] = [r.add[x][r.neg[r.mul[multiplier][y]]] + for x, y in zip(work[i], work[j], strict=True)] + return tuple(rows), tuple(cols) + + +def construct(m, r): + n = len(m) + require(1 <= n <= 4 and all(len(row) == n for row in m), "role capacity") + require(residue_rank(m, r) == n - 1, "requires residue corank exactly one") + h, x, fixed = scalar_charts(m, r) + a = mm(mm(inverse(x, r), m, r), h, r) + rows, cols = pivot_charts(a, r) + require(rows[:fixed] == cols[:fixed] == tuple(range(fixed)), "fixed columns retained") + a = tuple(tuple(a[i][j] for j in cols) for i in rows) + left = tuple(tuple(int(j == rows[i]) for j in range(n)) for i in range(n)) + right = tuple(tuple(int(i == cols[j]) for j in range(n)) for i in range(n)) + free_left = mm(x, inverse(left, r), r) + free_right = mm(inverse(right, r), inverse(h, r), r) + current, factors = identity(n), [] + for j in range(fixed, n): + target = tuple(tuple(a[i][c] if c <= j else int(i == c) + for c in range(n)) for i in range(n)) + factor = mm(inverse(current, r), target, r) + require(all(factor[i][c] == int(i == c) + for i in range(n) for c in range(n) if c != j), "paid right vector") + factors.append(factor) + current = mm(current, factor, r) + require(mm(mm(free_left, current, r), free_right, r) == m, "literal endpoint") + return free_left, tuple(factors), free_right, n - fixed + + +def expanded_rank(m, r): + columns = [tuple(c for row in m for c in r.coords[row[j]]) for j in range(len(m))] + return prime_rank(columns, r.p) + + +def direct_delta(m, charts, r): + n, values = len(m), [] + for t in charts: + mt = mm(m, t, r) + difference = tuple(tuple(r.add[mt[i][j]][r.neg[int(i == j)]] + for j in range(n)) for i in range(n)) + values.append(expanded_rank(difference, r)) + return min(values) + + +def fold(factors, n, r): + result = identity(n) + for factor in factors: + result = mm(result, factor, r) + return result + + +def apply_word(left, factors, right, vector, r): + value = mm(right, vector, r) + for factor in reversed(factors): + value = mm(factor, value, r) + return mm(left, value, r) + + +def check_target(m, r): + left, factors, right, cost = construct(m, r) + require(len(factors) == cost, "cost matches word") + for j in range(len(m)): + for coordinate in range(r.dimension): + data = tuple((r.p**coordinate if i == j else 0,) for i in range(len(m))) + require(apply_word(left, factors, right, data, r) == mm(m, data, r), + "basis-data execution") + return cost, (left, factors, right) + + +def expect_rejection(action): + try: + action() + except ValueError: + return + raise ValueError("negative control was accepted") + + +def controls(r, witness): + m, (left, factors, right) = witness + n = len(m) + require(len(factors) >= 2, "nontrivial control word") + expect_rejection(lambda: construct(identity(n), r)) + expect_rejection(lambda: construct(tuple(tuple(0 for _ in range(n)) for _ in range(n)), r)) + expect_rejection(lambda: inverse(m, r)) + target = lambda fs: mm(mm(left, fold(fs, n, r), r), right, r) + require(target(factors[:-1]) != m, "omitted final factor control") + require(target(tuple(reversed(factors))) != m, "factor order control") + require(mm(left, fold(factors, n, r), r) != m or + mm(fold(factors, n, r), right, r) != m, "free boundary control") + corrupted = [list(row) for row in factors[-1]] + corrupted[0][-1] = r.add[corrupted[0][-1]][1] + require(target(factors[:-1] + (tuple(tuple(row) for row in corrupted),)) != m, + "changed paid factor control") + radical = tuple(tuple(r.p if i == j else 0 for j in range(2)) for i in range(2)) + expect_rejection(lambda: construct(radical, r)) + return 8 + + +def sampled_targets(r, n, count): + rng, found = Random(17011 + r.size * 31 + n), set() + for _ in range(4000): + m = tuple(tuple(rng.randrange(r.size) for _ in range(n)) for _ in range(n)) + if residue_rank(m, r) == n - 1: + found.add(m) + if len(found) == count: + return tuple(sorted(found)) + raise ValueError("sample capacity exhausted") + + +def check_family(index, r, charts): + records, executions, calibrations, witness = [], 0, 0, None + for n, count in ((3, 80), (4, 40)): + targets = set(sampled_targets(r, n, count)) + if index == 0 and n == 3: + targets.update(tuple(tuple(int(i == j and i < 2) + 2*bits[3*i+j] + for j in range(3)) for i in range(3)) + for bits in product(range(2), repeat=9)) + histogram = [0] * (n + 1) + for position, m in enumerate(sorted(targets)): + cost, word = check_target(m, r) + histogram[cost] += 1 + executions += n * r.dimension + if r.p == 2 and n == 3 and position < 8: + require(direct_delta(m, charts, r) == cost, "independent chart minimum") + calibrations += len(charts) + if index == 0 and n == 3 and cost >= 2: + left, factors, right = word + if fold(factors, n, r) != fold(tuple(reversed(factors)), n, r): + if mm(left, fold(factors, n, r), r) != m: + witness = (m, word) + records.append({"algebra": r.name, "roles": n, "targets": len(targets), + "cost_histogram": histogram}) + return records, executions, calibrations, witness + + +def main(): + algebras = (Algebra("binary dual", 2, 2, "square"), + Algebra("ternary dual", 3, 2, "square"), + Algebra("binary two-generator square-zero", 2, 3, "square"), + Algebra("F4 over F2", 2, 2, "f4"), + Algebra("twisted F4 dual over F2", 2, 4, "twisted")) + charts = tuple(tuple(tuple(bits[3*i+j] for j in range(3)) for i in range(3)) + for bits in product(range(2), repeat=9) + if prime_rank([bits[3*i:3*i+3] for i in range(3)], 2) == 3) + require(len(charts) == 168, "GL3 binary calibration coverage") + records, executions, calibrations, witness = [], 0, 0, None + for index, r in enumerate(algebras): + rows, runs, trials, found = check_family(index, r, charts) + records.extend(rows) + executions += runs + calibrations += trials + if found is not None: + witness = found + require(witness is not None, "control fixture") + count = controls(algebras[0], witness) + comparison_ring = Algebra("commutative F4 dual over F2", 2, 4, "f4dual") + shared_targets = (((1, 0), (0, 4)), ((1, 4), (4, 0))) + shared_costs = tuple(check_target(m, comparison_ring)[0] for m in shared_targets) + require(shared_costs == (1, 2), "shared two-role boundary examples") + package = Path(__file__).resolve().parent + hashes = {name: sha256((package / name).read_bytes()).hexdigest() for name in + ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py")} + result = {"records": records, "basis_data_executions": executions, + "direct_chart_evaluations": calibrations, "controls": count, + "shared_F4_dual_two_role_costs": shared_costs, + "package_sha256": hashes} + print(json.dumps(result, sort_keys=True)) + print("PASS_LOCAL_CORANK_ONE_COST targets=" + str(sum(x["targets"] for x in records)) + + " controls=" + str(count) + " no_new_kappa") + + +if __name__ == "__main__": + main()