Prove exact mixed-target costs for binary semilinear groups

research/semilinear-mixed-tariff/PROOF.md

@@ -0,0 +1,172 @@
+# Mixed targets have no call sharing in prime-degree binary semilinear groups
+
+This is a scoped algebraic proof. It answers Nick Petalas's mixed-target
+question in PR #5202; his normal-C7 theorem, F8 representation and rank method
+retain their credit. Cinna Davis's PR #2011 supplies the order-21 model and
+earlier orbit census. Neither predecessor census is an assumption of the
+self-contained argument below. No physical supplier or new kappa is claimed.
+
+## Model and theorem
+
+Let p be an **odd prime**, F = F_(2^p), and
+
+    G_p = F^* semidirect C_p,
+    (a,j)(b,k) = (a b^(2^j), j+k mod p).
+
+Call a nonidentity element with j=0 **normal**, and an element with j!=0
+**outside**. At p=3 this is C7 semidirect C3 with the action in #2011/#5202.
+All nonidentity labels are allowed, at unit price.
+
+Work in Mat_r(F2[G_p]), for any finite r>=1. Every register starts arbitrarily
+dirty. A paid operation is
+
+    D_N(g) = I + N tensor ([g]+[1]),
+    g != 1,  N=x y^T over F2,  y^T x=1.
+
+Thus N is a rank-one idempotent. Arbitrary GL_r(F2) scalar maps may be
+interleaved freely. No other address operation, clean workspace, COPY or ERASE
+is free. The required endpoint is the **full formal operator**
+
+    T = diag([g_1],...,[g_r]).
+
+Let n be the number of normal targets, m the number of outside targets, and
+w=n+m. Identity targets designate restored dirty registers. Repeated target
+labels are permitted.
+
+**Theorem.** The minimum paid-call count is exactly w. If a word is optimal,
+then, after moving its free scalar maps to the right, it has exactly n normal
+calls and m outside calls. In every normalized normal call, both x and y are
+supported only on normal target roles. In every normalized outside call they
+are supported only on outside target roles. In particular, no normalized
+optimal paid factor touches a restored identity role, and the two target
+types never mix in a normalized optimal word.
+
+These support statements concern the normalized algebraic word. They do not
+claim that an implementation's interleaved free scalar maps avoid workspace.
+They also do not force coordinate projectors within either target class.
+
+## A constant-displacement representation
+
+On the p-dimensional binary vector space F, use
+
+    rho(a,j)(z) = a z^(2^j).
+
+This is a group representation by the displayed group law. For a!=1 and j=0,
+rho(a,0)-I is multiplication by a-1, so has binary rank p.
+
+For 0<j<p, a nonzero fixed point satisfies z^(2^j-1)=a^(-1). The standard
+Euclidean identity
+
+    gcd(2^j-1, 2^p-1) = 2^gcd(j,p)-1 = 1
+
+shows that this power map permutes the cyclic group F^*. There is exactly
+one nonzero fixed point, as well as zero. Hence rho(a,j)-I has a
+one-dimensional binary kernel and rank p-1. This uses primality of p.
+
+Choose a characteristic-two extension K containing a primitive p-th root of
+unity zeta. Such an extension exists because p is odd: p divides 2^(p-1)-1,
+and the multiplicative group of F_(2^(p-1)) is cyclic. Define the quotient
+character
+
+    chi(a,j) = zeta^j.
+
+Its displacement rank over K is zero on normal labels and one on outside
+labels. Extend the binary matrices rho to K and put R = rho direct-sum chi.
+Extension of scalars preserves the rank of a binary matrix. We obtain
+
+| label | rank(rho(g)-I) | rank(chi(g)-1) | rank(R(g)-I) |
+|---|---:|---:|---:|
+| identity | 0 | 0 | 0 |
+| normal | p | 0 | p |
+| outside | p-1 | 1 | p |
+
+The new quotient block makes the displacement rank **p for every paid
+label**, including the outside labels omitted from #5202's target theorem.
+Both representations extend linearly to the full group algebra. They need
+not be faithful as algebra maps: only necessary consequences of a formal
+endpoint are taken through them.
+
+## Free maps and the sharp lower bound
+
+For S in GL_r(F2),
+
+    S D_N(g) = D_(S N S^-1)(g) S.
+
+Conjugation preserves binary rank-one idempotence. Move all free scalar maps
+to the right. Augmentation [g] -> 1 sends every paid factor and T to I, so
+the remaining scalar product is I. We have a normalized paid-only word of
+the same length and the same labels.
+
+Under R, each paid factor A has
+
+    A-I = N tensor (R(g)-I),    rank(A-I)=p.
+
+The represented target has rank(R(T)-I)=p w. Rank subadditivity and
+
+    AB-I = (A-I)B + (B-I)
+
+give p w <= p L for a normalized word of L calls. Thus L>=w, with no
+restriction on r or on the number of restored dirty registers.
+
+Conversely, for each g_i!=1 apply D_(E_ii)(g_i). These w coordinate factors
+attain T **in the full formal algebra**, for every input in every role.
+The other roles are identically restored. This proves the exact minimum;
+equality merely in a representation is not used for attainment.
+
+Writing c_N,c_O for the two paid label counts, the separate representations
+also give
+
+    p c_N + (p-1)c_O >= p n + (p-1)m,
+    c_O >= m.
+
+At L=c_N+c_O=n+m the first inequality implies c_O<=m. Therefore c_O=m and
+c_N=n. At p=3 these are precisely the missing paired inequalities
+3c7+2c3>=3n+2m and c3>=m.
+
+## Rigidity of optimal normalized factors
+
+For any product A_1...A_L, telescoping from the right and from the left gives
+
+    col(A_1...A_L-I) <= sum_i col(A_i-I),
+    row(A_1...A_L-I) <= sum_i row(A_i-I).
+
+Here <= means subspace inclusion. For example, the first follows from
+the expansion sum_i (A_i-I) A_(i+1)...A_L; the second follows from
+sum_i A_1...A_(i-1)(A_i-I). If the word is optimal, the left side has
+dimension pL, while the sum of the individual dimensions on the right is
+also pL. Consequently both inclusions are equalities, and **each** factor's
+column and row spaces lie inside the corresponding target spaces.
+
+Project the column containment to one register role t. For a factor with
+N=x y^T and x_t=1, the projected column space is col(R(g)-I). The target's
+space in that role is col(R(g_t)-I). The identity target has zero space,
+so x_t must be zero there. A normal call has full dimension p in the rho
+block and zero in the chi block. It cannot fit inside an outside target's
+(p-1)-dimensional rho image. An outside call has a nonzero chi image, so
+cannot fit inside a normal target's zero chi block. Thus x has the stated
+type support. Applying the identical argument to row spaces and y proves
+the corresponding assertion for y. This proves the rigidity statement.
+
+## Boundary, credit and verification
+
+The p=3 all-normal case is already #5202's theorem. The additions are all
+mixed/outside target lists, the normalized optimal-factor support theorem,
+and the odd-prime-degree family. The proof above includes the inherited
+representation/rank steps to be readable without an unmerged dependency.
+The exact checks are finite corroboration, not a proof of universal quantifiers
+or independent human acceptance. Elementary finite-field facts and ordinary
+rank algebra are used explicitly, with no numerical or asymptotic premise.
+
+The prime-degree and odd-characteristic-order hypotheses are used at the two
+specified steps. No conclusion for composite degrees or p=2 follows from
+this argument. Nonuniform label prices, restricted alphabets, higher-rank
+paid factors, non-diagonal targets and extra free address maps have different
+boundaries. Native realization, ownership, routing, restoration implementation,
+precision, hosting, stock/compiler and full recursive/outer costs are unpriced.
+The theorem supplies no physical supplier or complete multiplication theorem.
+
+Predecessors: Nick Petalas, PR #5202 at
+`99ed6d2fc13101cb5ec0d3b1cdc826b75bc27fc7`; Cinna Davis / 1337isnot1337,
+PR #2011 at `b971a6c68d6f60c2693b2057ecf3489efb75efc4` and PR #3893;
+eumemic / #288 and the retained register-model lineage. Prepared by
+Krzysztof Wojt with substantial OpenAI Codex assistance. Apache-2.0.

