diff --git a/research/jordan-second-callee-count/PROOF.md b/research/jordan-second-callee-count/PROOF.md new file mode 100644 index 0000000000..9686b917aa --- /dev/null +++ b/research/jordan-second-callee-count/PROOF.md @@ -0,0 +1,162 @@ +# Exact optimal-callee counts for a two-dimensional Jordan block + +Prepared for NicholasStone with OpenAI Codex assistance. Apache-2.0. + +## Result + +Let F = F_q be any finite field, let lambda be nonzero, and put + + N = [[0,1],[0,0]], P = lambda I + N. + +Use the unchanged ordinary wrapper with chronological operations + + D -= H; F_P; D += H; F_Q; D = -D; D += H, + F_T(H,D) = (T D, T^-1 H). + +The second map Q must be invertible. Call it optimal when the rank of the +wrapper error relative to interchange J(H,D)=(D,H) is minimal over all such Q. + +**Theorem.** The exact number of optimal second maps is + + 1 if lambda^2 = 1; + q^2 if lambda^2 != 1 and lambda^2 = -1; + q(q-1) if lambda^2 != 1 and lambda^2 != -1. + +The order of these cases matters in characteristic 2, where 1=-1. In that +characteristic every lambda != 0,1 belongs to the third case. In the regular +case lambda^2 != 1, write A=P^2-I. All optimal second maps are uniquely + + Q = P + A S, + S = [[a,b],[c,-a]], a^2+bc = 0, + lambda^2 + (lambda^2+1)c != 0. (1) + +If lambda^2+1 is nonzero, the excluded parameters are exactly the q matrices + + c0 = -lambda^2/(lambda^2+1), + S_a = [[a, -a^2/c0], [c0, -a]], a in F. (2) + +Each regular-case optimal Q agrees with interchange on q^2 of the q^4 +input pairs. This is optimal agreement, not agreement on all inputs. + +## Attribution and the inherited reduction + +Nick Petalas's [PR5228](https://github.com/CrocSwap/integer-mult-bounds/pull/5228), +`research/optimal-second-callees/PROOF.md`, classifies all optimal second +callees using a square-zero endomorphism and an invertibility filter. +Its README explicitly leaves nonscalar filtered counting open, beginning +with one nonsemisimple block. Jerry Chen / CubeJerry's +[PR2950](https://github.com/CrocSwap/integer-mult-bounds/pull/2950) supplies +the already-known optimum and the attainer Q=P. These are predecessor +results, not new claims here. + +For clarity, the small amount of inherited algebra needed here is recorded. +Put R=Q-P, x=D-H and y=P^-1 H+P x. Direct execution gives + + H' = Q P^-1 H + Q P x, + D' = H' - Q^-1 P x. + +For e1=H'-D and e2=D'-H this yields + + e1 = A x + R y, Q(e2-e1)=R x. + +Both the input change to (x,y) and the output change to (e1,Q(e2-e1)) are +invertible. Therefore the error rank equals the rank of + + M = [[A,R],[R,0]]. (3) + +The minimum is rank A, since A is a submatrix and Q=P attains that lower +bound. If A is invertible, block elimination gives + + rank M = 2 + rank(R A^-1 R). + +Writing R=A S gives R A^-1 R=A S^2. Thus optimality is equivalent to +S^2=0, subject to Q being invertible. Since A is invertible, different S +give different Q. This is the invertible-A specialization of PR5228. + +## Square-zero matrices over every characteristic + +For a two-by-two matrix S, S^2=0 is equivalent to + + S = [[a,b],[c,-a]], a^2+bc=0. (4) + +Indeed, im S is contained in ker S, so det S=0. Cayley-Hamilton gives +S^2-(tr S)S=0; for nonzero S with S^2=0 this forces tr S=0, and S=0 has +zero trace as well. Conversely the square of the displayed matrix is +(a^2+bc)I. No division by 2 is used. + +For each fixed c there are exactly q solutions (a,b): + +* If c=0, a^2=0 forces a=0, while b is arbitrary. +* If c is nonzero, a is arbitrary and b=-a^2/c is uniquely determined. + +Consequently there are q^2 square-zero matrices, and the lower-left entry c +has q preimages for every field element. This uniform fiber count is the +counting step used below. + +## The determinant filter + +Assume lambda^2 != 1, so A is invertible. Since N^2=0, + + P^-1 = lambda^-1 I - lambda^-2 N, + B := P^-1 A = P-P^-1 + = (lambda-lambda^-1)I + (1+lambda^-2)N. + +For square-zero S, both tr S and det S vanish, and tr(NS)=c. The +two-dimensional identity det(I+T)=1+tr T+det T therefore gives + + det Q = det P det(I+B S) + = lambda^2 [1 + (1+lambda^-2)c] + = lambda^2 + (lambda^2+1)c. (5) + +If lambda^2+1=0, this determinant is the fixed nonzero value lambda^2, so +all q^2 parameters survive. Otherwise (5) vanishes at precisely the nonzero +value c0 in (2). The fiber over c0 has exactly q elements, yielding q^2-q +survivors and the complete rejection family (2). + +In fact, when lambda^2+1 != 0 the determinant map from the entire square-zero +parameter set to F is uniform: every determinant value has exactly q +preimages. Thus each prescribed nonzero determinant occurs for q optimal Q. +In the exceptional case every optimal Q has determinant lambda^2. + +For an alternative direct calculation, with d=lambda^2-1 one has + + Q = [[lambda+d a+2 lambda c, 1+d b-2 lambda a], + [d c, lambda-d a]]. + +Expanding this determinant and substituting a^2+bc=0 also gives (5). + +## The boundary lambda^2=1 + +Here A=2 lambda N. In characteristic 2, A=0 and the minimum error rank is +zero; (3) has rank zero only when R=0. Thus Q=P is the unique optimum. + +In odd characteristic, A has rank one. Equality rank M=rank A requires both +im R contained in im A and ker A contained in ker R: otherwise adjoining R +to A horizontally or vertically would already raise the rank. These two +containments force R=beta N. Deleting the zero rows and columns of (3) +leaves + + [[2 lambda,beta],[beta,0]]. + +If beta is nonzero its determinant is -beta^2 and its rank is two, exceeding +the minimum one. Hence beta=0 and again Q=P is the unique optimum. +This completes the theorem for every nonzero lambda over every finite field. + +## Scope + +The contribution is the explicit filtered count, determinant distribution +and rejection family for one two-dimensional nonscalar Jordan block. The +result is also invariant under simultaneous change of basis: conjugating P +and Q preserves wrapper error rank and gives a bijection of optimal maps. +The generic rational-canonical-data counting question and Jordan blocks of +size at least three remain open here. The finite verifier corroborates the +written proof; it is not a proof-kernel formalization. No implementation cost, +supplier, improved kappa or complete multiplication theorem is claimed. + +## Open next questions + +* For P=J_3(lambda), count the filtered square-zero parameters, first with + lambda^2 != 1. Every nonzero square-zero 3x3 matrix has rank one, so writing + S=u v^T with v^T u=0 may make the determinant filter tractable. +* Determine how this filtered count combines across several Jordan blocks; + off-diagonal parts of S couple the blocks and prevent a naive product rule. diff --git a/research/jordan-second-callee-count/README.md b/research/jordan-second-callee-count/README.md new file mode 100644 index 0000000000..da13fd8c53 --- /dev/null +++ b/research/jordan-second-callee-count/README.md @@ -0,0 +1,58 @@ +# Two-dimensional Jordan first map: solved filtered callee count + +This package resolves the two-dimensional nonsemisimple starting case of +the nonscalar counting question in Nick Petalas's PR5228. It does not close +that question for arbitrary rational canonical data. + +For P=J_2(lambda) over F_q with lambda nonzero, the number of optimal +invertible second maps in the fixed ordinary wrapper is: + +| Condition | Count | +| --- | ---: | +| lambda^2=1 | 1 | +| lambda^2!=1 and lambda^2=-1 | q^2 | +| lambda^2!=1 and lambda^2!=-1 | q(q-1) | + +For lambda^2!=1 the parameters are Q=P+(P^2-I)S with S^2=0. Write +S=[[a,b],[c,-a]], a^2+bc=0. The determinant is exactly +lambda^2+(lambda^2+1)c. Each c has q square-zero preimages, giving both the +count and a complete description of singular rejections. + +Examples: over F4 both eligible lambda give 12 optimal maps; over F5, +lambda=2,3 both give 25; over F7, lambda=2,3,4,5 each give 42. These examples +also show why the exceptional branch must be retained. + +See [PROOF.md](PROOF.md) for the all-field proof and predecessor credit. + +## Reproduce + +Standard library only; Python 3.12 or newer: + +```sh +python3 -I -W error -B research/jordan-second-callee-count/verify.py +python3 -I -O -W error -B research/jordan-second-callee-count/verify.py +``` + +The script prints a generated JSON receipt and writes no files. All checks +use explicit exceptions and remain active under Python -O. + +The fields are q=2,3,4,5,7,8,9,11,13,16. Polynomial-basis extension fields +are used for nonprime q; these are not integers modulo q. The script verifies +the finite field tables, enumerates every 2x2 matrix to find S^2=0 without +using the claimed parameterization, then compares both sets and all +determinant fibers. For each regular lambda it checks the rejection family +and the accepted count. For every q<=9 and every nonzero lambda, it separately +enumerates all invertible Q and runs the six literal wrapper operations on +all four basis inputs. The resulting error-rank-optimal set must equal the +predicted set, including the lambda^2=1 boundary. This second path does not +use the block-matrix reduction to calculate the wrapper error rank. + +`VALIDATION.json` records the actual interpreter and completed runs. +`SOURCES.json` records the pinned predecessor source. The predecessor documents are pinned at their canonical repository paths; +all predecessor attribution is retained in PROOF.md. + +## Open next questions + +The next narrow target is J_3(lambda); arbitrary block structures remain open. +See PROOF.md for the rank-one starting representation and the block-coupling +issue. This algebraic result does not change the selected multiplication bound. diff --git a/research/jordan-second-callee-count/SOURCES.json b/research/jordan-second-callee-count/SOURCES.json new file mode 100644 index 0000000000..0d4a480735 --- /dev/null +++ b/research/jordan-second-callee-count/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "13be6ac685845c1ff671f5d26e7166165abd998e", + "files": [ + { + "path": "research/optimal-second-callees/PROOF.md", + "usage": "provenance", + "git_blob": "4bd60b22144903be71870eef91a540e138208da3", + "sha256": "309c0c7b9c1452fd29c17cd72c83bb93b02a8ca44ccb80934d43ffa4cb5589f7" + }, + { + "path": "research/optimal-second-callees/README.md", + "usage": "provenance", + "git_blob": "01bf464c2cfbf576a089f1cdc5e71b367d7fcf85", + "sha256": "99c816abf0a7f0ef25843a7adb3b29b4ab983d108c04506827a622f696a5f33e" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + } + ] +} diff --git a/research/jordan-second-callee-count/TASK.json b/research/jordan-second-callee-count/TASK.json new file mode 100644 index 0000000000..28484ce0aa --- /dev/null +++ b/research/jordan-second-callee-count/TASK.json @@ -0,0 +1,73 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "13be6ac685845c1ff671f5d26e7166165abd998e", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "scope_change_reason": "Explicit user-selected follow-up to PR5228: solve the nonscalar filtered-count question for one two-dimensional Jordan block. No task picker reroll.", + "actual_scope": "Count every optimal invertible second callee for P=J_2(lambda) over every finite field, including characteristic two and lambda squared equal to one.", + "bottleneck_link": "Resolves the first nonsemisimple case of the optimal-callee counting handoff; no paid supplier or bound improvement follows.", + "stop_rule": "Stop after proof, finite corroboration and a focused PR. Higher Jordan blocks remain next questions.", + "outcome": "completed", + "evidence": "PROOF.md, verify.py and VALIDATION.json", + "author": "Nicholas Stone / NicholasStone", + "ai_assistance": "Substantial OpenAI Codex assistance. No independent human or proof-kernel review.", + "open_questions": [ + { + "question": "Count the optimal second callees for J_3(lambda).", + "why_it_matters": "Extends the first nonscalar block count.", + "first_step": "Represent nonzero square-zero parameters as rank-one u v^T with v^T u=0.", + "blocked_by": "The determinant filter is not derived here for dimension three." + } + ] +} diff --git a/research/jordan-second-callee-count/VALIDATION.json b/research/jordan-second-callee-count/VALIDATION.json new file mode 100644 index 0000000000..73b33fc35d --- /dev/null +++ b/research/jordan-second-callee-count/VALIDATION.json @@ -0,0 +1,660 @@ +{ + "status": "passed", + "commands": [ + { + "argv": [ + "python3", + "-I", + "-W", + "error", + "-B", + "verify.py" + ], + "exit_code": 0 + }, + { + "argv": [ + "python3", + "-I", + "-O", + "-W", + "error", + "-B", + "verify.py" + ], + "exit_code": 0 + } + ], + "normal_optimized_receipts_identical": true, + "verifier_sha256": "c14c44aec03638a9afe9e00b084e52a1d42011220abec527ab3dddc44438c921", + "receipt": { + "all_matrices_checked": 122774, + "field_count": 10, + "fields": [ + { + "all_matrices_checked": 16, + "cases": [ + { + "lambda_encoding": 1, + "lambda_squared": 1, + "literal_wrapper_optimal_count": 1, + "optimal_count": 1, + "singular_square_zero_parameters": null + } + ], + "characteristic": 2, + "literal_wrapper_pairs": 6, + "polynomial_low_to_high": [ + 0, + 1 + ], + "q": 2, + "square_zero_matrices": 4 + }, + { + "all_matrices_checked": 81, + "cases": [ + { + "lambda_encoding": 1, + "lambda_squared": 1, + "literal_wrapper_optimal_count": 1, + "optimal_count": 1, + "singular_square_zero_parameters": null + }, + { + "lambda_encoding": 2, + "lambda_squared": 1, + "literal_wrapper_optimal_count": 1, + "optimal_count": 1, + "singular_square_zero_parameters": null + } + ], + "characteristic": 3, + "literal_wrapper_pairs": 96, + "polynomial_low_to_high": [ + 0, + 1 + ], + "q": 3, + "square_zero_matrices": 9 + }, + { + "all_matrices_checked": 256, + "cases": [ + { + "lambda_encoding": 1, + "lambda_squared": 1, + "literal_wrapper_optimal_count": 1, + "optimal_count": 1, + "singular_square_zero_parameters": null + }, + { + "lambda_encoding": 2, + "lambda_squared": 3, + "literal_wrapper_optimal_count": 12, + "optimal_count": 12, + "singular_square_zero_parameters": 4 + }, + { + "lambda_encoding": 3, + "lambda_squared": 2, + "literal_wrapper_optimal_count": 12, + "optimal_count": 12, + "singular_square_zero_parameters": 4 + } + ], + "characteristic": 2, + "literal_wrapper_pairs": 540, + "polynomial_low_to_high": [ + 1, + 1, + 1 + ], + "q": 4, + "square_zero_matrices": 16 + }, + { + "all_matrices_checked": 625, + "cases": [ + { + "lambda_encoding": 1, + "lambda_squared": 1, + "literal_wrapper_optimal_count": 1, + "optimal_count": 1, + "singular_square_zero_parameters": null + }, + { + "lambda_encoding": 2, + "lambda_squared": 4, + "literal_wrapper_optimal_count": 25, + "optimal_count": 25, + "singular_square_zero_parameters": 0 + }, + { + "lambda_encoding": 3, + "lambda_squared": 4, + "literal_wrapper_optimal_count": 25, + "optimal_count": 25, + "singular_square_zero_parameters": 0 + }, + { + "lambda_encoding": 4, + "lambda_squared": 1, + "literal_wrapper_optimal_count": 1, + "optimal_count": 1, + "singular_square_zero_parameters": null + } + ], + "characteristic": 5, + "literal_wrapper_pairs": 1920, + "polynomial_low_to_high": [ + 0, + 1 + ], + "q": 5, + "square_zero_matrices": 25 + }, + { + "all_matrices_checked": 2401, + "cases": [ + { + "lambda_encoding": 1, + "lambda_squared": 1, + "literal_wrapper_optimal_count": 1, + "optimal_count": 1, + "singular_square_zero_parameters": null + }, + { + "lambda_encoding": 2, + "lambda_squared": 4, + "literal_wrapper_optimal_count": 42, + "optimal_count": 42, + "singular_square_zero_parameters": 7 + }, + { + "lambda_encoding": 3, + "lambda_squared": 2, + "literal_wrapper_optimal_count": 42, + "optimal_count": 42, + "singular_square_zero_parameters": 7 + }, + { + "lambda_encoding": 4, + "lambda_squared": 2, + "literal_wrapper_optimal_count": 42, + "optimal_count": 42, + "singular_square_zero_parameters": 7 + }, + { + "lambda_encoding": 5, + "lambda_squared": 4, + "literal_wrapper_optimal_count": 42, + "optimal_count": 42, + "singular_square_zero_parameters": 7 + }, + { + "lambda_encoding": 6, + "lambda_squared": 1, + "literal_wrapper_optimal_count": 1, + "optimal_count": 1, + "singular_square_zero_parameters": null + } + ], + "characteristic": 7, + "literal_wrapper_pairs": 12096, + "polynomial_low_to_high": [ + 0, + 1 + ], + "q": 7, + "square_zero_matrices": 49 + }, + { + "all_matrices_checked": 4096, + "cases": [ + { + "lambda_encoding": 1, + "lambda_squared": 1, + "literal_wrapper_optimal_count": 1, + "optimal_count": 1, + "singular_square_zero_parameters": null + }, + { + "lambda_encoding": 2, + "lambda_squared": 4, + "literal_wrapper_optimal_count": 56, + "optimal_count": 56, + "singular_square_zero_parameters": 8 + }, + { + "lambda_encoding": 3, + "lambda_squared": 5, + "literal_wrapper_optimal_count": 56, + "optimal_count": 56, + "singular_square_zero_parameters": 8 + }, + { + "lambda_encoding": 4, + "lambda_squared": 6, + "literal_wrapper_optimal_count": 56, + "optimal_count": 56, + "singular_square_zero_parameters": 8 + }, + { + "lambda_encoding": 5, + "lambda_squared": 7, + "literal_wrapper_optimal_count": 56, + "optimal_count": 56, + "singular_square_zero_parameters": 8 + }, + { + "lambda_encoding": 6, + "lambda_squared": 2, + "literal_wrapper_optimal_count": 56, + "optimal_count": 56, + "singular_square_zero_parameters": 8 + }, + { + "lambda_encoding": 7, + "lambda_squared": 3, + "literal_wrapper_optimal_count": 56, + "optimal_count": 56, + "singular_square_zero_parameters": 8 + } + ], + "characteristic": 2, + "literal_wrapper_pairs": 24696, + "polynomial_low_to_high": [ + 1, + 1, + 0, + 1 + ], + "q": 8, + "square_zero_matrices": 64 + }, + { + "all_matrices_checked": 6561, + "cases": [ + { + "lambda_encoding": 1, + "lambda_squared": 1, + "literal_wrapper_optimal_count": 1, + "optimal_count": 1, + "singular_square_zero_parameters": null + }, + { + "lambda_encoding": 2, + "lambda_squared": 1, + "literal_wrapper_optimal_count": 1, + "optimal_count": 1, + "singular_square_zero_parameters": null + }, + { + "lambda_encoding": 3, + "lambda_squared": 2, + "literal_wrapper_optimal_count": 81, + "optimal_count": 81, + "singular_square_zero_parameters": 0 + }, + { + "lambda_encoding": 4, + "lambda_squared": 6, + "literal_wrapper_optimal_count": 72, + "optimal_count": 72, + "singular_square_zero_parameters": 9 + }, + { + "lambda_encoding": 5, + "lambda_squared": 3, + "literal_wrapper_optimal_count": 72, + "optimal_count": 72, + "singular_square_zero_parameters": 9 + }, + { + "lambda_encoding": 6, + "lambda_squared": 2, + "literal_wrapper_optimal_count": 81, + "optimal_count": 81, + "singular_square_zero_parameters": 0 + }, + { + "lambda_encoding": 7, + "lambda_squared": 3, + "literal_wrapper_optimal_count": 72, + "optimal_count": 72, + "singular_square_zero_parameters": 9 + }, + { + "lambda_encoding": 8, + "lambda_squared": 6, + "literal_wrapper_optimal_count": 72, + "optimal_count": 72, + "singular_square_zero_parameters": 9 + } + ], + "characteristic": 3, + "literal_wrapper_pairs": 46080, + "polynomial_low_to_high": [ + 1, + 0, + 1 + ], + "q": 9, + "square_zero_matrices": 81 + }, + { + "all_matrices_checked": 14641, + "cases": [ + { + "lambda_encoding": 1, + "lambda_squared": 1, + "literal_wrapper_optimal_count": null, + "optimal_count": 1, + "singular_square_zero_parameters": null + }, + { + "lambda_encoding": 2, + "lambda_squared": 4, + "literal_wrapper_optimal_count": null, + "optimal_count": 110, + "singular_square_zero_parameters": 11 + }, + { + "lambda_encoding": 3, + "lambda_squared": 9, + "literal_wrapper_optimal_count": null, + "optimal_count": 110, + "singular_square_zero_parameters": 11 + }, + { + "lambda_encoding": 4, + "lambda_squared": 5, + "literal_wrapper_optimal_count": null, + "optimal_count": 110, + "singular_square_zero_parameters": 11 + }, + { + "lambda_encoding": 5, + "lambda_squared": 3, + "literal_wrapper_optimal_count": null, + "optimal_count": 110, + "singular_square_zero_parameters": 11 + }, + { + "lambda_encoding": 6, + "lambda_squared": 3, + "literal_wrapper_optimal_count": null, + "optimal_count": 110, + "singular_square_zero_parameters": 11 + }, + { + "lambda_encoding": 7, + "lambda_squared": 5, + "literal_wrapper_optimal_count": null, + "optimal_count": 110, + "singular_square_zero_parameters": 11 + }, + { + "lambda_encoding": 8, + "lambda_squared": 9, + "literal_wrapper_optimal_count": null, + "optimal_count": 110, + "singular_square_zero_parameters": 11 + }, + { + "lambda_encoding": 9, + "lambda_squared": 4, + "literal_wrapper_optimal_count": null, + "optimal_count": 110, + "singular_square_zero_parameters": 11 + }, + { + "lambda_encoding": 10, + "lambda_squared": 1, + "literal_wrapper_optimal_count": null, + "optimal_count": 1, + "singular_square_zero_parameters": null + } + ], + "characteristic": 11, + "literal_wrapper_pairs": 0, + "polynomial_low_to_high": [ + 0, + 1 + ], + "q": 11, + "square_zero_matrices": 121 + }, + { + "all_matrices_checked": 28561, + "cases": [ + { + "lambda_encoding": 1, + "lambda_squared": 1, + "literal_wrapper_optimal_count": null, + "optimal_count": 1, + "singular_square_zero_parameters": null + }, + { + "lambda_encoding": 2, + "lambda_squared": 4, + "literal_wrapper_optimal_count": null, + "optimal_count": 156, + "singular_square_zero_parameters": 13 + }, + { + "lambda_encoding": 3, + "lambda_squared": 9, + "literal_wrapper_optimal_count": null, + "optimal_count": 156, + "singular_square_zero_parameters": 13 + }, + { + "lambda_encoding": 4, + "lambda_squared": 3, + "literal_wrapper_optimal_count": null, + "optimal_count": 156, + "singular_square_zero_parameters": 13 + }, + { + "lambda_encoding": 5, + "lambda_squared": 12, + "literal_wrapper_optimal_count": null, + "optimal_count": 169, + "singular_square_zero_parameters": 0 + }, + { + "lambda_encoding": 6, + "lambda_squared": 10, + "literal_wrapper_optimal_count": null, + "optimal_count": 156, + "singular_square_zero_parameters": 13 + }, + { + "lambda_encoding": 7, + "lambda_squared": 10, + "literal_wrapper_optimal_count": null, + "optimal_count": 156, + "singular_square_zero_parameters": 13 + }, + { + "lambda_encoding": 8, + "lambda_squared": 12, + "literal_wrapper_optimal_count": null, + "optimal_count": 169, + "singular_square_zero_parameters": 0 + }, + { + "lambda_encoding": 9, + "lambda_squared": 3, + "literal_wrapper_optimal_count": null, + "optimal_count": 156, + "singular_square_zero_parameters": 13 + }, + { + "lambda_encoding": 10, + "lambda_squared": 9, + "literal_wrapper_optimal_count": null, + "optimal_count": 156, + "singular_square_zero_parameters": 13 + }, + { + "lambda_encoding": 11, + "lambda_squared": 4, + "literal_wrapper_optimal_count": null, + "optimal_count": 156, + "singular_square_zero_parameters": 13 + }, + { + "lambda_encoding": 12, + "lambda_squared": 1, + "literal_wrapper_optimal_count": null, + "optimal_count": 1, + "singular_square_zero_parameters": null + } + ], + "characteristic": 13, + "literal_wrapper_pairs": 0, + "polynomial_low_to_high": [ + 0, + 1 + ], + "q": 13, + "square_zero_matrices": 169 + }, + { + "all_matrices_checked": 65536, + "cases": [ + { + "lambda_encoding": 1, + "lambda_squared": 1, + "literal_wrapper_optimal_count": null, + "optimal_count": 1, + "singular_square_zero_parameters": null + }, + { + "lambda_encoding": 2, + "lambda_squared": 4, + "literal_wrapper_optimal_count": null, + "optimal_count": 240, + "singular_square_zero_parameters": 16 + }, + { + "lambda_encoding": 3, + "lambda_squared": 5, + "literal_wrapper_optimal_count": null, + "optimal_count": 240, + "singular_square_zero_parameters": 16 + }, + { + "lambda_encoding": 4, + "lambda_squared": 3, + "literal_wrapper_optimal_count": null, + "optimal_count": 240, + "singular_square_zero_parameters": 16 + }, + { + "lambda_encoding": 5, + "lambda_squared": 2, + "literal_wrapper_optimal_count": null, + "optimal_count": 240, + "singular_square_zero_parameters": 16 + }, + { + "lambda_encoding": 6, + "lambda_squared": 7, + "literal_wrapper_optimal_count": null, + "optimal_count": 240, + "singular_square_zero_parameters": 16 + }, + { + "lambda_encoding": 7, + "lambda_squared": 6, + "literal_wrapper_optimal_count": null, + "optimal_count": 240, + "singular_square_zero_parameters": 16 + }, + { + "lambda_encoding": 8, + "lambda_squared": 12, + "literal_wrapper_optimal_count": null, + "optimal_count": 240, + "singular_square_zero_parameters": 16 + }, + { + "lambda_encoding": 9, + "lambda_squared": 13, + "literal_wrapper_optimal_count": null, + "optimal_count": 240, + "singular_square_zero_parameters": 16 + }, + { + "lambda_encoding": 10, + "lambda_squared": 8, + "literal_wrapper_optimal_count": null, + "optimal_count": 240, + "singular_square_zero_parameters": 16 + }, + { + "lambda_encoding": 11, + "lambda_squared": 9, + "literal_wrapper_optimal_count": null, + "optimal_count": 240, + "singular_square_zero_parameters": 16 + }, + { + "lambda_encoding": 12, + "lambda_squared": 15, + "literal_wrapper_optimal_count": null, + "optimal_count": 240, + "singular_square_zero_parameters": 16 + }, + { + "lambda_encoding": 13, + "lambda_squared": 14, + "literal_wrapper_optimal_count": null, + "optimal_count": 240, + "singular_square_zero_parameters": 16 + }, + { + "lambda_encoding": 14, + "lambda_squared": 11, + "literal_wrapper_optimal_count": null, + "optimal_count": 240, + "singular_square_zero_parameters": 16 + }, + { + "lambda_encoding": 15, + "lambda_squared": 10, + "literal_wrapper_optimal_count": null, + "optimal_count": 240, + "singular_square_zero_parameters": 16 + } + ], + "characteristic": 2, + "literal_wrapper_pairs": 0, + "polynomial_low_to_high": [ + 1, + 1, + 0, + 0, + 1 + ], + "q": 16, + "square_zero_matrices": 256 + } + ], + "first_maps": 68, + "literal_wrapper_pairs": 85434, + "python": "3.14.4", + "status": "PASS_JORDAN_CALLEE_COUNT" + }, + "limits": [ + "Local finite enumeration only; general validity is established by PROOF.md.", + "No formal proof assistant or hosted CI run.", + "Python 3.12 was not run locally; actual interpreter version is in the receipt.", + "The general rational-canonical-data question is not resolved." + ], + "package_metadata_validation": "passed with check_pins=False in a local fixture; canonical Git history replay not run" +} diff --git a/research/jordan-second-callee-count/VERIFY.json b/research/jordan-second-callee-count/VERIFY.json new file mode 100644 index 0000000000..0d2fedbb4c --- /dev/null +++ b/research/jordan-second-callee-count/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": "Exact field tables, square-zero enumeration, determinant distribution and singular rejections; literal wrapper execution against all invertible Q for q <= 9." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact field tables, square-zero enumeration, determinant distribution and singular rejections; literal wrapper execution against all invertible Q for q <= 9." + } + ] +} diff --git a/research/jordan-second-callee-count/verify.py b/research/jordan-second-callee-count/verify.py new file mode 100644 index 0000000000..5ba269a593 --- /dev/null +++ b/research/jordan-second-callee-count/verify.py @@ -0,0 +1,220 @@ +#!/usr/bin/env python3 +"""Exact, standard-library finite checks of the 2x2 Jordan callee count.""" + +import itertools +import json +import platform +from collections import Counter + + +def require(condition, message): + if not condition: + raise RuntimeError(message) + + +class Field: + """Polynomial-basis F_p[x]/(monic polynomial), encoded in base p.""" + + def __init__(self, p, polynomial): + self.p = p + self.polynomial = polynomial + self.degree = len(polynomial) - 1 + self.q = p ** self.degree + digits = [tuple((a // p**i) % p for i in range(self.degree)) + for a in range(self.q)] + self.add = [[sum(((x + y) % p) * p**i + for i, (x, y) in enumerate(zip(a, b))) + for b in digits] for a in digits] + self.mul = [[self.multiply(a, b) for b in digits] for a in digits] + self.neg = [next(b for b in range(self.q) if self.add[a][b] == 0) + for a in range(self.q)] + self.inv = [0] + [next(b for b in range(1, self.q) + if self.mul[a][b] == 1) + for a in range(1, self.q)] + + def multiply(self, a, b): + d, p = self.degree, self.p + coefficients = [0] * (2 * d - 1) + for i, x in enumerate(a): + for j, y in enumerate(b): + coefficients[i + j] += x * y + for k in range(2 * d - 2, d - 1, -1): + value = coefficients[k] % p + for j in range(d + 1): + coefficients[k - d + j] -= value * self.polynomial[j] + return sum((coefficients[i] % p) * p**i for i in range(d)) + + def validate(self): + a, m, q = self.add, self.mul, self.q + for x, y, z in itertools.product(range(q), repeat=3): + require(a[a[x][y]][z] == a[x][a[y][z]], "add associativity") + require(m[m[x][y]][z] == m[x][m[y][z]], "mul associativity") + require(m[x][a[y][z]] == a[m[x][y]][m[x][z]], "distributivity") + for x, y in itertools.product(range(q), repeat=2): + require(a[x][y] == a[y][x] and m[x][y] == m[y][x], "commutativity") + for x in range(q): + require(a[x][0] == x and m[x][1] == x, "identities") + require(a[x][self.neg[x]] == 0, "additive inverse") + if x: + require(m[x][self.inv[x]] == 1, "multiplicative inverse") + + +ZERO = (0, 0, 0, 0) +IDENTITY = (1, 0, 0, 1) + + +def add(f, x, y): + return tuple(f.add[a][b] for a, b in zip(x, y)) + + +def sub(f, x, y): + return tuple(f.add[a][f.neg[b]] for a, b in zip(x, y)) + + +def mm(f, x, y): + a, m = f.add, f.mul + return tuple(a[m[x[2*i]][y[j]]][m[x[2*i+1]][y[2+j]]] + for i in range(2) for j in range(2)) + + +def mv(f, x, y): + a, m = f.add, f.mul + return tuple(a[m[x[2*i]][y[0]]][m[x[2*i+1]][y[1]]] + for i in range(2)) + + +def det(f, x): + return f.add[f.mul[x[0]][x[3]]][f.neg[f.mul[x[1]][x[2]]]] + + +def inverse(f, x): + d = det(f, x) + require(d != 0, "attempt to invert singular matrix") + return tuple(f.mul[f.inv[d]][a] + for a in (x[3], f.neg[x[1]], f.neg[x[2]], x[0])) + + +def rank(f, rows): + rows = [list(row) for row in rows] + result = 0 + for col in range(len(rows[0])): + pivot = next((i for i in range(result, len(rows)) if rows[i][col]), None) + if pivot is None: + continue + rows[result], rows[pivot] = rows[pivot], rows[result] + scale = f.inv[rows[result][col]] + rows[result] = [f.mul[scale][v] for v in rows[result]] + for i in range(result + 1, len(rows)): + factor = rows[i][col] + rows[i] = [f.add[x][f.neg[f.mul[factor][y]]] + for x, y in zip(rows[i], rows[result])] + result += 1 + if result == len(rows): + break + return result + + +def wrapper_rank(f, p, pinv, q, qinv): + """Execute the six literal operations on all four basis vectors.""" + columns = [] + for k in range(4): + initial = tuple(int(k == j) for j in range(4)) + h, d = initial[:2], initial[2:] + d = sub(f, d, h) + h, d = mv(f, p, d), mv(f, pinv, h) + d = add(f, d, h) + h, d = mv(f, q, d), mv(f, qinv, h) + d = tuple(f.neg[x] for x in d) + d = add(f, d, h) + columns.append(sub(f, h + d, initial[2:] + initial[:2])) + return rank(f, list(zip(*columns))) + + +def check_parameters(f, lam, square_zero): + q, a, m = f.q, f.add, f.mul + p = (lam, 1, 0, lam) + aa = sub(f, mm(f, p, p), IDENTITY) + l2 = m[lam][lam] + coefficient = a[l2][1] + histogram, accepted = Counter(), set() + for s in square_zero: + candidate = add(f, p, mm(f, aa, s)) + determinant = det(f, candidate) + require(determinant == a[l2][m[coefficient][s[2]]], "determinant identity") + histogram[determinant] += 1 + if determinant: + accepted.add(candidate) + predicted = q*q if coefficient == 0 else q*q-q + require(len(accepted) == predicted, "filtered cardinality") + expected_histogram = ({l2: q*q} if coefficient == 0 + else {value: q for value in range(q)}) + require(dict(histogram) == expected_histogram, "full determinant distribution") + if coefficient: + c = f.neg[m[l2][f.inv[coefficient]]] + excluded = {(x, f.neg[m[m[x][x]][f.inv[c]]], c, f.neg[x]) + for x in range(q)} + actual = {s for s in square_zero if det(f, add(f, p, mm(f, aa, s))) == 0} + require(actual == excluded and len(actual) == q, "exact rejection family") + return accepted, histogram[0] + + +def check_field(f): + f.validate() + q = f.q + square_zero = {s for s in itertools.product(range(q), repeat=4) + if mm(f, s, s) == ZERO} + parameterized = {(a, b, c, f.neg[a]) + for a, b, c in itertools.product(range(q), repeat=3) + if f.add[f.mul[a][a]][f.mul[b][c]] == 0} + require(square_zero == parameterized and len(square_zero) == q*q, + "square-zero parameterization") + records, candidates = [], 0 + invertibles = ([(s, inverse(f, s)) + for s in itertools.product(range(q), repeat=4) if det(f, s)] + if q <= 9 else []) + for lam in range(1, q): + p = (lam, 1, 0, lam) + l2 = f.mul[lam][lam] + if l2 == 1: + predicted_set, rejected = {p}, None + else: + predicted_set, rejected = check_parameters(f, lam, square_zero) + observed = None + if invertibles: + aa = sub(f, mm(f, p, p), IDENTITY) + minimum = rank(f, [aa[:2], aa[2:]]) + pinv, optimal = inverse(f, p), set() + for candidate, qinv in invertibles: + error_rank = wrapper_rank(f, p, pinv, candidate, qinv) + require(error_rank >= minimum, "known minimum error rank") + if error_rank == minimum: + optimal.add(candidate) + require(optimal == predicted_set, "literal wrapper optimal set") + observed = len(optimal) + candidates += len(invertibles) + records.append({"lambda_encoding": lam, "lambda_squared": l2, + "optimal_count": len(predicted_set), + "singular_square_zero_parameters": rejected, + "literal_wrapper_optimal_count": observed}) + return {"q": q, "characteristic": f.p, "polynomial_low_to_high": f.polynomial, + "square_zero_matrices": len(square_zero), "all_matrices_checked": q**4, + "literal_wrapper_pairs": candidates, "cases": records} + + +def main(): + specifications = [(2, [0, 1]), (3, [0, 1]), (2, [1, 1, 1]), + (5, [0, 1]), (7, [0, 1]), (2, [1, 1, 0, 1]), + (3, [1, 0, 1]), (11, [0, 1]), (13, [0, 1]), + (2, [1, 1, 0, 0, 1])] + results = [check_field(Field(p, polynomial)) for p, polynomial in specifications] + receipt = {"status": "PASS_JORDAN_CALLEE_COUNT", "python": platform.python_version(), + "field_count": len(results), + "first_maps": sum(len(item["cases"]) for item in results), + "all_matrices_checked": sum(item["all_matrices_checked"] for item in results), + "literal_wrapper_pairs": sum(item["literal_wrapper_pairs"] for item in results), + "fields": results} + print(json.dumps(receipt, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()