diff --git a/research/a5-rank-cap-threshold/PROOF.md b/research/a5-rank-cap-threshold/PROOF.md new file mode 100644 index 0000000000..97563c6814 --- /dev/null +++ b/research/a5-rank-cap-threshold/PROOF.md @@ -0,0 +1,134 @@ +# Sharp rank cap for the A5 conjugate-pair word + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Contract and theorem + +Let K be any field and V any finite-dimensional K-vector space. Work in the +full formal matrix algebra End_K(V)[A5], with scalar operators commuting with +group basis elements. Set x=(12)(34) and y=(135), with right-to-left permutation +composition. Let P,Q be nonzero idempotents with PQ=QP=0, of ranks r,s. +All of V has arbitrary initial data; the complementary space is restored. +For each g in {x,y}, one paid call is + +```text +F_g(N) = I + ([g]-[e])N, N^2=N, 1 <= rank(N) <= h. +T = I + ([xy]-[e])P + ([yx]-[e])Q. +``` + +Let h be a positive integer with h >= max(r,s). The exact minimum number +of paid calls for T is + +```text +3, if h >= r+s; +4, if max(r,s) <= h < r+s. +``` + +This holds with any finite number of additional restored dirty roles and with +arbitrary free scalar GL(V) maps. It counts paid calls only. It assigns no +physical or recursive price to a higher-rank call or to scalar mixing. + +## Attribution and new step + +Wentao Li's #4089 proves the binary r=s=h=1 case at arbitrary role count, +following Cinna Davis's #2246 finite-width result and question. In particular, +the support filter and the forced middle matrix P+Q in that special case +are predecessor ideas. We cite them without replaying their implementations. +The new step changes the paid alphabet: higher-rank idempotents are legal. +It gives the exact three/four-call transition for arbitrary r,s over every +field, together with an attaining three-call construction. It does not claim +that the rank-one lower-bound method or coordinate batching is new. + +## Free scalar maps + +Move any scalar GL(V) maps through the paid factors by conjugation. +Conjugation preserves idempotence and rank. The group-algebra augmentation +maps each [g] to 1, hence sends each paid factor and T to I. Therefore the +residual scalar map is I. A normalized paid word suffices for the lower bound; +the literal scalar maps and their physical costs are not classified. + +## Support lower bound + +Every group label in a product expansion is an ordered subsequence of its +paid labels. No word of length at most two has both xy and yx in its support. +Among the eight length-three words over {x,y}, only xyx and yxy do. This is a +finite permutation statement for these particular x,y, independent of K and +V. The verifier checks all fifteen label words of length zero through three +by expanding every ordered subsequence. Since P and Q are nonzero and xy,yx +are distinct group elements, T requires both coefficients. Thus at least +three paid calls are necessary. A direct hand check of the full-length +products is xxx=x, xxy=y, xyy=xy^2, yxx=y, yyx=y^2x and yyy=e for the six +nonalternating words. Their proper subsequences contain at most one of xy,yx; +direct permutation multiplication gives xy^2 != yx and y^2x != xy. +The two alternating words contain both xy and yx as length-two subsequences. + +## Every three-call word pays middle rank r+s + +Consider F_x(A)F_y(B)F_x(C). Write each factor as (I-N)+[g]N. +The labels xyx, xy, yx and y have the following coefficients: + +```text +[xyx] ABC +[xy] AB-ABC +[yx] BC-ABC +[y] B-AB-BC+ABC. +``` + +These four group elements are distinct; xyx and y are absent from T. +Matching coefficients gives ABC=0, AB=P, BC=Q, and then B=P+Q. +All identities use integer coefficients and subtraction only, so they hold +in every characteristic. We did not assume that A,B,C are idempotent or +that any factor is invertible in this necessity argument. + +For F_y(A)F_x(B)F_y(C), use the distinct labels yxy, xy, yx and x: + +```text +[yxy] ABC +[xy] BC-ABC +[yx] AB-ABC +[x] B-AB-BC+ABC. +``` + +They give ABC=0, BC=P, AB=Q and again B=P+Q. + +Because P,Q are orthogonal idempotents, V is the direct sum of im P, +im Q and ker P intersect ker Q. The map P+Q is identity on the first two +summands and zero on the third. Hence rank(B)=rank(P+Q)=r+s. A cap below r+s +therefore excludes every three-call implementation, including arbitrary +noncoordinate couplings and restored spectators. + +## Attainment + +The direct four-call word is + +```text +F_x(P) F_y(P) F_y(Q) F_x(Q) = T. +``` + +Each coupling has rank r or s, so it is legal for h>=max(r,s). +When h>=r+s, the shorter word is + +```text +F_x(P) F_y(P+Q) F_x(Q) = T. +``` + +On im P it acts by xy; on im Q it acts by yx; on the common kernel it is +identity. P+Q is itself idempotent. Its ranks are r,r+s,s, so every call +is legal exactly at the stated sufficient cap. The reversed alternating +word F_y(Q)F_x(P+Q)F_y(P) also attains T. These are full operator identities, +not target-row observations or finite-column assumptions. + +Both the four-call word and the three-call word have total coupling rank +2(r+s). Thus one paid-call overhead disappears at this rank threshold, but +the proof makes no claim of lower total rank mass, native speed or kappa. +Together with the lower bounds this proves the theorem. Stop here. + +## Limits + +The theorem requires full formal group-algebra equality, these two labels, +orthogonal idempotent target blocks and h>=max(r,s). It does not determine +the optimum when a target block itself exceeds the cap, a minimum under an +arbitrary rank-dependent tariff, or a physical implementation cost. The +necessity proof applies even to non-idempotent paid couplings, but the +specified legal alphabet and the attaining constructions use idempotents. +Independent human and formal proof-kernel review are unclaimed. diff --git a/research/a5-rank-cap-threshold/README.md b/research/a5-rank-cap-threshold/README.md new file mode 100644 index 0000000000..3bf27da736 --- /dev/null +++ b/research/a5-rank-cap-threshold/README.md @@ -0,0 +1,138 @@ +# Sharp A5 three-call rank threshold + +For every field and every finite dirty role space, the A5 conjugate-pair +operator with two orthogonal target blocks of ranks r,s has exact paid-call +minimum three when the allowed coupling rank h is at least r+s, and four +when max(r,s)<=h 0 and s > 0, "nonzero targets") + return r, s + + +def minimum(p, q, cap, prime): + r, s = valid_pair(p, q, prime) + need(type(cap) is int and cap >= max(r, s), "cap domain") + return 3 if cap >= r + s else 4 + + +def three_word(p, q, prime): + return ((X, p), (Y, add(p, q, prime)), (X, q)) + + +def four_word(p, q): + return ((X, p), (Y, p), (Y, q), (X, q)) + + +def support_check(): + """Independent ordered-subsequence expansion of all short label words.""" + hits = [] + for length in range(4): + for labels in itertools.product((X, Y), repeat=length): + support = set() + for mask in range(1 << length): + g = IDENTITY + for i in range(length): + if mask >> i & 1: + g = compose(g, labels[i]) + support.add(g) + if {compose(X, Y), compose(Y, X)} <= support: + hits.append(labels) + need(hits == [(X, Y, X), (Y, X, Y)], "short support patterns") + return {"short_label_words": 15, "admissible_support_patterns": 2} + + +def idempotents_two(prime): + result = [] + for entries in itertools.product(range(prime), repeat=4): + matrix = (entries[:2], entries[2:]) + if multiply(matrix, matrix, prime) == matrix: + result.append(matrix) + need(len(result) == prime * (prime + 1) + 2, "idempotent inventory") + return result + + +def census(prime): + """Full endpoint oracle; it does not use the middle-coupling argument.""" + matrices = idempotents_two(prime) + targets = {} + for p in matrices: + if rank(p, prime) == 1: + q = add(eye(2), p, prime, -1) + targets[tuple(sorted(target(p, q, prime).items()))] = (p, q) + hits = [] + words = 0 + for labels in itertools.product((X, Y), repeat=3): + for couplings in itertools.product(matrices, repeat=3): + state = word_endpoint(tuple(zip(labels, couplings)), prime, 2) + key = tuple(sorted(state.items())) + words += 1 + if key in targets: + p, q = targets[key] + need(couplings[1] == eye(2), "attaining middle rank") + expected = (p, eye(2), q) if labels == (X, Y, X) else (q, eye(2), p) + need(couplings == expected, "complete attaining triple") + hits.append((labels, couplings)) + need(len(hits) == 2 * prime * (prime + 1), "attainment count") + return {"field": prime, "idempotents": len(matrices), "words": words, + "targets": len(targets), "three_call_hits": len(hits)} + + +def conjugated_pair(n, r, s, prime): + """Explicit oblique projectors, with no enumeration or random choices.""" + p = tuple(tuple(int(i == j and i < r) for j in range(n)) for i in range(n)) + q = tuple(tuple(int(i == j and r <= i < r + s) for j in range(n)) + for i in range(n)) + for k in range(2 * n): + i, j = k % n, (k + 1) % n + amount = (k + 1) if prime else Fraction(k + 1, k + 2) + e = tuple(tuple(amount if (a, b) == (i, j) else 0 for b in range(n)) + for a in range(n)) + forward, inverse = add(eye(n), e, prime), add(eye(n), e, prime, -1) + need(multiply(forward, inverse, prime) == eye(n), "conjugator inverse") + p = multiply(multiply(forward, p, prime), inverse, prime) + q = multiply(multiply(forward, q, prime), inverse, prime) + return p, q + + +def endpoint_fixtures(): + count, controls = 0, 0 + for prime in (0, 2, 3, 5, 7): + for n, r, s in ((2, 1, 1), (3, 1, 1), (4, 1, 2), (5, 2, 2), + (6, 2, 3), (8, 3, 4)): + p, q = conjugated_pair(n, r, s, prime) + expected = target(p, q, prime) + for word in (three_word(p, q, prime), four_word(p, q)): + need(word_endpoint(word, prime, n) == expected, "full dirty endpoint") + count += 1 + for index in range(len(word)): + mutant = word[:index] + word[index + 1:] + need(word_endpoint(mutant, prime, n) != expected, "omission control") + controls += 1 + need(minimum(p, q, r + s, prime) == 3, "rank threshold upper side") + need(minimum(p, q, max(r, s), prime) == 4, "rank threshold lower side") + need(rank(add(p, q, prime), prime) == r + s, "rank additivity") + return {"complete_endpoints": count, "omission_controls": controls, + "oblique_pairs": count // 2} + + +def regular_action_check(): + """Act directly on all regular-module basis columns, without formal products.""" + group = [] + for g in itertools.permutations(range(5)): + inversions = sum(g[i] > g[j] for i in range(5) for j in range(i + 1, 5)) + if inversions % 2 == 0: + group.append(g) + need(len(group) == 60, "even permutation group") + n = 4 + p, q = conjugated_pair(n, 1, 2, 3) + endpoint = target(p, q, 3) + columns = 0 + for word in (three_word(p, q, 3), four_word(p, q)): + for source in range(n): + for address in group: + values = {(source, address): 1} + for label, coupling in reversed(word): + updated = dict(values) + for (j, g), value in values.items(): + for i in range(n): + coefficient = value * coupling[i][j] + for dest, sign in ((g, -1), (compose(label, g), 1)): + key = (i, dest) + updated[key] = (updated.get(key, 0) + sign * coefficient) % 3 + values = {key: v for key, v in updated.items() if v} + expected = {} + for g, coefficient in endpoint.items(): + for i in range(n): + if coefficient[i][source]: + expected[i, compose(g, address)] = coefficient[i][source] + need(values == expected, "literal regular-action column") + columns += 1 + return {"regular_action_basis_columns": columns} + + +def invalid_controls(): + p = ((1, 0), (0, 0)) + q = ((0, 0), (0, 1)) + tests = ((p, q, 0), (p, q, True), (p, p, 2), (zero(2), q, 2), + (((0, 1), (0, 0)), q, 2), (p, ((1,),), 2)) + for a, b, cap in tests: + try: + minimum(a, b, cap, 3) + except ValueError: + continue + raise ValueError("invalid input was accepted") + p3 = ((1, 0, 0), (0, 0, 0), (0, 0, 0)) + q3 = ((0, 0, 0), (0, 1, 0), (0, 0, 0)) + h3 = ((0, 0, 0), (0, 0, 0), (0, 0, 1)) + bad = three_word(p3, q3, 3) + ((X, h3),) + need(word_endpoint(bad, 3, 3) != target(p3, q3, 3), "dirty spectator control") + return {"invalid_input_controls": len(tests), "spectator_control": 1} + + +def main(): + evidence = {"support": support_check(), "censuses": [census(p) for p in (3, 5)], + "fixtures": endpoint_fixtures(), "regular": regular_action_check(), + "controls": invalid_controls()} + root = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + hashes = {name: hashlib.sha256((root / name).read_bytes()).hexdigest() for name in names} + print("PASS_A5_RANK_CAP_THRESHOLD " + json.dumps({"evidence": evidence, "sha256": hashes}, + sort_keys=True)) + + +if __name__ == "__main__": + main()