From 3b098803eb854afbd5d63ad3bf4d75cdb1e515d5 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 28 Oct 2026 00:19:05 +0000 Subject: [PATCH] feat(research): prove the fifth rational frame needs eight calls Exponent support forces a B call that the first-order floor misses, which excludes seven calls at every even-denominator slope; odd denominators keep the four-address floor. This settles the open seven-call case at t = 1/2. --- .../README.md | 157 ++++++++ .../SOURCES.json | 30 ++ .../TASK.json | 70 ++++ .../VERIFY.json | 19 + .../verify.py | 378 ++++++++++++++++++ 5 files changed, 654 insertions(+) create mode 100644 research/bit-fifth-rational-frame-every-rational-t/README.md create mode 100644 research/bit-fifth-rational-frame-every-rational-t/SOURCES.json create mode 100644 research/bit-fifth-rational-frame-every-rational-t/TASK.json create mode 100644 research/bit-fifth-rational-frame-every-rational-t/VERIFY.json create mode 100644 research/bit-fifth-rational-frame-every-rational-t/verify.py diff --git a/research/bit-fifth-rational-frame-every-rational-t/README.md b/research/bit-fifth-rational-frame-every-rational-t/README.md new file mode 100644 index 0000000000..a7c6b3a06b --- /dev/null +++ b/research/bit-fifth-rational-frame-every-rational-t/README.md @@ -0,0 +1,157 @@ +# A fifth rational frame never saves a call: the minimum is eight for every rational t + +**Scoped proof in a formal register model, with a finite exact check. No +selected supplier or new κ is claimed.** + +## Result + +Take the four-role target of +[PR #2085](https://github.com/CrocSwap/integer-mult-bounds/pull/2085), + +$$ +T=\operatorname{diag}([A+P],[A+Q],[B+P],[B+Q]), +$$ + +with $A=E_{11}$, $B=E_{22}$, $P=\tfrac12\begin{pmatrix}1&1\\1&1\end{pmatrix}$ +and $Q=A+B-P$. A paid call is $I_4+([F]-1)N$ with $N$ any of the 120 rank-one +idempotents in $M_4(\mathbb F_2)$, and free role mixing is allowed. Add the +fifth rational rank-one address + +$$ +R_t=(1,t)^T(1,t)=\begin{pmatrix}1&t\\t&t^2\end{pmatrix},\qquad t\in\mathbb Q . +$$ + +**Theorem.** For every rational $t$, every word over $\{A,B,P,Q,R_t\}$ that +equals $T$ in $M_4(\mathbb F_2[\Lambda_t])$, $\Lambda_t=\mathbb ZA+\mathbb ZB+\mathbb ZP+\mathbb ZR_t$, +has at least eight calls. The direct eight-call word attains this, so the +exact minimum is eight. + +For $t=1/2$ this settles the seven-call case that +[PR #2112](https://github.com/CrocSwap/integer-mult-bounds/pull/2112) left +open: its bound $7\le\min\le8$ becomes $\min=8$. It also answers the family +question in #2085's open-next-questions for the whole slope family $R_t$. + +## Proof + +Coordinates. Write a symmetric matrix $\begin{pmatrix}a&c\\c&b\end{pmatrix}$ as +$(a-c)A+(b-c)B+2cP$. Then $R_t=(1-t)A+(t^2-t)B+2tP$, and the four target +frames are $A+P$, $2A+B-P$, $B+P$ and $A+2B-P$. + +**Step 1 (exponent support).** Over $\mathbb F_2$, +$I+([F]-1)N=(I+N)+[F]N$. Expanding a product of $k$ such factors gives a sum +over subsets $S$ of calls of $[\sum_{j\in S}F_j]$ times a binary matrix. The +group elements $[x]$ are a basis of $\mathbb F_2[\Lambda_t]$, so the diagonal +entry $[C_i]$ of $T$ forces $C_i=\sum_F n_FF$ with $0\le n_F\le k_F$, where +$k_F$ is the number of calls with label $F$. This is an equality of rational +matrices, not a congruence. + +With $n_R=0$ each target has exactly one such representation: +$A+P$, $A+Q$, $B+P$, $B+Q$. With $n_R\ge1$, the $P$-coordinate equation +$n_P-n_Q+2n_Rt=c_P$ fixes $t$. Enumerating every $n$ with $\sum n_F\le7$ shows +that the only rational $t$ admitting such a representation is $t=0$, where +$R_0=A$. Hence, for $t\ne0$, a word with at most seven calls uses each of +$A,B,P,Q$ at least once. + +**Step 2 (first order).** Let $L$ be a lattice containing all labels and +targets. Modulo the square of the augmentation ideal, a word equal to $T$ +satisfies $\sum_F S_F\otimes\bar F=\sum_iE_{ii}\otimes\bar C_i$ in +$M_4(\mathbb F_2)\otimes L/2L$, where $S_F$ is the sum of the idempotents on +calls labelled $F$. A sum of $k$ rank-one idempotents has rank at most $k$ and +trace $k\bmod2$; write $f(S)$ for the resulting floor. This is the method of +#2085 and #2112. + +**Step 3 (lattice by denominator parity).** Let $t=p/q$ in lowest terms. The +coordinate $t^2-t=p(p-q)/q^2$ has exact denominator $q^2$, so +$\Lambda_t/\Lambda$ is cyclic of order $q^2$, with $\Lambda=\mathbb ZA+\mathbb ZB+\mathbb ZP$. + +- *$q$ odd.* The index is odd, so $\Lambda/2\Lambda\to\Lambda_t/2\Lambda_t$ is + an isomorphism. Two-adically $1-t\equiv1+p$, $t^2-t\equiv0$ and $2t\equiv0$, + so $R_t\equiv A$ ($p$ even) or $R_t\equiv0$ ($p$ odd). In the first case the + calls labelled $A$ or $R_t$ together sum to the old $S_A$; in the second, + $R_t$ calls add cost without first-order effect. Either way the floor is the + #2085 floor $\min_S f(S)+f(S+P_A)+f(S+P_B)+f(S+I)=8$, with + $P_A=\operatorname{diag}(1,0,0,1)$ and $P_B=\operatorname{diag}(0,1,1,0)$. + This case needs no support argument and holds for every word length. +- *$q$ even.* The two-part of $\Lambda_t/\Lambda$ is cyclic and nontrivial, so + $\Lambda/2\Lambda\to\Lambda_t/2\Lambda_t$ has a one-dimensional kernel. The + kernel is spanned by $q^2R_t\bmod 2\Lambda$, whose $B$-coordinate $p(p-q)$ is + odd and whose other coordinates are even: $B\in2\Lambda_t$. So $A,P,R_t$ + give a basis of $\Lambda_t/2\Lambda_t$, $Q\equiv A+P$, and the targets reduce + to $A+P$, $P$, $P$, $A+P$. A word that uses no $R_t$ lies in + $\mathbb F_2[\Lambda]$ and has the #2085 floor of eight. A word that uses + $R_t$ has $S_{R}=0$, so an even number $k_R\ge2$ of $R_t$ calls. By Step 1 + it also has $k_B\ge1$ and $k_A,k_P,k_Q\ge1$. With $g(S)=f(S)$ when $f(S)>0$ + and $g(0)=2$, + $$k_A+k_P+k_Q\ge\min_Sg(S)+g(S+P_A)+g(S+I)=5,$$ + so $k\ge5+2+1=8$. + +The case $t=0$ has odd denominator. This proves the theorem. + +The verifier recomputes every finite input: + +- both first-order minima over all 65,536 masks; +- the support enumeration over all rational $t$; +- the 120 idempotents, each of rank one and trace one; +- the parity classification of $\Lambda_t/2\Lambda_t$ on all 1,431 reduced + $t=p/q$ with $q\le24$ and $|p|\le48$. This is a check on the general + argument above, not its proof. + +It also multiplies the direct eight-call word exactly in the group algebra. +Two controls must fail: dropping one call, and dropping the $P$-bits of roles +2 and 3 from the even-case mask, which lowers that floor from five to three. + +## What is new and what is reused + +The model, target, rank/trace floor and the $t=1/2$ lattice come from Cinna +Davis's #2085 and #2112. #2112 excludes six calls at $t=1/2$ by enumerating +388,800 words; this package does not repeat or check that enumeration. The +new parts are the exponent-support step, which forces a $B$ call that the +first-order relaxation cannot see, the resulting seven-call exclusion, and the +reduction of every rational slope to the two denominator-parity cases. +Expanding a product of such factors over subsets of calls is elementary and +is not claimed as a new technique. + +## Scope + +This is a scoped proof in the formal paid-call model above: all word lengths +for odd-denominator $t$, and all words of at most seven calls for even +denominators (enough for the exact minimum). It does not cover other rank-one +addresses such as scalar multiples $cR_t$, two or more added frames, other +targets, frame construction, addition, precision, or interface charges. It +gives no supplier mapping and no κ change. Python 3.12 is the registered +runtime. The general lattice argument is a hand proof checked on a finite grid, +not a proof-assistant verification. + +## Reproduce + +From the repository root: + +```sh +python3.12 -I -B research/bit-fifth-rational-frame-every-rational-t/verify.py +python3.12 -B scripts/research_package.py --package research/bit-fifth-rational-frame-every-rational-t +``` + +Expected line (under a second): + +```text +PASS_FIFTH_RATIONAL_FRAME_EVERY_T_EXACT_MINIMUM_8 grid_odd=949 grid_even=482 support_exceptions=['0'] idempotents=120 odd_floor=8 even_visible_floor=5 even_total=8 mutated_visible_floor=3 direct_calls=8 +``` + +## Open next questions + +- **Scaled and two-frame alphabets.** Does any rational rank-one address + $c\,v^Tv$ in the symmetric span, or any pair of added frames, lower eight? + The support step still applies. The first step is to classify which + addresses can enter a target's exponent support with at most seven calls. + Only those can matter beyond the first-order floor. +- **Support-plus-first-order as a general screen.** The support step is + valid for any torsion-free address alphabet. Combining it with the + first-order floor may decide other open minimum-length cases in this model + family without enumerating words. The blocker is targets whose supports are + not unique. + +## Credit + +Produced by Nick Petalas. The model, target, rank/trace floor and the +$t=1/2$ instance are Cinna Davis's (1337isnot1337) #2085 and #2112, cited +above and pinned in [SOURCES.json](SOURCES.json). New work is Apache-2.0. diff --git a/research/bit-fifth-rational-frame-every-rational-t/SOURCES.json b/research/bit-fifth-rational-frame-every-rational-t/SOURCES.json new file mode 100644 index 0000000000..731dd16d40 --- /dev/null +++ b/research/bit-fifth-rational-frame-every-rational-t/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/bit-four-register-rational-frame-floor-seed3573e12e/README.md", + "usage": "provenance", + "git_blob": "32f600d6cb56c94f931a4dc98fb97573ecc134f7", + "sha256": "40cbc4ec8e5c49930d7cb8ecf9e462a08266fe604ea426aa5c7b0d5e547fdffd" + }, + { + "path": "research/bit-fifth-rational-frame-six-call-seed0d9888a6/README.md", + "usage": "provenance", + "git_blob": "9784de6be0f4a63995b63bcfa3bf8dacafe65e6b", + "sha256": "df38ee78d19b203a8847cba1342feeeb1d8cbab87fdf7850d3329404bb93183c" + } + ] +} diff --git a/research/bit-fifth-rational-frame-every-rational-t/TASK.json b/research/bit-fifth-rational-frame-every-rational-t/TASK.json new file mode 100644 index 0000000000..a0078c0c76 --- /dev/null +++ b/research/bit-fifth-rational-frame-every-rational-t/TASK.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "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_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "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": "For the four-role target diag([A+P],[A+Q],[B+P],[B+Q]) of PR #2085 and the five-address alphabet {A,B,P,Q,R_t}, R_t=(1,t)^T(1,t), with paid factors I+([F]-1)N over all rank-one idempotents N in M4(F2), determine the exact paid-call minimum for every rational t. This settles the seven-call case left open by PR #2112 at t=1/2.", + "scope_change_reason": "The card permits a specified legal operation alphabet. This keeps the four roles, target and model of PRs #2085/#2112 and answers their stated open questions (the R_t slope family and the seven-call case) instead of searching a new alphabet.", + "bottleneck_link": "Side result for the bit primitive in a favorable formal paid-call model: it removes one candidate saving route (a fifth symmetric rank-one frame) for this target. The selected result's complex primitive still binds; no supplier or kappa change follows.", + "budget_minutes": 60, + "stop_rule": "Stop once the exact minimum is decided for every rational t; do not extend to scaled frames or two added frames in this session.", + "outcome": "completed", + "evidence": "Exponent support: each target frame must equal a nonnegative subset sum of the word's labels; with at most seven calls R_t can enter such a sum only at t=0, so for t!=0 each of A,B,P,Q is used. First order: for odd-denominator t, L/2L is the old lattice mod 2 and R_t is A or 0, giving the PR #2085 floor 8 at every length. For even-denominator t, B lies in 2L, A,P,R_t give a basis mod 2, and a word using R_t needs an even number (>=2) of R_t calls, at least one B call and at least 5 A/P/Q calls (exact minimum over 65,536 masks), so at least 8. The direct eight-call word attains 8.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a scaled rational rank-one address c v^T v, or a pair of added frames, lower the eight-call minimum for this target?", + "why_it_matters": "This package closes only the one-parameter slope family R_t; the support step suggests that only addresses entering a target's exponent support can matter.", + "first_step": "Classify the addresses that can appear in a nonnegative support of a target frame using at most seven calls, then apply the first-order floor to those alone.", + "blocked_by": "Two added frames can make target supports non-unique, so the forced-label count used here no longer follows." + }, + { + "question": "Does exponent support plus the first-order floor decide other open minimum-length cases in torsion-free address models?", + "why_it_matters": "It replaces word enumeration by a small exact computation when target supports are unique.", + "first_step": "Apply the two screens to a recorded open minimum-length case with a torsion-free address group.", + "blocked_by": "Targets with several supports and finite (torsion) address groups, where the support step is weaker." + } + ] +} diff --git a/research/bit-fifth-rational-frame-every-rational-t/VERIFY.json b/research/bit-fifth-rational-frame-every-rational-t/VERIFY.json new file mode 100644 index 0000000000..a8e052a231 --- /dev/null +++ b/research/bit-fifth-rational-frame-every-rational-t/VERIFY.json @@ -0,0 +1,19 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Frame identities; parity classification of L/2L on 1,431 reduced slopes; exact exponent-support enumeration over all rational t (exceptions {0}); 120 idempotents; rank/trace first-order minima over all 65,536 masks (odd 8, even visible 5); direct eight-call word in the exact group algebra; dropped-call and mutated-mask controls." + } + ] +} diff --git a/research/bit-fifth-rational-frame-every-rational-t/verify.py b/research/bit-fifth-rational-frame-every-rational-t/verify.py new file mode 100644 index 0000000000..c58b77843e --- /dev/null +++ b/research/bit-fifth-rational-frame-every-rational-t/verify.py @@ -0,0 +1,378 @@ +#!/usr/bin/env python3 +"""Exact eight-call minimum for the fifth rational frame R_t, every rational t. + +Model (PR #2085 / PR #2112): four roles, target diag([A+P],[A+Q],[B+P],[B+Q]), +paid factors I + ([F]-1)N with F in {A,B,P,Q,R_t}, R_t = (1,t)^T(1,t), and N a +rank-one idempotent in M4(F2). The proof in README.md has three finite inputs, +each recomputed here: + +1. lattice: the images of the labels and targets in L/2L, L = ZA+ZB+ZP+ZR_t, + depend only on the parity of the denominator of t (checked on a grid; the + general argument is in the README); +2. support: every monomial of an expanded word has exponent equal to a subset + sum of its labels, so each target frame is such a sum; with at most seven + calls, R_t occurs in such a sum only at t = 0 (exact, all rational t); +3. first order: rank/trace floors over all 65,536 binary 4x4 masks. + +Positive control: the direct eight-call word, multiplied exactly in F2[L]. +Prepared by Nick Petalas. Apache-2.0. +""" + +from __future__ import annotations + +import itertools +import math +import sys +from fractions import Fraction as Fr + +ROLES = 4 +MAX_CALLS = 7 + +# Symmetric 2x2 rational matrices [[a, c], [c, b]] in the basis (A, B, P), +# where A = E11, B = E22, P = (1/2)[[1,1],[1,1]]: coordinates (a-c, b-c, 2c). +A = (Fr(1), Fr(0), Fr(0)) +B = (Fr(0), Fr(1), Fr(0)) +P = (Fr(0), Fr(0), Fr(1)) +Q = (Fr(1), Fr(1), Fr(-1)) # Q = A + B - P + + +def vadd(*vs): + return tuple(sum(x) for x in zip(*vs)) + + +def vscale(k, v): + return tuple(k * x for x in v) + + +def r_frame(t: Fr): + """R_t = (1,t)^T(1,t) = [[1,t],[t,t^2]] in (A,B,P) coordinates.""" + return (1 - t, t * t - t, 2 * t) + + +def as_matrix(v): + a, b, p = v + return ((a + p / 2, p / 2), (p / 2, b + p / 2)) + + +TARGETS = (vadd(A, P), vadd(A, Q), vadd(B, P), vadd(B, Q)) + + +def check(cond: bool, msg: str) -> None: + if not cond: + raise SystemExit(f"FAIL: {msg}") + + +# ---------------------------------------------------------------- frames ---- + +def check_frames() -> None: + expect = { + "A": ((1, 0), (0, 0)), + "B": ((0, 0), (0, 1)), + "P": ((Fr(1, 2), Fr(1, 2)), (Fr(1, 2), Fr(1, 2))), + "Q": ((Fr(1, 2), Fr(-1, 2)), (Fr(-1, 2), Fr(1, 2))), + } + for name, v in zip("ABPQ", (A, B, P, Q)): + check(as_matrix(v) == expect[name], f"frame {name}") + for t in (Fr(1, 2), Fr(-3, 4), Fr(5, 6), Fr(2, 3), Fr(7)): + m = as_matrix(r_frame(t)) + check(m == ((1, t), (t, t * t)), f"R_t matrix at t={t}") + check(m[0][0] * m[1][1] - m[0][1] * m[1][0] == 0, "R_t rank one") + dets = [as_matrix(c) for c in TARGETS] + for m in dets: + check(m[0][0] * m[1][1] - m[0][1] ** 2 == Fr(1, 2), "target det 1/2") + + +# --------------------------------------------------------------- lattice ---- + +def integer_basis(rows): + """Row-reduce integer vectors to a basis of their Z-span (echelon form).""" + rows = [list(r) for r in rows if any(r)] + basis = [] + col = 0 + ncols = len(rows[0]) if rows else 0 + while rows and col < ncols: + piv = [r for r in rows if r[col] != 0] + rest = [r for r in rows if r[col] == 0] + while len(piv) > 1: + piv.sort(key=lambda r: abs(r[col])) + head = piv[0] + new = [head] + for r in piv[1:]: + k = r[col] // head[col] + r = [x - k * y for x, y in zip(r, head)] + if r[col] != 0: + new.append(r) + elif any(r): + rest.append(r) + piv = new + if piv: + basis.append(piv[0]) + rows = [r for r in rest if any(r)] + col += 1 + return basis + + +def solve3(basis, v): + """Coordinates of v in a 3x3 rational basis (rows), by Cramer's rule.""" + def det(m): + return (m[0][0] * (m[1][1] * m[2][2] - m[1][2] * m[2][1]) + - m[0][1] * (m[1][0] * m[2][2] - m[1][2] * m[2][0]) + + m[0][2] * (m[1][0] * m[2][1] - m[1][1] * m[2][0])) + cols = [list(c) for c in zip(*basis)] # columns = basis vectors + d = det(cols) + out = [] + for i in range(3): + m = [row[:] for row in cols] + for r in range(3): + m[r][i] = v[r] + out.append(Fr(det(m), d)) + return out + + +def mod2_images(t: Fr): + """Images in L/2L (L = span of A,B,P,R_t) of the five labels and targets.""" + labels = {"A": A, "B": B, "P": P, "Q": Q, "R": r_frame(t)} + den = math.lcm(*(x.denominator for v in labels.values() for x in v)) + ints = [[int(x * den) for x in v] for v in labels.values()] + basis = integer_basis(ints) + check(len(basis) == 3, f"rank-three lattice at t={t}") + + def image(v): + coords = solve3(basis, [x * den for x in v]) + check(all(c.denominator == 1 for c in coords), f"lattice membership t={t}") + return tuple(int(c) % 2 for c in coords) + + return ({k: image(v) for k, v in labels.items()}, + [image(c) for c in TARGETS]) + + +def gf2_rank_vectors(vs): + rows = [int("".join(map(str, v)), 2) for v in vs] + rank = 0 + for bit in reversed(range(3)): + piv = next((r for r in rows if r >> bit & 1), None) + if piv is None: + continue + rank += 1 + rows = [r ^ piv if r >> bit & 1 else r for r in rows if r != piv] + return rank + + +def xor(u, v): + return tuple(a ^ b for a, b in zip(u, v)) + + +def check_lattice_grid(): + """Parity classification of L/2L on all t = p/q, 1<=q<=24, |p|<=48.""" + cases = {"odd": 0, "even": 0} + for q in range(1, 25): + for p in range(-48, 49): + if math.gcd(p, q) != 1: + continue + t = Fr(p, q) + img, tgt = mod2_images(t) + if q % 2: + # Inclusion ZA+ZB+ZP -> L is an isomorphism mod 2. + check(gf2_rank_vectors([img["A"], img["B"], img["P"]]) == 3, + f"odd q: A,B,P basis mod 2 at t={t}") + check(img["Q"] == xor(xor(img["A"], img["B"]), img["P"]), "Q odd") + want_r = img["A"] if p % 2 == 0 else (0, 0, 0) + check(img["R"] == want_r, f"odd q: R image at t={t}") + check(tgt == [xor(img["A"], img["P"]), xor(img["A"], img["Q"]), + xor(img["B"], img["P"]), xor(img["B"], img["Q"])], + "odd q: targets") + cases["odd"] += 1 + else: + check(img["B"] == (0, 0, 0), f"even q: B in 2L at t={t}") + check(gf2_rank_vectors([img["A"], img["P"], img["R"]]) == 3, + f"even q: A,P,R basis mod 2 at t={t}") + ap = xor(img["A"], img["P"]) + check(img["Q"] == ap, f"even q: Q = A+P mod 2L at t={t}") + check(tgt == [ap, img["P"], img["P"], ap], f"even q: targets t={t}") + cases["even"] += 1 + return cases + + +# --------------------------------------------------------------- support ---- + +def support_exceptions(): + """All rational t where a target is a nonnegative sum of <=7 labels using R_t. + + For n_R >= 1 the P-coordinate equation n_P - n_Q + 2 n_R t = c_P fixes t, + so the enumeration covers every rational t exactly. + """ + exceptional = {} + no_r_reps = {i: [] for i in range(ROLES)} + for n in itertools.product(range(MAX_CALLS + 1), repeat=5): + if sum(n) > MAX_CALLS: + continue + na, nb, np_, nq, nr = n + for i, c in enumerate(TARGETS): + if nr == 0: + s = vadd(vscale(na, A), vscale(nb, B), vscale(np_, P), vscale(nq, Q)) + if s == c: + no_r_reps[i].append(n) + continue + t = Fr(c[2] - np_ + nq, 2 * nr) + s = vadd(vscale(na, A), vscale(nb, B), vscale(np_, P), vscale(nq, Q), + vscale(nr, r_frame(t))) + if s == c: + exceptional.setdefault(t, []).append((i, n)) + return exceptional, no_r_reps + + +# ----------------------------------------------------------- first order ---- + +def gf2_rank_matrix(rows): + rows = list(rows) + rank = 0 + for bit in range(ROLES): + piv = next((r for r in rows if r >> bit & 1), None) + if piv is None: + continue + rank += 1 + rows = [r ^ piv if r >> bit & 1 else r for r in rows if r != piv] + return rank + + +def mask_rows(m): + return [(m >> (ROLES * i)) & 0xF for i in range(ROLES)] + + +def diag(bits): + return sum(1 << (ROLES * i + i) for i, b in enumerate(bits) if b) + + +RANK = [0] * (1 << 16) +TRACE = [0] * (1 << 16) + + +def fill_tables(): + for m in range(1 << 16): + rows = mask_rows(m) + RANK[m] = gf2_rank_matrix(rows) + TRACE[m] = sum(rows[i] >> i & 1 for i in range(ROLES)) & 1 + + +def f_floor(m): + """Fewest rank-one idempotents with sum m (rank and trace parity).""" + r = RANK[m] + return r + ((r - TRACE[m]) & 1) + + +def g_floor(m): + """Same, when the label must occur at least once.""" + v = f_floor(m) + return v if v else 2 + + +def check_idempotents(): + count = 0 + for x in range(1, 16): + for y in range(1, 16): + if bin(x & y).count("1") & 1: + m = sum(((x >> i & 1) * y) << (ROLES * i) for i in range(ROLES)) + check(RANK[m] == 1 and TRACE[m] == 1, "idempotent rank/trace") + count += 1 + check(count == 120, "120 rank-one idempotents") + return count + + +PA = diag((1, 0, 0, 1)) +PB = diag((0, 1, 1, 0)) +PI = diag((1, 1, 1, 1)) + + +def odd_floor(): + return min(f_floor(s) + f_floor(s ^ PA) + f_floor(s ^ PB) + f_floor(s ^ PI) + for s in range(1 << 16)) + + +def even_floor(m1=PA, m2=PI): + return min(g_floor(s) + g_floor(s ^ m1) + g_floor(s ^ m2) + for s in range(1 << 16)) + + +# ------------------------------------------------------- positive control ---- + +def ga_mul(x, y): + out = set() + for a in x: + for b in y: + out ^= {vadd(a, b)} + return frozenset(out) + + +ZERO = (Fr(0), Fr(0), Fr(0)) +ONE = frozenset({ZERO}) +NULL = frozenset() + + +def factor(label, role): + m = [[ONE if i == j else NULL for j in range(ROLES)] for i in range(ROLES)] + m[role][role] = frozenset({label}) + return m + + +def mat_mul(x, y): + out = [] + for i in range(ROLES): + row = [] + for j in range(ROLES): + acc = set() + for k in range(ROLES): + acc ^= set(ga_mul(x[i][k], y[k][j])) + row.append(frozenset(acc)) + out.append(row) + return out + + +def word_product(word): + m = [[ONE if i == j else NULL for j in range(ROLES)] for i in range(ROLES)] + for label, role in word: + m = mat_mul(m, factor(label, role)) + return m + + +def target_matrix(): + return [[frozenset({TARGETS[i]}) if i == j else NULL for j in range(ROLES)] + for i in range(ROLES)] + + +def main() -> int: + check_frames() + cases = check_lattice_grid() + exceptional, no_r = support_exceptions() + check(set(exceptional) == {Fr(0)}, f"exceptional set {sorted(exceptional)}") + expect_reps = {0: (1, 0, 1, 0, 0), 1: (1, 0, 0, 1, 0), + 2: (0, 1, 1, 0, 0), 3: (0, 1, 0, 1, 0)} + for i in range(ROLES): + check(no_r[i] == [expect_reps[i]], f"unique R-free support of role {i}") + + fill_tables() + idem = check_idempotents() + f8 = odd_floor() + check(f8 == 8, f"odd-denominator first-order floor {f8}") + g5 = even_floor() + check(g5 == 5, f"even-denominator visible floor {g5}") + even_total = g5 + 2 + 1 # two R calls with zero sum, at least one B call + check(even_total == 8, "even-denominator total") + # Control: dropping the P-coordinate bits of roles 2 and 3 lowers the + # visible floor, so those mask bits are live. + mutated = even_floor(m2=diag((1, 1, 0, 0))) + check(mutated < g5, "mutated mask lowers the floor") + + direct = [(A, 0), (P, 0), (A, 1), (Q, 1), (B, 2), (P, 2), (B, 3), (Q, 3)] + check(word_product(direct) == target_matrix(), "direct eight-call word") + check(word_product(direct[:-1]) != target_matrix(), "dropped call fails") + + print("PASS_FIFTH_RATIONAL_FRAME_EVERY_T_EXACT_MINIMUM_8 " + f"grid_odd={cases['odd']} grid_even={cases['even']} " + f"support_exceptions={sorted(str(t) for t in exceptional)} " + f"idempotents={idem} odd_floor={f8} even_visible_floor={g5} " + f"even_total={even_total} mutated_visible_floor={mutated} direct_calls=8") + return 0 + + +if __name__ == "__main__": + sys.exit(main())