Classify rational saturated-header Hurwitz orbits (no κ)

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.

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.

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."
+  }
+}