diff --git a/research/p104-dyadic-rank-seven/PROOF.md b/research/p104-dyadic-rank-seven/PROOF.md new file mode 100644 index 0000000000..49a95bec8e --- /dev/null +++ b/research/p104-dyadic-rank-seven/PROOF.md @@ -0,0 +1,158 @@ +# An exact Gaussian-dyadic Hermitian projection below the real P104 floor + +Jerry Chen (@CubeJerry), substantial OpenAI Codex assistance. Apache-2.0. + +## Statement and scope + +Let R contain one squared-norm-two representative from each of PR6211's +104 root lines: all 56 D8 lines and the 48 odd half-spin lines remaining +after the sixteen omissions in the pinned MISSING.json. Set S=2R and +K=RR^T/2=SS^T/8. There is a Hermitian orthogonal projector D over +Z[i,1/2] with complex rank seven such that + + C = R D R^T / 2, + rank_C C = 7, 0 <= C <= K, + max_(j,k) |K_jk-C_jk| = 16193/65536 < 1/4. + +The modulus is the complex modulus. The contraction 0<=D<=I concerns the +eight-dimensional carrier, not C relative to the 104-dimensional identity. +This answers PR6211's first open question, the exact Gaussian-dyadic +Hermitian projector. It is not an optimality or physical-supplier theorem. + +## Preserve the projection identity before approximating its coefficients + +Take the Gaussian-integer vector + + z = (73-53i, 31+118i, 73-51i, 88+16i, + 73-51i, -15-51i, -87-15i, -88-17i). + +Its squared norm is N=z* z=65536=2^16. Put P=zz*/N and D=I8-P. +Since P*=P and P^2=z(z*z)z*/N^2=P, P is a rank-one Hermitian orthogonal +projector. Thus D*=D, D^2=D, rank_C D=7 and 0<=D<=I. All its entries +are Gaussian-dyadic with common denominator 2^16. This exact identity +would not follow from entrywise dyadic rounding of an old matrix. + +The eight retained roots e_0 +/- e_1, e_2 +/- e_3, e_4 +/- e_5 and +e_6 +/- e_7 form an orthogonal basis, so R has column rank eight. +Multiplication on the left by R and on the right by R^T preserves the +rank of D: these maps have left and right inverses respectively. Also +C=(RD)(RD)*/2 and K-C=(Rz)(Rz)*/(2N). Hence C has rank seven and +0<=C<=K. Since R is dyadic, every C coefficient is Gaussian-dyadic. +The sufficient common denominator is 8N; the largest reduced component +denominator is actually 2^17, as the complete certificate checks. + +## Complete entry-error certificate + +Write w=Sz. Then K-C=ww*/(8N). For any complex vector w, +max_(j,k)|w_j conjugate(w_k)|=max_j|w_j|^2: a diagonal entry attains +the product bound. Exact enumeration of every retained row gives: + +| Root family | Rows | Maximum squared response | +| --- | ---: | ---: | +| D8 | 56 | 129544 | +| Odd half-spin | 48 | 128596 | +| Complete instance | 104 | 129544 | + +Use PR6211's order: D8 pairs lexicographic, signs minus then plus, +followed by lexicographic half-spin tails. The unique maximum is row 24, +S_24=2(e_1-e_7), where (Sz)_24=238+270i. Therefore + + max |K-C| = (238^2+270^2)/(8*65536) = 16193/65536, + 1/4 - max |K-C| = 191/65536 > 0. + +The primary verifier reconstructs the root set and checks all 10,816 +entries of the literal product SDS^T/8 against the residual formula. +It does not trust the search maximum. Rational Gaussian elimination +separately checks the rank of D and an eight-root principal minor of C. + +The second arithmetic path imports no primary or predecessor executable. +It uses separately ordered roots and Fraction arithmetic on the 16-by-16 +realification, checking symmetry, idempotence and rank fourteen. It +independently evaluates every residual entry using real and imaginary +outer products. Both paths are by the same contributor with AI assistance; +this is not independent human or formal-kernel review. + +## Real and operator-norm boundaries + +Writing z=u+iv gives + + u^T u=40230, u^T v=-2683, v^T v=25306, + det Gram(u,v)=1010861891 > 0. + +The two nonzero eigenvalues of uu^T+vv^T are positive and sum to N, +so each is less than N. Thus Re(D)=I-(uu^T+vv^T)/N is positive +definite and Re(C) has real rank eight. This does not yield a +seven-real-mode approximation or contradict PR6191's real theorem. + +For this root set S^T S=104 I, checked exactly. Thus ||w||_2^2=104N +and ||K-C||_2=104N/(8N)=13. The largest eigenvalue of K is also 13. +Smaller maximum coefficient error therefore does not supply vanishing +operator error: worst-case relative spectral error is one. This is a +scope calculation, not a new optimality result. + +Exact reconstruction of K through a linear seven-dimensional intermediate +is impossible, since rank K=8. Retaining the lost scalar response gives +the elementary seven-plus-one reconstruction, with eight independent +pieces of information before acquisition, transport or restoration costs. +No free residual correction or completed recursive invoice is assumed. + +## Bounded discovery + +The guide is PR6211's stronger Gaussian-rational witness, written as +sixteen interleaved real coordinates: + + a=(14,-10,6,23,14,-10,17,3,14,-10,-3,-10,-17,-3,-17,-3), + sum a_i^2=2456. + +For k=4,...,9 in increasing order, let +q_i=floor(2^k a_i/sqrt(2456)), restrict y_i to {q_i-1,q_i,q_i+1}, +and require sum y_i^2=4^k. Floors are calculated with integer square +roots and sign-aware exact comparisons. On that sphere, minimizing +squared distance from 2^k a/sqrt(2456) is equivalent to maximizing a dot y. + +The DP keeps the largest dot product at each partial squared norm. +The remaining coordinate choices depend only on the norm and position, +so a lower-scoring prefix cannot produce a better completion. Remaining +minimum/maximum squared norms discard only infeasible completions. +The nonce 0b7fc9054fc70396e2d971f95342f0a4 rotates the coordinate order +by four; tied scores take the lexicographically largest tuple in that +order. One selected nearest vector at each scale is tested for its error. + +| k | Error of the selected nearest vector | Strictly below 1/4? | +| ---: | --- | --- | +| 4 | 37/128 | no | +| 5 | 17/64 | no | +| 6 | 4121/16384 | no | +| 7 | 257/1024 | no | +| 8 | 16193/65536 | yes; stop | + +The search stops at k=8, leaving k=9 unsearched. Each completed box has +3^16 possible tuples before the norm constraint; the DP compresses them +by exact sufficient state. WITNESS.json retains all five selected vectors, +scores, state counts and transitions. search.py reproduces this record. +The certificate's validity does not depend on DP completeness. + +These are not error optima or smaller-denominator exclusions. Another +vector in the same box might have lower error. No larger search was run. +The initial exploratory root parser failed to canonicalize seven omitted +representatives and produced 111 rows; those outputs are invalid, not +search evidence. The corrected 104-row loader also reproduces PR6211's +exact guide maximum 4820 before any accepted search or verification. + +## New result and inherited obligations + +Armin Pourshafeie / apoursh's PR6211 already supplies complex Hermitian +rank-seven examples below 1/4. The present error lies between its +25/101 and 1205/4912 witnesses; the contribution is Gaussian-dyadic +coefficient feasibility, not a new best complex error. Nick Petalas's +PR6183 supplies the contractive question, real attaining projector and +omission data; apoursh's PR6191 supplies the sharp real comparison. +Matarener's PR6166 supplies the cited physical P104/root identification, +which is not independently audited here. Exact input pins and full +predecessor heads are recorded in SOURCES.json and README.md. + +Dyadic entries are not a native implementation. Gate synthesis, a caller, +source access, correction, dirty restoration and the complete paid/target +bill remain open. No inverse for this singular projection is claimed. +No selected assumption is discharged, no full multiplication theorem is +proved, and no new kappa or literature priority is claimed. diff --git a/research/p104-dyadic-rank-seven/README.md b/research/p104-dyadic-rank-seven/README.md new file mode 100644 index 0000000000..a849985ca0 --- /dev/null +++ b/research/p104-dyadic-rank-seven/README.md @@ -0,0 +1,130 @@ +# A dyadic rank-seven P104 projector below the real quarter-error floor + +**An exact Gaussian-dyadic Hermitian projector answers PR6211's first +open next question. No new κ.** + +For the same fixed 104-root Gram matrix K=RR^T/2, construct +D=I-zz*/65536 with complex rank seven and coefficients in Z[i,1/2]. +Its approximation C=RDR^T/2 has exact maximum complex entry error +**16193/65536**, below **1/4** by **191/65536**. Both C and K-C are +positive semidefinite. The complete witness is + +```text +z = (73-53i, 31+118i, 73-51i, 88+16i, + 73-51i, -15-51i, -87-15i, -88-17i), z* z = 2^16. +``` + +PR6211 already shows complex coefficients can beat the sharp real floor. +Its examples contain odd denominators; this result closes that specific +coefficient-ring gap. It does not improve on PR6211's stronger error +witness or claim optimal error/minimal denominator. Rounding the old +matrix is insufficient: the retained control has rank eight and fails +exact projector idempotence. + +## Reproduce + +From the repository root, with CPython 3.12 and the standard library: + +```sh +python3 -B scripts/research_package.py --package research/p104-dyadic-rank-seven +``` + +Expected: `PASS_REGISTERED_RESEARCH_PACKAGE`, with normal and optimized +copies of `PASS_P104_DYADIC_RANK_SEVEN`, `PASS_FRACTION_REALIFICATION` +and `PASS_BOUNDED_DYADIC_SEARCH`. Six bounded commands are registered. +All four external inputs are pinned in SOURCES.json. Frozen inputs, +shared code, selected records and upstream/ remain unchanged. + +The principal check also runs directly and reads files only: + +```sh +python3 -I -B -W error research/p104-dyadic-rank-seven/verify.py +``` + +[PROOF.md](PROOF.md) gives the exact argument and scope; WITNESS.json +records the vector, expected receipt and completed discovery coverage. +The same checks remain active under optimized Python (`-O`). + +## Evidence + +- All 10,816 entries of the literal Gram product are checked with exact + integer Gaussian arithmetic. The largest squared root response is + 129544, uniquely at zero-based row 24. Gaussian-rational elimination + checks the projector and an eight-root minor independently of the + projection rank formula. +- A second same-author checker imports no primary or predecessor code. + Fraction realification checks rank fourteen, real-part rank eight, + and all 10,816 residual entries with a different root order. +- Nine semantic rejecting controls cover wrong normalization, missing + conjugation, old odd denominators, a changed vector, false error, + naive rounding and malformed root omissions. Four source-byte controls + reject changed inputs. Sixteen real attaining projectors, global + conjugation and sign changes of omitted representatives are positive + scope controls. +- The bounded DP solves five closest-vector boxes on dyadic spheres, + guided by PR6211's stronger witness, and stops at k=8. It does not + minimize coefficient error. Failures at k=4..7 concern only the + selected vectors, not all vectors or denominators. Domain, nonce, + stopping rule and completed coverage are retained in PROOF/WITNESS. + +Actual execution and the initial root-parser correction are recorded in +TASK.json and VALIDATION.json. This is exact finite arithmetic plus a +written proof, not independent human or formal-kernel review. No selected +scientific cold replay or physical supplier replay is claimed. + +## Sources, overlap and scope + +Base: `2485805a6d47f36ea83ddde6327d453ac82d44dc`, priority revision 8. +The selected record identifies PR6030, κ=781451/250000000. Its binding-only +orientation passed. The older number in the priority narrative was not +used as the frontier. + +| Predecessor | Exact source head | Retained contribution | +| --- | --- | --- | +| [apoursh #6211](https://github.com/CrocSwap/integer-mult-bounds/pull/6211) | `369ad15647ad0df0b0ef6f4fcb060509b67f1823` | Complex witnesses, guide and explicit dyadic-projector handoff | +| [apoursh #6191](https://github.com/CrocSwap/integer-mult-bounds/pull/6191) | `be3fc854aa380b3d81e134ce9a4282468e4fa999` | Sharp real rank-seven comparison | +| [Nick Petalas #6183](https://github.com/CrocSwap/integer-mult-bounds/pull/6183) | `eaf77790466f34b86ce72080e3ec690e26dfacab` | Contractive problem, real projector and omission data | +| [Matarener #6166](https://github.com/CrocSwap/integer-mult-bounds/pull/6166) | `096938513138868f0ed27639061f1a5054900f96` | Cited P104-to-D8 physical identification | + +All four are archived as partially reviewed in the base ledger; archival +inclusion is not scientific acceptance. Physical coordinate identification +remains a cited premise. Replay inputs are pinned to their exact copies at +the base commit; no pending branch or predecessor executable is required. + +The repository handoff-first process led to an explicitly changed +coverage-law card for this local algebraic question. Bounded all-state +PR searches for 6191/6211, complex rank approximations and dyadic +projectors, the ledger and newest public handoffs found no competing +dyadic witness. Local overlap was sparse (79/8722 notes), and Discussion +coverage was incomplete. These checks do not certify novelty. +No pinned sprint issue was found, and connected tools cannot post to +Discussions; the advance claim and completion are recorded in TASK.json. + +The real part of C has rank eight, and the residual has spectral norm 13. +Smaller individual coefficient error is not vanishing operator error. +An exact linear seven-channel reconstruction would lose one required +direction. Source access, native realization, correction, dirty +restoration, caller installation and the complete paid/target invoice +remain open. No completed supplier or paid-work saving is claimed. +All five framework assumptions and the selected κ are unchanged. + +## Open next questions + +Can an actual caller use this projection and handle its nonzero residual +at a favorable complete cost? Start with one source/consumer, trace the +exact rank-one residual through every required output, and charge +acquisition, delivery, native realization and restoration. The missing +caller and complete invoice are the blockers. Another approximation or +denominator search alone would not resolve them. TASK.json records this +question structurally; no broader search is reserved. + +## Credit and license + +New witness, bounded construction, proof and verification by **Jerry Chen +(@CubeJerry)** with substantial OpenAI Codex assistance. Armin Pourshafeie / +apoursh, Nick Petalas and Matarener retain the specific predecessor credit +above. 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 +contributions. Hermitian projection, Gram-rank and dynamic programming +are classical; no literature-priority claim. Apache-2.0. diff --git a/research/p104-dyadic-rank-seven/SOURCES.json b/research/p104-dyadic-rank-seven/SOURCES.json new file mode 100644 index 0000000000..a4e505c971 --- /dev/null +++ b/research/p104-dyadic-rank-seven/SOURCES.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "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-complex-rank-seven/PROOF.md", + "usage": "input", + "git_blob": "78c8c0019b8d3d3f8435685102bbf9d541fb611f", + "sha256": "2e1d28966cc50faa857afe425c27cd0bd4142cb77e54d1b289200ac3c6dcfbee" + }, + { + "path": "research/p104-complex-rank-seven/README.md", + "usage": "input", + "git_blob": "fa6ac74b970edfdc1916c5844cc0079758f6c599", + "sha256": "a7298296c2c1b74a6e70dfb8cbbf3328719977bed53889b1f6676dcf4bca28e1" + }, + { + "path": "research/p104-contractive-gram-deflation/MISSING.json", + "usage": "input", + "git_blob": "d5f76681db5edb99899ce6509913b0db60f7280c", + "sha256": "9ddfcf087912e02c46722d5a82eea5f1221a4a33d5037a0d90d392dfcd3c06d4" + }, + { + "path": "research/p104-rank-seven-error-floor/PROOF.md", + "usage": "input", + "git_blob": "08778cc91fac7f668ac9c2f6074e79e9ba1ed0db", + "sha256": "2681e0879e0a0395aa9107f1db24a47a711573ce595ce04c706723bd4ac25305" + } + ] +} diff --git a/research/p104-dyadic-rank-seven/TASK.json b/research/p104-dyadic-rank-seven/TASK.json new file mode 100644 index 0000000000..dcfeaf9338 --- /dev/null +++ b/research/p104-dyadic-rank-seven/TASK.json @@ -0,0 +1,142 @@ +{ + "schema_version": 1, + "task_id": "coverage-law-change", + "priority_revision": 8, + "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "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": "Resolve PR6211 open question 1: one exact Gaussian-dyadic Hermitian rank-seven projector on the same 104 roots with complete maximum coefficient error below 1/4.", + "scope_change_reason": "The handoff identifies a coefficient-ring gap in a local approximate decoder. This is an algebraic feasibility result; it does not meet the original completed-call/full-invoice gate.", + "bottleneck_link": "The binding complex supplier motivates approximation research, but odd denominators in PR6211 preclude even a Gaussian-dyadic coefficient realization. Close only that ring-feasibility gap.", + "budget_minutes": 120, + "stop_rule": "Try k=4..9 in increasing order, each with integer coordinates within one of floor(2^k*z_i/sqrt(2456)); retain the best dot-product norm-4^k vector by exact dynamic programming. Stop at the first strict quarter-error witness, or after all six scales. No native search or wider optimization.", + "outcome": "completed", + "evidence": "WITNESS.json; PROOF.md; complete primary and separate Fraction checks; bounded search replay. Exact error16193/65536 with norm65536; no new kappa.", + "author": "Jerry Chen (@CubeJerry)", + "ai_assistance": "Substantial OpenAI Codex assistance in research, code, proof and verification; no independent human or proof-kernel review claimed.", + "open_questions": [ + { + "question": "Can a fully charged caller exploit the dyadic projection and handle its nonzero residual?", + "why_it_matters": "A smaller coefficient error earns no productive credit and need not reduce recursive cost.", + "first_step": "Specify one actual source/consumer and track this rank-one residual through every required output; charge acquisition, delivery and restoration.", + "blocked_by": "No complete physical caller or paid/target invoice." + } + ], + "selection": { + "track_integer": 44, + "track": "structural decoder research", + "seed": "0b7fc9054fc70396e2d971f95342f0a4", + "seed_role": "Rotate the sixteen real-coordinate DP order by seed modulo 16, breaking exact score ties lexicographically in that order.", + "candidate_tasks": [ + "Sharp complex rank-seven lower bound after PR6211: broad optimization remains, not selected.", + "Exact Gaussian-dyadic Hermitian projector below 1/4: explicit unfilled PR6211 handoff, selected.", + "Independent P104 physical-port/root-coordinate binding: valuable but different from the ring-feasibility handoff, not selected." + ] + }, + "claim": { + "status": "DONE", + "posted_at_utc": "2026-10-30T07:13:58.633437+00:00", + "expected_finish_utc": "2026-10-30T08:58:58.633437+00:00", + "coordination_limitation": "Only open issue #913 is unrelated; no pinned sprint coordination issue found. Connected GitHub tools have no Discussion mutation capability and gh is unavailable. Read live newest handoffs via public HTML and record claim here.", + "head": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "predecessor": "369ad15647ad0df0b0ef6f4fcb060509b67f1823", + "deliverable": "One exact witness, proof and bounded reproducible exact check with semantic controls.", + "result": "Exact Gaussian-dyadic Hermitian projector with error16193/65536; no new kappa.", + "artifact": "https://github.com/CubeJerry/integer-mult-bounds/tree/research/cubejerry-p104-dyadic-projector-20261030-81a6512", + "completion_note": "Local claim updated once with the verified local result and publication destination; remote verification belongs to the final handoff." + }, + "budget_gate": { + "milestone": "local algebraic module only", + "no_paid_gain_claim": "Rank seven is an algebraic factorization size, not a recursive paid rank. The nonzero residual, source acquisition, restoration, native realization and all caller costs remain unpriced. No supplier expansion is authorized by this local result." + }, + "experiment": { + "initial_scout_correction": "The first root loader omitted canonical sign normalization for seven negative-leading omitted representatives, yielding 111 roots. Those outputs are invalid and not scientific search coverage. Corrected to 104 lines and added PR6211 exact 4820 positive control before the declared search.", + "search_result": "First retained DP-selected witness below 1/4 at k=8; k=9 not run; five fully solved bounded closest-vector domains, not an error-optimality search.", + "predecessor_head": "369ad15647ad0df0b0ef6f4fcb060509b67f1823", + "output": "WITNESS.json" + }, + "checkpoints": [ + { + "utc": "2026-10-30T07:15:39.977568+00:00", + "canonical_main": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "priority_revision": 8, + "selected_kappa": "781451/250000000", + "selected_sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa", + "decision": "Continue local coefficient feasibility; selected baseline binding replay passed; current-priorities references historical5599 and is not used as frontier." + }, + { + "utc": "2026-10-30T07:35:43.090573+00:00", + "canonical_main": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "priority_revision": 8, + "selected_kappa": "781451/250000000", + "decision": "Before submission fetch and connected API agree; relevant guidance, selected record and pinned inputs unchanged. Continue completed local result; no frontier change." + } + ], + "overlap": { + "local_records": 81, + "head_records": 8722, + "local_head": "2485805a6d47f36ea83ddde6327d453ac82d44dc", + "remote_pr_searches": [ + "6191", + "6211", + "complex rank approximation", + "Gaussian-dyadic projector" + ], + "read_live_handoffs": "Newest public HTML comments on Discussion1166 at session entry; not exhaustive.", + "known_nearest": [ + "6211 exact rational witnesses and dyadic question", + "6191 real obstruction", + "6183 contractive real obstruction", + "6181 and6238 different joint-bank spectral-correction problem" + ], + "limitation": "Sparse local note corpus, bounded live search and incomplete Discussion coverage; no novelty guarantee." + } +} diff --git a/research/p104-dyadic-rank-seven/VALIDATION.json b/research/p104-dyadic-rank-seven/VALIDATION.json new file mode 100644 index 0000000000..ed82f3b87a --- /dev/null +++ b/research/p104-dyadic-rank-seven/VALIDATION.json @@ -0,0 +1,158 @@ +{ + "schema_version": 1, + "checked_at_utc": "2026-10-30T07:34:17.594950+00:00", + "environment": { + "python": "3.12.14", + "os": "Linux", + "machine": "x86_64" + }, + "commands": [ + { + "argv": [ + "/opt/codex/runtimes/codex-primary-runtime/dependencies/python/bin/python3", + "-I", + "-B", + "-W", + "error", + "research/p104-dyadic-rank-seven/verify.py" + ], + "returncode": 0, + "elapsed_seconds": 0.4883, + "stdout_sha256": "1c978a93f5f5e8ef27b470f58423dbe1eb407d5f9578af3ea534f2527787cbd8", + "status": "PASS_P104_DYADIC_RANK_SEVEN" + }, + { + "argv": [ + "/opt/codex/runtimes/codex-primary-runtime/dependencies/python/bin/python3", + "-I", + "-B", + "-W", + "error", + "-O", + "research/p104-dyadic-rank-seven/verify.py" + ], + "returncode": 0, + "elapsed_seconds": 0.4726, + "stdout_sha256": "1c978a93f5f5e8ef27b470f58423dbe1eb407d5f9578af3ea534f2527787cbd8", + "status": "PASS_P104_DYADIC_RANK_SEVEN" + }, + { + "argv": [ + "/opt/codex/runtimes/codex-primary-runtime/dependencies/python/bin/python3", + "-I", + "-B", + "-W", + "error", + "research/p104-dyadic-rank-seven/fraction_check.py" + ], + "returncode": 0, + "elapsed_seconds": 0.2198, + "stdout_sha256": "7b4b3a0747a397e31121015f68fe595609f3a8f2eb0325676d42eb428dac88cf", + "status": "PASS_FRACTION_REALIFICATION" + }, + { + "argv": [ + "/opt/codex/runtimes/codex-primary-runtime/dependencies/python/bin/python3", + "-I", + "-B", + "-W", + "error", + "-O", + "research/p104-dyadic-rank-seven/fraction_check.py" + ], + "returncode": 0, + "elapsed_seconds": 0.386, + "stdout_sha256": "7b4b3a0747a397e31121015f68fe595609f3a8f2eb0325676d42eb428dac88cf", + "status": "PASS_FRACTION_REALIFICATION" + }, + { + "argv": [ + "/opt/codex/runtimes/codex-primary-runtime/dependencies/python/bin/python3", + "-I", + "-B", + "-W", + "error", + "research/p104-dyadic-rank-seven/search.py" + ], + "returncode": 0, + "elapsed_seconds": 0.0821, + "stdout_sha256": "b387817a0ddc7ae005cc34ec9cac0c7ae01b5a8a5b476f938ded4ec87cf4be10", + "status": "PASS_BOUNDED_DYADIC_SEARCH" + }, + { + "argv": [ + "/opt/codex/runtimes/codex-primary-runtime/dependencies/python/bin/python3", + "-I", + "-B", + "-W", + "error", + "-O", + "research/p104-dyadic-rank-seven/search.py" + ], + "returncode": 0, + "elapsed_seconds": 0.2323, + "stdout_sha256": "b387817a0ddc7ae005cc34ec9cac0c7ae01b5a8a5b476f938ded4ec87cf4be10", + "status": "PASS_BOUNDED_DYADIC_SEARCH" + } + ], + "normal_optimized_outputs_identical": true, + "input_and_code_sha256": { + "research/p104-dyadic-rank-seven/SOURCES.json": "cebc36f2217aa3b18750b2985c68050372888693e9e7d3a04e7d4f573455a4c2", + "research/p104-dyadic-rank-seven/VERIFY.json": "b4f26200176583fe5b2dac75e977b8aef04c56822919aafd86061493a523c9fc", + "research/p104-dyadic-rank-seven/WITNESS.json": "1fae86302f021b748f533bf7c72e03f4a4096b37e0b4a43adfd3b617446ca55a", + "research/p104-dyadic-rank-seven/fraction_check.py": "22b208fbc331c06081e82a9f7b2642fa9519ccb34e3c2f20893b5027b6bd843f", + "research/p104-dyadic-rank-seven/search.py": "d44e06b8dd4eb2281945fb2b188f8c7854c6181505e2223a497d753c44f4029e", + "research/p104-dyadic-rank-seven/verify.py": "5aa716189efb334d0a1c6a5f0bd8a4cc610ca081f2ee1e8dd86edd72621e3649" + }, + "not_run": [ + "Selected scientific cold replay", + "Physical native/caller/rounded multiplier", + "Proof-assistant or independent human review", + "Hosted CI" + ], + "initial_failures": [ + "Exploratory root parsing omitted sign normalization and produced111roots; invalid outputs discarded.104root and rational predecessor controls added before accepted search.", + "Initial draft TASK outcome used a non-schema label; corrected to completed before metadata/registered acceptance." + ], + "portable": { + "mode": "Git-free, empty PATH, files0444/directories0555 during positive replays", + "files_checked": 13, + "all_file_bytes_unchanged": true, + "commands": [ + { + "script": "research/p104-dyadic-rank-seven/verify.py", + "optimized": false, + "status": "PASS_P104_DYADIC_RANK_SEVEN" + }, + { + "script": "research/p104-dyadic-rank-seven/verify.py", + "optimized": true, + "status": "PASS_P104_DYADIC_RANK_SEVEN" + }, + { + "script": "research/p104-dyadic-rank-seven/fraction_check.py", + "optimized": false, + "status": "PASS_FRACTION_REALIFICATION" + }, + { + "script": "research/p104-dyadic-rank-seven/fraction_check.py", + "optimized": true, + "status": "PASS_FRACTION_REALIFICATION" + }, + { + "script": "research/p104-dyadic-rank-seven/search.py", + "optimized": false, + "status": "PASS_BOUNDED_DYADIC_SEARCH" + }, + { + "script": "research/p104-dyadic-rank-seven/search.py", + "optimized": true, + "status": "PASS_BOUNDED_DYADIC_SEARCH" + } + ], + "actual_exported_byte_controls": [ + "source append rejected:source digest", + "changed witness coordinate rejected:Gaussian-dyadic coefficients" + ] + } +} diff --git a/research/p104-dyadic-rank-seven/VERIFY.json b/research/p104-dyadic-rank-seven/VERIFY.json new file mode 100644 index 0000000000..d845f37995 --- /dev/null +++ b/research/p104-dyadic-rank-seven/VERIFY.json @@ -0,0 +1,89 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-complex-rank-seven/PROOF.md", + "research/p104-complex-rank-seven/README.md", + "research/p104-contractive-gram-deflation/MISSING.json", + "research/p104-rank-seven-error-floor/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Complete exact Gram/projector identity, rank, dyadic coefficients, positive fixtures and semantic/source rejection controls" + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-W", + "error", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Complete exact Gram/projector identity, rank, dyadic coefficients, positive fixtures and semantic/source rejection controls" + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-W", + "error", + "{package}/fraction_check.py" + ], + "timeout_seconds": 30, + "checks": "Separate Fraction realification and all residual entries; no primary imports" + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-W", + "error", + "-O", + "{package}/fraction_check.py" + ], + "timeout_seconds": 30, + "checks": "Separate Fraction realification and all residual entries; no primary imports" + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-W", + "error", + "{package}/search.py" + ], + "timeout_seconds": 30, + "checks": "Exact replay of five bounded DP domains and first-success stopping rule" + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-W", + "error", + "-O", + "{package}/search.py" + ], + "timeout_seconds": 30, + "checks": "Exact replay of five bounded DP domains and first-success stopping rule" + } + ] +} diff --git a/research/p104-dyadic-rank-seven/WITNESS.json b/research/p104-dyadic-rank-seven/WITNESS.json new file mode 100644 index 0000000000..1db3b7eede --- /dev/null +++ b/research/p104-dyadic-rank-seven/WITNESS.json @@ -0,0 +1,285 @@ +{ + "schema_version": 1, + "z": [ + [ + 73, + -53 + ], + [ + 31, + 118 + ], + [ + 73, + -51 + ], + [ + 88, + 16 + ], + [ + 73, + -51 + ], + [ + -15, + -51 + ], + [ + -87, + -15 + ], + [ + -88, + -17 + ] + ], + "expected": { + "squared_norm": 65536, + "maximum_squared_response": 129544, + "max_entry_error": "16193/65536", + "gap_below_quarter": "191/65536", + "attaining_indices": [ + 24 + ], + "matrix_entries_checked": 10816, + "projector_rank": 7, + "Gram_rank": 7, + "real_part_rank": 8, + "real_direction_Gram": [ + 40230, + -2683, + 25306 + ], + "Gram_trace": 91, + "residual_operator_norm": 13, + "largest_Gram_coefficient_denominator": 131072 + }, + "search": [ + { + "k": 4, + "vector": [ + 4, + -3, + 2, + 7, + 5, + -3, + 6, + 1, + 5, + -3, + -1, + -3, + -5, + -1, + -6, + -1 + ], + "norm": 256, + "states": [ + 3, + 6, + 15, + 30, + 45, + 61, + 84, + 90, + 90, + 92, + 69, + 65, + 49, + 33, + 29, + 1 + ], + "transitions": 1958, + "dot_product": 790, + "maximum": 592, + "error": "37/128", + "passes": false + }, + { + "k": 5, + "vector": [ + 9, + -6, + 4, + 15, + 10, + -6, + 11, + 2, + 10, + -6, + -2, + -6, + -10, + -2, + -11, + -2 + ], + "norm": 1024, + "states": [ + 3, + 9, + 23, + 60, + 98, + 135, + 166, + 194, + 193, + 185, + 141, + 133, + 97, + 69, + 57, + 1 + ], + "transitions": 4059, + "dot_product": 1583, + "maximum": 2176, + "error": "17/64", + "passes": false + }, + { + "k": 6, + "vector": [ + 18, + -13, + 8, + 30, + 18, + -12, + 22, + 4, + 18, + -13, + -3, + -13, + -22, + -4, + -22, + -4 + ], + "norm": 4096, + "states": [ + 3, + 9, + 27, + 74, + 136, + 210, + 288, + 324, + 332, + 339, + 285, + 269, + 197, + 145, + 117, + 1 + ], + "transitions": 7044, + "dot_product": 3171, + "maximum": 8242, + "error": "4121/16384", + "passes": false + }, + { + "k": 7, + "vector": [ + 36, + -26, + 15, + 59, + 37, + -25, + 44, + 8, + 36, + -26, + -8, + -26, + -44, + -8, + -44, + -8 + ], + "norm": 16384, + "states": [ + 3, + 9, + 27, + 78, + 151, + 263, + 455, + 566, + 661, + 687, + 577, + 545, + 401, + 297, + 237, + 1 + ], + "transitions": 12550, + "dot_product": 6343, + "maximum": 32896, + "error": "257/1024", + "passes": false + }, + { + "k": 8, + "vector": [ + 73, + -53, + 31, + 118, + 73, + -51, + 88, + 16, + 73, + -51, + -15, + -51, + -87, + -15, + -88, + -17 + ], + "norm": 65536, + "states": [ + 3, + 9, + 27, + 78, + 152, + 287, + 573, + 791, + 1030, + 1185, + 1097, + 1074, + 801, + 593, + 473, + 1 + ], + "transitions": 20224, + "dot_product": 12686, + "maximum": 129544, + "error": "16193/65536", + "passes": true + } + ] +} diff --git a/research/p104-dyadic-rank-seven/fraction_check.py b/research/p104-dyadic-rank-seven/fraction_check.py new file mode 100644 index 0000000000..7ad489fcaf --- /dev/null +++ b/research/p104-dyadic-rank-seven/fraction_check.py @@ -0,0 +1,99 @@ +#!/usr/bin/env python3 +"""Second arithmetic path: realification over Fraction, no primary imports. + +Jerry Chen (@CubeJerry), substantial OpenAI Codex assistance. Apache-2.0. +This is same-author cross-checking, not independent human review. +""" + +import hashlib +import itertools +import json +from fractions import Fraction as Q +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def check(condition, message): + if not condition: + raise ValueError(message) + + +def rank(a): + a = [list(map(Q, row)) for row in a] + pivot = 0 + for column in range(len(a[0])): + choices = [i for i in range(pivot, len(a)) if a[i][column]] + if not choices: + continue + i = choices[0] + a[pivot], a[i] = a[i], a[pivot] + scale = a[pivot][column] + a[pivot] = [x / scale for x in a[pivot]] + for i in range(len(a)): + if i != pivot: + factor = a[i][column] + a[i] = [x - factor * y for x, y in zip(a[i], a[pivot], strict=True)] + pivot += 1 + if pivot == len(a): + break + return pivot + + +def main(): + sources = json.loads((HERE / "SOURCES.json").read_text()) + for source in sources["files"]: + if source["usage"] == "input": + data = (ROOT / source["path"]).read_bytes() + check(hashlib.sha256(data).hexdigest() == source["sha256"], "source hash") + data = json.loads((ROOT / "research/p104-contractive-gram-deflation/MISSING.json").read_text()) + absent = {tuple(Q(1 if c == "+" else -1) / 2 for c in s) for s in data["signs"]} + absent |= {tuple(-x for x in row) for row in absent} + roots = set() + for positions in itertools.combinations(range(8), 2): + for signs in itertools.product((-1, 1), repeat=2): + row = [Q(0)] * 8 + for i, sign in zip(positions, signs, strict=True): + row[i] = Q(sign) + if next(x for x in row if x) > 0: + roots.add(tuple(row)) + for signs in itertools.product((-1, 1), repeat=8): + row = tuple(Q(x, 2) for x in signs) + if signs.count(-1) % 2 and signs[0] > 0 and row not in absent: + roots.add(row) + roots = sorted(roots) + check(len(roots) == 104, "root count") + witness = json.loads((HERE / "WITNESS.json").read_text()) + u, v = zip(*witness["z"], strict=True) + n = sum(x * x + y * y for x, y in zip(u, v, strict=True)) + a = [[Q(int(i == j)) - Q(u[i] * u[j] + v[i] * v[j], n) + for j in range(8)] for i in range(8)] + b = [[Q(u[i] * v[j] - v[i] * u[j], n) for j in range(8)] for i in range(8)] + realified = [a[i] + [-x for x in b[i]] for i in range(8)] + realified += [b[i] + a[i] for i in range(8)] + for i, j in itertools.product(range(16), repeat=2): + check(realified[i][j] == realified[j][i], "realification symmetric") + check(sum(realified[i][k] * realified[k][j] for k in range(16)) + == realified[i][j], "realification projector") + check(rank(realified) == 14, "realification rank fourteen") + check(rank(a) == 8, "real part rank eight") + x = [sum(ri * ui for ri, ui in zip(r, u, strict=True)) for r in roots] + y = [sum(ri * vi for ri, vi in zip(r, v, strict=True)) for r in roots] + squared_errors = [] + for i, j in itertools.product(range(104), repeat=2): + er = (x[i] * x[j] + y[i] * y[j]) / (2 * n) + ei = (y[i] * x[j] - x[i] * y[j]) / (2 * n) + squared_errors.append(er * er + ei * ei) + check(er.denominator & (er.denominator - 1) == 0, "real dyadic residual") + check(ei.denominator & (ei.denominator - 1) == 0, "imaginary dyadic residual") + error = Q(witness["expected"]["max_entry_error"]) + check(max(squared_errors) == error * error and error < Q(1, 4), "full residual maximum") + print(json.dumps({"status": "PASS_FRACTION_REALIFICATION", "roots": len(roots), + "realification_rank": 14, "real_part_rank": 8, + "matrix_entries": len(squared_errors), + "max_squared_error": str(max(squared_errors))}, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-dyadic-rank-seven/search.py b/research/p104-dyadic-rank-seven/search.py new file mode 100644 index 0000000000..a281c90f3e --- /dev/null +++ b/research/p104-dyadic-rank-seven/search.py @@ -0,0 +1,94 @@ +#!/usr/bin/env python3 +"""Replay the bounded dyadic-sphere construction; no optimal-error claim. + +Jerry Chen / CubeJerry with substantial OpenAI Codex assistance. Apache-2.0. +""" + +import importlib.util +import json +from fractions import Fraction +from math import isqrt +from pathlib import Path + +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location("certificate", HERE / "verify.py") +certificate = importlib.util.module_from_spec(spec) +spec.loader.exec_module(certificate) +SEED = "0b7fc9054fc70396e2d971f95342f0a4" +Z = [x for pair in certificate.GUIDE for x in pair] +N = sum(x * x for x in Z) + + +def floor_coordinate(x, radius): + square = (radius * x) ** 2 + lower = isqrt(square // N) + return lower if x >= 0 else -lower - (lower * lower * N != square) + + +def closest(k): + radius = 2 ** k + offset = int(SEED, 16) % 16 + order = list(range(offset, 16)) + list(range(offset)) + choices = [list(range(floor_coordinate(Z[i], radius) - 1, + floor_coordinate(Z[i], radius) + 2)) for i in order] + low = [sum(min(x * x for x in c) for c in choices[j:]) for j in range(17)] + high = [sum(max(x * x for x in c) for c in choices[j:]) for j in range(17)] + dp, counts, transitions = {0: (0, ())}, [], 0 + for j, (i, options) in enumerate(zip(order, choices, strict=True)): + output = {} + for total, (score, vector) in dp.items(): + for x in options: + squared = total + x * x + if squared + low[j + 1] <= radius ** 2 <= squared + high[j + 1]: + candidate = (score + x * Z[i], vector + (x,)) + transitions += 1 + if squared not in output or candidate > output[squared]: + output[squared] = candidate + dp = output + counts.append(len(dp)) + if radius ** 2 not in dp: + return {"k": k, "no_norm_vector": True, "states": counts} + score, raw = dp[radius ** 2] + vector = [0] * 16 + for i, x in zip(order, raw, strict=True): + vector[i] = x + certificate.require(sum(x * x for x in vector) == radius ** 2, "search exact norm") + return {"k": k, "vector": vector, "norm": radius ** 2, + "states": counts, "transitions": transitions, "dot_product": score} + + +def replay(): + certificate.check_sources() + signs = json.loads((certificate.ROOT / certificate.DATA).read_text())["signs"] + roots, _ = certificate.roots_from_signs(signs) + certificate.require(max(map(certificate.norm, certificate.responses(roots, certificate.GUIDE))) + == 4820, "search predecessor positive control") + results = [] + for k in range(4, 10): + record = closest(k) + if "vector" in record: + v = record["vector"] + z = list(zip(v[::2], v[1::2], strict=True)) + maximum = max(map(certificate.norm, certificate.responses(roots, z))) + record.update(maximum=maximum, error=str(Fraction(maximum, 8 * record["norm"])), + passes=maximum < 2 * record["norm"]) + results.append(record) + if record.get("passes"): + break + return results + + +def main(): + result = replay() + witness = json.loads((HERE / "WITNESS.json").read_text()) + certificate.require(result == witness["search"], "search receipt") + flat = result[-1]["vector"] + certificate.require([list(x) for x in zip(flat[::2], flat[1::2], strict=True)] == witness["z"], + "search final witness") + print(json.dumps({"status": "PASS_BOUNDED_DYADIC_SEARCH", "seed": SEED, + "scales_completed": len(result), "stopped_at": result[-1]["k"], + "search": result}, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-dyadic-rank-seven/verify.py b/research/p104-dyadic-rank-seven/verify.py new file mode 100644 index 0000000000..6bf945e443 --- /dev/null +++ b/research/p104-dyadic-rank-seven/verify.py @@ -0,0 +1,265 @@ +#!/usr/bin/env python3 +"""Exact dyadic P104 certificate. Jerry Chen / CubeJerry, Codex-assisted. + +Apache-2.0. No predecessor executable, floating arithmetic or external library. +Complex numbers are pairs; the matrix audit uses integral common denominators. +""" + +import hashlib +import itertools +import json +from fractions import Fraction as F +from math import gcd +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +DATA = "research/p104-contractive-gram-deflation/MISSING.json" +GUIDE = [(14, -10), (6, 23), (14, -10), (17, 3), + (14, -10), (-3, -10), (-17, -3), (-17, -3)] +ZERO = (0, 0) + + +def require(ok, reason): + if not ok: + raise ValueError(reason) + + +def add(a, b): + return (a[0] + b[0], a[1] + b[1]) + + +def sub(a, b): + return (a[0] - b[0], a[1] - b[1]) + + +def mul(a, b): + return (a[0] * b[0] - a[1] * b[1], a[0] * b[1] + a[1] * b[0]) + + +def conj(a): + return (a[0], -a[1]) + + +def norm(a): + return a[0] ** 2 + a[1] ** 2 + + +def dot(a, b): + return sum(x * y for x, y in zip(a, b, strict=True)) + + +def gdot(a, b): + result = ZERO + for x, y in zip(a, b, strict=True): + result = add(result, mul(x, y)) + return result + + +def mm(a, b): + columns = list(zip(*b, strict=True)) + return [[gdot(row, col) for col in columns] for row in a] + + +def rank(matrix): + """Separate Gaussian-rational elimination; no projector rank shortcut.""" + a = [[(F(x), F(y)) for x, y in row] for row in matrix] + height, width, pivot_row = len(a), len(a[0]), 0 + for col in range(width): + pivot = next((i for i in range(pivot_row, height) if a[i][col] != ZERO), None) + if pivot is None: + continue + a[pivot_row], a[pivot] = a[pivot], a[pivot_row] + value = a[pivot_row][col] + inverse = (value[0] / norm(value), -value[1] / norm(value)) + a[pivot_row] = [mul(x, inverse) for x in a[pivot_row]] + for row in range(pivot_row + 1, height): + if a[row][col] != ZERO: + scale = a[row][col] + a[row] = [sub(x, mul(scale, y)) + for x, y in zip(a[row], a[pivot_row], strict=True)] + pivot_row += 1 + if pivot_row == height: + break + return pivot_row + + +def authenticate(payload, expected): + require(hashlib.sha256(payload).hexdigest() == expected, "source digest") + + +def check_sources(): + sources = json.loads((HERE / "SOURCES.json").read_text()) + rows = [r for r in sources["files"] if r["usage"] == "input"] + for row in rows: + path = ROOT / row["path"] + require(path.is_file() and not path.is_symlink(), "source regular file") + authenticate(path.read_bytes(), row["sha256"]) + return rows + + +def roots_from_signs(signs): + require(isinstance(signs, list) and len(signs) == 16, "sixteen omitted lines") + omitted = set() + for text in signs: + require(isinstance(text, str) and len(text) == 8 and set(text) <= {"+", "-"}, + "sign alphabet") + require(text.count("-") % 2 == 1, "odd spin parity") + row = tuple(1 if x == "+" else -1 for x in text) + omitted.add(tuple(row[0] * x for x in row)) + require(len(omitted) == 16, "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)) + roots += [(1, *tail) for tail in itertools.product((-1, 1), repeat=7) + if tail.count(-1) % 2 == 1 and (1, *tail) not in omitted] + require(len(roots) == len(set(roots)) == 104, "104 distinct roots") + require(all(dot(r, r) == 8 for r in roots), "doubled root norm") + return roots, sorted(omitted) + + +def responses(roots, z): + return [(dot(r, [x[0] for x in z]), dot(r, [x[1] for x in z])) for r in roots] + + +def projector(z, denominator=None, conjugate=True): + require(len(z) == 8 and all(len(x) == 2 for x in z), "eight Gaussian coordinates") + require(all(type(c) is int for x in z for c in x), "integer witness") + n = sum(map(norm, z)) if denominator is None else denominator + require(type(n) is int and n > 0, "positive denominator") + d = [[sub((n * (i == j), 0), mul(z[i], conj(z[j]) if conjugate else z[j])) + for j in range(8)] for i in range(8)] + return d, n + + +def dyadic(n): + return n > 0 and n & (n - 1) == 0 + + +def audit_projector(d, n): + require(all(d[i][j] == conj(d[j][i]) for i in range(8) for j in range(8)), + "Hermitian projector") + square = mm(d, d) + require(square == [[(n * x, n * y) for x, y in row] for row in d], + "projector idempotence") + require(sum(d[i][i][0] for i in range(8)) == 7 * n, "projector trace seven") + require(all(dyadic(n // gcd(n, c)) for row in d for entry in row for c in entry), + "Gaussian-dyadic coefficients") + require(rank(d) == 7, "complex projector rank seven") + + +def audit(z, roots, expected_error=None): + d, n = projector(z) + audit_projector(d, n) + require(dyadic(n), "power-of-two squared norm") + require(all(gdot(row, z) == ZERO for row in d), "projector kernel") + s = [[(x, 0) for x in row] for row in roots] + c = mm(mm(s, d), list(zip(*s, strict=True))) # common denominator 8n + values = responses(roots, z) + maximum = max(map(norm, values)) + max_residual_squared, max_denominator = 0, 1 + for i, row in enumerate(roots): + for j, other in enumerate(roots): + residual = sub((n * dot(row, other), 0), c[i][j]) + require(residual == mul(values[i], conj(values[j])), "literal residual identity") + max_residual_squared = max(max_residual_squared, norm(residual)) + for component in c[i][j]: + reduced_denominator = 8 * n // gcd(8 * n, component) + require(dyadic(reduced_denominator), "dyadic Gram coefficient") + max_denominator = max(max_denominator, reduced_denominator) + require(max_residual_squared == maximum ** 2, "maximum complex modulus") + error = F(maximum, 8 * n) + require(error < F(1, 4), "strict quarter error") + if expected_error is not None: + require(error == expected_error, "claimed error") + basis = [roots.index(tuple(2 * (int(k == i) + sign * int(k == i + 1)) + for k in range(8))) + for i in range(0, 8, 2) for sign in (-1, 1)] + minor = [[c[i][j] for j in basis] for i in basis] + require(rank(minor) == 7, "Gram minor rank seven") + real_minor = [[(x, 0) for x, y in row] for row in minor] + require(rank(real_minor) == 8, "real-part rank eight") + require(all(sum(r[i] * r[j] for r in roots) == 104 * (i == j) + for i in range(8) for j in range(8)), "tight root frame") + require(sum(c[i][i][0] for i in range(104)) == 91 * 8 * n, "Gram trace 91") + u, v = [x for x, _ in z], [y for _, y in z] + real_gram = [dot(u, u), dot(u, v), dot(v, v)] + require(real_gram[0] * real_gram[2] > real_gram[1] ** 2, "independent real directions") + return {"squared_norm": n, "maximum_squared_response": maximum, + "max_entry_error": str(error), "gap_below_quarter": str(F(1, 4) - error), + "attaining_indices": [i for i, x in enumerate(values) if norm(x) == maximum], + "matrix_entries_checked": len(roots) ** 2, "projector_rank": 7, + "Gram_rank": 7, "real_part_rank": 8, "real_direction_Gram": real_gram, + "Gram_trace": 91, "residual_operator_norm": 13, + "largest_Gram_coefficient_denominator": max_denominator} + + +def rejects(callback, reason): + try: + callback() + except ValueError as exc: + require(str(exc) == reason, "wrong rejection: " + str(exc)) + return + raise ValueError("control accepted: " + reason) + + +def controls(z, roots, signs, sources): + d, n = projector(z) + rejects(lambda: audit_projector(*projector(z, n // 2)), "projector idempotence") + rejects(lambda: audit_projector(*projector(z, conjugate=False)), "Hermitian projector") + rejects(lambda: audit_projector(*projector(GUIDE)), "Gaussian-dyadic coefficients") + bad = [tuple(x) for x in z] + bad[0] = (bad[0][0] + 1, bad[0][1]) + rejects(lambda: audit_projector(*projector(bad)), "Gaussian-dyadic coefficients") + rejects(lambda: audit(z, roots, F(1, 4)), "claimed error") + # Entrywise nearest dyadic rounding of the old matrix destroys exact rank. + old, old_n = projector(GUIDE) + rounded = [[tuple((2 * c * n + old_n) // (2 * old_n) for c in entry) + for entry in row] for row in old] + rejects(lambda: audit_projector(rounded, n), "projector idempotence") + rejects(lambda: roots_from_signs(signs[:-1]), "sixteen omitted lines") + rejects(lambda: roots_from_signs(signs[:-1] + [signs[0]]), "distinct omitted lines") + wrong_parity = list(signs) + wrong_parity[0] = ("-" if signs[0][0] == "+" else "+") + signs[0][1:] + rejects(lambda: roots_from_signs(wrong_parity), "odd spin parity") + for row in sources: + payload = (ROOT / row["path"]).read_bytes() + rejects(lambda: authenticate(payload + b" ", row["sha256"]), "source digest") + real_z = [(x, 0) for x, y in z] + real_error = F(max(map(norm, responses(roots, real_z))), + 8 * sum(map(norm, real_z))) + require(real_error >= F(1, 4), "real-part witness boundary") + return {"semantic_rejections": 9, "source_byte_rejections": len(sources), + "rounded_predecessor_rank": rank(rounded), "real_only_error": str(real_error)} + + +def main(): + sources = check_sources() + signs = json.loads((ROOT / DATA).read_text())["signs"] + roots, omitted = roots_from_signs(signs) + require(max(map(norm, responses(roots, GUIDE))) == 4820, "predecessor positive control") + witness = json.loads((HERE / "WITNESS.json").read_text()) + z = [tuple(x) for x in witness["z"]] + result = audit(z, roots, F(witness["expected"]["max_entry_error"])) + require(result == witness["expected"], "complete witness receipt") + # Changing root representatives and global conjugation must preserve the result. + reversed_signs = ["".join("-" if c == "+" else "+" for c in s) for s in signs] + require(roots_from_signs(reversed_signs)[0] == roots, "root representative invariance") + require(audit([conj(x) for x in z], roots)["max_entry_error"] == result["max_entry_error"], + "global conjugation invariance") + real_controls = 0 + for q in omitted: + require(F(max(dot(r, q) ** 2 for r in roots), 8 * dot(q, q)) == F(1, 4), + "predecessor real quarter-error fixture") + real_controls += 1 + result["controls"] = controls(z, roots, signs, sources) + result["real_attaining_controls"] = real_controls + result["status"] = "PASS_P104_DYADIC_RANK_SEVEN" + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()