Exclude scratch-reading two-FULL completions (no new κ)

research/scratch-reading-full-obstruction/PROOF.md

@@ -0,0 +1,134 @@
+# Two FULL shears on arbitrary owners retain a low-grade image
+
+This is a scoped algebraic proof, produced by Nick Petalas. It answers the
+scratch-reading follow-up in unpaidmoon's [PR #5843](https://github.com/CrocSwap/integer-mult-bounds/pull/5843).
+The changed hypothesis is the location of each elementary shear. Either
+source or destination may now be any owner, including an identity scratch
+owner. No physical realization of that larger macro is assumed.
+
+## Statement
+
+Let A be a unital algebra over a field K and B a unital subalgebra with
+finite positive dimension d over K. Let F_r be increasing K-linear
+subspaces of A with B contained in F_0, B F_r B contained in F_r, and
+F_r F_s contained in F_(r+s). Fix nonnegative s,t and a K-linear
+B-bimodule projection pi on A which fixes every element of F_(s+t).
+
+There are n >= 2 owners. Allow arbitrary L,W,R in GL_n(B). Let
+
+    D1 = diag(a_0,...,a_(n-1)),  a_i in F_s and a_i a unit of A,
+    D2 = diag(b_0,...,b_(n-1)),  b_i in F_t and b_i a unit of A.
+
+Choose any distinct p_1,q_1 and any distinct p_2,q_2 from the n owners.
+The two elementary shears and FULL factors are
+
+    E1 = I + e_(p_1) c_1 e_(q_1)^T,   T1 = D1 E1,
+    E2 = I + e_(p_2) c_2 e_(q_2)^T,   T2 = D2 E2,
+
+where c_1,c_2 are arbitrary elements of A. They need not be central, pure
+words, or invertible. Neither coefficient has a grade bound. Matrix
+products act on columns from right to left.
+
+Apply pi entrywise, and regard pi(L T2 W T1 R) as a K-linear map from
+B^n to A^n by left multiplication. Then
+
+    rank_K pi(L T2 W T1 R) >= (n-1)d.                 (1)
+
+In particular, if pi(g_0)=pi(g_1)=0, this word cannot equal
+
+    J = diag(g_0,g_1,I,...,I),
+
+because rank_K pi(J)=(n-2)d. The statement requires arbitrary initial
+scratch inputs and their identity endpoint. It grants reads and writes
+of those inputs inside either shear.
+
+## Proof
+
+Set S = {x in B^n : x_(q_1)=0}. It has dimension (n-1)d. On this exact
+subspace E1 x=x, regardless of whether q_1 is main or scratch. Therefore
+u=W D1 x has every coordinate in F_s. Also x -> u is injective, since
+D1 is invertible over A and W is invertible over B and hence over A.
+
+Suppose pi(D2 E2 u)=0. Row q_2 is untouched by E2 since p_2 != q_2.
+Its output is b_(q_2) u_(q_2), which lies in F_(s+t). The projection fixes
+this element, so its vanishing forces u_(q_2)=0 because b_(q_2) is a unit.
+This kills the entire c_2 u_(q_2) term. Every remaining output is now
+b_i u_i, again in F_(s+t). Projected vanishing forces all u_i=0. Thus
+pi(T2 W T1) is injective on S and has rank at least (n-1)d.
+
+Finally the bimodule property gives
+
+    pi(L T2 W T1 R) = L pi(T2 W T1) R.
+
+Right multiplication by R is an automorphism of the domain B^n. Left
+multiplication by L is an automorphism of the codomain A^n. Both preserve
+the K-rank. This proves (1). Since pi fixes B, the displayed target has
+exactly the scratch image B^(n-2), proving its exclusion.
+
+No commutation, positivity, domain property, or inverse grade bound is
+used. In particular B may have zero divisors. The free subspace is chosen
+using the actual first read coordinate, which removes any need for the
+main-only endpoint restriction on the two shears.
+
+## Sharpness and hypothesis controls
+
+When a unit g satisfies pi(g)=pi(g^-1)=0, take D1=D2=I and W=I. On any
+two owners choose E1=I+e_1 g e_0^T and E2=I-e_0 g^-1 e_1^T. The exact
+two-owner product is
+
+    E2 E1 = [[0,-g^-1],[g,1]].
+
+Its projection has rank d on those owners and identity on the others.
+Thus the uniform lower bound (n-1)d is attained. The labels 0,1 in this
+example can be replaced by any distinct owner indices, including scratch.
+This equality example is elementary algebra and is not a native construction.
+
+The unit condition, the cutoff s+t, and W in GL_n(B) are essential to this
+argument. Setting D1=0 destroys the bound. Two grade-one factors on
+different coordinates can have grade two, so cutoff one cannot retain
+them. A high-grade diagonal W outside Mat_n(B) can make the entire
+projected map vanish. Three queries can attain diag(g,g^-1), after a
+scalar signed swap, through the usual three-shear identity. These are
+explicit controls of the theorem's hypotheses, not new optimization claims.
+
+## Application to the cited FULL boundary
+
+Chris R / Clear1nsight's [PR #4920](https://github.com/CrocSwap/integer-mult-bounds/pull/4920)
+supplies the full-monomial Clifford grade model and its tensor-separation
+lemma. unpaidmoon's #5843 supplies the main-only two-shear rank argument
+with identity scratch and explicitly asks about a scratch-reading shear.
+The contribution here removes that restriction by choosing S using q_1.
+No predecessor numerical result is replayed or recertified.
+
+For that model, take B to be the full monomial subgroup algebra and F_r
+the span of words of Fourier grade at most r. These spaces have the
+required bimodule and product properties. Use s=t=8 and pi=pi_(<=16).
+The actual diagonal transverse factors have grade eight on main owners
+and identity on scratch, so they satisfy the hypotheses even when the
+new shear touches scratch. Two pure grade-17 main targets with restored
+identity scratch remain impossible in this enlarged algebraic class.
+
+The cited separation lemma transfers the obstruction to every sufficiently
+large tensor width in the fixed finite columnwise alphabet. This use is
+conditional on the predecessor's stated grade and separation premises.
+It supplies no new width bound, literal native implementation, or claim
+about accidental relations at small widths.
+
+thu-nmrc's [PR #5200](https://github.com/CrocSwap/integer-mult-bounds/pull/5200)
+is a different extension. It covers joint native main banks and identity
+scratch, with possibly dense query blocks confined to the main owners.
+The present result permits scratch in either single-coordinate query;
+it does not extend #5200's multiple-query block theorem to scratch blocks.
+Credit its joint-bank result and the retained Cinna Davis, Cao Yifan,
+zxv, Jacob Alan Sussman, Ali Romman, Dugongue and native/compiler lineage.
+
+## Evidence limits
+
+The executable is a fresh finite group-algebra example, not a Clifford
+operator replay. Its complete declared owner-pair enumeration corroborates
+the new coordinate freedom. The written argument proves the arbitrary
+field and owner-count statement. Neither is proof-kernel verification.
+Productive transformed helpers, clean COPY/CLEAR, noninvertible controls,
+new query blocks, changed transverse grades and noncolumnwise operations
+require their own analysis. No invoice, supplier admission, new kappa, or
+complete multiplication theorem is claimed.

