Bound nonlinear Eisenstein savings by coordinate restrictions (no κ)

research/eisenstein-nonlinear-restriction/PROOF.md

@@ -0,0 +1,127 @@
+# Coordinate faces bound the possible nonlinear saving
+
+This contribution is produced by Nick Petalas. New work is Apache-2.0.
+
+## Model and credited premise
+
+Use Michael Fischler's [PR814 fixed-support nonlinear model](../eisenstein-message-copy-bound/PROOF.md).
+There are forty Eisenstein E8 ports. Port t holds b_t independent binary
+coordinates. Put N=sum_t b_t. Each fixed-width message Y_j=f_j(X_Aj) has
+q_j bits, fixed source support A_j and fixed reader support R_j. Receiver t
+recovers all its input bits on every input, using its received messages and
+the inputs of ports orthogonal to t. Decoders need not be linear.
+
+The abstract charge is C=sum_j q_j c(R_j,A_j), where c is half the rational
+pairing rank of the two line-generated subspaces. Charges add per bit.
+This is a model premise, not a proved physical implementation price.
+
+We invoke Jose Manuel's [PR2017 fixed-support block-linear corollary](../eisenstein-reduction-copy-floor/README.md#fixed-support-block-linear-corollary).
+If all messages are binary linear in the independent input coordinates,
+then C is at least the total demand. This includes arbitrary unequal
+demands, zero demands, arbitrary fixed supports, and nonlinear decoders.
+An affine message has the same conclusion after its known constant is
+subtracted at each reader. The good-reduction and Schur-rank proof are
+credited premises; this package does not re-prove or replay them.
+
+## The new restriction lemma
+
+Fix a set S of h individual input coordinates to one specified assignment a.
+Suppose that, on this coordinate face, every output bit of every message
+is affine in the N-h unfixed coordinates. Then
+
+    C >= N-h.                                                    (1)
+
+Proof. The unfixed coordinates still range independently over their full
+binary product. Each port now demands exactly its own unfixed coordinates.
+Every old decoder remains correct on the face. Its fixed coordinates are
+known constants; its unfixed side information still comes only from
+orthogonal ports. Subtract the known affine constants of the messages.
+This gives a fixed-support block-linear protocol for total demand N-h.
+It may retain the original supports and widths. Apply the credited
+PR2017 theorem directly to obtain (1). Alternatively, remove inactive
+sources and readers. Restricting the bilinear pairing to smaller spans
+cannot increase its rank, so that version has charge at most the original
+C and gives the same inequality. This proves the lemma.
+
+Let h_* be the minimum number of coordinates fixed on any such affine
+face, allowing arbitrary specified zero or one values. A face always
+exists, since fixing all N coordinates makes every message constant. Thus
+
+    C >= N-h_*.                                                  (2)
+
+The face is a restriction used to prove an exact-code lower bound.
+It is not an input-dependent free routing header. No execution is given
+extra information about a random input. Arbitrary affine subspaces that
+couple different ports are excluded: they need not preserve the product
+of independent per-port demands required by the credited theorem.
+
+## An exact monomial hitting-set corollary
+
+Represent each transmitted bit by its unique squarefree algebraic normal
+form over F2, in all N individual input coordinates. Form a hypergraph E
+whose edges are all monomial supports of degree at least two appearing
+in at least one output bit. Let tau(E) be its minimum vertex-cover size.
+Here a vertex cover meets every edge, and the empty hypergraph has tau=0.
+
+Setting every variable in a cover S to zero removes every nonlinear
+monomial. All surviving terms are affine. Conversely, after fixing S to
+zero, every monomial disjoint from S survives unchanged, and distinct
+surviving monomials cannot cancel. Hence zero fixing makes all messages
+affine exactly when S meets every edge. The exact minimum zero-fixing
+number is tau(E). In particular h_*<=tau(E), and
+
+    C >= N-tau(E).                                               (3)
+
+For quadratic messages, E is the ordinary interaction graph across all
+output bits, so its vertex-cover number supplies the bound.
+The minimum is not a claim about computing vertex cover in polynomial time.
+The executable searches only the bounded domains stated in its README.
+
+Nonzero faces can improve (3). For one output with ANF
+
+    x0*x1 + x0*x2 + x1*x2 + x0*x1*x2,
+
+the zero-face cover number is two, since all three edges of a triangle
+occur. Fixing x2=1 instead leaves x0+x1, so h_*=1. The function is nonlinear
+on the full cube, making this minimum exact. This distinguishes (2) from
+the zero-face corollary.
+
+## Meaning for a cheaper nonlinear proposal
+
+Any proposed exact code with C<=N-d must satisfy h_*>=d and tau(E)>=d.
+For equal b-bit demands, N=40b. A proposed C<=31b therefore needs both
+parameters at least 9b. The number 31 is a conditional target, not an
+attained charge. It is motivated by Maximooch's historical PR1794 format
+screen, cited through PR2017; that screen is not replayed or assumed by
+the restriction proof. The inherited unrestricted nonlinear floor of 22b remains
+separate; combining it with (2) gives max(22b,40b-h_*).
+
+These inequalities do not prove a nonlinear code with C<N, or sharpness
+of (1) for any positive h. A nonlinear encoder can have no cost advantage.
+The new fixture illustrates this: on an orthogonal four-frame, send each
+of the first three input bits directly to its owner and send
+x3+x0*x1*x2 to the fourth owner. The fourth owner knows the first three
+inputs as permitted orthogonal side information. Each message has pairing
+price one. Add the other thirty-six direct singleton messages. The full
+code costs forty, has h_*=tau=1, and the new necessary floor is thirty-nine.
+The verifier checks the sixteen frame inputs and the separate direct-bit
+components; the written product decomposition covers all forty inputs.
+
+## Limits and predecessor credit
+
+The result requires deterministic zero-error decoding, independent product
+inputs, fixed supports and widths, permitted orthogonal side information,
+and additive per-bit pairing prices. It does not cover errors, correlated
+demands, adaptive or interactive messages, a private free header, or shared
+physical pricing. It supplies no native circuit, supplier admission, new
+kappa, or complete multiplication theorem. The all-width statement is an
+informal proof with finite corroboration; formal-kernel and independent
+human review are unclaimed.
+
+Credit Michael Fischler for the nonlinear model, Jose Manuel for the
+linear floor, Jonathan Lam and Joel Pulikkan / GamingPuzzled for the
+geometry and original pairing-cost model, and ywz65 for the distinct
+adaptive-affine public-broadcast theorem in PR2607. That theorem requires
+affine queries at every adaptive node; here the original fixed messages
+may be genuinely nonlinear. The new step is the coordinate-face
+restriction and the resulting quantified nonlinear-dependence obstruction.

