Prove vector-cocycle call floors beyond scalar characters (no κ)

research/vector-cocycle-rank-floor/PROOF.md

@@ -0,0 +1,183 @@
+# A rectangular cocycle rank floor
+
+## Formal boundary
+
+Let F be a field, G a group, V an F-vector space of finite positive
+dimension d, and R:G -> GL(V) a representation. Suppose c:G -> V is a
+crossed homomorphism, with convention
+
+```text
+c(gh) = c(g) + R(g)c(h).
+```
+
+Use the full formal group algebra F[G]. A register word has r finite
+scalar roles. Its paid factors are
+
+```text
+D_N(g) = I_r + ([g]-[1])N,
+N = xy^T in M_r(F), y^T x = 1.
+```
+
+Every input is arbitrary. Any declared dirty role must have its required
+full formal identity output, including all off-diagonal coefficients.
+Constant GL_r(F) matrices may be interspersed at no formal paid-call cost.
+No physical realization or price for those free matrices is asserted.
+
+This is the rank-one idempotent register convention of Cinna Davis's
+PR2116/2047/2248/2085 and Sagar Thakrar's PR4032. The new lemma uses a
+vector-valued affine representation in place of a scalar twisted functional.
+Nick Petalas's PR4898 supplies an earlier specific first-order instance;
+neither that instance nor the predecessor results are replayed here.
+Nick Petalas's PR6008 supplies the general full-operator representation
+rank cut. The charge here uses a common rectangular block, whose per-call
+rank is one even when the full operator defect has rank greater than one.
+This is a changed invariant, rather than substitution of another group
+into that full-operator cut.
+
+## Theorem
+
+For T in M_r(F[G]), define the rectangular matrix Delta_c(T) in
+M_(rd,r)(F) by replacing entry `sum_g a_ij,g [g]` with the d-by-1 column
+`sum_g a_ij,g c(g)`. If a register word equals T, then
+
+```text
+rank_F Delta_c(T) <= number of its paid calls with c(g) != 0.
+```
+
+The same statement holds with a call of projector rank k charged k units
+when c(g) is nonzero. In the rank-one alphabet, for a full diagonal target
+`diag([t_1],...,[t_w],1,...,1)`, the number of calls outside ker(c) is at
+least `#{i : c(t_i) != 0}`. The bound is independent of the number of
+restored dirty roles.
+
+### Proof
+
+The cocycle identity makes
+
+```text
+rho(g) = [ R(g)  c(g) ]
+         [   0      1 ]
+```
+
+a group representation, so it extends linearly to an algebra map on
+F[G]. Apply it entrywise and reorder the coordinates by putting all V
+coordinates first and all final scalar coordinates last. The resulting
+algebra map has the form
+
+```text
+rho_r(T) = [ A(T)  Delta_c(T) ]
+           [   0    eps(T)   ],
+```
+
+where eps is entrywise augmentation. Therefore
+
+```text
+Delta_c(UW) = A(U) Delta_c(W) + Delta_c(U) eps(W).
+rank Delta_c(UW) <= rank Delta_c(U) + rank Delta_c(W).
+```
+
+This uses only the rank inequalities for a sum and a product. In
+particular no simultaneous diagonalization or scalar character is needed.
+
+The cocycle identity at the identity gives c(1)=0. For a paid factor,
+
+```text
+Delta_c(D_N(g)) = N tensor c(g).
+```
+
+Its rank is one if c(g) is nonzero and zero otherwise. For the stated
+higher-rank variant it is rank(N) if c(g) is nonzero. The factor is legal
+and invertible since its inverse is D_N(g^-1), using N^2=N. Its upper
+block is `(I-N) tensor I_d + N tensor R(g)` and its lower block is I_r.
+
+A constant scalar matrix S has blocks S tensor I_d and S, with zero
+rectangular block. It contributes no rank charge. Iterating the product
+inequality proves the assertion even with interspersed free scalar mixing.
+
+For the diagonal target, column i of Delta is c(t_i) supported in its own
+V block. Distinct nonzero columns are independent because those blocks
+are disjoint. Identity spectator outputs give zero columns and rows.
+This proves the diagonal statement for every finite r. QED.
+
+The bound is necessary, not sufficient. A nonidentity element in ker(c)
+can have a nonidentity rho image with zero rectangular block. The full
+formal endpoint, rather than this representation alone, remains the
+correct acceptance condition for a construction.
+
+## Normal p-subgroup extension
+
+Let P be a finite p-group, H any group acting on P, and G=P semidirect H.
+Let Phi(P)=P^p[P,P] be the Frattini subgroup. Then V=P/Phi(P) is a finite
+Fp-vector space. H acts linearly on V because Phi(P) is characteristic.
+For the unique expression g=ph, set
+
+```text
+R(ph) = action of h on V,
+c(ph) = image of p in V.
+```
+
+Indeed `(ph)(qk) = p(hqh^-1)hk`, and taking the Frattini quotient gives
+the crossed homomorphism identity. The theorem applies over Fp, or after
+extending scalars to any field of characteristic p. Consequently every
+diagonal target label with nonzero Frattini component forces one call
+whose normal component also survives that quotient.
+
+There is no hypothesis on the order or commutativity of H, and no
+one-dimensional equivariant functional on V is required. This answers
+the existence of a vector-valued rank floor in PR4032's Open next
+question 2. It does not assert that every particular scalar-character
+floor, equality classification or shortest-word theorem extends. Elements
+of Phi(P), including central defects killed by that quotient, are not
+detected. For a nonsplit extension an appropriate cocycle would need to
+be supplied separately.
+
+## A sharp family invisible to abelianization
+
+Let p be any prime, d>=2, V=Fp^d and
+`G = V semidirect SL_d(Fp)`, with the natural action. Write its elements
+as (v,h), so multiplication is `(v,h)(w,k)=(v+hw,hk)`. The cocycle is
+c(v,h)=v and the representation is R(v,h)=h.
+
+Give every nonidentity group label unit paid-call price in the formal
+rank-one alphabet. For any nonzero vectors v_1,...,v_w and every finite
+r>=w, the full endpoint
+
+```text
+diag([(v_1,I)],...,[(v_w,I)],1,...,1)
+```
+
+has exact minimum w paid calls. The theorem gives the lower bound w,
+including arbitrary restored dirty workspace and free scalar mixing.
+The w coordinate projectors give the upper bound, with the exact full
+formal endpoint and no cross-role entries.
+
+Nevertheless every homomorphism from G to an abelian group kills all
+translations. To prove this, for i!=j use h=I+E_ij in SL_d(Fp) and the
+translation by e_j. With `[a,b]=aba^-1b^-1`, their commutator is the
+translation by `(h-I)e_j=e_i`. All translations are products of these
+basis translations. Thus V is contained in [G,G], and every abelian
+quotient sends the whole target to identity. In particular ordinary
+one-dimensional group characters cannot supply this nonzero target
+defect. This statement does not exclude other representation-theoretic
+lower bounds.
+
+The finite example uses p=3,d=2. Its complement is nonabelian and has
+order 24, divisible by 3. Thus the example actually exercises the
+removed complement-order restriction. The written proof establishes the
+family; finite checks are corroboration on this single group only.
+
+Affine representations of cocycles, Frattini quotients, elementary
+commutators and rank subadditivity are classical. No literature-wide
+priority is claimed. The contribution here is their rectangular-block
+register-word application and the stated scope extension of the
+predecessor first-order method.
+
+## Obligations outside this proof
+
+These are formal algebraic call counts. Native address operators, scalar
+basis conversion, permitted sources, ownership and erasure, chronology,
+restoration costs, hosting, precision/tape, compiler closure, recursive
+funding and the outer multiplication theorem are not provided. The
+selected result and its five framework assumptions are unchanged. The
+written proof has no claimed formal proof-kernel or independent human
+acceptance.

