From f2ebfc32f2f3ad644a7e380827fcd90f798ae7b8 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Mon, 2 Nov 2026 21:23:50 +0000 Subject: [PATCH] docs(research): prove vector-cocycle paid-call floors --- research/vector-cocycle-rank-floor/PROOF.md | 183 ++++++++++ research/vector-cocycle-rank-floor/README.md | 142 ++++++++ .../vector-cocycle-rank-floor/SOURCES.json | 36 ++ research/vector-cocycle-rank-floor/TASK.json | 113 +++++++ .../vector-cocycle-rank-floor/VERIFY.json | 34 ++ research/vector-cocycle-rank-floor/verify.py | 314 ++++++++++++++++++ 6 files changed, 822 insertions(+) create mode 100644 research/vector-cocycle-rank-floor/PROOF.md create mode 100644 research/vector-cocycle-rank-floor/README.md create mode 100644 research/vector-cocycle-rank-floor/SOURCES.json create mode 100644 research/vector-cocycle-rank-floor/TASK.json create mode 100644 research/vector-cocycle-rank-floor/VERIFY.json create mode 100644 research/vector-cocycle-rank-floor/verify.py diff --git a/research/vector-cocycle-rank-floor/PROOF.md b/research/vector-cocycle-rank-floor/PROOF.md new file mode 100644 index 0000000000..cf9e6f7b99 --- /dev/null +++ b/research/vector-cocycle-rank-floor/PROOF.md @@ -0,0 +1,183 @@ +# A rectangular cocycle rank floor + +## Formal boundary + +Let F be a field, G a group, V an F-vector space of finite positive +dimension d, and R:G -> GL(V) a representation. Suppose c:G -> V is a +crossed homomorphism, with convention + +```text +c(gh) = c(g) + R(g)c(h). +``` + +Use the full formal group algebra F[G]. A register word has r finite +scalar roles. Its paid factors are + +```text +D_N(g) = I_r + ([g]-[1])N, +N = xy^T in M_r(F), y^T x = 1. +``` + +Every input is arbitrary. Any declared dirty role must have its required +full formal identity output, including all off-diagonal coefficients. +Constant GL_r(F) matrices may be interspersed at no formal paid-call cost. +No physical realization or price for those free matrices is asserted. + +This is the rank-one idempotent register convention of Cinna Davis's +PR2116/2047/2248/2085 and Sagar Thakrar's PR4032. The new lemma uses a +vector-valued affine representation in place of a scalar twisted functional. +Nick Petalas's PR4898 supplies an earlier specific first-order instance; +neither that instance nor the predecessor results are replayed here. +Nick Petalas's PR6008 supplies the general full-operator representation +rank cut. The charge here uses a common rectangular block, whose per-call +rank is one even when the full operator defect has rank greater than one. +This is a changed invariant, rather than substitution of another group +into that full-operator cut. + +## Theorem + +For T in M_r(F[G]), define the rectangular matrix Delta_c(T) in +M_(rd,r)(F) by replacing entry `sum_g a_ij,g [g]` with the d-by-1 column +`sum_g a_ij,g c(g)`. If a register word equals T, then + +```text +rank_F Delta_c(T) <= number of its paid calls with c(g) != 0. +``` + +The same statement holds with a call of projector rank k charged k units +when c(g) is nonzero. In the rank-one alphabet, for a full diagonal target +`diag([t_1],...,[t_w],1,...,1)`, the number of calls outside ker(c) is at +least `#{i : c(t_i) != 0}`. The bound is independent of the number of +restored dirty roles. + +### Proof + +The cocycle identity makes + +```text +rho(g) = [ R(g) c(g) ] + [ 0 1 ] +``` + +a group representation, so it extends linearly to an algebra map on +F[G]. Apply it entrywise and reorder the coordinates by putting all V +coordinates first and all final scalar coordinates last. The resulting +algebra map has the form + +```text +rho_r(T) = [ A(T) Delta_c(T) ] + [ 0 eps(T) ], +``` + +where eps is entrywise augmentation. Therefore + +```text +Delta_c(UW) = A(U) Delta_c(W) + Delta_c(U) eps(W). +rank Delta_c(UW) <= rank Delta_c(U) + rank Delta_c(W). +``` + +This uses only the rank inequalities for a sum and a product. In +particular no simultaneous diagonalization or scalar character is needed. + +The cocycle identity at the identity gives c(1)=0. For a paid factor, + +```text +Delta_c(D_N(g)) = N tensor c(g). +``` + +Its rank is one if c(g) is nonzero and zero otherwise. For the stated +higher-rank variant it is rank(N) if c(g) is nonzero. The factor is legal +and invertible since its inverse is D_N(g^-1), using N^2=N. Its upper +block is `(I-N) tensor I_d + N tensor R(g)` and its lower block is I_r. + +A constant scalar matrix S has blocks S tensor I_d and S, with zero +rectangular block. It contributes no rank charge. Iterating the product +inequality proves the assertion even with interspersed free scalar mixing. + +For the diagonal target, column i of Delta is c(t_i) supported in its own +V block. Distinct nonzero columns are independent because those blocks +are disjoint. Identity spectator outputs give zero columns and rows. +This proves the diagonal statement for every finite r. QED. + +The bound is necessary, not sufficient. A nonidentity element in ker(c) +can have a nonidentity rho image with zero rectangular block. The full +formal endpoint, rather than this representation alone, remains the +correct acceptance condition for a construction. + +## Normal p-subgroup extension + +Let P be a finite p-group, H any group acting on P, and G=P semidirect H. +Let Phi(P)=P^p[P,P] be the Frattini subgroup. Then V=P/Phi(P) is a finite +Fp-vector space. H acts linearly on V because Phi(P) is characteristic. +For the unique expression g=ph, set + +```text +R(ph) = action of h on V, +c(ph) = image of p in V. +``` + +Indeed `(ph)(qk) = p(hqh^-1)hk`, and taking the Frattini quotient gives +the crossed homomorphism identity. The theorem applies over Fp, or after +extending scalars to any field of characteristic p. Consequently every +diagonal target label with nonzero Frattini component forces one call +whose normal component also survives that quotient. + +There is no hypothesis on the order or commutativity of H, and no +one-dimensional equivariant functional on V is required. This answers +the existence of a vector-valued rank floor in PR4032's Open next +question 2. It does not assert that every particular scalar-character +floor, equality classification or shortest-word theorem extends. Elements +of Phi(P), including central defects killed by that quotient, are not +detected. For a nonsplit extension an appropriate cocycle would need to +be supplied separately. + +## A sharp family invisible to abelianization + +Let p be any prime, d>=2, V=Fp^d and +`G = V semidirect SL_d(Fp)`, with the natural action. Write its elements +as (v,h), so multiplication is `(v,h)(w,k)=(v+hw,hk)`. The cocycle is +c(v,h)=v and the representation is R(v,h)=h. + +Give every nonidentity group label unit paid-call price in the formal +rank-one alphabet. For any nonzero vectors v_1,...,v_w and every finite +r>=w, the full endpoint + +```text +diag([(v_1,I)],...,[(v_w,I)],1,...,1) +``` + +has exact minimum w paid calls. The theorem gives the lower bound w, +including arbitrary restored dirty workspace and free scalar mixing. +The w coordinate projectors give the upper bound, with the exact full +formal endpoint and no cross-role entries. + +Nevertheless every homomorphism from G to an abelian group kills all +translations. To prove this, for i!=j use h=I+E_ij in SL_d(Fp) and the +translation by e_j. With `[a,b]=aba^-1b^-1`, their commutator is the +translation by `(h-I)e_j=e_i`. All translations are products of these +basis translations. Thus V is contained in [G,G], and every abelian +quotient sends the whole target to identity. In particular ordinary +one-dimensional group characters cannot supply this nonzero target +defect. This statement does not exclude other representation-theoretic +lower bounds. + +The finite example uses p=3,d=2. Its complement is nonabelian and has +order 24, divisible by 3. Thus the example actually exercises the +removed complement-order restriction. The written proof establishes the +family; finite checks are corroboration on this single group only. + +Affine representations of cocycles, Frattini quotients, elementary +commutators and rank subadditivity are classical. No literature-wide +priority is claimed. The contribution here is their rectangular-block +register-word application and the stated scope extension of the +predecessor first-order method. + +## Obligations outside this proof + +These are formal algebraic call counts. Native address operators, scalar +basis conversion, permitted sources, ownership and erasure, chronology, +restoration costs, hosting, precision/tape, compiler closure, recursive +funding and the outer multiplication theorem are not provided. The +selected result and its five framework assumptions are unchanged. The +written proof has no claimed formal proof-kernel or independent human +acceptance. diff --git a/research/vector-cocycle-rank-floor/README.md b/research/vector-cocycle-rank-floor/README.md new file mode 100644 index 0000000000..ac7855b8c0 --- /dev/null +++ b/research/vector-cocycle-rank-floor/README.md @@ -0,0 +1,142 @@ +# Vector-valued cocycle floors for formal register words + +For any finite-dimensional representation R of a group G over a field F +and crossed homomorphism `c(gh)=c(g)+R(g)c(h)`, every formal rank-one +register word realizing T obeys + +```text +number of calls with c(g)!=0 >= rank_F Delta_c(T). +``` + +Delta replaces each formal group-algebra entry with its c-weighted vector +column. A diagonal target forces one such call for every nonzero target +column, even with arbitrary finite restored dirty workspace and free +constant scalar mixing. [PROOF.md](PROOF.md) proves the statement and its +extension to every split normal p-subgroup via its Frattini quotient. +The complement can be nonabelian and have order divisible by p. + +The new step is the rectangular block of the affine cocycle representation. +It removes the need for a scalar twisted functional in Sagar Thakrar's +[PR4032](https://github.com/CrocSwap/integer-mult-bounds/pull/4032), Open next +question 2. The existing A4 and SL2(F3) results are cited and credited; +their checkers and searches are not run. This is a scoped algebraic proof +with finite exact corroboration, with no new kappa or selected-frontier change. + +For `G=Fp^d semidirect SL_d(Fp)`, d>=2, w nonzero translation targets have +exact formal paid-call minimum w at every finite dirty-workspace size. +Every abelian quotient kills all those translations, so ordinary group +abelianization sees no target defect. The general proof uses elementary +transvection commutators. The finite example is F3^2 semidirect SL2(F3), +whose complement is nonabelian and has order divisible by the characteristic. + +## Reproduce + +From the repository root, use CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/vector-cocycle-rank-floor/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/vector-cocycle-rank-floor/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/vector-cocycle-rank-floor +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/vector-cocycle-rank-floor --check-source-history +``` + +Any installed CPython 3.12 may replace the interpreter path. The expected +markers are `PASS_VECTOR_COCYCLE_RANK_FLOOR` and +`PASS_REGISTERED_RESEARCH_PACKAGE`. The standalone check needs neither Git +nor a network. Its stdout receipt is generated from exact computations and +SHA256 hashes of all six package files. `--emit /absolute/new/file.json` +writes that receipt with exclusive creation and refuses an existing path. +No generated output is required or retained in this package. + +The verifier enumerates the finite group's affine/cocycle identities, every +rank-one idempotent on one through three F3 roles and every group label. +It compares formal group-algebra products with their affine images for a +declared deterministic sample of words with interspersed invertible scalar +mixing on two through five roles. It +checks all nonzero translation-target lists of length at most three with +two restored dirty roles, using exact full formal endpoints. Two explicit +commutators establish the finite translation basis. Semantic controls cover +the ignored module action, invalid nilpotent and rank-two projectors, +zero-cocycle replacement, reversed order, an omitted target, and the +nonidentity kernel. This is not an exhaustive word census or a formal +proof of the quantified theorem. + +Both local modes pass 46,656 group pairs, 28,080 call images, 252 prefixes +of 72 sampled words, and 584 sharp full formal target lists. The projector +counts on one, two and three roles are 1, 12 and 117. Thirty-five sampled +words have strict slack in the rank inequality; no characterization of all +strict cases is claimed. Each direct command takes about 2.4 seconds +locally, comfortably below its registered two-minute limit. + +## Scope and credit + +Canonical scientific base is `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, +priority revision 8, selected PR6030. The selected binding control passed. +The task is a declared change from the formal-interface card to a written +formal-model lemma. It is a side result for the portfolio of changed +interfaces, without a claim to discharge a selected framework assumption. + +[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19360783). +Entry overlap checks included live open PRs, this account's recent PRs, +recent handoff comments, active Discussions, local reservations, main-tree +README searches and merged searches for radical rank, cocycles, Frattini +quotients and nonabelian complements. The cached helper reported complete +main-note inventory and remote pagination, with its own freshness times. +Arbitrary diffs, unpublished work and historical text outside those searches +remain outside coverage; this is not a literature novelty certificate. + +Credit Sagar Thakrar / thakrarsagar PR4032 for the twisted radical-rank +method and its normal-subgroup extension question; Cinna Davis +PR2116/2047/2248/2085 for the formal register and first-order lineage; +Nick Petalas PR4898 for the earlier SL2(F3) instance; and their retained +register-model predecessors. [SOURCES.json](SOURCES.json) pins predecessor +texts as provenance, with no executable import or scientific replay of them. +Affine cocycle representations, Frattini quotients and matrix-rank +subadditivity are classical. No literature-wide priority is claimed. + +Nick Petalas's PR6008 supplies the earlier full-operator representation +rank cut. This result extracts a common rectangular block, giving a +one-unit charge even when a full paid operator defect has larger rank. +Its main result is the general block invariant, rather than a counterpart +obtained by changing a group or target in the full-operator cut. + +This contribution was produced by Nick Petalas. Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. + +The gate is necessary rather than sufficient. It can miss nonidentity +elements in ker(c), including Frattini defects in the normal-subgroup +specialization. A nonsplit extension needs its own cocycle. Native maps, +scalar conversions, source access, ownership/erasure, physical restoration, +hosting, precision/tape, compiler closure and the complete signed supplier +and outer bills remain unproved here. No heavy native, Lean, Docker or +selected scientific cold replay is part of this claim. + +## Open next questions + +- Can several cocycle blocks give a strictly stronger joint weighted-call + bound for one supplied alphabet and full endpoint? This could rule out + words that pass each bound separately. First derive the linear call-count + constraints for one explicit alphabet and give a feasible dual witness. + Native prices and a promising physical endpoint are missing. +- Can a second-order representation detect a specified Frattini defect + that this gate kills, without losing the one-call charge? This could + separate central targets hidden from all first-order quotients. First + state an exact block-product law and its per-call rank change. A + suitable second-order invariant, rather than a larger census, is missing. + +## Implementation bounds + +The finite verifier uses fixed F3 arithmetic, group order 216, at most +seven roles, matrix dimension at most 21, words of length at most six, +and bounded Cartesian products. It has no recursion, dynamic code +generation, subprocesses or third-party imports. Functions are below +60 physical lines. Checks use explicit exceptions in normal and optimized +execution. Two exception-control callbacks have fixed visible targets. + +Power-of-Ten deviation, rule 3: CPython allocates integers, tuples and +dictionaries during this one-shot computation. Fixed finite domains bound +live memory; no caller-supplied size or unbounded search is accepted. A +fixed-buffer implementation would be needed for literal allocation-free +operation. Warning-strict normal and optimized commands are the available +diagnostics; no proof-assistant or independent scientific acceptance is +claimed by their success. diff --git a/research/vector-cocycle-rank-floor/SOURCES.json b/research/vector-cocycle-rank-floor/SOURCES.json new file mode 100644 index 0000000000..1341b1e38f --- /dev/null +++ b/research/vector-cocycle-rank-floor/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/a4-seven-call-radical-rank/README.md", + "usage": "provenance", + "git_blob": "ab5ea83019119dcada4b654b137d418503014cf5", + "sha256": "26c9a90b1e73ce90b6711417db3f023e79192acdde8b94f1e7cfa0a93fafd42b" + }, + { + "path": "research/sl2f3-all-dirty-minimum/README.md", + "usage": "provenance", + "git_blob": "b2b04a5a21e2a5f24f8641181f280b4982457b5d", + "sha256": "cf5ccd8c8b1aaa0f3b40e6a05558cfc568b23fb7f0239168c99cebcf8bebc98b" + }, + { + "path": "research/prime-exponent-rank-cut/README.md", + "usage": "provenance", + "git_blob": "a23cf9be5d5ec8b258156b7925a9349fe6bef8b3", + "sha256": "4e1936de8546a3ac91f58cb5176f11a2b35d7a1093814794b35622bd97347db7" + } + ] +} diff --git a/research/vector-cocycle-rank-floor/TASK.json b/research/vector-cocycle-rank-floor/TASK.json new file mode 100644 index 0000000000..16e00775ef --- /dev/null +++ b/research/vector-cocycle-rank-floor/TASK.json @@ -0,0 +1,113 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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_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": "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": "A vector-valued cocycle rectangular-rank floor for all finite register widths, its split normal-p-subgroup extension, and a sharp translation family invisible to abelianization.", + "scope_change_reason": "PR4032 Open next question 2 supplies an explicitly open formal-model extension. This is a self-contained written algebraic proof with finite corroboration, not a proof-assistant binding or predecessor audit.", + "bottleneck_link": "Side result for changed recursive interfaces: rejects formal rank-one call savings under an explicit alphabet before native/physical expansion. It does not alter the current signed supplier bill or discharge a selected assumption.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved scoped extension and finite exact corroboration; do not enlarge the word search or optimize a physical construction.", + "outcome": "completed", + "evidence": "PROOF.md and the source-bound stdout receipt from verify.py; finite corroboration is separate from the all-size written argument.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can several cocycles force a strictly stronger joint weighted-call floor on one explicit alphabet and endpoint?", + "why_it_matters": "Individual floors can leave incompatible call-count budgets undetected.", + "first_step": "Derive a finite family of linear constraints on label counts and give a feasible dual witness for one supplied full endpoint.", + "blocked_by": "A concrete alphabet with native prices and a promising physical target." + }, + { + "question": "Can a second-order representation detect one Frattini defect while retaining a useful per-call charge?", + "why_it_matters": "The first-order cocycle annihilates these defects.", + "first_step": "Specify an exact second-order block-product law and bound its rank change under one legal call.", + "blocked_by": "A second-order invariant with a justified charge." + } + ], + "question_source": { + "pr": 4032, + "author": "thakrarsagar", + "question": "Open next question 2, normal-subgroup extension of the radical-rank bound" + }, + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19360783", + "upstream_refresh": { + "commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "checked_at": "2026-11-02T21:22:36.726680+00:00", + "priority_revision": 8, + "selected_pr": 6030 + } +} diff --git a/research/vector-cocycle-rank-floor/VERIFY.json b/research/vector-cocycle-rank-floor/VERIFY.json new file mode 100644 index 0000000000..b4473446e0 --- /dev/null +++ b/research/vector-cocycle-rank-floor/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": "Exact affine/cocycle law, all finite call defects and inverses, formal/affine word comparison, sharp full endpoints and semantic controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Repeat the same checks with Python assertions disabled." + } + ] +} diff --git a/research/vector-cocycle-rank-floor/verify.py b/research/vector-cocycle-rank-floor/verify.py new file mode 100644 index 0000000000..4b0001f4c3 --- /dev/null +++ b/research/vector-cocycle-rank-floor/verify.py @@ -0,0 +1,314 @@ +"""Exact finite corroboration of the vector-cocycle register-word theorem.""" + +import argparse +import hashlib +import itertools +import json +from pathlib import Path + + +P = 3 +D = 2 +IDENTITY = ((1, 0), (0, 1)) +ZERO = (0, 0) + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def eye(n): + require(1 <= n <= 21, "matrix capacity") + return tuple(tuple(int(i == j) for j in range(n)) for i in range(n)) + + +def multiply(a, b): + require(1 <= len(a) <= 21 and len(a[0]) == len(b), "product shape") + require(1 <= len(b[0]) <= 21, "product capacity") + return tuple(tuple(sum(x * y for x, y in zip(row, col)) % P + for col in zip(*b)) for row in a) + + +def rank(a): + require(1 <= len(a) <= 21 and 1 <= len(a[0]) <= 21, "rank capacity") + rows = [list(row) for row in a] + pivot = 0 + for col in range(len(rows[0])): + chosen = next((i for i in range(pivot, len(rows)) if rows[i][col]), None) + if chosen is None: + continue + rows[pivot], rows[chosen] = rows[chosen], rows[pivot] + scale = pow(rows[pivot][col], -1, P) + rows[pivot] = [(scale * x) % P for x in rows[pivot]] + for i in range(pivot + 1, len(rows)): + scale = rows[i][col] + rows[i] = [(x - scale * y) % P + for x, y in zip(rows[i], rows[pivot])] + pivot += 1 + if pivot == len(rows): + break + return pivot + + +def action(h, v): + return tuple(sum(h[i][j] * v[j] for j in range(D)) % P for i in range(D)) + + +def group_product(g, k): + v, h = g + w, j = k + hw = action(h, w) + return tuple((v[i] + hw[i]) % P for i in range(D)), multiply(h, j) + + +def group_inverse(g): + v, h = g + a, b = h[0] + c, d = h[1] + inverse = ((d % P, -b % P), (-c % P, a % P)) + hv = action(inverse, v) + return tuple(-x % P for x in hv), inverse + + +def affine(g): + v, h = g + return tuple(tuple(h[i][j] for j in range(D)) + (v[i],) + for i in range(D)) + ((0, 0, 1),) + + +def groups(): + matrices = [] + for a, b, c, d in itertools.product(range(P), repeat=4): + if (a * d - b * c) % P == 1: + matrices.append(((a, b), (c, d))) + vectors = tuple(itertools.product(range(P), repeat=D)) + return tuple((v, h) for v in vectors for h in matrices) + + +def projectors(r): + require(1 <= r <= 3, "projector enumeration capacity") + vectors = tuple(itertools.product(range(P), repeat=r)) + output = set() + for x in vectors: + for y in vectors: + if sum(a * b for a, b in zip(x, y)) % P == 1: + output.add(tuple(tuple(a * b % P for b in y) for a in x)) + return tuple(sorted(output)) + + +def call_matrix(n, g): + r = len(n) + require(1 <= r <= 7, "call role capacity") + require(multiply(n, n) == n and rank(n) == 1, "not a rank-one idempotent") + rho = affine(g) + size = r * (D + 1) + return tuple(tuple((int(i == j) + n[i // 3][j // 3] + * (rho[i % 3][j % 3] - int(i % 3 == j % 3))) % P + for j in range(size)) for i in range(size)) + + +def defect(a, r): + require(len(a) == 3 * r, "defect shape") + return tuple(tuple(a[3 * i + k][3 * j + 2] for j in range(r)) + for i in range(r) for k in range(D)) + + +def group_checks(group): + cases = 0 + elements = set(group) + for g in group: + require(group_product(g, group_inverse(g)) == (ZERO, IDENTITY), "inverse") + for k in group: + result = group_product(g, k) + require(result in elements, "group closure") + require(affine(result) == multiply(affine(g), affine(k)), "affine law") + v, h = g + w, _ = k + expected = tuple((v[i] + action(h, w)[i]) % P for i in range(D)) + require(result[0] == expected, "crossed homomorphism") + cases += 1 + return cases + + +def call_checks(group): + counts = [] + cases = 0 + for r in range(1, 4): + alphabet = projectors(r) + counts.append(len(alphabet)) + for n in alphabet: + for g in group: + matrix = call_matrix(n, g) + require(rank(defect(matrix, r)) == int(g[0] != ZERO), "call rank") + inverse = call_matrix(n, group_inverse(g)) + require(multiply(matrix, inverse) == eye(3 * r), "call inverse") + cases += 1 + return counts, cases + + +def formal_identity(r): + return {(i, i, (ZERO, IDENTITY)): 1 for i in range(r)} + + +def formal_right_call(word, n, g): + r = len(n) + require(len(word) <= 7 * 7 * 216, "formal support capacity") + result = dict(word) + for (i, j, label), value in word.items(): + for k in range(r): + for term, sign in ((group_product(label, g), 1), (label, -1)): + key = i, k, term + result[key] = (result.get(key, 0) + sign * value * n[j][k]) % P + return {key: value for key, value in result.items() if value} + + +def formal_image(word, r): + matrix = [[0] * (3 * r) for _ in range(3 * r)] + for (i, j, g), value in word.items(): + rho = affine(g) + for u in range(3): + for v in range(3): + matrix[3 * i + u][3 * j + v] += value * rho[u][v] + return tuple(tuple(x % P for x in row) for row in matrix) + + +def scalar_matrix(s): + r = len(s) + return tuple(tuple(s[i // 3][j // 3] * int(i % 3 == j % 3) + for j in range(3 * r)) for i in range(3 * r)) + + +def formal_right_scalar(word, s): + result = {} + for (i, j, label), value in word.items(): + for k in range(len(s)): + key = i, k, label + result[key] = (result.get(key, 0) + value * s[j][k]) % P + return {key: value for key, value in result.items() if value} + + +def word_checks(group): + cases = 0 + words = 0 + strict_cases = 0 + for r in range(2, 6): + for trial in range(18): + image = eye(3 * r) + word = formal_identity(r) + charged = 0 + for step in range(1 + trial % 6): + x = tuple(int(i == (step + trial) % r) for i in range(r)) + y = tuple((1 if x[i] else (trial + i + step) % P) for i in range(r)) + n = tuple(tuple(a * b % P for b in y) for a in x) + g = group[(31 * trial + 17 * step + 7 * r) % len(group)] + word = formal_right_call(word, n, g) + image = multiply(image, call_matrix(n, g)) + charged += int(g[0] != ZERO) + s = tuple(tuple((int(i == j) + int(i == step % r and + j == (step + 1) % r)) % P + for j in range(r)) for i in range(r)) + word = formal_right_scalar(word, s) + image = multiply(image, scalar_matrix(s)) + require(formal_image(word, r) == image, "formal/image mismatch") + require(rank(defect(image, r)) <= charged, "word rank bound") + cases += 1 + s = tuple(tuple((int(i == j) + int(i == 0 and j == 1)) % P + for j in range(r)) for i in range(r)) + mixed = multiply(multiply(scalar_matrix(s), image), scalar_matrix(s)) + observed = rank(defect(mixed, r)) + require(observed == rank(defect(image, r)), "scalar mixing rank") + strict_cases += int(observed < charged) + words += 1 + return cases, strict_cases, words + + +def sharp_checks(): + vectors = tuple(v for v in itertools.product(range(P), repeat=D) if v != ZERO) + cases = 0 + for w in range(1, 4): + r = w + 2 + for targets in itertools.product(vectors, repeat=w): + word = formal_identity(r) + expected = {(i, i, (targets[i] if i < w else ZERO, IDENTITY)): 1 + for i in range(r)} + for i, v in enumerate(targets): + n = tuple(tuple(int(j == i and k == i) for k in range(r)) + for j in range(r)) + word = formal_right_call(word, n, (v, IDENTITY)) + require(word == expected, "sharp full formal endpoint") + require(rank(defect(formal_image(word, r), r)) == w, "sharp rank") + cases += 1 + return cases + + +def expect_rejection(callback, message): + try: + callback() + except ValueError: + return + raise ValueError(message) + + +def controls(): + e = (ZERO, IDENTITY) + translation = ((0, 1), IDENTITY) + shear = (ZERO, ((1, 1), (0, 1))) + require(group_product(shear, translation)[0] != (0, 1), "wrong-action control") + other_shear = (ZERO, ((1, 0), (1, 1))) + require(group_product(shear, other_shear) != group_product(other_shear, shear), + "complement must be nonabelian") + commutators = [] + for i in range(2): + h = ((1, 1), (0, 1)) if i == 0 else ((1, 0), (1, 1)) + v = (0, 1) if i == 0 else (1, 0) + a, b = (ZERO, h), (v, IDENTITY) + c = group_product(group_product(group_product(a, b), group_inverse(a)), + group_inverse(b)) + require(c == (tuple(int(i == j) for j in range(2)), IDENTITY), "commutator") + commutators.append(c[0]) + expect_rejection(lambda: call_matrix(((0, 1), (0, 0)), e), "nilpotent accepted") + expect_rejection(lambda: call_matrix(((1, 0), (0, 1)), e), "rank-two accepted") + invisible = call_matrix(((1,),), shear) + require(rank(defect(invisible, 1)) == 0 and invisible != eye(3), "kernel control") + nonzero = call_matrix(((1,),), translation) + require(rank(defect(nonzero, 1)) == 1, "zero-cocycle mutation") + require(affine(group_product(shear, translation)) != + multiply(affine(translation), affine(shear)), "order mutation") + word = formal_right_call(formal_identity(2), ((1, 0), (0, 0)), translation) + require(word != formal_identity(2), "omitted target accepted") + return {"commutator_basis": commutators, "semantic_controls": 7} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", type=Path, help="write a fresh source-bound receipt") + args = parser.parse_args() + group = groups() + require(len(group) == 216 and len(set(group)) == 216, "group enumeration") + pair_count = group_checks(group) + counts, call_count = call_checks(group) + prefixes, strict, words = word_checks(group) + sharp = sharp_checks() + control_report = controls() + package = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + hashes = {name: hashlib.sha256((package / name).read_bytes()).hexdigest() + for name in names} + report = {"status": "PASS_VECTOR_COCYCLE_RANK_FLOOR", "field": P, + "module_dimension": D, "group_order": len(group), + "complement_order": len({h for _, h in group}), + "group_pairs": pair_count, "projectors_by_roles": counts, + "calls": call_count, "sampled_word_prefixes": prefixes, + "sampled_words": words, "strict_word_examples": strict, + "sharp_formal_targets": sharp, "controls": control_report, + "source_sha256": hashes} + rendered = json.dumps(report, indent=2, sort_keys=True) + "\n" + if args.emit is not None: + with args.emit.open("x") as stream: + stream.write(rendered) + print(rendered, end="") + + +if __name__ == "__main__": + main()