From 9d167104f45dcc4f9ff3b7b207c894af8cf1d49f Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Tue, 20 Oct 2026 02:49:56 +0000 Subject: [PATCH] Price integer transvections on the shear target B^k. The unit alphabet already fails the supplier test. Allowing every nonzero integer coefficient makes B itself pass at two roles for a in [0, 1), and makes every higher power fail even before the idle role is dropped. Co-authored-by: unpaidmoon --- research/sl2z-transvection-moment/README.md | 100 ++++++++ .../sl2z-transvection-moment/SOURCES.json | 18 ++ research/sl2z-transvection-moment/TASK.json | 64 +++++ research/sl2z-transvection-moment/VERIFY.json | 18 ++ research/sl2z-transvection-moment/verify.py | 225 ++++++++++++++++++ 5 files changed, 425 insertions(+) create mode 100644 research/sl2z-transvection-moment/README.md create mode 100644 research/sl2z-transvection-moment/SOURCES.json create mode 100644 research/sl2z-transvection-moment/TASK.json create mode 100644 research/sl2z-transvection-moment/VERIFY.json create mode 100644 research/sl2z-transvection-moment/verify.py diff --git a/research/sl2z-transvection-moment/README.md b/research/sl2z-transvection-moment/README.md new file mode 100644 index 0000000000..279c57fe84 --- /dev/null +++ b/research/sl2z-transvection-moment/README.md @@ -0,0 +1,100 @@ +# Arbitrary integer transvections pass for B and fail for every higher power + +**Scoped moment calculation. No new κ, no supplier admission, no selected-frontier change.** +The selected conditional exponent remains `0.001672660197076918`. + +PR #4126 proves that the unit alphabet `{X, X^{-1}, Y, Y^{-1}}` makes every faithful word for `B^k = X^2 Y^2` fail the strict supplier test. Its open question asks whether one explicitly larger alphabet, still implementing the integer matrix rather than the three-bit quotient, can pass for some `a > 0`. This package names that alphabet and prices it. The three-bit quotient is not used as a substitute bill. + +## Alphabet and charge + +Let + +```text +X^t = [[1, t], [0, 1]], Y^t = [[1, 0], [t, 1]], t in Z, t != 0. +``` + +`X^t - I` and `Y^t - I` each have rank 1. The moment parameters are the ones fixed by PR #4126: address width `m = 2`, and a two-role diagonal word whose spectator role is never written. Each allowed transvection is one rank-1 child. There is no cleanup child. The strict test is + +```text +M(a) = (λ / W) * (1/2)^{1-a} < 1, a in [0, 1], +``` + +where `λ` is the number of transvections and `W` is the role count. Equivalently, for a rational `a = p/q`, + +```text +λ^q * 2^p < W^q * 2^q. +``` + +Two readings are reported. `W = 2` counts the idle spectator, as PR #4126 does. `W = 1` charges only the active role. Coefficient size is not a child in this alphabet: `X^2` is one letter, not two unit shears. That omission is stated below and is not treated as a zero cost in any other model. + +## Length + +Write `B = X^2 Y^2 = [[5, 2], [2, 1]]`. Then `B^2 = 6B - I`, so the entries + +```text +u_0 = 1, u_1 = 5, u_k = 6 u_{k-1} - u_{k-2}, +v_0 = 0, v_1 = 2, v_k = 2 u_{k-1} + v_{k-1} +``` + +satisfy `B^k = [[u_k, v_k], [v_k, u_{k-1}]]` and `u_k u_{k-1} - v_k^2 = 1`. The same square relation gives `u_k = 2 v_k + u_{k-1}` and `u_k >= 5 u_{k-1}` for `k >= 1`. + +Consecutive letters from the same family multiply: `X^a X^b = X^{a+b}`. A shortest word therefore alternates, and a word of length 3 that does not alternate reduces to length at most 2. + +- Length 1 is impossible: `v_k != 0`. +- Length 2 is `X^a Y^b = [[1+ab, a], [b, 1]]` or `Y^a X^b = [[1, b], [a, 1+ab]]`. One diagonal entry equals 1. This happens at `k = 1`, by the word `X^2 Y^2`. For `k >= 2` both diagonal entries are at least 5. +- Length 3 is `X^a Y^b X^c` or `Y^a X^b Y^c`. Expanding gives + +```text +X^a Y^b X^c = [[1+ab, a+c(1+ab)], [b, 1+bc]]. +``` + +Matching `B^k` forces `b = v_k`, `1+bc = u_{k-1}` and `1+ab = u_k`. Thus `v_k` must divide both `u_k - 1` and `u_{k-1} - 1`. Those two divisibility statements are equivalent: if `u_k = 1 + a v_k`, the determinant rearranges to `u_{k-1} - 1 = v_k (v_k - a u_{k-1})`, and the converse is the same calculation with the two diagonal entries exchanged. When the divisor exists, the remaining off-diagonal equation holds automatically, because its numerator is `u_k u_{k-1} - 1 = v_k^2`. + +For `k >= 2` the divisor does not exist. Indeed + +```text +v_k - (u_{k-1} - 1) = u_{k-1} + v_{k-1} + 1 > 0 +``` + +and `u_{k-1} - 1 > 0`, so the positive remainder of `u_{k-1} - 1` modulo `v_k` is `u_{k-1} - 1` itself. The `YXY` expansion imposes the same divisibility condition. Therefore `λ(B^k) >= 4` for every `k >= 2`, even if every nonzero integer coefficient is allowed. The explicit word `(X^2 Y^2)^k` shows the matching upper bound `λ(B^k) <= 2k`. + +At `k = 1` the same length-3 equations produce a zero exponent, so they degenerate into the length-2 word. Hence `λ(B) = 2`. + +## Moment + +With `W = 2`: + +- `λ(B) = 2` gives `M(a) = 2^{a-1}`. This is strictly less than 1 for every `a in [0, 1)`, and equals 1 at `a = 1`. The strict test therefore passes for the single matrix `B` at every positive exponent below 1. +- `λ(B^k) >= 4` gives `M(a) >= 2^a >= 1` for every `k >= 2` and every `a in [0, 1]`. The strict test fails for every higher power. + +With `W = 1`, `λ >= 2` gives `M(a) >= 2^a >= 1` for every `a in [0, 1]`. The strict test already fails for `B`. The pass above uses the idle spectator in the denominator. + +The unit sub-alphabet `{X^{±1}, Y^{±1}}` still needs four letters for `B`. A breadth-first search confirms that no shorter unit word exists, which is the `k = 1` case of PR #4126, recomputed here rather than imported. If every coefficient `t` must be expanded into `|t|` unit shears, `X^2 Y^2` costs four children again and the `W = 2` pass disappears. That expansion cost is unknown in the rank-only alphabet; it is not entered as zero. + +## What this does not establish + +This is not a register identity that escapes the three-register obstruction, not a native XOR bill, and not a multiplication theorem. The three-bit quotient of PR #3947 still has an unpriced conversion into these integer matrices. No selected cold replay, Lean proof, or supplier admission was run. An optimistic pass for one matrix, at one role count, is not acceptance under the catalogue gate. + +**Expansion decision: stop.** The unit alphabet fails, the coefficient-free alphabet fails for every power that a recurrence would call, and the single-matrix pass depends on counting an idle role. Another formal-word search is not justified. + +## Evidence + +The length classification and both moment readings are proved above. `verify.py` checks the matrix identities those proofs use through `B^{24}`, the two closed-form expansions on a sample of exponents, the unit-shear breadth-first control, and the strict comparison on every rational exponent with denominator at most 8. It also rejects the boundary `M = 1` and a damaged coefficient. These checks do not replace the divisibility argument. + +```sh +python3.12 -B scripts/research_package.py --package research/sl2z-transvection-moment +``` + +Python 3.12, standard library only. A direct run of `verify.py` is the same check. + +## Open next questions + +1. What child count should the coefficient `t` have if a double is one shift rather than either one child or `|t|` children? The `W = 2` pass and the unit-alphabet failure are the two extremes. A one-shift price for `t = 2` decides which side this alphabet lands on. The blocker is a native operation that is actually legal for that shift; the rank-only model does not provide one. + +## Credit + +- **1337isnot1337 / OpenAI Codex**, PR #3905: the shear generators, the target `B`, and the four-call unit word. +- **ToikY with OpenAI Codex**, PR #3937 and PR #3947: the commutative obstruction, the three-bit quotient, and the request for a supplier inequality. The quotient is not reused as a bill. +- **unpaidmoon**, PR #4126: the unit-alphabet inequality `λ >= 2k+1` in the rank-1 model, and open question 1, which asks for a larger integer alphabet. This package answers that question and does not reopen the unit-letter proof. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. diff --git a/research/sl2z-transvection-moment/SOURCES.json b/research/sl2z-transvection-moment/SOURCES.json new file mode 100644 index 0000000000..a604c6a640 --- /dev/null +++ b/research/sl2z-transvection-moment/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + } + ] +} diff --git a/research/sl2z-transvection-moment/TASK.json b/research/sl2z-transvection-moment/TASK.json new file mode 100644 index 0000000000..e4fd113a49 --- /dev/null +++ b/research/sl2z-transvection-moment/TASK.json @@ -0,0 +1,64 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 6, + "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f", + "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": "Price the integer transvection alphabet {X^t, Y^t : t nonzero} on B^k at the PR #4126 moment parameters, without using the three-bit quotient as a bill.", + "scope_change_reason": "The card asks for a new register identity escaping the three-register obstruction. This package does not build that identity. It answers the larger-alphabet question left open by the unit-shear supplier inequality, which is a different object on the same bit-mechanism track.", + "bottleneck_link": "Side result. A rank-only pass for the single matrix B would matter only if the coefficient were legally one child and the same bound held for the powers a recurrence calls. The powers fail, and dropping the idle role removes the pass, so the selected exponent is unchanged.", + "budget_minutes": 60, + "stop_rule": "Stop once the elementary-length classification and both role-count readings are checked. Do not open a third alphabet in this session.", + "outcome": "partial", + "evidence": "Written length classification for every k, plus exact checks through B^24 of the recurrence, the word (X^2 Y^2)^k, the closed forms, the unit breadth-first control, and the strict moment comparison on rationals of denominator at most 8.", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance for the proof writeup, the verifier, and the overlap selection.", + "open_questions": [ + { + "question": "If a coefficient t=2 is one shift plus a unit shear, rather than one child or two unit children, does M(a)<1 still hold for B at W=2?", + "why_it_matters": "The rank-only pass and the unit-alphabet failure are the two extremes. A legal shift price decides which side this alphabet lands on.", + "first_step": "Name one native operation that implements the shift, charge its rank and any dirty auxiliary, and recompute the two-role moment for the word that uses t=2.", + "blocked_by": "The rank-only model has no such native shift. Inventing one would be a new alphabet, not a corollary of this classification." + } + ] +} diff --git a/research/sl2z-transvection-moment/VERIFY.json b/research/sl2z-transvection-moment/VERIFY.json new file mode 100644 index 0000000000..356914ae7e --- /dev/null +++ b/research/sl2z-transvection-moment/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": 60, + "checks": "Recurrence and word identities through B^24, length obstructions, closed-form expansions, unit breadth-first length 4, and strict moment comparisons including the M=1 boundary rejection." + } + ] +} diff --git a/research/sl2z-transvection-moment/verify.py b/research/sl2z-transvection-moment/verify.py new file mode 100644 index 0000000000..02031d5b05 --- /dev/null +++ b/research/sl2z-transvection-moment/verify.py @@ -0,0 +1,225 @@ +#!/usr/bin/env python3 +"""Exact elementary length and supplier moment for integer transvections. + +The alphabet is {X^t, Y^t : t in Z, t != 0}, each letter one rank-1 child. +No new kappa is computed or claimed. +""" + +from fractions import Fraction + + +def X(t): + return ((1, t), (0, 1)) + + +def Y(t): + return ((1, 0), (t, 1)) + + +def mul(a, b): + return ( + (a[0][0] * b[0][0] + a[0][1] * b[1][0], a[0][0] * b[0][1] + a[0][1] * b[1][1]), + (a[1][0] * b[0][0] + a[1][1] * b[1][0], a[1][0] * b[0][1] + a[1][1] * b[1][1]), + ) + + +def power(word, k): + out = ((1, 0), (0, 1)) + step = ((1, 0), (0, 1)) + for factor in word: + step = mul(step, factor) + for _ in range(k): + out = mul(out, step) + return out + + +def sequence(limit): + """Return u[0..limit], v[0..limit] for B^k = [[u_k, v_k], [v_k, u_{k-1}]].""" + u = [1, 5] + v = [0, 2] + for k in range(2, limit + 1): + u.append(6 * u[k - 1] - u[k - 2]) + v.append(2 * u[k - 1] + v[k - 1]) + return u, v + + +def b_matrix(u, v, k): + return ((u[k], v[k]), (v[k], u[k - 1])) + + +def moment_strict(length, roles, exponent): + """True when (length/roles) * 2^(exponent-1) < 1, for a rational exponent.""" + if not isinstance(exponent, Fraction): + exponent = Fraction(exponent) + if exponent < 0 or exponent > 1: + raise ValueError("exponent outside [0, 1]") + # length * 2^p < roles * 2^q, where exponent = p/q. + p, q = exponent.numerator, exponent.denominator + return length ** q * 2 ** p < roles ** q * 2 ** q + + +def xyx_formula(a, b, c): + # X^a Y^b X^c = [[1+ab, a+c(1+ab)], [b, 1+bc]] + return ( + (1 + a * b, a + c * (1 + a * b)), + (b, 1 + b * c), + ) + + +def yxy_formula(a, b, c): + # Y^a X^b Y^c = [[1+bc, b], [a+c(1+ab), 1+ab]] + return ( + (1 + b * c, b), + (a + c * (1 + a * b), 1 + a * b), + ) + + +def unit_bfs(): + """Shortest positive-or-inverse unit word for B. Returns the length, or None.""" + target = mul(X(1), mul(X(1), mul(Y(1), Y(1)))) + seen = {((1, 0), (0, 1)): 0} + frontier = [((1, 0), (0, 1))] + letters = (X(1), X(-1), Y(1), Y(-1)) + while frontier: + current = frontier.pop(0) + depth = seen[current] + if current == target: + return depth + if depth == 4: + continue + for letter in letters: + nxt = mul(current, letter) + if nxt not in seen: + seen[nxt] = depth + 1 + frontier.append(nxt) + return None + + +def check_identities(limit): + u, v = sequence(limit) + base = mul(X(2), Y(2)) + if base != ((5, 2), (2, 1)): + raise SystemExit("X^2 Y^2 is not B") + # Cayley-Hamilton / the published square relation. + square = mul(base, base) + six = tuple(tuple(6 * entry for entry in row) for row in base) + if square != ( + (six[0][0] - 1, six[0][1]), + (six[1][0], six[1][1] - 1), + ): + raise SystemExit("B^2 != 6B - I") + running = ((1, 0), (0, 1)) + for k in range(1, limit + 1): + running = mul(running, base) + if running != b_matrix(u, v, k): + raise SystemExit(f"word (X^2 Y^2)^{k} missed the recurrence matrix") + det = u[k] * u[k - 1] - v[k] * v[k] + if det != 1: + raise SystemExit(f"determinant drifted at k={k}") + if u[k] != 2 * v[k] + u[k - 1]: + raise SystemExit(f"quotient identity failed at k={k}") + if v[k] != 2 * u[k - 1] + v[k - 1]: + raise SystemExit(f"companion identity failed at k={k}") + if k >= 1 and u[k] < 5 * u[k - 1]: + raise SystemExit(f"growth u_k >= 5 u_{{k-1}} failed at k={k}") + return u, v + + +def check_length(u, v, limit): + for k in range(1, limit + 1): + matrix = b_matrix(u, v, k) + # Length 1: a transvection has a zero off-diagonal entry. + if matrix[1][0] == 0 or matrix[0][1] == 0: + raise SystemExit(f"B^{k} collapsed to one transvection") + # Length 2: XY has bottom-right 1; YX has top-left 1. + if k == 1: + if matrix != mul(X(2), Y(2)): + raise SystemExit("k=1 is not the length-2 word X^2 Y^2") + else: + if matrix[1][1] == 1 or matrix[0][0] == 1: + raise SystemExit(f"B^{k} has an elementary length-2 shape") + gap = v[k] - (u[k - 1] - 1) + # v_k - (u_{k-1}-1) = u_{k-1} + v_{k-1} + 1 > 0, + # and u_{k-1}-1 > 0, so the remainder is not zero. + if gap != u[k - 1] + v[k - 1] + 1: + raise SystemExit(f"remainder gap formula failed at k={k}") + if not (0 < u[k - 1] - 1 < v[k]): + raise SystemExit(f"divisibility obstruction failed at k={k}") + if (u[k] - 1) % v[k] == 0 or (u[k - 1] - 1) % v[k] == 0: + raise SystemExit(f"unexpected length-3 divisor at k={k}") + + +def check_formula_control(): + samples = (-7, -1, 1, 2, 5) + for a in samples: + for b in samples: + for c in samples: + got = mul(X(a), mul(Y(b), X(c))) + if got != xyx_formula(a, b, c): + raise SystemExit("XYX expansion does not match multiplication") + got = mul(Y(a), mul(X(b), Y(c))) + if got != yxy_formula(a, b, c): + raise SystemExit("YXY expansion does not match multiplication") + # The third XYX coordinate identity is the determinant, not an extra constraint. + u, v = sequence(6) + for k in range(2, 7): + # Would-be exponents are not integers; the cleared numerator is v^2. + numerator = (u[k] - 1) + u[k] * (u[k - 1] - 1) + if numerator != v[k] * v[k]: + raise SystemExit("automatic third-coordinate identity failed") + + +def check_moments(limit): + grid = [Fraction(p, q) for q in range(1, 9) for p in range(q + 1)] + for exponent in grid: + if not moment_strict(2, 2, exponent) and exponent < 1: + raise SystemExit(f"W=2 length-2 moment should pass at {exponent}") + if moment_strict(2, 2, Fraction(1, 1)): + raise SystemExit("W=2 length-2 moment is not strict at a=1") + if moment_strict(2, 1, exponent): + raise SystemExit(f"W=1 length-2 moment should fail at {exponent}") + for length in (4, 6, 8): + if moment_strict(length, 2, exponent): + raise SystemExit(f"length {length} should fail the W=2 test at {exponent}") + # k=1 passes on [0, 1); every later checked power has length >= 4. + if limit < 2: + raise SystemExit("need at least B^2") + + +def check_negative_controls(): + if unit_bfs() != 4: + raise SystemExit("unit-shear control did not recover length 4") + # A false divisor claim at k=2 is rejected by the remainder test. + u, v = sequence(2) + if (u[2] - 1) % v[2] == 0: + raise SystemExit("control matrix accidentally had length 3") + # Swapping the strict comparison would accept the boundary M=1. + if moment_strict(4, 2, Fraction(0, 1)): + raise SystemExit("boundary M=1 was treated as a pass") + # Damaging the square coefficient breaks the word/recurrence agreement. + damaged = mul(X(3), Y(2)) + if damaged == mul(X(2), Y(2)): + raise SystemExit("damage control did not move the matrix") + + +def main(): + limit = 24 + u, v = check_identities(limit) + check_length(u, v, limit) + check_formula_control() + check_moments(limit) + check_negative_controls() + print( + "PASS_SL2Z_TRANSVECTION_MOMENT" + f" powers={limit}" + " lambda(B)=2" + " lambda(B^k)>=4_for_k>=2" + " W2_passes_on_[0,1)" + " W1_fails" + " powers_fail" + " no_new_kappa" + ) + + +if __name__ == "__main__": + main()