HANDOFF: Joint determinant and character obstruction for two added positive rank-one BIT frames

[JoyboyBrian]

R20 task03: two positive added BIT frames — bounded handoff

Status: incomplete investigation; no exact word and no seven-call exclusion.
Prepared by JoyboyBrian with substantial OpenAI Codex assistance. Apache-2.0.
Canonical discussion: #6104
Base: 721c038.
Inspected pending PR6089 head: a736cc6,
research/bit-positive-frame-use/{README.md,PROOF.md}. Credit apoursh for that
one-positive-frame classification; Cinna Davis PR2085/2112 for the model and
endpoint; Nick Petalas PR2910/6032 for determinant, support and character
methods; Philippe Van Velzen and the retained BIT lineage. This handoff uses
no pending executable and makes no independent acceptance claim for PR6089.
Root coordination performed the live source/overlap check. This bounded worker
read the pinned proof, CONTRIBUTING, autoresearch and family expansion gate.

Model and exact reduction

A=diag(1,0), B=diag(0,1), P=(1,1)(1,1)^T/2,
Q=(1,-1)(1,-1)^T/2. Target exponents are A+P,A+Q,B+P,B+Q.
Use the formal group algebra F2[Lambda], where Lambda is generated by these
addresses and two nonzero rational symmetric positive rank-one addresses R,S.
A paid factor is I+([F]-1)N with a binary rank-one idempotent N, on any finite
width w>=4. Free binary mixing can be absorbed by conjugation; augmentation
forces its final residual to identity. All dirty roles are restored exactly.
The additional labels must both be used; unused-label cases are predecessor
scope, not the new question.

Write counts a,b,p,q,r,s, with r,s>=1 and total at most seven. Determinants give

rR+sS = M = 4I-aA-bB-pP-qQ
     = (1/2)[[8-n-d,-e],[-e,8-n+d]],
n=a+b+p+q<=5, d=a-b, e=p-q.

Necessary positivity is M>=0, hence dd+ee <= (8-n)^2. For rank-one M,
positivity forces both added frames onto its line: for z in ker M,
0=r z^T R z+s z^T S z, so z belongs to both kernels. For positive-definite M,
ALL its rational positive rank-one decompositions are parameterized by a
nonzero rational vector u, modulo scaling:

X = u u^T / (u^T M^{-1} u),   R=X/r,   S=(M-X)/s.

Indeed the determinant lemma makes det(M-X)=0; conjugation by M^{-1/2}
makes X a rank-one orthogonal projector, proving M-X>=0 and rank one.
Conversely a positive rank-one X=t u u^T with det(M-X)=0 forces exactly this
t. This is a proof over rational matrices; the real square root is only used
to establish positivity. Thus finitely many count profiles still leave a
rational projective-line parameter for each positive-definite residual.
The predecessor's integer-circle equality does not extend to this case.

Joint necessary conditions still to be solved

For EACH character chi: Lambda -> F2, exact equality requires

sum_i chi(F_i) N_i = diag(chi(A+P),chi(A+Q),
                          chi(B+P),chi(B+Q),0,...,0).

Consequently the number of detected calls must be at least the number of
nonzero target character values. These are joint projector equations, not
merely separate rank inequalities. Lambda is free abelian of rank three
since it contains A,B,P and lies in Sym_2(Q), so it has eight binary characters.
Their values depend on the actual finitely generated integer lattice including R,S: arbitrarily
reducing rational matrix entries modulo two is invalid. A safe implementation
would compute an integer basis for Lambda, then all its mod-two characters.

For EACH target H, support additionally requires integers

0<=u_F<=count(F),    sum_F u_F F = H.

This follows by expanding each factor as (I-N)+[F]N. Cancellation can delete
exponents but cannot create them. These support conditions are necessary, not
sufficient and not independent constructions of the four target columns.
A successor should combine these exact conditions with the parameterization,
then address the simultaneous projector/coefficient equations. This worker
has NOT proved that any parameter survives all these necessary conditions.

A continuous determinant family really is eliminated by a safe character

Take a=b=p=q=r=s=1 (six calls), so M=2I. For coprime integers p0,q0,
not both zero, let h=p0^2+q0^2 and

R=2/h [[p0^2,p0*q0],[p0*q0,q0^2]], S=2I-R.

All rational directions occur. In the old basis (A,B,P), R has coordinates

(2*p0*(p0-q0)/h, 2*q0*(q0-p0)/h, 4*p0*q0/h).

Each coordinate is twice a rational with odd denominator: if p0,q0 have
different parity, h is odd; if both are odd, h=2k for odd k and p0-q0 is
even. Thus R,S lie in 2L_(2), where L_(2) is the old lattice with all odd
denominators allowed. The character chi(A)=chi(B)=1, chi(P)=chi(Q)=0
extends to L_(2) and restricts safely to Lambda. It kills R,S, detects only
the two A,B calls, and sends all four target exponents to one. Rank at most
two cannot equal four. This excludes this entire family, uniformly in dirty
width. It does not exclude the other count profiles or address scales.

Evidence and bounded stopping decision

The unpublished local-only companion check.py verifies the residual split and support example using
exact fractions, and checks parity certificates for primitive directions of
height <=8. The latter is a regression check, NOT the proof of the uniform
parity claim (the two-case argument above is the proof). It rejects a scaled
split mutant through the joint determinant equation. It does not enumerate
all rational slopes, words, projectors, or count profiles.

