From fc36a3b8636a200de26f55aaa7393a05b8ee3f69 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 22 Oct 2026 21:43:44 +0100 Subject: [PATCH] feat(research): prove the binary first-pivot quarter law --- .../generic-idempotent-first-guard/README.md | 217 ++++++++++++++++++ .../SOURCES.json | 30 +++ .../generic-idempotent-first-guard/TASK.json | 163 +++++++++++++ .../VERIFY.json | 34 +++ .../generic-idempotent-first-guard/verify.py | 203 ++++++++++++++++ 5 files changed, 647 insertions(+) create mode 100644 research/generic-idempotent-first-guard/README.md create mode 100644 research/generic-idempotent-first-guard/SOURCES.json create mode 100644 research/generic-idempotent-first-guard/TASK.json create mode 100644 research/generic-idempotent-first-guard/VERIFY.json create mode 100644 research/generic-idempotent-first-guard/verify.py diff --git a/research/generic-idempotent-first-guard/README.md b/research/generic-idempotent-first-guard/README.md new file mode 100644 index 0000000000..2e8829f28c --- /dev/null +++ b/research/generic-idempotent-first-guard/README.md @@ -0,0 +1,217 @@ +# The binary first-pivot quarter law + +This scoped counting proof was produced by Nick Petalas. Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. + +For every ordered pair of idempotents S,T over **F2** with invertible +commutator, exactly **one quarter** of complete uniform headers have both +first pivots nonzero. This is a dimension-uniform first-pivot count. It supplies +no full-guard chain, physical header cover, supplier admission or new kappa. +The theorem is restricted to F2. + +This answers one bounded transition-count question left open by MatShep's +[#4762](https://github.com/CrocSwap/integer-mult-bounds/pull/4762) and +codyw912's [#4735](https://github.com/CrocSwap/integer-mult-bounds/pull/4735). +Their factor invariant, split recurrence and the earlier seven-state table +are predecessors, not audit targets. The block reduction below is elementary +background; the contribution is the explicit header count and its proof. + +## Statement + +Let V be a positive-dimensional finite vector space over F2. Suppose S,T are +idempotents on V and C=ST-TS is invertible. Then dim V=2r and both projectors +have rank r, with r>=2. For a complete header G in GL_(2r)(F2), the first pivots +are the leading entries of G^-1 S G and G^-1 T G. The number of headers on which +both pivots are nonzero is exactly + +```text +|GL_(2r)(F2)| / 4. (1) +``` + +Equivalently, let a be the first column of G and beta the first row of G^-1. +A split satisfies beta(a)=1. Exactly + +```text +g(r) = 2^(2r-3) (2^(2r)-1) (2) +``` + +splits have beta(Sa)=beta(Ta)=1. Each has |GL_(2r-1)(F2)| complete-header +extensions. Nonzero and equal-to-one pivots coincide over this field. + +No assumption about a preceding commuting pair or Schur deletion is made. +The result covers any ordered pair satisfying the displayed binary hypotheses. +It does not assert that the residual pair after a successful pivot has an +invertible commutator, so (1) cannot be iterated without further work. + +## Proof + +### Reduce to one compression + +Use V=im S direct-sum ker S. In these coordinates write + +```text +S = [I 0], T = [A B], ST-TS = [0 B]. + [0 0] [C D] [C 0] +``` + +Invertibility of ST-TS forces B and C to be isomorphisms, so the two summands +have the same dimension r. Choose bases with B=I and rename the other blocks. +The top blocks of T^2=T give C=A+A^2 and D=I+A. Thus + +```text +S = [I 0], T = [A I ]. (3) + [0 0] [A(I+A) I+A] +``` + +Both A and I+A are invertible. The image of T is exactly +`{(z,(I+A)z): z in F2^r}`, so its rank is r. If r=1, the binary scalar A would +have to differ from both zero and one, which is impossible. Thus r>=2. +A simultaneous change of basis bijects complete headers and preserves their +pivot values, so it suffices to count (3). + +### Count first vectors and functionals + +Put a=(x,y) and N=2^r-1. If x=0 then Sa=0 and admission fails. Fix a nonzero x. +We have + +```text +Sa = (x,0), +Ta = (Ax+y, (I+A)(Ax+y)). (4) +``` + +The three values `y=0`, `y=Ax`, and `y=(I+A)x` are distinct, since x, Ax and +(I+A)x are all nonzero. When y=0, the vectors a=Sa and Ta are independent, +because A(I+A)x is nonzero. When y=(I+A)x, the vectors a=Ta and Sa are +independent. Each case therefore gives exactly 2^(2r-2) functionals with all +required evaluations equal to one. When y=Ax, Ta=0 and there are none. + +Every remaining y makes a,Sa,Ta independent. To prove this, y is nonzero, so +a and Sa are independent. Suppose Ta=u Sa+v a for binary scalars u,v. Put +t=u+v. Equation (4) implies + +```text +y=(t I+A)x, (t+v)Ax=t(1+v)x. (5) +``` + +The vectors x and Ax are independent: over F2 dependence would give Ax=0 or +Ax=x, contradicting invertibility of A or I+A. Hence (5) forces t=v and +t(1+v)=0. The only possibilities are t=v=0 and t=v=1. These give the already +excluded values y=Ax and y=(I+A)x. This proves the asserted independence. + +For each of the 2^r-3 remaining y, specifying the three evaluations to be one +leaves exactly 2^(2r-3) functionals. Summing over all N nonzero x gives + +```text +g(r) = N [2*2^(2r-2) + (2^r-3)*2^(2r-3)] + = 2^(2r-3) (2^r-1)(2^r+1), +``` + +which is (2). This step uses the binary scalar possibilities in (5); it is +not a proof over general characteristic-two fields. + +### Complete the header + +Every header gives a split beta(a)=1. Conversely, for such a split the remaining +columns of G are exactly an arbitrary ordered basis of ker beta. Thus the +completion fiber has |GL_(2r-1)(F2)| members, following the split-completion +method of #4735 and the earlier header-count lineage. + +There are `(2^(2r)-1)2^(2r-1)` splits in total. Both literal first pivots are +one precisely when beta(Sa)=beta(Ta)=1. Dividing (2) by that total gives 1/4; +multiplying by the common completion fiber proves (1). + +## Finite corroboration and reproduction + +The standard-library verifier computes observed counts by literal binary +matrix action and vector-functional enumeration. It does not use the proof's +dependent-triple partition for its observed counts. + +- It enumerates all 16 binary 2-by-2 compressions and all 512 binary 3-by-3 + compressions. Exactly 2 and 48 respectively satisfy invertibility of A and + I+A. Every admitted case has respectively 30 and 504 passing splits. +- A separate census fixes S=diag(I_2,0_2) and scans every one of the 65,536 + binary 4-by-4 matrices. It finds 802 idempotents and exactly 12 with + invertible commutator. All 12 have 30 passing splits. This corroborates + partners outside the B=I presentation; it is not an enumeration of every + first S. +- A literal GL4 census scans all 65,536 binary matrices, inverts each + invertible header and conjugates both requests. Exactly 5,040 of the 20,160 + headers pass the first pivots, agreeing with 30*|GL3|=30*168. It also exhibits + a first-passing header with a failed second leading minor, so no full-guard + interpretation is possible. +- Seven controls distinguish the two forbidden scalar compressions, singular + commutators, nonidempotent partners retaining invertible commutator, the + zero-vector denominator, missing completion multiplicity and first/full + guards. All checks use exceptions and remain active under optimization. + +From the repository root: + +```sh +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/generic-idempotent-first-guard +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/generic-idempotent-first-guard --check-source-history +~/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/generic-idempotent-first-guard/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/generic-idempotent-first-guard/verify.py +``` + +Expected markers are `PASS_GENERIC_IDEMPOTENT_FIRST_GUARD`, +`PASS_REGISTERED_RESEARCH_PACKAGE` and `PASS_RESEARCH_COMMIT_BYTES`. +Any CPython 3.12 interpreter may replace the local path. The standalone +verifier reads only its five package files to generate source hashes, writes +no files, imports no predecessor and runs without Git. Its deterministic +stdout receipt binds those five files; no receipt is handwritten or committed. +The registered runner additionally checks historical source metadata. + +Universal claims rest on the written proof. Finite corroboration is not a +formal proof or a complete multiplication theorem. No selected scientific +cold replay, native build, Lean or Docker run is claimed. Physical request +compatibility, header selection/emission, reads, dirty return, stock, +precision and the complete consumer bill remain unknown. + +All executable domains are fixed: raw matrix domains have at most 65,536 +members, vector/functional domains at most 64 members and dimensions at most +six. No recursion, persistent cache, subprocess or network is used. Functions +are under 60 lines. Python allocates during enumeration; these fixed domain +bounds are the managed-runtime deviation from a fixed-allocation discipline. +Warning-strict normal/optimized execution and package validation ran. +No external static analyzer was installed. + +## Sources, scope and credit + +Canonical base is `624de9dc66858af0945e5f8a0942488d62280d43`, priority revision 7. +The selected source-bound orientation passed. Selected conditional kappa remains +60403/20000000. [TASK.json](TASK.json) records the F2 scope and replacement +claim. [SOURCES.json](SOURCES.json) binds historical provenance; there are no +external mathematical inputs or pending-source runtime dependencies. + +- MatShep's #4762, head `3b4e0449262b0b1e07b80e009ef71cc0ca5bf816`, supplies + the complete factor invariant and leaves transition counts open. +- codyw912's #4735, head `4afbea22e79e19d1d65702eb4090d454ee39d967`, supplies + the binary split recurrence, rank-one invariant and block-centralizer method. +- Mihir Srivastava's #4689, head `3a72fbad148294aa9ca7f900a48dbb10e64232be`, + supplies the seven residual states for its specified binary initial profile. +- ssafwann's #4678/#4671 supply the sharp-block header counts and sector + criterion. Nick Petalas's #4597/#4278 and earlier header laws retain the + ordered Schur and completion lineage credit. +- Ryanson Jonathan, lee-phys, Cinna Davis, source527, commdata2338 and Jose + Manuel retain the earlier full-guard, dimension, request and normalizer credit. + +General commutators of idempotents have a substantial prior literature, such +as Drnovsek, Radjavi and Rosenthal's +[2002 characterization](https://doi.org/10.1016/S0024-3795(01)00533-X). +No global novelty for the block normalization is asserted. The family decision +is narrow and stop after this F2 first-pivot count; it authorizes no unpriced +construction expansion. + +## Open next questions + +1. What is the successor-state distribution after an admitted generic binary + first pivot? It would enable an honest second-step count. Start with r=2 + and retain ordered residual types and split multiplicities. The present + result supplies no successor distribution or repeated quarter law. +2. What replaces the count when the binary commutator has a kernel? This + covers many actual scalar-Schur residuals. First separate the generic part + from the singular representation data of #4762. The invertible off-diagonal + reduction here does not classify that remaining data. +3. Can an actual caller use a fully paid cover informed by this count? First + pin its field, allowed headers, selection/emission, reads and dirty-return + costs. A uniform complete-header count supplies none of that physical bill. diff --git a/research/generic-idempotent-first-guard/SOURCES.json b/research/generic-idempotent-first-guard/SOURCES.json new file mode 100644 index 0000000000..6048e3297d --- /dev/null +++ b/research/generic-idempotent-first-guard/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/generic-idempotent-first-guard/TASK.json b/research/generic-idempotent-first-guard/TASK.json new file mode 100644 index 0000000000..fe2d89996e --- /dev/null +++ b/research/generic-idempotent-first-guard/TASK.json @@ -0,0 +1,163 @@ +{ + "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 F2 first-pivot header count for positive-dimensional ordered idempotent pairs with invertible commutator.", + "scope_change_reason": "Answer one transition-count direction left open by MatShep PR4762 and codyw912 PR4735. The resumed task explicitly restricts the earlier predicted scope to F2; this is a written algebraic side proof, not an audit or formalization.", + "bottleneck_link": "Gives an exact admission frequency for one residual-pair stratum. Restricted paid covers and complete physical supplier costs remain unknown.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified F2 quarter law; do not extend it to later guards, other fields or physical construction.", + "outcome": "completed", + "evidence": "README.md proves the dimension-uniform binary law. verify.py checks 2 and 48 admissible compressions, all 65536 raw binary four-by-four partners, all 20160 GL4 headers and seven controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Successor-state distribution after one admitted generic binary pivot", + "why_it_matters": "A first-pivot density cannot be iterated without knowing the residual pair.", + "first_step": "For r=2, retain the ordered residual types and multiplicities of all admitted splits.", + "blocked_by": "This proof supplies no successor-state distribution." + }, + { + "question": "First-pivot count when the binary commutator has a kernel", + "why_it_matters": "Many scalar-Schur residuals lie outside the nonsingular stratum.", + "first_step": "Separate the generic component from the singular factor data of PR4762.", + "blocked_by": "The invertible off-diagonal block reduction does not classify the singular data." + }, + { + "question": "A fully paid cover for one actual caller", + "why_it_matters": "An algebraic uniform-header count does not imply a supplier improvement.", + "first_step": "Pin the field and allowed headers, then price selection, emission, reads and dirty return.", + "blocked_by": "Physical compatibility and the complete consumer bill are unknown." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19132371", + "original_claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19132091", + "correction_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19132156", + "playbook": "Autonomous local run", + "claim_type": "scoped counting proof with finite corroboration", + "overlap": { + "checked_at": "2026-10-22T20:39:11.563450+00:00", + "remote_coverage": { + "open_prs": { + "fetched_at": "2026-10-22T20:38:23.965178+00:00", + "complete_pagination": true, + "records": 340 + }, + "discussions": { + "fetched_at": "2026-10-22T20:39:11.097459+00:00", + "complete_pagination": true, + "records": 3772 + } + }, + "local_coverage": "Sparse helper coverage is incomplete; distinctive git grep queries searched all origin/main research READMEs.", + "main_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "merged_search_terms": [ + "invertible commutator", + "nonsingular commutator", + "first pivot quarter", + "1/4 idempotents" + ], + "required_recent_prs_read": [ + 4801, + 4803, + 4806, + 4807 + ], + "result": "No matching delivered F2 first-pivot quarter law found in the searched coverage. The question-specific helper found only the original claim.", + "limitations": "Arbitrary diffs and unpublished work are not exhaustively searched." + }, + "citations": [ + { + "pr": 4762, + "author": "MatShep", + "head": "3b4e0449262b0b1e07b80e009ef71cc0ca5bf816", + "usage": "Factor invariant and explicit transition-count question; context only." + }, + { + "pr": 4735, + "author": "codyw912", + "head": "4afbea22e79e19d1d65702eb4090d454ee39d967", + "usage": "Split recurrence and completion method; context only." + }, + { + "pr": 4689, + "author": "Mihir Srivastava", + "head": "3a72fbad148294aa9ca7f900a48dbb10e64232be", + "usage": "Earlier residual-state question and finite profile; not replayed." + } + ] +} diff --git a/research/generic-idempotent-first-guard/VERIFY.json b/research/generic-idempotent-first-guard/VERIFY.json new file mode 100644 index 0000000000..1c45a6e57e --- /dev/null +++ b/research/generic-idempotent-first-guard/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "All binary half-size compressions at r=2,3; complete raw four-by-four partner and GL4 header censuses; seven scope/semantic controls; generated five-file source hashes." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "All binary half-size compressions at r=2,3; complete raw four-by-four partner and GL4 header censuses; seven scope/semantic controls; generated five-file source hashes." + } + ] +} diff --git a/research/generic-idempotent-first-guard/verify.py b/research/generic-idempotent-first-guard/verify.py new file mode 100644 index 0000000000..a7f5b4203c --- /dev/null +++ b/research/generic-idempotent-first-guard/verify.py @@ -0,0 +1,203 @@ +#!/usr/bin/env python3 +"""Binary first-pivot quarter law, produced by Nick Petalas. Apache-2.0.""" + +import hashlib +from itertools import product +import json +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def identity(n): + return tuple(1 << i for i in range(n)) + + +def apply(a, x): + return sum(((row & x).bit_count() & 1) << i for i, row in enumerate(a)) + + +def multiply(a, b): + n = len(b) + result = [] + for row in a: + value = 0 + for j in range(n): + if row >> j & 1: + value ^= b[j] + result.append(value) + return tuple(result) + + +def plus(a, b): + return tuple(x ^ y for x, y in zip(a, b, strict=True)) + + +def rank(a): + rows = list(a) + n = len(rows) + lead = 0 + for col in range(n): + pivot = next((i for i in range(lead, n) if rows[i] >> col & 1), None) + if pivot is None: + continue + rows[lead], rows[pivot] = rows[pivot], rows[lead] + for i in range(n): + if i != lead and rows[i] >> col & 1: + rows[i] ^= rows[lead] + lead += 1 + return lead + + +def inverse(a): + n = len(a) + rows = [row | (1 << (n + i)) for i, row in enumerate(a)] + for col in range(n): + pivot = next((i for i in range(col, n) if rows[i] >> col & 1), None) + if pivot is None: + return None + rows[col], rows[pivot] = rows[pivot], rows[col] + for i in range(n): + if i != col and rows[i] >> col & 1: + rows[i] ^= rows[col] + result = tuple(row >> n for row in rows) + require(multiply(result, a) == identity(n), "inverse failed literal multiplication") + return result + + +def matrices(n): + require(1 <= n <= 4, "raw census dimension exceeds four") + yield from product(range(1 << n), repeat=n) + + +def pair(a): + r = len(a) + require(1 <= r <= 3, "half-dimension capacity") + require(all(0 <= row < 1 << r for row in a), "invalid binary row") + complement = plus(identity(r), a) + require(rank(a) == rank(complement) == r, "compression has a forbidden eigenvalue") + c = multiply(a, complement) + s = identity(r) + (0,) * r + t = tuple(a[i] | (1 << (r + i)) for i in range(r)) + t += tuple(c[i] | (complement[i] << r) for i in range(r)) + require(multiply(s, s) == s and multiply(t, t) == t, "nonidempotent construction") + require(rank(plus(multiply(s, t), multiply(t, s))) == 2 * r, "singular commutator") + return s, t + + +def functional_masks(n): + require(1 <= n <= 6, "functional census dimension exceeds six") + return tuple(sum(1 << beta for beta in range(1 << n) + if (beta & a).bit_count() & 1) for a in range(1 << n)) + + +def literal_splits(s, t, masks): + return sum((masks[a] & masks[apply(s, a)] & masks[apply(t, a)]).bit_count() + for a in range(1 << len(s))) + + +def predicted_splits(r): + require(2 <= r <= 3, "finite formula-check capacity") + return (1 << (2 * r - 3)) * ((1 << (2 * r)) - 1) + + +def compression_census(r): + masks = functional_masks(2 * r) + count = 0 + for a in matrices(r): + if rank(a) != r or rank(plus(identity(r), a)) != r: + continue + s, t = pair(a) + actual = literal_splits(s, t, masks) + require(actual == predicted_splits(r), "quarter-law split count failed") + require(4 * actual == ((1 << (2 * r)) - 1) * (1 << (2 * r - 1)), + "quarter-law normalized density failed") + count += 1 + require(count == {2: 2, 3: 48}[r], "compression census incomplete") + return {"r": r, "admissible_compressions": count, "passing_splits_each": predicted_splits(r)} + + +def raw_partner_census(): + s, _ = pair((2, 3)) + masks = functional_masks(4) + idempotents, generic = 0, 0 + for t in matrices(4): + if multiply(t, t) != t: + continue + idempotents += 1 + if rank(plus(multiply(s, t), multiply(t, s))) != 4: + continue + require(literal_splits(s, t, masks) == 30, "raw generic partner count failed") + generic += 1 + require((idempotents, generic) == (802, 12), "raw partner census incomplete") + return {"matrices": 65536, "idempotents": idempotents, + "generic_partners": generic, "passing_splits_each": 30} + + +def complete_header_census(): + s, t = pair((2, 3)) + total, passing = 0, 0 + first_not_full = None + for g in matrices(4): + gi = inverse(g) + if gi is None: + continue + sp = multiply(multiply(gi, s), g) + tp = multiply(multiply(gi, t), g) + total += 1 + if sp[0] & tp[0] & 1: + passing += 1 + leading_s = tuple(row & 3 for row in sp[:2]) + leading_t = tuple(row & 3 for row in tp[:2]) + if first_not_full is None and (rank(leading_s) < 2 or rank(leading_t) < 2): + first_not_full = g + require((total, passing) == (20160, 5040), "literal complete-header census failed") + require(passing == 30 * 168, "GL3 completion multiplier failed") + require(first_not_full is not None, "first/full guard distinction not exhibited") + return {"headers": total, "passing": passing, + "first_passing_full_failing_header": first_not_full} + + +def controls(): + for a in ((0,), (1,)): + try: + pair(a) + except ValueError: + pass + else: + raise ValueError("forbidden scalar compression accepted") + s, t = pair((2, 3)) + require(literal_splits(s, s, functional_masks(4)) == 60, + "singular-commutator contrast failed") + p, swap = (1, 0), (2, 1) + require(multiply(swap, swap) != swap, "nonidempotent control is idempotent") + require(rank(plus(multiply(p, swap), multiply(swap, p))) == 2, + "nonidempotent control must retain invertible commutator") + require(literal_splits(p, swap, functional_masks(2)) == 2, + "nonidempotent control lost its non-quarter density 2/6") + require(4 * 30 != 16 * 8, "zero-vector denominator control failed") + require(30 != 5040, "split/header completion distinction failed") + require(literal_splits(s, t, functional_masks(4)) == 30, "valid control fixture failed") + return ["forbidden_A_zero", "forbidden_A_one", "singular_commutator", + "nonidempotent_with_invertible_commutator", "zero_vector_denominator", + "missing_GL3_completion", "first_guard_is_not_full_guard"] + + +def main(): + result = {"claim_type": "scoped F2 counting proof with finite corroboration", + "compression_censuses": [compression_census(r) for r in (2, 3)], + "raw_partners": raw_partner_census(), + "complete_headers": complete_header_census(), "controls": controls()} + package = Path(__file__).resolve().parent + names = ("README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") + result["source_sha256"] = {name: hashlib.sha256((package / name).read_bytes()).hexdigest() + for name in names} + print(json.dumps(result, sort_keys=True, separators=(",", ":"))) + print("PASS_GENERIC_IDEMPOTENT_FIRST_GUARD") + + +if __name__ == "__main__": + main()