diff --git a/research/all-field-s3-shortest-rigidity/README.md b/research/all-field-s3-shortest-rigidity/README.md new file mode 100644 index 0000000000..b486d63785 --- /dev/null +++ b/research/all-field-s3-shortest-rigidity/README.md @@ -0,0 +1,198 @@ +# Shortest S3 single-target words are rigid over every field + +Scoped proof. For every field K, every finite number of dirty registers, and +every rank-one idempotent E, exactly three rank-one calls with simple S3 labels +implement the formal target I+([sts]-1)E only when their labels are sts or tst +and all three scalar couplings equal E. Non-idempotent couplings, complex +scalar mixing and more restored dirty registers do not produce another +normalized shortest word. No new kappa or supplier admission is claimed. + +This contribution was produced by Nick Petalas. New work: Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. + +## New step and predecessor credit + +Brian's [PR #4740](https://github.com/CrocSwap/integer-mult-bounds/pull/4740), +retained at `f2369119c5229405fd8ea8d9477c8f8cf1692f4d`, already proves the +binary shortest-word theorem. Its proof also explicitly supplies the +arbitrary-binary-matrix coefficient criterion, so removing the binary +idempotence restriction alone is inherited. The new result extends the +rigidity conclusion to every coefficient field, including characteristic +zero and odd characteristic. The signed expansion has terms with coefficient +2 which disappear in the predecessor's binary argument. The proof below +retains them and never divides by 2. + +Credit unpaidmoon / #4647 for the three-call question and shorter-word support +argument; Riquelme Soares / #4351, Cinna Davis, Wentao Li and the register-model +lineage credited in #4740. Their results are cited, not replayed. David Arias's +[Coxeter tariff theorem #2738](https://github.com/CrocSwap/integer-mult-bounds/pull/2738) +is a binary cost theorem for a much broader group family. It does not supply +this all-field equality classification. No predecessor executable is imported. + +## Model + +Work in M_n(K[S3]), n >= 1. Set s=(0 1), t=(1 2), z=sts=tst=(0 2), +with group product g h acting as g(h(i)). Define + +```text +F_h(A) = I + ([h]-[e]) A, h in {s,t}. +D_z(E) = I + ([z]-[e]) E, E^2=E, rank(E)=1. +``` + +Scalar matrices commute with group basis elements, and need not commute with +one another. Paid couplings A have rank one. They need not be idempotent. +This enlarged algebraic class even permits singular factors, making its +exclusion stronger than one restricted to legal invertible operations. +Non-idempotent factors need not be involutions outside characteristic two. + +Equality is coefficientwise in the full group algebra on all n inputs and +outputs. For E=e_j e_j^T, one register receives [z] and every other arbitrary +dirty register is restored. Observing just the target register is insufficient. +Factors are in written product order, with the rightmost acting first. + +Arbitrary free GL_n(K) maps are allowed. Move them through paid factors by +conjugating the couplings, which preserves rank. Augmentation [g] maps to 1 +and sends each paid factor and the target to I, so the residual free scalar +map is I. The theorem classifies these normalized couplings. It does not +assert uniqueness of the literal interleaved free maps or price those maps. + +## Theorem and proof + +**Theorem.** F_a(A) F_b(B) F_c(C)=D_z(E), with rank A=rank B=rank C=1, +if and only if (a,b,c) is (s,t,s) or (t,s,t) and A=B=C=E. +Consequently the minimum paid length is three for every n and K. + +Every term of an expansion has a group label given by an ordered subword of +the paid labels. No subword of length at most two is z. Among three-letter +words only sts and tst can contribute to [z]. This also excludes all shorter +programs. Interchanging s and t reduces the proof to F_s(A) F_t(B) F_s(C). + +The full signed expansion has the following coefficients, over the integers +before specializing to K. + +```text +[e] I-A-B-C+AB+BC+2AC-2ABC +[s] A+C-AB-BC-2AC+2ABC +[t] B-AB-BC+ABC +[st] AB-ABC +[ts] BC-ABC +[z] ABC +``` + +Match [z], [st], [ts], and [t], in that order. They give + +```text +ABC=E, AB=BC=E, B=E. +``` + +Thus AE=E and EC=E. The [s] coefficient gives + +```text +A+C=2AC. (1) +``` + +Since rank A=rank E=1 and AE=E, im A=im E. The idempotent E is the +identity on this image, hence EA=A. Left-multiply (1) by E, using EC=E, +to get A+E=2AC. Subtract (1) to get C=E. Now AC=AE=E, so (1) gives +A=E. This uses subtraction only, and remains valid in characteristic two. +The middle coupling already equals E. In fact the argument only needs the +rank-one condition on A; it forces the other two ranks automatically. + +For the converse, decompose the register space as im E plus ker E. Each +F_h(E) is [h] on im E and I on ker E. The alternating three-call words +therefore have exactly the claimed full formal endpoint. This proves both +directions and supplies the upper bound without scratch or free mixing. + +The same coefficient table gives a useful criterion for arbitrary A,B,C: +the alternating word attains D_z(E) if and only if + +```text +B=E, AE=E, EC=E, A+C=2AC. +``` + +The identity coefficient then equals I-E automatically. Rank restrictions +cannot be discarded from the rigidity theorem: A=C=I and B=E satisfy this +criterion in every field, while A and C have rank n. This example also shows +why a correct lower bound does not imply uniqueness in a larger alphabet. + +## Exact evidence and reproduction + +`verify.py` independently expands all eight label words with integer +noncommutative scalar coefficients. It checks the entire signed table and +the opposite alternating word. This is an exact coefficient calculation, +not a numerical field sample or a formal proof-kernel check. + +The new finite domain is K=F3 and n=2. The verifier enumerates every nonzero +rank-one matrix as an outer product and every three-call word using either +label. It compares every formal group coefficient and every register entry +against all rank-one-idempotent targets. This census includes nilpotents and +singular factors. All 262,144 words yield exactly 24 hits, two for each of the +12 targets. The binary census of #4740 is not rerun. + +A separate literal 12 by 12 left regular-action calculation checks a rational +oblique projector. Seven boundary-control groups cover a nilpotent middle +factor, a singular middle factor, wrong labels, an omitted factor, valid +higher-rank nonrigidity, dirty-spectator leakage and the false assumption that +every rank-one factor is an involution in odd characteristic. + +From the repository root, using the standard library only: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/all-field-s3-shortest-rigidity +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/all-field-s3-shortest-rigidity/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/all-field-s3-shortest-rigidity/verify.py +``` + +Use any CPython 3.12 executable at another installation. Every direct run is +read-only and emits a generated JSON receipt with recomputed counts and SHA256 +hashes of all five package files. Receipts and logs belong outside the checkout. +`SOURCES.json` pins historical provenance only; there are no live input imports. + +## Scope, budget and stopping decision + +Base `624de9dc66858af0945e5f8a0942488d62280d43`, priority revision 7. +The selected source-binding control passed; it was metadata orientation, not +a supplier replay. The card's historical balanced baseline is superseded by +the current guidance's `research_selected_baseline.py` command. + +This changes the bit-new-register-model card to an all-field equality side +result. The changed premise is the scalar coefficient field. It clarifies a +formal complex-mixing alternative to the binary register model without +claiming a physically priced alphabet. The original card's native supplier +acceptance gate remains unmet. Stop at this first verified extension. + +Initial searches covered live open PR titles and bodies, this account's recent +work, active Discussions, merged S3 rigidity searches and every main README +for distinctive field/rigidity terms. The cached card search covered 365 open +PRs and 3,819 Discussion records at 21:45-21:46 UTC on 2026-10-22. Sparse local +notes, arbitrary code diffs and unpublished work were not fully searched. +No-match searches do not establish novelty. The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19133362) +records the intended scope. + +No longer-word search, native implementation, paid mixing/hosting, precision, +recursive bill, all-size multiplier, selected frontier update, Lean or Docker +run is supplied. The all-field conclusion rests on the written proof; finite +checks corroborate it. No unbounded computation is used to infer it. + +## Open next questions + +Can a concrete native complex register interface realize and price these +rank-one calls with free scalar mixing replaced by its actual cost? This +matters before the formal all-field exclusion can be applied to a supplier. +Start with one reflection and an explicit noncoordinate projector, listing +every scalar operation, frame conversion and dirty return. No such native +contract is supplied here. Longer searches in this same three-call model +cannot change the equality theorem and are not a justified next step. + +## Verifier implementation limits + +The verifier has no recursion, subprocesses, network access, external mutable +state or generated code. Its largest enumeration is the explicit eight label +words times the cube of the 32-matrix ternary alphabet; all other loops use +fixed dimensions at most 12. Functions fit within 60 lines. Explicit exception +checks survive optimized execution. Python allocates tuples and small maps +dynamically; fixed loop domains bound their live sizes. Maximum live formal +state has six 2 by 2 coefficient blocks, with a separate 12 by 12 rational +matrix fixture. The registered runs enable warnings as errors in ordinary +and optimized Python. These are local verifier properties, not properties of +a physical multiplier. diff --git a/research/all-field-s3-shortest-rigidity/SOURCES.json b/research/all-field-s3-shortest-rigidity/SOURCES.json new file mode 100644 index 0000000000..fd829eefab --- /dev/null +++ b/research/all-field-s3-shortest-rigidity/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "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/s3-shortest-word-rigidity/README.md", + "usage": "provenance", + "git_blob": "9c5f825cfbec82766752bc022c9427152a198819", + "sha256": "b2f54faff0bac7aac74a7886decdcd30d193a6ee9f9ed48f4b7079469a68e841" + }, + { + "path": "research/coxeter-root-tariff/README.md", + "usage": "provenance", + "git_blob": "9ed141d29e7f552d9cbc9c0f499b4dc901bdee13", + "sha256": "e8ad34f2926dadd897d2f9c6ee7295ecc61cfa13c776ab1c6ea5be82fdc1fa93" + } + ] +} diff --git a/research/all-field-s3-shortest-rigidity/TASK.json b/research/all-field-s3-shortest-rigidity/TASK.json new file mode 100644 index 0000000000..1e11d2a030 --- /dev/null +++ b/research/all-field-s3-shortest-rigidity/TASK.json @@ -0,0 +1,64 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "All-field shortest-word rigidity for one rank-one S3 target, with arbitrary finite restored dirty workspace and rank-one scalar couplings.", + "scope_change_reason": "Replace the binary scalar coefficient field by an arbitrary field and prove an equality classification. This is a formal side result rather than native supplier admission.", + "bottleneck_link": "Clarifies whether complex scalar mixing can create a different shortest normalized register word; no paid-profile gain is claimed.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified all-field extension; do not extend the search.", + "outcome": "completed", + "evidence": "README.md contains the scoped proof. verify.py checks integer coefficients, the complete new ternary domain, an exact rational regular-action fixture and seven boundary-control groups.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can one concrete native complex interface realize and fully price these rank-one calls?", + "why_it_matters": "The formal theorem does not price scalar mixing, frames or restoration.", + "first_step": "Specify one reflection and noncoordinate projector with every scalar operation, frame conversion and dirty return.", + "blocked_by": "No native caller contract or favorable complete bill is supplied." + } + ] +} diff --git a/research/all-field-s3-shortest-rigidity/VERIFY.json b/research/all-field-s3-shortest-rigidity/VERIFY.json new file mode 100644 index 0000000000..95890641ae --- /dev/null +++ b/research/all-field-s3-shortest-rigidity/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": 180, + "checks": "Exact signed coefficients; complete ternary three-call census; rational regular-action fixture and semantic controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Repeat the complete evidence with optimized execution; all contracts remain enabled." + } + ] +} diff --git a/research/all-field-s3-shortest-rigidity/verify.py b/research/all-field-s3-shortest-rigidity/verify.py new file mode 100644 index 0000000000..4ba1115ad0 --- /dev/null +++ b/research/all-field-s3-shortest-rigidity/verify.py @@ -0,0 +1,196 @@ +#!/usr/bin/env python3 +"""Exact signed coefficients and a new ternary-domain census. Read-only.""" + +from fractions import Fraction +from hashlib import sha256 +from itertools import permutations, product +import json +from pathlib import Path + + +GROUP = tuple(permutations(range(3))) +IDENTITY = (0, 1, 2) +S = (1, 0, 2) +T = (0, 2, 1) +Z = (2, 1, 0) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def compose(g, h): + return tuple(g[h[i]] for i in range(3)) + + +def symbolic(labels): + """Expand with integer coefficients and noncommuting A,B,C.""" + terms = {(IDENTITY, ()): 1} + for variable, label in enumerate(labels): + out = {} + for (group, word), coefficient in terms.items(): + for address, suffix, sign in ( + (IDENTITY, (), 1), + (IDENTITY, (variable,), -1), + (label, (variable,), 1), + ): + key = (compose(group, address), word + suffix) + out[key] = out.get(key, 0) + sign * coefficient + terms = {key: value for key, value in out.items() if value} + return {g: {w: c for (h, w), c in terms.items() if h == g} for g in GROUP} + + +def check_symbolic(): + a, b, c = (0,), (1,), (2,) + ab, ac, bc, abc = (0, 1), (0, 2), (1, 2), (0, 1, 2) + expected = { + IDENTITY: {(): 1, a: -1, b: -1, c: -1, ab: 1, bc: 1, ac: 2, abc: -2}, + S: {a: 1, c: 1, ab: -1, bc: -1, ac: -2, abc: 2}, + T: {b: 1, ab: -1, bc: -1, abc: 1}, + compose(S, T): {ab: 1, abc: -1}, + compose(T, S): {bc: 1, abc: -1}, + Z: {abc: 1}, + } + need(symbolic((S, T, S)) == expected, "signed integer coefficient table") + swapped = {compose(Z, compose(g, Z)): v for g, v in expected.items()} + need(symbolic((T, S, T)) == swapped, "opposite alternating coefficient table") + for labels in product((S, T), repeat=3): + top = symbolic(labels)[Z] + need(bool(top) == (labels in ((S, T, S), (T, S, T))), "label support") + return 8 + + +def identity(n): + return tuple(int(i == j) for i in range(n) for j in range(n)) + + +def add(a, b, p): + return tuple((x + y) % p if p else x + y for x, y in zip(a, b, strict=True)) + + +def scale(a, scalar, p): + return tuple((scalar * x) % p if p else scalar * x for x in a) + + +def multiply(a, b, n, p): + out = tuple(sum(a[i*n+k] * b[k*n+j] for k in range(n)) + for i in range(n) for j in range(n)) + return tuple(x % p for x in out) if p else out + + +def factor(label, a, n, p): + return {IDENTITY: add(identity(n), scale(a, -1, p), p), label: a} + + +def formal_multiply(left, right, n, p): + out = {} + zero = (0,) * (n*n) + for g, a in left.items(): + for h, b in right.items(): + label = compose(g, h) + out[label] = add(out.get(label, zero), multiply(a, b, n, p), p) + return {g: a for g, a in out.items() if any(a)} + + +def word(labels, matrices, n, p): + out = {IDENTITY: identity(n)} + for label, matrix in zip(labels, matrices, strict=True): + out = formal_multiply(out, factor(label, matrix, n, p), n, p) + return out + + +def rank_one_ternary(): + vectors = tuple(v for v in product(range(3), repeat=2) if any(v)) + matrices = {tuple(x*y % 3 for x in u for y in v) for u in vectors for v in vectors} + need(len(matrices) == 32, "ternary rank-one matrix enumeration") + return tuple(sorted(matrices)) + + +def ternary_census(): + matrices = rank_one_ternary() + targets = tuple(a for a in matrices if multiply(a, a, 2, 3) == a) + need(len(targets) == 12, "ternary target enumeration") + target_lookup = { + tuple(sorted(factor(Z, a, 2, 3).items())): a for a in targets + } + hits = {a: 0 for a in targets} + words = 0 + for labels in product((S, T), repeat=3): + factors = tuple(tuple(factor(g, a, 2, 3) for a in matrices) for g in labels) + for i, a in enumerate(matrices): + for j, b in enumerate(matrices): + prefix = formal_multiply(factors[0][i], factors[1][j], 2, 3) + for k, c in enumerate(matrices): + endpoint = formal_multiply(prefix, factors[2][k], 2, 3) + target = target_lookup.get(tuple(sorted(endpoint.items()))) + if target is not None: + need(a == b == c == target, "unexpected nonrigid ternary word") + need(labels in ((S, T, S), (T, S, T)), "nonalternating hit") + hits[target] += 1 + words += 1 + need(set(hits.values()) == {2}, "two words per ternary target") + need(words == 8 * 32**3, "complete census coverage") + return {"words": words, "targets": len(targets), "hits": sum(hits.values())} + + +def regular_matrix(formal, n): + """Independent literal left regular action, without formal multiplication.""" + size = 6*n + rows = [[0] * size for _ in range(size)] + for g, a in formal.items(): + for column, h in enumerate(GROUP): + row = GROUP.index(compose(g, h)) + for i in range(n): + for j in range(n): + rows[6*i+row][6*j+column] += a[n*i+j] + return tuple(x for row in rows for x in row) + + +def rational_and_controls(): + e = (Fraction(1, 2), Fraction(1, 2), Fraction(1, 2), Fraction(1, 2)) + need(multiply(e, e, 2, 0) == e, "rational oblique target") + factors = tuple(regular_matrix(factor(g, e, 2, 0), 2) for g in (S, T, S)) + actual = multiply(multiply(factors[0], factors[1], 12, 0), factors[2], 12, 0) + need(actual == regular_matrix(factor(Z, e, 2, 0), 2), "rational regular endpoint") + zero, coord = (0, 0, 0, 0), (1, 0, 0, 0) + nilpotent, singular = (0, 1, 0, 0), (2, 0, 0, 0) + controls = ( + ((S, T, S), (coord, nilpotent, coord)), + ((S, T, S), (coord, singular, coord)), + ((S, S, T), (coord, coord, coord)), + ((S, T, S), (coord, coord, zero)), + ) + for labels, couplings in controls: + need(word(labels, couplings, 2, 3) != factor(Z, coord, 2, 3), "invalid word accepted") + # Rank two invalidates rigidity: scratch actions cancel. + full = identity(2) + need(word((S, T, S), (full, coord, full), 2, 3) == factor(Z, coord, 2, 3), + "higher-rank counterexample") + # Correct first output alone does not restore the dirty spectator. + leaking = (1, 0, 1, 0) + endpoint = word((S, T, S), (leaking, leaking, leaking), 2, 3) + target = factor(Z, coord, 2, 3) + need(all(endpoint.get(g, zero)[:2] == target.get(g, zero)[:2] for g in GROUP), + "data-only false-positive fixture") + need(endpoint != target, "dirty spectator leak missed") + # Arbitrary nilpotents are involutions only in characteristic two. + twice = word((S, S), (nilpotent, nilpotent), 2, 3) + need(twice != {IDENTITY: identity(2)}, "binary involution premise leaked") + return 7 + + +def main(): + labels = check_symbolic() + census = ternary_census() + controls = rational_and_controls() + package = Path(__file__).resolve().parent + names = ("README.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + hashes = {name: sha256((package / name).read_bytes()).hexdigest() for name in names} + receipt = {"status": "PASS_ALL_FIELD_S3_RIGIDITY", "symbolic_label_words": labels, + "ternary": census, "control_groups": controls, "sha256": hashes} + print(json.dumps(receipt, sort_keys=True)) + + +if __name__ == "__main__": + main()