diff --git a/research/finite-field-pencil-characters/.gitattributes b/research/finite-field-pencil-characters/.gitattributes new file mode 100644 index 0000000000..7467454cb8 --- /dev/null +++ b/research/finite-field-pencil-characters/.gitattributes @@ -0,0 +1 @@ +source/** -text diff --git a/research/finite-field-pencil-characters/INPUTS.json b/research/finite-field-pencil-characters/INPUTS.json new file mode 100644 index 0000000000..846f5608d4 --- /dev/null +++ b/research/finite-field-pencil-characters/INPUTS.json @@ -0,0 +1,30 @@ +[ + { + "local": "source/pencil.py", + "commit": "618fb04433927ade44ed5b507f8d30f9ede2bde5", + "path": "research/mixed-singular-kronecker-characters/source/pencil.py", + "git_blob": "6bc7fc076e6ce2418ec9ed05d85115deb3d4bdd2", + "sha256": "a714862853cc884e84eac34ba1d7ccb14a6326bcfadb630910034bb44bd305db" + }, + { + "local": "source/oracle.py", + "commit": "618fb04433927ade44ed5b507f8d30f9ede2bde5", + "path": "research/mixed-singular-kronecker-characters/oracle.py", + "git_blob": "6535d1363ece5521d75a6ef218f4e68a5c2eeb5d", + "sha256": "9713ec418b158055658c3a53766f305d6e3734e7b775c8bbd365a46e525966aa" + }, + { + "local": "source/SINGULAR.md", + "commit": "618fb04433927ade44ed5b507f8d30f9ede2bde5", + "path": "research/mixed-singular-kronecker-characters/PROOF.md", + "git_blob": "9de07b628089ab903751ea2571b62b08dba7e524", + "sha256": "2d0b2348bb27063e7bf34769b1a43c90d593902f043ffc438d7ec887f0016295" + }, + { + "local": "source/REGULAR.md", + "commit": "43142bedc7cb5c0f1f73ff3fea6d9bfd237949ee", + "path": "research/pencil-determinant-image/README.md", + "git_blob": "20f8262d3747f28e4535ec3f928f7481f8306749", + "sha256": "ba945687c23f6e675e2c320c7e5ccf345b17090e4d4283721ff950d62da5516e" + } +] diff --git a/research/finite-field-pencil-characters/NOTICE.md b/research/finite-field-pencil-characters/NOTICE.md new file mode 100644 index 0000000000..6040e2df53 --- /dev/null +++ b/research/finite-field-pencil-characters/NOTICE.md @@ -0,0 +1,7 @@ +# Attribution + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. + +Nick Petalas PR5250 supplies the invertible-slice theorem and the retained classical centralizer determinant proof, with Arne Storjohann and Ferrer/Mingueza/Montoro credit. apoursh PR5672 supplies the singular symmetric-power lifts and finite-field arithmetic. Ali Romman PR5683 supplies the complete singular mixing theorem and literal coefficient-equation oracle. David Ganz supplies the A030/A026/A029 atlas context. Classical Kronecker, companion-matrix and finite-field norm theory remain predecessor mathematics. + +The new contribution is the per-primary chart construction, the complete regular/singular determinant assembly, the no-rational-invertible-slice family, and the bounded exact checks. Four original source files are retained byte for byte. INPUTS.json and SOURCES.json identify their commits, paths, Git objects and SHA256 hashes. Global literature priority is not claimed. diff --git a/research/finite-field-pencil-characters/PROOF.md b/research/finite-field-pencil-characters/PROOF.md new file mode 100644 index 0000000000..2ab4d45401 --- /dev/null +++ b/research/finite-field-pencil-characters/PROOF.md @@ -0,0 +1,145 @@ +# Complete determinant images of supplied finite-field pencils + +## 1. Scope and conventions + +Let K=F_q. The input is a complete supplied Kronecker block model for a matrix pencil with positive total row and column dimensions m,n. The types are: + +- Right singular blocks R_e, of shape e by e+1, with s on the diagonal and t above it. +- Their transposes L_e. Zero indices are allowed. +- Finite regular blocks `(I,C(f^ell))`, where f is a monic irreducible polynomial over K, ell>=1, and C is the companion matrix with ones below the diagonal. +- Infinity blocks `(C(X^ell),I)`. + +Every type can have any positive multiplicity. All matrices and both tensor dimensions are finite. The model is supplied. This note does not implement its discovery from an arbitrary tensor. These are the full Kronecker types, not only semisimple or split regular blocks. + +Use the covariant action + +`(A0,A1) -> (P(a A0+b A1)Q^T, P(c A0+d A1)Q^T)`, + +where `R=[[a,b],[c,d]]` is invertible. Let Delta be the image of the stabilizer under `(det P,det Q,det R)`. Polynomial pencil identities are coefficient identities in independent indeterminates. They are not tests at only the q+1 rational directions. + +The singular Hom spaces and slice lifts are credited to PR5683 and apoursh PR5672. The regular centralizer determinant theorem is the classical result retained by Nick Petalas PR5250. New here are the per-primary chart construction, full mixed assembly and the removal of the global invertible-rational-slice premise. + +## 2. Normalize one primary block after any slice action + +Consider a finite block `(I,J)`, with J=C(f^ell). Set B=aI+bJ and D=cI+dJ. If B is invertible, put H=B^-1 D. Otherwise D is invertible: failure of both would make both linear polynomials a+bX and c+dX divisible by the same irreducible f, contrary to det R!=0. In the second case f must be linear. Put H=D^-1 B. Its only eigenvalue is zero, and its nilpotence index is ell. + +For an infinity block `(J,I)`, use B=aJ+bI and D=cJ+dI. If b!=0, B is invertible. If b=0, D is invertible and H=D^-1 B is nilpotent of index ell. Thus one chart is always available on each primary block even when no chart is invertible on the full pencil. + +In either chart H is a fractional linear function of J with nonzero determinant. Its inverse fractional expression is defined in K[J]. Hence `K[H]=K[J]`. The first coordinate vector v is cyclic for J and therefore for H. The matrix + +`S=[v,Hv,...,H^(k-1)v]` + +is invertible, where k is the block dimension. Then `S^-1 H S` is the companion matrix of the transformed monic primary polynomial. This gives a direct construction with no eigenvalue choice or extension-field embedding. + +In the finite chart take + +`P=S^-1 B^-1`, `Q=S^T`. + +The transformed block is `(I,S^-1 H S)`. In the infinity chart take `P=S^-1 D^-1`, `Q=S^T`; it is `(S^-1 H S,I)`. These formulas prove both literal identities, not only a determinant equality. The transformed primary degree and Jordan length are preserved, except that a linear finite primary can exchange with infinity. + +For a fixed R, normalize every regular block and compare the resulting multiset with the original regular multiset. Retain R exactly when the types and multiplicities match. Match equal blocks and apply the corresponding common row/column block permutation. Its determinant signs are part of the actual matrices. Combine these matrices with the credited singular slice lifts. This constructs a literal full-pencil stabilizer `(P_R,Q_R,R)` for every retained R. + +Conversely a full-pencil equivalence preserves its Kronecker types. This also follows from the Hom decomposition below: singular types remain singular with the same indices, while the regular diagonal must be a module isomorphism with equal primary lengths and multiplicities. Thus a rejected regular multiset cannot be repaired by singular/regular mixing. The retained R are exactly the possible slice actions. Let their explicit lift determinants be `(p_R,q_R,z_R)`. + +## 3. All fixed-slice mixing and its determinant image + +Set `C=Q^-T`. A fixed-slice stabilizer is precisely an automorphism satisfying `P A_i=A_i C` for both i. + +The singular Hom table from PR5683 is retained: right-to-right dimension max(e-f+1,0), left-to-left dimension max(f-e+1,0), right-to-left zero, and left-to-right dimension e+f. Its scalar recurrences include zero indices. + +For one finite regular block `(I,M)` of dimension k, comparison of the two coefficients gives: + +| Source | Destination | Hom dimension | +| --- | --- | ---: | +| R_e | regular | 0 | +| regular | R_e | k | +| regular | L_e | 0 | +| L_e | regular | k | + +For regular to R_e, the second matrix has rows `u,uM,...,uM^e`; the first consists of its first e rows. The row u is arbitrary. For L_e to regular, the first matrix has columns `v,Mv,...,M^e v`; the second consists of its first e columns. The column v is arbitrary. In the two zero directions, a zero boundary row or column propagates across the recurrence and forces every entry to zero. These formulas include e=0. Exchanging the two slices and using the singular slice lift proves the same statements for an infinity primary. Multiplicities give arbitrary matrices between multiplicity spaces. + +Order right types by increasing index, then all regular types, then left types by decreasing index. The full morphism is upper triangular between these three groups. Thus all regular/singular and singular inter-type mixing is included and has no effect on either determinant. + +Within the regular group, different projective primary points have zero Hom. For finite primaries this is the usual Bezout argument for relatively prime polynomials. For finite versus infinity, one equation gives U=M U N with N nilpotent, and iteration forces U=0. Infinity versus finite is the transpose argument. + +For one finite irreducible f of degree d, the regular module is + +`direct_sum_ell (K[X]/f^ell)^(r_ell)`. + +The filtration by powers of f has residue field E=K[X]/f. The exact-length-ell diagonal multiplicity map D_ell appears on ell successive layers. Maps between different lengths are triangular on each layer. Therefore + +`det_K P_regular = product_(f,ell) Norm_(E/K)(det_E D_(f,ell))^ell`. + +The same formula for infinity uses E=K. Each residue norm is onto K*. Conversely multiplication on one selected block by a unit lifting any residue element realizes that norm to the ell-th power. This is the credited classical centralizer theorem from PR5250, now applied separately at every projective primary point. Since Q=P^-T for this diagonal regular group, its determinant pairs are exactly `(h,h^-1)`, with + +`h in (K*)^g`, `g=gcd(all regular block lengths)`. + +The residue degree and the multiplicity do not replace the block length in g. + +For each distinct right singular index e, its multiplicity determinant gives `(u^e,u^(-e-1))`; for each left index it gives `(u^(-e-1),u^e)`. This uses the transposed parameter convention of PR5683. All u in K* occur. Hence the complete fixed-slice image F is the subgroup of `(K*)^2` generated by + +`(u^e,u^(-e-1))` for every right type, + +`(u^(-e-1),u^e)` for every left type, + +`(u^ell,u^-ell)` for every regular block length, + +for all u in K*. Repeated copies do not add generators. No block-diagonal assumption is used in the upper bound: the full Hom analysis gives it. + +For a mixed model with at least one singular type, choose its primitive vector v0 and the primitive row eta annihilating it as in PR5683. Then F is equivalently the condition + +`x^eta1 y^eta2 in (K*)^d`, + +where d is the gcd of all singular values `eta dot v_i` and all regular lengths. This follows because eta1-eta2 is 1 or -1. It explains why a regular semisimple block removes the row/column obstruction, while a length-two regular block need not do so. + +## 4. Complete image, labels and literal correction + +**Theorem.** For the supplied model over F_q, + +`Delta = union_(retained R) {(p_R x,q_R y,z_R) : (x,y) in F}`. (1) + +For necessity, divide any stabilizer by the constructed lift with its exact slice action R. The quotient fixes the slices, so its determinants lie in F by section 3. For sufficiency, compose the lift with a fixed-slice witness. This proves (1), attainment and independence from all block-matching choices. Different R with the same determinant can give different cosets. The algorithm must keep that union; it cannot choose one arbitrary representative per determinant. + +The ambient determinant map from `GL_m x GL_n x GL_2` onto `(K*)^3` is surjective because m,n>0. Its kernel is the product of the three special linear groups. Thus the SL orbits in the GL orbit are exactly `(K*)^3/Delta`. The executable returns the smallest triple in each finite coset as its label. Their number is `(q-1)^3/|Delta|`. + +If a supplied GL map g has determinant triple in Delta, take the literal stabilizer h with the same triple. Then `g h^-1` has three determinant-one factors and the same tensor image as g. A prescribed slice action can be requested only when its particular coset admits the triple; global membership does not imply membership for every R of the same determinant. + +A supplied change of coordinates to the model conjugates the stabilizer. Conjugation leaves all three determinants fixed. The formula therefore applies to any pencil with that supplied decomposition and checked factor maps. It does not discover those maps. + +## 5. A closed family with no invertible rational slice + +Take one length-ell Jordan primary at every point of P1(F_q), with common multiplicity r. Every rational slice is singular, but the homogeneous determinant polynomial is a nonzero scalar multiple of + +`(s^q t-s t^q)^(r ell)`. + +Thus the pencil is regular. Every GL2 action permutes these equally weighted primary types and is admitted. Write `H=(K*)^ell`. Then the exact character image is + +`Delta = {(x,y,z): x in H and x*y*z^(r ell)=1}`. (2) + +In particular y is also in H. There are exactly `(q-1)*gcd(q-1,ell)` SL orbits. For ell=1 this gives q-1, including the binary diag(s,t,s+t) case. For F5 with ell=2 there are eight, not four. For F4 with ell=3 there are nine. + +Here is the extra determinant argument needed for nonsemisimple lengths. The fixed-slice first determinant group is H. Therefore `R -> p_R mod H` is a group homomorphism. Every elementary unipotent in SL2 has p-power order, where p is the characteristic; K*/H has order prime to p. SL2 is generated by those elementary matrices, so its image is trivial. + +It remains to evaluate `R=diag(z,1)`. On each of the q finite primary blocks, the cyclic basis is diagonal with entries `1,z^-1,...,z^(-(ell-1))`. Its P determinant is `z^(ell(ell-3)/2)`. On infinity it is `z^(-ell(ell-1)/2)`. The common block permutation has a sign raised to r ell, which lies in H. The total exponent is + +`r*((q-1)*ell*(ell-3)/2-ell)`. + +Since ell(ell-3)/2 is an integer and z^(q-1)=1, this is an ell-th power. Hence p_R lies in H for every R. Conversely all x in H can be supplied by the regular fixed-slice group. Finally, `s^q t-s t^q` transforms by det R, so determinants of the pencil identity force `xy=z^(-r ell)`. This proves (2). A determinant-polynomial comparison alone would miss the condition x in H. + +## 6. Algorithm and cost boundary + +For fixed q and a supplied complete model, equation (1) gives deterministic polynomial-time image and label extraction in the total factor dimensions. Enumerate the fewer than q^4 matrices in GL2, normalize each companion block by matrix arithmetic, match its exact transformed companion polynomial, and compute F from the displayed exponent generators in the at most (q-1)^2-element group. No large matrix stabilizer is enumerated. The quotient has at most (q-1)^3 elements. The exact polynomial exponent is not optimized. + +The singular witnesses use the credited characteristic-safe symmetric powers. A regular witness needs a residue element of a specified norm. Existence is proved above. Uniform sampling in the finite residue field gives an exact Las Vegas construction: test the norm and accept only the required value. Its expected trial count is at most q, and each trial has polynomial field-operation cost. Deterministic enumeration also terminates, but no polynomial bound is claimed for that norm search in unbounded residue degree. The bounded executable enumerates residues of degree at most three. It does not implement the randomized general solver or claim polynomial complexity in log(q). + +The finite verifier uses F2/F3/F4/F5, singular indices 0..5, regular lengths 1..3, residue degrees 1..3, multiplicities 1..3, and total dimensions at most sixteen. Its declared models cover strict subdomains of those bounds; it does not enumerate every admissible model. The written theorem has no such dimension, length, degree or field-size restriction. + +A separate coefficient-equation oracle imports no lift or character formula. For each declared slice action it solves all `P B_i=A_i C` equations, enumerates every vector in that solution space, and retains exactly invertible P,C. Large fixtures explicitly mark a selected action set; the other fixtures cover all GL2. Literal witnesses cover every admitted GL2 action in every declared model. Malformed inputs, wrong determinant restrictions and corrupt literal maps reject. + +## 7. Use, limits and credit + +This completes the determinant-character interface for supplied finite-field pencil models, including nonsplit primary factors, all Jordan lengths, infinity, both singular orientations and zero indices. It resolves the missing global-slice premise in PR5250 and the regular/singular coupling question from PR5672/5683. It is not an arbitrary-tensor recognizer, a general tensor-atlas solution, a proof-assistant certificate or independent human acceptance. + +A multiplication use still needs a concrete native producer and consumer. Native maps, dirty ownership, movement, restoration, storage, precision, repeated preparation and the complete recursive bill remain unknown. They are not free. No new kappa or selected-frontier change follows from this algebraic result. + +Ali Romman with substantial OpenAI Codex assistance. Credit Nick Petalas PR5250 and its Arne Storjohann and Ferrer/Mingueza/Montoro lineage; apoursh PR5672; Ali Romman PR5683; David Ganz A030/A026/A029; and classical Kronecker, companion-matrix and finite-field norm theory. Original source notices remain under source/. The new assembly and checks are Apache-2.0. Global literature priority is unclaimed. diff --git a/research/finite-field-pencil-characters/README.md b/research/finite-field-pencil-characters/README.md new file mode 100644 index 0000000000..2e80e3d11d --- /dev/null +++ b/research/finite-field-pencil-characters/README.md @@ -0,0 +1,47 @@ +# Complete supplied finite-field pencil characters + +The determinant-character interface now covers every supplied Kronecker block model over a finite field. This includes regular pencils with no invertible rational slice, nonsplit primaries, arbitrary Jordan lengths and multiplicities, infinity, and all right/left singular mixtures. **No new kappa is claimed.** The model and its coordinate maps must be supplied; arbitrary-tensor extraction remains open. + +For each GL2 slice action R, normalize each regular primary block in its own affine chart. Its cyclic vector gives a literal companion-basis map. Retain R exactly when the transformed block multiset matches. Let `(p_R,q_R,z_R)` be the actual lift determinants, including permutation signs. Let F be the complete fixed-slice determinant subgroup from the singular vectors `(e,-e-1)`, `(-e-1,e)` and the regular length vectors `(ell,-ell)`. Then + +`Delta = union_R {(p_R*x,q_R*y,z_R) : (x,y) in F}`. + +The [proof](PROOF.md) includes all regular/singular Hom spaces, full determinant completeness, a constructive converse, finite SL labels and correction of supplied maps. It preserves the exact slice cosets instead of assuming that all actions of the same determinant have the same lift class. For fixed q, image extraction from the supplied model is deterministic polynomial time in dimension. General norm witnesses have an exact expected-polynomial randomized construction; the bounded executable uses finite enumeration instead. + +A closed family shows the new scope. Put a length-ell Jordan primary, with common multiplicity r, at every point of P1(F_q). Every rational slice is singular. The exact image is + +`Delta = {(x,y,z): x in (F_q*)^ell and x*y*z^(r*ell)=1}`. + +There are `(q-1)*gcd(q-1,ell)` SL orbits. The binary diag(s,t,s+t) example is included. F5 at length two has eight orbits, and F4 at length three has nine. The determinant polynomial alone misses the extra length restriction. + +## Evidence and replay + +```sh +python3.12 -B scripts/research_package.py --package research/finite-field-pencil-characters +python3.12 -I -O -W error -B research/finite-field-pencil-characters/verify.py +``` + +Expected: `PASS_COMPLETE_SUPPLIED_FINITE_FIELD_PENCIL_CHARACTERS`. Python 3.12 and the standard library suffice. Four source files are authenticated before any retained code is imported. Direct replay compares [RESULT.json](RESULT.json) and does not modify publication files. + +The exact finite evidence contains: + +- 320 coefficient-equation Hom cases over F2/F3/F4/F5, including zero indices and finite/infinity regular blocks. +- Sixteen literal stabilizer domains: all GL2 actions in fourteen, and explicit action subsets in two larger cases. All 52,807 linear solutions and 13,042 invertible stabilizers are enumerated across 429 selected slice actions. The oracle imports no lift or character formula. +- Twenty-seven supplied models, with all 4,032 GL2 actions screened and 2,194 literal admitted lifts. All fixed determinant cosets give 7,450 prescribed-action witnesses. +- All 567 determinant triples in those models: 239 witnesses and determinant-one corrections, plus 328 exclusions. Exact image closure and quotient cardinalities pass. +- Nine mathematical controls and nine malformed-model rejections. The controls include the source Jordan sign example, missing global invertible slices, coloured support, nonsplit norms, mixed gcd restrictions and damaged literal maps. + +The executable bounds are indices 0..5, residue degrees and lengths 1..3, multiplicities 1..3, and total dimensions at most sixteen. The declared models are a subset of that domain. The all-dimension finite-field result is the written theorem, not an exhaustive finite census. The bounded residue search is not a general fast norm solver. Polynomial complexity in log(q), arbitrary decomposition discovery and proof-kernel acceptance are not claimed. + +## Use and limits + +This closes the supplied matrix-pencil part of the determinant-image handoff from Nick Petalas PR5250, apoursh PR5672 and Ali Romman PR5683. It provides exact tensor-atlas admissibility and literal SL corrections. A multiplication use still needs a native producer and consumer, paid maps, ownership, movement, restoration, storage, precision and the complete recursive invoice. Those obligations remain unknown. + +Canonical base is `df0137efd35e11b4445734bf612bdd4c7ebc330c`, priority7. Selected .00310045 is unchanged. Normal/optimized replays, committed-byte checks and export checks are separate from hosted CI, independent human review and a complete multiplication theorem. Full-history ancestry preflight is unavailable in this shallow checkout. + +Credit Nick Petalas and the retained centralizer/canonical-form lineage; apoursh for the singular symmetric-power implementation; Ali Romman PR5683 for singular mixing and the coefficient-equation oracle; David Ganz A030/A026/A029; and classical Kronecker and finite-field theory. The four frozen files and notices remain unchanged. New construction, proof and checks: Ali Romman with substantial OpenAI Codex assistance; no subagents. Apache-2.0. Global literature priority is unclaimed. + +## Open next questions + +- Recover a complete Kronecker model and literal factor maps from an arbitrary rectangular tensor. Include zero indices and infinity; do not assume an invertible rational slice. +- Use one classified pencil in a concrete native multiplication interface and price the complete caller. An algebraic stabilizer does not make the correction maps free. diff --git a/research/finite-field-pencil-characters/RESULT.json b/research/finite-field-pencil-characters/RESULT.json new file mode 100644 index 0000000000..a50d4d16a9 --- /dev/null +++ b/research/finite-field-pencil-characters/RESULT.json @@ -0,0 +1,2828 @@ +{ + "controls": { + "malformed_models": 9, + "mathematical_controls": [ + "similarity_determinant", + "length_power_subgroup", + "global_invertible_slice_is_unnecessary", + "unrestricted_slice_group", + "mixed_length_gcd", + "mixed_coprime_characters", + "residue_degree_is_not_block_length", + "literal_row_map_corruption", + "uniform_projective_line_length_character" + ] + }, + "hom_domains": [ + { + "field": 2, + "mixed_Hom_dimension_sum": 48, + "ordered_Hom_cases": 80 + }, + { + "field": 3, + "mixed_Hom_dimension_sum": 48, + "ordered_Hom_cases": 80 + }, + { + "field": 4, + "mixed_Hom_dimension_sum": 48, + "ordered_Hom_cases": 80 + }, + { + "field": 5, + "mixed_Hom_dimension_sum": 48, + "ordered_Hom_cases": 80 + } + ], + "models": [ + { + "SL_orbits": 1, + "accepted_triples": 1, + "admissible_slice_actions": 6, + "determinant_image": [ + [ + 1, + 1, + 1 + ] + ], + "dimensions": [ + 3, + 3 + ], + "excluded_triples": 0, + "field": 2, + "fixed_image": [ + [ + 1, + 1 + ] + ], + "literal_oracle": { + "all_slice_actions": true, + "determinant_triples_seen": 1, + "equation_dimensions": [ + 3 + ], + "invertible_stabilizers": 6, + "linear_solutions": 48, + "slice_actions": 6 + }, + "model": [ + [ + "F", + [ + 0, + 1 + ], + 1, + 1 + ], + [ + "F", + [ + 1, + 1 + ], + 1, + 1 + ], + [ + "I", + 1, + 1 + ] + ], + "name": "binary_full_line", + "prescribed_slice_witnesses": 6, + "supplied_map_SL_corrections": 1, + "total_slice_actions": 6 + }, + { + "SL_orbits": 2, + "accepted_triples": 4, + "admissible_slice_actions": 48, + "determinant_image": [ + [ + 1, + 1, + 1 + ], + [ + 1, + 2, + 2 + ], + [ + 2, + 1, + 2 + ], + [ + 2, + 2, + 1 + ] + ], + "dimensions": [ + 4, + 4 + ], + "excluded_triples": 4, + "field": 3, + "fixed_image": [ + [ + 1, + 1 + ], + [ + 2, + 2 + ] + ], + "literal_oracle": { + "all_slice_actions": true, + "determinant_triples_seen": 4, + "equation_dimensions": [ + 4 + ], + "invertible_stabilizers": 768, + "linear_solutions": 3888, + "slice_actions": 48 + }, + "model": [ + [ + "F", + [ + 0, + 1 + ], + 1, + 1 + ], + [ + "F", + [ + 1, + 1 + ], + 1, + 1 + ], + [ + "F", + [ + 2, + 1 + ], + 1, + 1 + ], + [ + "I", + 1, + 1 + ] + ], + "name": "ternary_full_line", + "prescribed_slice_witnesses": 96, + "supplied_map_SL_corrections": 4, + "total_slice_actions": 48 + }, + { + "SL_orbits": 3, + "accepted_triples": 9, + "admissible_slice_actions": 180, + "determinant_image": [ + [ + 1, + 1, + 1 + ], + [ + 1, + 2, + 3 + ], + [ + 1, + 3, + 2 + ], + [ + 2, + 1, + 3 + ], + [ + 2, + 2, + 2 + ], + [ + 2, + 3, + 1 + ], + [ + 3, + 1, + 2 + ], + [ + 3, + 2, + 1 + ], + [ + 3, + 3, + 3 + ] + ], + "dimensions": [ + 5, + 5 + ], + "excluded_triples": 18, + "field": 4, + "fixed_image": [ + [ + 1, + 1 + ], + [ + 2, + 3 + ], + [ + 3, + 2 + ] + ], + "literal_oracle": { + "all_slice_actions": false, + "determinant_triples_seen": 9, + "equation_dimensions": [ + 5 + ], + "invertible_stabilizers": 1215, + "linear_solutions": 5120, + "slice_actions": 5 + }, + "model": [ + [ + "F", + [ + 0, + 1 + ], + 1, + 1 + ], + [ + "F", + [ + 1, + 1 + ], + 1, + 1 + ], + [ + "F", + [ + 2, + 1 + ], + 1, + 1 + ], + [ + "F", + [ + 3, + 1 + ], + 1, + 1 + ], + [ + "I", + 1, + 1 + ] + ], + "name": "quartic_full_line", + "prescribed_slice_witnesses": 540, + "supplied_map_SL_corrections": 9, + "total_slice_actions": 180 + }, + { + "SL_orbits": 1, + "accepted_triples": 1, + "admissible_slice_actions": 6, + "determinant_image": [ + [ + 1, + 1, + 1 + ] + ], + "dimensions": [ + 6, + 6 + ], + "excluded_triples": 0, + "field": 2, + "fixed_image": [ + [ + 1, + 1 + ] + ], + "literal_oracle": { + "all_slice_actions": true, + "determinant_triples_seen": 1, + "equation_dimensions": [ + 6 + ], + "invertible_stabilizers": 48, + "linear_solutions": 384, + "slice_actions": 6 + }, + "model": [ + [ + "F", + [ + 0, + 1 + ], + 2, + 1 + ], + [ + "F", + [ + 1, + 1 + ], + 2, + 1 + ], + [ + "I", + 2, + 1 + ] + ], + "name": "binary_thick_line", + "prescribed_slice_witnesses": 6, + "supplied_map_SL_corrections": 1, + "total_slice_actions": 6 + }, + { + "SL_orbits": 4, + "accepted_triples": 2, + "admissible_slice_actions": 48, + "determinant_image": [ + [ + 1, + 1, + 1 + ], + [ + 1, + 1, + 2 + ] + ], + "dimensions": [ + 8, + 8 + ], + "excluded_triples": 6, + "field": 3, + "fixed_image": [ + [ + 1, + 1 + ] + ], + "literal_oracle": { + "all_slice_actions": false, + "determinant_triples_seen": 2, + "equation_dimensions": [ + 8 + ], + "invertible_stabilizers": 5184, + "linear_solutions": 26244, + "slice_actions": 4 + }, + "model": [ + [ + "F", + [ + 0, + 1 + ], + 2, + 1 + ], + [ + "F", + [ + 1, + 1 + ], + 2, + 1 + ], + [ + "F", + [ + 2, + 1 + ], + 2, + 1 + ], + [ + "I", + 2, + 1 + ] + ], + "name": "ternary_thick_line", + "prescribed_slice_witnesses": 48, + "supplied_map_SL_corrections": 2, + "total_slice_actions": 48 + }, + { + "SL_orbits": 4, + "accepted_triples": 2, + "admissible_slice_actions": 12, + "determinant_image": [ + [ + 1, + 1, + 1 + ], + [ + 2, + 2, + 2 + ] + ], + "dimensions": [ + 2, + 2 + ], + "excluded_triples": 6, + "field": 3, + "fixed_image": [ + [ + 1, + 1 + ] + ], + "literal_oracle": { + "all_slice_actions": true, + "determinant_triples_seen": 2, + "equation_dimensions": [ + 0, + 2 + ], + "invertible_stabilizers": 72, + "linear_solutions": 144, + "slice_actions": 48 + }, + "model": [ + [ + "F", + [ + 0, + 1 + ], + 2, + 1 + ] + ], + "name": "ternary_jordan", + "prescribed_slice_witnesses": 12, + "supplied_map_SL_corrections": 2, + "total_slice_actions": 48 + }, + { + "SL_orbits": 1, + "accepted_triples": 8, + "admissible_slice_actions": 16, + "determinant_image": [ + [ + 1, + 1, + 1 + ], + [ + 1, + 1, + 2 + ], + [ + 1, + 2, + 1 + ], + [ + 1, + 2, + 2 + ], + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 2 + ], + [ + 2, + 2, + 1 + ], + [ + 2, + 2, + 2 + ] + ], + "dimensions": [ + 2, + 2 + ], + "excluded_triples": 0, + "field": 3, + "fixed_image": [ + [ + 1, + 1 + ], + [ + 2, + 2 + ] + ], + "literal_oracle": { + "all_slice_actions": true, + "determinant_triples_seen": 8, + "equation_dimensions": [ + 0, + 2 + ], + "invertible_stabilizers": 128, + "linear_solutions": 176, + "slice_actions": 48 + }, + "model": [ + [ + "F", + [ + 1, + 0, + 1 + ], + 1, + 1 + ] + ], + "name": "ternary_nonsplit", + "prescribed_slice_witnesses": 32, + "supplied_map_SL_corrections": 8, + "total_slice_actions": 48 + }, + { + "SL_orbits": 4, + "accepted_triples": 2, + "admissible_slice_actions": 16, + "determinant_image": [ + [ + 1, + 1, + 1 + ], + [ + 1, + 1, + 2 + ] + ], + "dimensions": [ + 4, + 4 + ], + "excluded_triples": 6, + "field": 3, + "fixed_image": [ + [ + 1, + 1 + ] + ], + "literal_oracle": { + "all_slice_actions": true, + "determinant_triples_seen": 2, + "equation_dimensions": [ + 0, + 4 + ], + "invertible_stabilizers": 1152, + "linear_solutions": 1328, + "slice_actions": 48 + }, + "model": [ + [ + "F", + [ + 1, + 0, + 1 + ], + 2, + 1 + ] + ], + "name": "ternary_nonsplit_thick", + "prescribed_slice_witnesses": 16, + "supplied_map_SL_corrections": 2, + "total_slice_actions": 48 + }, + { + "SL_orbits": 1, + "accepted_triples": 1, + "admissible_slice_actions": 6, + "determinant_image": [ + [ + 1, + 1, + 1 + ] + ], + "dimensions": [ + 4, + 4 + ], + "excluded_triples": 0, + "field": 2, + "fixed_image": [ + [ + 1, + 1 + ] + ], + "literal_oracle": { + "all_slice_actions": true, + "determinant_triples_seen": 1, + "equation_dimensions": [ + 4 + ], + "invertible_stabilizers": 72, + "linear_solutions": 96, + "slice_actions": 6 + }, + "model": [ + [ + "F", + [ + 1, + 1, + 1 + ], + 2, + 1 + ] + ], + "name": "binary_nonsplit_thick", + "prescribed_slice_witnesses": 6, + "supplied_map_SL_corrections": 1, + "total_slice_actions": 6 + }, + { + "SL_orbits": 1, + "accepted_triples": 1, + "admissible_slice_actions": 3, + "determinant_image": [ + [ + 1, + 1, + 1 + ] + ], + "dimensions": [ + 3, + 3 + ], + "excluded_triples": 0, + "field": 2, + "fixed_image": [ + [ + 1, + 1 + ] + ], + "literal_oracle": { + "all_slice_actions": true, + "determinant_triples_seen": 1, + "equation_dimensions": [ + 0, + 3 + ], + "invertible_stabilizers": 21, + "linear_solutions": 27, + "slice_actions": 6 + }, + "model": [ + [ + "F", + [ + 1, + 1, + 0, + 1 + ], + 1, + 1 + ] + ], + "name": "binary_cubic", + "prescribed_slice_witnesses": 3, + "supplied_map_SL_corrections": 1, + "total_slice_actions": 6 + }, + { + "SL_orbits": 1, + "accepted_triples": 8, + "admissible_slice_actions": 4, + "determinant_image": [ + [ + 1, + 1, + 1 + ], + [ + 1, + 1, + 2 + ], + [ + 1, + 2, + 1 + ], + [ + 1, + 2, + 2 + ], + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 2 + ], + [ + 2, + 2, + 1 + ], + [ + 2, + 2, + 2 + ] + ], + "dimensions": [ + 3, + 3 + ], + "excluded_triples": 0, + "field": 3, + "fixed_image": [ + [ + 1, + 1 + ], + [ + 2, + 2 + ] + ], + "literal_oracle": { + "all_slice_actions": true, + "determinant_triples_seen": 8, + "equation_dimensions": [ + 0, + 1, + 2, + 3 + ], + "invertible_stabilizers": 48, + "linear_solutions": 296, + "slice_actions": 48 + }, + "model": [ + [ + "F", + [ + 0, + 1 + ], + 2, + 1 + ], + [ + "I", + 1, + 1 + ] + ], + "name": "finite_infinity_lengths", + "prescribed_slice_witnesses": 8, + "supplied_map_SL_corrections": 8, + "total_slice_actions": 48 + }, + { + "SL_orbits": 2, + "accepted_triples": 4, + "admissible_slice_actions": 12, + "determinant_image": [ + [ + 1, + 1, + 1 + ], + [ + 1, + 1, + 2 + ], + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 2 + ] + ], + "dimensions": [ + 3, + 4 + ], + "excluded_triples": 4, + "field": 3, + "fixed_image": [ + [ + 1, + 1 + ], + [ + 2, + 1 + ] + ], + "literal_oracle": { + "all_slice_actions": true, + "determinant_triples_seen": 4, + "equation_dimensions": [ + 3, + 5 + ], + "invertible_stabilizers": 1296, + "linear_solutions": 3888, + "slice_actions": 48 + }, + "model": [ + [ + "R", + 1, + 1 + ], + [ + "F", + [ + 0, + 1 + ], + 2, + 1 + ] + ], + "name": "mixed_right_jordan", + "prescribed_slice_witnesses": 24, + "supplied_map_SL_corrections": 4, + "total_slice_actions": 48 + }, + { + "SL_orbits": 2, + "accepted_triples": 4, + "admissible_slice_actions": 12, + "determinant_image": [ + [ + 1, + 1, + 1 + ], + [ + 1, + 2, + 1 + ], + [ + 2, + 1, + 2 + ], + [ + 2, + 2, + 2 + ] + ], + "dimensions": [ + 2, + 3 + ], + "excluded_triples": 4, + "field": 3, + "fixed_image": [ + [ + 1, + 1 + ], + [ + 1, + 2 + ] + ], + "literal_oracle": { + "all_slice_actions": true, + "determinant_triples_seen": 4, + "equation_dimensions": [ + 3, + 5 + ], + "invertible_stabilizers": 1296, + "linear_solutions": 3888, + "slice_actions": 48 + }, + "model": [ + [ + "R", + 0, + 1 + ], + [ + "F", + [ + 0, + 1 + ], + 2, + 1 + ] + ], + "name": "mixed_zero_jordan", + "prescribed_slice_witnesses": 24, + "supplied_map_SL_corrections": 4, + "total_slice_actions": 48 + }, + { + "SL_orbits": 1, + "accepted_triples": 1, + "admissible_slice_actions": 6, + "determinant_image": [ + [ + 1, + 1, + 1 + ] + ], + "dimensions": [ + 5, + 5 + ], + "excluded_triples": 0, + "field": 2, + "fixed_image": [ + [ + 1, + 1 + ] + ], + "literal_oracle": { + "all_slice_actions": true, + "determinant_triples_seen": 1, + "equation_dimensions": [ + 10 + ], + "invertible_stabilizers": 1152, + "linear_solutions": 6144, + "slice_actions": 6 + }, + "model": [ + [ + "R", + 1, + 1 + ], + [ + "L", + 1, + 1 + ], + [ + "F", + [ + 1, + 1, + 1 + ], + 1, + 1 + ] + ], + "name": "mixed_both_nonsplit", + "prescribed_slice_witnesses": 6, + "supplied_map_SL_corrections": 1, + "total_slice_actions": 6 + }, + { + "SL_orbits": 1, + "accepted_triples": 1, + "admissible_slice_actions": 2, + "determinant_image": [ + [ + 1, + 1, + 1 + ] + ], + "dimensions": [ + 2, + 2 + ], + "excluded_triples": 0, + "field": 2, + "fixed_image": [ + [ + 1, + 1 + ] + ], + "literal_oracle": { + "all_slice_actions": true, + "determinant_triples_seen": 1, + "equation_dimensions": [ + 4, + 5 + ], + "invertible_stabilizers": 8, + "linear_solutions": 128, + "slice_actions": 6 + }, + "model": [ + [ + "R", + 0, + 1 + ], + [ + "L", + 0, + 1 + ], + [ + "F", + [ + 0, + 1 + ], + 1, + 1 + ] + ], + "name": "mixed_zero_both", + "prescribed_slice_witnesses": 2, + "supplied_map_SL_corrections": 1, + "total_slice_actions": 6 + }, + { + "SL_orbits": 2, + "accepted_triples": 4, + "admissible_slice_actions": 12, + "determinant_image": [ + [ + 1, + 1, + 1 + ], + [ + 1, + 1, + 2 + ], + [ + 2, + 2, + 1 + ], + [ + 2, + 2, + 2 + ] + ], + "dimensions": [ + 2, + 2 + ], + "excluded_triples": 4, + "field": 3, + "fixed_image": [ + [ + 1, + 1 + ], + [ + 2, + 2 + ] + ], + "literal_oracle": { + "all_slice_actions": true, + "determinant_triples_seen": 4, + "equation_dimensions": [ + 0, + 4 + ], + "invertible_stabilizers": 576, + "linear_solutions": 1008, + "slice_actions": 48 + }, + "model": [ + [ + "F", + [ + 0, + 1 + ], + 1, + 2 + ] + ], + "name": "repeated_regular", + "prescribed_slice_witnesses": 24, + "supplied_map_SL_corrections": 4, + "total_slice_actions": 48 + }, + { + "SL_orbits": 4, + "accepted_triples": 16, + "admissible_slice_actions": 480, + "determinant_image": [ + [ + 1, + 1, + 1 + ], + [ + 1, + 2, + 3 + ], + [ + 1, + 3, + 2 + ], + [ + 1, + 4, + 4 + ], + [ + 2, + 1, + 3 + ], + [ + 2, + 2, + 4 + ], + [ + 2, + 3, + 1 + ], + [ + 2, + 4, + 2 + ], + [ + 3, + 1, + 2 + ], + [ + 3, + 2, + 1 + ], + [ + 3, + 3, + 4 + ], + [ + 3, + 4, + 3 + ], + [ + 4, + 1, + 4 + ], + [ + 4, + 2, + 2 + ], + [ + 4, + 3, + 3 + ], + [ + 4, + 4, + 1 + ] + ], + "dimensions": [ + 6, + 6 + ], + "excluded_triples": 48, + "field": 5, + "fixed_image": [ + [ + 1, + 1 + ], + [ + 2, + 3 + ], + [ + 3, + 2 + ], + [ + 4, + 4 + ] + ], + "model": [ + [ + "F", + [ + 0, + 1 + ], + 1, + 1 + ], + [ + "F", + [ + 1, + 1 + ], + 1, + 1 + ], + [ + "F", + [ + 2, + 1 + ], + 1, + 1 + ], + [ + "F", + [ + 3, + 1 + ], + 1, + 1 + ], + [ + "F", + [ + 4, + 1 + ], + 1, + 1 + ], + [ + "I", + 1, + 1 + ] + ], + "name": "quinary_full_line", + "prescribed_slice_witnesses": 1920, + "supplied_map_SL_corrections": 16, + "total_slice_actions": 480 + }, + { + "SL_orbits": 8, + "accepted_triples": 8, + "admissible_slice_actions": 480, + "determinant_image": [ + [ + 1, + 1, + 1 + ], + [ + 1, + 1, + 4 + ], + [ + 1, + 4, + 2 + ], + [ + 1, + 4, + 3 + ], + [ + 4, + 1, + 2 + ], + [ + 4, + 1, + 3 + ], + [ + 4, + 4, + 1 + ], + [ + 4, + 4, + 4 + ] + ], + "dimensions": [ + 12, + 12 + ], + "excluded_triples": 56, + "field": 5, + "fixed_image": [ + [ + 1, + 1 + ], + [ + 4, + 4 + ] + ], + "model": [ + [ + "F", + [ + 0, + 1 + ], + 2, + 1 + ], + [ + "F", + [ + 1, + 1 + ], + 2, + 1 + ], + [ + "F", + [ + 2, + 1 + ], + 2, + 1 + ], + [ + "F", + [ + 3, + 1 + ], + 2, + 1 + ], + [ + "F", + [ + 4, + 1 + ], + 2, + 1 + ], + [ + "I", + 2, + 1 + ] + ], + "name": "quinary_thick_line", + "prescribed_slice_witnesses": 960, + "supplied_map_SL_corrections": 8, + "total_slice_actions": 480 + }, + { + "SL_orbits": 9, + "accepted_triples": 3, + "admissible_slice_actions": 180, + "determinant_image": [ + [ + 1, + 1, + 1 + ], + [ + 1, + 1, + 2 + ], + [ + 1, + 1, + 3 + ] + ], + "dimensions": [ + 15, + 15 + ], + "excluded_triples": 24, + "field": 4, + "fixed_image": [ + [ + 1, + 1 + ] + ], + "model": [ + [ + "F", + [ + 0, + 1 + ], + 3, + 1 + ], + [ + "F", + [ + 1, + 1 + ], + 3, + 1 + ], + [ + "F", + [ + 2, + 1 + ], + 3, + 1 + ], + [ + "F", + [ + 3, + 1 + ], + 3, + 1 + ], + [ + "I", + 3, + 1 + ] + ], + "name": "quartic_third_order_line", + "prescribed_slice_witnesses": 180, + "supplied_map_SL_corrections": 3, + "total_slice_actions": 180 + }, + { + "SL_orbits": 2, + "accepted_triples": 4, + "admissible_slice_actions": 4, + "determinant_image": [ + [ + 1, + 1, + 1 + ], + [ + 1, + 1, + 2 + ], + [ + 2, + 2, + 1 + ], + [ + 2, + 2, + 2 + ] + ], + "dimensions": [ + 4, + 4 + ], + "excluded_triples": 4, + "field": 3, + "fixed_image": [ + [ + 1, + 1 + ], + [ + 2, + 2 + ] + ], + "model": [ + [ + "F", + [ + 0, + 1 + ], + 1, + 2 + ], + [ + "F", + [ + 1, + 1 + ], + 1, + 1 + ], + [ + "I", + 1, + 1 + ] + ], + "name": "regular_colours", + "prescribed_slice_witnesses": 8, + "supplied_map_SL_corrections": 4, + "total_slice_actions": 48 + }, + { + "SL_orbits": 2, + "accepted_triples": 32, + "admissible_slice_actions": 32, + "determinant_image": [ + [ + 1, + 1, + 1 + ], + [ + 1, + 1, + 4 + ], + [ + 1, + 2, + 2 + ], + [ + 1, + 2, + 3 + ], + [ + 1, + 3, + 2 + ], + [ + 1, + 3, + 3 + ], + [ + 1, + 4, + 1 + ], + [ + 1, + 4, + 4 + ], + [ + 2, + 1, + 2 + ], + [ + 2, + 1, + 3 + ], + [ + 2, + 2, + 1 + ], + [ + 2, + 2, + 4 + ], + [ + 2, + 3, + 1 + ], + [ + 2, + 3, + 4 + ], + [ + 2, + 4, + 2 + ], + [ + 2, + 4, + 3 + ], + [ + 3, + 1, + 2 + ], + [ + 3, + 1, + 3 + ], + [ + 3, + 2, + 1 + ], + [ + 3, + 2, + 4 + ], + [ + 3, + 3, + 1 + ], + [ + 3, + 3, + 4 + ], + [ + 3, + 4, + 2 + ], + [ + 3, + 4, + 3 + ], + [ + 4, + 1, + 1 + ], + [ + 4, + 1, + 4 + ], + [ + 4, + 2, + 2 + ], + [ + 4, + 2, + 3 + ], + [ + 4, + 3, + 2 + ], + [ + 4, + 3, + 3 + ], + [ + 4, + 4, + 1 + ], + [ + 4, + 4, + 4 + ] + ], + "dimensions": [ + 2, + 2 + ], + "excluded_triples": 32, + "field": 5, + "fixed_image": [ + [ + 1, + 1 + ], + [ + 2, + 3 + ], + [ + 3, + 2 + ], + [ + 4, + 4 + ] + ], + "model": [ + [ + "F", + [ + 0, + 1 + ], + 1, + 1 + ], + [ + "I", + 1, + 1 + ] + ], + "name": "two_points_odd", + "prescribed_slice_witnesses": 128, + "supplied_map_SL_corrections": 32, + "total_slice_actions": 480 + }, + { + "SL_orbits": 8, + "accepted_triples": 8, + "admissible_slice_actions": 32, + "determinant_image": [ + [ + 1, + 1, + 1 + ], + [ + 1, + 1, + 4 + ], + [ + 1, + 4, + 2 + ], + [ + 1, + 4, + 3 + ], + [ + 4, + 1, + 2 + ], + [ + 4, + 1, + 3 + ], + [ + 4, + 4, + 1 + ], + [ + 4, + 4, + 4 + ] + ], + "dimensions": [ + 4, + 4 + ], + "excluded_triples": 56, + "field": 5, + "fixed_image": [ + [ + 1, + 1 + ], + [ + 4, + 4 + ] + ], + "model": [ + [ + "F", + [ + 0, + 1 + ], + 2, + 1 + ], + [ + "I", + 2, + 1 + ] + ], + "name": "two_points_even", + "prescribed_slice_witnesses": 64, + "supplied_map_SL_corrections": 8, + "total_slice_actions": 480 + }, + { + "SL_orbits": 1, + "accepted_triples": 64, + "admissible_slice_actions": 80, + "determinant_image": [ + [ + 1, + 1, + 1 + ], + [ + 1, + 1, + 2 + ], + [ + 1, + 1, + 3 + ], + [ + 1, + 1, + 4 + ], + [ + 1, + 2, + 1 + ], + [ + 1, + 2, + 2 + ], + [ + 1, + 2, + 3 + ], + [ + 1, + 2, + 4 + ], + [ + 1, + 3, + 1 + ], + [ + 1, + 3, + 2 + ], + [ + 1, + 3, + 3 + ], + [ + 1, + 3, + 4 + ], + [ + 1, + 4, + 1 + ], + [ + 1, + 4, + 2 + ], + [ + 1, + 4, + 3 + ], + [ + 1, + 4, + 4 + ], + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 2 + ], + [ + 2, + 1, + 3 + ], + [ + 2, + 1, + 4 + ], + [ + 2, + 2, + 1 + ], + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 3 + ], + [ + 2, + 2, + 4 + ], + [ + 2, + 3, + 1 + ], + [ + 2, + 3, + 2 + ], + [ + 2, + 3, + 3 + ], + [ + 2, + 3, + 4 + ], + [ + 2, + 4, + 1 + ], + [ + 2, + 4, + 2 + ], + [ + 2, + 4, + 3 + ], + [ + 2, + 4, + 4 + ], + [ + 3, + 1, + 1 + ], + [ + 3, + 1, + 2 + ], + [ + 3, + 1, + 3 + ], + [ + 3, + 1, + 4 + ], + [ + 3, + 2, + 1 + ], + [ + 3, + 2, + 2 + ], + [ + 3, + 2, + 3 + ], + [ + 3, + 2, + 4 + ], + [ + 3, + 3, + 1 + ], + [ + 3, + 3, + 2 + ], + [ + 3, + 3, + 3 + ], + [ + 3, + 3, + 4 + ], + [ + 3, + 4, + 1 + ], + [ + 3, + 4, + 2 + ], + [ + 3, + 4, + 3 + ], + [ + 3, + 4, + 4 + ], + [ + 4, + 1, + 1 + ], + [ + 4, + 1, + 2 + ], + [ + 4, + 1, + 3 + ], + [ + 4, + 1, + 4 + ], + [ + 4, + 2, + 1 + ], + [ + 4, + 2, + 2 + ], + [ + 4, + 2, + 3 + ], + [ + 4, + 2, + 4 + ], + [ + 4, + 3, + 1 + ], + [ + 4, + 3, + 2 + ], + [ + 4, + 3, + 3 + ], + [ + 4, + 3, + 4 + ], + [ + 4, + 4, + 1 + ], + [ + 4, + 4, + 2 + ], + [ + 4, + 4, + 3 + ], + [ + 4, + 4, + 4 + ] + ], + "dimensions": [ + 5, + 5 + ], + "excluded_triples": 0, + "field": 5, + "fixed_image": [ + [ + 1, + 1 + ], + [ + 1, + 2 + ], + [ + 1, + 3 + ], + [ + 1, + 4 + ], + [ + 2, + 1 + ], + [ + 2, + 2 + ], + [ + 2, + 3 + ], + [ + 2, + 4 + ], + [ + 3, + 1 + ], + [ + 3, + 2 + ], + [ + 3, + 3 + ], + [ + 3, + 4 + ], + [ + 4, + 1 + ], + [ + 4, + 2 + ], + [ + 4, + 3 + ], + [ + 4, + 4 + ] + ], + "model": [ + [ + "R", + 1, + 1 + ], + [ + "L", + 1, + 1 + ], + [ + "F", + [ + 0, + 1 + ], + 2, + 1 + ] + ], + "name": "mixed_coprime_lengths", + "prescribed_slice_witnesses": 1280, + "supplied_map_SL_corrections": 64, + "total_slice_actions": 480 + }, + { + "SL_orbits": 2, + "accepted_triples": 4, + "admissible_slice_actions": 12, + "determinant_image": [ + [ + 1, + 1, + 1 + ], + [ + 1, + 1, + 2 + ], + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 2 + ] + ], + "dimensions": [ + 6, + 8 + ], + "excluded_triples": 4, + "field": 3, + "fixed_image": [ + [ + 1, + 1 + ], + [ + 2, + 1 + ] + ], + "model": [ + [ + "R", + 1, + 1 + ], + [ + "R", + 3, + 1 + ], + [ + "F", + [ + 0, + 1 + ], + 2, + 1 + ] + ], + "name": "mixed_equal_index_gcd", + "prescribed_slice_witnesses": 24, + "supplied_map_SL_corrections": 4, + "total_slice_actions": 48 + }, + { + "SL_orbits": 2, + "accepted_triples": 4, + "admissible_slice_actions": 16, + "determinant_image": [ + [ + 1, + 1, + 1 + ], + [ + 1, + 2, + 2 + ], + [ + 2, + 1, + 1 + ], + [ + 2, + 2, + 2 + ] + ], + "dimensions": [ + 7, + 6 + ], + "excluded_triples": 4, + "field": 3, + "fixed_image": [ + [ + 1, + 1 + ], + [ + 2, + 1 + ] + ], + "model": [ + [ + "L", + 2, + 1 + ], + [ + "F", + [ + 1, + 0, + 1 + ], + 2, + 1 + ] + ], + "name": "mixed_left_nonsplit", + "prescribed_slice_witnesses": 32, + "supplied_map_SL_corrections": 4, + "total_slice_actions": 48 + }, + { + "SL_orbits": 1, + "accepted_triples": 27, + "admissible_slice_actions": 9, + "determinant_image": [ + [ + 1, + 1, + 1 + ], + [ + 1, + 1, + 2 + ], + [ + 1, + 1, + 3 + ], + [ + 1, + 2, + 1 + ], + [ + 1, + 2, + 2 + ], + [ + 1, + 2, + 3 + ], + [ + 1, + 3, + 1 + ], + [ + 1, + 3, + 2 + ], + [ + 1, + 3, + 3 + ], + [ + 2, + 1, + 1 + ], + [ + 2, + 1, + 2 + ], + [ + 2, + 1, + 3 + ], + [ + 2, + 2, + 1 + ], + [ + 2, + 2, + 2 + ], + [ + 2, + 2, + 3 + ], + [ + 2, + 3, + 1 + ], + [ + 2, + 3, + 2 + ], + [ + 2, + 3, + 3 + ], + [ + 3, + 1, + 1 + ], + [ + 3, + 1, + 2 + ], + [ + 3, + 1, + 3 + ], + [ + 3, + 2, + 1 + ], + [ + 3, + 2, + 2 + ], + [ + 3, + 2, + 3 + ], + [ + 3, + 3, + 1 + ], + [ + 3, + 3, + 2 + ], + [ + 3, + 3, + 3 + ] + ], + "dimensions": [ + 5, + 6 + ], + "excluded_triples": 0, + "field": 4, + "fixed_image": [ + [ + 1, + 1 + ], + [ + 1, + 2 + ], + [ + 1, + 3 + ], + [ + 2, + 1 + ], + [ + 2, + 2 + ], + [ + 2, + 3 + ], + [ + 3, + 1 + ], + [ + 3, + 2 + ], + [ + 3, + 3 + ] + ], + "model": [ + [ + "R", + 0, + 1 + ], + [ + "F", + [ + 0, + 1 + ], + 3, + 1 + ], + [ + "I", + 2, + 1 + ] + ], + "name": "mixed_regular_lengths", + "prescribed_slice_witnesses": 81, + "supplied_map_SL_corrections": 27, + "total_slice_actions": 180 + }, + { + "SL_orbits": 4, + "accepted_triples": 16, + "admissible_slice_actions": 480, + "determinant_image": [ + [ + 1, + 1, + 1 + ], + [ + 1, + 1, + 4 + ], + [ + 1, + 4, + 2 + ], + [ + 1, + 4, + 3 + ], + [ + 2, + 1, + 2 + ], + [ + 2, + 1, + 3 + ], + [ + 2, + 4, + 1 + ], + [ + 2, + 4, + 4 + ], + [ + 3, + 1, + 2 + ], + [ + 3, + 1, + 3 + ], + [ + 3, + 4, + 1 + ], + [ + 3, + 4, + 4 + ], + [ + 4, + 1, + 1 + ], + [ + 4, + 1, + 4 + ], + [ + 4, + 4, + 2 + ], + [ + 4, + 4, + 3 + ] + ], + "dimensions": [ + 4, + 4 + ], + "excluded_triples": 48, + "field": 5, + "fixed_image": [ + [ + 1, + 1 + ], + [ + 2, + 4 + ], + [ + 3, + 4 + ], + [ + 4, + 1 + ] + ], + "model": [ + [ + "R", + 1, + 1 + ], + [ + "L", + 2, + 1 + ] + ], + "name": "pure_singular_control", + "prescribed_slice_witnesses": 1920, + "supplied_map_SL_corrections": 16, + "total_slice_actions": 480 + } + ], + "scope": "All-dimension finite-field proof for supplied complete block models. Bounded literal evidence; no arbitrary extraction or physical caller.", + "status": "PASS_COMPLETE_SUPPLIED_FINITE_FIELD_PENCIL_CHARACTERS" +} diff --git a/research/finite-field-pencil-characters/SOURCES.json b/research/finite-field-pencil-characters/SOURCES.json new file mode 100644 index 0000000000..54c13dfc2d --- /dev/null +++ b/research/finite-field-pencil-characters/SOURCES.json @@ -0,0 +1,46 @@ +{ + "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/mixed-singular-kronecker-characters/source/pencil.py", + "usage": "provenance", + "pin": "head:618fb04433927ade44ed5b507f8d30f9ede2bde5:research/mixed-singular-kronecker-characters/source/pencil.py", + "git_blob": "6bc7fc076e6ce2418ec9ed05d85115deb3d4bdd2", + "sha256": "a714862853cc884e84eac34ba1d7ccb14a6326bcfadb630910034bb44bd305db" + }, + { + "path": "research/mixed-singular-kronecker-characters/oracle.py", + "usage": "provenance", + "pin": "head:618fb04433927ade44ed5b507f8d30f9ede2bde5:research/mixed-singular-kronecker-characters/oracle.py", + "git_blob": "6535d1363ece5521d75a6ef218f4e68a5c2eeb5d", + "sha256": "9713ec418b158055658c3a53766f305d6e3734e7b775c8bbd365a46e525966aa" + }, + { + "path": "research/mixed-singular-kronecker-characters/PROOF.md", + "usage": "provenance", + "pin": "head:618fb04433927ade44ed5b507f8d30f9ede2bde5:research/mixed-singular-kronecker-characters/PROOF.md", + "git_blob": "9de07b628089ab903751ea2571b62b08dba7e524", + "sha256": "2d0b2348bb27063e7bf34769b1a43c90d593902f043ffc438d7ec887f0016295" + }, + { + "path": "research/pencil-determinant-image/README.md", + "usage": "provenance", + "pin": "head:43142bedc7cb5c0f1f73ff3fea6d9bfd237949ee:research/pencil-determinant-image/README.md", + "git_blob": "20f8262d3747f28e4535ec3f928f7481f8306749", + "sha256": "ba945687c23f6e675e2c320c7e5ccf345b17090e4d4283721ff950d62da5516e" + } + ] +} diff --git a/research/finite-field-pencil-characters/TASK.json b/research/finite-field-pencil-characters/TASK.json new file mode 100644 index 0000000000..7894027389 --- /dev/null +++ b/research/finite-field-pencil-characters/TASK.json @@ -0,0 +1,101 @@ +{ + "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": "Complete determinant images, SL labels and literal corrections for supplied finite-field Kronecker models, including regular blocks without an invertible rational slice and all regular/singular mixing.", + "scope_change_reason": "The released PR5250/5672/5683 handoff requires a written finite-field theorem and exact evidence, not a Lean formalization. Per-primary chart normalization removes the missing global-slice premise.", + "bottleneck_link": "Exact tensor-atlas admissibility and map correction can screen alternatives without accepting invalid determinant classes. A physical caller and all its costs are still required; no kappa gain is inferred.", + "budget_minutes": 120, + "stop_rule": "Complete the supplied-model theorem and bounded independent checks. Do not add arbitrary-tensor extraction or an unpriced physical caller.", + "outcome": "completed", + "evidence": "PROOF.md and RESULT.json: 27 models, 320 Hom cases, 52807 literal solutions, 2194 admitted slice lifts, 7450 prescribed-action witnesses and 239 SL corrections.", + "author": "Ali Romman with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance for proof, implementation, exact verification and publication. No subagents.", + "open_questions": [ + { + "question": "Can an arbitrary rectangular pencil be reduced to this model with checked row, column and slice maps?", + "why_it_matters": "The input currently supplies a complete Kronecker model.", + "first_step": "Pin an exact canonical-form algorithm and return literal factor maps, including zero indices and regular infinity blocks.", + "blocked_by": "Constructive model extraction, not the supplied-model determinant theorem." + }, + { + "question": "Which native multiplication interface can use a classified pencil?", + "why_it_matters": "A tensor stabilizer does not provide a paid supplier.", + "first_step": "Name the actual producer and consumer, and charge native maps, ownership, routes, restoration, storage and precision.", + "blocked_by": "A complete physical construction and recursive bill." + } + ] +} diff --git a/research/finite-field-pencil-characters/VERIFY.json b/research/finite-field-pencil-characters/VERIFY.json new file mode 100644 index 0000000000..81e823f5e4 --- /dev/null +++ b/research/finite-field-pencil-characters/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 570, + "checks": "All declared literal equation spaces, primary-chart lifts, Hom dimensions, determinant cosets, prescribed-action witnesses, SL corrections and rejection controls" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 570, + "checks": "All declared literal equation spaces, primary-chart lifts, Hom dimensions, determinant cosets, prescribed-action witnesses, SL corrections and rejection controls" + } + ] +} diff --git a/research/finite-field-pencil-characters/pencils.py b/research/finite-field-pencil-characters/pencils.py new file mode 100644 index 0000000000..45c52fbee6 --- /dev/null +++ b/research/finite-field-pencil-characters/pencils.py @@ -0,0 +1,280 @@ +"""Exact determinant maps for bounded supplied finite-field pencil models. + +Credit the retained Kronecker lifts and field arithmetic. The regular block +normalization and mixed character assembly are new in this package. +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +from hashlib import sha256 +from itertools import product +from pathlib import Path +import importlib.util +import json + +ROOT = Path(__file__).resolve().parent +for item in json.loads((ROOT / 'INPUTS.json').read_text()): + if sha256((ROOT / item['local']).read_bytes()).hexdigest() != item['sha256']: + raise ValueError('Frozen source differs: ' + item['local']) +spec = importlib.util.spec_from_file_location('credited_pencil', ROOT / 'source/pencil.py') +old = importlib.util.module_from_spec(spec) +spec.loader.exec_module(old) +Field = old.Field +need = old.require + + +def poly_mul(a, b, f): + out = [0] * (len(a) + len(b) - 1) + for i, x in enumerate(a): + for j, y in enumerate(b): + out[i+j] = f.add(out[i+j], f.mul(x, y)) + return out + + +def poly_power(a, n, f): + out = [1] + for _ in range(n): + out = poly_mul(out, a, f) + return out + + +def remainder(a, b, f): + a = list(a) + while len(a) >= len(b): + x = f.mul(a[-1], f.inv(b[-1])); offset = len(a)-len(b) + for j, y in enumerate(b): + a[offset+j] = f.sub(a[offset+j], f.mul(x, y)) + a.pop() + return a + + +def irreducible(a, f): + for degree in range(1, (len(a)-1)//2+1): + for low in product(range(f.q), repeat=degree): + if not any(remainder(a, list(low)+[1], f)): + return False + return True + + +def companion(poly, f): + n = len(poly)-1 + out = [[0]*n for _ in range(n)] + for i in range(1, n): + out[i][i-1] = 1 + for i in range(n): + out[i][-1] = f.neg(poly[i]) + return out + + +def matrix_sum(a, b, x, y, f): + return [[f.add(f.mul(x, u), f.mul(y, v)) for u, v in zip(row, other)] + for row, other in zip(a, b)] + + +def evaluate(poly, matrix, f): + n = len(matrix); out = [[0]*n for _ in range(n)]; power = old.identity(n) + for coefficient in poly: + out = matrix_sum(out, power, 1, coefficient, f) + power = old.multiply(power, matrix, f) + return out + + +def normalized(model, f): + need(isinstance(model, (list, tuple)) and model, 'Nonempty supplied model') + out = []; total_m = total_n = 0; keys = set() + for block in model: + need(isinstance(block, (list, tuple)) and block, 'Block record') + side = block[0] + if side in ('R', 'L'): + need(len(block) == 3, 'Singular record arity') + _, e, r = block + need(type(e) is int and 0 <= e <= 5 and type(r) is int and 1 <= r <= 3, 'Singular bounds') + key = (side, e); m = (e+(side == 'L'))*r; n = (e+(side == 'R'))*r + out.append(dict(side=side, e=e, r=r, m=m, n=n, row=total_m, col=total_n, key=key)) + else: + need(side in ('F', 'I'), 'Known block type') + need(len(block) == (4 if side == 'F' else 3), 'Regular record arity') + if side == 'F': + _, poly, length, r = block + need(isinstance(poly, (tuple, list)) and 2 <= len(poly) <= 4 and poly[-1] == 1 and + all(type(x) is int and 0 <= x < f.q for x in poly), 'Monic bounded polynomial') + need(irreducible(poly, f), 'Irreducible regular primary') + poly = tuple(poly) + else: + _, length, r = block; poly = (0, 1) + need(type(length) is int and 1 <= length <= 3 and type(r) is int and 1 <= r <= 3, 'Regular bounds') + key = (side, poly, length); degree = (len(poly)-1)*length + m = n = degree*r + out.append(dict(side=side, poly=poly, length=length, r=r, degree=degree, + m=m, n=n, row=total_m, col=total_n, key=key)) + need(key not in keys, 'Combine identical block types in the supplied model') + keys.add(key); total_m += m; total_n += n + need(0 < total_m <= 16 and 0 < total_n <= 16, 'Positive total dimensions at most sixteen') + return out, total_m, total_n + + +def regular_instances(parts, f): + out = [] + for part in parts: + if part['side'] in ('F', 'I'): + poly = poly_power(part['poly'], part['length'], f) + j = companion(poly, f); identity = old.identity(len(j)) + a, b = (identity, j) if part['side'] == 'F' else (j, identity) + key = (part['side'], tuple(poly)) + for i in range(part['r']): + out.append(dict(a=a, b=b, key=key, part=part, row=part['row']+i*len(j), col=part['col']+i*len(j))) + return out + + +def put(matrix, block, row, col): + for i, values in enumerate(block): + matrix[row+i][col:col+len(values)] = values + + +def slices(parts, m, n, f): + a = [[0]*n for _ in range(m)]; b = [[0]*n for _ in range(m)] + for part in parts: + if part['side'] in ('R', 'L'): + for i in range(part['e']): + for j in range(part['r']): + x = part['row']+i*part['r']+j; y = part['col']+i*part['r']+j + a[x][y] = 1 + if part['side'] == 'R': b[x][y+part['r']] = 1 + else: b[x+part['r']][y] = 1 + for item in regular_instances(parts, f): + put(a, item['a'], item['row'], item['col']); put(b, item['b'], item['row'], item['col']) + return a, b + + +def singular_lift(part, action, determinant, f): + d = old.identity(part['r']); d[0][0] = determinant + if part['e']: p, q, _ = old.lift(part['e'], part['r'], action, d, f) + else: p, q = [], old.transpose(old.inverse(d, f)) + return (q, p) if part['side'] == 'L' else (p, q) + + +def cyclic_normalize(a, b, action, f): + """Use one primary block's affine chart and its cyclic vector.""" + first = matrix_sum(a, b, *action[0], f); second = matrix_sum(a, b, *action[1], f) + finite = old.determinant(first, f) != 0 + base, other = (first, second) if finite else (second, first) + need(old.determinant(base, f) != 0, 'A regular primary block has an invertible chart') + inverse = old.inverse(base, f); h = old.multiply(inverse, other, f); n = len(h) + v = [[int(i == 0)] for i in range(n)]; columns = [] + for _ in range(n): + columns.append([row[0] for row in v]); v = old.multiply(h, v, f) + krylov = old.transpose(columns); need(old.determinant(krylov, f) != 0, 'The fractional transform keeps the cyclic vector') + ki = old.inverse(krylov, f); canonical = old.multiply(old.multiply(ki, h, f), krylov, f) + poly = tuple(f.neg(row[-1]) for row in canonical)+(1,) + need(canonical == companion(poly, f), 'Literal companion normalization') + if not finite: need(poly == (0,)*n+(1,), 'The infinity chart is nilpotent') + return ('F' if finite else 'I', poly), old.multiply(ki, inverse, f), old.transpose(krylov) + + +def slice_lift(parts, m, n, action, f): + ps = [[0]*m for _ in range(m)]; qs = [[0]*n for _ in range(n)] + for part in parts: + if part['side'] in ('R', 'L'): + p, q = singular_lift(part, action, 1, f) + put(ps, p, part['row'], part['row']); put(qs, q, part['col'], part['col']) + instances = regular_instances(parts, f); unused = set(range(len(instances))) + for source in instances: + key, p, q = cyclic_normalize(source['a'], source['b'], action, f) + target = next((i for i in sorted(unused) if instances[i]['key'] == key), None) + if target is None: return None + unused.remove(target); dest = instances[target] + put(ps, p, dest['row'], source['row']); put(qs, q, dest['col'], source['col']) + return ps, qs, action + + +def norm_unit(poly, target, f): + """Bounded exhaustive residue search; no general fast norm solver is claimed.""" + small = companion(poly, f) + for coefficients in product(range(f.q), repeat=len(poly)-1): + if old.determinant(evaluate(coefficients, small, f), f) == target: + return coefficients + raise ValueError('Finite field norm must be onto') + + +def fixed_generators(parts, m, n, f): + out = [] + for part in parts: + for u in range(1, f.q): + p, q = old.identity(m), old.identity(n) + if part['side'] in ('R', 'L'): + bp, bq = singular_lift(part, old.identity(2), u, f) + else: + poly = poly_power(part['poly'], part['length'], f); j = companion(poly, f) + coefficients = norm_unit(part['poly'], u, f) if part['side'] == 'F' else [u] + bp = evaluate(coefficients, j, f); bq = old.transpose(old.inverse(bp, f)) + need(old.determinant(bp, f) == f.power(u, part['length']), 'Norm and length determinant') + put(p, bp, part['row'], part['row']); put(q, bq, part['col'], part['col']) + out.append((p, q)) + return out + + +def pair_mul(a, b, f): + return tuple(f.mul(x, y) for x, y in zip(a, b)) + + +def compile_model(model, f): + parts, m, n = normalized(model, f); a, b = slices(parts, m, n, f) + fixed = {(1, 1): (old.identity(m), old.identity(n))}; queue = [(1, 1)] + generators = [(tuple(old.determinant(x, f) for x in pair), pair) for pair in fixed_generators(parts, m, n, f)] + for key in queue: + for char, pair in generators: + target = pair_mul(key, char, f) + if target not in fixed: + fixed[target] = tuple(old.multiply(x, y, f) for x, y in zip(fixed[key], pair)); queue.append(target) + image = {}; lifts = []; actions = 0 + for action in old.general_linear_two(f): + actions += 1; lift = slice_lift(parts, m, n, action, f) + if lift is None: continue + need(old.fixes(a, b, lift, f), 'Literal regular and singular slice lift') + char = tuple(old.determinant(x, f) for x in lift); lifts.append((char, lift)) + for key, pair in fixed.items(): + triple = pair_mul(char, key+(1,), f) + image.setdefault(triple, (pair, lift)) + return dict(model=model, parts=parts, dimensions=(m, n), slices=(a, b), fixed=fixed, lifts=lifts, + image=image, slice_actions=actions, field=f) + + +def witness(compiled, triple, action=None): + f = compiled['field']; triple = tuple(triple) + need(len(triple) == 3 and all(type(x) is int and 0 < x < f.q for x in triple), 'Nonzero determinant triple') + need(triple in compiled['image'], 'Excluded determinant triple') + pair, lift = compiled['image'][triple] + if action is not None: + choices = [(char, candidate) for char, candidate in compiled['lifts'] if candidate[2] == action] + need(choices, 'Excluded prescribed slice action') + char, lift = choices[0] + need(char[2] == triple[2], 'Prescribed slice determinant') + key = tuple(f.mul(x, f.inv(y)) for x, y in zip(triple[:2], char[:2])) + need(key in compiled['fixed'], 'Excluded prescribed slice coset') + pair = compiled['fixed'][key] + result = tuple(old.multiply(x, y, f) for x, y in zip(pair, lift[:2]))+(lift[2],) + need(old.fixes(*compiled['slices'], result, f), 'Literal determinant witness') + need(tuple(old.determinant(x, f) for x in result) == triple, 'Requested determinant witness') + return result + + +def tensor_image(slices, maps, f): + a, b = slices; p, q, action = maps + return tuple(old.multiply(old.multiply(p, matrix_sum(a, b, x, y, f), f), old.transpose(q), f) for x, y in action) + + +def correct_map(compiled, maps): + f = compiled['field']; triple = tuple(old.determinant(x, f) for x in maps) + h = witness(compiled, triple) + result = tuple(old.multiply(g, old.inverse(x, f), f) for g, x in zip(maps, h)) + need(all(old.determinant(x, f) == 1 for x in result), 'Three determinant-one factors') + need(tensor_image(compiled['slices'], maps, f) == tensor_image(compiled['slices'], result, f), 'Unchanged tensor image') + return result + + +def orbit_labels(compiled): + f = compiled['field']; labels = {} + for triple in product(range(1, f.q), repeat=3): + if triple not in labels: + for delta in compiled['image']: + labels[pair_mul(triple, delta, f)] = triple + need(len(labels) == (f.q-1)**3 and len(set(labels.values()))*len(compiled['image']) == len(labels), 'Finite quotient cardinality') + return labels diff --git a/research/finite-field-pencil-characters/source/REGULAR.md b/research/finite-field-pencil-characters/source/REGULAR.md new file mode 100644 index 0000000000..20f8262d37 --- /dev/null +++ b/research/finite-field-pencil-characters/source/REGULAR.md @@ -0,0 +1,221 @@ +# Exact determinant images for invertible-slice matrix pencils + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Claim type: scoped written proof with exact finite corroboration.** +For every fixed finite field, the stabilizer determinant image of a square +matrix-pencil tensor with an invertible slice has an explicit formula and a +deterministic polynomial-time extraction algorithm. This settles that subclass +of David Ganz's [atlas A030](../pure-math-atlas-400/volumes/01-algebra.md#a030), +from [PR #2849](https://github.com/CrocSwap/integer-mult-bounds/pull/2849). +The general arbitrary-tensor proposal remains open. No new kappa, physical +supplier, selected-frontier change or complete multiplication theorem is claimed. +Global literature priority is unclaimed. + +The new step is the complete determinant-coset assembly over the slice actions, +including the similarity witness's determinant. Frobenius canonical forms, +centralizer structure and the atlas's character compression are predecessors. +The centralizer identity below is classical; it is not claimed as a new theorem +or offered as an audit of its authors. + +## Convention and theorem + +Let K=F_q, n>=1 and M in Mat_n(K). The tensor has ordered matrix slices (I,M), +with action + +```text +(P,Q,R): (I,M) -> (P(aI+bM)Q^T, P(cI+dM)Q^T), +R = [[a,b],[c,d]] in GL_2(K), P,Q in GL_n(K). +``` + +Write Delta_M for the image of its stabilizer under +`(P,Q,R) -> (det P, det Q, det R)`. +For each monic irreducible f, write the K[t]-module associated to M as + +```text +V_f = direct sum over e>=1 of (K[t]/f^e)^(m_f,e). +g = gcd(q-1, every e for which some m_f,e > 0). +H = {x^g : x in K*}. +``` + +For each R in GL_2(K), put B_R=aI+bM. Retain R precisely when B_R is invertible +and `N_R=(cI+dM) B_R^-1` is similar to M. Choose any P_R such that +`P_R N_R P_R^-1=M`, and set z_R=det P_R and b_R=det B_R. Then + +```text +Delta_M = union over retained R of + {(z_R h, (b_R z_R h)^-1, det R) : h in H}. (1) +``` + +Every triple on the right occurs, and no others occur. The answer is independent +of the choices of P_R. Scalar M and linearly dependent slices are included. +If an invertible slice exists but is not first, a search of the q+1 slice +directions finds one and a GL_2 action puts it first. For slices (A0,A1) with +A0 invertible, use M=A0^-1 A1. Normalization +is a GL tensor action. Conjugation of the stabilizer preserves each determinant, +so (1) gives the same determinant image in the original coordinates. + +## Proof + +The first stabilizer equation forces B_R invertible and +`Q^T=B_R^-1 P^-1`. Substitution into the second gives +`P N_R P^-1=M`. Conversely those two conditions and that definition of Q satisfy +both original equations. Thus retained R are exactly the feasible slice actions. +All admissible P for one retained R are `C P_R`, where C is an invertible +centralizer of M. Their determinants are exactly `z_R det(C)`. Taking the +determinant of the forced Q gives the second entry of (1). + +It remains to identify `det(C_GL_n(K)(M))` as H. Here are the module details, +including nonsplit primary factors. Distinct f-primary summands have no +intertwiners, by Bezout's identity, so their determinants multiply independently. +Fix f of degree d, put E=K[t]/f, and filter V_f by powers of f. Each quotient +`f^(k-1)V_f/f^k V_f` is an E-vector space with one group of m_f,e coordinates +for each e>=k. An intertwiner from a length-s summand to a length-e summand +has image divisible by `f^max(e-s,0)`. Consequently its induced matrix on +that quotient is triangular when the summands are ordered by length. Its +exact-length-e diagonal matrix U_f,e over E is the same on every layer k<=e. +Invertibility forces every U_f,e invertible. Multiplicativity of determinant +along this invariant filtration therefore gives + +```text +det_K C = product over f,e of Norm_(E/K)(det_E U_f,e)^e. (2) +``` + +For the reverse inclusion, choose one copy of K[t]/f^e and multiply it by any +unit lifting u in E*. This commutes with M, fixes the other copies, and has +K-determinant `Norm_(E/K)(u)^e`. The norm on finite fields is surjective: on +cyclic E* it is the power `(q^d-1)/(q-1)`, with image of order q-1. Hence the +centralizer determinant image contains every e-th power in K*. Equation (2) +gives the reverse containment in the subgroup generated by those powers. +Cyclicity of K* identifies that subgroup with H. This proves (1) and its +attainment statement. A different P_R differs by a centralizer element, so +it changes z_R only by an element of H. + +The Jordan/Weyr version of (2) is classical. See Josep Ferrer, David Mingueza +and M. Eulalia Montoro, *Determinant of any matrix that belongs to Z(J)*, +[EACA 2014, Theorem 4.3, printed pages 111-114](https://www.maia.ub.edu/~sombra/publications/EACA2014/2014_EACA_Conference_Proceedings.pdf#page=113). +The filtration above explains the finite-field norm needed here. + +## Deterministic extraction for each fixed q + +1. Compute a Frobenius form of M with its transformation matrix. This is a + deterministic polynomial-time subroutine over arbitrary fields, due to + [Arne Storjohann, FOCS 2001](https://doi.org/10.1109/SFCS.2001.959911). + The [Pernet-Storjohann primary paper, introduction](https://cs.uwaterloo.ca/~astorjoh/cpoly.pdf) + also records the deterministic result; its separate randomized large-field + algorithm is not the premise used here. +2. Squarefree-decompose each invariant-factor polynomial h of M and take the + gcd of q-1 and every multiplicity that occurs. This computes g without + irreducible factorization. Indeed those multiplicities are exactly the + elementary-divisor exponents appearing in h. Derivatives and polynomial + gcds separate unequal multiplicities. When a residual derivative vanishes, + take its characteristic-p-th root and multiply subsequent multiplicities + by p. Finite fields are perfect. Each such root lowers the positive degree, + so this procedure uses polynomially many field operations for fixed q. +3. Enumerate GL_2(K), at most q^4 matrices. Form B_R and N_R. Compare Frobenius + forms, and obtain P_R from their transformation matrices when they agree. + For `S_M^-1 M S_M = S_N^-1 N_R S_N`, take `P_R=S_M S_N^-1`. +4. Evaluate (1). At most `|GL_2(K)| |H|` triples are inserted. For fixed q + this is constant output size, independent of n. The algorithm enumerates + neither GL_n(K) nor the centralizer's units nor the tensor stabilizer. +5. If A030's equation-table output is wanted, enumerate the at most `(q-1)^3` + monomial characters and retain those equal to one on every output triple. + Their common kernel is Delta_M, by finite abelian duality. The annihilator + is generated by at most three characters, as in atlas A026/A029, so choose + a generating triple by a constant-size search and pad with zero rows. + +These steps prove deterministic polynomial time in n for each fixed q. They +make no uniform polynomial-in-log(q) claim. The general-size Frobenius and +squarefree-decomposition implementations are not supplied or benchmarked here; +they are established subroutines in this written reduction. The executable +below is an independent finite corroborator, not that polynomial-time program. + +## First discriminator and bounded evidence + +For `M=[[0,1],[0,0]]` over F3, g=2 and H={1}. The retained R have c=0 and +nonzero a,d. One may take `P_R=diag(a/d,1)`, giving z_R=a/d and b_R=a^2. +Equation (1) yields exactly + +```text +Delta_M = {(1,1,1), (2,2,2)}. +``` + +Replacing H by all of F3* or omitting z_R gives a different answer. Both are +explicit rejection controls in the verifier. + +The verifier uses no predecessor executable or external package. It enumerates +every P,Q,R literally on every 2-by-2 matrix M over F2 and F3, and compares +that determinant image with a separately implemented version of (1). + +- F2: 16 slices, 3,456 literal triples tested, 96 stabilizers. +- F3: 81 slices, 8,957,952 literal triples tested, 6,912 stabilizers. The image + sizes are 2 on 24 slices, 4 on 3 slices, and 8 on 54 slices. +- Eleven independent centralizer fixtures include repeated unequal block + lengths, coprime block-length gcd, scalar matrices, and nonsplit irreducible + degree-two blocks with exponents one and two. Their centralizer vector spaces + are enumerated exactly; the largest has 19,683 elements. + +These are finite corroboration of the written proof, not an exhaustive check +of all fields or dimensions. The centralizer checks support this new formula; +re-checking a predecessor result is not the deliverable. + +## Reproduce + +From the repository root, using CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/pencil-determinant-image/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/pencil-determinant-image/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/pencil-determinant-image +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/pencil-determinant-image --check-source-history +``` + +Any CPython 3.12 interpreter path may replace the absolute path. The direct +marker is `PASS_PENCIL_DETERMINANT_IMAGE fields=2,3 tensor_slices=97 controls=2`. +A generated JSON receipt binds the five package files and exact enumerated +results. The program writes no files, uses explicit checks that survive `-O`, +and needs no Git for direct replay. Each registered command has a 120-second +limit; local replay is below five seconds on the recorded environment. + +## Scope, engineering and credit + +The result requires a square pencil and an invertible slice over K. It does +not cover singular Kronecker blocks or regular pencils without a K-rational +invertible slice. The general arbitrary-tensor extraction proposal, transporter +height bounds and GL-to-SL compilation remain separate questions. There is no +physical access, dirty-state, routing, precision, recursive-invoice or supplier +admission result. Independent human and formal proof-kernel review are unclaimed. +No Lean build, selected cold replay or complete multiplication theorem was run. + +This package changes the formal-interface-lemma card to a mathematical tensor +side question explicitly left open in the atlas. It does not formalize a Lean +statement or resolve a selected-supplier hypothesis. Exact historical card and +source pins are in SOURCES.json; they are provenance, not live replay inputs. + +Engineering uses a fixed finite domain, pure arithmetic functions and explicit +invariant failures. Each loop has a finite bound from those fixtures; centralizer +enumeration enforces a 25,000-element cap before allocating combinations. No +function exceeds 60 lines. Python's managed allocation is a Power-of-Ten rule-3 +deviation: matrix tables have at most 81 entries per axis, module dimension is +at most five, and at most 19,683 centralizer candidates are generated one at a +time. Static inspection and both registered replays check these bounds. A future +CLI accepting general inputs must introduce explicit input/resource bounds before +reusing this finite verifier. No compiler diagnostics exist for this Python file; +warning-strict normal and optimized execution are the applicable checks. + +David Ganz retains credit for atlas A030, the determinant-image formulation, +A026/A029 and the atlas's cited tensor/stabilizer lineage. Arne Storjohann and +the cited canonical-form authors retain their algorithm credit. Ferrer, Mingueza +and Montoro retain the classical centralizer determinant credit. Only the +restricted extraction reduction and exact image assembly are claimed here. + +## Open next questions + +- Extend the determinant-image assembly to regular square pencils having no + invertible K-rational slice. The binary homogeneous elementary divisors offer + a first step; the missing issue is a coordinate-independent replacement for + B_R inverse. This would remove the rational-slice restriction. +- Handle singular Kronecker blocks and rectangular pencils. Begin with the + determinant characters of one left/right minimal-index block and its + multiplicity space. Couplings between block types and slice transformations + remain the obstruction to extending this proof. diff --git a/research/finite-field-pencil-characters/source/SINGULAR.md b/research/finite-field-pencil-characters/source/SINGULAR.md new file mode 100644 index 0000000000..9de07b6280 --- /dev/null +++ b/research/finite-field-pencil-characters/source/SINGULAR.md @@ -0,0 +1,146 @@ +# Determinant characters for all purely singular Kronecker sums + +## 1. Scope and action + +Let K be any field. Let R_e be the e by e+1 pencil with s on the diagonal and t above it, and let L_e=R_e^T be its left orientation. The predecessor calls the right block L_e; this note uses R and L to mark the two orientations. Minimal indices e can be zero. Thus R_0 has shape 0 by 1 and L_0 has shape 1 by 0. + +Let T be a finite direct sum of these blocks with positive multiplicities. Combine repeated equal types. Both total row and column dimensions m,n must be positive. The result does not include a regular block. The model is supplied; extraction from an arbitrary tensor is a separate task. + +Use exactly the predecessor's covariant action + +`(A0,A1) -> (P(a A0+b A1)Q^T, P(c A0+d A1)Q^T)`, + +where `R=[[a,b],[c,d]]` is the slice factor. Let Delta(T) be the image of its stabilizer under `(det P,det Q,det R)`. The right factor is Q^T, not Q^-1. All pencil equations are coefficient identities in two independent indeterminates, including over finite fields. + +The source is apoursh PR5672 at `81c0577b83cdafa73346da8ade1261b0b202e45f`, following Nick Petalas PR5250. Its single-type theorem, characteristic-safe slice lift and exact action convention remain predecessor work. This note supplies the complete mixed singular extension. + +## 2. Explicit intertwiner spaces + +A morphism from a source block to a destination block is a pair U,C with + +`U T_source(s,t)=T_destination(s,t) C`. + +For a source with shape ms by ns and destination with shape md by nd, U has shape md by ms and C has shape nd by ns. Comparing the s and t coefficients gives the following complete table: + +| Source | Destination | Dimension | Form | +| --- | --- | ---: | --- | +| R_e | R_f | max(e-f+1,0) | Rectangular upper Toeplitz | +| L_e | L_f | max(f-e+1,0) | Transpose dual of the preceding row | +| R_e | L_f | 0 | Zero | +| L_e | R_f | e+f | Rectangular Hankel | + +Here are explicit bases and completeness arguments. For R_e to R_f with e>=f, choose coefficients a_0,...,a_(e-f). Put `C_(i,j)=a_(j-i)` for `0<=i<=f`, `0<=j<=e`, with coefficients outside that range zero. Use the same rule for U on `0<=i=0`. + +The gcd of an all-zero list is zero. Define + +`chi(x,y,z)=x^ell1 y^ell2 z^(-ell1 A-ell2 B)`. + +**Theorem.** For every field K, + +`Delta(T) = {(x,y,z) in (K*)^3 : chi(x,y,z) in (K*)^d}`. (2) + +Here `(K*)^0={1}`. This convention recovers the exact equality for a single distinct block type. + +For necessity, apply chi to (1). Its value is `product_i u_i^c_i`, which is a d-th power when d>0 and is one when d=0. + +For sufficiency with d>0, let `w^d=chi(x,y,z)`. Choose integer Bezout coefficients b_i with `sum_i b_i c_i=d`, and set `u_i=w^b_i`. Remove the slice shifts and these u_i contributions from x,y, leaving X,Y with `X^ell1 Y^ell2=1`. For either base orientation, `a=(XY)^-1` supplies exactly the residual pair through `a^v0`. Multiply a into u_0. Equation (1) and the explicit block lifts now construct the requested stabilizer. When d=0, start with every u_i=1 and make the same kernel correction. No root is then needed. + +Over an arbitrary field, membership in the power subgroup includes the existence of w; a constructive witness can take w as input. The theorem does not assume an algorithm that extracts arbitrary roots in K. The bounded finite-field executable finds w by enumerating the at most q-1 nonzero elements. + +The kernel correction is elementary. For a right base, `X^(e0+1)Y^e0=1` gives `(XY)^(-e0)=X` and `(XY)^(e0+1)=Y`. For a left base, exchange X and Y. These formulas include e0=0. + +The primitive vector v0 can be completed to an integral basis. Hence d is also the gcd of all two-by-two minors of the type vectors. These minors are, up to sign, + +- Differences of two right indices. +- Differences of two left indices. +- Sums e+f+1 for a right index e and a left index f. + +This is a direct criterion using the full type list. It is independent of multiplicities. Multiplicities still affect A,B and therefore the actual character label; they cannot be dropped from the slice shift. + +## 6. Special-linear orbit labels and constructive correction + +Because m,n are positive, the determinant map from `GL_m(K) x GL_n(K) x GL_2(K)` onto `(K*)^3` is surjective, with kernel the product of the three special linear groups. Its orbits inside one GL orbit are therefore the cosets of Delta(T). + +The map chi is surjective onto K*: for a right base use `(x,y,z)=(u,u^-1,1)`, and for a left base exchange x,y. Equation (2) gives a complete label group + +`K*/(K*)^d`. + +Over F_q, the exact number of special-linear orbits is + +`gcd(q-1,d)`, with `gcd(q-1,0)=q-1`. + +For example, consecutive right indices give d=1 and one SL orbit. R_1 plus L_1 has d=3 and gives three SL orbits over F4. R_1 plus L_2 has d=4 and gives four over F5. Zero-index factors are included whenever both full factor dimensions are positive. In particular, a sum of R_0 and L_0 is a zero pencil with full determinant image, as d=1 requires. + +If a supplied GL map g has determinant triple in Delta(T), choose the stabilizer witness h with that same triple. Then `g h^-1` has determinant one in every factor and has the same action on T as g. This gives a literal SL correction when the model and map are supplied. It does not discover a canonical model or a GL map from an arbitrary tensor. Equal labels similarly give an SL transporter between two supplied presentations by composing their maps and the appropriate stabilizer witness. + +## 7. Verification boundary and use + +The exact verifier checks the Hom formulas against literal coefficient equations for every ordered pair of orientations and indices zero through three over F2, F3, F4 and F5. It then solves the full mixed stabilizer equations in twelve declared domains, enumerates every vector in each resulting linear solution space, and retains precisely invertible P,C. It uses neither the character formula nor the symmetric-power lift in that oracle. Cases marked with all_slice_actions cover every GL2 action. The other cases cover one representative for every nonzero slice determinant, with every GL2 action separately checked by literal constructed lifts. + +The finite evidence supports the all-field proof. It is not an exhaustive enumeration over all indices, dimensions or fields. The executable restricts indices to zero through five, combined multiplicities to one through three, fields to F2/F3/F4/F5, and both total factor dimensions to at most sixteen. The written proof has no such bounds. + +This closes the supplied purely singular determinant-character interface in the tensor atlas. Native realization, dirty-state ownership, movement, restoration, storage, precision and the complete recursive cost remain unknown. Regular blocks, arbitrary-tensor extraction and a paid multiplication consumer are outside the result. No new kappa, selected-frontier change, human acceptance or proof-kernel verification is claimed. + +New proof and checks: Ali Romman with substantial OpenAI Codex assistance. Credit apoursh PR5672; Nick Petalas PR5250; David Ganz's A030/A026/A029 atlas and the classical Kronecker and symmetric-power lineage. The source notice and action conventions remain unchanged. diff --git a/research/finite-field-pencil-characters/source/oracle.py b/research/finite-field-pencil-characters/source/oracle.py new file mode 100644 index 0000000000..6535d1363e --- /dev/null +++ b/research/finite-field-pencil-characters/source/oracle.py @@ -0,0 +1,71 @@ +"""Literal linear-equation oracle for mixed pencil stabilizers. + +No character formula, Hom recurrence or symmetric-power lift is used here. +The supplied field operations are shared exact arithmetic. +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +from itertools import product + + +def nullspace(rows,columns,field): + a=[row[:]for row in rows];pivots=[];at=0 + for col in range(columns): + pivot=next((i for i in range(at,len(a))if a[i][col]),None) + if pivot is None:continue + a[at],a[pivot]=a[pivot],a[at];scale=field.inv(a[at][col]);a[at]=[field.mul(scale,x)for x in a[at]] + for i in range(len(a)): + if i!=at and a[i][col]: + scale=a[i][col];a[i]=[field.sub(x,field.mul(scale,y))for x,y in zip(a[i],a[at])] + pivots.append(col);at+=1 + out=[] + for free in sorted(set(range(columns))-set(pivots)): + v=[0]*columns;v[free]=1 + for i,p in enumerate(pivots):v[p]=field.neg(a[i][free]) + out.append(v) + return out + + +def equations(source,target,src_dims,dst_dims,field): + ms,ns=src_dims;md,nd=dst_dims;columns=md*ms+nd*ns;rows=[] + for a,b in zip(source,target): + for i in range(md): + for j in range(ns): + row=[0]*columns + for k in range(ms):row[i*ms+k]=a[k][j] + for k in range(nd):row[md*ms+k*ns+j]=field.neg(b[i][k]) + rows.append(row) + return rows,columns + + +def stabilizer_space(first,second,action,field): + m,n=len(first),len(first[0]);mixed=[] + for x,y in action:mixed.append([[field.add(field.mul(x,a),field.mul(y,b))for a,b in zip(row,other)]for row,other in zip(first,second)]) + rows,columns=equations(mixed,(first,second),(m,n),(m,n),field) + return nullspace(rows,columns,field) + + +def determinant(a,field): + """Row elimination for complete literal matrix domains.""" + rows=[row[:]for row in a];out=1 + for k in range(len(rows)): + pivot=next((i for i in range(k,len(rows))if rows[i][k]),None) + if pivot is None:return 0 + if pivot!=k:rows[k],rows[pivot]=rows[pivot],rows[k];out=field.neg(out) + diagonal=rows[k][k];out=field.mul(out,diagonal);inv=field.inv(diagonal) + for i in range(k+1,len(rows)): + factor=field.mul(rows[i][k],inv) + for j in range(k,len(rows)):rows[i][j]=field.sub(rows[i][j],field.mul(factor,rows[k][j])) + return out + + +def enumerate_space(basis,m,n,field,limit=60000): + if field.q**len(basis)>limit:raise ValueError('explicit oracle domain exceeds enumeration limit') + columns=m*m+n*n;image=set();invertible=0 + for coefficients in product(range(field.q),repeat=len(basis)): + v=[0]*columns + for a,row in zip(coefficients,basis): + if a:v=[field.add(x,field.mul(a,y))for x,y in zip(v,row)] + p=[v[i*m:(i+1)*m]for i in range(m)];offset=m*m;c=[v[offset+i*n:offset+(i+1)*n]for i in range(n)] + x,z=determinant(p,field),determinant(c,field) + if x and z:image.add((x,field.inv(z)));invertible+=1 + return image,invertible diff --git a/research/finite-field-pencil-characters/source/pencil.py b/research/finite-field-pencil-characters/source/pencil.py new file mode 100644 index 0000000000..6bc7fc076e --- /dev/null +++ b/research/finite-field-pencil-characters/source/pencil.py @@ -0,0 +1,195 @@ +"""Bounded exact witnesses for the written Kronecker determinant theorem. + +The implementation is deliberately limited to small fixtures; PROOF.md supplies +the arbitrary-field/dimension argument. apoursh with OpenAI Codex; Apache-2.0. +""" +from itertools import product + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +class Field: + """F2, F3, F5, or F4=F2[w]/(w^2+w+1), encoded 0,1,w,w+1.""" + def __init__(self, order): + require(type(order) is int and order in (2, 3, 4, 5), 'unsupported field') + self.q = order + self.p = 2 if order == 4 else order + + def add(self, a, b): + return a ^ b if self.q == 4 else (a + b) % self.q + + def neg(self, a): + return a if self.q == 4 else -a % self.q + + def sub(self, a, b): + return self.add(a, self.neg(b)) + + def mul(self, a, b): + if self.q != 4: + return a * b % self.q + value = 0 + for bit in range(2): + if (b >> bit) & 1: + value ^= a << bit + return value ^ 7 if value & 4 else value + + def power(self, a, exponent): + if exponent < 0: + require(a != 0, 'inverse of zero') + exponent %= self.q - 1 + value = 1 + for _ in range(exponent): + value = self.mul(value, a) + return value + + def inv(self, a): + require(a != 0, 'inverse of zero') + return self.power(a, self.q - 2) + + +def identity(n): + return [[int(i == j) for j in range(n)] for i in range(n)] + + +def transpose(a): + return [list(row) for row in zip(*a)] + + +def multiply(a, b, field): + require(len(a[0]) == len(b), 'matrix dimension mismatch') + result = [[0] * len(b[0]) for _ in a] + for i, row in enumerate(a): + for k, value in enumerate(row): + if value: + for j, other in enumerate(b[k]): + result[i][j] = field.add(result[i][j], field.mul(value, other)) + return result + + +def mix(a, b, x, y, field): + return [[field.add(field.mul(x, u), field.mul(y, v)) + for u, v in zip(row, other)] for row, other in zip(a, b)] + + +def determinant(a, field): + rows = [row[:] for row in a] + result = 1 + for col in range(len(rows)): + pivot = next((i for i in range(col, len(rows)) if rows[i][col]), None) + if pivot is None: + return 0 + if pivot != col: + rows[col], rows[pivot] = rows[pivot], rows[col] + result = field.neg(result) + result = field.mul(result, rows[col][col]) + inv = field.inv(rows[col][col]) + for i in range(col + 1, len(rows)): + scale = field.mul(rows[i][col], inv) + rows[i] = [field.sub(x, field.mul(scale, y)) + for x, y in zip(rows[i], rows[col])] + return result + + +def inverse(a, field): + n = len(a) + rows = [row[:] + unit for row, unit in zip(a, identity(n))] + for col in range(n): + pivot = next((i for i in range(col, n) if rows[i][col]), None) + require(pivot is not None, 'singular matrix') + rows[col], rows[pivot] = rows[pivot], rows[col] + inv = field.inv(rows[col][col]) + rows[col] = [field.mul(inv, value) for value in rows[col]] + for i in range(n): + if i != col: + scale = rows[i][col] + rows[i] = [field.sub(x, field.mul(scale, y)) + for x, y in zip(rows[i], rows[col])] + return [row[n:] for row in rows] + + +def tensor(a, b, field): + return [[field.mul(x, y) for x in row for y in other] + for row in a for other in b] + + +def slices(e, r): + require(type(e) is int and type(r) is int and 1 <= e <= 5 and 1 <= r <= 3, + 'outside bounded positive-index fixture domain') + return ([[int(j == i) for j in range((e + 1) * r)] for i in range(e * r)], + [[int(j == i + r) for j in range((e + 1) * r)] for i in range(e * r)]) + + +def symmetric_power(k, action, field): + """Ordinary monomial substitution, using convolution without factorials.""" + require(type(k) is int and 0 <= k <= 5, 'unsupported degree') + columns = [] + for i in range(k + 1): + coefficients = [1] + for linear in [action[0]] * (k - i) + [action[1]] * i: + result = [0] * (len(coefficients) + 1) + for j, value in enumerate(coefficients): + result[j] = field.add(result[j], field.mul(value, linear[0])) + result[j + 1] = field.add(result[j + 1], field.mul(value, linear[1])) + coefficients = result + columns.append(coefficients) + return transpose(columns) + + +def general_linear_two(field): + for entries in product(range(field.q), repeat=4): + action = [list(entries[:2]), list(entries[2:])] + if determinant(action, field): + yield action + + +def lift(e, r, action, multiplicity, field): + slices(e, r) + require(len(action) == 2 and all(len(row) == 2 for row in action), + 'slice action dimension mismatch') + require(len(multiplicity) == r and all(len(row) == r for row in multiplicity), + 'multiplicity dimension mismatch') + require(all(type(x) is int and 0 <= x < field.q + for matrix in (action, multiplicity) for row in matrix for x in row), + 'matrix entry outside field') + require(determinant(action, field) != 0, 'singular slice action') + require(determinant(multiplicity, field) != 0, 'singular multiplicity action') + p = tensor(transpose(symmetric_power(e - 1, action, field)), multiplicity, field) + q = tensor(inverse(symmetric_power(e, action, field), field), + transpose(inverse(multiplicity, field)), field) + return p, q, action + + +def fixes(first, second, witness, field): + p, q, action = witness + for row, target in zip(action, (first, second)): + mixed = mix(first, second, *row, field) + if multiply(multiply(p, mixed, field), transpose(q), field) != target: + return False + return True + + +def character(e, r, triple, field, left=False): + x, y, z = triple + if left: + x, y = y, x + return field.mul(field.mul(field.power(x, e + 1), field.power(y, e)), + field.power(z, r * e * (e + 1) // 2)) + + +def witness_for_triple(e, r, triple, field, left=False): + slices(e, r) + require(len(triple) == 3, 'determinant triple dimension mismatch') + require(all(type(x) is int and 0 < x < field.q for x in triple), + 'determinants must be nonzero field elements') + require(character(e, r, triple, field, left) == 1, 'character excludes triple') + x, y, z = triple + if left: + x, y = y, x + u = field.mul(field.inv(field.mul(x, y)), field.power(z, -r * e)) + d = identity(r) + d[0][0] = u + p, q, action = lift(e, r, [[z, 0], [0, 1]], d, field) + return (q, p, action) if left else (p, q, action) diff --git a/research/finite-field-pencil-characters/verify.py b/research/finite-field-pencil-characters/verify.py new file mode 100644 index 0000000000..f7b132ba02 --- /dev/null +++ b/research/finite-field-pencil-characters/verify.py @@ -0,0 +1,222 @@ +"""Check the declared finite domains and compare the saved receipt. + +Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +""" +from itertools import product +from pathlib import Path +from math import gcd +import importlib.util +import json +import sys + +ROOT = Path(__file__).resolve().parent +sys.path.insert(0, str(ROOT)) +import pencils as P +spec = importlib.util.spec_from_file_location('literal_equations', ROOT/'source/oracle.py') +O = importlib.util.module_from_spec(spec); spec.loader.exec_module(O) + + +def full_line(q, length=1): + return [['F', [a, 1], length, 1] for a in range(q)]+[['I', length, 1]] + + +DOMAINS = [ + ('binary_full_line', 2, full_line(2), True), + ('ternary_full_line', 3, full_line(3), True), + ('quartic_full_line', 4, full_line(4), False), + ('binary_thick_line', 2, full_line(2, 2), True), + ('ternary_thick_line', 3, full_line(3, 2), False), + ('ternary_jordan', 3, [['F', [0, 1], 2, 1]], True), + ('ternary_nonsplit', 3, [['F', [1, 0, 1], 1, 1]], True), + ('ternary_nonsplit_thick', 3, [['F', [1, 0, 1], 2, 1]], True), + ('binary_nonsplit_thick', 2, [['F', [1, 1, 1], 2, 1]], True), + ('binary_cubic', 2, [['F', [1, 1, 0, 1], 1, 1]], True), + ('finite_infinity_lengths', 3, [['F', [0, 1], 2, 1], ['I', 1, 1]], True), + ('mixed_right_jordan', 3, [['R', 1, 1], ['F', [0, 1], 2, 1]], True), + ('mixed_zero_jordan', 3, [['R', 0, 1], ['F', [0, 1], 2, 1]], True), + ('mixed_both_nonsplit', 2, [['R', 1, 1], ['L', 1, 1], ['F', [1, 1, 1], 1, 1]], True), + ('mixed_zero_both', 2, [['R', 0, 1], ['L', 0, 1], ['F', [0, 1], 1, 1]], True), + ('repeated_regular', 3, [['F', [0, 1], 1, 2]], True), +] +EXTRA = [ + ('quinary_full_line', 5, full_line(5)), + ('quinary_thick_line', 5, full_line(5, 2)), + ('quartic_third_order_line', 4, full_line(4, 3)), + ('regular_colours', 3, [['F', [0, 1], 1, 2], ['F', [1, 1], 1, 1], ['I', 1, 1]]), + ('two_points_odd', 5, [['F', [0, 1], 1, 1], ['I', 1, 1]]), + ('two_points_even', 5, [['F', [0, 1], 2, 1], ['I', 2, 1]]), + ('mixed_coprime_lengths', 5, [['R', 1, 1], ['L', 1, 1], ['F', [0, 1], 2, 1]]), + ('mixed_equal_index_gcd', 3, [['R', 1, 1], ['R', 3, 1], ['F', [0, 1], 2, 1]]), + ('mixed_left_nonsplit', 3, [['L', 2, 1], ['F', [1, 0, 1], 2, 1]]), + ('mixed_regular_lengths', 4, [['R', 0, 1], ['F', [0, 1], 3, 1], ['I', 2, 1]]), + ('pure_singular_control', 5, [['R', 1, 1], ['L', 2, 1]]), +] + + +def reference_fixed(model, f): + vectors = [] + for block in model: + if block[0] == 'R': vectors.append((block[1], -block[1]-1)) + elif block[0] == 'L': vectors.append((-block[1]-1, block[1])) + else: + length = block[-2]; vectors.append((length, -length)) + subgroup = {(1, 1)} + for a, b in vectors: + subgroup = {P.pair_mul(pair, (f.power(u, a), f.power(u, b)), f) + for pair in subgroup for u in range(1, f.q)} + return subgroup + + +def action_subset(f, complete): + if complete: return list(P.old.general_linear_two(f)) + out = [[[z, 0], [0, 1]] for z in range(1, f.q)] + for x in ([[0, 1], [1, 0]], [[1, 1], [0, 1]]): + if x not in out: out.append(x) + return out + + +def oracle_check(compiled, complete): + f = compiled['field']; a, b = compiled['slices']; m, n = compiled['dimensions'] + lifts = {tuple(sum(lift[2], [])): char for char, lift in compiled['lifts']} + image = set(); tested = accepted = 0; dimensions = [] + for action in action_subset(f, complete): + space = O.stabilizer_space(a, b, action, f) + pairs, count = O.enumerate_space(space, m, n, f) + tested += f.q**len(space); accepted += count; dimensions.append(len(space)) + char = lifts.get(tuple(sum(action, []))) + expected = set() if char is None else {P.pair_mul(char[:2], key, f) for key in compiled['fixed']} + P.need(pairs == expected, 'Separate full coefficient-space image for one slice action') + z = O.determinant(action, f); image.update(pair+(z,) for pair in pairs) + if complete: P.need(image == set(compiled['image']), 'Complete literal determinant image') + return dict(all_slice_actions=complete, slice_actions=len(dimensions), equation_dimensions=sorted(set(dimensions)), + linear_solutions=tested, invertible_stabilizers=accepted, determinant_triples_seen=len(image)) + + +def witnesses(compiled): + f = compiled['field']; yes = no = prescribed = 0; m, n = compiled['dimensions'] + for triple in product(range(1, f.q), repeat=3): + if triple in compiled['image']: + P.witness(compiled, triple); yes += 1 + maps = [P.old.identity(m), P.old.identity(n), P.old.identity(2)] + for matrix, value in zip(maps, triple): + matrix[0][0] = value + if len(matrix) > 1: matrix[0][1] = 1 + P.correct_map(compiled, maps) + else: + try: P.witness(compiled, triple) + except ValueError: no += 1 + else: raise ValueError('Excluded determinant triple accepted') + for char, lift in compiled['lifts']: + for pair in compiled['fixed']: + triple = P.pair_mul(char, pair+(1,), f) + P.witness(compiled, triple, lift[2]); prescribed += 1 + return dict(accepted_triples=yes, excluded_triples=no, supplied_map_SL_corrections=yes, + prescribed_slice_witnesses=prescribed, SL_orbits=len(set(P.orbit_labels(compiled).values()))) + + +def singular_pair(side, e): + m, n = e+(side == 'L'), e+(side == 'R') + a = [[0]*n for _ in range(m)]; b = [[0]*n for _ in range(m)] + for i in range(e): + a[i][i] = 1 + if side == 'R': b[i][i+1] = 1 + else: b[i+1][i] = 1 + return (a, b), (m, n) + + +def hom_checks(): + report = [] + for q in (2, 3, 4, 5): + f = P.Field(q); regular = [] + for length in (1, 2): + for block in (['F', [0, 1], length, 1], ['I', length, 1]): + parts, m, n = P.normalized([block], f) + regular.append((P.slices(parts, m, n, f), (m, n), block)) + count = 0; total = 0 + for reg, dims, block in regular: + for side in ('R', 'L'): + for e in range(4): + sing, sd = singular_pair(side, e) + for source, target, ds, dt, expected in ( + (reg, sing, dims, sd, dims[0] if side == 'R' else 0), + (sing, reg, sd, dims, dims[0] if side == 'L' else 0)): + rows, columns = O.equations(source, target, ds, dt, f) + dimension = len(O.nullspace(rows, columns, f)) + P.need(dimension == expected, 'Regular/singular Hom dimension') + count += 1; total += dimension + for a, da, ta in regular: + for b, db, tb in regular: + rows, columns = O.equations(a, b, da, db, f) + expected = min(ta[-2], tb[-2]) if ta[0] == tb[0] else 0 + P.need(len(O.nullspace(rows, columns, f)) == expected, 'Finite/infinity regular Hom dimension') + count += 1 + report.append(dict(field=q, ordered_Hom_cases=count, mixed_Hom_dimension_sum=total)) + return report + + +def controls(compiled): + f = P.Field(3); names = [] + jordan = compiled['ternary_jordan']; exact = set(jordan['image']) + P.need(exact == {(1, 1, 1), (2, 2, 2)}, 'The source Jordan sign example survives') + names += ['similarity_determinant', 'length_power_subgroup'] + for name, q in [('ternary_full_line', 3), ('quartic_full_line', 4)]: + c = compiled[name]; field = c['field']; a, b = c['slices'] + P.need(all(P.old.determinant(P.matrix_sum(a, b, x, y, field), field) == 0 + for x, y in product(range(q), repeat=2) if x or y), 'No invertible rational slice') + names.append('global_invertible_slice_is_unnecessary') + P.need(len(compiled['regular_colours']['lifts']) < 48, 'Coloured support restricts the slice group') + names.append('unrestricted_slice_group') + P.need(set(compiled['mixed_right_jordan']['fixed']) != set(product((1, 2), repeat=2)), 'Regular length still restricts a singular mixture') + names.append('mixed_length_gcd') + P.need(len(compiled['mixed_coprime_lengths']['image']) == 64, 'Coprime mixed vectors remove the row/column restriction') + names.append('mixed_coprime_characters') + for name in ('ternary_nonsplit', 'ternary_nonsplit_thick'): + P.need(set(compiled[name]['fixed']) == reference_fixed(compiled[name]['model'], f), 'Nonsplit norms use the block length') + names.append('residue_degree_is_not_block_length') + for name in ('ternary_jordan', 'mixed_right_jordan', 'ternary_full_line'): + c = compiled[name]; field = c['field']; maps = P.witness(c, next(iter(c['image']))) + bad = [x[:] for x in maps[0]]; bad[0][0] = field.add(bad[0][0], 1) + P.need(not P.old.fixes(*c['slices'], (bad, maps[1], maps[2]), field), 'Corrupt literal lift rejects') + names.append('literal_row_map_corruption') + for name in ('quinary_full_line', 'quinary_thick_line', 'quartic_third_order_line'): + c = compiled[name]; field = c['field']; length = c['model'][0][-2] + powers = {field.power(u, length) for u in range(1, field.q)} + predicted = {t for t in product(range(1, field.q), repeat=3) + if t[0] in powers and field.mul(field.mul(t[0], t[1]), field.power(t[2], length)) == 1} + P.need(set(c['image']) == predicted and len(set(P.orbit_labels(c).values())) == (field.q-1)*gcd(field.q-1, length), + 'Full projective line with nonsemisimple length character') + names.append('uniform_projective_line_length_character') + bad_models = [[], [['X', 1, 1]], [['R', -1, 1]], [['F', [0, 0, 1], 1, 1]], [['F', [0, 1], 0, 1]], + [['F', [0, 1], 1, 0]], [['R', 0, 1]], [['I', 1, 1], ['I', 1, 1]], [['F', [0, 3], 1, 1]]] + for model in bad_models: + try: P.compile_model(model, f) + except ValueError: pass + else: raise ValueError('Malformed model accepted') + return dict(mathematical_controls=names, malformed_models=len(bad_models)) + + +def run(): + hom = hom_checks(); reports = []; compiled = {} + for name, q, model in [(n, q, m) for n, q, m, _ in DOMAINS]+EXTRA: + c = P.compile_model(model, P.Field(q)); compiled[name] = c + P.need(set(c['fixed']) == reference_fixed(model, c['field']), 'Independent exponent-generated fixed image') + P.need(all(P.pair_mul(x, y, c['field']) in c['image'] for x in c['image'] for y in c['image']), 'Complete determinant image is closed') + item = dict(name=name, field=q, model=model, dimensions=c['dimensions'], + admissible_slice_actions=len(c['lifts']), total_slice_actions=c['slice_actions'], + fixed_image=sorted(c['fixed']), determinant_image=sorted(c['image']), **witnesses(c)) + entry = next((x for x in DOMAINS if x[0] == name), None) + if entry: item['literal_oracle'] = oracle_check(c, entry[3]) + reports.append(item); print('PASS_PENCIL_DOMAIN', name, flush=True) + return dict(status='PASS_COMPLETE_SUPPLIED_FINITE_FIELD_PENCIL_CHARACTERS', hom_domains=hom, + models=reports, controls=controls(compiled), + scope='All-dimension finite-field proof for supplied complete block models. Bounded literal evidence; no arbitrary extraction or physical caller.') + + +if __name__ == '__main__': + result = json.loads(json.dumps(run())) + if sys.argv[1:] == ['--write']: + (ROOT/'RESULT.json').write_text(json.dumps(result, indent=2, sort_keys=True)+'\n') + else: + P.need(not sys.argv[1:], 'No unknown verifier arguments') + P.need(result == json.loads((ROOT/'RESULT.json').read_text()), 'Saved exact receipt differs') + print(result['status'])