research/semilinear-mixed-tariff/README.md

@@ -0,0 +1,128 @@
+# Exact mixed-target tariff for binary semilinear groups
+
+**Scoped written proof, with exact finite corroboration; no new kappa.**
+For every odd prime p, in the full formal algebra
+`F2[C_(2^p-1) semidirect C_p]` with Frobenius action, any diagonal target
+with w nonidentity entries needs **exactly w** unit-price rank-one idempotent
+calls. The theorem allows arbitrary finite restored dirty workspace and free
+binary scalar mixing. Repeated labels and arbitrary mixtures of normal and
+outside labels are included.
+
+At p=3 this answers the mixed-target question explicitly left open by
+[Nick Petalas's PR #5202](https://github.com/CrocSwap/integer-mult-bounds/pull/5202).
+His all-normal tariff and F8 rank representation retain their credit;
+[Cinna Davis's #2011](https://github.com/CrocSwap/integer-mult-bounds/pull/2011)
+retains the group/model and three-role orbit census. These earlier results are
+not repeated as the contribution.
+
+The new quotient character supplies the missing outside-call budget. Its
+sum with the natural representation has displacement rank p for **every**
+nonidentity group element. Rank telescoping gives the lower bound, while w
+coordinate calls attain the full formal endpoint. [PROOF.md](PROOF.md) gives
+all quantifiers and the proof without an unmerged code dependency.
+
+There is also an equality theorem: after scalar normalization, an optimal
+word has exactly as many normal/outside calls as the respective target counts.
+Both vectors of every paid rank-one projector stay within its own target type.
+No normalized optimal paid factor touches an identity-target dirty register.
+Interleaved free maps themselves may use workspace; within-type noncoordinate
+projectors are allowed and have a checked positive example.
+
+## Scope and evidence
+
+| Check | Exact finite coverage |
+|---|---|
+| Natural plus character representation | Every label at p=3,5,7: 21,155,889 labels |
+| Representation multiplication | All 441 and 24,025 ordered pairs at p=3,5; 3,556 left/right generator pairs at p=7 |
+| Paid displacement ranks | All 6 two-role idempotents for each nonidentity label: 6,372 matrices over finite fields |
+| Free scalar normalization | All 168 GL3(F2) maps and 28 idempotents: 4,704 covariances |
+| Separate full formal checker | All 14,400 two-role and 313,600 three-role ordered two-call words, without rank-based pruning |
+| Literal endpoints in that census | All 1,600 two-target endpoints attained; 672 are mixed-type; no support-rigidity violations |
+| Arbitrary-dirty regular action | Four mixed calls on five registers, surrounded by dense inverse scalar maps: all 105 basis inputs match and all 21 dirty-role basis inputs restore; a changed label gives 21 mismatches |
+| Hypothesis and corruption controls | Omitted representation blocks, rank-two paid gate, missing outside budget, composite degree, p=2 character, wrong group law, omitted formal terms, forbidden support and wrong target |
+
+The universal statements rest on the written proof, not on extrapolation from
+these dimensions. `small_words.py` was implemented separately by a supporting
+Luna agent, then inspected and run by the primary agent. It compares complete
+formal coefficients rather than represented ranks. This is AI-assisted
+corroboration, not independent human or proof-kernel review.
+
+The composite-degree fixture checks that Frobenius cubed on F512 has natural
+displacement rank 6, so adding one character gives 7, not 9. It invalidates
+that extension of this proof; it does **not** disprove the tariff for composite
+degrees. The p=2 control similarly tests the missing character hypothesis.
+
+## Reproduce
+
+CPython 3.12, standard library only, from the repository root:
+
+```sh
+python3.12 -I -W error -B research/semilinear-mixed-tariff/verify.py
+python3.12 -I -O -W error -B research/semilinear-mixed-tariff/verify.py
+python3.12 -B scripts/research_package.py --package research/semilinear-mixed-tariff
+python3.12 -B scripts/check_research_commit.py --package research/semilinear-mixed-tariff --check-source-history
+```
+
+The direct verifier prints `PASS_SEMILINEAR_MIXED_TARIFF`, exact coverage and
+fresh SHA256 values for every package file. It does not write artifacts, fetch
+sources or require Git. The registered commands additionally authenticate the
+package's historical provenance. Each command has a 60-second timeout; local
+direct runtime is about one second. Committed-package export and a Git-free
+read-only replay are separate publication checks, reported in the PR.
+
+## Value, coordination and boundaries
+
+Scientific base: canonical main `ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c`,
+priority revision 7. [Canonical investigation #5230](https://github.com/CrocSwap/integer-mult-bounds/discussions/5230)
+and [handoff pointer](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19146275)
+record the claim. This changes `bit-new-register-model` to the explicitly open
+mixed-target algebraic question. The result rules out call sharing throughout
+this formal family before any physical implementation is proposed.
+
+Before claim, the overlap scan covered 344 open PRs, 4,466 closed PRs, 4,453
+Discussion records and 6,996 main notes, with complete pagination; live open
+PR bodies and recent handoffs were checked again. Exact #2011 and #5202 heads
+were read. Recent krzysztofwojt scopes, including #5204 and the active
+fifteen-owner six-cycle investigation, were excluded. Related #5199, #5203
+and #5205 concern other groups/alphabets/targets. No conflicting mixed
+semilinear tariff appeared. Historical diffs and unpublished work remain
+coverage limits; the final live refresh is recorded in the PR.
+
+The price is one per arbitrary nonidentity label, not a physical recursive
+cost. Native realization, ownership, routing, restoration implementation,
+frames/hosting, precision, stock/compiler and full recursive/outer costs are
+**unknown** here. No native supplier, complete multiplication theorem, new
+kappa or selected-frontier change is claimed. No Lean, Docker, selected cold
+replay or predecessor census was run. The family is closed at this formal
+unit-price question; physical expansion would require a new contract and bill.
+
+## Open next questions
+
+1. What is the sharp tariff when normal and outside calls have different
+   positive prices? Begin with two normal order-21 targets and test whether
+   three outside calls can attain them; the paired rank inequalities permit
+   that count but do not supply a word. This could distinguish algebraic
+   count optimality from an actual priced interface. The nonuniform full
+   formal optimum and physical prices remain unknown.
+2. Does a constant-displacement certificate, or a genuine sharing word, exist
+   at an odd composite degree? Start at degree nine with the order-three
+   Frobenius elements exposed by the boundary control. The present single
+   character no longer equalizes ranks. No such extension is claimed or reserved.
+
+## Credit and exact sources
+
+- **Nick Petalas, #5202**, head `99ed6d2fc13101cb5ec0d3b1cdc826b75bc27fc7`:
+  normal-C7 theorem, natural rank budget, free-scalar normalization and the
+  explicit mixed-target handoff. Its `PROOF.md` SHA256 is
+  `7bd232212ba6359533ec333c36b781c7aba84490fa246c349ad5a3a510bb5d47`.
+  This is a citation, not a runtime input; the new proof is self-contained.
+- **Cinna Davis / 1337isnot1337, #2011**, head
+  `b971a6c68d6f60c2693b2057ecf3489efb75efc4`: order-21 model and prior orbit
+  census. Its retained main README is pinned as provenance in `SOURCES.json`.
+- **Cinna Davis, #3893**, the S3 representation-rank precedent; **eumemic,
+  #288**, and the retained register-model lineage.
+
+Prepared by **Krzysztof Wojt with substantial OpenAI Codex assistance**,
+including bounded Luna overlap inventory and an independently implemented
+finite checker, inspected and integrated by the primary agent. Apache-2.0.
+No independent human or formal proof-kernel review is claimed.

research/semilinear-mixed-tariff/SOURCES.json

@@ -0,0 +1,24 @@
+{
+  "schema_version": 1,
+  "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/bit-semidir21-orbit-seed8f89/README.md",
+      "usage": "provenance",
+      "git_blob": "13e399921e5dd556a7ce8645362ffb5d550b5e75",
+      "sha256": "534422d3f152b0f1e4a8357056036d1629b0aee75e58301c7436f5b723260eb0"
+    }
+  ]
+}