diff --git a/research/frobenius-product-characters/PROOF.md b/research/frobenius-product-characters/PROOF.md new file mode 100644 index 0000000000..a9f931a378 --- /dev/null +++ b/research/frobenius-product-characters/PROOF.md @@ -0,0 +1,350 @@ +# Determinant characters for split products of Frobenius-truncated algebras + +This note answers the split-product part of the open question in +[Ali Romman's PR5637](https://github.com/CrocSwap/integer-mult-bounds/pull/5637). +The local factor models and a decomposition certificate are supplied. We +derive their product's automorphism determinant image, full covariant tensor +stabilizer image, special-linear orbit label and constructive transporters. +We do not recognize an arbitrary tensor or recover a decomposition from it. +The result is an algebraic interface statement and does not improve kappa. + +## 1. Models and the main formula + +Fix one explicit finite field K = F_q of characteristic p. All algebra +automorphisms and tensor factor maps below are K-linear; coefficient-field +automorphisms are not allowed. Let s >= 1 +and define + + B_j = K[x_(j,1),...,x_(j,r_j)] / (x_(j,i)^(p^h_(j,i))), + A = product_(j=1)^s B_j, + N_j = dim_K B_j = p^(sum_i h_(j,i)), + n = dim_K A = sum_j N_j. + +Each height is a positive integer. An empty height list means B_j = K +and N_j = 1. A factor's **type** is its sorted height list. Within a factor, +use the monomial basis with lexicographically ordered exponent tuples. The +canonical product model orders factor types lexicographically; equal types +are consecutive copies of the same model. + +Set L = q-1, and for every variable define the integer + + E_(j,i) = N_j * (p^h_(j,i) - 1) / 2. + +It is integral: for odd p the second factor is even; for p = 2 every factor +containing a variable has even dimension. Include a swap generator precisely +when q is odd and some type occurs at least twice with odd component +dimension. Its exponent is T = L/2. Set + + g = gcd(L, all E_(j,i), T if that swap generator exists), + H_g = {c^g : c in K*}. + +The gcd of the singleton list (L) is L. This includes field factors with +empty height lists and q = 2, where L = g = 1. Every N_j in this family is +odd when q is odd; the dimension condition identifies the sign's source. + +**Theorem.** The image of Aut_K(A) under determinant is exactly H_g. For +multiplication mu_A and the covariant action on A* tensor A* tensor A, the +full stabilizer determinant image is + + Delta(mu_A) = {(u,v,w) in (K*)^3 : uvw in H_g} + = {(u,v,w) : (uvw)^(L/g) = 1}. + +It has L^3/g elements. The general-linear orbit of mu_A contains exactly g +orbits under SL_n(K)^3. Every allowed determinant triple is attained by an +explicit autotopism. For tensors supplied with verified factor maps, the +canonical type multiset and Section 6's label completely decide +special-linear equivalence. + +## 2. Local type and local determinant character + +We restate the local argument of PR5459 to identify the input to the product +calculation. In B = K[x_1,...,x_r]/(x_i^(p^h_i)), let J = (x_1,...,x_r). +An element with nonzero constant term is a unit by a finite geometric +series; all elements of J are nilpotent. Thus B is local with residue field +K. Its only idempotents are zero and one: one of e and 1-e is a unit, and +e(1-e) = 0 determines an idempotent e. + +The tangent quotient J/J^2 has the variables as a basis. Its intrinsic +height flag is + + V_e = (ker(a -> a^(p^e)) + J^2)/J^2. + +These kernels are K-subspaces even though the power map is semilinear over +an extension field. Frobenius removes mixed terms. A nonzero linear term +in x_i survives the p^e power exactly when h_i > e, and no term of degree +at least two can cancel its degree-p^e monomial. Therefore V_e is exactly +the span of variables of height at most e. Its dimension increments recover +the height multiset. Two displayed local factors are isomorphic if and only +if their types agree; equal dimension alone is insufficient. + +An automorphism's tangent map preserves this flag. Conversely, an invertible +flag-preserving linear substitution respects the defining power relations: +a variable of height h is sent only to variables whose heights are at most +h. Its inverse preserves the same flag, so this substitution is an +automorphism. A general automorphism and its linear substitution induce the +same map on the associated graded algebra for powers of J. A monomial basis +ordered by total degree shows that they have equal determinants. + +The flag-preserving group is generated by allowed elementary substitutions +and diagonal scalings. For an allowed substitution x_i -> x_i + c*x_k, +the monomial expansion is triangular when ordered by x_i exponent, with +diagonal one. Its determinant is one. Scaling x_i -> c*x_i has determinant +c^E_i: the sum of the x_i exponents over the N monomials is + + E_i = N * (p^h_i - 1) / 2. + +Elementary and diagonal matrices generate the full general-linear group +within each equal-height block, while the other allowed elementary matrices +generate the off-diagonal flag-preserving part. Thus the local determinant +image is generated exactly by the subgroups {c^E_i : c in K*}. With an empty +height list, the K-algebra K has only the identity automorphism. + +## 3. Primitive idempotents and the permutation contribution + +An idempotent of A has each coordinate zero or one. The nonzero primitive +idempotents are precisely the e_j supported on a single factor: any +idempotent supported on more than one factor splits into nonzero orthogonal +idempotents. Algebra automorphisms preserve this intrinsic property. + +An automorphism sending e_j to e_k restricts to an isomorphism e_j A -> e_k A, +so those factors have the same type. Conversely, any permutation among +copies of one type, together with an independent automorphism on each factor, +defines an automorphism of A. These are all the possibilities; there are +no additional maps mixing primitive factors. + +Factorwise automorphisms contribute the product of their local determinants. +Swapping two identical factors of dimension N swaps N pairs of matching +basis vectors, so its determinant is (-1)^N. This remains true for blocks +separated by other blocks: those same N basis-vector transpositions describe +the operation. Equivalently, conjugate by a fixed reordering that places the +copies together. For any allowed permutation the sign contribution is + + product_over_types type_permutation_sign^(dimension_of_that_type). + +Hence signs contribute only for repeated isomorphic odd-dimensional factors +in odd characteristic. In characteristic two every sign is one. Unequal +types cannot be swapped, even when they have the same dimension. + +The finite group K* is cyclic of order L. Relative to a generator zeta, the +determinant generators have exponents E_(j,i) and, when present, T = L/2. +They generate precisely = H_g. Each generator is attained by a +literal variable scaling or permitted block transposition. This proves +the automorphism image and its attainment. + +## 4. Unit determinants and the full tensor stabilizer + +For a unit a = (a_j), multiplication by a_j is triangular on its monomials +ordered by total degree. Its constant term c_j is on every diagonal entry. +Consequently + + det(L_a) = product_j c_j^N_j. + +This map is onto K*: choose one component and let all other components +equal one. The chosen N_j is a power of p and is coprime to L, so its scalar +constant can attain any desired determinant. For q = 2 the unit one suffices. +This uses one component dimension N_j, not the total dimension n, which +need not be coprime to L. + +We use the classical unital commutative autotopism normalization retained in +PR5252 and PR5459. Suppose invertible F,G,H satisfy + + F(x) * G(y) = H(x*y). + +Put a = F(1), b = G(1). Evaluation at one gives H(x) = F(x)*b = a*G(x). +Invertibility of F,G,H implies that multiplication by a and b is invertible, +so a and b are units. Then sigma = L_(ab)^(-1) H is a unital algebra +automorphism and + + F = L_a sigma, G = L_b sigma, H = L_(ab) sigma. + +Conversely these maps always form an autotopism. Write x = det L_a, +y = det L_b, z = det sigma. The corresponding covariant stabilizer element +is (F^(-T),G^(-T),H), with determinant triple + + (u,v,w) = (x^(-1) z^(-1), y^(-1) z^(-1), x*y*z). + +Its product is z^(-1), in H_g. Conversely, for a requested triple with +uvw in H_g, set + + z = (u*v*w)^(-1), x = v*w, y = u*w. + +The automorphism and unit determinant constructions attain these three +values and hence the requested triple. This proves the full image formula. +There are L^2 choices for the first two entries and L/g possible products, +so its cardinality is L^3/g. + +## 5. Constructive determinant witnesses + +Fix a generator zeta of K*. For a desired z in H_g, write z = zeta^k +with 0 <= k < L; membership is equivalent to g dividing k. Bezout +coefficients give + + g = b_0 L + sum_(j,i) b_(j,i) E_(j,i) + b_T T, + +omitting the final term when no swap generator exists. Scale variable (j,i) +by zeta^(b_(j,i)*k/g), and compose one fixed permitted transposition to +power b_T*k/g if needed. The resulting determinant is z. Negative +coefficients are allowed because the maps are invertible. If all character +generators are trivial, only z = 1 is requested and the identity suffices. + +For desired unit determinant x, choose a component j and an inverse r of +N_j modulo L. The unit with scalar x^r in that component and one elsewhere +has determinant x. In the trivial multiplicative group use the identity. +Together with Section 4 this constructs every allowed determinant triple. + +Primitive-element and discrete-log enumeration in an explicit finite field +suffice for a fixed q. This is not a polynomial bit-complexity claim in log q. +A different exact subgroup witness search can be used, provided it verifies +the same determinants and transported basis products. + +## 6. Supplied certificates and special-linear labels + +A tensor t: K^n x K^n -> K^n is supplied with model factor types and three +invertible matrices U,V,W, in the convention + + t(U*a,V*b) = W*mu_A(a,b). + +Columns are basis images from the declared model to the tensor. Check the +dimensions, invertibility and all n^2 model basis products. By bilinearity +these finite identities verify the supplied decomposition for all inputs. +They do not provide a procedure for discovering the certificate. + +The reference model must be fixed before comparing labels. Heights inside +each factor are sorted, and factor types are sorted lexicographically. +For another supplied component order, construct the monomial permutation +R from the canonical model to the supplied model, matching full types and +monomial coordinates. Normalize the factor maps to + + U_c = U*R, V_c = V*R, W_c = W*R. + +Thus, with d_raw = det(W)/(det(U)*det(V)), + + d = det(W_c)/(det(U_c)*det(V_c)) = d_raw/det(R), + label(t) = d^(L/g). + +Sorting type metadata alone can lose this permutation sign. If variable +order is also changed inside a supplied factor, its monomial permutation +must also be included, or the interface must require sorted heights from +the start. R changes the reference model coordinates, not the ambient +coordinates of t. + +Two choices of matching among identical factors differ by a model +automorphism, whose determinant lies in H_g, so the label is unchanged. +More generally, two valid certificates from the same canonical model differ +by a tensor stabilizer. Their determinant products differ by an element of +H_g. The label is therefore independent of the certificate. + +For completeness, let G = GL_n(K)^3 and S = SL_n(K)^3. The determinant map +G -> (K*)^3 has kernel S. Since S is normal, its orbits within a fixed +G-orbit correspond to cosets of the stabilizer determinant image. The product +map identifies these cosets with K*/H_g. The map d -> d^(L/g) has kernel +H_g, so its value is a complete label, with exactly g possible values. + +Different type multisets cannot be general-linearly equivalent. An isotopy +between multiplication in two unital commutative algebras normalizes exactly +as in Section 4, using units in the target algebra, to an algebra isomorphism. +It must match primitive idempotents and then local types. Conversely a type +matching gives a literal product algebra isomorphism. For verified +certificates over the same explicit field, therefore, + + SL-equivalent iff canonical type multisets agree and labels agree. + +Different presentations of the finite field need an explicit, checked field +isomorphism before their element-valued labels can be compared. + +## 7. Determinant-one transporters + +Let two normalized certificates (U_1,V_1,W_1) and (U_2,V_2,W_2) have the +same canonical model and label. Put + + a = det(U_1)/det(U_2), + b = det(V_1)/det(V_2), + c = det(W_1)/det(W_2). + +We need a model autotopism (P,Q,R_0) with determinants (a,b,c). In +Section 4's notation choose + + z = a*b/c, x = a/z, y = b/z. + +Equal labels imply (c/(a*b))^(L/g) = 1, hence z belongs to H_g. +Section 5 constructs the required automorphism and units. Then + + F = U_2 * P * U_1^(-1), + G = V_2 * Q * V_1^(-1), + H = W_2 * R_0 * W_1^(-1) + +all have determinant one and satisfy + + t_2(F*x,G*y) = H*t_1(x,y). + +Substitution in the certificate identities proves this. An executable can +also verify the three determinants and every transported basis product. +Unequal labels preclude such maps. + +## 8. Discriminating examples and boundary cases + +Over F_3, let B = F_3[x]/(x^9). Its height list is (2), dimension nine, +and local exponent 9*(9-1)/2 = 36. Since L = 2, the local automorphism +determinant image is {1}; its multiplication orbit splits into two +special-linear orbits. For B x B, a block transposition has determinant +(-1)^9 = -1. The product gcd is gcd(2,36,36,1) = 1, giving only one +special-linear orbit. A product rule using only local characters misses +this change. + +The factors F_3[x]/(x^9) and F_3[y,z]/(y^3,z^3) both have dimension nine, +but their height lists (2) and (1,1) have different tangent dimensions. +A proposed swap is not an algebra automorphism. Equal component size +does not authorize a permutation generator or component match. + +If all heights are empty, A = K^s. For s = 1 the automorphism image is +trivial and g = L. For s >= 2 and odd q, permutations add -1 and g = L/2; +in characteristic two they add nothing and g = L. This agrees with the +split finite-etale case of PR5252. For q = 2 every nonzero determinant and +label is one, and g = 1 for every model. + +Unequal component dimensions add no automorphism generators, but their block +ordering still affects normalization of a supplied certificate. The empty +product and zero-dimensional zero algebra are excluded. An empty height +list inside a nonempty product is a valid field factor. + +## 9. Cost, credit and remaining obligations + +The gcd formula only needs exponents modulo L. Compute +p^(sum_i h_(j,i)) * (p^h_(j,i)-1) modulo 2L and halve its even residue +to obtain E_(j,i) modulo L without materializing a large component dimension. +Modular powers, type comparison and gcd are polynomial in the parameter bit +lengths, given p,q and the finite-field contract. Building and checking +explicit matrices is instead polynomial in the explicit algebra dimension +at fixed q. These are different size statements: a short symbolic height +list can specify an algebra too large to materialize. The executable builds +literal model dimensions and local exponents; the modular method just +described is an arithmetic consequence of the formula, not an implemented +compressed-model runtime guarantee. + +Ali Romman's [PR5459 at bef3575ddb19c44434a7e2460a353eac7c4d9387](https://github.com/aliromman/integer-mult-bounds/blob/bef3575ddb19c44434a7e2460a353eac7c4d9387/research/frobenius-tensor-characters/README.md) +supplies the local height flag and determinant character; those local +results are predecessor work. His +[PR5637 at 86389e525d3efafe236e929f6ae401c68be1d115](https://github.com/aliromman/integer-mult-bounds/blob/86389e525d3efafe236e929f6ae401c68be1d115/research/extension-field-tensor-recognition/README.md) +supplies extension-field recognition, local special-linear labels and the +explicit product handoff. [apoursh's PR5502](https://github.com/CrocSwap/integer-mult-bounds/pull/5502) +supplies the prime-field table height criterion. +[Nick Petalas's PR5252](https://github.com/CrocSwap/integer-mult-bounds/pull/5252) +supplies finite-etale tensor determinants and the normalization lineage. +David Ganz and the retained atlas framework retain their credit. Primitive +idempotents, cyclic subgroup arithmetic and unital isotopy normalization are +classical; no general literature-priority claim is made. + +Open next questions are recovery of this decomposition from an arbitrary +tensor and local factors with residue fields larger than the base. The +latter requires coefficient-field identifications, norms and additional +automorphisms; it does not follow by dropping the residue-field hypothesis. +Neither task is supplied here. Physical coefficient preparation, native +implementation, precision, movement, restoration, supplier admission and +a new multiplication exponent remain outside this result. + +The written theorem covers general finite fields. Executable coverage is +limited to the field contract and domains stated in the package's README; +finite checks are corroboration, not a proof-kernel verification. + +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-product-characters/README.md b/research/frobenius-product-characters/README.md new file mode 100644 index 0000000000..4c496014d4 --- /dev/null +++ b/research/frobenius-product-characters/README.md @@ -0,0 +1,170 @@ +# Determinant characters for split Frobenius products + +This package extends the local-algebra character interface to a nonempty finite +product of Frobenius-truncated local algebras. It supplies a written proof, +explicit prime-field determinant witnesses, and a checker for a supplied +three-factor tensor certificate. It does not discover that certificate from an +arbitrary tensor. The selected multiplication bound is unchanged. + +The direct next question is the product/component-matching handoff in Ali +Romman's [PR #5637](https://github.com/CrocSwap/integer-mult-bounds/pull/5637), +at `86389e525d3efafe236e929f6ae401c68be1d115`. The +[canonical investigation](https://github.com/CrocSwap/integer-mult-bounds/discussions/5655) +records the claim and public status. Base is +`df0137efd35e11b4445734bf612bdd4c7ebc330c`, priority revision 7. +The selected conditional kappa at that base is `62009/20000000`. + +## Result + +Let K=F_q have characteristic p and let + +``` +A = product_j B_j, +B_j = K[x_1,...,x_sj]/(x_i^(p^h_ji)), h_ji >= 1, +N_j = p^(sum_i h_ji), +E_ji = N_j (p^h_ji-1)/2. +``` + +The empty height list means B_j=K. Each factor type is its sorted height list. +Let g be the gcd of q-1 and all E_ji, additionally including (q-1)/2 when q +is odd and some factor type occurs at least twice. Then + +``` +det Aut_K(A) = {c^g : c in K*}, +Delta(mu_A) = {(u,v,w) in (K*)^3 : (uvw)^((q-1)/g) = 1}. +``` + +Here Delta uses the covariant action on `A* tensor A* tensor A`. The GL orbit +of this tensor splits into exactly g orbits under SL x SL x SL. +[PROOF.md](PROOF.md) gives the component decomposition, local characters, +permutation signs, unit determinants, and autotopism normalization. + +Two distinctions are essential. Exponents use each **local** dimension N_j, +not the total dimension. Component permutations are allowed only between +isomorphic factors, not arbitrary equal-dimensional factors. For example, +over F3 the local algebra F3[x]/x^9 has trivial automorphism determinant image, +but the product of two copies acquires determinant -1 by exchanging them. +The dimension-nine factors with heights (2) and (1,1) are not isomorphic. + +Even when the total dimension is not coprime to q-1, unit determinants still +fill K*: vary a scalar on one component, whose dimension is a power of p. +Using a single common scalar on the whole product would miss valid witnesses. + +## Supplied-certificate contract + +The executable accepts prime fields only; the written theorem covers all finite +fields. It uses canonical residues 0,...,p-1, exact integer arithmetic, and +standard-library Python. Matrices act on column vectors. A tensor is indexed +by `tensor[i][j][k]`, with k the output coordinate. + +For a supplied product model and invertible matrices U,V,W, the checker tests +every basis product in + +``` +tensor(Ua,Vb) = W mu_A(a,b). +``` + +Acceptance verifies the certificate; it is not an algorithm to find U,V,W or +the component decomposition. Malformed data and incorrect certificates are +rejected. Heights are sorted inside each component, but supplied component +order is retained. To compare orbit labels, the checker first identifies this +order with the canonical lexicographic order of factor types. The determinant +of that permutation must be included: exchanging different types can change +an unnormalized coordinate label even though it is not an algebra automorphism +of the fixed ordered model. + +`model.py` exposes `make_model`, `determinant_character`, `automorphism`, +`autotopism`, `covariant_stabilizer`, `validate_certificate`, and +`sl_transporter`. Height parameters always define the internally sorted local +model; supplied matrices must use that model's ordered monomials. The executable +materializes the algebra and uses field-element enumeration; it makes no +polynomial bit-complexity claim in binary-encoded heights or log p. + +The code constructs automorphism and covariant stabilizer witnesses for every +admissible determinant request. The inverse-input convention is explicit: +an autotopism F(a)G(b)=H(ab) acts as `(F^-T,G^-T,H)` on the tensor. It also +constructs determinant-one maps between certified tensors with equal types +and canonical orbit labels, checking their determinants and every transported +basis product. + +## Verification + +From the repository root, with Python 3.12: + +```sh +python3.12 -B scripts/research_package.py --package research/frobenius-product-characters +``` + +For an exported package and its three declared proof-source inputs: + +```sh +python3.12 -I -B research/frobenius-product-characters/verify.py +python3.12 -I -O -B research/frobenius-product-characters/verify.py +``` + +Checks use explicit exceptions and remain active with optimizations enabled. +`SOURCES.json` pins the exact retained predecessor proof bytes, and the direct +verifier authenticates their hashes without Git. No predecessor executable is +imported. Finite enumeration corroborates the proof only in its stated domains; +it is not proof-kernel verification or independent human review. + +The separate checker enumerates all 40,487 matrices across six domains of +dimension at most three over F2 or F3: 22,854 are invertible and 23 are algebra +automorphisms. It checks 2,372 normalized autotopisms directly on basis products. +Separate polynomial substitution oracles exhaust all 4,374 automorphisms of +F3[x]/x^9 and all 500 automorphisms of F5[x]/x^5. The moderate product tests +accept 44 determinant triples and reject 36 outside the predicted image. + +Literal covariant coefficient-index checks over F5 and F7 accept 104 triples +and reject 176. Nonlinear substitution controls reject omitting the input +transpose. Twelve malformed or changed certificate controls are rejected. +Independent factor bases in dimension nine and component-order normalization +in dimension ten exercise the supplied-certificate interface; equal-label +special-linear transport succeeds and unequal-label transport is rejected. +These are bounded finite domains, not enumeration of all larger product +algebras. Each direct run takes about one second on the development machine. + +The selected-record source-binding orientation passed after materializing its +sparse inputs. That check did not replay the selected physical construction. +The written proof and executable were reviewed by separate Codex agents; +this is AI-assisted internal review, not independent human acceptance. + +## Sources, overlap and limitations + +Ali Romman's [PR #5459](https://github.com/CrocSwap/integer-mult-bounds/pull/5459) +supplies the local height-flag character formula; apoursh's +[PR #5502](https://github.com/CrocSwap/integer-mult-bounds/pull/5502) supplies the +intrinsic height flag. Nick Petalas's +[PR #5252](https://github.com/CrocSwap/integer-mult-bounds/pull/5252) supplies +the finite-etale determinant-image precedent and autotopism normalization. +Their retained files are pinned at the base in `SOURCES.json`. David Ganz and +the atlas lineage retain credit for the character/orbit framework. PR #5637 +is the pending handoff source, not an executable dependency of this package. + +Overlap checks covered current main guidance, the newest live handoffs and +bounded all-state PR searches for product/Frobenius/component terms. Sparse +local notes, arbitrary historical diffs and unpublished work were not completely +searched. No literature-priority claim follows from those checks. +`TASK.json` explicitly changes the formal-interface-lemma card to this written +algebraic interface proof; no Lean formalization is claimed. + +## Open next questions + +- Recover the product decomposition and three factor maps from an arbitrary + tensor. This would remove the supplied-certificate premise. Start with the + nucleus regular-module test and primitive idempotents, then apply the local + height recognizer. A complete decomposition algorithm and complexity bound + remain missing here. +- Allow nontrivial residue fields. This would cover nonsplit components. First + specify field embeddings and isomorphisms and account for their determinants; + the current proof assumes every residue field is K. +- Realize a certified tensor in a named native producer/consumer pair. A bound + improvement requires paying representation, coefficients, movement, precision + and restoration. No such physical construction or invoice is supplied here. + +## Credit + +New product proof and implementation: apoursh, with substantial OpenAI Codex +assistance, including a separate finite checker and proof audit. Predecessor +methods and notices retain the attribution above. Apache-2.0. No selected cold +replay, proof-assistant build, or independent human acceptance is claimed. diff --git a/research/frobenius-product-characters/SOURCES.json b/research/frobenius-product-characters/SOURCES.json new file mode 100644 index 0000000000..0ae2169d40 --- /dev/null +++ b/research/frobenius-product-characters/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/frobenius-tensor-characters/README.md", + "usage": "input", + "git_blob": "b62f9a906e6ed49605684cca52a221f064924461", + "sha256": "31573ba91ac69caff5b8e5a42ce7fd0d80a6d54673c08d7f225c9ee08e0e0893" + }, + { + "path": "research/frobenius-algebra-recognition/PROOF.md", + "usage": "input", + "git_blob": "0a0b7d1fe48576be453df5aa5de0cc66463352fa", + "sha256": "726d9c294f0b4b9085e3994ffb8c93737822b78d6f5d0c63f81e36b718419e28" + }, + { + "path": "research/etale-tensor-determinant-image/README.md", + "usage": "input", + "git_blob": "0f07df6ce2a8c43ea1fcc5f0081ee3532da28208", + "sha256": "2ec18042a1a63d5fd5da246f4f6060c5fb66cff338f25a2a1b95e3ea8b4f0fba" + } + ] +} diff --git a/research/frobenius-product-characters/TASK.json b/research/frobenius-product-characters/TASK.json new file mode 100644 index 0000000000..daf7580902 --- /dev/null +++ b/research/frobenius-product-characters/TASK.json @@ -0,0 +1,110 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c", + "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": "For split products of Frobenius-truncated local algebras with supplied and checked three-factor maps, prove the component-matching and determinant-character formula and construct exact prime-field witnesses.", + "scope_change_reason": "Handoff-first follow-up to PR5637: the local arbitrary-tensor and extension-field cases are already covered. This is a written algebraic interface proof with finite verification, not the card's proof-assistant formalization.", + "bottleneck_link": "Algebraic side result: extends the determinant-character interface and SL orbit classification to split products. It does not price any native supplier or alter the selected multiplication bound.", + "budget_minutes": 60, + "stop_rule": "Stop after a self-contained product proof, explicit prime-field witnesses, independent bounded enumeration and rejection controls, and reproducible package checks; do not broaden to arbitrary tensor recognition or non-split residue fields.", + "outcome": "completed", + "evidence": "PROOF.md: general finite-field theorem. verify.py: 40487 matrices across six complete tiny GL domains (22854 invertible,23 automorphisms),2372 normalized autotopisms,4374+500 complete local substitutions,44/36 moderate determinant triple accepts/rejects,104/176 covariant accepts/rejects,nonlinear transpose controls,12 certificate mutations. Separate Codex implementation and proof review; no independent human review.", + "author": "apoursh", + "ai_assistance": "Substantial OpenAI Codex assistance: task selection, proof drafting, implementation and separate finite checker; no independent human or proof-assistant verification.", + "open_questions": [ + { + "question": "Recover a split-product decomposition and component transporters from an arbitrary multiplication tensor.", + "why_it_matters": "Removes the supplied-decomposition certificate premise from this interface.", + "first_step": "Combine the nucleus regular-module test with primitive idempotent recovery, then apply the local height-flag recognizer componentwise and check all products.", + "blocked_by": "A complete decomposition algorithm with correctness and complexity guarantees is not supplied here." + }, + { + "question": "Extend component matching and characters to nontrivial residue fields.", + "why_it_matters": "Covers nonsplit commutative algebras over the ground field.", + "first_step": "Specify field embeddings and isomorphisms and compute the determinant contribution of residue-field automorphisms before composing local factors.", + "blocked_by": "The split residue-field hypothesis is used throughout this proof and executable." + }, + { + "question": "Realize a certified product tensor in a named paid native caller.", + "why_it_matters": "A character interface alone cannot improve kappa.", + "first_step": "Identify producer and consumer maps and charge representation, coefficients, movement, precision and restoration.", + "blocked_by": "No physical construction or complete paid invoice is provided." + } + ], + "coordination": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5655", + "chooser_seed": "681f0a658111610f1515559fc056b47e", + "overlap_coverage": "Current main guidance and selected bindings; newest live handoffs including PR5637; bounded all-state PR searches for product/Frobenius/component terms. Sparse local notes, arbitrary historical diffs and unpublished work remain outside coverage." +} diff --git a/research/frobenius-product-characters/VERIFY.json b/research/frobenius-product-characters/VERIFY.json new file mode 100644 index 0000000000..eb9180fc75 --- /dev/null +++ b/research/frobenius-product-characters/VERIFY.json @@ -0,0 +1,33 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/frobenius-tensor-characters/README.md", + "research/frobenius-algebra-recognition/PROOF.md", + "research/etale-tensor-determinant-image/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Exact split-product models, independent finite automorphism enumeration, determinant witnesses, supplied tensor certificates and failure controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "The same explicit checks with isolated imports and Python optimizations enabled." + } + ] +} diff --git a/research/frobenius-product-characters/model.py b/research/frobenius-product-characters/model.py new file mode 100644 index 0000000000..b193be0fe9 --- /dev/null +++ b/research/frobenius-product-characters/model.py @@ -0,0 +1,413 @@ +#!/usr/bin/env python3 +"""Exact split Frobenius-product character witnesses over prime fields. + +Matrices use row-major storage; columns are basis images. Input coordinates +must be canonical integers from 0 through p-1. A table uses table[i][j][k] +for the kth coefficient of e_i*e_j. Certificates use T(Ua,Vb)=W*mu(a,b), from a literal model to a +supplied tensor. Heights are sorted within factors; supplied factor order +is preserved. Labels explicitly normalize that order to lexicographic order. + +This executable handles prime fields only. Trial division, primitive-root +search and a direct discrete-log loop are finite fixture algorithms, not a +polynomial bit-complexity claim for variable characteristic. No recognition +of an arbitrary supplied tensor is attempted. + +Prepared by apoursh with substantial OpenAI Codex assistance. Apache-2.0. +""" + +from itertools import product +from math import gcd, isqrt + + +def _integer(value): + return isinstance(value, int) and not isinstance(value, bool) + + +def _prime(p): + 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") + + +def _components(components): + if not isinstance(components, (list, tuple)) or not components: + raise ValueError("a product must have at least one component") + result = [] + for heights in components: + if not isinstance(heights, (list, tuple)): + raise ValueError("each component must be a height list") + if any(not _integer(h) or h < 1 for h in heights): + raise ValueError("heights must be positive integers") + result.append(sorted(heights)) + return result + + +def _nonzero(value, p, name): + if not _integer(value) or not 1 <= value < p: + raise ValueError(name + " must be a nonzero canonical field element") + + +def identity(n): + if not _integer(n) or n < 1: + raise ValueError("matrix dimension must be a positive integer") + return [[int(i == j) for j in range(n)] for i in range(n)] + + +def transpose(matrix): + if not isinstance(matrix, (list, tuple)) or not matrix: + raise ValueError("transpose requires a nonempty square matrix") + if any(not isinstance(row, (list, tuple)) or len(row) != len(matrix) for row in matrix): + raise ValueError("transpose requires a square matrix") + if any(not _integer(x) or x < 0 for row in matrix for x in row): + raise ValueError("matrix entries must be nonnegative field integers") + return [list(row) for row in zip(*matrix)] + + +def _matrix(matrix, n, p, name): + if not isinstance(matrix, (list, tuple)) or len(matrix) != n: + raise ValueError(name + " must be an n by n matrix") + result = [] + for row in matrix: + if not isinstance(row, (list, tuple)) or len(row) != n: + raise ValueError(name + " must be an n by n matrix") + if any(not _integer(x) or not 0 <= x < p for x in row): + raise ValueError(name + " entries must be canonical field integers") + result.append(list(row)) + return result + + +def matmul(left, right, p): + _prime(p) + if not isinstance(left, (list, tuple)) or not left: + raise ValueError("multiplication requires nonempty square matrices") + n = len(left) + left, right = _matrix(left, n, p, "left matrix"), _matrix(right, n, p, "right matrix") + return [[sum(left[i][k] * right[k][j] for k in range(n)) % p + for j in range(n)] for i in range(n)] + + +def _apply(matrix, vector, p): + return [sum(a * b for a, b in zip(row, vector)) % p for row in matrix] + + +def determinant(matrix, p): + _prime(p) + if not isinstance(matrix, (list, tuple)) or not matrix: + raise ValueError("determinant requires a nonempty square matrix") + rows = _matrix(matrix, len(matrix), p, "matrix") + answer = 1 + for column in range(len(rows)): + pivot = next((i for i in range(column, len(rows)) if rows[i][column]), None) + if pivot is None: + return 0 + if pivot != column: + rows[column], rows[pivot] = rows[pivot], rows[column] + answer = -answer % p + value = rows[column][column] + answer = answer * value % p + scale = pow(value, -1, p) + for i in range(column + 1, len(rows)): + multiplier = rows[i][column] * scale % p + rows[i] = [(a - multiplier * b) % p for a, b in zip(rows[i], rows[column])] + return answer + + +def inverse(matrix, p): + _prime(p) + if not isinstance(matrix, (list, tuple)) or not matrix: + raise ValueError("inverse requires a nonempty square matrix") + n = len(matrix) + rows = [row + eye for row, eye in zip(_matrix(matrix, n, p, "matrix"), identity(n))] + for column in range(n): + pivot = next((i for i in range(column, n) if rows[i][column]), None) + if pivot is None: + raise ValueError("matrix is singular") + rows[column], rows[pivot] = rows[pivot], rows[column] + scale = pow(rows[column][column], -1, p) + rows[column] = [x * scale % p for x in rows[column]] + for i in range(n): + if i != column: + multiplier = rows[i][column] + rows[i] = [(a - multiplier * b) % p for a, b in zip(rows[i], rows[column])] + return [row[n:] for row in rows] + + +def _table(table, n, p): + if not isinstance(table, (list, tuple)) or len(table) != n: + raise ValueError("tensor table must have shape n by n by n") + return [_matrix(plane, n, p, "tensor plane") for plane in table] + + +def _multiply(table, left, right, p): + result = [0] * len(table) + for i, a in enumerate(left): + if a: + for j, b in enumerate(right): + if b: + for k, value in enumerate(table[i][j]): + result[k] = (result[k] + a * b * value) % p + return result + + +def make_model(p, components): + """Return the literal product table, retaining the supplied factor order.""" + _prime(p) + components = _components(components) + dimensions = [p ** sum(heights) for heights in components] + offsets, offset = [], 0 + exponents = [] + for heights, size in zip(components, dimensions): + offsets.append(offset) + offset += size + exponents.append([list(a) for a in product(*(range(p ** h) for h in heights))]) + n = sum(dimensions) + table = [[[0] * n for _ in range(n)] for _ in range(n)] + unit = [0] * n + for heights, start, basis in zip(components, offsets, exponents): + index = {tuple(a): i for i, a in enumerate(basis)} + sizes = [p ** h for h in heights] + unit[start] = 1 + for i, a in enumerate(basis): + for j, b in enumerate(basis): + combined = tuple(x + y for x, y in zip(a, b)) + if all(x < size for x, size in zip(combined, sizes)): + table[start + i][start + j][start + index[combined]] = 1 + return {"p": p, "components": components, "n": n, "dimensions": dimensions, + "offsets": offsets, "exponents": exponents, "table": table, "unit": unit} + + +def model_isomorphism(p, source_components, target_components): + """Map source model columns into a reordered target with identical types.""" + source = make_model(p, source_components) + target = make_model(p, target_components) + if sorted(source["components"]) != sorted(target["components"]): + raise ValueError("component height multisets are not isomorphic") + matrix = [[0] * source["n"] for _ in range(source["n"])] + available = list(range(len(target["components"]))) + for i, kind in enumerate(source["components"]): + j = next(j for j in available if target["components"][j] == kind) + available.remove(j) + for k in range(source["dimensions"][i]): + matrix[target["offsets"][j] + k][source["offsets"][i] + k] = 1 + return matrix + + +def determinant_character(p, components): + """Return the exact index g of the algebra-automorphism determinant image.""" + _prime(p) + components = _components(components) + dimensions = [p ** sum(heights) for heights in components] + local = [[size * (p ** h - 1) // 2 for h in heights] + for size, heights in zip(dimensions, components)] + pairs = [] + seen = {} + for i, kind in enumerate(components): + key = tuple(kind) + if key in seen: + pairs.append([seen[key], i]) + else: + seen[key] = i + g = p - 1 + for exponents in local: + for exponent in exponents: + g = gcd(g, exponent) + if p % 2 and pairs: + g = gcd(g, (p - 1) // 2) + return {"p": p, "n": sum(dimensions), "components": components, + "local_exponents": local, "swap_pairs": pairs, "index": g, + "label_exponent": (p - 1) // g} + + +def _primitive_root(p): + if p == 2: + return 1 + remainder, divisor, factors = p - 1, 2, [] + while divisor * divisor <= remainder: + if remainder % divisor == 0: + factors.append(divisor) + while remainder % divisor == 0: + remainder //= divisor + divisor += 1 + if remainder > 1: + factors.append(remainder) + return next(a for a in range(2, p) if all(pow(a, (p - 1) // q, p) != 1 for q in factors)) + + +def _extended_gcd(a, b): + old_r, r, old_s, s, old_t, t = a, b, 1, 0, 0, 1 + while r: + quotient = old_r // r + old_r, r = r, old_r - quotient * r + old_s, s = s, old_s - quotient * s + old_t, t = t, old_t - quotient * t + return old_r, old_s, old_t + + +def _exponent_word(p, exponents, desired): + """Solve a product of power generators by Bezout coefficients and one log.""" + root = _primitive_root(p) + value, logarithm = 1, 0 + while value != desired: + value = value * root % p + logarithm += 1 + if logarithm >= p - 1: + raise ValueError("requested determinant is not a nonzero field element") + divisor, coefficients = p - 1, [] + for exponent in exponents: + divisor, left, right = _extended_gcd(divisor, exponent) + coefficients = [left * c for c in coefficients] + [right] + if logarithm % divisor: + raise ValueError("requested determinant is outside the automorphism image") + return root, [c * (logarithm // divisor) for c in coefficients] + + +def _check_map(p, source, target, U, V, W): + n = len(source) + u_columns, v_columns = transpose(U), transpose(V) + for i in range(n): + for j in range(n): + if _multiply(target, u_columns[i], v_columns[j], p) != _apply(W, source[i][j], p): + raise ValueError("three-factor certificate fails a basis-product identity") + + +def automorphism(p, components, desired_det): + """Construct any attainable determinant using variable scales and swaps.""" + model = make_model(p, components) + _nonzero(desired_det, p, "desired determinant") + character = determinant_character(p, components) + instructions, exponents = [], [] + for j, values in enumerate(character["local_exponents"]): + for i, exponent in enumerate(values): + instructions.append(("scale", j, i)) + exponents.append(exponent) + if p % 2: + for first, second in character["swap_pairs"]: + instructions.append(("swap", first, second)) + exponents.append((p - 1) // 2) + root, coefficients = _exponent_word(p, exponents, desired_det) + matrix = identity(model["n"]) + scalings, swaps = [], [] + for instruction, coefficient in zip(instructions, coefficients): + kind, first, second = instruction + if kind == "scale": + scalar = pow(root, coefficient % (p - 1), p) + if scalar != 1: + start = model["offsets"][first] + for k, exponent in enumerate(model["exponents"][first]): + factor = pow(scalar, exponent[second], p) + matrix[start + k] = [factor * x % p for x in matrix[start + k]] + scalings.append({"component": first, "variable": second, "scalar": scalar}) + elif coefficient % 2: + first_start, second_start = model["offsets"][first], model["offsets"][second] + for k in range(model["dimensions"][first]): + matrix[first_start + k], matrix[second_start + k] = matrix[second_start + k], matrix[first_start + k] + swaps.append([first, second]) + if determinant(matrix, p) != desired_det: + raise RuntimeError("constructed automorphism has the wrong determinant") + if _apply(matrix, model["unit"], p) != model["unit"]: + raise RuntimeError("constructed automorphism does not preserve the unit") + _check_map(p, model["table"], model["table"], matrix, matrix, matrix) + return {"matrix": matrix, "determinant": desired_det, "scalings": scalings, + "swaps": swaps, "index": character["index"]} + + +def _unit_multiplier(model, desired_det): + p, n = model["p"], model["n"] + # One local dimension is a p-power, hence invertible modulo p-1. The + # total product dimension need not be: a global scalar is insufficient. + scalar = 1 if p == 2 else pow(desired_det, pow(model["dimensions"][0], -1, p - 1), p) + unit = list(model["unit"]) + unit[model["offsets"][0]] = scalar + matrix = identity(n) + for i in range(model["dimensions"][0]): + matrix[i][i] = scalar + if determinant(matrix, p) != desired_det: + raise RuntimeError("component unit multiplier has the wrong determinant") + return matrix, unit + + +def autotopism(p, components, a, b, c): + """Construct U,V,W with dets a,b,c and mu(Ux,Vy)=W mu(x,y).""" + model = make_model(p, components) + for value, name in [(a, "a"), (b, "b"), (c, "c")]: + _nonzero(value, p, name) + delta = a * b * pow(c, -1, p) % p + phi = automorphism(p, components, delta) + left, left_unit = _unit_multiplier(model, a * pow(delta, -1, p) % p) + right, right_unit = _unit_multiplier(model, b * pow(delta, -1, p) % p) + U = matmul(left, phi["matrix"], p) + V = matmul(right, phi["matrix"], p) + W = matmul(matmul(left, right, p), phi["matrix"], p) + actual = [determinant(matrix, p) for matrix in [U, V, W]] + if actual != [a, b, c]: + raise RuntimeError("autotopism determinant mismatch") + _check_map(p, model["table"], model["table"], U, V, W) + return {"U": U, "V": V, "W": W, "determinants": actual, + "left_unit": left_unit, "right_unit": right_unit, "automorphism": phi} + + +def covariant_stabilizer(p, components, a, b, c): + """Construct the covariant tensor stabilizer (U^-T,V^-T,W).""" + _prime(p) + for value, name in [(a, "a"), (b, "b"), (c, "c")]: + _nonzero(value, p, name) + witness = autotopism(p, components, pow(a, -1, p), pow(b, -1, p), c) + A, B, C = transpose(inverse(witness["U"], p)), transpose(inverse(witness["V"], p)), witness["W"] + if [determinant(matrix, p) for matrix in [A, B, C]] != [a, b, c]: + raise RuntimeError("covariant determinant mismatch") + return {"A": A, "B": B, "C": C, "determinants": [a, b, c], "autotopism": witness} + + +def validate_certificate(p, components, table, U, V, W): + """Check every model-to-tensor product and return its canonical SL label. + + If R maps the canonical factor order into the supplied model order, the + normalized certificate is (UR,VR,WR); its ratio is raw_d/det(R). + This sign matters when unequal component types are reordered. + """ + model = make_model(p, components) + n = model["n"] + table = _table(table, n, p) + U, V, W = [_matrix(matrix, n, p, name) for matrix, name in [(U, "U"), (V, "V"), (W, "W")]] + determinants = [determinant(matrix, p) for matrix in [U, V, W]] + if not all(determinants): + raise ValueError("certificate factor maps must be invertible") + _check_map(p, model["table"], table, U, V, W) + canonical = sorted(model["components"]) + R = model_isomorphism(p, canonical, model["components"]) + normalization_det = determinant(R, p) + raw_d = determinants[2] * pow(determinants[0] * determinants[1] % p, -1, p) % p + d = raw_d * pow(normalization_det, -1, p) % p + character = determinant_character(p, canonical) + return {"n": n, "components": canonical, "determinants": determinants, + "normalization_det": normalization_det, "raw_d": raw_d, "d": d, + "label": pow(d, character["label_exponent"], p), "index": character["index"], + "basis_products_checked": n * n, + "normalized_certificate": {"U": matmul(U, R, p), "V": matmul(V, R, p), "W": matmul(W, R, p)}} + + +def sl_transporter(p, left_components, left_table, left_certificate, + right_components, right_table, right_certificate): + """Construct right(Ax,By)=C left(x,y), with all three determinants one.""" + certificates = [] + for components, table, certificate in [(left_components, left_table, left_certificate), + (right_components, right_table, right_certificate)]: + if not isinstance(certificate, dict) or any(key not in certificate for key in ("U", "V", "W")): + raise ValueError("a certificate must supply U, V and W") + certificates.append(validate_certificate(p, components, table, certificate["U"], certificate["V"], certificate["W"])) + left, right = certificates + if left["components"] != right["components"]: + raise ValueError("component height multisets are not isomorphic") + if left["label"] != right["label"]: + raise ValueError("tensors have different special-linear orbit labels") + L, R = left["normalized_certificate"], right["normalized_certificate"] + desired = [determinant(L[key], p) * pow(determinant(R[key], p), -1, p) % p for key in ("U", "V", "W")] + correction = autotopism(p, left["components"], *desired) + maps = [matmul(matmul(R[key], correction[key], p), inverse(L[key], p), p) for key in ("U", "V", "W")] + if [determinant(matrix, p) for matrix in maps] != [1, 1, 1]: + raise RuntimeError("special-linear transporter determinant mismatch") + n = left["n"] + _check_map(p, _table(left_table, n, p), _table(right_table, n, p), *maps) + return {"A": maps[0], "B": maps[1], "C": maps[2], "determinants": [1, 1, 1], + "label": left["label"], "basis_products_checked": n * n} diff --git a/research/frobenius-product-characters/verify.py b/research/frobenius-product-characters/verify.py new file mode 100644 index 0000000000..c6a20be892 --- /dev/null +++ b/research/frobenius-product-characters/verify.py @@ -0,0 +1,489 @@ +#!/usr/bin/env python3 +"""Independent finite matrix checks for product Frobenius characters. + +Apache-2.0. Prepared by apoursh with substantial OpenAI Codex assistance. +All oracle arithmetic below is independent of model.py's implementations. +Full GL exhaustion is limited to the explicitly reported dimensions <= 3. +""" +import argparse +import copy +import hashlib +import importlib.util +import itertools +import json +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def authenticate_sources(): + package = Path(__file__).resolve().parent + root = package.parents[1] + manifest = json.loads((package / 'SOURCES.json').read_text()) + rows = [row for row in manifest['files'] if row.get('usage') == 'input'] + expected = {'research/frobenius-tensor-characters/README.md', + 'research/frobenius-algebra-recognition/PROOF.md', + 'research/etale-tensor-determinant-image/README.md'} + require({row['path'] for row in rows} == expected and len(rows) == 3, + 'live proof source set differs from the declared three inputs') + for row in rows: + actual = hashlib.sha256((root / row['path']).read_bytes()).hexdigest() + require(actual == row['sha256'], 'source hash mismatch: ' + row['path']) + return len(rows) + + +def load_model(): + path = Path(__file__).with_name('model.py') + spec = importlib.util.spec_from_file_location('product_model_target', path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def eye(n): + return [[int(i == j) for j in range(n)] for i in range(n)] + + +def determinant(matrix, p): + a = [list(row) for row in matrix] + result = 1 + for j in range(len(a)): + pivot = next((i for i in range(j, len(a)) if a[i][j] % p), None) + if pivot is None: + return 0 + if pivot != j: + a[j], a[pivot] = a[pivot], a[j] + result = -result + value = a[j][j] % p + result = result * value % p + reciprocal = pow(value, p-2, p) + for i in range(j+1, len(a)): + factor = a[i][j] * reciprocal % p + for k in range(j, len(a)): + a[i][k] = (a[i][k] - factor*a[j][k]) % p + return result % p + + +def inverse(matrix, p): + n = len(matrix) + a = [list(row) + unit for row, unit in zip(matrix, eye(n))] + for j in range(n): + pivot = next((i for i in range(j, n) if a[i][j] % p), None) + require(pivot is not None, 'oracle matrix is singular') + a[j], a[pivot] = a[pivot], a[j] + reciprocal = pow(a[j][j] % p, p-2, p) + a[j] = [(x*reciprocal) % p for x in a[j]] + for i in range(n): + if i != j: + factor = a[i][j] + a[i] = [(x-factor*y) % p for x, y in zip(a[i], a[j])] + return [row[n:] for row in a] + + +def apply(matrix, vector, p): + return [sum(x*y for x, y in zip(row, vector)) % p for row in matrix] + + +def matmul(left, right, p): + return [[sum(left[i][k]*right[k][j] for k in range(len(right))) % p + for j in range(len(right[0]))] for i in range(len(left))] + + +def columns(matrix): + return [list(column) for column in zip(*matrix)] + + +def multiply(table, left, right, p): + n = len(table) + out = [0]*n + for i, a in enumerate(left): + if a: + for j, b in enumerate(right): + if b: + for k, c in enumerate(table[i][j]): + if c: + out[k] = (out[k] + a*b*c) % p + return out + + +def oracle_model(p, components): + factors = [list(itertools.product(*(range(p**e) for e in heights))) + for heights in components] + n = sum(map(len, factors)) + table = [[[0]*n for _ in range(n)] for _ in range(n)] + unit, offset = [0]*n, 0 + for heights, exponents in zip(components, factors): + unit[offset] = 1 + positions = {powers: i for i, powers in enumerate(exponents)} + for i, a in enumerate(exponents): + for j, b in enumerate(exponents): + powers = tuple(x+y for x, y in zip(a, b)) + if all(x < p**e for x, e in zip(powers, heights)): + table[offset+i][offset+j][offset+positions[powers]] = 1 + offset += len(exponents) + return table, unit + + +def multiplication_matrix(table, value, p): + return columns([multiply(table, value, vector, p) for vector in eye(len(table))]) + + +def preserves_product(table, matrix, unit, p): + if apply(matrix, unit, p) != unit: + return False + basis_images = columns(matrix) + for i, left in enumerate(basis_images): + for j, right in enumerate(basis_images): + if multiply(table, left, right, p) != apply(matrix, table[i][j], p): + return False + return True + + +def endpoint(table, U, V, W, source, p): + uc, vc = columns(U), columns(V) + return all(multiply(table, uc[i], vc[j], p) == apply(W, source[i][j], p) + for i in range(len(table)) for j in range(len(table))) + + +def transformed_table(table, U, V, W, p): + ui, vi = columns(inverse(U, p)), columns(inverse(V, p)) + return [[apply(W, multiply(table, x, y, p), p) for y in vi] for x in ui] + + +def rejected(action, label): + try: + action() + except (ValueError, TypeError): + return 1 + raise ValueError('invalid case accepted: ' + label) + + +def enumerate_automorphisms(p, components): + table, unit = oracle_model(p, components) + n, invertible, automorphisms = len(table), 0, [] + for entries in itertools.product(range(p), repeat=n*n): + matrix = [list(entries[i*n:(i+1)*n]) for i in range(n)] + det = determinant(matrix, p) + if det: + invertible += 1 + if preserves_product(table, matrix, unit, p): + automorphisms.append(matrix) + return table, unit, invertible, automorphisms + + +def check_constructed_character(api, p, components, expected): + table, unit = oracle_model(p, components) + actual = set() + for value in range(1, p): + if value in expected: + result = api.automorphism(p, components, value) + matrix = result['matrix'] + require(determinant(matrix, p) == value, 'wrong constructed automorphism determinant') + require(preserves_product(table, matrix, unit, p), 'constructed map is not an automorphism') + actual.add(value) + else: + rejected(lambda value=value: api.automorphism(p, components, value), + 'unattainable automorphism determinant') + require(actual == expected, 'character image differs from independent matrix oracle') + return sorted(actual) + + +def tiny_exhaustions(api): + domains = [(2, [[], []], 2), (3, [[], []], 2), + (2, [[1], []], 1), (2, [[], [], []], 6), + (3, [[1]], 6), (3, [[], [], []], 6)] + reports = [] + for p, components, expected_count in domains: + table, unit, gl_count, autos = enumerate_automorphisms(p, components) + n = len(table) + require(len(autos) == expected_count, 'tiny automorphism count changed') + model = api.make_model(p, components) + require(model['table'] == table and model['unit'] == unit, 'model differs from independent table') + image = {determinant(phi, p) for phi in autos} + check_constructed_character(api, p, components, image) + units = [] + for value in itertools.product(range(p), repeat=n): + matrix = multiplication_matrix(table, value, p) + if determinant(matrix, p): + units.append((list(value), matrix)) + triples, normalized_count = set(), 0 + for phi in autos: + for u, mu in units: + for v, mv in units: + U, V = matmul(mu, phi, p), matmul(mv, phi, p) + W = matmul(multiplication_matrix(table, multiply(table, u, v, p), p), phi, p) + require(endpoint(table, U, V, W, table, p), 'normalized autotopism endpoint failed') + triples.add(tuple(determinant(matrix, p) for matrix in (U, V, W))) + normalized_count += 1 + for wanted in itertools.product(range(1, p), repeat=3): + if wanted in triples: + got = api.autotopism(p, components, *wanted) + matrices = [got[key] for key in ('U', 'V', 'W')] + require(tuple(determinant(matrix, p) for matrix in matrices) == wanted, + 'wrong constructed autotopism determinants') + require(endpoint(table, *matrices, table, p), 'constructed autotopism endpoint failed') + else: + rejected(lambda wanted=wanted: api.autotopism(p, components, *wanted), + 'unattainable autotopism determinant triple') + reports.append({'p': p, 'components': components, 'n': n, + 'all_matrices': p**(n*n), 'invertible_matrices': gl_count, + 'automorphisms': len(autos), 'automorphism_determinants': sorted(image), + 'units': len(units), 'normalized_autotopisms': normalized_count, + 'determinant_triples': [list(triple) for triple in sorted(triples)]}) + return reports + + +def polynomial_product(left, right, p): + n, result = len(left), [0]*len(left) + for i, x in enumerate(left): + if x: + for j in range(n-i): + if right[j]: + result[i+j] = (result[i+j] + x*right[j]) % p + return result + + +def cyclic_substitutions(p, height): + n, count, image = p**height, 0, set() + for linear in range(1, p): + for tail in itertools.product(range(p), repeat=n-2): + generator = [0, linear, *tail] + powers, current = [], [1]+[0]*(n-1) + for _ in range(n): + powers.append(current) + current = polynomial_product(current, generator, p) + require(not any(current), 'cyclic substitution violates truncation') + matrix = columns(powers) + value = determinant(matrix, p) + require(value != 0, 'nonzero-linear cyclic substitution was singular') + image.add(value) + count += 1 + return count, image + + +def representative_triples(api, p, components, phis, unit_values): + """Enumerate determinant triples from actual matrices representing each image.""" + table, unit = oracle_model(p, components) + triples = set() + for phi in phis: + require(preserves_product(table, phi, unit, p), 'bad oracle automorphism representative') + for u in unit_values: + for v in unit_values: + U = matmul(multiplication_matrix(table, u, p), phi, p) + V = matmul(multiplication_matrix(table, v, p), phi, p) + W = matmul(multiplication_matrix(table, multiply(table, u, v, p), p), phi, p) + require(endpoint(table, U, V, W, table, p), 'moderate representative endpoint failed') + triples.add(tuple(determinant(matrix, p) for matrix in (U, V, W))) + accepted, refused = 0, 0 + for wanted in itertools.product(range(1, p), repeat=3): + if wanted in triples: + got = api.autotopism(p, components, *wanted) + matrices = [got[key] for key in ('U', 'V', 'W')] + require(tuple(determinant(matrix, p) for matrix in matrices) == wanted, + 'moderate constructed determinant triple failed') + require(endpoint(table, *matrices, table, p), 'moderate constructed endpoint failed') + accepted += 1 + else: + refused += rejected(lambda wanted=wanted: api.autotopism(p, components, *wanted), + 'moderate determinant triple outside subgroup') + return {'p': p, 'components': components, 'accepted_triples': accepted, + 'rejected_triples': refused, + 'scope': 'All determinant triples; matrices use unit/automorphism image representatives.'} + + +def moderate_oracles(api): + count9, image9 = cyclic_substitutions(3, 2) + require(count9 == 4374 and image9 == {1}, 'F3[x]/x9 local oracle changed') + check_constructed_character(api, 3, [[2]], image9) + table18, unit18 = oracle_model(3, [[2], [2]]) + swap = [[int(j == (i+9) % 18) for j in range(18)] for i in range(18)] + require(preserves_product(table18, swap, unit18, 3) and determinant(swap, 3) == 2, + 'repeated odd-dimensional block swap failed') + check_constructed_character(api, 3, [[2], [2]], {1, 2}) + count5, image5 = cyclic_substitutions(5, 1) + require(count5 == 500 and image5 == {1, 4}, 'F5[x]/x5 local oracle changed') + check_constructed_character(api, 5, [[], [1]], image5) + wrong_total_dimension_image = {pow(a, 6*(5-1)//2, 5) for a in range(1, 5)} + require(wrong_total_dimension_image == {1} and wrong_total_dimension_image != image5, + 'wrong-total-dimension control does not discriminate') + table2, _ = oracle_model(3, [[], []]) + require(determinant(multiplication_matrix(table2, [1, 2], 3), 3) == 2, + 'componentwise unit determinant lost') + require({determinant(multiplication_matrix(table2, [a, a], 3), 3) + for a in (1, 2)} == {1}, 'global-scalar-unit control changed') + mixed, mixed_unit = oracle_model(2, [[2], [1, 1]]) + bad_swap = [[int(j == (i+4) % 8) for j in range(8)] for i in range(8)] + require(determinant(bad_swap, 2) == 1 and not preserves_product(mixed, bad_swap, mixed_unit, 2), + 'equal-dimensional nonisomorphic factor swap unexpectedly preserved product') + rejected(lambda: api.validate_certificate(2, [[2], [1, 1]], mixed, + bad_swap, bad_swap, bad_swap), 'nonisotype internal swap') + scaling5 = eye(6) + for exponent in range(5): + scaling5[1+exponent][1+exponent] = pow(2, exponent, 5) + triple_reports = [ + representative_triples(api, 3, [[2]], [eye(9)], + [[a]+[0]*8 for a in (1, 2)]), + representative_triples(api, 3, [[2], [2]], [eye(18), swap], + [[a]+[0]*8+[1]+[0]*8 for a in (1, 2)]), + representative_triples(api, 5, [[], [1]], [eye(6), scaling5], + [[a, 1]+[0]*4 for a in range(1, 5)]), + ] + return {'cyclic_f3_height2_substitutions': count9, 'cyclic_f3_height2_determinants': sorted(image9), + 'two_copies_swap_determinant': 2, 'cyclic_f5_height1_substitutions': count5, + 'cyclic_f5_height1_determinants': sorted(image5), + 'wrong_total_dimension_image': sorted(wrong_total_dimension_image), + 'component_unit_determinant': 2, 'global_scalar_unit_determinants': [1], + 'nonisotype_swap_rejected': True, + 'determinant_triple_checks': triple_reports, + 'scope': 'Local substitutions exhausted; repeated-product full automorphism group not enumerated.'} + + +def covariant_coefficient_action(table, A, B, C, p): + """Literal (A tensor B tensor C) action on every coefficient index.""" + n = len(table) + support = [(r, s, t, table[r][s][t]) for r, s, t in itertools.product(range(n), repeat=3) + if table[r][s][t]] + for i, j, k in itertools.product(range(n), repeat=3): + actual = sum(A[i][r]*B[j][s]*C[k][t]*value for r, s, t, value in support) % p + if actual != table[i][j][k]: + return False + return True + + +def covariant_controls(api): + reports = [] + for p in (5, 7): + table, _ = oracle_model(p, [[1]]) + # Independent diagonal substitution matrices determine these character + # generators; completeness of the character image uses the written proof. + scaling_dets = set() + for a in range(1, p): + matrix = [[int(i == j)*pow(a, i, p) for j in range(p)] for i in range(p)] + scaling_dets.add(determinant(matrix, p)) + accepted, refused = 0, 0 + for wanted in itertools.product(range(1, p), repeat=3): + if wanted[0]*wanted[1]*wanted[2] % p in scaling_dets: + got = api.covariant_stabilizer(p, [[1]], *wanted) + matrices = [got[key] for key in ('A', 'B', 'C')] + require(tuple(determinant(matrix, p) for matrix in matrices) == wanted, + 'wrong covariant determinants') + require(covariant_coefficient_action(table, *matrices, p), + 'literal covariant coefficient-index action failed') + accepted += 1 + else: + refused += rejected(lambda wanted=wanted: api.covariant_stabilizer(p, [[1]], *wanted), + 'covariant triple outside character subgroup') + # This explicit nonlinear substitution makes transpose errors visible; + # the constructive API's selected scaling matrices may be diagonal. + generator = [0, 1, 1]+[0]*(p-3) + powers, current = [], [1]+[0]*(p-1) + for _ in range(p): + powers.append(current) + current = polynomial_product(current, generator, p) + phi = columns(powers) + inv_phi = inverse(phi, p) + inverse_transpose = columns(inv_phi) + require(covariant_coefficient_action(table, inverse_transpose, inverse_transpose, phi, p), + 'nonlinear inverse-transpose coefficient control failed') + require(not covariant_coefficient_action(table, inv_phi, inv_phi, phi, p), + 'missing-transpose mutation escaped coefficient control') + reports.append({'p': p, 'n': p, 'accepted_covariant_triples': accepted, + 'rejected_covariant_triples': refused, + 'nonlinear_missing_transpose_mutation_rejected': True}) + return reports + + +def shear(n, p, shift): + result = eye(n) + for i in range(n): + j = (i+1+shift) % n + if i != j: + result[i] = [(x+y) % p for x, y in zip(result[i], result[j])] + return result + + +def certificate_controls(api): + p, components = 3, [[2]] + table, _ = oracle_model(p, components) + n = len(table) + U, V, W = shear(n, p, 0), shear(n, p, 2), shear(n, p, 4) + U[0] = [(2*x) % p for x in U[0]] + V[0] = [(2*x) % p for x in V[0]] + target = transformed_table(table, U, V, W, p) + require(endpoint(target, U, V, W, table, p), 'independent three-factor fixture is invalid') + got = api.validate_certificate(p, components, target, U, V, W) + require(got['label'] == 1, 'equal-class independent-basis certificate mislabeled') + mutations = 0 + for key in ('U', 'V', 'W'): + changed = {'U': copy.deepcopy(U), 'V': copy.deepcopy(V), 'W': copy.deepcopy(W)} + changed[key][0][0] = (changed[key][0][0]+1) % p + mutations += rejected(lambda changed=changed: api.validate_certificate( + p, components, target, changed['U'], changed['V'], changed['W']), 'changed factor map '+key) + broken = copy.deepcopy(target) + broken[0][0][0] = (broken[0][0][0]+1) % p + mutations += rejected(lambda: api.validate_certificate(p, components, broken, U, V, W), 'changed tensor') + mutations += rejected(lambda: api.validate_certificate(p, components, target, U[:-1], V, W), 'wrong map shape') + mutations += rejected(lambda: api.validate_certificate(p, components, target, [[0]*n for _ in range(n)], V, W), + 'singular map') + for invalid in (-1, p): + changed_map = copy.deepcopy(U) + changed_map[0][0] = invalid + mutations += rejected(lambda changed_map=changed_map: api.validate_certificate( + p, components, target, changed_map, V, W), 'noncanonical map entry') + changed_table = copy.deepcopy(target) + changed_table[0][0][0] = invalid + mutations += rejected(lambda changed_table=changed_table: api.validate_certificate( + p, components, changed_table, U, V, W), 'noncanonical tensor entry') + # The same ambient tensor has a certificate in either supplied factor order. + canonical, _ = oracle_model(3, [[], [2]]) + R = api.model_isomorphism(3, [[2], []], [[], [2]]) + require(determinant(R, 3) == 2, 'factor-order permutation lost odd block sign') + order_a = api.validate_certificate(3, [[], [2]], canonical, eye(10), eye(10), eye(10)) + order_b = api.validate_certificate(3, [[2], []], canonical, R, R, R) + require(order_a['label'] == order_b['label'] == 1, 'label depends on supplied component order') + require(order_a['d'] == order_b['d'] == 1 and order_a['raw_d'] != order_b['raw_d'], + 'factor-order determinant normalization not exercised') + mutations += rejected(lambda: api.model_isomorphism(2, [[2]], [[1, 1]]), 'same-size different type') + left = {'U': eye(n), 'V': eye(n), 'W': eye(n)} + right = {'U': U, 'V': V, 'W': W} + transfer = api.sl_transporter(p, components, table, left, components, target, right) + matrices = [transfer[key] for key in ('A', 'B', 'C')] + require(all(determinant(matrix, p) == 1 for matrix in matrices), 'SL transporter determinant failed') + require(endpoint(target, *matrices, table, p), 'SL transporter endpoint failed') + bad_U = eye(n) + bad_U[0][0] = 2 + different = transformed_table(table, bad_U, eye(n), eye(n), p) + other = {'U': bad_U, 'V': eye(n), 'W': eye(n)} + different_label = api.validate_certificate(p, components, different, **other) + require(different_label['label'] == 2, 'different SL class mislabeled') + mutations += rejected(lambda: api.sl_transporter(p, components, table, left, + components, different, other), 'unequal SL labels') + return {'independent_factor_basis_dimension': n, 'permuted_factor_order_dimension': 10, + 'same_label_sl_transporter_checked': True, 'different_label_sl_transporter_rejected': True, + 'malformed_or_changed_certificates_rejected': mutations} + + +def run(): + source_count = authenticate_sources() + api = load_model() + return {'status': 'PASS_FROBENIUS_PRODUCT_CHARACTERS', 'authenticated_source_files': source_count, + 'tiny_full_GL_exhaustions': tiny_exhaustions(api), + 'moderate_substitution_oracles': moderate_oracles(api), + 'covariant_coefficient_controls': covariant_controls(api), + 'certificate_controls': certificate_controls(api), + 'scope': 'Finite exact matrix checks support the separate proof; no exhaustive large-product orbit search or new kappa.'} + + +if __name__ == '__main__': + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--json', action='store_true') + args = parser.parse_args() + report = run() + if args.json: + print(json.dumps(report, indent=2, sort_keys=True)) + else: + print(report['status']) + print(json.dumps({key: value for key, value in report.items() if key != 'status'}, sort_keys=True))