Exclude the third positive-frame profile for every power-of-two m (no κ)

research/bit-positive-frame-third-profile/PROOF.md

@@ -0,0 +1,112 @@
+# The profile (0,1,3,3,m) is impossible when m is a power of two
+
+Proof by Nick Petalas. Apache-2.0.
+
+## Model
+
+The model, target and notation are those of apoursh's PR6089
+(`research/bit-positive-frame-use`, pinned in [SOURCES.json](SOURCES.json)). It
+keeps Cinna Davis's PR2085/2112 endpoint. Here $A,B,P,Q$ are the four old 2×2
+addresses, with $A+B=P+Q=I_2$. The added frame is $R=F/m$ for an old address $F$
+and an integer $m\ge1$. Calls are $D_N(F)=I_w+([F]-1)N$ over the formal group
+algebra $\mathbb F_2[\Lambda]$ with $N^2=N$ and $\operatorname{rank}N=1$. Free
+$\operatorname{GL}_w(\mathbb F_2)$ mixing is allowed, the $w-4\ge0$ extra roles
+are dirty workspace restored exactly, and the target is
+
+$$T_w=\operatorname{diag}([A+P],[A+Q],[B+P],[B+Q],1,\ldots,1).$$
+
+PR6089 proves that every exact word using $R$ has one of the multiplicity profiles
+$(1,2,2,2,m)$, $(0,2,2,2,2m)$ or $(0,1,3,3,m)$, in order $(F,F^\perp,G,H,R)$. It
+constructs the first two and excludes the third for $m=1$. PR6089 Section 3 gives
+exact symmetries that reduce every $F$ to $F=A$. Under that reduction the third
+profile is: no $A$ call, one $B$ call, three $P$ calls, three $Q$ calls and $m$
+calls labelled $R=A/m$.
+
+## Theorem
+
+**If $m=2^k$ for an integer $k\ge0$, no exact word in this model has the profile
+$(0,1,3,3,m)$, at any finite width $w\ge4$.**
+
+The case $k=0$ is PR6089's $m=1$ exclusion; the argument below also covers it.
+For $F\ne A$ the statement follows by PR6089's symmetries, which preserve counts.
+
+## Proof
+
+**Normal form.** As in PR6089 Section 1, conjugate every free binary matrix through
+the later paid factors. A conjugated rank-one idempotent is still one, with the same
+label. The word becomes a product of paid factors followed by one free matrix $G$.
+Applying the augmentation $[F]\mapsto1$ turns every paid factor and the target into
+the identity, so $G=I_w$. Thus
+
+$$\prod_{i=1}^{L}D_{N_i}(F_i)=T_w$$
+
+exactly, in word order, where the $N_i$ are rank-one idempotents in
+$M_w(\mathbb F_2)$. Write $E_1,\ldots,E_m$ for the projectors of the $R$ calls in
+word order, $N_B$ for the $B$ call, and $N_{Q,1},N_{Q,2},N_{Q,3}$ for the $Q$ calls.
+Let $D_w=\operatorname{diag}(1,1,1,1,0,\ldots,0)$.
+
+**The lattice.** $\Lambda=\mathbb ZR+\mathbb ZB+\mathbb ZP$ is free on $R,B,P$,
+because $A=mR$ and $A,B,P$ are linearly independent. In this basis
+
+$$A=mR,\qquad Q=A+B-P=mR+B-P.$$
+
+Any additive map $\psi:\Lambda\to\mathbb Z$ therefore defines a ring homomorphism
+$\mathbb F_2[\Lambda]\to\mathbb F_2[s]/(s^K)$, $[\lambda]\mapsto(1+s)^{\psi(\lambda)}$,
+since $1+s$ is a unit. Applied entrywise, it sends $D_N(F)$ to
+$I+((1+s)^{\psi(F)}-1)N$.
+
+**Step 1: the $R$ character at order $m$.** Take $\psi_R(R)=1$ and
+$\psi_R(B)=\psi_R(P)=0$, so $\psi_R(A)=\psi_R(Q)=m$, and truncate at $K=m+1$. Because
+$m=2^k$, over $\mathbb F_2$
+
+$$(1+s)^m=1+s^m,\qquad (1+s)^{2m}=1+s^{2m}\equiv1\pmod{s^{m+1}}.$$
+
+The $B$ and $P$ calls map to $I$. An $R$ call maps to $I+sE_i$, and a $Q$ call maps
+to $I+s^mN_{Q,j}$. Expand the product over subsets of calls. The $s^m$ coefficient
+gets one term from each subset of total order $m$. These are the subset of all $m$
+$R$ calls, contributing $E_1E_2\cdots E_m$ in word order, and each single $Q$ call.
+Any subset containing a $Q$ call and another call has order at least $m+1$. The
+target exponents have $\psi_R$ values $m,2m,0,m$ on the active roles and $0$ on the
+workspace, so the image of $T_w$ is $I+s^m\operatorname{diag}(1,0,0,1,0,\ldots,0)$
+modulo $s^{m+1}$. Comparing $s^m$ coefficients:
+
+$$E_1E_2\cdots E_m+\sum_jN_{Q,j}=\operatorname{diag}(1,0,0,1,0,\ldots,0).\tag{1}$$
+
+**Step 2: the $B$ character at first order.** Take $\chi_B(B)=1$ and
+$\chi_B(R)=\chi_B(P)=0$, so $\chi_B(Q)=1$ and $\chi_B(A)=0$, and truncate at $K=2$.
+Only the $B$ and $Q$ calls are nontrivial, each mapping to $I+sN$. The target values
+are $0,1,1,2$, and $(1+s)^2\equiv1\pmod{s^2}$. Hence
+
+$$N_B+\sum_jN_{Q,j}=\operatorname{diag}(0,1,1,0,0,\ldots,0).\tag{2}$$
+
+This is the first-order character equation used in PR6089 Section 4.
+
+**Step 3: rank.** Adding (1) and (2) gives
+
+$$N_B+E_1E_2\cdots E_m=D_w.$$
+
+The left side is a sum of a rank-one matrix and a product of rank-one matrices, so
+its rank is at most $2$. The right side has rank $4$. This is a contradiction. ∎
+
+## Why the argument stops at powers of two
+
+For $m=2^k o$ with $o\ge3$ odd, the same two steps give
+
+$$N_B=D_w+e_{2^k}(E_1,\ldots,E_m),$$
+
+where $e_j$ is the sum of the ordered products of $j$ distinct $R$ projectors, taken
+in word order. Lower orders also force $e_j(E)=0$ for $1\le j<2^k$. Once $o\ge3$,
+$e_{2^k}(E)$ is no longer a single product and its rank can exceed $2$, so the rank step no longer closes.
+For example, when $m=3$ the condition reads $E_1+E_2+E_3+N_B=D_w$, which the four
+coordinate projectors satisfy. Neither realizability nor impossibility is proved for
+such $m$.
+
+## Scope
+
+This is a scoped written proof in PR6089's formal model. It is not a native
+supplier, a κ change or a multiplication theorem. It does not alter PR6089's sharp
+minimum $m+7$ or its length spectrum $\{m+7,2m+6\}$. It sharpens the count-profile
+classification. For $m$ a power of two, the attained profiles are exactly the two
+subdivision profiles. Clean ancillas, discarded roles, address-dependent free
+mixing, signed or multiple added frames, and changed endpoints are outside scope,
+as in PR6089.

