Derive two-write spectator constraints with exact middle-label projection

research/two-write-spectator-projection/README.md

@@ -0,0 +1,154 @@
+# Exactly two writes: a support-sensitive projector constraint
+
+**Scoped written lemma and exact finite corroboration; no new kappa.** This
+continues Nick Petalas's PR6012 at `3d9d5eb2ae784356497771661960ad0455b137db`,
+`research/two-three-cycles-every-dimension/PROOF.md`, Sections 2–4 and Open next
+question 3. It derives the two-write analogue with all middle-label terms
+retained. It does not exclude the residual ten-call case.
+
+## Model and projection
+
+Use PR6012's formal model `M_2(F2[GL_n(F2)])`, with ordinary matrix product for
+address labels and row `k` represented by `e_k^T`. A call is
+`D(g,N)=(I+N)+[g]N`, where `g=E_ij=I+e_i e_j^T` writes `i`, reads `j`, and
+`N` is a rank-one binary idempotent. Every endpoint coefficient is formal.
+Free scalar maps are normalized into the call projectors as in the source;
+move scalar maps to one end by conjugating the projectors. Augmentation of
+the endpoint `[c]I` forces that terminal scalar map to be `I`. Thus every
+normalized subword has augmentation `I`.
+
+Suppose exactly two calls write coordinate `k`. Write the complete word as
+
+`P=A D(g,N) B D(h,M) C`, with `g=E_kj`, `h=E_kl`, `j,l != k`.
+
+The factors in `A,B,C` do not write `k`; all their address support belongs to
+`S_k={b:e_k^T b=e_k^T}`. Write `B=sum_b [b] B_b`, and let `pi_k` retain only
+labels in `S_k`. Define the **selected and relabelled** middle polynomial
+
+`T_(j,l)(B)=sum_(b in S_k : e_j^T b=e_l^T) [g b h] B_b`.
+
+Then the exact identity is
+
+`pi_k(P)=A ((I+N) B (I+M) + N T_(j,l)(B) M) C`.             (1)
+
+Proof: expand the two calls into their four terms. The term using neither
+address label lies in `S_k`. The two terms using exactly one lie outside it:
+`S_k g S_k` and `S_k h S_k` are disjoint from the subgroup. In the double
+term, put `r=e_j^T b`. Since `b` fixes row `k`,
+
+`e_k^T g b h = e_k^T + r + (1+r_k)e_l^T`.
+
+This equals `e_k^T` precisely when `r=e_l^T`: if `r_k=1`, equality would force
+`r=0`, impossible for an invertible `b`; if `r_k=0`, it forces `r=e_l^T`.
+Multiplication on either side by support in `S_k` preserves membership in
+`S_k`, proving (1). In general `g b h` is not `b`, so merely filtering `B`
+without relabelling is incorrect. All scalar matrix orders in (1) matter.
+
+## Equal and complementary projector pairs
+
+Let the endpoint be `[c]I`, as for the two equal coordinate 3-cycles. Put
+`S=sum_(e_j^T b=e_l^T) B_b`, the augmentation of the selected middle terms.
+The augmentation of `A,B,C` is `I`.
+
+If `c` fixes row `k`, applying augmentation to (1) gives
+
+`I=(I+N)(I+M)+N S M`.                                    (2)
+
+Multiply (2) on the left by `I+N` to get `(I+N)M=0`, and on the right by
+`I+M` to get `N(I+M)=0`. Thus `M=NM=N`. Equation (2) then reduces to
+`N S N=N`. This is a necessary projector condition for **any restored
+coordinate written exactly twice**, without restricting the intermediate reads.
+The equality conclusion uses idempotence; it holds beyond rank one as well,
+but only the stated rank-one source model is used here.
+
+If `c` moves row `k`, then `pi_k([c]I)=0`, so instead
+
+`0=(I+N)(I+M)+N S M`.                                    (3)
+
+Left multiplication by `I+N` gives `(I+N)(I+M)=0`. This alone does not
+force complementary projectors. Each paid call is an involution, so the inverse is a legal reversed word.
+Apply the same argument to that inverse:
+its two writer projectors occur in order `M,N`; every other label still fixes
+row `k`. Since a subgroup is closed under inversion, `c^{-1}` also moves row
+`k`. Thus `(I+M)(I+N)=0` as well. In dimension two, the first equality gives
+`im(N)=ker(M)` and the second gives `im(M)=ker(N)`. Consequently `MN=NM=0`,
+and the first equality now yields **`M=I+N`**. The two projections of the word
+and its inverse are both essential. The remaining necessary coefficient
+condition from (3) is `N S (I+N)=0`.
+
+## Residual ten-call consequence and limits
+
+PR6012's cited reduction leaves `n=5`, two scalar roles and the ten-call
+write profile `(target,spectator)=(6,4)`. Both spectators are therefore written
+exactly twice. Their two writer projectors must be equal by (2). Applying the
+transpose/reversed-word version gives the same necessary equality for the
+two reads of each spectator. Total length ten and PR6012's two-read minimum
+for each of the five coordinates force exactly two reads per coordinate.
+Each of the three target coordinates is also written and read exactly twice;
+its writer pair and reader pair must each be complementary. These equalities
+are necessary, not sufficient for a full formal endpoint;
+no length-ten or length-eleven exclusion is asserted.
+
+## A live two-write spectator and a necessary relabelling term
+
+Take distinct address coordinates `i,j,k`, put `g=E_kj`, `h=E_ik`,
+`t=E_ij`, and fix any one rank-one projector `N`. In the address group,
+`g h g h t=e`. Products with the same projector satisfy
+`D(a,N)D(b,N)=(I+N)+[ab]N`. Consequently
+
+`D(g,N) D(h,N) D(g,N) D(h,N) D(t,N)=I`.
+
+Coordinate `k` is written twice and read twice, and all inputs are restored.
+This refutes an unrestricted claim that every live restored spectator must
+be written at least three times. It is not a ten-call two-cycle counterexample.
+For the middle `B=D(h,N)`, both support labels pass the selection with `j=l`,
+but `g h g != h`. Omitting the relabelling in (1) changes the result. The
+identity can be inserted before the known twelve-call endpoint, giving a
+seventeen-call positive endpoint with a live two-write spectator.
+
+## Evidence and reproduction
+
+```sh
+python3.12 -I -W error -B research/two-write-spectator-projection/verify.py
+python3.12 -I -W error -B research/two-write-spectator-projection/independent.py
+python3.12 -B scripts/research_package.py --package research/two-write-spectator-projection
+```
+
+The standard-library checker compares all 3,600 two-write contexts with a
+middle of zero or one calls in the declared three-coordinate domain, checks
+all 576 augmented `(N,M,S)` cases and all six commutator fixtures. It finds
+6 restored pairs, 12 forward-zero pairs, but only 6 pairs passing both forward
+and inverse conditions: exactly the complements. Controls reject missing
+middle support selection, missing relabelling and each deleted commutator
+call; the extra forward-only pairs refute the insufficient one-sided argument.
+`independent.py` uses complete permutations of all address vectors as group
+**labels**, retaining a separate scalar coefficient for every permutation.
+It does not accept equality merely in the permutation-module representation.
+Its separate dense scalar arithmetic checks all 288 GL(3,2) return-filter
+cases, 72 five-coordinate contexts with outer subwords and longer middles,
+the twelve-call positive endpoint, and all six seventeen-call insertions.
+Both engines were prepared in this session; this is implementation diversity,
+not independent human review. A separate read-only agent review independently
+checked the proof, augmented matrices and group fixtures; no proof-kernel
+acceptance is claimed. Finite checks corroborate the written proof. No unrestricted length-ten or
+length-eleven search is part of this task.
+
+## Open next questions
+
+Can the full off-subgroup equations combine the equal spectator pairs and
+complementary target pairs to exclude the residual `(6,4)` case? First analyze
+these constraints on the read/write incidence cycles, then bind a proposed
+strengthening to the complete endpoint.
+The missing implication is formal cancellation, not a larger sampled word set.
+
+## Credit and scope
+
+Canonical base `721c03822c421b7f7fcbb2598993b947c4d88419`, priority 8, selected
+PR6030 kappa `0.003125804`, unchanged. [Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/6075).
+Credit Nick Petalas/PR6012 for the single-write projection and reduction,
+Mihir Srivastava/PR4939 for the formal model, James Reed/jwr404 #5005/#5379 for
+the cited exact small-dimension costs, and JoyboyBrian/#4974 for the prior
+single-cycle reduction. The commutator identity is standard, not a new group
+identity. This application and checks were prepared by JoyboyBrian with
+substantial OpenAI Codex assistance. Apache-2.0. No native tariff, physical
+supplier, complete multiplication theorem or new kappa is claimed.

