From 8ab280c8a3ef0544f13ff23a1c69df4757cd4900 Mon Sep 17 00:00:00 2001 From: ssafwann Date: Fri, 23 Oct 2026 22:54:31 +0800 Subject: [PATCH] Prove nilpotent Schur residual extension and fixed-H weights --- research/schur-nilpotent-extension/README.md | 354 +++++++++++++ .../schur-nilpotent-extension/SOURCES.json | 60 +++ research/schur-nilpotent-extension/TASK.json | 235 +++++++++ .../schur-nilpotent-extension/VERIFY.json | 34 ++ research/schur-nilpotent-extension/verify.py | 487 ++++++++++++++++++ 5 files changed, 1170 insertions(+) create mode 100644 research/schur-nilpotent-extension/README.md create mode 100644 research/schur-nilpotent-extension/SOURCES.json create mode 100644 research/schur-nilpotent-extension/TASK.json create mode 100644 research/schur-nilpotent-extension/VERIFY.json create mode 100644 research/schur-nilpotent-extension/verify.py diff --git a/research/schur-nilpotent-extension/README.md b/research/schur-nilpotent-extension/README.md new file mode 100644 index 0000000000..1e738614a4 --- /dev/null +++ b/research/schur-nilpotent-extension/README.md @@ -0,0 +1,354 @@ +# Nilpotent identity-block Schur deletion: the whole residual and its weight + +This is a written algebraic side result with bounded exact corroboration, +prepared for ssafwann with substantial OpenAI Codex (gpt-6-astra) assistance, +one agent; Apache-2.0. It answers the whole-residual extension handoff in +[PR5256](https://github.com/CrocSwap/integer-mult-bounds/pull/5256) for nilpotent +compressed products. That pending PR is motivation, not a theorem premise. +Independent human and formal proof-kernel review are unclaimed. + +**Result.** Fix a commuting idempotent pair and its four joint-sector dimensions. +Among identity-block deletions with a specified nilpotent matrix H and maximal +Schur-commutator rank, the entire ordered residual pair has one simultaneous +conjugacy orbit. We give an explicit representative over any field. In odd +characteristic its central operator has one chain of length k and one of length +k+1 for every H Jordan block of length k, plus specified scalar summands. Over +finite fields we count exactly the splits and complete headers in this fixed-H +event. This is not the unconditional mass of the residual orbit. + +The generic factor equivalence and stabilizer method are predecessor results; +the contribution is their application to this Schur family, the explicit +complementary attachments, and the resulting whole-residual Jordan law. This +does not reopen the earlier minimum-dimension problem or scalar state census. +No selected-frontier file changes: selected conditional κ remains 0.00302015. +Physical header selection/emission, reads, owned/borrowed state, dirty restoration, +precision, storage, stock, dispatch and the complete consumer bill remain +unknown, not zero. + +## Contract and statement + +Let F be any field, U=F^d with d>=1, and P0,Q0 commuting idempotents on V. +Write V as its ordered joint eigenspaces V00,V10,V01,V11, of dimensions r_j. +A split is i:U->V and π:V->U with πi=I. A complete header is an ordered basis +M=[i,B], with B an ordered basis of ker π. In that header put + +```text +P=M^-1 P0 M=[I b; c D], Q=M^-1 Q0 M=[I f; g E], +S=D-cb, T=E-gf, +H=π P0 Q0 i, K=ST-TS, Z=(S-T)^2. +``` + +Block idempotency gives S²=S and T²=T. Consequently +Z=S+T-ST-TS commutes with both residual maps. + +Restrict to headers with the displayed common identity pivot, nilpotent H, +and rank K=2d (called sharp here). Set a=dim ker H, W=I-H. Then necessarily + +```text +r00=d+s00, r10=d+s10, r01=d+s01, r11=d+a+s11, s_j>=0. (1) +``` + +Conversely every such profile admits a sharp split with that exact H. For fixed +H and profile, all resulting ordered pairs (S,T) are simultaneously similar. +Their representative is the minimal pair below, plus the scalar pairs + +```text +(0,0)^s00 direct-sum (1,0)^s10 direct-sum +(0,1)^s01 direct-sum (1,1)^s11. (2) +``` + +There is no claim that different H/profile data always give distinct orbits. + +Choose N:F^a->U whose image complements im H. On U^3 direct-sum F^a, with +coordinates (x,y,z,t), the minimal pair is + +```text +S(x,y,z,t) = (H(x-z)-Nt, 0, W(z-x)-Nt, t), +T(x,y,z,t) = (0, H(y-z)-Nt, W(z-y)-Nt, t). (3) +``` + +Its dimension is 3d+a. All choices of N yield the same ordered-pair orbit. + +If char F is not 2, put R=2I-H. In coordinates (u,v,t,c), (3) is a common +zero summand of dimension d and the following core on U^2 direct-sum F^a: + +```text + [ H/2 H/2 -N ] [ H/2 -H/2 N ] +S_core = [ R/2 R/2 N ], T_core = [ -R/2 R/2 N ]. (4) + [ 0 0 I ] [ 0 0 I ] +``` + +If the nilpotent Jordan block lengths of H are k_1,...,k_a, the complete +Jordan form of Z is + +```text +direct-sum_i (J_(k_i)(0) direct-sum J_(k_i+1)(0)) + direct-sum 0_(d+s00+s11) direct-sum I_(s10+s01). (5) +``` + +In particular, for j>=1, + +```text +rank Z^j = rank H^j + rank H^(j-1) + s10+s01, (6) +m_Z(t) = t^(max_i k_i+1) (t-1)^epsilon, +epsilon = 1 if s10+s01>0, otherwise 0. +``` + +Nilpotent Jordan blocks exist over every field. The odd-characteristic +qualification matters: for F2,d=1,H=0 and no padding, Z=0, whereas (5) would +contain J2(0). Equations (1)--(3) and the counting result below still hold in +characteristic two; (4)--(6) are not asserted there. + +Over F_q (any prime power), write G_r=|GL_r(F_q)|, G_0=1. The number of sharp +splits for the **fixed original ordered pair** and **exact matrix H** is + +```text +N_H = (G_r00 G_r10 G_r01 G_r11) / + (G_s00 G_s10 G_s01 G_s11 q^(a^2+2a s11)). (7) +``` + +The number of complete ordered headers in this event is N_H G_(n-d), where +n=sum r_j. All those headers reach the same residual orbit, but headers with +other H may reach it too. Thus (7) does not compute its unconditional transition +probability or the number of occurrences of one coordinate representative. +There is no division by GL_d or by a similarity-class size: H is fixed in the +ordered leading coordinates, and changing i's basis changes the split. + +## Proof + +### The sector data and existence + +Let E_j be the four joint-sector projectors, Y_j=E_j i and X_j=π|V_j. +The equations πi=πP0i=πQ0i=I and πP0Q0i=H give + +```text +X00Y00=-W, X10Y10=W, X01Y01=W, X11Y11=H. (8) +``` + +We use the all-field sharp-sector criterion of Nick Petalas +[PR4746](https://github.com/CrocSwap/integer-mult-bounds/pull/4746): under these +identity-pivot hypotheses, rank K=2d iff each of Y10,Y01,Y11 is injective and +each of X10,X01,X11 is onto. This criterion, and its factor-capacity consequence, +are credited premises, not newly claimed results. Since H is nilpotent, W is +invertible; (8) also makes Y00 injective and X00 onto. + +For any onto X:F^r->U and injective Y:U->F^r with XY=A, the intersection +im Y intersect ker X is Y ker A. Hence r>=d+nullity A. Applying this to (8) +gives (1). Attainment uses + +```text +X00=-W, X10=X01=W, X11=[H,N], +Y00=Y10=Y01=I, Y11=[I;0], (9) +``` + +with unused zero columns/rows for the s_j padding coordinates. Their combined +πi is -W+W+W+H=I, both compressed projectors are I, and all four X/Y pairs +have full ranks. The cited criterion gives sharpness. + +### Why the whole ordered residual is forced + +We use the inclusion/observation extension principle of codyw912 +[PR4735](https://github.com/CrocSwap/integer-mult-bounds/pull/4735), generalized +by MatShep [PR4762](https://github.com/CrocSwap/integer-mult-bounds/pull/4762). +Here is its short specialization, to expose exactly the required hypotheses. + +Suppose X,Y and X',Y' have the same ambient dimension, X,X' are onto, Y,Y' +are injective, and XY=X'Y'=A. On L=im Y, the map Yu->Y'u is an isomorphism +respecting X and X'. Its restriction sends L intersect ker X to +im Y' intersect ker X', because both are the images of ker A. Extend it to +an isomorphism ker X->ker X', and therefore to L+ker X. Complete the domain +and target bases by lifts under X and X' of the same basis of a complement +to im A in U. The resulting invertible g obeys + +```text +gY=Y', X'g=X. (10) +``` + +Apply (10) independently in the four sectors to any sharp split and (9), +including its padding. Their direct sum g commutes with P0,Q0 and satisfies +gi=i', π'g=π. For any headers M,M' completing the splits, + +```text +(M')^-1 g M = diag(I_d,L), L invertible. +``` + +The two full pairs and hence their Schur complements are conjugated by this +block-diagonal map. Thus L simultaneously intertwines S,T with S',T'. This +controls the entire residual, including coordinates outside im K. It is not +merely equality of central spectra. It also proves independence of N. + +In the padded representative, i and π vanish on each unused sector direction. +Those directions are therefore untouched scalar residual summands, giving (2). +For the minimal representative, ker π has the parametrization + +```text +(v00,v10,v01,v11,extra11) + = (x+y+W^-1 Hz+W^-1 Nt, x, y, z, t). (11) +``` + +The residual of P0 on ker π is P0-P0 i πP0, and similarly for Q0: this follows +by subtracting the lower-left times upper-right block using πP0i=πQ0i=I. +Substitution of (11) gives exactly (3). + +### The extra nilpotent chains in odd characteristic + +Both W and R are invertible. Set + +```text +u=x-y, v=x+y-2z, c=z+WR^-1 v+R^-1 Nt. +``` + +This is an invertible change of coordinates: z=c-WR^-1v-R^-1Nt, +x=z+(v+u)/2 and y=z+(v-u)/2. Substitution into (3) shows both maps kill +c-directions and have output c=0; their remaining action is (4). In particular, +with Θ=H(2I-H)=HR, + +```text +S_core-T_core = [ 0 H -2N ], + [ R 0 0 ], + [ 0 0 0 ] + +Z_core = [ Θ 0 0 ], + [ 0 Θ -2RN ], + [ 0 0 0 ]. (12) +``` + +The invertible R commutes with H, so rank Θ^j=rank H^j for every j. Thus Θ has +exactly H's nilpotent block lengths. Put B=-2RN. Since R preserves im H and +induces an invertible map on U/im H, im B complements im Θ=im H. For +E=[Θ B;0 0], acting on U direct-sum F^a, + +```text +E^j = [Θ^j Θ^(j-1)B;0 0], +im E^j = im Θ^(j-1), j>=1. (13) +``` + +Consequently E has the nilpotent chains k_i+1: their rank sequence is +sum_i max(k_i+1-j,0)=rank H^(j-1), which uniquely determines a nilpotent +Jordan partition. Combine (12), the d common zero coordinates, and the scalar +summands (2) to obtain (5), (6), and the stated minimal polynomial. + +### The exact fixed-H weight + +For a sector product A of nullity c, take r=d+c+s. The argument (10) says GL_r +acts transitively on its full-rank factor pairs. We specialize the extension +stabilizer calculation of Nick Petalas +[PR4915](https://github.com/CrocSwap/integer-mult-bounds/pull/4915); the generic +method is credited rather than presented as new. + +Put L=im Y and K0=ker X. Choose + +```text +F^r = (L intersect K0) direct-sum R0 direct-sum Z0 direct-sum J, +dimensions: c, d-c, s, c, +L=(L intersect K0)+R0, K0=(L intersect K0)+Z0. +``` + +The stabilizer gY=Y, Xg=X consists exactly of + +```text +[ I 0 U V ] +[ 0 I 0 0 ] +[ 0 0 G E ] +[ 0 0 0 I ], +``` + +where G is arbitrary in GL_s and U,V,E have dimensions c-by-s, c-by-c, +s-by-c. Indeed g-I vanishes on L and has image in K0; these are precisely +the two stabilizer equations, and invertibility is equivalent to that of G. +Its order is G_s q^(c^2+2cs), so the sector factor count is +G_r/(G_s q^(c^2+2cs)). In (8), the first three products have c=0 and the last +has c=a. The four factor choices are independent: (8) already ensures all +split/pivot equations. Their product proves (7). Every split has exactly +G_(n-d) ordered bases of ker π, proving the complete-header count. + +## Concrete first fixtures + +For F3,H=J3(0), the minimal input profile is (3,3,3,4), n=13. The residual +has dimension 10 and Z has blocks (4,3,1,1,1). This explains the t^4 whole +minimal polynomial that motivated the handoff; a restricted t^3 annihilator +cannot remove the extra length-four chain. + +For d=1,H=0, profile (1,1,1,2), over F3 equation (7) gives +2^3*48/3=128 splits and 128*|GL4(F3)|=3,105,423,360 complete headers. +The complete split inventory contains 19,602 splits; the verifier computes +literal Schur ranks on every identity-pivot H=0 candidate and constructs an +actual ordered-pair intertwiner for every sharp one. Over F2 the count is +3 splits / 60,480 headers, recovering the earlier ssafwann +[PR4678](https://github.com/CrocSwap/integer-mult-bounds/pull/4678) fixture, +not claiming it as new. Binary padding in sectors 00,10,11 gives respectively +18,18,21 splits; padding 11 to dimension 3 checks the mixed exponent 2a s11. + +## Reproduction and evidentiary limits + +```sh +python3.12 -B scripts/research_package.py --package research/schur-nilpotent-extension +python3.12 -I -W error -B research/schur-nilpotent-extension/verify.py +python3.12 -I -W error -O -B research/schur-nilpotent-extension/verify.py +``` + +The standard-library checker uses explicit exception-based checks. It does not +import predecessor executables, access the network, invoke Git, or write files. +It checks: + +- All 834 nilpotent H in the complete domains d=1,2,3 over F2/F3 and d=1,2 + over F5. Full commuting pairs are built and literal Schur complements + compared by invertible coordinate maps to (3); all 765 odd-field cases are + also compared to (4), with their full central rank sequences checked. +- 45 padded fixtures, including J3 and J3 direct-sum J1. Both ordered padding + decompositions and concrete factor/header/residual intertwiners are checked. +- Five exhaustive scalar split domains, with all 188 sharp outcomes transported + to the canonical ordered residual; six independent full-rank factor censuses + check the stabilizer denominator (including binary d=2,r=4). +- Nine rejecting controls: nonsquare/nonnilpotent H, negative padding, binary + use of the odd formula, missing extended chain, missing stabilizer exponents, + and a rank-defective factor. Normal and optimized runs exercise the same checks. + +These are finite prime-field corroborations of the written proof, not an +exhaustive theorem check over arbitrary fields or a proof-kernel certificate. +The symbolic argument covers arbitrary fields / prime powers at the stated +boundaries. General nonnilpotent H, the characteristic-two central Jordan law, +later full-guard survival, unconditional state multiplicities, physical supplier +costs and selected-caller admission are unproved here. No Lean, Docker or full +selected scientific cold replay is claimed. The prior source-binding orientation +stopped at a sparse-omitted checkpoint; it was not a baseline pass. + +The package records exact main-source pins, source-head citations, overlap +coverage, verification environment and scope change in TASK.json/SOURCES.json. +Only these five package files are proposed for archive. Committed-byte, +source-history and exported read-only checks are recorded in the PR/handoff +because a package cannot embed its own final commit ID without changing it. + +## Open next questions + +1. For this same nilpotent family in characteristic two, determine the full + central Jordan partition from (3), starting with H=J2 and H=J3. The odd + change of coordinates is invalid there. This is a distinct bounded algebraic + question; no claim is held and no further census is authorized by this note. +2. If a named consumer actually needs these states, specify its header law and + cost allowance before asking for unconditional or later-guard transition + probabilities. Equation (7) is only fixed-H event mass. Different H may + coalesce into one residual orbit; physical cover and selection costs remain + unknown. Without that contract, stop this branch at the present result. + +## Attribution and source status + +Exact main-based source bytes are pinned in SOURCES.json. These are archived +predecessors, not automatically scientifically accepted theorems. We rely on the +stated sharp criterion in #4746 and give the used factor/stabilizer specialization +above so its application is independently reviewable. + +- Nick Petalas: [#4746](https://github.com/CrocSwap/integer-mult-bounds/pull/4746) + all-field sector criterion/construction, [#4597](https://github.com/CrocSwap/integer-mult-bounds/pull/4597) + ordered Schur factorization, [#4801](https://github.com/CrocSwap/integer-mult-bounds/pull/4801) + scalar central law/block question, and #4915 extension-stabilizer weights. +- MatShep #4762 and codyw912 #4735: factor-system equivalence and extension lemma. +- ssafwann: [#4657](https://github.com/CrocSwap/integer-mult-bounds/pull/4657), + [#4671](https://github.com/CrocSwap/integer-mult-bounds/pull/4671), #4678, + and pending #5256 at `c72d6ff431cf5c979f5010018d8eba0c15577bce`; the last supplies + the handoff and adapted matrix helpers, with no runtime dependency on its branch. +- Ryanson Jonathan #4609/#4617 and lee-phys #4634 retain sharpness/seed credit. + Mihir Srivastava #4689, JoyboyBrian #5072 and Krzysztof Wojt #5128 are distinct + successor state/incidence/arbitrary-pivot results, not reclassified as ours. +- Cinna Davis #4100 and source527/commdata2338/Jose Manuel retain the BIT/header + and normalizer context. Repository workflow tooling retains its original credit. diff --git a/research/schur-nilpotent-extension/SOURCES.json b/research/schur-nilpotent-extension/SOURCES.json new file mode 100644 index 0000000000..662387e7df --- /dev/null +++ b/research/schur-nilpotent-extension/SOURCES.json @@ -0,0 +1,60 @@ +{ + "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/all-field-identity-schur/README.md", + "usage": "provenance", + "git_blob": "c3a64475cc52ba7025d57d2c1a810a35c563ca40", + "sha256": "e702c6e05e3283363294ed10a1b9bc4b589c46cc2fb7df198ec9c6841ec78f78" + }, + { + "path": "research/idempotent-factor-invariant/README.md", + "usage": "provenance", + "git_blob": "48ce67bdc3c7c35081cc04f86b7ee20c6a5dd06b", + "sha256": "fae88ccbea3a16d041666f5956d0416b6a21ef57a21f1a0996c7c3a74f7fa3d1" + }, + { + "path": "research/schur-invariant-transitions/README.md", + "usage": "provenance", + "git_blob": "d5118b9f5911949964245eb8942065faff972900", + "sha256": "fccdd2bff1ee00c120796bb1b6c3739cce90dcffbff7c96e897300ed81bba72e" + }, + { + "path": "research/idempotent-stabilizer-multiplicity/README.md", + "usage": "provenance", + "git_blob": "bcc52c12f7b6324cc9426e6c5ec8e5f9438324c0", + "sha256": "fe79c166616cd0561783d3c858435927c6b02a4601ed78be5f5c50ad98fcb53a" + }, + { + "path": "research/identity-pivot-sector-bound/README.md", + "usage": "provenance", + "git_blob": "80c587372713ca47a79d4880dab330e642c3a25a", + "sha256": "c997446a1fc4683694987feea5f2a8423b57d48d5513a27e178f84ecf56ffc12" + }, + { + "path": "research/schur-header-count/README.md", + "usage": "provenance", + "git_blob": "5e644cf316312c0fdd489c8d33911583f1b88af2", + "sha256": "472295f32ebf3fcdc8daa4137af63db70d9943de7cbb97e47ed272823b2a227e" + }, + { + "path": "research/schur-central-spectrum/README.md", + "usage": "provenance", + "git_blob": "29444eb40edd3fb9dd0cb606f5ba5e84a3f69c86", + "sha256": "f2d8568923f9762da88c7dcc8d29266ef5d8fe518bf7884ab5984c8949923620" + } + ] +} diff --git a/research/schur-nilpotent-extension/TASK.json b/research/schur-nilpotent-extension/TASK.json new file mode 100644 index 0000000000..42c0550610 --- /dev/null +++ b/research/schur-nilpotent-extension/TASK.json @@ -0,0 +1,235 @@ +{ + "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": "Written nilpotent-H sharp identity-block Schur theorem: whole ordered-residual rigidity and representative, odd-characteristic central Jordan form, exact fixed-H split/header mass.", + "scope_change_reason": "Took the explicit whole-residual extension handoff in pending PR5256 after checking current handoffs. The formal-interface-lemma card is changed to a scoped algebraic side proof, not a formalization or selected-caller audit. The missing obligation is the complementary attachment beyond im K; this is not another dimension or scalar state census.", + "bottleneck_link": "Side result in the BIT/header setting only. It identifies a whole residual and fixed-H event weight; it neither supplies a physical caller nor removes selected theorem assumptions.", + "budget_minutes": 60, + "stop_rule": "Stop after this nilpotent class and its exact bounded verification. Do not expand to general H, an unrestricted state census, full guards or physical supply without a named contract/cost allowance.", + "outcome": "completed", + "evidence": "README.md gives the scoped proof. verify.py checks 834 nilpotent H, 45 padded transported fixtures, five complete split inventories (188 sharp outcomes), six sector-factor censuses and nine rejecting controls. Author-checked written proof with exact finite corroboration, not independent human or proof-kernel acceptance.", + "author": "ssafwann", + "ai_assistance": "Substantial OpenAI Codex (gpt-6-astra, max reasoning) assistance in T3 Code: research, algebra, writing, implementation, exact verification and GitHub coordination. One agent; no delegated reviewer. Standard-library Python, git, gh and GitHub connector.", + "open_questions": [ + { + "question": "What is the whole central Jordan partition for the same nilpotent family in characteristic two?", + "why_it_matters": "The odd-coordinate split divides by two and fails already for d=1,H=0.", + "first_step": "Use the displayed all-field model (3) for H=J2 and H=J3; derive a symbolic characteristic-two law before any larger census.", + "blocked_by": "A separate bounded claim and proof; no current claim on this follow-up." + }, + { + "question": "Does a named consumer need unconditional or later-guard transition weights for these residuals?", + "why_it_matters": "Fixed-H event mass is not total state mass; multiple H may coalesce and physical selection costs remain unknown.", + "first_step": "Specify the consumer, header distribution, orbit equivalence target and cost allowance.", + "blocked_by": "No named physical consumer/cover contract or complete cost budget; stop this expansion without one." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4653", + "handoff_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19147813", + "assignment_seed": "a49ec20c9cc4033f413c0e726d61159e", + "family_decision": { + "decision": "narrow to an explicit missing extension obligation", + "input": "Fixed commuting field idempotents, common identity-block split, nilpotent exact H, sharp Schur-commutator rank 2d.", + "output": "One whole ordered-residual orbit for specified H and profile; explicit representative, odd central Jordan partition and fixed-H finite-field event weight.", + "predecessor_status": "Main-archived #4746/#4762/#4915 supply credited criteria/extension/counting methods. Pending #5256 supplies the question, fixture and adapted helpers only, not a theorem premise. Archive merge is not scientific acceptance.", + "proved": "Written proof at the stated boundaries, with finite corroboration only in the enumerated prime-field domains.", + "unknown_costs": [ + "physical header cover", + "selection/emission", + "reads", + "owned/borrowed state", + "dirty restoration", + "precision", + "storage", + "stock", + "dispatch", + "complete consumer bill" + ], + "alternative_considered": "Current precision/native-fusion/fitting-rank handoffs have different contracts; this is an explicit unused whole-module extension handoff rather than another seed in the closed dimension/count census.", + "reopen": "A separately scoped characteristic-two proof or a named consumer/header law and cost allowance; no blanket continuation." + }, + "overlap": { + "initial": { + "local": { + "head": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "records": 7091, + "head_records": 7091, + "complete_head_inventory": true, + "unsearched_head_paths": [] + }, + "open_prs": { + "fetched_at": "2026-10-23T14:29:03.205160+00:00", + "complete_pagination": true, + "records": 323 + }, + "discussions": { + "fetched_at": "2026-10-23T14:32:04.499932+00:00", + "complete_pagination": true, + "records": 4525 + } + }, + "queries": [ + "Schur", + "nilpotent extension", + "5256", + "residual rigidity", + "Jordan blocks" + ], + "result": "Found the predecessor handoff and generic factor/stabilizer sources, no matching nilpotent whole-residual extension within the inspected coverage.", + "limits": "PR bodies, Discussion prose and in-scope local README/TASK/ledger; excludes arbitrary diffs, nested notes, exhaustive closed-PR bodies and unpublished work. Targeted all-state PR search supplemented the cache.", + "warnings": [], + "final": { + "local": { + "head": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "records": 7093, + "head_records": 7091, + "complete_head_inventory": true, + "unsearched_head_paths": [] + }, + "open_prs": { + "fetched_at": "2026-10-23T14:49:11.988840+00:00", + "complete_pagination": true, + "records": 327 + }, + "discussions": { + "fetched_at": "2026-10-23T14:52:33.903274+00:00", + "complete_pagination": true, + "records": 4530 + } + }, + "final_warnings": [], + "final_result": "No matching competing extension found. Direct inspection of all Schur-matching open PR bodies locates predecessor #5256 and unrelated #5249 P112 diagonal completions / #5247 downset inertia. All 7091 tracked in-scope notes searched; two additional local package records included." + }, + "predecessor_heads": { + "4801": "98bc071317b17fd8bb4f21044328914c7561d3cb", + "4746": "5f014560d6225cae17598ac479fb29d2947d8e6b", + "4597": "dfeb8ca729a04aea4aa290438f2ed50a37a9c7cb", + "4671": "8d2e3bc76aa7d43e5c629daaf1e72d4dd5a81ed9", + "5072": "6896b92a34b6db839a7ba0ddfa0159f56af5c148", + "5128": "2839d35e58b3285a1992a3ecbae2809ebef7661b", + "4735": "4afbea22e79e19d1d65702eb4090d454ee39d967", + "4762": "3b4e0449262b0b1e07b80e009ef71cc0ca5bf816", + "4915": "906be31cc1337f599dae85718fbe8187a97453f2", + "4678": "af9cf805c501e4e9e947c98c0b97b2281b6b6e97", + "5256": "c72d6ff431cf5c979f5010018d8eba0c15577bce" + }, + "pending_helper_source": { + "head": "c72d6ff431cf5c979f5010018d8eba0c15577bce", + "path": "research/schur-block-central-law/verify.py", + "git_blob": "7bfce0e512f56121d2da9834ec97f37193a4efd0", + "sha256": "d474332a32991f4bb92ac75559f878f4ec99205844c6c7ae90d53622ad9cdfe5", + "usage": "Adapted standard-library matrix helpers with attribution; no external runtime input or dependence on pending scientific claims. Not a main-ancestry source pin." + }, + "environment": { + "python": "CPython 3.12.11", + "os": "macOS arm64", + "dependencies": "standard library only", + "baseline_orientation": "Attempt stopped at sparse-omitted certificates/checkpoints/frontier4359.json; no baseline pass claimed.", + "unrun": [ + "Lean", + "Docker", + "selected scientific cold replay", + "independent human review", + "proof-kernel review" + ] + }, + "validation": { + "direct": "Isolated warning-strict CPython 3.12.11 replay passed.", + "proof_review": "Single-agent algebra reread and concrete coordinate/ordered-pair intertwiner checks. No separate reviewer or proof-kernel acceptance.", + "registered": "Both isolated warning-strict normal and optimized commands passed under CPython 3.12.11 with identical scientific stdout. No assertion-based checks." + }, + "upstream_checkpoint": { + "commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "checked_utc": "2026-10-23T14:48:49Z", + "change": "Canonical main unchanged; guidance, current priority revision 7 and selected frontier unchanged." + }, + "evidence_details": { + "proof": "README.md: factor-transport specialization, explicit whole residual, odd-characteristic core and Jordan proof, sector-stabilizer specialization and complete-header count.", + "verifier": "verify.py: 834 nilpotent H, 45 padded transported fixtures, five complete split inventories (188 sharp outcomes), six sector factor censuses, nine rejecting controls.", + "claim_type": "Author-checked written proof with finite prime-field corroboration; no independent human or proof-kernel acceptance." + }, + "source_status_recheck": { + "checked_utc": "2026-10-23T14:50:00Z", + "unchanged_heads": { + "4746": "merged archive", + "4762": "merged archive", + "4915": "merged archive", + "5256": "open, author-checked pending source; no theorem dependency" + }, + "acceptance_limit": "Archived or merged is not independent scientific acceptance." + } +} diff --git a/research/schur-nilpotent-extension/VERIFY.json b/research/schur-nilpotent-extension/VERIFY.json new file mode 100644 index 0000000000..7f2e1fb530 --- /dev/null +++ b/research/schur-nilpotent-extension/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": "Whole ordered-residual coordinate intertwiners, odd central Jordan ranks, exact split and sector-factor counts, explicit rejecting controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Whole ordered-residual coordinate intertwiners, odd central Jordan ranks, exact split and sector-factor counts, explicit rejecting controls." + } + ] +} diff --git a/research/schur-nilpotent-extension/verify.py b/research/schur-nilpotent-extension/verify.py new file mode 100644 index 0000000000..e9c78dd723 --- /dev/null +++ b/research/schur-nilpotent-extension/verify.py @@ -0,0 +1,487 @@ +#!/usr/bin/env python3 +"""Nilpotent Schur extension: bounded exact corroboration, not a general proof. + +ssafwann with substantial OpenAI Codex (gpt-6-astra) assistance. Apache-2.0. +Matrix helpers adapted from ssafwann PR5256, exact head c72d6ff431cf5c979f5010018d8eba0c15577bce. +Sector construction: Nick Petalas PR4746. Factor transport: MatShep PR4762 / +codyw912 PR4735. Stabilizer method: Nick Petalas PR4915. No runtime imports +from those packages; the written argument in README.md is the general proof. +""" +from itertools import product +from math import prod +import json + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def zero(n, m): + return tuple((0,) * m for _ in range(n)) + + +def eye(n): + return tuple(tuple(int(i == j) for j in range(n)) for i in range(n)) + + +def add(a, b, q, scale=1): + require(len(a) == len(b) and all(len(r) == len(s) for r, s in zip(a, b)), + 'addition shape') + return tuple(tuple((x+scale*y) % q for x, y in zip(r, s)) + for r, s in zip(a, b)) + + +def mul(a, b, q): + require(a and b and all(len(row) == len(b) for row in a), 'product shape') + require(all(len(row) == len(b[0]) for row in b), 'ragged product') + bt = tuple(zip(*b)) + return tuple(tuple(sum(x*y for x, y in zip(r, c)) % q for c in bt) + for r in a) + + +def block(a, b, c, d): + return tuple(x+y for x, y in zip(a, b)) + tuple(x+y for x, y in zip(c, d)) + + +def rref(a, q, columns=None): + m = [list(row) for row in a] + width = len(m[0]) if m else 0 + pivots = [] + for j in range(width if columns is None else columns): + pivot = next((i for i in range(len(pivots), len(m)) if m[i][j]), None) + if pivot is None: + continue + k = len(pivots) + m[k], m[pivot] = m[pivot], m[k] + inv = pow(m[k][j], -1, q) + m[k] = [(x*inv) % q for x in m[k]] + for i in range(len(m)): + if i != k and m[i][j]: + t = m[i][j] + m[i] = [(x-t*y) % q for x, y in zip(m[i], m[k])] + pivots.append(j) + return tuple(tuple(row) for row in m), tuple(pivots) + + +def rank(a, q): + return len(rref(a, q)[1]) + + +def inverse(a, q): + n = len(a) + reduced, pivots = rref(tuple(r+s for r, s in zip(a, eye(n))), q, n) + require(len(pivots) == n, 'singular matrix') + return tuple(row[n:] for row in reduced) + + +def kernel(a, q): + reduced, pivots = rref(a, q) + width = len(a[0]) + columns = [] + for j in range(width): + if j not in pivots: + v = [0]*width + v[j] = 1 + for i, p in enumerate(pivots): + v[p] = -reduced[i][j] % q + columns.append(tuple(v)) + return tuple(zip(*columns)) + + +def schur(p, d, q): + r = tuple(row[d:] for row in p[:d]) + c = tuple(row[:d] for row in p[d:]) + tail = tuple(row[d:] for row in p[d:]) + return add(tail, mul(c, r, q), q, -1) + + + +def scale(a, c, q): + return tuple(tuple(c*x % q for x in row) for row in a) + + +def columns(a): + return list(zip(*a)) + + +def from_columns(cs, rows): + return tuple(zip(*cs)) if cs else zero(rows, 0) + + +def diag(*blocks): + n = sum(len(b) for b in blocks) + out, offset = [], 0 + for b in blocks: + out.extend((0,)*offset + row + (0,)*(n-offset-len(b)) for row in b) + offset += len(b) + return tuple(out) + + +def solve(a, v, q): + reduced, pivots = rref(tuple(row+(x,) for row, x in zip(a, v)), q, len(a[0])) + require(not any(not any(row[:-1]) and row[-1] for row in reduced), 'no lift') + result = [0]*len(a[0]) + for i, j in enumerate(pivots): + result[j] = reduced[i][-1] + return tuple(result) + + +def extend(cs, candidates, rows, q): + added = [] + for c in candidates: + if rank(from_columns(cs+added+[c], rows), q) > len(cs)+len(added): + added.append(c) + return added + + +def nilpotent(h, q): + d = len(h) + require(d > 0 and all(len(row) == d for row in h), 'square H') + power = eye(d) + for _ in range(d): + power = mul(power, h, q) + return power == zero(d, d) + + +def factors(h, pads, q): + require(nilpotent(h, q), 'nilpotent family') + require(len(pads) == 4 and all(isinstance(s, int) and s >= 0 for s in pads), + 'nonnegative four-sector padding') + d = len(h) + w = add(eye(d), h, q, -1) + cs = columns(h) + # Use only independent columns when selecting a complement to im H. + independent = [] + for c in cs: + independent += extend(independent, [c], d, q) + nc = extend(independent, columns(eye(d)), d, q) + n = from_columns(nc, d) + ts = (scale(w, -1, q), w, w, h) + out = [] + for j, t in enumerate(ts): + x = tuple(row + (n[i] if j == 3 else ()) + (0,)*pads[j] + for i, row in enumerate(t)) + out.append((x, eye(d)+zero(len(x[0])-d, d))) + return out, n + + +def split_pair(fs, q, require_sharp=True): + d = len(fs[0][0]) + pi = tuple(sum((x[i] for x, _ in fs), ()) for i in range(d)) + inc = sum((y for _, y in fs), ()) + require(mul(pi, inc, q) == eye(d), 'split identity') + basis = tuple(a+b for a, b in zip(inc, kernel(pi, q))) + inv = inverse(basis, q) + sector = sum(((j,)*len(y) for j, (_, y) in enumerate(fs)), ()) + pair = [] + for support in ((1, 3), (2, 3)): + p0 = tuple(tuple(int(i == j and sector[i] in support) + for j in range(len(inc))) for i in range(len(inc))) + p = mul(mul(inv, p0, q), basis, q) + require(tuple(row[:d] for row in p[:d]) == eye(d), 'identity pivot') + pair.append(p) + p, t = pair + require(mul(p, p, q) == p and mul(t, t, q) == t, 'full idempotents') + pq = mul(p, t, q) + require(pq == mul(t, p, q), 'full commuting pair') + s, u = schur(p, d, q), schur(t, d, q) + require(mul(s, s, q) == s and mul(u, u, q) == u, 'residual idempotents') + if require_sharp: + require(rank(add(mul(s, u, q), mul(u, s, q), q, -1), q) == 2*d, + 'sharp commutator') + return basis, s, u, tuple(row[:d] for row in pq[:d]) + + +def transport(x, y, x0, y0, q): + """Construct gY=Y0, X0g=X, rather than compare rank fingerprints.""" + d, r = len(x), len(y) + require(rank(x, q) == d and rank(y, q) == d, 'active factor ranks') + require(rank(x0, q) == d and rank(y0, q) == d and len(y0) == r, + 'target factor ranks') + t = mul(x, y, q) + require(t == mul(x0, y0, q), 'equal products') + b, b0 = columns(y), columns(y0) + b += extend(b, columns(kernel(x, q)), r, q) + b0 += extend(b0, columns(kernel(x0, q)), r, q) + image = [] + for c in columns(t): + image += extend(image, [c], d, q) + for v in extend(image, columns(eye(d)), d, q): + b.append(solve(x, v, q)) + b0.append(solve(x0, v, q)) + require(len(b) == r and len(b0) == r, 'transport bases') + g = mul(from_columns(b0, r), inverse(from_columns(b, r), q), q) + require(rank(g, q) == r and mul(g, y, q) == y0 and mul(x0, g, q) == x, + 'factor intertwiner') + return g + + +def residual_transport(fs, target, q): + m, s, t, h = split_pair(fs, q) + m0, s0, t0, h0 = split_pair(target, q) + require(h == h0, 'fixed H') + g = diag(*(transport(x, y, x0, y0, q) + for (x, y), (x0, y0) in zip(fs, target))) + change = mul(mul(inverse(m0, q), g, q), m, q) + d = len(h) + k = tuple(row[d:] for row in change[d:]) + require(change == diag(eye(d), k) and rank(k, q) == len(k), 'header transport') + require(mul(k, s, q) == mul(s0, k, q) and mul(k, t, q) == mul(t0, k, q), + 'whole residual ordered intertwiner') + + +def model(h, n, q): + """Explicit (x,y,z,t) action; independently compared to literal Schur.""" + d, a = len(h), len(n[0]) + w = add(eye(d), h, q, -1) + z = zero(d, d) + nn = scale(n, -1, q) + s = tuple(h[i]+z[i]+scale(h, -1, q)[i]+nn[i] for i in range(d)) + s += zero(d, 3*d+a) + s += tuple(scale(w, -1, q)[i]+z[i]+w[i]+nn[i] for i in range(d)) + s += tuple((0,)*(3*d)+row for row in eye(a)) + t = zero(d, 3*d+a) + t += tuple(z[i]+h[i]+scale(h, -1, q)[i]+nn[i] for i in range(d)) + t += tuple(z[i]+scale(w, -1, q)[i]+w[i]+nn[i] for i in range(d)) + t += tuple((0,)*(3*d)+row for row in eye(a)) + return s, t + + +def odd_form(h, n, q): + require(q in (3, 5), 'odd characteristic required') + d, a = len(h), len(n[0]) + w = add(eye(d), h, q, -1) + r = add(scale(eye(d), 2, q), h, q, -1) + ri = inverse(r, q) + half = pow(2, -1, q) + hh, rh = scale(h, half, q), scale(r, half, q) + nn = scale(n, -1, q) + sc = tuple(hh[i]+hh[i]+nn[i] for i in range(d)) + sc += tuple(rh[i]+rh[i]+n[i] for i in range(d)) + sc += tuple((0,)*(2*d)+row for row in eye(a)) + tc = tuple(hh[i]+scale(hh, -1, q)[i]+n[i] for i in range(d)) + tc += tuple(scale(rh, -1, q)[i]+rh[i]+n[i] for i in range(d)) + tc += tuple((0,)*(2*d)+row for row in eye(a)) + # F maps (u,v,t,c) to (x,y,z,t), using the displayed inverse formula. + size = 3*d+a + zrow = tuple((0,)*d+scale(mul(w, ri, q), -1, q)[i] + +scale(mul(ri, n, q), -1, q)[i]+eye(d)[i] for i in range(d)) + xrow = add(zrow, tuple(scale(eye(d), half, q)[i] + +scale(eye(d), half, q)[i]+(0,)*(a+d) + for i in range(d)), q) + yrow = add(zrow, tuple(scale(eye(d), -half, q)[i] + +scale(eye(d), half, q)[i]+(0,)*(a+d) + for i in range(d)), q) + f = xrow+yrow+zrow+tuple((0,)*(2*d)+row+(0,)*d for row in eye(a)) + require(len(f) == size and rank(f, q) == size, 'odd coordinate isomorphism') + return diag(sc, zero(d, d)), diag(tc, zero(d, d)), f + + +def check_h(h, pads, q): + fs, n = factors(h, pads, q) + basis, s, t, found = split_pair(fs, q) + require(found == h, 'compressed product') + d, a = len(h), len(n[0]) + if any(pads): + minimal, _ = factors(h, (0, 0, 0, 0), q) + minimal_basis, sm, tm, _ = split_pair(minimal, q) + # Embed the minimal kernel and append the unused sector coordinates. + # This checks the full ordered padding decomposition, not just Z. + embedded, extra, old_offset, offset = [], [], 0, 0 + total = len(basis) + for j, (_, y) in enumerate(minimal): + size = len(y) + embedded += [row[d:] for row in minimal_basis[old_offset:old_offset+size]] + embedded += list(zero(pads[j], len(sm))) + for k in range(pads[j]): + extra.append(tuple(int(i == offset+size+k) for i in range(total))) + old_offset += size + offset += size+pads[j] + v = tuple(row+tail for row, tail in zip(embedded, from_columns(extra, total))) + change = mul(inverse(basis, q), v, q) + require(change[:d] == zero(d, total-d), 'padded kernel coordinates') + change = change[d:] + sp = diag(sm, zero(pads[0], pads[0]), eye(pads[1]), + zero(pads[2], pads[2]), eye(pads[3])) + tp = diag(tm, zero(pads[0], pads[0]), zero(pads[1], pads[1]), + eye(pads[2]), eye(pads[3])) + require(rank(change, q) == total-d and mul(s, change, q) == mul(change, sp, q) + and mul(t, change, q) == mul(change, tp, q), 'ordered padding decomposition') + # Compare the minimal literal Schur pair to the independent coordinate model. + if not any(pads): + w = add(eye(d), h, q, -1) + wi = inverse(w, q) + v0 = tuple(eye(d)[i]+eye(d)[i]+mul(wi, h, q)[i]+mul(wi, n, q)[i] + for i in range(d)) + v = v0 + tuple(eye(d)[i]+(0,)*(2*d+a) for i in range(d)) + v += tuple((0,)*d+eye(d)[i]+(0,)*(d+a) for i in range(d)) + v += tuple((0,)*(2*d)+eye(d)[i]+(0,)*a for i in range(d)) + v += tuple((0,)*(3*d)+row for row in eye(a)) + change = mul(inverse(basis, q), v, q) + require(change[:d] == zero(d, 3*d+a), 'kernel coordinates') + change = change[d:] + sm, tm = model(h, n, q) + require(rank(change, q) == 3*d+a and mul(s, change, q) == mul(change, sm, q) + and mul(t, change, q) == mul(change, tm, q), 'literal Schur model') + if q != 2: + sc, tc, f = odd_form(h, n, q) + require(mul(sm, f, q) == mul(f, sc, q) + and mul(tm, f, q) == mul(f, tc, q), 'odd core plus common zero') + if q != 2: + delta = add(s, t, q, -1) + z = mul(delta, delta, q) + hp, zp = eye(d), eye(len(s)) + for _ in range(1, d+2): + oldrank = rank(hp, q) + hp, zp = mul(hp, h, q), mul(zp, z, q) + require(rank(zp, q) == rank(hp, q)+oldrank+pads[1]+pads[2], + 'whole central Jordan ranks') + # Powers of Z only see nonzero primary dimensions; also distinguish + # exactly the claimed size-one blocks at eigenvalue one. + require(rank(add(z, eye(len(z)), q, -1), q) == len(z)-pads[1]-pads[2], + 'unit padding eigenblocks') + return s, t + + +def gl(n, q): + return prod(q**n-q**j for j in range(n)) + + +def split_count(h, pads, q): + require(nilpotent(h, q), 'nilpotent count family') + d, a = len(h), len(h)-rank(h, q) + sizes = [d+s for s in pads] + sizes[3] += a + numerator = prod(gl(r, q) for r in sizes) + denominator = prod(gl(s, q) for s in pads)*q**(a*a+2*a*pads[3]) + require(numerator % denominator == 0, 'integral mass') + return numerator//denominator + + +def scalar_census(q, pads): + h = ((0,),) + target, _ = factors(h, pads, q) + sizes = tuple(len(y) for _, y in target) + n = sum(sizes) + require(q**(2*n) <= 60000, 'split census capacity') + vecs = list(product(range(q), repeat=n)) + accepted, splits, legal = 0, 0, 0 + for inc in vecs: + for pi in vecs: + if sum(x*y for x, y in zip(inc, pi)) % q != 1: + continue + splits += 1 + off, fs, prods = 0, [], [] + for size in sizes: + x, y = (tuple(pi[off:off+size]),), tuple((v,) for v in inc[off:off+size]) + fs.append((x, y)) + prods.append(mul(x, y, q)[0][0]) + off += size + if prods != [q-1, 1, 1, 0]: + continue + legal += 1 + _, s, t, _ = split_pair(fs, q, require_sharp=False) + sharp = rank(add(mul(s, t, q), mul(t, s, q), q, -1), q) == 2 + require(sharp == all(rank(x, q) == 1 and rank(y, q) == 1 for x, y in fs), + 'sector criterion against literal Schur rank') + if not sharp: + continue + residual_transport(fs, target, q) + accepted += 1 + require(splits == (q**n-1)*q**(n-1), 'complete split inventory') + require(accepted == split_count(h, pads, q), 'exact fixed-H split mass') + return {'q': q, 'sectors': sizes, 'all_splits': splits, 'identity_H0_splits': legal, + 'fixed_H_splits': accepted, + 'complete_headers': accepted*gl(n-1, q)} + + +def factor_census(q, d, r, t): + require(q**(2*d*r) <= 70000, 'factor census capacity') + xs, ys = [], [] + for values in product(range(q), repeat=d*r): + x = tuple(tuple(values[i*r:(i+1)*r]) for i in range(d)) + if rank(x, q) == d: + xs.append(x) + ys.append(tuple(zip(*x))) + count = sum(mul(x, y, q) == t for x in xs for y in ys) + c = d-rank(t, q) + s = r-d-c + require(s >= 0, 'factor capacity premise') + den = gl(s, q)*q**(c*c+2*c*s) + require(gl(r, q) % den == 0 and count == gl(r, q)//den, 'sector stabilizer count') + return {'q': q, 'd': d, 'r': r, 'rank_product': d-c, 'pairs': count} + + +def rejected(action, label): + try: + action() + except ValueError: + return label + raise ValueError('control failed to reject: '+label) + + +def main(): + counts = [] + for q, d in ((2, 1), (2, 2), (2, 3), (3, 1), (3, 2), (3, 3), (5, 1), (5, 2)): + count = 0 + for values in product(range(q), repeat=d*d): + h = tuple(tuple(values[i*d:(i+1)*d]) for i in range(d)) + if nilpotent(h, q): + check_h(h, (0, 0, 0, 0), q) + count += 1 + require(count == q**(d*d-d), 'nilpotent inventory cross-check') + counts.append({'q': q, 'd': d, 'nilpotent_H': count}) + j3 = ((0, 1, 0), (0, 0, 1), (0, 0, 0)) + fixtures = [((0,),), j3, diag(j3, ((0,),))] + padded = 0 + for q in (2, 3, 5): + for h in fixtures: + for pads in ((1, 0, 0, 0), (0, 1, 0, 0), (0, 0, 1, 0), + (0, 0, 0, 2), (1, 1, 1, 1)): + check_h(h, pads, q) + fs, _ = factors(h, pads, q) + moved = [] + for x, y in fs: + r = len(y) + g = [list(row) for row in eye(r)] + if r > 1: + g[0][-1] = 1 + g = tuple(tuple(row) for row in g) + moved.append((mul(x, inverse(g, q), q), mul(g, y, q))) + residual_transport(moved, fs, q) + padded += 1 + census = [scalar_census(3, (0, 0, 0, 0))] + census += [scalar_census(2, p) for p in ((0, 0, 0, 0), (1, 0, 0, 0), + (0, 1, 0, 0), (0, 0, 0, 1))] + fc = [factor_census(q, d, r, t) for q, d, r, t in + ((2, 1, 3, ((0,),)), (3, 1, 3, ((0,),)), (5, 1, 2, ((0,),)), + (3, 1, 2, ((1,),)), (2, 2, 3, ((0, 1), (0, 0))), + (2, 2, 4, ((0, 1), (0, 0))))] + s2, t2 = check_h(((0,),), (0, 0, 0, 0), 2) + z2 = mul(add(s2, t2, 2, -1), add(s2, t2, 2, -1), 2) + s3, t3 = check_h(j3, (0, 0, 0, 0), 3) + z3 = mul(add(s3, t3, 3, -1), add(s3, t3, 3, -1), 3) + z3cube = mul(mul(z3, z3, 3), z3, 3) + controls = [ + rejected(lambda: factors(eye(2), (0, 0, 0, 0), 3), 'nonnilpotent H'), + rejected(lambda: factors(((0, 0),), (0, 0, 0, 0), 3), 'nonsquare H'), + rejected(lambda: factors(((0,),), (0, 0, 0, -1), 3), 'negative padding'), + rejected(lambda: odd_form(((0,),), ((1,),), 2), 'division by two'), + rejected(lambda: require(rank(z2, 2) == 1, 'binary exception'), 'odd Jordan law in F2'), + rejected(lambda: require(z3cube == zero(len(z3), len(z3)), 'missing chain'), 'omit extended Jordan chain'), + rejected(lambda: require(split_count(((0,),), (0, 0, 0, 0), 3) == 384, + 'missing unipotent denominator'), 'omit q^(a squared)'), + rejected(lambda: require(split_count(((0,),), (0, 0, 0, 1), 2) == 84, + 'missing mixed exponent'), 'omit 2 a s11'), + rejected(lambda: transport(((0,),), ((1,),), ((0,),), ((1,),), 3), 'non-surjective factor'), + ] + print(json.dumps({'nilpotent_domains': counts, 'padded_transport_fixtures': padded, + 'split_censuses': census, 'factor_censuses': fc, + 'ternary_J3_whole_Jordan': [4, 3, 1, 1, 1], + 'rejection_controls': controls}, sort_keys=True)) + print('PASS_SCHUR_NILPOTENT_EXTENSION') + + +if __name__ == '__main__': + main()