diff --git a/research/ranktwo-overlap-ternary/README.md b/research/ranktwo-overlap-ternary/README.md new file mode 100644 index 0000000000..078fb0f7bb --- /dev/null +++ b/research/ranktwo-overlap-ternary/README.md @@ -0,0 +1,175 @@ +# Positive correlation for overlapping ternary rank-two full guards + +This package was produced by Nick Petalas. Apache-2.0. + +**Claim type: exact finite certificate with a written counting reduction.** +For the fixed commuting projectors over F3 + +```text +P = diag(0,1,0,1), Q = diag(0,0,1,1), +``` +exactly **2,409,984 of 24,261,120** complete headers in GL4(F3) pass +both requests' full guards. Their joint fraction is **523/5265**. +Each marginal is **361/1170**, so their covariance is strictly positive: + +```text +523/5265 - (361/1170)^2 = 5659/1368900 > 0. +``` + +A request passes G when the leading principal minors of GPG^-1 or GQG^-1 +of orders one and two are both nonzero. This is a fixed, uniform complete +header cover and a fixed pair chosen before the header. The result applies +to every commuting ternary projector pair with joint-sector dimensions +(00,10,01,11) = (1,1,1,1), by simultaneous conjugation. + +This supplies an explicit positive-correlation example beyond the orthogonal +and corank-one families. It answers one bounded part of the nonlaminar +full-guard question and gives a new residual-state fixture for state-aware +recursion. No new kappa, supplier admission or multiplication theorem follows. + +## Exact residual distribution + +After a passing first pivot, each Schur complement is a rank-one idempotent +on F3^3. In the following table S and T are ordered. The middle count is the +number of first split pairs reaching that type. The next column counts +second split pairs passing both terminal guards, out of 234. Multiplication +by 48 gives the passing complete GL3 continuation headers per first split. + +| Residual type | First splits | Passing second splits | Full GL4 headers | +|---|---:|---:|---:| +| S = T | 44 | 114 | 240,768 | +| Same image, different kernels | 88 | 78 | 329,472 | +| Same kernel, different images | 88 | 78 | 329,472 | +| ST = TS = 0 | 294 | 44 | 620,928 | +| ST = 0, TS != 0 | 168 | 50 | 403,200 | +| TS = 0, ST != 0 | 168 | 50 | 403,200 | +| Different images/kernels, tr(ST) = 1 | 32 | 54 | 82,944 | +| Different images/kernels, tr(ST) not in {0,1} | 0 | 56 | 0 | +| Total | 882 | | 2,409,984 | + +The table's terminal counts are the specialization of Nick Petalas's +[#4240 rank-one pair law](../projector-pair-header-law/README.md). +The new quantities are the initial residual distribution, its weighted +full-guard count and the positive covariance. The verifier computes the +second-split count separately for **every** initial split; its total does +not assume that a residual type is a sufficient invariant or use the +predecessor formula to generate successful events. In particular, generic +residuals occur zero times in this enumerated domain only. + +## Counting reduction + +1. Write x=e1^T G and y=G^-1 e1. Then xy=1. There are + (3^4-1)3^3=2160 such pairs. For each, choose W=[y,B], where B is the + explicit ordered basis of ker x in the verifier. Thus xW=e1^T and + G0=W^-1 has first row x. Every header with this same split pair has + the unique form diag(1,K)G0 for K in GL3(F3). This proves the common + completion factor |GL3(F3)|=11232 and total denominator 24,261,120. + +2. For either conjugated request R=G0 P G0^-1 or G0 Q G0^-1, write + R=[[p,b],[c,D]]. When p is nonzero its Schur complement is + S=D-cb/p. The leading two-by-two determinant after the remaining + change K is p times (K S K^-1)[0,0]. Therefore the two full guards + are equivalent to both initial pivots being nonzero and both + residual first pivots being nonzero. Standard idempotent Schur + deletion gives rank one; the verifier also checks nonzero rank and + S^2=S at every applicable split. This scalar deletion is credited + to the retained #4228/#4278 lineage. + +3. Put a=e1^T K and b=K^-1 e1 in dimension three. There are + (3^3-1)3^2=234 split pairs ab=1, each with exactly |GL2(F3)|=48 + completions by the same basis argument. Count the terminal events + by directly evaluating aSb and aTb. The verifier visits all + 2160*234=505440 two-stage split paths. The successful totals before + the final completion multiplier are 155952 for either marginal + and 50208 for their intersection. Consequently the full counts + are 7,485,696 for either marginal and 2,409,984 jointly. + +4. All idempotent commuting pairs with the stated four sector dimensions + are simultaneously conjugate to P,Q. Multiplication of G by a fixed + conjugating matrix permutes the complete GL4 cover. Thus the count + depends on that sector profile, rather than the chosen axis labels. + +This proof reduces an exact finite enumeration to its explicitly enumerated +finite domain; it does not assert a formula uniform in field size or rank. + +## Reproduction and evidence + +From the repository root, use CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/ranktwo-overlap-ternary/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/ranktwo-overlap-ternary/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/ranktwo-overlap-ternary +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/ranktwo-overlap-ternary --check-source-history +``` + +The verifier prints `PASS_RANKTWO_OVERLAP_TERNARY` in a generated JSON receipt +binding every package file's SHA256. It writes no files. The registered +normal and optimized runs use explicit exceptions, so -O retains every check. + +Besides the complete two-stage split enumeration, the verifier scans all +19,683 ternary three-by-three matrices to obtain GL3. For one original split +in each of the seven occupied residual types, it checks all 11,232 literal +complete headers in the continuation fibre. These **78,624** direct header +checks evaluate the original requests' one-by-one and two-by-two minors +without Schur complements. They corroborate each class's continuation count; +this is not a raw scan of all 24,261,120 GL4 headers. + +Reversing the completion kernel basis preserves the residual type for every +one of the 882 jointly admitted first splits. Eight controls cover a singular +matrix, two invalid split pairs, a zero pivot, loss of continuation information +under commutator-only state identification, first-pivot/full-guard confusion, +a missing completion multiplier and the complete denominator. + +Power of Ten scope is this standalone verifier. Its dimension is fixed at +four, its field at three, functions are below 60 lines, and it uses no recursion, +subprocesses or runtime-generated code. Every loop is bounded by these fixed +domains; the largest raw scan is 19,683 matrices. Python's managed allocation +requires a rule 3 deviation: the live GL3 list is bounded at 11,232 matrix/inverse +pairs, first splits at 2160 and terminal splits at 234; there is no user-selected +size. A fixed-capacity implementation is a follow-up only if these bounds change. +Warning-strict execution and the repository's package checks provide available +Python diagnostics; no new repository-wide analyzer configuration is introduced. + +## Scope, predecessor credit and limitations + +This takes the nonlaminar question of Nick Petalas #4240/#4259 and the +state-aware continuation question of **ssafwann #4678**, **Mihir Srivastava +#4689**, and **codyw912 #4735**. Their one-block, binary rank-three profile and +binary transition results retain their credit. **MatShep #4762** supplies the +related all-field factor-invariant framework. None of those results is the +deliverable being rechecked here, and none of their executable code is imported. + +Credit Nick Petalas's #4240 terminal law and #4228/#4278 scalar completion/Schur +lineage; **Ryanson Jonathan** for the separate-family full-guard census and +sharpness work; **lee-phys** for dimension work; **Cinna Davis** for the BIT +request context; and **source527**, **commdata2338**, and **Jose Manuel** for +the normalizer lineage. Exact main-source blobs are historical provenance in +[SOURCES.json](SOURCES.json). Their original credit lines remain unchanged. + +Canonical base is 624de9dc66858af0945e5f8a0942488d62280d43, priority revision 7. +[TASK.json](TASK.json) marks formal-interface-lemma as changed to this algebraic +side result. The card's old balanced-transfer baseline fails on the current +certificate with KeyError 'bit_lower'; its documented replacement +`research_selected_baseline.py` passes source-binding orientation. Neither +baseline is scientific evidence for this count. + +Finite exactness is the claim. Other fields, sector profiles, restricted or +weighted header covers and adaptive requests remain outside scope. Ternary +rank two is within the odd-field algebraic model, but no actual producer, +header selection/emission, physical reads, dirty restoration, stock, dispatch +or complete consumer bill is provided. No selected scientific cold replay, +Lean or Docker run is required or claimed. Independent human and formal +proof-kernel review are unclaimed. + +## Open next questions + +1. Determine an exact field-uniform law for this same four-sector pair. + This would identify when its positive correlation persists. Start by + counting the residual-type multiplicities symbolically from sector dot + products; the missing ingredient is that distribution, rather than the + already known terminal rank-one laws. +2. Extend a state-aware recursion to one larger nonlaminar profile using + #4762's factor invariant. First retain actual transition multiplicities + and compare them with a literal finite sample. A complete higher-rank + transition law and its cost remain missing. diff --git a/research/ranktwo-overlap-ternary/SOURCES.json b/research/ranktwo-overlap-ternary/SOURCES.json new file mode 100644 index 0000000000..ca3e061771 --- /dev/null +++ b/research/ranktwo-overlap-ternary/SOURCES.json @@ -0,0 +1,54 @@ +{ + "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/projector-pair-header-law/README.md", + "usage": "provenance", + "git_blob": "e8b79e95d0ee8105d3c931766eaf53e45a680005", + "sha256": "49e2f01d95f856e366fd254320b78fa7e48dbad622b605fe2222b5755c403156" + }, + { + "path": "research/laminar-header-law/README.md", + "usage": "provenance", + "git_blob": "b39ea17c2764764e507d8d3c8b2f079dc2a96efa", + "sha256": "5cf3ff2b00615c59c8a534552517eeab966bcdd8e7b5029aaa1919b4fb942d09" + }, + { + "path": "research/schur-header-count/README.md", + "usage": "provenance", + "git_blob": "5e644cf316312c0fdd489c8d33911583f1b88af2", + "sha256": "472295f32ebf3fcdc8daa4137af63db70d9943de7cbb97e47ed272823b2a227e" + }, + { + "path": "research/schur-residual-orbits/README.md", + "usage": "provenance", + "git_blob": "a2361477d9373969ccb7ab0f4f3c4b9919c051ba", + "sha256": "15e2f1a7d4edcc8f71e75ead949928c2ac883a3fb8268bb5827f290de4d28d76" + }, + { + "path": "research/schur-invariant-transitions/README.md", + "usage": "provenance", + "git_blob": "d5118b9f5911949964245eb8942065faff972900", + "sha256": "fccdd2bff1ee00c120796bb1b6c3739cce90dcffbff7c96e897300ed81bba72e" + }, + { + "path": "research/idempotent-factor-invariant/README.md", + "usage": "provenance", + "git_blob": "48ce67bdc3c7c35081cc04f86b7ee20c6a5dd06b", + "sha256": "fae88ccbea3a16d041666f5956d0416b6a21ef57a21f1a0996c7c3a74f7fa3d1" + } + ] +} diff --git a/research/ranktwo-overlap-ternary/TASK.json b/research/ranktwo-overlap-ternary/TASK.json new file mode 100644 index 0000000000..de1c9bd208 --- /dev/null +++ b/research/ranktwo-overlap-ternary/TASK.json @@ -0,0 +1,128 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact finite full-guard count and positive covariance for the ternary commuting rank-two projector pair with joint sectors (1,1,1,1).", + "scope_change_reason": "Take the explicit nonlaminar full-guard and state-continuation questions as an algebraic side result; no proof-assistant or selected caller claim.", + "bottleneck_link": "The joint law supplies a new nonlaminar state-aware header fixture; it alone supplies no paid header cover or supplier improvement.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified original finite result; leave field-uniform and larger-profile laws as open questions.", + "outcome": "completed", + "evidence": "505440 enumerated two-stage split paths and 78624 literal complete-header checks, with exact residual multiplicities and positive covariance.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the field-uniform full-guard law for this four-sector pair?", + "why_it_matters": "It would classify persistence of positive correlation.", + "first_step": "Count initial residual types symbolically using sector dot products.", + "blocked_by": "An exact field-uniform residual distribution." + }, + { + "question": "Can the factor invariant yield an explicit next-pivot law for a larger nonlaminar profile?", + "why_it_matters": "This is needed for scalable state-aware header recursion.", + "first_step": "Choose one profile, retain multiplicities and compare literal samples.", + "blocked_by": "Higher-rank transition multiplicities and complete physical costs." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19132056", + "upstream_refresh": { + "commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "priority_revision": 7, + "utc": "2026-10-22T20:13:41Z" + }, + "overlap": { + "open_prs": 326, + "discussion_records": 3754, + "coverage_time": "2026-10-22T20:19:43.415699+00:00", + "local_notes": 119, + "head_notes": 6319, + "limits": "Sparse local-note coverage; main README searches supplement it. Arbitrary diffs and unpublished work excluded. Merged PR searches checked rank-two header, Schur count and residual orbit terms." + }, + "preserved_prior_branch": "research/w6-1022g-header-extension", + "preserved_prior_head": "9997ae7d1c99ecf5eb915aad28eb7b61e778956c", + "claim_type": "exact finite certificate with written reduction", + "environment": { + "python": "3.12.15", + "platform": "macOS 27.0.1 arm64", + "requirements": "standard library only" + }, + "local_check_times_seconds": { + "normal": 1.27, + "optimized": 1.27, + "registered_total": 2.86 + } +} diff --git a/research/ranktwo-overlap-ternary/VERIFY.json b/research/ranktwo-overlap-ternary/VERIFY.json new file mode 100644 index 0000000000..1c9068105a --- /dev/null +++ b/research/ranktwo-overlap-ternary/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact split enumeration, literal complete-header fibres, residual types, positive covariance and eight semantic controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Identical finite certificate with assertions disabled; every contract remains active." + } + ] +} diff --git a/research/ranktwo-overlap-ternary/verify.py b/research/ranktwo-overlap-ternary/verify.py new file mode 100644 index 0000000000..ad7e2abbdd --- /dev/null +++ b/research/ranktwo-overlap-ternary/verify.py @@ -0,0 +1,270 @@ +#!/usr/bin/env python3 +"""Exact ternary overlapping-projector count, produced by Nick Petalas. Apache-2.0.""" + +from collections import Counter +from fractions import Fraction +import hashlib +from itertools import product +import json +from pathlib import Path +import sys + + +Q = 3 +MASKS = ((0, 1, 0, 1), (0, 0, 1, 1)) +FILES = ("README.md", "SOURCES.json", "TASK.json", "VERIFY.json", "verify.py") +TYPES = ("equal", "same_image", "same_kernel", "orthogonal", + "st_zero", "ts_zero", "generic", "degenerate") +EXPECTED = dict(zip(TYPES, (44, 88, 88, 294, 168, 168, 0, 32))) +TERMINAL = dict(zip(TYPES, (114, 78, 78, 44, 50, 50, 56, 54))) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def dot(a, b): + need(len(a) == len(b) <= 4, "bounded dot dimensions") + return sum(x * y for x, y in zip(a, b)) % Q + + +def identity(n): + need(1 <= n <= 4, "identity dimension") + return tuple(tuple(int(i == j) for j in range(n)) for i in range(n)) + + +def multiply(a, b): + need(1 <= len(a) <= 4 and 1 <= len(b) <= 4, "matrix dimensions") + need(all(len(r) == len(b) for r in a), "inner dimensions") + return tuple(tuple(dot(r, c) for c in zip(*b)) for r in a) + + +def inverse(a): + n = len(a) + need(1 <= n <= 4 and all(len(r) == n for r in a), "square dimension") + b = [list(r) + list(e) for r, e in zip(a, identity(n))] + for k in range(n): + pivot = next((i for i in range(k, n) if b[i][k]), None) + if pivot is None: + return None + b[k], b[pivot] = b[pivot], b[k] + scale = pow(b[k][k], -1, Q) + b[k] = [z * scale % Q for z in b[k]] + for i in range(n): + if i != k: + factor = b[i][k] + b[i] = [(u - factor * v) % Q for u, v in zip(b[i], b[k])] + return tuple(tuple(r[n:]) for r in b) + + +def splits(n): + need(n in (3, 4), "split dimension") + vectors = tuple(product(range(Q), repeat=n)) + return tuple((x, y) for x in vectors for y in vectors if dot(x, y) == 1) + + +def completion(x, y, reverse=False): + need(len(x) == len(y) == 4 and dot(x, y) == 1, "split pair") + pivot = next(i for i, value in enumerate(x) if value) + indices = [j for j in range(4) if j != pivot] + if reverse: + indices.reverse() + columns = [y] + for j in indices: + column = [0] * 4 + column[j] = 1 + column[pivot] = -x[j] * pow(x[pivot], -1, Q) % Q + columns.append(tuple(column)) + w = tuple(zip(*columns)) + g = inverse(w) + need(g is not None and g[0] == x, "completion first row") + need(multiply(g, w) == identity(4), "completion inverse") + return g, w + + +def conjugate_diagonal(g, w, mask): + need(len(g) == len(w) == len(mask) == 4, "conjugation dimension") + return multiply(g, tuple(tuple(mask[i] * z % Q for z in w[i]) + for i in range(4))) + + +def schur(a): + need(len(a) == 4 and a[0][0] != 0, "nonzero first pivot") + scale = pow(a[0][0], -1, Q) + s = tuple(tuple((a[i][j] - a[i][0] * a[0][j] * scale) % Q + for j in range(1, 4)) for i in range(1, 4)) + need(multiply(s, s) == s, "residual idempotency") + # Every nonzero column and row must span the respective rank-one space. + need(any(any(r) for r in s), "nonzero residual") + rows = {normalize(r) for r in s if any(r)} + need(len(rows) == 1, "rank-one residual") + return s + + +def normalize(vector): + need(1 <= len(vector) <= 4 and any(vector), "nonzero projective vector") + scale = pow(next(z for z in vector if z), -1, Q) + return tuple(z * scale % Q for z in vector) + + +def pair_type(s, t): + need(len(s) == len(t) == 3, "terminal dimension") + if s == t: + return "equal" + images = [] + kernels = [] + for a in (s, t): + images.append(normalize(next(c for c in zip(*a) if any(c)))) + kernels.append(normalize(next(r for r in a if any(r)))) + if images[0] == images[1]: + return "same_image" + if kernels[0] == kernels[1]: + return "same_kernel" + st, ts = multiply(s, t), multiply(t, s) + nz_st, nz_ts = any(any(r) for r in st), any(any(r) for r in ts) + if not nz_st and not nz_ts: + return "orthogonal" + if not nz_st: + return "st_zero" + if not nz_ts: + return "ts_zero" + trace = sum(st[i][i] for i in range(3)) % Q + return "degenerate" if trace == 1 else "generic" + + +def terminal_counts(s, t, pairs): + need(len(pairs) == 234, "complete second split domain") + count_s = count_t = joint = 0 + for a, b in pairs: + ps = s is not None and dot(tuple(dot(a, c) for c in zip(*s)), b) != 0 + pt = t is not None and dot(tuple(dot(a, c) for c in zip(*t)), b) != 0 + count_s += ps + count_t += pt + joint += ps and pt + return count_s, count_t, joint + + +def enumerate_first(pairs): + distribution = Counter({kind: 0 for kind in TYPES}) + witnesses = {} + totals = [0, 0, 0] + first_counts = [0, 0, 0] + first_pairs = splits(4) + need(len(first_pairs) == 2160, "complete first split domain") + for x, y in first_pairs: + g, w = completion(x, y) + matrices = tuple(conjugate_diagonal(g, w, mask) for mask in MASKS) + residuals = tuple(schur(a) if a[0][0] else None for a in matrices) + for i in range(2): + first_counts[i] += residuals[i] is not None + first_counts[2] += all(s is not None for s in residuals) + counts = terminal_counts(*residuals, pairs) + totals = [a + b for a, b in zip(totals, counts)] + if all(s is not None for s in residuals): + kind = pair_type(*residuals) + distribution[kind] += 1 + witnesses.setdefault(kind, (x, y)) + need(counts == (114, 114, TERMINAL[kind]), "terminal class count") + h, v = completion(x, y, reverse=True) + alternate = tuple(schur(conjugate_diagonal(h, v, m)) for m in MASKS) + need(pair_type(*alternate) == kind, "completion-basis invariance") + need(dict(distribution) == EXPECTED, "original residual distribution") + need(first_counts == [1368, 1368, 882], "first-pivot counts") + need(totals == [155952, 155952, 50208], "two-stage split counts") + return distribution, witnesses, totals, first_counts + + +def gl3(): + result = [] + for entries in product(range(Q), repeat=9): + g = tuple(tuple(entries[3 * i:3 * i + 3]) for i in range(3)) + h = inverse(g) + if h is not None: + need(multiply(g, h) == identity(3), "GL3 inverse") + result.append((g, h)) + need(len(result) == 11232, "complete GL3 cardinality") + return result + + +def direct_guard(x, y, z, v, mask): + a = sum(x[i] * mask[i] * y[i] for i in range(4)) % Q + b = sum(x[i] * mask[i] * v[i] for i in range(4)) % Q + c = sum(z[i] * mask[i] * y[i] for i in range(4)) % Q + d = sum(z[i] * mask[i] * v[i] for i in range(4)) % Q + return a != 0 and (a * d - b * c) % Q != 0 + + +def literal_fibres(witnesses): + headers = gl3() + counts = {} + for kind, (x, y) in sorted(witnesses.items()): + g, w = completion(x, y) + passed = 0 + for k, h in headers: + # Actual second row of diag(1,K)G and column of W diag(1,K^-1). + z = tuple(sum(k[0][j] * g[j + 1][i] for j in range(3)) % Q + for i in range(4)) + v = tuple(sum(w[i][j + 1] * h[j][0] for j in range(3)) % Q + for i in range(4)) + passed += all(direct_guard(x, y, z, v, m) for m in MASKS) + need(passed == TERMINAL[kind] * 48, "literal complete-header fibre") + counts[kind] = passed + need(len(counts) == 7, "every occupied type has a literal fibre") + return counts + + +def controls(distribution, totals): + need(inverse(((1, 0), (0, 0))) is None, "singular inverse control") + rejected = 0 + for x, y in (((0, 0, 0, 0), (1, 0, 0, 0)), + ((1, 0, 0, 0), (0, 1, 0, 0))): + try: + completion(x, y) + except ValueError: + rejected += 1 + need(rejected == 2, "invalid split controls") + try: + schur(tuple((0, 0, 0, 0) for _ in range(4))) + except ValueError: + rejected += 1 + need(rejected == 3, "zero first pivot rejected") + need(distribution["equal"] and distribution["orthogonal"], "distinct commuting types") + need(TERMINAL["equal"] != TERMINAL["orthogonal"], "commutator-only state loses counts") + need(882 * 11232 != totals[2] * 48, "first/full guard control") + need(totals[2] != totals[2] * 48, "completion multiplier control") + need(2160 * 11232 == 24261120, "full header denominator") + return 8 + + +def main(): + need(len(sys.argv) == 1, "no command-line arguments are supported") + pairs = splits(3) + distribution, witnesses, totals, first_counts = enumerate_first(pairs) + literal = literal_fibres(witnesses) + n_controls = controls(distribution, totals) + denominator = 2160 * 11232 + joint = Fraction(totals[2] * 48, denominator) + marginal = Fraction(totals[0] * 48, denominator) + gap = joint - marginal * marginal + need(joint == Fraction(523, 5265), "joint fraction") + need(marginal == Fraction(361, 1170), "marginal fraction") + need(gap == Fraction(5659, 1368900) and gap > 0, "strict positive correlation") + package = Path(__file__).resolve().parent + receipt = { + "status": "PASS_RANKTWO_OVERLAP_TERNARY", "field": 3, + "first_splits": 2160, "second_splits": len(pairs), + "first_pivot_counts": first_counts, "distribution": dict(distribution), + "two_stage_counts": totals, "complete_header_count": denominator, + "joint_headers": totals[2] * 48, "marginal_headers": totals[0] * 48, + "joint_fraction": str(joint), "marginal_fraction": str(marginal), + "positive_covariance": str(gap), "literal_fibre_counts": literal, + "literal_headers_checked": 7 * 11232, "controls": n_controls, + "file_sha256": {name: hashlib.sha256((package / name).read_bytes()).hexdigest() + for name in FILES}, + } + print(json.dumps(receipt, sort_keys=True)) + + +if __name__ == "__main__": + main()