Skip to content

Lift prime-field recovery certificates to extension-field algebras (no κ) #7473

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

Open
petalas wants to merge 1 commit into
base: main
Choose a base branch
from
+954 −0
Open

Lift prime-field recovery certificates to extension-field algebras (no κ) #7473

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
141 changes: 141 additions & 0 deletions research/commutative-scalar-ascent/PROOF.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,141 @@
# Scalar ascent of a recovered commutative multiplication tensor

This constructive proof and certificate adapter were produced by Nick Petalas.
Apache-2.0. Restriction of scalars and normalization of a unital isotope are
classical. The contribution here is the explicit bridge between the existing
prime-field recovery interface and a general extension-field certificate.
No literature-priority claim is made for the underlying algebraic facts.

## Proposition and conventions

Let K/F be a finite field extension of degree d. The fields themselves need
not be finite. Let t:U x V -> Z be K-bilinear, with all three K-dimensions
equal to n > 0. Matrices act on column vectors. Restriction uses one fixed
F-basis of K and the same coordinate packing in each of U,V,Z.

The following conditions are equivalent.

1. t is K-isotopic to multiplication in a commutative associative unital
K-algebra of dimension n.
2. Res(t) is F-isotopic to multiplication in a commutative associative
unital F-algebra of dimension dn.

More precisely, suppose a certificate for condition 2 supplies an F-algebra
B, its multiplication table, and invertible F-linear maps

Res(t)(P a, Q b) = S(ab).

The maps P,Q,S need not be K-linear and B is not initially supplied with a
K-vector-space structure. Let e be its unit, and pack the vectors P e and Q e
as u in U and v in V. Define K-linear slices

R_v(x) = t(x,v), L_u(y) = t(u,y).

Both slices are invertible. The explicit K-bilinear product on Z

mu(x,y) = t(R_v^(-1) x, L_u^(-1) y)

is commutative, associative and unital, with unit t(u,v). Its K-table and
the three maps R_v^(-1), L_u^(-1), I_Z form a certificate for condition 1.
This construction requires no decomposition of the K-nucleus and no
Frobenius height computation.

## Proof

Condition 1 implies condition 2 by restricting every map and algebra operation
to F. For the converse, apply the given isotopy with b=e and with a=e:

R_v P = S, L_u Q = S.

Thus the restricted F-linear maps R_v and L_u are invertible. They are also
K-linear by the stipulated K-bilinearity of t. Their inverses are K-linear:
if A is a K-linear bijection, A(A^(-1)(lambda z)) = lambda z =
A(lambda A^(-1)z), and injectivity equates the two inverse values.

Now write x=S a and y=S b as F-vectors. The two displayed slice identities
give

mu(S a,S b) = t(P a,Q b) = S(ab).

Consequently S is an F-algebra isomorphism from B to (Z,mu). Commutativity,
associativity and the unit S e are identities of the product and therefore
hold for every vector of Z, regardless of scalar presentation. The product
is K-bilinear by its formula. These facts make (Z,mu) a commutative
associative unital K-algebra. Finally S e=t(Pe,Qe)=t(u,v), and the formula
for mu is exactly the claimed K-isotopy. This proves the proposition.

In particular, the K-action on the recovered algebra could also be described
by a conjugated F-linear action through S. The adapter need not discover or
diagonalize that action. It uses the output coordinates already present in t.

## Recovering the unit and constructing the certificate

The source interface returns a multiplication table and P,Q,S, without a
separate unit vector. Solve the linear equations

sum_i e_i B[i,j,k] = delta[j,k]

for e. A unital algebra has a unique solution, since two left identities in
a commutative algebra agree by multiplying them. The reference also checks
both unit identities, associativity, commutativity, every source basis
isotopy equality and invertibility of the three supplied maps. Invalid
certificates are rejected before ascent. This is certificate consumption,
not a call to an existing recognizer or a replay of its scientific suite.

