Prove exact four-call alternating lattice descent (no κ)

research/bit-four-use-alternating-descent/PROOF.md

@@ -0,0 +1,154 @@
+# Alternating four-call lattice descent
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Model and statement
+
+Let K be any field of characteristic two, let n be a positive integer,
+and let P,Q in M_n(K) be rank-one idempotents. Work over the Laurent
+polynomial ring K[z,z^-1], with z an indeterminate. Put
+
+    E_z(P) = I + (z-1)P,
+    W(P,Q) = E_z(P) E_z(Q) E_z(P) E_z(Q),
+    tau = tr(PQ).
+
+Products act on columns with the rightmost factor acting first. A matrix
+is even if every entry belongs to K[z^2,z^-2]. In address notation z=[s],
+this is descent from Zs to its subgroup 2Zs. There are no intervening
+address-dependent operations in the alternating word studied here.
+
+**Theorem.** W(P,Q) is even if and only if
+
+    P=Q or tau=0.
+
+Every even W(P,Q) is a product of exactly two rank-one calls labelled z^2:
+
+1. If P=Q, then W(P,P) = E_(z^2)(P) E_(z^2)(P).
+2. If P!=Q and tau=0, put
+
+       P' = P+PQ,       Q' = Q+QP.
+
+   These are rank-one idempotents with P'Q'=Q'P'=0, and
+
+       W(P,Q) = E_(z^2)(P') E_(z^2)(Q')
+              = I+(z^2-1)(P'+Q').
+
+The sum P'+Q' is a rank-two projector. The two-call count is minimal
+among words of rank-one z^2 calls and arbitrary constant invertible maps.
+This is an algebraic call count. It makes no assertion that a coarse
+label has the same native price as a fine label.
+
+## The odd coefficient determines descent
+
+Write P=u v and Q=x y, where u,x are nonzero columns, v,y are rows,
+and vu=yx=1. These factorizations exist for rank-one idempotents.
+With alpha=vx and beta=yu, elementary multiplication gives
+
+    tau=alpha beta,
+    PQP=tau P,       QPQ=tau Q,       (PQ)^2=tau PQ.
+
+Set a=z+1, N=P+Q and B=PQ. Then
+
+    E_z(P) E_z(Q) = I+aN+a^2 B,
+    N^2 = N+PQ+QP,
+    NB+BN = tau N.
+
+Squaring the first identity, keeping the matrix order, yields
+
+    W(P,Q) = I + a^2(N+PQ+QP) + a^3 tau N + a^4 tau PQ.
+
+In characteristic two a^2=1+z^2, a^4=1+z^4 and
+a^3=1+z+z^2+z^3. Hence the coefficients of both z and z^3 in W
+are exactly tau(P+Q). There are no other odd degrees. Since K is a
+field, that coefficient vanishes precisely when tau=0 or P=Q. This
+proves the necessary-and-sufficient criterion, for every finite n.
+
+No reduction of a rational address label modulo the field characteristic
+is used. The address exponent and the scalar coefficient field are
+different objects.
+
+## Constructive descent
+
+If P=Q, idempotence gives E_z(P)^2=E_(z^2)(P), proving case 1.
+Suppose tau=0. The displayed rank-one identities give
+
+    (P+PQ)^2=P+PQ,       (Q+QP)^2=Q+QP,
+    (P+PQ)(Q+QP)=0,      (Q+QP)(P+PQ)=0.
+
+The image of P+PQ lies in the one-dimensional image of P. Also
+(P+PQ)u=u, because PQP=0. Thus P' has rank one. The same argument
+gives rank Q'=1. Orthogonality makes their images disjoint, so P'+Q'
+is an idempotent of rank two. In particular tau=0 already implies P!=Q.
+
+The odd-coefficient expansion now reduces to
+
+    W(P,Q)=I+(z^2+1)(P+Q+PQ+QP).
+
+Multiplying the two proposed coarse calls, their cross term vanishes by
+P'Q'=0. Their product is this same matrix. This proves case 2 and its
+complete action on arbitrary input columns, including all spectators.
+
+For minimality, a rank-one idempotent is similar over K to
+diag(1,0,...,0). Consequently det E_z(P)=z and det W=z^4.
+A word with L rank-one z^2 calls and constant invertible maps has
+determinant c z^(2L), for a nonzero constant c. Equality with W forces
+L=2 and c=1. The argument allows free constant maps anywhere in the word.
+
+## A smallest failure of adjacent-pair descent
+
+Over F2 take
+
+    P = [[1,0],       Q = [[0,1],
+         [0,0]],          [0,1]].
+
+Here QP=0 and PQ=[[0,1],[0,0]] is nonzero. In particular P and Q do
+not commute. The theorem supplies
+
+    P'=[[1,1],[0,0]],     Q'=Q,     P'+Q'=I,
+    W(P,Q)=z^2 I_2.
+
+No proper nonempty consecutive block of this four-call word is even.
+Blocks of length one or three have determinant z or z^3, whereas the
+determinant of an even matrix is even. Every length-two block is an
+alternating pair of distinct projectors. Its coefficient of z is P+Q,
+which is nonzero. These are all nine proper consecutive blocks.
+
+This is the smallest example relevant to iterating a two-use reduction.
+An odd number of positive rank-one z calls cannot have an even endpoint
+by determinant parity. A two-call word is even exactly when its two
+projectors agree, by the same coefficient calculation, and then the
+two-use contraction already applies. Four calls therefore give the first
+even endpoint with no even adjacent pair.
+
+Embedding P,Q as zero on any additional coordinates gives this example at
+every n>=2. W is diag(z^2,z^2,1,...,1), so the additional coordinates
+are restored for arbitrary initial data. No zero-initialized scratch is
+assumed.
+
+The example does not contradict the two-use theorem of CubeJerry's
+[PR6148](https://github.com/CrocSwap/integer-mult-bounds/pull/6148).
+That theorem assumes exactly two odd calls in the block being contracted.
+The example has four. It rules out a proposed shortcut that would require
+every even four-call endpoint to expose an even adjacent pair. The new
+coarse projectors show how this particular alternating class descends
+despite the absence of such a pair.
+
+## Scope and remaining obligations
+
+The universal statement is this written proof. The verifier independently
+multiplies full polynomial matrices and applies the literal factors to
+basis columns over finite fields. Those checks corroborate the proof in
+their stated finite domains. They are not its all-width justification.
+
+The result assumes an infinite-order address generator, one repeated fine
+label, constant rank-one projectors, characteristic two, and the alternating
+four-factor order. Four unrelated projectors, arbitrary intervening even
+operations, finite-order address collisions, and other characteristics are
+outside its classification. It does not establish a universal four-use
+descent rule or classify the surviving eight-call profiles of PR6111.
+
+No complete supplier bill, native conversion for 2s, restored physical
+caller, target inventory, stock, compiler, precision/tape implementation,
+new kappa or complete multiplication theorem is supplied. The current
+selected record and its five framework assumptions are unchanged.
+Independent human and formal proof-kernel review are unclaimed.

research/bit-four-use-alternating-descent/README.md

@@ -0,0 +1,131 @@
+# Exact descent for four alternating BIT calls
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+**Claim type: scoped written proof with finite exact corroboration.** No new
+kappa, native supplier or complete multiplication theorem is claimed.
+
+Let K be any characteristic-two field and let P,Q be rank-one idempotents
+of any finite size. Write E_z(P)=I+(z-1)P, with z an infinite-order address
+monomial. Then
+
+    E_z(P) E_z(Q) E_z(P) E_z(Q) is even
+    if and only if P=Q or tr(PQ)=0.
+
+Here even means that every entry has only even powers of z. If P=Q, the
+word equals E_(z^2)(P)^2. Otherwise, for tr(PQ)=0, its exact factorization is
+
+    E_(z^2)(P+PQ) E_(z^2)(Q+QP).
+
+The new projectors are rank one and mutually orthogonal. Exactly two coarse
+calls are necessary by determinant degree, even with arbitrary free constant
+invertible maps. Their native cost is not established by this algebraic count.
+
+A noncommuting example has
+
+    P=[[1,0],[0,0]],  Q=[[0,1],[0,1]],  word=z^2 I_2.
+
+All nine proper nonempty consecutive blocks are not even. Four is the
+smallest call count that can have an even endpoint without exposing an even
+adjacent pair. Thus iterating an adjacent-pair rule cannot exhaust even
+four-use words. The explicit coarse factorization resolves this alternating
+class without such a rule. The complete argument is in [PROOF.md](PROOF.md).
+
+## Evidence
+
+The verifier enumerates all ordered rank-one idempotent pairs in each row.
+One engine multiplies polynomial matrices. A second engine applies literal
+factors to every basis column without polynomial matrix multiplication.
+Both compare the complete endpoint, including arbitrary dirty spectator
+columns. Every even case also has its proposed coarse factors multiplied.
+
+| Field | Width | Ordered pairs | Equal | Orthogonal distinct | Noncommuting even | Not even |
+|---|---:|---:|---:|---:|---:|---:|
+| F2 | 1 | 1 | 1 | 0 | 0 | 0 |
+| F2 | 2 | 36 | 6 | 6 | 12 | 12 |
+| F2 | 3 | 784 | 28 | 168 | 336 | 252 |
+| F2 | 4 | 14400 | 120 | 3360 | 6720 | 4200 |
+| F4 | 1 | 1 | 1 | 0 | 0 | 0 |
+| F4 | 2 | 400 | 20 | 20 | 120 | 240 |
+| F8 | 1 | 1 | 1 | 0 | 0 | 0 |
+| F8 | 2 | 5184 | 72 | 72 | 1008 | 4032 |
+
+There are 20807 pairs in total. Separate controls enumerate the nine proper
+blocks, check five semantic predicates including missing cross-term and
+changed-call mutations, and reject six invalid inputs with exact reasons.
+The generated stdout receipt binds the package files by SHA256. No receipt
+is handwritten and replay writes no files.
+
+## Reproduce
+
+From the repository root, using the Python 3.12 standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -B -W error research/bit-four-use-alternating-descent/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -B -W error research/bit-four-use-alternating-descent/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/bit-four-use-alternating-descent
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/bit-four-use-alternating-descent --check-source-history
+```
+
+Other hosts may use any CPython 3.12 interpreter. The expected receipt status
+is `PASS_BIT_FOUR_USE_ALTERNATING_DESCENT`. Each registered command has a
+120-second timeout. Direct replay is also Git-free and needs only these six
+package files. Source pins are historical provenance, not imported code or
+runtime dependencies. The selected baseline binding command passed at
+canonical main `7c49fe32c55de02c2c873655c804b16e4c3fef0a`.
+
+## Credit and scope
+
+CubeJerry's [PR6148](https://github.com/CrocSwap/integer-mult-bounds/pull/6148)
+poses the four-odd-call question and proves two-use descent. This result
+answers its suggested first step for an alternating class; it does not
+replay the predecessor or settle general four-use descent. Its README is
+pinned as provenance in [SOURCES.json](SOURCES.json).
+
+Credit JosieElliston PR6111 and JoyboyBrian PR6104 for the two-frame questions,
+apoursh PR6089 for the one-frame work, Nick Petalas PR2910 for the determinant
+model, Cinna Davis PR2085/2112 for the endpoint/operation model, Philippe Van
+Velzen for the earlier BIT call floor, and their retained lineage. Rank-one
+factorization, determinant degree and characteristic-two expansion are
+classical methods; no literature priority for them is claimed.
+
+The originating card is explicitly changed to this algebraic side result in
+[TASK.json](TASK.json). No actual native doubled-frame tariff, target inventory,
+physical caller, stock, compiler, precision/tape implementation or outer bill
+is supplied. No general four-projector theorem, arbitrary intervening-even
+operation theorem, finite-order address claim or other-characteristic claim
+is made. The universal claim rests on the written proof. The finite census
+has only its displayed coverage. Independent human and formal proof-kernel
+review are unclaimed. Lean, Docker, predecessor scientific suites and the
+selected complete replay were not run. The selected frontier is unchanged.
+
+## Code constraints
+
+Scientific loops have fixed domains: width at most four, field size at most
+eight, word length at most four and polynomial degree at most four. The
+largest pair domain has 14400 entries and is streamed. Matrices have at most
+16 entries, the largest projector list used has 120 entries, and no search,
+subprocess, recursion or external import is used. Every function has fewer
+than 60 physical lines. Checks use explicit exceptions and remain active
+under optimized Python. Both registered commands make warnings errors.
+
+Power-of-ten rule 3 deviation: Python integers, tuples and standard-library
+operations allocate dynamically. The fixed domains above bound live data;
+only one pair's polynomial endpoint is retained at a time. There is no
+real-time guarantee. Extending the finite domains requires revisiting those
+bounds before enlarging the replay. The package's standalone verifier has
+no public mutable state or cleanup ownership. Optional external analyzers
+are not part of its environment; syntax is checked by in-memory compilation.
+
+## Open next questions
+
+1. Does an even word of four unrelated rank-one projectors always admit two
+   coarse calls? Start with full polynomial endpoints at width two and seek
+   a counterexample or a replacement invariant. The alternating-square
+   calculation does not cover that question.
+2. Can an actual BIT profile use this factorization with a favorable native
+   invoice? First identify the exact four-call region, source/target contracts
+   and a priced doubled-frame implementation. No physical realization or
+   complete bill is supplied here.
+
+TASK.json records why these questions matter, their first steps and blockers.

research/bit-four-use-alternating-descent/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-two-use-lattice-descent/README.md",
+      "usage": "provenance",
+      "git_blob": "0b29fc26fe73f5cdc44b121ed406b65bdce59e12",
+      "sha256": "d078d83e7f902b0cc68a43e33825ab0ae869acd6c97eda31990814e75d46b7a4"
+    }
+  ]
+}

research/bit-four-use-alternating-descent/TASK.json

@@ -0,0 +1,78 @@
+{
+  "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": "Classify even endpoints and construct coarse factorizations for four alternating rank-one calls over every characteristic-two field, with a smallest noncommuting example having no proper even consecutive block.",
+  "scope_change_reason": "The current picker suggested verification tooling. The explicit original-result assignment takes precedence; this takes Open next question 2 of CubeJerry PR6148 as an algebraic side result instead of repeating a census or auditing a predecessor.",
+  "bottleneck_link": "An exact descent rule can strengthen BIT profile pruning. The example prevents rejecting four-use words solely because no even adjacent pair is exposed; native coarse-label pricing and an actual supplier remain separate.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first proved and reproducible original improvement; do not extend from this alternating class to general four-call words.",
+  "outcome": "completed",
+  "evidence": "PROOF.md proves the all-field/all-width criterion and two-call factorization. verify.py checks 20807 ordered pairs over F2/F4/F8 with two literal polynomial engines, all nine proper blocks of the noncommuting example, five semantic checks and six invalid inputs.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Does every even product of four arbitrary rank-one z calls admit a two-call z^2 factorization, when its projectors are not alternating?",
+      "why_it_matters": "This would decide whether the same exact coarse-label simplification extends beyond the proved family.",
+      "first_step": "Expand four independent projectors over F2 at width two and seek a counterexample or a separate factorization invariant; retain exact full polynomial endpoints.",
+      "blocked_by": "The single trace invariant proved here uses the alternating square and does not settle four independent projectors."
+    },
+    {
+      "question": "Can a source-bound BIT profile use this descent at a favorable complete native cost?",
+      "why_it_matters": "Only native prices, restored inputs and independent productive targets could turn the algebraic simplification into a supplier improvement.",
+      "first_step": "Identify one exact four-call region, its complete boundary contract and the actual implementation/tariff of the doubled frame before any construction search.",
+      "blocked_by": "No doubled-frame native implementation, physical caller or complete paid/target invoice is supplied."
+    }
+  ],
+  "question_source": {
+    "pr": 6148,
+    "author": "CubeJerry",
+    "question": "Open next question 2: four calls in the odd coset",
+    "source_head": "d2cba5a85ff80532661f9370700abe6c3678aaf9"
+  },
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19358875",
+  "baseline": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY at selected6030; source orientation only, no scientific replay."
+}