Prove eight-call floor for two arbitrary signed rank-one frames (no κ)

research/bit-two-signed-frame-floor/PROOF.md

@@ -0,0 +1,209 @@
+# Two signed added frames still require eight calls
+
+Prepared by apoursh with substantial OpenAI Codex assistance. Apache-2.0.
+
+## Model and dependencies
+
+Use Cinna Davis's PR2085/2112 formal register model. Addresses are rational
+symmetric 2-by-2 matrices, with
+
+```
+A = diag(1,0), B = diag(0,1),
+P = [[1,1],[1,1]]/2, Q = [[1,-1],[-1,1]]/2.
+A+B = P+Q = I2.
+```
+
+Add two arbitrary nonzero symmetric rational rank-one addresses R,S. Either
+sign is allowed, including equal addresses, opposite addresses and old-label
+duplicates. A real symmetric rank-one matrix has exactly one nonzero real
+eigenvalue: it is positive or negative semidefinite, never indefinite.
+
+Let Lambda be the additive lattice generated by A,B,P,R,S. Over F2[Lambda],
+a paid factor is D_N(F)=I_w+([F]-1)N, where N is any binary rank-one idempotent
+and F is one of the six labels. Arbitrary address-independent GL_w(F2)
+maps are free. Every role initially contains arbitrary data. For any finite
+w>=4 the required complete endpoint is
+
+```
+T_w = diag([A+P],[A+Q],[B+P],[B+Q],1,...,1).
+```
+
+Extra roles must be restored exactly; no clean workspace is assumed. The
+objective is paid-call count only, with no physical native tariff asserted.
+
+**Theorem.** The exact minimum is eight, even with these two signed additions.
+
+The new result is the sign reduction below. The final positive-case
+exclusion is **Josie Elliston's PR6111 theorem**, pinned in SOURCES.json;
+the one-added-frame case is **apoursh's PR6079 theorem**, also pinned.
+These are explicit theorem dependencies, not new proofs or fresh scientific
+replays of those predecessors. The reduction itself is proved below without
+relying on a search or on PR6111's finite support classification.
+
+## 1. Necessary invariants
+
+Normalize interspersed free maps into conjugates of paid factors and one
+trailing free map. Augmentation [F]->1 sends every paid factor and T_w to
+identity, so that trailing free map is identity. Conjugation preserves
+rank-one idempotence. This is the normalization retained in PR6089.
+
+Write a,b,p,q,r,s for the six nonnegative label counts, and n=a+b+p+q.
+For a hypothetical word of at most seven calls using both added labels,
+r,s>=1 and n<=5. The rank-one determinant identity (PR2910) gives
+
+```
+rR+sS = M = 4I2 - aA - bB - pP - qQ.                 (1)
+```
+
+Indeed det D_N(F)=[F], and all free binary invertible maps have determinant
+one. The target determinant is [4I2]; monomials in this torsion-free group
+algebra are distinct.
+
+Expanding each paid factor as (I+N)+[F]N shows that every target exponent
+H in {A+P,A+Q,B+P,B+Q} must be a subset sum of the paid labels, with each
+occurrence used at most once. Cancellation can remove support; it cannot
+create an exponent absent from every subset. This is necessary, not sufficient.
+
+For an additive character chi:Lambda->F2, substitute [F]->1+chi(F)e,
+where e^2=0. The first-order equation implies
+
+```
+number of calls detected by chi >= number of targets detected by chi. (2)
+```
+
+This follows from rank subadditivity for the sum of the detected N's, and
+holds at every restored width. These determinant, support and character
+methods retain their predecessor attribution.
+
+## 2. Positive-definite residuals force positive summands
+
+If X,Y are nonzero real symmetric rank-one matrices and X+Y is positive
+definite, both X and Y are positive semidefinite. Take nonzero v in ker Y.
+Then v^T X v=v^T(X+Y)v>0, so the unique nonzero eigenvalue of X is positive.
+Exchange X and Y. Apply this to X=rR,Y=sS; their positive integer
+multiplicities preserve signs.
+
+Thus only non-positive-definite M could allow a negative added frame.
+
+## 3. Every indefinite residual fails target support
+
+Put d=a-b, e=p-q. Direct calculation gives
+
+```
+2M = [[8-n-d,-e],[-e,8-n+d]],
+4 det M = (8-n)^2-d^2-e^2,
+|d|+|e| <= n,   d+e = n (mod 2).                    (3)
+```
+
+If n<=4, each old address is an orthogonal projector bounded above by I2,
+so M>= (4-n)I2>=0. An indefinite M therefore requires n=5. Equation (3)
+then requires d^2+e^2>9. Since |d|+|e| is odd and at most five, it must be
+five: if it were at most three, d^2+e^2<=9. Equality with n says there is
+no cancellation within either opposite pair. Hence all five old calls use
+at most one E from {A,B} and at most one G from {P,Q}. If a pair is absent,
+choose either of its members. Also r=s=1.
+
+The matrices E,G,I2 are linearly independent over Q. Define the rational
+linear functional ell by ell(E)=ell(G)=0, ell(I2)=1. The four target
+exponents have ell-values {0,1,1,2}, since the other two old frames are
+I2-E and I2-G. Meanwhile (1) gives ell(R)+ell(S)=4.
+All old calls have ell-value zero, and each of R,S occurs once. Therefore
+every subset sum has ell-value in
+
+```
+{0, rho, 4-rho, 4}, where rho=ell(R).
+```
+
+This set cannot contain both one and two: containing one forces rho=1
+or rho=3, and then two is absent. At least one required target lacks
+support. This excludes the indefinite case even without the rank-one
+assumption on R,S. There are twenty such count profiles; enumeration is
+only a corroboration of this argument.
+
+## 4. Every rank-one residual is also excluded
+
+Since tr M=8-n>=3, a singular residual is nonzero positive rank one.
+If nonzero symmetric rank-one X,Y have rank(X+Y)=1, their image lines
+coincide. Write X=c uu^T,Y=t vv^T with c,t nonzero; then
+
+```
+det(X+Y)=ct (u1*v2-u2*v1)^2.
+```
+
+Thus R,S lie on the whole rational line of M, regardless of their signs.
+
+Equation (3) and |d|+|e|<=n imply n>=4. At n=4 or n=5 the circles
+d^2+e^2=16 or 9 have only axial integer solutions. Up to old-alphabet
+symmetry, the possible old-call multisets are exactly:
+
+| Old calls | Residual | Exclusion |
+|---|---|---|
+| 4E | 4Eperp | Span |
+| 4E+Eperp | 3Eperp | Span |
+| 3E+G+Gperp | 3Eperp | Character |
+
+Here Eperp=I2-E, and {G,Gperp} is the other opposite pair.
+The first row permits r+s<=3; the other rows force r=s=1.
+
+In the first two rows every available label lies in span_Q(E,Eperp).
+Each target combines one frame from each pair and lies outside that span,
+so target support fails.
+
+In the third row choose an integer-valued linear functional on the actual
+lattice: 2*offdiag when E belongs to {A,B}, or first diagonal minus second
+diagonal when E belongs to {P,Q}. It vanishes on the **entire rational**
+line of Eperp as well as on E, and takes values +/-1 on G,Gperp. Thus its
+reduction modulo two is well-defined even if R,S have even denominators.
+It detects only the two G,Gperp calls, but all four targets. Equation (2)
+gives the contradiction 2>=4.
+
+This excludes every rank-one residual. The finite count check has twenty
+full profiles: sixteen span cases and four character cases.
+
+## 5. Conclusion and sharpness
+
+Every residual has positive trace, so the three cases above are exhaustive.
+Any hypothetical <=7-call word using both R,S must have a positive-definite
+residual, which forces both added frames positive. PR6111 excludes that
+case for all directions, scales and finite restored widths.
+
+For words omitting one or both added labels, restrict to the subgroup
+generated by the labels actually used and the target labels. Its group
+algebra injects into F2[Lambda], so the equality also holds in that smaller
+algebra. This restriction matters: unused fractional frames need not allow
+old-lattice characters to extend to the original larger Lambda.
+
+If only one extra label occurs, PR6079 already proves the eight-call floor
+for arbitrary signed scaling. If neither occurs, the two old-lattice
+characters chi_AB and chi_PQ separately require a+b>=4 and p+q>=4, hence
+at least eight calls. Assigning the two displayed summands of each H to
+its own coordinate gives the familiar eight-call word, proving sharpness.
+
+The signed premise is meaningful at longer lengths: replace one A in this
+direct word by 2A,-A on the same coordinate projector. This gives an exact
+nine-call word using both a positive and a negative added frame. Thus the
+reduction is a short-word statement, not an all-length positivity theorem.
+
+## 6. Independent exact corroboration
+
+independent.py separately enumerates all 462 six-count profiles, without
+any sign or PSD filter. In basis (A,B,P), with X=rR and S=(M-X)/s, a
+target subset with added multiplicities i,j satisfies
+
+```
+(s*i-r*j) X = r*s*(H-old_subset) - r*j*M.
+```
+
+A nonzero coefficient pins X; a zero coefficient gives a free solution
+exactly when its right side is zero. Candidate pins are filtered only for
+nonzero symmetric rank one, admitting both signs. Intersecting the four
+target sets gives 435 empty profiles, seven free families, and 32 splits
+across twenty other profiles. All pinned splits turn out positive, and
+each free residual is positive definite. This agrees with the sign
+reduction through an independent classification route. None of these
+necessary-condition survivors is asserted to be a realizable word.
+
+Finite fixtures and mutation controls are implementation evidence. The
+unbounded direction, denominator and width quantifiers come from the
+written reduction and explicitly credited predecessor theorems. No
+independent human review or formal proof-kernel acceptance is claimed.