research/bit-positive-frame-third-profile/README.md

@@ -0,0 +1,96 @@
+# Positive-frame third profile: impossible for every power-of-two m
+
+**Scoped written proof with exact finite corroboration. No κ change.**
+
+This answers part of Open next question 2 of apoursh's PR6089
+(`research/bit-positive-frame-use`). The question asks whether the third necessary
+multiplicity profile $(0,1,3,3,m)$ occurs for any $m\ge2$. The model is PR6089's
+formal PR2085/2112 four-target model: rank-one binary idempotent calls over
+$\mathbb F_2[\Lambda]$, free $\operatorname{GL}_w(\mathbb F_2)$ mixing, exactly
+restored dirty workspace and any finite width $w\ge4$. The profile is ordered as
+$(F,F^\perp,G,H,R)$, with added frame $R=F/m$.
+
+## Result
+
+**Theorem.** If $m=2^k$ for some $k\ge0$, no exact word has the profile
+$(0,1,3,3,m)$, at any finite width.
+
+For $m=1$ this is PR6089's exclusion. For $m=2,4,8,\ldots$ it is new. Combined with
+PR6089, the attained count profiles for these $m$ are exactly the two subdivision
+profiles $(1,2,2,2,m)$ and $(0,2,2,2,2m)$.
+
+**The idea.** Write $E_1,\ldots,E_m$ for the projectors of the $R$ calls, in word
+order. Send $[R]\mapsto1+s$ and $[B],[P]\mapsto1$. Then $[A],[Q]\mapsto(1+s)^m=1+s^m$
+over $\mathbb F_2$. The $s^m$ coefficient of the word is the single ordered product
+$E_1\cdots E_m$ plus the three $Q$ projectors. PR6089's first-order $B$ character
+gives a second equation. Together they give
+
+$$N_B+E_1E_2\cdots E_m=\operatorname{diag}(1,1,1,1,0,\ldots,0).$$
+
+The left side has rank at most 2, and the right side has rank 4.
+
+[PROOF.md](PROOF.md) has the complete argument and scope. It also shows why the
+argument stops when $m$ has an odd factor $o\ge3$: the $s^{2^k}$ coefficient becomes
+an elementary sum of $R$ projector products, and its rank is not bounded by one.
+
+## Evidence
+
+[verify.py](verify.py) uses exact F2 and group-algebra arithmetic and needs only the
+standard library. It checks:
+
+- the pinned PR6089 proof bytes;
+- the lattice identities, the determinant balance of the profile and both character
+  value tables for $m=2^k$, $k=0,\ldots,10$;
+- on 1,600 random profile words at $w=4,5$ and $m=1,2,4,8$, that the $[R]\mapsto1+s$
+  image has $e_j(E)$ at every order $j<m$ and $E_1\cdots E_m+\sum N_Q$ at order $m$,
+  and that the $B$ character has $N_B+\sum N_Q$ at first order;
+- 72 checks that specializing the exact $\mathbb F_2[\Lambda]$ product equals
+  specializing call by call;
+- that both of PR6089's attained subdivision words equal $T_w$ exactly at $w=4,5$ and
+  $m=1,2,4$ and satisfy the same coefficient equations. A mutated word is rejected;
+- exhaustively at $w=4,5$, that $D_w$ plus any matrix of rank at most one has rank at
+  least 3, which is the finite form of the rank step.
+
+The random words corroborate the coefficient lemma but do not prove it. The proof
+covers every $k$ and every $w$, and no bounded search is part of it.
+
+## Reproduce
+
+From the repository root:
+
+```sh
+~/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/bit-positive-frame-third-profile/verify.py
+~/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/bit-positive-frame-third-profile/verify.py
+python3.12 -B scripts/research_package.py --package research/bit-positive-frame-third-profile
+```
+
+Each verifier run prints `PASS_POSITIVE_FRAME_THIRD_PROFILE_POWERS_OF_TWO` in under
+a second.
+
+## Limitations
+
+Only powers of two are settled. For $m=3,5,6,7,\ldots$ the profile is neither
+constructed nor excluded. Nothing here changes PR6089's minimum $m+7$, its length
+spectrum, the selected frontier or κ. No native implementation, independent human
+review or formal-kernel check is supplied.
+
+## Open next questions
+
+1. **Is $(0,1,3,3,m)$ realizable when $m$ has an odd factor $o\ge3$?** Start at
+   $m=3$. The two characters reduce the problem to $E_1+E_2+E_3+N_B=D_w$, which
+   coordinate projectors satisfy, so a second-order character is needed. One example
+   is $[R]\mapsto1+s$ with $[P]\mapsto(1+s)^c$ modulo $s^3$, or a map that sends
+   $[R]$ to an $o$-th root of unity times $1+s$. Alternatively, search for an exact
+   10-call word at $w=4$ under the three first-order constraints.
+2. **Does a uniform obstruction exist?** A full exclusion would complete PR6089's
+   profile classification. The blocker is the rank of the elementary sum
+   $e_{2^k}(E)$ once $o\ge3$.
+
+## Credit
+
+This package was produced by Nick Petalas. apoursh's PR6089 supplies the model
+reduction, the symmetries, the necessary profile list, the $B$ character and the
+subdivision words, and poses the question. Cinna Davis's PR2085/2112 supply the
+model and endpoint. Nick Petalas's PR2910 supplies the determinant method, and
+PR6032 the support and first-order approach. The retained BIT predecessor lineage
+carries over. New work is Apache-2.0.

