diff --git a/research/ut4-mixed-relaxation-optimum/PROOF.md b/research/ut4-mixed-relaxation-optimum/PROOF.md new file mode 100644 index 0000000000..eb2a23a5ed --- /dev/null +++ b/research/ut4-mixed-relaxation-optimum/PROOF.md @@ -0,0 +1,139 @@ +# Exact mixed middle-factor optimum + +Work over F2. Let S,T,H be diagonal r by r matrices. Every diagonal triple +(s_i,t_i,h_i) is either zero or one of the seven nonzero binary triples. +Let E be the coordinate subspace on the d nonzero triples, and let k count +the pure-central triples (0,0,1). Consider finite n and matrices + + X,U : F2^n -> F2^r, Y,V : F2^r -> F2^n + +with all X columns and all Y rows nonzero, E contained in im X and in the +row space of Y, and + + XY=0, UY=S, XV=T, UV=H. (1) + +The exact minimum is + + n_min = 2d+k+[d=k=1]. (2) + +For d=0 the empty factorization attains zero. The written theorem permits +all finite r and d. The executable constructor is deliberately bounded to +64 active roles and two additional dirty identity roles. + +This is an exact necessary coefficient relaxation. A column gives a nonzero +rank-one middle coupling x_j y_j^T, but U and V need not come from preceding +and following paid chronological paths. No formal group-algebra word follows. + +## Lower bound, credited premise restated + +This is the mixed quotient argument from Nick Petalas #2175, using the +mixed active-span constraints from Gareth Davidson #2027 and ToikY #1662's +central quotient method. It is restated to specify the solved optimization, +not claimed as a new lower bound. + +Let pi delete output coordinates where S has a one. Restrict the input to +ker T. Since XV=T, V(ker T) lies in ker X. Since UY=S, pi U annihilates +im Y. Since XY=0, im Y is contained in ker X. Therefore pi H restricted +to ker T factors through ker X/im Y. Its rank is exactly k, as the only +surviving diagonal ones have s=t=0 and h=1. Thus + + k <= n-rank X-rank Y <= n-2d. + +At d=k=1, n=3 would force both ranks to equal one. Over F2 all nonzero +X columns are the same vector x and all nonzero Y rows the same row y. +Then XY=3xy=xy is nonzero, a contradiction. Thus n>=4 in that case. +This binary exceptional case is inherited from ToikY #1662. + +## New step: mixed blocks attain the lower bound + +Direct sums preserve all four equations, nonzero columns and rows, and the +active-span constraints. The task is therefore to allocate small blocks +without paying a four-column singleton for an isolated pure-central role. + +For a single noncentral triple (s,t,h), use X=Y^T=(1,1). Choose two-entry +binary rows U and V^T with sums s and t and dot product h. Such rows exist +whenever (s,t) differs from (0,0): if s=1 choose U=(1,0) and V=(h,t+h); +if s=0,t=1 choose V=(1,0) and U=(h,h). This costs two columns. + +The following new five-column blocks pair one pure-central coordinate with +any one of the six noncentral coordinates. Encode a two-vector (a,b) by +a+2b. In every row of this table set + + X columns = (1,1,1,2,3), Y rows = (1,1,2,2,2). + +The targets are S=diag(0,s), T=diag(0,t), H=diag(1,h). + +| (s,t,h) | U columns | V rows | +| --- | --- | --- | +| (0,1,0) | (0,0,1,0,1) | (0,1,0,3,1) | +| (0,1,1) | (0,0,1,2,3) | (0,1,0,3,1) | +| (1,0,0) | (0,0,1,0,3) | (0,1,1,0,0) | +| (1,0,1) | (0,0,1,0,3) | (0,1,3,2,2) | +| (1,1,0) | (0,0,1,0,3) | (0,1,1,2,0) | +| (1,1,1) | (0,0,1,0,3) | (0,1,3,0,2) | + +Each equality in (1) follows by adding the five outer products over F2. +Both X and Y have rank two and no zero column or row. This is a finite +algebraic table, not a search failure or a chronological witness. #2175's +single z/uz fixture already establishes one member's attainability. We use +its X and Y and supply a uniform table for all six partner labels. Neither +that existing special case nor its lower bound is new credit here. + +For completeness the pure blocks below are ToikY #1662's construction. +For two pure-central coordinates take X=Y^T with columns +(1,1,2,2,3,3). For three take columns (1,2,3,4,5,6,7,1,1). +In both cases XX^T=0, X has full row rank q, and n=3q. The q-dimensional +quotient ker X/im X^T has a basis. Take representatives as the columns of V, +and take U to be their dual functionals, vanishing on im X^T and extended +to the ambient space. Then (1) holds with S=T=0 and H=I_q. +The executable independently constructs representatives and duals by bounded +binary elimination. It does not import or run a predecessor program. + +Now allocate the roles. If k=0, use noncentral singletons. If k>=2, write +k as a sum of twos and threes, use the inherited pure blocks, and use +noncentral singletons for the rest. This costs 3k+2(d-k)=2d+k. +If k=1 and d>=2, use one new five-column mixed block and d-2 noncentral +singletons, for 5+2(d-2)=2d+1 columns. If d=k=1, the inherited four-column +fixture is X=Y^T=(1,1,1,1), U=(1,0,0,1), V=(1,0,1,0)^T. +Zero-padding and simultaneous coordinate permutation place every block on +its original coordinates and preserve arbitrary identity-role coordinates. +This proves (2) for every finite diagonal target family. + +## Consequence and limits + +No strengthened mixed-root lower bound can follow from precisely (1), these +two span constraints, and the nonzero coupling restrictions alone. They are +already attained at 2d+k except for the inherited one-role exception. Any +stronger formal-word bound must retain further chronological or coefficient +information, or another constraint omitted from this relaxation. This does +not exclude stronger methods and does not decide any remaining UT4 word cost. + +The pure-central endpoint, quotient/spans and single mixed fixture are +predecessor work. The contribution is the six-partner mixed construction +and its uniform allocation theorem, closing the general mixed relaxation. +No literature-priority claim is made for rank-nullity, direct sums or dual bases. + +## Verification and code bounds + +The checker multiplies the four binary matrices directly, checks all nonzero +couplings, both exact active spans, the formula and every zero-padded coordinate. +It exhausts all seven-label sequences through four active roles, then covers +larger mixed multiplicities and the 64-role boundary. A separate scalar census +enumerates every U,V through four columns to recover all seven scalar minima. +Semantic controls alter a mixed coefficient, delete a column and exchange the +target coordinates. Invalid labels, Boolean integers and out-of-range requests +reject. Normal and optimized execution use explicit exceptions, not assertions. + +All loops have finite bounds. The largest construction has at most 192 columns +and 66 role coordinates. Pure-block searches enumerate at most 512 vectors; +the exhaustive family domain is fixed at d<=4. Functions remain below 60 lines. +Python and its standard library allocate dynamically; this is a documented +managed-runtime deviation from fixed allocation. Bounded input dimensions bound +the live mathematical arrays. No recursion, generated code or network is used. +Strict Python warnings are enabled in registered commands. No separate static +analyzer or proof kernel is claimed. + +This contribution is produced by Nick Petalas. Credit ToikY, Gareth Davidson, +Nick Petalas, Aaron Wang, Josie Elliston, steph4n-gh, Arham Tahir, Hanson Sun, +and the retained formal register-model lineage in the pinned sources. +Apache-2.0. Independent human and formal proof-kernel review are unclaimed. diff --git a/research/ut4-mixed-relaxation-optimum/README.md b/research/ut4-mixed-relaxation-optimum/README.md new file mode 100644 index 0000000000..26bcab0641 --- /dev/null +++ b/research/ut4-mixed-relaxation-optimum/README.md @@ -0,0 +1,81 @@ +# Exact mixed-root UT4 middle-factor relaxation + +A scoped all-size proof determines the exact necessary coefficient-relaxation +minimum for every diagonal mixture of UT4 u/v/z targets: + + n_min = 2d+k+[d=k=1], + +where d counts active coordinates and k counts pure-central coordinates. +The new step pairs a lone pure-central coordinate with any noncentral partner +in five columns. Together with credited predecessor blocks, this attains the +mixed lower bound uniformly. The full statement and six explicit blocks are +in [PROOF.md](PROOF.md). + +This is a sharp limit of the declared four-matrix relaxation, not a paid +chronological word. Stronger word bounds need further coefficient or chronology +information. No physical supplier, new kappa or selected-frontier change is claimed. + +## Credit and relation to earlier work + +This contribution is produced by Nick Petalas. ToikY's +[PR1662](https://github.com/CrocSwap/integer-mult-bounds/pull/1662) already solves +the pure-central relaxation. Gareth Davidson's +[PR2027](https://github.com/CrocSwap/integer-mult-bounds/pull/2027) supplies the +mixed-root span unions and asks about mixed pure-central targets. Nick Petalas's +[PR2175](https://github.com/CrocSwap/integer-mult-bounds/pull/2175) supplies the +mixed 2d+k lower bound and one z/uz fixture. Those results are credited premises, +not replay or audit deliverables. The new result uniformly attains the mixed +relaxation, including every one-pure-central partner type. + +The pinned proofs retain the complete register-model lineage. Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. + +## Reproduce + +From the repository root, using CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/ut4-mixed-relaxation-optimum/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/ut4-mixed-relaxation-optimum/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/ut4-mixed-relaxation-optimum +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/ut4-mixed-relaxation-optimum --check-source-history +``` + +Any CPython 3.12 path may replace the local interpreter path. Normal execution +is read-only and prints `PASS_UT4_MIXED_RELAXATION_OPTIMUM`. The registered hook +runs both normal and optimized checks. RESULT.json is generated from scientific +outputs and SHA256 hashes of package files and pinned live proofs. Explicit +`--emit NEW_PATH` writes an external receipt and refuses an occupied path. + +Local exact checks cover 5,602 exhaustive mixed/padded fixtures through four +active roles, 1,098 larger fixtures through 64 roles, all seven scalar minima, +15 independently multiplied block templates with 176 entries, and eight +rejection controls. The universal statement rests on the written proof. + +The generic card's historical first command, `scripts/research_baseline.py`, +fails at `KeyError: 'bit_lower'` on the selected record. This unrelated source +orientation failure was recorded; no shared code or selected record was changed. +The selected review and source manifest were read directly. + +## Limitations + +The proof is quantified over every finite diagonal family and dirty identity +extension. The executable constructor supports at most 64 active roles and two +dirty coordinates. All four equations and active-span restrictions are necessary +conditions, so an attaining fixture is not a formal operator construction. +Physical address realization, native/compiler, hosting, precision/tape, actual +paid paths and outer transfer remain unrun obligations. No selected cold replay, +Lean build, independent human acceptance or formal verification is claimed. + +## Open next questions + +1. Which additional chronological equation gives a stronger mixed-family bound? + Start with one pure-central and one u target, impose actual prefix/suffix + paths on the five-column table, and charge all outer calls. The present + relaxation deliberately omits these paths. +2. Can the larger mixed families' complete paid tariffs be characterized? + Start with a named target outside the existing z/uz weighted region, retaining + all formal coefficients and arbitrary dirty restoration. Relaxation attainment + alone does not establish an upper word or its tariff. + +Structured questions and exact source pins are in TASK.json and SOURCES.json. diff --git a/research/ut4-mixed-relaxation-optimum/RESULT.json b/research/ut4-mixed-relaxation-optimum/RESULT.json new file mode 100644 index 0000000000..390fba0144 --- /dev/null +++ b/research/ut4-mixed-relaxation-optimum/RESULT.json @@ -0,0 +1,18 @@ +{ + "columns_in_exhaustive_fixtures": 46022, + "dense_entries": 176, + "dense_templates": 15, + "exhaustive_mixed_fixtures": 5602, + "larger_fixtures": 1098, + "rejection_controls": 8, + "scalar_labels": 7, + "source_sha256": { + "PROOF.md": "04c4c2b99aee384e6c02626eb794eaf15b735bb5046a5d62cd1d92fad8583952", + "README.md": "5fdff565b3483aa121ee112efcd2699362708c4af00ad5cb5f9a33676bd26089", + "SOURCES.json": "f47516a3aa1ecc43109611aa403a7fdce1fff4aa4f094ad7f1a6edada1b99b52", + "TASK.json": "ead7f0289c238bf0fa1093b103f8e4987134ef700e3f731cf2287cb53feca136", + "VERIFY.json": "0c5d313f390291aa442be22a5fb73aefffc9c5ea81a37497cb6dfd43ac049316", + "verify.py": "da320b4bcd3ef9393d27d585b77ab5565ce0fc3533f8a807546ac76a31b9a5cd" + }, + "transcript_sha256": "6fbda0ece976154c38094411f2256ef868f49ba7b7dbdca3252824da84ca4b6a" +} diff --git a/research/ut4-mixed-relaxation-optimum/SOURCES.json b/research/ut4-mixed-relaxation-optimum/SOURCES.json new file mode 100644 index 0000000000..f18631a4ff --- /dev/null +++ b/research/ut4-mixed-relaxation-optimum/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/ut4-central-tariff-relaxation/PROOF.md", + "usage": "input", + "git_blob": "8137274359979a786568da60bc802eeba2728e7f", + "sha256": "4820f0771cc6d5828492bf8cb0bacda2a74d3f00b58a02b8df056ab1db040f21" + }, + { + "path": "research/ut4-mixed-central-middle/PROOF.md", + "usage": "input", + "git_blob": "e6a7c24d20c7718989a2b00e97ef9638f7804226", + "sha256": "34a5dc532b9010b5e8afd67273a9d4b1cf17e1362f5f432c4b433581cc7784d5" + }, + { + "path": "research/ut4-mixed-root-tariffs/PROOF.md", + "usage": "input", + "git_blob": "633a7d5137ad13fafe719cc042099977ad1f96e5", + "sha256": "c0def58338a69a57ac95f1d32a744993aa07656c46eba88a99354b276917bd8e" + } + ] +} diff --git a/research/ut4-mixed-relaxation-optimum/TASK.json b/research/ut4-mixed-relaxation-optimum/TASK.json new file mode 100644 index 0000000000..99602698b0 --- /dev/null +++ b/research/ut4-mixed-relaxation-optimum/TASK.json @@ -0,0 +1,113 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "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": "Exact necessary four-matrix middle-factor relaxation for every diagonal mixed UT4 u/v/z target family.", + "scope_change_reason": "The new step solves a coefficient relaxation uniformly; it does not construct a larger native alphabet or a physical supplier.", + "bottleneck_link": "Side result: identifies the precise limit of the mixed rank quotient, directing stronger formal-word bounds to missing chronology or coefficient constraints.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified uniform mixed attainment; do not search for full words.", + "outcome": "completed", + "evidence": "PROOF.md and generated RESULT.json; direct matrix products, exhaustive small mixed families and scalar minima, larger constructive fixtures and semantic rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Which additional chronological equation strengthens the mixed-family bound?", + "why_it_matters": "The solved relaxation alone cannot exceed its exact optimum.", + "first_step": "Require actual prefix/suffix paid paths for one z and one u target.", + "blocked_by": "No actual paid outer paths are constructed here." + }, + { + "question": "What are the complete tariffs for larger mixed pure-central families?", + "why_it_matters": "Relaxation sharpness does not price a formal word.", + "first_step": "Fix one target beyond the z/uz region and retain every full coefficient and dirty endpoint.", + "blocked_by": "Full chronological and restoration constraints remain." + } + ], + "coordination": { + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19134037", + "base": "624de9dc66858af0945e5f8a0942488d62280d43", + "priority_revision": 7, + "coverage_limitations": "Sparse local notes; live helper refresh and explicit main/merged term searches supplement each other. Arbitrary diffs and unpublished work are not exhaustive." + }, + "preserved_workspace": { + "branch": "research/w9-1022k-scoped-result", + "head": "93a05b2221fb68c9e134d45b70e289bd7b7bc289", + "parent": "624de9dc66858af0945e5f8a0942488d62280d43" + }, + "playbook": "investigation", + "orientation": { + "command": "/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_baseline.py", + "result": "Failed with KeyError: 'bit_lower'; selected review/source manifest read directly; no predecessor mathematical replay." + }, + "validation": { + "interpreter": "3.12.15 (main, Oct 14 2026, 00:55:37) [Clang 23.1.3 ]", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "scientific_counts": { + "columns_in_exhaustive_fixtures": 46022, + "dense_entries": 176, + "dense_templates": 15, + "exhaustive_mixed_fixtures": 5602, + "larger_fixtures": 1098, + "rejection_controls": 8, + "scalar_labels": 7, + "transcript_sha256": "6fbda0ece976154c38094411f2256ef868f49ba7b7dbdca3252824da84ca4b6a" + }, + "diagnostics": "Strict Python warnings; ruff is unavailable; no external static analyzer.", + "unrun": "Physical/native/compiler/hosting/precision/tape/outer obligations, chronological words, selected cold replay, human or proof-kernel review.", + "overlap": { + "open_prs": 395, + "open_prs_fetched_at": "2026-10-22T22:41:30.157812+00:00", + "discussion_records": 3893, + "discussions_fetched_at": "2026-10-22T22:42:30.040386+00:00", + "pagination_complete": true, + "local_notes_before_widening": 101, + "local_head_notes": 6319, + "main_term_search": "Full origin/main README/proof searches supplement sparse local notes. Exact matching predecessor quantities are credited.", + "precommit_refresh": "Canonical main remains 624de9dc66858af0945e5f8a0942488d62280d43; live UT4 open-PR search returned no open work; latest 20 claims contain only this target." + } + } +} diff --git a/research/ut4-mixed-relaxation-optimum/VERIFY.json b/research/ut4-mixed-relaxation-optimum/VERIFY.json new file mode 100644 index 0000000000..022b1c5747 --- /dev/null +++ b/research/ut4-mixed-relaxation-optimum/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/ut4-central-tariff-relaxation/PROOF.md", + "research/ut4-mixed-central-middle/PROOF.md", + "research/ut4-mixed-root-tariffs/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact mixed coefficient witnesses, all small families, scalar minimum census, larger constructions and rejection controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact mixed coefficient witnesses, all small families, scalar minimum census, larger constructions and rejection controls." + } + ] +} diff --git a/research/ut4-mixed-relaxation-optimum/verify.py b/research/ut4-mixed-relaxation-optimum/verify.py new file mode 100644 index 0000000000..089c0d93ee --- /dev/null +++ b/research/ut4-mixed-relaxation-optimum/verify.py @@ -0,0 +1,265 @@ +"""Exact binary middle-factor witnesses. Standard library; read-only by default.""" +import argparse +import hashlib +import itertools +import json +from pathlib import Path + +LABELS = tuple(t for t in itertools.product(range(2), repeat=3) if any(t)) +MIXED = { + (0, 1, 0): ((0, 0, 1, 0, 1), (0, 1, 0, 3, 1)), + (0, 1, 1): ((0, 0, 1, 2, 3), (0, 1, 0, 3, 1)), + (1, 0, 0): ((0, 0, 1, 0, 3), (0, 1, 1, 0, 0)), + (1, 0, 1): ((0, 0, 1, 0, 3), (0, 1, 3, 2, 2)), + (1, 1, 0): ((0, 0, 1, 0, 3), (0, 1, 1, 2, 0)), + (1, 1, 1): ((0, 0, 1, 0, 3), (0, 1, 3, 0, 2)), +} + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def rank(vectors): + pivots = {} + for value in vectors: + for bit in range(value.bit_length() - 1, -1, -1): + if value >> bit & 1: + if bit in pivots: + value ^= pivots[bit] + else: + pivots[bit] = value + break + return len(pivots) + + +def pairing(a, b): + return (a & b).bit_count() % 2 + + +def product_rows(left, right, r): + """Multiply a column list by a row list, returning binary matrix rows.""" + result = [0] * r + for x, y in zip(left, right, strict=True): + for i in range(r): + if x >> i & 1: + result[i] ^= y + return tuple(result) + + +def pure_block(d): + """Only the inherited dimension-two/three pure blocks are needed.""" + need(d in (1, 2, 3), 'pure block dimension') + if d == 1: + return (1,) * 4, (1,) * 4, (1, 0, 0, 1), (1, 0, 1, 0) + x = (1, 1, 2, 2, 3, 3) if d == 2 else tuple(range(1, 8)) + (1, 1) + n = len(x) + rows = tuple(sum(((v >> i) & 1) << j for j, v in enumerate(x)) for i in range(d)) + basis = list(rows) + representatives = [] + for value in range(1 << n): + if all(pairing(value, row) == 0 for row in rows): + if rank(basis + [value]) > len(basis): + basis.append(value) + representatives.append(value) + if len(representatives) == d: + break + need(len(representatives) == d, 'quotient dimension') + duals = [] + for i in range(d): + candidates = [v for v in range(1 << n) + if all(pairing(v, row) == 0 for row in rows) + and all(pairing(v, rep) == int(i == j) + for j, rep in enumerate(representatives))] + need(bool(candidates), 'dual existence') + duals.append(candidates[0]) + u = tuple(sum(((row >> j) & 1) << i for i, row in enumerate(duals)) for j in range(n)) + v = tuple(sum(((row >> j) & 1) << i for i, row in enumerate(representatives)) for j in range(n)) + return x, x, u, v + + +PURE = {d: pure_block(d) for d in (1, 2, 3)} + + +def singleton(label): + s, t, h = label + for u in itertools.product(range(2), repeat=2): + for v in itertools.product(range(2), repeat=2): + if sum(u) % 2 == s and sum(v) % 2 == t and sum(a*b for a, b in zip(u, v)) % 2 == h: + return (1, 1), (1, 1), u, v + raise ValueError('pure singleton needs four columns') + + +def embed(block, indices): + return tuple(tuple(sum(((value >> i) & 1) << index + for i, index in enumerate(indices)) for value in family) + for family in block) + + +def construct(labels, dirty=0): + need(type(dirty) is int and 0 <= dirty <= 2, 'dirty range') + need(isinstance(labels, tuple) and len(labels) <= 64, 'label count') + need(all(type(t) is tuple and len(t) == 3 + and all(type(v) is int and v in (0, 1) for v in t) + and t in LABELS for t in labels), 'active labels') + pure = [i for i, t in enumerate(labels) if t == (0, 0, 1)] + other = [i for i, t in enumerate(labels) if t != (0, 0, 1)] + blocks = [] + if len(pure) == 1: + if other: + j = other.pop(0) + u, v = MIXED[labels[j]] + block = ((1, 1, 1, 2, 3), (1, 1, 2, 2, 2), u, v) + blocks.append(embed(block, (pure.pop(), j))) + else: + blocks.append(embed(PURE[1], (pure.pop(),))) + if len(pure) % 2: + blocks.append(embed(PURE[3], tuple(pure[:3]))) + pure = pure[3:] + for i in range(0, len(pure), 2): + blocks.append(embed(PURE[2], tuple(pure[i:i+2]))) + for i in other: + blocks.append(embed(singleton(labels[i]), (i,))) + return tuple(tuple(v for block in blocks for v in block[j]) for j in range(4)) + + +def inspect(labels, dirty, witness): + d = len(labels) + r = d + dirty + x, y, u, v = witness + n = len(x) + need(all(len(f) == n for f in witness), 'family lengths') + need(all(type(a) is int and 0 <= a < (1 << r) for f in witness for a in f), 'binary vectors') + need(all(x) and all(y), 'nonzero paid coupling') + need(rank(x) == d and rank(y) == d, 'active spans') + need(all(a < (1 << d) for a in x + y), 'active coordinate support') + zero = (0,) * r + targets = tuple(tuple(((labels[i][j] << i) if i < d else 0) + for i in range(r)) for j in range(3)) + actual = (product_rows(x, y, r), product_rows(u, y, r), + product_rows(x, v, r), product_rows(u, v, r)) + need(actual == (zero,) + targets, 'four coefficient equations') + k = labels.count((0, 0, 1)) + need(n == 2*d + k + int(d == k == 1), 'optimum column count') + return n + + +def scalar_minima(): + observed = {} + for n in range(1, 5): + if n % 2: + continue # nonzero scalar X,Y force XY=n modulo two. + for u in itertools.product(range(2), repeat=n): + for v in itertools.product(range(2), repeat=n): + label = (sum(u) % 2, sum(v) % 2, + sum(a*b for a, b in zip(u, v)) % 2) + if label in LABELS: + observed.setdefault(label, n) + need(observed == {t: 4 if t == (0, 0, 1) else 2 for t in LABELS}, 'scalar exhaustive optimum') + return observed + + +def dense_template_controls(): + """Independent entrywise arithmetic for every block used in the proof.""" + families = [(label,) for label in MIXED] + families += [((0, 0, 1), label) for label in MIXED] + families += [((0, 0, 1),)*q for q in (1, 2, 3)] + entries = 0 + for labels in families: + x, y, u, v = construct(labels) + d = len(labels) + for equation, (left, right) in enumerate(((x, y), (u, y), (x, v), (u, v))): + for i in range(d): + for j in range(d): + observed = sum(((left[k] >> i) & 1) * ((right[k] >> j) & 1) + for k in range(len(x))) % 2 + target = int(i == j) * (labels[i][equation-1] if equation else 0) + need(observed == target, 'independent dense template') + entries += 1 + return len(families), entries + + +def rejection_controls(): + labels = ((0, 0, 1), (1, 0, 0)) + witness = construct(labels) + bad = list(witness) + bad[2] = (bad[2][0] ^ 1,) + bad[2][1:] + jobs = [lambda: construct(((True, 0, 1),)), lambda: construct(((0, 0, 0),)), + lambda: construct(((1, 0, 0),), -1), lambda: construct(((1, 0, 0),), True), + lambda: construct(((1, 0, 0),)*65), lambda: inspect(labels, 0, tuple(bad)), + lambda: inspect(labels, 0, tuple(f[:-1] for f in witness)), + lambda: inspect(tuple(reversed(labels)), 0, witness)] + for job in jobs: + try: + job() + except ValueError: + continue + raise ValueError('negative control accepted') + return len(jobs) + + +def scientific_result(): + digest = hashlib.sha256() + cases = 0 + columns = 0 + for d in range(5): + for labels in itertools.product(LABELS, repeat=d): + for dirty in (0, 2): + witness = construct(labels, dirty) + columns += inspect(labels, dirty, witness) + digest.update(repr((labels, dirty, witness)).encode()) + cases += 1 + larger = 0 + for d in range(5, 33): + for k in range(d + 1): + labels = ((0, 0, 1),)*k + tuple(tuple(MIXED)[j % 6] for j in range(d-k)) + for dirty in (0, 2): + witness = construct(labels, dirty) + inspect(labels, dirty, witness) + digest.update(repr((labels, dirty, witness)).encode()) + larger += 1 + for k in (0, 1, 2, 3, 63, 64): + labels = ((0, 0, 1),)*k + ((1, 1, 1),)*(64-k) + witness = construct(labels, 2) + inspect(labels, 2, witness) + digest.update(repr((labels, witness)).encode()) + larger += 1 + scalar_minima() + templates, entries = dense_template_controls() + return {'exhaustive_mixed_fixtures': cases, 'columns_in_exhaustive_fixtures': columns, + 'larger_fixtures': larger, 'scalar_labels': 7, + 'dense_templates': templates, 'dense_entries': entries, + 'rejection_controls': rejection_controls(), 'transcript_sha256': digest.hexdigest()} + + +def authenticated_result(): + package = Path(__file__).resolve().parent + root = package.parent.parent + sources = json.loads((package / 'SOURCES.json').read_text()) + for item in sources['files']: + if item['usage'] == 'input': + need(hashlib.sha256((root / item['path']).read_bytes()).hexdigest() == item['sha256'], 'source hash') + result = scientific_result() + result['source_sha256'] = {p.name: hashlib.sha256(p.read_bytes()).hexdigest() + for p in sorted(package.iterdir()) if p.is_file() and p.name != 'RESULT.json'} + return result + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--emit', type=Path) + args = parser.parse_args() + result = authenticated_result() + if args.emit: + with args.emit.open('x') as stream: + json.dump(result, stream, indent=2, sort_keys=True) + stream.write('\n') + else: + expected = json.loads((Path(__file__).parent / 'RESULT.json').read_text()) + need(json.dumps(result, sort_keys=True) == json.dumps(expected, sort_keys=True), 'generated receipt mismatch') + print('PASS_UT4_MIXED_RELAXATION_OPTIMUM', json.dumps(result, sort_keys=True)) + + +if __name__ == '__main__': + main()