From c72d6ff431cf5c979f5010018d8eba0c15577bce Mon Sep 17 00:00:00 2001 From: ssafwann Date: Fri, 23 Oct 2026 22:22:43 +0800 Subject: [PATCH] Prove the block Schur central-action and annihilator law --- research/schur-block-central-law/README.md | 304 ++++++++++++++++ research/schur-block-central-law/SOURCES.json | 48 +++ research/schur-block-central-law/TASK.json | 198 +++++++++++ research/schur-block-central-law/VERIFY.json | 34 ++ research/schur-block-central-law/verify.py | 327 ++++++++++++++++++ 5 files changed, 911 insertions(+) create mode 100644 research/schur-block-central-law/README.md create mode 100644 research/schur-block-central-law/SOURCES.json create mode 100644 research/schur-block-central-law/TASK.json create mode 100644 research/schur-block-central-law/VERIFY.json create mode 100644 research/schur-block-central-law/verify.py diff --git a/research/schur-block-central-law/README.md b/research/schur-block-central-law/README.md new file mode 100644 index 0000000000..60940ce955 --- /dev/null +++ b/research/schur-block-central-law/README.md @@ -0,0 +1,304 @@ +# Central action after an identity-block Schur deletion + +**Scoped all-field algebraic proof with finite exact corroboration; no new κ.** +Prepared for ssafwann with substantial OpenAI Codex (gpt-6-astra) assistance, +by one agent. Apache-2.0. + +Nick Petalas's [#4801](https://github.com/CrocSwap/integer-mult-bounds/pull/4801) +proves a central-spectrum law for a scalar identity pivot and explicitly asks +for the ordered block replacement. This package answers that question. For a +common identity block of size d and compressed product H, the replacement is +an **intertwiner with two copies of Θ = 2H−H²**, rather than a scalar equation +between matrices of different sizes. When the Schur commutator has rank 2d, +this gives the exact restricted operator, including its nonsemisimple data. + +## Theorem and domain + +Let F be any field, d >= 1, n > d, and let P,Q in M_n(F) be commuting +idempotents. Both leading d-by-d blocks must be I_d. Write + +```text +P = [I R; C D], Q = [I L; E F0], H = (PQ)11, +S = D−CR, T = F0−EL, K = ST−TS, +Z = (S−T)², J = H(I−H), Θ = 2H−H². +``` + +No symmetry, invertibility of H, semisimplicity, characteristic restriction, +or maximal-rank hypothesis is imposed initially. Put G=(PQ)21 and define + +```text +A = [G−EH, C−E] : F^(2d) -> F^(n−d), +U_H = [I−H −I; −J H], V_H = [I I; 0 0]. +``` + +Then the ordered identities are + +```text +S A = A U_H, T A = A V_H, +Z A = A diag(Θ,Θ). (1) +``` + +For every polynomial p in F[t] satisfying p(Θ)=0, + +```text +p(Z) K = 0, Z(Z−I) p(Z) = 0. (2) +``` + +In particular, with m_Θ the minimal polynomial of Θ, the minimal polynomial +of Z divides `t(t−1)m_Θ(t)`. One may instead use the characteristic polynomial +of Θ to get a generally weaker annihilator of degree d+2. Repeated factors +must be retained. Over an algebraic closure the spectrum of Z is contained +in `{0,1} ∪ spectrum(Θ)`; this does not imply diagonalizability. + +If additionally **rank K = 2d**, then im K = im A and A is an isomorphism +onto that subspace. Consequently: + +- the ordered pair restricted to im K is simultaneously similar to `(U_H,V_H)`; +- `Z|im K` is similar to `Θ ⊕ Θ`; +- its minimal polynomial is exactly m_Θ, and its characteristic polynomial + is exactly the square of the characteristic polynomial of Θ; +- over a splitting field, each Jordan block of Θ occurs twice in `Z|im K`. + +These conclusions concern the indicated invariant subspace, not all n−d +residual coordinates. They do not classify the entire residual pair or count +headers. The dimension minimum is the credited #4671/#4746 result, not a new +claim here. At d=1, (2) recovers #4801's scalar law with Θ=h(2−h). + +## Proof, with ordered products retained + +Let i:F^d -> F^n and π:F^n -> F^d be the coordinate inclusion and projection. +Thus πi=πPi=πQi=I and πPQi=H. Define the full-space Schur lifts + +```text +P̂ = P−PiπP, Q̂ = Q−QiπQ. +``` + +In the original block coordinates these are `diag(0,S)` and `diag(0,T)`. +For example P̂i=0 and πP̂=0, and expanding P̂² using P²=P and πPi=I gives +P̂²=P̂. Thus S,T are idempotents. The same facts hold for Q̂. + +Define two block columns and a block row: + +```text +a = PQi−QiH, b = (P−Q)i, + = [a,b], +B̂ = [π(P−Q); −πPQ+HπQ]. +``` + +Their top d rows / first d columns vanish respectively: πÂ=0 and B̂i=0. +The following expansion gives the identity-pivot specialization of Petalas's +ordered Schur factorization (#4597), also used in #4671/#4746: + +```text +[P̂,Q̂] = PQiπ(P−Q) − (P−Q)iπPQ + PiHπQ − QiHπP = ÂB̂. +``` + +Indeed expand `(P−PiπP)(Q−QiπQ)` and its reversed product, cancel PQ=QP, +and use πPQi=πQPi=H. Removing the zero first blocks gives `K=AB`, where +`B=[R−L; −(PQ)12+HL]`. This derivation does not commute any rectangular factors. + +Now compute the four actions directly: + +```text +P̂a = PQi(I−H) − Pi(H−H²) = a(I−H)−bJ, +P̂b = PiH−PQi = −a+bH, +Q̂a = a, +Q̂b = a. (3) +``` + +For example πPa=H−H² and πQa=0; πPb=I−H and πQb=H−I. +These four identities prove the first two equations of (1). Their difference +has the right-acting block matrix + +```text +U_H−V_H = [−H −2I; −J H]. +``` + +Here J=H−H² is a polynomial in H, so HJ=JH. Squaring this particular matrix, +with its order retained, gives + +```text +(U_H−V_H)² = [H²+2J 0; 0 H²+2J] = diag(Θ,Θ). +``` + +This proves the last equation of (1). The commutation used in this step is +between two polynomials in H; it is not an assumption on arbitrary original +matrix blocks. Repeated application and linear combination give +`p(Z)A = A diag(p(Θ),p(Θ))`. Multiplying by B proves the first equation of (2). + +For any two idempotents S,T, with no commutation assumption on them, + +```text +Z = S+T−ST−TS, +ZS = SZ = S−STS, ZT = TZ = T−TST, +K² = Z²−Z. (4) +``` + +Each line follows by expansion and S²=S,T²=T. These central identities are +credited to the existing projector/Schur lineage, especially Ryanson +Jonathan #4609 and Petalas #4801. Multiplying `p(Z)K=0` by K and using (4) +proves the second equation of (2), since all polynomial factors in Z commute. + +Finally K=AB implies im K ⊆ im A and rank K <= rank A <= 2d. Under the stated +sharpness hypothesis every inequality is equality. A then identifies F^(2d) +with im K, and (1) gives both restricted similarities. The minimal polynomial, +characteristic polynomial and Jordan statements follow from this actual +isomorphism, not merely from an annihilating polynomial. This completes the +all-field proof, including singular and nonsemisimple H. + +## Attained repeated roots and an indispensable endpoint factor + +Take the nilpotent three-by-three Jordan block + +```text +H = [0 1 0; 0 0 1; 0 0 0]. +``` + +The credited sector construction below produces full commuting pairs with +n=13, d=3 and rank K=6, over both F2 and F3. + +| Field | Θ | Minimal polynomial on im K | Ranks of K, ZK, Z²K, Z³K | Minimal polynomial on the whole residual | +|---|---|---|---|---| +| F2 | H² | t² | 6,2,0,0 | t² | +| F3 | 2H−H² | t³ | 6,4,2,0 | t⁴ | + +Thus replacing m_Θ by its square-free part is false even on im K. In the +ternary example, m_Θ(Z) is nonzero on the full residual, of rank one; an +additional factor t is needed there. The second identity in (2) permits it. +This is a concrete block-pivot example, beyond #4801's scalar repeated root. +The displayed whole-space values are finite exact fixture claims, verified +by the first linear dependence of complete matrix powers. + +For an example without scalar eigenvalues over F2, use +`H=[0 1; 1 1]`. Then Θ=H² and m_Θ=t²+t+1. The constructed n=8 pair has +rank K=4 and whole-space minimal polynomial `t(t²+t+1)`. Consequently a +scalar-eigenvalue check alone cannot verify this theorem. The same displayed +H over F5 supplies an odd-characteristic sign control and a repeated-root +shift; it is a separate field calculation. + +### Explicit fixture construction + +This is a padded version of Petalas #4746's all-field construction, following +ssafwann #4671's binary construction. It is included to make every example +independently reproducible, not as a new dimension result. Let W=I−H. In the +00 sector choose `X00=−W, Y00=I`, of dimension d. For each active sector +10,01,11 with target F respectively W,W,H, choose columns N complementing +im F and set `X=[F,N], Y=[I;0]`. Then X is onto, Y is injective and XY=F. + +Concatenate X's to π0 and stack Y's to i0. Their products sum to +`−W+W+W+H=I`, so π0i0=I. On the four sectors let +`P0=diag(0,I,0,I), Q0=diag(0,0,I,I)`. Take `M=[i0, basis(ker π0)]` and form +`P=M^-1 P0 M, Q=M^-1 Q0 M`. The pivots are identities and `(PQ)11=H`. +The six active ranks give sharpness by #4746; the new checker independently +checks the resulting full-matrix commutator rank in every case. Dimension is +`4d+nullity(H)+2 nullity(I−H)`, at most 6d. No optimality is claimed for the +padded 00 sector. Greedy standard-coordinate complements make the executable +construction deterministic. + +## Verification + +Python 3.12 standard library, no network, Git or predecessor-code dependency +in the scientific verifier. All checks use explicit exceptions under `-O`. + +```sh +python3.12 -B scripts/research_package.py --package research/schur-block-central-law +python3.12 -B scripts/check_research_commit.py --package research/schur-block-central-law --check-source-history +python3.12 -I -W error -B research/schur-block-central-law/verify.py +python3.12 -I -W error -O -B research/schur-block-central-law/verify.py +``` + +On macOS arm64 / CPython 3.12.11, the registered normal and optimized +replays pass in 6.32 seconds combined (local duration, not a speed comparison). +The registered replay runs both direct modes and emits +`PASS_SCHUR_BLOCK_CENTRAL_LAW`. The verifier writes no files. + +- All **1,244** H in seven complete domains: d=1,2,3 over F2 and d=1,2 over + each of F3,F5. For each it constructs P,Q, verifies their premises and H, + forms literal Schur complements, checks K=AB, both ordered actions, the + central intertwiner, both polynomial laws and exact restricted minimal + polynomial. Complete-matrix powers acting on K check the latter without + using the proposed intertwiner as an oracle. +- Every **1,472** ordered commuting identity-pivot binary projector pair at + `(n,d)=(3,1),(4,2)`: respectively 253 and 1,219 pairs. These credited small + domains test the new laws beyond the sharp fixture construction. No pair + in these domains is sharp; rank-zero and rank-one commutators occur. +- Four displayed fixtures additionally check every rank sequence + `rank((Z−λI)^j K)=2 rank((Θ−λI)^j)` for every λ in their field and + j=0,...,d+1, and compute their whole-space minimal polynomials. +- Nine rejection controls distinguish repeated roots, the full-space + endpoint factor, H from Θ, the odd-field sign, sharpness, pivot validity, + idempotency, input commutation and the census capacity limit. + +Universal claims rest on the written argument. The finite domains are prime +fields only; no characteristic-zero, extension-field or arbitrary-dimensional +census is claimed. Source-history/committed-byte checking and export transport +integrity are separate from mathematical validity. No independent human or +formal proof-kernel acceptance, Lean, Docker, full-history replay or selected +scientific cold replay is claimed. Hosted CI is reported separately in the PR. + +## Scope, overlap and attribution + +Base: canonical main `ff3cc58e370d0f678e529246f8c73e8094e18fcf`, priority revision +7, selected conditional κ=0.00302015. The scoped handoff is claimed in +[Discussion #4653](https://github.com/CrocSwap/integer-mult-bounds/discussions/4653), +with a [#1166 pointer](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19147366). +The `formal-interface-lemma` card is explicitly **changed** to a written +algebraic side result. It supplies a necessary residual constraint and, under +sharpness, one exact restricted representation. It does not audit the selected +supplier's uniform implementation. The source-binding orientation command +stopped at the sparse-omitted `certificates/checkpoints/frontier4359.json`; +no selected baseline pass is claimed. + +Initial overlap covers all 7,091 tracked in-scope notes on this base, 319 open +PR bodies and 4,505 Discussion records, with complete pagination and no coverage +warnings. The final refresh covers 322 open PRs (14:19 UTC), 4,520 Discussion +records (14:21 UTC), and all 7,091 tracked notes, without coverage warnings. +Canonical main is unchanged. TASK.json records these snapshots. +Targeted all-state PR searches supplement this, but arbitrary diffs, nested +notes, an exhaustive closed-PR body inventory and unpublished work remain +outside coverage. No absence-of-matches claim establishes novelty. + +Exact base-main README bytes are provenance-pinned in SOURCES.json; their +historical claims retain their stated review status. None is a runtime input. +The immediate #4801/#4746 predecessors were merged when checked; archive acceptance +does not imply independent scientific approval. + +- **Nick Petalas #4801**, head `98bc071317b17fd8bb4f21044328914c7561d3cb`, + supplies the scalar law and explicit block question. **#4597**, head + `dfeb8ca729a04aea4aa290438f2ed50a37a9c7cb`, supplies the ordered factorization; + #4278/#4259/#4228 retain the scalar Schur/header lineage. +- **Nick Petalas #4746**, head `5f014560d6225cae17598ac479fb29d2947d8e6b`, + supplies the signed all-field sectors and fixture construction, extending + **ssafwann #4671**, head `8d2e3bc76aa7d43e5c629daaf1e72d4dd5a81ed9`; + #4657/#4678 retain the identity-pivot and counting lineage. +- **Ryanson Jonathan #4609**, with disclosed Claude Code assistance, supplies + central-operator/idempotent context; #4617 and **lee-phys #4634** retain + their binary dimension/sharpness contributions. +- **Mihir Srivastava #4689**, **codyw912 #4735**, **MatShep #4762**, + **Nick Petalas #4915**, and **JoyboyBrian #5072** supply the distinct residual + census, recurrence, descriptor, orbit weights and scalar incidence work. + Those quantities are not repeated here. **Krzysztof Wojt #5128** supplies + arbitrary-pivot dimension minima, a different obligation. +- **Cinna Davis #4100** and the retained source527, commdata2338 and Jose + Manuel normalizer lineage supply the BIT/header context. + +Substantial predecessor AI-assistance disclosures and Apache-2.0 credit are +retained in their unchanged sources. No shared code, frozen evidence, existing +package, priority or selected-frontier file is modified. + +## Open next questions + +The block-central identity is closed at this scope. A next useful question is +whether, for one specified singular H, the extension of the restricted pair +on im K to the whole residual can be classified and weighted. Start with the +ternary H=J3 example above: its central nilpotency grows from three to four. +The missing data are how the complementary residual directions attach to +im K, and their split/header multiplicities. The present theorem is not a +complete state invariant or transition law; another dimension scan is not +needed to answer it. No follow-up claim is held. + +Nonidentity block pivots and subsequent noncommuting deletions require new +hypotheses and a new derivation. Physical production separately needs a named +header cover and priced selection/emission, reads, ownership, dirty restoration, +precision, storage, stock, dispatch and the complete consumer bill. Those costs +remain unknown, not zero. This session stops at the one-deletion theorem. diff --git a/research/schur-block-central-law/SOURCES.json b/research/schur-block-central-law/SOURCES.json new file mode 100644 index 0000000000..e859748925 --- /dev/null +++ b/research/schur-block-central-law/SOURCES.json @@ -0,0 +1,48 @@ +{ + "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/schur-central-spectrum/README.md", + "usage": "provenance", + "git_blob": "29444eb40edd3fb9dd0cb606f5ba5e84a3f69c86", + "sha256": "f2d8568923f9762da88c7dcc8d29266ef5d8fe518bf7884ab5984c8949923620" + }, + { + "path": "research/all-field-identity-schur/README.md", + "usage": "provenance", + "git_blob": "c3a64475cc52ba7025d57d2c1a810a35c563ca40", + "sha256": "e702c6e05e3283363294ed10a1b9bc4b589c46cc2fb7df198ec9c6841ec78f78" + }, + { + "path": "research/block-schur-commutator/README.md", + "usage": "provenance", + "git_blob": "79790ccea54cfea1aab611768927651a81f2fb18", + "sha256": "945c1420fe9fb5c26dec49e7d6005d77382ca9dc6ca0f424d8baa1500bfc092c" + }, + { + "path": "research/identity-pivot-sector-bound/README.md", + "usage": "provenance", + "git_blob": "80c587372713ca47a79d4880dab330e642c3a25a", + "sha256": "c997446a1fc4683694987feea5f2a8423b57d48d5513a27e178f84ecf56ffc12" + }, + { + "path": "research/schur-projector-refinement/README.md", + "usage": "provenance", + "git_blob": "c6fc0e77d9f1022d519df8e3d8266672df793adb", + "sha256": "7edb11d24ffd6fa4604ebfa9d27215d74a684ea23a484a0cf36a970f08571232" + } + ] +} diff --git a/research/schur-block-central-law/TASK.json b/research/schur-block-central-law/TASK.json new file mode 100644 index 0000000000..6f489dd3e1 --- /dev/null +++ b/research/schur-block-central-law/TASK.json @@ -0,0 +1,198 @@ +{ + "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": "Prove the ordered identity-block Schur central intertwiner with two copies of Theta=2H-H^2, its annihilator laws, and the exact sharp restricted representation over every field.", + "scope_change_reason": "Take Open next question 2 of Nick Petalas #4801 as a written algebraic side theorem; the earlier residual census, descriptor and scalar-incidence handoffs have been completed by credited successors. This is not a formalization or selected supplier audit.", + "bottleneck_link": "An exact restricted residual-state constraint for later Schur/header recursion. It supplies neither a complete conjugacy classifier nor a priced physical header cover.", + "budget_minutes": 60, + "stop_rule": "Stop after the ordered block identity, sharp restriction and bounded singular/nonsharp controls. No new dimension scan, full-guard census or automatic supplier expansion.", + "outcome": "completed", + "evidence": "README.md contains a self-contained all-field proof. verify.py checks all 1244 prescribed products in seven finite domains, all 1472 small nonsharp commuting binary pairs, four Jordan/minimal-polynomial fixtures and nine controls.", + "author": "ssafwann", + "ai_assistance": "Substantial OpenAI Codex (gpt-6-astra) assistance, one agent; no independent human or proof-kernel acceptance.", + "open_questions": [ + { + "question": "How does the restricted pair on im K extend to the full residual for one specified singular H, with what split/header multiplicities?", + "why_it_matters": "The exact restricted representation alone cannot supply a full residual-state transition law.", + "first_step": "Classify the complementary attachments in the ternary H=J3 fixture, where central nilpotency grows from three to four.", + "blocked_by": "Extension data, multiplicities and a sufficient whole-state invariant remain unknown; physical cover and complete costs remain separate." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4653", + "handoff_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19147366", + "assignment_seed": "1af73a39980cf518fa63c60070e08343", + "family_decision": { + "decision": "narrow", + "contract": "Commuting field idempotents with common I_d pivot -> one residual pair S,T and central Z=(S-T)^2.", + "proved": "Ordered block action, annihilator laws and sharp restricted similarity, by the written proof; finite corroboration only for the listed prime-field domains.", + "unknown_costs": [ + "header selection/emission", + "physical reads", + "owned/borrowed storage", + "dirty restoration", + "precision", + "stock", + "dispatch", + "complete consumer bill" + ], + "alternative_considered": "Live native-fusion and CRT work has different physical contracts; do not duplicate the completed residual census or scalar incidence formula.", + "reopen": "A specified extension/state-transition problem or actual caller/cover contract with cost allowance." + }, + "overlap": { + "initial": { + "local": { + "head": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "records": 7091, + "head_records": 7091, + "complete_head_inventory": true, + "unsearched_head_paths": [] + }, + "open_prs": { + "fetched_at": "2026-10-23T14:06:13.126191+00:00", + "complete_pagination": true, + "records": 319 + }, + "discussions": { + "fetched_at": "2026-10-23T14:08:46.663587+00:00", + "complete_pagination": true, + "records": 4505 + } + }, + "result": "Located #4801 explicit block question and completed successors; no duplicate block-central law found within coverage.", + "related_scopes": { + "4801": "scalar central polynomial and explicit block question", + "4746": "all-field identity-pivot minimum and fixture construction", + "5128": "arbitrary invertible block-pivot dimension minimum", + "4689": "one binary residual state census", + "4735": "binary recurrence and terminal invariant", + "4762": "arbitrary idempotent factor descriptor", + "4915": "centralizer/orbit multiplicities", + "5072": "binary scalar sector incidence" + }, + "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.", + "final": { + "local": { + "head": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "records": 7093, + "head_records": 7091, + "complete_head_inventory": true, + "unsearched_head_paths": [] + }, + "open_prs": { + "fetched_at": "2026-10-23T14:19:11.601875+00:00", + "complete_pagination": true, + "records": 322 + }, + "discussions": { + "fetched_at": "2026-10-23T14:21:51.751176+00:00", + "complete_pagination": true, + "records": 4520 + } + } + }, + "predecessor_heads": { + "4801": "98bc071317b17fd8bb4f21044328914c7561d3cb", + "4746": "5f014560d6225cae17598ac479fb29d2947d8e6b", + "4597": "dfeb8ca729a04aea4aa290438f2ed50a37a9c7cb", + "4671": "8d2e3bc76aa7d43e5c629daaf1e72d4dd5a81ed9", + "5072": "6896b92a34b6db839a7ba0ddfa0159f56af5c148", + "5128": "2839d35e58b3285a1992a3ecbae2809ebef7661b" + }, + "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": { + "registered": "Both isolated warning-strict normal and optimized commands passed on CPython 3.12.11; combined wall time 6.32 seconds.", + "direct_normal_seconds": 3.18, + "proof_review": "Single-agent reread of the ordered full-space expansion, restricted action and polynomial implications; no separate reviewer or proof-kernel acceptance." + }, + "upstream_checkpoint": { + "commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "checked_utc": "2026-10-23T14:19:03Z", + "change": "Canonical main unchanged; guidance, selected record and immediate source paths unchanged." + } +} diff --git a/research/schur-block-central-law/VERIFY.json b/research/schur-block-central-law/VERIFY.json new file mode 100644 index 0000000000..2f306f81ca --- /dev/null +++ b/research/schur-block-central-law/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": "Literal full matrices: ordered block actions, central/annihilator laws, exact sharp restricted minimal polynomial, nonsharp domains, four Jordan fixtures and nine rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Literal full matrices: ordered block actions, central/annihilator laws, exact sharp restricted minimal polynomial, nonsharp domains, four Jordan fixtures and nine rejection controls." + } + ] +} diff --git a/research/schur-block-central-law/verify.py b/research/schur-block-central-law/verify.py new file mode 100644 index 0000000000..7bfce0e512 --- /dev/null +++ b/research/schur-block-central-law/verify.py @@ -0,0 +1,327 @@ +#!/usr/bin/env python3 +"""Block Schur central-action law: exact finite corroboration. + +ssafwann with substantial OpenAI Codex assistance. Apache-2.0. +Sector fixtures follow Petalas #4746 and ssafwann #4671; ordered factors +follow Petalas #4597. No predecessor executable is imported. +""" +from itertools import product +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 matrices(q, d): + require(q in (2, 3, 5) and 0 < d <= 3 and q**(d*d) <= 625, + 'census capacity') + for data in product(range(q), repeat=d*d): + yield tuple(tuple(data[i*d:(i+1)*d]) for i in range(d)) + + +def complete_factor(t, q): + """X=[T,N] is onto, Y=[I;0] is injective, XY=T (#4746).""" + d = len(t) + x = t + for j in range(d): + trial = tuple(row+(int(i == j),) for i, row in enumerate(x)) + if rank(trial, q) > rank(x, q): + x = trial + y = eye(d) + zero(len(x[0])-d, d) + require(rank(x, q) == d and mul(x, y, q) == t, 'factor fixture') + return x, y + + +def construct(h, q): + """A sharp full pair with H prescribed; the 00 sector is padded to d.""" + d = len(h) + w = add(eye(d), h, q, -1) + factors = [(add(zero(d, d), w, q, -1), eye(d))] + factors += [complete_factor(t, q) for t in (w, w, h)] + x = tuple(sum((factor[0][i] for factor in factors), ()) for i in range(d)) + y = sum((factor[1] for factor in factors), ()) + sizes = tuple(len(factor[1]) for factor in factors) + require(mul(x, y, q) == eye(d), 'split construction') + basis = tuple(a+b for a, b in zip(y, kernel(x, q))) + inv = inverse(basis, q) + sectors = sum(((j,)*s for j, s in enumerate(sizes)), ()) + p0 = tuple(tuple(int(i == j and sectors[i] in (1, 3)) + for j in range(len(y))) for i in range(len(y))) + q0 = tuple(tuple(int(i == j and sectors[i] in (2, 3)) + for j in range(len(y))) for i in range(len(y))) + return mul(mul(inv, p0, q), basis, q), mul(mul(inv, q0, q), basis, q) + + +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 poly(a, coefficients, q): + out = zero(len(a), len(a)) + for c in reversed(coefficients): + out = add(mul(out, a, q), eye(len(a)), q, c) + return out + + +def minimal_polynomial(a, q): + """First exact linear dependence of I,A,...,A^d; no root sampling.""" + d = len(a) + powers = [eye(d)] + for degree in range(1, d+1): + powers.append(mul(powers[-1], a, q)) + system = tuple(tuple(p[i][j] for p in powers[:-1]) + + (-powers[-1][i][j] % q,) + for i in range(d) for j in range(d)) + reduced, pivots = rref(system, q, degree) + if any(not any(row[:degree]) and row[degree] for row in reduced): + continue + require(len(pivots) == degree, 'first dependence uniqueness') + coefficients = tuple(reduced[i][-1] for i in range(degree)) + (1,) + require(poly(a, coefficients, q) == zero(d, d), 'annihilator computation') + return coefficients + raise ValueError('no minimal polynomial by dimension') + + +def inspect_pair(p, t, d, q): + n = len(p) + require(q in (2, 3, 5) and 1 <= d < n <= 18, 'field/dimension contract') + require(all(len(row) == n for row in p+t) and len(t) == n, 'square pair') + require(mul(p, p, q) == p and mul(t, t, q) == t, 'idempotent premise') + pq = mul(p, t, q) + require(pq == mul(t, p, q), 'commuting premise') + require(tuple(row[:d] for row in p[:d]) == eye(d) and + tuple(row[:d] for row in t[:d]) == eye(d), 'identity pivot premise') + h = tuple(row[:d] for row in pq[:d]) + s, u = schur(p, d, q), schur(t, d, q) + m = n-d + a1 = add(tuple(row[:d] for row in pq[d:]), + mul(tuple(row[:d] for row in t[d:]), h, q), q, -1) + a2 = add(tuple(row[:d] for row in p[d:]), + tuple(row[:d] for row in t[d:]), q, -1) + a = tuple(x+y for x, y in zip(a1, a2)) + b1 = add(tuple(row[d:] for row in p[:d]), tuple(row[d:] for row in t[:d]), q, -1) + b2 = add(mul(h, tuple(row[d:] for row in t[:d]), q), + tuple(row[d:] for row in pq[:d]), q, -1) + c = add(mul(s, u, q), mul(u, s, q), q, -1) + delta = add(s, u, q, -1) + z = mul(delta, delta, q) + w, j = add(eye(d), h, q, -1), add(h, mul(h, h, q), q, -1) + ks = block(w, add(zero(d, d), eye(d), q, -1), + add(zero(d, d), j, q, -1), h) + kt = block(eye(d), eye(d), zero(d, d), zero(d, d)) + theta = add(add(h, h, q), mul(h, h, q), q, -1) + theta2 = block(theta, zero(d, d), zero(d, d), theta) + require(mul(s, s, q) == s and mul(u, u, q) == u, 'residual idempotents') + require(mul(a, b1+b2, q) == c, 'ordered Schur factorization') + require(mul(s, a, q) == mul(a, ks, q), 'S action') + require(mul(u, a, q) == mul(a, kt, q), 'T action') + require(mul(z, a, q) == mul(a, theta2, q), 'block central intertwiner') + require(mul(z, s, q) == mul(s, z, q) and mul(z, u, q) == mul(u, z, q), + 'centrality') + require(mul(c, c, q) == mul(z, add(z, eye(m), q, -1), q), 'C squared') + mp = minimal_polynomial(theta, q) + pz = poly(z, mp, q) + require(mul(pz, c, q) == zero(m, m), 'commutator annihilator') + require(mul(mul(z, add(z, eye(m), q, -1), q), pz, q) == zero(m, m), + 'whole residual annihilator') + return {'h': h, 's': s, 't': u, 'a': a, 'c': c, 'z': z, + 'theta': theta, 'mp': mp, 'n': n, 'd': d, 'q': q} + + +def sharp_checks(data): + q, d, c, z = (data[k] for k in ('q', 'd', 'c', 'z')) + require(rank(c, q) == 2*d and rank(data['a'], q) == 2*d, 'sharp fixture') + powers = [c] + for _ in range(len(data['mp'])-2): + powers.append(mul(z, powers[-1], q)) + flat = tuple(tuple(x for row in p for x in row) for p in powers) + require(rank(flat, q) == len(data['mp'])-1, 'exact restriction minimal polynomial') + + +def jordan_check(data): + q, d, c, z, theta = (data[k] for k in ('q', 'd', 'c', 'z', 'theta')) + rows = [] + for lam in range(q): + left, right = c, eye(d) + zl = add(z, eye(len(z)), q, -lam) + tl = add(theta, eye(d), q, -lam) + ranks = [] + for _ in range(d+2): + require(rank(left, q) == 2*rank(right, q), 'doubled Jordan rank sequence') + ranks.append(rank(left, q)) + left, right = mul(zl, left, q), mul(tl, right, q) + rows.append(ranks) + return rows + + +def exhaustive_nonsharp(n, d): + free = [(i, j) for i in range(n) for j in range(n) if i >= d or j >= d] + projectors = [] + for values in product(range(2), repeat=len(free)): + p = [list(row) for row in eye(n)] + for (i, j), value in zip(free, values): + p[i][j] = value + p = tuple(tuple(row) for row in p) + if mul(p, p, 2) == p: + projectors.append(p) + count, histogram = 0, {} + for p in projectors: + for t in projectors: + if mul(p, t, 2) == mul(t, p, 2): + data = inspect_pair(p, t, d, 2) + r = rank(data['c'], 2) + histogram[r] = histogram.get(r, 0)+1 + count += 1 + return {'n': n, 'd': d, 'pairs': count, 'commutator_ranks': histogram} + + +def rejected(call, label): + try: + call() + except ValueError: + return label + raise ValueError('control accepted: '+label) + + +def controls(nilpotent, ternary, odd, nonscalar): + z, c = nilpotent['z'], nilpotent['c'] + out = [] + out.append(rejected(lambda: require(mul(z, c, 2) == zero(len(z), len(z)), + 'square-free replacement'), 'drop repeated root')) + z3 = ternary['z'] + out.append(rejected(lambda: require(poly(z3, ternary['mp'], 3) == zero(len(z3), len(z3)), + 'whole-space overclaim'), 'omit endpoint factors')) + a, h = nonscalar['a'], nonscalar['h'] + bad = block(h, zero(len(h), len(h)), zero(len(h), len(h)), h) + out.append(rejected(lambda: require(mul(nonscalar['z'], a, 2) == mul(a, bad, 2), + 'H in place of Theta'), 'replace Theta by H')) + h = odd['h'] + bad_theta = add(add(h, h, 5), mul(h, h, 5), 5) + bad = block(bad_theta, zero(2, 2), zero(2, 2), bad_theta) + out.append(rejected(lambda: require(mul(odd['z'], odd['a'], 5) == mul(odd['a'], bad, 5), + 'wrong odd-field sign'), 'replace minus by plus')) + identity = inspect_pair(eye(3), eye(3), 1, 2) + out.append(rejected(lambda: sharp_checks(identity), 'drop sharpness hypothesis')) + out.append(rejected(lambda: inspect_pair(eye(3), zero(3, 3), 1, 2), 'zero pivot')) + badp = ((1, 1, 0), (0, 0, 1), (0, 0, 0)) + out.append(rejected(lambda: inspect_pair(badp, eye(3), 1, 2), 'nonidempotent input')) + p = ((1, 0, 0), (0, 1, 0), (0, 0, 0)) + t = ((1, 0, 0), (0, 0, 0), (0, 1, 1)) + out.append(rejected(lambda: inspect_pair(p, t, 1, 2), 'noncommuting inputs')) + out.append(rejected(lambda: list(matrices(3, 3)), 'census capacity')) + return out + + +def main(): + coverage = [] + for q, d in ((2, 1), (2, 2), (2, 3), (3, 1), (3, 2), (5, 1), (5, 2)): + count = 0 + for h in matrices(q, d): + p, t = construct(h, q) + data = inspect_pair(p, t, d, q) + require(data['h'] == h, 'prescribed compressed product') + sharp_checks(data) + count += 1 + coverage.append({'q': q, 'd': d, 'all_H': count}) + fixtures = [] + for q, h in ((2, ((0, 1, 0), (0, 0, 1), (0, 0, 0))), + (3, ((0, 1, 0), (0, 0, 1), (0, 0, 0))), + (5, ((0, 1), (1, 1))), + (2, ((0, 1), (1, 1)))): + data = inspect_pair(*construct(h, q), len(h), q) + sharp_checks(data) + data['jordan_ranks'] = jordan_check(data) + data['whole_mp'] = minimal_polynomial(data['z'], q) + fixtures.append(data) + extra = [exhaustive_nonsharp(3, 1), exhaustive_nonsharp(4, 2)] + require([x['pairs'] for x in extra] == [253, 1219], 'credited small-domain sizes') + require(fixtures[0]['mp'] == (0, 0, 1), 'binary nilpotent fixture') + require(fixtures[1]['mp'] == (0, 0, 0, 1) and + fixtures[1]['whole_mp'] == (0, 0, 0, 0, 1), 'ternary endpoint multiplicity') + failure_controls = controls(*fixtures) + receipt = {'sharp_H_domains': coverage, 'nonsharp_domains': extra, + 'fixtures': [{k: data[k] for k in ('q', 'd', 'n', 'h', 'theta', 'mp', 'whole_mp', 'jordan_ranks')} + for data in fixtures], 'rejected_controls': failure_controls} + print(json.dumps(receipt, sort_keys=True, indent=2)) + print('PASS_SCHUR_BLOCK_CENTRAL_LAW') + + +if __name__ == '__main__': + main()