Compile a nilpotent chain with optimal reflection calls (no κ)

research/nilpotent-chain-reflection-compiler/PROOF.md

@@ -0,0 +1,148 @@
+# Optimal fixed-involution compilation of a nilpotent chain
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## Contract and theorem
+
+Work over the full formal group algebra F2[C2], where C2={1,g} and g is a
+fixed nonidentity involution. Put Q=1+[g], so Q is nonzero and Q^2=0.
+Let J_n have ones immediately above its diagonal and zero elsewhere.
+The complete endpoint on n arbitrary input roles is
+
+    D_n = I + Q J_n.
+
+Any finite number of additional arbitrary dirty roles is permitted, but the
+endpoint on all roles must be I+Q(J_n direct-sum 0). Every extra role must
+be restored without residual couplings. Clean initialization, erasure,
+discarded roles, other address labels and address-dependent free maps are
+excluded. A paid call is I+Q P for a binary rank-one idempotent P.
+Arbitrary constant binary invertible scalar maps may occur freely anywhere.
+
+For every positive integer n, the exact minimum paid-call count is
+
+    L_n = 2 floor(n/2).
+
+Thus L_n=n-1 for odd n and L_n=n for even n. This includes L_1=0.
+An explicit stream needs no extra role, uses exactly 2(n-1) scalar XORs,
+and contains every scalar conjugator and its inverse. Scalar optimality is
+not claimed. The executable emits this stream for 1<=n<=64; that bound is
+an implementation limit, not a restriction of the proof.
+
+## Lower bound with arbitrary restored dirty workspace
+
+The normalization here is the standard register-model argument retained in
+PR2716 and the earlier register lineage. Conjugating a paid call by a constant
+binary invertible scalar matrix conjugates P, preserving rank-one
+idempotence. Commute all scalar maps to one end. Augmentation [g] -> 1
+makes every paid call and the required endpoint the identity, so their
+remaining scalar product must be the identity as well.
+
+Because Q is central and Q^2=0, the complete word now satisfies
+
+    product_j (I+Q P_j) = I+Q sum_j P_j.
+
+Comparing the coefficient of [g] in the full formal algebra gives
+
+    J_n direct-sum 0 = sum_(j=1)^L P_j.
+
+Rank subadditivity gives L>=rank(J_n)=n-1. Each rank-one idempotent has trace
+one over F2, whereas J_n has trace zero. Consequently L is even. The
+smallest even integer at least n-1 is 2 floor(n/2). Dirty padding changes
+neither rank nor trace, so the lower bound covers every finite allowed
+workspace and every placement of free scalar maps.
+
+The rank, trace and normalization tools are credited background. The new
+step is a matching stream for these non-square-zero chain targets.
+
+## Pair adjacent edges
+
+For three consecutive coordinates a,b,c, write e_a,e_b,e_c for the coordinate
+columns. The two matrices
+
+    P = (e_a+e_b)e_b^T,
+    R = e_b(e_b^T+e_c^T)
+
+are rank-one idempotents. Their defining column/row pairings both equal one.
+Their sum is
+
+    P+R = e_a e_b^T + e_b e_c^T.
+
+The repeated diagonal term e_b e_b^T cancels in characteristic two.
+It follows in the complete formal algebra that
+
+    (I+Q R)(I+Q P) = I+Q(e_a e_b^T+e_b e_c^T).
+
+No commutation of P and R is assumed. Every cross term vanishes because
+it contains Q^2. These two adjacent chain edges therefore cost two calls.
+
+Here is the full chronological coordinate stream, where each addition is
+a scalar whole-role XOR and g acts only on the indicated role:
+
+    a += b
+    b <- g(b)
+    a += b
+    b += c
+    b <- g(b)
+    b += c
+
+For arbitrary initial a,b,c, the first three operations leave
+(a+b+g(b), g(b), c). The last three leave
+
+    (a+b+g(b), b+c+g(c), c).
+
+This derives the full dirty-state endpoint without assuming any input is
+zero. The stream has exactly two reflections and four scalar additions.
+
+## Complete chain and invoice
+
+Partition the n-1 edges into consecutive pairs, starting with edges
+(0,1),(1,2), then (2,3),(3,4), and so on. Use the six-operation stream for
+each pair. If n is even, one edge (n-2,n-1) remains. For that edge use the
+retained factorwise four-operation stream
+
+    a += b; b <- g(b); a += b; b <- g(b).
+
+It maps (a,b) to (a+b+g(b),b), using two reflections and two scalar additions.
+The paired streams can share endpoint roles. Their formal product is still
+I+Q times the sum of their edge matrices, since all cross terms contain Q^2.
+Thus they compose to D_n in any order and leave every spectator untouched.
+
+There are floor((n-1)/2) pairs and one remaining edge exactly when n is even.
+The reflection total is 2 floor((n-1)/2)+2*1_(n even)=2 floor(n/2).
+The scalar total is 4 floor((n-1)/2)+2*1_(n even)=2(n-1).
+This attains the lower bound and proves the theorem. Reversing the complete
+stream gives its inverse, and D_n^2=I by Q^2=0.
+
+At complete stationary primitive prices R for a coordinate reflection and
+C for a whole-role scalar XOR, the specified local bills are
+
+    factorwise PR2716 lowering: 2(n-1)R + 2(n-1)C;
+    supplied joint lowering:  2 floor(n/2)R + 2(n-1)C.
+
+The exact reduction is (n-1)R for odd n and (n-2)R for even n. It is strictly
+positive for n>=3 and R>0. These are primitive-count identities, not measured
+runtime or admitted recursive supplier prices. A supplied scalar change of
+basis S transports the construction to S J_n S^-1, but S and S^-1 must be
+charged. No method for finding or physically hosting a favorable S is supplied.
+
+## Scope and predecessors
+
+ywz65's PR2716 supplies the arbitrary-coupling motivation, Q^2 product identity
+and factorwise dirty lowering. Its dihedral tariff and executable are cited,
+not audited or replayed. Adam Gall PR1911 and the retained eumemic PR288,
+Ali Romman PR468, woklerx PR1443, Gareth Davidson PR1333, Arham Tahir PR1589
+and Cinna Davis PR2290 register-model lineage retain credit.
+
+Nick Petalas's older PR4912 proves a different tariff for square-zero
+couplings. Its extra rank-saturation obstruction is inapplicable to J_n for
+n>=3, because J_n^2 is nonzero. JoyboyBrian's PR5007 changes the workspace
+contract to returned clean roles. Nick Petalas's PR5857 reduces scalar work
+in that clean square-zero stream. The present result has arbitrary dirty
+inputs, requires no clean role, and changes both the endpoint and the
+reflection-count question. None of those predecessor executables is imported.
+
+The universal conclusion rests on the written proof. The finite exact checks
+corroborate it. Native legality, complete routing/frame/basis/ownership,
+precision/tape/stock costs, recursive child admission and the multiplication
+theorem remain open. No new kappa, selected-frontier change, independent human
+review or formal proof-kernel acceptance is claimed.