Pack Pe,Qe into K-vectors using the fixed field basis. Compute the slices,
invert them over K and evaluate the product on all pairs of K-basis vectors.
The reference returns `table`, `unit`, `U`, `V`, `W`, with W the identity.
It checks the returned K-certificate as well. For a symbolic recognizer,
the forward implication and this adapter show that applying the general
F-recognizer to Res(t) is a necessary-and-sufficient K-recognition procedure.
The predecessor recognition theorem remains a cited premise.

The procedure is polynomial in n and d for a supplied exact field interface.
Dense source certificate validation costs at most O((dn)^5) F-operations
and the displayed slice/table construction at most O(n^5) K-operations
using literal contractions. These are loose operation bounds, not a speed
claim, bit-complexity bound or bound on constructing the field. The reference
has hard finite capacities listed in README.md.

## Two hypotheses that cannot be silently dropped

K-bilinearity is essential. With F=F2, K=F4, the map t(x,y)=x^2 y is
F-bilinear and F-isotopic to field multiplication, since squaring is an
invertible F-linear map. It is not K-linear in its first argument:
t(a,1)=a^2 differs from a t(1,1)=a for a outside F2. Composing with
invertible K-linear factor maps cannot change that failure of K-bilinearity.
Thus an arbitrary F-tensor with a guessed K-coordinate grouping is outside
the proposition.

The general commutative recognizer is required. It cannot be replaced by the
prime-field local characteristic-power truncated-polynomial recognizer.
For example, K=F4, n=1, t is K multiplication. Res(t) is multiplication in
the reduced F2-algebra F4 of dimension two. The only dimension-two nonempty
truncated model over F2 is F2[x]/x^2, which has a nonzero square-zero element.
These algebras are not isomorphic. They are not isotopic either: for unital
commutative associative algebras, any isotopy normalizes to an isomorphism
by multiplying its output by the inverse of the images of the two units.
Equivalently, field multiplication has every nonzero slice invertible,
whereas multiplication by x in the dual numbers is a nonzero singular slice.
The reference checks this reduced/nilpotent boundary directly.

This proposition does not transfer a prescribed algebra-class label, a
special-linear determinant label or an automorphism count through restriction.
Those tasks require their own scalar-aware arguments.

## Relationship to prior recognition

Ali Romman's #5540 supplies general prime-field recovery, including
nonreduced algebras, and asks for an extension-field input layer. Its
necessity/sufficiency theorem and source implementation are not rechecked.
Ali Romman's #5637 implements a direct extension-field recognizer for local
characteristic-power truncated polynomial algebras. Its README explicitly
leaves general residue fields and products outside that implementation.

Nick Petalas's older #6464 already gives a general recognition theorem over
any supplied exact field, using a different cyclic-module construction.
No claim to extend that theorem is made here and its construction is not
used. The new artifact is a scalar-restriction certificate adapter. It
allows the existing prime-field recovery contract to supply K-linear output
without implementing nucleus decomposition over K. Neither its proof nor
its implementation imports a predecessor executable.
170 changes: 170 additions & 0 deletions research/commutative-scalar-ascent/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,170 @@
# Lift recovered prime-field tensors to extension-field algebras

This constructive proof and certificate adapter were produced by Nick Petalas.
Apache-2.0.

Let K/F be a finite field extension and t a K-bilinear square tensor. Then t
is K-isotopic to multiplication in a commutative associative unital K-algebra
if and only if its restriction to F is F-isotopic to multiplication in a
commutative associative unital F-algebra. The explicit certificate bridge is

```text
source unit e; u=P e; v=Q e
R_v(x)=t(x,v); L_u(y)=t(u,y)
mu(x,y)=t(R_v^(-1)x,L_u^(-1)y)
K-certificate: table(mu), unit=t(u,v), U=R_v^(-1), V=L_u^(-1), W=I
```

The source maps P,Q,S can be arbitrary F-linear maps. They do not need to be
K-linear. Both displayed slices are invertible K-linear maps, and mu is the
required K-algebra product. [PROOF.md](PROOF.md) proves the quantified
statement and explains both necessary boundary restrictions.

Claim type: scoped constructive proof with exact finite corroboration.
The contribution is the explicit scalar-restriction certificate adapter and
its bounded implementation. It is not a new general recognition theorem.
No kappa, supplier admission or selected-frontier change is claimed.

