Prove faithful integer-shear words fail the supplier moment test.

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.

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"
+    }
+  ]
+}

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."
+    }
+  ]
+}

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."
+    }
+  ]
+}

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()