research/bit-two-signed-frame-floor/README.md

@@ -0,0 +1,143 @@
+# Two signed added rank-one frames still require eight calls
+
+**Scoped proof with exact corroboration.** Allowing either sign for two added
+nonzero symmetric rational rank-one addresses does not lower the eight-call
+minimum for the PR2085/2112 four-target endpoint. Arbitrary finite restored
+dirty workspace and free address-independent binary mixing are allowed.
+This closes the short-word non-positive-frame question in Josie Elliston's
+[PR6111](https://github.com/CrocSwap/integer-mult-bounds/pull/6111).
+
+The new contribution is an elementary **signed-to-positive reduction**.
+The final positive-case exclusion is PR6111's theorem; the one-extra case
+uses [PR6079](https://github.com/CrocSwap/integer-mult-bounds/pull/6079).
+Both sources are archived and `partially_reviewed` in the current central
+ledger. They are explicit mathematical dependencies; their scientific
+replays and independent acceptance are not claimed here.
+
+## Result and proof
+
+Let A=diag(1,0), B=diag(0,1), P=[[1,1],[1,1]]/2 and
+Q=[[1,-1],[-1,1]]/2. The complete endpoint is
+`diag([A+P],[A+Q],[B+P],[B+Q],1,...)`. Each paid factor is
+`I+([F]-1)N`, with binary rank-one idempotent N and
+`F in {A,B,P,Q,R,S}`. R and S may be positive, negative, coincident,
+opposite, or duplicates of old frames. They remain nonzero and rank one.
+
+[PROOF.md](PROOF.md) gives all hypotheses and the width-independent proof.
+For a hypothetical word using both additions in at most seven calls,
+determinant conservation gives
+`rR+sS=M=4I-aA-bB-pP-qQ`, with at most five old calls.
+
+- If M is indefinite, a scalar projection requires both 1 and 2 in
+  `{0,rho,4-rho,4}`, which is impossible.
+- If M has rank one, both additions lie on its line. Exact target support
+  or a first-order character with capacity two and demand four excludes it.
+- If M is positive definite, evaluating on the two kernels forces R and S
+  positive. PR6111 then applies.
+
+The direct eight-call word attains the minimum. Negative frames really can
+appear at longer lengths: replace one A call by 2A followed by -A to get
+an exact nine-call word. This is not an all-length positivity theorem.
+
+There is no native supplier, paid-profile saving, new κ or discharge of any
+selected framework assumption. The selected conditional result remains
+`781451/250000000`. Formal paid calls do not automatically price physical
+operations, and all native/caller/compiler/precision/recovery obligations
+remain separate.
+
+## Evidence and reproduction
+
+Python 3.12, standard library only:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/bit-two-signed-frame-floor
+python3.12 -I -W error -B research/bit-two-signed-frame-floor/verify.py
+python3.12 -I -O -W error -B research/bit-two-signed-frame-floor/verify.py
+```
+
+Expected markers are `PASS_SIGNED_TWO_FRAME_SUPPORT` and
+`PASS_TWO_SIGNED_FRAME_REDUCTION`; the registered runner executes both modes.
+The direct verifier needs only this package and its two declared README
+inputs. It uses no Git, network, nonstandard package or predecessor code.
+
+The elementary check reconstructs all 462 profiles as 422 positive-definite,
+20 indefinite, 16 singular-span and four singular-character cases. It also
+checks the two-summand determinant/sign identity on 576 rational fixtures
+and the three-summand counterexample `-A+2A+B=I` to any overgeneralization.
+
+The separately written checker uses integer subset equations in the rational
+basis (A,B,P), rather than the primary check's physical matrix entries.
+It applies **no PSD or positive-trace filter** to candidate splits. Its
+complete classification gives 435 empty profiles, seven free families and
+32 pinned splits across twenty profiles. Positivity of every pinned split
+is checked afterward. All 148 concrete opposite-sign residual splits fail
+literal target support. Twenty-four control checks include negative rotated
+frames, zero/rank-two rejection, the nine-call signed word on four/six roles,
+omitting its negative call, the ordinary eight-call positive control and
+a changed target. Controls include positive fixtures; “24” is not a count
+of rejected mutants. The independent inventory digest is
+`ed1b074151ab497af3c585f532ad0b0dd4c0cecb4b764721e4109f448d434443`.
+
+These are exact finite checks, not finite extrapolation to arbitrary widths
+or denominators. The written proof supplies those quantifiers. Local
+environment: CPython 3.12.14, macOS arm64. Normal/optimized registered replay,
+source metadata and committed-byte/export checks are separate obligations.
+No formal proof kernel, independent human review or selected cold replay
+is claimed.
+
+## Coordination, sources and scope
+
+Canonical main was fetched before work, and this branch starts at
+`3f0152a32eeebac0df11946dbd50cabe5a7f7839`, priority revision 8.
+[Canonical claim/status](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19270802).
+Task `bit-new-register-model` has **changed scope**, recorded with the full
+original card in [TASK.json](TASK.json): a formal alphabet theorem rather
+than a native larger/nonabelian construction.
+
+The expansion decision is to settle this explicitly open sign hypothesis
+before any implementation campaign. Three added positive frames were
+considered as a different mechanism and remain unreserved. This result
+does not justify more search inside the now-excluded two-frame short model.
+
+Current handoffs and all-state searches for signed/two/rank-one frames,
+three positive frames and PR6111 were inspected on October 29, 2026.
+PR6148 excludes one eight-call half-frame example; PR6186 accelerates
+PR6111's positive checker. Neither supplies this signed reduction.
+The offline helper searched 24 of 8,567 local notes with no usable remote
+snapshot. Sparse local coverage and bounded live searches are not a proof
+of novelty or coverage of unpublished work.
+
+The selected record, source manifest, certificate, review, baseline script
+and all 1,227 previously materialized orientation inputs are unchanged from
+the preceding successful binding-only orientation at main `721c03822`.
+That orientation is reused after a Git-diff check, not described as a fresh
+scientific replay. The selected record hash remains
+`9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa`.
+
+[SOURCES.json](SOURCES.json) pins the exact canonical theorem READMEs:
+PR6111 head `961b749fa40a1117d0746064528d2dfa290c57e0` and PR6079 head
+`44745c427f710e406cb2d2c6de458b7f93d81f01`. Catalogue and selected record
+are historical provenance. Predecessor bytes remain unchanged.
+
+## Open next questions
+
+Can three or more signed additions beat eight? The two-summand kernel
+argument fails already at `-A+2A+B=I`. Start with one explicit three-frame
+candidate and its determinant/support constraints; an exact word and full
+native invoice would still be required for a multiplication improvement.
+No larger search or follow-up is reserved. Structured relevance, first
+step and blockers are in TASK.json.
+
+## Credit
+
+Prepared by **apoursh** with substantial OpenAI Codex assistance in proof,
+implementation and separate agent mathematical/code audits. Apache-2.0.
+Agent reviews are not independent human or proof-kernel acceptance.
+
+Josie Elliston/Claude retains PR6111's positive two-frame theorem and support
+classification; JoyboyBrian retains #6104's question and split formulation;
+apoursh retains PR6089/6079's classification and single-frame result;
+Nick Petalas retains PR2910's determinant method; Cinna Davis retains the
+PR2085/2112 model and endpoint; Philippe Van Velzen and the retained BIT
+lineage keep their prior floor and framework credit. Kernel, determinant
+and rank algebra are classical; no literature-wide priority is claimed.

research/bit-two-signed-frame-floor/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "3f0152a32eeebac0df11946dbd50cabe5a7f7839",
+  "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-single-scaled-frame-floor/README.md",
+      "usage": "input",
+      "git_blob": "826e8e4e7a3a50a56bdec49e6af758069a8ed06f",
+      "sha256": "dae847a3e40b3999c2797b7222d2ff7ad2762e0193b251dd8e9c2a493ab0b27d"
+    },
+    {
+      "path": "research/bit-two-positive-frames-seven-call/README.md",
+      "usage": "input",
+      "git_blob": "98eb6718d0ae424c129cf08b186fd2a5593ca783",
+      "sha256": "8832e843b129a1fc802e1f0db54d6f731eb9bd7b2b82f583c7809dbd9c0857d5"
+    }
+  ]
+}