diff --git a/research/nonfield-one-relation/PROOF.md b/research/nonfield-one-relation/PROOF.md new file mode 100644 index 0000000000..7ec9cbd09d --- /dev/null +++ b/research/nonfield-one-relation/PROOF.md @@ -0,0 +1,154 @@ +# A residue-field extension of the one-relation obstruction + +This scoped proof is produced by Nick Petalas. The every-field theorem of +Josie Elliston's [PR6044](https://github.com/CrocSwap/integer-mult-bounds/pull/6044), +head `4ebdea4e95fa4cbf227b4be630f656105d96e5f7`, is a cited mathematical +premise. Its proof and scientific census are not replayed here. The new step +is specialization of the coefficient ring, including factors that disappear. + +## Setting and cited premise + +Let R be a nonzero commutative ring with identity. Let A_1,...,A_k be +nonzero rank-one rational d-by-d matrices. Write H for their additive +integer span. In the formal group algebra R[H], distinct matrices h give +independent basis symbols [h], and [h][g]=[h+g]. The integer exponent +labels are not reduced modulo the characteristic of R. + +For W>=1 let N_j be idempotent W-by-W matrices over R, and suppose the +following formal identity holds: + + product_(j=1,...,k) (I + ([A_j]-1) N_j) + = diag([C_1],...,[C_W]). (1) + +The C_w belong to H, so are rational d-by-d matrices. Zero C_w are restored dirty registers. +The identity acts on arbitrary register contents; no zero initialization is +assumed. A global normalized outer product N_j=x_j y_j^T, y_j^T x_j=1, +is one important allowed case. + +We use the following statement from PR6044. Over any field K, if all paid +projectors are rank-one idempotents and the rational span of the k paid +frames has dimension at least k-1, a formal diagonal monomial endpoint +has pairwise disjoint assignments + + C_w = sum_(j in I_w) A_j. + +Consequently sum_w rank_Q(C_w)<=k. This is the exact prerequisite imported +from that work, including its arbitrary register count and restored roles. + +## Theorem: one qualified residue field suffices + +Choose a maximal ideal m of R and put K=R/m. Reduce N_j entrywise to +bar(N_j). Suppose every bar(N_j) has rank zero or one over K. Let + + J_m = { j : bar(N_j) != 0 }, n_m = |J_m|. + +If n_m>0, assume + + dim_Q span { A_j : j in J_m } >= n_m-1. (2) + +Then there are pairwise disjoint subsets I_w of J_m such that + + C_w = sum_(j in I_w) A_j, + sum_w rank_Q(C_w) <= n_m. (3) + +If J_m is empty, every C_w is zero and the same conclusion holds with +empty assignments. The hypothesis concerns this one residue field; no +constant rank or global outer-product representation of N_j is needed. + +### Proof + +The unital quotient map R->K induces a coefficientwise homomorphism +R[H]->K[H]. It fixes every formal label [h]. In particular its action on +(1) retains exactly the same C_w on the right. Distinct labels remain +linearly independent because 1_K is nonzero. + +The reduced matrices are still idempotent. A zero reduced projector gives +an identity factor, which can be removed without changing the order of the +remaining factors. A nonzero rank-one reduced projector has a normalized +outer product: choose a nonzero vector x spanning its image. There is a +linear functional y^T with N(v)=x y^T(v). Idempotence and x!=0 give +N(x)=x, hence y^T x=1. Thus every surviving factor has precisely PR6044's +field form. + +Let H_m be the additive integer span of the surviving frames. The entire +reduced left side lies in M_W(K[H_m]). Inclusion K[H_m]->K[H] is injective +on formal basis elements. Therefore each endpoint C_w belongs to H_m: +otherwise its coefficient 1 on the right could not occur on the left. +For n_m>0, apply the cited field theorem to this reduced, ordered word and +(2). It gives the disjoint subsets in (3). Rank subadditivity and the +rank-one hypothesis on each A_j give the displayed rank bound. + +If n_m=0, the left side is I. Independence of formal labels gives +[C_w]=[0], hence C_w=0 for every w. This proves the empty case. QED. + +## Corollary: nonfield free rank-one projectors do not escape + +Suppose every N_j=x_j y_j^T over R with y_j^T x_j=1_R, and + + dim_Q span {A_1,...,A_k} >= k-1. + +Then (1) implies disjoint assignment of the C_w to the original paid +frames and sum_w rank_Q(C_w)<=k, for every nonzero commutative R. + +Indeed R has a maximal ideal. At every such ideal the normalized outer +product remains normalized, so each reduced projector is nonzero and has +rank one. Thus J_m is the full index set, and the theorem applies. This +covers Z/2^e for every e>=1, other Z/m with m>=2, nilpotents and zero +divisors. It uses the cited field theorem, rather than extending its +individual domain or graph arguments to rings with zero divisors. + +The bound is sharp over every such R. Take k=d, A_j=E_jj, and N_j=E_11 +on W>=1 scalar registers. Their product has endpoint + + diag([I_d],[0],...,[0]). + +The rational target rank sum is d=k. All other registers are restored on +arbitrary inputs. There is no physical/native tariff claim in this example. + +## Varying rank and the sharper active count + +More generally suppose every N_j has rank at most one at every maximal +ideal, and the full frame list has at most one rational relation. Every +sublist also has at most one relation: its relation space injects into +the relation space of the full list by extending coefficients with zeros. +Thus the theorem applies at every maximal ideal, and + + sum_w rank_Q(C_w) <= min_m |J_m|. (4) + +The minimum exists because its possible values lie in {0,...,k}. The +assigned subsets may depend on the chosen ideal. We assert neither one +assignment simultaneously describing all projectors nor a global +factorization of every idempotent. Vanishing two-by-two minors over R are +a sufficient, though unnecessary, way to ensure the required fiber rank. + +For a concrete example over Z/6, take W=2 and + + N_1=3 E_11, N_2=4 E_11, A_1=A_2=A!=0. + +Both matrices are idempotent, their product is zero, and their sum is +E_11. Multiplication gives + + (I+([A]-1)N_1)(I+([A]-1)N_2) + = diag([A],[0]). + +Exactly one factor survives modulo 2 and exactly one survives modulo 3. +Formula (4) gives the sharp bound one, although the written ring word has +two nonzero factors. Neither N_j admits a normalized global outer product: +it vanishes in one residue field, contradicting the reduction of y^T x=1. + +By itself the first factor has diagonal entry 4+3[A], which is a monomial +in each residue field with different exponents there. It is not a formal +monomial over Z/6. This explains why the fixed global endpoint (1) matters; +component-dependent endpoints cannot be substituted for it. + +## Scope + +This extends PR6044's explicit nonfield question for commutative rings and +the stated residue-rank hypothesis. The general theorem can also apply +when the full frame list has more relations, provided one surviving +sublist satisfies (2). Noncommutative rings, rank-two residue projectors, +and surviving lists with two or more independent relations remain outside +this argument. A ring quotient alone does not supply a native operation, +legal physical endpoint, hosting, compiler, rounding or complete paid bill. +There is no new kappa or complete multiplication theorem. Independent human +and formal proof-kernel review are unclaimed. diff --git a/research/nonfield-one-relation/README.md b/research/nonfield-one-relation/README.md new file mode 100644 index 0000000000..9540106f62 --- /dev/null +++ b/research/nonfield-one-relation/README.md @@ -0,0 +1,106 @@ +# Nonfield coefficients do not escape the one-relation paid-rank floor + +This scoped mathematical proof is produced by Nick Petalas. For every nonzero +commutative coefficient ring R, a formal word with normalized rank-one scalar +projectors and at most one rational relation among its paid rank-one address +frames has disjoint target assignments and + + sum_w rank_Q(C_w) <= number of paid factors. + +This answers Open next question 2 of Josie Elliston's +[PR6044](https://github.com/CrocSwap/integer-mult-bounds/pull/6044) for the stated +commutative-ring class. It includes Z/2^e, arbitrary composite moduli, +nilpotents, zero divisors and any finite number of restored dirty registers. +The [proof](PROOF.md) uses PR6044's every-field theorem as a cited premise. +It does not recheck that theorem or rerun its scientific executable. + +The new specialization theorem permits projectors without a global normalized +outer product. It is enough that one residue field sees only rank-zero and +rank-one projectors, and that the surviving frames have at most one relation. +The bound then counts only surviving factors. If every residue qualifies, +take their minimum. A Z/6 example has two nonzero ring factors but only one +active factor in each residue and attains that sharper floor. A second +example attains the ordinary rank-two floor over Z/4. The written construction +attains the general k-factor bound over every nonzero commutative ring. + +## Evidence and reproduction + +From the repository root, using CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/nonfield-one-relation +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/nonfield-one-relation/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/nonfield-one-relation/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/nonfield-one-relation --check-source-history +``` + +A reviewer may substitute their CPython 3.12 path. The direct verifier works +from a Git-free export. Expected marker: `PASS_NONFIELD_ONE_RELATION`. +Normal verification writes no files. Optional `--emit-to EXTERNAL_NEW_FILE` +creates a generated receipt containing all six source hashes and every result; +`--check-receipt FILE` recomputes and checks its canonical bytes. Creation +refuses overwrites and paths inside the package. No receipt is hand-written. + +The exact finite evidence checks the new composite-ring setting: + +- Enumerate every two-by-two matrix over Z/m for m=4,6,8,9,10,12. Retain + exactly 864 idempotents with zero determinant among 42,945 matrices. Compare the full + residue-rank histogram with the classical prime-power/CRT formula. +- Multiply every two-factor word on those projectors for m=4,6,8,9, using + independent frames A=diag(1,0), B=diag(0,1). Also multiply every three-factor + word over Z/4 with frames A,B,A, which have one relation. Compare every + coefficient after specialization on 45,821 words, and check disjoint assignment and the + sharper active-factor bound at all 85 diagonal monomial endpoints. +- Check the Z/6 partial-projector example, its glued endpoint, its rejection + as a global monomial before gluing, and the sharp rank-two Z/4 example. +- Nine rejection controls cover the zero ring, a map that is not a residue + quotient, failed idempotence, rank-two fibers, excess relations, nonunit + coefficients, off-diagonal endpoints, nonmonomial diagonal entries and + reduction of rational address labels modulo the characteristic. + +These finite checks corroborate the written extension. They do not prove +PR6044's universal field theorem or replace its review. + +## Limits and implementation + +Claim type: scoped written algebraic proof using a credited theorem, with +exact finite corroboration. No new kappa, physical supplier, selected-frontier +change or discharge of the five selected assumptions is claimed. No predecessor +scientific replay, Lean, Docker or selected cold replay is required or run. +Independent human and formal proof-kernel review are unclaimed. + +The new verifier has no recursion, network, subprocesses or dynamic code +loading. The matrix census visits at most 12^4 matrices per modulus; stored +projector lists have at most 325 entries. Words have at most three factors, +formal supports at most eight labels and assignment searches at most 27 +possibilities. Functions are below 60 lines. Explicit exceptions keep all +checks active under optimized Python. Python managed allocation is a deviation +from fixed allocation, bounded here by these fixed finite domains and one-MiB +source/receipt limits. A larger or externally parametrized replay would need +new capacities or a fixed-storage runtime. Warning-strict normal and optimized execution provide +the available diagnostics. No shared configuration or predecessor code changes. + +## Open next questions + +1. Can a surviving frame list with exactly two relations beat the rank floor + over a commutative ring? First seek such a field word, since the present + specialization transfers every qualifying field obstruction. A shorter + field endpoint and a complete native tariff remain missing. +2. Can a noncommutative coefficient ring evade this particular specialization + argument? First specify a ring, a paid alphabet and a diagonal endpoint. + The residue field and scalar rank-one decomposition used here need not + exist. No saving follows merely from that failure. + +Structured first steps and blockers are in [TASK.json](TASK.json). + +## Credit + +Credit Josie Elliston / PR6044 for the every-field one-relation theorem and +its explicit nonfield question. Credit Hanson Sun / PR1454, woklerx / PR1456, +theon199, Ali Romman / PR468, eumemic / PR288 and huxint / PR203 for the +retained register-model and one-relation lineage. Maximal-ideal reduction, +rank-one idempotent factorization over fields, CRT and prime-power projector +counts are classical. No general literature-priority claim is made. +[SOURCES.json](SOURCES.json) pins the predecessor statement and historical +orientation sources; no predecessor executable is imported. New files are +under Apache-2.0. diff --git a/research/nonfield-one-relation/SOURCES.json b/research/nonfield-one-relation/SOURCES.json new file mode 100644 index 0000000000..0bbd52b445 --- /dev/null +++ b/research/nonfield-one-relation/SOURCES.json @@ -0,0 +1,25 @@ +{ + "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/bit-one-relation-every-field/README.md", + "usage": "provenance", + "pin": "head:4ebdea4e95fa4cbf227b4be630f656105d96e5f7:research/bit-one-relation-every-field/README.md", + "git_blob": "e454cd51dd1b870fd83a48a829e7484c34044cc1", + "sha256": "6b40d96ad12201832626be9fdad2d8941e09a5f082f15e7bbe15709ebe0de654" + } + ] +} diff --git a/research/nonfield-one-relation/TASK.json b/research/nonfield-one-relation/TASK.json new file mode 100644 index 0000000000..d9d7c94800 --- /dev/null +++ b/research/nonfield-one-relation/TASK.json @@ -0,0 +1,88 @@ +{ + "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": "changed", + "actual_scope": "A residue-field extension of the one-relation paid-rank obstruction to nonzero commutative coefficient rings, with a sharper surviving-factor bound.", + "scope_change_reason": "Answer PR6044 Open next question 2. The changed coefficient ring is a scoped algebraic side result, rather than the card's completed larger/nonabelian native construction.", + "bottleneck_link": "Closes the commutative-ring escape from this low-relation register obstruction. It does not supply native conversion or improve the selected BIT budget.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved ring extension and sharp finite example; leave multiple-relation or noncommutative models to follow-on work.", + "outcome": "completed", + "evidence": "PROOF.md proves the extension using PR6044 as a cited premise. verify.py enumerates composite-ring projectors and checks formal specialization, disjoint assignment, sharp fixtures and nine rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a surviving frame list with exactly two relations beat the rank floor over a commutative ring?", + "why_it_matters": "Identifies the first relation dimension outside the transferred obstruction.", + "first_step": "Find one fully specified shorter field word before considering a ring lift.", + "blocked_by": "No such exact endpoint or complete native tariff is supplied." + }, + { + "question": "Can a noncommutative coefficient ring evade this specialization argument?", + "why_it_matters": "The residue-field proof depends on commutativity.", + "first_step": "Specify a noncommutative ring, its legal paid alphabet and a diagonal formal endpoint.", + "blocked_by": "A field quotient and scalar rank-one decomposition may be absent; no saving is established." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19372283", + "scientific_dependency": { + "pr": 6044, + "author": "JosieElliston", + "head": "4ebdea4e95fa4cbf227b4be630f656105d96e5f7", + "used_as": "Cited every-field theorem; no predecessor scientific replay." + }, + "environment": { + "python": "Python 3.12.15", + "platform": "macOS arm64", + "dependencies": "Python standard library only" + }, + "upstream_checkpoint": { + "commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "priority_revision": 8, + "selected_pr": 6030, + "utc": "2026-11-03T11:03:38Z" + } +} diff --git a/research/nonfield-one-relation/VERIFY.json b/research/nonfield-one-relation/VERIFY.json new file mode 100644 index 0000000000..82636a0f2f --- /dev/null +++ b/research/nonfield-one-relation/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact composite-ring projector census, all declared formal words, residue specialization, sharp examples and nine rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same finite evidence with optimization enabled and all explicit checks retained." + } + ] +} diff --git a/research/nonfield-one-relation/verify.py b/research/nonfield-one-relation/verify.py new file mode 100644 index 0000000000..39ae33b79e --- /dev/null +++ b/research/nonfield-one-relation/verify.py @@ -0,0 +1,296 @@ +#!/usr/bin/env python3 +"""Exact nonfield specialization checks. Standard library; no predecessor replay.""" + +import argparse +from collections import Counter +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path + + +MODULI = (4, 6, 8, 9, 10, 12) +PRIMES = (2, 3, 5) +ZERO = (0, 0, 0, 0) +IDENTITY = (1, 0, 0, 1) +PACKAGE_FILES = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", + "VERIFY.json", "verify.py") + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def mmul(a, b, modulus): + return ((a[0]*b[0]+a[1]*b[2]) % modulus, + (a[0]*b[1]+a[1]*b[3]) % modulus, + (a[2]*b[0]+a[3]*b[2]) % modulus, + (a[2]*b[1]+a[3]*b[3]) % modulus) + + +def reduced(a, modulus): + return tuple(value % modulus for value in a) + + +def residue_primes(modulus): + require(modulus in MODULI, "modulus outside the fixed composite corpus") + return tuple(p for p in PRIMES if modulus % p == 0) + + +def check_projector(a, modulus): + require(len(a) == 4, "matrix must be two by two") + require(mmul(a, a, modulus) == a, "matrix is not idempotent") + require((a[0]*a[3]-a[1]*a[2]) % modulus == 0, + "matrix has a rank-two residue fiber") + + +def local_projector_count(modulus, prime): + power = 1 + for exponent in range(1, 5): + power *= prime + if modulus % (power*prime) != 0: + return prime**(2*(exponent-1))*prime*(prime+1) + raise ValueError("prime-power exponent exceeds the fixed corpus") + + +def projector_census(modulus): + primes = residue_primes(modulus) + matrices = [] + histogram = Counter() + for a in product(range(modulus), repeat=4): + if mmul(a, a, modulus) != a: + continue + if (a[0]*a[3]-a[1]*a[2]) % modulus: + continue + check_projector(a, modulus) + pattern = tuple(int(reduced(a, p) != ZERO) for p in primes) + histogram[pattern] += 1 + matrices.append(a) + expected = {} + for pattern in product((0, 1), repeat=len(primes)): + count = 1 + for active, prime in zip(pattern, primes): + if active: + count *= local_projector_count(modulus, prime) + expected[pattern] = count + require(dict(histogram) == expected, "CRT/projector count mismatch") + return tuple(matrices), {"".join(map(str, key)): histogram[key] + for key in sorted(histogram)} + + +def accumulate(polynomial, exponent, matrix, modulus): + old = polynomial.get(exponent, ZERO) + value = tuple((x+y) % modulus for x, y in zip(old, matrix)) + if value == ZERO: + polynomial.pop(exponent, None) + else: + polynomial[exponent] = value + + +def formal_word(frames, projectors, modulus): + require(len(frames) == len(projectors) <= 3, "word length exceeds three") + polynomial = {(0, 0): IDENTITY} + for frame, projector in zip(frames, projectors): + require(len(frame) == 2, "frame exponent dimension must be two") + check_projector(projector, modulus) + complement = tuple((x-y) % modulus + for x, y in zip(IDENTITY, projector)) + following = {} + for exponent, matrix in polynomial.items(): + accumulate(following, exponent, mmul(matrix, complement, modulus), + modulus) + shifted = (exponent[0]+frame[0], exponent[1]+frame[1]) + accumulate(following, shifted, mmul(matrix, projector, modulus), + modulus) + require(len(following) <= 8, "formal support capacity exceeded") + polynomial = following + return polynomial + + +def reduce_polynomial(polynomial, modulus, prime): + require(prime in PRIMES and modulus % prime == 0, + "not a unital residue-field quotient of this ring") + result = {} + for exponent, matrix in polynomial.items(): + value = reduced(matrix, prime) + if value != ZERO: + result[exponent] = value + return result + + +def diagonal_endpoint(polynomial): + if any(matrix[1] or matrix[2] for matrix in polynomial.values()): + return None + endpoint = [] + for diagonal in (0, 3): + terms = [(key, matrix[diagonal]) for key, matrix in polynomial.items() + if matrix[diagonal]] + if len(terms) != 1 or terms[0][1] != 1: + return None + endpoint.append(terms[0][0]) + return tuple(endpoint) + + +def assignments(frames): + require(len(frames) <= 3, "assignment capacity exceeded") + endpoints = set() + for owners in product(range(3), repeat=len(frames)): + rows = [[0, 0], [0, 0]] + for owner, frame in zip(owners, frames): + if owner < 2: + rows[owner][0] += frame[0] + rows[owner][1] += frame[1] + endpoints.add(tuple(tuple(row) for row in rows)) + return endpoints + + +def eligible(frames): + """For this fixture, A=diag(1,0) and B=diag(0,1).""" + require(all(frame in ((1, 0), (0, 1)) for frame in frames), + "frame outside the two-axis fixture") + require(len(frames)-len(set(frames)) <= 1, + "active frame list has more than one rational relation") + + +def check_word(frames, projectors, modulus, possible_endpoints): + ring_word = formal_word(frames, projectors, modulus) + endpoint = diagonal_endpoint(ring_word) + for prime in residue_primes(modulus): + images = tuple(reduced(n, prime) for n in projectors) + specialized = formal_word(frames, images, prime) + require(reduce_polynomial(ring_word, modulus, prime) == specialized, + "specialization does not preserve the full formal word") + if endpoint is not None: + active = tuple(frame for frame, n in zip(frames, images) if n != ZERO) + eligible(active) + require(endpoint in assignments(active), "disjoint assignment failed") + rank_sum = sum(int(value != 0) for row in endpoint for value in row) + require(rank_sum <= len(active), "active-fiber paid-rank floor failed") + if endpoint is not None: + require(endpoint in possible_endpoints, "global assignment failed") + return endpoint is not None + + +def word_census(projectors): + counts = {} + independent_frames = ((1, 0), (0, 1)) + possible = assignments(independent_frames) + for modulus in (4, 6, 8, 9): + diagonal = 0 + matrices = projectors[modulus] + for word in product(matrices, repeat=2): + diagonal += check_word(independent_frames, word, modulus, possible) + counts[str(modulus)+"_independent"] = { + "words": len(matrices)**2, "diagonal_endpoints": diagonal} + related_frames = ((1, 0), (0, 1), (1, 0)) + possible = assignments(related_frames) + diagonal = 0 + for word in product(projectors[4], repeat=3): + diagonal += check_word(related_frames, word, 4, possible) + counts["4_one_relation"] = { + "words": len(projectors[4])**3, "diagonal_endpoints": diagonal} + return counts + + +def fixtures(): + partial = (3, 0, 0, 0) + complement = (4, 0, 0, 0) + a = (1, 0) + require(diagonal_endpoint(formal_word((a,), (partial,), 6)) is None, + "a component-dependent monomial was accepted globally") + glued = formal_word((a, a), (partial, complement), 6) + require(diagonal_endpoint(glued) == (a, (0, 0)), "CRT gluing failed") + for prime in (2, 3): + require(sum(reduced(n, prime) != ZERO for n in (partial, complement)) == 1, + "partial-projector active count failed") + sharp = formal_word(((1, 0), (0, 1)), ((1, 0, 0, 0),)*2, 4) + require(diagonal_endpoint(sharp) == ((1, 1), (0, 0)), + "sharp rank-two target or dirty restoration failed") + return {"partial_projector_modulus": 6, "glued_paid_factors": 2, + "active_factors_in_each_residue": 1, "sharp_rank_sum": 2, + "sharp_paid_factors": 2} + + +def controls(): + rejected = 0 + cases = (("modulus", 1), ("quotient", 5), ("idempotent", (0, 1, 0, 0)), + ("rank", IDENTITY), ("relations", ((1, 0),)*3)) + for kind, value in cases: + try: + if kind == "modulus": + residue_primes(value) + elif kind == "quotient": + reduce_polynomial({(0, 0): IDENTITY}, 6, value) + elif kind in ("idempotent", "rank"): + check_projector(value, 4) + else: + eligible(value) + except ValueError: + rejected += 1 + else: + raise ValueError("a negative control was accepted") + require(diagonal_endpoint({(0, 0): (2, 0, 0, 1)}) is None, + "nonunit endpoint coefficient accepted") + require(diagonal_endpoint({(0, 0): (1, 1, 0, 1)}) is None, + "off-diagonal endpoint accepted") + require(diagonal_endpoint({(0, 0): IDENTITY, (1, 0): (1, 0, 0, 0)}) is None, + "two-term diagonal accepted as a monomial") + twice = formal_word(((1, 0),)*2, ((1, 0, 0, 0),)*2, 2) + require(diagonal_endpoint(twice) == ((2, 0), (0, 0)), + "rational address labels were reduced modulo the characteristic") + return rejected+4 + + +def report(): + projectors = {} + histograms = {} + for modulus in MODULI: + projectors[modulus], histograms[str(modulus)] = projector_census(modulus) + return {"schema": "nonfield-one-relation-checks/1", + "claim_type": "scoped proof using PR6044 as a cited premise", + "projector_histograms": histograms, + "word_censuses": word_census(projectors), + "fixtures": fixtures(), "rejection_controls": controls()} + + +def read_limited(path): + with path.open("rb") as handle: + data = handle.read(1_048_577) + require(len(data) <= 1_048_576, "file exceeds one MiB") + return data + + +def bound_receipt(result): + root = Path(__file__).resolve().parent + hashes = {} + for name in PACKAGE_FILES: + data = read_limited(root/name) + hashes[name] = sha256(data).hexdigest() + return {"result": result, "source_sha256": hashes} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit-to", type=Path) + parser.add_argument("--check-receipt", type=Path) + options = parser.parse_args() + result = report() + receipt = bound_receipt(result) + encoded = json.dumps(receipt, sort_keys=True, indent=2)+"\n" + if options.check_receipt is not None: + data = read_limited(options.check_receipt) + # Canonical bytes also reject JSON true substituted for integer one. + require(data.decode("utf-8") == encoded, "receipt or source hashes differ") + if options.emit_to is not None: + root = Path(__file__).resolve().parent + require(not options.emit_to.resolve().is_relative_to(root), + "receipt must be outside the package") + with options.emit_to.open("x", encoding="utf-8") as handle: + require(handle.write(encoded) == len(encoded), "short receipt write") + print(json.dumps(result, sort_keys=True)) + print("PASS_NONFIELD_ONE_RELATION") + + +if __name__ == "__main__": + main()