From f69863ddefafa183babe2b59a8e5c91a92786fd1 Mon Sep 17 00:00:00 2001 From: Mihir Srivastava Date: Fri, 23 Oct 2026 12:15:23 -0700 Subject: [PATCH 1/2] Prove primary gluing for sharp ordered Schur residuals --- research/schur-primary-gluing/README.md | 307 +++++++++++++ research/schur-primary-gluing/SOURCES.json | 48 ++ research/schur-primary-gluing/TASK.json | 175 ++++++++ research/schur-primary-gluing/VERIFY.json | 34 ++ research/schur-primary-gluing/verify.py | 482 +++++++++++++++++++++ 5 files changed, 1046 insertions(+) create mode 100644 research/schur-primary-gluing/README.md create mode 100644 research/schur-primary-gluing/SOURCES.json create mode 100644 research/schur-primary-gluing/TASK.json create mode 100644 research/schur-primary-gluing/VERIFY.json create mode 100644 research/schur-primary-gluing/verify.py diff --git a/research/schur-primary-gluing/README.md b/research/schur-primary-gluing/README.md new file mode 100644 index 0000000000..f828cc5923 --- /dev/null +++ b/research/schur-primary-gluing/README.md @@ -0,0 +1,307 @@ +# Primary gluing for the whole ordered Schur residual + +**Scoped written proof with exact finite corroboration.** For a sharp common +identity-block Schur deletion over any field, the compressed matrix H and the +four original ordered sector dimensions determine one simultaneous-conjugacy +orbit of the entire ordered residual pair. No extra sector00 factor invariant +survives. This finishes the general-H gluing question left by +[Ali Romman's #5348](https://github.com/CrocSwap/integer-mult-bounds/pull/5348), +following [ssafwann's #5267](https://github.com/CrocSwap/integer-mult-bounds/pull/5267) +and [the released handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/5337). + +The new step is a constructive decomposition of the sector factors, especially +sector00, followed by explicit full residual intertwiners. The sector-capacity +criterion, full-rank factor extension lemma, and H=1 normal form retain +predecessor credit. We also justify the earlier nilpotent formula on the entire +W-invertible component; nilpotence is not assumed there. + +This is an algebraic side result for one deletion, not a physical supplier or +an improvement to kappa. Distinct H/profile data may yield the same residual +orbit: the result is sufficiency of fixed data, not an injective classification +of all parameter choices. The selected conditional kappa remains 0.00302015. + +## Contract and explicit representative + +Work over any field F. Let P0,Q0 be commuting idempotents on V, with ordered +joint sectors V00,V10,V01,V11 of dimensions r00,r10,r01,r11. Let +i:U->V and pi:V->U, U=F^d, d>=1, satisfy + +```text +pi i = pi P0 i = pi Q0 i = I, H = pi P0 Q0 i. +``` + +In any header M=[i,B] with B a basis of ker pi, write + +```text +M^-1 P0 M = [I b; c D], M^-1 Q0 M = [I f; g E], +S=D-cb, T=E-gf. +``` + +Require rank(ST-TS)=2d. Put W=I-H, a0=nullity H and a1=nullity W. +We retain Nick Petalas's [#4746](https://github.com/CrocSwap/integer-mult-bounds/pull/4746) +sharp criterion and capacity theorem: + +```text +r00 >= d-a1, +r10 = d+a1+s10, r01 = d+a1+s01, r11 = d+a0+s11, s10,s01,s11 >= 0. (1) +``` + +Every profile (1) is attainable for the prescribed H. This is a cited result, +not a new dimension minimum. The source construction permits larger r00 by +adding unused sector00 directions. + +Use the Fitting decomposition for W, without a splitting-field extension: + +```text +U = Uc direct-sum U1, Uc=im W^d, U1=ker W^d, +dc=dim Uc, d1=dim U1, +H=Hc direct-sum H1, Wc=I-Hc invertible, W1=I-H1 nilpotent. (2) +``` + +Thus H1 is invertible, nullity Hc=a0 and nullity W1=a1. Choose +N0:F^a0->Uc complementing im Hc, and N1:F^a1->U1 complementing im W1. +Zero-dimensional components and empty blocks are allowed. + +On Uc^3 direct-sum F^a0 define + +```text +Sc(x,y,z,t) = (Hc(x-z)-N0t, 0, Wc(z-x)-N0t, t), +Tc(x,y,z,t) = (0, Hc(y-z)-N0t, Wc(z-y)-N0t, t). (3) +``` + +On E1=U1 direct-sum F^a1 put A=[W1 N1; 0 0]. On E1 direct-sum E1 set + +```text +S1(u,v)=(u+Av,0), T1(u,v)=(0,Au+v). (4) +``` + +**Theorem.** Every admitted ordered residual (S,T) is simultaneously similar to + +```text +(Sc,Tc) direct-sum (S1,T1) + direct-sum (0,0)^(r00-dc) + direct-sum (1,0)^s10 direct-sum (0,1)^s01 direct-sum (1,1)^s11. (5) +``` + +Here r00-dc>=d1-a1>=0. Its dimension is + +```text +(3dc+a0) + 2(d1+a1) + (r00-dc) + s10+s01+s11 + = r00+r10+r01+r11-d. +``` + +All choices of primary bases and complements give the same ordered-pair +orbit. The formula includes arbitrary characteristic, repeated primary factors, +and irreducible factors that do not split over F. It never divides by two. + +## Proof + +### Source factors and active sectors + +Let E_j be the original joint-sector projectors, Y_j=E_j i and X_j=pi|V_j. +The source equations are + +```text +X00Y00=-W, X10Y10=W, X01Y01=W, X11Y11=H. (6) +``` + +The source sharp criterion says that Y10,Y01,Y11 are injective and +X10,X01,X11 are onto. It imposes no such requirement in sector00. + +For onto X and injective Y with XY=B, choose the columns Y of a basis of U, +then lifts under X of a basis N complementing im B, then a basis of the +remaining kernel directions. The resulting coordinates give + +```text +X=[B N 0], Y=[I;0;0]. (7) +``` + +Indeed im Y intersects ker X in Y ker B. The added lifts are independent +modulo im Y+ker X, and the remaining ker X directions complete the basis. +This is the full-rank extension principle of codyw912 #4735 and MatShep #4762, +also specialized explicitly in #5267; it is a credited lemma. + +Under (2), choose N separately in Uc and U1. For sectors10 and01, only U1 +needs the a1 extra lift directions because Wc is invertible. For sector11, +only Uc needs the a0 extra directions because H1 is invertible. Each active +sector splits into its two primary factor systems and s_j unused directions. +The unused directions give the last three scalar summands in (5). + +### Splitting the arbitrary sector00 factor + +This step cannot be replaced by applying (7) to sector00: its maps can have +deficient ranks. Write X=X00, Y=Y00 and let Pc:U->Uc be the projection in (2). +Since XY=-W, Y|Uc is injective. Define + +```text +J = (Y|Uc) (-Wc)^-1 Pc X : V00 -> V00. (8) +``` + +For u in Uc, JYu=Yu. Thus J is the projection onto YUc and + +```text +V00 = YUc direct-sum V001, V001=ker(Pc X). (9) +``` + +Consequently dim V001=r00-dc. The map X sends V001 into U1, and Y sends U1 +into V001 because Pc X Y|U1=-Pc W|U1=0. Choosing coordinates on YUc via Y gives + +```text +X00 = (-Wc) direct-sum X1, Y00 = I direct-sum Y1, +X1Y1=-W1. (10) +``` + +No rank assumption on X1 or Y1 was added. This also covers absent primary +components. The classical Fitting decomposition is applicable because the +image and kernel of W^d are stable, disjoint and have complementary dimensions; +W is invertible on the image and nilpotent on the kernel. All operations in +(8)-(10) are over F. + +Together with the active-sector construction, both i and pi respect Uc+U1 +and the corresponding ambient decomposition. P0,Q0 respect it too, since all +ambient basis changes occur within original joint sectors. Concatenating bases +of the two kernels makes the entire Schur residual a direct sum of the two +residuals and the active scalar padding. This proves the primary gluing before +any central-spectrum argument. + +### The W-invertible component needs no nilpotence assumption + +Its normalized factors are + +```text +X00=-Wc, X10=X01=Wc, X11=[Hc N0], +Y00=Y10=Y01=I, Y11=[I;0]. (11) +``` + +The kernel of their combined projection is parametrized by + +```text +(v00,v10,v01,v11,extra11) + = (x+y+Wc^-1 Hc z+Wc^-1 N0 t, x, y, z, t). (12) +``` + +On ker pi the residual of P0 is the restriction of P0-P0 i pi P0, and +similarly for Q0. These maps preserve ker pi because the common pivot is I. +In (12), pi P0 equals Wc x+Hc z+N0t. Subtracting its injection from the active +sectors gives Sc in (3); Q0 gives Tc. Nilpotence of Hc was not used: invertible +Wc is sufficient. This justifies extending the displayed model from #5267. +Its nilpotent Jordan and weight claims are not generalized here. + +### The remaining sector00 data disappear on U1 + +Retain X1,Y1 in (10). For ambient coordinates (v,x,b,y,c,z) in +V001,U1,F^a1,U1,F^a1,U1, solve the kernel equation using invertible H1: + +```text +z = -H1^-1(X1v+W1x+N1b+W1y+N1c). (13) +``` + +The literal residual maps on the five free coordinates are + +```text +S(v,x,b,y,c)=(0, x+X1v+W1y+N1c, b, 0, 0), +T(v,x,b,y,c)=(0, 0, 0, y+X1v+W1x+N1b, c). (14) +``` + +Y1 has disappeared. Put C=(I+W1)^-1, which exists over every field since W1 +is nilpotent. The invertible change + +```text +xbar=x+C X1v, ybar=y+C X1v (15) +``` + +removes X1v from both formulas because (I+W1)C=I. The v directions become a +common zero summand of dimension r00-dc; the remaining maps are (4). This is +#5348's coordinate removal, applied after the justified split (9), without +assuming invertibility of I+W on all of U. + +These steps prove (5) and construct an intertwiner. Compose the sector basis +changes with (12), (13), and the inverse of (15). All component maps are +invertible onto their claimed spaces. Express the resulting columns in any +header's ker pi basis to obtain invertible G with SG=GScan and TG=GTcan. +Mapping two admitted residuals to the same (5) proves the fixed-data orbit +statement. Choosing other complements or bases constructs another such map. + +## Exact checks and reproduction + +The standalone standard-library checker imports no predecessor code. It +constructs i,pi and diagonal P0,Q0, chooses a separate nullspace header M, +inverts M and computes both literal Schur complements. It constructs the proof's +embedding separately and checks invertible G, SG=GScan and TG=GTcan. Input +pivots, H, idempotence, original commutation and sharp rank are also checked. +Matching central spectra would not suffice. + +- **111 complete H-domain cases:** every d=1,2 matrix over F2/F3 and every + d=1 matrix over F4/F5, using the credited attaining factors. +- **364 arbitrary sector00 factor pairs:** every X in M_(d,r00) and Y in + M_(r00,d), with H=I+XY, for F2,d=2,r00=0,1,2 and F3,d=1,r00=0,1,2. + The active sectors use full-rank factors; deterministic invertible shears + change sector bases. Deficient sector00 maps remain permitted. +- **40 larger fixtures:** mixed primary components, Jordan blocks through + size three, repeated quadratic components, changed leading/sector bases and + scalar padding over F2,F3,F4,F5. The quadratic x^2-x-1 is irreducible over + F2/F3, so some fixtures genuinely cover nonsplit repeated factors. +- **Eight controls:** missing (15), globally singular W, wrong sector00 sign, + a deficient active factor, an unstabilized Fitting split, wrong scalar + padding, an empty leading block, and omission of the sector profile. + +F4 is F2[t]/(t^2+t+1), not integers modulo four. Explicit exceptions remain +enabled under optimized Python. The checker prints executed domain counts, a +fixture digest and `PASS_SCHUR_PRIMARY_GLUING`; it accesses no network/Git and +writes no files. The arbitrary-field theorem rests on the written proof and +cited sharp-sector lemma; finite tests are corroboration, not proof-kernel or +independent human acceptance. + +From the repository root with Python 3.12: + +```sh +python -B scripts/research_package.py --package research/schur-primary-gluing +python -I -W error -B research/schur-primary-gluing/verify.py +python -I -W error -O -B research/schur-primary-gluing/verify.py +``` + +Registered commands run serially with a 60-second cap each. Source provenance +is pinned in `SOURCES.json`; the checker has no external runtime inputs. +`TASK.json` records scope, overlap and remaining obligations. Committed-byte +and export checks are recorded in the PR rather than embedding a self-commit. + +No Lean, Docker, native operator, selected cold replay, physical stock/caller, +compiler or multiplication-theorem audit is part of this package. Selected +orientation reported sparse omissions, not a baseline pass. The selected +record, certificate, manifest and review were read; this result does not consume +their scientific inputs. + +## Open next questions + +Fixed-H/profile sufficiency is closed by the stated proof. A distinct question +is whether two different parameter data yield the same ordered residual orbit. +Begin with (5) on specified profiles only if a named consumer actually needs +state deduplication. No injectivity or full orbit algorithm is supplied, and no +larger census is proposed without that need. + +Header probabilities, later-guard survival and physical use remain separate. +Before expanding into a supplier, name a consumer and its complete cost +allowance: selection/emission, reads, restoration, precision, storage, stock +and dispatch remain unknown. A local normal form does not make them zero. +Stop this contribution at the gluing result. + +## Attribution + +Prepared for **Mihir Srivastava (@mihir-s-05)** with substantial **OpenAI Codex** +assistance, one agent; Apache-2.0. No literature-wide novelty claim is made. + +- **ssafwann #5267:** nilpotent whole-residual rigidity, explicit model and + full-rank factor specialization. Its Jordan/weight claims retain their scope. +- **Ali Romman #5348:** H=1 ordered normal form and sector00 removal. + **#5287** already answers the whole-central-class and characteristic-two + questions; those are not new claims here. +- **Nick Petalas #4746/#4597:** signed sector criterion, attaining construction + and ordered Schur factorization. **MatShep #4762** and **codyw912 #4735**: + factor-system extension and the sufficient-invariant question. +- **JoyboyBrian:** released general-H handoff. **Ryanson Jonathan, lee-phys, + ssafwann's earlier work, Cinna Davis, source527, commdata2338 and Jose Manuel** + retain the Schur, dimension, header, BIT and normalizer lineage credited in + the pinned sources. Fitting decomposition and basis extension are classical. + +Predecessors are archived, partially reviewed contributions; merging is not +scientific acceptance. Their frozen files and attribution remain unchanged. diff --git a/research/schur-primary-gluing/SOURCES.json b/research/schur-primary-gluing/SOURCES.json new file mode 100644 index 0000000000..c9c84b11ac --- /dev/null +++ b/research/schur-primary-gluing/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "7c472563474e60185e6ca101a17622133d047e56", + "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-nilpotent-extension/README.md", + "usage": "provenance", + "git_blob": "1e738614a419c8f91941886179bdf235e4e5ed52", + "sha256": "7e5e74f4e5ddc1793ac6e427a80492d8d978aa78f01f189e33d2831147c9639a" + }, + { + "path": "research/unipotent-ordered-schur/README.md", + "usage": "provenance", + "git_blob": "ec69444b2ee172fa69b781fcba9347c01801c566", + "sha256": "2129db3ec31fde78d0e3533cfdbc47214810a3bf01c53783fabb1d929b1d65e3" + }, + { + "path": "research/schur-whole-central-class/PROOF.md", + "usage": "provenance", + "git_blob": "223069d517d14758c5b71e90295065bdd5568f3a", + "sha256": "24d54ea4de5c1d6e33bb1bf65898f13bf20bae5f6f60cb52f338724e76d5f84c" + } + ] +} diff --git a/research/schur-primary-gluing/TASK.json b/research/schur-primary-gluing/TASK.json new file mode 100644 index 0000000000..83c22fda40 --- /dev/null +++ b/research/schur-primary-gluing/TASK.json @@ -0,0 +1,175 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "7c472563474e60185e6ca101a17622133d047e56", + "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 general-H primary gluing and construct full ordered residual intertwiners for sharp common identity-block Schur deletion over arbitrary fields, with fixed H and ordered input sector dimensions.", + "scope_change_reason": "Handoff-first override: Discussion 5337 and PR5348 leave this algebraic implication open. This is a written side-result proof with exact finite corroboration, not Lean formalization or a selected-caller audit.", + "bottleneck_link": "Removes a stated ambiguity in an algebraic residual-state interface. A consumer and full physical bill are absent; no supplier or kappa gain follows.", + "budget_minutes": 60, + "stop_rule": "Stop after the primary-gluing proof and bounded exact intertwiners, or a counterexample. No state census expansion, header weights, physical implementation or selected-frontier edit.", + "outcome": "completed", + "evidence": "README gives a constructive arbitrary-field proof under the credited sharp-sector criterion. verify.py checks 111 complete-H cases, 364 arbitrary sector00 factor pairs, 40 mixed/padded fixtures and eight controls using literal Schur complements and invertible intertwiners for both ordered maps. Finite tests are corroboration, not human or proof-kernel acceptance.", + "author": "Mihir Srivastava (@mihir-s-05)", + "ai_assistance": "Substantial OpenAI Codex assistance for proof development, independent checker implementation, verification and documentation; one agent, no subagents.", + "open_questions": [ + { + "question": "For a specified consumer, when do two different H/profile data give the same ordered residual orbit?", + "why_it_matters": "Would permit state deduplication if that consumer actually needs it; fixed-data sufficiency is not parameter injectivity.", + "first_step": "Compare the explicit normal forms on a named bounded pair of profiles and retain the full ordered operators.", + "blocked_by": "No named consumer or cost allowance; no new census or implementation campaign is justified here." + } + ], + "claim_type": "scoped written mathematical proof with exact finite corroboration", + "canonical_claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5337#discussioncomment-19152839", + "environment": { + "python": "3.12.0", + "platform": "Windows-11-10.0.26300-SP0", + "dependencies": "standard library only" + }, + "family_gate": { + "decision": "narrow and stop at this result", + "proved": "Primary gluing and fixed-H/profile sufficiency under the cited sharp criterion", + "constructively_upper_bounded": "Finite-dimensional algebraic basis/intertwiner construction; no physical tariff", + "unknown": "Header law, later-guard survival, selection/emission, reads, restoration, precision, storage, stock, dispatch and full consumer costs", + "why_this_step_matters": "Closes the explicit general-H gap left by the H=1 component result, without starting a supplier construction." + }, + "limitations": [ + "No injectivity of H/profile parameters or unconditional orbit weights.", + "No physical supplier/caller, compiler, native, Lean, Docker or selected cold replay.", + "Selected orientation reported 503 sparse-omitted inputs; no baseline pass is claimed.", + "Optional full-history provenance preflight is unavailable in this shallow clone; all declared source pins use the accessible base commit." + ], + "predecessors": [ + { + "pr": 5348, + "author": "Ali Romman", + "head": "3c7650ef0ebf845f8f920c4892fdbbfe2e0bf95b", + "scope": "H=1 ordered normal form and arbitrary sector00 removal" + }, + { + "pr": 5267, + "author": "ssafwann", + "head": "8ab280c8a3ef0544f13ff23a1c69df4757cd4900", + "scope": "Nilpotent whole residual and full-rank factor specialization" + }, + { + "pr": 4746, + "author": "Nick Petalas", + "head": "5f014560d6225cae17598ac479fb29d2947d8e6b", + "scope": "All-field signed sharp-sector criterion and capacity theorem" + }, + { + "pr": 4762, + "author": "MatShep", + "head": "3b4e0449262b0b1e07b80e009ef71cc0ca5bf816", + "scope": "Factor-system extension following codyw912 #4735" + }, + { + "pr": 5287, + "author": "Ali Romman", + "head": "d17a8b3d237a8cb8685cc108bf2bb17dfea0ca78", + "scope": "Already completed whole central class; excluded from new claim" + } + ], + "overlap": { + "scope": "All open PR bodies and Discussions through the reported complete snapshots, plus partial local notes and targeted all-state GitHub Schur/gluing search; relevant predecessor notes materialized and read.", + "open_prs": { + "fetched_at": "2026-10-23T19:00:24.760499+00:00", + "complete_pagination": true, + "records": 305 + }, + "discussions": { + "fetched_at": "2026-10-23T19:02:14.934078+00:00", + "complete_pagination": true, + "records": 4623 + }, + "local": { + "head": "7c472563474e60185e6ca101a17622133d047e56", + "records": 5418, + "head_records": 7267, + "complete_head_inventory": false + }, + "omitted_local_note_paths": 1851, + "nearest": [ + "#5267 nilpotent whole pair", + "#5287 whole central class", + "#5348 H=1 primary whole pair", + "#5337 released general-H gluing" + ], + "added_value": "Justified sector00 primary split, extension of the W-invertible model, and explicit intertwiners that glue the entire ordered pair for arbitrary H.", + "limits": "No matches is not proof of novelty. Local inventory is incomplete; arbitrary historical diffs, nested notes and unpublished work are not covered." + } +} diff --git a/research/schur-primary-gluing/VERIFY.json b/research/schur-primary-gluing/VERIFY.json new file mode 100644 index 0000000000..32e8d2db47 --- /dev/null +++ b/research/schur-primary-gluing/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": 60, + "checks": "Exact full ordered Schur/intertwiner comparisons, mixed and nonsplit primary factors, arbitrary sector00 factors, and eight failure/scope controls" + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Exact full ordered Schur/intertwiner comparisons, mixed and nonsplit primary factors, arbitrary sector00 factors, and eight failure/scope controls" + } + ] +} diff --git a/research/schur-primary-gluing/verify.py b/research/schur-primary-gluing/verify.py new file mode 100644 index 0000000000..6f7adb6388 --- /dev/null +++ b/research/schur-primary-gluing/verify.py @@ -0,0 +1,482 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of general-H ordered Schur primary gluing. + +Mihir Srivastava with substantial OpenAI Codex assistance. Apache-2.0. +Standalone implementation; predecessor proof credit is in README.md. +""" +from dataclasses import dataclass +from itertools import product +import hashlib +import json + + +class CheckError(ValueError): + pass + + +def require(condition, message): + if not condition: + raise CheckError(message) + + +@dataclass(frozen=True) +class Field: + q: int + + def add(self, a, b): + return a ^ b if self.q == 4 else (a + b) % self.q + + def neg(self, a): + return a if self.q == 4 else (-a) % self.q + + def mul(self, a, b): + if self.q != 4: + return a * b % self.q + value = 0 + while b: + if b & 1: + value ^= a + b >>= 1 + a <<= 1 + if a & 4: + a ^= 7 # F4 = F2[t]/(t^2+t+1), not integers modulo 4. + return value + + def inv(self, a): + require(a != 0, "zero field inverse") + return next(b for b in range(1, self.q) if self.mul(a, b) == 1) + + +@dataclass(frozen=True) +class Matrix: + field: Field + rows: int + cols: int + data: tuple + + def __add__(self, other): + require((self.field, self.rows, self.cols) == + (other.field, other.rows, other.cols), "addition shape") + return mat(self.field, self.rows, self.cols, + lambda i, j: self.field.add(self.data[i][j], other.data[i][j])) + + def __neg__(self): + return mat(self.field, self.rows, self.cols, + lambda i, j: self.field.neg(self.data[i][j])) + + def __sub__(self, other): + return self + (-other) + + def __matmul__(self, other): + require(self.field == other.field and self.cols == other.rows, "product shape") + out = [[0] * other.cols for _ in range(self.rows)] + f = self.field + for i in range(self.rows): + for k in range(self.cols): + a = self.data[i][k] + if a: + for j, b in enumerate(other.data[k]): + if b: + out[i][j] = f.add(out[i][j], f.mul(a, b)) + return mat(f, self.rows, other.cols, lambda i, j: out[i][j]) + + def sub(self, r0, r1, c0, c1): + return mat(self.field, r1-r0, c1-c0, lambda i, j: self.data[r0+i][c0+j]) + + def power(self, exponent): + require(self.rows == self.cols and exponent >= 0, "power domain") + result = eye(self.field, self.rows) + for _ in range(exponent): + result = result @ self + return result + + +def mat(f, n, m, value=lambda i, j: 0): + return Matrix(f, n, m, tuple(tuple(value(i, j) for j in range(m)) for i in range(n))) + + +def eye(f, n): + return mat(f, n, n, lambda i, j: int(i == j)) + + +def hcat(*blocks): + f, n = blocks[0].field, blocks[0].rows + require(all(b.field == f and b.rows == n for b in blocks), "horizontal shape") + data = [sum((list(b.data[i]) for b in blocks), []) for i in range(n)] + return mat(f, n, sum(b.cols for b in blocks), lambda i, j: data[i][j]) + + +def vcat(*blocks): + f, m = blocks[0].field, blocks[0].cols + require(all(b.field == f and b.cols == m for b in blocks), "vertical shape") + data = sum((list(b.data) for b in blocks), []) + return mat(f, len(data), m, lambda i, j: data[i][j]) + + +def rref(a): + f = a.field + rows = [list(r) for r in a.data] + pivots = [] + for col in range(a.cols): + row = next((i for i in range(len(pivots), a.rows) if rows[i][col]), None) + if row is None: + continue + p = len(pivots) + rows[p], rows[row] = rows[row], rows[p] + inv = f.inv(rows[p][col]) + rows[p] = [f.mul(inv, x) for x in rows[p]] + for i in range(a.rows): + if i != p and rows[i][col]: + scale = f.neg(rows[i][col]) + rows[i] = [f.add(x, f.mul(scale, y)) for x, y in zip(rows[i], rows[p])] + pivots.append(col) + if len(pivots) == a.rows: + break + return mat(f, a.rows, a.cols, lambda i, j: rows[i][j]), pivots + + +def rank(a): + return len(rref(a)[1]) + + +def columns(a, indices): + return mat(a.field, a.rows, len(indices), lambda i, j: a.data[i][indices[j]]) + + +def kernel(a): + reduced, pivots = rref(a) + free = [j for j in range(a.cols) if j not in pivots] + pos = {p: i for i, p in enumerate(pivots)} + return mat(a.field, a.cols, len(free), + lambda i, j: a.field.neg(reduced.data[pos[i]][free[j]]) if i in pos + else int(i == free[j])) + + +def solve(a, b): + require(a.rows == b.rows and b.cols == 1, "solve shape") + reduced, pivots = rref(hcat(a, b)) + require(a.cols not in pivots, "inconsistent linear system") + positions = {p: i for i, p in enumerate(pivots)} + return mat(a.field, a.cols, 1, + lambda i, j: reduced.data[positions[i]][a.cols] if i in positions else 0) + + +def inverse(a): + require(a.rows == a.cols, "inverse shape") + reduced, pivots = rref(hcat(a, eye(a.field, a.rows))) + require(pivots == list(range(a.rows)), "singular inverse") + return reduced.sub(0, a.rows, a.cols, 2*a.cols) + + +def extend(base, candidates, target): + chosen = base + for j in range(candidates.cols): + if chosen.cols == target: + break + trial = hcat(chosen, columns(candidates, [j])) + if rank(trial) == trial.cols: + chosen = trial + require(chosen.cols == target, "basis extension failed") + return chosen + + +def complement(a): + basis = columns(a, rref(a)[1]) + full = extend(basis, eye(a.field, a.rows), a.rows) + return full.sub(0, a.rows, basis.cols, a.rows) + + +def direct_sum(*blocks): + f = blocks[0].field + n, m = sum(b.rows for b in blocks), sum(b.cols for b in blocks) + data = [[0] * m for _ in range(n)] + r = c = 0 + for b in blocks: + for i in range(b.rows): + for j in range(b.cols): + data[r+i][c+j] = b.data[i][j] + r += b.rows + c += b.cols + return mat(f, n, m, lambda i, j: data[i][j]) + + +def linear_map(f, n, m, action): + basis = eye(f, m) + output = [action(columns(basis, [j])) for j in range(m)] + return hcat(*output) if output else mat(f, n, 0) + + +def full_factor(a, padding=0): + f, d = a.field, a.rows + extra = complement(a) + x = hcat(a, extra, mat(f, d, padding)) + y = vcat(eye(f, d), mat(f, extra.cols+padding, d)) + return x, y + + +def rank_factor(a, padding=0): + basis = columns(a, rref(a)[1]) + coeff = linear_map(a.field, basis.cols, a.cols, lambda v: solve(basis, a @ v)) + return hcat(basis, mat(a.field, a.rows, padding)), vcat(coeff, mat(a.field, padding, a.cols)) + + +def fitting(h): + d, f = h.rows, h.field + w = eye(f, d)-h + wd = w.power(d) + c = columns(wd, rref(wd)[1]) + one = kernel(wd) + basis = hcat(c, one) + require(rank(basis) == d, "Fitting basis not direct") + split = inverse(basis) @ h @ basis + dc = c.cols + require(split.sub(0, dc, dc, d) == mat(f, dc, d-dc), "Fitting cross block") + require(split.sub(dc, d, 0, dc) == mat(f, d-dc, dc), "Fitting cross block") + hc, h1 = split.sub(0, dc, 0, dc), split.sub(dc, d, dc, d) + require(rank(eye(f, dc)-hc) == dc, "complement W not invertible") + require((eye(f, d-dc)-h1).power(d) == mat(f, d-dc, d-dc), "primary W not nilpotent") + return basis, hc, h1 + + +def adapt_active(x, y, basis, ac, a1): + """Explicit full-rank factor basis from Y, preimage lifts and ker X.""" + f, d, dc = x.field, x.rows, ac.rows + xu, yu = inverse(basis) @ x, y @ basis + nc, n1 = complement(ac), complement(a1) + lifted = [] + for first, a, extra in ((0, ac, nc), (dc, a1, n1)): + block = columns(yu, list(range(first, first+a.rows))) + for j in range(extra.cols): + target = mat(f, d, 1, lambda i, k: extra.data[i-first][j] + if first <= i < first+a.rows else 0) + block = hcat(block, solve(xu, target)) + lifted.append(block) + core = hcat(*lifted) + require(rank(core) == core.cols, "factor core dependency") + result = extend(core, kernel(xu), x.cols) + require(rank(result) == x.cols, "active factor basis singular") + return result + + +def construct_intertwiner(h, factors, drop_correction=False): + f, d = h.field, h.rows + require(d >= 1 and h.cols == d, "H domain") + w = eye(f, d)-h + products = (-w, w, w, h) + for j, ((x, y), a) in enumerate(zip(factors, products)): + require(x @ y == a, "sector product") + if j: + require(rank(x) == rank(y) == d, "sharp active ranks") + basis, hc, h1 = fitting(h) + dc, d1 = hc.rows, h1.rows + wc, w1 = eye(f, dc)-hc, eye(f, d1)-h1 + n0, n1 = complement(hc), complement(w1) + a0, a1 = n0.cols, n1.cols + x00, y00 = factors[0] + xu = inverse(basis) @ x00 + tail00 = kernel(xu.sub(0, dc, 0, x00.cols)) + b00 = hcat(y00 @ basis.sub(0, d, 0, dc), tail00) + require(rank(b00) == x00.cols, "sector00 Fitting split singular") + x1 = (xu @ tail00).sub(dc, d, 0, tail00.cols) + b10 = adapt_active(*factors[1], basis, wc, w1) + b01 = adapt_active(*factors[2], basis, wc, w1) + b11 = adapt_active(*factors[3], basis, hc, h1) + sizes = [x.cols for x, _ in factors] + pads = (sizes[1]-d-a1, sizes[2]-d-a1, sizes[3]-d-a0) + z00 = sizes[0]-dc + require(min(z00, *pads) >= 0, "negative capacity") + iwc, ih1 = inverse(wc), inverse(h1) + correction = inverse(eye(f, d1)+w1) @ x1 + lengths = [dc, dc, dc, a0, d1, a1, d1, a1, z00, *pads] + m = sum(lengths) + + def unpack(v): + out, offset = [], 0 + for length in lengths: + out.append(v.sub(offset, offset+length, 0, 1)) + offset += length + return out + + def embed(v): + x, y, z, t, xb, b, yb, c, u, p10, p01, p11 = unpack(v) + shift = mat(f, d1, 1) if drop_correction else correction @ u + xx, yy = xb-shift, yb-shift + zz = -(ih1 @ (x1 @ u+w1 @ xx+n1 @ b+w1 @ yy+n1 @ c)) + v00 = vcat(x+y+iwc @ (hc @ z+n0 @ t), u) + return vcat(b00 @ v00, b10 @ vcat(x, xx, b, p10), + b01 @ vcat(y, yy, c, p01), b11 @ vcat(z, t, zz, p11)) + + def canonical(v, which): + x, y, z, t, xb, b, yb, c, u, p10, p01, p11 = unpack(v) + zero_c, zero_1, zero_a = mat(f, dc, 1), mat(f, d1, 1), mat(f, a1, 1) + if which == 0: + head = [hc @ (x-z)-n0 @ t, zero_c, wc @ (z-x)-n0 @ t, t] + middle = [xb+w1 @ yb+n1 @ c, b, zero_1, zero_a] + tail = [mat(f, z00, 1), p10, mat(f, pads[1], 1), p11] + else: + head = [zero_c, hc @ (y-z)-n0 @ t, wc @ (z-y)-n0 @ t, t] + middle = [zero_1, zero_a, yb+w1 @ xb+n1 @ b, c] + tail = [mat(f, z00, 1), mat(f, pads[0], 1), p01, p11] + return vcat(*(head+middle+tail)) + + embedding = linear_map(f, sum(sizes), m, embed) + sc = linear_map(f, m, m, lambda v: canonical(v, 0)) + tc = linear_map(f, m, m, lambda v: canonical(v, 1)) + return embedding, sc, tc, (dc, d1, a0, a1, z00, *pads) + + +def literal_schur(h, factors): + f, d = h.field, h.rows + sizes = [x.cols for x, _ in factors] + n = sum(sizes) + inc, proj = vcat(*(y for _, y in factors)), hcat(*(x for x, _ in factors)) + require(proj @ inc == eye(f, d), "split identity") + p0 = direct_sum(*(eye(f, r) if j in (1, 3) else mat(f, r, r) for j, r in enumerate(sizes))) + q0 = direct_sum(*(eye(f, r) if j in (2, 3) else mat(f, r, r) for j, r in enumerate(sizes))) + header = hcat(inc, kernel(proj)) + ih = inverse(header) + p, q = ih @ p0 @ header, ih @ q0 @ header + require(p @ p == p and q @ q == q and p @ q == q @ p, "commuting idempotents") + require(p.sub(0, d, 0, d) == q.sub(0, d, 0, d) == eye(f, d), "identity pivots") + require((p @ q).sub(0, d, 0, d) == h, "compressed H") + s = p.sub(d, n, d, n)-p.sub(d, n, 0, d) @ p.sub(0, d, d, n) + t = q.sub(d, n, d, n)-q.sub(d, n, 0, d) @ q.sub(0, d, d, n) + require(rank(s @ t-t @ s) == 2*d, "literal sharpness") + return s, t, ih, proj + + +def check_case(h, factors, drop_correction=False): + embedding, sc, tc, signature = construct_intertwiner(h, factors, drop_correction) + s, t, ih, proj = literal_schur(h, factors) + d, n = h.rows, embedding.rows + require(proj @ embedding == mat(h.field, d, embedding.cols), "embedding outside ker pi") + g = (ih @ embedding).sub(d, n, 0, embedding.cols) + require(rank(g) == g.rows == g.cols, "residual intertwiner singular") + require(s @ g == g @ sc, "S intertwiner failed") + require(t @ g == g @ tc, "T intertwiner failed") + require(sc @ sc == sc and tc @ tc == tc, "canonical idempotents") + return signature, sc, tc + + +def make_factors(h, padding=(0, 0, 0, 0), arbitrary00=None): + w = eye(h.field, h.rows)-h + return [arbitrary00 if arbitrary00 is not None else rank_factor(-w, padding[0]), + full_factor(w, padding[1]), full_factor(w, padding[2]), full_factor(h, padding[3])] + + +def all_matrices(f, n, m): + for entries in product(range(f.q), repeat=n*m): + yield mat(f, n, m, lambda i, j: entries[i*m+j]) + + +def scramble(factors, seed): + result = [] + for slot, (x, y) in enumerate(factors): + f, r = x.field, x.cols + g = eye(f, r) + for j in range(max(0, r-1)): + a, b = (j, j+1) if (seed+slot+j) % 2 else (j+1, j) + shear = mat(f, r, r, lambda u, v: int(u == v) if (u, v) != (a, b) + else 1+(seed+j+slot) % (f.q-1)) + g = shear @ g + result.append((x @ inverse(g), g @ y)) + return result + + +def jordan(f, n, eigenvalue): + return mat(f, n, n, lambda i, j: eigenvalue if i == j else int(j == i+1)) + + +def rejected(action): + try: + action() + except CheckError: + return + raise CheckError("negative control unexpectedly accepted") + + +def run(): + count = {"complete_H": 0, "arbitrary_sector00": 0, "mixed_fixtures": 0, "controls": 0} + domains = [] + for q, d in ((2, 1), (2, 2), (3, 1), (3, 2), (4, 1), (5, 1)): + f, local = Field(q), 0 + for h in all_matrices(f, d, d): + check_case(h, make_factors(h)) + local += 1 + domains.append({"q": q, "d": d, "matrices": local}) + count["complete_H"] += local + factor_domains = [] + for q, d, r in ((2, 2, 0), (2, 2, 1), (2, 2, 2), + (3, 1, 0), (3, 1, 1), (3, 1, 2)): + f, local = Field(q), 0 + for x in all_matrices(f, d, r): + for y in all_matrices(f, r, d): + h = eye(f, d)+x @ y + factors = make_factors(h, arbitrary00=(x, y)) + check_case(h, scramble(factors, count["arbitrary_sector00"])) + count["arbitrary_sector00"] += 1 + local += 1 + factor_domains.append({"q": q, "d": d, "r00": r, "pairs": local}) + signatures = [] + for q in (2, 3, 4, 5): + f = Field(q) + nonsplit = mat(f, 2, 2, lambda i, j: ((0, 1), (1, 1))[i][j]) + repeated = vcat(hcat(nonsplit, eye(f, 2)), hcat(mat(f, 2, 2), nonsplit)) + for blocks in ((jordan(f, 2, 0), jordan(f, 2, 1)), + (nonsplit, jordan(f, 2, 1)), + (repeated, jordan(f, 2, 1)), + (jordan(f, 2, 2 if q > 2 else 0), jordan(f, 1, 1)), + (jordan(f, 1, 0), jordan(f, 3, 1), jordan(f, 1, 0))): + h0 = direct_sum(*blocks) + leading = scramble([(eye(f, h0.rows), eye(f, h0.rows))], q)[0][1] + h = inverse(leading) @ h0 @ leading + for pad in ((0, 0, 0, 0), (2, 1, 2, 1)): + result = check_case(h, scramble(make_factors(h, pad), q+sum(pad))) + signatures.append([q, *result[0]]) + count["mixed_fixtures"] += 1 + f = Field(3) + h = direct_sum(jordan(f, 1, 0), jordan(f, 2, 1)) + factors = scramble(make_factors(h, (1, 1, 0, 1)), 3) + rejected(lambda: check_case(h, factors, drop_correction=True)) + count["controls"] += 1 + rejected(lambda: inverse(eye(f, h.rows)-h)) + count["controls"] += 1 + bad = list(factors) + bad[0] = (-bad[0][0], bad[0][1]) + rejected(lambda: check_case(h, bad)) + count["controls"] += 1 + deficient_h = eye(f, 1) + bad = make_factors(deficient_h) + x, y = bad[1] + bad[1] = (x, mat(f, y.rows, y.cols)) + require(bad[1][0] @ bad[1][1] == mat(f, 1, 1), "control changed product") + rejected(lambda: check_case(deficient_h, bad)) + count["controls"] += 1 + w = eye(f, 2)-jordan(f, 2, 1) + rejected(lambda: inverse(hcat(columns(w, rref(w)[1]), kernel(w)))) + count["controls"] += 1 + good, sc, tc, _ = construct_intertwiner(h, factors) + s, t, ih, _ = literal_schur(h, factors) + g = (ih @ good).sub(h.rows, good.rows, 0, good.cols) + padding_index = sc.rows-2 # The one (1,0) padding coordinate in this fixture. + wrong = sc+mat(f, sc.rows, sc.cols, + lambda i, j: f.neg(1) if i == j == padding_index else 0) + rejected(lambda: require(s @ g == g @ wrong, "wrong scalar padding")) + count["controls"] += 1 + rejected(lambda: construct_intertwiner(mat(f, 0, 0), [(mat(f, 0, 0), mat(f, 0, 0))]*4)) + count["controls"] += 1 + # Same H and residual dimension alone do not fix the ordered pair. + scalar_h = mat(f, 1, 1) + _, s00, _ = check_case(scalar_h, make_factors(scalar_h, (1, 0, 0, 0))) + _, s10, _ = check_case(scalar_h, make_factors(scalar_h, (0, 1, 0, 0))) + require(s00.rows == s10.rows and rank(s00) != rank(s10), "profile discriminator failed") + count["controls"] += 1 + report = {"counts": count, "complete_domains": domains, "factor_domains": factor_domains, + "mixed_signatures_sha256": hashlib.sha256(json.dumps(signatures).encode()).hexdigest(), + "scope": "finite full ordered intertwiners, not a proof kernel or supplier replay"} + print(json.dumps(report, sort_keys=True)) + print("PASS_SCHUR_PRIMARY_GLUING") + + +if __name__ == "__main__": + run() From abcf271670e7981ef0dde6582173952902544dc8 Mon Sep 17 00:00:00 2001 From: Mihir Srivastava Date: Fri, 23 Oct 2026 12:16:31 -0700 Subject: [PATCH 2/2] Credit concurrent independent gluing and refresh scope coverage --- research/schur-primary-gluing/README.md | 11 +++++++++++ research/schur-primary-gluing/TASK.json | 24 +++++++++++++++++++----- 2 files changed, 30 insertions(+), 5 deletions(-) diff --git a/research/schur-primary-gluing/README.md b/research/schur-primary-gluing/README.md index f828cc5923..b324f0cfc1 100644 --- a/research/schur-primary-gluing/README.md +++ b/research/schur-primary-gluing/README.md @@ -20,6 +20,17 @@ an improvement to kappa. Distinct H/profile data may yield the same residual orbit: the result is sufficiency of fixed data, not an injective classification of all parameter choices. The selected conditional kappa remains 0.00302015. +**Concurrent independent work.** The final overlap refresh found Ali Romman's +[independent proof and constructive map](https://github.com/aliromman/integer-mult-bounds/blob/49373a6f433fef560a4297f65f3826a8add7cd44/research/general-ordered-schur/PROOF.md). +It reaches the same Fitting decomposition and ordered representative. +[The coordination reply](https://github.com/CrocSwap/integer-mult-bounds/discussions/5337#discussioncomment-19153030) +records that Ali moved the primary focus of that contribution to the +complementary fixed-H header weights. Our proof and separate checker were +frozen at `f69863ddefafa183babe2b59a8e5c91a92786fd1` before reading that proof. +The concurrent code is not imported or an executable dependency, and its +reported checks were not replayed here. Credit is shared for the independently +obtained gluing result; no exclusive discovery claim is made. + ## Contract and explicit representative Work over any field F. Let P0,Q0 be commuting idempotents on V, with ordered diff --git a/research/schur-primary-gluing/TASK.json b/research/schur-primary-gluing/TASK.json index 83c22fda40..e8cb893c9d 100644 --- a/research/schur-primary-gluing/TASK.json +++ b/research/schur-primary-gluing/TASK.json @@ -147,14 +147,14 @@ "overlap": { "scope": "All open PR bodies and Discussions through the reported complete snapshots, plus partial local notes and targeted all-state GitHub Schur/gluing search; relevant predecessor notes materialized and read.", "open_prs": { - "fetched_at": "2026-10-23T19:00:24.760499+00:00", + "fetched_at": "2026-10-23T19:12:56.555770+00:00", "complete_pagination": true, "records": 305 }, "discussions": { - "fetched_at": "2026-10-23T19:02:14.934078+00:00", + "fetched_at": "2026-10-23T19:14:31.495535+00:00", "complete_pagination": true, - "records": 4623 + "records": 4638 }, "local": { "head": "7c472563474e60185e6ca101a17622133d047e56", @@ -167,9 +167,23 @@ "#5267 nilpotent whole pair", "#5287 whole central class", "#5348 H=1 primary whole pair", - "#5337 released general-H gluing" + "#5337 released general-H gluing", + "Concurrent independent general-H proof by Ali Romman at 49373a6f433fef560a4297f65f3826a8add7cd44; author moved primary contribution to fixed-H header weights." ], "added_value": "Justified sector00 primary split, extension of the W-invertible model, and explicit intertwiners that glue the entire ordered pair for arbitrary H.", - "limits": "No matches is not proof of novelty. Local inventory is incomplete; arbitrary historical diffs, nested notes and unpublished work are not covered." + "limits": "No matches is not proof of novelty. Local inventory is incomplete; arbitrary historical diffs, nested notes and unpublished work are not covered. The independent concurrent gluing proof was found and credited, not suppressed. Its executable checks were not replayed here." + }, + "submission_refresh": { + "canonical_main": "7c472563474e60185e6ca101a17622133d047e56", + "checked_at_utc": "2026-10-23T19:14:54Z", + "priority_revision": 7, + "result": "No main, relevant guidance, selected record or pinned predecessor change." + }, + "concurrent_work": { + "author": "Ali Romman", + "head": "49373a6f433fef560a4297f65f3826a8add7cd44", + "proof": "https://github.com/aliromman/integer-mult-bounds/blob/49373a6f433fef560a4297f65f3826a8add7cd44/research/general-ordered-schur/PROOF.md", + "coordination": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5337#discussioncomment-19153030", + "relationship": "Independent matching gluing proof, read after our proof/checker commit f69863ddefafa183babe2b59a8e5c91a92786fd1; no code imported, no runtime or theorem dependency; their reported checks not replayed here. Complementary header weights remain their scope." } }