diff --git a/research/idempotent-stabilizer-multiplicity/README.md b/research/idempotent-stabilizer-multiplicity/README.md new file mode 100644 index 0000000000..bcc52c12f7 --- /dev/null +++ b/research/idempotent-stabilizer-multiplicity/README.md @@ -0,0 +1,238 @@ +# Exact orbit multiplicities for ordered idempotents + +This scoped finite-field counting proof was produced by Nick Petalas. +Apache-2.0. It extends the factor descriptor of +[MatShep, PR4762](https://github.com/CrocSwap/integer-mult-bounds/pull/4762) +with the exact size of each simultaneous-conjugacy orbit. The new step is an +exact centralizer sequence and its extension-group order. The predecessor's +classification and active-dimension theorem are cited, not re-audited. + +The result supplies a weight for a residual state once its smaller factor-data +stabilizer is known. It does not enumerate a transition table, count passing +headers, price a physical caller or improve kappa. Independent human and formal +proof-kernel review are unclaimed. + +## Statement + +Let P,Q be ordered idempotents on an n-dimensional space V over F_q, where q +is any prime power. Use the predecessor's rank factorizations + +```text +P=XY, YX=I_r, Q=ZW, WZ=I_s, +U=F_q^r direct-sum F_q^s, +C=[X Z]:U->V, D=[Y;W]:V->U, +K=ker C, L=im D, M=DC. +``` + +Set a=rank C, b=rank D, c=rank M and + +```text +h=a-c, j=b-c, z=n-a-b+c. +``` + +All three numbers are nonnegative. The predecessor identifies n-z as the +minimum active dimension. Define the factor-data stabilizer + +```text +H = {g=diag(A,B) in GL_r(F_q) x GL_s(F_q): + gK=K, gL=L, gM=Mg}. +``` + +Write G_d(q)=|GL_d(F_q)|, with G_0(q)=1. Then the simultaneous centralizer +Z(P,Q) in GL_n(F_q) has order + +```text +|Z(P,Q)| = |H| G_z(q) q^(hj+hz+jz). (1) +``` + +Consequently the simultaneous-conjugacy orbit of the ordered pair has size + +```text +G_n(q) / (|H| G_z(q) q^(hj+hz+jz)). (2) +``` + +If the first projector is fixed to diag(I_r,0), the number of second +projectors in this pair's orbit under its centralizer is + +```text +G_r(q) G_(n-r)(q) / (|H| G_z(q) q^(hj+hz+jz)). (3) +``` + +These statements include zero ranks, full ranks, coincident projectors and +noncommuting pairs. They do not require invertibility of M. + +## Proof + +Every f in Z(P,Q) preserves im P and im Q. Their chosen image bases define +unique A in GL_r and B in GL_s with fX=XA and fZ=ZB. Commuting with P also +gives Yf=AY: indeed YP=Y, Pf=fP and YfX=A. The same argument gives Wf=BW. +Thus, with g=diag(A,B), + +```text +fC=Cg, Df=gD. (4) +``` + +These equations imply gK=K, gL=L and Mg=gM. Restriction therefore defines +a group homomorphism rho:Z(P,Q)->H. + +The map rho is surjective. For g in H, consider the two systems (C,D) and +(Cg,g^-1 D). Their C kernels, D images and DC products agree. The +inclusion/observation extension lemma of codyw912 PR4735, generalized by +MatShep PR4762, supplies an invertible f with fC=Cg and (g^-1 D)f=D. +Those are (4), which in turn imply fP=Pf and fQ=Qf. This uses the cited +extension lemma without checking its predecessor census. + +It remains to count the kernel of rho. Put A0=im C and B0=ker D. +The restriction of D to A0 has rank c, so T=A0 intersect B0 has dimension +h. Choose a complement R of T in A0, a complement Z0 of T in B0, and a +complement J of A0+B0 in V. Their dimensions are c,z,j respectively: + +```text +V = T direct-sum R direct-sum Z0 direct-sum J. +``` + +An element of ker rho fixes A0 pointwise and satisfies Df=D. Conversely +these two conditions characterize ker rho. Relative to the displayed +decomposition its matrix is exactly + +```text + T R Z0 J +T [ I 0 U V ] +R [ 0 I 0 0 ] +Z0 [ 0 0 G E ] +J [ 0 0 0 I ]. (5) +``` + +Here U is any h-by-z matrix, V any h-by-j matrix, E any z-by-j matrix, +and G any invertible z-by-z matrix. To see necessity, f-I vanishes on A0 +and takes all other vectors into B0=T direct-sum Z0. Invertibility is +equivalent to invertibility of G. Each such matrix also suffices, with no +further constraints. Hence + +```text +|ker rho| = G_z(q) q^(hz+hj+zj). +``` + +The finite exact sequence 1->ker rho->Z(P,Q)->H->1 proves (1). No splitting +of this sequence is asserted or needed. Orbit-stabilizer proves (2). +The centralizer of diag(I_r,0) is GL_r x GL_(n-r), which proves (3). + +## First fixture and checks + +Use the sharp rank-one pair displayed in MatShep's package: + +```text +P = [1 1 0], Q = [0 0 0]. + [0 0 0] [1 1 1] + [0 0 0] [0 0 0] +``` + +It has h=j=1, z=0 and |H|=q-1. Its centralizer therefore has order +q(q-1). Appending one simultaneous zero coordinate changes that order to +q^3(q-1)^2. Over F2 these orders are 2 and 8. Over F3 they are 6 and 108, +and over F5 they are 20 and 2000. These are algebraic illustrations of (1), +not newly claimed classifications of the displayed pair. + +The standalone verifier tests (1) against direct matrix commutation on +859 fixed-first-projector pairs. Each listed domain enumerates every second +projector of the specified rank. It independently checks domain completeness +against the ordinary idempotent count G_n/(G_s G_(n-s)). + +| q | n | r | s | Second projectors | +|---:|---:|---:|---:|---:| +| 2 | 4 | 1 | 1 | 120 | +| 2 | 4 | 2 | 2 | 560 | +| 3 | 3 | 1 | 2 | 117 | +| 5 | 2 | 0 | 1 | 30 | +| 5 | 2 | 1 | 0 | 1 | +| 5 | 2 | 1 | 2 | 1 | +| 5 | 2 | 2 | 1 | 30 | + +The direct count enumerates GL_r x GL_(n-r) and retains matrices commuting +with Q. The formula separately enumerates GL_r x GL_s and tests its action +on ker C, im D and M. The two centralizer calculations do not share a +commutation test for their different ambient spaces. They share elementary +finite-field matrix arithmetic. The verifier does not build class signatures +or compare the predecessor's state counts. + +Five omission controls use these direct counts to reject deletion of each +factor q^hj, q^hz, q^jz, G_z and |H|. The output records a concrete mismatch +for each detected omission. Six sharp-pair fixtures cover q=2,3,5 and z=0,1. +A capacity control rejects enumeration of all 3^(4*4) matrices. The written +proof covers extension fields; the finite checks use prime fields only. + +Every successful invocation prints a generated JSON record containing results +and SHA256 hashes of all five package files. No receipt is written by hand. + +## Reproduction and implementation limits + +From the repository root, with the local interpreter used for this package: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/idempotent-stabilizer-multiplicity/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/idempotent-stabilizer-multiplicity +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/idempotent-stabilizer-multiplicity --check-source-history +``` + +The registered checks use normal and optimized Python, with warnings treated +as errors. A reviewer can use any CPython 3.12 interpreter in place of the +machine-specific path. The verifier needs only this package and the standard +library; predecessor files are historical provenance, not runtime inputs. + +The implementation has no recursion. All census parameters are fixed in main; +no raw enumeration exceeds 65,536 matrices. Matrices have at most eight rows +and columns, and the GL cache has at most twenty entries. Each function is +under sixty lines. Python's managed runtime allocates small bounded temporary +matrices; this is the documented fixed-allocation deviation from Power of Ten. +The dataclass decorator and bounded cache are explicit library mechanisms, +rather than generated arithmetic. Explicit exceptions preserve all scientific +checks under -O. There is no external process, network access or output file. + +Computing H can still require an exponential search in r and s. Formula (1) +removes the extension-space enumeration once H is known; it is not a general +polynomial-time canonical-form algorithm or a measured runtime comparison. +No full-guard recurrence, physical header cover, recursive implementation, +precision/tape analysis or stock bound follows. No selected cold replay, Lean +or Docker run is needed or claimed. Selected kappa stays 60403/20000000. + +## Sources and scope + +Base main is 624de9dc66858af0945e5f8a0942488d62280d43, priority revision 7. +This changes the formal-interface-lemma card to a finite-field algebraic side +result. The first working orientation used research_selected_baseline.py, +the current-priorities replacement for the card's historical baseline command; +it passed the selected source-binding check. Family decision: narrow to the +orbit-weight formula and stop. A useful residual-state weight does not price +any missing physical consumer, so it justifies no construction expansion. + +- MatShep, [PR4762](https://github.com/CrocSwap/integer-mult-bounds/pull/4762), + head 3b4e0449262b0b1e07b80e009ef71cc0ca5bf816, supplies the complete + (K,L,M) descriptor, active dimension and explicit transition-multiplicity + question. Its README is pinned as historical provenance in SOURCES.json. +- codyw912, [PR4735](https://github.com/CrocSwap/integer-mult-bounds/pull/4735), + head 4afbea22e79e19d1d65702eb4090d454ee39d967, supplies the original + inclusion/observation extension argument and residual-transition context. +- Mihir Srivastava, [PR4689](https://github.com/CrocSwap/integer-mult-bounds/pull/4689), + supplies the seven-state motivation. The retained lineage includes ssafwann + PR4678/PR4671, Nick Petalas's ordered Schur/header work, Ryanson Jonathan, + lee-phys, Cinna Davis and the source527, commdata2338 and normalizer sources. + No earlier numerical result is republished as a new contribution here. + +Live PR titles/bodies, latest handoffs, active Discussions and distinct main +README and merged-PR searches found no matching formula within their coverage. +The card-wide helper snapshot searched 428 open PRs and 3,964 discussion +records, but only 111 of 6,319 local note paths were materialized then. The +separate main README search includes omitted packages. Arbitrary package files, +PR diffs and unpublished work remain outside these novelty checks. + +## Open next questions + +1. Can the factor stabilizer H be computed without enumerating GL_r x GL_s + for one actual higher-rank residual family? That is the remaining algebraic + cost in (1). First express the block-diagonal commutation and K/L constraints + as an endomorphism algebra, then count its units. The algebra's radical and + semisimple structure are not supplied here. +2. Can these orbit weights be used in a caller-specific split-transition + table? First pin one residual ensemble and count split maps into each + descriptor orbit, using (1) for its stabilizer fibers. The present theorem + supplies weights only; split incidence and all physical costs remain open. diff --git a/research/idempotent-stabilizer-multiplicity/SOURCES.json b/research/idempotent-stabilizer-multiplicity/SOURCES.json new file mode 100644 index 0000000000..6048e3297d --- /dev/null +++ b/research/idempotent-stabilizer-multiplicity/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "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/idempotent-factor-invariant/README.md", + "usage": "provenance", + "git_blob": "48ce67bdc3c7c35081cc04f86b7ee20c6a5dd06b", + "sha256": "fae88ccbea3a16d041666f5956d0416b6a21ef57a21f1a0996c7c3a74f7fa3d1" + }, + { + "path": "research/schur-invariant-transitions/README.md", + "usage": "provenance", + "git_blob": "d5118b9f5911949964245eb8942065faff972900", + "sha256": "fccdd2bff1ee00c120796bb1b6c3739cce90dcffbff7c96e897300ed81bba72e" + } + ] +} diff --git a/research/idempotent-stabilizer-multiplicity/TASK.json b/research/idempotent-stabilizer-multiplicity/TASK.json new file mode 100644 index 0000000000..787b354b05 --- /dev/null +++ b/research/idempotent-stabilizer-multiplicity/TASK.json @@ -0,0 +1,132 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "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": "Exact finite-field simultaneous-centralizer and orbit-size formula from the ordered-idempotent factor-data stabilizer, including removable zero-space extensions.", + "scope_change_reason": "MatShep PR4762 Open next question 1 asks for residual transition multiplicities. The new contribution is their algebraic orbit-weight step, not a formalization or audit of a predecessor result.", + "bottleneck_link": "Algebraic side result: residual state identity alone does not determine its multiplicity. The formula supplies orbit weights conditional on computing the factor stabilizer. It does not discharge a physical supplier obligation.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved and locally corroborated orbit-weight formula; defer transition tables and faster stabilizer algorithms.", + "outcome": "completed", + "evidence": "Written exact-sequence proof; direct centralizer equality on 859 fixed-first-projector pairs; five distinct omission controls, six sharp fixtures and a rejected oversized enumeration. Ordinary and optimized registered replay are required.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can H be counted through its endomorphism algebra without enumerating GL_r x GL_s for one actual residual family?", + "why_it_matters": "The new formula leaves H as its remaining algebraic counting cost.", + "first_step": "Write the block-diagonal commutation and K/L constraints as a finite-dimensional algebra and determine its radical.", + "blocked_by": "No radical or semisimple quotient calculation for a caller family is supplied." + }, + { + "question": "Can the new orbit weights produce one caller-specific residual split-transition table?", + "why_it_matters": "Weights do not yet count which split maps lead to each state.", + "first_step": "Pin a residual ensemble and count split incidence into the descriptor orbits.", + "blocked_by": "Split incidence and the physical header implementation remain unspecified." + } + ], + "environment": { + "python": "3.12.15", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "dependencies": "Python standard library only" + }, + "coordination": { + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19134592", + "checked_main": "624de9dc66858af0945e5f8a0942488d62280d43", + "checked_at_utc": "2026-10-22T23:42:31.569251+00:00", + "overlap_coverage": "428 live open PR title/body records, 3964 discussion records, latest handoffs; distinctive complete-main README and merged PR searches. Local helper note coverage 111/6319; arbitrary files, diffs and unpublished work not searched.", + "family_decision": "narrow to orbit weights and stop; no construction expansion" + }, + "predecessors": [ + { + "pr": 4762, + "author": "MatShep", + "head": "3b4e0449262b0b1e07b80e009ef71cc0ca5bf816", + "used": "Complete descriptor and inclusion/observation extension lemma; active-space notation." + }, + { + "pr": 4735, + "author": "codyw912", + "head": "4afbea22e79e19d1d65702eb4090d454ee39d967", + "used": "Original inclusion/observation extension argument." + }, + { + "pr": 4689, + "author": "Mihir Srivastava", + "used": "Residual-state counting motivation only." + } + ] +} diff --git a/research/idempotent-stabilizer-multiplicity/VERIFY.json b/research/idempotent-stabilizer-multiplicity/VERIFY.json new file mode 100644 index 0000000000..ac36a4ed37 --- /dev/null +++ b/research/idempotent-stabilizer-multiplicity/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 centralizer formula versus direct commutation on 859 pairs; five omission controls, six fixtures, enumeration bound and generated file-hash record." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same complete mathematical domain and controls with assertions optimized away." + } + ] +} diff --git a/research/idempotent-stabilizer-multiplicity/verify.py b/research/idempotent-stabilizer-multiplicity/verify.py new file mode 100644 index 0000000000..7abb360fc0 --- /dev/null +++ b/research/idempotent-stabilizer-multiplicity/verify.py @@ -0,0 +1,239 @@ +"""Exact corroboration of the new centralizer formula; standard library only.""" + +import hashlib +import itertools +import json +import platform +from dataclasses import dataclass +from functools import lru_cache +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +@dataclass(frozen=True) +class Matrix: + n: int + m: int + rows: tuple + + def __post_init__(self): + require(0 <= self.n <= 8 and 0 <= self.m <= 8, "matrix capacity") + require(len(self.rows) == self.n, "row count") + require(all(len(row) == self.m for row in self.rows), "column count") + + +def matrix(n, m, entries): + values = tuple(entries) + require(len(values) == n * m, "entry count") + return Matrix(n, m, tuple(values[i*m:(i+1)*m] for i in range(n))) + + +def identity(n): + return matrix(n, n, (int(i == j) for i in range(n) for j in range(n))) + + +def multiply(a, b, q): + require(a.m == b.n, "product dimensions") + return matrix(a.n, b.m, ( + sum(a.rows[i][k] * b.rows[k][j] for k in range(a.m)) % q + for i in range(a.n) for j in range(b.m))) + + +def transpose(a): + return matrix(a.m, a.n, (a.rows[i][j] for j in range(a.m) for i in range(a.n))) + + +def horizontal(a, b): + require(a.n == b.n, "horizontal dimensions") + return Matrix(a.n, a.m+b.m, tuple(x+y for x, y in zip(a.rows, b.rows))) + + +def vertical(a, b): + require(a.m == b.m, "vertical dimensions") + return Matrix(a.n+b.n, a.m, a.rows+b.rows) + + +def block_diagonal(a, b): + rows = tuple(row+(0,)*b.m for row in a.rows) + rows += tuple((0,)*a.m+row for row in b.rows) + return Matrix(a.n+b.n, a.m+b.m, rows) + + +def reduce_rows(a, q): + rows = [list(row) for row in a.rows] + pivots = [] + for col in range(a.m): + if len(pivots) == a.n: + break + candidates = [i for i in range(len(pivots), a.n) if rows[i][col]] + if not candidates: + continue + pos = len(pivots) + selected = candidates[0] + rows[pos], rows[selected] = rows[selected], rows[pos] + scale = pow(rows[pos][col], -1, q) + rows[pos] = [x * scale % q for x in rows[pos]] + for i in range(a.n): + if i != pos: + factor = rows[i][col] + rows[i] = [(x-factor*y) % q for x, y in zip(rows[i], rows[pos])] + pivots.append(col) + return Matrix(a.n, a.m, tuple(tuple(row) for row in rows)), tuple(pivots) + + +def rank(a, q): + return len(reduce_rows(a, q)[1]) + + +def inverse(a, q): + require(a.n == a.m, "inverse dimensions") + reduced, pivots = reduce_rows(horizontal(a, identity(a.n)), q) + require(pivots == tuple(range(a.n)), "singular inverse") + return Matrix(a.n, a.n, tuple(row[a.n:] for row in reduced.rows)) + + +def factor(projector, q): + n = projector.n + pivots = reduce_rows(projector, q)[1] + r = len(pivots) + x = matrix(n, r, (projector.rows[i][j] for i in range(n) for j in pivots)) + chosen = reduce_rows(transpose(x), q)[1] + square = Matrix(r, r, tuple(x.rows[i] for i in chosen)) + selected = Matrix(r, n, tuple(projector.rows[i] for i in chosen)) + y = multiply(inverse(square, q), selected, q) + require(multiply(x, y, q) == projector, "factor reconstruction") + require(multiply(y, x, q) == identity(r), "projector factor identity") + return x, y + + +def gl_order(n, q): + value = 1 + for i in range(n): + value *= q**n - q**i + return value + + +@lru_cache(maxsize=20) +def general_linear(n, q): + require(q in (2, 3, 5) and q**(n*n) <= 65536, "enumeration capacity") + result = tuple(a for entries in itertools.product(range(q), repeat=n*n) + if rank(a := matrix(n, n, entries), q) == n) + require(len(result) == gl_order(n, q), "GL enumeration") + return result + + +def data(p, t, q): + x, y = factor(p, q) + z, w = factor(t, q) + c_map, d_map = horizontal(x, z), vertical(y, w) + m_map = multiply(d_map, c_map, q) + a, b, c = rank(c_map, q), rank(d_map, q), rank(m_map, q) + return c_map, d_map, m_map, a-c, b-c, p.n-a-b+c, x.m, z.m + + +def factor_stabilizer(c_map, d_map, m_map, r, s, q): + a, b = rank(c_map, q), rank(d_map, q) + count = 0 + for left in general_linear(r, q): + for right in general_linear(s, q): + g = block_diagonal(left, right) + if multiply(m_map, g, q) != multiply(g, m_map, q): + continue + if rank(vertical(c_map, multiply(c_map, g, q)), q) != a: + continue + if rank(horizontal(d_map, multiply(g, d_map, q)), q) != b: + continue + count += 1 + require(count > 0, "identity missing from factor stabilizer") + return count + + +def predicted(p, t, q): + c_map, d_map, m_map, h, j, z, r, s = data(p, t, q) + require(min(h, j, z) >= 0, "negative decomposition dimension") + stabilizer = factor_stabilizer(c_map, d_map, m_map, r, s, q) + value = stabilizer * gl_order(z, q) * q**(h*j + h*z + j*z) + return value, (h, j, z, stabilizer) + + +def fixed_first_centralizer(n, r, q): + return tuple(block_diagonal(a, b) for a in general_linear(r, q) + for b in general_linear(n-r, q)) + + +def census(n, r, s, q): + require(n <= 4 and q**(n*n) <= 65536, "projector domain capacity") + p = matrix(n, n, (int(i == j and i < r) for i in range(n) for j in range(n))) + ambient = fixed_first_centralizer(n, r, q) + count, histogram, mutations = 0, {}, {} + for entries in itertools.product(range(q), repeat=n*n): + t = matrix(n, n, entries) + if multiply(t, t, q) != t or rank(t, q) != s: + continue + expected, (h, j, z, stabilizer) = predicted(p, t, q) + actual = sum(multiply(f, t, q) == multiply(t, f, q) for f in ambient) + require(actual == expected, f"centralizer mismatch: {(n,r,s,q,t)}") + require(gl_order(n, q) % actual == 0, "nonintegral orbit") + divisors = {"omit_hj": q**(h*j), "omit_hz": q**(h*z), + "omit_jz": q**(j*z), "omit_GLz": gl_order(z, q), + "omit_factor_stabilizer": stabilizer} + for name, divisor in divisors.items(): + if divisor > 1 and name not in mutations: + require(actual != expected // divisor, "omission survived direct count") + mutations[name] = {"actual": actual, "mutant": expected // divisor, + "h": h, "j": j, "z": z} + histogram[actual] = histogram.get(actual, 0) + 1 + count += 1 + total = gl_order(n, q) // (gl_order(s, q)*gl_order(n-s, q)) + require(count == total, "incomplete projector census") + return {"q": q, "n": n, "r": r, "s": s, "pairs": count, + "centralizer_histogram": histogram, "omission_controls": mutations} + + +def fixture_checks(): + fixtures = [] + p0 = matrix(3, 3, (1, 1, 0, 0, 0, 0, 0, 0, 0)) + t0 = matrix(3, 3, (0, 0, 0, 1, 1, 1, 0, 0, 0)) + for q in (2, 3, 5): + for z in (0, 1): + zero = matrix(z, z, (0 for _ in range(z*z))) + p, t = block_diagonal(p0, zero), block_diagonal(t0, zero) + actual, (h, j, padding, stabilizer) = predicted(p, t, q) + require((h, j, padding, stabilizer) == (1, 1, z, q-1), "sharp fixture") + expected = (q-1)*gl_order(z, q)*q**(1+2*z) + require(actual == expected, "sharp fixture order") + fixtures.append({"q": q, "z": z, "centralizer": actual}) + require(gl_order(0, 2) == 1, "zero-dimensional GL") + try: + general_linear(4, 3) + except ValueError: + pass + else: + raise ValueError("oversized enumeration admitted") + return fixtures + + +def main(): + domains = ((4, 1, 1, 2), (4, 2, 2, 2), (3, 1, 2, 3), + (2, 0, 1, 5), (2, 1, 0, 5), (2, 1, 2, 5), (2, 2, 1, 5)) + checks = [census(*domain) for domain in domains] + fixtures = fixture_checks() + omitted = {name for check in checks for name in check["omission_controls"]} + require(omitted == {"omit_hj", "omit_hz", "omit_jz", "omit_GLz", + "omit_factor_stabilizer"}, "missing omission control") + package = Path(__file__).resolve().parent + hashes = {name: hashlib.sha256((package/name).read_bytes()).hexdigest() + for name in ("README.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py")} + print(json.dumps({"status": "PASS_IDEMPOTENT_STABILIZER_MULTIPLICITY", + "python": platform.python_version(), "checks": checks, + "fixtures": fixtures, "distinct_omissions_rejected": len(omitted), + "oversized_domain_rejected": True, + "source_sha256": hashes}, sort_keys=True)) + + +if __name__ == "__main__": + main()