diff --git a/research/p104-complex-rank-seven/PROOF.md b/research/p104-complex-rank-seven/PROOF.md new file mode 100644 index 0000000000..78c8c0019b --- /dev/null +++ b/research/p104-complex-rank-seven/PROOF.md @@ -0,0 +1,171 @@ +# Complex rank seven beats the real quarter-error floor + +Prepared by apoursh with substantial OpenAI Codex assistance. Apache-2.0. +Nick Petalas's PR6183 retains the contractive Gram question and the real +omitted-root projector; Matarener's PR6166 retains the cited coordinate +identification and omitted lines. The real comparison theorem is credited +to apoursh's [PR6191](https://github.com/CrocSwap/integer-mult-bounds/blob/be3fc854aa380b3d81e134ce9a4282468e4fa999/research/p104-rank-seven-error-floor/PROOF.md). + +## 1. Fixed matrix and statement + +Use the 104 root lines retained by +`research/p104-contractive-gram-deflation/MISSING.json`: all 56 D8 lines +`e_i +/- e_j` and 48 odd-parity half-spin lines in eight coordinates. +Each row of R is a root of squared norm two, with its first nonzero +coordinate positive. Write S=2R and K=RR^T/2=SS^T/8. The sixteen omitted +half-spin lines are part of the pinned instance, not a search parameter. + +There is a Hermitian orthogonal projector D over Q(i), of complex rank +seven, such that C=RDR^T/2 has complex rank seven, satisfies +`0 <= C <= K` in Hermitian positive-semidefinite order, and + +```text +max_(j,k) |K_jk-C_jk| = 25/101 < 1/4. +``` + +The absolute value is the complex modulus. In contrast, every real +104-by-104 matrix of real rank at most seven has error at least 1/4 +against this K (section 4). Thus extending the coefficient field changes +the approximation problem even with a positive contractive carrier filter. +The assertion `0<=D<=I` is about the eight-dimensional filter, not about +C being a contraction on the 104-dimensional ambient space. + +## 2. Exact witness + +Take + +```text +z = (5-5i, 3+9i, 5-5i, 7, 5-5i, -1-4i, -7, -7), +N = z* z = 404, +D = I8 - z z*/N. +``` + +Here * denotes conjugate transpose. Since z is nonzero, `zz*/N` is a +rank-one Hermitian orthogonal projector. Consequently D is Hermitian, +`D^2=D`, `0<=D<=I`, and `rank_C D=7`. R has full column rank: the +eight retained roots `e_(2j)+e_(2j+1)` and `e_(2j)-e_(2j+1)` for +j=0,1,2,3 form an orthogonal basis. Thus + +```text +C = (RD)(RD)*/2, rank_C C = rank_C(RD) = 7, +K-C = (Rz)(Rz)*/(2N) = (Sz)(Sz)*/(8N). +``` + +Both C and K-C are positive semidefinite, proving `0<=C<=K`. +If `m=max_j |(Sz)_j|^2`, the last rank-one formula gives + +```text +max_(j,k) |K_jk-C_jk| = m/(8N). +``` + +Indeed each product `|(Sz)_j| |(Sz)_k|` is at most m, and a diagonal +entry with maximal squared modulus attains m. Complete exact enumeration +of the fixed 104 rows gives m=800, in both the D8 and retained half-spin +parts. Therefore the error is `800/(8*404)=25/101`, whose gap below +1/4 is exactly `1/404`. + +For a reproducible row ordering, enumerate pairs i=...>=t8 are the ordered moduli of x, then +`||a||_1 <= t1+t2+t3+t4 <= 2(t1+t2)`. The retained D8 rows give +`||Rx||_infinity=t1+t2` when restricted to that subsystem. For +`delta=max|K-F|`, therefore + +```text +delta ||a||_1 >= ||(K-F)[:,J]a||_infinity + = ||Rx||_infinity/2 >= (t1+t2)/2, +delta >= 1/4. +``` + +An omitted real half-spin root gives equality by PR6183's projection, +so the real floor is exactly 1/4. The displayed two-coordinate identity +is specific to real numbers: s=1,t=i already makes its left side sqrt(2) +and right side 1. It cannot be applied to the complex kernel vector. + +There is also no contradiction obtained by taking real parts. Write +z=u+iv for the small witness. Then + +```text +u^T u = 232, v^T v = 172, u^T v = -44, +det [[232,-44],[-44,172]] = 37968 > 0, +Re(D) = I8 - (uu^T+vv^T)/404. +``` + +The real matrix `uu^T+vv^T` has two strictly positive eigenvalues whose +sum is 404, so each is strictly less than 404. Thus Re(D) is positive +definite and `rank_R Re(C)=8`. The complex rank-seven construction does +not yield a seven-real-mode implementation; its usual realification has +rank fourteen. + +## 5. Scope and proof obligations + +The mathematical object is the fixed root Gram matrix with its specified +sixteen omitted lines. The physical identification with selected P104 +ports remains a cited premise from Matarener's PR6166; its source code, +native operators and coordinate identification are not independently +replayed here. Nick Petalas's PR6183 retains the Gram convention and +contractive question, with Rohan Arun/Chafik Boukhalfa and the retained +root/frame/native/helper/compiler/BIT lineage credited in the README. + +The complete finite root census proves the two stated errors for this +instance; the projection and rank arguments are written mathematics. +No universal complex optimum, asymptotically vanishing residual, native +Gaussian-dyadic implementation, source/consumer installation, residual +correction, dirty restoration, paid/target saving, new kappa or complete +multiplication theorem follows. The selected result and its five framework +assumptions retain their status. diff --git a/research/p104-complex-rank-seven/README.md b/research/p104-complex-rank-seven/README.md new file mode 100644 index 0000000000..fa6ac74b97 --- /dev/null +++ b/research/p104-complex-rank-seven/README.md @@ -0,0 +1,144 @@ +# Complex rank-seven P104 approximation below 1/4 + +**Exact finite construction and field separation; no new kappa.** + +Complex coefficients can beat the sharp real rank-seven error floor for the +fixed P104 Gram matrix. This answers the released complex-field question in +[PR6191](https://github.com/CrocSwap/integer-mult-bounds/pull/6191), at +`be3fc854aa380b3d81e134ce9a4282468e4fa999`. It does not contradict that +PR's theorem, whose coefficient field is real. + +Let R contain the 104 retained roots, each of squared norm two, and let +`K=RR^T/2`. The explicit vector + +```text +z = (5-5i, 3+9i, 5-5i, 7, 5-5i, -1-4i, -7, -7) +``` + +has `z* z=404`. The filter `D=I-zz*/404` is a Hermitian orthogonal +projector of complex rank seven, hence `0<=D<=I`. Its approximation +`C=RDR^T/2` has complex rank seven and exact maximum complex entry error +**25/101 < 1/4**, a gap of **1/404**. A second retained witness gives the +stronger bound **1205/4912 < 1/4**, with gap **23/4912**. Neither value is +claimed optimal. [PROOF.md](PROOF.md) contains both vectors and the proof. + +The distinction matters: C is Hermitian positive semidefinite with +`0<=C<=K`; the contraction claim applies to D, not to C relative to the +104-dimensional identity. Both candidates have trace 91. Their real parts +have real rank eight, so these are not seven-real-mode implementations. +Their coefficients contain odd denominators and are not Gaussian-dyadic. + +## Evidence and reproduction + +`verify.py` authenticates the three pinned predecessor inputs, reconstructs +all 104 roots, checks an orthogonal eight-root basis, and certifies both +projectors and every entry of both full Gram approximations: **21,632 +entries**. It checks real-part rank eight both by exact elimination and +by the real/imaginary Gram determinant. Nine controls cover all sixteen +real omitted-root quarter-error witnesses, a retained-root unit error, +dropping imaginary coordinates, missing conjugation, projector and Gram +normalizations, wrong parity, duplicate lines and a missing line. + +`independent.py` was written separately, without reading or importing the +primary checker. It reconstructs the roots in a different order, uses +Gaussian pairs of `Fraction` values instead of a common integer denominator, +checks every residual entry, and independently certifies complex rank seven +and real-part rank eight through the orthogonal-root minor. Four additional +projector controls reject wrong normalization and missing conjugation. + +Run from the repository root with Python 3.12 and its standard library: + +```sh +python3.12 -B scripts/research_package.py --package research/p104-complex-rank-seven --check-only +python3.12 -B scripts/research_package.py --package research/p104-complex-rank-seven +``` + +The registered commands run each checker normally and with `-O`, with +isolated imports and warnings treated as errors. Expected markers are +`PASS_P104_COMPLEX_RANK_SEVEN` and `PASS_INDEPENDENT_COMPLEX_RANK_SEVEN`. +For the official Git-free source export, run these direct commands from its +root, once normally and once with `-O` added: + +```sh +python3.12 -I -B -W error research/p104-complex-rank-seven/verify.py +python3.12 -I -B -W error research/p104-complex-rank-seven/independent.py +``` + +The export must include the three external inputs declared in +[VERIFY.json](VERIFY.json). [SOURCES.json](SOURCES.json) pins their base +commit, Git blobs and SHA256 digests. The original card and selected record +are historical provenance; the three PR6183 files are live inputs. The +primary verifier checks all three live hashes before arithmetic. The +independent checker separately pins the root-data hash. Both write no files +and preserve every mathematical check under optimized Python. + +## Sources, scope and coordination + +Canonical main was refreshed first at +`a5bff3bf133e482541c09eba4e773884bdb2b1b7`, priority revision 8. The selected +record identifies conditional `kappa=781451/250000000` and five remaining +framework assumptions; neither changes here. Binding-only orientation was +reused after confirming all 1227 bound inputs unchanged since checkpoint +`3f0152a32eeebac0df11946dbd50cabe5a7f7839`. No selected scientific cold replay +was run. + +The original `coverage-law-change` card is retained in [TASK.json](TASK.json), +with scope explicitly changed to this algebraic field-extension question. +This identifies a limitation of a real approximation obstruction, but does +not meet the original completed-call and full-invoice acceptance gate. +The [canonical claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19275237) +records the two previously unpublished local candidates and stops after +their exact certification. No additional numerical search was run. + +The local overlap helper searched 30 of 8623 notes (8593 absent in the +sparse checkout), without a usable remote cache. Live checks covered the +newest 20 PRs, newest 15 handoff comments, and all-state searches for +P104/complex/rank, 6191 and Gram/contractive. Nearest results are PR6191's +real theorem and Nick Petalas's [PR6183](https://github.com/CrocSwap/integer-mult-bounds/pull/6183) +contractive theorem. PR6194 concerns a different paid frame-graph objective. +No competing complex witness appeared in the checked results; this is not +an exhaustive novelty audit. + +PR6183 at `eaf77790466f34b86ce72080e3ec690e26dfacab` supplies the retained +root data, contractive question and Gram convention. Matarener's PR6166 +at `096938513138868f0ed27639061f1a5054900f96` supplies the cited P104-to-D8 +identification and omitted lines. Those physical coordinates are a cited +premise, not independently audited here. Their archival retention does not +constitute scientific acceptance. PR6191 remains a pending comparison +source; its real lower-bound argument is restated with credit in PROOF.md, +and no replay requires its pending Git objects or executable code. + +The proof establishes two finite counterexamples to extending the real +quarter-error floor over Q(i). It does not give the optimum complex error, +an asymptotically vanishing residual, native implementation, side correction, +source/consumer installation, ownership/dirty restoration, full paid/target +invoice or multiplication theorem. Independent human and formal proof-kernel +review are unclaimed. No Lean, Docker or physical/native replay was run. + +## Open next questions + +- **Can a Gaussian-dyadic rank-seven filter also beat 1/4?** The odd + denominators leave a coefficient-field gap before native implementation. + A bounded first step is one exact dyadic Hermitian projector on these same + 104 roots, checking its complete coefficient error. No such projector or + native circuit is supplied here; any wider search needs a justified scope. +- **Can an actual caller use and correct this residual profitably?** A lower + coefficient error alone earns no independent target credit. Start with + one source-bound scalar word, track this exact rank-one residual through + every retained output, and price restoration and correction. The absent + caller and complete bill are blockers; no additional parameter search is + justified as a bound improvement before that gate. + +Structured questions, relevance, first steps and blockers are in TASK.json. + +## Credit + +Prepared by **apoursh**, with substantial OpenAI Codex assistance in witness +discovery, separately written exact verification, mathematical audit, proof +and packaging. Nick Petalas retains PR6183's contractive question and real +attaining projection; Matarener retains PR6166's D8 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 lineage retain their source credit. +Hermitian projection and Gram-rank facts are classical; no general literature +priority is claimed. New material is Apache-2.0; predecessor files are unchanged. diff --git a/research/p104-complex-rank-seven/SOURCES.json b/research/p104-complex-rank-seven/SOURCES.json new file mode 100644 index 0000000000..7c6e80cb7d --- /dev/null +++ b/research/p104-complex-rank-seven/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-complex-rank-seven/TASK.json b/research/p104-complex-rank-seven/TASK.json new file mode 100644 index 0000000000..a2de9c2def --- /dev/null +++ b/research/p104-complex-rank-seven/TASK.json @@ -0,0 +1,82 @@ +{ + "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": "Certify two complex rank-seven Hermitian contractive carrier filters for the fixed P104 Gram matrix with maximum entry error below the real floor 1/4.", + "scope_change_reason": "Take the released complex-field question in PR6191 at be3fc854aa380b3d81e134ce9a4282468e4fa999. This changes the card from completed productive credit to an algebraic coefficient-field separation; the original complete supplier acceptance gate remains unmet.", + "bottleneck_link": "Side result for approximate carrier deletion: the real error obstruction does not extend to Gaussian-rational filters. Physical delivery, odd denominators, residual correction and a complete paid/target invoice remain unpriced.", + "budget_minutes": 60, + "stop_rule": "Certify the two already discovered exact witnesses and the real/complex distinction, then stop. No further optimization, new caller search or supplier expansion in this round.", + "outcome": "completed", + "evidence": "PROOF.md; two separately written exact checkers verifying both complete 104x104 residuals, projector/rank identities, real-part rank eight and hypothesis controls. No optimality or selected cold replay claimed.", + "author": "apoursh", + "ai_assistance": "Substantial OpenAI Codex assistance for earlier witness discovery, separate primary and independent exact checkers, mathematical audit, proof, source binding and packaging. Prepared by apoursh.", + "open_questions": [ + { + "question": "Can a Gaussian-dyadic Hermitian rank-seven carrier filter also beat 1/4?", + "why_it_matters": "The current odd denominators leave a coefficient-field gap before native implementation.", + "first_step": "Check one exact dyadic rank-seven projector against all 104 fixed roots, with complete entrywise error and coefficient authentication.", + "blocked_by": "No such dyadic projector or native circuit is supplied; a wider search needs a separate justified scope." + }, + { + "question": "Can an actual source/consumer use and correct this exact rank-one residual profitably?", + "why_it_matters": "Reduced coefficient error alone does not earn independent productive target credit or a paid-work saving.", + "first_step": "Choose one source-bound scalar word, propagate the residual through all retained outputs, and price correction, restoration and every other paid/target charge.", + "blocked_by": "No matched caller, native implementation or complete invoice is supplied; do not expand a parameter search as a bound claim before that gate." + } + ], + "scope_key": "2bf6355a8dd01ca324fb", + "chooser_seed": "21a3942db45090da1dd169e51a914a29", + "coordination_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19275237" +} diff --git a/research/p104-complex-rank-seven/VERIFY.json b/research/p104-complex-rank-seven/VERIFY.json new file mode 100644 index 0000000000..2680058f76 --- /dev/null +++ b/research/p104-complex-rank-seven/VERIFY.json @@ -0,0 +1,63 @@ +{ + "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", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Two exact complex rank-seven witnesses; all 21632 residual entries; source hashes, real-part rank eight and nine hypothesis controls." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-W", + "error", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Two exact complex rank-seven witnesses; all 21632 residual entries; source hashes, real-part rank eight and nine hypothesis controls. Optimized Python control." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-W", + "error", + "{package}/independent.py" + ], + "timeout_seconds": 120, + "checks": "Separately written Gaussian Fraction checker, different root order, both full residual matrices and rank minors, four projector controls." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-W", + "error", + "-O", + "{package}/independent.py" + ], + "timeout_seconds": 120, + "checks": "Separately written Gaussian Fraction checker, different root order, both full residual matrices and rank minors, four projector controls. Optimized Python control." + } + ] +} diff --git a/research/p104-complex-rank-seven/independent.py b/research/p104-complex-rank-seven/independent.py new file mode 100644 index 0000000000..2dc7d7654a --- /dev/null +++ b/research/p104-complex-rank-seven/independent.py @@ -0,0 +1,213 @@ +#!/usr/bin/env python3 +"""Separate exact rational audit of two complex P104 rank-seven witnesses. + +Prepared by apoursh with substantial OpenAI Codex assistance. Apache-2.0. +Nick Petalas (PR6183) retains the deflation construction and Matarener +(PR6166) the cited D8 coordinate identification and omitted-root data. +No primary or predecessor executable code is imported. +""" + +import hashlib +import itertools +import json +from fractions import Fraction as F +from pathlib import Path + +ZERO = (F(0), F(0)) +SOURCE_SHA256 = '9ddfcf087912e02c46722d5a82eea5f1221a4a33d5037a0d90d392dfcd3c06d4' + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def plus(x, y): + return x[0] + y[0], x[1] + y[1] + + +def minus(x, y): + return x[0] - y[0], x[1] - y[1] + + +def times(x, y): + return x[0] * y[0] - x[1] * y[1], x[0] * y[1] + x[1] * y[0] + + +def scale(x, scalar): + return x[0] * scalar, x[1] * scalar + + +def conjugate(x): + return x[0], -x[1] + + +def squared(x): + return x[0] ** 2 + x[1] ** 2 + + +def divide(x, y): + require(y != ZERO, 'nonzero Gaussian pivot') + return scale(times(x, conjugate(y)), 1 / squared(y)) + + +def gaussian_dot(row, column): + answer = ZERO + for x, y in zip(row, column, strict=True): + answer = plus(answer, times(x, y)) + return answer + + +def matrix_product(a, b): + columns = list(zip(*b, strict=True)) + return [[gaussian_dot(row, col) for col in columns] for row in a] + + +def matrix_rank(matrix): + rows = [row[:] for row in matrix] + rank = 0 + for col in range(len(rows[0])): + pivot = next((i for i in range(rank, len(rows)) if rows[i][col] != ZERO), None) + if pivot is None: + continue + rows[pivot], rows[rank] = rows[rank], rows[pivot] + divisor = rows[rank][col] + rows[rank] = [divide(x, divisor) for x in rows[rank]] + for i in range(rank + 1, len(rows)): + if rows[i][col] != ZERO: + multiplier = rows[i][col] + rows[i] = [minus(x, times(multiplier, y)) + for x, y in zip(rows[i], rows[rank], strict=True)] + rank += 1 + if rank == min(len(rows), len(rows[0])): + break + return rank + + +def root_rows(): + source = Path(__file__).resolve().parents[1] / 'p104-contractive-gram-deflation/MISSING.json' + raw = source.read_bytes() + require(hashlib.sha256(raw).hexdigest() == SOURCE_SHA256, 'pinned root-data bytes') + omitted = set() + for signs in json.loads(raw)['signs']: + require(len(signs) == 8 and set(signs) <= {'+', '-'}, 'root signs') + row = tuple(1 if c == '+' else -1 for c in signs) + omitted.add(row if row[0] == 1 else tuple(-x for x in row)) + shell = {(1, *tail) for tail in itertools.product((1, -1), repeat=7) + if tail.count(-1) % 2 == 1} + require(len(omitted) == 16 and omitted <= shell, 'sixteen distinct odd omitted lines') + # Half-spin rows first; this ordering is deliberately independent of port labels. + rows = sorted(shell - omitted) + for i, j in itertools.combinations(range(8), 2): + for sign in (1, -1): + row = [0] * 8 + row[i], row[j] = 2, 2 * sign + rows.append(tuple(row)) + require(len(rows) == len(set(rows)) == 104, '104 distinct retained lines') + require(all(sum(x * x for x in row) == 8 for row in rows), 'doubled root norms') + return rows + + +def frame_indices(rows): + indices = [] + for i in range(0, 8, 2): + for sign in (1, -1): + row = [0] * 8 + row[i], row[i + 1] = 2, 2 * sign + indices.append(rows.index(tuple(row))) + gram = [[sum(x * y for x, y in zip(rows[i], rows[j], strict=True)) + for j in indices] for i in indices] + require(gram == [[8 * (i == j) for j in range(8)] for i in range(8)], + 'invertible orthogonal root submatrix') + return indices + + +def projector(z, norm): + return [[minus((F(i == j), F(0)), scale(times(x, conjugate(y)), F(1, norm))) + for j, y in enumerate(z)] for i, x in enumerate(z)] + + +def literal_gram_candidate(rows, d): + # Multiply S D first, then by S^T/8. No outer-residual formula is used here. + left = [] + for row in rows: + new = [] + for j in range(8): + value = ZERO + for i in range(8): + value = plus(value, scale(d[i][j], row[i])) + new.append(value) + left.append(new) + candidate = [] + for row in left: + new = [] + for source in rows: + value = ZERO + for x, coefficient in zip(row, source, strict=True): + value = plus(value, scale(x, coefficient)) + new.append(scale(value, F(1, 8))) + candidate.append(new) + return candidate + + +def check_witness(rows, indices, integer_pairs, expected_norm, expected_max, expected_error): + z = [(F(a), F(b)) for a, b in integer_pairs] + norm = sum(squared(x) for x in z) + require(norm == expected_norm, 'exact vector norm') + d = projector(z, norm) + require(all(d[i][j] == conjugate(d[j][i]) for i in range(8) for j in range(8)), 'Hermitian D') + require(matrix_product(d, d) == d, 'projector idempotence') + require(all(gaussian_dot(row, z) == ZERO for row in d), 'projector kernel') + require(matrix_rank(d) == 7, 'complex projector rank seven') + real_d = [[(x[0], F(0)) for x in row] for row in d] + require(matrix_rank(real_d) == 8, 'real part has rank eight') + values = [gaussian_dot([(F(x), F(0)) for x in row], z) for row in rows] + maximum = max(squared(x) for x in values) + require(maximum == expected_max, 'exact doubled-root maximum') + candidate = literal_gram_candidate(rows, d) + minor = [[candidate[i][j] for j in indices] for i in indices] + require(matrix_rank(minor) == 7, 'rank-seven full candidate via nonsingular-root minor') + require(matrix_rank([[(x[0], F(0)) for x in row] for row in minor]) == 8, + 'real candidate has rank eight') + error_squared, entries = F(0), 0 + for i, left in enumerate(rows): + for j, right in enumerate(rows): + gram = (F(sum(x * y for x, y in zip(left, right, strict=True)), 8), F(0)) + error = minus(gram, candidate[i][j]) + outer = scale(times(values[i], conjugate(values[j])), F(1, 8 * norm)) + require(error == outer, 'literal full-matrix residual') + require(candidate[i][j] == conjugate(candidate[j][i]), 'Hermitian C') + error_squared = max(error_squared, squared(error)) + entries += 1 + require(error_squared == expected_error ** 2, 'attained exact coefficient error') + require(maximum / (8 * norm) == expected_error < F(1, 4), 'strict real-bound separation') + bad = projector(z, norm + 1) + require(matrix_product(bad, bad) != bad, 'wrong-norm projector control') + wrong_conjugation = [[minus((F(i == j), F(0)), scale(times(x, y), F(1, norm))) + for j, y in enumerate(z)] for i, x in enumerate(z)] + require(any(wrong_conjugation[i][j] != conjugate(wrong_conjugation[j][i]) + for i in range(8) for j in range(8)), 'missing-conjugation Hermitian control') + require(matrix_product(wrong_conjugation, wrong_conjugation) != wrong_conjugation, + 'missing-conjugation projector control') + return {'norm': str(norm), 'max_doubled_root_squared': str(maximum), + 'max_entry_error': str(expected_error), 'gap_below_quarter': str(F(1, 4) - expected_error), + 'literal_residual_entries': entries, 'complex_rank': 7, + 'real_part_rank': 8, 'projector_controls': 2} + + +def main(): + rows = root_rows() + indices = frame_indices(rows) + fixtures = [ + ([(5,-5),(3,9),(5,-5),(7,0),(5,-5),(-1,-4),(-7,0),(-7,0)], + 404, 800, F(25,101)), + ([(14,-10),(6,23),(14,-10),(17,3),(14,-10),(-3,-10),(-17,-3),(-17,-3)], + 2456, 4820, F(1205,4912)), + ] + results = [check_witness(rows, indices, *fixture) for fixture in fixtures] + print('PASS_INDEPENDENT_COMPLEX_RANK_SEVEN ' + json.dumps({ + 'root_lines': len(rows), 'source_sha256': SOURCE_SHA256, 'witnesses': results}, sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/p104-complex-rank-seven/verify.py b/research/p104-complex-rank-seven/verify.py new file mode 100644 index 0000000000..955919c08a --- /dev/null +++ b/research/p104-complex-rank-seven/verify.py @@ -0,0 +1,306 @@ +#!/usr/bin/env python3 +"""Exact complex rank-seven P104 witnesses; Python standard library only. + +Prepared by apoursh with substantial OpenAI Codex assistance. Apache-2.0. +Retains Nick Petalas's Gram convention, Matarener's cited coordinates and +the predecessor attribution recorded in README.md. No optimality claim. +""" + +import hashlib +import itertools +import json +from fractions import Fraction +from pathlib import Path + + +WITNESSES = { + "small": { + "z": [(5, -5), (3, 9), (5, -5), (7, 0), + (5, -5), (-1, -4), (-7, 0), (-7, 0)], + "norm_squared": 404, + "maximum_squared": 800, + "error": "25/101", + }, + "stronger": { + "z": [(14, -10), (6, 23), (14, -10), (17, 3), + (14, -10), (-3, -10), (-17, -3), (-17, -3)], + "norm_squared": 2456, + "maximum_squared": 4820, + "error": "1205/4912", + }, +} +SOURCE_DIRECTORY = "research/p104-contractive-gram-deflation" + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def add(x, y): + return x[0] + y[0], x[1] + y[1] + + +def mul(x, y): + return x[0] * y[0] - x[1] * y[1], x[0] * y[1] + x[1] * y[0] + + +def conjugate(x): + return x[0], -x[1] + + +def scale(a, x): + return a * x[0], a * x[1] + + +def total(values): + result = (0, 0) + for value in values: + result = add(result, value) + return result + + +def dot(x, y): + return sum(a * b for a, b in zip(x, y, strict=True)) + + +def matrix_product(left, right): + columns = list(zip(*right, strict=True)) + return [[total(mul(a, b) for a, b in zip(row, column, strict=True)) + for column in columns] for row in left] + + +def matrix_scale(a, matrix): + return [[scale(a, value) for value in row] for row in matrix] + + +def hermitian(matrix): + return all(matrix[i][j] == conjugate(matrix[j][i]) + for i in range(len(matrix)) for j in range(len(matrix))) + + +def rational_rank(matrix): + rows = [[Fraction(value) for value in row] for row in matrix] + rank = 0 + for column in range(len(rows[0])): + pivot = next((i for i in range(rank, len(rows)) if rows[i][column]), None) + if pivot is None: + continue + rows[rank], rows[pivot] = rows[pivot], rows[rank] + divisor = rows[rank][column] + rows[rank] = [value / divisor for value in rows[rank]] + for i in range(rank + 1, len(rows)): + coefficient = rows[i][column] + rows[i] = [x - coefficient * y + for x, y in zip(rows[i], rows[rank], strict=True)] + rank += 1 + return rank + + +def authenticate_sources(package): + repository = package.parents[1] + manifest = json.loads((package / "SOURCES.json").read_text()) + inputs = [item for item in manifest["files"] if item["usage"] == "input"] + required = {f"{SOURCE_DIRECTORY}/{name}" for name in + ("MISSING.json", "PROOF.md", "README.md")} + need(len(inputs) == 3 and {item["path"] for item in inputs} == required, + "exact three declared predecessor inputs") + payloads, hashes = {}, {} + for item in inputs: + path = (repository / item["path"]).resolve() + need(path.is_relative_to(repository), "input path stays inside checkout") + data = path.read_bytes() + digest = hashlib.sha256(data).hexdigest() + need(digest == item["sha256"], "input digest: " + item["path"]) + payloads[item["path"]] = data + hashes[item["path"]] = digest + return json.loads(payloads[f"{SOURCE_DIRECTORY}/MISSING.json"]), hashes + + +def roots_and_missing(data): + signs = data["signs"] + need(isinstance(signs, list) and len(signs) == 16, "sixteen omitted lines") + missing = set() + for text in signs: + need(isinstance(text, str) and len(text) == 8 + and set(text) <= {"+", "-"}, "eight valid half-spin signs") + need(text.count("-") % 2 == 1, "odd half-spin parity") + row = tuple(1 if sign == "+" else -1 for sign in text) + missing.add(row if row[0] > 0 else tuple(-x for x in row)) + need(len(missing) == 16, "sixteen distinct omitted lines") + roots = [] + for i, j in itertools.combinations(range(8), 2): + for sign in (-1, 1): + row = [0] * 8 + row[i], row[j] = 2, 2 * sign + roots.append(tuple(row)) + half = [(1, *tail) for tail in itertools.product((-1, 1), repeat=7) + if tail.count(-1) % 2 == 1] + need(len(roots) == 56 and len(half) == 64 and missing <= set(half), + "D8 and half-spin shell counts") + roots.extend(row for row in half if row not in missing) + need(len(roots) == len(set(roots)) == 104, "104 distinct retained lines") + need(all(dot(row, row) == 8 for row in roots), "doubled root norms") + return roots, sorted(missing) + + +def root_frame(roots): + frame = [] + for i in range(0, 8, 2): + for sign in (1, -1): + row = [0] * 8 + row[i], row[i + 1] = 2, 2 * sign + frame.append(roots.index(tuple(row))) + need(all(dot(roots[frame[i]], roots[frame[j]]) == 8 * int(i == j) + for i in range(8) for j in range(8)), "full column rank frame") + return frame + + +def projector_numerator(z, denominator, multiplier=1, use_conjugate=True): + return [[add((denominator * int(i == j), 0), + scale(-multiplier, mul(z[i], conjugate(z[j]) + if use_conjugate else z[j]))) + for j in range(8)] for i in range(8)] + + +def projector_certificate(z): + norm = sum(a * a + b * b for a, b in z) + need(norm > 0, "nonzero deleted direction") + matrix = projector_numerator(z, norm) + need(hermitian(matrix), "Hermitian carrier filter") + need(matrix_product(matrix, matrix) == matrix_scale(norm, matrix), + "idempotent carrier filter") + need(total(matrix[i][i] for i in range(8)) == (7 * norm, 0), + "idempotent has rank-seven trace") + need(all(total(mul(row[j], z[j]) for j in range(8)) == (0, 0) + for row in matrix), "deleted direction lies in kernel") + # Hermitian idempotence proves 0 <= D <= I. Rank is its trace. + real, imag = [a for a, _ in z], [b for _, b in z] + aa, bb, ab = dot(real, real), dot(imag, imag), dot(real, imag) + determinant = aa * bb - ab * ab + need(aa + bb == norm and determinant > 0, "independent real and imaginary parts") + real_matrix = [[value[0] for value in row] for row in matrix] + need(rational_rank(real_matrix) == 8, "real part restores real rank eight") + return norm, matrix, {"real_norm_squared": aa, "imag_norm_squared": bb, + "real_imag_dot": ab, "gram_determinant": determinant} + + +def literal_matrix_certificate(roots, z, norm, matrix): + products = [total(scale(a, b) for a, b in zip(row, z, strict=True)) + for row in roots] + norms = [a * a + b * b for a, b in products] + maximum = max(norms) + left = [[total(scale(row[k], matrix[k][j]) for k in range(8)) + for j in range(8)] for row in roots] + # With S the doubled roots, C has denominator 8*norm. + candidate = [[total(scale(column[k], row[k]) for k in range(8)) + for column in roots] for row in left] + need(hermitian(candidate), "Hermitian complete Gram approximation") + largest_squared = 0 + for i, row in enumerate(roots): + for j, column in enumerate(roots): + gram = (norm * dot(row, column), 0) + error = add(gram, scale(-1, candidate[i][j])) + need(error == mul(products[i], conjugate(products[j])), + "literal full-matrix rank-one error identity") + size_squared = error[0] * error[0] + error[1] * error[1] + need(size_squared <= maximum * maximum, "full-matrix entry bound") + largest_squared = max(largest_squared, size_squared) + need(largest_squared == maximum * maximum, "attained entry bound") + trace = Fraction(sum(candidate[i][i][0] for i in range(len(roots))), 8 * norm) + need(trace > 7, "C is not an ambient rank-seven positive contraction") + return maximum, [i for i, value in enumerate(norms) if value == maximum], trace + + +def verify_witness(roots, fixture): + z = fixture["z"] + norm, matrix, real_imag = projector_certificate(z) + maximum, attaining, trace = literal_matrix_certificate(roots, z, norm, matrix) + error = Fraction(maximum, 8 * norm) + need(norm == fixture["norm_squared"], "declared direction norm") + need(maximum == fixture["maximum_squared"], "declared root maximum") + need(str(error) == fixture["error"] and error < Fraction(1, 4), + "declared strict complex-field separation") + return {"z": z, "norm_squared": norm, + "max_doubled_root_inner_product_squared": maximum, + "error": str(error), "gap_from_one_quarter": str(Fraction(1, 4) - error), + "attaining_root_indices": attaining, "carrier_complex_rank": 7, + "candidate_complex_rank": 7, "real_part_rank": 8, + "real_imag_certificate": real_imag, "candidate_trace": str(trace), + "literal_matrix_entries": len(roots) ** 2} + + +def real_direction_error(roots, direction): + norm = dot(direction, direction) + need(norm > 0, "nonzero real direction") + return Fraction(max(dot(row, direction) ** 2 for row in roots), 8 * norm) + + +def rejected_root_control(data, signs, diagnostic): + try: + roots_and_missing({**data, "signs": signs}) + except ValueError as error: + need(str(error) == diagnostic, "specific malformed-root diagnostic") + else: + raise ValueError("malformed root data accepted") + + +def controls(data, roots, missing): + omitted_errors = {real_direction_error(roots, row) for row in missing} + need(omitted_errors == {Fraction(1, 4)}, "all omitted roots attain real quarter") + retained_error = real_direction_error(roots, roots[56]) + need(retained_error == 1, "retained half-spin deletion has unit error") + z = WITNESSES["small"]["z"] + real_error = real_direction_error(roots, [a for a, _ in z]) + need(real_error >= Fraction(1, 4), "dropping imaginary coordinates loses escape") + norm = sum(a * a + b * b for a, b in z) + unconjugated = projector_numerator(z, norm, use_conjugate=False) + need(not hermitian(unconjugated), "bilinear deletion is not Hermitian") + need(matrix_product(unconjugated, unconjugated) != matrix_scale(norm, unconjugated), + "bilinear deletion is not idempotent") + reflection = projector_numerator(z, norm, multiplier=2) + squared = matrix_product(reflection, reflection) + identity = [[(norm * norm * int(i == j), 0) for j in range(8)] for i in range(8)] + need(squared == identity, "misnormalized deletion is invertible of rank eight") + need(squared != matrix_scale(norm, reflection), "misnormalized deletion is not idempotent") + signs = data["signs"] + rejected_root_control(data, ["++++++++", *signs[1:]], "odd half-spin parity") + rejected_root_control(data, [signs[0], *signs[:-1]], "sixteen distinct omitted lines") + rejected_root_control(data, signs[:-1], "sixteen omitted lines") + error = Fraction(WITNESSES["small"]["error"]) + need(2 * error > Fraction(1, 4), "RR^T normalization cannot claim quarter escape") + return { + "omitted_half_spin_real_quarter": {"directions": len(missing), "error": "1/4"}, + "retained_half_spin_unit_error": str(retained_error), + "dropping_imaginary_part": str(real_error), + "missing_conjugation": "rejected: not Hermitian or idempotent", + "wrong_projector_normalization": "rejected: rank-eight reflection, not idempotent", + "wrong_half_spin_parity": "rejected", + "duplicate_omitted_line": "rejected", + "wrong_omitted_count": "rejected", + "wrong_gram_normalization": {"error_for_doubled_target_and_candidate": str(2 * error)}, + } + + +def main(): + package = Path(__file__).resolve().parent + data, hashes = authenticate_sources(package) + roots, missing = roots_and_missing(data) + frame = root_frame(roots) + witnesses = {name: verify_witness(roots, fixture) + for name, fixture in WITNESSES.items()} + control_results = controls(data, roots, missing) + result = {"schema_version": 1, "claim_type": "exact finite complex-field separation", + "metric": "maximum complex entry modulus", "root_order": "D8 pairs then odd half-spin", + "d8_lines": 56, "retained_half_spin_lines": 48, "retained_lines": len(roots), + "omitted_lines": len(missing), "root_frame_indices": frame, + "source_sha256": hashes, "witnesses": witnesses, + "literal_matrix_entries": sum(item["literal_matrix_entries"] + for item in witnesses.values()), + "control_count": len(control_results), "controls": control_results} + print(json.dumps(result, sort_keys=True)) + print("PASS_P104_COMPLEX_RANK_SEVEN") + + +if __name__ == "__main__": + main()