research/two-write-spectator-projection/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/three-cycle-address-floor/README.md",
+      "usage": "input",
+      "git_blob": "6a65c91f29e5b226cebd32d0c1d6963a60a98761",
+      "sha256": "a63c4ea4c874cac1fb064e1aff07f8ef791391eb795aec22a2154eb44a8fa81e"
+    },
+    {
+      "path": "research/two-three-cycles-every-dimension/PROOF.md",
+      "usage": "input",
+      "git_blob": "ca692812836f82484d228d8b4eb0f250c007d7a8",
+      "sha256": "b7af7801ddd5ff1e8d07d50dcd6f537f052d515839b828f0c4fd040351b8bce3"
+    }
+  ]
+}

research/two-write-spectator-projection/TASK.json

@@ -0,0 +1,64 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-new-register-model",
+  "priority_revision": 8,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "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": "changed",
+  "actual_scope": "Derive the exact two-write row-stabilizer projection for PR6012; prove equal restored-row projector pairs and complementary moved-row pairs, retaining inverse-word and middle-label conditions.",
+  "scope_change_reason": "Take PR6012 Open next question 3 and the public Discussion 6075 claim: a support-sensitive two-write lemma rather than a new physical register construction.",
+  "bottleneck_link": "Provides necessary writer/read constraints on the residual ten-call (6,4) case; does not decide it or give a supplier.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop with the scoped lemma, exact finite controls and explicit live-two-write counterexample. No unrestricted length10/11 census.",
+  "outcome": "partial",
+  "evidence": "python3.12 -B scripts/research_package.py --package research/two-write-spectator-projection",
+  "author": "JoyboyBrian",
+  "ai_assistance": "Substantial OpenAI Codex assistance in proof, checker and documentation; separate agent read-only review, no independent human or proof-kernel acceptance.",
+  "open_questions": [
+    {
+      "question": "Do equal spectator pairs, complementary target pairs and the full off-subgroup equations exclude the residual ten-call (6,4) case?",
+      "why_it_matters": "This is the remaining five-coordinate case identified by PR6012, distinct from already excluded lengths below 10.",
+      "first_step": "Analyze the read/write incidence cycles with these projector constraints and retain exact middle support and labels.",
+      "blocked_by": "Projector constraints are only necessary; full noncommutative formal coefficient cancellation remains unresolved."
+    }
+  ]
+}

research/two-write-spectator-projection/VERIFY.json

@@ -0,0 +1,62 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/three-cycle-address-floor/README.md",
+    "research/two-three-cycles-every-dimension/PROOF.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Exact 3600 two-write contexts, 576 augmented matrices, 6 commutator identities and rejecting controls"
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "All projection, classification and control checks remain active under optimization"
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/independent.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Independent complete-permutation group labels: 288 return filters, 72 outer contexts, six 17-call positive endpoints"
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/independent.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Independent formal-coefficient and positive endpoint checks under optimization"
+    }
+  ]
+}