From 2f98b7ec3e092e1299a9190af6ae45372497137f Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 23 Oct 2026 12:48:07 +0100 Subject: [PATCH] feat(research): certify the ternary quaternion pair minimum --- research/ternary-q8-negative-pair/README.md | 179 +++++++++++++++ research/ternary-q8-negative-pair/RESULT.json | 140 +++++++++++ .../ternary-q8-negative-pair/SOURCES.json | 30 +++ research/ternary-q8-negative-pair/TASK.json | 70 ++++++ research/ternary-q8-negative-pair/VERIFY.json | 59 +++++ research/ternary-q8-negative-pair/regular.py | 131 +++++++++++ research/ternary-q8-negative-pair/verify.py | 217 ++++++++++++++++++ 7 files changed, 826 insertions(+) create mode 100644 research/ternary-q8-negative-pair/README.md create mode 100644 research/ternary-q8-negative-pair/RESULT.json create mode 100644 research/ternary-q8-negative-pair/SOURCES.json create mode 100644 research/ternary-q8-negative-pair/TASK.json create mode 100644 research/ternary-q8-negative-pair/VERIFY.json create mode 100644 research/ternary-q8-negative-pair/regular.py create mode 100644 research/ternary-q8-negative-pair/verify.py diff --git a/research/ternary-q8-negative-pair/README.md b/research/ternary-q8-negative-pair/README.md new file mode 100644 index 0000000000..c9d67c1eb7 --- /dev/null +++ b/research/ternary-q8-negative-pair/README.md @@ -0,0 +1,179 @@ +# The ternary quaternion negative pair costs exactly six calls + +This finite exact certificate establishes the minimum **six** for +`diag([i^-1],[j^-1])` in the full formal algebra `F3[Q8]`, with exactly two +arbitrary dirty roles, positive paid labels `i,j`, all ternary rank-one +idempotent couplings, and arbitrary free `GL2(F3)` scalar mixing. Changing +the scalar field from F2 to F3 supplies no sharing gain for this endpoint. +No new kappa or selected-frontier change is claimed. + +This contribution was produced by Nick Petalas. Independent human and +formal proof-kernel review are unclaimed. New work is Apache-2.0. + +## Model and exact conclusion + +Write `Q8={1,z,i,zi,j,zj,k,zk}`, where `i^2=j^2=z`, `z^2=1`, `ij=k` and +`ji=zk`. These are eight independent formal basis elements over F3. In +particular `[zi]` is not the coefficient multiple `2[i]`. + +A charged factor is + +```text +D_N(g) = I_2 + ([g]-[1])N, +g in {i,j}, N in M_2(F3), rank(N)=1, N^2=N. +``` + +All input values are independent and arbitrary. The complete endpoint is +equality in `M_2(F3[Q8])`, including both zero off-diagonal blocks. No extra +role, free address permutation, erasure, clean allocation or nonlinear scalar +operation is part of this model. Scalar `GL2(F3)` operations alone are free. + +The result is an exact finite minimum, not a failed search extrapolated to +other fields, role counts or endpoints. The binary endpoint was already +settled by Aaron Wang's [#2318](https://github.com/CrocSwap/integer-mult-bounds/pull/2318). +The new quantity is the minimum with ternary coefficients and all twelve +ternary projectors. Its value agrees with that cited binary value; +the binary census is not replayed here. + +## Why the certificate proves a minimum + +**Normalize free scalar mixing.** Augmentation sends every group basis +element to 1, so every charged factor and the target augment to `I_2`. +Moving all free scalar maps to the left conjugates each N by a scalar +invertible matrix and preserves its rank and idempotence. The remaining +scalar product must be `I_2` by augmentation. Thus every legal presentation +has a same-length charged-only presentation in the enumerated alphabet. +This is the predecessor normalization argument over the changed field. + +**The alphabet is complete.** The primary checker enumerates all 81 ternary +two-by-two matrices, retaining exactly those with determinant zero, trace +one and `N^2=N`. These are precisely the rank-one idempotents. The separate +checker enumerates all outer products `uv^T` with `v^T u=1` and deduplicates +them. Both obtain twelve projectors, hence 24 charged factors. The primary +checker also verifies conjugation closure under all 48 scalar invertibles. + +**Every candidate below six has even length.** Apply the group character +`i -> -1, j -> 1` and then the ordinary two-by-two determinant over F3. +For a rank-one projector, + +```text +det(I_2 + (c-1)N) = c. +``` + +The target character has determinant -1. Consequently the number of i +calls is odd. The character `i -> 1, j -> -1` likewise forces an odd number +of j calls. Both characters send z to 1. Hence the total length is even; +it is enough to exclude lengths zero, two and four. Interleaved free scalar +maps have already been normalized away. + +**The complete four-call meet is empty.** Starting at identity, enumerate +all products through two charged calls. Starting at the target, enumerate +all products through two inverse factors. Both breadth-first searches have +new-state layers `(1,24,466)`, total 491 states, from exactly 600 transitions +each. Their intersection is empty. Every word of length at most four splits +into two parts of lengths at most two and would produce an intersection. +Deduplicating equal full matrices loses no continuation because future +left multiplication depends only on the current matrix. + +The reverse factors are `D_N(g^-1)` because +`D_N(g^-1)D_N(g)=I_2`. They undo charged calls in the meet; +they do not enlarge the paid operation alphabet. + +**Six calls attain the endpoint.** Let `E_1=diag(1,0)` and `E_2=diag(0,1)`. +Three i calls on `E_1`, followed by three j calls on `E_2`, give + +```text +D_E2(j)^3 D_E1(i)^3 = diag([i^3],[j^3]) = diag([zi],[zj]). +``` + +This identity holds in the full formal algebra. It acts correctly on every +dirty input, with no preparation or cleanup omitted. Together with parity +and the exhaustive meet, it gives minimum six. + +## Reproduce and evidence + +Use CPython 3.12 and the standard library, from the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/ternary-q8-negative-pair/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/ternary-q8-negative-pair/regular.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/ternary-q8-negative-pair +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/ternary-q8-negative-pair --check-source-history +``` + +Any CPython 3.12 installation can replace the displayed interpreter path. +`VERIFY.json` registers ordinary and optimized runs of both checkers. Each +command is read-only. The expected scientific markers are +`PASS_TERNARY_Q8_NEGATIVE_PAIR` and `PASS_TERNARY_Q8_REGULAR_ACTION`. + +`verify.py` stores all 32 formal coefficients directly. `regular.py` imports +no producer code. It independently constructs the group using Hamilton +quaternions, the projectors using outer products, and all factors as dense +16-by-16 matrices in the faithful regular action over F3. The complete two +forward/reverse sets agree after recovering formal coefficients from the +identity-input columns. The regular action is faithful as an algebra action; +a smaller faithful group representation would not suffice for this check. +These are two arithmetic implementations in one contribution, not independent +human review. + +Both checkers verify the six-call witness, reject each of its six single-call +omissions and find a planted four-call target with the same meet routine. +The primary checker additionally checks all 512 associativity triples, gate +inverses and determinant characters, rejects invalid projectors and labels, +and distinguishes dirty off-diagonal leakage and group sign from scalar minus. + +The generated `RESULT.json` records full-set digests, counts, the witness and +SHA256 hashes of the other six package files. Default replay recomputes it +and rejects a mismatch, including Boolean aliases for integers and duplicate +JSON keys. Explicit `verify.py --emit` prints a fresh generated receipt for +comparison; it writes no files. Source manifests are historical provenance, +not executable dependencies. No predecessor verifier is imported or replayed. + +The fixed-domain Python programs use managed allocation, a Power of Ten rule +3 deviation. Each formal state has 32 coefficients and each regular state +has 256 entries. Each search retains at most 601 states and at most 576 +next-layer candidates; all loops have fixed bounds or iterate bounded package +data. Functions are under 60 physical lines, control flow is nonrecursive, +and failures use explicit exceptions that remain active under `-O`. +The compensating control is the fixed field, role count and search radius; +expanding any of them requires new capacity limits and a separate task. +Warnings-as-errors replay is the registered Python diagnostic check. + +## Scope, overlap and credit + +Base `a5df48c55ea806d7952b65acc9c76d878ff09b13`, priority revision 7. +The `bit-new-register-model` card is changed to a coefficient-field side +question. Its historical binary baseline is not the first working example +for this field; the six-call ternary coordinate word is the first fixture. +`TASK.json` records the changed premise and the stop at this first result. + +[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19144877). +Live PRs, active Discussions and recent handoffs, this account's recent +contributions, distinctive all-main README searches and merged-PR searches +were checked. The cached helper covered 331 open PRs and 4,359 Discussion +records, with incomplete sparse local-note coverage. Arbitrary diffs and +unpublished work remain outside coverage; no-match searches prove no novelty. + +Credit Aaron Wang's #1822/#2318 for the Q8 pair model, binary precedents, +full-boundary convention and exact-search direction; eumemic #288 for the +scalar-idempotent register model; woklerx #1443 for the formal group-algebra +and normalization predecessor; Ali Romman #468, Gareth Davidson #1333 and +the retained register-model lineage. The twelve-projector enumeration and +ternary endpoint certificate here are new. No historical priority is claimed +for determinant characters or meet-in-the-middle enumeration. + +Physical ternary address realization, scalar-map charges, source access, +restoration, frame/hosting, precision, tape, stock, recursive supplier +admission and the complete multiplication theorem remain outside scope. +Lean, Docker, predecessor scientific replays and the selected cold replay +are unrun. None of these unknown costs is treated as zero in a physical bill. + +## Open next questions + +1. Does the same six-call minimum hold with an arbitrary number of restored + dirty ternary roles? Start with a role-uniform invariant or a three-role + exact word. The two-role meet supplies no extra-role lower bound. +2. Can a written argument exclude four calls over every odd field? The + determinant parity proof survives, but the projector inventory changes. + Start with the forced label counts `(1,3)` and `(3,1)` and retain all eight + formal group coefficients. No general-field exclusion is claimed here. diff --git a/research/ternary-q8-negative-pair/RESULT.json b/research/ternary-q8-negative-pair/RESULT.json new file mode 100644 index 0000000000..90ef990e48 --- /dev/null +++ b/research/ternary-q8-negative-pair/RESULT.json @@ -0,0 +1,140 @@ +{ + "schema_version": 1, + "field": 3, + "roles": 2, + "exact_minimum": 6, + "group_basis": [ + "1", + "z", + "i", + "zi", + "j", + "zj", + "k", + "zk" + ], + "target_indices": [ + 3, + 5 + ], + "projectors": [ + [ + 0, + 0, + 0, + 1 + ], + [ + 0, + 0, + 1, + 1 + ], + [ + 0, + 0, + 2, + 1 + ], + [ + 0, + 1, + 0, + 1 + ], + [ + 0, + 2, + 0, + 1 + ], + [ + 1, + 0, + 0, + 0 + ], + [ + 1, + 0, + 1, + 0 + ], + [ + 1, + 0, + 2, + 0 + ], + [ + 1, + 1, + 0, + 0 + ], + [ + 1, + 2, + 0, + 0 + ], + [ + 2, + 1, + 1, + 2 + ], + [ + 2, + 2, + 2, + 2 + ] + ], + "paid_factors": 24, + "forward_layers": [ + 1, + 24, + 466 + ], + "reverse_layers": [ + 1, + 24, + 466 + ], + "forward_transitions": 600, + "reverse_transitions": 600, + "forward_sha256": "0b670842ad89b3a2710529da060da32adafe244cfe570c5eb41acd76219a322a", + "reverse_sha256": "917083ec84edd4422d8ec7cb674bcb66c62c23a92724c277964d775239974655", + "meet_intersections": 0, + "attaining_word_indices": [ + 10, + 10, + 10, + 1, + 1, + 1 + ], + "algebra_checks": { + "associativity_triples": 512, + "scalar_invertibles": 48, + "scalar_conjugations": 576, + "factor_inverse_checks": 24, + "factor_character_checks": 48 + }, + "controls": { + "omission_rejections": 6, + "planted_four_call_meet": true, + "dirty_leak_rejection": true, + "group_sign_control": true, + "invalid_factor_rejections": 3 + }, + "source_sha256": { + "README.md": "fc845b053d6ac8d54d6630d02b9b17e163e02de61fbcb6d57b07ee0794f17398", + "TASK.json": "171102f705b8e893558d2ae6b5cbf61d4454e1e1d5c87bf1ae7f698ed8afa5ce", + "SOURCES.json": "569f268cc252c778db4c11d45754d3f0e45151f91bc019f657920aa58bafc77d", + "VERIFY.json": "3f5fcaebd5834ed6444e8c1e4d146ccdc6f826b1969db535ca43fa113fb9aafa", + "verify.py": "e3b14984c20954a0cb51d9bb87fd5776923c827ae544858b5ddcf28b0599ff12", + "regular.py": "af761e038f90a197f2fca4af9e9051733413ccbf5d41f003979edcca502d6181" + } +} diff --git a/research/ternary-q8-negative-pair/SOURCES.json b/research/ternary-q8-negative-pair/SOURCES.json new file mode 100644 index 0000000000..be7b7d1818 --- /dev/null +++ b/research/ternary-q8-negative-pair/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13", + "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/q8-central-commutator-pair/README.md", + "usage": "provenance", + "git_blob": "7a6277dc860ea5440ab39b06160c337f93353357", + "sha256": "ee819ee843e1a93d7d320d02ccd5f47af0d912295de9d9c379ccc22c90093948" + }, + { + "path": "research/q8-inverse-label-pair-census/README.md", + "usage": "provenance", + "git_blob": "9d7ce15b9605e817d26b69f8548cf4dba29dcc50", + "sha256": "7dcea87a46b0a0baa76fa86794bcee8cfdb820f08c84628b16230fdb482cc15e" + } + ] +} diff --git a/research/ternary-q8-negative-pair/TASK.json b/research/ternary-q8-negative-pair/TASK.json new file mode 100644 index 0000000000..b07b287aa4 --- /dev/null +++ b/research/ternary-q8-negative-pair/TASK.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 7, + "base_commit": "a5df48c55ea806d7952b65acc9c76d878ff09b13", + "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 six-call minimum for diag([i^-1],[j^-1]) over formal F3[Q8], exactly two dirty roles, ternary rank-one idempotents and free GL2(F3) scalar mixing.", + "scope_change_reason": "The card suggests changing the register model. This result instead changes the scalar field in the credited binary Q8 model and computes one previously unreported ternary minimum.", + "bottleneck_link": "A coefficient-field change must be tested before importing binary no-sharing barriers. This finite side result excludes a saving at this one ternary endpoint, without admitting any supplier.", + "budget_minutes": 60, + "stop_rule": "Stop after the first exact original minimum; package the finite meet, parity argument and attaining word. Do not extend to other targets or fields.", + "outcome": "completed", + "evidence": "README.md argument; verify.py formal meet; regular.py separate regular-action meet; generated RESULT.json", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does the minimum survive arbitrary restored dirty ternary roles?", + "why_it_matters": "Two-role exclusions do not bar workspace sharing.", + "first_step": "Derive a role-uniform invariant or test a complete three-role formal word.", + "blocked_by": "No invariant replacing the two-role exhaustive meet." + }, + { + "question": "Does every odd coefficient field have the same minimum?", + "why_it_matters": "The scalar field changes the legal projector family.", + "first_step": "Analyze the forced four-call label counts (1,3) and (3,1).", + "blocked_by": "No field-uniform four-call exclusion is supplied." + } + ] +} diff --git a/research/ternary-q8-negative-pair/VERIFY.json b/research/ternary-q8-negative-pair/VERIFY.json new file mode 100644 index 0000000000..147d26b434 --- /dev/null +++ b/research/ternary-q8-negative-pair/VERIFY.json @@ -0,0 +1,59 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Full ternary formal-coefficient meet, parity fixtures, endpoint, controls and authenticated receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Full ternary formal-coefficient meet, parity fixtures, endpoint, controls and authenticated receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/regular.py" + ], + "timeout_seconds": 60, + "checks": "Separate Hamilton regular-action meet, full-set agreement, planted hit and omissions." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/regular.py" + ], + "timeout_seconds": 60, + "checks": "Separate Hamilton regular-action meet, full-set agreement, planted hit and omissions." + } + ] +} diff --git a/research/ternary-q8-negative-pair/regular.py b/research/ternary-q8-negative-pair/regular.py new file mode 100644 index 0000000000..67fafdb982 --- /dev/null +++ b/research/ternary-q8-negative-pair/regular.py @@ -0,0 +1,131 @@ +#!/usr/bin/env python3 +"""Separate dense regular-action enumeration, with no producer imports. Apache-2.0.""" + +import hashlib +import itertools +import json +from pathlib import Path + +ROOT = Path(__file__).resolve().parent +BASIS = tuple(tuple(sign if a == b else 0 for a in range(4)) + for b in range(4) for sign in (1, -1)) + + +def check(ok, message): + if not ok: + raise ValueError(message) + + +def hamilton(u, v): + a, b, c, d = u + e, f, g, h = v + return (a*e-b*f-c*g-d*h, a*f+b*e+c*h-d*g, + a*g-b*h+c*e+d*f, a*h+b*g-c*f+d*e) + + +def multiply(a, b): + out = [0] * 256 + for i in range(16): + for k in range(16): + value = a[16*i+k] + if value: + for j in range(16): + out[16*i+j] += value * b[16*k+j] + return bytes(x % 3 for x in out) + + +def diagonal(a, b): + out = [0] * 256 + for role, group in enumerate((a, b)): + for address in range(8): + image = BASIS.index(hamilton(BASIS[group], BASIS[address])) + out[16*(8*role+image)+8*role+address] = 1 + return bytes(out) + + +def projectors(): + found = set() + for u, v in itertools.product(itertools.product(range(3), repeat=2), repeat=2): + if sum(x*y for x, y in zip(u, v)) % 3 == 1: + found.add(tuple(x*y % 3 for x in u for y in v)) + check(len(found) == 12, "outer-product projector inventory") + return sorted(found) + + +def factor(p, group): + out = [int(i == j) for i in range(16) for j in range(16)] + for r, s, address in itertools.product(range(2), range(2), range(8)): + image = BASIS.index(hamilton(BASIS[group], BASIS[address])) + out[16*(8*r+image)+8*s+address] += p[2*r+s] + out[16*(8*r+address)+8*s+address] -= p[2*r+s] + return bytes(x % 3 for x in out) + + +def search(start, gates): + seen, frontier = {start}, {start} + layers, transitions = [1], 0 + for _depth in range(2): + following = set() + for value in frontier: + for gate in gates: + following.add(multiply(gate, value)) + transitions += 1 + following.difference_update(seen) + layers.append(len(following)) + seen.update(following) + frontier = following + check(len(seen) <= 601, "search capacity") + return seen, layers, transitions + + +def coefficient_digest(states): + # The two identity-input columns recover all formal coefficients. + payloads = [] + for state in states: + payloads.append(bytes(state[16*(8*r+h)+8*s] + for r in range(2) for s in range(2) for h in range(8))) + check(len(set(payloads)) == len(states), "regular-action coefficient injectivity") + return hashlib.sha256(b"".join(sorted(payloads))).hexdigest() + + +def main(): + certificate = json.loads((ROOT / "RESULT.json").read_text()) + ps = projectors() + gates = [factor(p, g) for p in ps for g in (2, 4)] + inverses = [factor(p, g) for p in ps for g in (3, 5)] + identity, target = diagonal(0, 0), diagonal(3, 5) + for gate, inverse in zip(gates, inverses): + check(multiply(gate, inverse) == identity, "literal gate inverse") + forward, fs, ft = search(identity, gates) + backward, bs, bt = search(target, inverses) + check(not forward & backward, "dense shorter word found") + check(fs == bs == [1, 24, 466], "dense layer counts") + check(fs == certificate["forward_layers"] and bs == certificate["reverse_layers"], + "producer layer disagreement") + check(ft == bt == 600, "dense transition counts") + check(coefficient_digest(forward) == certificate["forward_sha256"], "forward set") + check(coefficient_digest(backward) == certificate["reverse_sha256"], "reverse set") + word = [factor((1, 0, 0, 0), 2)]*3 + [factor((0, 0, 0, 1), 4)]*3 + state = identity + for gate in word: + state = multiply(gate, state) + check(state == target, "dense attaining word") + for removed in range(6): + state = identity + for position, gate in enumerate(word): + if position != removed: + state = multiply(gate, state) + check(state != target, "dense omission") + planted = identity + for gate in word[:4]: + planted = multiply(gate, planted) + planted_reverse, _, _ = search(planted, inverses) + check(bool(forward & planted_reverse), "dense planted hit missed") + check(certificate["exact_minimum"] == 6 and certificate["meet_intersections"] == 0, + "certificate conclusion") + print("PASS_TERNARY_Q8_REGULAR_ACTION matrices=982 transitions=1200 " + "minimum=6 planted_hit=1 omissions=6 no_new_kappa") + + +if __name__ == "__main__": + main() diff --git a/research/ternary-q8-negative-pair/verify.py b/research/ternary-q8-negative-pair/verify.py new file mode 100644 index 0000000000..b96cc29ab0 --- /dev/null +++ b/research/ternary-q8-negative-pair/verify.py @@ -0,0 +1,217 @@ +#!/usr/bin/env python3 +"""Exact ternary quaternion pair certificate. Apache-2.0.""" + +import argparse +import hashlib +import itertools +import json +from pathlib import Path + +ROOT = Path(__file__).resolve().parent +SOURCE_NAMES = ( + "README.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py", "regular.py" +) +# Group basis: 1,z,i,zi,j,zj,k,zk. This sign is a group coordinate. +AXIS = ((0, 1, 2, 3), (1, 0, 3, 2), (2, 3, 0, 1), (3, 2, 1, 0)) +NEG = ((0, 0, 0, 0), (0, 1, 0, 1), (0, 1, 1, 0), (0, 0, 1, 1)) + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def group_product(a, b): + x, y = a // 2, b // 2 + return 2 * AXIS[x][y] + (a % 2 + b % 2 + NEG[x][y]) % 2 + + +TABLE = tuple(tuple(group_product(a, b) for b in range(8)) for a in range(8)) + + +def scalar_product(a, b): + return tuple( + sum(a[2 * i + k] * b[2 * k + j] for k in range(2)) % 3 + for i in range(2) for j in range(2) + ) + + +def determinant(p): + return (p[0] * p[3] - p[1] * p[2]) % 3 + + +def is_projector(p): + return (len(p) == 4 and all(type(x) is int and 0 <= x < 3 for x in p) + and (p[0] + p[3]) % 3 == 1 and determinant(p) == 0 + and scalar_product(p, p) == p) + + +def endpoint(a, b): + out = [0] * 32 + out[a] = out[24 + b] = 1 + return bytes(out) + + +def apply_factor(matrix, p, label): + """Left multiply by I+([label]-[1])p, retaining every formal coefficient.""" + require(len(matrix) == 32 and all(x < 3 for x in matrix), "bad matrix") + require(is_projector(p) and label in (2, 3, 4, 5), "bad factor") + out = list(matrix) + for i, j, k in itertools.product(range(2), repeat=3): + c = p[2 * i + k] + if c: + for h in range(8): + source = (2 * k + j) * 8 + h + out[(2 * i + j) * 8 + h] -= c * matrix[source] + out[(2 * i + j) * 8 + TABLE[label][h]] += c * matrix[source] + return bytes(value % 3 for value in out) + + +def ball(start, factors, inverse=False): + seen, frontier = {start: ()}, {start: ()} + sizes, transitions = [1], 0 + for _depth in range(2): + following = {} + for matrix, word in frontier.items(): + for index, (p, label) in enumerate(factors): + value = apply_factor(matrix, p, label + 1 if inverse else label) + transitions += 1 + if value not in seen and value not in following: + following[value] = word + (index,) + sizes.append(len(following)) + seen.update(following) + frontier = following + require(len(seen) <= 1 + 24 + 24**2, "ball capacity exceeded") + return seen, sizes, transitions + + +def digest(states): + return hashlib.sha256(b"".join(sorted(states))).hexdigest() + + +def evaluate(word, factors): + value = endpoint(0, 0) + for index in word: + require(0 <= index < len(factors), "invalid word index") + value = apply_factor(value, *factors[index]) + return value + + +def character_matrix(matrix, which): + weights = (1, 1, 2, 2, 1, 1, 2, 2) if which == 0 else ( + 1, 1, 1, 1, 2, 2, 2, 2) + return tuple(sum(matrix[8 * e + h] * weights[h] for h in range(8)) % 3 + for e in range(4)) + + +def algebra_checks(projectors, factors): + for a, b, c in itertools.product(range(8), repeat=3): + require(TABLE[TABLE[a][b]][c] == TABLE[a][TABLE[b][c]], "associativity") + require(TABLE[2][2] == TABLE[4][4] == 1, "generator squares") + require(TABLE[2][4] == 6 and TABLE[4][2] == 7, "noncommuting order") + invertibles = [s for s in itertools.product(range(3), repeat=4) if determinant(s)] + closure = 0 + for s in invertibles: + invdet = determinant(s) + si = tuple(invdet * x % 3 for x in (s[3], -s[1], -s[2], s[0])) + require(scalar_product(s, si) == (1, 0, 0, 1), "scalar inverse") + for p in projectors: + require(scalar_product(scalar_product(s, p), si) in projectors, "closure") + closure += 1 + identity = endpoint(0, 0) + for p, label in factors: + value = apply_factor(identity, p, label) + require(apply_factor(value, p, label + 1) == identity, "inverse factor") + for which in range(2): + expected = 2 if label == (2, 4)[which] else 1 + require(determinant(character_matrix(value, which)) == expected, "character") + return {"associativity_triples": 512, "scalar_invertibles": len(invertibles), + "scalar_conjugations": closure, "factor_inverse_checks": len(factors), + "factor_character_checks": 2 * len(factors)} + + +def controls(factors, word, target): + omissions = 0 + for index in range(len(word)): + require(evaluate(word[:index] + word[index + 1:], factors) != target, "omission") + omissions += 1 + planted = evaluate(word[:4], factors) + forward, _, _ = ball(endpoint(0, 0), factors) + reverse, _, _ = ball(planted, factors, inverse=True) + require(bool(forward.keys() & reverse.keys()), "planted meet missed") + leak = bytearray(target) + leak[16] = 1 + require(bytes(leak) != target and leak[:8] == target[:8] + and leak[24:] == target[24:], "dirty off-diagonal control") + wrong = bytearray(32) + wrong[2] = wrong[28] = 2 + require(bytes(wrong) != target, "group inverse confused with scalar minus") + require(character_matrix(target, 0) == (2, 0, 0, 1), "first target character") + require(character_matrix(target, 1) == (1, 0, 0, 2), "second target character") + require(character_matrix(endpoint(0, 0), 0) != character_matrix(target, 0), "parity") + rejected = 0 + for p, g in (((0, 1, 0, 0), 2), ((1, 0, 0, 1), 2), ((1, 0, 0, 0), 0)): + try: + apply_factor(target, p, g) + except ValueError: + rejected += 1 + require(rejected == 3, "invalid factors admitted") + return {"omission_rejections": omissions, "planted_four_call_meet": True, + "dirty_leak_rejection": True, "group_sign_control": True, + "invalid_factor_rejections": rejected} + + +def compute(): + projectors = tuple(p for p in itertools.product(range(3), repeat=4) if is_projector(p)) + require(len(projectors) == 12, "incomplete projector set") + factors = tuple((p, g) for p in projectors for g in (2, 4)) + target = endpoint(3, 5) + forward, fs, ft = ball(endpoint(0, 0), factors) + backward, bs, bt = ball(target, factors, inverse=True) + require(not forward.keys() & backward.keys(), "shorter word found") + word = (factors.index(((1, 0, 0, 0), 2)),) * 3 + ( + factors.index(((0, 0, 0, 1), 4)),) * 3 + require(evaluate(word, factors) == target, "six-call endpoint") + return { + "schema_version": 1, "field": 3, "roles": 2, "exact_minimum": 6, + "group_basis": ["1", "z", "i", "zi", "j", "zj", "k", "zk"], + "target_indices": [3, 5], "projectors": projectors, "paid_factors": 24, + "forward_layers": fs, "reverse_layers": bs, + "forward_transitions": ft, "reverse_transitions": bt, + "forward_sha256": digest(forward), "reverse_sha256": digest(backward), + "meet_intersections": 0, "attaining_word_indices": word, + "algebra_checks": algebra_checks(projectors, factors), + "controls": controls(factors, word, target), + "source_sha256": {name: hashlib.sha256((ROOT / name).read_bytes()).hexdigest() + for name in SOURCE_NAMES}, + } + + +def unique_object(pairs): + result = {} + for key, value in pairs: + require(key not in result, "duplicate JSON key") + result[key] = value + return result + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", action="store_true", help="print a generated receipt") + args = parser.parse_args() + actual = compute() + if args.emit: + print(json.dumps(actual, indent=2) + "\n", end="") + return + expected = json.loads((ROOT / "RESULT.json").read_text(), object_pairs_hook=unique_object) + require(canonical(actual) == canonical(expected), "receipt differs from recomputation") + print("PASS_TERNARY_Q8_NEGATIVE_PAIR minimum=6 projectors=12 " + "forward=491 reverse=491 intersections=0 no_new_kappa") + + +if __name__ == "__main__": + main()