diff --git a/research/infinite-dihedral-register-bound/README.md b/research/infinite-dihedral-register-bound/README.md new file mode 100644 index 0000000000..531ddbd164 --- /dev/null +++ b/research/infinite-dihedral-register-bound/README.md @@ -0,0 +1,215 @@ +# Infinite dihedral targets: exact separate reflection bills with dirty workspace + +**Scoped negative theorem, no new kappa.** Let +`G = `, let `r=xy`, and write each target uniquely as +`g_i=r^{k_i} x^{e_i}`, with `k_i` an integer and `e_i` in `{0,1}`. +For every finite register count `R >= W`, the exact formal endpoint + +``` +diag([g_1], ..., [g_W], 1, ..., 1) +``` + +requires at least `A=sum_i |k_i+e_i|` paid **x** calls and +`B=sum_i |k_i|` paid **y** calls. A direct word simultaneously attains both +bounds. Positive per-label prices `alpha,beta` therefore give the exact bill +`alpha*A + beta*B`; in unit prices it is `A+B`. +In particular, arbitrary signed rotation powers cost `2 sum_i |k_i|`, even +with arbitrarily many restored dirty registers. This is a uniform written +proof, not an extrapolation from a finite word census or finite columns. + +## Alphabet, boundary, and changed premise + +Work in `M_R(F2[G])`. A paid call is +`D_N(g)=I+([g]+1)N`, where `g` is **only x or y** and +`N=u v^T` is a binary rank-one idempotent (`v^T u=1`). Scalar `GL_R(F2)` +changes are allowed free in this optimistic paid-call relaxation. No other +address maps, direct rotation primitive, erasure, COPY or clean state are +free. All W target inputs and all R-W workspace inputs are arbitrary dirty +data. Every workspace input must be restored, with no residual target coupling. +Every paid restoration call counts. This explicitly replaces the rational +abelian frame group of the three-register obstruction by a nonabelian group; +it does not reduce rational frames modulo two. + +Free scalar mixing can be normalized away: commute it through the paid calls, +conjugating N within the complete projector alphabet. Augmentation `[g] -> 1` +forces the final scalar matrix to be I. Hence it suffices to bound products of +paid calls alone. This standard normalization is credited to the retained +register-model lineage, not claimed as a new result. + +## Uniform lower-bound proof + +Put `L=F2[t,t^-1]`, and define two group representations by + +``` +C = [[0,1],[1,0]], V = [[0,t],[t^-1,0]], +rho(x)=C, rho(y)=V; sigma(x)=V, sigma(y)=C. +``` + +Both C and V square to I, so these are representations of the presented +infinite dihedral group. They induce algebra maps on every formal coefficient. +No converse from represented equality to formal equality is used. + +For an invertible Laurent matrix M, let `delta(M)` be the maximum Laurent +degree of every nonzero square minor of M, over **all sizes**, including the +empty minor 1. Thus delta is nonnegative. Cauchy--Binet gives + +``` +delta(AB) <= delta(A)+delta(B). +``` + +Indeed each minor of AB is a sum of products of equal-sized minors of A and B; +cancellation can only decrease degree. Every invertible constant binary matrix +and its inverse have delta zero. Applying the inequality in both directions +shows delta is unchanged by constant invertible left or right multiplication. + +A rank-one idempotent N is scalar-similar to `diag(1,0,...,0)`: its image and +kernel give a direct sum since N is idempotent. After applying rho or sigma, +a represented paid call is therefore constant-similar to `diag(C,I)` or +`diag(V,I)`. Every minor of `diag(C,I)` is constant. The only nonzero minors +of V have degrees `1,-1,0`; its determinant is 1. Minors of `diag(V,I)` are +zero or products of these with identity minors. Consequently + +``` +delta(rho(D_N(x)))=0, delta(rho(D_N(y)))=1; +delta(sigma(D_N(x)))=1, delta(sigma(D_N(y)))=0. +``` + +For the endpoint, `rho(r)=diag(t^-1,t)` and +`sigma(r)=diag(t,t^-1)`. The block for `r^k x^e` is a monomial permutation +matrix with its two nonzero exponents `-k,k` under rho and +`k+e,-(k+e)` under sigma. A nonzero minor of a monomial permutation matrix +selects some of its nonzero entries, with distinct rows and columns. Its maximum +degree is exactly the sum of positive exponents: select all positive entries +for equality, and none of the negative ones. Identity spectator blocks add +zero. Thus the two endpoint deltas are respectively B and A. Subadditivity +now gives `#y >= B` and `#x >= A` for **every word length and every R**. + +## Uniform attaining identity and complete invoice + +For a fixed coordinate projector E_i, idempotence directly gives +`D_{E_i}(g)D_{E_i}(h)=D_{E_i}(gh)` in the full group algebra. Calls on distinct +coordinate projectors commute. On role i use the freely reduced literal word +`(xy)^{k_i} x^{e_i}` (negative powers mean repetitions of yx). For `e_i=0` +it has `|k_i|` of each label; for `e_i=1`, it has `|k_i+1|` x labels and +`|k_i|` y labels. This proves the endpoint uniformly as a formal identity, +with the stated matching bills. No representation is used to certify this +upper bound. + +Products use the usual left-action convention: the rightmost factor acts first. +To execute a displayed word as successive in-place address permutations, run +its letters from right to left. This does not change either label's invoice. + +| Resource | Attaining implementation | +|---|---| +| Arbitrary target registers | W; all input data retained under specified permutations | +| Dirty workspace | R-W allowed by theorem, **zero needed** by attaining word | +| x calls / y calls | A / B, including all endpoint work | +| Free scalar basis changes / scalar row additions | Zero in the attaining word | +| Clean allocation, COPY, frame preparation, extra restoration | Zero in this formal implementation | +| Direct rotation or arbitrary address call | Not admitted | + +A concrete action is `x(a)=-a`, `y(a)=-a-1` on integer addresses; `r(a)=a+1`. +The formal identity holds under every action of G, including cyclic addresses +`Z/LZ` for every L. For a concrete finite in-place bit-array implementation, +store W arrays of L bits (plus any explicitly retained spectators), use the +fixed schedule above, and implement each reflection by disjoint swaps. For odd +L each reflection fixes one address and uses `(L-1)/2` swaps; hence the witness +uses exactly `(A+B)(L-1)/2` bit swaps, at most +`3(A+B)(L-1)/2` XOR assignments with the three-XOR swap, no clean data bit, +and O(log L + log(1+max |k_i|) + log(1+W)) address/counter bits. For even L, +x fixes two addresses and y fixes none, giving `A(L-2)/2+B L/2` swaps. +This invoice describes this witness, **not** an optimal physical finite-array +algorithm: finite cyclic quotient relations admit shortcuts absent formally. + +No bridge makes these paid reflections admissible native bit-supplier children. +Frame/compiler, hosting, precision/tape, recursive coverage and analytic transfer +are unestablished, not zero-cost claims about the selected construction. Since +there is no formal saving even with scalar mixing priced at zero, this alphabet +fails the local compression target before those nonnegative adoption costs. +The selected complex supplier still binds; no frontier file is changed. + +## Reproduce and evidence scope + +``` +python3 -I -O -B research/infinite-dihedral-register-bound/verify.py +uv run --python 3.12 --no-project scripts/research_package.py --package research/infinite-dihedral-register-bound +``` + +The standard-library verifier checks the complete projector sets for R=1,2,3,4, +call involutions, all-minor degrees for R<=2, and two independent group laws: +integer-affine normal forms and literal free reduction of x/y words. All 144 +two-call words over the full two-register projector alphabet are checked with +both formal engines and both represented degree bounds, including mixed +non-coordinate projectors. It also verifies +100 heterogeneous two-target formal endpoints with exponents in [-2,2], plus +four- and seven-register signed fixtures, exact per-label invoices, every +single-call omission, wrong order/label and dirty-restoration controls. A +finite-quotient alias control demonstrates why finite columns cannot establish +this lower bound. Checks use explicit exceptions and remain active under -O. +The checker corroborates finite instances; the universal conclusion comes from +the proof above. Neither proof-assistant nor independent human review is claimed. + +Observed initial verification on 2026-10-14, macOS arm64, CPython 3.12.12: +metadata/pins passed; registered isolated optimized replay passed in 0.23 s; +direct isolated unoptimized replay passed in 0.13 s. Both emitted +`formal_targets=102`, `generator_minor_checks=28`, `omission_controls=540`, +`other_controls=4`, `projectors=155` and `PASS_INFINITE_DIHEDRAL_REGISTER_BOUND`. +The publication replay additionally passed `mixed_words=144`; registered +optimized replay took 0.29 s and direct unoptimized replay took 0.18 s. +Timings are observations, not performance guarantees. No selected cold replay +was run; the prescribed source-binding positive control passed separately. + +## Sources, overlap, and credit + +Base `0b1cccf86e2f5132ed286a26ef0a681a495740ea`; selected-record SHA256 +`10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32`. +Local predecessor byte pins are in SOURCES.json. Credit eumemic PR288 for the +scalar-idempotent model, Ali Romman PR468 and the retained three-register note, +woklerx PR1443 for the D8 formal-alphabet predecessor, Gareth Davidson PR1333 +for the nonabelian affine direction, and the subsequent all-register work. + +Closest live work, inspected by complete PR or discussion bodies: + +- [PR1573](https://github.com/CrocSwap/integer-mult-bounds/pull/1573), steph4n-gh, + head `0b8c5a69297c794f2de22c04494c83e41300ae36`: already proves all-register + D8 central targets cost 4k, with separate label tariffs. We do not claim that + conclusion anew. Its finite-group zero-projector-sum proof differs from the + Laurent minor-degree proof here; infinite rotations have no torsion relation. +- [PR1478](https://github.com/CrocSwap/integer-mult-bounds/pull/1478), juper997, + head `b30fdba48f3db70e3589ba740b0782b56ec0ba2e`: D8 with R=2,3, superseded + in register scope by PR1573. +- [PR1821](https://github.com/CrocSwap/integer-mult-bounds/pull/1821), Cinna Davis, + head `a986127fa82b680a5bbb29f49fec4c8c3a944bde`: D16 central pair, R=2, + exact 16-call search. Our Laurent representation does **not** factor through + that finite group, so our theorem does not generalize its result. +- [PR1733](https://github.com/CrocSwap/integer-mult-bounds/pull/1733), Cinna Davis, + head `01ac3f397eaaa9f7a72ecafc7f0fbf128571424a`: four rational registers, + fixed 15-address two-relation ansatz, finite negative census. Different group, + target and method; not reopened here. +- [PR1822](https://github.com/CrocSwap/integer-mult-bounds/pull/1822), Aaron Wang, + head `ee736b4b11bbd63b04d94c8edafb3790161ebdea`: Q8 central and mixed pair, + R=2,3. Different finite group and label-square relation. + +Overlap helper snapshot on 2026-10-14 13:15Z covered 540 open PRs (including +drafts) and 524 discussions with complete pagination. Exact `infinite dihedral`, +`Laurent`, `dihedral` search returned no infinite-dihedral match; this is not +proof of novelty. Closed PR coverage is only through local notes/ledger, and +arbitrary code diffs were not searched. Live heads and claims remain provisional. +Before publication, an offline exact-term recheck at 13:42Z used the shared +cache covering 543 open PRs (13:23:53Z) and 529 discussions (13:25:07Z), +both completely paginated. Only this local package matched `infinite dihedral`; +the helper explicitly warned that cached records may miss current changes. +Parent coordination: [Discussion1884](https://github.com/CrocSwap/integer-mult-bounds/discussions/1884). +Prepared for Adam Gall with substantial OpenAI Codex assistance in the proof, +implementation, overlap investigation and writing. Apache-2.0. + +## Open next questions + +1. Can a finite-dihedral torsion-aware substitute for maximal-minor degree give + arbitrary-register lower bounds for powers beyond the D8 result? This would + close the workspace gap in the D16 census. First test the proposed invariant + on the relation `(xy)^n=1`; the Laurent invariant here fails precisely there. +2. Is either reflection a justified native supplier operation at the claimed + unit tariff? First derive its actual all-size compiler and full interface + invoice. No such bridge is supplied; without it this remains a formal-model + side result, not a multiplication improvement. diff --git a/research/infinite-dihedral-register-bound/SOURCES.json b/research/infinite-dihedral-register-bound/SOURCES.json new file mode 100644 index 0000000000..b8da7147e1 --- /dev/null +++ b/research/infinite-dihedral-register-bound/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "06c96f5579bb67ed1b86d334e78fbed7da6945f1", + "sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075" + }, + { + "path": "research/binary-affine-register-bound/README.md", + "usage": "input", + "git_blob": "7b68583becf8be6f3cf666b05b0943e7eb99270c", + "sha256": "7951868efdf35fdb2aacdd302ca825cbde0586a5fae6df23aee78e29f30c332a" + }, + { + "path": "research/bit-dihedral-commutator/README.md", + "usage": "input", + "git_blob": "b7619a5d56f32daf7f48d6cc3a0e260c5a333510", + "sha256": "4f3f9df6d6d96a26ccb0fcd2ef947cce5d53b0d992da22e866f1e025be4c0492" + }, + { + "path": "research/bit-three-register-lower-bound/README.md", + "usage": "input", + "git_blob": "25e41c370c101a33a6deb978de08b03ed7539b79", + "sha256": "c12b33ef388deece0cbf891505a2ce2c0779a0c3a6cf1f0f7f7039bab59cbebd" + } + ] +} diff --git a/research/infinite-dihedral-register-bound/TASK.json b/research/infinite-dihedral-register-bound/TASK.json new file mode 100644 index 0000000000..baac06616f --- /dev/null +++ b/research/infinite-dihedral-register-bound/TASK.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 3, + "base_commit": "0b1cccf86e2f5132ed286a26ef0a681a495740ea", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json" + ], + "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.", + "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": "Write a complete operation alphabet outside one named premise and price a baseline before searching identities.", + "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." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "refined", + "actual_scope": "Infinite dihedral F2[C2*C2] with x/y paid reflections, arbitrary finite dirty-register count and all diagonal targets r^k x^e: sharp separate label bills sum|k+e| and sum|k|.", + "scope_change_reason": "Instantiate the allowed nonabelian-operation variation, replacing rational abelian frames by an explicitly infinite dihedral group. Arbitrary signed powers and mixed reflection targets distinguish this from finite D8/D16/Q8 work.", + "bottleneck_link": "Formal-model side result: no local paid-call compression even before nonnegative physical adoption costs; no native supplier mapping or kappa gain is claimed.", + "budget_minutes": 60, + "stop_rule": "Prove the two Laurent minor-degree inequalities, replay bounded exact controls, and stop; no finite-group census or supplier changes.", + "outcome": "completed", + "evidence": "README.md uniform proof and implementation invoice; verify.py exact full-coefficient words, independent literal reductions, minor checks and negative controls; parent coordination Discussion1884.", + "author": "Adam Gall with OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in proof development, exact checker implementation, source investigation and documentation; no independent human review.", + "open_questions": [ + { + "question": "Can a torsion-aware finite-dihedral invariant close arbitrary-workspace bounds beyond D8?", + "why_it_matters": "The D16 two-register census does not cover arbitrary workspace, and this infinite-group representation does not factor through D16.", + "first_step": "Test a candidate invariant against (xy)^n=1 before any word search.", + "blocked_by": "Laurent degree is not invariant under finite cyclic quotient relations." + } + ,{ + "question": "Can the paid reflections be admitted as native bit-supplier operations?", + "why_it_matters": "A formal alphabet is not a physical supplier or exponent improvement.", + "first_step": "Derive one all-size reflection compiler and its full frame, hosting, precision and recursive invoice.", + "blocked_by": "No native interface mapping is established here." + } + ] +} diff --git a/research/infinite-dihedral-register-bound/VERIFY.json b/research/infinite-dihedral-register-bound/VERIFY.json new file mode 100644 index 0000000000..625ed0c936 --- /dev/null +++ b/research/infinite-dihedral-register-bound/VERIFY.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/binary-affine-register-bound/README.md", + "research/bit-dihedral-commutator/README.md", + "research/bit-three-register-lower-bound/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact formal and independent literal endpoints; all-minor generator/target degree checks; paid invoices, omitted calls, wrong labels/order, dirty spectator and finite-quotient alias controls." + } + ] +} diff --git a/research/infinite-dihedral-register-bound/verify.py b/research/infinite-dihedral-register-bound/verify.py new file mode 100755 index 0000000000..54a6bdb9a3 --- /dev/null +++ b/research/infinite-dihedral-register-bound/verify.py @@ -0,0 +1,246 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the written arbitrary-register theorem. + +No finite matrix test is used to infer the universal formal identity. +Only Python's standard library is needed; checks survive python -O. +""" +from itertools import combinations, permutations, product +import json + +E = (0, 0) +X = (0, 1) +Y = (-1, 1) +ZERO = frozenset() +ONE = frozenset({E}) + + +def require(value, message): + if not value: + raise ValueError(message) + + +def group_mul(a, b): + return (a[0] + (-1 if a[1] else 1) * b[0], a[1] ^ b[1]) + + +def convolution(a, b, multiply): + out = set() + for x in a: + for y in b: + z = multiply(x, y) + if z in out: + out.remove(z) + else: + out.add(z) + return frozenset(out) + + +def matmul(a, b, multiply): + n = len(a) + return tuple(tuple(sum_cells(convolution(a[i][k], b[k][j], multiply) + for k in range(n)) for j in range(n)) + for i in range(n)) + + +def sum_cells(cells): + out = ZERO + for cell in cells: + out = out ^ cell + return out + + +def identity(n, one=ONE): + return tuple(tuple(one if i == j else ZERO for j in range(n)) for i in range(n)) + + +def projectors(n): + for u in range(1, 1 << n): + for v in range(1, 1 << n): + if (u & v).bit_count() % 2: + yield tuple(tuple(((u >> i) & 1) * ((v >> j) & 1) + for j in range(n)) for i in range(n)) + + +def diagonal_projector(n, role): + return tuple(tuple(int(i == role and j == role) for j in range(n)) for i in range(n)) + + +def call(n, g, projector): + return tuple(tuple((ONE if i == j else ZERO) ^ + (frozenset({E, g}) if projector[i][j] else ZERO) + for j in range(n)) for i in range(n)) + + +def reduced(word): + stack = [] + for letter in word: + if stack and stack[-1] == letter: + stack.pop() + else: + stack.append(letter) + return tuple(stack) + + +def letters(g): + k, flip = g + word = ('x', 'y') * k if k >= 0 else ('y', 'x') * -k + return reduced(word + (('x',) if flip else ())) + + +def direct(targets, n): + return [(X if label == 'x' else Y, diagonal_projector(n, role)) + for role, target in enumerate(targets) for label in letters(target)] + + +def endpoint(targets, n): + return tuple(tuple(frozenset({targets[i] if i < len(targets) else E}) + if i == j else ZERO for j in range(n)) for i in range(n)) + + +def replay(word, n): + out = identity(n) + for g, projector in word: + out = matmul(out, call(n, g, projector), group_mul) + return out + + +def literal_replay(word, n): + """Independent group arithmetic: cancellation of literal x/y words.""" + unit = frozenset({()}) + out = identity(n, unit) + for g, projector in word: + label = ('x',) if g == X else ('y',) + factor = tuple(tuple((unit if i == j else ZERO) ^ + (frozenset({(), label}) if projector[i][j] else ZERO) + for j in range(n)) for i in range(n)) + out = matmul(out, factor, lambda a, b: reduced(a + b)) + return out + + +def representation(matrix, swapped=False): + """Map formal cells to 2-by-2 Laurent blocks, storing exponents exactly.""" + n = len(matrix) + out = [[ZERO for _ in range(2 * n)] for _ in range(2 * n)] + for i in range(n): + for j in range(n): + for k, flip in matrix[i][j]: + power = k + flip if swapped else -k + for a in range(2): + b = a ^ flip + out[2 * i + a][2 * j + b] ^= frozenset({power if a == 0 else -power}) + return tuple(tuple(row) for row in out) + + +def determinant(matrix): + n = len(matrix) + terms = [] + for p in permutations(range(n)): + term = frozenset({0}) + for i, j in enumerate(p): + term = convolution(term, matrix[i][j], lambda a, b: a + b) + terms.append(term) + return sum_cells(terms) + + +def minor_degree(matrix): + """Maximum degree of every square minor, including the empty minor.""" + n = len(matrix) + result = 0 + for size in range(1, n + 1): + for rows in combinations(range(n), size): + for cols in combinations(range(n), size): + det = determinant(tuple(tuple(matrix[i][j] for j in cols) for i in rows)) + if det: + result = max(result, max(det)) + return result + + +def main(): + counts = {"projectors": 0, "generator_minor_checks": 0, "mixed_words": 0, + "formal_targets": 0, "omission_controls": 0, "other_controls": 0} + for n, expected in ((1, 1), (2, 6), (3, 28), (4, 120)): + ps = tuple(projectors(n)) + require(len(ps) == expected, "projector census") + counts['projectors'] += len(ps) + for p in ps: + require(all(sum(p[i][k] * p[k][j] for k in range(n)) % 2 == p[i][j] + for i in range(n) for j in range(n)), "idempotence") + for label in (X, Y): + c = call(n, label, p) + require(matmul(c, c, group_mul) == identity(n), "call involution") + if n <= 2: + for swapped in (False, True): + actual = minor_degree(representation(c, swapped)) + expected_degree = int((label == X) == swapped) + require(actual == expected_degree, "generator degree") + counts['generator_minor_checks'] += 1 + generators = tuple(product((X, Y), projectors(2))) + for word in product(generators, repeat=2): + formal = replay(word, 2) + literal = tuple(tuple(frozenset(letters(g) for g in cell) for cell in row) + for row in formal) + require(literal_replay(word, 2) == literal, "mixed-projector word") + for swapped in (False, True): + represented = matmul(representation(call(2, *word[0]), swapped), + representation(call(2, *word[1]), swapped), + lambda a, b: a + b) + require(representation(formal, swapped) == represented, + "mixed-word representation") + charged_label = X if swapped else Y + require(minor_degree(represented) <= sum(g == charged_label for g, _ in word), + "mixed-word degree bound") + counts["mixed_words"] += 1 + group_window = tuple(product(range(-2, 3), range(2))) + for a, b in product(group_window, repeat=2): + require(reduced(letters(a) + letters(b)) == letters(group_mul(a, b)), + "independent group law") + for swapped in (False, True): + left = representation(((frozenset({group_mul(a, b)}),),), swapped) + right = matmul(representation(((frozenset({a}),),), swapped), + representation(((frozenset({b}),),), swapped), + lambda x, y: x + y) + require(left == right, "representation homomorphism") + fixtures = [(list(ts), 2) for ts in product(group_window, repeat=2)] + fixtures += [([(2, 0), (-2, 1), (1, 1)], 4), + ([(7, 0), (-5, 1), (0, 1), (-3, 0)], 7)] + for targets, n in fixtures: + word = direct(targets, n) + goal = endpoint(targets, n) + require(replay(word, n) == goal, "formal endpoint") + literal_goal = tuple(tuple(frozenset(letters(g) for g in cell) for cell in row) + for row in goal) + require(literal_replay(word, n) == literal_goal, "literal endpoint") + require(sum(g == X for g, _ in word) == sum(abs(k + f) for k, f in targets), + "x invoice") + require(sum(g == Y for g, _ in word) == sum(abs(k) for k, _ in targets), + "y invoice") + if n == 2: + for swapped in (False, True): + require(minor_degree(representation(goal, swapped)) == + sum(abs(k + (f if swapped else 0)) for k, f in targets), + "target degree") + for i in range(len(word)): + require(replay(word[:i] + word[i + 1:], n) != goal, "omission accepted") + counts['omission_controls'] += 1 + counts['formal_targets'] += 1 + dirty_targets, n = [(1, 0), (-1, 1)], 4 + word = direct(dirty_targets, n) + goal = endpoint(dirty_targets, n) + require(replay(word + [(X, diagonal_projector(n, 3))], n) != goal, + "dirty spectator mutation accepted") + require(replay(list(reversed(word)), n) != goal, "reversed rotation accepted") + require(replay([(Y, p) if g == X else (X, p) for g, p in word], n) != goal, + "swapped labels accepted") + counts['other_controls'] += 3 + # Finite cyclic specialization is deliberately NOT a lower-bound oracle. + finite_alias = ((frozenset({E, (4, 0)}),),) + require(finite_alias[0][0] != ZERO, "formal alias control") + require(sum_cells(frozenset({(k % 4, f)}) for k, f in finite_alias[0][0]) == ZERO, + "finite quotient control") + counts['other_controls'] += 1 + print(json.dumps(counts, sort_keys=True)) + print('PASS_INFINITE_DIHEDRAL_REGISTER_BOUND finite_checks_only; universal_proof=README.md') + + +if __name__ == '__main__': + main()