Commands, from this worktree:

python3 -I -W error -B build/research-coordination/r20/check.py
python3 -I -O -W error -B build/research-coordination/r20/check.py

Source inspection:

git show a736cc61b1436ddb5b8689398e28f51021177839:research/bit-positive-frame-use/PROOF.md

The seven-minute gate stopped expansion at the uncontrolled continuous family.
This written handoff is public in this claim; its companion checker and execution receipts remain local-only. It is not a registered research package
or proposed PR. No official package export/source-history checks are relevant
to a nonpublished build-directory handoff; no full predecessor replay was run.

Open next questions

1. Can denominator-safe character rank inequalities plus four bounded support
   systems eliminate every positive-definite split for n<=5 and r+s<=7-n?
   First isolate a fixed count profile and symbolically eliminate u using the
   four support systems; do not substitute a rational slope census. This would
   decide whether the first-order route can close the proposed escape.
2. If a profile survives, can common rank-one binary idempotents satisfy all
   character equations AND full group-algebra coefficient cancellation?
   A necessary-condition survivor is not a seven-call word. Arbitrary restored
   dirty width remains a universal obligation. Native pricing, a multiplication
   bound, selected-frontier updates and an all-field claim remain outside scope.

This claim is released. No continuing reservation, selected-frontier change or supplier admission is implied.

{
  "schema": "integer-mult-coordination/v1",
  "kind": "HANDOFF",
  "task": "bit-new-register-model",
  "scope": "Joint determinant and character obstruction for two added positive rank-one BIT frames",
  "base": "721c03822c421b7f7fcbb2598993b947c4d88419",
  "expiry": null,
  "artifact": null
}

[JosieElliston]

CLAIM (advisory, about 60 minutes): open question 1 of this handoff. For every count profile (a,b,p,q,r,s) with r,s >= 1 and at most seven calls, I will apply the four exact support systems (each either pins the split X to finitely many values or leaves the family free) and then the denominator-safe character rank inequality on the exact integer lattice of each pinned candidate. The output is the list of eliminated profiles and the exact surviving families, if any, with a stdlib verifier.

Base 721c03822. Predecessors: this handoff (JoyboyBrian, parameterization and the M=2I family), PR6089 (apoursh, one positive frame), PR2910 (Nick Petalas, determinant method). Prepared for JosieElliston by Claude Opus 5.5 via Claude Code.

{
  "schema": "integer-mult-coordination/v1",
  "kind": "CLAIM",
  "task": "bit-new-register-model",
  "scope": "Two added positive rank-one BIT frames, <= 7 calls: support systems plus exact-lattice character rank over every count profile",
  "base": "721c03822c421b7f7fcbb2598993b947c4d88419",
  "expiry": "2026-10-28T10:30:00Z",
  "artifact": null
}

[JosieElliston]

DONE: open question 1 of this handoff is answered negatively. No exact word of at most seven calls uses two added positive rank-one frames, for any directions or scales of R and S (coincident ones included) and any restored dirty width. This settles the general seven-call question left open here.

Public artifact: #6111 (research/bit-two-positive-frames-seven-call/, base 721c03822).

The proof uses only necessary conditions, with no word census:

• Determinant. There are 442 positive semidefinite residual profiles.
• Exact support. Each support solution either holds for every split (alpha = 0, K = 0) or pins it. Exactly 7 profiles are free: (1,1,1,1,r,s) with (r,s) in {(1,1),(1,2),(2,1)}, and the four doubled-old-frame profiles. The rest give 32 pinned splits, all on old directions.
• Pinned splits. Every one fails the character rank inequality on the exact integer lattice, with 2 detected calls against 4 targets.
• Free families. R and S lie in Z_(2)<A,B,P>, and chi_PQ or chi_AB (chosen by the parity of the direction) kills both. That gives 2 detected calls against 4 targets. This extends your M = 2I, r = s = 1 argument to r or s = 2 and to M = diag(1,2) and its images.

The stdlib verifier takes about 30 s with normal and -O. It checks:

• every finite step;
• 7,784 free-family grid regressions;
• an independent concrete-split route: 46,916 splits, 648 support survivors, all killed;
• positive controls at eight calls, including a literal word;
• negative controls.

A read-only Codex adversarial review found no errors. This is AI review only, not human or proof-kernel acceptance.

Combined with #6089's one-frame theorem (pending), no word with at most two added positive frames beats eight calls. Still open:

• three or more frames;
• indefinite frames;
• realizability of the eight-call two-frame survivors, e.g. (1,3,0,1,1,2) with R = 2A, S = P/2.

My claim is released.

Credit: JoyboyBrian (this handoff), apoursh (#6089), Nick Petalas (PR2910), Cinna Davis (PR2085/2112), Philippe Van Velzen. Prepared for JosieElliston by Claude Opus 5.5 via Claude Code.

{
  "schema": "integer-mult-coordination/v1",
  "kind": "DONE",
  "task": "bit-new-register-model",
  "scope": "Two added positive rank-one BIT frames, <= 7 calls: excluded for every count profile",
  "base": "721c03822c421b7f7fcbb2598993b947c4d88419",
  "expiry": null,
  "artifact": "https://github.com/CrocSwap/integer-mult-bounds/pull/6111"
}