research/bit-positive-frame-third-profile/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "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/bit-positive-frame-use/PROOF.md",
+      "usage": "input",
+      "git_blob": "0580cc135fc7af60f177575c3c272f1661fdc1d4",
+      "sha256": "6ac09ee1756f51341c5fb2a480e5c8c3813ed0abc5a4969349ff0010ce872197"
+    }
+  ]
+}

research/bit-positive-frame-third-profile/TASK.json

@@ -0,0 +1,70 @@
+{
+  "schema_version": 1,
+  "task_id": "bit-new-register-model",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "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": "Is the third necessary positive-frame count profile (0,1,3,3,m) from PR6089 realizable for m>=2 in the formal PR2085/2112 four-target model? Settled negatively for every power of two m; other m remain open.",
+  "scope_change_reason": "Takes Open next question 2 of apoursh's PR6089 (research/bit-positive-frame-use), a formal alphabet/count-profile classification question in the same changed register model, rather than the card's native larger/nonabelian construction.",
+  "bottleneck_link": "Side result: sharpens the count-profile classification of usable positive added frames in the BIT four-target model. It does not change the minimum call count, a native supplier or kappa.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first verified exclusion (powers of two) and record odd-part m as open.",
+  "outcome": "partial",
+  "evidence": "PROOF.md (written proof for every m=2^k and every finite width); verify.py exact corroboration: lattice/character tables, 1,600 random-word coefficient-lemma checks, homomorphism checks, attained-profile controls and exhaustive w=4,5 rank step.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Is the profile (0,1,3,3,m) realizable when m has an odd factor o>=3, starting at m=3?",
+      "why_it_matters": "It would complete PR6089's count-profile classification for the remaining m.",
+      "first_step": "At m=3 the two characters only give E1+E2+E3+N_B=D_w; add a second-order character such as [R]->1+s, [P]->(1+s)^c mod s^3, or search exact 10-call words at w=4 under the three first-order constraints.",
+      "blocked_by": "The s^(2^k) coefficient is an elementary sum of ordered R-projector products whose rank is not bounded by one."
+    },
+    {
+      "question": "Is there a uniform obstruction for every m>=2?",
+      "why_it_matters": "A uniform exclusion would show that the attained profiles are exactly the two subdivision profiles for every m.",
+      "first_step": "Combine the order-2^k equation N_B = D_w + e_{2^k}(E) with higher-order R characters or a root-of-unity specialization of [R].",
+      "blocked_by": "No rank bound on e_{2^k}(E) is known when m is not a power of two."
+    }
+  ]
+}

research/bit-positive-frame-third-profile/VERIFY.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/bit-positive-frame-use/PROOF.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Pinned PR6089 proof bytes; lattice identities and character tables for m=2^k, k<=10; random-word coefficient lemma at w=4,5 and m=1,2,4,8; group-algebra homomorphism checks; exact attained subdivision words and a mutated rejection; exhaustive w=4,5 rank step."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Pinned PR6089 proof bytes; lattice identities and character tables for m=2^k, k<=10; random-word coefficient lemma at w=4,5 and m=1,2,4,8; group-algebra homomorphism checks; exact attained subdivision words and a mutated rejection; exhaustive w=4,5 rank step."
+    }
+  ]
+}