diff --git a/research/s4-stable-four-call/PROOF.md b/research/s4-stable-four-call/PROOF.md new file mode 100644 index 0000000000..5f654c3df6 --- /dev/null +++ b/research/s4-stable-four-call/PROOF.md @@ -0,0 +1,123 @@ +# Exact four-call minimum with every odd S4 label + +## Model and theorem + +Let A=F2[S4] be the full formal group algebra, with [g][h]=[gh] +and gh acting as g after h. Fix any finite register count r>=2. +All register inputs are arbitrary. A paid call has unit cost and matrix + + D_N(g) = I + ([g]+[e])N = [e](I+N) + [g]N, + +where g is any odd permutation and N is any rank-one idempotent in M_r(F2). +Every scalar GL_r(F2) map is free and may occur anywhere. No address map, +reset, clean register, erasure or additional operation is free. + +For any nonidentity a,b in A4, including a=b, the target is the complete +formal matrix + + T = diag([a],[b],[e],...,[e]). + +In particular all extra registers return individually to their arbitrary +entrance values and every off-diagonal coupling is zero. + +**Theorem.** The exact paid-call minimum is four, independently of r. +This remains a four-call lower bound if any subset of the odd labels is +permitted; attainment below uses the full odd-label alphabet. + +## 1. Normalize the scalar maps + +For any scalar G in GL_r(F2), + + G D_N(g) G^-1 = D_(G N G^-1)(g). + +Conjugation preserves rank one and idempotence. Move all free scalar maps +to the right, to write an arbitrary word as a product of the same number +of paid factors followed by one scalar map S. + +The augmentation homomorphism aug:A->F2 sends every group element to 1. +It sends each paid factor to I, and sends T to I. Applying it to the word +shows S=I. Thus it suffices to study a product of paid factors alone. +This step counts scalar mixing at intermediate cuts and does not restrict +which dirty roles a paid projector can couple. + +## 2. Every valid word has even length + +The sign map S4->C2 extends to an algebra homomorphism + + pi:A->F2[C2], pi([g]) = z for odd g, + z^2=1, pi([g]) = 1 for even g. + +The ring F2[C2] is commutative. A scalar basis diagonalizes N to +`diag(1,0,...,0)`, since an idempotent splits its image and kernel. +Consequently pi(D_N(g)) is similar to diag(z,1,...,1), and its determinant +is z. Determinants multiply over this commutative ring. A product of L +paid factors therefore has determinant z^L after pi, whereas pi(T)=I +has determinant 1. The formal basis elements 1 and z are distinct even +in characteristic two. Hence L is even. + +This is the sign-determinant method already used by Cinna Davis in #1734. +No determinant of a matrix over the noncommutative algebra A is taken. + +## 3. Two calls cannot deliver two active even targets + +Write a formal matrix as M=sum_g [g] C_g, where C_g is a binary scalar +matrix. Define its nonidentity even coefficient rank sum by + + E(M) = sum_(g even, g!=e) rank_F2(C_g). + +The proposed target always has E(T)=2. If a!=b, its two nonidentity +even coefficients are the two distinct coordinate projectors, each of +rank one. If a=b, the single coefficient at a has rank two. Restored +spectators contribute only to the identity coefficient. + +For odd s,t and rank-one idempotents N,M, direct multiplication gives + + D_N(s) D_M(t) + = [e](I+N+M+NM) + + [s](N+NM) + [t](M+NM) + [st]NM. (1) + +Repeated group labels in (1) are combined by addition in F2. The labels +s and t are odd. Thus the only possible nonidentity even label is st. +If st=e there is none. Otherwise its coefficient is NM, whose rank is +at most one. Therefore E(D_N(s)D_M(t))<=1, contradicting E(T)=2. + +Zero calls cannot realize T because a and b are nonidentity formal basis +elements. Section 2 excludes one and three calls, and (1) excludes two. +Every valid word therefore has at least four calls. This is a written +argument for every finite r, rather than an inference from a register census. + +## 4. Four calls attain every target + +Fix the odd transposition tau=(12). For each even h, put u_h=tau h. +It is odd, and tau u_h=h. If E_i is the i-th coordinate projector, then +idempotence gives the formal identity + + D_(E_i)(g) D_(E_i)(h) = D_(E_i)(gh). + +It follows that + + D_(E_1)(tau) D_(E_1)(u_a) + D_(E_2)(tau) D_(E_2)(u_b) = T. (2) + +Equation (2) uses four paid calls, requires no extra registers or scalar +changes, and acts identically on every dirty spectator. Some u_h are +four-cycles, so the larger paid alphabet is used. These calls are +invertible but need not be involutions; their inverses use inverse labels. + +## Scope and predecessor boundary + +Cinna Davis's #1749 establishes a finite four-role result for eight +noncommuting three-cycle pairs using only adjacent transpositions. +Ross Richardson's #1989 already proves all-register exact inversion tariffs +for that adjacent-label alphabet, including those pairs. Neither earlier +statement is claimed as new here. The new theorem allows every odd S4 +permutation at unit price, including nonadjacent transpositions and all +four-cycles, and covers every ordered pair of nonidentity even targets. +The proof combines the credited sign method with the two-call coefficient +rank sum in (1). No literature priority is claimed for determinant parity, +group-algebra expansion, rank submultiplicativity or coordinate projectors. + +This is a scoped formal-alphabet proof. It supplies no native address +implementation, physical scalar or routing price, precision bound, stock +bound, supplier admission or complete multiplication theorem. All such +obligations remain unproved here. The selected frontier is unchanged. diff --git a/research/s4-stable-four-call/README.md b/research/s4-stable-four-call/README.md new file mode 100644 index 0000000000..6548c9cbab --- /dev/null +++ b/research/s4-stable-four-call/README.md @@ -0,0 +1,118 @@ +# Four calls remain optimal with every odd S4 permutation + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped written proof with exact finite corroboration. For every +finite r>=2, every target diag([a],[b],1,...,1), with nonidentity even +permutations a,b in S4, has exact paid-call minimum four in the following +formal binary group-algebra model. A paid call is I+([g]+1)N, where g is +any odd permutation at unit cost and N is any binary rank-one idempotent. +Arbitrary scalar GL_r(F2) maps are free. Every extra register is dirty and +must return to its individual input value. The case a=b is included. + +The changed hypothesis is the paid alphabet. All twelve odd permutations +are available, including six four-cycles. Cinna Davis's [#1749](https://github.com/CrocSwap/integer-mult-bounds/pull/1749) gives the +four-role adjacent-transposition case; Ross Richardson's [#1989](https://github.com/CrocSwap/integer-mult-bounds/pull/1989) already +settles adjacent-transposition tariffs with arbitrary dirty workspace. +Those theorems are cited, not replayed. The new maximum-alphabet result +covers all ordered pairs of the eleven nonidentity even S4 permutations. +No kappa, native supplier or selected-frontier change is claimed. + +## Proof + +[PROOF.md](PROOF.md) gives the complete argument. Augmentation normalizes +all free scalar maps away from the endpoint. The inherited sign-determinant +method forces an even number of odd-label calls. A two-call product has at +most one nonidentity even coefficient, of scalar rank at most one. The +target's even coefficient rank sum is two, including when a=b. Four +coordinate calls attain every target. The proof applies at every finite +register count; the finite checks below only corroborate it. + +## Evidence and reproduction + +From the worktree root, using CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/s4-stable-four-call/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/s4-stable-four-call/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/s4-stable-four-call +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/s4-stable-four-call --check-source-history +``` + +A reviewer can substitute any CPython 3.12 executable. The expected marker +is PASS_S4_STABLE_FOUR_CALL. The verifier writes only stdout and prints a +generated receipt with the SHA256 of every package file. No receipt is +handwritten or committed. Explicit exceptions retain all checks with -O. + +The verifier multiplies the full formal group-algebra matrices for all +118,080 two-call words in the larger alphabet at r=2,3. It checks (1) independently +against convolution and checks the even coefficient rank bound. It builds +363 four-call endpoints for all 121 target pairs at r=2,3,5 and checks +29,040 dirty basis columns through a separate literal permutation-action +implementation. All 484 single-call omissions are rejected. +It also checks 650 sign determinants at r=2,3,4,5, all 432 two-role scalar +covariances and five hypothesis controls. These +include two-call counterexamples if even paid labels or scalar rank two +are allowed, and a rejection of treating four-cycle calls as involutions. + +The card's historical first command, scripts/research_baseline.py, was +attempted and failed with KeyError: 'bit_lower' under the selected schema. +The current scripts/research_selected_baseline.py passed with +PASS_RESEARCH_BASELINE_BINDINGS_ONLY. Neither is a scientific dependency +or an operator replay, and neither was changed here. + +## Limits and implementation bounds + +Only odd paid labels and rank-one idempotents are covered. Free address +maps, even paid labels, higher-rank paid calls, clean-only endpoints and +changed restoration contracts can change the answer. Nothing here prices +coefficient preparation, native implementation, scalar basis changes, +routing, physical restoration, tape, precision or a completed consumer. +These costs remain unknown. Independent human and formal proof-kernel +review are unclaimed. Lean, Docker and selected cold replay were not run. + +The verifier has no recursion or subprocesses. Its loop domains are fixed +at 24 group elements and at most five roles. It streams two-call words, +retaining at most 24 scalar coefficient blocks per formal matrix. Finite +Python tuples, dictionaries, integers and JSON serialization require +managed allocation; this is a bounded-domain deviation from fixed +steady-state allocation. Each hashed file is limited to 256 KiB. No +shared code, pinned evidence or predecessor file changes. + +The bit-new-register-model card is changed to a formal side result with +an enlarged paid-label set. It is not a physical construction expansion. +Historical provenance, source pins and structured next questions are in +[TASK.json](TASK.json) and [SOURCES.json](SOURCES.json). + +## Open next questions + +1. Can three nonidentity even targets share fewer than six calls in the + maximal odd-label alphabet? Start with four calls, the only remaining + candidate after parity. The two-call coefficient rank proof does not + bound the even coefficient sum of a four-call word. +2. Can a physical interface supply any nonadjacent odd permutation below + its complete adjacent-word price? Start with one four-cycle, accounting + for address preparation, scalar maps, restoration and routing. No such + implementation or complete consumer is supplied here. + +These follow-ups are not investigated or reserved. + +## Credit and overlap + +Cinna Davis #1749 supplies the original three-cycle/extra-register question +and #1734 supplies the sign-determinant precedent. Ross Richardson #1989 +supplies the exact adjacent-label theorem and normalization context, with +Adam Gall #1941 and Ross Richardson #1966 retaining the cut-method lineage. +Retain eumemic #288, Ali Romman #468, David Govea #720 and Gareth Davidson +#1333 for the register-model lineage. Original predecessor credit lines +and files remain unchanged. The new result is the enlarged-alphabet +four-call theorem and its coefficient-rank proof. + +[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19145529). +Live open PRs, this account's recent work, the latest handoffs and local +reservations were checked before claiming. Distinctive searches covered +merged PRs and all main-branch README paths. The cached overlap report +covered 314 open PRs and 4,389 Discussion records, but only 178 of 6,996 +main README paths in the sparse checkout; direct Git searches supplied +the main-branch coverage. Arbitrary diffs and unpublished work remain +outside that coverage. This is not a novelty certificate. diff --git a/research/s4-stable-four-call/SOURCES.json b/research/s4-stable-four-call/SOURCES.json new file mode 100644 index 0000000000..e8693b29a2 --- /dev/null +++ b/research/s4-stable-four-call/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/s4-double-transposition-seedb270/README.md", + "usage": "provenance", + "git_blob": "a15eea3cb33e00ed69e5695e3a27d0ffecbd24ec", + "sha256": "70098225ba21e1d2ef76600e3d4ba0f1368f4cdc2e8c9705f91eba0a1d11e4f5" + }, + { + "path": "research/s4-noncommuting-threecycle-r4-seeda27b/README.md", + "usage": "provenance", + "git_blob": "5af621bac9e1f05e92bcb436781a781d9764eb5b", + "sha256": "c52c66784a662ef63854a2944ed56f8540e288e1fb1674a0d4e7fa0fd51ce430" + }, + { + "path": "research/symmetric-adjacent-cut-bound/README.md", + "usage": "provenance", + "git_blob": "cdb3f431acc07b4a75abdd3998093fd68d9a498f", + "sha256": "4fb453c83d7cd15a93fc7c65b82f2f67cb609a31285ac9ebd1f44b675777d154" + } + ] +} diff --git a/research/s4-stable-four-call/TASK.json b/research/s4-stable-four-call/TASK.json new file mode 100644 index 0000000000..b04a732c0d --- /dev/null +++ b/research/s4-stable-four-call/TASK.json @@ -0,0 +1,106 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 7, + "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "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 four-call minimum for every nonidentity even S4 target pair, all finite dirty-register counts, all odd permutations available as unit-cost rank-one-idempotent calls, and free binary scalar mixing.", + "scope_change_reason": "The card is narrowed to a formal algebraic side result. Unlike the already-settled adjacent-label tariff, the paid alphabet includes all twelve odd permutations at unit cost.", + "bottleneck_link": "This rules out pair sharing even after granting every odd S4 address operation at unit price. Native implementation and the complete recursive invoice remain unknown.", + "budget_minutes": 60, + "stop_rule": "Stop at the first original written bound with a matching exact endpoint.", + "outcome": "completed", + "evidence": "Written augmentation/parity/coefficient-rank proof plus exact full-algebra convolution and separate regular-action finite corroboration.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can three nonidentity even targets use four maximal-odd calls?", + "why_it_matters": "It is the next possible sharing threshold after the proved pair obstruction.", + "first_step": "Fix a literal triple and inspect the even coefficients of four calls.", + "blocked_by": "No four-call coefficient-rank bound is supplied." + }, + { + "question": "Can one odd four-cycle be supplied below its complete adjacent-word price?", + "why_it_matters": "A formal enlarged alphabet gives no physical savings by itself.", + "first_step": "Specify and fully price one physical four-cycle caller.", + "blocked_by": "Native address preparation, scalar, routing and restoration costs are unknown." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19145529", + "predecessors": [ + { + "pr": 1749, + "author": "Cinna Davis", + "head": "90405b9498e4abfdd7d0eececcf11c7e83c6d13b", + "role": "Original finite adjacent-label question; cited only." + }, + { + "pr": 1989, + "author": "Ross Richardson", + "head": "8b9f3ec8b1e5745c42fec68d75da5fbc82ea91ec", + "role": "Already-settled arbitrary-workspace adjacent tariff; cited only." + }, + { + "pr": 1734, + "author": "Cinna Davis", + "role": "Sign-determinant precedent; cited only." + } + ], + "preserved_checkout": { + "branch": null, + "state": "detached HEAD, clean before work", + "head": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "prior_commits": [ + "e0c2e09b9443f22bb9e3c76ab08d1224493040e3", + "e5d7e4dc31331f19fb9ee795f180e6058ccf779c", + "3e1645cdee74aa5efb722f7d218f7465d219e66c", + "1e8187bea856a358ece55fb844189078bfae48b3" + ] + }, + "local_environment": { + "python": "CPython 3.12.15", + "platform": "macOS arm64", + "dependencies": "standard library only" + } +} diff --git a/research/s4-stable-four-call/VERIFY.json b/research/s4-stable-four-call/VERIFY.json new file mode 100644 index 0000000000..cc067f1384 --- /dev/null +++ b/research/s4-stable-four-call/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": "Full new-alphabet two-call coefficients, sign determinants, attaining dirty endpoints, separate regular action and hypothesis controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same exact checks under optimized Python, with explicit exceptions." + } + ] +} diff --git a/research/s4-stable-four-call/verify.py b/research/s4-stable-four-call/verify.py new file mode 100644 index 0000000000..a50269e7f3 --- /dev/null +++ b/research/s4-stable-four-call/verify.py @@ -0,0 +1,287 @@ +"""Exact corroboration for the maximal-odd S4 alphabet; writes only stdout.""" +from hashlib import sha256 +from itertools import permutations, product +import json +from pathlib import Path +import sys + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def identity(r): + return tuple(1 << i for i in range(r)) + + +def add(a, b): + need(len(a) == len(b), "matrix sizes differ") + return tuple(x ^ y for x, y in zip(a, b)) + + +def multiply(a, b): + r = len(a) + need(len(b) == r and 2 <= r <= 5, "matrix capacity") + result = [0] * r + for i in range(r): + for j in range(r): + if a[i] >> j & 1: + result[i] ^= b[j] + return tuple(result) + + +def rank(a): + rows = list(a) + r = len(a) + pivot = 0 + for column in range(r): + selected = next((i for i in range(pivot, r) + if rows[i] >> column & 1), None) + if selected is None: + continue + rows[pivot], rows[selected] = rows[selected], rows[pivot] + for i in range(r): + if i != pivot and rows[i] >> column & 1: + rows[i] ^= rows[pivot] + pivot += 1 + return pivot + + +def projectors(r): + need(2 <= r <= 5, "projector capacity") + result = [] + for u in range(1, 1 << r): + for v in range(1, 1 << r): + if (u & v).bit_count() % 2: + n = tuple(v if u >> i & 1 else 0 for i in range(r)) + need(multiply(n, n) == n and rank(n) == 1, + "projector definition") + result.append(n) + need(len(set(result)) == len(result), "duplicate projector") + return result + + +def group_data(): + elements = tuple(permutations(range(4))) + index = {g: i for i, g in enumerate(elements)} + table = tuple(tuple(index[tuple(g[h[i]] for i in range(4))] + for h in elements) for g in elements) + parity = tuple(sum(g[i] > g[j] for i in range(4) + for j in range(i + 1, 4)) % 2 for g in elements) + e = index[(0, 1, 2, 3)] + odd = tuple(i for i in range(24) if parity[i]) + even = tuple(i for i in range(24) if not parity[i] and i != e) + need(len(odd) == 12 and len(even) == 11, "S4 inventory") + for g, h in product(range(24), repeat=2): + need(parity[table[g][h]] == parity[g] ^ parity[h], "sign map") + return elements, table, parity, e, odd, even + + +def insert(result, g, matrix): + value = add(result.get(g, (0,) * len(matrix)), matrix) + if any(value): + result[g] = value + elif g in result: + del result[g] + + +def formal_product(a, b, table): + need(len(a) <= 24 and len(b) <= 24, "formal support capacity") + result = {} + for g, x in a.items(): + for h, y in b.items(): + insert(result, table[g][h], multiply(x, y)) + return result + + +def factor(g, n, e): + need(g != e and multiply(n, n) == n, "paid factor domain") + result = {} + insert(result, e, add(identity(len(n)), n)) + insert(result, g, n) + return result + + +def endpoint(a, b, r, e): + result = {} + for i in range(r): + matrix = tuple(1 << i if j == i else 0 for j in range(r)) + insert(result, (a, b)[i] if i < 2 else e, matrix) + return result + + +def word_product(word, r, e, table): + result = {e: identity(r)} + for g, n in word: + result = formal_product(result, factor(g, n, e), table) + return result + + +def ring_multiply(a, b): + # F2[C2], bit 0 is [e] and bit 1 is [z], with z*z=e. + return (((a & 1) * (b & 1) ^ (a >> 1) * (b >> 1)) + | (((a & 1) * (b >> 1) ^ (a >> 1) * (b & 1)) << 1)) + + +def quotient_determinant(n): + r = len(n) + need(2 <= r <= 5, "determinant capacity") + result = 0 + for permutation in permutations(range(r)): + term = 1 + for i, j in enumerate(permutation): + bit = n[i] >> j & 1 + value = ((i == j) ^ bit) | (bit << 1) + term = ring_multiply(term, value) + result ^= term + return result + + +def check_two_calls(table, parity, e, odd): + checked = even_supported = 0 + for r in (2, 3): + ps = projectors(r) + for s, t, n, m in product(odd, odd, ps, ps): + actual = formal_product(factor(s, n, e), factor(t, m, e), table) + nm = multiply(n, m) + expanded = {} + insert(expanded, e, add(add(add(identity(r), n), m), nm)) + insert(expanded, s, add(n, nm)) + insert(expanded, t, add(m, nm)) + insert(expanded, table[s][t], nm) + need(actual == expanded, "two-call expansion") + mass = sum(rank(c) for g, c in actual.items() + if g != e and not parity[g]) + need(mass <= 1, "two-call even coefficient rank") + if all(not parity[g] for g in actual): + even_supported += 1 + need(n == m, "even support requires a common projector") + checked += 1 + return {"two_call_words": checked, "even_supported_words": even_supported} + + +def regular_action(word, values, elements): + # Independent literal permutation composition, with no group table. + r = len(values) + for g, n in reversed(word): + source = 0 + first = next(i for i in range(r) if n[i]) + v = n[first] + for j in range(r): + if v >> j & 1: + source ^= values[j] + shifted = 0 + for h in range(24): + if source >> h & 1: + image = tuple(elements[g][elements[h][i]] for i in range(4)) + shifted ^= 1 << elements.index(image) + delta = shifted ^ source + values = tuple(value ^ (delta if n[i] else 0) + for i, value in enumerate(values)) + return values + + +def check_attainers(elements, table, parity, e, odd, even): + t = elements.index((1, 0, 2, 3)) + endpoints = columns = omissions = four_cycle_uses = 0 + for r in (2, 3, 5): + for a, b in product(even, repeat=2): + word = [] + for i, target in enumerate((a, b)): + n = tuple(1 << i if j == i else 0 for j in range(r)) + other = table[t][target] + need(other in odd and table[t][other] == target, "odd factorization") + word.extend(((t, n), (other, n))) + four_cycle_uses += (table[other][other] != e) + expected = endpoint(a, b, r, e) + need(word_product(word, r, e, table) == expected, "four-call endpoint") + need(sum(rank(c) for g, c in expected.items() + if g != e and not parity[g]) == 2, "target rank mass") + endpoints += 1 + for role, h in product(range(r), range(24)): + values = tuple(1 << h if j == role else 0 for j in range(r)) + actual = regular_action(word, values, elements) + target = (a, b)[role] if role < 2 else e + image = tuple(elements[target][elements[h][i]] for i in range(4)) + wanted = tuple(1 << elements.index(image) if j == role else 0 + for j in range(r)) + need(actual == wanted, "literal dirty regular action") + columns += 1 + if r == 3: + for omitted in range(4): + mutant = word[:omitted] + word[omitted + 1:] + need(word_product(mutant, r, e, table) != expected, + "omitted call accepted") + omissions += 1 + need(four_cycle_uses > 0, "enlarged alphabet was unused") + return {"four_call_endpoints": endpoints, "regular_basis_columns": columns, + "omission_rejections": omissions, "four_cycle_uses": four_cycle_uses} + + +def check_scalar_covariance(table, e, odd): + gl = tuple(a for a in product(range(4), repeat=2) if rank(a) == 2) + checked = 0 + for g in gl: + inverse = next(h for h in gl if multiply(g, h) == identity(2)) + for n, label in product(projectors(2), odd): + conjugate = multiply(multiply(g, n), inverse) + actual = formal_product(formal_product({e: g}, factor(label, n, e), table), + {e: inverse}, table) + need(actual == factor(label, conjugate, e), "free scalar covariance") + checked += 1 + return checked + + +def check_hypothesis_controls(elements, table, e, odd, even): + n, m = (1, 0), (0, 2) + # Even paid labels reach the two-target endpoint in two calls. + a, b = even[:2] + need(word_product(((a, n), (b, m)), 2, e, table) == endpoint(a, b, 2, e), + "even-label boundary control") + # Scalar rank two reaches a repeated even target in two calls. + s = elements.index((1, 0, 2, 3)) + t = elements.index((0, 2, 1, 3)) + a = table[s][t] + need(word_product(((s, identity(2)), (t, identity(2))), 2, e, table) + == endpoint(a, a, 2, e), "rank-two boundary control") + # A four-cycle call is invertible, but is not an involution. + c = next(g for g in odd if table[g][g] != e) + inverse = next(g for g in odd if table[c][g] == e) + need(word_product(((c, n), (c, n)), 2, e, table) != {e: identity(2)}, + "wrong involution shortcut") + need(word_product(((c, n), (inverse, n)), 2, e, table) == {e: identity(2)}, + "four-cycle inverse control") + # One even target is attained in two calls. + need(word_product(((s, n), (t, n)), 2, e, table) == factor(a, n, e), + "single-target control") + return 5 + + +def main(): + elements, table, parity, e, odd, even = group_data() + determinants = 0 + for r in (2, 3, 4, 5): + for n in projectors(r): + need(quotient_determinant(n) == 2, "sign determinant") + determinants += 1 + result = check_two_calls(table, parity, e, odd) + result.update(check_attainers(elements, table, parity, e, odd, even)) + result["scalar_covariances"] = check_scalar_covariance(table, e, odd) + result["hypothesis_controls"] = check_hypothesis_controls(elements, table, e, odd, even) + result["sign_determinants"] = determinants + result["ordered_even_target_pairs"] = len(tuple(product(even, repeat=2))) + source_hashes = {} + for name in ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py"): + raw = Path(__file__).with_name(name).read_bytes() + need(len(raw) <= 262144, "source byte capacity") + source_hashes[name] = sha256(raw).hexdigest() + receipt = {"status": "PASS_S4_STABLE_FOUR_CALL", "counts": result, + "python": sys.version.split()[0], "source_sha256": source_hashes} + canonical = json.dumps(receipt, sort_keys=True, separators=(",", ":")) + print(canonical) + print("PASS_S4_STABLE_FOUR_CALL receipt_sha256=" + sha256(canonical.encode()).hexdigest()) + + +if __name__ == "__main__": + main()