diff --git a/research/pattern-pool-cardinality/PROOF.md b/research/pattern-pool-cardinality/PROOF.md new file mode 100644 index 0000000000..4fce5d3b6a --- /dev/null +++ b/research/pattern-pool-cardinality/PROOF.md @@ -0,0 +1,134 @@ +# Sharp binary off-diagonal pool cardinality + +This scoped proof was produced by Nick Petalas. Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. + +## Model and theorem + +Let W>=1, and let V be a d-dimensional linear subspace of the zero-diagonal +matrices in M_W(F2). Write off(N) for N with its diagonal deleted. Define + +``` +P(V) = {N : rank(N)=1, N^2=N, off(N) in V, off(N)!=0}. +``` + +These are scalar projectors, with no rational address frames or word order. +In particular, coordinate projectors do not belong to P(V). +Let R(V) be the nonzero elements of V which occur as off(N), and let e(V) +count the matrix units E_ij in V with i!=j. + +**Theorem.** For every W and V, + +``` +|P(V)| = |R(V)| + e(V) <= 2^d + d - 1. +``` + +For every d>=1 and W>=d+1, some V attains equality. For d=0 the pool is +empty. Thus the maximum over all ambient register counts is exactly +2^d+d-1. This does not assert attainment at every smaller feasible W. + +## 1. All fibers of diagonal deletion + +**Lemma.** A realizable nonzero off-diagonal pattern has exactly one +rank-one-idempotent lift, except when it is a matrix unit E_ab with a!=b. +That pattern has precisely the two lifts + +``` +E_aa + E_ab = e_a (e_a+e_b)^T, +E_bb + E_ab = (e_a+e_b) e_b^T. +``` + +To prove this, suppose distinct rank-one idempotents N and M have the same +off-diagonal pattern. Then D=N+M is a nonzero diagonal matrix of rank at +most two. A rank-one idempotent has trace one, so trace(D)=0 in F2. +The number of nonzero diagonal entries of D is therefore even and at most +two. It is exactly two, at positions a and b. + +Write N=x y^T and M=u v^T, with y^T x=v^T u=1. The rank-two image of D +is contained in span(x,u), so that span equals span(e_a,e_b). Applying the +same argument to D^T puts y and v in span(e_a,e_b). Both projectors are +therefore supported on the same two-by-two coordinate block, and differ +there by the identity. + +For completeness, the rank-one idempotents on that binary block are + +``` +[[1,0],[0,0]], [[0,0],[0,1]], +[[1,1],[0,0]], [[0,1],[0,1]], +[[1,0],[1,0]], [[0,0],[1,1]]. +``` + +This list follows by taking nonzero x,y in F2^2 with y^T x=1. +The only repeated nonzero off-diagonal patterns are the two single edges. +Their displayed lifts work in every ambient dimension. Any third lift +would, by the same argument with N, have to be in this list. This proves +the lemma. The zero pattern has the W coordinate projectors as its lifts; +its exclusion is essential. + +woklerx's PR1456 already proves uniqueness for cyclic patterns. The lemma +retains that conclusion and treats every acyclic pattern and every +ambient dimension as well. The rank and trace facts are standard linear +algebra, not new methods claimed here. + +## 2. Exact count and upper bound + +Every pattern in R(V) contributes one projector. By the lemma, the only +extra projectors are one additional lift for each E_ij in V. All these +matrix units are realizable, so the exact count is |R(V)|+e(V). + +There are at most 2^d-1 nonzero vectors in V. Distinct off-diagonal matrix +units are linearly independent, since they have disjoint one-entry +supports. A d-dimensional V consequently contains at most d of them. +The asserted upper bound follows. + +One consequence useful before a scalar-pool search is + +``` +dim(sum_{N in P(V)} im(N)) <= |P(V)| <= 2^d+d-1. +``` + +The joint image is invariant under every projector in the pool. If the pool +is nonempty and W>2^d+d-1, it is a nonzero proper common invariant subspace. +This is a necessary restriction on the pool alone. Adding coordinate +projectors or other patterns to a chronological word can invalidate this +particular invariant subspace. + +## 3. A family attaining the bound + +Use coordinates 0,1,...,d, padding by arbitrary further coordinates if +W>d+1. Let + +``` +V = span(E_01, E_02, ..., E_0d). +``` + +For every nonempty subset J of {1,...,d}, the projector + +``` +N_J = e_0 (e_0 + sum_{j in J} e_j)^T +``` + +has off-diagonal pattern sum_{j in J} E_0j. Thus all 2^d-1 nonzero patterns +in V are realized. Exactly d of them are single edges, and their second +lifts are (e_0+e_j)e_j^T. These projectors are distinct and give precisely +2^d-1+d elements of P(V), proving sharpness. The fiber lemma excludes +additional lifts on padded coordinates. + +## Scope and predecessor boundary + +PR1456's open question asks for further pattern-space classification at +relation nullity two. This result gives an exact all-dimension size bound +before such a classification. PR1846's four-role flag and reducibility +census is cited context, not a dependency of this proof and not replayed. +Neither its flags nor any predecessor count is used above. + +The field is specifically F2. For example, over F7 the distinct matrices +[[3,1],[1,5]] and [[5,1],[1,3]] are rank-one idempotents with the same +two-edge cyclic pattern, so the fiber lemma does not carry over unchanged. +The finite verifier checks this boundary literally. + +No rational-frame feasibility, two-relation word, native implementation, +physical restoration, full cost invoice, supplier admission, improved kappa +or complete multiplication theorem follows from this scalar count. The +finite checks corroborate the written proof and do not establish its +unbounded quantifiers by enumeration. diff --git a/research/pattern-pool-cardinality/README.md b/research/pattern-pool-cardinality/README.md new file mode 100644 index 0000000000..ae404ea1d8 --- /dev/null +++ b/research/pattern-pool-cardinality/README.md @@ -0,0 +1,117 @@ +# A sharp size bound for binary scalar pattern pools + +For every d-dimensional off-diagonal pattern space over F2, the pool of +rank-one idempotents with a nonzero pattern has at most `2^d+d-1` elements, +independently of the number of registers. A common-row construction attains +the bound whenever at least d+1 registers are available. In particular, +two-dimensional spaces have at most five noncoordinate projectors. + +Claim type: scoped written mathematical proof with finite exact corroboration. +This contribution was produced by Nick Petalas. Apache-2.0. Independent human +and formal proof-kernel review are unclaimed. + +[PROOF.md](PROOF.md) gives the complete argument. Deleting the diagonal has +one lift per realizable nonzero pattern, except a single directed edge has +two. A d-dimensional space contains at most d distinct edge patterns. The +exact count is the number of realized nonzero patterns plus the number of +matrix units in the space. No predecessor scientific suite is imported or run. + +## Evidence and reproduction + +The read-only standard-library verifier enumerates binary projectors on five +and six registers. A separate oracle tries every diagonal completion for +every realized pattern, including the zero-pattern boundary. It also checks +all pairs of distinct realized five-register patterns, explicit attaining +stars through dimension ten with padded spectators, and semantic controls. +These checks corroborate the new proof, rather than reproducing the +four-register flag classification. + +Local CPython 3.12.15 checks pass for 2,501 noncoordinate projectors, +141,888 diagonal completions, 110,685 spanning pairs and 55 attaining star +shapes containing 4,237 literal projectors. Five malformed dimensions and +seven semantic control groups pass. Three disposable optimized-code mutants +reject a missing edge charge, missing second lifts and admitted nilpotents. +The two registered commands took 0.305 and 0.261 seconds in individual local +runs, below their 120-second limits. These timings check the replay budget. + +From the repository root, run: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/pattern-pool-cardinality/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/pattern-pool-cardinality/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/pattern-pool-cardinality +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/pattern-pool-cardinality --check-source-history +``` + +Any CPython 3.12 executable may replace this installation path. A direct run +prints `PASS_PATTERN_POOL_CARDINALITY` followed by a generated JSON receipt +with exact counts and SHA256 hashes of all six package files. Save stdout +outside the checkout. There is no handwritten scientific receipt. Direct +replay works without Git or network; provenance validation needs full Git +history. The verifier does not read predecessor files at runtime. + +## Sources, scope and stopping decision + +The source question is the Open next questions section of woklerx's +[PR1456](https://github.com/CrocSwap/integer-mult-bounds/pull/1456), at +`83b6ad2ace819a96128131a3600ee914a66dd0dd`. Its cyclic-pattern uniqueness +argument and arbitrary-role Laurent method retain their credit. Ali Romman, +eumemic and the register-model lineage remain predecessor credit. +woklerx's [PR1846](https://github.com/CrocSwap/integer-mult-bounds/pull/1846) +supplies the separate finite four-role flag classification. Neither result +is audited here. Exact retained source blobs are pinned in SOURCES.json. + +Base canonical main is `de5ec2e7a6074068452f45b1a191b5c72832df4a`, priority +revision eight. The selected-baseline metadata control passed. The card is +changed to a scalar reconstruction side result. It supplies a bounded pool +before word synthesis, and meets no native supplier acceptance gate. +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19217787) +records this scope. Stop at the sharp size theorem; no word search is reserved. + +The joint image of the pool has dimension at most its size, giving a proper +common invariant subspace when the ambient dimension exceeds the bound and +the pool is nonempty. Coordinate projectors are excluded. Interleaving them +can destroy this particular invariant subspace. This does not eliminate a +complete two-relation word or extend the rational span-six obstruction of +PR5231, which has different premises and a different conclusion. + +Entry searches covered live open PR bodies, recent account PRs, active +Discussions and the latest handoff comments, the cached card search, merged +pattern/dihedral searches, and all main package READMEs for distinctive +pattern/fiber/count terms. The cached helper reports sparse local omissions; +Git searches cover committed READMEs, not arbitrary nested code, unpublished +work or every historical PR body. No match is not proof of novelty. + +The selected frontier is unchanged. Rational address frames, chronology, +full native/physical/precision/tape/ownership costs, independent targets, +compiler admission and the complete multiplication theorem remain outside +scope. No Lean, Docker, historical scientific replay or selected operator +replay is run. The universal result rests on the written proof. + +## Open next questions + +- Which pattern spaces attain the maximum? Begin by imposing equality in + both the realized-pattern and edge counts, then classify the resulting + directed-edge sets. This could remove redundant extremal search families; + the present proof supplies an attaining family without classifying all of them. +- What is the sharp joint-image dimension at fixed d? The cardinality bound + gives a finite ambient threshold for irreducible pools, but can be loose. + Start with d=2 and retain every possible diagonal lift. Adding coordinate + gates to full words is a separate obstacle. + +Structured questions and blockers are in TASK.json. + +## Verifier implementation limits + +All loops have fixed finite domains. Exhaustive oracle widths are five and +six; stars use at most eleven registers and dimension ten. The plane pass +accepts at most 500 realized patterns and counts spanning pairs, not distinct +planes. No recursion, subprocess, network or scientific output write occurs. +Python dynamically allocates bounded tuples/maps; static allocation is not +available in this runtime. At most the fixed projector/fiber tables, a +64-completion oracle set and one star of at most 1,033 projectors are live. +Functions are below sixty physical lines. Explicit exception checks survive +optimized execution, and registered commands make warnings errors. Package +hashing reads exactly six bounded source files. +Syntax compilation and the standard-library indentation check pass. No +dedicated linter is installed on this host. diff --git a/research/pattern-pool-cardinality/SOURCES.json b/research/pattern-pool-cardinality/SOURCES.json new file mode 100644 index 0000000000..f8a59e36bb --- /dev/null +++ b/research/pattern-pool-cardinality/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/bit-one-relation-any-registers/README.md", + "usage": "provenance", + "git_blob": "7453a3f10c9cbaad746f108dc65dcfc514d0fdb5", + "sha256": "1f2899320e646a4158531c3f8260ba32b4761ae883fdb5bce4d3e3b0a4d8cb8c" + }, + { + "path": "research/bit-one-relation-any-registers/PROOF.md", + "usage": "provenance", + "git_blob": "9b42c6cd2e93514bd8c5247e2ef2d516d6603ae6", + "sha256": "38805f881d0bd625418fd8bdc9410d06fe3873374db9678c722d13abd3bfe392" + }, + { + "path": "research/bit-four-role-two-patterns/README.md", + "usage": "provenance", + "git_blob": "e79087d9cd8f4473e6e48fa4e521902b7809f3a4", + "sha256": "e4ee830e783b20bfb0886ae8c91133a6138157ed5dcaac90ce16ddc616c8d49f" + }, + { + "path": "docs/research/current-priorities.md", + "usage": "provenance", + "git_blob": "6f5d40d13d8f3bdc12ce7954c8c3eb4ab1f8be91", + "sha256": "70f61c8d140ae6e892f2b8f065bba4eae3e76f7a8f55f632fd4e2f9f34039bdc" + } + ] +} diff --git a/research/pattern-pool-cardinality/TASK.json b/research/pattern-pool-cardinality/TASK.json new file mode 100644 index 0000000000..d777ffa0ca --- /dev/null +++ b/research/pattern-pool-cardinality/TASK.json @@ -0,0 +1,94 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Sharp universal cardinality of noncoordinate binary rank-one-idempotent pools in a d-dimensional off-diagonal pattern space, with an explicit attaining common-row family.", + "scope_change_reason": "The card is changed from native larger-register construction to a scalar reconstruction side result, following the explicit pattern-space classification question in woklerx PR1456. It neither realizes a rational two-relation word nor extends the separate PR5231 rational span-six obstruction.", + "bottleneck_link": "Side result: a fixed pattern dimension gives a sharp finite pool size independent of ambient register count, before any chronological word or native supplier search. The original native acceptance gate remains unmet.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified sharp pool-size theorem and its attaining family. No word synthesis, flag census, successor construction or supplier expansion.", + "outcome": "completed", + "evidence": "PROOF.md establishes |P(V)|=|R(V)|+e(V)<=2^d+d-1 and sharpness for W>=d+1. New exact checks enumerate 2501 noncoordinate projectors on five/six roles, 141888 diagonal completions, 110685 five-role spanning pairs and 55 attaining star shapes containing 4237 literal projectors.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Which off-diagonal pattern spaces attain the cardinality maximum?", + "why_it_matters": "An equality classification could remove redundant extremal families before word synthesis.", + "first_step": "Impose equality in the realized-pattern and matrix-unit counts, then classify the directed-edge sets.", + "blocked_by": "This contribution proves one attaining common-row family but does not classify every maximizing space." + }, + { + "question": "What is the sharp joint-image dimension at fixed pattern dimension?", + "why_it_matters": "It could lower the ambient threshold beyond which a nonempty pool must be reducible.", + "first_step": "Start with d=2 while retaining every possible diagonal lift.", + "blocked_by": "Cardinality bounds the image dimension but may be loose; adding coordinate gates to full words has a separate contract." + } + ], + "claim_type": "scoped-proof", + "coordination": { + "thread": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166", + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19217787", + "question_source": "https://github.com/CrocSwap/integer-mult-bounds/pull/1456", + "source_author": "woklerx" + }, + "environment": { + "python": "3.12.15", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "dependencies": "standard library only" + }, + "selection": { + "nonce": "818e3fc81a233da670922d7f4978c24b", + "selected_task": "bit-new-register-model", + "first_step": "research_selected_baseline.py returned PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "overlap_scope": "Live open PR bodies, account PRs, latest handoff comments and active Discussions; cached task search with sparse local omissions; committed README Git searches and targeted merged PR searches. Arbitrary code diffs and unpublished work are not fully covered." + }, + "freshness": { + "upstream_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "priority_revision": 8, + "checked_at_utc": "2026-10-27T13:34:41.308690+00:00", + "decision": "Continue completed scoped theorem. Canonical main and relevant guidance are unchanged; live claims and new PR titles are disjoint. Cached card overlap covered 470 open PRs and 5426 Discussion records with complete remote pagination; sparse local omissions were supplemented by committed README searches." + } +} diff --git a/research/pattern-pool-cardinality/VERIFY.json b/research/pattern-pool-cardinality/VERIFY.json new file mode 100644 index 0000000000..65e2d3ff61 --- /dev/null +++ b/research/pattern-pool-cardinality/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "New fiber/count theorem via complete five/six-role diagonal-completion oracle, all five-role realized-pattern spanning pairs, attaining stars and semantic controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete scientific checks with Python assertions disabled." + } + ] +} diff --git a/research/pattern-pool-cardinality/verify.py b/research/pattern-pool-cardinality/verify.py new file mode 100644 index 0000000000..47152cd24b --- /dev/null +++ b/research/pattern-pool-cardinality/verify.py @@ -0,0 +1,192 @@ +#!/usr/bin/env python3 +"""Exact corroboration of the binary off-diagonal pool theorem. + +Produced by Nick Petalas. Apache-2.0. +No predecessor executable or external scientific input is imported. +""" + +import hashlib +import json +from pathlib import Path +import sys + + +PACKAGE_FILES = ( + "PROOF.md", "README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py" +) + + +def need(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def bound(d: int) -> int: + need(type(d) is int and 0 <= d <= 10, "unsupported pattern dimension") + return (1 << d) + d - 1 + + +def outer(x: int, y: int, n: int) -> tuple[int, ...]: + need(0 < x < 1 << n and 0 < y < 1 << n, "invalid outer-product vectors") + return tuple(y if x >> i & 1 else 0 for i in range(n)) + + +def pattern(rows: tuple[int, ...]) -> int: + n = len(rows) + need(1 <= n <= 11, "unsupported matrix width") + return sum((row & ~(1 << i)) << (n * i) for i, row in enumerate(rows)) + + +def projector(rows: tuple[int, ...]) -> bool: + """Recognize rank one and idempotence from the literal row action.""" + n = len(rows) + need(1 <= n <= 11, "unsupported matrix width") + need(all(type(row) is int and 0 <= row < 1 << n for row in rows), "bad row") + pivot = next((row for row in rows if row), 0) + if not pivot or any(row not in (0, pivot) for row in rows): + return False + image = sum(1 << i for i, row in enumerate(rows) if row) + return (pivot & image).bit_count() % 2 == 1 + + +def fibers(n: int) -> dict[int, set[tuple[int, ...]]]: + need(n in (5, 6), "census width must be five or six") + result: dict[int, set[tuple[int, ...]]] = {} + for x in range(1, 1 << n): + for y in range(1, 1 << n): + if (x & y).bit_count() % 2: + rows = outer(x, y, n) + code = pattern(rows) + if code: + result.setdefault(code, set()).add(rows) + return result + + +def diagonal_oracle(code: int, n: int) -> set[tuple[int, ...]]: + """Try every diagonal completion, independently of the outer-product list.""" + need(n in (5, 6), "unsupported exhaustive oracle width") + mask = (1 << n) - 1 + off = tuple(code >> (n * i) & mask for i in range(n)) + need(all(row >> i & 1 == 0 for i, row in enumerate(off)), "nonzero diagonal") + result = set() + for diagonal in range(1 << n): + rows = tuple(row | ((diagonal >> i & 1) << i) for i, row in enumerate(off)) + if projector(rows): + result.add(rows) + return result + + +def check_fibers(n: int) -> tuple[dict[int, set[tuple[int, ...]]], dict[str, int]]: + data = fibers(n) + matrices = sum(len(value) for value in data.values()) + for code, value in data.items(): + need(value == diagonal_oracle(code, n), "diagonal oracle disagrees") + expected = 2 if code.bit_count() == 1 else 1 + need(len(value) == expected, "nonzero-pattern fiber theorem fails") + if expected == 2: + position = code.bit_length() - 1 + i, j = divmod(position, n) + a = outer(1 << i, (1 << i) | (1 << j), n) + b = outer((1 << i) | (1 << j), 1 << j, n) + need(value == {a, b}, "wrong single-edge lifts") + zeros = diagonal_oracle(0, n) + need(len(zeros) == n, "zero fiber must contain every coordinate projector") + return data, { + "width": n, + "noncoordinate_projectors": matrices, + "nonzero_patterns": len(data), + "diagonal_completions": (len(data) + 1) * (1 << n), + } + + +def check_planes(data: dict[int, set[tuple[int, ...]]]) -> dict[str, int]: + codes = sorted(data) + need(len(codes) <= 500, "plane enumeration capacity exceeded") + pairs = 0 + maximum = 0 + for index, p in enumerate(codes): + for q in codes[index + 1:]: + vectors = (p, q, p ^ q) + actual = sum(len(data.get(code, ())) for code in vectors) + realized = sum(code in data for code in vectors) + edges = sum(code.bit_count() == 1 for code in vectors) + need(actual == realized + edges, "exact pool identity fails") + need(actual <= bound(2), "two-dimensional pool exceeds bound") + maximum = max(maximum, actual) + pairs += 1 + need(maximum == bound(2), "sharp two-dimensional witness absent") + return {"spanning_pairs": pairs, "maximum_pool_size": maximum} + + +def star(d: int, n: int) -> tuple[tuple[int, ...], ...]: + need(1 <= d <= 10 and d + 1 <= n <= 11, "invalid star shape") + primary = tuple(outer(1, 1 | (subset << 1), n) for subset in range(1, 1 << d)) + secondary = tuple(outer(1 | (1 << j), 1 << j, n) for j in range(1, d + 1)) + return primary + secondary + + +def check_stars() -> dict[str, int]: + total = 0 + shapes = 0 + for d in range(1, 11): + for n in range(d + 1, 12): + pool = star(d, n) + need(len(set(pool)) == len(pool) == bound(d), "star cardinality fails") + grouped: dict[int, int] = {} + for rows in pool: + need(projector(rows), "star has a nonprojector") + code = pattern(rows) + need(code != 0, "coordinate projector entered star") + grouped[code] = grouped.get(code, 0) + 1 + need(len(grouped) == (1 << d) - 1, "star omits a nonzero pattern") + need(sum(code.bit_count() == 1 for code in grouped) == d, "bad star edges") + for code, size in grouped.items(): + need(size == (2 if code.bit_count() == 1 else 1), "bad star fiber") + total += len(pool) + shapes += 1 + return {"shapes": shapes, "literal_projectors": total} + + +def check_controls() -> dict[str, int]: + rejected = 0 + for invalid in (-1, 11, True, 1.0, "2"): + try: + bound(invalid) + except ValueError: + rejected += 1 + need(rejected == 5, "dimension validation failed") + need(bound(0) == 0, "zero-dimensional noncoordinate pool must be empty") + need(not projector((0, 0)), "zero matrix accepted") + need(not projector((1, 2)), "rank-two matrix accepted") + need(not projector((3, 3)), "rank-one nilpotent accepted") + need(projector((1, 0)) and pattern((1, 0)) == 0, "coordinate control fails") + # Over F7 two distinct cyclic-pattern projectors have the same off-diagonal. + odd = (((3, 1), (1, 5)), ((5, 1), (1, 3))) + for rows in odd: + square = tuple(tuple(sum(rows[i][k] * rows[k][j] for k in range(2)) % 7 + for j in range(2)) for i in range(2)) + need(square == rows and (rows[0][0] * rows[1][1] - 1) % 7 == 0, + "odd-characteristic scope control fails") + need(odd[0] != odd[1], "odd-field example collapsed") + return {"invalid_dimensions_rejected": rejected, "semantic_groups": 7} + + +def main() -> None: + need(len(sys.argv) == 1, "this fixed-domain verifier takes no arguments") + first, first_counts = check_fibers(5) + _, second_counts = check_fibers(6) + counts = { + "fibers": [first_counts, second_counts], + "planes": check_planes(first), + "attaining_stars": check_stars(), + "controls": check_controls(), + } + root = Path(__file__).resolve().parent + hashes = {name: hashlib.sha256((root / name).read_bytes()).hexdigest() + for name in PACKAGE_FILES} + print("PASS_PATTERN_POOL_CARDINALITY") + print(json.dumps({"counts": counts, "package_sha256": hashes}, sort_keys=True)) + + +if __name__ == "__main__": + main()