From af9cf805c501e4e9e947c98c0b97b2281b6b6e97 Mon Sep 17 00:00:00 2001 From: ssafwann Date: Thu, 22 Oct 2026 23:32:58 +0800 Subject: [PATCH] Count complete headers for sharp identity-pivot Schur blocks --- research/schur-header-count/README.md | 331 +++++++++++++++++++++++ research/schur-header-count/SOURCES.json | 18 ++ research/schur-header-count/TASK.json | 209 ++++++++++++++ research/schur-header-count/VERIFY.json | 32 +++ research/schur-header-count/verify.py | 318 ++++++++++++++++++++++ 5 files changed, 908 insertions(+) create mode 100644 research/schur-header-count/README.md create mode 100644 research/schur-header-count/SOURCES.json create mode 100644 research/schur-header-count/TASK.json create mode 100644 research/schur-header-count/VERIFY.json create mode 100644 research/schur-header-count/verify.py diff --git a/research/schur-header-count/README.md b/research/schur-header-count/README.md new file mode 100644 index 0000000000..5e644cf316 --- /dev/null +++ b/research/schur-header-count/README.md @@ -0,0 +1,331 @@ +# Exact complete-header counts for a sharp Schur block + +**Written counting theorem with exact finite corroboration; no new kappa.** +Prepared for **ssafwann** with substantial **OpenAI Codex (gpt-6-astra)** +assistance, by one agent. Apache-2.0. + +[PR4671](https://github.com/CrocSwap/integer-mult-bounds/pull/4671) determines +when an identity-pivot Schur commutator attains rank 2d, and asks how often +complete headers satisfy its six map conditions. This package supplies an +exact count for **every fixed commuting binary idempotent pair**, in terms of +its four joint-sector dimensions. It retains the dependence through the common +compressed product H; it does not multiply the six marginal probabilities. + +Two scalar examples have **60,480** and **181,440** sharp complete headers in +GL_5(F2), with exact densities **3/496** and **9/496**. The four equal +2-dimensional sectors have sharp density **27/2,763,520** at block size d=2. + +**The sample space is complete headers; the acceptance event is one block.** +The event requires both leading d-by-d blocks to be I_d and their Schur +commutator to have rank 2d. It does **not** require every later leading minor +to pass. Thus this is not a full-guard-chain law, a physical caller, or a +supplier admission. The distinction matters when comparing the predecessor +full-guard counts of Nick Petalas and Ryanson Jonathan. + +## 1. Exact count + +Fix commuting idempotents P0,Q0 on V=F2^n. Their four joint eigenspaces have +dimensions r=(r00,r10,r01,r11), in that order, with nonnegative entries summing +to n. Choose a complete ordered header M uniformly from GL_n(F2), and put +P=M^-1 P0 M and Q=M^-1 Q0 M. This is equivalent to the G P0 G^-1 convention +in prior header work by taking G=M^-1. Fix 1<=d<=n. + +Let Z count headers with both leading blocks I_d. Let N count such headers +whose Schur-commutator rank is 2d. When d=n the Schur space is zero and N=0. +All probabilities below concern fixed requests, chosen before the header. + +Define the injection count + +\[ +I(s,k)=\prod_{j=0}^{k-1}(2^s-2^j) +\] + +for 0<=k<=s, and zero otherwise. An empty product is one, so +|GL_0(F2)|=I(0,0)=1. Put G(s)=I(s,s) and + +\[ +{m\brack k}_2=I(m,k)/G(k) +\] + +for 0<=k<=m, and zero otherwise. For a fixed T in M_d(F2) of rank rho, +define two counts of factorizations X Y=T through F2^r: + +\[ +U(r,d,\rho)=\sum_{k=\rho}^{\min(d,r)} + {d-\rho\brack d-k}_2\, I(r,k)\,2^{d(r-k)}, \tag{1} +\] +\[ +A(r,d,\rho)= +\begin{cases} + I(r,d)\,2^{\rho(r-d)} I(r-d,d-\rho),&r\ge d,\\ + 0,&r=1. + +For H in M_d(F2), write h=rank H and w=rank(I+H). Then the exact counts are + +\[ +\boxed{\begin{aligned} +N&=G(n-d)\sum_{H\in M_d(\mathbb F_2)} + U(r_{00},d,w)A(r_{10},d,w)A(r_{01},d,w)A(r_{11},d,h),\\ +Z&=G(n-d)\sum_{H\in M_d(\mathbb F_2)} + U(r_{00},d,w)U(r_{10},d,w)U(r_{01},d,w)U(r_{11},d,h). +\end{aligned}} \tag{3} +\] + +Thus the unconditional sharp density is N/G(n), and its conditional density +among identity-pivot headers is N/Z when Z>0. When Z=0, no conditional +probability is asserted. The sum retains the actual joint distribution of +rank H and rank(I+H). They must not be sampled independently. + +This is a finite formula for every d, not an efficient large-d algorithm. +The checker groups the 2^(d²) matrices by their rank pairs and evaluates d<=3. +There is no quotient by a sector centralizer: different ordered headers are +different elements of the stated sample space, even when they conjugate the +pair to the same matrices. + +## 2. Proof of the factor counts + +For (1), condition on k=rank Y. The equation X Y=T is solvable exactly when +ker Y is a (d-k)-dimensional subspace of ker T. There are +`[d-rho choose d-k]_2` choices for that kernel. For any chosen kernel, there +are I(r,k) embeddings of the quotient F2^d/ker Y into F2^r, hence that many +maps Y with precisely this kernel. X is then uniquely prescribed on im Y +by X(Yv)=Tv. On a complement of dimension r-k, it is an arbitrary map to +F2^d, giving 2^(d(r-k)) choices. Sum over k. The Gaussian coefficient itself +counts subspaces because each has G(d-k) ordered bases, whereas the ambient +kernel has I(d-rho,d-k) ordered independent tuples. + +For (2), there are I(r,d) choices for the injective Y. In a basis starting +with its image, write X=(T L). For X to be onto, the image of L in the quotient +F2^d/im T, of dimension d-rho, must be onto. There are I(r-d,d-rho) such +surjections. Each has 2^(rho(r-d)) lifts L, proving (2). This argument also +explains the zero count when r<2d-rho; injectivity alone is insufficient. + +## 3. From sector factors to complete headers + +Let i be the first d columns of M, and pi the first d rows of M^-1. Then +pi i=I. Conversely, every split pair (i,pi) with pi i=I has exactly +**G(n-d)** header completions: append any ordered basis of ker pi to i. +These are all the completions, and each header gives one split pair. Replacing +the kernel basis N by NK conjugates both Schur complements by K^-1 on the +left and K on the right. Thus their commutator rank is unchanged throughout +a completion fibre. In particular the total number of split pairs is + +\[ +I(n,d)2^{d(n-d)}=G(n)/G(n-d). \tag{4} +\] + +The factor 2^{d(n-d)} belongs to choosing pi for a fixed i. It is not an +additional multiplier after the complete split pair has already been counted. +This extends the equal-completion principle in Nick Petalas's earlier scalar +header proofs to a d-dimensional block, with the full multiplicity retained. + +Choose fixed bases in the four joint sectors. Let Y_j:U->V_j be the component +of i and X_j:V_j->U the restriction of pi. The identity-pivot conditions are + +\[ +\begin{aligned} +X_{10}Y_{10}+X_{11}Y_{11}&=I,\\ +X_{01}Y_{01}+X_{11}Y_{11}&=I,\\ +\sum_j X_jY_j&=I. +\end{aligned} +\] + +Putting H=X11 Y11 gives + +\[ +X_{00}Y_{00}=X_{10}Y_{10}=X_{01}Y_{01}=I+H,\qquad X_{11}Y_{11}=H. \tag{5} +\] + +Conversely, (5) implies all three equations, so it already enforces pi i=I, +including injectivity of the assembled i and surjectivity of the assembled pi. +There is no additional global compatibility test. Once H is fixed, the four +factorization choices are independent **as choices of maps in fixed sectors**. +Every resulting split pair determines H uniquely; summing over H does not +count a pair twice. + +The six-map criterion from #4671, restated with proof below, says that sharpness +requires exactly the X/Y maps in sectors 10,01,11 to be onto/one-to-one. Thus +use U for sector 00 and A for the other three to count sharp split pairs. +Use U in all four sectors to count all identity-pivot split pairs. Multiply +both counts by G(n-d) to obtain (3). The whole derivation applies to any fixed +pair with these sector dimensions by simultaneous change of basis, which +permutes the uniform complete-header sample space. + +### Credited six-map criterion, with its algebraic justification + +Write P=[[I,R],[C,D]], Q=[[I,L],[E,F]], S=D+CR and T=F+EL. The ordered +factorization from Nick Petalas's #4597, specialized in #4657/#4671, is + +\[ +[S,T]=(TC\ \ C+E)\begin{pmatrix}R+L\\RT\end{pmatrix}. \tag{6} +\] + +To check it directly, set J=(PQ)21 and B=(PQ)12. Commutation gives +RE=LC=H+I, DE=J+C, FC=J+E, RF=B+L, LD=B+R and DF+FD=ER+CL. +Expansion yields `[S,T]=J(R+L)+(C+E)B+CHL+EHR`, while TC=J+EH and RT=B+HL, +which verifies (6). + +In ambient coordinates define + +\[ +\mathcal A=(QPi+QiH\ \ (P+Q)i),\qquad +\mathcal B=\begin{pmatrix}\pi(P+Q)\\\pi PQ+H\pi Q\end{pmatrix}. +\] + +We have pi A=0 and B i=0. Corestricting A to ker pi and restricting B to +ker pi gives the two factors in (6). In sector coordinates, + +\[ +\mathcal A(x,y)=(0,Y_{10}y,Y_{01}(Hx+y),Y_{11}(I+H)x), +\] +\[ +\mathcal B(v)=(X_{10}v_{10}+X_{01}v_{01},\ HX_{01}v_{01}+(I+H)X_{11}v_{11}). +\] + +Sharpness makes A injective. A nonzero z in ker Y10 forces Hz=z and makes +A(z,z)=0; a nonzero z in ker Y01 forces Hz=z and makes A(z,0)=0; a nonzero +z in ker Y11 forces Hz=0 and also makes A(z,0)=0. Therefore all three Y maps +are injective. Apply the same argument to P^T,Q^T to obtain surjectivity of +all three X maps: rank(E_j^T i)=rank(pi E_j)=rank X_j. + +Conversely injectivity of the three Y maps makes A injective: its zero vector +equations give y=0, Hx=0 and (I+H)x=0. A row (u,v) annihilating B must satisfy +u X10=0, (u+vH)X01=0 and v(I+H)X11=0. Surjectivity of the X maps gives +u=0 and v=0, so B is onto. Since B kills iU, its restriction to ker pi is +onto too. The product in (6) has rank 2d. This establishes the precise cited +criterion without importing a predecessor executable or relying on an +unavailable pending source at replay time. + +## 4. Exact examples and a dependence countercheck + +The table reports both the complete-header count and the correct denominator. +A split pair includes a labeled d-dimensional inclusion and its projection. + +| Sector dimensions (00,10,01,11) | d | Identity-pivot split pairs | Sharp split pairs | Sharp complete headers | N/G(n) | N/Z | +|---|---:|---:|---:|---:|---:|---:| +| (1,1,1,2) | 1 | 172 | 3 | 60,480 | 3/496 | 3/172 | +| (0,2,2,1) | 1 | 100 | 9 | 181,440 | 9/496 | 9/100 | +| (2,2,2,2) | 2 | 1,932,288 | 2,592 | 52,251,375,697,920 | 27/2,763,520 | 27/20,128 | + +The first two pairs both have rank P0=rank Q0=3 in dimension five, yet +their sharp densities differ by a factor of three. Individual projector ranks +alone do not determine the count. + +For the first two rows, G(4)=20,160 and G(5)=9,999,360. In the third row, +G(6)=20,158,709,760 and G(8)=5,348,063,769,211,699,200. +At (2,2,2,2), sharpness permits only the two H for which both H and I+H are +invertible; each contributes G(2)^4=1,296 split pairs. + +There is a simple numerical check against the independence shortcut. Among +the 100 identity-pivot split pairs for (0,2,2,1), the six full-rank event counts +are **60,60,60,60,100,100**. Their joint fraction is **9/100**. Multiplying +marginals instead gives **81/625**, a different number. For (1,1,1,2), the +marginal counts are 64,64,64,64,168,168 among 172, and again their product +differs from the joint fraction 3/172. The sum over shared H in (3) retains +this dependence. + +## 5. Verification and reproduction + +```sh +python3.12 -B scripts/research_package.py --package research/schur-header-count +python3.12 -B scripts/check_research_commit.py --package research/schur-header-count --check-source-history +``` + +The standard-library verifier prints `PASS_SCHUR_HEADER_COUNT`. Registered +ordinary and optimized (`-O`) modes use explicit exceptions, not assertions. +A Git-free exported package can run `python3.12 -I -W error -O -B verify.py`. +No external mathematical input, compiler or predecessor executable is needed. + +The checks deliberately use direct matrix calculations separately from the +counting formulas: + +- All **270,759** pairs (X,Y) with d=1,2,3 and sector size r=0,1,2,3 are + enumerated. Product matrices and both factor ranks give exact counts for + every T, agreeing with (1) and (2), including zero-sized sectors. +- Complete literal header censuses cover GL3 at profile (0,1,1,1), d=1, and + GL4 at profiles (1,1,1,1), d=1,2, and (0,1,1,2), d=1. There are + **60,648 header/context cases**; identity-pivot counts are 54, 5,040, 36 and + 9,072 respectively, and all sharp counts are zero. +- For each of the two n=5 profiles, **all 496 scalar split pairs** are checked + by constructing a header and directly computing the Schur rank for each + identity-pivot pair. No six-map test is used to select the positive pairs. +- All G4 completions of the resulting 3 and 9 positive split pairs are + explicitly formed, inverted and checked by literal conjugation and Schur + multiplication: **241,920 positive complete-header cases**, distinct for each fixed pair. This is + not a raw enumeration of every GL5 header; completeness of this positive + census uses the proved equal-completion bijection and rank invariance under + a change of basis in ker pi. Distinctness is checked within each fixed pair. +- Seven controls reject the wrong conditional denominator, independent + marginals, a missing completion multiplier, forcing full rank in sector 00, + omitting surjectivity, negative sector dimensions and zero block size. + +The d=2,n=8 number is evaluated by the proved formula, supported by the complete +small factor census; the 5.3e18-element header space is **not** enumerated. +Universal claims rest on the written proof, with these finite checks as +corroboration. Human/formal-kernel acceptance is unclaimed. Lean, Docker and +the selected scientific cold replay were not run. Hosted CI is reported +separately in the PR, rather than inferred from local success. + +## 6. Task, scope and attribution + +Base: canonical main `b58ad9ef4d4e861b0eaa5dba41742bdc072dca51`, priority revision 7, +selected conditional kappa 0.00302015. This takes the explicit #4671 handoff +and marks `formal-interface-lemma` **changed** to an algebraic counting side +result. The [canonical Discussion4653](https://github.com/CrocSwap/integer-mult-bounds/discussions/4653) +records overlap and the decision to keep the completed dimension question +closed and narrow this round to the specified header ensemble. + +**Obligation ledger.** The criterion, factor counts and complete-header +multiplicity are proved above. Production header covers, header selection and +emission, physical reads, owned/borrowed state, dirty compensation/restoration, +stock, dispatch, later guards and the complete consumer bill remain unknown, +not zero. No physical saving or supplier implementation follows from a positive +count. No selected-frontier change is made. + +Credit and exact primary sources: + +- **ssafwann, #4671**, `8d2e3bc76aa7d43e5c629daaf1e72d4dd5a81ed9`: + the six-map criterion, dimension theorem and explicit counting handoff; + substantial OpenAI Codex assistance. The criterion is retained and proved + above, not claimed as the new contribution. +- **ssafwann, #4657**, `b79f90bc8d839a4998a40b10bcb437e87baa8397`: + preceding identity-pivot factorization and 4d construction. +- **Nick Petalas, #4597**, `dfeb8ca729a04aea4aa290438f2ed50a37a9c7cb`: + ordered block-Schur factorization; #4278/#4259/#4246/#4228 retain the + scalar Schur and equal-completion/full-header lineage. Their original + attribution and assistance disclosures are preserved in those sources. +- **Ryanson Jonathan, #4609/#4617**, and **lee-phys, #4634**: preceding binary + sharpness, minimum-dimension constructions and questions, with their + disclosed Claude Code / OpenAI Codex assistance. +- **Cinna Davis, #4100**: earlier BIT request/header setting; source527, + commdata2338 and Jose Manuel retain the earlier normalizer lineage credit. + +Related inspected work #4598 (`c80f445e8c3c22d341d467254b89245fbddb9eb2`) and +#4599 (`19ca650c67ad2722790dc60c0bfd12989479b06a`) counts corank-one full guards, +not the one-block identity-pivot/Schur-rank event here. The merged +`full-guard-header-census` provides literal full-guard checks with Ryanson +Jonathan's attribution; it is context, not an imported verifier. This package +makes no numerical comparison between those different events. Exact source +paths, Git blobs and byte hashes are recorded as citations in TASK.json; +pending PRs are not runtime Git dependencies. + +The new contribution is the exact header law (3), with the elementary factor +counts (1)–(2) derived explicitly, the exact examples and finite corroboration. +Repository tooling retains its contributors' attribution. Apache-2.0. + +## Open next questions + +Can this one-block count feed a state-aware full-guard recursion? The next +Schur pair generally does not commute, so applying (3) again is unjustified. +Start with one of the n=5 profiles and classify the residual pair up to +simultaneous conjugacy, retaining how many complete headers reach each state; +compare with the orbit question already identified in #4597. The blocker is +the residual-state distribution, not another seed or a product of marginals. +Any use by a real producer additionally needs its actual header cover and a +complete cost allowance. No claim is held on that follow-up. diff --git a/research/schur-header-count/SOURCES.json b/research/schur-header-count/SOURCES.json new file mode 100644 index 0000000000..4916cee8e5 --- /dev/null +++ b/research/schur-header-count/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "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" + } + ] +} diff --git a/research/schur-header-count/TASK.json b/research/schur-header-count/TASK.json new file mode 100644 index 0000000000..c62524592f --- /dev/null +++ b/research/schur-header-count/TASK.json @@ -0,0 +1,209 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "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": "Count complete M in GL_n(F2) giving common I_d pivots and Schur-commutator rank 2d for any fixed commuting idempotent pair, using its joint-sector dimensions; give unconditional and identity-pivot-conditioned densities.", + "scope_change_reason": "Handoff-first selection of PR4671's explicit count question. This is a written algebraic counting side theorem with exact corroboration, not a Lean formalization, another dimension construction or a selected-caller audit.", + "bottleneck_link": "Quantifies the frequency of a maximal one-block Schur transition in the complete-header ensemble. It does not establish full-guard-chain densities, production-header feasibility, physical cost savings, supplier admission or a new kappa.", + "budget_minutes": 60, + "stop_rule": "Stop after the one-block formula and discriminating exact examples. Keep dimension work closed; do not automatically extend to full-guard recursion or physical implementation.", + "outcome": "completed", + "evidence": "README gives the exact factor and header counts with proofs. verify.py independently enumerates 270759 matrix-factor pairs, 60648 small header/context cases, both 496-element scalar split domains, and all 241920 positive complete-header cases, distinct for each fixed pair. Seven semantic/domain rejection controls are included.", + "author": "ssafwann", + "ai_assistance": "Substantial OpenAI Codex (gpt-6-astra) assistance, by one agent; no delegated agents. Apache-2.0.", + "open_questions": [ + { + "question": "Can the one-block law feed a state-aware recursion for full guard chains?", + "why_it_matters": "After the deletion the Schur pair generally no longer commutes, so multiplying this formula at later stages would be unjustified.", + "first_step": "For one n=5 sector profile, classify the residual pair up to simultaneous conjugacy and retain how many complete headers reach each state; compare with the orbit question in PR4597.", + "blocked_by": "Residual-state distribution and transition law; a real producer additionally needs its actual header ensemble and complete physical cost allowance." + } + ], + "coordination": { + "canonical": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4653", + "handoff": "https://github.com/CrocSwap/integer-mult-bounds/pull/4671", + "claim_started": "2026-10-22T15:19:00+00:00", + "claim_expires": "2026-10-22T17:19:00+00:00", + "main_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "main_refresh_started": "2026-10-22T15:12:32+00:00", + "guidance_changes": false, + "initial_overlap": { + "local": { + "head": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "records": 5860, + "head_records": 5860, + "complete_head_inventory": true, + "unsearched_head_paths": [] + }, + "open_prs": { + "fetched_at": "2026-10-22T15:15:08.862104+00:00", + "complete_pagination": true, + "records": 443 + }, + "discussions": { + "fetched_at": "2026-10-22T15:17:34.531980+00:00", + "complete_pagination": true, + "records": 3599 + } + }, + "overlap_limits": "Open PR bodies, Discussion records and in-scope local notes; not arbitrary diffs, closed remote PRs or unpublished work.", + "submission_refresh": { + "main_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "started_at": "2026-10-22T15:28:59+00:00", + "guidance_changes": false, + "predecessor_heads_unchanged": true, + "coverage": { + "local": { + "head": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "records": 5862, + "head_records": 5860, + "complete_head_inventory": true, + "unsearched_head_paths": [] + }, + "open_prs": { + "fetched_at": "2026-10-22T15:29:10.770941+00:00", + "complete_pagination": true, + "records": 445 + }, + "discussions": { + "fetched_at": "2026-10-22T15:31:35.834501+00:00", + "complete_pagination": true, + "records": 3589 + } + }, + "warnings": [] + } + }, + "family_decision": { + "decision": "narrow to the new complete-header count; dimension work stays closed", + "contract": "Fixed commuting binary idempotent pair; uniform complete GL_n header; one common leading d-block equal to I; count maximal Schur-commutator rank and both denominators.", + "proved": "Written six-map criterion (credited), elementary factor counts, complete-header completion bijection and count formula; exact finite corroboration.", + "unknown": "Restricted production covers; header selection/emission; physical reads; owned/borrowed state; dirty compensation/restoration; stock; dispatch; later guards and complete consumer bill. Unknown costs are not zero.", + "decision_changed": "Exact frequency of a maximal one-block transition; no claimed removal of paid work.", + "comparison": "Current Gaussian-gate follow-ups and PR4598/4599 full-guard counts concern different events. This is the separately specified PR4671 counting handoff.", + "reopen_only": "Named residual-state/ensemble question or actual caller contract with a full cost allowance." + }, + "source_citations": [ + { + "pr": 4671, + "author": "ssafwann", + "commit": "8d2e3bc76aa7d43e5c629daaf1e72d4dd5a81ed9", + "path": "research/identity-pivot-sector-bound/README.md", + "git_blob": "80c587372713ca47a79d4880dab330e642c3a25a", + "sha256": "c997446a1fc4683694987feea5f2a8423b57d48d5513a27e178f84ecf56ffc12", + "usage": "Exact mathematical/attribution citation; no runtime dependency. Pending evidence is author-reported, not scientific acceptance." + }, + { + "pr": 4657, + "author": "ssafwann", + "commit": "b79f90bc8d839a4998a40b10bcb437e87baa8397", + "path": "research/identity-pivot-schur/README.md", + "git_blob": "9adb808ca32317e202003cd98aabba3358eb06df", + "sha256": "5a85e1fa1b3f0927e27d63e306ba5089dd801d86433bec8dcae79c0de6db2ace", + "usage": "Exact mathematical/attribution citation; no runtime dependency. Pending evidence is author-reported, not scientific acceptance." + }, + { + "pr": 4597, + "author": "Nick Petalas", + "commit": "dfeb8ca729a04aea4aa290438f2ed50a37a9c7cb", + "path": "research/block-schur-commutator/README.md", + "git_blob": "79790ccea54cfea1aab611768927651a81f2fb18", + "sha256": "945c1420fe9fb5c26dec49e7d6005d77382ca9dc6ca0f424d8baa1500bfc092c", + "usage": "Exact mathematical/attribution citation; no runtime dependency. Pending evidence is author-reported, not scientific acceptance." + }, + { + "pr": 4259, + "author": "Nick Petalas", + "commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "path": "research/laminar-header-law/README.md", + "git_blob": "b39ea17c2764764e507d8d3c8b2f079dc2a96efa", + "sha256": "5cf3ff2b00615c59c8a534552517eeab966bcdd8e7b5029aaa1919b4fb942d09", + "usage": "Exact mathematical/attribution citation; no runtime dependency. Pending evidence is author-reported, not scientific acceptance." + } + ], + "related_work": [ + { + "pr": 4598, + "head": "c80f445e8c3c22d341d467254b89245fbddb9eb2", + "scope": "Five corank-one full-guard threshold header count, a different acceptance event; body inspected." + }, + { + "pr": 4599, + "head": "19ca650c67ad2722790dc60c0bfd12989479b06a", + "scope": "Four corank-one full-guard product inequality, a different acceptance event; body inspected." + } + ] +} diff --git a/research/schur-header-count/VERIFY.json b/research/schur-header-count/VERIFY.json new file mode 100644 index 0000000000..fa22725d74 --- /dev/null +++ b/research/schur-header-count/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact factor counts, direct complete-header and split-pair censuses, all positive scalar completions, denominators and seven controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same checks remain active under optimization." + } + ] +} diff --git a/research/schur-header-count/verify.py b/research/schur-header-count/verify.py new file mode 100644 index 0000000000..0da95c051b --- /dev/null +++ b/research/schur-header-count/verify.py @@ -0,0 +1,318 @@ +#!/usr/bin/env python3 +"""Exact one-block header counts over F2; standard library, no external inputs. + +Prepared for ssafwann with substantial OpenAI Codex assistance. Apache-2.0. +The six-map criterion is credited to PR4671, with Nick Petalas's Schur lineage. +Bit-packed matrix enumeration below is separate from the counting formulas. +""" +from collections import Counter +from fractions import Fraction +from functools import lru_cache +import itertools +import json +import math + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def eye(n): + return tuple(1 << i for i in range(n)) + + +def add(a, b): + require(len(a) == len(b), "addition shape") + return tuple(x ^ y for x, y in zip(a, b)) + + +def mul(a, b): + out = [] + for row in a: + value = 0 + while row: + bit = row & -row + value ^= b[bit.bit_length() - 1] + row ^= bit + out.append(value) + return tuple(out) + + +def rank(rows): + basis = {} + for row in rows: + while row: + pivot = row.bit_length() + if pivot not in basis: + basis[pivot] = row + break + row ^= basis[pivot] + return len(basis) + + +def inverse(a): + n = len(a) + rows = [row | 1 << (n + i) for i, row in enumerate(a)] + for col in range(n): + pivot = next((j for j in range(col, n) if rows[j] >> col & 1), None) + require(pivot is not None, "singular header") + rows[col], rows[pivot] = rows[pivot], rows[col] + for j in range(n): + if j != col and rows[j] >> col & 1: + rows[j] ^= rows[col] + return tuple(row >> n for row in rows) + + +def from_columns(cols, n): + return tuple(sum((v >> i & 1) << j for j, v in enumerate(cols)) for i in range(n)) + + +def matrices(rows, cols): + return itertools.product(range(1 << cols), repeat=rows) + + +def gl_headers(n): + def extend(cols, span): + if len(cols) == n: + yield from_columns(cols, n) + else: + for v in range(1, 1 << n): + if v not in span: + yield from extend(cols + [v], span | {x ^ v for x in span}) + yield from extend([], {0}) + + +def inj(n, k): + if not 0 <= k <= n: + return 0 + return math.prod((1 << n) - (1 << j) for j in range(k)) + + +def gaussian(n, k): + if not 0 <= k <= n: + return 0 + return inj(n, k) // inj(k, k) + + +@lru_cache(maxsize=None) +def unrestricted_factor(r, d, rho): + require(r >= 0 and d >= 1 and 0 <= rho <= d, "factor dimensions") + return sum(gaussian(d - rho, d - k) * inj(r, k) * (1 << (d * (r - k))) + for k in range(rho, min(d, r) + 1)) + + +@lru_cache(maxsize=None) +def full_factor(r, d, rho): + require(r >= 0 and d >= 1 and 0 <= rho <= d, "factor dimensions") + if r < d: + return 0 + return inj(r, d) * (1 << (rho * (r - d))) * inj(r - d, d - rho) + + +@lru_cache(maxsize=None) +def rank_pair_classes(d): + return Counter((rank(h), rank(add(eye(d), h))) for h in matrices(d, d)) + + +def predict(profile, d): + require(len(profile) == 4 and all(type(r) is int and r >= 0 for r in profile), + "four nonnegative integer sector dimensions") + n = sum(profile) + require(type(d) is int and 1 <= d <= n, "pivot dimension") + identity = sharp = 0 + for (rh, rw), multiplicity in rank_pair_classes(d).items(): + r00, r10, r01, r11 = profile + outside = unrestricted_factor(r00, d, rw) + identity += multiplicity * outside * unrestricted_factor(r10, d, rw) * \ + unrestricted_factor(r01, d, rw) * unrestricted_factor(r11, d, rh) + sharp += multiplicity * outside * full_factor(r10, d, rw) * \ + full_factor(r01, d, rw) * full_factor(r11, d, rh) + tail = inj(n - d, n - d) + total = inj(n, n) + split_total = inj(n, d) * (1 << (d * (n - d))) + require(tail * split_total == total, "GL completion normalization") + require(0 <= sharp <= identity <= split_total, "count containment") + return {"profile": profile, "d": d, "identity_splits": identity, "sharp_splits": sharp, + "split_total": split_total, "completion_multiplicity": tail, + "identity_headers": identity * tail, "sharp_headers": sharp * tail, + "total_headers": total, "sharp_density": str(Fraction(sharp * tail, total)), + "sharp_given_identity": str(Fraction(sharp, identity)) if identity else None} + + +def masks(profile): + offset = 0 + sectors = [] + for r in profile: + sectors.append(((1 << r) - 1) << offset) + offset += r + return sectors, sectors[1] | sectors[3], sectors[2] | sectors[3] + + +def schur(a, d): + low = (1 << d) - 1 + require(tuple(row & low for row in a[:d]) == eye(d), "identity pivot") + r = tuple(row >> d for row in a[:d]) + c = tuple(row & low for row in a[d:]) + dd = tuple(row >> d for row in a[d:]) + return add(dd, mul(c, r)) + + +def inspect_header(header, profile, d): + """Literal conjugation and direct Schur multiplication; no count formula.""" + n = len(header) + require(n == sum(profile), "header dimension") + back = inverse(header) + _, pmask, qmask = masks(profile) + p = mul(back, tuple(row if pmask >> i & 1 else 0 for i, row in enumerate(header))) + q = mul(back, tuple(row if qmask >> i & 1 else 0 for i, row in enumerate(header))) + low = (1 << d) - 1 + if any(tuple(row & low for row in a[:d]) != eye(d) for a in (p, q)): + return None + s, z = schur(p, d), schur(q, d) + return rank(add(mul(s, z), mul(z, s))) + + +def factor_census(): + checked = 0 + for d in (1, 2, 3): + for r in range(4): + all_counts, full_counts = Counter(), Counter() + xs, ys = list(matrices(d, r)), list(matrices(r, d)) + for x in xs: + for y in ys: + t = mul(x, y) + all_counts[t] += 1 + if rank(x) == rank(y) == d: + full_counts[t] += 1 + for t in matrices(d, d): + rho = rank(t) + require(all_counts[t] == unrestricted_factor(r, d, rho), "unrestricted factor count") + require(full_counts[t] == full_factor(r, d, rho), "full-rank factor count") + checked += len(xs) * len(ys) + return checked + + +def direct_small_headers(): + receipts = [] + domains = [(3, (0, 1, 1, 1), 1), (4, (1, 1, 1, 1), 1), + (4, (0, 1, 1, 2), 1), (4, (1, 1, 1, 1), 2)] + for n, profile, d in domains: + identity = sharp = total = 0 + for header in gl_headers(n): + rk = inspect_header(header, profile, d) + total += 1 + identity += rk is not None + sharp += rk == 2 * d + predicted = predict(profile, d) + require((total, identity, sharp) == (predicted["total_headers"], + predicted["identity_headers"], predicted["sharp_headers"]), "literal full-header census") + receipts.append({"n": n, "profile": profile, "d": d, "total": total, + "identity": identity, "sharp": sharp}) + return receipts + + +def scalar_pair_header(x, covector, n): + cols = [x] + span = {0} + for v in range(1, 1 << n): + if (v & covector).bit_count() % 2 == 0 and v not in span: + cols.append(v) + span |= {u ^ v for u in span} + require(len(cols) == n, "kernel completion") + return from_columns(cols, n) + + +def scalar_split_census(profile): + n = sum(profile) + sectors, pmask, qmask = masks(profile) + all_pairs = admitted = sharp = 0 + marginals = [0] * 6 + positive_headers = [] + for x in range(1, 1 << n): + for covector in range(1 << n): + if (x & covector).bit_count() % 2 != 1: + continue + all_pairs += 1 + if any((x & covector & mask).bit_count() % 2 != 1 for mask in (pmask, qmask)): + continue + admitted += 1 + conditions = [value != 0 for s in sectors[1:] for value in (x & s, covector & s)] + marginals = [count + condition for count, condition in zip(marginals, conditions)] + header = scalar_pair_header(x, covector, n) + rk = inspect_header(header, profile, 1) + require(rk is not None, "split pair has identity pivots") + require((rk == 2) == all(conditions), "scalar six-map equivalence") + if rk == 2: + sharp += 1 + positive_headers.append(header) + pred = predict(profile, 1) + require((all_pairs, admitted, sharp) == (pred["split_total"], pred["identity_splits"], + pred["sharp_splits"]), "all scalar split pairs") + return {"profile": profile, "all_pairs": all_pairs, "identity": admitted, + "sharp": sharp, "six_marginal_counts": marginals, + "marginal_product_given_identity": str(math.prod(Fraction(m, admitted) for m in marginals))}, positive_headers + + +def positive_header_completions(profile, seeds, tails): + """Enumerate every completion of each directly accepted scalar split pair.""" + seen = set() + n = sum(profile) + for seed in seeds: + for tail in tails: + change = (1,) + tuple(row << 1 for row in tail) + header = mul(seed, change) + require(inspect_header(header, profile, 1) == 2, "positive completion direct Schur rank") + key = sum(row << (n * i) for i, row in enumerate(header)) + require(key not in seen, "distinct complete headers") + seen.add(key) + require(len(seen) == predict(profile, 1)["sharp_headers"], "complete positive-header count") + return len(seen) + + +def rejects(label, call): + try: + call() + except ValueError: + return label + raise ValueError("control did not reject: " + label) + + +def main(): + factor_pairs = factor_census() + small = direct_small_headers() + profiles = [(1, 1, 1, 2), (0, 2, 2, 1)] + tails = list(gl_headers(4)) + require(len(tails) == 20160, "complete GL4 tail domain") + scalar, completed = [], [] + for profile in profiles: + receipt, seeds = scalar_split_census(profile) + scalar.append(receipt) + completed.append(positive_header_completions(profile, seeds, tails)) + examples = [predict(profile, 1) for profile in profiles] + [predict((2, 2, 2, 2), 2)] + require([r["sharp_headers"] for r in examples[:2]] == [60480, 181440], "scalar examples") + require(examples[2]["sharp_splits"] == 2592 and examples[2]["identity_splits"] == 1932288, + "d=2 example") + controls = [] + controls.append(rejects("all-headers-versus-conditioned", lambda: require( + examples[0]["sharp_density"] == examples[0]["sharp_given_identity"], "different denominators"))) + controls.append(rejects("independent-six-events", lambda: require( + scalar[0]["marginal_product_given_identity"] == examples[0]["sharp_given_identity"], + "six events are dependent"))) + controls.append(rejects("missing-completion-multiplicity", lambda: require( + examples[0]["sharp_headers"] == examples[0]["sharp_splits"], "headers are not split pairs"))) + controls.append(rejects("fourth-sector-full-rank", lambda: require( + full_factor(0, 1, 0) > 0, "inactive sector need not have full-rank maps"))) + fake = sum(unrestricted_factor(1, 1, rank(add(eye(1), h))) for h in matrices(1, 1)) + controls.append(rejects("omit-surjectivity", lambda: require( + fake == predict((1, 1, 1, 1), 1)["sharp_splits"], "injectivity alone overcounts"))) + controls.append(rejects("negative-sector", lambda: predict((-1, 1, 1, 2), 1))) + controls.append(rejects("zero-pivot-size", lambda: predict((1, 1, 1, 2), 0))) + print(json.dumps({"raw_factor_pairs": factor_pairs, "literal_small_header_censuses": small, + "scalar_split_censuses": scalar, "distinct_positive_headers": completed, + "examples": examples, "rejection_controls": controls}, sort_keys=True)) + print("PASS_SCHUR_HEADER_COUNT") + + +if __name__ == "__main__": + main()