Encode local Frobenius automorphisms without a full table (no κ)

research/frobenius-automorphism-codec/PROOF.md

@@ -0,0 +1,135 @@
+# A table-free bijection for local Frobenius automorphisms
+
+This scoped constructive proof was produced by Nick Petalas. Apache-2.0.
+
+## Statement and credited premises
+
+Fix an enumerated finite field L of size Q and characteristic p. Its element
+indices are 0 through Q-1, with zero at index zero. Field arithmetic and this
+enumeration are supplied. Let
+
+```text
+B = L[x_1,...,x_r]/(x_i^(p^h_i)),   h_i >= 1,
+t_i = p^h_i,    N = product_i t_i,
+r_e = number of i with h_i=e,
+k_e = N - p^(sum_j max(h_j-e,0)),
+C = sum_i k_(h_i) - sum_e r_e^2,
+M = Q^C product_e product_(j=0)^(r_e-1) (Q^r_e-Q^j).
+```
+
+Empty height lists are allowed: B=L and M=1.
+
+**Theorem.** There are explicit inverse maps between the integers
+`0 <= z < M` and the L-algebra automorphisms of B, represented by the r
+generator images, each in its N-monomial basis. Both maps use polynomially
+many field operations and integer bit operations in r, N and log Q, with
+supplied polynomial-cost field arithmetic. They require no N-by-N algebra
+multiplication table and no rejection of a candidate substitution. A uniform
+input integer therefore gives an exactly uniform automorphism.
+
+The local power-kernel description, tangent criterion and order M are inputs
+from Nick Petalas's [#6578, local count sections 1-3](https://github.com/CrocSwap/integer-mult-bounds/pull/6578).
+That package credits apoursh's #5663 intrinsic coefficient-field and type
+structure and Ali Romman's #5459 height flag. Those results and their
+scientific executables are not replayed here. The new assertion is the
+explicit invertible encoding and its resource bound, answering #6578's Open
+next question. Ordered-basis completion and positional integer notation are
+classical. No global literature-priority claim is made.
+
+## 1. Decode an invertible tangent block without rejection
+
+For an n-dimensional L-space, let v_0,...,v_(j-1) be the columns already
+chosen. Complete them to an ordered basis P by scanning the standard unit
+vectors in coordinate order and appending a vector precisely when it increases
+the span. This is deterministic and always finishes after n candidates.
+
+Every vector outside the old span has unique P-coordinates `(a,b)`, where
+`a` has j field elements and `b` has n-j field elements and is nonzero.
+For a vector of field indices define
+
+```text
+enc(c_0,...,c_(s-1)) = sum_i index(c_i) Q^i.
+```
+
+Thus the next column is indexed bijectively by
+
+```text
+d = enc(a) + Q^j (enc(b)-1),
+0 <= d < Q^n-Q^j.
+```
+
+Decode d by division by Q^j, adding one to the quotient before decoding b.
+The quotient range is exactly 1 through Q^(n-j)-1, so b cannot be zero.
+Coordinates in P give the next column. Conversely, solve in the same
+deterministically completed basis to recover a, b and d.
+
+Use the successive radices `Q^n-Q^j`, j=0,...,n-1, with the first digit
+least significant. This gives inverse integer codecs for GL_n(L).
+Induction on j proves that all intermediate columns are independent and
+that the forward and inverse constructions use the same P. Each ordered
+basis occurs once. For n=0 the unique basis is empty and its index is zero.
+
+## 2. Select exactly the free generator coefficients
+
+Enumerate the exponent tuples `a` with `0 <= a_j < t_j` lexicographically.
+For image y_i, let E_i be the monomials for which
+
+```text
+there exists j with a_j p^h_i >= t_j.
+```
+
+The cited power-kernel theorem says precisely that y_i is a linear
+combination of E_i. In particular, the allowed degree-one monomials are x_j
+with h_j<=h_i. The same-height coefficients of the images with height e
+form one square block in GL_(r_e)(L). All remaining coefficients on E_i
+are unrestricted. Call their ordered position set F, sorted first by i
+and then by the monomial order. Exactly the same-height diagonal blocks
+have been removed, so `|F|=C` by the cited dimensions k_e.
+
+Decode z first in the GL-block radices, in increasing height order. Fill
+each same-height tangent block using section 1. Decode the residual integer
+into C base-Q field indices and put these into F. Put zero in every
+forbidden position. The first GL block and first free coefficient are the
+least significant digits of their respective stages.
+
+Every image obeys its defining power relation. The tangent matrix is block
+triangular with invertible diagonal blocks, so the cited tangent criterion
+makes this substitution an automorphism. Conversely, every automorphism
+has exactly these allowed positions and invertible diagonal blocks. Extract
+those blocks with the inverse GL codec, read the free coefficients, and
+recombine the same positional digits. This is inverse to decoding in both
+directions. It proves bijectivity, including surjectivity, without using a
+finite test as a universal argument.
+
+## 3. Costs and exact uniformity
+
+Scanning the N exponent tuples for each generator takes O(r^2 N) elementary
+exponent comparisons. The generator-image output itself has rN field
+entries. The ordered-basis algorithm in section 1 can use at most n unit
+candidates at each of n stages, with a Gaussian rank calculation costing
+O(n^3) field operations per candidate. Coordinate solves cost O(n^3).
+The GL work is therefore O(sum_e r_e^5), and filling or extracting the
+remaining coefficients adds O(rN). This is a deliberately loose polynomial
+bound, not a performance measurement or an optimality claim.
+
+Live storage consists of the exponent list and generator images, O(rN)
+field indices or small exponent entries, plus O(r^2) elimination workspace
+and the integer index. The index has at most rN log2 Q bits because every
+automorphism is among Q^(rN) image tuples. Standard integer arithmetic and
+radix operations consequently have polynomial bit cost. No products of
+algebra basis elements or N-by-N multiplication table are needed for either
+codec. The separate finite oracle computes products only to test the new maps.
+
+Each automorphism has exactly one index. If z is uniform on 0,...,M-1,
+each output has probability 1/M. This is a rejection-free decoder given
+a uniform integer. It does not claim a fixed-length fair-bit sampler for
+arbitrary M, nor implement a randomness source.
+
+## Limits
+
+This is a supplied-field, supplied-height local-algebra construction.
+Residue-field discovery, nonsplit product permutations, semilinear
+automorphisms, tensor-character transport, arbitrary-tensor recognition and
+physical native execution are separate. No new kappa or multiplication theorem
+follows. The universal assertion rests on this proof and the named premises;
+the executable's bounded domains only corroborate the construction.

