From d2704e235f3b9e8ac01cd794d96db0ece1be4672 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 3 Nov 2026 12:16:35 +0000 Subject: [PATCH] feat(research): prove exact monomial reflection tariffs --- research/monomial-reflection-tariff/PROOF.md | 159 ++++++++++ research/monomial-reflection-tariff/README.md | 127 ++++++++ .../monomial-reflection-tariff/SOURCES.json | 30 ++ research/monomial-reflection-tariff/TASK.json | 76 +++++ .../monomial-reflection-tariff/VERIFY.json | 37 +++ research/monomial-reflection-tariff/verify.py | 277 ++++++++++++++++++ 6 files changed, 706 insertions(+) create mode 100644 research/monomial-reflection-tariff/PROOF.md create mode 100644 research/monomial-reflection-tariff/README.md create mode 100644 research/monomial-reflection-tariff/SOURCES.json create mode 100644 research/monomial-reflection-tariff/TASK.json create mode 100644 research/monomial-reflection-tariff/VERIFY.json create mode 100644 research/monomial-reflection-tariff/verify.py diff --git a/research/monomial-reflection-tariff/PROOF.md b/research/monomial-reflection-tariff/PROOF.md new file mode 100644 index 0000000000..dab4497d45 --- /dev/null +++ b/research/monomial-reflection-tariff/PROOF.md @@ -0,0 +1,159 @@ +# A full monomial reflection alphabet has an additive register tariff + +## Exact model + +Let K be a field with an element zeta of exact finite order m, and let n>=1. +Write G=G(m,1,n) for the monomial matrices with nonzero entries in . +The notation also covers m=1. Encode an element g=(p,a) by + + g e_j = zeta^(a_j) e_(p(j)), a_j in Z/mZ. + +Let b(g) count the cycles C of p for which sum_(j in C) a_j=0 mod m. +These are the balanced cycles, including balanced fixed coordinates. +The ordinary reflection-length formula n-b(g) is classical; see +[Jian-yi Shi](https://www.sciencedirect.com/science/article/pii/S0021869307003882) and +[Briana Foster-Greenwood, Section 3](https://arxiv.org/html/1202.0266v1#S3). Section 2 gives +its elementary construction here, so no external classification is needed. + +Use the full formal group algebra K[G], with R>=W finite register roles. +All inputs are arbitrary. Free scalar operations are GL_R(K) matrices. +A paid unit operation is + + D_N(t) = I + ([t]-[e]) N, + rank_K(N)=1, N^2=N, rank_K(t-I)=1, t in G. + +The address alphabet is every monomial reflection, not just adjacent swaps. +It consists exactly of: + +- a phase multiplication zeta^a on one coordinate, a!=0 mod m; +- a swap of coordinates i,j with phases zeta^a,zeta^(-a). + +Indeed, Section 1 shows that displacement rank one allows either one +unbalanced singleton, or one balanced two-cycle, with every other coordinate +balanced and fixed. Phase operations may have order greater than two. +The inverse of each operation is in the same paid alphabet. Idempotence +also gives D_N(t)^(-1)=D_N(t^(-1)), so all paid factors are invertible. + +The required complete endpoint is + + F = diag([g_1],...,[g_W],[e],...,[e]) in M_R(K[G]). + +Every spectator is restored, and every off-diagonal entry vanishes. Scalar +preparation and restoration are free only in this explicit optimistic model. +Every address operation, including undoing one, is counted. No address map, +reset, erasure, or clean state is free. + +**Theorem.** The minimum paid-call count is + + sum_(j=1)^W (n-b(g_j)), + +for every finite number of arbitrary restored dirty spectators. Identity +and empty target lists are allowed. A common positive unit price multiplies +the formula. This is a scoped formal-algebra theorem, not a native supplier. + +## 1. Displacement rank and the lower bound + +On a permutation cycle, a fixed vector satisfies + + x_(p(j)) = zeta^(a_j) x_j. + +After one circuit this gives x_j=zeta^(sum a) x_j. The fixed space on that +cycle has dimension one exactly when the cycle is balanced, and zero +otherwise. Distinct cycles use independent coordinates. Hence + + rank_K(g-I)=n-b(g). + +This proof also covers characteristic two when the stated roots exist. +No real ordering, semisimplicity, or division by |G| is used. + +We use the augmentation normalization and displacement-rank method of +Gareth Davidson's PR1333. They are prior methods, not new principles here. +Augmentation sends every [g] to 1 and every D_N(t) to I. It sends F to I. +Move every scalar basis change to the right of the chronological product. +Conjugation only replaces N by B N B^(-1), still a rank-one idempotent. +The remaining scalar product is I by augmentation. Therefore the endpoint +has a normalized factorization entirely into paid factors of the same count. + +Apply the natural monomial representation to the group algebra. A normalized +paid factor becomes + + I + N tensor (t-I). + +Its difference from I has rank exactly one, by the rank formula for a +Kronecker product. For invertible A,B, the elementary identity + + AB-I = A(B-I)+(A-I) + +gives rank(AB-I)<=rank(A-I)+rank(B-I). The represented diagonal endpoint +has displacement rank sum_j rank(g_j-I), since its blocks are independent +and its spectators have zero displacement. Iterating the inequality proves +the claimed lower bound for every R. Scalar mixing and dirty helpers do not +remove any term from it. + +The natural representation is only a necessary lower-bound image. Equality +in that image is never used to certify a formal endpoint. For example, when +m=3,n=2 over C, the nonzero group-algebra norm sum_(g in G)[g] maps to zero: +for each possible nonzero matrix position its three phases sum to zero. +An off-diagonal norm leak is still a dirty leak in the formal model. + +## 2. An attaining cycle splitter + +Use composition g h = g after h. Start with a cycle containing i and +j=p(i), with j!=i. Right multiply by the weighted swap t defined by + + t e_i = zeta^(a_i) e_j, + t e_j = zeta^(-a_i) e_i. + +Then + + (g t)e_j = e_j, + (g t)e_i = zeta^(a_i+a_j) e_(p(j)). + +Thus j becomes a balanced singleton and the old cycle loses one coordinate, +while its total phase is unchanged. Repeating on an original cycle of length +ell takes ell-1 weighted swaps and leaves one singleton carrying that cycle's +phase. A balanced cycle is now fully fixed. An unbalanced cycle needs exactly +one diagonal phase operation, its inverse phase, to reach the identity. +The number of right peels is ell-1 or ell respectively, hence n-b(g) in total. + +If g t_1 ... t_L=e, then + + g=t_L^(-1) ... t_1^(-1). + +Execute t_1^(-1),...,t_L^(-1) chronologically on one coordinate register. +The full formal product is [g]. This uses no scalar mixing or spectator. +For several targets, concatenate their independent coordinate-register +words. The full endpoint is F in K[G], with exactly the lower-bound bill. +This proves simultaneous attainment and the theorem. + +## 3. First new example and interpretation + +Take m=3,n=2 and g e_0=zeta e_1, g e_1=e_0. Its only cycle is unbalanced, +so it costs two paid reflections. The two-register endpoint diag([g],[g^-1]) +costs exactly four with any finite restored dirty workspace. The splitter +uses one phase-weighted swap and one phase operation per target. The inverse +phase operations are paid units too. This is an address alphabet absent from +the simple-reflection Coxeter model, and its scalar field contains a genuine +third root of unity. + +Allowing all nonadjacent phase-weighted swaps and higher-order phases does +not create a sharing saving under this unit-reflection invoice. A productive +escape must change a further hypothesis, for example give selected higher-rank +operations a concave price, or supply a different free-operation boundary. +This conclusion does not exclude those changed models. + +## 4. Proof and certificate boundaries + +The all-parameter conclusion is the written argument above. The finite +verifier independently enumerates small groups, runs an unpruned Cayley +search, computes displacement ranks, and checks the new splitter's words. +Its complete rational group-algebra fixtures mix a dirty spectator through +oblique projectors, check all off-diagonal entries, and run the literal +inverse. They do not enumerate all register circuits; the lower-bound proof +covers those. + +No native address implementation, scalar/routing/storage cost, child-rank +moment, compiler/hosting admission, precision/tape bound, new kappa, or +complete multiplication theorem is supplied. Independent human and formal +proof-kernel review are unclaimed. The selected frontier and its five +framework assumptions are unchanged. diff --git a/research/monomial-reflection-tariff/README.md b/research/monomial-reflection-tariff/README.md new file mode 100644 index 0000000000..5fe3081ed1 --- /dev/null +++ b/research/monomial-reflection-tariff/README.md @@ -0,0 +1,127 @@ +# Exact tariffs for full monomial reflection words + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Claim type: scoped written proof with exact finite corroboration.** +For G(m,1,n), allow every monomial rank-one reflection as a unit paid call, +including nonadjacent phase-weighted swaps and higher-order phase operations. +For arbitrary diagonal targets g_j, free scalar mixing, and any finite number +of restored arbitrary dirty registers, the exact minimum count is + + sum_j (n - b(g_j)), + +where b(g) counts permutation cycles whose accumulated phase is one. The +coefficient field may be any field containing an element of exact order m. +Every target has a constructive attaining word, with no helper or scalar +preparation. [PROOF.md](PROOF.md) gives the full model and proof. + +For example, with a primitive third root zeta, the two-coordinate map +`g e_0=zeta e_1, g e_1=e_0` has one unbalanced cycle. The endpoint +`diag([g],[g^-1])` costs exactly four calls, regardless of the number of +restored dirty spectators. Both phase and swap calls are charged. + +The new contribution is this register-model tariff for a changed alphabet. +The ordinary reflection-length formula is classical, including +[Jian-yi Shi's formula](https://www.sciencedirect.com/science/article/pii/S0021869307003882) +and [Briana Foster-Greenwood's length/codimension treatment](https://arxiv.org/html/1202.0266v1#S3). +The proof restates the elementary cycle construction and uses the established +augmentation/displacement-rank method. No new reflection-length principle +or literature-wide priority is claimed. + +## Evidence and reproduction + +The standalone checker imports no predecessor executable and writes only to +standard output. Its generated receipt binds every package file by SHA256. +The fixed finite domains are G(1,1,4), G(2,1,4), G(3,1,3), G(3,1,4), +G(4,1,3), G(5,1,3) and G(6,1,3). + +- An unpruned Cayley search visits all 4,944 group elements and 130,344 + directed transitions. Every distance equals n-b(g). Every constructed + word has that length and the exact formal group label. Separate dense + finite-field multiplication and displacement ranks agree, using primitive + roots over F5, F7 or F11. +- All 324 ordered G(3,1,2) target pairs have complete rational group-algebra + endpoints and inverse restoration with a genuinely mixed dirty spectator. + The fixtures contain 972 paid events. Each of the 323 nonempty words fails + when its first call is omitted. No basis-only endpoint test is used. +- Controls distinguish an unbalanced cycle, chronological order, a nonprimitive + root and a formal dirty leak that vanishes in the natural representation. + The nonzero eighteen-term group norm is retained by the formal oracle. + +From the repository root, with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/monomial-reflection-tariff/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/monomial-reflection-tariff/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/monomial-reflection-tariff +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/monomial-reflection-tariff --check-source-history +``` + +Other hosts may substitute their CPython 3.12 executable. Expected markers +are `PASS_MONOMIAL_REFLECTION_TARIFF`, `PASS_REGISTERED_RESEARCH_PACKAGE` +and `PASS_RESEARCH_COMMIT_BYTES`. Both registered commands run the same +finite coverage in normal and optimized Python. Each has a 60-second limit. +The written proof supplies the universal conclusion; the finite cases +corroborate it. No receipt is handwritten or regenerated during verification. + +## Sources, overlap and limits + +The source question is David Arias / DavidAriasC's +[PR2738](https://github.com/CrocSwap/integer-mult-bounds/pull/2738), +Open next question 2. That theorem covers simple Coxeter generators. This +package changes the paid alphabet to all monomial reflections, including +operations of order greater than two. Gareth Davidson / bitplane's +[PR1333](https://github.com/CrocSwap/integer-mult-bounds/pull/1333) +supplies augmentation normalization and the displacement-rank method, +retaining eumemic, Ali Romman / PR468, David Govea / PR720 and their credited +register-model lineage. Adam Gall and Ross Richardson's cut-method lineage +remains credited by PR2738. These results are cited, not audited or replayed. + +Scientific base is canonical main +`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8, selected +PR6030. [SOURCES.json](SOURCES.json) pins the question and method statements. +[TASK.json](TASK.json) records the changed card scope. The +[advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19373434) +precedes the computation. Source-binding orientation passed. Cached overlap +covered 556 open PRs and 6,600 Discussion records with complete pagination; +only 123 local notes were materialized against 8,917 HEAD note paths. +Targeted all-main general-form searches and merged-PR searches supplement +that sparse local coverage. Arbitrary diffs and unpublished work are limits. + +This closes a sharing route within an optimistic unit-reflection model. +It does not price higher-rank calls concavely, classify nonuniform generator +prices, or implement a native address instruction. Scalar work, routing, +ownership, storage, precision, stock, tape, hosting, complete recursive +invoices and outer use remain separate obligations. No supplier admission, +new kappa, selected-frontier change or complete multiplication theorem is +claimed. All five selected framework assumptions remain. Independent human +and formal proof-kernel review are unclaimed. Lean, Docker, predecessor +scientific replays and selected cold replay were not run. + +## Verifier bounds + +There is no recursion, network, subprocess, dynamic code or external callback. +Each fixed search has at most 1,944 group states and 33 generators. Matrix +rank checks have at most four rows. Formal fixtures have three registers, +eighteen possible group labels and rational coefficients. Every loop is +bounded by these fixed domains or by the finite collection it reads. +Every function is shorter than 60 physical lines. Explicit exceptions keep +checks active under optimized Python; warning-strict normal and optimized +execution are the available diagnostics. No separate static analyzer is +installed. Source reads authenticate the two fixed predecessor text inputs. + +Power-of-ten rule 3 deviation: Python allocates tuples, integers, fractions, +sets and dictionaries dynamically. The fixed domains above bound live data; +Python offers no static allocation guarantee. A larger externally supplied +search is outside the executable contract. No repository-wide build settings +or predecessor code are changed. + +## Open next questions + +Can selected higher-rank monomial calls with concave prices beat this +unit-reflection invoice after their native implementation costs are included? +This changes the price contract and may admit sharing. Start with one +explicit primitive and complete formal endpoint, then compare its full +boundary bill. The present rank-one proof does not charge such a primitive +one unit or establish physical profitability. Without that changed contract, +further dirty-workspace searches in this alphabet are unnecessary. diff --git a/research/monomial-reflection-tariff/SOURCES.json b/research/monomial-reflection-tariff/SOURCES.json new file mode 100644 index 0000000000..69e60de223 --- /dev/null +++ b/research/monomial-reflection-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/binary-affine-register-bound/PROOF.md", + "usage": "input", + "git_blob": "b1152a39b559f7a058489ec74231488e4f8edd83", + "sha256": "36a33434222798434b0a17476ae5f9bc8a2a3891871c46e77cc50ce2e132206b" + }, + { + "path": "research/coxeter-root-tariff/README.md", + "usage": "input", + "git_blob": "9ed141d29e7f552d9cbc9c0f499b4dc901bdee13", + "sha256": "e8ad34f2926dadd897d2f9c6ee7295ecc61cfa13c776ab1c6ea5be82fdc1fa93" + } + ] +} diff --git a/research/monomial-reflection-tariff/TASK.json b/research/monomial-reflection-tariff/TASK.json new file mode 100644 index 0000000000..311f093ba5 --- /dev/null +++ b/research/monomial-reflection-tariff/TASK.json @@ -0,0 +1,76 @@ +{ + "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 additive dirty-register tariff for the full monomial reflection alphabet G(m,1,n), over fields with a primitive m-th root.", + "scope_change_reason": "Replace the rational/adjacent primitive alphabet by all monomial rank-one reflections, including higher-order phases; prove a scoped obstruction before any native implementation.", + "bottleneck_link": "Side result screening a changed nonabelian instruction alphabet. An optimistic sharing obstruction prevents a fruitless workspace search; it supplies no selected supplier or kappa gain.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified exact tariff or explicit counterexample; do not extend to other groups or prices.", + "outcome": "completed", + "evidence": "Written all-parameter proof; complete finite Cayley/rank/splitter domains, rational formal dirty endpoints and inverse/omission/kernel controls in verify.py.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a physically implemented higher-rank monomial primitive with a concave price beat the unit-reflection invoice?", + "why_it_matters": "The rank-one unit-price bound does not price the larger recursive call alphabet.", + "first_step": "Specify one primitive, its complete formal endpoint and all boundary charges, then compare the signed invoice.", + "blocked_by": "No such native primitive and complete caller bill is supplied." + } + ], + "source_question": { + "pr": 2738, + "author": "DavidAriasC", + "head": "833b8e05bbed0d77419c1d05d057bfde34bac551", + "question": "Open next question 2, changed operation alphabet" + }, + "predecessor_method": { + "pr": 1333, + "author": "bitplane", + "head": "7f25b6d0e1d7e995d4d2840f231d98b1a1a9fec2" + }, + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19373434" +} diff --git a/research/monomial-reflection-tariff/VERIFY.json b/research/monomial-reflection-tariff/VERIFY.json new file mode 100644 index 0000000000..dfda558c09 --- /dev/null +++ b/research/monomial-reflection-tariff/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/binary-affine-register-bound/PROOF.md", + "research/coxeter-root-tariff/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "All fixed Cayley, displacement, constructive, formal dirty endpoint, inverse and rejection domains; hash-bound receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "All fixed Cayley, displacement, constructive, formal dirty endpoint, inverse and rejection domains; hash-bound receipt." + } + ] +} diff --git a/research/monomial-reflection-tariff/verify.py b/research/monomial-reflection-tariff/verify.py new file mode 100644 index 0000000000..66b6d86d47 --- /dev/null +++ b/research/monomial-reflection-tariff/verify.py @@ -0,0 +1,277 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the monomial-reflection register tariff.""" +from collections import Counter +from fractions import Fraction +from hashlib import sha256 +from itertools import permutations, product +import json +from math import factorial +from pathlib import Path + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def identity(n): + return tuple(range(n)), (0,) * n + + +def compose(g, h, m): + p, a = g + q, b = h + return tuple(p[q[j]] for j in range(len(p))), tuple( + (b[j] + a[q[j]]) % m for j in range(len(p))) + + +def inverse(g, m): + p, a = g + q, b = [0] * len(p), [0] * len(p) + for j, k in enumerate(p): + q[k], b[k] = j, -a[j] % m + return tuple(q), tuple(b) + + +def reflections(m, n): + out = [] + for i in range(n): + for a in range(1, m): + phase = [0] * n + phase[i] = a + out.append((tuple(range(n)), tuple(phase))) + for j in range(i + 1, n): + for a in range(m): + p, phase = list(range(n)), [0] * n + p[i], p[j], phase[i], phase[j] = j, i, a, -a % m + out.append((tuple(p), tuple(phase))) + need(len(set(out)) == n * (m - 1) + m * n * (n - 1) // 2, + 'reflection alphabet cardinality') + return tuple(out) + + +def balanced_cycles(g, m): + p, a = g + seen, count = set(), 0 + for start in range(len(p)): + if start in seen: + continue + j, phase = start, 0 + for _ in range(len(p)): + seen.add(j) + phase = (phase + a[j]) % m + j = p[j] + if j == start: + break + else: + raise ValueError('cycle did not close') + count += phase == 0 + return count + + +def factor(g, m): + n, current, word = len(g[0]), g, [] + for _ in range(n): + i = next((i for i in range(n) if current[0][i] != i), None) + if i is None: + break + j, phase = current[0][i], current[1][i] + p, a = list(range(n)), [0] * n + p[i], p[j], a[i], a[j] = j, i, phase, -phase % m + t = tuple(p), tuple(a) + current = compose(current, t, m) + need(current[0][j] == j and current[1][j] == 0, 'peel fixed coordinate') + word.append(inverse(t, m)) + for i in range(n): + phase = current[1][i] + if phase: + a = [0] * n + a[i] = -phase % m + t = tuple(range(n)), tuple(a) + current = compose(current, t, m) + word.append(inverse(t, m)) + need(current == identity(n), 'peeling endpoint') + return tuple(word) + + +def dense(g, prime, root): + p, a = g + return [[pow(root, a[j], prime) if p[j] == i else 0 + for j in range(len(p))] for i in range(len(p))] + + +def multiply(a, b, prime): + n = len(a) + return [[sum(a[i][k] * b[k][j] for k in range(n)) % prime + for j in range(n)] for i in range(n)] + + +def rank(a, prime): + a = [[v % prime for v in row] for row in a] + rows, cols, r = len(a), len(a[0]), 0 + for col in range(cols): + pivot = next((i for i in range(r, rows) if a[i][col]), None) + if pivot is None: + continue + a[r], a[pivot] = a[pivot], a[r] + scale = pow(a[r][col], -1, prime) + a[r] = [v * scale % prime for v in a[r]] + for i in range(r + 1, rows): + scale = a[i][col] + a[i] = [(x - scale * y) % prime for x, y in zip(a[i], a[r])] + r += 1 + return r + + +def domain(m, n, prime, root): + need(1 <= m <= 6 and 1 <= n <= 4, 'finite verification domain') + need(prime in (5, 7, 11) and pow(root, m, prime) == 1, + 'root domain') + need(all(pow(root, k, prime) != 1 for k in range(1, m)), 'primitive root') + e, generators = identity(n), reflections(m, n) + order, queue, distance = factorial(n) * m ** n, [e], {e: 0} + transitions = 0 + for cursor in range(order): + need(cursor < len(queue), 'Cayley search exhausted too soon') + g = queue[cursor] + for t in generators: + h = compose(t, g, m) + transitions += 1 + if h not in distance: + need(len(queue) < order, 'Cayley search exceeded group order') + distance[h] = distance[g] + 1 + queue.append(h) + expected = {(p, a) for p in permutations(range(n)) for a in product(range(m), repeat=n)} + need(set(queue) == expected, 'complete independent object enumeration') + for g in queue: + length = n - balanced_cycles(g, m) + need(distance[g] == length, 'exact shortest address tariff') + matrix = dense(g, prime, root) + need(rank([[matrix[i][j] - (i == j) for j in range(n)] + for i in range(n)], prime) == length, 'displacement rank') + word, state, represented = factor(g, m), e, dense(e, prime, root) + need(len(word) == length and all(t in generators for t in word), 'attaining word') + for t in word: + state = compose(t, state, m) + represented = multiply(dense(t, prime, root), represented, prime) + need(state == g and represented == matrix, 'formal label and dense endpoints') + for t in generators: + a = dense(t, prime, root) + need(rank([[a[i][j] - (i == j) for j in range(n)] + for i in range(n)], prime) == 1, 'paid displacement rank one') + return {'m': m, 'n': n, 'prime': prime, 'root': root, 'objects': order, + 'transitions': transitions, 'distance_histogram': dict(sorted(Counter(distance.values()).items()))} + + +def scalar_state(b, e): + return [[{e: Fraction(v)} if v else {} for v in row] for row in b] + + +def scalar_left(b, state): + size, out = len(b), [[{} for _ in b] for _ in b] + for i, j, k in product(range(size), repeat=3): + for g, coefficient in state[k][j].items(): + out[i][j][g] = out[i][j].get(g, 0) + b[i][k] * coefficient + return [[{g: v for g, v in cell.items() if v} for cell in row] for row in out] + + +def paid_left(state, t, u, v, m): + size, out = len(state), [[dict(cell) for cell in row] for row in state] + for i, j, k in product(range(size), repeat=3): + scale = u[i] * v[k] + if not scale: + continue + for g, coefficient in state[k][j].items(): + h, value = compose(t, g, m), scale * coefficient + out[i][j][h] = out[i][j].get(h, 0) + value + out[i][j][g] = out[i][j].get(g, 0) - value + return [[{g: c for g, c in cell.items() if c} for cell in row] for row in out] + + +def endpoint(targets, e): + return [[{targets[i]: Fraction(1)} if i == j else {} + for j in range(len(targets))] for i in range(len(targets))] + + +def formal_fixtures(): + m, n, e = 3, 2, identity(2) + b = ((1, 1, 0), (0, 1, 1), (1, 0, 1)) + c = tuple(tuple(Fraction(v, 2) for v in row) for row in + ((1, -1, 1), (1, 1, -1), (-1, 1, 1))) + need(all(sum(b[i][k] * c[k][j] for k in range(3)) == (i == j) + for i, j in product(range(3), repeat=2)), 'scalar gauge inverse') + group = tuple((p, a) for p in permutations(range(n)) for a in product(range(m), repeat=n)) + fixtures, events, omissions, inverses = 0, 0, 0, 0 + for g, h in product(group, repeat=2): + calls = tuple((j, t) for j, target in enumerate((g, h)) for t in factor(target, m)) + state = scalar_state(b, e) + for j, t in calls: + u, v = tuple(b[i][j] for i in range(3)), c[j] + need(sum(x * y for x, y in zip(u, v)) == 1, 'idempotent call') + state = paid_left(state, t, u, v, m) + state = scalar_left(c, state) + need(state == endpoint((g, h, e), e), 'complete rational formal dirty endpoint') + state = scalar_left(b, state) + for j, t in reversed(calls): + u, v = tuple(b[i][j] for i in range(3)), c[j] + state = paid_left(state, inverse(t, m), u, v, m) + state = scalar_left(c, state) + need(state == endpoint((e, e, e), e), 'formal inverse restoration') + inverses += 1 + fixtures, events = fixtures + 1, events + len(calls) + if calls: + state = scalar_state(b, e) + for j, t in calls[1:]: + state = paid_left(state, t, tuple(b[i][j] for i in range(3)), c[j], m) + need(scalar_left(c, state) != endpoint((g, h, e), e), 'omitted call detection') + omissions += 1 + return {'ordered_target_pairs': fixtures, 'paid_events': events, + 'complete_inverse_checks': inverses, 'omitted_first_calls_rejected': omissions} + + +def controls(): + e = identity(2) + g = ((1, 0), (1, 0)) + need(2 - balanced_cycles(g, 3) == 2, 'unbalanced two-cycle costs two') + need(factor(g, 3) != tuple(reversed(factor(g, 3))), 'noncommuting order witness') + need(compose(*factor(g, 3), 3) != g, 'wrong chronological order rejected') + all_group = tuple((p, a) for p in permutations(range(2)) for a in product(range(3), repeat=2)) + norm = [[sum(dense(h, 7, 2)[i][j] for h in all_group) % 7 + for j in range(2)] for i in range(2)] + need(norm == [[0, 0], [0, 0]], 'representation-kernel fixture') + leaked = endpoint((g, e), e) + leaked[0][1] = {h: Fraction(1) for h in all_group} + need(leaked != endpoint((g, e), e), 'formal norm leak must remain nonzero') + try: + domain(3, 2, 7, 1) + except ValueError as error: + need(str(error) == 'primitive root', 'wrong root rejection reason') + else: + raise ValueError('nonprimitive root accepted') + return {'controls': ['unbalanced_cycle', 'noncommuting_fixture', 'wrong_order', + 'zero_represented_norm', 'nonzero_formal_leak', 'nonprimitive_root'], + 'norm_terms': len(all_group)} + + +def main(): + package = Path(__file__).resolve().parent + root = package.parent.parent + sources = json.loads((package / 'SOURCES.json').read_text()) + for source in sources['files']: + if source['usage'] == 'input': + need(sha256((root / source['path']).read_bytes()).hexdigest() == source['sha256'], + 'source hash: ' + source['path']) + cases = ((1, 4, 5, 1), (2, 4, 5, 4), (3, 3, 7, 2), (3, 4, 7, 2), + (4, 3, 5, 2), (5, 3, 11, 3), (6, 3, 7, 3)) + results = [domain(*case) for case in cases] + result = {'marker': 'PASS_MONOMIAL_REFLECTION_TARIFF', 'domains': results, + 'objects': sum(row['objects'] for row in results), + 'transitions': sum(row['transitions'] for row in results), + 'formal': formal_fixtures(), 'controls': controls()} + names = ('README.md', 'PROOF.md', 'TASK.json', 'SOURCES.json', 'VERIFY.json', 'verify.py') + result['package_sha256'] = {name: sha256((package / name).read_bytes()).hexdigest() for name in names} + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == '__main__': + main()