Prove eight-call minimum for one arbitrary scaled rank-one frame

research/bit-single-scaled-frame-floor/README.md

@@ -0,0 +1,257 @@
+# One arbitrary scaled rank-one frame still needs eight calls
+
+**Scoped proof.** For the four-target endpoint of PR2085, adding any one
+symmetric rational rank-one address matrix does not reduce the minimum below
+**eight paid calls**. This includes arbitrary signed rational scaling and any
+finite number of additional dirty roles, provided those roles are exactly
+restored. Free mixing is address-independent and binary. This settles the
+one-added-frame part of PR6032's scaled-frame question; two added frames remain
+outside the theorem.
+
+The proof combines the determinant method already used in PR2910 with
+exponent support and first-order rank constraints. The new part is the
+all-scalings reduction: every hypothetical word of at most seven calls reduces
+to four doubled-axis count profiles, and each has rank capacity two where the
+target needs four. There is no native supplier, paid-profile improvement, or
+new multiplication bound here. The selected result is unchanged.
+
+## Exact model and theorem
+
+Write rational symmetric 2-by-2 matrices as addresses, with
+
+```
+A = [[1,0],[0,0]]          B = [[0,0],[0,1]]
+P = (1/2)[[1,1],[1,1]]    Q = (1/2)[[1,-1],[-1,1]].
+```
+
+Thus `Q=A+B-P`; each old address has trace one. Fix one nonzero symmetric
+rational rank-one matrix `R`. Equivalently, `R=c vv^T` for nonzero rational
+`c` and rational vector `v`; neither sign nor normalization is restricted.
+Let `Lambda` be the additive subgroup of `Sym_2(Q)` generated by these five
+addresses. In the commutative group algebra `F_2[Lambda]`, `[F][G]=[F+G]` and
+`[0]=1`; distinct addresses remain distinct formal monomials.
+
+For any finite `w>=4`, a paid call is
+
+```
+D_N(F) = I_w + ([F]-1)N,
+F in {A,B,P,Q,R},   N in M_w(F_2),   rank N=1,   N^2=N.
+```
+
+Arbitrary interspersed matrices in `GL_w(F_2)` are free. They cannot depend on
+addresses. Every role starts arbitrary (no clean auxiliary assumption). The
+required endpoint on all roles is
+
+```
+T_w = diag([A+P], [A+Q], [B+P], [B+Q], 1, ..., 1).
+```
+
+**Theorem.** Every exact finite word for `T_w` uses at least eight paid calls,
+and eight suffice, for every such `R` and `w`. Allowing `R=0` as a redundant
+identity call also leaves the minimum eight. Inverse old addresses are not
+extra free or paid labels; a negative `R` is permitted only as that one label.
+The theorem does not assert that every exact word has length eight.
+
+## Proof
+
+### 1. Normalize mixing and take the determinant
+
+Each paid factor augments to `I_w` under `[F] -> 1`. The target does too, so the
+product of all free binary matrices is `I_w`. Move the free matrices to one end
+by conjugating paid projectors. Conjugation preserves rank, idempotence and
+address labels; the residual free product is identity. It is therefore enough
+to study a product of the specified paid factors.
+
+A rank-one idempotent is conjugate over `F_2` to `diag(1,0,...,0)`, so
+`det D_N(F)=[F]`. Binary invertible matrices have determinant one. If the
+multiplicities are `(a,b,p,q,r)`, an exact word consequently satisfies
+
+```
+a A + b B + p P + q Q + r R = 4 I_2.                 (1)
+```
+
+This is equality of rational matrices, since the formal monomials are
+independent. If `r=0`, taking traces gives exactly eight calls. Zero-address
+calls can simply be deleted, giving the same lower bound when `R=0`.
+
+Suppose for contradiction that `k=a+b+p+q+r<=7` and `r>=1`. Put
+`n=a+b+p+q`, `d=a-b`, `e=p-q`. Equation (1) gives
+
+```
+2 r R = [[8-n-d, -e], [-e, 8-n+d]],
+d^2 + e^2 = (8-n)^2.                                (2)
+```
+
+Nonnegative counts give `|d|+|e|<=n`. Hence `8-n<=n`, so `4<=n<=6`.
+For radii `8-n=4,3,2`, the integer circle in (2) has only axial points.
+Substitution back into (2) gives
+
+```
+r R = (8-n) F,  F in {A,B,P,Q},  1<=r<=7-n.
+```
+
+In particular every candidate is `R=sF` with `s>1`. The possible scales are
+`4,3,2,3/2,4/3`. This conclusion was derived without assuming that `R` is
+positive or aligned. It eliminates every negative or off-axis `R` from a
+word of at most seven calls. The exact finite enumeration finds 40 count
+profiles, with 20 distinct matrices `R`.
+
+### 2. Exponent support leaves four profiles
+
+Expanding the normalized word, every monomial exponent is a subset sum of
+its paid addresses; cancellations may remove exponents but cannot create a
+new one. Thus each of the four required diagonal exponents must have a
+nonnegative integral representation using the available label counts.
+
+Every target exponent has trace two and rank two. No such representation
+can contain `R=sF` with `s>1`: if an old label is also used, the trace exceeds
+two; if only copies of `R` are used, the sum has rank at most one. Without
+`R`, trace two forces exactly two old labels. Comparing the ten unordered
+old pairs shows that each target has its unique named pair. Consequently
+`a,b,p,q>=1`.
+
+It follows that `|d|+|e|<=n-4`. Combined with (2), this gives `8-n<=n-4`,
+so `n=6`. Now `r=1`, and the only remaining profiles are
+
+| R | a | b | p | q | r |
+|---|---:|---:|---:|---:|---:|
+| 2A | 1 | 3 | 1 | 1 | 1 |
+| 2B | 3 | 1 | 1 | 1 | 1 |
+| 2P | 1 | 1 | 1 | 3 | 1 |
+| 2Q | 1 | 1 | 3 | 1 | 1 |
+
+### 3. First-order rank excludes those profiles at every width
+
+For these four cases `R=2F`, the address lattice is exactly
+`Lambda_0=ZA+ZB+ZP`, a free rank-three group, and `R` is zero modulo
+`2 Lambda_0`. Map its group algebra to the square-zero algebra with variables
+`x_A,x_B,x_P`, where all products of variables vanish, by sending a monomial
+with coordinates `(u,v,z)` to `1+(u mod2)x_A+(v mod2)x_B+(z mod2)x_P`.
+This is a ring homomorphism. In particular `Q` contributes to all three
+variables, while `R` contributes zero.
+
+Let `S_F` be the sum over `F`-labelled call projectors. The first-order
+coefficient equations of the exact word are
+
+```
+S_A + S_Q = diag(1,0,0,1,0,...,0),
+S_B + S_Q = diag(0,1,1,0,0,...,0),
+S_P + S_Q = D,       D=diag(1,1,1,1,0,...,0).
+```
+
+Adding the first two also gives `S_A+S_B=D`. If `R=2A` or `2B`, the counts
+of `P` and `Q` are one each, so `rank(S_P+S_Q)<=2`. If `R=2P` or `2Q`, the
+counts of `A` and `B` are one each, so `rank(S_A+S_B)<=2`. Both contradict
+`rank D=4`. This argument holds for every finite `w`; it does not enumerate
+projectors or assume that auxiliary roles are untouched between calls.
+
+### 4. Attainment
+
+On active role 1 use `A,P`; on role 2 use `A,Q`; on role 3 use `B,P`; on
+role 4 use `B,Q`. Use its coordinate projector for each call. The two calls
+on a role multiply to the monomial at the sum of their addresses; all other
+roles are unchanged. This is an eight-call identity for every `w` and every
+choice of `R`, because it does not use the added label.
+
+Signed scales do permit longer words: after this construction, an `A` call
+and an `R=-A` call on the same projector multiply to identity. Thus a
+10-call exact word may use the extra frame. The minimum, rather than
+prohibition of all extra-frame uses, is what was proved.
+
+## Reproduction and evidence
+
+Python 3.12, standard library only. The registered runner validates source
+and task metadata and executes both ordinary and optimized modes:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/bit-single-scaled-frame-floor
+python3.12 -I -W error -B research/bit-single-scaled-frame-floor/verify.py
+python3.12 -I -O -W error -B research/bit-single-scaled-frame-floor/verify.py
+```
+
+`verify.py` authenticates the three live predecessor READMEs, verifies the
+integer-circle reduction and unique old-pair supports, and loads the literal
+bytes of `independent.py` without a bytecode-cache import. The independent
+checker derives `R` from all 462 nonnegative multiplicity profiles with
+`r>=1` and total count at most seven. It obtains 40 determinant candidates,
+20 frames, 160 target-support checks, four survivors, and four rank-two
+versus rank-four certificates. It does not assume axis alignment in advance.
+
+Literal group-algebra multiplication verifies six direct/free-conjugated
+attaining words at widths 4, 5 and 7, including non-coordinate projectors and transient writes to dirty roles;
+49 dropped-factor, doubled-address and non-idempotent mutations are rejected.
+Additional controls check longer words for `R=-A` and `R=A/2`, a broken
+negative loop, a failure to restore an extra dirty role, and two hand-computed products of
+noncommuting projectors that distinguish reversed multiplication. These finite
+fixtures test the code and hypotheses. The universal result is the proof
+above, not an exhaustive search over rational frames or role widths.
+
+Local evidence: CPython 3.12.14, macOS arm64; normal and optimized replay.
+No native conversion, addition invoice, all-size multiplication theorem,
+formal-kernel proof, or new selected-frontier cold replay is supplied.
+
+## Task, overlap and source context
+
+Base `721c03822c421b7f7fcbb2598993b947c4d88419`, priority revision 8.
+Task `bit-new-register-model`, scope key `7084092dd726e7ba1f2f`; the full
+original catalogue card is retained in [TASK.json](TASK.json).
+**Scope changed:** the user selected PR6032's one-scaled-frame handoff,
+so this is a formal alphabet barrier for its four-target endpoint, rather
+than a native larger/nonabelian supplier construction. It identifies a
+specific extension that cannot save a call; no κ implication is asserted.
+The selected-record binding orientation passed at this same base; that is
+not a scientific replay of the selected construction.
+
+Canonical claim/status:
+[handoff reply](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19233747).
+Live all-state PR searches on 2026-10-28 for `6032`, `scaled frame eight`
+and `rank-one 2910` found the predecessors below and no general one-scaled-frame
+successor. The offline overlap helper searched only 18 local note records
+out of 8,348 at HEAD, with no usable cached remote snapshot. These searches
+are not a novelty certificate; sparse files and unpublished work remain
+coverage gaps. The inspected handoff and nearest merged results determine
+this bounded scope.
+
+| Predecessor | Inspected head | Role here |
+|---|---|---|
+| [PR2085](https://github.com/CrocSwap/integer-mult-bounds/pull/2085) | `5302b9bad6345413a0cabb0afd926d84e44c12e3` | Four-target model and augmentation method |
+| [PR2910](https://github.com/CrocSwap/integer-mult-bounds/pull/2910) | `26ce4ed46112438b237fab54e6da1953c1d16174` | Earlier determinant obstruction for the fixed t=1/2 frame, including dirty workspace |
+| [PR6032](https://github.com/CrocSwap/integer-mult-bounds/pull/6032) | `3b098803eb854afbd5d63ad3bf4d75cdb1e515d5` | Every normalized rational-slope frame, support method, and scaled-frame next question |
+
+[SOURCES.json](SOURCES.json) pins their canonical README bytes at the base.
+No predecessor executable is imported, and no finite predecessor census is
+needed for the zero-extra-call case: determinant trace already gives eight.
+PR2910 had settled the fixed `t=1/2` case before PR6032; it is not a new
+conclusion of this package.
+
+## Open next questions
+
+Structured relevance, first steps and blockers are in [TASK.json](TASK.json).
+
+1. **Can two added rational rank-one frames beat eight for this endpoint?**
+   Start with the joint determinant equation and simultaneous exponent-support
+   constraints for at most seven calls, then test surviving first-order
+   equations. This is the remaining alphabet extension explicitly suggested
+   in PR6032. A candidate still needs an exact word and a fully charged native
+   implementation before it can contribute to the multiplication bound.
+2. **Which positive rank-one frames can occur in any exact word, at any
+   length?** The present proof excludes savings, not all uses. Start from
+   equation (1) and the support/rank constraints without the seven-call cap;
+   distinguish reciprocal old-frame subdivisions (which have explicit longer
+   words) from off-axis frames. An all-length classification is not proved
+   or certified here.
+
+## Credit and license
+
+Prepared by **apoursh**, with substantial OpenAI Codex assistance in proof,
+implementation and separate adversarial proof/code audits. These are agent
+audits, not independent human or formal-kernel acceptance. Apache-2.0.
+
+Cinna Davis's PR2085/2112 supplies the endpoint, four-register/fifth-frame
+investigations and augmentation lineage. Nick Petalas's PR2910 supplies the
+earlier determinant obstruction; PR6032 supplies the all-rational normalized
+family and scaled-frame handoff. Credit also Philippe Van Velzen's earlier
+fixed-frame argument, as retained in PR2910 and
+[Discussion2091](https://github.com/CrocSwap/integer-mult-bounds/discussions/2091#discussioncomment-18935374),
+and the retained BIT precursor lineage. The determinant lemma, subset-support
+necessity and first-order technique are inherited methods, not new claims.

research/bit-single-scaled-frame-floor/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "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/bit-fifth-frame-determinant-obstruction/README.md",
+      "usage": "input",
+      "git_blob": "608a24af8bc3d27ee1554c94872601bb3a409f67",
+      "sha256": "fa3f0f951146caa5b1eb7b7417175eb7a380cae8674e4a470407517dac40f227"
+    },
+    {
+      "path": "research/bit-fifth-rational-frame-every-rational-t/README.md",
+      "usage": "input",
+      "git_blob": "a7c6b3a06b8f215b983536934bb37cd6a0324945",
+      "sha256": "90ba9a56a928c4dc44fa771413e0356ea2ab05979b5cd91f14aa5ed2eeaafe3e"
+    },
+    {
+      "path": "research/bit-four-register-rational-frame-floor-seed3573e12e/README.md",
+      "usage": "input",
+      "git_blob": "32f600d6cb56c94f931a4dc98fb97573ecc134f7",
+      "sha256": "40cbc4ec8e5c49930d7cb8ecf9e462a08266fe604ea426aa5c7b0d5e547fdffd"
+    }
+  ]
+}

research/bit-single-scaled-frame-floor/TASK.json

@@ -0,0 +1,72 @@
+{
+  "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": "Prove the exact eight-call minimum for the PR2085 four-target endpoint after adding one arbitrary symmetric rational rank-one address, including signed scaling and any finite number of restored dirty roles with free address-independent binary mixing.",
+  "scope_change_reason": "Explicit user-selected follow-up to PR6032 Open next questions. This is a scoped formal alphabet barrier, not the original card's larger/nonabelian native supplier construction. It removes one proposed escape without claiming a paid supplier or kappa gain.",
+  "bottleneck_link": "Side result: one scaled rank-one extension cannot improve the eight-call formal primitive. Two-frame alphabets or changed endpoints remain possible; native implementation and complete paid invoices are separate obligations.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after a self-contained proof, independent exact count/support/rank verification, meaningful controls and one focused package; stop earlier if a gap invalidates the theorem. Do not launch broader word searches.",
+  "outcome": "completed",
+  "evidence": "README.md gives the arbitrary-R/all-finite-width proof. verify.py and independent.py check 462 count profiles, 40 determinant candidates/20 frames, 160 support conditions, four survivors/four rank obstructions, six exact words at widths 4/5/7, 49 rejected mutations, two longer-word witnesses and three additional failure controls and two hand-computed noncommuting products. Source hashes and normal/optimized registered replay are checked. Universal claims rest on the proof, not finite fixtures.",
+  "author": "apoursh",
+  "ai_assistance": "Substantial OpenAI Codex assistance in proof, code, source review and separate agent proof/code audits; no independent human or formal-kernel acceptance claimed.",
+  "open_questions": [
+    {
+      "question": "Can two added rational rank-one frames beat eight calls for the same endpoint?",
+      "why_it_matters": "This is the next alphabet extension suggested by PR6032 and is not excluded by the one-frame theorem.",
+      "first_step": "Use the joint determinant equation and target-support constraints for at most seven calls; test the first-order equations only for surviving multiplicities.",
+      "blocked_by": "No joint universal classification or exact saving word is supplied. Native implementation and a full paid invoice are required before any multiplication-bound use."
+    },
+    {
+      "question": "Which positive rank-one frames can occur in exact words of arbitrary length?",
+      "why_it_matters": "The minimum-eight theorem does not classify all possible extra-frame use; reciprocal old-frame subdivisions have explicit longer words.",
+      "first_step": "Remove the seven-call cap from the determinant/support/rank argument and classify positive frames, beginning with reciprocal old-frame subdivisions.",
+      "blocked_by": "An all-length classification and its certificate are not provided in this package."
+    }
+  ],
+  "coordination_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19233747",
+  "scope_key": "7084092dd726e7ba1f2f"
+}