From c09b7a57f81f941b7f9ee6882172eb21a683ded1 Mon Sep 17 00:00:00 2001 From: apoursh <8867770+apoursh@users.noreply.github.com> Date: Sun, 25 Oct 2026 00:37:07 -0400 Subject: [PATCH] Recognize Frobenius-truncated prime-field algebra tables --- .../frobenius-algebra-recognition/PROOF.md | 279 ++++++++++++++ .../frobenius-algebra-recognition/README.md | 149 ++++++++ .../SOURCES.json | 30 ++ .../frobenius-algebra-recognition/TASK.json | 137 +++++++ .../frobenius-algebra-recognition/VERIFY.json | 63 ++++ .../check_exhaustive.py | 244 +++++++++++++ .../recognize.py | 343 ++++++++++++++++++ .../frobenius-algebra-recognition/verify.py | 275 ++++++++++++++ 8 files changed, 1520 insertions(+) create mode 100644 research/frobenius-algebra-recognition/PROOF.md create mode 100644 research/frobenius-algebra-recognition/README.md create mode 100644 research/frobenius-algebra-recognition/SOURCES.json create mode 100644 research/frobenius-algebra-recognition/TASK.json create mode 100644 research/frobenius-algebra-recognition/VERIFY.json create mode 100644 research/frobenius-algebra-recognition/check_exhaustive.py create mode 100644 research/frobenius-algebra-recognition/recognize.py create mode 100644 research/frobenius-algebra-recognition/verify.py diff --git a/research/frobenius-algebra-recognition/PROOF.md b/research/frobenius-algebra-recognition/PROOF.md new file mode 100644 index 0000000000..0a0b7d1fe4 --- /dev/null +++ b/research/frobenius-algebra-recognition/PROOF.md @@ -0,0 +1,279 @@ +# Recognizing Frobenius-truncated algebras from a multiplication table + +This note gives a recognition criterion and an explicit algebra isomorphism +for a supplied multiplication table over a prime field. It answers a restricted +part of [Ali Romman's PR5459 handoff](https://github.com/CrocSwap/integer-mult-bounds/pull/5459): +the inputs and output already refer to one common vector space. It does not +recognize an arbitrary three-factor tensor up to independent basis changes, +extract its nucleus, or supply the reductions needed to obtain that table. +It does not change the selected multiplication bound. + +## 1. Input contract and criterion + +Let `p` be a prime and let `A` be a nonzero, `n`-dimensional vector space over +`F_p`, supplied by its structure constants. First check commutativity and +associativity on a basis. Recover the identity by solving the `n^2` linear +coordinate equations `u*b_j = b_j` for its `n` unknown coordinates, and check +the resulting element on both sides of every basis vector. Reject if the +system is inconsistent or any check fails. Commutativity makes a left unit +two-sided, and a two-sided unit is unique. These finite checks establish the +algebra laws for all inputs by bilinearity and trilinearity. A malformed table +is rejected before the criterion below. +Primality of `p` is a separate input condition: arithmetic modulo a composite +integer is not a substitute for `F_p`. + +Write `F(a) = a^p`. This is an `F_p`-linear endomorphism because `A` is +commutative of characteristic `p`. Let `E` be the least nonnegative integer +such that `p^E >= n`, and set + +``` +J = ker(F^E), Q = J / J^2, +K_e = ker(F^e), 0 <= e <= E, +V_e = (K_e + J^2) / J^2, 0 <= e <= E. +``` + +Here `F^0` is the identity, so `K_0 = 0`; `J^2` denotes the span of products +of pairs of elements of `J`. Every `K_e` lies in `J`, so `V_e` is a subspace +of `Q`. The spaces `V_e` form an increasing flag from `0` to `Q`. +Define + +``` +d_e = dim(V_e) - dim(V_(e-1)), 1 <= e <= E, +N = p^(sum_(e=1)^E e*d_e). +``` + +**Theorem.** The checked table is isomorphic, as a unital `F_p`-algebra, to + +``` +B = F_p[x_1,...,x_r] / (x_i^(p^h_i) : 1 <= i <= r), +``` + +with positive heights `h_i`, if and only if + +1. `J` has codimension one in `A`; and +2. `N = n`. + +The multiset of heights is intrinsic: height `e` occurs `d_e` times. An empty +list is allowed, in which case `B = F_p` and `n = 1`. Acceptance produces +generators `g_i` of the prescribed heights and the invertible matrix whose +columns are their ordered monomials. This matrix, together with its inverse, +is an explicit transporter between the common-basis multiplication tables. + +The word "transporter" here means an algebra isomorphism with the same map +on both inputs and the output. It is not a general tensor-orbit transporter. + +## 2. The Frobenius kernel recovers the nilradical + +Let `R` be the set of nilpotent elements of `A`. In a commutative algebra, +`R` is an ideal: products with arbitrary elements remain nilpotent, and a +sufficiently large characteristic-power Frobenius kills a sum of nilpotents. +Choose a vector-space basis `b_1,...,b_s` of `R` and positive integers `t_i` +with `b_i^t_i = 0`. The ideal generated by these basis elements is `R`. +Every product of more than `sum_i(t_i-1)` generators contains a factor +`b_i^t_i`, so `R` is nilpotent. + +The chain `R, R^2, ...` decreases strictly until it reaches zero. Indeed, if +`R^k = R^(k+1)` is nonzero, multiplication by further powers of `R` makes all +later powers equal, contrary to nilpotence. Since `1` is not nilpotent, +`dim R <= n-1`, and therefore `R^n = 0`. + +Every `a` in `R` consequently satisfies `a^(p^E) = 0`, since `p^E >= n`. +Conversely, every element killed by this power is nilpotent. Thus + +``` +J = ker(F^E) = R, J^n = 0. +``` + +This derivation does not assume that `A` is local. If `J` has codimension +one, the scalar copy of `F_p` maps isomorphically onto `A/J`. Every element +outside `J` then has the form `c*1 + j`, where `c != 0` and `j` is nilpotent, +and is a unit by a finite geometric series. Thus `J` is the unique maximal +ideal, and `A` is local with residue field exactly `F_p`. + +The codimension test matters. An extension field such as `F_4` viewed as a +two-dimensional `F_2`-algebra has zero nilradical but is outside this family; +its radical has codimension two. Products of fields are also excluded. + +## 3. Necessity and recovery of the heights + +Suppose `A` is the displayed algebra `B`. Its monomials + +``` +x_1^a_1 ... x_r^a_r, 0 <= a_i < p^h_i, +``` + +form a basis, its radical is `(x_1,...,x_r)`, and its tangent quotient +`J/J^2` has basis the classes of `x_1,...,x_r`. In particular, `J` has +codimension one and `n = p^(sum_i h_i)`, so every `h_i <= E`. + +If `h_i <= e`, the element `x_i` is killed by `F^e`; hence its tangent class +belongs to `V_e`. For the converse, expand an element of `J` into its linear +part and terms of total degree at least two. Frobenius raises every monomial +separately to its `p^e` power. If the linear coefficient of `x_i` is nonzero +and `h_i > e`, its power contributes a nonzero coefficient to +`x_i^(p^e)`. No other linear term contributes that monomial. No term of +degree at least two contributes it either: its surviving power has total +degree at least `2*p^e`; terms killed by a truncation contribute nothing. +Thus this coefficient cannot cancel. + +It follows that + +``` +V_e = span{x_i + J^2 : h_i <= e}. +``` + +Therefore `d_e` counts exactly the variables of height `e`, and the dimension +test `N = n` is necessary. The proof is invariant under an arbitrary common +change of basis in `A`; the identity and radical need not be coordinate axes +in the supplied table. + +## 4. Sufficiency and an explicit transporter + +Assume the two tests pass. For `e = 1,...,E`, extend a basis of `V_(e-1)` +to a basis of `V_e`, and choose the new representatives directly in `K_e`. +Linear elimination on a basis of `K_e` modulo `J^2` constructs such lifts. +Call the resulting elements `g_1,...,g_r` and assign height `h_i = e` to +each lift added at step `e`. Their classes form a basis of `J/J^2`, and + +``` +g_i^(p^h_i) = 0. +``` + +The classes are chosen by first entry into the flag. A lift of height `e` +cannot already lie in `K_(e-1)`, since its class would then belong to +`V_(e-1)`. No minimal-exponent test beyond the flag is needed. + +The substitution `x_i -> g_i` defines a unital homomorphism `phi: B -> A`, +because all defining power relations hold. It is surjective. One way to see +this is the finite nilpotent form of Nakayama's lemma. Let `C` be the +`F_p`-subalgebra generated by `1,g_1,...,g_r`. Tangent spanning gives +`J = span{g_i} + J^2`. For each `k >= 1`, express every factor of a product +in `J^k` by this formula. The product of its linear parts lies in `C`, and +every other term lies in `J^(k+1)`. Hence + +``` +J^k is contained in C + J^(k+1). +``` + +Starting from `A = F_p*1 + J` and repeating this containment through +`J^n = 0` gives `A = C`. This is also a direct proof of the particular +Nakayama implication used here. + +The monomial basis of `B` has size `N`, and the dimension test gives +`dim B = N = n = dim A`. A surjective linear map between these equal finite +dimensions is invertible. Therefore `phi` is the required isomorphism. + +For a concrete certificate, order the exponent tuples in a declared fixed +order and form the matrix + +``` +P[:,a] = g_1^a_1 ... g_r^a_r +``` + +in the supplied basis of `A`. Its constant column is the recovered unit. +The certificate consists of the heights, the generators, `P` and `P^-1`. +An independent checker can verify invertibility, the unit column, every +defining generator power and every basis-product identity + +``` +mu_A(P*u_a, P*u_b) = P*mu_B(u_a,u_b). +``` + +These `n^2` identities imply the identity for all pairs by bilinearity. +They check the actual transporter rather than trusting the recognition +path or the inferred heights. Equivalently, +`mu_B(u,v) = P^-1*mu_A(P*u,P*v)`. + +## 5. Why tangent Frobenius alone is insufficient + +The filtration uses images of kernels in the algebra before quotienting: +`V_e = (ker(F^e) + J^2)/J^2`. It must not be replaced by the kernel of the +induced Frobenius on `J/J^2`. Indeed, `a^p` lies in `J^p`, which is contained +in `J^2` for every `p >= 2`, so the latter induced map is always zero. + +For the explicit example `A = F_2[t]/(t^4)`, the radical is +`span{t,t^2,t^3}`, with square `span{t^2,t^3}`. Squaring gives + +``` +(a*t + b*t^2 + c*t^3)^2 = a*t^2. +``` + +Thus `ker F = span{t^2,t^3}`, `V_1 = 0`, and `V_2 = J/J^2`. +The correct height list is `(2)`, and the predicted dimension is four. +Frobenius on the tangent quotient alone would give height `(1)` and the +wrong predicted dimension two. + +The dimension test also cannot be dropped. For the square-zero algebra +`F_2 + J` with `dim J = 3` and `J^2 = 0`, all three tangent generators have +height one, but `dim A = 4` while the predicted truncated-polynomial +dimension is `2^3 = 8`. The generators give a surjection with additional +relations, not an isomorphism to the proposed model. + +## 6. Finite algorithm, cost and the one-dimensional edge + +All steps are finite linear algebra and arithmetic on the supplied table: + +1. Validate commutativity and associativity on basis vectors, recover the + unit by solving its linear equations, and check it on both sides. +2. Compute Frobenius on basis vectors by repeated squaring, its successive + kernels through `E`, and a basis of `J^2` from pairwise radical products. +3. Compute the flag dimensions and adapted lifts by Gaussian elimination; + reject unless the codimension and dimension tests pass. +4. Enumerate the `n` model monomials after acceptance, compute their images, + invert the resulting matrix, and check every basis-product identity. + +For fixed prime `p`, this is a deterministic polynomial algorithm in `n`. +There are at most `ceil(log_2 n)` Frobenius levels. Dense table multiplication +uses at most `O(n^3)` field operations, and the table-law and final +basis-product checks use polynomially many such operations (a conservative +bound for a direct implementation is `O(n^6 + n^4 log p)`). No search over +all algebra elements, all bases or all automorphisms is required. Computing +the exact candidate dimension is polynomial: its bit length is at most +`O(n*(log n + log p))`, and is `O(n log n)` for fixed `p`. The implementation +may compute that exact integer. Optionally, capped multiplication can stop +as soon as the candidate exceeds `n`; it is not needed for the complexity +guarantee. + +Conditional on a prime input, ordinary field arithmetic and powering are +also polynomial in `log p`; primality certification must be accounted for +separately in any variable-characteristic bit-complexity claim. In particular, +trial division is sufficient for bounded prime fixtures but does not by itself +establish a polynomial primality algorithm in the bit length of `p`. + +When `n = 1`, `E = 0`, `J = ker F^0 = 0`, the flag and height list are +empty, and the empty product gives `N = 1`. The recovered unit is nonzero and +forms a basis, so `P` is its single coordinate column. This covers `F_p` +without introducing a height-zero variable. The zero-dimensional zero ring +is outside the input contract. + +## 7. Scope, credit and remaining work + +The criterion establishes the promised algebra class from a checked common- +basis multiplication table over `F_p`, and constructs an isomorphism to its +standard monomial model. The written theorem covers every such dimension; +the package's finite fixtures corroborate it and are not a proof-kernel check. + +The immediate source is Ali Romman's +[PR5459 at `bef3575ddb19c44434a7e2460a353eac7c4d9387`](https://github.com/aliromman/integer-mult-bounds/blob/bef3575ddb19c44434a7e2460a353eac7c4d9387/research/frobenius-tensor-characters/README.md), +which supplies the unequal-height family, height flag and explicit +recognition/transporter handoff. His [PR5316](https://github.com/CrocSwap/integer-mult-bounds/pull/5316) +supplies the truncated-polynomial predecessor. Nick Petalas's +[PR5252](https://github.com/CrocSwap/integer-mult-bounds/pull/5252) supplies +the finite-etale comparison, nilpotent follow-up and tensor normalization +context; David Ganz and the retained atlas lineage retain their credit. +Nilradicals, tangent generators, [Nakayama's lemma](https://stacks.math.columbia.edu/tag/00DV) +and truncated-polynomial presentations are classical commutative algebra. +Section 4 gives the finite nilpotent argument used here directly. No general literature +priority is claimed for this criterion. + +Open next questions are the reduction from an independently based input +tensor to this checked table, with certified factor maps, and an extension +to supplied non-prime finite fields with the appropriate semilinear +Frobenius calculations. Neither follows merely by applying the present +`F_p`-linear kernel routine. Determinant-character extraction can subsequently +use the verified heights under its separately pinned theorem. Physical +coefficient preparation, native realization, precision, movement, supplier +admission and a new multiplication exponent remain outside this result. + +Prepared by apoursh with substantial OpenAI Codex assistance. Apache-2.0. +No independent human or formal proof-kernel acceptance is claimed. diff --git a/research/frobenius-algebra-recognition/README.md b/research/frobenius-algebra-recognition/README.md new file mode 100644 index 0000000000..bd119b93ad --- /dev/null +++ b/research/frobenius-algebra-recognition/README.md @@ -0,0 +1,149 @@ +# Recognize Frobenius-truncated prime-field algebra tables + +Given a nonzero multiplication table over a prime field `F_p`, this package +decides whether it is isomorphic to + +``` +F_p[x_1,...,x_r] / (x_i^(p^h_i)), h_i >= 1, +``` + +recovers the height multiset, and constructs a verified monomial change of +basis and its inverse. The input uses one common basis for both inputs and +the output; the unit need not be a coordinate vector and is recovered. +The empty height list represents `F_p`. + +This answers the supplied prime-field algebra-table part of +[Ali Romman's recognition handoff in PR5459](https://github.com/CrocSwap/integer-mult-bounds/pull/5459). +The [canonical investigation thread](https://github.com/CrocSwap/integer-mult-bounds/discussions/5493) +records the advance claim and public status. There is no new kappa, physical +supplier, arbitrary tensor isotopy recognizer, or formal proof-kernel result. + +## Criterion and implementation + +After checking the commutative, associative and unital laws, let `F(a)=a^p`, +let `E` be the least integer with `p^E >= n`, and compute + +``` +J = ker(F^E), +V_e = (ker(F^e) + J^2)/J^2, +d_e = dim(V_e) - dim(V_(e-1)). +``` + +The table belongs to the displayed family if and only if `codim J = 1` +and `p^(sum e*d_e) = n`. Height `e` occurs `d_e` times. Actual kernel lifts +give tangent generators and hence a surjection from the proposed model; +dimension equality makes it an isomorphism. [PROOF.md](PROOF.md) proves both +directions, the nilradical bound, coordinate invariance, constructive witness +and polynomial complexity for fixed `p`. + +The order of operations matters: Frobenius induced on `J/J^2` is always zero. +Taking its kernel there would incorrectly assign height one to +`F_2[t]/(t^4)`. We instead take the kernels in the full algebra and then +project them to the tangent quotient. + +[`recognize.py`](recognize.py) exports `recognize(p, table)` and +`validate_witness(p, table, witness)`. Structure constants use +`table[i][j][k]`; integer coefficients are normalized modulo `p`. Malformed +input raises `ValueError`. A well-formed table outside the family returns +`status="rejected"` with its reason and available diagnostics. + +An accepted result contains `heights`, `generators`, `unit`, +`monomial_exponents`, `transporter` (a list of columns), and `inverse` +(matrix rows). Exponent tuples are lexicographic, last coordinate fastest. +The witness checker verifies generator relations, all monomial columns, +both inverse identities and every model basis product. It does not trust +the computed radical or height flag. Primality uses trial division, so the +implementation does not claim polynomial primality testing in `log p`. + +## Evidence and reproduction + +The package uses only the Python standard library. In CPython 3.12.14, +the registered normal and optimized commands check: + +- 46 positive presentations over primes 2, 3, 5 and 7, through dimension 16, + including mixed heights, changes mixing the unit and radical, a + noncoordinate one-dimensional unit, and a hidden short generator; + 3,217 independent basis-product identities. +- Nine nonmember controls, six malformed inputs, two coefficient-normalization + controls and seven rejected witness mutations. The nonmembers include + nonlocal algebras, a nonsplit residue field, extra relations, failed algebra + laws, and `F_2[x,y,z]/(x^2+yz,y^2,z^2)`: dimension eight, recovered heights + `(1,1,2)`, predicted dimension sixteen. +- An independent bitset/finite-span oracle covers all 525 commutative fixed-unit + tables: four two-dimensional `F_2` tables, 512 three-dimensional `F_2` + tables and nine two-dimensional `F_3` tables. Exactly 64 of the 512 + three-dimensional tables are associative; their nilradical dimensions + 0, 1 and 2 occur 24, 24 and 16 times respectively. +- Complete unit-fixing basis orbits of both four-dimensional target algebras over `F_2`: + 1,344 basis changes per target yield 336 cyclic and 56 elementary distinct + tables. Every accepted transporter is checked independently. This is not + an enumeration of all `2^24` four-dimensional commutative fixed-unit tables. + +From the repository root, run the four bounded commands in `VERIFY.json`: + +```sh +python3.12 -B scripts/research_package.py --package research/frobenius-algebra-recognition +``` + +The launcher checks source metadata and uses a fresh bytecode-cache namespace +for each command. Expected markers include `PASS_FROBENIUS_ALGEBRA_RECOGNITION` +and `PASS_REGISTERED_RESEARCH_PACKAGE`. Both verifiers accept `--json` for +deterministic reports. Their direct Git-free forms, also suitable for a +checked committed-package export, are: + +```sh +python3.12 -I -B -X pycache_prefix=/tmp/frobenius-fresh-cache research/frobenius-algebra-recognition/verify.py --json +python3.12 -I -B -X pycache_prefix=/tmp/frobenius-fresh-cache research/frobenius-algebra-recognition/check_exhaustive.py --json +``` + +Use a fresh cache path for each replay; repeat with `-O` for the optimization +control. Explicit exceptions implement all verification conditions, so +optimized Python cannot remove them. Finite tests corroborate the written +all-dimension theorem; they do not replace a mathematical review. + +## Scope and provenance + +Base `32890bc5de034ab8fc93ac88ead7279a6a416d04`, priority revision 7. +The `formal-interface-lemma` card is retained verbatim in `TASK.json`, with +the changed scope explicitly recorded: a written algebra-recognition theorem +and implementation, not a proof-assistant build or the card's acceptance gate. +The selected record and retained predecessor notes are provenance-only pins +in `SOURCES.json`; replay has no external scientific inputs, network calls, +or dependency on an unmerged predecessor commit. + +Ali Romman's PR5459 at `bef3575ddb19c44434a7e2460a353eac7c4d9387` supplies +the unequal-height family, height flag and recognition handoff. His PR5316 +at `c777c9a4b5f50a0e1561b2e24304486f40e8d001` supplies the univariate +predecessor. Nick Petalas's PR5252 at +`07e6f55d18d2d3fd6dcea19bd642d71657c5fe14` supplies the etale comparison, +normalization and nilpotent follow-up. David Ganz and the retained atlas +lineage retain their credit. No pending executable or source archive is +imported. The proof uses classical commutative algebra, including the finite +nilpotent form of [Nakayama's lemma](https://stacks.math.columbia.edu/tag/00DV); +no general literature-priority claim is made. + +The advance overlap check covered the live handoff, relevant all-state PR +keyword searches and a Frobenius Discussion search. Sparse local search +covered only 5 of 7,402 tracked notes. Neither this coverage nor an absent +keyword match proves novelty. The separately claimed finite-etale recognition +and native/caller/CRT work are outside this package. + +## Open next questions + +1. **Recover a compatible algebra table from an arbitrary three-factor tensor.** + This would remove the remaining coordinate/isotopy promise. Start with a + faithful regular nucleus action and verify both input transports and the + output map before using this recognizer. No such reconstruction is supplied. +2. **Extend to supplied non-prime finite fields.** This would match the broader + predecessor family. Start with explicit field coordinates and the + semilinear characteristic-power Frobenius kernels; this implementation + assumes prime-field linearity and supplies no extension-field layer. + +Neither task alone supplies physical coefficient preparation, native gates, +precision/movement accounting or supplier admission. No selected construction +cold replay or proof-assistant build was needed or run. + +Prepared by **apoursh**, with substantial OpenAI Codex assistance across the +coordinator, proof, implementation and separate finite-domain audit workers. +The separate oracle is an implementation cross-check, not independent human +or proof-kernel acceptance. New contribution: Apache-2.0. diff --git a/research/frobenius-algebra-recognition/SOURCES.json b/research/frobenius-algebra-recognition/SOURCES.json new file mode 100644 index 0000000000..884b57fa8d --- /dev/null +++ b/research/frobenius-algebra-recognition/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "files": [ + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903" + }, + { + "path": "research/truncated-tensor-characters/README.md", + "usage": "provenance", + "git_blob": "9dac5ac07eb867ff2ff44bd8f033d0ac1114fb82", + "sha256": "2ebd7660dc342ea7a20c3c67dd58530b8ebf3d224ca13c5f689956338d3a32d7" + }, + { + "path": "research/etale-tensor-determinant-image/README.md", + "usage": "provenance", + "git_blob": "0f07df6ce2a8c43ea1fcc5f0081ee3532da28208", + "sha256": "2ec18042a1a63d5fd5da246f4f6060c5fb66cff338f25a2a1b95e3ea8b4f0fba" + } + ] +} diff --git a/research/frobenius-algebra-recognition/TASK.json b/research/frobenius-algebra-recognition/TASK.json new file mode 100644 index 0000000000..448c8cdd62 --- /dev/null +++ b/research/frobenius-algebra-recognition/TASK.json @@ -0,0 +1,137 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Recognize prime-field Frobenius-truncated polynomial algebras from a supplied multiplication table and return an exact monomial change of basis.", + "scope_change_reason": "Take the explicit recognition handoff in PR5459, restricted to checked commutative unital algebra tables over prime fields; a written theorem and exact implementation rather than a proof-assistant or arbitrary-tensor recognition project.", + "bottleneck_link": "Algebraic interface side result: removes the algebra-class promise in the supplied-table case of the tensor-character pipeline. It supplies no paid-profile or kappa improvement.", + "budget_minutes": 60, + "stop_rule": "One iff criterion, constructive transporter, exact positive/negative fixtures and bounded independent small-table census. Stop before arbitrary tensor isotopy, extension-field reconstruction or physical supplier work.", + "outcome": "completed", + "evidence": "PROOF.md; recognize.py; verify.py: 46 positive presentations, 3217 independent product checks, 9 nonmembers, 6 malformed inputs, 2 normalization controls, 7 witness mutations; check_exhaustive.py: 525 tiny tables and 392 positive four-dimensional orbit presentations.", + "author": "apoursh", + "ai_assistance": "Substantial OpenAI Codex assistance from coordinator, proof worker, implementation worker and separate finite-domain audit worker; not independent human or proof-kernel verification.", + "open_questions": [ + { + "question": "Can this recognition be lifted from supplied algebra tables to arbitrary three-factor tensors?", + "why_it_matters": "It would remove the remaining input-coordinate and isotopy promise.", + "first_step": "Recover a faithful regular nucleus action and prove compatible input/output transport before invoking this table recognizer.", + "blocked_by": "No arbitrary-tensor nucleus/regularity/transport reconstruction is supplied here." + }, + { + "question": "Can this recognition extend to supplied non-prime finite fields?", + "why_it_matters": "It would match the broader predecessor family.", + "first_step": "Implement explicit field coordinates and semilinear characteristic-power Frobenius kernels.", + "blocked_by": "Current input and linear algebra assume prime fields." + } + ], + "predecessors": [ + { + "pr": 5459, + "head": "bef3575ddb19c44434a7e2460a353eac7c4d9387", + "usage": "Ali Romman unequal-height family and recognition handoff; context only, no imported pending executable" + }, + { + "pr": 5316, + "head": "c777c9a4b5f50a0e1561b2e24304486f40e8d001", + "usage": "Ali Romman univariate nilpotent family" + }, + { + "pr": 5252, + "head": "07e6f55d18d2d3fd6dcea19bd642d71657c5fe14", + "usage": "Nick Petalas etale normalization, arbitrary tensor extraction and nilpotent question" + } + ], + "overlap": { + "checked_utc": "2026-10-25T04:30:00Z", + "live_handoff": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19169304", + "queries": [ + "Frobenius recognition", + "truncated recognize", + "5459", + "local algebra transporter" + ], + "coverage": "Live handoff and relevant all-state GitHub PR keyword search; local overlap helper searched 5 of 7402 tracked notes. No complete Discussion/diff/unpublished-work coverage claimed. Live Discussion search for Frobenius also checked.", + "separation": "Finite-etale tensor recognition is separately claimed by aliromman. Ten current native/caller/CRT followups are separately claimed by JoyboyBrian. This task is supplied-table nilpotent recognition." + }, + "coordination_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5493", + "completion_refresh": { + "checked_utc": "2026-10-25T04:34:33Z", + "canonical_main": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "priority_revision": 7, + "result": "Canonical upstream unchanged; fresh all-state Frobenius recognition PR query adds no competing supplied-table claim. Keyword-search coverage limits remain." + } +} diff --git a/research/frobenius-algebra-recognition/VERIFY.json b/research/frobenius-algebra-recognition/VERIFY.json new file mode 100644 index 0000000000..84f85a72e4 --- /dev/null +++ b/research/frobenius-algebra-recognition/VERIFY.json @@ -0,0 +1,63 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "-W", + "error", + "{package}/verify.py", + "--json" + ], + "timeout_seconds": 120, + "checks": "Exact positive and negative algebra tables, independent transporter products, recovered-unit and hidden-generator charts, normalization and malformed-input controls, and witness mutations." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-W", + "error", + "-O", + "{package}/verify.py", + "--json" + ], + "timeout_seconds": 120, + "checks": "Exact positive and negative algebra tables, independent transporter products, recovered-unit and hidden-generator charts, normalization and malformed-input controls, and witness mutations." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-W", + "error", + "{package}/check_exhaustive.py", + "--json" + ], + "timeout_seconds": 120, + "checks": "Independent finite-span/bitset census of 525 tiny tables and complete unit-fixing positive GL4 target orbits (392 distinct tables)." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-W", + "error", + "-O", + "{package}/check_exhaustive.py", + "--json" + ], + "timeout_seconds": 120, + "checks": "Independent finite-span/bitset census of 525 tiny tables and complete unit-fixing positive GL4 target orbits (392 distinct tables)." + } + ] +} diff --git a/research/frobenius-algebra-recognition/check_exhaustive.py b/research/frobenius-algebra-recognition/check_exhaustive.py new file mode 100644 index 0000000000..9c0cd2f7c2 --- /dev/null +++ b/research/frobenius-algebra-recognition/check_exhaustive.py @@ -0,0 +1,244 @@ +#!/usr/bin/env python3 +"""Independent tiny-field and target-orbit checks for recognize.py. + +The oracle uses F2 bitsets and complete vector-space enumeration, not the +recognizer's Gaussian elimination or Frobenius filtration implementation. +It is a finite regression certificate; the iff theorem is proved separately. +""" + +import argparse +import importlib.util +import json +from itertools import product +from pathlib import Path + + +def load_recognizer(): + path = Path(__file__).with_name("recognize.py") + spec = importlib.util.spec_from_file_location("recognize_oracle_target", path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module.recognize + + +recognize = load_recognizer() + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def multiply_bits(left, right, table): + """F2 bilinear multiplication in an independently encoded table.""" + result = 0 + for i, row in enumerate(table): + if (left >> i) & 1: + for j, value in enumerate(row): + if (right >> j) & 1: + result ^= value + return result + + +def power_bits(value, exponent, table): + result = 1 # Every oracle table has its unit in coordinate zero. + for _ in range(exponent): + result = multiply_bits(result, value, table) + return result + + +def span_bits(vectors): + values = {0} + for vector in vectors: + values |= {value ^ vector for value in values} + return values + + +def associative_bits(table): + n = len(table) + return all( + multiply_bits(table[i][j], 1 << k, table) + == multiply_bits(1 << i, table[j][k], table) + for i, j, k in product(range(n), repeat=3) + ) + + +def coefficient_table(table): + n = len(table) + return [ + [[(value >> k) & 1 for k in range(n)] for value in row] + for row in table + ] + + +def vector_bits(vector, n): + require(isinstance(vector, list) and len(vector) == n, "bad witness vector") + require(all(type(value) is int and value in (0, 1) for value in vector), + "witness coefficients are not canonical F2 elements") + return sum(value << i for i, value in enumerate(vector)) + + +def check_witness_bits(table, witness, expected_heights): + """Check the supplied transporter without importing production checks.""" + n = len(table) + require(witness.get("status") == "accepted", "positive oracle case rejected") + require(witness.get("n") == n, "wrong witness dimension") + heights = witness.get("heights") + require(heights == expected_heights, "wrong canonical height sequence") + require(vector_bits(witness.get("unit"), n) == 1, "wrong unit") + generators = [vector_bits(vector, n) for vector in witness.get("generators", [])] + require(len(generators) == len(heights), "wrong generator count") + for generator, height in zip(generators, heights): + require(power_bits(generator, 2 ** height, table) == 0, + "generator nilpotence relation fails") + exponents = list(product(*(range(2 ** height) for height in heights))) + require(witness.get("monomial_exponents") == [list(powers) for powers in exponents], + "wrong monomial exponent order") + columns = [vector_bits(vector, n) for vector in witness.get("transporter", [])] + require(len(columns) == n == len(exponents), "wrong transporter size") + for column, powers in zip(columns, exponents): + value = 1 + for generator, exponent in zip(generators, powers): + value = multiply_bits(value, power_bits(generator, exponent, table), table) + require(column == value, "transporter column is not its declared monomial") + require(len(span_bits(columns)) == 2 ** n, "transporter is singular") + # Check every product in the alleged truncated-polynomial basis. + position = {powers: i for i, powers in enumerate(exponents)} + for i, j in product(range(n), repeat=2): + powers = tuple(a + b for a, b in zip(exponents[i], exponents[j])) + expected = 0 if any(a >= 2 ** e for a, e in zip(powers, heights)) else columns[position[powers]] + require(multiply_bits(columns[i], columns[j], table) == expected, + "transporter does not intertwine multiplication") + inverse = witness.get("inverse") + require(isinstance(inverse, list) and len(inverse) == n, "wrong inverse size") + for i, row in enumerate(inverse): + row_bits = vector_bits(row, n) + for j, column in enumerate(columns): + require((row_bits & column).bit_count() % 2 == int(i == j), + "reported inverse does not invert transporter") + + +def check_dimension_two(): + accepted = 0 + for square in range(4): + table = [[1, 2], [2, square]] + require(associative_bits(table), "unexpected nonassociative 2D oracle table") + witness = recognize(2, coefficient_table(table)) + # An element other than zero is square-zero exactly for square=0 or 1. + nilpotents = [value for value in range(1, 4) if multiply_bits(value, value, table) == 0] + expected = len(nilpotents) == 1 + require((witness.get("status") == "accepted") == expected, + "2D exhaustive oracle disagrees") + if expected: + accepted += 1 + check_witness_bits(table, witness, [1]) + require(accepted == 2, "unexpected 2D orbit count") + return {"fixed_unit_tables": 4, "associative": 4, "accepted": accepted} + + +def check_dimension_three(): + counts = {"nonassociative": 0, "nilradical_dimension_0": 0, + "nilradical_dimension_1": 0, "nilradical_dimension_2": 0} + for xx, xy, yy in product(range(8), repeat=3): + table = [[1, 2, 4], [2, xx, xy], [4, xy, yy]] + if not associative_bits(table): + counts["nonassociative"] += 1 + else: + nilpotents = [value for value in range(8) if power_bits(value, 4, table) == 0] + # These are all nilpotents: nilpotence index is at most dimension 3. + require(len(nilpotents) in (1, 2, 4), "unexpected nilradical size") + require(span_bits(nilpotents) == set(nilpotents), "nilpotents fail linearity") + counts[f"nilradical_dimension_{len(nilpotents).bit_length() - 1}"] += 1 + result = recognize(2, coefficient_table(table)) + require(result.get("status") == "rejected", "3D F2 table cannot be a p-group target") + require(counts == {"nonassociative": 448, "nilradical_dimension_0": 24, + "nilradical_dimension_1": 24, "nilradical_dimension_2": 16}, + "independent 3D enumeration counts changed") + return {"fixed_unit_tables": 512, "accepted": 0, **counts} + + +def unit_fixing_bases_four(): + for second in range(2, 16): + span_two = span_bits([1, second]) + for third in range(1, 16): + if third in span_two: + continue + span_three = span_bits([1, second, third]) + for fourth in range(1, 16): + if fourth not in span_three: + yield (1, second, third, fourth) + + +def transport_table(table, basis): + inverse = {} + for coordinates in range(16): + value = 0 + for i, column in enumerate(basis): + if (coordinates >> i) & 1: + value ^= column + require(value not in inverse, "oracle basis is singular") + inverse[value] = coordinates + return tuple(tuple(inverse[multiply_bits(left, right, table)] for right in basis) + for left in basis) + + +def check_dimension_four_orbits(): + # Independently written standard multiplication tables in monomial bases. + cyclic = [[1, 2, 4, 8], [2, 4, 8, 0], [4, 8, 0, 0], [8, 0, 0, 0]] + elementary = [[1, 2, 4, 8], [2, 0, 8, 0], [4, 8, 0, 0], [8, 0, 0, 0]] + bases = list(unit_fixing_bases_four()) + require(len(bases) == 1344, "wrong unit-fixing GL4 stabilizer size") + orbits = [] + report = {"unit_fixing_bases": len(bases)} + for name, table, heights, count in ( + ("cyclic", cyclic, [2], 336), + ("elementary", elementary, [1, 1], 56), + ): + orbit = {transport_table(table, basis) for basis in bases} + require(len(orbit) == count, "wrong independently generated target orbit size") + for changed_table in sorted(orbit): + require(associative_bits(changed_table), "transported target lost associativity") + result = recognize(2, coefficient_table(changed_table)) + check_witness_bits(changed_table, result, heights) + orbits.append(orbit) + report[f"{name}_distinct_tables"] = len(orbit) + require(not orbits[0].intersection(orbits[1]), "nonisomorphic target orbits intersect") + report["accepted_distinct_tables"] = sum(map(len, orbits)) + # Completeness here is for the two positive isomorphism orbits, not for all + # 2^24 fixed-unit commutative multiplication tables of dimension four. + report["scope"] = "complete unit-fixing positive target orbits only" + return report + + +def check_dimension_two_f3(): + for a, b in product(range(3), repeat=2): + table = [[[1, 0], [0, 1]], [[0, 1], [a, b]]] + result = recognize(3, table) + require(result.get("status") == "rejected", "2D F3 table cannot be a p-group target") + return {"fixed_unit_tables": 9, "accepted": 0} + + +def run_checks(): + return { + "status": "passed", + "f2_dimension_two": check_dimension_two(), + "f2_dimension_three": check_dimension_three(), + "f2_dimension_four": check_dimension_four_orbits(), + "f3_dimension_two": check_dimension_two_f3(), + "independent_method": "F2 bitsets, complete finite spans, target basis orbits", + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--json", action="store_true", help="emit the deterministic verification report") + args = parser.parse_args() + report = run_checks() + if args.json: + print(json.dumps(report, indent=2, sort_keys=True)) + else: + print("PASS: all 525 tiny fixed-unit tables and 392 positive 4D target presentations") + + +if __name__ == "__main__": + main() diff --git a/research/frobenius-algebra-recognition/recognize.py b/research/frobenius-algebra-recognition/recognize.py new file mode 100644 index 0000000000..875be1c29d --- /dev/null +++ b/research/frobenius-algebra-recognition/recognize.py @@ -0,0 +1,343 @@ +#!/usr/bin/env python3 +"""Exact recognition of prime-field Frobenius-truncated algebras. + +The input structure constants have convention table[i][j][k] = coefficient +of basis vector k in basis_i * basis_j. The basis need not contain the unit. +Integer coefficients are reduced modulo p. Malformed input raises ValueError; +a well-formed table outside the target class returns status="rejected". + +An accepted result includes an explicit change of basis, with transporter +stored as a list of columns and inverse stored as matrix rows. Exponent tuples +are in lexicographic order, with their last coordinate varying fastest. +validate_witness checks that certificate without running the recognition flag. + +Only Python's standard library is used. Primality uses trial division: the +fixed-prime recognition algorithm is polynomial in the algebra dimension, +but this primality check is not polynomial in the bit length of a variable p. +""" + +from itertools import product +from math import isqrt + + +def _integer(value): + return isinstance(value, int) and not isinstance(value, bool) + + +def _input(p, table): + if not _integer(p) or p < 2: + raise ValueError("p must be a prime integer") + if p != 2 and (p % 2 == 0 or any(p % d == 0 for d in range(3, isqrt(p) + 1, 2))): + raise ValueError("p must be prime") + if not isinstance(table, (list, tuple)) or not table: + raise ValueError("table must have positive dimension") + n = len(table) + normalized = [] + for plane in table: + if not isinstance(plane, (list, tuple)) or len(plane) != n: + raise ValueError("table must have shape n by n by n") + result_plane = [] + for row in plane: + if not isinstance(row, (list, tuple)) or len(row) != n: + raise ValueError("table must have shape n by n by n") + if any(not _integer(value) for value in row): + raise ValueError("structure constants must be integers") + result_plane.append([value % p for value in row]) + normalized.append(result_plane) + return normalized + + +def _basis(n): + return [[int(i == j) for i in range(n)] for j in range(n)] + + +def _multiply(left, right, table, p): + result = [0] * len(table) + for i, a in enumerate(left): + if a: + for j, b in enumerate(right): + if b: + scale = a * b + for k, value in enumerate(table[i][j]): + result[k] = (result[k] + scale * value) % p + return result + + +def _power(value, exponent, unit, table, p): + result = list(unit) + base = list(value) + while exponent: + if exponent & 1: + result = _multiply(result, base, table, p) + exponent //= 2 + if exponent: + base = _multiply(base, base, table, p) + return result + + +def _rref(matrix, p, coefficient_columns): + rows = [[value % p for value in row] for row in matrix] + pivots = [] + for column in range(coefficient_columns): + pivot = next((r for r in range(len(pivots), len(rows)) if rows[r][column]), None) + if pivot is None: + continue + row_index = len(pivots) + rows[row_index], rows[pivot] = rows[pivot], rows[row_index] + scale = pow(rows[row_index][column], -1, p) + rows[row_index] = [(scale * value) % p for value in rows[row_index]] + for r, row in enumerate(rows): + if r != row_index and row[column]: + scale = row[column] + rows[r] = [(a - scale * b) % p for a, b in zip(row, rows[row_index])] + pivots.append(column) + if len(pivots) == len(rows): + break + return rows, pivots + + +def _kernel(columns, p): + n = len(columns) + rows, pivots = _rref(list(map(list, zip(*columns))), p, n) + result = [] + for free in range(n): + if free not in pivots: + vector = [0] * n + vector[free] = 1 + for r, pivot in enumerate(pivots): + vector[pivot] = -rows[r][free] % p + result.append(vector) + return result + + +def _add_column(echelon, vector, p): + """Extend a column span in place; report whether its dimension increased.""" + reduced = [value % p for value in vector] + for pivot in sorted(echelon): + if reduced[pivot]: + scale = reduced[pivot] + reduced = [(a - scale * b) % p for a, b in zip(reduced, echelon[pivot])] + pivot = next((i for i, value in enumerate(reduced) if value), None) + if pivot is None: + return False + scale = pow(reduced[pivot], -1, p) + echelon[pivot] = [(scale * value) % p for value in reduced] + return True + + +def _apply(columns, vector, p): + return [sum(columns[j][i] * vector[j] for j in range(len(columns))) % p + for i in range(len(columns))] + + +def _inverse(columns, p): + n = len(columns) + rows = [[columns[j][i] for j in range(n)] + [int(i == j) for j in range(n)] + for i in range(n)] + reduced, pivots = _rref(rows, p, n) + if len(pivots) != n: + return None + return [row[n:] for row in reduced] + + +def _algebra_error(table, p): + n = len(table) + for i in range(n): + for j in range(i): + if table[i][j] != table[j][i]: + return "table is not commutative" + for i in range(n): + for j in range(n): + for k in range(n): + left = [sum(table[i][j][r] * table[r][k][s] for r in range(n)) % p + for s in range(n)] + right = [sum(table[j][k][r] * table[i][r][s] for r in range(n)) % p + for s in range(n)] + if left != right: + return "table is not associative" + return None + + +def _recover_unit(table, p): + n = len(table) + equations = [[table[i][j][k] for i in range(n)] + [int(j == k)] + for j in range(n) for k in range(n)] + reduced, pivots = _rref(equations, p, n) + if any(not any(row[:n]) and row[n] for row in reduced): + return None + unit = [0] * n + for r, pivot in enumerate(pivots): + unit[pivot] = reduced[r][n] + for vector in _basis(n): + if _multiply(unit, vector, table, p) != vector: + return None + if _multiply(vector, unit, table, p) != vector: + return None + return unit + + +def recognize(p, table): + """Recognize a tensor product of F_p[x]/(x**(p**h)), and return its witness.""" + table = _input(p, table) + n = len(table) + result = {"status": "rejected", "reason": "", "n": n} + error = _algebra_error(table, p) + if error is not None: + result["reason"] = error + return result + unit = _recover_unit(table, p) + if unit is None: + result["reason"] = "table has no two-sided unit" + return result + + levels, bound = 0, 1 + while bound < n: + levels += 1 + bound *= p + result["frobenius_levels"] = levels + identity = _basis(n) + kernels = [] + current = identity + if levels: + frobenius = [_power(vector, p, unit, table, p) for vector in identity] + for _ in range(levels): + current = [_apply(frobenius, column, p) for column in current] + kernels.append(_kernel(current, p)) + radical = kernels[-1] if kernels else [] + result["radical_dimension"] = len(radical) + if len(radical) != n - 1: + result["reason"] = "Frobenius radical does not have codimension one" + return result + + quotient_span = {} + for i, left in enumerate(radical): + for right in radical[i:]: + _add_column(quotient_span, _multiply(left, right, table, p), p) + square_dimension = len(quotient_span) + result["radical_square_dimension"] = square_dimension + result["tangent_dimension"] = len(radical) - square_dimension + heights, generators, flag_dimensions = [], [], [0] + for e, kernel in enumerate(kernels, 1): + for vector in kernel: + if _add_column(quotient_span, vector, p): + heights.append(e) + generators.append(list(vector)) + flag_dimensions.append(len(quotient_span) - square_dimension) + result["flag_dimensions"] = flag_dimensions + result["heights"] = heights + predicted_dimension = p ** sum(heights) + result["predicted_dimension"] = predicted_dimension + if predicted_dimension != n: + result["reason"] = "adapted Frobenius heights predict a different dimension" + return result + + sizes = [p ** height for height in heights] + exponents = [list(exponent) for exponent in product(*(range(size) for size in sizes))] + powers = [[_power(generator, exponent, unit, table, p) for exponent in range(size)] + for generator, size in zip(generators, sizes)] + columns = [] + for exponent in exponents: + column = list(unit) + for i, value in enumerate(exponent): + column = _multiply(column, powers[i][value], table, p) + columns.append(column) + inverse = _inverse(columns, p) + if inverse is None: + raise RuntimeError("recognition criterion passed but monomial columns are singular") + result.update({ + "status": "accepted", + "reason": "verified monomial basis for the recovered Frobenius heights", + "generators": generators, + "unit": unit, + "monomial_exponents": exponents, + "transporter": columns, + "inverse": inverse, + }) + validate_witness(p, table, result) + return result + + +def _witness_vectors(value, count, n, p, name): + if not isinstance(value, list) or len(value) != count: + raise ValueError(name + " has the wrong number of vectors") + for vector in value: + if not isinstance(vector, list) or len(vector) != n: + raise ValueError(name + " has a vector of the wrong dimension") + if any(not _integer(a) or not 0 <= a < p for a in vector): + raise ValueError(name + " must use canonical prime-field coordinates") + return value + + +def validate_witness(p, table, witness): + """Independently check a monomial transporter; return True or raise ValueError. + + The checker does not use Frobenius kernels, radical dimensions, flag + dimensions or the recognition decision. It verifies the declared model's + relations, all monomial columns, both inverse identities, and every basis + product in the source and target. Diagnostic fields are not certificate + premises and are deliberately ignored. + """ + table = _input(p, table) + n = len(table) + if not isinstance(witness, dict) or witness.get("status") != "accepted": + raise ValueError("witness must declare an accepted certificate") + if not _integer(witness.get("n")) or witness["n"] != n: + raise ValueError("witness dimension does not match table") + error = _algebra_error(table, p) + if error is not None: + raise ValueError(error) + unit = _witness_vectors([witness.get("unit")], 1, n, p, "unit")[0] + for vector in _basis(n): + if _multiply(unit, vector, table, p) != vector or _multiply(vector, unit, table, p) != vector: + raise ValueError("witness unit does not satisfy both identity laws") + heights = witness.get("heights") + if not isinstance(heights, list) or any(not _integer(h) or h < 1 for h in heights): + raise ValueError("heights must be positive integers") + # This bound also avoids constructing a maliciously large p**h value. + maximum_height, bound = 0, 1 + while bound < n: + maximum_height += 1 + bound *= p + if any(h > maximum_height for h in heights) or len(heights) > n: + raise ValueError("heights exceed the model dimension") + if p ** sum(heights) != n: + raise ValueError("model dimension does not match table") + generators = _witness_vectors(witness.get("generators"), len(heights), n, p, "generators") + columns = _witness_vectors(witness.get("transporter"), n, n, p, "transporter") + inverse = _witness_vectors(witness.get("inverse"), n, n, p, "inverse") + sizes = [p ** height for height in heights] + exponents = [list(exponent) for exponent in product(*(range(size) for size in sizes))] + supplied_exponents = witness.get("monomial_exponents") + if not isinstance(supplied_exponents, list) or len(supplied_exponents) != n: + raise ValueError("monomial exponents have the wrong length") + for actual, expected in zip(supplied_exponents, exponents): + if not isinstance(actual, list) or any(not _integer(a) for a in actual) or actual != expected: + raise ValueError("monomial exponents are not the declared lexicographic order") + zero = [0] * n + powers = [] + for generator, height, size in zip(generators, heights, sizes): + if _power(generator, size, unit, table, p) != zero: + raise ValueError("generator violates its truncation relation") + if _power(generator, p ** (height - 1), unit, table, p) == zero: + raise ValueError("generator has a smaller Frobenius height") + powers.append([_power(generator, a, unit, table, p) for a in range(size)]) + for column, exponent in zip(columns, exponents): + expected = list(unit) + for i, a in enumerate(exponent): + expected = _multiply(expected, powers[i][a], table, p) + if column != expected: + raise ValueError("transporter column does not equal its generator monomial") + for i in range(n): + for j in range(n): + if sum(columns[k][i] * inverse[k][j] for k in range(n)) % p != int(i == j): + raise ValueError("transporter times inverse is not the identity") + if sum(inverse[i][k] * columns[j][k] for k in range(n)) % p != int(i == j): + raise ValueError("inverse times transporter is not the identity") + monomial_index = {tuple(exponent): i for i, exponent in enumerate(exponents)} + for i, a in enumerate(exponents): + for j, b in enumerate(exponents): + combined = tuple(x + y for x, y in zip(a, b)) + expected = zero if any(x >= size for x, size in zip(combined, sizes)) else columns[monomial_index[combined]] + if _multiply(columns[i], columns[j], table, p) != expected: + raise ValueError("transporter fails a model basis-product identity") + return True diff --git a/research/frobenius-algebra-recognition/verify.py b/research/frobenius-algebra-recognition/verify.py new file mode 100644 index 0000000000..ee91366864 --- /dev/null +++ b/research/frobenius-algebra-recognition/verify.py @@ -0,0 +1,275 @@ +#!/usr/bin/env python3 +"""Exact recognition, coordinate-change and witness controls. Apache-2.0. + +Prepared by apoursh with substantial OpenAI Codex assistance. +The fixture builder does not import the recognizer's arithmetic helpers. +""" +import argparse +import copy +import importlib.util +import itertools +import json +from pathlib import Path + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def load_recognizer(): + path = Path(__file__).with_name('recognize.py') + spec = importlib.util.spec_from_file_location('recognize_local', path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def identity(n): + return [[int(i == j) for j in range(n)] for i in range(n)] + + +def inverse(matrix, p): + n = len(matrix) + rows = [list(row) + eye for row, eye in zip(matrix, identity(n))] + for col in range(n): + pivot = next((i for i in range(col, n) if rows[i][col] % p), None) + require(pivot is not None, 'singular fixture change of basis') + rows[col], rows[pivot] = rows[pivot], rows[col] + scale = pow(rows[col][col], -1, p) + rows[col] = [(x * scale) % p for x in rows[col]] + for i in range(n): + if i != col: + scale = rows[i][col] + rows[i] = [(x - scale*y) % p for x, y in zip(rows[i], rows[col])] + return [row[n:] for row in rows] + + +def product(table, x, y, p): + n = len(table) + result = [0] * n + for i, a in enumerate(x): + if a: + for j, b in enumerate(y): + if b: + for k, c in enumerate(table[i][j]): + result[k] = (result[k] + a*b*c) % p + return result + + +def model(p, heights): + bounds = [p**e for e in heights] + exponents = list(itertools.product(*(range(b) for b in bounds))) + lookup = {a: i for i, a in enumerate(exponents)} + n = len(exponents) + table = [[[0]*n for _ in range(n)] for _ in range(n)] + for i, a in enumerate(exponents): + for j, b in enumerate(exponents): + c = tuple(x+y for x, y in zip(a, b)) + if all(x < bound for x, bound in zip(c, bounds)): + table[i][j][lookup[c]] = 1 + return table + + +def rebase(table, matrix, p): + """Columns of matrix are the new basis in the old coordinates.""" + n = len(table) + inv = inverse(matrix, p) + columns = list(map(list, zip(*matrix))) + result = [] + for x in columns: + row = [] + for y in columns: + z = product(table, x, y, p) + row.append([sum(a*b for a, b in zip(r, z)) % p for r in inv]) + result.append(row) + return result + + +def scrambled_basis(n, p, variant): + rows = identity(n) + if n == 1: + rows[0][0] = p-1 + return rows + # Elementary invertible changes mix the unit, tangent and higher terms. + for k in range(3*n): + i = (k + variant) % n + j = (i + 1 + (k % (n-1))) % n + if i == j: + j = (j+1) % n + c = 1 + (k % (p-1)) + rows[i] = [(a+c*b) % p for a, b in zip(rows[i], rows[j])] + rows = rows[variant % n:] + rows[:variant % n] + return rows + + +def square_zero(p, radical_dimension): + n = radical_dimension + 1 + table = [[[0]*n for _ in range(n)] for _ in range(n)] + for i in range(n): + table[0][i][i] = table[i][0][i] = 1 + return table + + +def check_transporter_independently(p, table, witness): + columns = witness['transporter'] + n = len(table) + matrix = list(map(list, zip(*columns))) + require(inverse(matrix, p) == witness['inverse'], 'wrong inverse certificate') + target = model(p, witness['heights']) + require(len(target) == n, 'wrong model dimension') + for i in range(n): + for j in range(n): + left = product(table, columns[i], columns[j], p) + right = [sum(target[i][j][a]*columns[a][k] for a in range(n)) % p + for k in range(n)] + require(left == right, 'independent transporter endpoint mismatch') + return n*n + + +def rejection_controls(api): + fixtures = [] + fixtures.append(('square_zero_dimension', 2, square_zero(2, 3))) + twisted = square_zero(2, 3) + twisted[1][1][3] = twisted[2][2][3] = 1 + fixtures.append(('quadratic_identification', 2, twisted)) + # F2[x,y,z]/(x^2+yz,y^2,z^2): eight square-free monomials remain, + # but x has height two while y,z have height one. The model therefore + # predicts sixteen monomials; the extra mixed relation must be detected. + exponents = list(itertools.product(range(2), repeat=3)) + lookup = {a: i for i, a in enumerate(exponents)} + mixed_relation = [[[0]*8 for _ in range(8)] for _ in range(8)] + for i, a in enumerate(exponents): + for j, b in enumerate(exponents): + x, y, z = (u+v for u, v in zip(a, b)) + if x == 2: + x, y, z = 0, y+1, z+1 + if y < 2 and z < 2: + mixed_relation[i][j][lookup[(x, y, z)]] = 1 + fixtures.append(('twisted_complete_intersection', 2, mixed_relation)) + field4 = square_zero(2, 1) + field4[1][1] = [1, 1] + fixtures.append(('nonsplit_residue_field', 2, field4)) + split = square_zero(2, 1) + split[1][1] = [0, 1] + fixtures.append(('product_of_fields', 2, split)) + # F2[t]/t^3 is local but its truncation is not a characteristic power. + cube = square_zero(2, 2) + cube[1][1][2] = 1 + fixtures.append(('non_power_truncation', 2, cube)) + noncomm = square_zero(2, 2) + noncomm[1][2][1] = 1 + fixtures.append(('noncommutative', 2, noncomm)) + nonassoc = square_zero(2, 2) + nonassoc[1][1][2] = nonassoc[2][2][1] = 1 + fixtures.append(('nonassociative', 2, nonassoc)) + fixtures.append(('no_unit', 2, [[[0, 0] for _ in range(2)] for _ in range(2)])) + results = [] + for name, p, table in fixtures: + got = api.recognize(p, table) + require(got['status'] == 'rejected', 'accepted nonmember '+name) + result = {'case': name, 'reason': got['reason']} + if name == 'twisted_complete_intersection': + require(got.get('radical_dimension') == 7, 'wrong twisted radical dimension') + require(got.get('heights') == [1, 1, 2], 'wrong twisted Frobenius heights') + require(got.get('predicted_dimension') == 16, 'wrong twisted model dimension') + result.update({'heights': got['heights'], + 'predicted_dimension': got['predicted_dimension']}) + results.append(result) + return results + + +def malformed_controls(api): + cases = [(4, model(2, [1])), (True, model(2, [1])), (2, []), + (2, [[[0]] , [[0]]]), (2, [[[True]]]), + (2, [[[0.0]]])] + count = 0 + for p, table in cases: + try: + api.recognize(p, table) + except ValueError: + count += 1 + else: + raise ValueError('malformed input was accepted') + return count + + +def normalization_controls(api): + canonical = api.recognize(3, [[[2]]]) + require(canonical['status'] == 'accepted', 'normalization baseline rejected') + for coefficient in (5, -1): + got = api.recognize(3, [[[coefficient]]]) + require(got == canonical, 'integer coefficient normalization changed recognition') + require(api.validate_witness(3, [[[coefficient]]], got), + 'normalized witness did not verify') + return 2 + + +def witness_controls(api): + table = model(2, [1, 2]) + original = api.recognize(2, table) + require(original['status'] == 'accepted', 'witness control lacks positive baseline') + mutations = [] + x = copy.deepcopy(original); x['unit'] = [0]*8; mutations.append(('unit', x)) + x = copy.deepcopy(original); x['inverse'][0][0] ^= 1; mutations.append(('inverse', x)) + x = copy.deepcopy(original); x['generators'][0] = [0]*8; mutations.append(('generator', x)) + x = copy.deepcopy(original); x['heights'][0] += 1; mutations.append(('height', x)) + x = copy.deepcopy(original); x['transporter'][1][0] ^= 1; mutations.append(('column', x)) + x = copy.deepcopy(original); x['transporter'].pop(); mutations.append(('missing_column', x)) + x = copy.deepcopy(original); x['monomial_exponents'][0] = [1, 0]; mutations.append(('exponent_order', x)) + count = 0 + for name, witness in mutations: + try: + api.validate_witness(2, table, witness) + except ValueError: + count += 1 + else: + raise ValueError('accepted witness mutation '+name) + return count + + +def run(): + api = load_recognizer() + domains = [(2, []), (2, [1]), (2, [2]), (2, [3]), (2, [1, 1]), + (2, [1, 2]), (2, [2, 2]), (2, [1, 1, 1]), (2, [1, 3]), + (3, []), (3, [1]), (3, [2]), (3, [1, 1]), (5, [1]), (7, [1])] + cases, product_checks = [], 0 + for p, heights in domains: + table = model(p, heights) + for variant in range(3): + actual = table if variant == 0 else rebase(table, scrambled_basis(len(table), p, variant), p) + got = api.recognize(p, actual) + require(got['status'] == 'accepted', 'target rejected '+str((p, heights, variant))) + require(got['heights'] == heights, 'incorrect recovered heights') + product_checks += check_transporter_independently(p, actual, got) + cases.append({'p': p, 'heights': heights, 'n': len(table), 'chart': variant}) + # In this chart the short variable is hidden as x+y^2, not a coordinate axis. + table = model(2, [1, 3]) + chart = identity(16) + chart[2][8] = 1 + hidden = api.recognize(2, rebase(table, chart, 2)) + require(hidden['status'] == 'accepted' and hidden['heights'] == [1, 3], 'nonlinear lift lost') + product_checks += check_transporter_independently(2, rebase(table, chart, 2), hidden) + cases.append({'p': 2, 'heights': [1, 3], 'n': 16, 'chart': 'hidden_short_generator'}) + trap = api.recognize(2, model(2, [2])) + require(trap['heights'] == [2], 'tangent Frobenius trap') + return {'status': 'PASS_FROBENIUS_ALGEBRA_RECOGNITION', + 'positive_presentations': len(cases), 'positive_cases': cases, + 'independent_basis_product_checks': product_checks, + 'nonmember_controls': rejection_controls(api), + 'malformed_controls': malformed_controls(api), + 'normalization_controls': normalization_controls(api), + 'witness_mutations_rejected': witness_controls(api), + 'scope': 'Supplied common-basis prime-field algebra tables; no arbitrary tensor recognition or new kappa.'} + + +if __name__ == '__main__': + parser = argparse.ArgumentParser() + parser.add_argument('--json', action='store_true') + args = parser.parse_args() + result = run() + if args.json: + print(json.dumps(result, sort_keys=True, indent=2)) + else: + print(result['status'], json.dumps({k: v for k, v in result.items() + if k not in ('status', 'positive_cases')}, sort_keys=True))