research/vector-cocycle-rank-floor/README.md

@@ -0,0 +1,142 @@
+# Vector-valued cocycle floors for formal register words
+
+For any finite-dimensional representation R of a group G over a field F
+and crossed homomorphism `c(gh)=c(g)+R(g)c(h)`, every formal rank-one
+register word realizing T obeys
+
+```text
+number of calls with c(g)!=0 >= rank_F Delta_c(T).
+```
+
+Delta replaces each formal group-algebra entry with its c-weighted vector
+column. A diagonal target forces one such call for every nonzero target
+column, even with arbitrary finite restored dirty workspace and free
+constant scalar mixing. [PROOF.md](PROOF.md) proves the statement and its
+extension to every split normal p-subgroup via its Frattini quotient.
+The complement can be nonabelian and have order divisible by p.
+
+The new step is the rectangular block of the affine cocycle representation.
+It removes the need for a scalar twisted functional in Sagar Thakrar's
+[PR4032](https://github.com/CrocSwap/integer-mult-bounds/pull/4032), Open next
+question 2. The existing A4 and SL2(F3) results are cited and credited;
+their checkers and searches are not run. This is a scoped algebraic proof
+with finite exact corroboration, with no new kappa or selected-frontier change.
+
+For `G=Fp^d semidirect SL_d(Fp)`, d>=2, w nonzero translation targets have
+exact formal paid-call minimum w at every finite dirty-workspace size.
+Every abelian quotient kills all those translations, so ordinary group
+abelianization sees no target defect. The general proof uses elementary
+transvection commutators. The finite example is F3^2 semidirect SL2(F3),
+whose complement is nonabelian and has order divisible by the characteristic.
+
+## Reproduce
+
+From the repository root, use CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/vector-cocycle-rank-floor/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/vector-cocycle-rank-floor/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/vector-cocycle-rank-floor
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/vector-cocycle-rank-floor --check-source-history
+```
+
+Any installed CPython 3.12 may replace the interpreter path. The expected
+markers are `PASS_VECTOR_COCYCLE_RANK_FLOOR` and
+`PASS_REGISTERED_RESEARCH_PACKAGE`. The standalone check needs neither Git
+nor a network. Its stdout receipt is generated from exact computations and
+SHA256 hashes of all six package files. `--emit /absolute/new/file.json`
+writes that receipt with exclusive creation and refuses an existing path.
+No generated output is required or retained in this package.
+
+The verifier enumerates the finite group's affine/cocycle identities, every
+rank-one idempotent on one through three F3 roles and every group label.
+It compares formal group-algebra products with their affine images for a
+declared deterministic sample of words with interspersed invertible scalar
+mixing on two through five roles. It
+checks all nonzero translation-target lists of length at most three with
+two restored dirty roles, using exact full formal endpoints. Two explicit
+commutators establish the finite translation basis. Semantic controls cover
+the ignored module action, invalid nilpotent and rank-two projectors,
+zero-cocycle replacement, reversed order, an omitted target, and the
+nonidentity kernel. This is not an exhaustive word census or a formal
+proof of the quantified theorem.
+
+Both local modes pass 46,656 group pairs, 28,080 call images, 252 prefixes
+of 72 sampled words, and 584 sharp full formal target lists. The projector
+counts on one, two and three roles are 1, 12 and 117. Thirty-five sampled
+words have strict slack in the rank inequality; no characterization of all
+strict cases is claimed. Each direct command takes about 2.4 seconds
+locally, comfortably below its registered two-minute limit.
+
+## Scope and credit
+
+Canonical scientific base is `7c49fe32c55de02c2c873655c804b16e4c3fef0a`,
+priority revision 8, selected PR6030. The selected binding control passed.
+The task is a declared change from the formal-interface card to a written
+formal-model lemma. It is a side result for the portfolio of changed
+interfaces, without a claim to discharge a selected framework assumption.
+
+[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19360783).
+Entry overlap checks included live open PRs, this account's recent PRs,
+recent handoff comments, active Discussions, local reservations, main-tree
+README searches and merged searches for radical rank, cocycles, Frattini
+quotients and nonabelian complements. The cached helper reported complete
+main-note inventory and remote pagination, with its own freshness times.
+Arbitrary diffs, unpublished work and historical text outside those searches
+remain outside coverage; this is not a literature novelty certificate.
+
+Credit Sagar Thakrar / thakrarsagar PR4032 for the twisted radical-rank
+method and its normal-subgroup extension question; Cinna Davis
+PR2116/2047/2248/2085 for the formal register and first-order lineage;
+Nick Petalas PR4898 for the earlier SL2(F3) instance; and their retained
+register-model predecessors. [SOURCES.json](SOURCES.json) pins predecessor
+texts as provenance, with no executable import or scientific replay of them.
+Affine cocycle representations, Frattini quotients and matrix-rank
+subadditivity are classical. No literature-wide priority is claimed.
+
+Nick Petalas's PR6008 supplies the earlier full-operator representation
+rank cut. This result extracts a common rectangular block, giving a
+one-unit charge even when a full paid operator defect has larger rank.
+Its main result is the general block invariant, rather than a counterpart
+obtained by changing a group or target in the full-operator cut.
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+Independent human and formal proof-kernel review are unclaimed.
+
+The gate is necessary rather than sufficient. It can miss nonidentity
+elements in ker(c), including Frattini defects in the normal-subgroup
+specialization. A nonsplit extension needs its own cocycle. Native maps,
+scalar conversions, source access, ownership/erasure, physical restoration,
+hosting, precision/tape, compiler closure and the complete signed supplier
+and outer bills remain unproved here. No heavy native, Lean, Docker or
+selected scientific cold replay is part of this claim.
+
+## Open next questions
+
+- Can several cocycle blocks give a strictly stronger joint weighted-call
+  bound for one supplied alphabet and full endpoint? This could rule out
+  words that pass each bound separately. First derive the linear call-count
+  constraints for one explicit alphabet and give a feasible dual witness.
+  Native prices and a promising physical endpoint are missing.
+- Can a second-order representation detect a specified Frattini defect
+  that this gate kills, without losing the one-call charge? This could
+  separate central targets hidden from all first-order quotients. First
+  state an exact block-product law and its per-call rank change. A
+  suitable second-order invariant, rather than a larger census, is missing.
+
+## Implementation bounds
+
+The finite verifier uses fixed F3 arithmetic, group order 216, at most
+seven roles, matrix dimension at most 21, words of length at most six,
+and bounded Cartesian products. It has no recursion, dynamic code
+generation, subprocesses or third-party imports. Functions are below
+60 physical lines. Checks use explicit exceptions in normal and optimized
+execution. Two exception-control callbacks have fixed visible targets.
+
+Power-of-Ten deviation, rule 3: CPython allocates integers, tuples and
+dictionaries during this one-shot computation. Fixed finite domains bound
+live memory; no caller-supplied size or unbounded search is accepted. A
+fixed-buffer implementation would be needed for literal allocation-free
+operation. Warning-strict normal and optimized commands are the available
+diagnostics; no proof-assistant or independent scientific acceptance is
+claimed by their success.

research/vector-cocycle-rank-floor/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "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/a4-seven-call-radical-rank/README.md",
+      "usage": "provenance",
+      "git_blob": "ab5ea83019119dcada4b654b137d418503014cf5",
+      "sha256": "26c9a90b1e73ce90b6711417db3f023e79192acdde8b94f1e7cfa0a93fafd42b"
+    },
+    {
+      "path": "research/sl2f3-all-dirty-minimum/README.md",
+      "usage": "provenance",
+      "git_blob": "b2b04a5a21e2a5f24f8641181f280b4982457b5d",
+      "sha256": "cf5ccd8c8b1aaa0f3b40e6a05558cfc568b23fb7f0239168c99cebcf8bebc98b"
+    },
+    {
+      "path": "research/prime-exponent-rank-cut/README.md",
+      "usage": "provenance",
+      "git_blob": "a23cf9be5d5ec8b258156b7925a9349fe6bef8b3",
+      "sha256": "4e1936de8546a3ac91f58cb5176f11a2b35d7a1093814794b35622bd97347db7"
+    }
+  ]
+}