research/scratch-reading-full-obstruction/README.md

@@ -0,0 +1,100 @@
+# Scratch access does not rescue two elementary FULL shears
+
+This scoped algebraic proof is produced by Nick Petalas. It answers the
+scratch-reading follow-up in unpaidmoon's
+[PR #5843](https://github.com/CrocSwap/integer-mult-bounds/pull/5843).
+Either shear may read or write any owner, including dirty scratch. Under
+the stated low-grade transverse and free-control hypotheses, its projected
+image still has rank at least `(n-1) dim B`. Two pure high-grade targets
+with restored identity scratch have rank only `(n-2) dim B`, so remain
+impossible. No new kappa is claimed.
+
+[PROOF.md](PROOF.md) states and proves the more general filtered-algebra
+theorem. The new step chooses the first read-coordinate kernel regardless
+of which owner the shear reads. It requires no commutation or domain
+property. Its lower bound is sharp in the declared algebraic class.
+
+## Reproduce
+
+From the repository root, use CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -B -W error research/scratch-reading-full-obstruction/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -B -W error research/scratch-reading-full-obstruction/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/scratch-reading-full-obstruction
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/scratch-reading-full-obstruction --check-source-history
+```
+
+The standalone command prints `PASS_SCRATCH_READING_FULL_OBSTRUCTION` in
+its JSON result. Both registered checks run the same finite domain under
+normal and optimized execution. They write nothing into the checkout.
+
+## Finite evidence
+
+The checker constructs `F2[S3^3]`, dimension 216, with the dimension-eight
+subgroup algebra of `{identity,(01)}^3`. Grade counts coordinates outside
+that subgroup. The projection retains grades at most two. Diagonal units
+have grade at most one. The two target units have grade three.
+
+Every ordered pair of distinct first-shear owners and every ordered pair
+of distinct second-shear owners is checked for each of four explicit
+coefficient/diagonal/free-control fixtures, at n=2,3,4. This gives 736
+cases, including 512 with a scratch read, 512 with a scratch write and
+176 with a scratch-to-scratch shear. The categories overlap. In 368 cases
+the diagonal transverse factors remain identity on scratch, as in the
+predecessor's setup; the rest exercise the theorem's wider diagonal class.
+These are fixed fixtures, not every group-algebra coefficient or control.
+
+Direct binary elimination finds full projected rank in all 736 cases:
+16 cases at rank 16, 144 at rank 24 and 576 at rank 32. It separately
+checks rank `(n-1)*8` on the actual first-read kernel, the projected target,
+and whole maps with outer subgroup-algebra controls. Bitset coefficients
+lift to integral group-algebra coefficients. Full rank modulo two also
+certifies full rational rank for those lifted whole-word fixtures.
+
+Separate equality examples attain the sharp `(n-1)*8` lower bound. The
+controls exercise a too-low cutoff, a nonfree middle matrix, a nonunit
+diagonal and an additional third query, plus noncommutativity, a nonzero
+nilpotent free coefficient and a rejected same-owner shear.
+The runtime JSON is generated from the arithmetic and records its scope.
+
+## Sources and limits
+
+The exact question source is #5843, pinned in [TASK.json](TASK.json).
+[SOURCES.json](SOURCES.json) pins the main-branch grade proof from Chris R /
+Clear1nsight #4920 and the distinct joint-bank theorem of thu-nmrc #5200
+as provenance. They are cited premises, not audited deliverables or runtime
+imports. Credit unpaidmoon for the question and clean-output argument,
+Chris R / Clear1nsight for the full-monomial grade framework, thu-nmrc for
+joint-main-bank stability, and their retained predecessor lineage.
+
+The finite checker uses a small untwisted group algebra. It does not
+reconstruct the physical Clifford macro. The written proof covers twisted
+algebras when the stated filtration and bimodule hypotheses hold. The
+source application's all-large-width implication uses #4920's separation
+lemma. No new sufficient width, native/compiler/precision/tape/outer replay,
+formal proof-kernel review, or independent human acceptance is claimed.
+The selected frontier is unchanged. New material is Apache-2.0.
+
+The chosen card's baseline command passed source-binding orientation.
+The actual scope changes from helper construction to the explicit
+scratch-access obstruction, as recorded in TASK.json. This rules out one
+escape before anyone pays for a larger native or invoice search.
+
+## Open next questions
+
+Can a changed FULL macro with two independent query source coordinates
+evade this obstruction at a favorable complete tariff? First specify a
+legal macro and its complete target, transverse, restoration and paid-call
+contract, then compute its projected image. The proof uses one read
+coordinate per shear. No physical macro or complete invoice for that
+changed premise is supplied here. TASK.json records the same question.
+
+## Engineering notes
+
+The verifier has no recursion, dynamic code generation or external
+dependencies. Its fixed algebra has 216 basis elements, at most four owners
+and at most 32 domain columns. All loops are bounded by these declarations
+or finite case products. Python requires dynamic integer and collection
+allocation; those dimensions bound live data. Each function is below 60
+lines. Acceptance uses explicit exceptions and remains active under `-O`.

research/scratch-reading-full-obstruction/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/two-full-central-obstruction/grade/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "4cdf1e1a29b2113e88513f7a7d983f1e52adb6db",
+      "sha256": "8fd775a9903eca0f53b186d7fb684d9f5f74afc9c105082b3d4981bd950fca33"
+    },
+    {
+      "path": "research/two-full-dirty-stability/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "fc8bbd4cfc9bf5b349aecaa8b87740d1a23144d5",
+      "sha256": "5c9331d51246ec9f3c6aabcb11b25eb6e438a3db4aee15cb61a9d24f55bfdf2f"
+    }
+  ]
+}

research/scratch-reading-full-obstruction/TASK.json

@@ -0,0 +1,81 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-new-helper-inventory",
+  "priority_revision": 8,
+  "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a",
+  "original_card": {
+    "id": "complex-new-helper-inventory",
+    "question": "Can a changed helper inventory earn productive credit that survives completion, compilation and the actual caller?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Specify all arbitrary inputs, owned fields, restored outputs and a physically legal consumer. Compare complete P and T, including target debits and precision/stock costs. #5599 is a positive control for target refinement, not permission to split every helper for free. #5614 is a hypothetical compiler budget, not an emitted 145-split word. Stop at the first unpaid boundary or a failing optimistic full bill.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "productive helper",
+      "target refinement",
+      "5599",
+      "5614"
+    ],
+    "existing_checks": [
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "A low-grade projected-rank obstruction for two elementary FULL shears on arbitrary owner pairs, including scratch reads and writes.",
+  "scope_change_reason": "The donation assignment requests an original result rather than auditing predecessors. This answers the scratch-reading question in PR5843, changing its main-only shear hypothesis while retaining identity scratch at the endpoint.",
+  "bottleneck_link": "Scratch access cannot rescue two FULLs with low-grade diagonal transverse factors and monomial-algebra controls. A proposed escape must change another named hypothesis before native or invoice development.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first proved scratch-reading extension after exact finite corroboration; do not optimize or expand the construction.",
+  "outcome": "completed",
+  "evidence": "PROOF.md gives the arbitrary-field filtered-algebra theorem. verify.py enumerates the declared finite group-algebra fixtures and checks projected ranks directly.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can a changed FULL macro with two independent query source coordinates evade this obstruction at a favorable complete tariff?",
+      "why_it_matters": "The proof uses one source coordinate per shear. A higher-dimensional query block changes that hypothesis.",
+      "first_step": "Specify one legal macro and its complete target, transverse, restoration and paid-call contract before testing its projected image.",
+      "blocked_by": "No source-bound physical macro or complete invoice is supplied here."
+    }
+  ],
+  "claim_type": "scoped proof",
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19215589",
+  "question_source": {
+    "pr": 5843,
+    "head": "050b99f3f355a83f90189218c4c95c8131f8a991",
+    "question": "One FULL shear that reads a scratch owner, with its projected image."
+  }
+}

research/scratch-reading-full-obstruction/VERIFY.json

@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "-W",
+        "error",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Direct finite group-algebra projected ranks for every declared owner pair, sharpness and hypothesis rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-B",
+        "-W",
+        "error",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "The same finite arithmetic and controls with assertions disabled."
+    }
+  ]
+}