From 11b1aa6e16ef680b2bc3ab8b665b6902e227ec4c Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 11 Nov 2026 13:33:26 +0000 Subject: [PATCH] feat(research): encode local Frobenius automorphisms bijectively --- .../frobenius-automorphism-codec/PROOF.md | 135 ++++++++++++++++ .../frobenius-automorphism-codec/README.md | 118 ++++++++++++++ .../frobenius-automorphism-codec/SOURCES.json | 30 ++++ .../frobenius-automorphism-codec/TASK.json | 90 +++++++++++ .../frobenius-automorphism-codec/VERIFY.json | 32 ++++ .../frobenius-automorphism-codec/codec.py | 65 ++++++++ .../frobenius-automorphism-codec/linear.py | 153 ++++++++++++++++++ .../frobenius-automorphism-codec/oracle.py | 109 +++++++++++++ .../frobenius-automorphism-codec/verify.py | 146 +++++++++++++++++ 9 files changed, 878 insertions(+) create mode 100644 research/frobenius-automorphism-codec/PROOF.md create mode 100644 research/frobenius-automorphism-codec/README.md create mode 100644 research/frobenius-automorphism-codec/SOURCES.json create mode 100644 research/frobenius-automorphism-codec/TASK.json create mode 100644 research/frobenius-automorphism-codec/VERIFY.json create mode 100644 research/frobenius-automorphism-codec/codec.py create mode 100644 research/frobenius-automorphism-codec/linear.py create mode 100644 research/frobenius-automorphism-codec/oracle.py create mode 100644 research/frobenius-automorphism-codec/verify.py diff --git a/research/frobenius-automorphism-codec/PROOF.md b/research/frobenius-automorphism-codec/PROOF.md new file mode 100644 index 0000000000..0e7be2d184 --- /dev/null +++ b/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. diff --git a/research/frobenius-automorphism-codec/README.md b/research/frobenius-automorphism-codec/README.md new file mode 100644 index 0000000000..944e66e5a3 --- /dev/null +++ b/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. diff --git a/research/frobenius-automorphism-codec/SOURCES.json b/research/frobenius-automorphism-codec/SOURCES.json new file mode 100644 index 0000000000..6b03ded970 --- /dev/null +++ b/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" + } + ] +} diff --git a/research/frobenius-automorphism-codec/TASK.json b/research/frobenius-automorphism-codec/TASK.json new file mode 100644 index 0000000000..624855a1d2 --- /dev/null +++ b/research/frobenius-automorphism-codec/TASK.json @@ -0,0 +1,90 @@ +{ + "schema_version": 1, + "task_id": "coverage-law-change", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "coverage-law-change", + "question": "Can a completed call earn more independent productive target credit without an offsetting paid bill?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Use #5599 as a completed positive control, then choose one uncovered cut/module beyond an applicable frozen exclusion. Derive independence, saturation and chronological availability rather than counting rational rank alone. Price target credits and all new jobs together, then check compiler and actual caller compatibility. Stop on a nonphysical credit or an unfavorable complete relaxation.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "target credit", + "helper split", + "coverage law" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Construct inverse integer codecs for all local characteristic-power algebra automorphisms, given the coefficient field and height list.", + "scope_change_reason": "Answer PR6578 Open next question on uniform sampling. This is an algebraic side result, not a productive-credit construction.", + "bottleneck_link": "Explicit changed-basis inputs for future algebraic tests; no physical supplier or complete signed invoice is supplied.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved and verified local rank/unrank codec; no extension to products or paid native execution.", + "outcome": "completed", + "evidence": "PROOF.md supplies the universal bijection and polynomial resource proof. verify.py executes exact inverse, literal-substitution and rejection checks.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can this local encoding be joined to a supplied product decomposition with residue-field Galois actions?", + "why_it_matters": "It would cover the full nonsplit product class rather than local L-linear automorphisms.", + "first_step": "Specify the component permutation, coefficient-field and generator-image data and prove a joint bijection.", + "blocked_by": "A concrete supplied decomposition and semilinear arithmetic contract." + }, + { + "question": "Which physical changed-basis consumer benefits after coefficient preparation and restoration are charged?", + "why_it_matters": "A uniform abstract sample does not improve a paid multiplication supplier.", + "first_step": "Choose one literal native producer/consumer and price one encoded substitution.", + "blocked_by": "No physical consumer, native alignment or complete paid invoice is provided." + } + ], + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19542478", + "upstream_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "selected_source_pr": 7000, + "priority_revision": 8, + "source_pr": 6578, + "source_author": "petalas", + "predecessor_author": "petalas", + "checked_at_utc": "2026-11-11T13:27:18Z", + "scope": "Live open and closed PR title/body source search, Discussions and local reservations; sparse local notes and arbitrary diffs are not complete." + } +} diff --git a/research/frobenius-automorphism-codec/VERIFY.json b/research/frobenius-automorphism-codec/VERIFY.json new file mode 100644 index 0000000000..627ee15ea9 --- /dev/null +++ b/research/frobenius-automorphism-codec/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact inverse codecs, literal polynomial substitutions and nonsingular maps, extension fields, invalid-domain and corrupted-image controls; generated SHA256-bound receipt." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact inverse codecs, literal polynomial substitutions and nonsingular maps, extension fields, invalid-domain and corrupted-image controls; generated SHA256-bound receipt." + } + ] +} diff --git a/research/frobenius-automorphism-codec/codec.py b/research/frobenius-automorphism-codec/codec.py new file mode 100644 index 0000000000..8bba47a3fd --- /dev/null +++ b/research/frobenius-automorphism-codec/codec.py @@ -0,0 +1,65 @@ +"""Generator-image codec for local characteristic-power algebras. Apache-2.0.""" + +from itertools import product +from math import prod + +from linear import Field, gl_order, gl_rank, gl_unrank, require + + +class Codec: + """No multiplication table is constructed. Bounds apply to the executable.""" + + def __init__(self, q, heights): + self.field = Field(q) + require(isinstance(heights, tuple) and len(heights) <= 4, "height shape") + require(all(type(h) is int and 1 <= h <= 6 for h in heights), "height range") + self.heights = heights + self.cutoffs = tuple(self.field.p**h for h in heights) + require(prod(self.cutoffs) <= 64, "algebra dimension capacity") + self.monomials = tuple(product(*(range(t) for t in self.cutoffs))) + self.n = len(self.monomials) + self.units = tuple(self.monomials.index(tuple(int(i == j) for j in range(len(heights)))) + for i in range(len(heights))) + self.groups = tuple(tuple(i for i, h in enumerate(heights) if h == e) + for e in sorted(set(heights))) + self.allowed = tuple(tuple(any(a * self.field.p**h >= t + for a, t in zip(exponent, self.cutoffs)) + for exponent in self.monomials) for h in heights) + diagonal = {(i, self.units[j]) for group in self.groups for i in group for j in group} + self.free = tuple((i, a) for i in range(len(heights)) for a in range(self.n) + if self.allowed[i][a] and (i, a) not in diagonal) + self.block_orders = tuple(gl_order(q, len(group)) for group in self.groups) + self.order = q**len(self.free) * prod(self.block_orders) + + def unrank(self, index): + require(type(index) is int and 0 <= index < self.order, "automorphism index") + images = [[0] * self.n for _ in self.heights] + for group, block_order in zip(self.groups, self.block_orders): + index, block_index = divmod(index, block_order) + block = gl_unrank(self.field, len(group), block_index) + for i, column in zip(group, block): + for j, coefficient in zip(group, column): + images[i][self.units[j]] = coefficient + for i, a in self.free: + index, images[i][a] = divmod(index, self.field.q) + require(index == 0, "automorphism index was not exhausted") + return tuple(tuple(image) for image in images) + + def rank(self, images): + require(isinstance(images, tuple) and len(images) == len(self.heights), "image shape") + require(all(isinstance(v, tuple) and len(v) == self.n for v in images), "image length") + for i, image in enumerate(images): + for a, coefficient in enumerate(image): + require(type(coefficient) is int and 0 <= coefficient < self.field.q, + "coefficient range") + require(self.allowed[i][a] or coefficient == 0, "power relation violated") + index, place = 0, 1 + for group, block_order in zip(self.groups, self.block_orders): + block = tuple(tuple(images[i][self.units[j]] for j in group) for i in group) + index += place * gl_rank(self.field, block) + place *= block_order + for i, a in self.free: + index += place * images[i][a] + place *= self.field.q + require(place == self.order and index < place, "rank range invariant") + return index diff --git a/research/frobenius-automorphism-codec/linear.py b/research/frobenius-automorphism-codec/linear.py new file mode 100644 index 0000000000..7cb515d9f6 --- /dev/null +++ b/research/frobenius-automorphism-codec/linear.py @@ -0,0 +1,153 @@ +"""Small exact fields and an ordered-basis integer codec. Apache-2.0.""" + +from math import prod + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +class Field: + """Polynomial coordinates for these explicitly supplied finite fields.""" + + def __init__(self, q): + specifications = { + 2: (2, (0, 1)), 3: (3, (0, 1)), 4: (2, (1, 1, 1)), + 5: (5, (0, 1)), 7: (7, (0, 1)), + 8: (2, (1, 1, 0, 1)), 9: (3, (1, 0, 1)), + } + require(type(q) is int and q in specifications, "unsupported field") + self.q = q + self.p, self.modulus = specifications[q] + self.degree = len(self.modulus) - 1 + + def digits(self, value): + require(type(value) is int and 0 <= value < self.q, "field element") + return tuple((value // self.p**i) % self.p for i in range(self.degree)) + + def add(self, a, b): + return sum(((x + y) % self.p) * self.p**i + for i, (x, y) in enumerate(zip(self.digits(a), self.digits(b)))) + + def neg(self, a): + return sum((-x % self.p) * self.p**i for i, x in enumerate(self.digits(a))) + + def mul(self, a, b): + aa, bb = self.digits(a), self.digits(b) + out = [0] * (2 * self.degree - 1) + for i, x in enumerate(aa): + for j, y in enumerate(bb): + out[i + j] = (out[i + j] + x * y) % self.p + for i in range(len(out) - 1, self.degree - 1, -1): + lead = out[i] + for j, coefficient in enumerate(self.modulus): + out[i - self.degree + j] = ( + out[i - self.degree + j] - lead * coefficient) % self.p + return sum(out[i] * self.p**i for i in range(self.degree)) + + def inv(self, a): + require(type(a) is int and 0 < a < self.q, "nonzero inverse required") + result, power, exponent = 1, a, self.q - 2 + for _ in range(exponent.bit_length()): + if exponent & 1: + result = self.mul(result, power) + power = self.mul(power, power) + exponent >>= 1 + require(self.mul(a, result) == 1, "supplied field is invalid") + return result + + +def reduce_rows(field, rows, width): + """RREF, with optional trailing right-hand-side columns.""" + require(0 <= width <= 64 and len(rows) <= 64, "matrix capacity") + require(all(width <= len(row) <= 65 for row in rows), "matrix shape") + work = [list(row) for row in rows] + pivots = [] + for column in range(width): + candidates = [i for i in range(len(pivots), len(work)) if work[i][column]] + if not candidates: + continue + pivot = len(pivots) + source = candidates[0] + work[pivot], work[source] = work[source], work[pivot] + inverse = field.inv(work[pivot][column]) + work[pivot] = [field.mul(inverse, x) for x in work[pivot]] + for i in range(len(work)): + if i != pivot: + scale = field.neg(work[i][column]) + work[i] = [field.add(x, field.mul(scale, y)) + for x, y in zip(work[i], work[pivot])] + pivots.append(column) + return work, tuple(pivots) + + +def rank(field, columns, n): + rows = [[column[i] for column in columns] for i in range(n)] + return len(reduce_rows(field, rows, len(columns))[1]) + + +def complete(field, columns, n): + """Extend independent columns by the earliest available standard vectors.""" + require(0 <= n <= 4 and len(columns) <= n, "basis capacity") + require(all(len(c) == n for c in columns), "column shape") + basis = list(columns) + require(rank(field, basis, n) == len(basis), "dependent prefix") + for i in range(n): + candidate = tuple(int(i == j) for j in range(n)) + if len(basis) < n and rank(field, basis + [candidate], n) > len(basis): + basis.append(candidate) + require(len(basis) == n, "basis completion failed") + return basis + + +def coordinates(field, basis, vector): + n = len(basis) + rows = [[basis[j][i] for j in range(n)] + [vector[i]] for i in range(n)] + reduced, pivots = reduce_rows(field, rows, n) + require(pivots == tuple(range(n)), "singular basis") + return tuple(row[n] for row in reduced) + + +def base_digits(value, radix, length): + require(type(value) is int and 0 <= value < radix**length, "digit range") + return tuple((value // radix**i) % radix for i in range(length)) + + +def gl_order(q, n): + return prod(q**n - q**j for j in range(n)) + + +def gl_unrank(field, n, index): + require(type(n) is int and 0 <= n <= 4, "GL dimension capacity") + require(type(index) is int and 0 <= index < gl_order(field.q, n), "GL index") + columns = [] + for j in range(n): + radix = field.q**n - field.q**j + index, digit = divmod(index, radix) + low = digit % field.q**j + high = digit // field.q**j + 1 + coefficients = base_digits(low, field.q, j) + base_digits(high, field.q, n - j) + basis = complete(field, columns, n) + vector = [0] * n + for c, coefficient in zip(basis, coefficients): + vector = [field.add(x, field.mul(coefficient, y)) for x, y in zip(vector, c)] + columns.append(tuple(vector)) + require(index == 0, "GL index was not exhausted") + return tuple(columns) + + +def gl_rank(field, columns): + n = len(columns) + require(n <= 4 and all(len(c) == n for c in columns), "GL shape") + index, place = 0, 1 + for j, vector in enumerate(columns): + basis = complete(field, columns[:j], n) + coefficients = coordinates(field, basis, vector) + low = sum(x * field.q**i for i, x in enumerate(coefficients[:j])) + high = sum(x * field.q**i for i, x in enumerate(coefficients[j:])) + require(high != 0, "singular tangent block") + digit = low + field.q**j * (high - 1) + index += place * digit + place *= field.q**n - field.q**j + return index diff --git a/research/frobenius-automorphism-codec/oracle.py b/research/frobenius-automorphism-codec/oracle.py new file mode 100644 index 0000000000..ab8140331d --- /dev/null +++ b/research/frobenius-automorphism-codec/oracle.py @@ -0,0 +1,109 @@ +"""Literal sparse-polynomial substitution, independent of the codec layout.""" + +from itertools import permutations + +from linear import require + + +def multiply(field, cutoffs, left, right): + result = {} + for a, x in left.items(): + for b, y in right.items(): + exponent = tuple(s + t for s, t in zip(a, b)) + if all(s < t for s, t in zip(exponent, cutoffs)): + value = field.add(result.get(exponent, 0), field.mul(x, y)) + if value: + result[exponent] = value + else: + result.pop(exponent, None) + return result + + +def power(field, cutoffs, value, exponent): + require(0 <= exponent <= 64, "power capacity") + result = {tuple(0 for _ in cutoffs): 1} + for _ in range(exponent): + result = multiply(field, cutoffs, result, value) + return result + + +def substitute(field, cutoffs, images, exponent): + result = {tuple(0 for _ in cutoffs): 1} + for image, degree in zip(images, exponent): + result = multiply(field, cutoffs, result, power(field, cutoffs, image, degree)) + return result + + +def determinant(field, columns): + """Leibniz formula, separate from the ordered-basis elimination.""" + n = len(columns) + require(n <= 4, "determinant capacity") + result = 0 + for permutation in permutations(range(n)): + inversions = sum(permutation[i] > permutation[j] + for i in range(n) for j in range(i + 1, n)) + term = 1 + for j, i in enumerate(permutation): + term = field.mul(term, columns[j][i]) + result = field.add(result, field.neg(term) if inversions % 2 else term) + return result + + +def binary_rank(columns): + """Integer XOR elimination, not the field RREF used by the codec.""" + pivots = {} + for column in columns: + value = sum(x << i for i, x in enumerate(column)) + for bit in range(len(column) - 1, -1, -1): + if value & (1 << bit): + if bit in pivots: + value ^= pivots[bit] + else: + pivots[bit] = value + break + return len(pivots) + + +def column_rank(field, columns): + """Normalize sparse leading columns instead of reducing the transposed rows.""" + pivots = {} + for column in columns: + value = list(column) + for i in range(len(value)): + if not value[i]: + continue + if i in pivots: + scale = field.neg(value[i]) + value = [field.add(x, field.mul(scale, y)) + for x, y in zip(value, pivots[i])] + else: + inverse = field.inv(value[i]) + pivots[i] = tuple(field.mul(inverse, x) for x in value) + break + return len(pivots) + + +def inspect(codec, images, all_products=False): + field = codec.field + sparse = tuple({a: x for a, x in zip(codec.monomials, image) if x} for image in images) + for image, cutoff in zip(sparse, codec.cutoffs): + require(not power(field, codec.cutoffs, image, cutoff), "literal relation failed") + substitutions = tuple(substitute(field, codec.cutoffs, sparse, a) for a in codec.monomials) + columns = tuple(tuple(image.get(a, 0) for a in codec.monomials) for image in substitutions) + if field.q == 2: + require(binary_rank(columns) == codec.n, "literal binary substitution singular") + elif codec.n <= 4: + require(determinant(field, columns) != 0, "literal substitution determinant zero") + else: + require(column_rank(field, columns) == codec.n, "literal substitution singular") + checked = 0 + if all_products: + for a, left in zip(codec.monomials, substitutions): + for b, right in zip(codec.monomials, substitutions): + exponent = tuple(s + t for s, t in zip(a, b)) + expected = (substitute(field, codec.cutoffs, sparse, exponent) + if all(s < t for s, t in zip(exponent, codec.cutoffs)) else {}) + require(multiply(field, codec.cutoffs, left, right) == expected, + "literal product not preserved") + checked += 1 + return checked diff --git a/research/frobenius-automorphism-codec/verify.py b/research/frobenius-automorphism-codec/verify.py new file mode 100644 index 0000000000..295d5f5d0f --- /dev/null +++ b/research/frobenius-automorphism-codec/verify.py @@ -0,0 +1,146 @@ +"""Exact finite corroboration of the new inverse codecs. Apache-2.0.""" + +import hashlib +import json +from pathlib import Path +import sys + +PACKAGE = Path(__file__).resolve().parent +sys.path.insert(0, str(PACKAGE)) + +from codec import Codec +from linear import Field, gl_order, gl_rank, gl_unrank, require +from oracle import determinant, inspect + + +def rejects(operation): + try: + operation() + except ValueError: + return 1 + raise RuntimeError("negative control was accepted") + + +def fields(): + checked = 0 + for q in (2, 3, 4, 5, 7, 8, 9): + field = Field(q) + for a in range(q): + require(field.add(a, field.neg(a)) == 0, "additive inverse") + if a: + require(field.mul(a, field.inv(a)) == 1, "multiplicative inverse") + for b in range(q): + require(field.mul(a, b) == field.mul(b, a), "commutative product") + for c in range(q): + require(field.mul(a, field.add(b, c)) == + field.add(field.mul(a, b), field.mul(a, c)), "distributivity") + require(field.mul(a, field.mul(b, c)) == + field.mul(field.mul(a, b), c), "associative product") + checked += 1 + return checked + + +def general_linear(): + checked = 0 + for q, n in ((2, 0), (2, 1), (2, 2), (2, 3), (3, 2), (4, 2)): + field = Field(q) + seen = set() + for index in range(gl_order(q, n)): + columns = gl_unrank(field, n, index) + require(gl_rank(field, columns) == index, "GL inverse failed") + require(determinant(field, columns) != 0, "GL determinant zero") + require(columns not in seen, "duplicate GL encoding") + seen.add(columns) + checked += 1 + return checked + + +def exhaustive_codecs(): + contexts, maps, products = [], 0, 0 + for q, heights in ((2, ()), (2, (1,)), (2, (1, 1)), (2, (1, 2)), + (3, (1,)), (4, (1, 1)), (8, (1,)), (9, (1,))): + codec = Codec(q, heights) + seen = set() + for index in range(codec.order): + images = codec.unrank(index) + require(codec.rank(images) == index, "local codec inverse failed") + require(images not in seen, "duplicate generator images") + seen.add(images) + products += inspect(codec, images, index in (0, codec.order // 2, codec.order - 1)) + maps += 1 + contexts.append({"q": q, "heights": heights, "indices": codec.order}) + return contexts, maps, products + + +def larger_codecs(): + checked = 0 + contexts = [] + for q, heights in ((2, (2, 2)), (2, (1, 1, 1)), (2, (2, 1)), + (3, (1, 1)), (4, (1, 2)), (5, (1,))): + codec = Codec(q, heights) + indices = sorted({0, 1, codec.order // 3, codec.order // 2, codec.order - 1}) + for index in indices: + images = codec.unrank(index) + require(codec.rank(images) == index, "larger codec inverse failed") + # Large nonbinary cases check the actual defining relations and products. + inspect(codec, images, all_products=codec.field.q != 2) + checked += 1 + contexts.append({"q": q, "heights": heights, "order": str(codec.order), + "tested_indices": [str(i) for i in indices]}) + return contexts, checked + + +def controls(): + codec = Codec(2, (1, 2)) + good = codec.unrank(codec.order - 1) + constant = [list(v) for v in good] + constant[0][0] = 1 + high = [list(v) for v in good] + high[0][codec.units[1]] = 1 + singular = [list(v) for v in good] + singular[0][codec.units[0]] = 0 + malformed = [list(v) for v in good] + malformed[0][1] = 2 + requests = [lambda: codec.unrank(-1), lambda: codec.unrank(codec.order), + lambda: codec.unrank(True), lambda: codec.rank(good[:-1]), + lambda: codec.rank(tuple(tuple(v) for v in constant)), + lambda: codec.rank(tuple(tuple(v) for v in high)), + lambda: codec.rank(tuple(tuple(v) for v in singular)), + lambda: codec.rank(tuple(tuple(v) for v in malformed)), + lambda: Codec(6, (1,)), lambda: Codec(2, (0,)), + lambda: Codec(2, (4, 4)), lambda: gl_rank(Field(2), ((1, 0), (1, 0))), + lambda: gl_unrank(Field(2), 2, gl_order(2, 2)), + lambda: inspect(codec, tuple(tuple(v) for v in constant)), + lambda: inspect(codec, tuple(tuple(v) for v in high)), + lambda: inspect(codec, tuple(tuple(v) for v in singular))] + return sum(rejects(request) for request in requests) + + +def receipt(): + files = sorted(PACKAGE.iterdir()) + require(len(files) <= 16, "package file capacity") + hashes = {} + for path in files: + if path.is_file(): + require(path.stat().st_size <= 128 * 1024, "package file size") + hashes[path.name] = hashlib.sha256(path.read_bytes()).hexdigest() + return hashes + + +def main(): + field_identities = fields() + gl_indices = general_linear() + exhaustive, indices, products = exhaustive_codecs() + larger, larger_indices = larger_codecs() + failures = controls() + report = {"status": "PASS_FROBENIUS_AUTOMORPHISM_CODEC", + "field_identities": field_identities, "gl_indices": gl_indices, + "exhaustive_contexts": exhaustive, "exhaustive_indices": indices, + "basis_products_in_exhaustive_contexts": products, + "larger_contexts": larger, "larger_indices": larger_indices, + "rejecting_controls": failures, "sha256": receipt()} + print(json.dumps(report, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()