From 125ed77d114e0db0cb2c684494c7a5c90f559d60 Mon Sep 17 00:00:00 2001 From: Cinna Davis <1337isnot1337@users.noreply.github.com> Date: Wed, 14 Oct 2026 11:58:47 -0500 Subject: [PATCH] Research: exact SL2(F3) mixed-triple call minimum --- .../CERTIFICATE.json | 65 +++ .../sl2f3-conjugate-triple-seed592f/README.md | 67 +++ .../SOURCES.json | 24 + .../sl2f3-conjugate-triple-seed592f/TASK.json | 88 ++++ .../VERIFY.json | 20 + .../sl2f3-conjugate-triple-seed592f/verify.py | 415 ++++++++++++++++++ 6 files changed, 679 insertions(+) create mode 100644 research/sl2f3-conjugate-triple-seed592f/CERTIFICATE.json create mode 100644 research/sl2f3-conjugate-triple-seed592f/README.md create mode 100644 research/sl2f3-conjugate-triple-seed592f/SOURCES.json create mode 100644 research/sl2f3-conjugate-triple-seed592f/TASK.json create mode 100644 research/sl2f3-conjugate-triple-seed592f/VERIFY.json create mode 100644 research/sl2f3-conjugate-triple-seed592f/verify.py diff --git a/research/sl2f3-conjugate-triple-seed592f/CERTIFICATE.json b/research/sl2f3-conjugate-triple-seed592f/CERTIFICATE.json new file mode 100644 index 0000000000..7a17c8efc8 --- /dev/null +++ b/research/sl2f3-conjugate-triple-seed592f/CERTIFICATE.json @@ -0,0 +1,65 @@ +{ + "direct_paid_bill": 5, + "direct_word": [ + "D[i;100*100^T]", + "D[w;010*010^T]", + "D[w^-1;001*001^T]", + "D[i;001*001^T]", + "D[w;001*001^T]" + ], + "free_scalar_mixing_covered": true, + "group_generated_by": [ + "i", + "i^-1", + "w", + "w^-1" + ], + "group_order": 24, + "i_matrix_mod3": [ + [ + 0, + 1 + ], + [ + 2, + 0 + ] + ], + "limitations": [ + "finite nonabelian address algebra only", + "address-operation implementation cost not priced", + "no selected supplier or kappa change claimed" + ], + "model": "M3(F2[SL2(F3)])", + "mutated_generator_control": true, + "omission_controls": 5, + "one_call_states": 112, + "paid_call_alphabet": 112, + "positive_control_minimum": 2, + "rank_one_idempotents": 28, + "result_minimum": 5, + "schema_version": 1, + "search_depth": 4, + "short_witness": null, + "short_witness_indices": null, + "target_c": "w^-1*i*w", + "target_diagonal": [ + "i", + "w", + "c" + ], + "two_call_distinct_states": 8905, + "two_call_full_convolution_cross_checks": 12544, + "two_call_state_sha256": "7313957379a9c51963604fae5f6a69edda1771006526c9c2ef4ab068e76bed95", + "two_call_words": 12544, + "w_matrix_mod3": [ + [ + 0, + 2 + ], + [ + 1, + 2 + ] + ] +} diff --git a/research/sl2f3-conjugate-triple-seed592f/README.md b/research/sl2f3-conjugate-triple-seed592f/README.md new file mode 100644 index 0000000000..519b393c8c --- /dev/null +++ b/research/sl2f3-conjugate-triple-seed592f/README.md @@ -0,0 +1,67 @@ +# Exact five-call minimum for a binary tetrahedral register endpoint + +**Scoped exact negative result; no new `kappa`.** In the finite nonabelian model below, the heterogeneous target `diag([i],[w],[w^-1 i w])` has exact paid-call minimum **five**. Its direct word costs five. An exhaustive exact search excludes every word with four or fewer factors, so this target gives no paid-call saving in this model. + +## Model and complete bill + +Let `G = SL2(F3)`, the 24 matrices of determinant one over `F3`, and work in the full formal group algebra `R = F2[G]`. Use + +```text +i = [[0, 1], [-1, 0]], w = [[0, -1], [1, -1]] (entries modulo 3), +c = w^-1 i w. +``` + +The four paid address labels are `i`, `i^-1`, `w`, and `w^-1`; they generate all of `G`. A paid factor is + +```text +D_N(g) = I + ([g] + [e]) N, +``` + +where `N = x y^T` is a rank-one idempotent in `M3(F2)`, so `x,y` are nonzero binary three-vectors with `y^T x = 1`. There are 28 such idempotents and therefore 112 paid factors. Each costs one. The three registers are all targets; there is no extra dirty workspace, clean state, COPY/ERASE, or uncharged paid call. Free scalar `GL3(F2)` mixing is allowed. + +The target is + +```text +diag([i], [w], [c]). +``` + +The direct word applies `i` to role 0 and `w` to role 1, then applies `w^-1, i, w` in that order to role 2. This is an exact five-call word. The element `c` has order four and shortest length three in the four-label address alphabet. + +## Exact coverage + +The verifier stores each of the nine entries as a 24-bit coefficient support, so equality means equality of every coefficient in `F2[G]`. All four-call words are covered by a meet-in-the-middle join of two-call prefix and suffix states. There are 12,544 ordered two-call words and 8,905 distinct exact states. For each distinct suffix state `B`, the verifier computes `target * B^-1` and checks exact membership in the complete two-call prefix table. This covers all `112^4 = 157,351,936` raw four-call words, including duplicates. The same suffix set checks every three-call word as a one-plus-two split; words of length zero, one and two are checked directly. In total, every word at each length zero through four is excluded. + +Each factor satisfies `D_N(g)^-1 = D_N(g^-1)`, so the suffix inverse is exact. The fast rank-one transition is independently cross-checked against full coefficient convolution for all 12,544 two-call products. The complete rank-one idempotent set absorbs arbitrary free `GL3(F2)` changes of basis: augmentation `[g] -> 1` sends each paid factor and the target to identity, forcing the net free scalar map to be identity, and pushing each free map through a factor only conjugates `N` within the enumerated set. + +The exact minimum is therefore five **only for this fixed group, generator alphabet, target, three roles, and one-call factor definition**. `CERTIFICATE.json` records the two-call state count and a digest of the canonically ordered states; exact tuple equality, not the digest, decides the joins. + +## Reproduce + +From the repository root with Python 3.12 and the standard library: + +```sh +python3.12 -I -B research/sl2f3-conjugate-triple-seed592f/verify.py +python3.12 scripts/research_package.py --package research/sl2f3-conjugate-triple-seed592f +``` + +Expected verifier line: + +```text +PASS_SL2F3_CONJUGATE_TRIPLE group=24 calls=112 target_minimum=5 pair_words=12544 distinct_pair_states=8905 short_witness=none +``` + +`verify.py --write` regenerates the deterministic coverage certificate after review. Normal replay checks the regenerated result against the committed `CERTIFICATE.json`. The package pins the exact three-register predecessor source and the selected record/catalogue provenance in [SOURCES.json](SOURCES.json). + +## Predecessors, relevance, and limits + +The source result remains the maintainer-reviewed conditional finite construction with `kappa = 836330098538459/500000000000000000`. Its review is [`community-batch1099-review.md`](../../docs/research/community-batch1099-review.md) (SHA-256 `7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb`); the selected source manifest is `research/community-frontier1094-audit/SELECTED-SOURCE.json` (SHA-256 `79b3de5db3dbcb9829789ba58e9e45758926031e2a7d80667a08429d369be53b`); the assembly certificate SHA-256 is `1122cb3a575f8c788345fc1bf4c108ac7c3250fb81a5988671f5eb04b3ab3045`; its recorded reproduction command is `make frontier1094-verify`. This experiment does not use those supplier files, change the selected construction, or alter `kappa`. + +The model descends from the scoped three-register abelian bit result in PR [#468](https://github.com/CrocSwap/integer-mult-bounds/pull/468), which explicitly excludes other address groups. The closest nonabelian predecessors are PR [#1822](https://github.com/CrocSwap/integer-mult-bounds/pull/1822), a Q8 repeated central-commutator pair, and PR [#1925](https://github.com/CrocSwap/integer-mult-bounds/pull/1925), Q8 mixed targets on three and four roles. This package changes the address group to its order-three binary tetrahedral extension and tests a heterogeneous `i,w,w^-1iw` target. It imports no predecessor implementation. + +An eight-call result in the opening claim was narrowed before search to this smallest decisive heterogeneous endpoint, reducing the direct bill to five and the exhaustive saving threshold to four. The updated scope and exact budget are recorded in [Discussion #1999](https://github.com/CrocSwap/integer-mult-bounds/discussions/1999); the mechanism index is [Discussion #1167 comment](https://github.com/CrocSwap/integer-mult-bounds/discussions/1167#discussioncomment-18929640). + +The group elements are treated as unit-cost address labels in this finite model. Their physical realization, source access, compiler, frame conversions, hosting, precision, restoration in a selected supplier, and recursive-moment effect are not priced. The result supplies neither a multiplication construction nor a universal impossibility theorem. It is an exact negative result for one new operation alphabet and endpoint, prepared with substantial OpenAI Codex assistance; no independent human review or proof-assistant formalization is claimed. + +## Open next questions + +Does one arbitrary restored dirty scalar role lower the five-call minimum for this same `SL2(F3)` endpoint? That tests whether workspace sharing helps while keeping the nonabelian target fixed. A first step is to enumerate the four-role rank-one idempotents and screen exact depth-four meet-in-the-middle coverage against the unchanged direct word. The larger `4 x 4` formal matrix states and the missing physical address-operation implementation are the blockers. diff --git a/research/sl2f3-conjugate-triple-seed592f/SOURCES.json b/research/sl2f3-conjugate-triple-seed592f/SOURCES.json new file mode 100644 index 0000000000..c84b038c98 --- /dev/null +++ b/research/sl2f3-conjugate-triple-seed592f/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "1c47876ef742ba64bf9140b0527d63acf656a3b4", + "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/bit-three-register-lower-bound/README.md", + "usage": "input", + "git_blob": "25e41c370c101a33a6deb978de08b03ed7539b79", + "sha256": "c12b33ef388deece0cbf891505a2ce2c0779a0c3a6cf1f0f7f7039bab59cbebd" + } + ] +} diff --git a/research/sl2f3-conjugate-triple-seed592f/TASK.json b/research/sl2f3-conjugate-triple-seed592f/TASK.json new file mode 100644 index 0000000000..cda7539044 --- /dev/null +++ b/research/sl2f3-conjugate-triple-seed592f/TASK.json @@ -0,0 +1,88 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 3, + "base_commit": "1c47876ef742ba64bf9140b0527d63acf656a3b4", + "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": "In M3(F2[SL2(F3)]), with i=[[0,1],[-1,0]] and w=[[0,-1],[1,-1]] over F3, use the four paid address labels i,i^-1,w,w^-1 and all 28 rank-one idempotents N in M3(F2). Determine the exact minimum paid-call count for diag([i],[w],[w^-1 i w]), with free scalar GL3(F2) interleavings allowed, by exhausting every word through depth four and comparing with the direct five-call word.", + "scope_change_reason": "The catalogue explicitly permits a specified nonabelian operation family. This refines that broad option to the order-24 binary tetrahedral group SL2(F3), its four-generator alphabet, and one heterogeneous three-role endpoint so the full search through one call below the direct bill is finite and exactly coverable.", + "bottleneck_link": "A four-call factorization would remove one paid call from this five-call finite bit-register endpoint. The exact minimum is five, so this particular nonabelian extension supplies no saving. The model does not price any selected-supplier source, hosting, or physical address-operation implementation, and no kappa change follows.", + "budget_minutes": 60, + "stop_rule": "Exhaust all words of lengths zero through four over the 112 paid factors in M3(F2[SL2(F3)]), with exact full-coefficient equality, and verify the direct five-call endpoint and controls. Do not expand to a different group, target, or register count in this cycle.", + "outcome": "negative-result", + "evidence": "SL2(F3) has 24 elements and is generated by i,w. There are 28 rank-one idempotents and 112 paid factors. Exact meet-in-the-middle coverage checks every word of lengths 0..4 (112^k raw words at length k): the 12,544 two-call words yield 8,905 distinct exact states, each checked as a suffix for both 1+2 and 2+2 splits. The two-call transition is cross-checked against full group-algebra convolution for all 12,544 pairs. No target hit occurs through four calls; the direct five-call word realizes diag([i],[w],[w^-1 i w]), so the exact minimum is five in this model. Five omitted-call controls, a generator mutation, a two-call positive control, all gate inverses, and all group-table associativity checks pass.", + "author": "Cinna Davis", + "ai_assistance": "Substantial OpenAI Codex assistance in scope refinement, exact algebra/search implementation, verification and writing. No independent human review or proof-assistant formalization is claimed.", + "open_questions": [ + { + "question": "Does one arbitrary restored dirty scalar role lower the five-call minimum for this same SL2(F3) endpoint?", + "why_it_matters": "This tests whether workspace sharing can beat the exact three-role result while preserving the same nonabelian target and paid address alphabet.", + "first_step": "Extend the formal state to four roles, derive the 120 rank-one idempotents and 480 paid factors, then compute the exact two-call state set and screen complete depth-four meet-in-the-middle coverage against the unchanged five-call direct word.", + "blocked_by": "The four-role matrix state is larger, and the exact finite address model still has no priced translation into a selected integer-multiplication supplier." + } + ], + "seed": "592f04c45f93ecfac35ea0ab971b12ba", + "track": "bit-mechanisms", + "scope_key": "d03e83a1b42a1002ba51", + "selector_scope_key": "7084092dd726e7ba1f2f", + "catalogue_revision": 3, + "catalogue_sha256": "6686ad58f1fbdbc87134a78901b60fd53a20d3984355e91defbbebc9e9fa8075", + "selected_record_sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32", + "predecessors": [ + { + "pr": 468, + "scope": "abelian three-register bit model; lower bound at exact base pin in package" + }, + { + "pr": 1822, + "head": "ee736b4b11bbd63b04d94c8edafb3790161ebdea", + "scope": "Q8 repeated central-commutator pair" + }, + { + "pr": 1925, + "head": "009ed860f34ed5d7b0d626098ce93c4c2a7eb4df", + "scope": "Q8 mixed diagonal triples" + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1999", + "claim_update_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1999#discussioncomment-18929639", + "mechanism_index_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1167#discussioncomment-18929640", + "finished_utc": "2026-10-14T16:55:22Z", + "certificate_sha256": "92870cc9c4bb777d816453bcbdfbbae2b3f90e39b95e0358931f2da1d2582f43" +} diff --git a/research/sl2f3-conjugate-triple-seed592f/VERIFY.json b/research/sl2f3-conjugate-triple-seed592f/VERIFY.json new file mode 100644 index 0000000000..a912b350b3 --- /dev/null +++ b/research/sl2f3-conjugate-triple-seed592f/VERIFY.json @@ -0,0 +1,20 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/bit-three-register-lower-bound/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Construct SL2(F3) and all 112 paid gates exactly; exhaust words through four calls by exact meet-in-the-middle in the full group algebra; cross-check all 12,544 two-call products by independent convolution; verify the five-call direct endpoint, a two-call positive control, inverse laws, omitted-call and mutated-generator failures, and the committed state digest." + } + ] +} diff --git a/research/sl2f3-conjugate-triple-seed592f/verify.py b/research/sl2f3-conjugate-triple-seed592f/verify.py new file mode 100644 index 0000000000..e022295c05 --- /dev/null +++ b/research/sl2f3-conjugate-triple-seed592f/verify.py @@ -0,0 +1,415 @@ +#!/usr/bin/env python3 +"""Exact depth-four search in F2[SL2(F3)] for a heterogeneous triple.""" + +from __future__ import annotations + +import argparse +import hashlib +import json +from pathlib import Path + + +ROOT = Path(__file__).resolve().parent +CERTIFICATE = ROOT / "CERTIFICATE.json" + + +def require(condition: bool, message: str) -> None: + if not condition: + raise SystemExit("FAIL_SL2F3_CONJUGATE_TRIPLE: " + message) + + +def mat2_mul(a: tuple[int, ...], b: tuple[int, ...]) -> tuple[int, ...]: + return tuple( + sum(a[2 * r + k] * b[2 * k + c] for k in range(2)) % 3 + for r in range(2) + for c in range(2) + ) + + +def mat2_det(a: tuple[int, ...]) -> int: + return (a[0] * a[3] - a[1] * a[2]) % 3 + + +def build_group(): + elements = sorted( + (a, b, c, d) + for a in range(3) + for b in range(3) + for c in range(3) + for d in range(3) + if (a * d - b * c) % 3 == 1 + ) + index = {g: i for i, g in enumerate(elements)} + identity = index[(1, 0, 0, 1)] + table = tuple( + tuple(index[mat2_mul(a, b)] for b in elements) for a in elements + ) + inverses = tuple( + next(j for j in range(len(elements)) if table[i][j] == identity and table[j][i] == identity) + for i in range(len(elements)) + ) + return elements, index, identity, table, inverses + + +ELEMENTS, GROUP_INDEX, E, GROUP_MUL, GROUP_INV = build_group() +I2 = GROUP_INDEX[(0, 1, 2, 0)] +W = GROUP_INDEX[(0, 2, 1, 2)] +IW = GROUP_INV[W] +C = GROUP_MUL[GROUP_MUL[IW][I2]][W] +GENERATOR_IDS = (I2, GROUP_INV[I2], W, IW) +GENERATOR_NAMES = ("i", "i^-1", "w", "w^-1") + + +def group_power(g: int, n: int) -> int: + out = E + for _ in range(n): + out = GROUP_MUL[out][g] + return out + + +def generator_word_distance(target: int) -> int: + frontier = [E] + seen = {E: 0} + while frontier: + g = frontier.pop(0) + if g == target: + return seen[g] + for h in GENERATOR_IDS: + gh = GROUP_MUL[g][h] + if gh not in seen: + seen[gh] = seen[g] + 1 + frontier.append(gh) + raise RuntimeError("target not generated") + + +def right_translate(mask: int, g: int) -> int: + """Right-multiply a basis support by one group element over F2.""" + out = 0 + while mask: + bit = mask & -mask + a = bit.bit_length() - 1 + out |= 1 << GROUP_MUL[a][g] + mask ^= bit + return out + + +def left_translate(mask: int, g: int) -> int: + """Left-multiply a basis support by one group element over F2.""" + out = 0 + while mask: + bit = mask & -mask + a = bit.bit_length() - 1 + out |= 1 << GROUP_MUL[g][a] + mask ^= bit + return out + + +def identity_state() -> tuple[int, ...]: + one = 1 << E + return tuple(one if r == c else 0 for r in range(3) for c in range(3)) + + +def right_call(state: tuple[int, ...], call: tuple[int, int, int]) -> tuple[int, ...]: + """Return state * (I + ([g]+[e]) x y^T), exactly over F2[G].""" + g, x, y = call + out = list(state) + for r in range(3): + accumulated = 0 + for k in range(3): + if (x >> k) & 1: + accumulated ^= state[3 * r + k] + delta = accumulated ^ right_translate(accumulated, g) + for c in range(3): + if (y >> c) & 1: + out[3 * r + c] ^= delta + return tuple(out) + + +def direct_gate(call: tuple[int, int, int]) -> tuple[int, ...]: + """Construct I+([g]+[e])N entry by entry, independent of right_call.""" + g, x, y = call + one = 1 << E + out = [] + for r in range(3): + for c in range(3): + support = one if r == c else 0 + if ((x >> r) & 1) and ((y >> c) & 1): + support ^= one ^ (1 << g) + out.append(support) + return tuple(out) + + +def convolution(a: int, b: int) -> int: + """Independent full coefficient multiplication in F2[G].""" + out = 0 + aa = a + while aa: + abit = aa & -aa + ga = abit.bit_length() - 1 + bb = b + while bb: + bbit = bb & -bb + gb = bbit.bit_length() - 1 + out ^= 1 << GROUP_MUL[ga][gb] + bb ^= bbit + aa ^= abit + return out + + +def formal_matrix_product(a: tuple[int, ...], b: tuple[int, ...]) -> tuple[int, ...]: + out = [0] * 9 + for r in range(3): + for c in range(3): + value = 0 + for k in range(3): + value ^= convolution(a[3 * r + k], b[3 * k + c]) + out[3 * r + c] = value + return tuple(out) + + +def word_state(calls: tuple[tuple[int, int, int], ...]) -> tuple[int, ...]: + state = identity_state() + for call in calls: + state = right_call(state, call) + return state + + +def target_state(diagonal: tuple[int, int, int]) -> tuple[int, ...]: + out = [0] * 9 + for r, g in enumerate(diagonal): + out[3 * r + r] = 1 << g + return tuple(out) + + +def left_diagonal(state: tuple[int, ...], diagonal: tuple[int, int, int]) -> tuple[int, ...]: + return tuple( + left_translate(state[3 * r + c], diagonal[r]) + for r in range(3) + for c in range(3) + ) + + +def pair_state(a: int, b: int, gates): + return right_call(gates[a], CALLS[b]) + + +def make_calls(): + calls = [] + for g in GENERATOR_IDS: + for x in range(1, 8): + for y in range(1, 8): + dot = sum(((x >> k) & 1) * ((y >> k) & 1) for k in range(3)) & 1 + if dot == 1: + calls.append((g, x, y)) + return tuple(calls) + + +CALLS = make_calls() +CALL_NAMES = {g: name for g, name in zip(GENERATOR_IDS, GENERATOR_NAMES)} + + +def idempotent_name(x: int, y: int) -> str: + def vec(v): + return "".join(str((v >> k) & 1) for k in range(3)) + return f"{vec(x)}*{vec(y)}^T" + + +def call_name(call: tuple[int, int, int]) -> str: + g, x, y = call + return f"D[{CALL_NAMES[g]};{idempotent_name(x, y)}]" + + +def make_direct_word(call_index): + def at(g: int, role: int): + e = 1 << role + return call_index[(g, e, e)] + + return ( + at(I2, 0), + at(W, 1), + at(IW, 2), + at(I2, 2), + at(W, 2), + ) + + +def search_minimum(target: tuple[int, ...], diagonal: tuple[int, int, int], gates, pair_words, call_inverse): + one_words = {gates[i]: (i,) for i in range(len(CALLS))} + if target == identity_state(): + return () + if target in one_words: + return one_words[target] + if target in pair_words: + return pair_words[target] + + # Every three-call word splits 1+2. Every four-call word splits 2+2. + # For a suffix b1 b2, its inverse is b2^-1 b1^-1. + for suffix_state, (a, b) in pair_words.items(): + inv_suffix = pair_state(call_inverse[b], call_inverse[a], gates) + need_prefix = left_diagonal(inv_suffix, diagonal) + if need_prefix in one_words: + return one_words[need_prefix] + (a, b) + + for suffix_state, (a, b) in pair_words.items(): + inv_suffix = pair_state(call_inverse[b], call_inverse[a], gates) + need_prefix = left_diagonal(inv_suffix, diagonal) + if need_prefix in pair_words: + return pair_words[need_prefix] + (a, b) + return None + + +def state_digest(states) -> str: + digest = hashlib.sha256() + for state in sorted(states): + for coefficient_support in state: + digest.update(coefficient_support.to_bytes(3, "little")) + return digest.hexdigest() + + +def controls(gates, call_index, direct, target): + direct_state = word_state(tuple(CALLS[i] for i in direct)) + require(direct_state == target, "direct five-call identity failed") + for pos in range(len(direct)): + reduced = direct[:pos] + direct[pos + 1 :] + require(word_state(tuple(CALLS[i] for i in reduced)) != target, + f"omission control unexpectedly passed at direct position {pos}") + wrong = list(direct) + old = CALLS[wrong[-1]] + wrong[-1] = call_index[(GROUP_INV[old[0]], old[1], old[2])] + require(word_state(tuple(CALLS[i] for i in wrong)) != target, + "mutated-generator control unexpectedly passed") + positive = target_state((I2, W, E)) + positive_word = (call_index[(I2, 1, 1)], call_index[(W, 2, 2)]) + require(word_state(tuple(CALLS[i] for i in positive_word)) == positive, + "two-call positive control failed") + return positive_word + + +def main() -> None: + parser = argparse.ArgumentParser() + parser.add_argument("--write", action="store_true", help="write the deterministic coverage certificate") + args = parser.parse_args() + + require(len(ELEMENTS) == 24, "SL2(F3) must have 24 elements") + require(len(GENERATOR_IDS) == 4 and len(set(GENERATOR_IDS)) == 4, + "the paid address generators must be four distinct elements") + require(len(CALLS) == 112, "expected 4 times 28 paid gates") + require(all(GROUP_MUL[GROUP_MUL[a][b]][c] == GROUP_MUL[a][GROUP_MUL[b][c]] + for a in range(24) for b in range(24) for c in range(24)), + "group multiplication table is not associative") + generated = {E} + frontier = [E] + while frontier: + a = frontier.pop() + for g in GENERATOR_IDS: + b = GROUP_MUL[a][g] + if b not in generated: + generated.add(b) + frontier.append(b) + require(len(generated) == 24, "i and w do not generate all of SL2(F3)") + require(group_power(I2, 4) == E and group_power(I2, 2) != E, + "i must have order four") + require(group_power(W, 3) == E and W != E, + "w must have order three") + require(group_power(C, 4) == E and group_power(C, 2) != E, + "c must have order four") + require(generator_word_distance(C) == 3, "the stated three-letter direct word is not shortest") + + gates = tuple(right_call(identity_state(), call) for call in CALLS) + require(all(gates[i] == direct_gate(call) for i, call in enumerate(CALLS)), + "rank-one update and direct gate construction disagree") + call_index = {call: i for i, call in enumerate(CALLS)} + call_inverse = tuple( + call_index[(GROUP_INV[g], x, y)] for g, x, y in CALLS + ) + identity = identity_state() + for k, gate in enumerate(gates): + require(right_call(gate, CALLS[call_inverse[k]]) == identity, + f"inverse formula failed for {call_name(CALLS[k])}") + + target_diagonal = (I2, W, C) + target = target_state(target_diagonal) + direct = make_direct_word(call_index) + positive_word = controls(gates, call_index, direct, target) + + pair_words = {} + for a, gate in enumerate(gates): + for b, call in enumerate(CALLS): + state = right_call(gate, call) + require(state == formal_matrix_product(gate, gates[b]), + f"rank-one transition disagrees with full convolution at pair ({a},{b})") + pair_words.setdefault(state, (a, b)) + + found = search_minimum(target, target_diagonal, gates, pair_words, call_inverse) + if found is None: + minimum = 5 # The exact search excludes lengths 0..4; direct word attains 5. + witness = direct + else: + minimum = len(found) + witness = found + require(word_state(tuple(CALLS[i] for i in witness)) == target, + "reported short witness fails full group-algebra replay") + require(minimum <= 5, "direct word did not bound the exact minimum") + + positive_pairs = {} + for a, gate in enumerate(gates): + for b, call in enumerate(CALLS): + positive_pairs.setdefault(right_call(gate, call), (a, b)) + positive_target = target_state((I2, W, E)) + positive_minimum = search_minimum( + positive_target, (I2, W, E), gates, positive_pairs, call_inverse + ) + require(positive_minimum is not None and len(positive_minimum) == 2 + and word_state(tuple(CALLS[i] for i in positive_minimum)) == positive_target, + "search failed its known two-call positive control") + + cert = { + "schema_version": 1, + "model": "M3(F2[SL2(F3)])", + "group_order": len(ELEMENTS), + "group_generated_by": ["i", "i^-1", "w", "w^-1"], + "i_matrix_mod3": [[0, 1], [2, 0]], + "w_matrix_mod3": [[0, 2], [1, 2]], + "target_c": "w^-1*i*w", + "target_diagonal": ["i", "w", "c"], + "rank_one_idempotents": 28, + "paid_call_alphabet": len(CALLS), + "direct_paid_bill": 5, + "search_depth": 4, + "one_call_states": len(set(gates)), + "two_call_words": len(CALLS) ** 2, + "two_call_distinct_states": len(pair_words), + "two_call_full_convolution_cross_checks": len(CALLS) ** 2, + "two_call_state_sha256": state_digest(pair_words), + "result_minimum": minimum, + "short_witness_indices": list(witness) if len(witness) <= 4 else None, + "short_witness": [call_name(CALLS[i]) for i in witness] if len(witness) <= 4 else None, + "positive_control_minimum": len(positive_minimum), + "direct_word": [call_name(CALLS[i]) for i in direct], + "omission_controls": len(direct), + "mutated_generator_control": True, + "free_scalar_mixing_covered": True, + "limitations": [ + "finite nonabelian address algebra only", + "address-operation implementation cost not priced", + "no selected supplier or kappa change claimed", + ], + } + + if args.write: + CERTIFICATE.write_text(json.dumps(cert, indent=2, sort_keys=True) + "\n", encoding="utf-8") + else: + require(CERTIFICATE.exists(), "missing CERTIFICATE.json; run verify.py --write after review") + expected = json.loads(CERTIFICATE.read_text(encoding="utf-8")) + require(cert == expected, "recomputed certificate differs from CERTIFICATE.json") + + print( + "PASS_SL2F3_CONJUGATE_TRIPLE " + f"group=24 calls={len(CALLS)} target_minimum={minimum} " + f"pair_words={len(CALLS)**2} distinct_pair_states={len(pair_words)} " + f"short_witness={'yes' if len(witness) <= 4 else 'none'}" + ) + + +if __name__ == "__main__": + main()