diff --git a/research/rational-header-orbit-lattice/PROOF.md b/research/rational-header-orbit-lattice/PROOF.md new file mode 100644 index 0000000000..2478c1db3c --- /dev/null +++ b/research/rational-header-orbit-lattice/PROOF.md @@ -0,0 +1,158 @@ +# Rational header orbits retain their integer lattice + +This scoped proof was produced by Nick Petalas. Apache-2.0. + +## Contract and cited inputs + +Fix an even integer n >= 2, V = Q^n, and a nondegenerate alternating +rational form omega. A normalized saturated header is an ordered tuple +T = ((x_i,y_i)) for i = 0,...,n, with + +```text +y_i = omega(x_i, .), +y_i x_j = sgn(i-j), +U_i = I - 2 x_i y_i, +U_n ... U_0 = -I. +``` + +The form and ambient rational coordinates are fixed. Allowed equivalence +is a finite sequence of the normalized Hurwitz moves + +```text +mu_i^+ : (x_i,x_(i+1)) -> (x_(i+1), 2x_(i+1)-x_i), +mu_i^- : (x_i,x_(i+1)) -> (2x_i-x_(i+1), x_i), +``` + +with the corresponding covectors obtained from the same fixed omega. +There are no additional rational changes of frame or rescalings in this +equivalence relation. A simultaneous global sign may be quotiented out +without changing the result below, since it changes neither invariant. + +We cite DreamingOfClouds's #6842, `p104-header-braid-classification`, +Theorems 1, 3 and 4, for the normalized header structure, the moves and +the integral-frame classification. In particular the unique relation is +sum_i (-1)^i x_i = 0, the first n vectors are a basis, and in a fixed +integral unimodular frame two integral normalized headers are equivalent +exactly when their vector multisets modulo 2 agree. These results are +premises here, not results independently checked by this package. + +The integral sufficiency input in dimensions n >= 4 uses the pure braid +image theorem, Brendle and Margalit, *The level four braid group*, +[Theorem 3.3(1)](https://arxiv.org/pdf/1410.7416), which states the +surjectivity for genus g >= 2 and credits A'Campo. We do not reprove it. +For n = 2 the elementary argument at the end of the next section suffices. + +## The lattice and the classification + +Define L(T) = sum_i Z x_i inside V. This is an embedded integer lattice, +not the rational span and not the 2-local span. Define C(T) to be the +multiset of the classes x_i + 2L(T) in the intrinsic quotient L(T)/2L(T). +Comparing C(T) and C(T') is meaningful as an equality in the same quotient +only after L(T) = L(T') has been established. + +**Theorem.** For two normalized rational headers in the same fixed form, + +```text +T ~ T' iff L(T) = L(T') and C(T) = C(T'). +``` + +Thus the missing rational invariant is the embedded integer lattice. +Once that lattice is fixed, the remaining classification is exactly the +predecessor's integral one, evaluated intrinsically in that lattice. + +**Proof.** Let B have columns x_0,...,x_(n-1). The cited alternating +relation expresses x_n as an integral combination of these columns. +Consequently L(T) = B Z^n. Its Gram matrix is + +```text +B^T omega B = S, S_ij = sgn(i-j), 0 <= i,j < n. +``` + +It is an integral unimodular alternating matrix, by the cited header +structure. In particular L(T) is an integral unimodular symplectic lattice +even when its embedding in the original coordinate lattice is rational. + +A forward move replaces two generators a,b by b,2b-a. Conversely +a = 2b-(2b-a), so the integer span is unchanged. An inverse move gives +the same conclusion. Modulo 2L the move just exchanges the two classes, +so the multiset C is also unchanged. This proves necessity without any +braid-image theorem. + +For sufficiency suppose L(T') = L(T) = L. Choose the single lattice basis +B from T, and express both entire headers in its coordinates. Both vector +tuples are integral; their covectors are integral because the form S is +integral. The form is the same fixed unimodular S for both tuples. Their +ambient integral residue multisets in these coordinates are exactly C(T) +and C(T'). Apply #6842's integral classification to obtain a finite +Hurwitz word connecting them. Every move is an integer linear formula, +so changing coordinates back by B carries that same literal word from T +to T'. This proves sufficiency. No rational frame change has been added +to the allowed operations; the single coordinate chart is only used in +the proof. + +For n = 2, the three residue vectors of a normalized header are exactly +the three nonzero elements of L/2L. The two differences +d_0 = x_0-x_1 and d_1 = x_1-x_2 = x_0 are an integer basis with pairing +-1. The two move transformations are the transvections along d_0,d_1, +which in that basis are the two elementary unipotent generators of +SL_2(Z), up to inverse and sign conventions. They generate SL_2(Z) by +the integer Euclidean algorithm. Rigidity gives a symplectic integral +transition between any two headers on L, so all of them are connected. +This establishes the required dimension-two sufficiency directly. QED. + +The theorem is independent of a chosen basis of L: changing the common +basis applies one invertible linear map to both intrinsic multisets. +Using a separately chosen basis for each header and comparing the two +coordinate lists would discard the invariant and is not the criterion. + +## An infinite obstruction invisible modulo 2 + +Take n = 2, omega = [[0,-1],[1,0]], and for each positive odd integer m set + +```text +x_0(m) = (1/m, 0), +x_1(m) = (0, m), +x_2(m) = (-1/m, m), +y_i(m) = x_i(m)^T omega. +``` + +These are the conjugates of the normalized header at m = 1 by the +symplectic rational matrix G_m = diag(1/m,m), so they are normalized +headers in the same fixed omega. Equivalently, their covectors are +(0,-1/m), (m,0), (m,1/m); their pairings give the required sign Gram, +and multiplying the three literal units gives -I. + +All coordinates lie in Z_(2), the rationals with odd denominators. +Reduction of any odd integer or its inverse modulo 2 is 1. Hence every +tuple has the identical ambient reduction + +```text +{(1,0), (0,1), (1,1)} in F_2^2. +``` + +But L_m = (1/m)Z e_0 + m Z e_1. Its first-coordinate projection is +(1/m)Z, so equality L_m = L_k for positive m,k implies m = k. +Necessity in the theorem therefore proves that these headers occupy +pairwise different Hurwitz orbits. Each lattice has covolume one and +the same unimodular form; neither covolume nor ambient mod-2 data detects +the obstruction. In dimension two the lattice alone is also sufficient, +as established above. + +This conclusion does not contradict #6842's integral theorem, whose +integral ambient-frame hypothesis forces L = Z^n. It shows why replacing +that hypothesis by 2-local integrality while keeping only ambient mod-2 +data would lose information. It excludes connecting distinct L_m by +Hurwitz moves, not connecting them by an explicitly paid rational frame +change or by a larger operation alphabet. + +## Evidence boundary + +The theorem and the infinite family follow from the written argument. +The new standalone checker corroborates rational instances, literal +Hurwitz walks, both invariants, and the full product on each checked +tuple. It also supplies a same-lattice pair with different intrinsic +residue multisets, demonstrating the need for both parts in dimension +four. This is not a census of rational headers or an independent replay +of #6842. Native implementation, site-mask legality, compiler closure, +physical frame changes, precision, storage and complete pricing remain +outside scope. No multiplication theorem or new kappa follows. diff --git a/research/rational-header-orbit-lattice/README.md b/research/rational-header-orbit-lattice/README.md new file mode 100644 index 0000000000..42bf3e88cf --- /dev/null +++ b/research/rational-header-orbit-lattice/README.md @@ -0,0 +1,138 @@ +# Rational header orbits need an integer-lattice invariant + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: scoped written proof with exact finite corroboration. +For normalized saturated headers on Q^n, n even, in one fixed rational +symplectic form, the exact Hurwitz-equivalence criterion is + +```text +T ~ T' iff L(T) = L(T') and C(T) = C(T'), +L(T) = sum_i Z x_i, +C(T) = multiset {x_i + 2L(T)} in L(T)/2L(T). +``` + +The integer lattice is embedded in the original rational coordinate +space. The two residue multisets must be compared in that same lattice. +Rational changes of frame are not allowed as extra equivalences. + +DreamingOfClouds's [#6842](https://github.com/CrocSwap/integer-mult-bounds/pull/6842) +classifies the integral case and explicitly leaves non-integral frames +outside its scope. Its structure and integral classification are cited +premises. The new step is the embedded-lattice invariant, the transport of +that classification to rational headers, and an infinite counterexample +to using only ambient mod-2 data in the 2-local domain. + +For every positive odd integer m, in the fixed form [[0,-1],[1,0]], take + +```text +x_0 = (1/m,0), x_1 = (0,m), x_2 = (-1/m,m), +y_i = x_i^T omega, U_i = I-2x_i y_i. +``` + +These are normalized headers with U_2 U_1 U_0 = -I. All have the same +ambient reduction {(1,0),(0,1),(1,1)} modulo 2 and covolume one. +Their lattices (1/m)Z e_0 + m Z e_1 are pairwise distinct, so their +Hurwitz orbits are pairwise distinct. In dimension two the lattice alone +is also sufficient. [PROOF.md](PROOF.md) gives the universal argument. + +## Evidence and reproduction + +The standalone exact checker enumerates new rational instances only: + +- Twelve rational initial headers, dimensions 2, 4, 6 and 8, followed + through 16 literal Hurwitz moves each. All 192 steps preserve the + lattice and intrinsic residues and pass the full header product. +- Sixteen odd-denominator headers, m = 1,3,...,31. All 120 pairs have + distinct embedded lattices despite identical ambient mod-2 data. +- One rational dimension-four pair has the same lattice but different + intrinsic residue multisets. This demonstrates why the second + invariant is still required when the lattice is fixed. +- Five rejection controls cover singular bases, even denominators, + vectors outside the chosen lattice, an invalid move and an altered + normalized header. + +From the worktree root, with CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/rational-header-orbit-lattice/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/rational-header-orbit-lattice/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/rational-header-orbit-lattice +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/rational-header-orbit-lattice --check-source-history +``` + +Another CPython 3.12 path may be substituted. The direct marker is +`PASS_RATIONAL_HEADER_ORBIT_LATTICE`; the registered runner prints +`PASS_REGISTERED_RESEARCH_PACKAGE`. The final command checks committed +publication bytes and source history. The verifier accepts no arguments, +writes no files and prints a generated receipt bound to SHA256 hashes of +all six package files. There is no handwritten or committed receipt. +It also runs in a Git-free export of these six files. + +## Scope, provenance and credit + +Base is canonical main e54523517d0f03e58352e647c403a5af3e525a57, priority +revision 8. The selected #7000 record, not the older narrative checkpoint, +is the baseline. Its cheap binding orientation passed; its scientific +replay was not run. The formal-interface-lemma card changes scope to this +algebraic side result. It does not discharge a selected assumption. + +[The advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19538524) +records the rational-header question. Live PRs, recent account submissions, +handoffs, local reservations, distinctive main README searches and merged +searches were checked. The overlap snapshot covered 477 open PRs and +7,129 Discussion records with complete pagination; sparse local notes +were incomplete. These checks do not establish absence of unpublished work. +No open PR studying this rational-header equivalence was found. + +Credit DreamingOfClouds #6842 for normalized header structure, Hurwitz +action, the integral theorem and this excluded domain; #6832/#6833/#6836, +CubeJerry #6839/#6840 and zxv #6726 retain its root lineage. Brendle and +Margalit's *The level four braid group*, Theorem 3.3(1), supplies the +cited higher-dimensional pure braid image, with A'Campo credited there. +The dimension-two elementary-generation argument is written here. +Lattice transport and the Euclidean algorithm are classical; no +literature-wide priority is claimed. SOURCES.json pins predecessor texts +as provenance. No predecessor code is imported or scientifically replayed. +All predecessor files and credit lines remain unchanged. + +The classification assumes normalized headers, the same rational form, +exactly n+1 square-zero rank-one units and only the stated Hurwitz moves. +It is not an orbit classification under rational conjugacy, a bounded +word-length result or a constructive braid-synthesis algorithm. Its +sufficiency cites the integral theorem; the lattice obstruction itself +does not need that input. The finite checks corroborate the new instances; +the written proof supplies the universal and infinite claims. + +No new kappa, native supplier, legal site-mask program, physical frame +conversion, complete paid/target bill, compiler closure, precision/tape +or stock bound follows. No selected cold replay, Lean, Docker or complete +multiplication theorem was run or claimed. Independent human and formal +proof-kernel review are unclaimed. + +## Open next questions + +Can a physically legal rational frame change join two distinct header +lattices at a favorable complete cost? Begin with one literal root and +conversion, charging dirty restoration, every native conversion, movement +and target effect. The present invariant rules out a Hurwitz-only route; +it does not price a changed operation alphabet. TASK.json records the +first step and the missing physical contract. Research stops at the +classification and explicit infinite family. + +## Verifier constraints + +Power of Ten inspection covers the single new Python file. Functions +are below 60 lines. The fixed computation has matrices of dimension at +most nine, 12 walks of exactly 16 steps and 16 family members. There is +no recursion, subprocess, network, dynamic code execution or external +scientific dependency. State is local, checks use explicit exceptions, +and warning-strict normal and optimized modes are registered. Six hash +reads are capped at 256 KiB each, and the verifier rejects CLI inputs. + +Rule 3 has a managed-runtime deviation. CPython allocates exact integers, +Fractions and containers dynamically; the fixed fixtures and bounded +walks bound algorithmic collections. Interpreter allocation has not been +instrumented, and a fixed-storage implementation would require separate +work. Rule 10 uses the registered warning-strict executions and AST +inspection; no separate static type checker or proof assistant is claimed. diff --git a/research/rational-header-orbit-lattice/SOURCES.json b/research/rational-header-orbit-lattice/SOURCES.json new file mode 100644 index 0000000000..2932410caa --- /dev/null +++ b/research/rational-header-orbit-lattice/SOURCES.json @@ -0,0 +1,52 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/p104-header-braid-classification/PROOF.md", + "usage": "provenance", + "git_blob": "d565a4831291c88cfae2d2e3c39068cf75dc5523", + "sha256": "0bc551ef8f418ac250534bdbe66f05d0579e28093e900c557bfc667658d754ec" + }, + { + "path": "research/p104-header-braid-classification/README.md", + "usage": "provenance", + "git_blob": "1a6023cd067135fba4f4415934d7611139e4dc7f", + "sha256": "e45d4088a932e236e0bf66624375e3b5b2505bd2376b8b233d627c0aa3056371" + }, + { + "path": "docs/research/current-priorities.md", + "usage": "provenance", + "git_blob": "6f5d40d13d8f3bdc12ce7954c8c3eb4ab1f8be91", + "sha256": "70f61c8d140ae6e892f2b8f065bba4eae3e76f7a8f55f632fd4e2f9f34039bdc" + }, + { + "path": "docs/research/research-family-status.md", + "usage": "provenance", + "git_blob": "3c19b18ef7225b47f0abcd9d51ae7c83d0cdfd15", + "sha256": "92c8010dfd9fc33e921f70526231f8689e06ea784f1b1387d895344b227f36d7" + } + ], + "external_citation": { + "title": "The level four braid group", + "authors": [ + "Tara E. Brendle", + "Dan Margalit" + ], + "url": "https://arxiv.org/pdf/1410.7416", + "version": "v3, 21 April 2021", + "use": "Theorem 3.3(1), genus at least two, cited input behind the predecessor integral classification; not a runtime dependency." + } +} diff --git a/research/rational-header-orbit-lattice/TASK.json b/research/rational-header-orbit-lattice/TASK.json new file mode 100644 index 0000000000..e9aa627d1c --- /dev/null +++ b/research/rational-header-orbit-lattice/TASK.json @@ -0,0 +1,109 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Classify normalized rational saturated-header Hurwitz orbits in a fixed rational form by their embedded integer lattice and intrinsic mod-2 multiset; exhibit infinitely many 2-locally integral orbits with the same ambient mod-2 data.", + "scope_change_reason": "An algebraic side result extends the explicitly excluded non-integral domain of DreamingOfClouds PR6842. This is a written proof, not an audit, proof-assistant formalization, selected assumption discharge or supplier improvement.", + "bottleneck_link": "Rational helper/root frame changes need their own implementation and price. The new invariant prevents treating equality of ambient mod-2 headers as a sufficient rational Hurwitz connection. No full signed invoice gain is claimed.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved lattice classification and explicit infinite counterexample family; package it without extending to priced frame changes.", + "outcome": "completed", + "evidence": "PROOF.md gives the universal argument; verify.py checks new rational headers, literal walks, distinct lattices and semantic controls. Its stdout is a generated hash-bound receipt.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can one physically legal rational frame change join distinct header lattices at a favorable complete cost?", + "why_it_matters": "The obstruction applies to Hurwitz moves, while a paid frame change may alter the lattice and enable a new native root.", + "first_step": "Pin one root and proposed rational frame change, then charge all native conversions, dirty restoration, movement and target effects.", + "blocked_by": "No physical conversion or complete price is provided by the algebraic classification." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19538524", + "predecessor": { + "pr": 6842, + "author": "DreamingOfClouds", + "package": "research/p104-header-braid-classification", + "use": "Cited structure, Hurwitz action and integral classification; no predecessor scientific replay." + }, + "playbook": "autonomous local run", + "environment": { + "python": "CPython 3.12.15", + "platform": "macOS arm64", + "dependencies": "standard library only" + }, + "claim_type": "scoped written proof with exact finite corroboration" +} diff --git a/research/rational-header-orbit-lattice/VERIFY.json b/research/rational-header-orbit-lattice/VERIFY.json new file mode 100644 index 0000000000..7f73d42648 --- /dev/null +++ b/research/rational-header-orbit-lattice/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "New rational header full products and normalized pairings; integer-lattice and intrinsic-residue invariance on literal walks; odd-denominator family with identical ambient reductions and pairwise distinct lattices; same-lattice distinct-residue example; five rejection controls; generated package-file hashes. All checks remain active under optimization." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "New rational header full products and normalized pairings; integer-lattice and intrinsic-residue invariance on literal walks; odd-denominator family with identical ambient reductions and pairwise distinct lattices; same-lattice distinct-residue example; five rejection controls; generated package-file hashes. All checks remain active under optimization." + } + ] +} diff --git a/research/rational-header-orbit-lattice/verify.py b/research/rational-header-orbit-lattice/verify.py new file mode 100644 index 0000000000..35db2a1acc --- /dev/null +++ b/research/rational-header-orbit-lattice/verify.py @@ -0,0 +1,238 @@ +#!/usr/bin/env python3 +"""Exact corroboration of rational header lattice invariants. Apache-2.0.""" + +from collections import Counter +from fractions import Fraction as F +from hashlib import sha256 +from itertools import combinations +import json +from pathlib import Path +import sys + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def identity(n): + require(1 <= n <= 8, "matrix dimension") + return [[F(i == j) for j in range(n)] for i in range(n)] + + +def transpose(a): + return [list(row) for row in zip(*a)] + + +def multiply(a, b): + require(1 <= len(a) <= 9 and len(a[0]) == len(b) <= 9, "matrix shape") + require(1 <= len(b[0]) <= 9, "matrix width") + return [[sum(x * y for x, y in zip(row, col)) + for col in zip(*b)] for row in a] + + +def inverse(a): + n = len(a) + aug = [list(row) + tail for row, tail in zip(a, identity(n))] + for j in range(n): + pivot = next((i for i in range(j, n) if aug[i][j]), None) + require(pivot is not None, "singular matrix") + aug[j], aug[pivot] = aug[pivot], aug[j] + scale = aug[j][j] + aug[j] = [x / scale for x in aug[j]] + for i in range(n): + if i != j: + scale = aug[i][j] + aug[i] = [x - scale * y for x, y in zip(aug[i], aug[j])] + return [row[n:] for row in aug] + + +def sign_form(n): + require(n in (2, 4, 6, 8), "even dimension") + return [[F((i > j) - (i < j)) for j in range(n)] for i in range(n)] + + +def canonical(n): + return identity(n) + [[F(-((-1) ** i)) for i in range(n)]] + + +def apply(a, vectors): + return transpose(multiply(a, transpose(vectors))) + + +def basis(vectors): + n = len(vectors[0]) + require(len(vectors) == n + 1, "saturated tuple") + return transpose(vectors[:n]) + + +def same_lattice(a, b): + ab = multiply(inverse(a), b) + ba = multiply(inverse(b), a) + return all(x.denominator == 1 for m in (ab, ba) for row in m for x in row) + + +def residues(vectors, lattice_basis): + coords = apply(inverse(lattice_basis), vectors) + require(all(x.denominator == 1 for row in coords for x in row), + "vector outside lattice") + return Counter(tuple(x.numerator % 2 for x in row) for row in coords) + + +def ambient_residues(vectors): + require(all(x.denominator % 2 for row in vectors for x in row), + "not 2-locally integral") + return Counter(tuple(x.numerator % 2 for x in row) for row in vectors) + + +def move(vectors, index, direction): + require(direction in (-1, 1) and 0 <= index < len(vectors) - 1, + "Hurwitz move") + result = [list(row) for row in vectors] + a, b = result[index:index + 2] + if direction == 1: + result[index:index + 2] = [b, [2 * y - x for x, y in zip(a, b)]] + else: + result[index:index + 2] = [[2 * x - y for x, y in zip(a, b)], a] + return result + + +def check_header(vectors, omega): + n = len(omega) + require(n in (2, 4, 6, 8) and len(vectors) == n + 1, "header shape") + rows = multiply(vectors, omega) + gram = multiply(rows, transpose(vectors)) + expected = [[F((i > j) - (i < j)) for j in range(n + 1)] + for i in range(n + 1)] + require(gram == expected, "normalized Gram") + product = identity(n) + for x, y in zip(vectors, rows): + unit = [[F(i == j) - 2 * x[i] * y[j] for j in range(n)] + for i in range(n)] + product = multiply(unit, product) + require(product == [[F(-(i == j)) for j in range(n)] for i in range(n)], + "full header product") + b = basis(vectors) + require(multiply(multiply(transpose(b), omega), b) == sign_form(n), + "intrinsic integral frame") + + +def rational_transvection(omega, vector, parameter): + row = multiply([vector], omega)[0] + n = len(vector) + return [[F(i == j) + parameter * vector[i] * row[j] for j in range(n)] + for i in range(n)] + + +def rational_walks(): + fixtures = steps = 0 + for n in (2, 4, 6, 8): + omega = sign_form(n) + for denominator in (3, 5, 7): + v = [F((i % 3) - 1) for i in range(n)] + g = rational_transvection(omega, v, F(1, denominator)) + start = apply(g, canonical(n)) + check_header(start, omega) + b = basis(start) + invariant = residues(start, b) + fixtures += 1 + current = start + for k in range(16): + index, direction = (3 * k + 1) % n, (-1 if k % 3 == 0 else 1) + following = move(current, index, direction) + check_header(following, omega) + require(same_lattice(b, basis(following)), "changed lattice") + require(residues(following, b) == invariant, "changed intrinsic residues") + require(move(following, index, -direction) == current, "inverse move") + current = following + steps += 1 + return {"rational_fixtures": fixtures, "literal_walk_steps": steps} + + +def odd_denominator_family(): + omega = sign_form(2) + family = [] + for m in range(1, 32, 2): + g = [[F(1, m), F(0)], [F(0), F(m)]] + vectors = apply(g, canonical(2)) + check_header(vectors, omega) + require(ambient_residues(vectors) == ambient_residues(canonical(2)), + "ambient reduction differs") + require(residues(vectors, g) == residues(canonical(2), identity(2)), + "intrinsic reference coordinates") + family.append((m, vectors, g)) + pairs = 0 + for (_, _, a), (_, _, b) in combinations(family, 2): + require(not same_lattice(a, b), "family lattices coincide") + require(a[0][0] * a[1][1] == b[0][0] * b[1][1] == 1, + "covolume control") + pairs += 1 + return {"odd_denominator_headers": len(family), "distinct_lattice_pairs": pairs} + + +def intrinsic_counterexample(): + omega = sign_form(4) + g = rational_transvection(omega, [F(1), F(0), F(1), F(0)], F(1, 3)) + start = apply(g, canonical(4)) + h = rational_transvection(omega, [F(1), F(0), F(0), F(0)], F(1)) + other = apply(multiply(g, h), canonical(4)) + check_header(start, omega) + check_header(other, omega) + require(same_lattice(basis(start), basis(other)), "same-lattice control") + require(residues(start, basis(start)) != residues(other, basis(start)), + "intrinsic residue obstruction absent") + return {"same_lattice_different_residue_pairs": 1} + + +def rejection_controls(): + caught = 0 + try: + inverse([[F(1), F(2)], [F(2), F(4)]]) + except ValueError: + caught += 1 + try: + ambient_residues([[F(1, 2), F(0)]]) + except ValueError: + caught += 1 + try: + residues([[F(1, 3), F(0)]], identity(2)) + except ValueError: + caught += 1 + try: + move(canonical(2), 2, 1) + except ValueError: + caught += 1 + altered = canonical(2) + altered[2][0] += 1 + try: + check_header(altered, sign_form(2)) + except ValueError: + caught += 1 + require(caught == 5, "rejection controls") + return {"rejection_controls": caught} + + +def source_hashes(): + root = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + result = {} + for name in names: + with (root / name).open("rb") as source: + raw = source.read(256 * 1024 + 1) + require(len(raw) <= 256 * 1024, "package file size") + result[name] = sha256(raw).hexdigest() + return result + + +def main(): + require(len(sys.argv) == 1, "no command-line arguments accepted") + result = {"status": "PASS_RATIONAL_HEADER_ORBIT_LATTICE", "no_new_kappa": True} + for counts in (rational_walks(), odd_denominator_family(), + intrinsic_counterexample(), rejection_controls()): + result.update(counts) + result["source_sha256"] = source_hashes() + print(json.dumps(result, sort_keys=True, indent=2)) + + +if __name__ == "__main__": + main()