research/frobenius-automorphism-codec/README.md

@@ -0,0 +1,118 @@
+# Table-free integer encoding of local Frobenius automorphisms
+
+Scoped constructive proof with exact finite corroboration.
+This work was produced by Nick Petalas. Apache-2.0.
+No new kappa or selected-frontier change is claimed.
+
+For every supplied finite field L of characteristic p and every supplied height
+list h, [PROOF.md](PROOF.md) constructs inverse integer rank/unrank maps for
+all L-algebra automorphisms of
+
+```text
+B = L[x_1,...,x_r]/(x_i^(p^h_i)).
+```
+
+The output consists of the r generator images in the N-monomial basis.
+The decoder constructs no N-by-N multiplication table and rejects no candidate
+substitution. It uses O(sum_e r_e^5 + rN) field operations, with polynomial
+integer bit cost, for r_e variables of each height e. A uniform integer index
+therefore gives an exactly uniform automorphism. This assumes a uniform integer
+source; it is not a fixed-length fair-bit sampling claim.
+
+Nick Petalas's [#6578](https://github.com/CrocSwap/integer-mult-bounds/pull/6578)
+supplies the local power-kernel, tangent and counting premises and asks the
+uniform-sampling question. This package adds the explicit encoding, its inverse
+and its resource proof. It does not replay that predecessor's scientific code
+or recount its product and tensor orbits. Credit apoursh / #5663 and Ali
+Romman / #5459 for the retained structural lineage. The ordered-basis and
+positional-integer methods are classical; global literature priority is unclaimed.
+
+## Evidence
+
+The self-contained verifier checks the new maps directly:
+
+- Every one of 5,039 indices in eight local contexts, including F4 and F9,
+  round-trips and has distinct generator images. Literal sparse-polynomial
+  substitution checks every decoded defining relation and an independently
+  computed nonsingular full substitution map.
+- All 404 ordered-basis indices in six GL contexts round-trip and pass a
+  separate Leibniz determinant calculation.
+- Thirty selected indices in six larger or differently ordered contexts
+  round-trip, including dimensions eight, nine and sixteen. These are sampled
+  indices, not exhaustive large-domain claims.
+- Literal basis-product checks run at selected decoded maps. Sixteen controls
+  reject invalid indices, forbidden coefficients, singular tangent blocks,
+  malformed fields/heights and corrupted literal substitutions.
+
+The verifier prints a generated JSON receipt bound to the current package-file
+SHA256 hashes and writes no files. The universal assertion rests on the proof
+and cited premises, rather than on these finite checks.
+
+## Reproduce
+
+From the repository root, with CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/frobenius-automorphism-codec/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/frobenius-automorphism-codec/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/frobenius-automorphism-codec
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/frobenius-automorphism-codec --check-source-history
+```
+
+Another CPython 3.12 path may replace the local path. Expected markers are
+`PASS_FROBENIUS_AUTOMORPHISM_CODEC`, `PASS_REGISTERED_RESEARCH_PACKAGE` and
+`PASS_RESEARCH_COMMIT_BYTES`. Normal and optimized checks are registered.
+
+## Scope and limitations
+
+The `coverage-law-change` card explicitly changes to this algebraic side
+result. It supplies varied changed-basis inputs for future tests; it does not
+meet the card's productive-credit acceptance gate. No physical consumer,
+native alignment, coefficient-preparation bill, dirty restoration or complete
+signed invoice is supplied. All five selected framework assumptions remain.
+
+The executable bounds q to 2,3,4,5,7,8,9, generator count to four, heights to
+six and algebra dimension to 64. Its exhaustive contexts are smaller. The
+written algorithm covers arbitrary supplied finite fields and finite height
+lists. Coefficient-field discovery, semilinear maps, nonsplit products,
+tensor-character transport and arbitrary-tensor recognition are separate.
+Independent human and formal proof-kernel review are unclaimed. No selected
+cold replay, predecessor scientific suite, Lean or Docker build is run.
+
+[SOURCES.json](SOURCES.json) pins the older source text, catalogue and selected
+record as provenance at `e54523517d0f03e58352e647c403a5af3e525a57`. There are
+no external executable inputs. Live source-reference searches covered all
+paginated open and closed PR titles/bodies and found no matching recent
+source reuse. Main/merged term searches, active Discussions and reservations
+were checked. Sparse local notes, arbitrary diffs and unpublished work remain
+overlap limits. [Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19542478).
+
+## Open next questions
+
+1. Join the local codec to a supplied product decomposition and residue-field
+   Galois actions. First specify component permutations, coefficient fields
+   and generator-image data and prove a joint bijection. A supplied
+   decomposition and semilinear arithmetic contract are prerequisites.
+2. Identify a physical changed-basis consumer and price one encoded
+   substitution, including coefficients and restoration. That complete paid
+   contract is missing; uniform abstract sampling alone does not improve a
+   supplier. Structured questions are in [TASK.json](TASK.json).
+
+## Verifier constraints
+
+All code is nonrecursive. Every loop ranges over a bounded field, at most
+64 monomials, four generators, a fixed context list, bounded matrix entries
+or the finite codec index interval stated above. Every function is below
+60 physical lines. Invariants use explicit exceptions and remain enabled
+under optimized Python. The finite field definitions are checked on all
+their elements before the codecs run. The only local imports are the three
+named package modules; no network or subprocess runs occur.
+
+Power of Ten rule 3 deviation: CPython allocates managed integers and
+containers during execution. The stated domain guards bound each polynomial,
+matrix and index. The exhaustive verifier retains at most 2,880 decoded image
+tuples in its uniqueness set; the codec itself retains no census or full
+algebra table. Rule 9 deviation: Python field methods, iterator operations
+and the sixteen fixed rejection callbacks use runtime dispatch. Their
+targets are package-local and bounded. Warning-strict normal and optimized
+checks and AST/function-size inspection cover the touched implementation.

research/frobenius-automorphism-codec/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8",
+      "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/nonsplit-frobenius-orders/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "e75ee12a9d8e9a359756b1a6fe97f375f4fc43e4",
+      "sha256": "84c7b58eed9f6c92a58b3cf082612f1769e3559e06367f705de84007b99eb944"
+    },
+    {
+      "path": "research/nonsplit-frobenius-orders/README.md",
+      "usage": "provenance",
+      "git_blob": "b2e3bc4b0d686728bc39d392614319fe66f71f34",
+      "sha256": "1d8288484e9d8714af751c6b5f9130b21b00958ed9f3c066bb323589989f2912"
+    }
+  ]
+}