From 41f8f1ffb0c1dd1ba5a87ca67dc40b4bf4c2c12e Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Tue, 20 Oct 2026 02:31:32 +0000 Subject: [PATCH] Prove faithful integer-shear words fail the supplier moment test. The PR3947 one-XOR quotient does not bound the shear-letter bill: B^k needs at least 2k+1 letters, and that charging never satisfies M(a)<1. Co-authored-by: unpaidmoon --- .../README.md | 163 ++++++++ .../SOURCES.json | 18 + .../TASK.json | 64 +++ .../VERIFY.json | 27 ++ .../test_verify.py | 40 ++ .../verify.py | 364 ++++++++++++++++++ 6 files changed, 676 insertions(+) create mode 100644 research/sl2z-shear-recurrence-inequality/README.md create mode 100644 research/sl2z-shear-recurrence-inequality/SOURCES.json create mode 100644 research/sl2z-shear-recurrence-inequality/TASK.json create mode 100644 research/sl2z-shear-recurrence-inequality/VERIFY.json create mode 100644 research/sl2z-shear-recurrence-inequality/test_verify.py create mode 100644 research/sl2z-shear-recurrence-inequality/verify.py diff --git a/research/sl2z-shear-recurrence-inequality/README.md b/research/sl2z-shear-recurrence-inequality/README.md new file mode 100644 index 0000000000..579886658d --- /dev/null +++ b/research/sl2z-shear-recurrence-inequality/README.md @@ -0,0 +1,163 @@ +# The integer-shear supplier inequality fails on faithful words + +**Negative result. No new κ, no supplier admission, no selected-frontier change.** +The selected conditional exponent remains 0.001672660197076918. + +PR #3905 proves that the integer matrix \(B=X^2Y^2\) costs exactly four calls in +its formal shear alphabet, and that the two-role diagonal word restores the +second role with no extra call. PR #3937 shows every commutative algebra +carrier sends \(B\) to the identity. PR #3947 gives a three-bit noncommutative +quotient in which \(\rho(B)\) is one XOR, and stops before the +supplier/recurrence inequality. This package supplies that inequality for the +faithful shear-word bill, and shows why the one-XOR moment cannot replace it. + +## Charging + +Address width \(m=2\), role count \(W=2\), and each letter of +\(\{X,X^{-1},Y,Y^{-1}\}\) is one rank-1 paid child. This is the PR #3905 +model: every legal label differs from the identity by a rational rank-one +matrix, and the displayed endpoint uses two roles. The repository moment is + +\[ +M(a)=\frac{L}{W}\left(\frac{1}{m}\right)^{1-a}=\frac{L}{W}\,m^{a-1} +=\frac{L}{Wm}\,m^{a}, +\qquad a\in[0,1]. +\] + +For \(m>1\), \(M\) is strictly increasing in \(a\). Its minimum on the interval +is \(M(0)=L/(Wm)\) and its maximum is \(M(1)=L/W\). The strict supplier test +is \(M(a)<1\). + +## Faithful length + +Let \(u_k=(B^k)_{11}\). Direct multiplication gives \(B^2=6B-I\), so +\(u_0=1\), \(u_1=5\) and \(u_{k+1}=6u_k-u_{k-1}\). If \(u_k\ge 5u_{k-1}\ge 0\), +then + +\[ +u_{k+1}-5u_k=(6u_k-u_{k-1})-5u_k=u_k-u_{k-1}\ge 4u_{k-1}\ge 0. +\] + +The two linear forms \((6x-y)-5x\) and \(x-y\) agree on the basis pairs +\((1,0)\) and \((0,1)\), hence for every integer pair. Starting from +\(u_1=5u_0\), induction gives \(u_k\ge 5^k\) for every \(k\ge 0\). + +Right multiplication by any one of the four generators replaces each entry by +an integer linear form whose coefficients have \(\ell_1\) norm at most 2 +(explicitly: sums or differences of at most two previous entries). Therefore +every product of \(L\) letters has max-absolute entry at most \(2^L\). Since +\(u_k\ge 5^k>4^k=2^{2k}\) for every \(k\ge 1\), every shear word for \(B^k\) +has length at least \(2k+1\). + +The same Cayley graph, searched through length 4, contains \(B\) and contains +no shorter word. The positive word \(X^2Y^2\) has length 4, so that minimum +is sharp. In particular the growth bound's \(2\cdot 1+1=3\) is not sharp at +\(k=1\); the enumeration is the \(k=1\) input to the moment. + +## The inequality + +Let \(L_k\) be the minimum letter count of \(B^k\). Then \(L_1=4\) and +\(L_k\ge 2k+1\) for \(k\ge 2\), so \(L_k\ge 2k+1\) for every \(k\ge 1\) and the +\(k=1\) count is one larger. + +- For \(k=1\), \(M(0)=4/(2\cdot 2)=1\) and \(M(a)=2^a>1\) for every + \(a\in(0,1]\). The strict test \(M(a)<1\) fails for every \(a\in[0,1]\). +- For \(k\ge 2\), \(M(0)\ge(2k+1)/4>1\), so \(M(a)>1\) for every + \(a\in[0,1]\). + +Raising the rank of a letter above 1 only increases \(M\), because +\(r\mapsto(r/m)^{1-a}\) is increasing for \(1\le r\le m\) and \(a\in[0,1)\). +The rank-1 charging is the most favorable per-letter reading, and it still +fails. + +## What the three-bit quotient does not transfer + +Reducing the integer matrices modulo 3 and passing to the sum-zero subspace +of \(\mathbb F_2^4\) reproduces the PR #3947 matrices. The image of \(B\) is +the single XOR \(b\oplus=c\), and that matrix squares to the identity, so +\(\rho(B^k)\) costs at most one XOR for every \(k\). On width 3 and two roles +that one rank-1 child has \(M(a)\le 1/2<1\). + +There is still no constant \(C\) with \(L_k\le C\) for every \(k\), because +\(L_k\ge 2k+1\). The quotient moment is an upper screen for a different +operation. It is not an upper bound on the faithful supplier moment, and it +does not make the unknown conversion cost zero. The same obstruction applies +to the separate 18-bit matrix boundary in PR #3947: three XORs are still +\(O(1)\) in \(k\), while the faithful letter count is not. + +## Dirty restoration inside the diagonal model + +For \(N=E_{11}\), each paid factor left-multiplies only the first role. The +ordered product \(D([X])^2D([Y])^2\), applied rightmost first, sends an +arbitrary dirty pair \((u,v)\) to \((Bu,v)\). The spectator is not written, so +the four-call bill has no cleanup term to add back. The moment failure above +is the letter count itself. The quotient likewise leaves its second three-bit +block untouched. Neither restoration clause repairs \(M(a)<1\). + +The formal output of \(B^k\) is an integer matrix whose \((1,1)\) entry is +\(u_k\ge 5^k\). The quotient output is three bits. No decode map between them +is priced here, and none is claimed to be free. + +## Evidence + +The length, growth, doubling, moment comparison, diagonal endpoint and +quotient identity are proved above. `verify.py` checks the finite algebraic +steps those proofs use: the matrix for \(B\), Cayley–Hamilton, the linear-form +identity, powers through \(B^{24}\), the length-4 Cayley ball, doubling on +every word through length 6, four dirty pairs, and the three-bit matrices. +`test_verify.py` repeats the strict-failure receipt and rejects an \(\ell_1\) +factor of 1, a length-3 witness, a passing four-letter moment, and a length-4 +witness for \(B^2\). These checks do not replace the induction. + +```sh +python3.12 -B scripts/research_package.py --package research/sl2z-shear-recurrence-inequality +``` + +Python 3.12, standard library only. A direct run of the two scripts is the +same check. No selected cold replay, Lean proof, native bit-supplier +admission, or full group-algebra multiplication was run. + +## Scope + +Card `bit-new-register-model`, scope **changed**. The card asks for a new +register identity. This package does not construct one. It prices the +released supplier/recurrence question on the shear alphabet already fixed by +PR #3905, PR #3937 and PR #3947. Span-four and span-six dirty-auxiliary +censuses are a different question on the same card and are not refined here. + +**Expansion decision: stop.** A passing quotient moment is not acceptance. +Another formal-word search in this alphabet is not justified by a bill that +already fails \(M(a)<1\). + +## Open next questions + +1. Does one explicitly larger legal alphabet, still implementing the integer + matrix \(B\) rather than a quotient, have a paid bill with \(M(a)<1\) at + some \(a>0\)? This is the only nearby route that could make the shear + target a supplier primitive. First name the alphabet, the rank of each + paid gate, and the role count, then apply the same moment test to a proved + letter lower bound. The blocker is that free maps between the present + shear letters are outside this charging; they need their own lemma before + they can be treated as unpaid. + +## Credit + +- **1337isnot1337 / OpenAI Codex (macbook-02)**, PR #3905 at + `b27bf4c72a822b21f483e08cb3241ad9d165b66f`: the shear alphabet, the target + \(B\), the four-call minimum and the diagonal dirty-role bill. +- **ToikY with OpenAI Codex**, PR #3937 at + `5ee1c9cee717e682db01bff4c398b87011a135a2`: the commutative-carrier + obstruction and the request to price a noncommutative bill and the + supplier/recurrence inequality. +- **ToikY with OpenAI Codex**, PR #3947 at + `4026d068981e6e2d5e9f0b96c3cb1ba9957b841f`: the three-bit quotient, the + one-XOR endpoint, and the explicit statement that no supplier inequality + was proved. The matrices checked here are recomputed from the integer + action, not copied as a source archive. +- **eumemic** and **huxint** remain the register-model predecessors cited by + PR #3905. The moment shape is the repository supplier test + \((1/W)\sum n_r(r/m)^{1-a}\). + +New inequality, proofs and checks by **unpaidmoon** with substantial AI +assistance (Cursor Grok 4.7). Apache-2.0. No independent human or +formal-kernel review is claimed. diff --git a/research/sl2z-shear-recurrence-inequality/SOURCES.json b/research/sl2z-shear-recurrence-inequality/SOURCES.json new file mode 100644 index 0000000000..a604c6a640 --- /dev/null +++ b/research/sl2z-shear-recurrence-inequality/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-shear-recurrence-inequality/TASK.json b/research/sl2z-shear-recurrence-inequality/TASK.json new file mode 100644 index 0000000000..b6ff43463c --- /dev/null +++ b/research/sl2z-shear-recurrence-inequality/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": "Prove the supplier moment inequality for faithful shear words of B^k=X^2Y^2, and separate it from the PR3947 one-XOR quotient moment.", + "scope_change_reason": "The card asks for a new register identity that might escape the three-register obstruction. This package does not build one. It answers the supplier/recurrence inequality left open by PR3937 and PR3947 on the shear alphabet those papers already fixed. Span-four and span-six dirty-auxiliary censuses are a different question and are not refined here.", + "bottleneck_link": "A one-XOR quotient moment below 1 does not change the bit primitive. The faithful letter bill fails M(a)<1, so this alphabet is not a supplier saving.", + "budget_minutes": 60, + "stop_rule": "Prove the faithful length lower bound and the moment comparison, check the diagonal spectator and the three-bit quotient, then stop. No new alphabet and no word search past the length-4 ball.", + "outcome": "negative-result", + "evidence": "Every shear word for B^k has at least 2k+1 letters, and B itself has exactly 4. With m=2, W=2 and rank-1 letters, M(a)=2^a at k=1 and M(a)>1 for every a in [0,1] when k>=2. The strict test M(a)<1 fails. The PR3947 quotient costs at most one XOR for every k, so its moment is not a faithful supplier bound.", + "author": "unpaidmoon", + "ai_assistance": "Substantial assistance from Cursor Grok 4.7 in the proof writeup, verifier and checks.", + "open_questions": [ + { + "question": "Does one explicitly larger legal alphabet, still implementing the integer matrix B rather than a quotient, have a paid bill with M(a)<1 at some a>0?", + "why_it_matters": "The present shear alphabet already fails the strict supplier test. Only a changed gate set could make this target a bit-supplier primitive.", + "first_step": "Name the alphabet, the rank of each paid gate and the role count, then apply the same moment test to a proved letter lower bound.", + "blocked_by": "Free maps between the present shear letters are outside this charging and need their own lemma before they can be treated as unpaid." + } + ] +} diff --git a/research/sl2z-shear-recurrence-inequality/VERIFY.json b/research/sl2z-shear-recurrence-inequality/VERIFY.json new file mode 100644 index 0000000000..06ca9cc1f4 --- /dev/null +++ b/research/sl2z-shear-recurrence-inequality/VERIFY.json @@ -0,0 +1,27 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Faithful length of B^k, doubling, moment comparison, diagonal spectator pairs, and the three-bit quotient identity." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 60, + "checks": "Reject an l1 factor of 1, a length-3 witness for B, a passing four-letter moment, and a length-4 witness for B^2." + } + ] +} diff --git a/research/sl2z-shear-recurrence-inequality/test_verify.py b/research/sl2z-shear-recurrence-inequality/test_verify.py new file mode 100644 index 0000000000..9cc5ece157 --- /dev/null +++ b/research/sl2z-shear-recurrence-inequality/test_verify.py @@ -0,0 +1,40 @@ +#!/usr/bin/env python3 +"""Failure controls for the shear recurrence inequality.""" + +import importlib.util +from pathlib import Path + +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location("shear_recurrence", HERE / "verify.py") +verify = importlib.util.module_from_spec(spec) +spec.loader.exec_module(verify) + + +def main() -> None: + receipt = verify.run_checks() + if receipt["strict_supplier_inequality"] is not False or receipt["length_B"] != 4: + raise SystemExit("the faithful bill was reported as a strict supplier pass") + if verify.forms_obey(1): + raise SystemExit("control: l1 factor 1 must reject a two-entry shear") + base = verify.b_matrix() + if verify.shortest_word_length(base, 3) is not None: + raise SystemExit("control: length 3 must not reach B") + if verify.moment_clears_one(4) == "below": + raise SystemExit("control: four rank-1 letters must not satisfy M<1") + if verify.moment_clears_one(5) != "above": + raise SystemExit("control: five letters must lie strictly above 1") + # A length-4 word cannot be B^2: its (1,1) entry is already 29 > 16. + values = verify.diagonal_entries(2) + if not values[2] > 2 ** 4: + raise SystemExit("control: B^2 no longer rules out length 4") + # A spectator write is a different endpoint: Y^2 does not fix Y. + if verify.matmul(verify.Y, verify.Y) == verify.Y: + raise SystemExit("control: a written spectator collapsed") + got_first, got_second = verify.diagonal_endpoint(verify.X, verify.Y) + if got_second != verify.Y or got_first != verify.matmul(base, verify.X): + raise SystemExit("control: diagonal endpoint drifted") + print("PASS_SL2Z_SHEAR_RECURRENCE_TESTS groups=6") + + +if __name__ == "__main__": + main() diff --git a/research/sl2z-shear-recurrence-inequality/verify.py b/research/sl2z-shear-recurrence-inequality/verify.py new file mode 100644 index 0000000000..a681843a22 --- /dev/null +++ b/research/sl2z-shear-recurrence-inequality/verify.py @@ -0,0 +1,364 @@ +#!/usr/bin/env python3 +"""Faithful integer-shear words fail the strict supplier moment inequality. + +The three-bit quotient of PR #3947 implements rho(B^k) with at most one XOR. +Every word for the same integer matrix in the shear alphabet is at least +2k+1 letters, and that bill does not satisfy M(a) < 1. Standard library only. +""" + +from __future__ import annotations + +X = ((1, 1), (0, 1)) +XI = ((1, -1), (0, 1)) +Y = ((1, 0), (1, 1)) +YI = ((1, 0), (-1, 1)) +IDENT = ((1, 0), (0, 1)) +GENERATORS = (X, XI, Y, YI) +# Each right multiplication, as coefficient rows (a, b, c, d) of the four +# output entries in row-major order. The l1 norm of a row is the entry-growth +# factor proved below. +RIGHT_FORMS = { + "X": ((1, 0, 0, 0), (1, 1, 0, 0), (0, 0, 1, 0), (0, 0, 1, 1)), + "Xinv": ((1, 0, 0, 0), (-1, 1, 0, 0), (0, 0, 1, 0), (0, 0, -1, 1)), + "Y": ((1, 1, 0, 0), (0, 1, 0, 0), (0, 0, 1, 1), (0, 0, 0, 1)), + "Yinv": ((1, -1, 0, 0), (0, 1, 0, 0), (0, 0, 1, -1), (0, 0, 0, 1)), +} + + +def fail(message: str) -> None: + raise SystemExit("FAIL: " + message) + + +def matmul(left, right): + return tuple( + tuple(sum(left[i][t] * right[t][j] for t in range(2)) for j in range(2)) + for i in range(2) + ) + + +def entry_max(matrix) -> int: + return max(abs(matrix[i][j]) for i in range(2) for j in range(2)) + + +def b_matrix(): + return matmul(matmul(X, X), matmul(Y, Y)) + + +def diagonal_endpoint(first, second): + """Apply D(X), D(X), D(Y), D(Y) with the rightmost factor first. + + Each factor left-multiplies only the first role. The second role is the + arbitrary dirty spectator. + """ + for label in (Y, Y, X, X): + first = matmul(label, first) + return first, second + + +def cayley_hamilton_square(base): + # B^2 - (tr B) B + (det B) I, checked by multiplication for this B. + trace = base[0][0] + base[1][1] + det = base[0][0] * base[1][1] - base[0][1] * base[1][0] + square = matmul(base, base) + predicted = ( + (trace * base[0][0] - det, trace * base[0][1]), + (trace * base[1][0], trace * base[1][1] - det), + ) + return square, predicted, trace, det + + +def diagonal_entries(limit: int) -> list[int]: + """(B^k)_11 for k = 0..limit, from the integer recurrence.""" + if limit < 1: + fail("need at least B^1") + values = [1, 5] + previous, current = 1, 5 + for _ in range(2, limit + 1): + previous, current = current, 6 * current - previous + values.append(current) + return values + + +def inductive_ratio_step(current: int, previous: int) -> int: + """Return u_{k+1} - 5 u_k given u_k, u_{k-1}.""" + return (6 * current - previous) - 5 * current + + +def forms_obey(factor: int) -> bool: + return all( + sum(abs(coefficient) for coefficient in row) <= factor + for rows in RIGHT_FORMS.values() + for row in rows + ) + + +def apply_form(form, matrix): + entries = (matrix[0][0], matrix[0][1], matrix[1][0], matrix[1][1]) + values = [sum(coefficient * entries[index] for index, coefficient in enumerate(row)) for row in form] + return ((values[0], values[1]), (values[2], values[3])) + + +def shortest_word_length(target, max_length: int) -> int | None: + seen = {IDENT: 0} + frontier = [IDENT] + for length in range(max_length): + nxt = [] + for matrix in frontier: + for generator in GENERATORS: + product = matmul(matrix, generator) + if product in seen: + continue + seen[product] = length + 1 + nxt.append(product) + if product == target: + return length + 1 + frontier = nxt + return None + + +def words_obey_doubling(max_length: int) -> bool: + frontier = [IDENT] + for length in range(1, max_length + 1): + nxt = [] + allowance = 2**length + for matrix in frontier: + for generator in GENERATORS: + product = matmul(matrix, generator) + if entry_max(product) > allowance: + return False + nxt.append(product) + frontier = nxt + return True + + +def faithful_length_lower_bound(power: int) -> int: + """Minimum shear-letter count of B^power. Sharp at power 1; growth for power > 1.""" + if power < 1: + fail("power must be positive") + if power == 1: + return 4 + return 2 * power + 1 + + +def moment_clears_one(letter_count: int, width: int = 2, roles: int = 2) -> str: + """Compare M(a) = (L/W) * (1/m)^(1-a) with 1 on a in [0, 1]. + + For m > 1 the minimum is M(0) = L/(W m) and the maximum is M(1) = L/W. + Returns 'above', 'touches-zero', or 'below'. + """ + if letter_count < 0 or width < 2 or roles < 1: + fail("bad moment parameters") + floor = letter_count * 1 + unit = roles * width + top = letter_count * 1 + role_unit = roles + if floor > unit: + return "above" + if floor == unit and top > role_unit: + return "touches-zero" + if top < role_unit: + return "below" + if floor == unit and top == role_unit: + return "flat-one" + return "mixed" + + +def quotient_data(): + """Projective action of the integer generators modulo 3, on the sum-zero space.""" + lines = ((1, 0), (0, 1), (1, 1), (1, 2)) + + def normalize(vector): + x, y = vector[0] % 3, vector[1] % 3 + if (x, y) == (0, 0): + fail("projective image of zero") + pivot = x if x else y + inverse = 1 if pivot == 1 else 2 + return ((x * inverse) % 3, (y * inverse) % 3) + + def permutation(matrix): + images = [] + for line in lines: + image = normalize( + ( + matrix[0][0] * line[0] + matrix[0][1] * line[1], + matrix[1][0] * line[0] + matrix[1][1] * line[1], + ) + ) + images.append(lines.index(image)) + if len(set(images)) != 4: + fail("line map is not a permutation") + return tuple(images) + + def apply_permutation(perm, vector): + inverse = [0, 0, 0, 0] + for source, image in enumerate(perm): + inverse[image] = source + return tuple(vector[inverse[index]] for index in range(4)) + + basis = ((0, 1, 0, 1), (1, 1, 1, 1), (0, 1, 1, 0)) + + def coordinates(vector): + rows = [[basis[col][row] for col in range(3)] + [vector[row]] for row in range(4)] + pivot_row = 0 + where = [] + for col in range(3): + selected = next((row for row in range(pivot_row, 4) if rows[row][col]) , None) + if selected is None: + continue + rows[pivot_row], rows[selected] = rows[selected], rows[pivot_row] + for row in range(4): + if row != pivot_row and rows[row][col]: + for entry in range(4): + rows[row][entry] ^= rows[pivot_row][entry] + where.append((pivot_row, col)) + pivot_row += 1 + for row in range(pivot_row, 4): + if rows[row][3]: + fail("vector left the sum-zero subspace") + coeffs = [0, 0, 0] + for row, col in where: + coeffs[col] = rows[row][3] + return tuple(coeffs) + + def representation(perm): + columns = [coordinates(apply_permutation(perm, vector)) for vector in basis] + return tuple(tuple(columns[col][row] for col in range(3)) for row in range(3)) + + def mul2(left, right): + return tuple( + tuple(sum(left[i][t] * right[t][j] for t in range(3)) % 2 for j in range(3)) + for i in range(3) + ) + + image_x = representation(permutation(X)) + image_y = representation(permutation(Y)) + image_b = mul2(mul2(image_x, image_x), mul2(image_y, image_y)) + return image_x, image_y, image_b + + +def run_checks() -> dict: + base = b_matrix() + if base != ((5, 2), (2, 1)): + fail("B is not X^2 Y^2") + square, predicted, trace, det = cayley_hamilton_square(base) + if trace != 6 or det != 1 or square != predicted: + fail("Cayley-Hamilton step failed") + if matmul(matmul(X, X), X) == IDENT: + fail("X^3 collapsed in the integer matrices") + + probe = ((2, -3), (5, 7)) + for name, generator in zip(("X", "Xinv", "Y", "Yinv"), GENERATORS): + if apply_form(RIGHT_FORMS[name], probe) != matmul(probe, generator): + fail("linear form disagrees with " + name) + if not forms_obey(2): + fail("shear forms exceed doubling") + if forms_obey(1): + fail("control: l1 bound 1 should reject a genuine two-entry sum") + if not words_obey_doubling(6): + fail("explicit words exceeded 2^L") + + values = diagonal_entries(24) + matrix_power = IDENT + for power, entry in enumerate(values): + if power: + matrix_power = matmul(matrix_power, base) + if matrix_power[0][0] != entry: + fail("recurrence disagrees with matrix power at " + str(power)) + if power == 0: + continue + if entry < 5**power or not entry > 2 ** (2 * power): + fail("growth failed at " + str(power)) + previous = values[power - 1] + if entry < 5 * previous: + fail("ratio failed at " + str(power)) + if inductive_ratio_step(entry, previous) < 4 * previous: + fail("inductive surplus failed") + # (6x-y)-5x and x-y are linear and agree on a basis, hence for every integer pair. + for sample_x, sample_y in ((1, 0), (0, 1)): + if inductive_ratio_step(sample_x, sample_y) != sample_x - sample_y: + fail("recurrence gap is not the ratio gap") + + dirty_pairs = ( + (IDENT, IDENT), + (X, Y), + (YI, matmul(X, Y)), + (base, XI), + ) + for first, second in dirty_pairs: + got_first, got_second = diagonal_endpoint(first, second) + if got_second != second or got_first != matmul(base, first): + fail("diagonal four-call bill changed a spectator or missed B") + + length_b = shortest_word_length(base, 4) + if length_b != 4: + fail("B word length is not 4, found " + str(length_b)) + if shortest_word_length(base, 3) is not None: + fail("a length-3 word reached B") + + for power in range(1, 13): + lower = faithful_length_lower_bound(power) + if power == 1 and lower != 4: + fail("sharp length drifted") + if power > 1 and lower != 2 * power + 1: + fail("growth length drifted") + if lower <= 2 * power: + fail("length lower bound is not past 2k") + kind = moment_clears_one(lower) + if power == 1 and kind != "touches-zero": + fail("four-letter moment should touch 1 only at a=0") + if power > 1 and kind != "above": + fail("longer powers should lie strictly above 1") + # Any legal letter count at least this large stays out of M<1. + if moment_clears_one(lower + 5) == "below": + fail("adding letters created a passing moment") + + if moment_clears_one(1, width=3, roles=2) != "below": + fail("one rank-1 child on width 3 should pass the optimistic screen") + + image_x, image_y, image_b = quotient_data() + published_x = ((0, 0, 1), (0, 1, 0), (1, 0, 1)) + published_y = ((1, 0, 1), (1, 1, 0), (1, 0, 0)) + transvection = ((1, 0, 0), (0, 1, 1), (0, 0, 1)) + if image_x != published_x or image_y != published_y or image_b != transvection: + fail("quotient matrices disagree with the pinned three-bit action") + identity3 = ((1, 0, 0), (0, 1, 0), (0, 0, 1)) + t_square = tuple( + tuple(sum(image_b[i][t] * image_b[t][j] for t in range(3)) % 2 for j in range(3)) + for i in range(3) + ) + if t_square != identity3: + fail("rho(B) is not an involution") + changed = sum( + 1 + for i in range(3) + for j in range(3) + if transvection[i][j] != identity3[i][j] + ) + if changed != 1: + fail("rho(B) is not a single coordinate XOR") + + # No constant quotient bill dominates every faithful length. + for constant in range(0, 12): + if all(faithful_length_lower_bound(power) <= constant for power in range(1, 20)): + fail("a constant dominated the faithful lengths") + + return { + "length_B": length_b, + "u_8": values[8], + "moment_B": "touches-zero", + "moment_B2": "above", + "quotient_xor": 1, + "strict_supplier_inequality": False, + } + + +def main() -> None: + receipt = run_checks() + print( + "PASS_SL2Z_SHEAR_RECURRENCE_INEQUALITY " + + " ".join(key + "=" + str(value) for key, value in receipt.items()) + ) + + +if __name__ == "__main__": + main()