Complete raw finite-field pencil SL recognition and transport

research/raw-pencil-sl-transport/EVIDENCE.md

@@ -0,0 +1,95 @@
+# Validation and limits
+
+The base is canonical main df0137efd35e11b4445734bf612bdd4c7ebc330c.
+Priority revision 7 and selected conditional kappa 0.00310045 remain unchanged.
+The eleven source inputs are exact retained bytes from the two consumed
+packages. SOURCES.json gives every blob, SHA256 and retention commit.
+
+## Complete finite domains
+
+The normal Python 3.14.7 checks cover every one of 81,244 raw pencils in
+eleven domains. Independent elementary-transvection traversals give exactly
+76 SL orbits in total across those separate domains. Every raw input has
+its label compared with that partition and every returned map has all three
+determinants and both coefficient matrices checked separately.
+
+| Field | Matrix shapes | Raw pencils | SL orbits |
+| --- | --- | ---: | ---: |
+| F2 | 2x2, 2x3, 3x2 | 8,448 | 28 |
+| F3 | 2x2, 1x1, 1x2, 2x1 | 6,732 | 24 |
+| F4 | 2x2, 1x1, 1x2, 2x1 | 66,064 | 24 |
+
+The 65,536 F4 two-by-two pencils alone give twelve SL orbits. The normal
+extension phase took about 439 seconds in this session with at most four
+process workers. This is verification runtime, not an algorithm benchmark.
+
+The larger checks have 24 fixtures over F2,F3,F4,F9, with 23 arbitrary-basis
+raw-to-raw transports. They include degree-four primaries, length four,
+index six, multiplicity four, a seventeen-row zero pencil, and three regular
+full-projective-line families. Eleven square fixture pencils have no
+invertible rational slice; three of these are regular. There are 29 malformed,
+inequivalent-input and singular-map controls. The public transporter also
+passes an identity and a nontrivial raw-to-raw endpoint.
+
+The norm phase checks 112 nonzero targets over all declared field/degree
+pairs, with degrees one through eight. It uses 648 sampled residues. Separate
+multiplication determinants check all returned norms and 336 lifts at lengths
+one, two and four. Three invalid norm problems reject. The supplied-character
+comparison covers all 180 determinant triples in fifteen declared model GL
+orbits and agrees exactly on the SL partition.
+
+An initial proposed negative control from diag(s,t) over F3 was equivalent,
+not a counterexample. It was replaced by the 1x2 pencils with stacked
+coefficient determinants one and two. That independent determinant invariant
+proves their inequivalence under SL1 x SL2 x SL2. No classification formula
+was changed to fit that mistaken fixture expectation.
+
+## Final registered replay
+
+All five final commands pass on Python 3.12.14, followed by
+PASS_REGISTERED_RESEARCH_PACKAGE. Their declared caps are 180,600,300,60,60
+seconds, for a total of 1,200 seconds. The final verifier adds the nontrivial
+public-transporter control and streams irreducible-fixture candidates without
+materializing all candidates. The executable classifier is unchanged from the
+normal run. RESULT.json records both normal and registered receipts.
+
+## Sealed exported replay and publication checks
+
+All five phases pass from the official committed export of scientific commit
+3afe93780f111c6368badd47394ce761d4421317. The export has no Git directory.
+Python 3.12.14 runs with -I -O -B and an empty executable PATH. All 21 files,
+including the export manifest, keep their bytes and permissions after the
+read-only run. An actual changed source input fails authentication before
+replay. The source is restored before the full run. RESULT.json records this
+receipt. The official committed-byte and export integrity checks pass for
+all twenty package files.
+
+The final overlap search covers all 7,676 main notes, 392 open PRs and 5,043
+Discussion records, with separate literal terms and a cached-body scan. Its
+last remote refresh is 2026-10-26T08:23:49Z. It finds no competing raw-SL or
+residue-norm claim within that coverage. Closed unretained work and unpublished
+work are outside this search. Both consumed predecessors are released.
+Canonical main was fetched again at 2026-10-26T08:35Z and has the same commit.
+The final commit adds receipts and coordination metadata only; executable
+sources and the proof are unchanged from the sealed replay.
+
+## Hosted CI and omitted obligations
+
+The nine earlier contributions in this session have completed hosted plan
+jobs that fail the same two CurrentCiNavigationTests subcases: review and
+source_manifest. Their package replay jobs are skipped. The inspected logs
+include [the exact PR5707 job](https://github.com/CrocSwap/integer-mult-bounds/actions/runs/40287155528/job/121453417199).
+The shared main documentation defect already has
+[PR #5659](https://github.com/CrocSwap/integer-mult-bounds/pull/5659) and
+[PR #5703](https://github.com/CrocSwap/integer-mult-bounds/pull/5703).
+This package does not duplicate or merge those repairs. Its own hosted status
+must be read separately; no hosted success is inferred from local success.
+
+No complete physical caller, native preparation/routing/storage/precision
+invoice, selected-frontier replay, independent human review or proof-kernel
+acceptance ran. The shallow checkout cannot establish the full-history
+publication preflight; exact source bytes and immediate retained-source
+ancestry are checked. The norm witness is exact Las Vegas sampling, with
+expected polynomial cost for fixed field and no deterministic worst-case
+runtime claim. Finite tests do not by themselves establish the written
+unbounded theorem. No new kappa or physical speedup is claimed.

research/raw-pencil-sl-transport/PROOF.md

@@ -0,0 +1,209 @@
+# Raw finite-field pencil special-linear recognition
+
+Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0.
+
+## Claim and source boundary
+
+Fix a supplied finite field K=F_q with one common element encoding. Let
+m,n>0. A tensor is any ordered pair X=(A,B) of m-by-n matrices. The action is
+
+```text
+(P,Q,S).X = (P(s11 A+s12 B)Q^T, P(s21 A+s22 B)Q^T).
+```
+
+This package gives a deterministic complete label for the orbits of
+SL_m(K) x SL_n(K) x SL_2(K), a fixed representative for each label, and
+literal determinant-one maps to that representative. It also gives a map
+between two equivalent raw inputs. The decision has polynomial cost in the
+factor dimensions for fixed q. Map construction has expected polynomial
+cost, with exact checked residue norms. No dimension, index, primary degree,
+length or multiplicity cap is imposed by the implementation.
+
+The field is common to both inputs. Field automorphisms, changes between
+unrelated field encodings and tensors with more than two slices are outside
+the claim. Zero pencils, linearly dependent slices, rectangular shapes,
+zero minimal indices and pencils with no invertible rational slice are in
+scope. The complete kappa calculation does not change.
+
+PR5692 supplies raw strict Kronecker decomposition and its actual maps.
+PR5689 supplies the complete fixed-slice determinant subgroup, including
+all off-diagonal mixing. Those are credited prerequisites, not new theorems
+here. This package supplies their raw SL interface, basis/order determinant
+handling, an executable unbounded-degree norm witness, and independent
+finite SL-orbit checks. The bounded character code is only a comparison
+oracle. It is neither patched nor used as an unbounded implementation.
+
+## Strict canonical coordinates and every determinant
+
+The retained extractor returns blocks, R and Q with
+
+```text
+A Q = R A0,       B Q = R B0.
+```
+
+Order its individual blocks by their exact type records. Apply the actual
+row and column block permutations E and F. Then
+
+```text
+g=(E R^-1, F Q^T, I2)
+```
+
+maps the raw pencil to the sorted block model C. Thus det(g_row)=det(E)/det(R)
+and det(g_col)=det(F)det(Q). The program keeps these matrices and checks both
+coefficient equations. It does not discard signs or identify equal block
+orders without their actual maps.
+
+The raw extractor writes finite regular blocks as `(Comp(f^ell),I)` and
+infinity as `(I,Comp(X^ell))`. The supplied-character source uses the opposite
+slice convention. Exchanging both coefficient equations does not change
+the fixed-slice stabilizer. The subgroup below therefore applies directly.
+Every slice action in the new algorithm is applied to the actual matrices;
+no implicit slice swap or uncharged determinant correction occurs.
+
+## Complete fixed-slice character subgroup
+
+For a sorted model C, let H(C) be the image in (K*)^2 of its row/column
+stabilizer with the slices fixed. The source theorem gives the subgroup
+generated by the following pairs, for every u in K*:
+
+```text
+right index e:       (u^e, u^(-e-1)),
+left index e:        (u^(-e-1), u^e),
+regular length ell:  (u^ell, u^-ell).
+```
+
+This includes index zero. The regular residue degree and repeated-copy
+count do not replace ell. Repeated identical generators may be omitted.
+The source proof uses the full Hom algebra, not a block-diagonal assumption.
+Distinct singular types and singular/regular Hom maps are triangular in
+an appropriate order. For a regular primary, the residue multiplicity map
+of exact length ell appears on ell filtration layers. Its determinant is
+Norm(det D)^ell. Off-diagonal/radical maps add no determinant factor.
+This proves the upper bound. Varying one block or one multiplicity coordinate
+attains each displayed generator, so the bound is exact.
+
+The program closes these generators in the finite group (K*)^2 by breadth
+first search. It stores a generator path for each element. There are at
+most (q-1)^2 elements. This is an exact finite group calculation, not a scan
+of the large matrix stabilizer.
+
+## Complete raw SL label
+
+Enumerate every S in SL_2(K). For each, apply S to X, compute its sorted
+strict model C_S and a strict map g_S. The full map from X is
+`(g_S_row,g_S_col,S)`. Let d_S be its pair of row and column determinants.
+Let l_S be the least pair in the coset d_S H(C_S), using the fixed integer
+encoding of K elements. The label is the least pair
+
+```text
+(sorted block records of C_S, l_S)
+```
+
+over all S, together with m,n. The associated representative is C_S with
+its first row multiplied by l_S[0]^-1 and its first column multiplied by
+l_S[1]^-1. Positive m,n make these diagonal maps well defined. This label
+is relative to the declared common field encoding.
+
+First, it is independent of the extractor's coordinate choices. Two strict
+maps to the same model differ by a fixed-slice stabilizer. Their determinant
+pairs differ by H(C_S), so their cosets and labels agree.
+
+Next, suppose Y=(U,V,T).X with det U=det V=det T=1. For every slice action
+S on Y, the corresponding action on X is ST. The row/column maps U,V have
+determinant one. Hence the sets of strict types and determinant cosets are
+the same as S ranges over SL_2. Their least labels are equal. This proves
+invariance under the entire product group, including slice actions.
+
+Conversely, choose the winning S and d=d_S. Since l is in dH, put
+h=l/d componentwise. The stored path supplies a literal fixed-slice
+stabilizer (H_row,H_col) with determinants h. Let D_row,D_col have first
+diagonal entries l[0]^-1,l[1]^-1 and all other entries one. Then
+
+```text
+(D_row H_row g_row, D_col H_col g_col, S)
+```
+
+maps X to the stated representative. Its two determinant products are
+l^-1 h d=1, and det S=1. Thus equal labels give SL maps to one identical
+representative and imply equivalence. The label is complete.
+
+If w_X and w_Y map X and Y to that representative, the transporter from
+X to Y is `w_Y^-1 w_X`, component by component. The program checks all three
+determinants and both literal coefficient matrices. Different labels return
+no transporter. This is a decision for all raw pencils in the stated class,
+not a promised-model recognition test.
+
+## Exact norm witnesses without a degree cap
+
+For a finite primary f of degree d, choose a uniform residue polynomial a
+with d coefficients in K. For nonzero a, compute
+
+```text
+N(a)=a^((q^d-1)/(q-1)) mod f.
+```
+
+This is an element of K. Accept exactly when it is the requested nonzero u.
+The norm map on the cyclic multiplicative group of F_(q^d) is onto K*.
+Each nonzero target has (q^d-1)/(q-1) preimages among all q^d sampled residues.
+The success probability is at least 1/q. Independent uniform trials therefore
+terminate almost surely with expected trial count at most q. The result is
+checked exactly; randomness affects runtime and the selected witness, not
+correctness, the orbit label or the representative.
+
+On a length-ell block, use P=a(Comp(f^ell)) and Q=P^-T. The residue unit
+lifts to a unit, commutes with the companion matrix and has determinant
+N(a)^ell=u^ell. Infinity uses a constant unit u. Right and left blocks use
+the literal scalar maps from the displayed character formulas, with empty
+local factors allowed at index zero. Insert each generator in the full
+block coordinates, multiply along the stored path, and check the full
+fixed-slice identity. There is no enumeration of q^d residues in this code.
+
+The default uses SystemRandom. Reproducible verification uses specified
+Random seeds. The expected-time theorem assumes independent uniform draws;
+it is not a deterministic worst-case bound for a supplied random stream.
+
+## Positive preparation and caller limits
+
+There are q(q^2-1) special-linear slice actions. The code tests fewer than
+q^4 candidate two-by-two matrices and invokes the retained polynomial raw
+extractor on their transformed coefficients. It keeps a per-input cache of
+identical transformed pencils only. Sorting, all row/column maps, determinant
+calculations, character closure and all coefficient checks are paid work.
+For fixed q their counts and workspace are polynomial in m+n. No discrete
+logarithm or unpriced large stabilizer oracle is used.
+
+A norm trial uses polynomial arithmetic modulo f and an exponent with
+O(d log q) bits. Verification of irreducibility uses the retained exact
+factorization routine. Lifting to length ell and multiplying the full maps
+has polynomial matrix cost. Each character path has fewer than (q-1)^2
+steps. The witness therefore has expected polynomial preparation cost for
+fixed q. The implementation builds explicit finite-field operation tables;
+no complexity polynomial in log q is claimed. The polynomial exponent and
+large-field constants are not optimized.
+
+This preparation is an algebraic tool for the tensor-atlas interface. A
+multiplication mechanism still needs native realizations, a producer and
+consumer, physical moves, dirty restoration, storage, precision, repeated
+preparation and a complete paid recursive bill. These costs remain unknown,
+not zero. No physical caller, supplier admission, kappa improvement or
+practical multiplication speedup follows from this package.
+
+## Evidence and attribution
+
+The verifier constructs independent complete small SL-orbit partitions
+using elementary transvections on all three tensor factors. It compares
+labels on every raw input and checks every returned map by a separate
+coefficient sum and small determinant formula. Larger fixtures include
+extension fields, degree-four primaries, length four, index six, multiplicity
+four, dimension seventeen, zero pencils and full projective-line pencils
+with no invertible rational slice. Exact norm tests extend through degree
+eight and length-four lifts. The frozen supplied-model program supplies a
+separate comparison for its own bounded character domain.
+
+These are exact finite tests plus a written all-input argument. Independent
+human review, proof-kernel acceptance and a production physical bill remain
+open. Credit PR5692, PR5689, Nick Petalas PR5250, apoursh PR5672, Ali Romman
+PR5683, David Ganz A030/A026/A029, and the classical Kronecker, module,
+centralizer and finite-field norm results retained in those sources. Original
+notices remain byte-exact under vendor/. No global literature priority is
+claimed. No subagents were used.

research/raw-pencil-sl-transport/README.md

@@ -0,0 +1,76 @@
+# Raw pencil special-linear recognition and transport
+
+This closes the raw-input boundary for finite-field two-slice tensors.
+Given any two m-by-n coefficient matrices over one common finite field,
+with m,n>0, it returns a complete SL_m x SL_n x SL_2 orbit label, a fixed
+representative and a literal determinant-one map to it. Two equivalent raw
+inputs receive an explicit transporter. No supplied block model or invertible
+rational slice is required. The complete kappa calculation is unchanged.
+
+The [proof](PROOF.md) gives the complete-orbit argument and positive costs.
+[sl.py](sl.py) contains the implementation. [RESULT.json](RESULT.json) and
+[EVIDENCE.md](EVIDENCE.md) state the exact checks and limits.
+[SOURCES.json](SOURCES.json) pins all eleven retained source files.
+
+The deterministic decision enumerates SL2 slice actions, extracts the raw
+strict model, and keeps its actual row/column determinants modulo the complete
+fixed-slice character subgroup. Exact general-degree norm witnesses remove
+the degree-three limit of the supplied-model executable. Map construction
+has expected polynomial cost for fixed field under uniform sampling; this
+is not a deterministic worst-case runtime guarantee.
+
+The implementation accepts all finite dimensions, minimal indices, primary
+degrees, lengths and multiplicities. This includes zero pencils, zero-index
+singular blocks, infinity, nonsplit factors and no-invertible-slice pencils.
+The common field encoding is part of the interface. Field isomorphisms and
+tensors with more than two slices are outside the claim.
+
+## Reproduce
+
+Use Python 3.12 and its standard library:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/raw-pencil-sl-transport
+```
+
+The five phases report `PASS_RAW_PENCIL_SL_SMALL`,
+`PASS_RAW_PENCIL_SL_EXTENSION`, `PASS_RAW_PENCIL_SL_FIXTURES`,
+`PASS_RAW_PENCIL_SL_NORMS`, and `PASS_RAW_PENCIL_SL_CHARACTERS`.
+The runner then reports `PASS_REGISTERED_RESEARCH_PACKAGE`.
+The declared caps sum to 1,200 seconds. The two exhaustive phases use at
+most four process workers and write no package data. VERIFY.json also gives
+the exact commands for a Git-free export.
+
+`analyze` gives the deterministic label and representative. `canonicalize`
+also gives the three determinant-one maps. `transporter` gives maps from the
+first input to the second, or None for different orbits. The action convention
+and all input domains are stated in PROOF.md.
+
+## Credit and scope
+
+Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. No subagents.
+The consumed packages use the same assistant family; this is not independent
+human review. The new finite-orbit oracle does not use their classification
+or character formulas.
+
+[PR #5692](https://github.com/CrocSwap/integer-mult-bounds/pull/5692), head
+e34ae992744db135b9d4e378bfe26fd31fb82ad7, supplies raw strict extraction.
+[PR #5689](https://github.com/CrocSwap/integer-mult-bounds/pull/5689), head
+29172b129a7bb4dbbb3b42ac128fa32ffec1f93b, supplies complete fixed-slice
+characters and the norm construction argument. The latter's bounded code
+is a separate comparison oracle. All sources and notices remain byte-exact.
+
+Credit also Nick Petalas's
+[PR #5250](https://github.com/CrocSwap/integer-mult-bounds/pull/5250),
+apoursh's [PR #5672](https://github.com/CrocSwap/integer-mult-bounds/pull/5672),
+Ali Romman's [PR #5683](https://github.com/CrocSwap/integer-mult-bounds/pull/5683),
+David Ganz's tensor atlas and the classical Kronecker/module/centralizer/norm
+lineage retained in those sources. Global literature priority is unclaimed.
+
+## Open next questions
+
+- Name a concrete native producer and consumer that uses this admissibility
+  tool, then price all physical preparation, routes, dirty restoration,
+  storage, precision and recursive work. Those costs are unknown here.
+- Give a deterministic general-degree residue norm solver with its actual
+  cost. The present exact witness has expected polynomial runtime.