diff --git a/research/p104-rank-seven-error-floor/PROOF.md b/research/p104-rank-seven-error-floor/PROOF.md new file mode 100644 index 0000000000..08778cc91f --- /dev/null +++ b/research/p104-rank-seven-error-floor/PROOF.md @@ -0,0 +1,121 @@ +# Sharp error for every real rank-seven Gram approximation + +## Statement and scope + +Let the rows of R be one representative of squared norm 2 from each of +the 56 D8 lines e_i +/- e_j in R^8, together with any proper subset of +the 64 half-spin lines of one parity. Write m for the number of rows and +K=RR^T/2. Then + + min { max_ij |K_ij-C_ij| : C in R^(m x m), rank C <= 7 } = 1/4. + +There is no assumption on C's symmetry, sign, spectrum, or row and column +spaces. In particular C need not have the form RDR^T/2. This strengthens +Nick Petalas's PR6183 theorem for symmetric positive contractive carrier +filters, answering its first open question and the larger unrestricted +real-matrix question. Its attaining projection is retained with credit. + +The theorem uses the full coefficient matrix, real scalars, and the fixed +Gram target. It is not a statement about masked entries, complex matrices, +nonlinear consumers, a changed total target, or physical implementation cost. + +## Eight columns detect every deficient-rank candidate + +Choose the eight retained column labels J corresponding to + + e_1+e_2, e_1-e_2, e_3+e_4, e_3-e_4, + e_5+e_6, e_5-e_6, e_7+e_8, e_7-e_8. + +Let U=R[J,:]. Stored representatives may differ by row signs. These roots +are mutually orthogonal with squared norm 2, so UU^T=U^TU=2I. + +For arbitrary C of rank at most seven, the m-by-8 submatrix C[:,J] has +a nonzero real null vector a. Put z=U^T a. Then z is nonzero, +a=Uz/2, and K[:,J]a=Rz/2. For real s,t, + + (|s+t|+|s-t|)/2 = max(|s|,|t|). + +Consequently, writing b_1>=...>=b_8 for the sorted absolute coordinates +of z and h=b_1+b_2>0, + + ||a||_1 = sum_(four coordinate pairs) max(|z_i|,|z_j|) + <= b_1+b_2+b_3+b_4 <= 2h. + +The first inequality holds because the four maxima select four distinct +coordinates; the second uses b_3<=b_1 and b_4<=b_2. Row sign choices in +U do not change its left-hand side. The retained D8 roots include a signed +root joining the two largest absolute coordinates of z. Hence + + ||Rz||_infinity >= h. + +The extra half-spin rows may make this inequality strict. If +epsilon=max_ij |K_ij-C_ij|, coefficientwise triangle inequality gives + + h/2 <= ||K[:,J]a||_infinity + = ||(K-C)[:,J]a||_infinity + <= epsilon ||a||_1 <= 2 epsilon h. + +Divide by h to obtain epsilon>=1/4. This is an all-real-matrix proof, +not an inference from the finite verifier. It uses only the D8 rows and +eight D8 columns; no projection back to the carrier spaces is needed. + +Equivalently, an approximation with entry error strictly below 1/4 must +have eight independent columns at J, and therefore rank at least eight. +The norm ratio is sharp: take z with one nonzero coordinate in each of +the four pairs, all of the same magnitude. Then ||a||_1=2h. + +## Attainment (PR6183's construction) + +Choose an omitted half-spin root q. It has squared norm 2. Set + + D = I-qq^T/2, + C = RDR^T/2 = K-(Rq)(Rq)^T/4. + +D is a rank-seven orthogonal projector. R has column rank eight because +it contains U. Therefore C has rank seven: a left inverse of R shows +rank D<=rank(RDR^T), and the opposite inequality is immediate. + +For every D8 root r, r dot q belongs to {-1,0,1}. For two distinct lines +in the same half-spin parity shell, their sign patterns differ in an +even number of coordinates, and the inner product also belongs to +{-1,0,1}. The line of q is absent, so + + |K_ij-C_ij| = |(r_i dot q)(r_j dot q)|/4 <= 1/4. + +A D8 root has inner product of magnitude one with q; its diagonal error +is 1/4. This proves attainment, including when the half-spin subset is +empty. No optimality or invention of this projection is attributed here. + +## P104 binding, precision consequence, and limits + +Matarener's PR6166 at 096938513138868f0ed27639061f1a5054900f96 identifies +the relevant P104 configuration with all 56 D8 lines plus 48 half-spin +lines in orthonormal coordinates. This identification remains a cited +premise, as it was in PR6183; it is not independently audited here. +The source-pinned MISSING.json from PR6183 records its sixteen omitted +lines. The verifier constructs and checks the resulting mathematical +root set and the sixteen attaining matrices. That is distinct from +checking the physical selected ports' coordinate identification. + +PR6183 at eaf77790466f34b86ce72080e3ec690e26dfacab supplies the preceding +question, Gram convention and attaining projection. Rohan Arun's PR1972, +Chafik Boukhalfa's PR1991 and their retained lineage supply the earlier +Gram channel. Their native/operator theorems are not replayed or adopted +as new results here. + +For any real rank-seven C, some entry (i,j) of K-C has magnitude at least +1/4. On input B e_j the i-th output bias is at least |B|/4. Unlike the +positive-error predecessor, this argument need not locate a diagonal +entry. The maximum-entry norm here equals the induced l1-to-l_infinity +norm; the theorem does not assert an l2 operator-norm optimum. +Increasing arithmetic precision cannot make this fixed approximation +bias vanish. Any changed side correction or consumer must account for it. + +This closes arbitrary real linear rank-seven replacement of this whole +Gram block. It does not price corrections, transport, restoration, +native calls, compiler operations, precision/tape work or the completed +supplier. No selected framework assumption is discharged and no kappa +improvement follows. General literature priority, independent human +review and formal proof-kernel acceptance are unclaimed. + +Prepared by apoursh with substantial OpenAI Codex assistance. Apache-2.0. diff --git a/research/p104-rank-seven-error-floor/README.md b/research/p104-rank-seven-error-floor/README.md new file mode 100644 index 0000000000..ffab6d53c8 --- /dev/null +++ b/research/p104-rank-seven-error-floor/README.md @@ -0,0 +1,116 @@ +# Every real rank-seven P104 Gram approximation has error at least 1/4 + +The exact minimum maximum coefficient error is **1/4 over all real +104-by-104 matrices of rank at most seven**. This removes symmetry, +positivity, contractivity, and fixed carrier row/column spaces from +Nick Petalas's [PR6183](https://github.com/CrocSwap/integer-mult-bounds/pull/6183) +result. It answers that package's first open question. No new kappa is claimed. + +Eight orthogonal D8 root columns turn any deficient-rank candidate into +a nonzero null vector. A sharp l1 norm comparison forces the error floor. +PR6183's omitted-root projector attains it. The [written proof](PROOF.md) +covers every real candidate; exact finite checks corroborate its identities +and exercise candidates outside the predecessor's domain. + +The P104 coordinate identification remains an explicitly cited premise +from Matarener's PR6166, retained through PR6183. This contribution verifies +the resulting root configuration, not its physical port identification. +Both predecessors are archived as partially reviewed in the current ledger; +archival inclusion is not scientific acceptance. +The theorem also applies to all D8 lines plus any proper subset of one +half-spin shell. Root representative signs do not matter. + +## Reproduce + +With CPython 3.12 and the standard library, from the repository root: + +```sh +python3.12 -I -W error -B research/p104-rank-seven-error-floor/verify.py +python3.12 -I -W error -O -B research/p104-rank-seven-error-floor/verify.py +python3.12 -I -W error -O -B research/p104-rank-seven-error-floor/independent.py +python3.12 -B scripts/research_package.py --package research/p104-rank-seven-error-floor +``` + +The direct marker is `PASS_P104_RANK_SEVEN_ERROR_FLOOR`; the registered +marker is `PASS_REGISTERED_RESEARCH_PACKAGE`. Direct runs read only and +emit a deterministic JSON receipt with computed coverage counts. They work +in a Git-free export with an empty PATH when Python is invoked absolutely. +SOURCES.json authenticates the three predecessor document/data inputs; +VERIFY.json declares all of them. No predecessor executable is imported. + +The checks cover the orthogonal eight-column frame, exact null-vector norm +inequalities, all sixteen attaining projections and every matrix entry, +oblique filters, candidates with row/column spaces outside the root code, +and hypothesis/normalization controls. Normal and optimized replay pass +6,560 nonzero ternary directions, 128 rational directions, sixteen projections +with 173,056 literal matrix-error entries, three carrier fixtures and one +candidate outside both carrier spaces. Four boundary/normalization controls +and three malformed-input rejections also pass. The proof, rather than these +finite fixtures, establishes the universal quantifier. See the emitted receipt +for exact counts and [TASK.json](TASK.json) for verification coverage. + +The separately written `independent.py` uses literal Fraction roots and a +different root order, with no primary-checker import. Its optimized registered +replay passes 147 vector fixtures (including two tight norm witnesses) and +194,688 matrix entries across sixteen attaining projectors, an oblique +projector (error 3/8), and a matrix outside the carrier factorization +(error 1/2). It corroborates arithmetic and scope boundaries; it does not +mechanically prove the universal statement or constitute human review. + +## Selection, overlap, and expansion decision + +Canonical main was pulled first at +`a5bff3bf133e482541c09eba4e773884bdb2b1b7`, priority revision 8. The selected +record still specifies conditional kappa `781451/250000000` with five +framework assumptions. Its previously passing binding-only orientation +was reused after all 1,227 recorded inputs were unchanged from the prior +checkpoint; this is not a fresh scientific replay. + +This takes the released [PR6183 handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19268192). +The original `coverage-law-change` card is retained in TASK.json, with +scope explicitly changed to an algebraic approximation question. The +[canonical investigation](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19271534) +records the initial arbitrary-carrier question and its extension to all +real rank-seven matrices. Bounded all-state PR searches and the newest +visible handoffs found no competing result. The local overlap helper +searched only 28 of 8,623 notes and had no remote cache; neither it nor +the bounded live search certifies exhaustive novelty. + +Nearest work: PR6183 proves the contractive case and provides attainment; +PR6181 concerns exact joint-bank spectral conjugacy over Gaussian dyadics; +PR6173 concerns generalized code support over F3 and Q. Their different +quantities are not compared numerically or silently treated as validated. + +Decision: close this approximation escape, then stop. The boundary is the +whole real Gram block on arbitrary inputs. A seven-dimensional real linear +intermediate cannot approximate it arbitrarily accurately, even with new +encoder/decoder spaces. Correction, native implementation, restoration +and complete costs remain unknown. This local proof justifies no further +construction campaign or selected-frontier change on its own. + +## Open next questions + +- Can a changed side correction absorb an attaining residual at a favorable + complete cost? Start with one omitted-root residual in an actual scalar + word, charging acquisition, delivery and restoration. A physical caller + and complete invoice are missing. This is PR6183's remaining second question. +- What is the optimum for arbitrary **complex** rank-seven approximants? + The real absolute-value identity used here does not hold for complex + coordinates. Start with a dual norm certificate or an exact complex + factorization beating 1/4; numerical searches alone cannot settle it. + No complex lower bound or physical realization is supplied. + +## Credit and limits + +New lower-bound proof and verifier: apoursh, with substantial OpenAI Codex +assistance and separate agent proof checks. Nick Petalas retains PR6183's +question, contractive theorem and attaining projection. Matarener retains +the D8 coordinate identification and omitted lines. Rohan Arun, Chafik +Boukhalfa, Ali Romman, DreamingOfClouds, Cinna Davis, Pierre-Loic Doulcet, +icekylinx, zxv, Jacob Alan Sussman and the retained P104/root/frame/native/ +helper/compiler/BIT contributors retain their source results. + +This is a scoped written proof with exact finite corroboration, not a +physical supplier, full multiplication theorem, independent human review, +or formal proof-kernel result. Masked accuracy and nonlinear consumers +remain outside scope. Sources and shared code are unchanged. Apache-2.0. diff --git a/research/p104-rank-seven-error-floor/SOURCES.json b/research/p104-rank-seven-error-floor/SOURCES.json new file mode 100644 index 0000000000..7c6e80cb7d --- /dev/null +++ b/research/p104-rank-seven-error-floor/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7", + "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/p104-contractive-gram-deflation/MISSING.json", + "usage": "input", + "git_blob": "d5f76681db5edb99899ce6509913b0db60f7280c", + "sha256": "9ddfcf087912e02c46722d5a82eea5f1221a4a33d5037a0d90d392dfcd3c06d4" + }, + { + "path": "research/p104-contractive-gram-deflation/PROOF.md", + "usage": "input", + "git_blob": "2cf92ff47f0271c6fd2266884a1b307a09b35c63", + "sha256": "8e44fe3d11d777535131e0a4c7cdde8fbc4c0d2b69254e587432c71ce39a61a6" + }, + { + "path": "research/p104-contractive-gram-deflation/README.md", + "usage": "input", + "git_blob": "d3a11f74d5c908d7b9bf28235c36ea9850e458b3", + "sha256": "5643af3d891e2731237c0f8a4ae97d5ae0515b03d369e835fbf80cc612821415" + } + ] +} diff --git a/research/p104-rank-seven-error-floor/TASK.json b/research/p104-rank-seven-error-floor/TASK.json new file mode 100644 index 0000000000..f3b13e34aa --- /dev/null +++ b/research/p104-rank-seven-error-floor/TASK.json @@ -0,0 +1,100 @@ +{ + "schema_version": 1, + "task_id": "coverage-law-change", + "priority_revision": 8, + "base_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7", + "original_card": { + "id": "coverage-law-change", + "question": "Can a completed call earn more independent productive target credit without an offsetting paid bill?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Use #5599 as a completed positive control, then choose one uncovered cut/module beyond an applicable frozen exclusion. Derive independence, saturation and chronological availability rather than counting rational rank alone. Price target credits and all new jobs together, then check compiler and actual caller compatibility. Stop on a nonphysical credit or an unfavorable complete relaxation.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "target credit", + "helper split", + "coverage law" + ], + "existing_checks": [ + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Sharp maximum-entry error 1/4 for every real matrix of rank at most seven approximating the complete D8 plus partial half-spin Gram block; P104 identification remains cited.", + "scope_change_reason": "Takes PR6183 Open next question 1 after the released handoff. The native coverage-law card is narrowed to an algebraic carrier-saving decision. The initial arbitrary-carrier claim was strengthened to all real low-rank matrices by an eight-column null-vector argument; this does not satisfy the full supplier acceptance gate.", + "bottleneck_link": "Rules out vanishing-error replacement of the complete P104 Gram block through seven real linear intermediates, even with arbitrary encoder and decoder spaces. A fixed coefficient bias cannot be repaired by arithmetic precision alone; changed correction and full physical costs remain open.", + "budget_minutes": 60, + "stop_rule": "Finish the first sharp proof and bounded corroboration; no wider construction or parameter search.", + "outcome": "negative-result", + "evidence": "PROOF.md establishes the universal result. Registered Python 3.12 normal and optimized runs pass: 6560 nonzero ternary directions, 128 rational directions, 16 attaining projectors, 173056 literal matrix-error entries, three carrier fixtures, a rank-seven candidate outside both carrier spaces, four boundary/normalization controls and three malformed-input rejections. Separate agent proof/code audits found no blocker; no human or formal-kernel review is claimed. Separately written independent.py passes 147 vector fixtures and 194688 full matrix entries over sixteen attaining projections, an oblique projector and a candidate outside the carrier factorization. Source-byte corruption is rejected before replay. The registered three-command run passes in about 4.4 seconds locally.", + "author": "apoursh", + "ai_assistance": "Substantial OpenAI Codex assistance, including separate agent mathematical audits and a separately written arithmetic corroboration. No independent human or formal proof-kernel review claimed.", + "open_questions": [ + { + "question": "Can a changed side correction absorb an attaining rank-one residual with a favorable complete invoice?", + "why_it_matters": "The approximation obstruction does not forbid a different complete construction.", + "first_step": "Trace one omitted-root residual through an actual scalar word and charge acquisition, delivery and restoration.", + "blocked_by": "No physical caller or complete invoice is supplied." + }, + { + "question": "What is the sharp maximum-entry error for arbitrary complex rank-seven approximants?", + "why_it_matters": "The real two-coordinate absolute-value identity does not extend to complex coordinates.", + "first_step": "Find an exact complex witness below 1/4 or a valid dual norm lower-bound certificate.", + "blocked_by": "No complex lower bound or physical realization is supplied." + } + ], + "coordination": { + "url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19271534", + "handoff": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19268192", + "seed": "1ef70b206102747a3010a0c5f0ad669b", + "scope_key": "2bf6355a8dd01ca324fb" + }, + "refresh": { + "upstream_commit": "a5bff3bf133e482541c09eba4e773884bdb2b1b7", + "checked_utc": "2026-10-29T15:53:20Z", + "priority_revision": 8, + "guidance_changed": false, + "pre_submission_utc": "2026-10-29T16:03:01Z", + "pre_submission_main": "a5bff3bf133e482541c09eba4e773884bdb2b1b7" + }, + "orientation": { + "mode": "source-bound reuse of prior binding-only PASS, not scientific replay", + "prior_checkpoint": "3f0152a32eeebac0df11946dbd50cabe5a7f7839", + "recorded_inputs": 1227, + "changed_recorded_inputs": 0, + "selected_record_sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + } +} diff --git a/research/p104-rank-seven-error-floor/VERIFY.json b/research/p104-rank-seven-error-floor/VERIFY.json new file mode 100644 index 0000000000..20cc1bebe5 --- /dev/null +++ b/research/p104-rank-seven-error-floor/VERIFY.json @@ -0,0 +1,51 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-contractive-gram-deflation/MISSING.json", + "research/p104-contractive-gram-deflation/PROOF.md", + "research/p104-contractive-gram-deflation/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact orthogonal frame, real null-vector norm inequality, attaining projections, arbitrary rank-seven factors outside the carrier code, and hypothesis/rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact orthogonal frame, real null-vector norm inequality, attaining projections, arbitrary rank-seven factors outside the carrier code, and hypothesis/rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 120, + "checks": "Separately written Fraction-root corroboration: 147 directions, literal full matrices for sixteen attaining projectors, an oblique projector and a candidate outside fixed carrier factorization." + } + ] +} diff --git a/research/p104-rank-seven-error-floor/independent.py b/research/p104-rank-seven-error-floor/independent.py new file mode 100644 index 0000000000..4eacc39192 --- /dev/null +++ b/research/p104-rank-seven-error-floor/independent.py @@ -0,0 +1,158 @@ +#!/usr/bin/env python3 +"""Independent rational corroboration of the eight-column rank obstruction. + +Prepared by apoursh with substantial OpenAI Codex assistance. Apache-2.0. +No primary or predecessor executable code is imported. +""" +import argparse +import hashlib +import itertools +import json +from fractions import Fraction as F +from pathlib import Path + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def dot(x, y): + return sum((a * b for a, b in zip(x, y, strict=True)), F(0)) + + +def transpose(matrix): + return [list(column) for column in zip(*matrix, strict=True)] + + +def multiply(a, b): + columns = transpose(b) + return [[dot(row, column) for column in columns] for row in a] + + +def rank(matrix): + a = [list(map(F, row)) for row in matrix] + pivot = 0 + for column in range(len(a[0])): + found = next((i for i in range(pivot, len(a)) if a[i][column]), None) + if found is None: + continue + a[pivot], a[found] = a[found], a[pivot] + denominator = a[pivot][column] + a[pivot] = [value / denominator for value in a[pivot]] + for row in range(pivot + 1, len(a)): + scale = a[row][column] + if scale: + a[row] = [x - scale * y for x, y in zip(a[row], a[pivot], strict=True)] + pivot += 1 + if pivot == min(len(a), len(a[0])): + break + return pivot + + +def roots(path): + raw = path.read_bytes() + need(hashlib.sha256(raw).hexdigest() == + '9ddfcf087912e02c46722d5a82eea5f1221a4a33d5037a0d90d392dfcd3c06d4', + 'pinned omitted-root source bytes') + data = json.loads(raw) + omitted = {tuple(F(1 if c == '+' else -1, 2) for c in s) for s in data['signs']} + omitted = {q if q[0] > 0 else tuple(-x for x in q) for q in omitted} + need(len(omitted) == 16, 'sixteen distinct omitted lines') + shell = {tuple(F(x, 2) for x in (1, *tail)) + for tail in itertools.product((1, -1), repeat=7) if tail.count(-1) % 2} + need(omitted <= shell, 'omitted parity and coordinates') + ordinary = [] + for i, j in itertools.combinations(range(8), 2): + for sign in (1, -1): + row = [F(0)] * 8 + row[i], row[j] = F(1), F(sign) + ordinary.append(tuple(row)) + retained = ordinary + sorted(shell - omitted) + need(len(retained) == 104, '104 roots') + return retained, sorted(omitted) + + +def frame_indices(retained): + indices = [] + for i in range(0, 8, 2): + for sign in (1, -1): + row = [F(0)] * 8 + row[i], row[i + 1] = F(1), F(sign) + indices.append(retained.index(tuple(row))) + return indices + + +def vector_checks(retained, frame): + vectors = [[F(((k + 3) * (i + 5) ** 2) % 29 - 14, (i + k) % 5 + 1) + for i in range(8)] for k in range(137)] + vectors += [[F(int(i % 2 == parity)) for i in range(8)] for parity in (0, 1)] + vectors += [[F(int(i == j)) for i in range(8)] for j in range(8)] + tight = 0 + for z in vectors: + a = [dot(row, z) / 2 for row in frame] + need([dot(column, a) for column in transpose(frame)] == z, 'frame inverse') + ordered = sorted(map(abs, z), reverse=True) + h = sum(ordered[:2]) + mass = sum(map(abs, a)) + paired = sum(max(abs(z[i]), abs(z[i + 1])) for i in range(0, 8, 2)) + need(mass == paired and mass <= sum(ordered[:4]) <= 2 * h, 'real pair norm bound') + need(max(abs(dot(r, z)) for r in retained[:56]) == h, 'D8 support function') + # A second, unrelated decomposition also bounds the D8 atomic mass. + layer_mass = ordered[0] + sum(ordered[2:]) / 2 + need(layer_mass <= 2 * h, 'layer decomposition bound') + tight += int(mass == 2 * h) + return len(vectors), tight + + +def candidate(retained, indices, target, d, left=None, right=None): + left = retained if left is None else left + right = retained if right is None else right + c = [[x / 2 for x in row] for row in multiply(multiply(left, d), transpose(right))] + minor = [[c[i][j] for j in indices] for i in indices] + need(rank(d) == 7 and rank(minor) == 7, 'rank-seven factor and witness minor') + error = max(abs(x - y) for row, other in zip(target, c, strict=True) + for x, y in zip(row, other, strict=True)) + need(error >= F(1, 4), 'rank-seven error floor') + return error, c + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--missing', type=Path) + args = parser.parse_args() + source = args.missing or Path(__file__).resolve().parents[1] / 'p104-contractive-gram-deflation/MISSING.json' + r, omitted = roots(source) + j = frame_indices(r) + u = [r[i] for i in j] + need(multiply(u, transpose(u)) == [[F(2 * (i == k)) for k in range(8)] for i in range(8)], 'orthogonal frame') + count, tight = vector_checks(r, u) + target = [[x / 2 for x in row] for row in multiply(r, transpose(r))] + for q in omitted: + d = [[F(i == k) - q[i] * q[k] / 2 for k in range(8)] for i in range(8)] + need(multiply(d, d) == d, 'projector identity') + error, unused = candidate(r, j, target, d) + need(error == F(1, 4), 'attaining exact quarter') + q = omitted[0] + w = [q[0], -q[1], *([F(0)] * 6)] + d = [[F(i == k) - q[i] * (q[k] + w[k]) / 2 for k in range(8)] for i in range(8)] + need(d != transpose(d) and multiply(d, d) == d, 'oblique projector') + oblique, unused = candidate(r, j, target, d) + d = [[F(i == k) - q[i] * q[k] / 2 for k in range(8)] for i in range(8)] + outside = next(i for i in range(len(r)) if i not in j) + left, right = [list(row) for row in r], [list(row) for row in r] + left[outside][0] += 1 + right[outside][1] -= 1 + unrestricted, c = candidate(r, j, target, d, left, right) + recovered = multiply(multiply(transpose(u), [[c[i][k] for k in j] for i in j]), u) + recovered = [[x / 2 for x in row] for row in recovered] + carrier = [[x / 2 for x in row] for row in multiply(multiply(r, recovered), transpose(r))] + need(c != carrier, 'candidate outside fixed carrier factorization') + print('PASS_INDEPENDENT_RANK_SEVEN_ERROR ' + json.dumps({ + 'rational_vectors': count, 'sharp_norm_vectors': tight, + 'attaining_projectors': len(omitted), 'literal_matrix_entries': (len(omitted) + 2) * len(r) ** 2, + 'oblique_error': str(oblique), 'outside_carrier_error': str(unrestricted)}, sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/p104-rank-seven-error-floor/verify.py b/research/p104-rank-seven-error-floor/verify.py new file mode 100644 index 0000000000..27177fadc2 --- /dev/null +++ b/research/p104-rank-seven-error-floor/verify.py @@ -0,0 +1,278 @@ +#!/usr/bin/env python3 +"""Exact fixtures for the unrestricted P104 rank-seven error theorem. + +Prepared by apoursh with substantial OpenAI Codex assistance. Apache-2.0. +Nick Petalas retains the attaining projection; Matarener the cited root data. +""" + +import hashlib +import itertools +import json +from fractions import Fraction as F +from pathlib import Path + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def dot(a, b): + return sum(x * y for x, y in zip(a, b, strict=True)) + + +def transpose(matrix): + return list(map(list, zip(*matrix, strict=True))) + + +def multiply(a, b): + columns = transpose(b) + return [[dot(row, column) for column in columns] for row in a] + + +def reduce_rows(matrix): + rows = [[F(x) for x in row] for row in matrix] + pivots = [] + for column in range(len(rows[0])): + pivot = next((i for i in range(len(pivots), len(rows)) if rows[i][column]), None) + if pivot is None: + continue + row_index = len(pivots) + rows[row_index], rows[pivot] = rows[pivot], rows[row_index] + divisor = rows[row_index][column] + rows[row_index] = [x / divisor for x in rows[row_index]] + for i in range(len(rows)): + if i != row_index and rows[i][column]: + scale = rows[i][column] + rows[i] = [x - scale * y for x, y in zip(rows[i], rows[row_index], strict=True)] + pivots.append(column) + return rows, pivots + + +def rank(matrix): + return len(reduce_rows(matrix)[1]) + + +def kernel_vector(matrix): + rows, pivots = reduce_rows(matrix) + free = next((j for j in range(len(matrix[0])) if j not in pivots), None) + need(free is not None, "kernel is required") + vector = [F(j == free) for j in range(len(matrix[0]))] + for i, pivot in enumerate(pivots): + vector[pivot] = -rows[i][free] + need(any(vector) and all(dot(row, vector) == 0 for row in matrix), "kernel residual") + return vector + + +def canonical(vector): + first = next((x for x in vector if x), 0) + need(len(vector) == 8 and first != 0, "nonzero eight-coordinate vector") + return tuple(x if first > 0 else -x for x in vector) + + +def build_roots(data): + signs = data.get("signs") + need(isinstance(signs, list) and len(signs) == 16, "sixteen omitted lines") + omitted = set() + for row in signs: + need(isinstance(row, str) and len(row) == 8 and set(row) <= {"+", "-"}, "sign row") + need(row.count("-") % 2 == 1, "odd half-spin parity") + omitted.add(canonical(tuple(1 if s == "+" else -1 for s in row))) + need(len(omitted) == 16, "distinct omitted lines") + d8 = [] + for i, j in itertools.combinations(range(8), 2): + for sign in (-1, 1): + row = [0] * 8 + row[i], row[j] = 2, sign * 2 + d8.append(tuple(row)) + half = {(1, *tail) for tail in itertools.product((-1, 1), repeat=7) + if tail.count(-1) % 2 == 1} + need(omitted <= half, "omitted lines belong to shell") + roots = sorted(set(d8) | (half - omitted)) + need(len(d8) == 56 and len(half - omitted) == 48 and len(roots) == 104, "shell sizes") + need(all(dot(row, row) == 8 for row in roots), "doubled root norms") + return d8, roots, sorted(omitted) + + +def paired_columns(roots): + u = [] + for i in range(0, 8, 2): + for sign in (1, -1): + row = [0] * 8 + row[i], row[i + 1] = 1, sign + u.append(row) + indices = [roots.index(tuple(2 * x for x in row)) for row in u] + need(multiply(u, transpose(u)) == [[2 * (i == j) for j in range(8)] for i in range(8)], + "paired D8 basis orthogonality") + return u, indices + + +def norm_fixture(vector, u, d8): + absolute = sorted(map(abs, vector), reverse=True) + h = absolute[0] + absolute[1] + need(h > 0, "nonzero direction") + coefficient_norm = sum(abs(dot(row, vector)) / F(2) for row in u) + pair_max = sum(max(abs(vector[i]), abs(vector[i + 1])) for i in range(0, 8, 2)) + need(coefficient_norm == pair_max <= sum(absolute[:4]) <= 2 * h, "fixed-pair norm inequality") + need(max(abs(dot(row, vector)) for row in d8) == 2 * h, "D8 support functional") + + +def direction_fixtures(u, d8): + integer_count = 0 + for vector in itertools.product((-1, 0, 1), repeat=8): + if any(vector): + norm_fixture(vector, u, d8) + integer_count += 1 + rational_count = 0 + for t in range(1, 129): + vector = [F(((t + 3) * (j + 5) ** 2) % 37 - 18, 1 + (t + 2 * j) % 11) for j in range(8)] + need(any(vector), "rational fixture nonzero") + norm_fixture(vector, u, d8) + rational_count += 1 + return integer_count, rational_count + + +def attaining_projectors(roots, omitted, indices): + entries = 0 + for q in omitted: + d = [[8 * (i == j) - q[i] * q[j] for j in range(8)] for i in range(8)] + need(multiply(d, d) == [[8 * x for x in row] for row in d], "projector idempotence") + need(rank(d) == 7 and all(dot(row, q) == 0 for row in d), "rank-seven projector") + products = [dot(row, q) for row in roots] + candidate = multiply(multiply(roots, d), transpose(roots)) + maximum = 0 + for i, left in enumerate(roots): + for j, right in enumerate(roots): + candidate_numerator = candidate[i][j] + error_numerator = 8 * dot(left, right) - candidate_numerator + need(error_numerator == products[i] * products[j], "literal entry identity") + maximum = max(maximum, abs(error_numerator)) + entries += 1 + need(maximum == 16, "attained maximum error is 16/64") + block = [[8 * dot(roots[i], roots[j]) - products[i] * products[j] + for j in indices] for i in indices] + need(rank(block) == 7, "attaining 104-by-104 matrix has rank seven") + return entries + + +def kernel_error_witness(candidate, a, roots, u, indices): + need(all(sum(row[j] * a[k] for k, j in enumerate(indices)) == 0 for row in candidate), + "selected-column null vector") + z = [dot(column, a) for column in transpose(u)] + need(any(z), "basis injectivity") + need([dot(row, z) / F(2) for row in u] == a, "coefficient reconstruction") + h = sum(sorted(map(abs, z), reverse=True)[:2]) + norm = sum(map(abs, a)) + need(norm <= 2 * h, "coefficient norm bound") + error = max(abs(F(dot(left, right), 8) - candidate[i][j]) + for i, left in enumerate(roots) for j, right in enumerate(roots)) + residual = max(abs(dot(row, z) / F(4)) for row in roots) + need(h / 2 <= residual <= error * norm and error >= F(1, 4), "unrestricted error witness") + return {"max_entry_error": str(error), "kernel_l1": str(norm), + "top_two_sum": str(h), "gram_residual_linf": str(residual)} + + +def carrier_fixtures(roots, omitted, u, indices): + q = omitted[0] + oblique = [[F(i == j) - F(q[i] * (j == 0), q[0]) for j in range(8)] for i in range(8)] + expansive = [[F(2 * (i == j)) - F(q[i] * q[j], 4) for j in range(8)] for i in range(8)] + indefinite = [[F((i == j) * (-1 if i == 0 else i < 7)) for j in range(8)] for i in range(8)] + need(oblique != transpose(oblique), "oblique fixture is nonsymmetric") + need(indefinite[0][0] < 0 < indefinite[1][1], "indefinite fixture signs") + output = {} + for name, d in (("nonsymmetric_oblique", oblique), ("noncontractive", expansive), + ("symmetric_indefinite", indefinite)): + need(rank(d) == 7, "carrier fixture rank seven") + raw = multiply(multiply(roots, d), transpose(roots)) + candidate = [[x / F(8) for x in row] for row in raw] + a = kernel_vector(multiply(d, transpose(u))) + output[name] = kernel_error_witness(candidate, a, roots, u, indices) + return output + + +def unrestricted_fixture(roots, u, indices): + a_factor = [list(row[:7]) for row in roots] + b_factor = [list(row[:7]) for row in roots] + a_factor[0][0] += 3 + b_factor[1][1] -= 5 + need(rank(a_factor) == rank(b_factor) == 7, "unrestricted factor ranks") + augmented_a = [list(row) + [a_factor[i][0]] for i, row in enumerate(roots)] + augmented_b = [list(row) + [b_factor[i][1]] for i, row in enumerate(roots)] + need(rank(roots) == 8 and rank(augmented_a) == rank(augmented_b) == 9, + "both factors leave carrier column space") + raw = multiply(a_factor, transpose(b_factor)) + candidate = [[F(x, 8) for x in row] for row in raw] + a = kernel_vector(transpose([b_factor[j] for j in indices])) + result = kernel_error_witness(candidate, a, roots, u, indices) + need(candidate != transpose(candidate), "unrestricted candidate is nonsymmetric") + result.update({"left_factor_rank": 7, "right_factor_rank": 7, + "left_augmented_rank": 9, "right_augmented_rank": 9}) + return result + + +def controls(data, roots, u): + results = [] + k = [[F(dot(left, right), 8) for right in roots] for left in roots] + need(rank(multiply(u, transpose(u))) == 8 and all(k[i][i] == 1 for i in range(104)), + "full-rank exact Gram control") + results.append("rank_eight_exact_gram_has_zero_error") + only_basis = [[F(i == j) - F(1, 8) for j in range(8)] for i in range(8)] + need(rank(only_basis) == 7 and max(abs(F(i == j) - only_basis[i][j]) + for i in range(8) for j in range(8)) == F(1, 8), "incomplete-root control") + results.append("orthogonal_eight_only_allows_one_eighth") + q = roots[0] + need(max(abs(dot(left, q) * dot(right, q)) for left in roots for right in roots) == 64, + "retained-root projection has error one") + results.append("retained_root_projection_error_one") + need(F(dot(roots[0], roots[0]), 4) != 1, "wrong Gram normalization detected") + results.append("wrong_coefficient_normalization_detected") + mutants = [dict(data, signs=["++++++++", *data["signs"][1:]]), + dict(data, signs=[data["signs"][0], *data["signs"][:-1]]), + dict(data, signs=["bad", *data["signs"][1:]])] + for index, mutant in enumerate(mutants): + try: + build_roots(mutant) + except ValueError: + results.append("malformed_missing_data_" + str(index)) + else: + raise ValueError("malformed missing data accepted") + return results + + +def source_inputs(package): + repository = package.parents[1] + manifest = json.loads((package / "SOURCES.json").read_text()) + verified = {} + for entry in manifest["files"]: + if entry.get("usage") == "input": + path = Path(entry["path"]) + need(not path.is_absolute() and ".." not in path.parts, "relative source input") + digest = hashlib.sha256((repository / path).read_bytes()).hexdigest() + need(digest == entry["sha256"], "source digest: " + str(path)) + verified[str(path)] = digest + missing_path = "research/p104-contractive-gram-deflation/MISSING.json" + need(missing_path in verified, "omitted-root input is declared") + return verified, json.loads((repository / missing_path).read_text()) + + +def main(): + package = Path(__file__).resolve().parent + sources, data = source_inputs(package) + d8, roots, omitted = build_roots(data) + u, indices = paired_columns(roots) + integer_count, rational_count = direction_fixtures(u, d8) + entries = attaining_projectors(roots, omitted, indices) + result = {"schema_version": 1, "sharp_unrestricted_rank_seven_error": "1/4", + "d8_root_lines": len(d8), "retained_root_lines": len(roots), + "paired_root_columns": indices, "attaining_projectors": len(omitted), + "literal_attaining_error_entries": entries, + "ternary_nonzero_directions": integer_count, "rational_directions": rational_count, + "carrier_fixtures": carrier_fixtures(roots, omitted, u, indices), + "outside_carrier_fixture": unrestricted_fixture(roots, u, indices), + "controls": controls(data, roots, u), "source_sha256": sources} + print(json.dumps(result, sort_keys=True)) + print("PASS_P104_RANK_SEVEN_ERROR_FLOOR") + + +if __name__ == "__main__": + main()