## Before and after

Ali Romman's [#5540](https://github.com/CrocSwap/integer-mult-bounds/pull/5540)
recovers arbitrary commutative unital multiplication from prime-field tensors
and leaves an extension-field input layer open. The adapter consumes that
certificate shape and returns a K-table and K-linear factor maps without
implementing an extension-field nucleus decomposition. It handles products,
non-Gorenstein algebras and nonsplit residue fields under the same general
commutative contract.

Ali Romman's [#5637](https://github.com/CrocSwap/integer-mult-bounds/pull/5637)
already supplies a direct extension-field implementation for the local
characteristic-power truncated-polynomial class. Nick Petalas's older
[#6464](https://github.com/CrocSwap/integer-mult-bounds/pull/6464) already proves
general recognition over any supplied exact field. Those results are credited
premises/background, not replay targets or claimed new coverage. This package
uses neither predecessor implementation. It supplies the explicit restriction
bridge to the existing prime-field interface.

Restriction does not preserve every class label: Res(F4) is a field over F2,
whereas F2[x]/x^2 is not. The adapter must consume a general commutative
recovery certificate. Nor can an arbitrary F-bilinear tensor be passed off as
a K-bilinear input. The semilinear map x^2 y over F4 is a boundary witness.

## Reproduce

From the repository root, CPython 3.12 and the standard library suffice:

```sh
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/commutative-scalar-ascent/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/commutative-scalar-ascent/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/commutative-scalar-ascent
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/commutative-scalar-ascent --check-source-history
```

Another CPython 3.12 path can replace the recorded interpreter. The direct
marker is `PASS_COMMUTATIVE_SCALAR_ASCENT`. The program emits a generated
receipt binding all eight package files by SHA256 and the complete ordered
fixture output by a deterministic digest. It writes nothing. Both registered
commands run the same checks with runtime requirements enabled under `-O`.

`ascent.py` exports `ascend(tensor, certificate, field)`. Tensor entries are
`t[i][j][k]`. The input certificate contains `table`, `U`, `V`, `W` in the
restricted prime-field coordinates, with each original K-coordinate expanded
into consecutive low-to-high polynomial coefficients. Its maps use columns
as basis images and satisfy `Res(t)(U a,V b)=W table(a,b)`. The adapter checks
the supplied certificate and returns the corresponding K-certificate plus
`unit`. Invalid certificates raise `ValueError`. It never invokes a recognizer.

## Evidence

Local normal and optimized replay passes 78 constructed certificates, 684
K-basis products, 75 non-K-linear recovery bases, 16,930 field-law triples,
ten rejecting controls and two boundary witnesses. Both registered checks
and the package metadata runner pass on CPython 3.12.15. Generated normal
and optimized reports agree exactly.

The verifier constructs its own tensors and source certificates. It exercises
F4, F8, F9 and F25, nilpotent and non-Gorenstein algebras, direct products,
nonsplit quadratic residue fields, and dual-number extensions of those
nonsplit fields. Three deterministic independent input/output presentations
are used for each algebra. Prime-field recovery bases are changed separately,
including bases that do not commute with multiplication by the field
coordinate. Returned tables and units are compared with the original
fixture's explicit output-space algebra, independently of the adapter's
slice formula.

It also checks every field-law triple in the four finite arithmetic domains.
Named controls reject singular maps, an invertible but wrong output map,
noncanonical entries, missing keys, unsupported fields, wrong dimensions,
nonassociative multiplication and noncommutative multiplication. Two explicit
boundary witnesses cover K-bilinearity and the class-recognizer restriction.
The emitted receipt enumerates all counts. These finite checks corroborate
the written proof; they are not a complete tensor census or a replay of
another contributor's numbers.

## Scope, limits and credit

This is a changed `formal-interface-lemma` scope at canonical main
`e54523517d0f03e58352e647c403a5af3e525a57`, priority revision 8. It is an
algebraic interface side result, with no proof-assistant acceptance. The
source-binding baseline command passed for selected #7000. No selected
scientific replay was run. Historical source text and the task card are
pinned as provenance in SOURCES.json, rather than imported at runtime.

The reference accepts the explicitly listed polynomial fields in algebra.py,
with q at most 25 and restricted dimension dn at most 12. These are executable
capacities, not bounds on the theorem. It consumes a certificate; it does not
implement a new end-to-end recognizer or classify the recovered K-algebra.
No special-linear label, automorphism count, rational bit-complexity bound or
runtime speedup is claimed. There is no native implementation, physical
coefficient preparation, dirty restoration program, paid caller, compiler
closure, precision/tape admission or complete multiplication theorem. All
five selected assumptions remain. Independent human and formal proof-kernel
review are unclaimed.

Credit Ali Romman for #5540's question and recovery interface, #5525 and
#5637; apoursh for #5502; Nick Petalas for #5252; and David Ganz and the
retained tensor/algebra lineage. Restriction of scalars, exact elimination
and unital isotope normalization are classical. No predecessor code is copied.
The new bridge, bounded reference, proof and fixture checks were produced by
Nick Petalas. The #6464 cyclic-module construction is background and is not
used as a step.

Live PR titles/bodies, recent handoffs, batch reservations, merged searches
and all-main README searches were checked before the
[advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19572847).
The cached search reports its own coverage limits, including omitted sparse
notes. Search absence does not prove novelty. Related open work is recorded
in the PR body; no competing result is audited here.

## Open next questions

1. Can a public caller connect an actual #5540 recovery certificate to this
adapter with a general exact finite-field input contract? Start with one
source-owned output certificate and its precise coordinate basis. This
package supplies a bounded adapter and new fixtures, not that integration.
2. Which prescribed K-algebra class or determinant labels can be reconstructed
from the restricted F-algebra together with its embedded scalar action?
Start with one nonsplit local component. Ignoring that scalar action is
invalid; no classification or special-linear label transfer is supplied.
3. Can one recovered K-table be used in an affordable native caller? First
charge all coefficient maps, workspace, returns and restoration. No such
physical cost contract is supplied by recognition or this bridge.

## Verifier engineering bounds

Every dimension is bounded by 12 and every supported field has at most 25
values. All loops range over those explicit finite domains or fixed fixture
lists. There is no recursion, subprocess, runtime code generation or write.
Functions remain below sixty physical lines. Internal arithmetic helpers trust
representations validated at the public tensor, matrix and certificate
boundaries. Runtime requirements use explicit exceptions and remain enabled
under optimization. Warning-strict normal/optimized execution and syntax
inspection provide diagnostics; no separate static analyzer is claimed.

Power of Ten rule 3 deviation: CPython allocates integers, lists and tuples
throughout exact arithmetic. Live tensors have at most 12^3 coefficients,
linear systems at most 12^2 rows and 13 columns, and field tables at most
25^2 entries. Fixtures execute sequentially. Revisit these bounds before
accepting larger dimensions or a production caller. Rules 8 and 9 retain
ordinary Python module loading from two fixed siblings and a fixed list of
negative-control lambdas; no arbitrary imported target or callback is accepted.
30 changes: 30 additions & 0 deletions research/commutative-scalar-ascent/SOURCES.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
{
"schema_version": 1,
"base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
"files": [
{
"path": "certificates/selected-result.json",
"usage": "provenance",
"git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8",
"sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1"
},
{
"path": "docs/research/agent-task-catalog.json",
"usage": "provenance",
"git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
"sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
},
{
"path": "research/extension-field-tensor-recognition/README.md",
"usage": "provenance",
"git_blob": "d0c74a3c49fba38e389b6ef8c714882bdd0bf797",
"sha256": "4b297e57762284c69c7202ee183f43c5fe170fbc9104e4ff0cce3faa345c7c97"
},
{
"path": "research/nonreduced-tensor-recognition/README.md",
"usage": "provenance",
"git_blob": "826c6b010725d98b6ca6599a748c4179264140e9",
"sha256": "2eaed94a9f12ad7b6bb7253b14bff95b86549b3e320f0e91fa4e35c0025536de"
}
]
}
Loading
Loading