research/nilpotent-chain-reflection-compiler/README.md

@@ -0,0 +1,129 @@
+# Optimal reflection compilation of a nilpotent chain
+
+This contribution was produced by Nick Petalas.
+
+For a binary nilpotent Jordan chain J_n, the exact fixed-involution
+reflection-call minimum is **2 floor(n/2)**, with arbitrary free binary scalar
+mixing and any finite restored dirty workspace. An explicit stream attains
+it without extra roles, using exactly 2(n-1) scalar XORs. Claim type: scoped
+written algebraic proof with exact finite corroboration.
+
+The first new case, n=3, costs two reflections and four XORs. Applying
+ywz65's [PR2716](https://github.com/CrocSwap/integer-mult-bounds/pull/2716)
+factorwise lowering to its two edges costs four reflections and four XORs.
+Pairing adjacent edges saves address work without adding scalar operations.
+The improvement stops here; multiple-block optimization is left open.
+
+The endpoint is I+(1+[g])J_n over full formal F2[C2], for one fixed nonidentity
+involution g. A paid call has a binary rank-one idempotent coupling. Every
+input is arbitrary dirty data; spectators must be restored. [PROOF.md](PROOF.md)
+derives the full endpoint, its rank/trace lower bound and the complete
+chronological primitive invoice. [compiler.py](compiler.py) emits the literal
+stream for 1<=n<=64; the written theorem covers every positive n.
+
+At complete stationary primitive prices R,C, the supplied local bill is
+2 floor(n/2)R+2(n-1)C instead of 2(n-1)R+2(n-1)C. Common basis transport
+must be charged separately. No native prices or scalar-network optimum are
+claimed. The result gives no new kappa or selected-frontier change.
+
+## Reproduce and evidence
+
+From the repository root with CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/nilpotent-chain-reflection-compiler/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/nilpotent-chain-reflection-compiler/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/nilpotent-chain-reflection-compiler
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/nilpotent-chain-reflection-compiler --check-source-history
+```
+
+Substitute another CPython 3.12 interpreter elsewhere. Direct replay prints
+`PASS_NILPOTENT_CHAIN_REFLECTION_COMPILER` in a generated JSON receipt bound
+to the package-file hashes. Normal verification writes nothing. Registered
+normal and optimized modes use explicit checks that remain active under -O.
+
+The verifier checks 64 complete formal endpoints and their inverses, 2,048
+rank-one idempotent summands, and every primitive invoice. A separate literal
+bit-array interpreter checks all 87,380 two-address states at chain lengths
+1 through 8, another 21,504 states with two dirty spectators, and 52,083
+complete input columns across every involutory permutation on one through
+six addresses. This last domain contains 119 permutations, including identity
+actions as upper-bound controls. Literal checks compare against simultaneous
+updates of immutable original inputs, so an in-place ordering error is exposed.
+
+Separate complete two-call domains contain 784 ordered projector pairs on
+three roles and 14,400 on four roles. Each has exactly two witnesses for the
+new J_3 endpoint and no one-call witness. These small enumerations corroborate
+the construction; the universal minimum comes from the written rank/parity
+argument. All 84 single-primitive omissions at n=3 through 8 fail. Six invalid
+compiler boundaries, a noninvolutory address substitution and a wrong reflection
+role are rejected. No predecessor executable or census is imported or replayed.
+
+## Scope and provenance
+
+The `bit-new-register-model` card is changed to this constructive compiler side
+question. It does not satisfy the card's native-supplier admission gate.
+The prescribed current selected-baseline metadata command passed before work;
+that check is not a mathematical premise. Canonical base is
+7c49fe32c55de02c2c873655c804b16e4c3fef0a, priorities revision 8, selected PR6030
+with conditional kappa 0.003125804 and all five framework assumptions retained.
+[TASK.json](TASK.json) records the scope change and source diversity.
+[SOURCES.json](SOURCES.json) pins cited proof context as historical provenance;
+the verifier needs no predecessor input, Git, network or third-party package.
+
+The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19370175)
+followed live PR bodies, recent account submissions, handoffs, local reservations,
+all-main README searches and merged distinctive-term searches. The overlap
+helper's initial local coverage was 133 of 8,917 HEAD notes, so sparse no-match
+results were supplemented by full main-tree searches. Its complete remote
+pagination covered 506 open PR bodies at 09:05:30 UTC and 6,500 Discussion
+records at 09:06:46 UTC on November 3, 2026. Remote text snapshots,
+unpublished work and arbitrary historical diffs limit novelty coverage.
+
+Only the fixed-involution formal endpoint and the supplied primitive stream
+are settled. Several Jordan blocks, other paid labels, clean or discarded
+workspace, native reflection legality, complete routing/frame/basis/ownership,
+precision/tape/stock, recursive admission and the multiplication theorem remain
+outside scope. No selected cold scientific replay, Lean or Docker run is supplied.
+Independent human and formal proof-kernel review are unclaimed.
+
+## Open next questions
+
+- Determine the exact joint tariff for several nilpotent Jordan blocks. Start
+  with one specified partition and its rank/trace lower bound; independent
+  block compilation can leave parity or sharing opportunities. This proof
+  supplies no general minimum over all nilpotent matrices.
+- Bind one actual native caller to the two-edge stream. Price the coordinate
+  reflection, every scalar XOR, basis transport and all movement, ownership,
+  restoration, precision and stock obligations before drawing a supplier or
+  multiplication-bound consequence. Those native contracts remain unknown.
+
+## Credit and implementation limits
+
+Credit ywz65/PR2716 for the arbitrary-coupling interface, square-zero coefficient
+product and factorwise dirty lowering; Adam Gall/PR1911 and the retained
+eumemic/PR288, Ali Romman/PR468, woklerx/PR1443, Gareth Davidson/PR1333,
+Arham Tahir/PR1589 and Cinna Davis/PR2290 register-model lineage. Rank, trace,
+Jordan chains and elementary conjugation are classical. Nick Petalas/PR4912
+settles square-zero couplings, JoyboyBrian/PR5007 supplies a returned-clean
+compiler, and Nick Petalas/PR5857 optimizes that clean stream's scalar work.
+Their results and credits are retained. The new result is the non-square-zero
+single-chain compiler and its exact reflection tariff. Apache-2.0.
+
+Build the Lever led to the literal stream emitter and repeatable checker.
+Prove It Works led to full dirty-column execution and omission controls.
+Power of Ten bounds the emitter to 64 roles and the census to 87,380 main
+states, 21,504 spectator states, 720 candidate permutations per size and
+14,400 ordered projector pairs per case. Functions are below 60 physical
+lines; there is no recursion, subprocess, network or runtime code generation.
+The one-shot verifier reads at most one MiB per package file.
+
+Rule 3 has a managed-runtime deviation at compiler.py and verify.py: CPython
+allocates bounded lists, tuples and integers dynamically. There is no
+fixed-pool or steady-service claim. Live state is bounded by 64 role rows,
+at most 190 operation records and 120 four-role projectors; exhaustive input
+states are streamed. A fixed-storage runtime would require a separate port.
+Rule 9 has one fixed local import and standard sorting of the seven local
+file names; no unknown callback or dynamic target is accepted. Warning-strict
+normal and optimized execution provide interpreter diagnostics. No unavailable
+external static analyzer or formal kernel is claimed.

research/nilpotent-chain-reflection-compiler/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/dihedral-arbitrary-couplings/README.md",
+      "usage": "provenance",
+      "git_blob": "66027d2a8856d931e7b1c8fa9811a65196d01637",
+      "sha256": "17bc49fd6215c155aacb0e4a8ce4a8e33e83226b8a1b937a638256a39b99f8ee"
+    }
+  ]
+}