Scoped negative result: asymmetric Hurwitz E8 copy cost is exactly 10

research/hurwitz-asymmetric-copy-floor/CLAIM.md

@@ -0,0 +1,54 @@
+# Sprint claim
+
+- Track: structural decoder research; OS assignment seed **49**
+  (`secrets.randbelow(100)`, drawn 2026-10-13 04:06 UTC).
+- Exact base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`.
+- Scope: the ten-line quaternionic E8 unit in #620, with arbitrary asymmetric
+  binary rank-one decoder totals and Theorem-C Gram-block copy charges.
+- Method: reconstruct the rational geometry; use all 32 orthogonal-pair
+  transversals to seek a weighted rank lower bound; exhaust all reader/source
+  supports and exhibit an attaining abstract decoder if the bound is sharp.
+- Expected deliverable: a scoped proof or counterexample, portable exact
+  standard-library verifier, deterministic receipt and negative controls.
+- Started: 2026-10-13 04:06 UTC. Expected finish: 04:46 UTC. Final ten minutes
+  reserved for verification and handoff; orientation ended before 04:14 UTC.
+
+Three candidates considered: (0) off-pattern E8 decoders beyond nine totals;
+(1) the Hurwitz asymmetric copy floor; (2) asymmetric P112 sink geometry.
+Seed 49 modulo 3 selects candidate 1. Unlike merely extending a search, the
+new method replaces #620's unfinished SAT query with a rank-averaging proof.
+P112 already has the #595 construction and #620 screens; #631 addresses
+star punctures, #669 asymmetric hypercube stars, #634 Lorentzian minrank and
+#682 tensor E8 depth. None covers this ten-line asymmetric copy floor.
+
+The selected certificate, current status, maintainer construction review and
+PR ledger were read. Accepted conditional kappa remains
+`51110230636731/31250000000000000` (#626 with #543); no frontier edit is planned.
+PR metadata checked through #686. GitHub reports no pinned issues, so no
+coordination issue was created; this is the local claim. #620 is partially
+reviewed in the ledger. Its current head is
+`e9cf03bbdf7094b5a83f6dbd1d74bfd77a05fb87`; the report explicitly calls the
+asymmetric case open despite the stronger wording in a script docstring.
+
+## Single result update — 2026-10-13 04:27 UTC
+
+Completed: the minimum abstract copy charge is exactly ten quaternionic
+rank units for every fitting asymmetric decoder, with no bound on the
+number of totals. A weighted rank argument over all 32 orthogonal-pair
+transversals proves the floor. The resulting optimistic Dfc deficit is
+negative for every positive stage count.
+
+The stopping rule was completion of the proof, all 1,048,576 support pairs,
+all 1,024 fitting matrices, the exact geometry and the rejection controls;
+all completed. Verification and handoff began at 04:21 UTC. Two Python
+versions, isolated optimized relocation, source/receipt corruption,
+selected-record integrity and staged whitespace checks pass. This is a
+scoped negative result, with no new kappa.
+
+[Reviewable result and reproduction instructions](https://github.com/CrocSwap/integer-mult-bounds/tree/research/decoder-seed49/research/hurwitz-asymmetric-copy-floor).
+
+Final metadata refresh: 520 open PRs through #700; main still at the exact
+base above. No pinned issue exists. #620's current head is unchanged from
+the initial check; its four relevant extension-ring source files match the
+retained base. New #697 changes source scheduling for a different complex
+E8 supplier, not the ten-line quaternionic decoder problem.

research/hurwitz-asymmetric-copy-floor/NOTICE.md

@@ -0,0 +1,49 @@
+# Attribution, license and source status
+
+Prepared by **Douglas R. Colkitt (@Mister-Meeseeks)**, with substantial
+**OpenAI Codex** assistance in research selection, proof development,
+implementation, checking and documentation. No human-only or independent
+human review is claimed. New files are under the repository's
+[Apache-2.0 license](../../LICENSE).
+
+The ten-line quaternionic E8 model, orthogonality observation, symmetric
+cost-ten result, exact asymmetric SAT formulation and open question come
+from **Joel Pulikkan / GamingPuzzled's
+[PR #620](https://github.com/CrocSwap/integer-mult-bounds/pull/620)**, prepared
+with Claude Opus 5.5 assistance. This contribution supplies the weighted
+transversal proof and a new standard-library exact implementation. It does
+not claim to have discovered that geometry or the cost-ten upper bound.
+
+The pairing-rank accounting is inherited from **DreamingOfClouds'
+#446/#595** work as used by #620; the conditional deficit screen uses the
+retained [format-limits-corrected](../format-limits-corrected/README.md)
+accounting. The Hamilton multiplication law and E8 root coordinates are
+standard. The implementation uses no copied predecessor routines.
+
+The main-branch base is 66849e1475c930fd7732b1a0067ffee7e1e95f60.
+The maintainer's retained #620 head was
+419c7374c3bf5f2eee28f08b1e50c1d57934081c, with a **partial** review.
+The current open head inspected for overlap was
+e9cf03bbdf7094b5a83f6dbd1d74bfd77a05fb87. Its four relevant extension-ring
+source files have the same Git blob IDs as the retained base files.
+Its later README adds an E6 correction and unrelated unit/dispatch work;
+the Hurwitz asymmetric case remains marked open. All consumed file bytes
+and base Git blob IDs are pinned in [SOURCES.json](SOURCES.json).
+
+The predecessor's hurwitz_exact.py docstring says costs below ten are
+UNSAT. Its accompanying REPORT.md explicitly says that run **did not
+finish**. We treat the case as open in that source and do not cite the
+docstring as evidence of solver success. The new proof and exact replay
+stand independently of any claimed SAT outcome.
+
+Concurrent work checked for overlap includes Zhao Chi / vectorsss' #631
+on star punctures, Sam Sung / the-missionary-company's #669 on asymmetric
+hypercube stars, Shike Chen's #634 on coding/Lorentzian families, and
+Scott Woolsey Biggart's #682 auditing Artus / artuskg's #647 tensor E8
+profile. These contributions concern different objects and are not
+dependencies. The selected #626/#543 construction and its full predecessor
+lineage retain their existing credit and assumptions.
+
+Before submission, metadata was refreshed through #700. Scott Woolsey
+Biggart's newer #697 directly reads sources in the complex #647 supplier;
+it does not address the quaternionic ten-line decoder considered here.

research/hurwitz-asymmetric-copy-floor/PROOF.md

@@ -0,0 +1,183 @@
+# The asymmetric copy floor for the ten Hurwitz E8 lines
+
+**Result.** In the scalar-total model specified below, the minimum copied
+information is **10 quaternionic rank units = 40 rational rank units**.
+This holds for every fitting decoder matrix separately, including every
+nonsymmetric completion and decompositions with arbitrarily many totals.
+It closes the particular asymmetric case left open in
+[#620's extension-ring report](../e8-decoder-floors-and-cold14-notes/s1-extension-rings/REPORT.md).
+It is a statement about that finite model, not a new supplier or a universal
+lower bound for integer multiplication.
+
+## 1. Geometry and the exact model
+
+Use the 240 E8 roots in doubled standard coordinates in Q^8:
+
+- all vectors with two nonzero coordinates, each equal to +2 or -2;
+- all vectors in {+1,-1}^8 with an even number of minus signs.
+
+Identify Q^8 with two copies of the rational Hamilton quaternions, and let
+1, i, j, k act by **left** multiplication on both blocks. The Q-span of these
+four translates of a root is a four-dimensional line over the quaternions.
+The roots partition into ten such Q-subspaces L_0,...,L_9, with 24 roots each.
+Our deterministic ordering has orthogonal pairs
+
+    (0,9), (1,8), (2,7), (3,6), (4,5).
+
+Each pair of distinct lines spans Q^8. Each line is orthogonal to precisely
+its mate. The verifier constructs this geometry from scratch using the
+Hamilton multiplication formula. Equality of the matrices 8 P_L, where P_L
+is the orthogonal projector onto L, identifies the lines; no floating rank
+test or tolerance is used.
+
+Let B be a 10 by 10 matrix over F2. Its fitting conditions are
+
+    B_tt = 1;
+    B_ts = 0 whenever t != s and L_t is not orthogonal to L_s.
+
+There is no restriction on either directed mate entry. In particular B need
+not be symmetric. Write an arbitrary finite scalar-total decomposition as
+
+    B = sum_j 1_{R_j} 1_{A_j}^T    over F2,
+
+where R_j is the reader set and A_j is the source set. Every binary rank-one
+term has this form. Both sets may be empty, terms may repeat, and no bound on
+the number of terms or on rank(B) is assumed.
+
+For a set S, concatenate the four-vector bases of its lines into a matrix
+V_S. Define the charge exactly as in #620's proposed Theorem-C relaxation:
+
+    c(R,A) = rank_Q(V_R V_A^T) / 4.
+
+The total charge is C = sum_j c(R_j,A_j). This is the proposed pairing-rank
+copy floor, not the F2 rank of the decoder rectangle. The factor four must
+be restored when using the repository's rational-rank accounting.
+
+For this geometry, direct linear algebra gives
+
+    c(R,A) = 0  if either set is empty, or R={t}, A={mate(t)};
+             1  otherwise, if either nonempty set is a singleton;
+             2  if both sets have at least two elements.
+
+Indeed two distinct lines span Q^8, so two sets of size at least two have a
+Gram block of rank eight. A singleton against a spanning set has rank four.
+Two quaternionic lines have a zero Gram block when orthogonal and an
+invertible four by four Gram block otherwise. The verifier checks all 3,025
+ordered pairs of singleton or two-line sets with two independent rational
+rank implementations. Every larger set has the same span as its first two
+lines; this is an exact reduction, not a sample of larger supports.
+
+## 2. A weighted transversal rank bound
+
+A transversal T chooses one line from each of the five orthogonal pairs.
+There are 32 transversals. Two different elements of T are nonorthogonal,
+so the fitting conditions force
+
+    B[T,T] = I_5.
+
+For a single rectangle R x A, its restriction to T x T has rank one exactly
+when R meets T and A meets T, and otherwise has rank zero. Denote this
+indicator by a_T(R,A). Rank subadditivity over F2 yields, for each T,
+
+    5 <= sum_j a_T(R_j,A_j).                         (1)
+
+For every rectangle the following local inequality holds:
+
+    (1/16) sum_T a_T(R,A) <= c(R,A).                 (2)
+
+There are only three cases:
+
+1. If c=0, an empty set makes all indicators zero. In the other zero-cost
+   case, a transversal cannot contain both orthogonal mates, so again all
+   indicators are zero.
+2. If c=1, at least one set is a singleton. Its one line belongs to exactly
+   16 transversals, so the sum of indicators is at most 16.
+3. If c=2, there are only 32 transversals, so the sum is at most 32.
+
+Multiply (1) by 1/16 and sum it over the 32 transversals. Then apply (2)
+term by term:
+
+    10 = (32/16)*5
+       <= sum_j (1/16) sum_T a_T(R_j,A_j)
+       <= sum_j c(R_j,A_j) = C.
+
+This is the complete lower-bound argument. In particular it does not
+assume that all totals have full rank, that B has minimum possible rank,
+that the decomposition is symmetric, or that the number of totals is ten.
+Zero-cost terms are allowed and are invisible to every inequality (1).
+No solver infeasibility claim is used.
+
+The same argument works for 2m distinct lines in quaternionic dimension
+two when their orthogonality graph is a perfect matching and the displayed
+charge formula holds: average over the 2^m transversals and obtain C >= 2m.
+Only the m=5 E8 instance is certified here.
+
+## 3. Sharpness, including nonsymmetric matrices
+
+For the symmetric completion with all directed mate entries equal to one,
+use one total R=A={t,mate(t)} per orthogonal pair. These five disjoint two
+by two all-one blocks satisfy the fitting pattern. Each costs two, so C=10.
+Its F2 rank is five, also the minimum possible by B[T,T]=I_5.
+
+More strongly, **every** fitting B has a cost-ten decomposition. For each
+row t, take R={t} and A equal to that row's nonzero positions. The set A is
+either {t} or {t,mate(t)}; the charge is one in both cases. These ten
+rectangles sum to B. Combining this with the lower bound proves that
+the minimum charge is ten for each of the 1,024 directed completions.
+
+There are 32 symmetric and 992 nonsymmetric completions. Their ranks
+5,6,7,8,9,10 occur with multiplicities 1,15,90,270,405,243 respectively.
+Each mate block has rank one only when both free entries are one, and
+rank two for the other three choices, giving these counts. The replay
+also enumerates and row-reduces all completions independently.
+
+This attains the abstract Gram-block charge. It does not assert that a
+complete physical supplier implements it without any additional expense.
+
+## 4. Optimistic complete-budget screen
+
+The [format accounting, axiom Dfc](../format-limits-corrected/README.md)
+and #620's rank-four scaling give, conditionally on using that same stage
+format, v=10, k=4 and cst=4C >= 40:
+
+    D/T = (s-1) v k - s cst
+        <= (s-1)*40 - s*40
+         = -40
+
+for every positive stage count s. Equivalently x_K=C/v >= 1, with equality
+already at the most favorable abstract copy cost. Even granting zero
+additional cost for helpers, source access, frame changes, restoration,
+and recursive work cannot make this accounting produce positive deficit.
+There is therefore no reason to implement a paid supplier for this
+particular mechanism before changing another premise. No assembly or
+other supplier can turn this negative local deficit into a positive one
+within the stated Dfc criterion.
+
+The finite receipt checks the arithmetic for s=1,...,32 as error controls;
+the displayed identity, not those examples, supplies the all-s argument.
+The abstract floor does not depend on the validity of this accounting
+interface. Its application to a multiplication bound does.
+
+## 5. Scope and verification
+
+The finite exhaustive domain is all 1,024 reader sets times all 1,024
+source sets, all 32 transversals, and all 1,024 fitting matrices. The
+certificate records every transversal and the exact weight 1/16. The
+verifier checks each local inequality (2), all principal identities (1),
+and attaining decompositions. Eight deliberately corrupted controls are
+rejected; nonsymmetric and zero-cost examples are accepted.
+
+The written rank argument extends the finite certificate to every finite
+number of totals. Enumeration alone is not presented as that proof.
+This is not a proof-assistant formalization.
+
+The result does not address arbitrary rational sub-line supports,
+matrix-valued or vector-linear totals, altered fitting patterns, punctured
+units, other Gaussian/Eisenstein units, changing the stage format, or
+physical realizations outside the declared pairing-rank model. In
+particular it is not a universal obstruction to quaternionic methods.
+It neither improves the selected kappa nor discharges the selected
+construction's compiler, hosting, precision, tape or analytic assumptions.
+
+Prepared by Douglas R. Colkitt with substantial OpenAI Codex assistance.
+See [NOTICE.md](NOTICE.md) for predecessor credit and source status.

research/hurwitz-asymmetric-copy-floor/README.md

@@ -0,0 +1,44 @@
+# Scoped negative result: asymmetric Hurwitz E8 copy floor
+
+Every scalar-total binary decoder on #620's ten quaternionic E8 lines has
+copy charge at least **10 quaternionic rank units = 40 rational rank units**.
+The bound is sharp for every fitting matrix, including all 992 nonsymmetric
+completions. Allowing arbitrary reader/source asymmetry and any number of
+totals therefore does not repair this unit's negative optimistic deficit.
+**No new kappa or physical supplier is claimed.**
+
+The new ingredient is a short weighted rank argument over the 32 choices
+of one line from each orthogonal pair. It resolves the asymmetric case
+explicitly left open by Joel Pulikkan / GamingPuzzled's #620 extension-ring
+report, using a method independent of its unfinished SAT run.
+
+From the repository root, with Python 3.10+ and no third-party dependencies:
+
+    python3 -B research/hurwitz-asymmetric-copy-floor/verify.py
+
+Expected final line:
+
+    PASS_HURWITZ_ASYMMETRIC_COPY_FLOOR: cost 10; 1048576 support pairs; 1024 decoders; 8 negative controls
+
+The command reconstructs all 240 roots and ten quaternionic lines, checks
+3,025 Gram blocks with two exact rational implementations, exhausts all
+reader/source supports and fitting matrices, runs the controls, and compares
+the complete result with [RESULTS.json](RESULTS.json). To regenerate a
+separate receipt, append --write /tmp/hurwitz-results.json.
+
+[PROOF.md](PROOF.md) specifies the model, proves the bound and sharpness, and
+prices the optimistic budget. Its all-total lower bound is a written rank
+argument; finite replay is not a formal proof of the multiplication theorem.
+[SOURCES.json](SOURCES.json) pins the inherited files, and
+[CLAIM.md](CLAIM.md) records seed 49, the bounded scope and overlap checks.
+The completed checks and their limits are in [VALIDATION.md](VALIDATION.md).
+
+Base: 66849e1475c930fd7732b1a0067ffee7e1e95f60.
+The accepted conditional kappa at this base remains
+51110230636731/31250000000000000 (#626 with #543). Its construction and
+selected pointer are untouched. Only this research directory is added.
+
+The source hashes check context; no predecessor code or SAT solver is
+imported. The package distinguishes #620's retained reviewed head from its
+later open head. See [NOTICE.md](NOTICE.md) for attribution, source status
+and substantial AI-assistance disclosure.