From 81c0577b83cdafa73346da8ade1261b0b202e45f Mon Sep 17 00:00:00 2001 From: apoursh <8867770+apoursh@users.noreply.github.com> Date: Mon, 26 Oct 2026 00:33:07 -0400 Subject: [PATCH] Determine singular Kronecker block determinant images --- research/kronecker-determinant-image/PROOF.md | 335 ++++++++++++++++++ .../kronecker-determinant-image/README.md | 140 ++++++++ .../kronecker-determinant-image/SOURCES.json | 44 +++ .../kronecker-determinant-image/TASK.json | 120 +++++++ .../kronecker-determinant-image/VERIFY.json | 34 ++ .../kronecker-determinant-image/oracle.py | 175 +++++++++ .../kronecker-determinant-image/pencil.py | 195 ++++++++++ .../kronecker-determinant-image/verify.py | 189 ++++++++++ 8 files changed, 1232 insertions(+) create mode 100644 research/kronecker-determinant-image/PROOF.md create mode 100644 research/kronecker-determinant-image/README.md create mode 100644 research/kronecker-determinant-image/SOURCES.json create mode 100644 research/kronecker-determinant-image/TASK.json create mode 100644 research/kronecker-determinant-image/VERIFY.json create mode 100644 research/kronecker-determinant-image/oracle.py create mode 100644 research/kronecker-determinant-image/pencil.py create mode 100644 research/kronecker-determinant-image/verify.py diff --git a/research/kronecker-determinant-image/PROOF.md b/research/kronecker-determinant-image/PROOF.md new file mode 100644 index 0000000000..77ff305e1c --- /dev/null +++ b/research/kronecker-determinant-image/PROOF.md @@ -0,0 +1,335 @@ +# Determinant image of an isotypic singular Kronecker pencil + +This note gives a self-contained proof for one positive right minimal index +with arbitrary positive multiplicity, and obtains the left-block case by +transposition. It addresses the corresponding open question in Nick Petalas's +[pencil-determinant-image package at its pinned head](https://github.com/CrocSwap/integer-mult-bounds/blob/43142bedc7cb5c0f1f73ff3fea6d9bfd237949ee/research/pencil-determinant-image/README.md). +The block and symmetric-power constructions are classical; no literature +novelty is claimed. The addition here is the explicit determinant-image formula, +its action conventions, and its bounded verification package. This is a scoped +proof, not a new multiplication bound or a classification of arbitrary pencils. + +## 1. Pencil and action conventions + +Let K be any field, and let e,r be positive integers. Define + +``` +A_0 = [I_e | 0], A_1 = [0 | I_e], +L_e(s,t) = s A_0 + t A_1. +``` + +Thus L_e is e by e+1, with s on its main diagonal and t immediately above +that diagonal. Set + +``` +T_0 = A_0 tensor I_r, T_1 = A_1 tensor I_r, +T(s,t) = L_e(s,t) tensor I_r. +``` + +The row dimension is er and the column dimension is (e+1)r. The tensor-product +ordering groups each monomial index into an r-dimensional block. A simultaneous +permutation of rows and columns identifies this pencil with the direct sum of +r identical L_e blocks. + +For P in GL_(er)(K), Q in GL_((e+1)r)(K), and + +``` +R = [[a,b], [c,d]] in GL_2(K), +``` + +use exactly the action + +``` +(T_0,T_1) -> (P(a T_0 + b T_1)Q^T, P(c T_0 + d T_1)Q^T). +``` + +In particular the right factor in the action is Q^T, not Q^(-1). If +z=(s,t)^T, the mixed pencil is T(R^T z), because + +``` +s(a T_0+b T_1) + t(c T_0+d T_1) + = (as+ct)T_0 + (bs+dt)T_1. +``` + +Let Stab(T) be the stabilizer under this action, and let + +``` +Delta(T) = { (det P, det Q, det R) : (P,Q,R) in Stab(T) }. +``` + +All equalities of pencils below are polynomial equalities in independent +indeterminates s,t. No interpolation over the points of K is used. + +## 2. The exact image + +**Theorem.** For every field K and all e,r >= 1, + +``` +Delta(L_e tensor I_r) + = { (u^e z^[r e(e-1)/2], + u^[-(e+1)] z^[-r e(e+1)/2], + z) : u,z in K^* } + = { (x,y,z) in (K^*)^3 : + x^(e+1) y^e z^[r e(e+1)/2] = 1 }. +``` + +The half-products in these exponents are integers. They do not denote division +inside K, so the statement includes characteristic two. + +For the transposed block the result is + +``` +Delta(L_e^T tensor I_r) + = { (x,y,z) in (K^*)^3 : + x^e y^(e+1) z^[r e(e+1)/2] = 1 }. +``` + +The proof also constructs a stabilizer element for every triple in the stated +image, with any prescribed R having determinant z. + +## 3. A characteristic-safe lift of every slice transformation + +For k >= 0 let V_k be the homogeneous degree-k polynomials in X,Y, with ordered +basis + +``` +X^k, X^(k-1)Y, ..., Y^k. +``` + +Let S_k(R) be the matrix of polynomial substitution + +``` +f(X,Y) -> f(aX+bY,cX+dY) +``` + +on coefficient columns in this basis. Equivalently, column i, with +0 <= i <= k, consists of the coefficients of + +``` +(aX+bY)^(k-i) (cX+dY)^i. +``` + +In particular S_0(R)=[1] and S_1(R)=R^T. This convention matters for the +transposes in the lift. Substitution by R^(-1) is inverse to substitution by R, +so S_k(R) is invertible in every characteristic. + +Use ordinary monomials and binomial coefficients reduced in K. There are no +normalized monomials, divided factorials, or assumptions that k! is invertible. +The substitution identities remain valid when some binomial coefficients +vanish in K. + +The determinant is + +``` +det S_k(R) = (det R)^[k(k+1)/2]. (1) +``` + +For completeness, this follows on generators of GL_2(K). For a diagonal +R=diag(alpha,beta), S_k is diagonal with entries alpha^(k-i) beta^i, +whose product is (alpha beta)^[k(k+1)/2]. Upper and lower unitriangular +matrices act triangularly with all diagonal entries one. For the matrix +interchanging X,Y, S_k reverses k+1 basis vectors, with determinant +(-1)^[k(k+1)/2]. These matrices generate GL_2(K) by row elimination. +With the stated coefficient-column convention, composition satisfies +S_k(R)S_k(U)=S_k(UR). Determinants are multiplicative in either order, +proving (1) for all R. This proof also works in characteristic two. + +Let B_e(s,t)=L_e(s,t)^T. It is the coefficient matrix of multiplication by +sX+tY from V_(e-1) to V_e. Substituting the two linear forms into this product +gives + +``` +S_e(R) B_e(s,t) = B_e(as+ct,bs+dt) S_(e-1)(R). +``` + +Transposing and rearranging proves + +``` +L_e(as+ct,bs+dt) + = S_(e-1)(R)^(-T) L_e(s,t) S_e(R)^T. (2) +``` + +Consequently a stabilizer lift of every R is + +``` +P_R = S_(e-1)(R)^T tensor I_r, +Q_R = S_e(R)^(-1) tensor I_r. (3) +``` + +Indeed (2) says P_R T(R^T z) Q_R^T = T(z). There is no residual sign and +no restriction on R beyond invertibility. + +## 4. The complete fixed-slice stabilizer + +Suppose R=I_2 and (P,Q,I_2) fixes T. Put C=Q^(-T). The two equations are + +``` +P T_0 = T_0 C, P T_1 = T_1 C. (4) +``` + +Write P as an e by e block matrix and C as an e+1 by e+1 block matrix, +with every block of size r by r. Use indices starting at zero. The first +equation of (4) says that the first e block rows of C equal [P | 0]. The +second says that the last e block rows of C equal [0 | P]. In their overlap, +for 1 <= i <= e-1, one obtains + +``` +P_(i,0) = 0, +P_(i,j) = P_(i-1,j-1) for 1 <= j <= e-1, +P_(i-1,e-1) = 0. (5) +``` + +The recurrence makes each block diagonal constant. The first boundary +condition kills every diagonal below the main diagonal; the last kills every +diagonal above it. Thus + +``` +P = I_e tensor D, C = I_(e+1) tensor D +``` + +for one r by r matrix D. When e=1 there is no overlapping block row, +but the two equations directly give C=diag(P,P), which is the same conclusion. +Invertibility of P forces D to be invertible. Conversely every invertible D +satisfies (4). Therefore the fixed-slice stabilizer is exactly + +``` +(P,Q) = (I_e tensor D, I_(e+1) tensor D^(-T)), + D in GL_r(K). (6) +``` + +In particular arbitrary mixing between the r equal blocks is already included; +it contributes one full GL_r(K), not just r independent scalar factors. + +## 5. All stabilizers and their determinants + +Fix R. Both a given stabilizer (P,Q,R) and the lift (P_R,Q_R,R) send +T(R^T z) to T(z). Their quotient on the row and column factors therefore +fixes the unmixed pencil T(z). Equation (6) applies. Since the factors acting +on the monomial index commute with those acting on the multiplicity index, +every stabilizer with slice factor R is uniquely of the form + +``` +P = S_(e-1)(R)^T tensor D, +Q = S_e(R)^(-1) tensor D^(-T), D in GL_r(K). (7) +``` + +More explicitly, putting H=P P_R^(-1) and J=Q Q_R^(-1) gives +H T(z) J^T=T(z), so (6) gives H=I_e tensor D and +J=I_(e+1) tensor D^(-T). This proves necessity as well as sufficiency of (7). + +Let u=det D and z=det R. Applying (1) and +det(A tensor B)=(det A)^(dim B)(det B)^(dim A) to (7) gives + +``` +det P = u^e z^[r e(e-1)/2], +det Q = u^[-(e+1)] z^[-r e(e+1)/2]. (8) +``` + +The determinant maps GL_r(K)->K^* and GL_2(K)->K^* are surjective, +as witnessed by diagonal matrices. Hence every u,z in K^* occurs, proving +the parametrized form of the theorem. Eliminating u from (8) gives + +``` +(det P)^(e+1) (det Q)^e (det R)^[r e(e+1)/2] = 1. +``` + +## 6. Constructive converse without root extraction + +Suppose x,y,z are nonzero and satisfy + +``` +x^(e+1) y^e z^[r e(e+1)/2] = 1. (9) +``` + +Define + +``` +u = (xy)^(-1) z^(-re). (10) +``` + +There is no need to take an e-th root or an (e+1)-st root. To check (10), +put A=r e(e-1)/2 and B=r e(e+1)/2. Then A+B=re^2 and +2B=re(e+1). Equation (9) gives + +``` +u^e z^A + = x^(-e) y^(-e) z^(-re^2+A) + = x z^(B-re^2+A) = x, + +u^[-(e+1)] z^(-B) + = x^(e+1) y^(e+1) z^[re(e+1)-B] + = y z^[re(e+1)-2B] = y. +``` + +Take D=diag(u,1,...,1), and take any R with determinant z, for example +diag(z,1). Equations (7) then give an explicit stabilizer with determinant +triple (x,y,z). This proves that (9) is the only constraint, over any field. +Conversely (8) implies xy=u^(-1)z^(-re), so (10) also proves uniqueness +of u for a given image triple. + +## 7. Transposition and the finite-field orbit count + +Transposing the two slice equations exchanges P and Q and leaves R unchanged. +Thus (P,Q,R) stabilizes (T_0,T_1) if and only if (Q,P,R) stabilizes +(T_0^T,T_1^T). The determinant image for the left block is exactly the right +block's image with its first two coordinates exchanged. This proves the +transposed formula in Section 2. + +For K=F_q, the parametrization (8) is injective in (u,z), by (10), so + +``` +|Delta(T)| = (q-1)^2. +``` + +Let G=GL_(er)(F_q) x GL_((e+1)r)(F_q) x GL_2(F_q) and let N be the +product of its three special linear subgroups. The determinant map identifies +G/N with (F_q^*)^3. Because N is normal, the N-orbits within the single +G-orbit of T are indexed by + +``` +(F_q^*)^3 / Delta(T). +``` + +The character + +``` +chi(x,y,z) = x^(e+1) y^e z^[r e(e+1)/2] +``` + +has kernel Delta(T) and is surjective: chi(w,w^(-1),1)=w. +Consequently there are exactly q-1 such special-linear orbits. For the left +block exchange x and y in this character. This is an orbit statement about +the displayed isotypic pencil only. + +## 8. Boundaries of the result and checks that can falsify mistakes + +The theorem covers e>=1 and r>=1 only. The degree-zero right and left blocks +have shapes 0 by 1 and 1 by 0, respectively. They represent unused columns +or rows and require separate treatment of zero-dimensional factors; the lift +above would also call for the undefined V_(-1). Adjoining such blocks to a +positive-index pencil introduces extra fixed-slice maps that are outside the +recurrence proved here. This exclusion is a scope boundary, not a claim that +the displayed equation has been disproved under some extension of conventions. + +Different positive minimal indices, mixtures of right and left blocks, and +regular/singular coupling are also outside this theorem. Their off-diagonal +homomorphisms have not been classified here. No result is claimed for the +separate regular-pencil question with no invertible rational slice. + +Useful discriminating finite checks include: + +- For e=1,r=1, the lift reads P=[u] and Q=u^(-1)R^(-T). The equation is + x^2 y z=1, which checks the sign and the inverse transpose on the right. +- For e=2,r=1 over F_3, the image equation is x=z with y unrestricted. + Dropping the slice determinant exponent would instead require x=1. +- For e=1,r=2 over F_3, the equation is y=1 with x,z unrestricted, + whereas e=1,r=1 gives y=z. This detects an omitted multiplicity factor. +- In characteristic two, e at least two exercises vanishing binomial + coefficients in S_e. F_4 provides nontrivial determinant characters; + testing only F_2 cannot distinguish determinant exponents. +- Directly solve the stabilizer slice equations in small dimensions instead + of checking only matrices generated by (7). Such a check can falsify the + completeness assertion in Sections 4 and 5. + +Finite checks support the implementation and expose convention errors. They +do not replace the arbitrary-field proof above or settle any excluded case. diff --git a/research/kronecker-determinant-image/README.md b/research/kronecker-determinant-image/README.md new file mode 100644 index 0000000000..eed3f5378d --- /dev/null +++ b/research/kronecker-determinant-image/README.md @@ -0,0 +1,140 @@ +# Determinant images for repeated singular Kronecker blocks + +**Scoped written proof with exact finite corroboration; no new kappa.** +This answers the single-minimal-index/multiplicity next question in Nick +Petalas's [PR #5250](https://github.com/CrocSwap/integer-mult-bounds/pull/5250). +It complements that package's regular square pencils with an invertible slice. +It does not classify mixed pencils or recover a decomposition from arbitrary +input tensors. + +For any field K and positive integers e,r, let L_e(s,t) be the e by e+1 pencil +with s on the diagonal and t on the superdiagonal, repeated as L_e tensor I_r. +Use the action `(P,Q,R)` on slices `(A,B)` given by + +``` +(P(aA+bB)Q^T, P(cA+dB)Q^T), R=[[a,b],[c,d]]. +``` + +The exact stabilizer determinant image is + +``` +Delta = {(x,y,z) in (K*)^3 : x^(e+1) y^e z^[r e(e+1)/2] = 1}. +``` + +For the transposed pencil exchange x and y. [PROOF.md](PROOF.md) proves +necessity and sufficiency, explicitly lifts every GL2 slice action in every +characteristic, and constructs a witness for every allowed triple without root +extraction. The half-product is an integer exponent, including characteristic +two. Over F_q the image has size (q-1)^2 and the GL orbit splits into exactly +q-1 orbits under the product of the three special linear groups. + +## Why this scope and what it adds + +PR #5250, exact head `43142bedc7cb5c0f1f73ff3fea6d9bfd237949ee`, explicitly +leaves singular blocks and their multiplicity spaces open. Its README at this +package's base has the identical Git blob. The new step is the complete +one-type determinant image, its explicit slice-action lifts and constructive +converse. Classical Kronecker blocks and symmetric powers are not claimed as +new mathematics; global literature priority is unclaimed. + +This takes that concrete handoff before a random assignment. The original +`formal-interface-lemma` card is retained verbatim in [TASK.json](TASK.json) +with **changed scope**: a written mathematical side result, not a Lean +formalization or a selected-supplier implication. Canonical main was pulled at +`df0137efd35e11b4445734bf612bdd4c7ebc330c`, priority revision 7; selected kappa +remains 0.00310045. The schema-aware source-binding baseline passed; its +metadata check is not a cold scientific replay. Coordination and the five-point +family comparison are in TASK.json and [Discussion #5670](https://github.com/CrocSwap/integer-mult-bounds/discussions/5670). + +## Reproducible evidence + +Use CPython 3.12 and its standard library from the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/kronecker-determinant-image +python3.12 -B scripts/check_research_commit.py --package research/kronecker-determinant-image --check-source-history +``` + +The registered commands run both ordinary and optimized Python with warnings +as errors. Direct replay also works without Git or repository files: + +```sh +python3.12 -I -W error -B research/kronecker-determinant-image/verify.py +python3.12 -I -O -W error -B research/kronecker-determinant-image/verify.py +``` + +The success marker is `PASS_KRONECKER_DETERMINANT_IMAGE`. The preceding `RESULT` +JSON gives all tested domains, determinant images and counts; `PACKAGE_SHA256` +binds the local package files. The program writes no files. Each registered +command has a 120-second limit. [SOURCES.json](SOURCES.json) pins historical +provenance only: no predecessor executable or external scientific input is +imported, and no live input is omitted from VERIFY.json. + +- **Completeness discriminator:** [oracle.py](oracle.py) independently enumerates + every P and R and solves both literal equations for the unique Q transpose. + Eight fixed (e,r,q) domains are (1,1,2/3/5), (2,1,2/3), (1,2,2/3) and + (3,1,2): 7,710 candidate pairs and 4,470 stabilizers. Its determinant images + agree exactly with the character kernel. It uses no symmetric powers or + predicted-image formula. +- **Constructive checks:** [pencil.py](pencil.py) uses polynomial convolution, + without factorial division, over F2, F3, F4 and F5. Thirteen explicit domains + in `verify.py:LIFT_DOMAINS` cover indices through five and multiplicities + through three. Every GL2 action and every nonzero multiplicity determinant + is tested in those domains, including nonscalar repeated-block mixing: + 4,932 right-block lifts and 4,932 transposed lifts. +- **Converse:** all 454 nonzero determinant triples across both orientations + in those domains are checked: 154 produce literal stabilizers with exactly + the requested determinants and 300 are excluded by the character. +- **Failure controls:** six mathematical mutants detect a missing slice + exponent, missing multiplicity, wrong orientation, two incorrect right-factor + conventions and binomial reduction modulo q instead of the characteristic. + Fourteen malformed/domain controls reject; 224 finite-field triples check + associativity and distributivity. These explicit checks survive `-O`. + +These are bounded checks, not exhaustive verification of every field or index. +F4 lift checks exercise characteristic two with nontrivial determinants; the +independent exhaustive stabilizer oracle is over prime fields only. Necessity +in general dimensions rests on the written block recurrence. Code limits are +e<=5, r<=3 and q in {2,3,4,5}; admitted bounds do not mean every combination was +tested. The oracle caps raw matrix enumeration at 625, retained group size at +480 and P,R pairs at 2,304 per fixture. No dependencies were added. Functions +are short, loops are bounded, and Python's managed allocation is used for these +small matrices; this is not an unbounded public tensor API. + +## Boundaries and credit + +Excluded: degree-zero unused rows/columns, unequal minimal indices, mixtures +of left and right blocks, regular/singular coupling, and regular pencils with +no invertible base-field rational slice. No arbitrary-tensor recognition or +uniform bit-complexity result is supplied. Native realization, dirty-state +ownership, routing, storage, precision, compiler cost and the full recursive +invoice remain **unknown**, not free. No physical supplier, selected-frontier +change, complete multiplication theorem, Lean build or selected cold replay is +claimed. Human and formal proof-kernel review remain unclaimed; parallel agent +checks are AI-assisted review. + +Nick Petalas retains credit for the restricted regular-pencil extraction and +this explicit handoff. David Ganz retains atlas A030/A026/A029 and its cited +tensor/stabilizer lineage. The classical Kronecker, symmetric-power and +centralizer/canonical-form results remain predecessor work; this package does +not reproduce or claim the regular-pencil algorithms of Arne Storjohann or +the determinant work of Ferrer, Mingueza and Montoro. Source pins and the atlas +attribution file are recorded in SOURCES.json. Prepared by **apoursh** with +substantial **OpenAI Codex** assistance, including parallel proof, overlap and +independent corroborator work. Apache-2.0. + +## Open next questions + +- **Mixed positive minimal indices and block types.** Classify the fixed-slice + homomorphisms of L_1 direct sum L_2, then determine how they affect determinant + characters before adding any regular block. This is needed to combine the + one-type result with PR5250; a mixed-block filtration and complete slice-action + analysis are missing here. +- **Regular pencils without an invertible rational slice.** Start with + diag(s,t,s+t) over F2 and its homogeneous elementary divisors. Its determinant + polynomial is nonzero but all base-field projective slices are singular. + A coordinate-independent replacement for B_R inverse and compatible descent + remain the separate blocker in PR5250. + +Structured relevance, first steps and blockers are also in TASK.json. Neither +question is reserved by this submission. diff --git a/research/kronecker-determinant-image/SOURCES.json b/research/kronecker-determinant-image/SOURCES.json new file mode 100644 index 0000000000..e2692032e4 --- /dev/null +++ b/research/kronecker-determinant-image/SOURCES.json @@ -0,0 +1,44 @@ +{ + "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/pencil-determinant-image/README.md", + "usage": "provenance", + "git_blob": "20f8262d3747f28e4535ec3f928f7481f8306749", + "sha256": "ba945687c23f6e675e2c320c7e5ccf345b17090e4d4283721ff950d62da5516e" + }, + { + "path": "research/pure-math-atlas-400/volumes/01-algebra.md", + "usage": "provenance", + "git_blob": "c3f1e94af804e35da07c3c8f61557e4b4d480c3d", + "sha256": "43aeda6c0de1cc8e64f0207fc98f2436f0e883d4d0f7183719d3e8c6e5bebfbf" + }, + { + "path": "research/pure-math-atlas-400/ATTRIBUTION.md", + "usage": "provenance", + "git_blob": "3e11aa228de6d6c7bf42b3cdc6344ed36986af33", + "sha256": "d53e93d56ae9ad488a95e71e190600b0547eed1b11e81f2bb401ff6d079a1830" + } + ], + "predecessor": { + "pr": 5250, + "head": "43142bedc7cb5c0f1f73ff3fea6d9bfd237949ee", + "readme_blob": "20f8262d3747f28e4535ec3f928f7481f8306749", + "status": "Merged archival package, central ledger partially reviewed. Not scientific acceptance.", + "credit": "Nick Petalas; David Ganz atlas A030/A026/A029 and retained classical lineage." + }, + "source_policy": "All rows are historical provenance; no external executable or live scientific input is imported. Direct replay requires only this package. The predecessor README at the base has the identical blob to its exact source head." +} diff --git a/research/kronecker-determinant-image/TASK.json b/research/kronecker-determinant-image/TASK.json new file mode 100644 index 0000000000..f473b83d4c --- /dev/null +++ b/research/kronecker-determinant-image/TASK.json @@ -0,0 +1,120 @@ +{ + "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": "Written determinant-image theorem for L_e tensor I_r, e,r >= 1, and its transpose; exact bounded independent corroboration.", + "scope_change_reason": "Take the explicit singular-pencil handoff in PR5250 rather than the original Lean formalization card; no selected-supplier or full multiplication implication.", + "bottleneck_link": "Mathematical side result: closes the homogeneous singular block character gap in atlas A030. No paid physical realization or kappa claim.", + "budget_minutes": 60, + "stop_rule": "Stop at one minimal-index block type with multiplicity and transpose, or publish a counterexample/precise obstruction; exclude mixed block types and physical compilation.", + "outcome": "completed", + "evidence": "PROOF.md and registered bounded replay: independent literal stabilizer oracle, characteristic-safe lifts, constructive converse and controls. Publication-byte/export checks recorded in the PR after final commit.", + "author": "apoursh", + "ai_assistance": "Substantial OpenAI Codex assistance, including parallel mathematical derivation, overlap triage and independent corroborator work.", + "open_questions": [ + { + "question": "Determine the determinant image for mixed positive minimal indices, both orientations and regular/singular couplings.", + "why_it_matters": "This is the remaining singular-pencil obstruction to combining the one-type theorem with PR5250.", + "first_step": "Classify fixed-slice homomorphisms for L_1 direct sum L_2 and track their determinant factors before introducing any regular block.", + "blocked_by": "No mixed-block endomorphism filtration or complete slice-action analysis in this package." + }, + { + "question": "Extend regular-square-pencil assembly when every base-field rational slice is singular.", + "why_it_matters": "The separate rational-slice restriction of PR5250 remains.", + "first_step": "Study diag(s,t,s+t) over F2 via homogeneous elementary divisors and an extension-field invertible slice.", + "blocked_by": "A coordinate-independent replacement for B_R inverse and a descent-compatible determinant assembly." + } + ], + "coordination": { + "upstream_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c", + "checked_at_utc": "2026-10-26T04:25:24Z", + "predecessor_pr": 5250, + "predecessor_head": "43142bedc7cb5c0f1f73ff3fea6d9bfd237949ee", + "live_coverage": "Newest handoffs, active Discussions and Kronecker discussion search; all-state narrow PR searches. No competing successor found; not exhaustive novelty evidence.", + "local_overlap_limit": "Sparse offline helper searched only 3 working notes; live targeted searches supplement this incomplete inventory.", + "canonical_discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5670", + "hub_claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19188415", + "submission_refresh_utc": "2026-10-26T04:32:44Z", + "submission_refresh": "Canonical main unchanged at df0137e; two fresh all-state PR searches still return only predecessor #5250. No new conflicting scope found." + }, + "family_expansion_gate": { + "exact_evidence": "PR5250 explicit singular next question at head 43142bedc7cb5c0f1f73ff3fea6d9bfd237949ee; merged archive is not theorem acceptance.", + "boundary": "Single positive minimal-index type L_e tensor I_r and transpose; written character theorem, no recognition of arbitrary tensors.", + "cost_ledger": "Native realization, routing, dirty-state/storage, precision, compiler and full recursive invoice UNKNOWN; no supplier or kappa admission.", + "decision": "Replace the singular homogeneous-block unknown with an exact character and constructive witnesses.", + "alternative_and_stop": "Further PR5668 nonsplit expansion lacks a named physical consumer. Resolve this explicit one-type handoff; stop before mixed types or physical compilation." + } +} diff --git a/research/kronecker-determinant-image/VERIFY.json b/research/kronecker-determinant-image/VERIFY.json new file mode 100644 index 0000000000..baf4dd961e --- /dev/null +++ b/research/kronecker-determinant-image/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": 120, + "checks": "Independent exhaustive P,R enumeration with unique Q solve; all prescribed slice lifts and transpose equations over F2/F3/F4/F5; constructive determinant converse; mutation and malformed-domain controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Independent exhaustive P,R enumeration with unique Q solve; all prescribed slice lifts and transpose equations over F2/F3/F4/F5; constructive determinant converse; mutation and malformed-domain controls." + } + ] +} diff --git a/research/kronecker-determinant-image/oracle.py b/research/kronecker-determinant-image/oracle.py new file mode 100644 index 0000000000..eb8e16712b --- /dev/null +++ b/research/kronecker-determinant-image/oracle.py @@ -0,0 +1,175 @@ +#!/usr/bin/env python3 +"""Independent literal stabilizer enumeration on eight bounded prime-field cases. + +No determinant-image formula or symmetric-power construction is used. For each +P and R, Gaussian elimination solves both stabilizer equations for Q transpose. +The right Kronecker block convention is A=[I_e 0], B=[0 I_e], tensored with I_r. +New material: apoursh, with substantial OpenAI Codex assistance; Apache-2.0. +""" + +from itertools import product + + +DOMAINS = ( + (1, 1, 2), (1, 1, 3), (1, 1, 5), + (2, 1, 2), (2, 1, 3), + (1, 2, 2), (1, 2, 3), (3, 1, 2), +) +MAX_MATRIX_CANDIDATES = 625 +MAX_GROUP_SIZE = 480 +MAX_PR_PAIRS = 2304 + + +def _determinant(matrix, prime): + """Determinant by row elimination, including permutation signs.""" + rows = [list(row) for row in matrix] + size = len(rows) + value = 1 + for col in range(size): + pivot = next((i for i in range(col, size) if rows[i][col]), None) + if pivot is None: + return 0 + if pivot != col: + rows[col], rows[pivot] = rows[pivot], rows[col] + value = -value + diagonal = rows[col][col] + value = value * diagonal % prime + inverse = pow(diagonal, -1, prime) + for i in range(col + 1, size): + scale = rows[i][col] * inverse % prime + for j in range(col, size): + rows[i][j] = (rows[i][j] - scale * rows[col][j]) % prime + return value % prime + + +def _general_linear(size, prime): + """Enumerate all matrices first; retain precisely nonzero determinants.""" + candidate_count = prime ** (size * size) + if candidate_count > MAX_MATRIX_CANDIDATES: + raise ValueError("matrix enumeration exceeds the fixed oracle cap") + group = [] + for entries in product(range(prime), repeat=size * size): + matrix = tuple(entries[i * size:(i + 1) * size] for i in range(size)) + determinant = _determinant(matrix, prime) + if determinant: + if len(group) >= MAX_GROUP_SIZE: + raise ValueError("group enumeration exceeds the fixed oracle cap") + group.append((matrix, determinant)) + return tuple(group) + + +def _multiply(left, right, prime): + return tuple( + tuple(sum(a * b for a, b in zip(row, col)) % prime + for col in zip(*right)) + for row in left + ) + + +def _mix(first, second, a, b, prime): + return tuple(tuple((a * x + b * y) % prime for x, y in zip(row, other)) + for row, other in zip(first, second)) + + +def _right_slices(index, multiplicity): + row_count = index * multiplicity + col_count = (index + 1) * multiplicity + first = tuple(tuple(int(j == i) for j in range(col_count)) + for i in range(row_count)) + second = tuple(tuple(int(j == i + multiplicity) for j in range(col_count)) + for i in range(row_count)) + return first, second + + +def _solve_unique(coefficients, targets, prime): + """Solve C X=D by full-column-rank elimination; reject inconsistency.""" + row_count = len(coefficients) + col_count = len(coefficients[0]) + target_count = len(targets[0]) + width = col_count + target_count + rows = [list(left + right) for left, right in zip(coefficients, targets)] + for col in range(col_count): + pivot = next((i for i in range(col, row_count) if rows[i][col]), None) + if pivot is None: + raise RuntimeError("right-pencil stack unexpectedly lacks full rank") + rows[col], rows[pivot] = rows[pivot], rows[col] + inverse = pow(rows[col][col], -1, prime) + rows[col] = [(entry * inverse) % prime for entry in rows[col]] + for i in range(row_count): + if i == col: + continue + scale = rows[i][col] + for j in range(width): + rows[i][j] = (rows[i][j] - scale * rows[col][j]) % prime + if any(any(row[col_count:]) for row in rows[col_count:]): + return None + return tuple(tuple(row[col_count:]) for row in rows[:col_count]) + + +def _candidate(first, second, left, action, prime): + """Return Q transpose if this P,R pair is a literal tensor stabilizer.""" + (a, b), (c, d) = action + mixed_first = _mix(first, second, a, b, prime) + mixed_second = _mix(first, second, c, d, prime) + top = _multiply(left, mixed_first, prime) + bottom = _multiply(left, mixed_second, prime) + right_transpose = _solve_unique(top + bottom, first + second, prime) + if right_transpose is None: + return None + if _determinant(right_transpose, prime) == 0: + return None + if (_multiply(_multiply(left, mixed_first, prime), right_transpose, prime) + != first): + raise RuntimeError("first literal stabilizer equation failed") + if (_multiply(_multiply(left, mixed_second, prime), right_transpose, prime) + != second): + raise RuntimeError("second literal stabilizer equation failed") + return right_transpose + + +def enumerate_image(index, multiplicity, prime): + """Return the exact determinant image and stabilizer count on a fixed case. + + Full-column-rank stacking makes Q unique for every pair P,R. Thus exhaustive + P,R enumeration with equation solving counts every stabilizer exactly once. + This function deliberately rejects every input outside DOMAINS. + """ + values = (index, multiplicity, prime) + if any(type(value) is not int for value in values) or values not in DOMAINS: + raise ValueError("unsupported oracle case; use one of the eight DOMAINS") + first, second = _right_slices(index, multiplicity) + left_group = _general_linear(index * multiplicity, prime) + slice_group = _general_linear(2, prime) + tested_pairs = len(left_group) * len(slice_group) + if tested_pairs > MAX_PR_PAIRS: + raise ValueError("P,R pair enumeration exceeds the fixed oracle cap") + image = set() + stabilizer_count = 0 + for left, left_det in left_group: + for action, action_det in slice_group: + right_transpose = _candidate(first, second, left, action, prime) + if right_transpose is not None: + stabilizer_count += 1 + right_det = _determinant(right_transpose, prime) + image.add((left_det, right_det, action_det)) + return { + "index": index, + "multiplicity": multiplicity, + "prime": prime, + "image": tuple(sorted(image)), + "stabilizer_count": stabilizer_count, + "tested_pr_pairs": tested_pairs, + "left_group_size": len(left_group), + "slice_group_size": len(slice_group), + } + + +def report(): + """Replay all eight independent fixed domains without writing any files.""" + return tuple(enumerate_image(*case) for case in DOMAINS) + + +if __name__ == "__main__": + import json + + print(json.dumps(report(), sort_keys=True)) diff --git a/research/kronecker-determinant-image/pencil.py b/research/kronecker-determinant-image/pencil.py new file mode 100644 index 0000000000..6bc7fc076e --- /dev/null +++ b/research/kronecker-determinant-image/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/kronecker-determinant-image/verify.py b/research/kronecker-determinant-image/verify.py new file mode 100644 index 0000000000..253b107d2a --- /dev/null +++ b/research/kronecker-determinant-image/verify.py @@ -0,0 +1,189 @@ +#!/usr/bin/env python3 +"""Exact bounded checks, not a formal proof of arbitrary-field completeness. + +apoursh with substantial OpenAI Codex assistance; Apache-2.0. +""" +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path +import sys +from types import ModuleType + +HERE = Path(__file__).resolve().parent + + +def load(name): + # Execute current source bytes; -B alone still permits stale cache reads. + module = ModuleType(name) + path = HERE / (name + '.py') + exec(compile(path.read_bytes(), str(path), 'exec'), module.__dict__) + return module + + +pencil = load('pencil') +oracle = load('oracle') +require = pencil.require +LIFT_DOMAINS = ((1, 1, 2), (2, 1, 2), (3, 2, 2), (5, 1, 2), + (2, 2, 3), (3, 2, 3), (4, 2, 3), + (2, 1, 4), (3, 1, 4), (2, 2, 4), (3, 2, 4), (2, 3, 4), (4, 1, 5)) + + +def field_checks(): + count = 0 + for q in (2, 3, 4, 5): + f = pencil.Field(q) + for a, b, c in product(range(q), repeat=3): + require(f.mul(f.mul(a, b), c) == f.mul(a, f.mul(b, c)), 'associativity') + require(f.mul(a, f.add(b, c)) == f.add(f.mul(a, b), f.mul(a, c)), + 'distributivity') + count += 1 + for a in range(1, q): + require(f.mul(a, f.inv(a)) == 1, 'field inverse') + return count + + +def kernel(e, r, f, left=False): + return {triple for triple in product(range(1, f.q), repeat=3) + if pencil.character(e, r, triple, f, left) == 1} + + +def oracle_checks(): + reports = oracle.report() + for row in reports: + e, r, q = row['index'], row['multiplicity'], row['prime'] + f = pencil.Field(q) + require(set(row['image']) == kernel(e, r, f), 'independent image mismatch') + # GL_r size is a separate elementary count, not a generated witness count. + glr = 1 + for i in range(r): + glr *= q ** r - q ** i + require(row['stabilizer_count'] == glr * (q*q-1) * (q*q-q), + 'complete stabilizer count mismatch') + require(sum(row['tested_pr_pairs'] for row in reports) == 7710, 'oracle coverage') + require(sum(row['stabilizer_count'] for row in reports) == 4470, 'oracle count') + return reports + + +def determinants(witness, field): + return tuple(pencil.determinant(matrix, field) for matrix in witness) + + +def check_witness(e, r, witness, field, left=False): + first, second = pencil.slices(e, r) + if left: + first, second = pencil.transpose(first), pencil.transpose(second) + require(pencil.fixes(first, second, witness, field), 'literal lift equation') + require(pencil.character(e, r, determinants(witness, field), field, left) == 1, + 'witness determinant character') + + +def lift_checks(): + reports = [] + for e, r, q in LIFT_DOMAINS: + f = pencil.Field(q) + count = 0 + for action in pencil.general_linear_two(f): + z = pencil.determinant(action, f) + for u in range(1, q): + d = pencil.identity(r) + d[0][0] = u + if r > 1: + d[0][1] = 1 # non-scalar mixing between repeated blocks + witness = pencil.lift(e, r, action, d, f) + check_witness(e, r, witness, f) + check_witness(e, r, (witness[1], witness[0], action), f, True) + predicted = (f.mul(f.power(u, e), f.power(z, r*e*(e-1)//2)), + f.mul(f.power(u, -e-1), f.power(z, -r*e*(e+1)//2)), z) + require(determinants(witness, f) == predicted, 'parametrized determinant') + count += 1 + reports.append({'index': e, 'multiplicity': r, 'field': q, + 'right_lifts': count, 'transposed_lifts': count}) + return reports + + +def converse_checks(): + accepted = rejected = 0 + for e, r, q in LIFT_DOMAINS: + f = pencil.Field(q) + for left in (False, True): + image = kernel(e, r, f, left) + require(len(image) == (q-1)**2, 'image size') + for triple in product(range(1, q), repeat=3): + if triple in image: + w = pencil.witness_for_triple(e, r, triple, f, left) + check_witness(e, r, w, f, left) + require(determinants(w, f) == triple, 'constructive converse') + accepted += 1 + else: + try: + pencil.witness_for_triple(e, r, triple, f, left) + except ValueError: + rejected += 1 + else: + raise ValueError('excluded determinant triple accepted') + return {'accepted': accepted, 'excluded': rejected} + + +def mutation_checks(): + f3, f4, f5 = (pencil.Field(q) for q in (3, 4, 5)) + require(kernel(2, 1, f3) != {t for t in product((1, 2), repeat=3) if t[0] == 1}, + 'omitted slice exponent was not detected') + require(kernel(1, 2, f3) != kernel(1, 1, f3), 'omitted multiplicity undetected') + require(kernel(2, 1, f3) != kernel(2, 1, f3, True), 'omitted orientation undetected') + first, second = pencil.slices(1, 1) + w = pencil.lift(1, 1, [[1, 1], [0, 2]], [[1]], f5) + for bad_q in (pencil.transpose(w[1]), pencil.inverse(w[1], f5)): + require(not pencil.fixes(first, second, (w[0], bad_q, w[2]), f5), + 'wrong right-factor convention undetected') + # Squaring X+Y in characteristic two has no XY term; F4 is not Z/4Z. + sym = pencil.symmetric_power(2, [[1, 1], [0, 1]], f4) + require(sym[1][0] == 0 and f4.mul(2, 2) == 3, 'characteristic-two arithmetic') + bad = [row[:] for row in sym] + bad[1][0] = 2 # incorrect binomial coefficient modulo q instead of p + p = pencil.transpose(pencil.symmetric_power(1, [[1, 1], [0, 1]], f4)) + a, b = pencil.slices(2, 1) + require(not pencil.fixes(a, b, (p, pencil.inverse(bad, f4), [[1, 1], [0, 1]]), f4), + 'incorrect characteristic reduction undetected') + return 6 + + +def invalid_checks(): + f = pencil.Field(3) + operations = ( + lambda: pencil.Field(6), lambda: pencil.Field(True), + lambda: pencil.slices(0, 1), lambda: pencil.slices(1, 0), + lambda: pencil.slices(6, 1), lambda: pencil.slices(True, 1), + lambda: pencil.lift(1, 1, [[1, 0], [0, 0]], [[1]], f), + lambda: pencil.lift(1, 1, [[1, 0], [0, 1]], [[0]], f), + lambda: pencil.witness_for_triple(1, 1, (0, 1, 1), f), + lambda: oracle.enumerate_image(2, 2, 3), + lambda: pencil.witness_for_triple(10**9, 1, (1, 1, 1), f), + lambda: pencil.witness_for_triple(1, 1, (1, 1), f), + lambda: pencil.lift(1, 1, [[1]], [[1]], f), + lambda: pencil.lift(1, 1, [[1, 0], [0, 1]], [[3]], f), + ) + for operation in operations: + try: + operation() + except ValueError: + continue + raise ValueError('invalid fixture accepted') + return len(operations) + + +def main(): + result = {'field_axiom_triples': field_checks(), 'oracle': oracle_checks(), + 'lift_domains': lift_checks(), 'converse': converse_checks(), + 'mutation_controls': mutation_checks(), 'invalid_controls': invalid_checks(), + 'claim': 'scoped written proof with bounded exact corroboration; no new kappa'} + hashes = {p.name: sha256(p.read_bytes()).hexdigest() + for p in sorted(HERE.iterdir()) if p.is_file()} + print('RESULT ' + json.dumps(result, sort_keys=True)) + print('PACKAGE_SHA256 ' + json.dumps(hashes, sort_keys=True)) + print('PASS_KRONECKER_DETERMINANT_IMAGE') + return 0 + + +if __name__ == '__main__': + sys.exit(main())