research/eisenstein-nonlinear-restriction/README.md

@@ -0,0 +1,145 @@
+# A coordinate-restriction obstruction for nonlinear Eisenstein messages
+
+This contribution is produced by Nick Petalas. New work is Apache-2.0.
+
+For the fixed-support nonlinear Eisenstein message model, let N be the
+total independent input demand. If fixing h individual input coordinates
+to specified constants makes every transmitted bit affine, then the
+original additive pairing charge satisfies **C >= N-h**. Consequently
+
+    C >= N-h_* >= N-tau(E),
+
+where h_* is the minimum fixing over all coordinate faces and tau(E) is
+the minimum hitting set of the nonlinear monomial supports across every
+output bit's algebraic normal form. For zero-valued fixings the minimum
+is exactly tau(E). Nonzero faces can give a strictly stronger bound.
+
+This is a scoped proof with finite corroboration. The new step is the
+model-preserving restriction of a genuinely nonlinear message map to
+Jose Manuel's credited block-linear theorem. It does not settle the
+unrestricted nonlinear optimum or give a new kappa.
+
+## Result and relevance
+
+[PROOF.md](PROOF.md) gives the all-width argument and the exact monomial
+criterion. A coordinate restriction leaves the unfixed bits independent
+within and across ports. The old receivers still recover them. Known
+affine constants can be subtracted, so the retained linear floor applies.
+Removing inactive supports can only decrease their pairing ranks.
+
+A putative saving d below N therefore requires h_*>=d and tau(E)>=d.
+For equal b-bit demands, a proposed charge at most 31b requires at least
+9b fixed bits to linearize the message map, under either parameter.
+These are necessary conditions, with no assertion that such a cheaper
+nonlinear code exists. The inherited unrestricted nonlinear floor 22b
+combines with this result as max(22b,40b-h_*).
+
+The new exact fixture uses ports 0,28,29,39, an orthogonal four-frame in
+the pinned geometry. Its fourth message is x3+x0*x1*x2, and the first
+three messages are their owners' input bits. The fourth receiver has
+the other three frame inputs as permitted side information. Thirty-six
+direct messages complete the code. Each of its forty message prices is
+one, and h_*=tau=1. The new lower bound is 39; the exhibited code costs
+40. This is no claim of an attaining cost-39 code.
+
+The strict-face example is x0*x1+x0*x2+x1*x2+x0*x1*x2. Its zero-fixing
+minimum is two, while fixing x2=1 leaves x0+x1, so h_*=1.
+
+## Reproduce
+
+From the repository root, using Python 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/eisenstein-nonlinear-restriction
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/eisenstein-nonlinear-restriction/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/eisenstein-nonlinear-restriction/verify.py
+```
+
+Another Python 3.12 executable can replace the local interpreter path.
+Each registered command has a 120-second limit. Expected final status:
+
+```text
+PASS_EISENSTEIN_NONLINEAR_RESTRICTION {"faces":18086,"maps":366,"new_fixture_lower_bound":39,"rejections":9,"semantic_controls":3}
+```
+
+The checker enumerates every Boolean function through three variables
+and 88 deterministic multibit maps in four and five variables, totaling
+366 maps, 18,086 coordinate faces and 164,114 point/output substitution
+checks. An independent truth-value affine oracle corroborates symbolic
+substitution, including cancellations on nonzero faces. Exact minimizers
+are compared with exhaustive face and zero-face scans.
+
+The code fixture checks sixteen frame inputs, 64 receiver observations,
+and 72 separate direct-bit component cases, together with all forty
+actual rational pairing prices. Its product argument is written in the
+proof; the checker does not enumerate 2^40 full inputs. Nine rejected
+inputs/contracts and three semantic controls cover malformed ANFs,
+search bounds, missing side information, retained nonlinear terms,
+cancellation and a deleted cubic term. Explicit checks remain enabled
+with Python optimization.
+
+Default replay writes no files. To generate a receipt bound to the new
+proof/code and declared source hashes, add `--output NEW_PATH` to a direct
+command. Use a scratch path outside the checkout. Existing outputs are
+never replaced. No receipt is handwritten or committed.
+
+`restrictions.py` accepts at most forty variables, forty outputs and 256
+monomials per output. The exact zero-cut search accepts at most twelve
+variables, and the exact arbitrary-face search at most eight. The census
+uses at most five. These executable limits do not limit the written proof.
+The code has no recursive path; every search is finite. Managed Python
+allocations and the fixed rejection-control callbacks are documented
+Power of Ten deviations from static allocation and direct-only calls.
+The input and iteration caps bound their lifetimes and target sets.
+Warning-strict ordinary/optimized replay supplies the available runtime
+diagnostics; no new static-analysis dependency is introduced.
+
+## Scope, provenance and credit
+
+[SOURCES.json](SOURCES.json) pins base
+624de9dc66858af0945e5f8a0942488d62280d43, priority revision 7. The original
+card was `complex-rank-shape-decoder`. [TASK.json](TASK.json) records the
+change to a nonlinear interface obstruction, outside the already closed
+linear search. The selected metadata orientation passed. The card's
+predecessor scientific replay was skipped because this assignment asks
+for original work and excludes predecessor re-verification.
+
+Credit Michael Fischler / shiftybitshiftr [#814](https://github.com/CrocSwap/integer-mult-bounds/pull/814)
+for the nonlinear fixed-support model and its 22b lower bound, Jose Manuel /
+jmbarrancoml [#2017](https://github.com/CrocSwap/integer-mult-bounds/pull/2017)
+for good reduction and the block-linear total-demand floor, and Jonathan
+Lam [#798](https://github.com/CrocSwap/integer-mult-bounds/pull/798) following
+Joel Pulikkan / GamingPuzzled for the geometry and pairing-cost model.
+Maximooch's historical #1794 format screen motivates the example target
+31b, without supplying a current selected-frontier comparison here.
+ywz65's [#2607](https://github.com/CrocSwap/integer-mult-bounds/pull/2607)
+is the distinct adaptive public affine-query extension. No predecessor
+verifier is imported, executed or independently certified here. Geometry
+data is read unchanged to price only the new fixture.
+
+The overlap check covered live PR lists, this account's past-day work,
+recent handoffs, main-package searches and the cached task search.
+The latter reports 410 open PR records at 23:02:36 UTC and 3,919 Discussion
+records at 23:03:21 UTC on October 22. The sparse local-note search was
+incomplete, so a separate Git-tree source search was used. Closed-PR
+metadata in the cache was older; live merged searches supplemented it.
+These are bounded searches, not proof of novelty.
+
+The proof requires exact deterministic decoding, independent product
+inputs, fixed supports/widths, orthogonal side information and additive
+per-bit prices. Coupled cross-port affine restrictions, correlated inputs,
+errors, adaptive/private routing and shared physical tariffs are excluded.
+No physical supplier, compiler, hosting, precision or multiplication-theorem
+obligation is discharged. Independent human and formal proof-kernel review
+are unclaimed. The selected frontier is unchanged.
+
+## Open next questions
+
+- Can an exact genuinely nonlinear code have C<N under the unchanged
+  supports and prices? Start with a small complete code and enumerate
+  receiver observations; compute an affine-face witness before enlarging
+  it. No attaining nonlinear saving is supplied here.
+- Can within-port affine changes of input coordinates reveal a larger
+  product restriction? Start with one nonlinear block map, preserving
+  independence across ports. A proved invariant beyond coordinate faces
+  and its bounded search remain open.

research/eisenstein-nonlinear-restriction/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/eisenstein-message-copy-bound/PROOF.md",
+      "usage": "input",
+      "git_blob": "86d6e25ed60488646c0316a2c930e1f9e3ade99a",
+      "sha256": "dd8c7890d661ae87167d038d12356845470a2822733c45bd9ab4c9208e381311"
+    },
+    {
+      "path": "research/eisenstein-reduction-copy-floor/README.md",
+      "usage": "input",
+      "git_blob": "ebf030c2592de812a6189722b5bf7bdf854bc4ae",
+      "sha256": "f3f243524fd1ddc0fc893b144994ce184fee8fd8e7e49d544281863559f8c1de"
+    },
+    {
+      "path": "research/eisenstein-message-copy-bound/certificate.json",
+      "usage": "input",
+      "git_blob": "db72bdcfd825ba5d1fc94f24ec4beecfc1e0474c",
+      "sha256": "37b041ad7a9c84961e6468cf59ec97f2f80ae68a2fc2670eab931b9ad131ad4e"
+    }
+  ]
+}