Two added positive rank-one BIT frames cannot give a seven-call word: answers #6104 Q1 (no new κ)

research/bit-two-positive-frames-seven-call/README.md

@@ -0,0 +1,243 @@
+# Two added positive frames cannot give a seven-call word
+
+This package answers open question 1 of JoyboyBrian's
+[handoff #6104](https://github.com/CrocSwap/integer-mult-bounds/discussions/6104),
+which is also apoursh's two-frame question in
+[PR #6089](https://github.com/CrocSwap/integer-mult-bounds/pull/6089). Add two
+nonzero positive rational rank-one addresses `R` and `S` to the PR2085/2112
+four-target alphabet. Then **no exact word of at most seven calls uses both
+of them**. This holds for every direction and scale of `R` and `S`, every
+finite restored dirty width and any free binary mixing.
+
+The proof uses only necessary conditions: the determinant identity, the four
+target-support systems, and first-order character rank on the exact address
+lattice. It needs no word census. A stdlib verifier enumerates every count
+profile, settles the pinned splits exactly, and checks the uniform lemma for
+the seven continuous families on a direction grid. No new κ, supplier or
+native saving is claimed.
+
+## Model
+
+As in PR6089 and the handoff, put
+
+```text
+A = [[1,0],[0,0]]   B = [[0,0],[0,1]]
+P = (1/2)[[1,1],[1,1]]   Q = (1/2)[[1,-1],[-1,1]]     (A+B = P+Q = I)
+```
+
+Let `R`, `S` be nonzero positive semidefinite rational symmetric rank-one
+matrices. They may coincide with each other or with an old address. Let
+`Lambda = ZA + ZB + ZP + ZR + ZS`, which has rank three. Work in
+`F2[Lambda]`. A paid call is `I_w + ([F]-1)N` with `F in {A,B,P,Q,R,S}` and
+`N` a binary rank-one idempotent on any finite width `w >= 4`. Free
+address-independent `GL_w(F2)` maps cost nothing. The endpoint is
+
+```text
+T_w = diag([A+P], [A+Q], [B+P], [B+Q], 1, ..., 1)
+```
+
+with every extra role restored. Write `a,b,p,q,r,s` for the label counts. The
+question requires `r, s >= 1` and `a+b+p+q+r+s <= 7`, so `n = a+b+p+q <= 5`.
+
+## Theorem
+
+For every finite `w >= 4` and every such `R, S`, no exact word with at most
+seven paid calls has `r >= 1` and `s >= 1`.
+
+Combined with PR6089's single-frame theorem (an `R`-using word has at least
+`m+7 >= 8` calls) and the known eight-call floor for `{A,B,P,Q}`, this means
+no word with at most two added positive frames beats eight calls. That
+combined statement inherits PR6089's review status. PR6089 is pending and is
+not re-verified here.
+
+## Proof
+
+**Step 1 (determinant; Nick Petalas, PR2910).** `det(I+([F]-1)xy^T) = [F]`,
+free maps have determinant 1, and `det T_w = [4I]`. So
+
+```text
+rR + sS = M := 4I - aA - bB - pP - qQ.
+```
+
+Since `R` and `S` are positive and nonzero, `M` is positive semidefinite and
+nonzero. Write `X = rR`, so that `S = (M-X)/s`. Both `X` and `M-X` must be
+positive rank one. Of the profiles with `r,s >= 1` and `n+r+s <= 7`, 442 have
+positive semidefinite nonzero `M`.
+
+**Step 2 (support).** Conjugate the free maps to the end. By augmentation the
+last free map is the identity (PR6089 §1). Expand each factor as
+`(I+N) + [F]N`. The coefficient of `[H]` in a diagonal entry is a sum over
+subsets of calls whose labels sum to `H`. So for each target exponent
+`H_j`, there are integers `0 <= u_F <= count(F)` with
+`sum_F u_F F = H_j`. With `alpha = u_R/r - u_S/s` and `beta = u_S/s`, this
+reads
+
+```text
+alpha X = H_j - (u_A A + u_B B + u_P P + u_Q Q) - beta M =: K.
+```
+
+There are two cases:
+
+- If `alpha = 0`, the solution holds for every split exactly when `K = 0`.
+  Call that solution *free*.
+- If `alpha != 0`, it forces `X = K/alpha`. This counts only when `X` and
+  `M-X` are positive rank one.
+
+A target with no free solution confines `X` to a finite set. Exactly seven
+profiles have a free solution for all four targets:
+`(1,1,1,1,1,1)`, `(1,1,1,1,1,2)`, `(1,1,1,1,2,1)`, `(2,1,1,1,1,1)`,
+`(1,2,1,1,1,1)`, `(1,1,2,1,1,1)` and `(1,1,1,2,1,1)`. All seven use the
+old-only support, which is unique: for `A+P` it is `u_A = u_P = 1` and the
+rest zero, and similarly for the other targets. The enumeration finds no
+balanced free support (`alpha = 0`, `beta > 0`) at seven calls. In every other
+profile, the four finite sets intersect in 32 splits in total. Every one of
+them has `R` and `S` proportional to old addresses, for example
+`(0,1,1,1,1,3)` with `R = 2B` and `S = A`.
+
+**Step 3 (characters; method from PR6089 and the handoff).** An additive
+`chi: Lambda -> F2` induces the ring map `[F] -> 1 + chi(F) eps` into
+`F2[eps]/(eps^2)`. Exactness gives
+`sum_{i: chi(F_i)=1} N_i = diag(chi(H_1),...,chi(H_4),0,...)`. Hence the
+number of detected calls is at least the number of targets with
+`chi(H_j) = 1`. For each of the 32 pinned splits, the verifier computes an
+integer basis of the actual `Lambda` and tests all eight characters. Each
+split fails for some character, with 2 detected calls against 4 targets.
+
+**Step 4 (the seven continuous families).** Let
+`L = Z_(2)A + Z_(2)B + Z_(2)P`, the old lattice with odd denominators
+allowed. Its coordinates are `(alpha, beta, gamma) = (m11-m12, m22-m12, 2m12)`.
+If `R, S` lie in `L`, then two functionals restrict to characters of
+`Lambda`:
+
+```text
+chi_PQ = gamma mod 2      (A,B -> 0; P,Q -> 1; all four targets -> 1)
+chi_AB = alpha+beta mod 2 (A,B -> 1; P,Q -> 0; all four targets -> 1)
+```
+
+If such a character also kills `R` and `S`, it detects exactly two calls in
+every family (`p+q = 2` or `a+b = 2` respectively) against four targets. That
+is a contradiction. Write the split direction as a primitive integer vector
+`(x,y)` and `pi = (x^2, y^2, xy)/h` with `h = x^2+y^2`.
+
+- *`M = 2I`: profiles `(1,1,1,1,r,s)`, `(r,s)` in `{(1,1),(1,2),(2,1)}`.*
+  Here `det(2I - t vv^T) = 0` forces `X = 2 pi_u` and `M - X = 2 pi_{u⊥}`.
+  So `{R,S}` is `{2pi_u, 2pi_{u⊥}}`, `{2pi_u, pi_{u⊥}}` or `{pi_u, 2pi_{u⊥}}`.
+  - If `x` and `y` have opposite parity, `h` is odd. Then `pi_u` and `pi_{u⊥}`
+    have 2-integral entries and lie in `L`. Their `gamma = ±2xy/h` is even, so
+    `chi_PQ` kills all four matrices.
+  - If `x` and `y` are both odd, then `h = 2k` with `k` odd. Now
+    `2pi_u = (x^2,y^2,xy)/k` lies in `L` with `alpha+beta = (x-y)^2/k`, which
+    is divisible by 4. Also `pi_{u⊥} = (y^2,x^2,-xy)/(2k)` has
+    `alpha = y(y+x)/(2k)`, `beta = x(x+y)/(2k)` and `gamma = -xy/k`, so it
+    lies in `L` with `alpha+beta = (x+y)^2/(2k)`, which is even. The
+    `u <-> u⊥` swap covers the remaining two matrices. So `chi_AB` kills them.
+
+  This extends the handoff's `M = 2I` argument to `r` or `s` equal to 2, where
+  `R` or `S` is no longer in `2L`.
+- *`M = diag(1,2)`: profile `(2,1,1,1,1,1)`.* The matrix determinant lemma
+  forces `X = 2uu^T/(2x^2+y^2)`, with `R = X` and `S = M - X`.
+  - If `y` is odd, the denominator is odd, `X` lies in `L`, and
+    `gamma = 4xy/(2x^2+y^2)` is even.
+  - If `y = 2y1`, then `x` is odd and `X = (x^2, 4y1^2, 2xy1)/k` with `k`
+    odd. So `X` lies in `L` and `gamma = 4xy1/k` is even.
+
+  Since `M = A + 2B` has `chi_PQ(M) = 0`, `chi_PQ` kills `R` and `S`.
+- *The other three doubled profiles.* They are images of `(2,1,1,1,1,1)` under
+  PR6089 §3's symmetries. Conjugation by `J` fixes `chi_PQ`. Conjugation by
+  `H` permutes `A,B,P,Q`, preserves `L`, and exchanges `chi_PQ` with
+  `chi_AB`. So `(1,2,1,1,1,1)` uses `chi_PQ`, and `(1,1,2,1,1,1)` and
+  `(1,1,1,2,1,1)` use `chi_AB`. The verifier checks all four doubled
+  profiles directly, without using the symmetry.
+
+Every profile is now excluded. QED
+
+## Evidence
+
+`verify.py` uses only the stdlib and exact `Fraction` arithmetic. It imports
+no repository module or predecessor executable. It checks the following:
+
+- the live source hash;
+- all 442 positive semidefinite residual profiles of length at most seven;
+- the support classification: exactly the seven free families and 32 pinned
+  splits;
+- an exact-lattice integer basis and all eight characters for every pinned
+  split;
+- for each free family and every primitive direction with
+  `|x|, y <= 30`, 7,784 cases in all:
+  - the parameterization;
+  - membership in `L`;
+  - the lemma's character kills `R` and `S`, with 2 detected calls against 4
+    targets;
+  - an independent exact-lattice check that agrees.
+
+These grid cases are regression checks; the uniform claim rests on Step 4.
+
+As an independent route that bypasses the `alpha`/`K` classification, the
+verifier also picks 46,916 concrete splits over all 442 profiles. It uses
+primitive directions up to height 8 for definite `M` and rational scales
+`k/m`, `m <= 40`, for rank-one `M`. It tests literal subset sums for all four
+targets: 648 pass, and the exact-lattice characters kill every one of them.
+The verifier also runs these controls:
+
+- *Positive control.* At eight calls, real words survive every filter: 77
+  survivors, including `R = S = A` at `(0,2,2,2,1,1)` and the free
+  `(1,1,2,2,1,1)`. One literal eight-call word, with `R = A` and `S = B`
+  relabelled, is multiplied out in `F2[Lambda]` and equals the endpoint.
+- *Negative controls.* Without the support step, 28 seven-call profiles
+  survive the characters at the split `u = (1,0)`. Naive mod-2 reduction of
+  `1/2` is rejected. A mutated target changes the free-family list.
+
+Runtime is about 30 s per command.
+
+## Reproduce
+
+```sh
+python3.12 -I -W error -B research/bit-two-positive-frames-seven-call/verify.py
+python3.12 -I -O -W error -B research/bit-two-positive-frames-seven-call/verify.py
+```
+
+## Limits
+
+- This is a formal-model lower bound. It provides no native operation,
+  tariff, supplier or κ change, and makes no all-field claim.
+- Only at most two added positive rank-one frames are covered. Three or more
+  frames, negative or indefinite frames, and higher-rank added addresses are
+  not covered.
+- The combined "nothing beats eight" corollary depends on the pending PR6089
+  and is not independently re-verified here.
+- The grid checks are regression evidence, not the proof of Step 4.
+
+## Open next questions
+
+1. **Three or more added positive frames.** With `k` frames, the residual
+   becomes a `k`-term positive rank-one decomposition of `M`. That gives
+   `k-1` continuous parameters. Relevance: this would close the "more
+   positive frames" route for this endpoint at seven calls. First step:
+   repeat Step 2 with `alpha` replaced by a linear form in the `k` split
+   matrices. Check whether the free families still need
+   `a, b, p, q >= 1`, which leaves at most `7-4 = 3` added calls. Blocker:
+   the 2-local membership of a general decomposition is not automatic.
+2. **Eight-call words using two frames.** The eight-call survivors include
+   new non-duplicate candidates, for example `(1,3,0,1,1,2)` with `R = 2A`
+   and `S = P/2`. Decide which are realizable, as in PR6089's `{m+7, 2m+6}`
+   spectrum. Relevance: this is the complete length spectrum, not a cheaper
+   word. First step: try subdivision words.
+3. **Non-positive added frames.** The positivity of `M` is what makes the
+   finite residual list. Indefinite rank-one frames remove it. A different
+   bound on the residual is needed first.
+
+## Credit
+
+- JoyboyBrian (#6104): the two-frame question, the residual
+  parameterization, and the `M = 2I`, `r = s = 1` character argument
+  extended here.
+- apoursh (PR6089): the one-frame classification, the reduction to paid-only
+  words, and the symmetries.
+- Nick Petalas (PR2910): the determinant method.
+- Cinna Davis (PR2085/2112): the model and endpoint.
+- Philippe Van Velzen: the eight-call floor.
+- The retained BIT lineage credited in those sources.
+
+New material prepared for JosieElliston by Claude Opus 5.5 via Claude Code,
+Apache-2.0. Substantial AI assistance. There is no human or proof-kernel
+acceptance.

research/bit-two-positive-frames-seven-call/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "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"
+    }
+  ]
+}

