Skip to content

Extract exact matrix-pencil stabilizer determinant images (no new κ) #5250

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Mister-Meeseeks merged 1 commit into from
Oct 23, 2026
Merged

Extract exact matrix-pencil stabilizer determinant images (no new κ) #5250

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
221 changes: 221 additions & 0 deletions research/pencil-determinant-image/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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.
44 changes: 44 additions & 0 deletions research/pencil-determinant-image/SOURCES.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,44 @@
{
"schema_version": 1,
"base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
"files": [
{
"path": "certificates/selected-result.json",
"usage": "provenance",
"git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
"sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
},
{
"path": "docs/research/agent-task-catalog.json",
"usage": "provenance",
"git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
"sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
},
{
"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"
}
],
"literature": [
{
"authors": "Arne Storjohann",
"title": "Deterministic computation of the Frobenius form",
"url": "https://doi.org/10.1109/SFCS.2001.959911",
"usage": "Classical deterministic polynomial-time form and transformation subroutine."
},
{
"authors": "Josep Ferrer, David Mingueza, M. Eulalia Montoro",
"title": "Determinant of any matrix that belongs to Z(J)",
"url": "https://www.maia.ub.edu/~sombra/publications/EACA2014/2014_EACA_Conference_Proceedings.pdf#page=113",
"usage": "Classical Jordan/Weyr centralizer determinant formula, Theorem 4.3."
}
]
}
106 changes: 106 additions & 0 deletions research/pencil-determinant-image/TASK.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,106 @@
{
"schema_version": 1,
"task_id": "formal-interface-lemma",
"priority_revision": 7,
"base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf",
"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": "Exact stabilizer determinant image and deterministic fixed-field extraction for square matrix pencils with an invertible slice.",
"scope_change_reason": "Take David Ganz atlas A030 invertible-slice subclass as an original mathematical side result; no Lean formalization or predecessor audit.",
"bottleneck_link": "Scoped tensor-automorphism side result; no selected supplier obligation or new kappa is claimed.",
"budget_minutes": 60,
"stop_rule": "Stop at the first verified exact image formula and independently checkable proof, or at a precise failed implication.",
"outcome": "completed",
"evidence": "README.md proof and standalone verify.py literal tensor census and source-bound generated receipt.",
"author": "Nick Petalas",
"ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
"open_questions": [
{
"question": "Extend to regular pencils without an invertible K-rational slice.",
"why_it_matters": "Removes the invertible-slice restriction on the extraction theorem.",
"first_step": "Use binary homogeneous elementary divisors to replace the B_R inverse normalization.",
"blocked_by": "No coordinate-independent determinant-coset assembly is proved here."
},
{
"question": "Extend to singular Kronecker blocks and rectangular pencils.",
"why_it_matters": "Would cover the remaining matrix-pencil tensor classes.",
"first_step": "Compute determinant characters of a single minimal-index block and its multiplicity space.",
"blocked_by": "Interactions between block types and slice transformations."
}
],
"environment": {
"python": "3.12.15",
"platform": "macOS-27.0.1-arm64-arm-64bit",
"dependencies": "CPython standard library only"
}
}
Loading