Research: Eisenstein nonlinear message copy floor 22b under explicit width pricing

research/eisenstein-message-copy-bound/CLAIM.md

@@ -0,0 +1,36 @@
+# Sprint claim
+
+- Track: structural decoder research. OS-random assignment seed: **41**.
+- Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`.
+- Started: 2026-10-13 05:47:37 UTC. Budget: 50 minutes; verification begins by 06:25 UTC. Expected finish: 06:37 UTC.
+- Object: the 40-line Eisenstein E8 (Witting) decoder geometry in GamingPuzzled PR #620, with arbitrary scalar binary totals and the source/reader pairing-rank copy charge.
+- Hypothesis: a weighted nonorthogonality-clique certificate gives a useful unconditional finite copy-cost lower bound without a full-rank-total assumption.
+- Method: independently reconstruct exact rational geometry; enumerate geometric flats and all maximum cliques; check a rational uniform weight over every flat pair. Stop after this finite domain, whether or not the bound helps.
+- Deliverable: one scoped research note with proof, source pins, portable exact checker, certificate and negative controls; no new kappa claim.
+
+## Selection and overlap
+
+Three candidates considered: (0) vector-valued full-E8 decoder factors; (1) mixed-port E8 extensions; (2) the Eisenstein extension geometry. Seed 41 modulo 3 selects candidate 2. Candidate 0 is close to #765 tensor-basis work; candidate 1 overlaps #715. Candidate 2 changes geometry from the Gaussian #738/#770 and Hurwitz #703/#785 certificates and answers an explicitly unresolved #620 copy-cost question. It does not repeat the predecessor CP-SAT search.
+
+GitHub reported no pinned issues, and the only open issue was #650 (Discussions). No separate reservation issue was opened. The local claim is used instead. Open PR metadata was checked through #796 (615 open PRs), including #620, #634, #703, #738, #761, #765 and #770. #620's reported Eisenstein lower bound is 9 and its feasible symmetric cost is 40; the search was not certified optimal. The ledger marks #620 partially reviewed and #446 unreviewed.
+
+At the exact starting base, the selected accepted conditional result was #626 with #543, kappa = 51110230636731/31250000000000000. Larger pending titles are not treated as accepted.
+
+## Evidence-driven pivot
+
+At the first experiment refresh, new PR #798 (Jonathan Lam, head `0aea3382e49abd9a59d3cb6676cdb26fd15b04e5`) already supplied the scalar Eisenstein bound and clique-method optimum. Our independent exact geometry replay had found all 772 flats, 2,880 maximum cliques and the uniform maximum-clique floor 280/13. That scalar investigation will not be submitted as new.
+
+The revised scope is fixed-support, deterministic, zero-error nonlinear messages and arbitrary finite bit widths on the same 40 Eisenstein lines. We will check an exact weighted demand bound by combining the #798 geometric inequality with the conditional-transcript argument of #785 (Hurwitz). The deliverable must explicitly price each message by its bit width times source/reader pairing rank, distinguish this model premise from a physical-circuit theorem, and test nonlinear and side-information boundary examples. No second pivot is planned.
+
+## Result update
+
+Completed 2026-10-13 06:16 UTC: submitted one research-note PR, [#814](https://github.com/CrocSwap/integer-mult-bounds/pull/814). Construction/proof commit: `f916c8b20060706bcc50a931a8138bab998aa0de`.
+
+- Result: fixed-support, deterministic, zero-error nonlinear messages on the 40 Eisenstein E8 lines obey C >= 22b for equal b-bit demands, with additive width-times-pairing-rank pricing. Unequal demands obey the weighted 11/20 sum bound and the maximum clique-demand bound. The physical pricing premise is explicit. No new kappa or supplier is claimed.
+- Complete geometric coverage: all 772 flats, 298,378 unordered flat pairs, 30,880 line extensions and 2,970 maximal cliques. Stopping rule: exhaust that finite domain and the declared message controls, then package one result. No incompleteness or timeout is presented as an impossibility theorem.
+- New evidence beyond #798/#785: the Eisenstein nonlinear and unequal-demand composition; 4,096 nonlinear inputs and 303,104 conditional transcripts; unequal-width and side-information boundary examples; exact reconstruction and a separate modular/Fraction arithmetic checker. The geometric scalar result and transcript method retain predecessor credit.
+- Validation: both implementations pass on CPython 3.14.4 and 3.12.13; 12 rejection controls, relocation, source/certificate tampering, output preservation, committed-byte equality and selected-record integrity pass. Structured autoreview reports no actionable findings. See VALIDATION.md for exact scope and commands.
+- Final pre-submission refresh: 625 open PRs through #812; #798 and #785 remain at their pinned heads. New #801 is a distinct format-ceiling/coordinate-total note. No pinned coordination issue exists; no reservation issue was opened. This is the single result update to the local claim.
+- Upstream advanced to `7ee02b7c96d85f22b38d28bd7ed49bb8c1aeb261` and selected #741 at kappa 1661202643272239/1000000000000000000. Its review was read. All pinned base geometry files remain byte-identical. The contribution retains its exact starting base and changes no selected or upstream file.
+
+Reproduce (Python 3.10+): `python3 -B research/eisenstein-message-copy-bound/verify.py`. Expected prefix: `PASS_EISENSTEIN_MESSAGE_BOUND`. Prepared by Michael Fischler (@shiftybitshiftr) with substantial OpenAI Codex assistance; Apache-2.0.

research/eisenstein-message-copy-bound/NOTICE.md

@@ -0,0 +1,39 @@
+# Attribution and license
+
+New material is contributed by Michael Fischler (@shiftybitshiftr) under
+the repository's Apache-2.0 license. OpenAI Codex substantially assisted
+with mathematical development, implementation, verification and writing.
+No independent human mathematical review is claimed.
+
+- **Jonathan Lam (@jonathanlam), PR798**, pinned at
+  `0aea3382e49abd9a59d3cb6676cdb26fd15b04e5`: the exact Eisenstein scalar
+  weighted-clique bound, geometric certificate and method ceiling. Its
+  `PROOF.md` is retained verbatim in `sources/pr798-PROOF.md`, including
+  its original attribution and AI disclosure. This submission independently
+  replays the geometric premise and does not claim priority for it.
+- **Alexander Templeton (@azide0x37), PR785**, pinned at
+  `83e78085ae9c110a34bff87e71387292d85e47c0`: conditional transcript
+  injectivity for nonlinear Hurwitz messages, explicit width pricing and
+  nonlinear examples. Its proof is retained verbatim in
+  `sources/pr785-PROOF.md`. The general argument is credited, not renamed
+  as a new technique.
+- **Joel Pulikkan / GamingPuzzled, PR620**: the Eisenstein E8 geometry,
+  extension-ring screen, original cost search and open question. The base
+  tree retains head `419c7374c3bf5f2eee28f08b1e50c1d57934081c`; inspected
+  open head is `e9cf03bbdf7094b5a83f6dbd1d74bfd77a05fb87`. The base ledger
+  marks this research partially reviewed.
+- **Douglas R. Colkitt (@Mister-Meeseeks), PR703**, and **Sagar Thakrar
+  (@thakrarsagar), PR738**: weighted-clique and geometric-closure methods
+  on Hurwitz and Gaussian geometries. No executable code is imported.
+- **DreamingOfClouds, PR446/PR595**: scalar pairing-rank interpretation
+  and conditional deficit accounting. PR446 is unreviewed in the base
+  ledger. Neither premise is promoted to a nonlinear physical theorem.
+- Earlier E8 and multiplication work by Jacob Sussman, Dylan Crow,
+  eumemic, icekylinx, Jeremy Kothe, Chafik Boukhalfa and the community
+  remains credited in the repository's contributor and construction records.
+  The base #626/#543 construction and all existing suppliers are untouched.
+
+The two retained proofs are Apache-2.0 material according to their own
+notices. Their bytes are pinned in SOURCES.json. The current contribution
+adds a composition with distinct message-model coverage, not a new
+headline exponent or a new scalar decoder optimum.

research/eisenstein-message-copy-bound/PROOF.md

@@ -0,0 +1,220 @@
+# Fixed-support nonlinear messages on the Eisenstein E8 lines
+
+This note extends Jonathan Lam's [PR798](https://github.com/CrocSwap/integer-mult-bounds/pull/798)
+scalar Eisenstein certificate to finite messages that may mix payload bits
+nonlinearly. It uses Alexander Templeton's conditional-transcript argument
+from [PR785](https://github.com/CrocSwap/integer-mult-bounds/pull/785), which
+treats a different, Hurwitz geometry. Neither method is claimed as new here.
+The new result is their composition on the Eisenstein geometry, including
+unequal demands, a concentration bound, and explicit nonlinear controls.
+
+## Statement and model
+
+Let the 40 ports be the Eisenstein E8 lines specified below. Port t holds an
+independent input X_t ranging freely over all b_t-bit strings, where b_t is a
+nonnegative integer. There are finitely many messages. Message j has fixed
+source and reader sets A_j,R_j, fixed integer width q_j >= 0, and value
+
+    Y_j = f_j((X_a)_(a in A_j)) in {0,1}^{q_j}.
+
+Every reader in R_j receives the same complete Y_j. Receiver t must recover
+X_t on **every** input tuple, using all its received messages and the full
+inputs of ports orthogonal to t. Functions and joint decoders may be
+nonlinear. Supports, widths and functions are fixed before the input is
+chosen. Granting full orthogonal inputs as free side information is an
+optimistic model of residual correction.
+
+For line sets R,A, let V_R,V_A be rational row bases of their spans and set
+
+    c(R,A) = rank_Q(V_R V_A^T)/2,
+    C = sum_j q_j c(R_j,A_j).
+
+**The charge is a premise of this message model:** every transmitted bit
+pays its support pairing rank, and charges add over messages. PR446's
+scalar copy-tree interpretation does not establish this pricing for
+arbitrary nonlinear physical circuits. Sharing physical work between bits
+more cheaply would be outside the result.
+
+Write Q for any clique of pairwise nonorthogonal lines, including singletons.
+The following bound holds for all finite widths and message counts:
+
+    C >= max( ceil(11 sum_t b_t / 20), max_Q sum_(t in Q) b_t ).       (1)
+
+In particular, if every port demands b bits, **C >= 22b Eisenstein rank
+units**, or **44b rational rank units**. This is a lower bound, not the
+optimum decoder cost. Direct messages give the abstract upper bound 40b.
+
+This model excludes adaptive/interactive supports, correlated inputs,
+errors, variable-length or average-cost messages, rational sub-line
+supports, and additional nonorthogonal side information. It includes
+fixed-support block-linear codes, coordinate mixing, arbitrary nonlinear
+encoding and joint decoding. It does not assert that every physical
+vector-valued circuit has the declared additive charge.
+
+## Exact geometric premise (predecessor work, replayed independently)
+
+Use the 240 doubled E8 roots: two nonzero coordinates in {2,-2}, or eight
+coordinates in {1,-1} with an even number of minus signs. Each has norm
+squared eight. The root order and four mutually orthogonal A2 pairs in the
+certificate match the `standard_e8`/`a2_rotation` object in Joel Pulikkan /
+GamingPuzzled's archived PR620. For a root a, its reflection is
+
+    s_a(x) = x - (x dot a) a / 4.
+
+Let J be the product of s_a s_b over the four pairs. The checker reconstructs
+J and verifies J^2+J+I=0, J^T J=I, and preservation of every root. The six-root
+orbits under ±J are exactly the roots in their rational two-dimensional
+spans. They define 40 K-lines for K=Q(omega), in K-dimension four. The
+certificate uses `rotation4 = 4J` to keep integer coordinates.
+
+Every line-generated space is J-invariant. So is the kernel of its pairing
+with another such space: orthogonality of J gives invariance of X_A^perp.
+Domain and kernel therefore have even rational dimension. Thus c is an
+integer, independent of the chosen row bases. Pairing rank need not equal
+either support's dimension.
+
+The scalar certificate in PR798 assigns weight 1/40 to each of the 40
+singletons, and 1/960 to each of the 2,880 seven-line nonorthogonal cliques.
+Call these weights lambda_Q. Its geometric inequality is
+
+    sum_Q lambda_Q [Q meets R and A] <= c(R,A).                      (2)
+
+Our implementation imports no predecessor executable code. It reconstructs
+the geometry and checks the following integer form of (2) on every pair
+of flats F,G:
+
+    24 |F intersect G| + H_7(F,G) <= 960 c(F,G).                     (3)
+
+Here H_7 counts seven-line cliques meeting both flats. The exact census is
+772 flats and 298,378 unordered pairs including empty supports. Symmetry
+covers both orders. All 30,880 one-line extensions remain in the flat list.
+Flats are generated from the empty span by adjoining a line and taking
+closure. Every flat has a line basis, so induction on basis size proves
+completeness. Closing arbitrary supports preserves their spans and pairing
+rank and can only increase clique-hit indicators. Hence (3) proves (2) for
+all support pairs, not just the enumerated flat masks.
+
+Every port lies in exactly 504 seven-line cliques, as checked literally for
+each of the 40 ports. Its total weight is therefore
+
+    sum_(Q contains t) lambda_Q = 1/40 + 504/960 = 11/20.            (4)
+
+The flat census by (K-rank, cardinality) is
+
+    (0,0):1; (1,1):40; (2,2):240; (2,4):90;
+    (3,5):360; (3,12):40; (4,40):1.
+
+The geometric inequality and its scalar application belong to PR798.
+This note does not claim a new optimality theorem for clique weights; that
+PR also gives a separate dual certificate, which is not needed here.
+
+## Conditional transcript proof for arbitrary widths
+
+Fix a nonorthogonal clique Q and **any** assignment of all inputs outside
+Q. Let J_Q be the messages whose source and reader sets both meet Q. Then
+
+    X_Q -> (Y_j)_(j in J_Q)
+
+is injective. If two assignments of X_Q had the same displayed transcript,
+each receiver in Q would have the same received messages: omitted messages
+have all sources outside Q, so their values were fixed. Each receiver's
+orthogonal side information is also outside Q, since distinct vertices of
+Q are nonorthogonal. Every deterministic receiver would return the same
+X_t in both assignments, contradicting their difference.
+
+Counting input tuples and possible fixed-width transcripts now gives
+
+    sum_(t in Q) b_t <= sum_j q_j [Q meets R_j and A_j].             (5)
+
+This is the argument from PR785, applied to general nonorthogonal cliques.
+It uses no linearity and holds for every finite width by proof, rather than
+by extrapolating the truth-table controls.
+
+Multiply (5) by lambda_Q, sum over Q, and apply (2) and (4):
+
+    (11/20) sum_t b_t
+      <= sum_j q_j sum_Q lambda_Q [Q meets R_j and A_j]
+      <= sum_j q_j c(R_j,A_j) = C.
+
+Integrality of q_j and c gives the ceiling in (1).
+
+For the other part of (1), if a clique meets both supports, choose a line
+from each intersection. They are either the same nonzero line or two
+nonorthogonal lines. The corresponding Gram block is nonzero. Evenness of
+pairing rank gives c(R,A) >= 1. Thus (5) directly yields
+C >= sum_(t in Q) b_t for every Q. Since b_t >= 0, the largest such demand
+sum occurs on an inclusion-maximal clique. The checker enumerates all
+2,970 maximal cliques, including the 90 of size four that are not contained
+in seven-line cliques.
+
+The concentration term matters: demands supported on a seven-line clique
+give C >= sum_t b_t, whereas (11/20) times their total alone is weaker.
+No claim is made that (1) is the strongest inequality for every demand vector.
+
+## Nonlinear examples and assumption controls
+
+The seed-41 control chooses an exact partition into ten orthogonal
+four-frames. For the first three frames, let z_0,z_1,z_2 be their input
+parities. Broadcast to those 12 ports the three-bit message
+
+    (z_0, z_1, z_2 XOR (z_0 AND z_1)).
+
+Receivers invert the last Boolean update. A receiver knows its other three
+frame inputs as orthogonal side information, so its frame parity recovers
+its own bit. The source and reader spans are full K-rank four, giving
+charge 3*4=12. Its mixed Boolean derivative is nonzero, so this encoding is
+nonlinear. The verifier exhausts all 4,096 inputs, all 12 receivers and
+303,104 conditional transcripts from 74 distinct projections of the
+weighted cliques. Adding 28 direct one-bit messages gives a cost-40 code
+on all 40 ports. This product extension is justified algebraically; the
+checker does not claim to enumerate 2^40 inputs. Independent repetitions
+give cost 40b for arbitrary equal b, without claiming optimality.
+
+A second control uses demands 0,1,2,3 on one orthogonal four-frame, sending
+each active bit-plane parity only to the ports with that bit. It checks all
+64 inputs and 192 transcripts, with charge six and bound four. Inactive
+and unequal-width ports are thus exercised explicitly.
+
+Two boundary examples show why the premises cannot be dropped:
+
+- Charging the three-bit nonlinear message just once would cost four,
+  below the certified integer bound seven for its 12 active inputs. It is
+  the per-bit charge, not a scalar copy theorem, that prevents this.
+- Seven pairwise nonorthogonal ports could all recover from one parity
+  if each were given the other six inputs for free. Their joint span has
+  K-rank four, giving charge four versus the clique demand seven. This
+  code is correct on all 128 inputs, but violates the side-information
+  premise. The verifier accepts its decoding and rejects its admission.
+
+Twelve rejection controls cover understated widths, undeclared sources,
+dropped message bits, constant messages, a missing nonlinear inverse,
+illegal side information, underpriced width, a non-clique, the rational
+rank conversion, excessive geometric weights, omitted singleton weights
+and negative demands. These test mathematical failure modes.
+
+## Optimistic cost screen and remaining obligations
+
+Only if the physical implementation obeys the message pricing and the
+inherited Dfc accounting may one substitute v=40, rational port rank 2b,
+and cst=2C. Then
+
+    D/T = (s-1)*80b - s*2C <= b*(36s-80).
+
+At three stages the upper deficit is **28b**, which is positive. This
+result does **not** exclude a three-stage supplier. The nonlinear cost-40b
+example has deficit -80b for every stage count and supplies no saving.
+Helpers, source access, encoding, decoding, frame changes, further copies,
+restoration and recursive children have all been granted zero additional
+expense in this optimistic screen. Any achieved supplier must price them;
+none is constructed here. The other supplier and outer assembly are not
+replaced or repriced, and no new kappa follows.
+
+This contribution changes no selected record or supplier. All-size realization,
+compiler, hosting, precision, tape and analytic obligations are inherited
+and unresolved by this finite result. The transcript argument is a written
+proof; the geometry has exhaustive finite premises. Neither is a
+proof-assistant formalization of integer multiplication.
+
+Prepared by Michael Fischler (@shiftybitshiftr) with substantial OpenAI Codex
+assistance in proof development, implementation, verification and writing.
+Apache-2.0. See SOURCES.json and NOTICE.md for predecessor pins and credit.