research/bit-two-positive-frames-seven-call/TASK.json

@@ -0,0 +1,76 @@
+{
+  "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": "In the PR2085/2112 four-target formal register model extended by two nonzero positive rational rank-one added addresses R,S (any direction and scale, possibly coinciding), prove that no exact word of at most seven paid calls uses both R and S, for every finite restored dirty width and free binary mixing.",
+  "scope_change_reason": "Took the open handoff #6104 question 1 (JoyboyBrian), which is also PR6089's two-frame open question, instead of the card's native larger/nonabelian construction. This is a formal alphabet lower bound on the same endpoint.",
+  "bottleneck_link": "Scoped side result: adding up to two positive rank-one frames cannot produce a cheaper (fewer than eight call) primitive for this endpoint; such extensions are not a route to a BIT saving here.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at a complete necessary-condition elimination of every count profile with an exact verifier, or at the first surviving profile (reported as the remaining obligation). No word census.",
+  "outcome": "completed",
+  "evidence": "README.md proof: determinant residual (442 psd profiles), exact support systems (7 free families with old-only supports, 32 pinned splits, all on old directions), exact-lattice character rank kills all pinned splits, uniform 2-local chi_PQ/chi_AB lemma kills the seven free families. verify.py (stdlib, ~5 s) checks all finite steps, 7784 grid regression cases for the free families against both the lemma and the exact lattice a direct-subset-sum regression over 46916 concrete splits of all 442 profiles (648 support survivors, all killed by exact-lattice characters), an eight-call positive control (77 survivors incl. literal word multiplied out) and negative controls.",
+  "author": "Josie Elliston (Claude Opus 5.5 via Claude Code)",
+  "ai_assistance": "Proof, verifier and package prepared by Claude Opus 5.5 via Claude Code for JosieElliston; an independent read-only OpenAI Codex adversarial review was requested. No human or proof-kernel acceptance.",
+  "open_questions": [
+    {
+      "question": "Do three or more added positive rank-one frames allow a word of at most seven calls?",
+      "why_it_matters": "Closes the positive-frame extension route for this endpoint at seven calls.",
+      "first_step": "Repeat the support classification with the split replaced by a k-term positive rank-one decomposition of M; check whether free families still force a,b,p,q>=1.",
+      "blocked_by": "2-local membership of a general multi-term decomposition is not automatic."
+    },
+    {
+      "question": "Which eight-call two-frame survivors (for example (1,3,0,1,1,2) with R=2A, S=P/2) are realizable?",
+      "why_it_matters": "Gives the complete two-frame length spectrum, as PR6089 did for one frame; not a cheaper word.",
+      "first_step": "Try subdivision words for each of the 77 eight-call survivors.",
+      "blocked_by": "None known."
+    },
+    {
+      "question": "Do indefinite added rank-one frames escape the eight-call floor?",
+      "why_it_matters": "Positivity of the residual is what makes the profile list finite here.",
+      "first_step": "Find a substitute bound on the residual counts without positivity.",
+      "blocked_by": "No finite residual list without positivity."
+    }
+  ]
+}

research/bit-two-positive-frames-seven-call/VERIFY.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/bit-fifth-frame-determinant-obstruction/README.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Source hash; all 442 psd determinant profiles of length <=7; exact support classification (7 free, 32 pinned); exact-lattice characters on pinned splits; 2-local lemma and exact lattice on 7784 free-family grid cases (regression); eight-call positive controls incl. a literal word; negative controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Source hash; all 442 psd determinant profiles of length <=7; exact support classification (7 free, 32 pinned); exact-lattice characters on pinned splits; 2-local lemma and exact lattice on 7784 free-family grid cases (regression); eight-call positive controls incl. a literal word; negative controls."
+    }
+  ]
+}