diff --git a/research/heisenberg-vector-central-tariff/PROOF.md b/research/heisenberg-vector-central-tariff/PROOF.md new file mode 100644 index 0000000000..7ac44b5804 --- /dev/null +++ b/research/heisenberg-vector-central-tariff/PROOF.md @@ -0,0 +1,146 @@ +# Exact central-target tariff with vector labels + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Model and statement + +All vectors and matrices in this note are binary. For positive integers m,n, +let H(m,n) consist of triples (u,v,Z) in F2^m × F2^n × M_(m,n)(F2), with + + (u,v,Z)(p,q,W) = (u+p,v+q,Z+W+u q^T). + +Write x(u)=(u,0,0), y(v)=(0,v,0), and z(Z)=(0,0,Z). A paid call is + + D_N(g) = I_r + ([g]+[1])N, + +in M_r(F2[H(m,n)]), where N is any nonzero rank-one binary r×r matrix and +g is any x(u) with u≠0 or any y(v) with v≠0. Every such vector label costs +one paid call. In particular, its coordinate decomposition is not separately +charged. Arbitrary invertible binary scalar mixing is free. All r input +roles may be dirty and no clean initialization, erasure or free address map +is available. Equality means equality in the full formal group algebra. + +Choose nonzero matrices Z_1,...,Z_P and r≥P. The target has [z(Z_t)] on +role t for 1≤t≤P and [1] on every other diagonal entry; off-diagonal entries +are zero. Put K=Σ_t rank(Z_t). + +**Theorem.** The exact minimum number of paid calls is 2(K+P), for every +finite r≥P. Zero target matrices may be omitted. The identity target costs +zero. Arbitrary restored dirty spectator roles do not lower this minimum. + +The changed alphabet is essential. Cinna Davis's PR2258 proves a coordinate +edge tariff in this same group family. Its calls only allow x(e_i),y(e_j), +and its outputs are distinct edge coordinates. Here both the allowed labels +and the central targets change: an entire arbitrary vector is one label, +and a target may have any matrix rank. The new result is the matching +tariff for that explicitly enlarged alphabet. It does not contradict the +coordinate-edge theorem or price vector-label production in a bit supplier. + +## Upper bound by a closed vector walk + +For nonzero Z of rank k, take a rank factorization + + Z = Σ_(i=1)^k u_i v_i^T, + +where both lists are linearly independent. Let u_0=0 and V=Σ_i v_i. Use + + x(u_1)y(v_1)x(u_1+u_2)y(v_2)...x(u_(k-1)+u_k)y(v_k)x(u_k)y(V). + +There are k+1 x-labels and k+1 y-labels. Every label is nonzero by +independence, including V. Immediately before the i-th y(v_i), the running +u coordinate is u_i; after the last x(u_k), it is zero. The group law +therefore gives final coordinates u=v=0 and central coordinate +Σ_i u_i v_i^T=Z. This proves the full group identity, not just an identity +in a representation. + +Apply this word to coordinate projector E_tt for each target t. The product +acts by [z(Z_t)] on that role and identically on every other role. All calls +are counted and every dirty spectator is restored. Total length is 2(K+P). +For Z=I_2, the word is x(e_1)y(e_1)x(e_1+e_2)y(e_2)x(e_2)y(e_1+e_2), +of length six, versus eight for two separate rank-one commutators. + +## Lower bound + +First normalize free scalar maps by pushing them through the paid calls. +Conjugation preserves rank one. Augmentation sends every paid call and +the target to I_r, so the final scalar map is I_r. It suffices to bound a +pure paid word. Each factor is invertible, even for nilpotent N: g is an +involution, so ([g]+[1])²=0 and D_N(g)²=I_r. + +Use the natural representation and its contragredient: + + rho(u,v,Z) = [ I_m u Z ] rho_dual(g) = rho(g)^(-T). + [ 0 1 v^T] + [ 0 0 I_n] + +These are group homomorphisms. In rho, x(u) has only the off-diagonal block +u at position (1,2), and y(v) only v^T at (2,3). The central target is Z +at (1,3). In rho_dual, x(u) has only u^T at (2,1), y(v) only v at (3,2), +and z(Z) only Z^T at (3,1). Signs disappear in characteristic two. +Apply each representation entrywise to the full register matrix. + +For each x-labelled occurrence s, write N_s=a_s b_s^T and let u_s be its +label vector. Define + + A = [u_s ⊗ a_s]_s, B = [b_s^T]_s. + +The target has zero (1,2) block. In the natural representation this block +is exactly Σ_s u_s⊗N_s=AB. No product of two strictly upper blocks can +contribute to (1,2). Thus AB=0 and + + rank(A)+rank(B) ≤ n_x, + +where n_x is the number of x-labelled calls. Its central block C is the +ordered sum of x-then-y products. Consequently im(C)⊆im(A). After a +permutation of tensor coordinates, the target C is the block diagonal +matrix with blocks Z_t and zero spectator blocks. Hence rank(C)=K and +rank(A)≥K. + +In the dual representation, the central block C_dual is a sum of y-then-x +products. Its row space is contained in the span of all rows +u_s^T⊗b_s^T. For each nonzero target Z_t, the row space of C_dual contains +a nonzero row q^T⊗e_t^T. Choose a nonzero coordinate of q and contract the +address tensor coordinate there. This yields e_t^T. Applying the same +contraction to any u_s^T⊗b_s^T yields either zero or b_s^T. Thus every +active e_t^T belongs to row(B). The P active coordinate vectors are +independent, so rank(B)≥P. Therefore n_x≥K+P. + +For completeness, the y-labelled argument uses + + A_y=[a_s]_s, B_y=[v_s^T⊗b_s^T]_s. + +The natural (2,3) block gives A_y B_y=0. Its central block has row space +inside row(B_y), giving rank(B_y)≥K. The dual central block has column +space inside the span of v_s⊗a_s. Contracting a nonzero address coordinate +in each active target column gives e_t in im(A_y), so rank(A_y)≥P. It +follows that n_y≥K+P. Every paid call is of exactly one label type, whence + + length = n_x+n_y ≥ 2(K+P). + +Together with the explicit full-formal word, this proves the theorem for +all finite dimensions and every finite number of dirty spectators. No +finite search supplies this universal quantifier. + +## Evidence and scope + +The standalone verifier enumerates bounded central matrices, independently +computes their ranks by minors, constructs full group endpoints, and obtains +their exact one-role word distances by complete Cayley BFS. It also excludes +every normalized word of length at most five for the new rank-two target +with a restored second dirty role, using exact full-formal balls of radii +three and two. Arbitrary rank-one binary couplings, including nilpotents, +are present in that finite exclusion. Literal four-role formal matrices +check heterogeneous targets and dirty spectator restoration. + +The theorem counts only this abstract alphabet. Producing arbitrary vector +labels, native implementations, scalar mixing costs, physical read/write +access, caller scheduling, hosting, precision, tapes, compiler closure, +recursive moments and outer recovery remain unproved. It establishes no +new κ and leaves all five selected framework assumptions intact. + +Credit Cinna Davis / 1337isnot1337, PR2258, for the H(m,n) coordinate-edge +model and natural/contragredient rank-nullity strategy. That package credits +the eumemic / woklerx normalized register model and preceding UT3/UT4 +shared-middle tariffs. Rank factorization, unitriangular representations, +rank-nullity and closed-walk accumulation are classical. No broad +literature-priority claim or independent human/kernel review is made. diff --git a/research/heisenberg-vector-central-tariff/README.md b/research/heisenberg-vector-central-tariff/README.md new file mode 100644 index 0000000000..930ef68125 --- /dev/null +++ b/research/heisenberg-vector-central-tariff/README.md @@ -0,0 +1,130 @@ +# Exact vector-label Heisenberg central-target tariff + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Scoped proof with exact finite corroboration; no new κ.** In the binary +group algebra of H(m,n), allow a paid rank-one register call to carry any +nonzero vector label x(u) or y(v), at one call per vector. For nonzero +central targets Z_t on P independent dirty roles, put K=Σ_t rank(Z_t). +The exact minimum is + + 2(K+P) = 2 Σ_t (rank(Z_t)+1), + +for every finite number of exactly restored dirty spectator roles. +Arbitrary invertible scalar mixing and nilpotent rank-one couplings are +allowed. Zero target matrices need no calls. + +The [written proof](PROOF.md) gives an explicit closed vector walk of this +length in the full group, and matching natural/contragredient rank-nullity +bounds. Its rank-two example takes six calls instead of the eight needed +by two separate rank-one commutator words: + + x(e1) y(e1) x(e1+e2) y(e2) x(e2) y(e1+e2) = z(I2). + +This is a new tariff for an enlarged alphabet. Cinna Davis's +[PR2258](https://github.com/CrocSwap/integer-mult-bounds/pull/2258) supplies +the coordinate-edge H(m,n) model and proof strategy. Its edge theorem is +cited, not audited or replayed. The cost of producing a vector label from +coordinate operations is outside the changed unit-call model. In +particular, this is no claim of a physical supplier saving. + +## Evidence + +The standard-library [verifier](verify.py) is standalone and read-only: + +- It enumerates all 682 central matrices for 1≤m,n≤3. Independent minor + ranks agree with the constructive decomposition. Complete Cayley BFS + covers 37,448 group elements across these nine groups and proves the + predicted one-role minimum for every central matrix in that domain. +- For Z=I2 with a restored second dirty role, its 54 generators include all + nine nonzero rank-one binary 2×2 matrices and all six vector labels. + Exact full-formal balls have layers 1, 54, 1,971 and 64,044. All 2,026 + radius-two join queries have no radius-three hit for the target. This + covers every normalized word of length at most five. The explicit + six-call witness is also found by the same join adapter at split 3+3. +- Five literal four-role formal endpoint fixtures include different target + ranks, zero targets and arbitrary restored dirty spectators, through a + rank-four central matrix. Every one of the 56 single-call omissions is + rejected. Four invalid matrices and a chronology mutation are rejected; + reversal is checked as a valid inverse control. + +Finite checks corroborate the proof; they do not establish its universal +quantifier. Each invocation prints a generated JSON record with source +hashes for the verifier and proof, followed by +`PASS_HEISENBERG_VECTOR_CENTRAL_TARIFF`. No receipt is hand-written. + +## Reproduce + +From the repository root, with CPython 3.12 and no third-party dependencies: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -B -W error research/heisenberg-vector-central-tariff/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -B -W error research/heisenberg-vector-central-tariff/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/heisenberg-vector-central-tariff +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/heisenberg-vector-central-tariff --check-source-history +``` + +Any CPython 3.12 path may replace the local interpreter above. Normal and +optimized scientific replays are registered separately in [VERIFY.json](VERIFY.json). +The source/history check requires the package to have been committed. +The optional `--skip-mixed` direct mode omits the finite two-role search +and is not the registered complete replay. + +## Limits and credit + +This counts formal paid calls. Arbitrary vector labels cost one by +hypothesis; their production, physical scalar mixing, native implementation, +source access, hosting, caller scheduling, precision/tapes, compiler closure, +recursive invoices and recovery are unproved. All five selected framework +assumptions remain. No selected record is changed. Independent human and +formal proof-kernel review are unclaimed. + +Credit Cinna Davis / 1337isnot1337, PR2258, for the main predecessor, +including its eumemic / woklerx normalized-register and UT3/UT4 +shared-middle lineage. Rank factorization, unitriangular representations, +rank-nullity and closed-walk accumulation are classical. No general +literature-priority claim is made. [SOURCES.json](SOURCES.json) pins the +predecessor proof and README as provenance, not scientific replay inputs. + +The `bit-new-register-model` card has changed scope to a formal +changed-alphabet cost theorem. The selected binding-only first example +passes. This is a small mechanism/obstruction result rather than a native +implementation or complete multiplication theorem. The +[advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19376637) +records the proposed formula before the checks. + +Overlap checks inspected canonical main +`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, live open/account PR lists, +recent handoffs, active Discussions, targeted all-state/merged searches, +and a complete cached scan of 598 open PRs and 6,673 discussion records. +Distinctive and general-form terms included Heisenberg, vector labels, +compound labels, central matrices and rank-based commutator tariffs. +The cached scan is timestamped November 3, 2026, 14:58 UTC. Closed PRs +outside targeted searches, arbitrary diffs and unpublished work remain +coverage limits; no-match searches are not novelty certificates. + +## Open next questions + +1. What is the exact tariff when label costs depend on the support size of + u or v? The unit-vector-label assumption is the unpriced physical step. + Start with the rank-two six-call word and charge each coordinate + constituent, then seek a weighted lower bound. The blocker is a specified + native vector-label interface and cost model. +2. Can a concrete bit supplier realize these labels and central outputs at + a favorable complete signed bill? Start by binding the six-call rank-two + word to one exact source/consumer boundary, including every dirty return. + No such mapping or caller invoice is supplied here. + +## Verification design + +The verifier has no recursion, subprocesses, network, dynamic code or writes. +Its fixed replay dimensions bound every loop: the largest Cayley domain is +32,768 elements, the mixed search has at most 1+54+54²+54³ stored states, +and formal fixtures have four roles with m,n≤4. Python allocates integers +and collections dynamically, a managed-runtime deviation from Power of Ten +rule 3. Live memory is bounded by these finite capacities; formal group +supports have at most 2^24 bits per matrix entry. Increasing these domains +requires a new capacity review. Functions fit within 60 physical lines; +explicit `require` checks remain active under optimized Python. Strict +warnings and AST compilation provide available interpreter diagnostics; +no additional static analyzer is installed in the command environment. diff --git a/research/heisenberg-vector-central-tariff/SOURCES.json b/research/heisenberg-vector-central-tariff/SOURCES.json new file mode 100644 index 0000000000..53359ff034 --- /dev/null +++ b/research/heisenberg-vector-central-tariff/SOURCES.json @@ -0,0 +1,30 @@ +{ + "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/heisenberg-commutator-incidence-seedb054/PROOF.md", + "usage": "provenance", + "git_blob": "8cbd78b3790f6dfc50cc74d3f6057457d14a1fc9", + "sha256": "dfb7bb979c11ba895f0e0efb38028195f1c8c050a14e1961dc2c675012ddea7b" + }, + { + "path": "research/heisenberg-commutator-incidence-seedb054/README.md", + "usage": "provenance", + "git_blob": "af9d60e661168678bb286e4987788f850824107f", + "sha256": "e55bec07f4b542c6c7d2690f4d13244b7a9a7d53f83063dddee17c6c9f1474f0" + } + ] +} diff --git a/research/heisenberg-vector-central-tariff/TASK.json b/research/heisenberg-vector-central-tariff/TASK.json new file mode 100644 index 0000000000..50d84dbfe1 --- /dev/null +++ b/research/heisenberg-vector-central-tariff/TASK.json @@ -0,0 +1,88 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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": "Exact vector-label Heisenberg central-target tariff 2 sum(rank(Z_t)+1) for arbitrary finite restored dirty workspace.", + "scope_change_reason": "Enlarge coordinate labels to arbitrary binary vector labels charged once per vector, and allow arbitrary central target matrices. This is a formal alphabet cost theorem, not a native implementation or repetition of the excluded abelian three-register model.", + "bottleneck_link": "Changing the operation alphabet permits a six-call rank-two central output instead of eight separate commutator calls. A matching dirty-workspace obstruction identifies the exact formal gain; physical label production and a complete recursive invoice remain necessary before this can affect BIT or kappa.", + "budget_minutes": 60, + "stop_rule": "Ship the first proved original tariff with exact finite corroboration; do not extend to weighted labels or physical implementation.", + "outcome": "completed", + "evidence": "PROOF.md gives the uniform theorem; verify.py independently enumerates 682 central matrices, exact Cayley minima, all two-role words of length <=5 through complete joins, full formal endpoints and controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the exact tariff for support-weighted vector labels?", + "why_it_matters": "Unit vector-label production is unpriced by this formal model.", + "first_step": "Charge the coordinate constituents of the six-call rank-two word and derive a weighted lower bound.", + "blocked_by": "A specified vector-label native interface and cost model." + }, + { + "question": "Can a concrete bit supplier realize this word with a favorable complete signed invoice?", + "why_it_matters": "A formal paid-call gain alone does not change the recursive exponent.", + "first_step": "Bind the six-call rank-two word to one exact source and consumer, including dirty returns.", + "blocked_by": "No physical label mapping or complete caller invoice is supplied." + } + ], + "claim_type": "scoped proof with finite corroboration", + "predecessor": { + "pr": 2258, + "author": "1337isnot1337", + "head": "6f43f8941fbe73ce411fa4698b8c0d96fb938e9e" + }, + "coordination": { + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19376637", + "upstream_checked_at": "2026-11-03T15:04:06.040951+00:00", + "priority_revision": 8, + "selected_pr": 6030 + }, + "question_source": "Original question motivated by the changed-alphabet limitation of PR2258; no predecessor open question is claimed to be settled.", + "environment": { + "python": "CPython 3.12.15", + "platform": "macOS 27.0.1 arm64", + "dependencies": "standard library only" + } +} diff --git a/research/heisenberg-vector-central-tariff/VERIFY.json b/research/heisenberg-vector-central-tariff/VERIFY.json new file mode 100644 index 0000000000..3bf83a0945 --- /dev/null +++ b/research/heisenberg-vector-central-tariff/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete vector-label central tariff corroboration: Cayley minima, dirty-workspace exact joins, full formal endpoints and rejection controls" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete vector-label central tariff corroboration: Cayley minima, dirty-workspace exact joins, full formal endpoints and rejection controls under optimized Python" + } + ] +} diff --git a/research/heisenberg-vector-central-tariff/verify.py b/research/heisenberg-vector-central-tariff/verify.py new file mode 100644 index 0000000000..65d602efbf --- /dev/null +++ b/research/heisenberg-vector-central-tariff/verify.py @@ -0,0 +1,280 @@ +#!/usr/bin/env python3 +"""Exact corroboration of the vector-label central tariff; stdlib only.""" + +import argparse +import hashlib +import itertools +import json +from collections import deque +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def outer(u, v, m, n): + return sum(((u >> i) & 1) * ((v >> j) & 1) << (i * n + j) + for i in range(m) for j in range(n)) + + +def multiply(a, b, m, n): + u, v, z = a + p, q, w = b + return u ^ p, v ^ q, z ^ w ^ outer(u, q, m, n) + + +def decompose(z, m, n): + """Row-pivot elimination as a sum of independent rank-one matrices.""" + require(1 <= m <= 4 and 1 <= n <= 4, "matrix dimensions out of bounds") + require(0 <= z < (1 << (m * n)), "matrix bits out of bounds") + residual = z + terms = [] + for _ in range(min(m, n)): + if not residual: + break + pivot = next(i for i in range(m) if (residual >> (i * n)) & ((1 << n) - 1)) + v = (residual >> (pivot * n)) & ((1 << n) - 1) + column = (v & -v).bit_length() - 1 + u = sum(((residual >> (i * n + column)) & 1) << i for i in range(m)) + terms.append((u, v)) + residual ^= outer(u, v, m, n) + require(residual == 0, "rank decomposition incomplete") + return terms + + +def minor_rank(z, m, n): + """Independent rank oracle: largest nonsingular binary minor.""" + for k in range(min(m, n), 0, -1): + for rows in itertools.combinations(range(m), k): + for cols in itertools.combinations(range(n), k): + determinant = 0 + for permutation in itertools.permutations(range(k)): + product = 1 + for i in range(k): + product &= (z >> (rows[i] * n + cols[permutation[i]])) & 1 + determinant ^= product + if determinant: + return k + return 0 + + +def central_word(z, m, n): + terms = decompose(z, m, n) + if not terms: + return [] + word = [] + previous = 0 + total_v = 0 + for u, v in terms: + word.extend([(u ^ previous, 0, 0), (0, v, 0)]) + previous = u + total_v ^= v + word.extend([(previous, 0, 0), (0, total_v, 0)]) + require(all(u or v for u, v, _ in word), "zero vector in constructed word") + return word + + +def endpoint(word, m, n): + state = (0, 0, 0) + for label in word: + state = multiply(state, label, m, n) + return state + + +def scalar_distances(m, n): + """Complete one-role Cayley BFS, including all central targets.""" + generators = [(u, 0, 0) for u in range(1, 1 << m)] + generators += [(0, v, 0) for v in range(1, 1 << n)] + capacity = 1 << (m + n + m * n) + distances = {(0, 0, 0): 0} + queue = deque([(0, 0, 0)]) + for _ in range(capacity): + if not queue: + break + state = queue.popleft() + for label in generators: + image = multiply(state, label, m, n) + if image not in distances: + distances[image] = distances[state] + 1 + queue.append(image) + require(not queue and len(distances) == capacity, "incomplete Cayley BFS") + return distances + + +def matrix_census(): + cases = 0 + states = 0 + ranks = {} + for m, n in itertools.product(range(1, 4), repeat=2): + distances = scalar_distances(m, n) + states += len(distances) + for z in range(1 << (m * n)): + k = minor_rank(z, m, n) + require(len(decompose(z, m, n)) == k, "rank oracles disagree") + word = central_word(z, m, n) + require(endpoint(word, m, n) == (0, 0, z), "wrong central endpoint") + tariff = 2 * (k + 1) if z else 0 + require(len(word) == tariff, "wrong construction length") + require(distances[(0, 0, z)] == tariff, "Cayley minimum differs") + cases += 1 + ranks[k] = ranks.get(k, 0) + 1 + return {"central_matrices": cases, "cayley_states": states, "rank_counts": ranks} + + +def group_index(g, m, n): + u, v, z = g + return u | (v << m) | (z << (m + n)) + + +def group_element(index, m, n): + return index & ((1 << m) - 1), (index >> m) & ((1 << n) - 1), index >> (m + n) + + +def translate(bits, label, m, n, left): + result = 0 + for _ in range(1 << (m + n + m * n)): + if not bits: + break + low = bits & -bits + g = group_element(low.bit_length() - 1, m, n) + h = multiply(label, g, m, n) if left else multiply(g, label, m, n) + result ^= 1 << group_index(h, m, n) + bits ^= low + require(bits == 0, "group support exceeded capacity") + return result + + +def formal_call(state, label, a, b, r, m, n): + """Right multiply the full formal matrix by I+([label]+1)ab^T.""" + result = list(state) + for i in range(r): + column = 0 + for j in range(r): + if (a >> j) & 1: + column ^= state[i * r + j] + delta = column ^ translate(column, label, m, n, False) + for j in range(r): + if (b >> j) & 1: + result[i * r + j] ^= delta + return tuple(result) + + +def identity(r): + return tuple(int(i == j) for i in range(r) for j in range(r)) + + +def formal_word(words, r, m, n): + state = identity(r) + for t, word in enumerate(words): + for label in word: + state = formal_call(state, label, 1 << t, 1 << t, r, m, n) + return state + + +def formal_target(targets, r, m, n): + return tuple((1 << group_index((0, 0, targets[i]), m, n) if i < len(targets) else 1) + if i == j else 0 for i in range(r) for j in range(r)) + + +def formal_fixtures(): + count = 0 + omissions = 0 + for m, n in [(2, 2), (2, 3), (3, 2), (3, 3), (4, 4)]: + full = sum(1 << (i * n + i) for i in range(min(m, n))) + targets = [full, 1, 0] + words = [central_word(z, m, n) for z in targets] + expected = formal_target(targets, 4, m, n) + require(formal_word(words, 4, m, n) == expected, "dirty endpoint mismatch") + count += 1 + for t, word in enumerate(words): + for j in range(len(word)): + changed = list(words) + changed[t] = word[:j] + word[j + 1:] + require(formal_word(changed, 4, m, n) != expected, "omission escaped") + omissions += 1 + return {"formal_dirty_fixtures": count, "omission_rejections": omissions} + + +def mixed_short_word_exclusion(): + """All normalized two-role words of length <=5, for rank-two Z=I2.""" + m = n = r = 2 + labels = [(u, 0, 0) for u in range(1, 4)] + [(0, v, 0) for v in range(1, 4)] + generators = list(itertools.product(labels, range(1, 4), range(1, 4))) + base = identity(r) + balls = {base: 0} + frontier = [base] + layers = [1] + ball2 = None + for depth in range(1, 4): + next_frontier = [] + for state in frontier: + for label, a, b in generators: + image = formal_call(state, label, a, b, r, m, n) + if image not in balls: + balls[image] = depth + next_frontier.append(image) + frontier = next_frontier + layers.append(len(frontier)) + if depth == 2: + ball2 = tuple(balls) + require(ball2 is not None, "missing short ball") + z = 1 | (1 << 3) + target = formal_target([z], r, m, n) + hits = 0 + for state in ball2: + image = tuple(translate(bits, (0, 0, z), m, n, True) if i < r else bits + for i, bits in enumerate(state)) + hits += int(image in balls) + require(hits == 0, "short dirty-workspace saving found") + word = central_word(z, m, n) + require(len(word) == 6 and formal_word([word], r, m, n) == target, "six-call witness failed") + suffix = identity(r) + for label in reversed(word[3:]): + suffix = formal_call(suffix, label, 1, 1, r, m, n) + joined = tuple(translate(bits, (0, 0, z), m, n, True) if i < r else bits + for i, bits in enumerate(suffix)) + require(joined == formal_word([word[:3]], r, m, n), "join adapter is wrong") + require(suffix in balls and joined in balls, "positive 3+3 join missing") + return {"mixed_generators": len(generators), "mixed_ball_layers": layers, + "mixed_join_queries": len(ball2), "mixed_short_hits": hits, + "mixed_minimum": 6, "mixed_positive_join": True} + + +def controls(): + rejected = 0 + for args in [(1, 0, 2), (1, 2, 5), (16, 2, 2), (-1, 2, 2)]: + try: + decompose(*args) + except ValueError: + rejected += 1 + else: + raise ValueError("invalid matrix accepted") + word = central_word(9, 2, 2) + require(endpoint(list(reversed(word)), 2, 2) == (0, 0, 9), "reverse control failed") + require(endpoint(sorted(word), 2, 2) != (0, 0, 9), "chronology control failed") + require(len(word) == 6 and len(word) < 4 * minor_rank(9, 2, 2), "changed-alphabet gain missing") + return {"invalid_inputs_rejected": rejected, "chronology_controls": 2, + "rank_two_cost": len(word), "separate_rank_one_commutators": 8} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--skip-mixed", action="store_true", help="omit the finite dirty-workspace search") + args = parser.parse_args() + result = {"claim_type": "scoped proof with finite corroboration", "no_new_kappa": True} + result.update(matrix_census()) + result.update(formal_fixtures()) + result.update(controls()) + if not args.skip_mixed: + result.update(mixed_short_word_exclusion()) + package = Path(__file__).resolve().parent + result["source_sha256"] = {name: hashlib.sha256((package / name).read_bytes()).hexdigest() + for name in ["verify.py", "PROOF.md"]} + print(json.dumps(result, sort_keys=True)) + print("PASS_HEISENBERG_VECTOR_CENTRAL_TARIFF") + + +if __name__ == "__main__": + main()