From 17aa6d42667a7c3412c8d0ad40491db3efbd1d4f Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 11 Nov 2026 21:58:14 +0000 Subject: [PATCH] feat(research): exclude shared length-two S3 transposition words --- .../PROOF.md | 82 ++++++++ .../README.md | 93 +++++++++ .../SOURCES.json | 24 +++ .../TASK.json | 70 +++++++ .../VERIFY.json | 34 +++ .../verify.py | 195 ++++++++++++++++++ 6 files changed, 498 insertions(+) create mode 100644 research/s3-shared-length2-transposition-floor/PROOF.md create mode 100644 research/s3-shared-length2-transposition-floor/README.md create mode 100644 research/s3-shared-length2-transposition-floor/SOURCES.json create mode 100644 research/s3-shared-length2-transposition-floor/TASK.json create mode 100644 research/s3-shared-length2-transposition-floor/VERIFY.json create mode 100644 research/s3-shared-length2-transposition-floor/verify.py diff --git a/research/s3-shared-length2-transposition-floor/PROOF.md b/research/s3-shared-length2-transposition-floor/PROOF.md new file mode 100644 index 0000000000..db19be0e52 --- /dev/null +++ b/research/s3-shared-length2-transposition-floor/PROOF.md @@ -0,0 +1,82 @@ +# Proof: shared length two cannot write the transposition + +## Model + +Let `G = S3` act on the labels `{0,1,2}`, and write + +```text +s = (1 2) = (1,0,2), t = (2 3) = (0,2,1). +``` + +Let `ell(g)` be the reduced word length of `g` with respect to the generating +set `{s,t}`. The six values are + +```text +ell(identity)=0, ell(s)=ell(t)=1, ell(st)=ell(ts)=2, ell((1 3))=3. +``` + +A **paid shared call** is a pair `(g, M)`, where `g` is an element of `G` and +`M` is a nonempty set of registers; the call writes `g` to every register in +`M`. Its cost is `ell(g)`. A **shared word** is a finite sequence of paid +shared calls, and its total cost is the sum of the call costs. If register +`r` belongs to the masks of calls `i1 < i2 < ... < ik`, its induced element is +the ordered product `g_i1 g_i2 ... g_ik`. Registers not written by any call +are left at the identity. + +This is the natural shared-letter cost of the paid alphabet in #4351: one +letter of the alphabet is dispatched to a chosen set of registers, and the +letter is charged its reduced generator length. + +## Proposition + +For every shared word `W` of total cost `L`, every register `r` satisfies +`ell(W_r) <= L`. + +**Proof.** `W_r` is a product of a subsequence of the letters of `W`. The +reduced word length is subadditive: `ell(ab) <= ell(a) + ell(b)` for all +`a,b` in `G`, because concatenating reduced words for `a` and `b` is a word +for `ab`. By induction over the subsequence, + +```text +ell(W_r) <= sum over the calls that write r of ell(g_i) + <= sum over all calls of ell(g_i) = L. +``` + +The second inequality holds because every term is nonnegative. Scratch +registers are ordinary registers in this argument; their number does not +enter. + +## Corollary + +No shared word of total cost at most two writes the transposition `(1 3)` on +any register, with any number of scratch registers. + +**Proof.** If `W_r = (1 3)`, the proposition gives +`3 = ell((1 3)) <= L`, so `L >= 3`. + +The bound is sharp in the stated cost model: the coordinate word +`s, t, s` has cost `3` and writes `(1 3)`. Sharing does not lower that cost, +but it does let one scratch register be restored for one extra call. The +four-call word + +```text +(s, {0,1}), (t, {0}), (s, {0}), (s, {1}) +``` + +writes `s t s = (1 3)` on register `0` and `s s = identity` on register `1`, +at total cost `4`. So a restored scratch costs at least one call beyond the +three-call target word, and no cost-two word can replace it. + +## Finite corroboration + +`verify.py` rebuilds the multiplication table, inverses and the reduced length +table, checks subadditivity on all `36` ordered pairs, and enumerates every +shared word of total cost at most two on two and on three registers. The +enumeration covers every nonempty mask, every cost-one letter, every cost-two +letter, and both positions of a two-call word: `272` words and `768` +register evaluations in total. Every evaluation is distinct in the count and +none equals `(1 3)`. The cost-three, shared cost-four and mutation controls +are asserted separately. + +The finite enumeration is corroboration, not the proof. The all-size +statement is the subadditivity proposition above. diff --git a/research/s3-shared-length2-transposition-floor/README.md b/research/s3-shared-length2-transposition-floor/README.md new file mode 100644 index 0000000000..7279fede6c --- /dev/null +++ b/research/s3-shared-length2-transposition-floor/README.md @@ -0,0 +1,93 @@ +# Shared length two cannot write the S3 transposition + +**Scoped written proof with exact finite corroboration. No new kappa.** +The selected record is unchanged. + +## Result + +In the paid S3 alphabet of +[#4351](../s3-diagonal-rank-screen/README.md), with labels +`s = (1 2)` and `t = (2 3)` and cost equal to reduced generator length, no +shared word of total cost at most **two** writes the transposition +`(1 3)` on any register. This holds for every number of scratch registers. + +The proof is the word-metric inequality: a register receives a product of a +subsequence of the paid letters, so its reduced length is at most the total +paid cost. Since `(1 3)` has length three, cost two cannot produce it. The +bound is sharp: the coordinate word `s, t, s` has cost three and writes +`(1 3)`, and the shared four-call word + +```text +(s, {0,1}), (t, {0}), (s, {0}), (s, {1}) +``` + +writes `(1 3)` on register 0 and restores register 1 at total cost four. + +This answers the open question in #4351: a scratch register does not lower the +length-three floor for `(1 3)`. It does not show that every register model is +exhausted. + +## Model and scope + +A paid shared call is a pair `(g, M)`: one alphabet element `g` written to +every register in the nonempty mask `M`, charged `ell(g)`. A register's +induced element is the ordered product over the calls that write it. This is +the natural shared-letter model for the #4351 alphabet. + +The result is conditional on that cost model. If one paid call may write +*different* alphabet elements to different registers at a single unit cost, +then the induced element is no longer a subsequence product of the charged +letters and the norm bound does not apply. That alternative model is not +addressed here. + +No native source generation, hosting, precision, transfer to the selected +rational-frame supplier, new kappa, register-model escape or complete +multiplication theorem is claimed. The selected frontier and its five +assumptions are unchanged. + +## Evidence + +The standalone verifier imports no predecessor executable and reads no +predecessor file. It rebuilds the S3 multiplication table, inverses and the +reduced length table, checks subadditivity on all 36 ordered pairs, and +enumerates every cost-at-most-two shared word on two and on three registers: +272 words and 768 register evaluations. No induced element is `(1 3)`. The +cost-three attainment, the shared cost-four scratch restoration and two +length-two mutation controls are asserted separately. + +From the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/s3-shared-length2-transposition-floor/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -I -W error -B research/s3-shared-length2-transposition-floor/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/s3-shared-length2-transposition-floor +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/s3-shared-length2-transposition-floor --check-source-history +``` + +Any CPython 3.12 with the standard library can replace the interpreter path. +Expected marker: `PASS_S3_SHARED_LENGTH2_TRANSPOSITION_FLOOR`. The run writes +no files; its receipt hashes the present package files. + +## Open next questions + +1. **Does a different shared-call cost model break the norm bound?** If one + paid call can carry different alphabet elements on different registers for + one unit, the induced element is not a subsequence product. First step: + state that model's exact cost and enumerate its cost-two calls. Blocked by: + the cost is undefined in #4351, so no lower bound can be claimed for it. +2. **Can the same norm obstruction be combined with a target screen at length + three or more?** A cost-three word attains `(1 3)`, so the question becomes + whether a shared schedule can attain a whole diagonal target below the sum + of coordinate costs. First step: pin one target and count shared letters + against its representation rank. Blocked by: no native conversion or + supplier instance is supplied by #4351 or this package. + +## Credit and overlap + +This contribution was produced by Nick Petalas. Riquelme Soares (@hevlyo), PR #4351, supplies the paid S3 alphabet, the +two-dimensional representation, the diagonal target screen and the scratch +question answered here. The reduced word norm, its subadditivity and the +length table of S3 are classical. The finite checks and the proof are new. +Predecessor verifiers, censuses and representation screens were cited rather +than replayed. Apache-2.0. Independent human and formal proof-kernel review +are unclaimed. diff --git a/research/s3-shared-length2-transposition-floor/SOURCES.json b/research/s3-shared-length2-transposition-floor/SOURCES.json new file mode 100644 index 0000000000..6f023a179b --- /dev/null +++ b/research/s3-shared-length2-transposition-floor/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/s3-diagonal-rank-screen/README.md", + "usage": "provenance", + "git_blob": "bb7d255229c794ed21ef9c690f8fe10eec2f11fd", + "sha256": "cbaf17a0d5dc222437dbc94dad5a1b94dd827f193355488df806841857995da9" + } + ] +} diff --git a/research/s3-shared-length2-transposition-floor/TASK.json b/research/s3-shared-length2-transposition-floor/TASK.json new file mode 100644 index 0000000000..086071325d --- /dev/null +++ b/research/s3-shared-length2-transposition-floor/TASK.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "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_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "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": "refined", + "actual_scope": "Fixed nonabelian S3 paid alphabet of #4351: no shared word of total cost at most two writes the transposition (1 3) on any register, for any number of scratch registers.", + "scope_change_reason": "The card asks whether a nonabelian register model escapes the three-register obstruction. #4351 supplies one exact S3 paid alphabet and a screen; this package answers its shared-length-two sub-question at that fixed alphabet. It claims no register-model escape, target identity or paid saving.", + "bottleneck_link": "Side result on the nonabelian register-model route: it closes the cheapest sharing escape (total cost two) for one exact alphabet. The length-three target screen and every native/paid conversion remain open. No kappa, supplier admission or selected-frontier change is claimed.", + "budget_minutes": 60, + "stop_rule": "Stop after the all-size subadditivity proof, the complete cost-at-most-two enumeration and the cost-three and shared cost-four controls. Do not search length three or a different alphabet.", + "outcome": "negative-result", + "evidence": "PROOF.md proves the all-size word-norm bound. verify.py rebuilds S3, checks subadditivity on all 36 ordered pairs, enumerates 272 shared words at total cost at most two on two and three registers (768 register evaluations), and asserts cost-3 attainment, shared cost-4 scratch restoration and two mutation controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does a different shared-call cost model break the word-norm bound?", + "why_it_matters": "If one paid call can carry different alphabet elements on different registers for one unit, the induced element is not a subsequence product.", + "first_step": "State that model exact cost and enumerate its cost-two calls.", + "blocked_by": "The cost is undefined in #4351, so no lower bound can be claimed for that model." + }, + { + "question": "Can the same norm obstruction be combined with a target screen at length three or more?", + "why_it_matters": "A cost-three word attains (1 3), so a whole diagonal target is the next place a sharing gain could appear.", + "first_step": "Pin one target and count shared letters against its representation rank.", + "blocked_by": "No native conversion or supplier instance is supplied by #4351 or this package." + } + ] +} diff --git a/research/s3-shared-length2-transposition-floor/VERIFY.json b/research/s3-shared-length2-transposition-floor/VERIFY.json new file mode 100644 index 0000000000..0e47803a73 --- /dev/null +++ b/research/s3-shared-length2-transposition-floor/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": "S3 table and lengths, subadditivity on 36 pairs, 272 cost<=2 shared words, 768 register evaluations, cost-3 and shared cost-4 controls, two mutations" + }, + { + "argv": [ + "{python}", + "-O", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same acceptance checks under optimization; assertions remain active" + } + ] +} diff --git a/research/s3-shared-length2-transposition-floor/verify.py b/research/s3-shared-length2-transposition-floor/verify.py new file mode 100644 index 0000000000..1833d744c4 --- /dev/null +++ b/research/s3-shared-length2-transposition-floor/verify.py @@ -0,0 +1,195 @@ +#!/usr/bin/env python3 +"""Exact check for the shared length-2 S3 transposition floor. + +Model: a paid call is a pair (g, mask), where g is an S3 element written to +every register selected by the nonempty mask, and the cost is the reduced +generator length of g with respect to s = (1 2) and t = (2 3). A register's +induced element is the ordered product over the calls whose mask contains it. + +The script enumerates every shared word of total cost at most two on two and +three registers, checks that no register receives the transposition (1 3), +and supplies cost-3 and cost-4 attaining controls. Standard library only. +""" + +import hashlib +import itertools +import os + +S = (1, 0, 2) +T = (0, 2, 1) +E = (0, 1, 2) +TARGET = (2, 1, 0) +REGISTER_COUNTS = (2, 3) +PACKAGE_FILES = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", + "VERIFY.json", "verify.py") + + +def compose(a, b): + """Return a after b, acting on positions 0,1,2.""" + return tuple(a[b[i]] for i in range(3)) + + +def inverse(a): + out = [0, 0, 0] + for i, value in enumerate(a): + out[value] = i + return tuple(out) + + +def all_elements(): + return [perm for perm in itertools.permutations(range(3))] + + +def word_lengths(): + """Breadth-first reduced lengths for the generating set {S, T}.""" + distance = {E: 0} + frontier = [E] + while frontier: + nxt = [] + for word in frontier: + for letter in (S, T): + image = compose(letter, word) + if image not in distance: + distance[image] = distance[word] + 1 + nxt.append(image) + frontier = nxt + return distance + + +def products(letters): + out = E + for letter in letters: + out = compose(letter, out) + return out + + +def masks(count): + return [mask for mask in range(1, 1 << count)] + + +def selected(mask, register): + return (mask >> register) & 1 + + +def induce(calls, count): + """Induced element on each register for a shared word.""" + out = [] + for register in range(count): + letters = [g for g, mask in calls if selected(mask, register)] + out.append(products(letters)) + return out + + +def enumerate_cost_at_most_two(count, distance): + """Every nonempty shared word of total paid cost at most two.""" + one_cost = [g for g in all_elements() if distance.get(g) == 1] + two_cost = [g for g in all_elements() if distance.get(g) == 2] + words = [] + for mask in masks(count): + for g in one_cost: + words.append([(g, mask)]) + for g in two_cost: + words.append([(g, mask)]) + for first in masks(count): + for second in masks(count): + for g in one_cost: + for h in one_cost: + words.append([(g, first), (h, second)]) + return words + + +def check_group(distance): + """Multiplication, inverse, length table and subadditivity.""" + elements = all_elements() + assert len(elements) == 6 + for a in elements: + assert compose(a, inverse(a)) == E + assert compose(inverse(a), a) == E + for a in elements: + for b in elements: + c = compose(a, b) + assert distance[c] <= distance[a] + distance[b] + expected = {E: 0, S: 1, T: 1, + compose(S, T): 2, compose(T, S): 2, TARGET: 3} + assert distance == expected, (distance, expected) + assert compose(S, compose(T, S)) == TARGET + assert compose(T, compose(S, T)) == TARGET + return len(elements) ** 2 + + +def check_cost_two(count, distance): + """No cost-at-most-two shared word writes TARGET on any register.""" + words = enumerate_cost_at_most_two(count, distance) + evaluations = 0 + for calls in words: + induced = induce(calls, count) + for register, value in enumerate(induced): + assert value != TARGET, (count, calls, register) + evaluations += 1 + return len(words), evaluations + + +def check_controls(count, distance): + """Cost 3 attains; cost 4 attains and restores one scratch register.""" + assert induce([(S, 1), (T, 1), (S, 1)], count)[0] == TARGET + full = (1 << count) - 1 + restored = [(S, full), (T, 1), (S, 1), (S, 2)] + induced = induce(restored, count) + assert induced[0] == TARGET, induced + if count >= 2: + assert induced[1] == E, induced + # Sharing the same three letters across both registers writes TARGET twice. + shared = [(S, full), (T, full), (S, full)] + assert induce(shared, count)[0] == TARGET + if count >= 2: + assert induce(shared, count)[1] == TARGET + # A cost-2 product is a 3-cycle, never the transposition. + assert compose(S, T) != TARGET and compose(T, S) != TARGET + return 3 + len(restored) + len(shared) + 2 + + +def check_mutation_rejected(count): + """A length-2 product is a 3-cycle, not the transposition.""" + calls = [(S, 1), (T, 1)] + assert induce(calls, count)[0] != TARGET + calls = [(T, 1), (S, 1)] + assert induce(calls, count)[0] != TARGET + return 2 + + +def receipt(): + root = os.path.dirname(os.path.abspath(__file__)) + digest = hashlib.sha256() + present = 0 + for name in PACKAGE_FILES: + path = os.path.join(root, name) + if not os.path.isfile(path): + continue + with open(path, "rb") as handle: + digest.update(name.encode("ascii") + b"\0" + handle.read() + b"\0") + present += 1 + return digest.hexdigest(), present + + +def main(): + distance = word_lengths() + pairs = check_group(distance) + total_words = 0 + total_evaluations = 0 + for count in REGISTER_COUNTS: + words, evaluations = check_cost_two(count, distance) + total_words += words + total_evaluations += evaluations + controls = check_controls(count, distance) + mutation = check_mutation_rejected(count) + print("registers=%d words=%d evaluations=%d controls=%d mutation=%d" + % (count, words, evaluations, controls, mutation)) + digest, present = receipt() + print("PASS_S3_SHARED_LENGTH2_TRANSPOSITION_FLOOR " + "pairs=%d words=%d evaluations=%d target_length=3 " + "shared_cost=4 receipt=%s files=%d" + % (pairs, total_words, total_evaluations, digest[:16], present)) + + +if __name__ == "__main__": + main()