From 6354da68f7a78b9e4db91c796476ae9ebae89a86 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 22 Oct 2026 21:21:13 +0100 Subject: [PATCH] feat(research): count the ternary right-vector threshold population --- .../ternary-product-threshold-count/PROOF.md | 111 ++++++++++ .../ternary-product-threshold-count/README.md | 112 ++++++++++ .../SOURCES.json | 36 ++++ .../ternary-product-threshold-count/TASK.json | 89 ++++++++ .../VERIFY.json | 34 ++++ .../ternary-product-threshold-count/verify.py | 191 ++++++++++++++++++ 6 files changed, 573 insertions(+) create mode 100644 research/ternary-product-threshold-count/PROOF.md create mode 100644 research/ternary-product-threshold-count/README.md create mode 100644 research/ternary-product-threshold-count/SOURCES.json create mode 100644 research/ternary-product-threshold-count/TASK.json create mode 100644 research/ternary-product-threshold-count/VERIFY.json create mode 100644 research/ternary-product-threshold-count/verify.py diff --git a/research/ternary-product-threshold-count/PROOF.md b/research/ternary-product-threshold-count/PROOF.md new file mode 100644 index 0000000000..14ededd81c --- /dev/null +++ b/research/ternary-product-threshold-count/PROOF.md @@ -0,0 +1,111 @@ +# The ternary threshold population + +## Statement and cited input + +Let K=F3 and R=K^4. A target has two roles and four invertible +components M_i in GL_2(K). Paid factors are I+u y^T with u in R^2 and +y in K^2. Common GL_2(K) maps are free anywhere. Components and their +order are distinguished; scalar multiples are different matrix targets. + +Exactly 9,216 of the 48^4=5,308,416 targets have paid cost three. +The exact fraction is 1/576. The corresponding unordered sets of four +projective actions are precisely the left cosets of the regular C4 and +V4 subgroups of S4. Eighteen cosets have cyclic type and six have Klein +type, giving respectively 6,912 and 2,304 ordered matrix targets. + +This is a new counting consequence of ToikY's field-product theorem in +[PR #4334](https://github.com/CrocSwap/integer-mult-bounds/pull/4334), +retained at the source pinned in SOURCES.json. Sections 2 and 3 there +are cited inputs: + +* cost is at most two exactly when some nonzero common row phi and + column t satisfy phi M_i t != 0 for every component; +* every invertible field-product target costs at most three. + +Those statements and their proof are not reverified here. They follow +the low-factor criteria of Nick Petalas #4276 and the alphabet of +Wentao Li #4099 following #2513. The count below is in that exact model. + +## 1. Reduction to four permutations + +The projective input lines are represented by (1,0), (0,1), (1,1), (1,2). +For each nonzero vector M_i t there is exactly one projective row phi +annihilating it. Thus the cited criterion fails exactly when, for every +input line T, the four output lines M_i T cover all four projective lines. +The upper bound then makes the cost exactly three. + +GL_2(F3) has (3^2-1)(3^2-3)=48 elements. Its action on these four lines +has kernel {I,-I}. Indeed, fixing the coordinate lines forces a matrix +to be diagonal; fixing the line of (1,1) forces equal diagonal entries. +The resulting faithful quotient has order 24, so its image is all S4. +Every permutation has exactly two matrix lifts. + +Write p_1,...,p_4 for the projective permutations. A cost-three target +therefore has {p_1(T),...,p_4(T)} equal to the whole line set for every T. +In particular these permutations are distinct. Their 4-by-4 output array +is a Latin square. We count it directly, without importing a Latin-square +table or claiming the classical order-four enumeration as new mathematics. + +## 2. Classify the normalized supports + +Let S be a four-permutation support with the stated coverage. Left-multiply +all its elements by the inverse of any element g in S. Coverage is +preserved, and the normalized support H=g^-1 S contains the identity. +Every other element of H is a derangement, and any two elements disagree +on every input. + +The derangements of S4 are its three double transpositions and six +four-cycles. If H contains no four-cycle, it consists of the identity and +all three double transpositions. This is the regular Klein group V4. + +If H contains a four-cycle c, relabel its points so c=(1 2 3 4). A +permutation d compatible with both identity and c must satisfy +d(i) not in {i,c(i)} for all i. There are exactly two such permutations, +c^2 and c^3. For completeness, if d(1)=3, then d(3)=1 and the remaining +values force d=(3,4,1,2)=c^2. If d(1)=4, the remaining distinct values +force d=(4,1,2,3)=c^3. Hence H={1,c,c^2,c^3}, a regular cyclic group. + +There is one regular Klein subgroup and three cyclic subgroups of order four, +since the six four-cycles pair with their distinct inverses. Conversely, +each of these four regular subgroups, and each of its left cosets, meets +the coverage condition. This proves the claimed classification. + +## 3. Count without duplicate cosets + +Each subgroup has index six in S4 and therefore six left cosets. Cosets +arising from different subgroups cannot coincide. If S=gH=g'H', choose +s in S; then s^-1 S equals both H and H', so H=H'. Consequently there +are 3*6=18 cyclic supports and 1*6=6 Klein supports, 24 in total. + +Every support has 4!=24 orders and each of its four permutations has two +independent matrix lifts. The number of matrix targets is therefore + +```text +cyclic: 18 * 24 * 2^4 = 6,912 +Klein: 6 * 24 * 2^4 = 2,304 +total: 24 * 24 * 2^4 = 9,216 +fraction: 9,216 / 48^4 = 1/576. +``` + +There is no quotient by the free maps in this enumeration. A free map +changes the paid metric but does not identify distinct target matrices. +Likewise, ordering the algebra components is part of the target data. +Counting supports without the 24 orderings or forgetting the sixteen +scalar lifts would answer different questions. + +## Scope and credit + +This is a scoped counting proof with an exhaustive finite certificate. +The cited theorem supplies the cost interpretation. The new result is +its exact ternary four-component population and its projective coset +classification, produced by Nick Petalas. ToikY #4334, Nick Petalas +#4276/#4243, Wentao Li #4099 and the #2513 lineage retain predecessor +credit. The projective action, elementary permutation groups and +order-four Latin squares are classical. + +Other fields, other component counts, singular targets and local-algebra +lifts are outside this theorem. Native coefficient preparation, routing, +control, restoration, precision, stock and complete supplier costs remain +unknown. No supplier, selected frontier or complete multiplication theorem +changes. Independent human and formal proof-kernel review are unclaimed. +Apache-2.0. diff --git a/research/ternary-product-threshold-count/README.md b/research/ternary-product-threshold-count/README.md new file mode 100644 index 0000000000..d2df0fb095 --- /dev/null +++ b/research/ternary-product-threshold-count/README.md @@ -0,0 +1,112 @@ +# Exact ternary right-vector threshold count + +Scoped counting proof with an exhaustive finite certificate. No new kappa. + +For two roles over R=F3^4, exactly **9,216 of 5,308,416** invertible targets +need three paid factors I+u y^T with y over F3 and arbitrary common free +GL2(F3) maps anywhere. The exact fraction is **1/576**. + +Their unordered projective actions are exactly the left cosets of the +regular cyclic and Klein four subgroups of S4. The eighteen cyclic cosets +give 6,912 ordered matrix targets; the six Klein cosets give 2,304. +[PROOF.md](PROOF.md) derives the classification and count. This quantifies +the first ternary obstruction population left undetermined by ToikY's +[#4334](https://github.com/CrocSwap/integer-mult-bounds/pull/4334). +Its common-unit-pivot criterion and three-factor upper bound are cited +inputs, not audit deliverables. The projective/Latin-square facts are +classical; the claimed contribution is their exact cost consequence. + +## Evidence and reproduction + +The standard-library verifier uses two counting routes. It enumerates all +10,626 four-element subsets of S4 and proves the 24 covering supports are +exactly the classified cosets. Separately, it constructs all 48 invertible +ternary matrices and enumerates all 48^4 ordered matrix tuples using their +sixteen literal bilinear pivot values. The second route does not call the +projective action or subgroup classifier. Its 9,216 obstructed tuples agree +with 24*24*16 from the support count. No tuple is quotiented out by the free +maps or by scalar multiplication. + +It also checks all 2,304 projective multiplication pairs, both scalar lifts +of every action, 96 repeated-component controls, singular/wrong-size domain +rejections and a partial-input coverage control. Explicit exceptions remain +active under optimization. Each run emits a generated SHA256 receipt for +all six package files. It writes only stdout; no receipt is handwritten. + +From the repository root, with CPython 3.12 and no third-party packages: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -B -W error research/ternary-product-threshold-count/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -B -W error research/ternary-product-threshold-count/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/ternary-product-threshold-count +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/ternary-product-threshold-count --check-source-history +``` + +Any CPython 3.12 installation can replace the local interpreter path. +Expected marker is `PASS_TERNARY_PRODUCT_THRESHOLD_COUNT targets=5308416 cost3=9216 probability=1/576 no_new_kappa`. +Normal and optimized runs are separately registered with 120-second limits. +SOURCES.json pins the cited predecessor statements and historical task +context at main 624de9dc66858af0945e5f8a0942488d62280d43. The standalone +verifier imports no predecessor code and needs no Git or network access. + +The connector-alphabet-change card is explicitly changed to an algebraic +counting side question in TASK.json. Its 945-pairing positive control passes. +This does not supply the changed native operation or favorable complete +budget sought by the original card. + +## Limits and code inspection + +The exact-cost interpretation uses the cited field-product theorem. The +new proof and enumeration cover F3, two roles, four ordered components and +invertible endpoints. Other fields, lengths, singular endpoints and local +lifts are outside scope. Native coefficient preparation, routing, control, +restoration, precision, stock and the complete supplier invoice remain +unknown. No supplier admission, selected-frontier update or complete +multiplication theorem follows. Independent human and formal proof-kernel +review are unclaimed. Lean, Docker and selected operator replay are unrun +and unnecessary for this isolated counting result. + +The verifier has no recursion, process launch, network call or CLI input. +All domains are fixed: 81 candidate matrices, 48 invertible matrices, 24 +permutations, 10,626 candidate supports, and 48^4 matrix tuples. The largest +census streams one tuple at a time; it stores no target table. All function +bodies are below 60 lines. Receipt reads are bounded to six files of at most +1 MiB each. Warning-strict ordinary and optimized checks provide recurring +runtime diagnostics; no separate static analyzer is claimed. + +Power of Ten rule 3 has a managed-runtime deviation at verify.py. CPython +allocates integers, tuples and finite sets during enumeration. Fixed input +domains bound retained state to 24 supports, four subgroups and their 24 +cosets, 48 matrices and masks, and at most 24 action entries. The two +10,626-subset scans are streamed. The registered checks exercise the full +capacity. If these domains grow, a fixed-buffer or explicitly budgeted +implementation is required before expanding the census. Python has no raw +pointer or preprocessing operations; data access is shallow and direct. + +## Open next questions + +1. Count cost-three invertible targets over F3^k for k>4. Begin with a + finite inclusion-exclusion over missing entries in the four-by-four + permutation coverage board. This would measure how quickly the common + chart obstruction becomes typical; repeated projective components mean + the threshold coset classification alone does not count longer tuples. +2. Count the first obstruction population over F4^5. Begin with the + sharply transitive five-element subsets of PGL2(F4). Its image is a + proper subgroup of S5, so unrestricted order-five Latin-square counts + cannot be substituted. +3. Specify a literal native producer/consumer for this common-right-vector + alphabet and price coefficient preparation, access, restoration and + precision before using the count in a supplier. Those costs are unknown. + +TASK.json gives relevance, first steps and blockers for these questions. +No follow-on census is included in this contribution. + +## Credit + +This contribution was produced by Nick Petalas. ToikY #4334 supplies the +field-product criterion, upper bound and sharp threshold. Nick Petalas +#4276/#4243 supplies the low-factor criteria and free-map normalization. +Wentao Li #4099, following #2513, supplies the alphabet and column bound. +Projective actions, elementary permutation groups and Latin squares +retain their classical credit. Predecessor files and credit are unchanged. +Apache-2.0. diff --git a/research/ternary-product-threshold-count/SOURCES.json b/research/ternary-product-threshold-count/SOURCES.json new file mode 100644 index 0000000000..c45935a9a5 --- /dev/null +++ b/research/ternary-product-threshold-count/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "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/right-vector-commutative-products/PROOF.md", + "usage": "provenance", + "git_blob": "f149515c1684ac16bcb1ef0fd014b98d6f92f5db", + "sha256": "b401a15bc3a11e2040cdde9d99d4a5b8ec7b4f92643eac547f21b7c667fbf408" + }, + { + "path": "research/right-vector-commutative-products/README.md", + "usage": "provenance", + "git_blob": "fc9889d41621b596209c707b6057517744b4642f", + "sha256": "6222431360182204f502334d1c707eefc39a174d06578ef75c52f37b5873055f" + }, + { + "path": "docs/research/research-family-status.md", + "usage": "provenance", + "git_blob": "743a1afcbc46c715d2035037797e2f81b32e58a5", + "sha256": "21ea61004c0270388258c4251b1c586b65f06bc807395b281deacfb886204934" + } + ] +} diff --git a/research/ternary-product-threshold-count/TASK.json b/research/ternary-product-threshold-count/TASK.json new file mode 100644 index 0000000000..77eb7f2e5f --- /dev/null +++ b/research/ternary-product-threshold-count/TASK.json @@ -0,0 +1,89 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "original_card": { + "id": "connector-alphabet-change", + "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/universal-connector-boundary/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Construct and charge a legal extra operation on a minimal instance.", + "Prove a target-specific bound after adding one specified operation family." + ], + "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free. 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", + "research/universal-connector-boundary/verify.py" + ], + "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY", + "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.", + "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.", + "allowed_variations": [ + "Choose one additional operation and a small source count for its first counterexample." + ], + "scope_change_triggers": [ + "Keeping the alphabet and only increasing the source count; record this as a changed assignment.", + "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions." + ], + "overlap_terms": [ + "universal connector", + "source-toggle", + "connector alphabet" + ] + }, + "scope_status": "changed", + "actual_scope": "Count and classify all exact-cost-three invertible two-role targets over F3^4 in the common-right-vector alphabet.", + "scope_change_reason": "Keep the formal alphabet and take a counting side question extending ToikY #4334, rather than adding a native operation. The first ternary obstruction population was not counted by the predecessor.", + "bottleneck_link": "Side result: quantifies the common-chart obstruction in the formal alphabet; no physical supplier cost is improved.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified exact threshold population and classification; defer larger fields and component counts.", + "outcome": "completed", + "evidence": "Written coset proof; complete 10626-support census; independent literal 5308416-target pivot enumeration with 9216 cost-three targets; normal and optimized rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Count cost-three invertible targets over F3^k for k>4.", + "why_it_matters": "Measures frequency of the shared-chart obstruction beyond the threshold.", + "first_step": "Use inclusion-exclusion over missing cells of the four-by-four permutation coverage board.", + "blocked_by": "Repeated projective actions invalidate the distinct-support threshold count." + }, + { + "question": "Count cost-three targets at the F4^5 invertible threshold.", + "why_it_matters": "Tests how the population changes when the projective action is a proper subgroup of the symmetric group.", + "first_step": "Enumerate sharply transitive five-element subsets of PGL2(F4).", + "blocked_by": "The S4 surjectivity used here does not extend to S5." + }, + { + "question": "Price one native producer/consumer for the formal alphabet.", + "why_it_matters": "Formal paid factors alone do not admit a physical supplier.", + "first_step": "Specify all coefficient preparation, access, frame, restoration, precision and stock contracts before an invoice.", + "blocked_by": "These physical costs remain unknown." + } + ], + "canonical_claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19132065", + "overlap": { + "open_prs": 326, + "discussion_records": 3748, + "remote_complete_pagination": true, + "sparse_local_complete": false, + "base_readme_search": "Latin.square; ternary.*product.*count; permutation.cover; 9216/9,216 with distinct right-vector terms", + "merged_pr_searches": [ + "Latin square", + "Latin", + "9216 right-vector", + "right-vector count" + ], + "limitations": "Unpublished work, arbitrary code and omitted local notes are outside coverage." + } +} diff --git a/research/ternary-product-threshold-count/VERIFY.json b/research/ternary-product-threshold-count/VERIFY.json new file mode 100644 index 0000000000..dcdcccc098 --- /dev/null +++ b/research/ternary-product-threshold-count/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete ternary matrix threshold enumeration, independent projective support/coset census, domain and coverage controls; generated six-file SHA256 receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete enumeration and explicit rejection controls under optimized Python." + } + ] +} diff --git a/research/ternary-product-threshold-count/verify.py b/research/ternary-product-threshold-count/verify.py new file mode 100644 index 0000000000..a4432d0498 --- /dev/null +++ b/research/ternary-product-threshold-count/verify.py @@ -0,0 +1,191 @@ +#!/usr/bin/env python3 +"""Exact ternary threshold count; standard library, no runtime dependencies.""" + +from collections import Counter +from hashlib import sha256 +from itertools import combinations, permutations, product +import json +from pathlib import Path + + +IDENTITY = (0, 1, 2, 3) +LINES = ((1, 0), (0, 1), (1, 1), (1, 2)) +FULL = (1 << 16) - 1 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def compose(a, b): + return tuple(a[b[i]] for i in range(4)) + + +def inverse(a): + return tuple(a.index(i) for i in range(4)) + + +def multiply(a, b): + return tuple(sum(a[2 * i + h] * b[2 * h + j] for h in range(2)) % 3 + for i in range(2) for j in range(2)) + + +def action(matrix): + result = [] + a, b, c, d = matrix + for x, y in LINES: + u, v = (a * x + b * y) % 3, (c * x + d * y) % 3 + require(u != 0 or v != 0, "singular projective action") + line = (1, v * pow(u, -1, 3) % 3) if u else (0, 1) + result.append(LINES.index(line)) + return tuple(result) + + +def literal_zero_mask(matrix): + """Bit (i,j) records phi_j M t_i=0, with literal F3 arithmetic.""" + a, b, c, d = matrix + mask = 0 + for i, (x, y) in enumerate(LINES): + for j, (r, s) in enumerate(LINES): + value = r * (a * x + b * y) + s * (c * x + d * y) + if value % 3 == 0: + mask |= 1 << (4 * i + j) + require(mask.bit_count() == 4, "one annihilator per input line") + return mask + + +def covers(support): + require(len(support) == 4, "threshold support must have four permutations") + return all(len({p[i] for p in support}) == 4 for i in range(4)) + + +def normalized_groups(all_permutations): + groups = set() + for p in all_permutations: + p2 = compose(p, p) + if p2 != IDENTITY and compose(p2, p2) == IDENTITY: + groups.add(frozenset((IDENTITY, p, p2, compose(p2, p)))) + doubles = tuple(p for p in all_permutations + if p != IDENTITY and compose(p, p) == IDENTITY + and all(p[i] != i for i in range(4))) + require(len(doubles) == 3, "three double transpositions") + groups.add(frozenset((IDENTITY, *doubles))) + require(len(groups) == 4, "three cyclic groups and one Klein group") + for group in groups: + require(covers(group), "regular group action") + require(all(compose(a, b) in group for a in group for b in group), + "subgroup closure") + return groups + + +def check_supports(all_permutations): + groups = normalized_groups(all_permutations) + supports = {frozenset(s) for s in combinations(all_permutations, 4) + if covers(s)} + cosets = {frozenset(compose(p, h) for h in group) + for p in all_permutations for group in groups} + require(len(supports) == 24 and supports == cosets, "coset classification") + require({s for s in supports if IDENTITY in s} == groups, + "complete normalized classification") + kinds = Counter() + for support in supports: + first = min(support) + normal = frozenset(compose(inverse(first), p) for p in support) + require(normal in groups, "normalization lands in a classified group") + kinds["cyclic" if any(compose(p, p) != IDENTITY for p in normal) + else "klein"] += 1 + require(kinds == {"cyclic": 18, "klein": 6}, "coset type counts") + return supports, kinds + + +def matrix_census(matrices): + """Enumerate every ordered GL2(F3)^4 target, without projective actions.""" + masks = tuple(literal_zero_mask(m) for m in matrices) + count, visited = 0, 0 + for a in masks: + for b in masks: + ab = a | b + for c in masks: + abc = ab | c + for d in masks: + visited += 1 + count += abc | d == FULL + require(visited == 48 ** 4, "complete ordered matrix census") + require(count == 9216, "literal matrix threshold count") + return visited, count + + +def controls(all_permutations, matrices, supports): + checks = 0 + for support in supports: + for removed in support: + remaining = tuple(p for p in support if p != removed) + require(not covers((*remaining, remaining[0])), "duplicate control") + checks += 1 + for matrix in matrices: + negative = tuple(-x % 3 for x in matrix) + require(action(matrix) == action(negative), "scalar-lift invariance") + require(literal_zero_mask(matrix) == literal_zero_mask(negative), + "literal scalar-lift invariance") + checks += 1 + try: + action((1, 0, 0, 0)) + except ValueError: + checks += 1 + else: + raise ValueError("singular matrix accepted") + try: + covers(all_permutations[:3]) + except ValueError: + checks += 1 + else: + raise ValueError("wrong component count accepted") + partial = next(s for s in combinations(all_permutations, 4) + if all(len({p[i] for p in s}) == 4 for i in range(2)) + and not covers(s)) + require(not covers(partial), "partial-input coverage is insufficient") + checks += 1 + return checks + + +def receipt(results): + directory = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", + "VERIFY.json", "verify.py") + hashes = {} + for name in names: + path = directory / name + require(path.stat().st_size <= 1024 * 1024, "receipt file capacity") + hashes[name] = sha256(path.read_bytes()).hexdigest() + print(json.dumps({"schema": "ternary-product-threshold-count/v1", + "results": results, "sha256": hashes}, sort_keys=True)) + + +def main(): + all_permutations = tuple(permutations(range(4))) + matrices = tuple(m for m in product(range(3), repeat=4) + if (m[0] * m[3] - m[1] * m[2]) % 3) + require(len(matrices) == 48, "GL2(F3) order") + actions = Counter(action(m) for m in matrices) + require(actions == {p: 2 for p in all_permutations}, "two lifts per S4 action") + for a in matrices: + for b in matrices: + require(action(multiply(a, b)) == compose(action(a), action(b)), + "projective multiplication convention") + supports, kinds = check_supports(all_permutations) + visited, count = matrix_census(matrices) + require(count == len(supports) * 24 * 2 ** 4, "independent count agreement") + require(visited == count * 576, "exact probability 1/576") + checks = controls(all_permutations, matrices, supports) + results = {"targets": visited, "cost_three": count, + "projective_supports": len(supports), "support_types": dict(kinds), + "cyclic_targets": kinds["cyclic"] * 24 * 16, + "klein_targets": kinds["klein"] * 24 * 16, "controls": checks} + receipt(results) + print(f"PASS_TERNARY_PRODUCT_THRESHOLD_COUNT targets={visited} " + f"cost3={count} probability=1/576 no_new_kappa") + + +if __name__ == "__main__": + main()