diff --git a/research/ut4-hyperbolic-middle-floor/PROOF.md b/research/ut4-hyperbolic-middle-floor/PROOF.md new file mode 100644 index 0000000000..9f448b55bb --- /dev/null +++ b/research/ut4-hyperbolic-middle-floor/PROOF.md @@ -0,0 +1,138 @@ +# Sharp central-target tariffs from a paired middle quotient + +This scoped written proof was produced by Nick Petalas. Apache-2.0. + +## Statement and inherited model + +Use ToikY's [PR1662](https://github.com/CrocSwap/integer-mult-bounds/pull/1662) +formal model. Let G=UT4(F2), with a=I+E12, b=I+E23, c=I+E34 and +z=I+E14. On any finite r>=w>=1 roles, every paid factor is + + I_r + ([g]+1) x y^T, g in {a,b,c}, x,y nonzero in F2^r. + +Both idempotent and nilpotent scalar couplings are allowed. The complete +endpoint is I_r+([z]+1)P, where P=diag(I_w,0), or any common scalar +conjugate of that projector. Every role has arbitrary input, every extra +role is restored, and all paid factors, including restoration, are counted. +Interleaved free scalar GL_r(F2) mixing normalizes into the couplings as in +PR1662. Augmentation forces the final free scalar map to be identity. +There are no other free address operations, COPY, ERASE or initialized roles. + +Every such word satisfies the new bound + + n_b >= 2w + rank(X_b) + rank(Y_b) >= 4w. + +Together with PR1662's n_a,n_c>=2w, and its direct word, this gives the +exact complete tariff for all nonnegative uniform per-letter prices: + + min cost = 2w alpha + 4w beta + 2w gamma. + +In particular, the unit minimum is 8w for every finite dirty workspace. +The theorem excludes the (2,3) and (3,2) seven-b cases left open by Victor +Li's [PR3938](https://github.com/CrocSwap/integer-mult-bounds/pull/3938). +It also supplies a direct algebraic exclusion of every n_b<4w case. +No chronological search or predecessor census is a premise of this proof. + +## Coefficient premises + +We use PR1662's fixed degree-three algebra homomorphism + + F2[G] -> Q = F2/(A^2,B^2,C^2,AC-CA, degree>=4), + [a] -> 1+A, [b] -> 1+B, [c] -> 1+C, + [z] -> 1+ABC+ACB+BAC+CBA. + +Its fixed homomorphism lemma and the outer-letter span bound are credited +premises, not new audit deliverables. Q has the basis + + 1,A,B,C,AB,AC,BA,BC,CB,ABA,ABC,ACB,BAB,BAC,BCB,CBA,CBC. + +For a scalar-matrix word, write H_s for the coefficient of a basis +monomial s in its product over Q. Since ABA, ABC, CBA and CBC have no +alternative representative from AC=CA, each is the literal ordered +subsequence sum with those three labels. The endpoint therefore implies + + H_B=H_AB=H_CB=H_BA=H_BC=0, + H_ABA=H_CBC=0, H_ABC=H_CBA=P. (1) + +All equations hold as full r-by-r matrices, including every dirty block. + +## The new paired factorization + +Number the n=n_b middle calls in product order. Write their couplings as +B_j=x_j y_j^T and put + + X = [x_1 ... x_n], Y = [y_1^T; ...; y_n^T]. + +For each middle call j, let A_j^- and C_j^- be the sums of the a and c +couplings strictly before it. Let A_j^+ and C_j^+ be the corresponding +sums strictly after it. Define + + U_A = [A_j^- x_j]_j, V_A = [y_j^T A_j^+]_j, + U_C = [C_j^- x_j]_j, V_C = [y_j^T C_j^+]_j, + U = [U_A; U_C], V = [V_A V_C]. + +Here X has shape r-by-n, Y has shape n-by-r, U has shape 2r-by-n, +and V has shape n-by-2r. Distributivity in the original chronological +order, without commuting scalar matrices, gives + + XY = H_B, + UY = [H_AB; H_CB], + XV = [H_BA H_BC], + UV = [ H_ABA H_ABC ] = [ 0 P ]. + [ H_CBA H_CBC ] [ P 0 ] (2) + +For example, every term in U_A V_C chooses one a call before middle call +j and one c call after it, so it contributes exactly once to H_ABC. +The same expansion gives the other three blocks. No assumption that an +a prefix equals its suffix is needed. + +By (1), XY=UY=XV=0. Thus im(Y) is a subspace of ker(X), V takes values +in ker(X), and U vanishes on im(Y). The product UV factors through + + ker(X)/im(Y), dimension n-rank(X)-rank(Y). + +The matrix on the right of (2) has rank 2 rank(P)=2w: its two image +blocks are separate copies of im(P). Therefore + + 2w <= n-rank(X)-rank(Y). (3) + +This is the new step. Keeping only H_ABC uses a rank-w product and gives +the weaker middle quotient bound in PR1662. The zero ABA and CBC blocks +allow both cross coefficients to contribute their ranks simultaneously. + +For completeness, PR1662's remaining middle span argument is short. +The H_BAC coefficient also includes the BCA subsequences because AC=CA. +Every summand starts with a b coupling. Its image is consequently in +im(X). Since H_BAC=P, rank(X)>=w. Similarly H_ACB includes CAB, every +summand ends with a b coupling, and its row space lies in row(Y). +Since H_ACB=P, rank(Y)>=w. Substitution in (3) proves n_b>=4w. + +## Attainment and exact weighted optimum + +PR1662's direct group word (abcb)^2=z has counts (2,4,2). +On one coordinate role the scalar coupling is the coordinate projector, +so the same word acts by z on that role and by identity on all others. +Use it separately on all w active roles. The resulting word has counts +(2w,4w,2w), implements the complete formal endpoint, and restores every +dirty role. A common free scalar conjugation gives any conjugate P. + +The inherited outer bounds n_a,n_c>=2w and the new n_b>=4w hold +simultaneously for every word. The direct word attains them simultaneously, +so its tariff is minimal for any nonnegative alpha,beta,gamma. This +conclusion permits zero prices, but still concerns finite words only. +It does not price role-dependent calls or a physical implementation. + +## Evidence and limitations + +The universal statement is the written factorization and dimension argument. +The local verifier checks the new paired identity by two different finite +calculations: polynomial coefficient expansion and prefix/suffix arrays. +It checks attaining words against the full 64-element group algebra. +No predecessor program or stored census is imported or executed. + +The result is a scoped proof in this formal operation alphabet. It is not +a native supplier, a rational-frame identity or a complete multiplication +theorem. Common-label compilation, physical realization, stock, precision, +tape, analytic recovery and all five selected framework assumptions remain +separate. No new kappa or selected-frontier change is claimed. Independent +human and formal proof-kernel review are unclaimed. diff --git a/research/ut4-hyperbolic-middle-floor/README.md b/research/ut4-hyperbolic-middle-floor/README.md new file mode 100644 index 0000000000..b427d157ba --- /dev/null +++ b/research/ut4-hyperbolic-middle-floor/README.md @@ -0,0 +1,110 @@ +# Exact central UT4 tariffs for every restored dirty workspace + +This contribution was produced by Nick Petalas. Apache-2.0. + +Scoped proof: in ToikY's PR1662 formal F2[UT4(F2)] model, w central +targets require at least 4w paid b calls, for every finite number of +arbitrary restored dirty roles. The stronger bound is + + n_b >= 2w + rank(X_b) + rank(Y_b). + +With the credited outer bounds and direct construction, the exact complete +tariff is 2w alpha+4w beta+2w gamma for all nonnegative uniform letter +prices. The unit minimum is 8w. In particular, neither remaining +seven-b rank pattern, (2,3) or (3,2), can realize two central targets. +This settles the mixed-rank question in Victor Li's +[PR3938](https://github.com/CrocSwap/integer-mult-bounds/pull/3938). + +The new step stacks both a/c prefix maps and concatenates both suffix +maps. Their product is [[0,P],[P,0]], of rank 2w, and factors through +ker(X_b)/im(Y_b). [PROOF.md](PROOF.md) gives the full argument. +The lower bound already holds in the retained degree-three quotient; +no larger census or higher coefficient is needed. No new kappa or +selected-frontier change is claimed. + +## Reproduce + +From the worktree root with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/ut4-hyperbolic-middle-floor/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/ut4-hyperbolic-middle-floor +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/ut4-hyperbolic-middle-floor --check-source-history +``` + +Other machines may substitute their CPython 3.12 path. The standalone +verifier works in a Git-free six-file export and writes nothing. It emits +PASS_UT4_HYPERBOLIC_MIDDLE_FLOOR and a generated receipt containing all +six file hashes. Registered warning-strict normal and optimized checks +use explicit exceptions, so optimization cannot disable the checks. + +Finite corroboration checks the new paired coefficient identities on +20,632 words, consisting of every two-role word through length three +and 192 deterministic eighteen-call three-role words. Polynomial +multiplication and prefix/suffix construction use different paths. +Forty-two attaining words through six roles have complete full-group +algebra endpoint checks, including common scalar conjugations and every +dirty output block. Eighty omitted-call controls and ten additional +contract, endpoint and hypothesis controls reject. The universal result +is the written rank argument, not extrapolation from these fixtures. + +## Credit, overlap and scope + +Credit ToikY / [PR1662](https://github.com/CrocSwap/integer-mult-bounds/pull/1662) +for the alphabet, fixed quotient homomorphism, outer and middle span +bounds, earlier rank-w middle quotient and direct (2,4,2) word. Credit +Victor Li / PR3938 and +[PR3887](https://github.com/CrocSwap/integer-mult-bounds/pull/3887) for +the mixed-rank question and earlier scoped exclusions. Credit Josie +Elliston / [PR1816](https://github.com/CrocSwap/integer-mult-bounds/pull/1816) +for two-target unit optimality and the weighted question. Retain Aaron +Wang / PR1690's profile lineage, ToikY / PR1680's workspace reduction, +and the steph4n-gh / PR1573, Arham Tahir / PR1589 and Hanson Sun / PR1607 +register-model lineage credited by PR1662. The direct upper word and +outer floors are inherited. The paired middle quotient is the new result. + +All source files in [SOURCES.json](SOURCES.json) are provenance only. +No predecessor program or census is imported, audited or replayed. +The scientific base is 7c49fe32c55de02c2c873655c804b16e4c3fef0a, +priority revision 8. The selected-binding baseline passed. The +[advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19360859) +asked about seven middle calls; the same new argument yields the uniform +tariff directly. Live PR bodies, recent account work, handoffs, batch +reservations, merged searches and distinctive main README searches were +checked. Sparse local coverage and unpublished work remain limitations. + +The historical bit-new-register-model card is refined to this formal +tariff obstruction. It gives a stopping rule for this alphabet, rather +than a physical BIT improvement. Role-dependent prices, extra free +address maps, rational frames, clean allocation, native realization, +compiler/hosting, stock, precision, tape and analytic recovery are outside +the result. The five selected framework assumptions remain. No selected +supplier replay, Lean or Docker run was made. Independent human and +formal proof-kernel review are unclaimed. + +## Open next questions + +Can a changed operation alphabet, such as an additional paid address +letter, escape the 4w middle floor? Start by computing its image in Q +and deciding which equations in (1) of the proof cease to hold. A +candidate must pay for the added operation and retain arbitrary dirty +restoration before it can affect a supplier invoice. The present theorem +does not cover that changed alphabet. Structured details are in +[TASK.json](TASK.json). + +## Verifier constraints + +The six-file verifier has no recursion, subprocesses, network or output +files. Its fixed domains have at most six roles, 48 calls, 64 group +elements and 20,632 coefficient fixtures. Functions are below 60 lines; +matrix/rank dimensions and file reads have explicit limits. Failures +propagate as exceptions. The local AST/compile inspection and both +warning-strict modes are the available Python diagnostics. + +Power-of-ten rule 3 deviation: CPython allocates managed integers and +containers during the finite command. Live state is bounded by the +fixed domains above, with at most 64 group matrices or 17 quotient +matrices per endpoint. Rule 9 deviation: rejection controls dispatch +only to quotient_rank, coupling, validate_word and central_check with +fixed local fixtures. No arbitrary callback or code loading is accepted. +An embedded fixed-allocation implementation would need a separate runtime. diff --git a/research/ut4-hyperbolic-middle-floor/SOURCES.json b/research/ut4-hyperbolic-middle-floor/SOURCES.json new file mode 100644 index 0000000000..7c0547baea --- /dev/null +++ b/research/ut4-hyperbolic-middle-floor/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/ut4-central-tariff-relaxation/PROOF.md", + "usage": "provenance", + "git_blob": "8137274359979a786568da60bc802eeba2728e7f", + "sha256": "4820f0771cc6d5828492bf8cb0bacda2a74d3f00b58a02b8df056ab1db040f21" + }, + { + "path": "research/ut4-two-target-nb7-ranks-22/README.md", + "usage": "provenance", + "git_blob": "d65cec816eb2dc658bd616cc55ca67f807055fa7", + "sha256": "5297e8a16e22cdfc54445f3c3e747ebd8f36162dd00ee227dde56e05f1d0be09" + }, + { + "path": "research/ut4-two-target-fifteen/README.md", + "usage": "provenance", + "git_blob": "3d314e22e7a9d1941269b161c833fbd3bcfc8934", + "sha256": "fb1026abcf357b5a409a2398eb18c9ae7c72541176dafa0b02c819b79e8f9b5f" + } + ] +} diff --git a/research/ut4-hyperbolic-middle-floor/TASK.json b/research/ut4-hyperbolic-middle-floor/TASK.json new file mode 100644 index 0000000000..751d9e29d9 --- /dev/null +++ b/research/ut4-hyperbolic-middle-floor/TASK.json @@ -0,0 +1,116 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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": "refined", + "actual_scope": "Prove n_b >= 2w+rank(X_b)+rank(Y_b) >= 4w for the formal UT4 central target on every finite restored dirty workspace, settling the seven-b mixed-rank gate and the exact complete nonnegative uniform-letter tariff.", + "scope_change_reason": "The assigned nonabelian register card is refined to the mixed-rank open question of PR3938. Combining its two cross coefficients with the two zero self coefficients yields a uniform bound directly; no predecessor census is audited.", + "bottleneck_link": "Closes a formal BIT mechanism search direction: central UT4 targets cannot share calls at any nonnegative uniform per-letter tariff. Physical supplier costs and selected kappa are unchanged.", + "budget_minutes": 60, + "stop_rule": "Stop at the first original checked bound. Package the paired middle quotient and inherited attaining word; do not extend the alphabet or run a larger census.", + "outcome": "completed", + "evidence": "Written universal proof in PROOF.md; 20632 paired coefficient word fixtures, 42 full formal attaining words, 80 omitted-call controls and 10 further rejection controls. No predecessor executable or census is replayed.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a changed paid address alphabet escape the 4w middle floor?", + "why_it_matters": "The present formal alphabet admits no central-target sharing, so a cheaper mechanism must change a hypothesis that enforces the paired coefficient equations.", + "first_step": "Compute the additional generator image in Q, identify exactly which endpoint coefficient equation changes, and price one arbitrary-dirty completed word.", + "blocked_by": "No additional native paid address operation or complete supplier invoice is constructed here." + } + ], + "coordination": { + "source": "PR #3938", + "source_author": "VictorLiwentao", + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19360859", + "upstream_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "priority_revision": 8, + "checked_utc": "2026-11-02T21:24:00Z" + }, + "environment": { + "python": "CPython 3.12.15", + "platform": "macOS arm64", + "dependencies": "Python standard library only" + }, + "validation": { + "commands": [ + { + "argv": [ + "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12", + "-W", + "error", + "-B", + "research/ut4-hyperbolic-middle-floor/verify.py" + ], + "seconds": 0.523, + "result": "PASS_UT4_HYPERBOLIC_MIDDLE_FLOOR" + }, + { + "argv": [ + "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12", + "-W", + "error", + "-B", + "-O", + "research/ut4-hyperbolic-middle-floor/verify.py" + ], + "seconds": 0.518, + "result": "PASS_UT4_HYPERBOLIC_MIDDLE_FLOOR" + } + ], + "registered_replay": "PASS_REGISTERED_RESEARCH_PACKAGE", + "registered_seconds": 1.365, + "metadata": "PASS_PACKAGE_METADATA_AND_PINS", + "normal_optimized_receipts": "identical", + "static": "AST parse and in-memory compile pass; 22 functions, maximum 26 physical lines", + "unrun": [ + "independent human review", + "proof-kernel formalization", + "selected supplier cold replay", + "native/compiler/hosting/precision/tape/analytic transfer", + "hosted CI pending" + ] + } +} diff --git a/research/ut4-hyperbolic-middle-floor/VERIFY.json b/research/ut4-hyperbolic-middle-floor/VERIFY.json new file mode 100644 index 0000000000..413d047634 --- /dev/null +++ b/research/ut4-hyperbolic-middle-floor/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": "New paired coefficient identities, sharp complete formal endpoints, omission and hypothesis controls; generated file-hash receipt." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "New paired coefficient identities, sharp complete formal endpoints, omission and hypothesis controls; generated file-hash receipt." + } + ] +} diff --git a/research/ut4-hyperbolic-middle-floor/verify.py b/research/ut4-hyperbolic-middle-floor/verify.py new file mode 100644 index 0000000000..97f4a3da4e --- /dev/null +++ b/research/ut4-hyperbolic-middle-floor/verify.py @@ -0,0 +1,293 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Exact corroboration of the paired UT4 middle-factor rank argument.""" + +import hashlib +import itertools +import json +from pathlib import Path + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def identity(size): + return tuple(1 << i for i in range(size)) + + +def plus(left, right): + need(len(left) == len(right), "matrix row mismatch") + return tuple(a ^ b for a, b in zip(left, right)) + + +def multiply(left, right): + need(len(right) <= 64, "inner dimension limit") + need(all(0 <= row < (1 << len(right)) for row in left), "matrix shape") + return tuple(xor_values(right[k] for k in range(len(right)) + if (row >> k) & 1) for row in left) + + +def xor_values(values): + answer = 0 + for value in values: + answer ^= value + return answer + + +def rank(rows): + need(len(rows) <= 64 and all(0 <= x < 2**64 for x in rows), "rank limit") + basis = [0] * 64 + answer = 0 + for original in rows: + row = original + for bit in range(63, -1, -1): + if (row >> bit) & 1: + if basis[bit]: + row ^= basis[bit] + else: + basis[bit] = row + answer += 1 + break + return answer + + +def coupling(x, y, roles): + need(type(roles) is int and 1 <= roles <= 6, "role limit") + need(type(x) is int and type(y) is int + and 0 < x < 1 << roles and 0 < y < 1 << roles, "nonzero vectors") + return tuple(y if (x >> i) & 1 else 0 for i in range(roles)) + + +def validate_word(word, roles): + need(isinstance(word, tuple) and len(word) <= 48, "word limit") + for label, x, y in word: + need(label in "abc" and len(label) == 1, "generator") + coupling(x, y, roles) + + +def monomial(word): + if len(word) >= 4: + return None + # At most one interchange is possible in a word of length at most three. + canonical = word.replace("ca", "ac") + if any(letter * 2 in canonical for letter in "abc"): + return None + return canonical + + +def coefficients(word, roles): + """Direct polynomial multiplication, without prefix/suffix formulas.""" + validate_word(word, roles) + zero = (0,) * roles + result = {"": identity(roles)} + for label, x, y in word: + matrix = coupling(x, y, roles) + updated = result.copy() + for name, rows in result.items(): + destination = monomial(name + label) + if destination is not None: + updated[destination] = plus(updated.get(destination, zero), + multiply(rows, matrix)) + result = updated + return result + + +def middle_arrays(word, roles): + """Build X,Y and both prefix/suffix pairs independently of coefficients.""" + validate_word(word, roles) + zero = (0,) * roles + totals = {label: zero for label in "ac"} + for label, x, y in word: + if label in totals: + totals[label] = plus(totals[label], coupling(x, y, roles)) + prefix = {label: zero for label in "ac"} + xs, ys, ua, uc, va, vc = [], [], [], [], [], [] + for label, x, y in word: + if label != "b": + prefix[label] = plus(prefix[label], coupling(x, y, roles)) + continue + xs.append(x) + ys.append(y) + ua.append(tuple((row & x).bit_count() & 1 for row in prefix["a"])) + uc.append(tuple((row & x).bit_count() & 1 for row in prefix["c"])) + va.append(multiply((y,), plus(totals["a"], prefix["a"]))[0]) + vc.append(multiply((y,), plus(totals["c"], prefix["c"]))[0]) + xrows = tuple(sum(((x >> i) & 1) << j for j, x in enumerate(xs)) + for i in range(roles)) + urows = tuple(sum(column[i] << j for j, column in enumerate(columns)) + for columns in (ua, uc) for i in range(roles)) + vrows = tuple(a | (c << roles) for a, c in zip(va, vc)) + return xrows, tuple(ys), urows, vrows + + +def check_identities(word, roles): + coeff = coefficients(word, roles) + x, y, u, v = middle_arrays(word, roles) + zero = (0,) * roles + need(multiply(x, y) == coeff.get("b", zero), "B identity") + need(multiply(u, y) == coeff.get("ab", zero) + coeff.get("cb", zero), + "stacked prefix identity") + expect = tuple(a | (c << roles) for a, c in + zip(coeff.get("ba", zero), coeff.get("bc", zero))) + need(multiply(x, v) == expect, "concatenated suffix identity") + expect = tuple(a | (c << roles) for first, second in + (("aba", "abc"), ("cba", "cbc")) + for a, c in zip(coeff.get(first, zero), coeff.get(second, zero))) + need(multiply(u, v) == expect, "paired cubic identity") + return x, y, u, v + + +def quotient_rank(x, y, u, v): + need(not any(multiply(x, y)), "XY must vanish") + need(not any(multiply(u, y)), "UY must vanish") + need(not any(multiply(x, v)), "XV must vanish") + capacity = len(y) - rank(x) - rank(y) + need(rank(multiply(u, v)) <= capacity, "quotient rank inequality") + return capacity + + +def central_check(word, roles, projector): + coeff = coefficients(word, roles) + names = ("", "a", "b", "c", "ab", "ac", "ba", "bc", "cb", + "aba", "abc", "acb", "bab", "bac", "bcb", "cba", "cbc") + for name in names: + expected = identity(roles) if name == "" else (0,) * roles + if name in ("abc", "acb", "bac", "cba"): + expected = projector + need(coeff.get(name, (0,) * roles) == expected, "central coefficient " + name) + x, y, u, v = check_identities(word, roles) + width = rank(projector) + need(rank(multiply(u, v)) == 2 * width, "hyperbolic block rank") + capacity = quotient_rank(x, y, u, v) + need(rank(x) >= width and rank(y) >= width, "middle span lower bounds") + need(len(y) >= 2 * width + rank(x) + rank(y) >= 4 * width, + "four-per-target middle floor") + return capacity + + +def group_product(left, right): + a, b, c, d, e, f = ((left >> i) & 1 for i in range(6)) + p, q, r, s, t, u = ((right >> i) & 1 for i in range(6)) + values = (a ^ p, b ^ q, c ^ r, d ^ s ^ (a & q), + e ^ t ^ (b & r), f ^ u ^ (a & t) ^ (d & r)) + return sum(value << i for i, value in enumerate(values)) + + +def formal_endpoint(word, roles): + """Full 64-element group algebra, without a truncated quotient.""" + validate_word(word, roles) + result = {0: identity(roles)} + for label, x, y in word: + matrix = coupling(x, y, roles) + updated = result.copy() + generator = {"a": 1, "b": 2, "c": 4}[label] + for element, rows in result.items(): + increment = multiply(rows, matrix) + for destination in (element, group_product(element, generator)): + updated[destination] = plus(updated.get(destination, (0,) * roles), + increment) + result = {element: rows for element, rows in updated.items() if any(rows)} + return result + + +def direct_word(roles, width, changed_basis): + need(1 <= width <= roles <= 6, "direct fixture dimensions") + basis = identity(roles) + inverse = identity(roles) + if changed_basis and roles >= 2: + # One scalar involution, including mixing an active and a dirty role. + shear = list(basis) + shear[roles - 1] ^= 1 + basis = inverse = tuple(shear) + word = tuple((label, xor_values((1 << i) for i in range(roles) + if (basis[i] >> role) & 1), inverse[role]) + for role in range(width) for label in "abcbabcb") + diagonal = tuple(1 << i if i < width else 0 for i in range(roles)) + projector = multiply(multiply(basis, diagonal), inverse) + return word, projector + + +def reject(function, arguments): + try: + function(*arguments) + except ValueError: + return 1 + raise ValueError("negative control accepted") + + +def fixtures(): + counts = {"attaining_words": 0, "omissions": 0} + for roles in range(1, 7): + for width in range(1, roles + 1): + for changed in (False, True): + word, projector = direct_word(roles, width, changed) + need(central_check(word, roles, projector) == 2 * width, + "sharp quotient capacity") + expected = {0: plus(identity(roles), projector), 32: projector} + expected = {g: rows for g, rows in expected.items() if any(rows)} + need(formal_endpoint(word, roles) == expected, "full formal endpoint") + need(tuple(sum(label == g for label, _, _ in word) for g in "abc") + == (2 * width, 4 * width, 2 * width), "attaining counts") + counts["attaining_words"] += 1 + if roles <= 3 and not changed: + for i in range(len(word)): + counts["omissions"] += reject( + central_check, (word[:i] + word[i + 1:], roles, projector)) + return counts + + +def identity_checks(): + alphabet = tuple(itertools.product("abc", range(1, 4), range(1, 4))) + count = 0 + for length in range(4): + for word in itertools.product(alphabet, repeat=length): + check_identities(word, 2) + count += 1 + # Longer words and all three role directions, including nilpotent couplings. + for seed in range(192): + word = tuple(("abc"[(seed + i * i) % 3], + 1 + (seed * 3 + i * 5) % 7, + 1 + (seed * 5 + i * 3) % 7) for i in range(18)) + check_identities(word, 3) + count += 1 + return count + + +def controls(): + total = 0 + total += reject(quotient_rank, ((1,), (1,), (1,), (1,))) + total += reject(quotient_rank, ((0, 0), (1, 2), (1, 2), (1, 2))) + total += reject(quotient_rank, ((1, 2), (0, 0), (1, 2), (1, 2))) + total += reject(coupling, (0, 1, 2)) + total += reject(coupling, (1, 4, 2)) + total += reject(coupling, (1, 1, 7)) + total += reject(validate_word, ((("d", 1, 1),), 2)) + total += reject(validate_word, ((("a", 1, 1),) * 49, 2)) + need(rank((1, 1)) == 1 and rank((2, 1)) == 2, + "self-cubic zeros are needed for doubled rank") + word, projector = direct_word(3, 2, True) + total += reject(central_check, (word, 3, identity(3))) + changed = (("c", word[0][1], word[0][2]),) + word[1:] + total += reject(central_check, (changed, 3, projector)) + return total + + +def main(): + counts = fixtures() + counts["coefficient_words"] = identity_checks() + counts["controls"] = controls() + package = Path(__file__).resolve().parent + hashes = {} + for name in ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", + "VERIFY.json", "verify.py"): + path = package / name + need(path.stat().st_size <= 2**20, "package file limit") + hashes[name] = hashlib.sha256(path.read_bytes()).hexdigest() + print(json.dumps({"status": "PASS_UT4_HYPERBOLIC_MIDDLE_FLOOR", + "counts": counts, "sha256": hashes}, sort_keys=True)) + + +if __name__ == "__main__": + main()