Prove exact monomial-reflection tariffs with dirty workspace (no κ)

research/monomial-reflection-tariff/PROOF.md

@@ -0,0 +1,159 @@
+# A full monomial reflection alphabet has an additive register tariff
+
+## Exact model
+
+Let K be a field with an element zeta of exact finite order m, and let n>=1.
+Write G=G(m,1,n) for the monomial matrices with nonzero entries in <zeta>.
+The notation also covers m=1. Encode an element g=(p,a) by
+
+    g e_j = zeta^(a_j) e_(p(j)),     a_j in Z/mZ.
+
+Let b(g) count the cycles C of p for which sum_(j in C) a_j=0 mod m.
+These are the balanced cycles, including balanced fixed coordinates.
+The ordinary reflection-length formula n-b(g) is classical; see
+[Jian-yi Shi](https://www.sciencedirect.com/science/article/pii/S0021869307003882) and
+[Briana Foster-Greenwood, Section 3](https://arxiv.org/html/1202.0266v1#S3). Section 2 gives
+its elementary construction here, so no external classification is needed.
+
+Use the full formal group algebra K[G], with R>=W finite register roles.
+All inputs are arbitrary. Free scalar operations are GL_R(K) matrices.
+A paid unit operation is
+
+    D_N(t) = I + ([t]-[e]) N,
+    rank_K(N)=1, N^2=N, rank_K(t-I)=1, t in G.
+
+The address alphabet is every monomial reflection, not just adjacent swaps.
+It consists exactly of:
+
+- a phase multiplication zeta^a on one coordinate, a!=0 mod m;
+- a swap of coordinates i,j with phases zeta^a,zeta^(-a).
+
+Indeed, Section 1 shows that displacement rank one allows either one
+unbalanced singleton, or one balanced two-cycle, with every other coordinate
+balanced and fixed. Phase operations may have order greater than two.
+The inverse of each operation is in the same paid alphabet. Idempotence
+also gives D_N(t)^(-1)=D_N(t^(-1)), so all paid factors are invertible.
+
+The required complete endpoint is
+
+    F = diag([g_1],...,[g_W],[e],...,[e]) in M_R(K[G]).
+
+Every spectator is restored, and every off-diagonal entry vanishes. Scalar
+preparation and restoration are free only in this explicit optimistic model.
+Every address operation, including undoing one, is counted. No address map,
+reset, erasure, or clean state is free.
+
+**Theorem.** The minimum paid-call count is
+
+    sum_(j=1)^W (n-b(g_j)),
+
+for every finite number of arbitrary restored dirty spectators. Identity
+and empty target lists are allowed. A common positive unit price multiplies
+the formula. This is a scoped formal-algebra theorem, not a native supplier.
+
+## 1. Displacement rank and the lower bound
+
+On a permutation cycle, a fixed vector satisfies
+
+    x_(p(j)) = zeta^(a_j) x_j.
+
+After one circuit this gives x_j=zeta^(sum a) x_j. The fixed space on that
+cycle has dimension one exactly when the cycle is balanced, and zero
+otherwise. Distinct cycles use independent coordinates. Hence
+
+    rank_K(g-I)=n-b(g).
+
+This proof also covers characteristic two when the stated roots exist.
+No real ordering, semisimplicity, or division by |G| is used.
+
+We use the augmentation normalization and displacement-rank method of
+Gareth Davidson's PR1333. They are prior methods, not new principles here.
+Augmentation sends every [g] to 1 and every D_N(t) to I. It sends F to I.
+Move every scalar basis change to the right of the chronological product.
+Conjugation only replaces N by B N B^(-1), still a rank-one idempotent.
+The remaining scalar product is I by augmentation. Therefore the endpoint
+has a normalized factorization entirely into paid factors of the same count.
+
+Apply the natural monomial representation to the group algebra. A normalized
+paid factor becomes
+
+    I + N tensor (t-I).
+
+Its difference from I has rank exactly one, by the rank formula for a
+Kronecker product. For invertible A,B, the elementary identity
+
+    AB-I = A(B-I)+(A-I)
+
+gives rank(AB-I)<=rank(A-I)+rank(B-I). The represented diagonal endpoint
+has displacement rank sum_j rank(g_j-I), since its blocks are independent
+and its spectators have zero displacement. Iterating the inequality proves
+the claimed lower bound for every R. Scalar mixing and dirty helpers do not
+remove any term from it.
+
+The natural representation is only a necessary lower-bound image. Equality
+in that image is never used to certify a formal endpoint. For example, when
+m=3,n=2 over C, the nonzero group-algebra norm sum_(g in G)[g] maps to zero:
+for each possible nonzero matrix position its three phases sum to zero.
+An off-diagonal norm leak is still a dirty leak in the formal model.
+
+## 2. An attaining cycle splitter
+
+Use composition g h = g after h. Start with a cycle containing i and
+j=p(i), with j!=i. Right multiply by the weighted swap t defined by
+
+    t e_i = zeta^(a_i) e_j,
+    t e_j = zeta^(-a_i) e_i.
+
+Then
+
+    (g t)e_j = e_j,
+    (g t)e_i = zeta^(a_i+a_j) e_(p(j)).
+
+Thus j becomes a balanced singleton and the old cycle loses one coordinate,
+while its total phase is unchanged. Repeating on an original cycle of length
+ell takes ell-1 weighted swaps and leaves one singleton carrying that cycle's
+phase. A balanced cycle is now fully fixed. An unbalanced cycle needs exactly
+one diagonal phase operation, its inverse phase, to reach the identity.
+The number of right peels is ell-1 or ell respectively, hence n-b(g) in total.
+
+If g t_1 ... t_L=e, then
+
+    g=t_L^(-1) ... t_1^(-1).
+
+Execute t_1^(-1),...,t_L^(-1) chronologically on one coordinate register.
+The full formal product is [g]. This uses no scalar mixing or spectator.
+For several targets, concatenate their independent coordinate-register
+words. The full endpoint is F in K[G], with exactly the lower-bound bill.
+This proves simultaneous attainment and the theorem.
+
+## 3. First new example and interpretation
+
+Take m=3,n=2 and g e_0=zeta e_1, g e_1=e_0. Its only cycle is unbalanced,
+so it costs two paid reflections. The two-register endpoint diag([g],[g^-1])
+costs exactly four with any finite restored dirty workspace. The splitter
+uses one phase-weighted swap and one phase operation per target. The inverse
+phase operations are paid units too. This is an address alphabet absent from
+the simple-reflection Coxeter model, and its scalar field contains a genuine
+third root of unity.
+
+Allowing all nonadjacent phase-weighted swaps and higher-order phases does
+not create a sharing saving under this unit-reflection invoice. A productive
+escape must change a further hypothesis, for example give selected higher-rank
+operations a concave price, or supply a different free-operation boundary.
+This conclusion does not exclude those changed models.
+
+## 4. Proof and certificate boundaries
+
+The all-parameter conclusion is the written argument above. The finite
+verifier independently enumerates small groups, runs an unpruned Cayley
+search, computes displacement ranks, and checks the new splitter's words.
+Its complete rational group-algebra fixtures mix a dirty spectator through
+oblique projectors, check all off-diagonal entries, and run the literal
+inverse. They do not enumerate all register circuits; the lower-bound proof
+covers those.
+
+No native address implementation, scalar/routing/storage cost, child-rank
+moment, compiler/hosting admission, precision/tape bound, new kappa, or
+complete multiplication theorem is supplied. Independent human and formal
+proof-kernel review are unclaimed. The selected frontier and its five
+framework assumptions are unchanged.

research/monomial-reflection-tariff/README.md

@@ -0,0 +1,127 @@
+# Exact tariffs for full monomial reflection words
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+**Claim type: scoped written proof with exact finite corroboration.**
+For G(m,1,n), allow every monomial rank-one reflection as a unit paid call,
+including nonadjacent phase-weighted swaps and higher-order phase operations.
+For arbitrary diagonal targets g_j, free scalar mixing, and any finite number
+of restored arbitrary dirty registers, the exact minimum count is
+
+    sum_j (n - b(g_j)),
+
+where b(g) counts permutation cycles whose accumulated phase is one. The
+coefficient field may be any field containing an element of exact order m.
+Every target has a constructive attaining word, with no helper or scalar
+preparation. [PROOF.md](PROOF.md) gives the full model and proof.
+
+For example, with a primitive third root zeta, the two-coordinate map
+`g e_0=zeta e_1, g e_1=e_0` has one unbalanced cycle. The endpoint
+`diag([g],[g^-1])` costs exactly four calls, regardless of the number of
+restored dirty spectators. Both phase and swap calls are charged.
+
+The new contribution is this register-model tariff for a changed alphabet.
+The ordinary reflection-length formula is classical, including
+[Jian-yi Shi's formula](https://www.sciencedirect.com/science/article/pii/S0021869307003882)
+and [Briana Foster-Greenwood's length/codimension treatment](https://arxiv.org/html/1202.0266v1#S3).
+The proof restates the elementary cycle construction and uses the established
+augmentation/displacement-rank method. No new reflection-length principle
+or literature-wide priority is claimed.
+
+## Evidence and reproduction
+
+The standalone checker imports no predecessor executable and writes only to
+standard output. Its generated receipt binds every package file by SHA256.
+The fixed finite domains are G(1,1,4), G(2,1,4), G(3,1,3), G(3,1,4),
+G(4,1,3), G(5,1,3) and G(6,1,3).
+
+- An unpruned Cayley search visits all 4,944 group elements and 130,344
+  directed transitions. Every distance equals n-b(g). Every constructed
+  word has that length and the exact formal group label. Separate dense
+  finite-field multiplication and displacement ranks agree, using primitive
+  roots over F5, F7 or F11.
+- All 324 ordered G(3,1,2) target pairs have complete rational group-algebra
+  endpoints and inverse restoration with a genuinely mixed dirty spectator.
+  The fixtures contain 972 paid events. Each of the 323 nonempty words fails
+  when its first call is omitted. No basis-only endpoint test is used.
+- Controls distinguish an unbalanced cycle, chronological order, a nonprimitive
+  root and a formal dirty leak that vanishes in the natural representation.
+  The nonzero eighteen-term group norm is retained by the formal oracle.
+
+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/monomial-reflection-tariff/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/monomial-reflection-tariff/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/monomial-reflection-tariff
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/monomial-reflection-tariff --check-source-history
+```
+
+Other hosts may substitute their CPython 3.12 executable. Expected markers
+are `PASS_MONOMIAL_REFLECTION_TARIFF`, `PASS_REGISTERED_RESEARCH_PACKAGE`
+and `PASS_RESEARCH_COMMIT_BYTES`. Both registered commands run the same
+finite coverage in normal and optimized Python. Each has a 60-second limit.
+The written proof supplies the universal conclusion; the finite cases
+corroborate it. No receipt is handwritten or regenerated during verification.
+
+## Sources, overlap and limits
+
+The source question is David Arias / DavidAriasC's
+[PR2738](https://github.com/CrocSwap/integer-mult-bounds/pull/2738),
+Open next question 2. That theorem covers simple Coxeter generators. This
+package changes the paid alphabet to all monomial reflections, including
+operations of order greater than two. Gareth Davidson / bitplane's
+[PR1333](https://github.com/CrocSwap/integer-mult-bounds/pull/1333)
+supplies augmentation normalization and the displacement-rank method,
+retaining eumemic, Ali Romman / PR468, David Govea / PR720 and their credited
+register-model lineage. Adam Gall and Ross Richardson's cut-method lineage
+remains credited by PR2738. These results are cited, not audited or replayed.
+
+Scientific base is canonical main
+`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8, selected
+PR6030. [SOURCES.json](SOURCES.json) pins the question and method statements.
+[TASK.json](TASK.json) records the changed card scope. The
+[advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19373434)
+precedes the computation. Source-binding orientation passed. Cached overlap
+covered 556 open PRs and 6,600 Discussion records with complete pagination;
+only 123 local notes were materialized against 8,917 HEAD note paths.
+Targeted all-main general-form searches and merged-PR searches supplement
+that sparse local coverage. Arbitrary diffs and unpublished work are limits.
+
+This closes a sharing route within an optimistic unit-reflection model.
+It does not price higher-rank calls concavely, classify nonuniform generator
+prices, or implement a native address instruction. Scalar work, routing,
+ownership, storage, precision, stock, tape, hosting, complete recursive
+invoices and outer use remain separate obligations. No supplier admission,
+new kappa, selected-frontier change or complete multiplication theorem is
+claimed. All five selected framework assumptions remain. Independent human
+and formal proof-kernel review are unclaimed. Lean, Docker, predecessor
+scientific replays and selected cold replay were not run.
+
+## Verifier bounds
+
+There is no recursion, network, subprocess, dynamic code or external callback.
+Each fixed search has at most 1,944 group states and 33 generators. Matrix
+rank checks have at most four rows. Formal fixtures have three registers,
+eighteen possible group labels and rational coefficients. Every loop is
+bounded by these fixed domains or by the finite collection it reads.
+Every function is shorter than 60 physical lines. Explicit exceptions keep
+checks active under optimized Python; warning-strict normal and optimized
+execution are the available diagnostics. No separate static analyzer is
+installed. Source reads authenticate the two fixed predecessor text inputs.
+
+Power-of-ten rule 3 deviation: Python allocates tuples, integers, fractions,
+sets and dictionaries dynamically. The fixed domains above bound live data;
+Python offers no static allocation guarantee. A larger externally supplied
+search is outside the executable contract. No repository-wide build settings
+or predecessor code are changed.
+
+## Open next questions
+
+Can selected higher-rank monomial calls with concave prices beat this
+unit-reflection invoice after their native implementation costs are included?
+This changes the price contract and may admit sharing. Start with one
+explicit primitive and complete formal endpoint, then compare its full
+boundary bill. The present rank-one proof does not charge such a primitive
+one unit or establish physical profitability. Without that changed contract,
+further dirty-workspace searches in this alphabet are unnecessary.

research/monomial-reflection-tariff/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "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/binary-affine-register-bound/PROOF.md",
+      "usage": "input",
+      "git_blob": "b1152a39b559f7a058489ec74231488e4f8edd83",
+      "sha256": "36a33434222798434b0a17476ae5f9bc8a2a3891871c46e77cc50ce2e132206b"
+    },
+    {
+      "path": "research/coxeter-root-tariff/README.md",
+      "usage": "input",
+      "git_blob": "9ed141d29e7f552d9cbc9c0f499b4dc901bdee13",
+      "sha256": "e8ad34f2926dadd897d2f9c6ee7295ecc61cfa13c776ab1c6ea5be82fdc1fa93"
+    }
+  ]
+}