From a59c2bf803d05799cceb19e201b38f4e6b852fd5 Mon Sep 17 00:00:00 2001 From: pinterbanget Date: Thu, 22 Oct 2026 17:10:57 +0700 Subject: [PATCH] =?UTF-8?q?Literally=20check=20#4601's=20radical-invarianc?= =?UTF-8?q?e=20cost=20formula=20on=20a=20noncommutative=20local=20algebra?= =?UTF-8?q?=20(F4[e;Frob]/e^2)=20and=20three=20further=20local=20rings:=20?= =?UTF-8?q?holds=20on=20every=20target=20(no=20new=20=CE=BA)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 5.5 --- .../pr4601-noncommutative-check/README.md | 59 ++++++ .../pr4601-noncommutative-check/SOURCES.json | 18 ++ .../pr4601-noncommutative-check/TASK.json | 100 +++++++++ .../pr4601-noncommutative-check/VERIFY.json | 18 ++ .../pr4601-noncommutative-check/verify.py | 193 ++++++++++++++++++ 5 files changed, 388 insertions(+) create mode 100644 research/pr4601-noncommutative-check/README.md create mode 100644 research/pr4601-noncommutative-check/SOURCES.json create mode 100644 research/pr4601-noncommutative-check/TASK.json create mode 100644 research/pr4601-noncommutative-check/VERIFY.json create mode 100644 research/pr4601-noncommutative-check/verify.py diff --git a/research/pr4601-noncommutative-check/README.md b/research/pr4601-noncommutative-check/README.md new file mode 100644 index 0000000000..75fe3514c9 --- /dev/null +++ b/research/pr4601-noncommutative-check/README.md @@ -0,0 +1,59 @@ +# Literal check of #4601 on a noncommutative local algebra + +**Task:** independent-moment (independent check). **Base:** canonical main `f626db5c`. **No κ is claimed.** + +## The claim + +petalas's #4601 (head `4b2322fc`) concerns finite products R of local K-algebras, with **no commutativity assumed**, and invertible 2×2 targets M in the two-role alphabet. The alphabet has paid factors I + u yᵀ (u ∈ R², y ∈ K²) and free maps in GL₂(K) anywhere. #4601 proves + +```text +cost_R(M) ≤ 2 ⇔ cost_D(M̄) ≤ 2, cost_R(M) = max(δ_R(M), cost_D(M̄)), D = R/J. +``` + +Its census covers the commutative dual numbers (F₂[e]/e²)^k only. + +## What is checked here + +Costs are computed **literally from the definition**. There is no pivot test and nothing is imported. + +- **Cost sets.** cost ≤ c means M lies in S_c, where S₀ = GL₂(K) and S_c = S_{c−1} · P · GL₂(K). +- **Right cosets suffice.** Conjugation by GL₂(K) permutes the paid factors: g P(u,y) g⁻¹ = P(gu, g⁻ᵀy). So only right-coset representatives of S_{c−1} need to be multiplied. +- **Invertible factors suffice.** M₂ of a finite ring is Dedekind-finite, so non-invertible factors can never appear in an invertible product. +- **Invertibility test.** A matrix is invertible exactly when v ↦ xv is injective on R². +- **Residue costs** are computed the same way over D. + +Each ring is checked on every invertible target (k = 1): + +| ring R (K) | D | invertible targets | cost 0/1/2/3 | targets where δ raises the cost above the residue cost | +|---|---|---|---|---| +| **F₄[e; Frobenius]/e² (F₂), noncommutative** | F₄ | 46,080 | 6 / 1,710 / 44,364 / 0 | 23,130 | +| F₂[x]/x³ (F₂) | F₂ | 1,536 | 6 / 270 / 1,260 / 0 | 1,530 | +| F₃[e]/e² (F₃) | F₃ | 3,888 | 48 / 1,536 / 2,304 / 0 | 3,840 | +| F₂[e]/e² (F₂), control | F₂ | 96 | **6 / 54 / 36 / 0** | 90 | + +The noncommutative ring has multiplication (a + be)(c + de) = ac + (ad + bc²)e. The verifier checks that it is local, that its non-units form a two-sided ideal, and that it is genuinely noncommutative: ω·e ≠ e·ω. + +## Results + +- **#4601's formula holds on every target of every ring,** including the noncommutative one. So does the two-factor invariance cost_R ≤ 2 ⇔ cost_D ≤ 2. +- **Control.** The F₂[e]/e² histogram reproduces #4601's published k = 1 histogram [6, 54, 36, 0], from independent code. +- **Failure control.** The residue cost alone is wrong on many targets in each ring, as the last column shows. The δ term is therefore needed. + +## Verify + +```text +python3 -B research/pr4601-noncommutative-check/verify.py +``` + +The check takes about 4 s and uses the standard library only. + +## Limitations + +- **One component only.** Cost-three targets need k ≥ q + 1 components, and none arise here. So this package checks the radical-invariance and δ parts of the formula, including the noncommutative case, but not the three-factor regime. #4601's own (F₂[e]/e²)³ census covers that regime in the commutative case. +- **Not claimed.** A supplier or κ. + +## Open next questions + +- **Noncommutative three-factor regime.** Check it with T₄³ or a smaller noncommutative local algebra over F₂ with k = 3. First step: find the smallest noncommutative local F₂-algebra (order 16 is the candidate). Its k = 3 product has about 10¹⁴ targets, so a symmetry-reduced census is needed. + +Credit: petalas (Nick Petalas) for #4601; ToikY (#4334), #4276 and Wentao Li (#4099) for the alphabet and its predecessor results. Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. diff --git a/research/pr4601-noncommutative-check/SOURCES.json b/research/pr4601-noncommutative-check/SOURCES.json new file mode 100644 index 0000000000..a2a5ea8bbd --- /dev/null +++ b/research/pr4601-noncommutative-check/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40", + "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + } + ] +} diff --git a/research/pr4601-noncommutative-check/TASK.json b/research/pr4601-noncommutative-check/TASK.json new file mode 100644 index 0000000000..b70eff6ae4 --- /dev/null +++ b/research/pr4601-noncommutative-check/TASK.json @@ -0,0 +1,100 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 7, + "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1", + "original_card": { + "id": "independent-moment", + "question": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/staged544-mixed-fourth-entry/README.md", + "research/staged-fourth-mixture-ceiling/README.md", + "research/r437-two-window-carrier/README.md" + ], + "methods": [ + "Independently reconstruct one changed paid ledger or pooled dual with exact source and model binding.", + "Check a genuinely uncovered moment implication with a different enclosure method and semantic controls." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Choose one uncovered implication in #4088 literal mixed fill, #4091 pooled dual/model binding or #4067 changed frame/host bill. #4091 pins an earlier #4088 head: validate word, capacity and stock equivalence before applying that ceiling to the later fill.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Independently reconstruct one changed ledger or pooled certificate with a positive case and a semantic failure control. Compare exact sources and name what existing checks miss. Keep this separate from supplier-boundary-audit (ordinary/outer dispatch) and uniform-transfer-audit (all-size proof). Stop after the chosen implication; more digits of an unchanged root are not additional mechanism coverage.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification.", + "Calling an aggregate histogram or source archive an independently accepted physical supplier." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering", + "4088", + "4091", + "4067", + "staged544-mixed-fourth-entry", + "staged-fourth-mixture-ceiling", + "r437-two-window-carrier" + ], + "existing_checks": [ + { + "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.", + "evidence": "research/staged-fourth-mixture-ceiling/README.md", + "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.", + "status": "author-checked", + "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.", + "evidence": "research/r437-two-window-carrier/README.md", + "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.", + "status": "author-checked", + "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "unchanged", + "actual_scope": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?", + "scope_change_reason": null, + "bottleneck_link": "Independent literal coverage of #4601's noncommutative-local claim, beyond its commutative census.", + "budget_minutes": 60, + "stop_rule": "Stop at k = 1 rings.", + "outcome": "completed", + "evidence": "Literal cost closure on every invertible target of F4[e;Frob]/e^2 (noncommutative, 46,080), F2[x]/x^3 (1,536), F3[e]/e^2 (3,888), F2[e]/e^2 (96, reproduces [6,54,36,0]); formula max(delta, cost_D) and two-factor invariance hold everywhere; residue-only control fails on many targets.", + "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance", + "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance; no independent human review.", + "open_questions": [ + { + "question": "Noncommutative three-factor regime (k >= q+1).", + "why_it_matters": "Tests #4601 where cost 3 occurs without commutativity.", + "first_step": "Symmetry-reduced census on a product of three noncommutative local F2-algebras.", + "blocked_by": "Size (~1e14 targets)." + } + ] +} diff --git a/research/pr4601-noncommutative-check/VERIFY.json b/research/pr4601-noncommutative-check/VERIFY.json new file mode 100644 index 0000000000..a024e0cf5c --- /dev/null +++ b/research/pr4601-noncommutative-check/VERIFY.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Literal cost closure over four local rings incl. noncommutative T4; #4601 formula and two-factor invariance on every target; published k=1 histogram control; residue-only failure control; locality/noncommutativity checks." + } + ] +} diff --git a/research/pr4601-noncommutative-check/verify.py b/research/pr4601-noncommutative-check/verify.py new file mode 100644 index 0000000000..bbcc482078 --- /dev/null +++ b/research/pr4601-noncommutative-check/verify.py @@ -0,0 +1,193 @@ +#!/usr/bin/env python3 +"""Literal check of PR #4601 (petalas) on a noncommutative local algebra and further local rings. + +#4601 (head 4b2322fc): over a finite product R of local K-algebras (non-units a proper two-sided ideal J, no +commutativity assumed), for invertible 2 x 2 targets M in the two-role alphabet + paid factors P(u, y) = I + u y^T (u in R^2, y in K^2), free maps GL_2(K) anywhere, + delta_R(M) = min_{T in GL_2(K)} dim_K((M T - I) K^2), +it proves cost_R(M) <= 2 iff cost_D(Mbar) <= 2, and cost_R(M) = max(delta_R(M), cost_D(Mbar)), D = R/J. +Its census enumerates (F2[e]/e^2)^k, k <= 3 (commutative). + +Independent literal check (no pivot test, no imported predecessor code): costs are computed from the definition as +the least c with M in S_c, S_0 = GL_2(K), S_c = S_{c-1} P GL_2(K). Because g P(u,y) g^-1 = P(g u, g^-T y), it +suffices to multiply right-coset representatives of S_{c-1} by every paid factor. Paid factors are restricted to +invertible ones: M_2 of a finite ring is finite, hence Dedekind-finite, so a product is invertible only if every +factor is. Residue costs over D are computed the same way over D. Rings, all with k = 1: + * T4 = F4[e; Frobenius]/e^2 over K = F2: (a + b e)(c + d e) = ac + (ad + b c^2) e; NONCOMMUTATIVE local, D = F4; + * F2[x]/x^3 (K = F2, D = F2), F3[e]/e^2 (K = F3, D = F3); + * F2[e]/e^2, whose cost histogram must reproduce #4601's published k = 1 histogram [6, 54, 36, 0]. +Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0. +""" +from itertools import product +import json +import sys + +GF4_MUL = [[0, 0, 0, 0], [0, 1, 2, 3], [0, 2, 3, 1], [0, 3, 1, 2]] # 2 = w, 3 = w + 1, w^2 = w + 1 + + +def need(condition, message): + if not condition: + raise AssertionError(message) + + +class Ring: + def __init__(self, name, elems, add, mul, p, scalar, coords, residue): + self.name, self.p = name, p + self.elems = list(elems) + self.index = {e: i for i, e in enumerate(self.elems)} + n = len(self.elems) + self.add = [[self.index[add(a, b)] for b in self.elems] for a in self.elems] + self.mul = [[self.index[mul(a, b)] for b in self.elems] for a in self.elems] + self.zero, self.one = self.index[scalar(0)], self.index[scalar(1)] + self.scalar = [self.index[scalar(k)] for k in range(p)] + self.neg = [next(j for j in range(n) if self.add[i][j] == self.zero) for i in range(n)] + self.coords = [coords(e) for e in self.elems] + self.residue = [residue(e) for e in self.elems] + self.units = {i for i in range(n) if any(self.mul[i][j] == self.one and self.mul[j][i] == self.one + for j in range(n))} + + def mat_mul(self, x, y): + a, m = self.add, self.mul + return (a[m[x[0]][y[0]]][m[x[1]][y[2]]], a[m[x[0]][y[1]]][m[x[1]][y[3]]], + a[m[x[2]][y[0]]][m[x[3]][y[2]]], a[m[x[2]][y[1]]][m[x[3]][y[3]]]) + + def invertible(self, x): + """v -> x v is a right-linear self-map of the finite module R^2; it is invertible iff injective, and its + inverse is again left multiplication by a matrix, so x is invertible iff the kernel is zero.""" + a, m, z = self.add, self.mul, self.zero + return not any(a[m[x[0]][v1]][m[x[1]][v2]] == z and a[m[x[2]][v1]][m[x[3]][v2]] == z + for v1, v2 in self.nonzero_vectors) + + def setup(self): + n = len(self.elems) + self.ident = (self.one, self.zero, self.zero, self.one) + self.nonzero_vectors = [v for v in product(range(n), repeat=2) if v != (self.zero, self.zero)] + self.gl = [x for x in product(range(n), repeat=4) if self.invertible(x)] + self.glset = set(self.gl) + s = self.scalar + self.free = [g for g in (tuple(s[v] for v in t) for t in product(range(self.p), repeat=4)) if g in self.glset] + self.paid = [] + for u1, u2 in product(range(n), repeat=2): + for y1, y2 in product(range(self.p), repeat=2): + if (y1, y2) == (0, 0): + continue + m = self.mul + f = (self.add[self.one][m[u1][s[y1]]], m[u1][s[y2]], m[u2][s[y1]], self.add[self.one][m[u2][s[y2]]]) + if f in self.glset: + self.paid.append(f) + return self + + def costs(self, max_cost=4): + cost = {g: 0 for g in self.free} + layer = set(self.free) + for c in range(1, max_cost + 1): + reps = {min(self.mat_mul(x, g) for g in self.free) for x in layer} + new = set() + for x in reps: + for f in self.paid: + t = self.mat_mul(x, f) + for g in self.free: + h = self.mat_mul(t, g) + if h not in cost: + cost[h] = c + new.add(h) + layer = {h for h, v in cost.items() if v <= c} + if len(cost) == len(self.gl): + break + return cost + + def delta(self, x): + best = 2 + for t in self.free: + mt = self.mat_mul(x, t) + cols = [] + for j in range(2): + e1 = self.add[mt[j]][self.neg[self.one if j == 0 else self.zero]] + e2 = self.add[mt[2 + j]][self.neg[self.one if j == 1 else self.zero]] + cols.append(self.coords[e1] + self.coords[e2]) + best = min(best, rank_mod(cols, self.p)) + return best + + + +def rank_mod(rows, p): + rows, r = [list(x) for x in rows], 0 + for c in range(len(rows[0])): + piv = next((i for i in range(r, len(rows)) if rows[i][c] % p), None) + if piv is None: + continue + rows[r], rows[piv] = rows[piv], rows[r] + inv = pow(rows[r][c], p - 2, p) + rows[r] = [v * inv % p for v in rows[r]] + for i in range(len(rows)): + if i != r and rows[i][c] % p: + f = rows[i][c] + rows[i] = [(a - f * b) % p for a, b in zip(rows[i], rows[r])] + r += 1 + return r + + +def gf4_bits(a): + return (a & 1, a >> 1 & 1) + + +def rings(): + t4 = Ring("F4[e;Frob]/e^2 over F2", product(range(4), repeat=2), + lambda x, y: (x[0] ^ y[0], x[1] ^ y[1]), + lambda x, y: (GF4_MUL[x[0]][y[0]], GF4_MUL[x[0]][y[1]] ^ GF4_MUL[x[1]][GF4_MUL[y[0]][y[0]]]), + 2, lambda k: (k, 0), lambda e: gf4_bits(e[0]) + gf4_bits(e[1]), lambda e: (e[0],)) + f4 = Ring("F4 over F2", product(range(4), repeat=1), lambda x, y: (x[0] ^ y[0],), + lambda x, y: (GF4_MUL[x[0]][y[0]],), 2, lambda k: (k,), lambda e: gf4_bits(e[0]), lambda e: e) + + def trunc(p, length): + def mul(x, y): + out = [0] * length + for i in range(length): + for j in range(length - i): + out[i + j] = (out[i + j] + x[i] * y[j]) % p + return tuple(out) + return Ring("F%d[x]/x^%d" % (p, length), product(range(p), repeat=length), + lambda x, y: tuple((a + b) % p for a, b in zip(x, y)), mul, p, + lambda k: (k,) + (0,) * (length - 1), lambda e: e, lambda e: (e[0],)) + + def field(p): + return Ring("F%d" % p, product(range(p), repeat=1), lambda x, y: ((x[0] + y[0]) % p,), + lambda x, y: (x[0] * y[0] % p,), p, lambda k: (k,), lambda e: e, lambda e: e) + return [(t4, f4), (trunc(2, 3), field(2)), (trunc(3, 2), field(3)), (trunc(2, 2), field(2))] + + +def main(): + out = {} + for big, small in rings(): + big.setup() + small.setup() + if big.name.startswith("F4[e"): + x, y = big.index[(2, 0)], big.index[(0, 1)] + need(big.mul[x][y] != big.mul[y][x], "T4 is noncommutative") + need(all((big.residue[i] != (0,)) == (i in big.units) for i in range(len(big.elems))), "local: units by residue") + need(all(big.mul[a][j] not in big.units and big.mul[j][a] not in big.units + for j in range(len(big.elems)) if j not in big.units for a in range(len(big.elems))), + "non-units form a two-sided ideal") + cost_r, cost_d = big.costs(), small.costs() + need(len(cost_r) == len(big.gl) and len(cost_d) == len(small.gl), "every invertible target reached") + res_index = {e: i for i, e in enumerate(small.elems)} + hist, bad, residue_only_wrong = [0] * 4, 0, 0 + for m, c in cost_r.items(): + mbar = tuple(res_index[big.residue[v]] for v in m) + hist[c] += 1 + cd = cost_d[mbar] + bad += (c != max(big.delta(m), cd)) + ((c <= 2) != (cd <= 2)) + residue_only_wrong += c != cd + need(bad == 0, "#4601 formula and two-factor invariance on every target of %s" % big.name) + need(residue_only_wrong > 0, "failure control: the residue cost alone is wrong on some targets") + out[big.name] = {"invertible_targets": len(big.gl), "cost_histogram_0_3": hist, + "targets_where_delta_raises_cost": residue_only_wrong, + "free": len(big.free), "paid_invertible_factors": len(big.paid)} + need(out["F2[x]/x^2"]["cost_histogram_0_3"] == [6, 54, 36, 0], "#4601 published k = 1 histogram") + out["F2[e]/e^2 (= F2[x]/x^2) control"] = out.pop("F2[x]/x^2") + print(json.dumps({"status": "PASS_PR4601_LITERAL_LOCAL_CHECK", "rings": out, "new_kappa_claimed": False}, + indent=1)) + + +if __name__ == "__main__": + sys.exit(main())