Prove exact two-channel P104 support 72 over F3 and Q (no new κ)

research/p104-two-channel-support/PORTS.json

@@ -0,0 +1 @@
+[11, 19, 35, 131, 259, 13, 21, 37, 69, 133, 261, 41, 73, 265, 49, 81, 145, 273, 161, 193, 321, 385, 14, 22, 38, 70, 134, 262, 26, 74, 138, 50, 146, 274, 98, 290, 194, 322, 386, 28, 44, 140, 268, 84, 148, 276, 100, 164, 292, 196, 324, 388, 56, 88, 152, 280, 168, 296, 200, 328, 392, 112, 176, 304, 208, 336, 400, 224, 352, 416, 508, 506, 502, 494, 478, 446, 382, 254, 505, 501, 493, 477, 445, 381, 253, 499, 475, 443, 379, 251, 487, 471, 439, 375, 247, 463, 431, 367, 239, 415, 351, 223, 319, 191]

research/p104-two-channel-support/PROOF.md

@@ -0,0 +1,154 @@
+# Exact second support weight of the P104 root code
+
+This contribution was produced by Nick Petalas. New material is Apache-2.0.
+
+## 1. Object and inherited input
+
+Use the ordered 104 odd-weight binary ports in `PORTS.json`, copied byte for
+byte from Matarener's [PR6166 coordinate fixture](https://github.com/CrocSwap/integer-mult-bounds/blob/096938513138868f0ed27639061f1a5054900f96/research/p104-carrier-code-uniqueness/e8/ports.json).
+Coordinates of a binary port are indexed 0 through 8. Its rational root is
+
+- `r(q) = e_i - e_j` for a weight-seven port with zeros `i < j`;
+- `r(q) = sum_{i in supp(q)} e_i - (1/3) sum_{i=0}^8 e_i` for a weight-three port.
+
+Let `M[a,b] = r(q_a) . r(q_b) / 2`. Although the roots use thirds, every
+entry of M is an integer or a half-integer. Reduce these entries modulo 3,
+using `1/2 = 2`. The clique indices
+
+```text
+T = (1, 5, 18, 20, 80, 85, 100, 103)
+```
+
+give `M[T,T] = I_8`, over both Q and F3. Write `G = M[T,:]` and let `C_Q`
+and `C_3` be its row spaces over Q and F3 respectively. These definitions
+specify the two codes independently of any word replay.
+
+The identification of `C_3`, up to coordinate signs, with every
+8-dimensional ternary P104 decoding code is Matarener's PR6166 theorem.
+Its code uniqueness, single-channel weight 49, and binary hyperplane port
+capacity 60 are cited dependencies, not newly checked results here. The
+predecessor's local-word lineage is Ali Romman PR5827 and DreamingOfClouds
+PR5907/6030, with their retained E8/native/controller contributors.
+
+## 2. Statement
+
+For a linear code C define its second generalized support weight by
+
+```text
+d_2(C) = min |supp(u) union supp(v)|,
+         over linearly independent u,v in C.
+```
+
+The finite certificate proves
+
+```text
+d_2(C_3) = d_2(C_Q) = 72.
+```
+
+There are exactly 704 minimizing two-dimensional subcodes of `C_3`.
+This count is a finite enumeration, not a classification up to symmetry.
+The value 72 and these minimizers are the new result. The mathematical
+notion of a generalized Hamming weight is standard.
+
+## 3. Exhaustive lower bound over F3
+
+Since G restricts to the identity on T, the map `c -> cG` is injective on
+`F3^8`. Every projective coefficient line has exactly one representative
+whose first nonzero entry is 1. Enumerating the eight trits gives
+
+```text
+(3^8 - 1)/2 = 3280 representatives.
+```
+
+Two distinct representatives are linearly independent. Every independent
+pair of codewords has the same support union as one of the unordered
+pairs of representatives. Thus all cases are covered by
+
+```text
+binomial(3280,2) = 5377560 pairs.
+```
+
+`verify.py` evaluates each representative at all 104 coordinates and stores
+its exact support as an integer bitset. For each distinct pair it computes
+`(support_a | support_b).bit_count()`. The complete histogram, recomputed
+on every replay and compared to `RESULT.json`, has minimum 72.
+
+An F3 plane has four projective lines and six unordered pairs. Every pair
+in that plane spans it and has the same support union. The replay forms
+the four canonical representatives of every minimizing plane as
+`a, b, a+b, a+2b`, then groups their sorted tuples. It obtains 4224 pairs
+in 704 groups and checks that every group occurs exactly six times.
+The total number of planes covered by the pair census is 5377560/6 = 896260.
+No support test is sampled or inferred from the minimum-weight distribution.
+
+The 832 Gram entries used to construct G are checked by two expressions:
+the intersection-size formula and explicit nine-coordinate rational roots.
+This is a construction check for this certificate, not a replay of the
+predecessor's uniqueness proof or its word counts.
+
+## 4. Rational lower bound and sharp witness
+
+Suppose a two-dimensional subspace of `C_Q` is supported on a set S of
+fewer than 72 coordinates. Its coefficient plane is in the kernel of
+`G[:, outside(S)]^T`, so that rational matrix has rank at most six.
+All its denominators are powers of two. Reduction modulo 3 cannot raise
+its rank, since a nonzero reduced minor has a nonzero rational determinant.
+Its F3 kernel therefore has dimension at least two. Injectivity of the
+ternary coefficient map gives a two-dimensional subcode of `C_3` supported
+inside S, contradicting section 3. Hence `d_2(C_Q) >= 72`.
+
+In the ordered eight-row basis G, take
+
+```text
+a = (0,0,0,1,0,0,0,0)
+b = (0,0,0,0,1,1,1,0).
+```
+
+Their coefficient minor on positions 3 and 4 is the identity. Their rational
+codewords have individual weights 49 and 71, and their union has weight 72.
+Over F3 their individual weights are 49 and 69 and their union is the same
+72-coordinate set. The checker calculates every rational and ternary entry;
+`RESULT.json` records the union as binary port values. This proves sharpness
+in both fields. The rational assertion follows from exact arithmetic and
+the rank argument, rather than identifying rational zeros with modular zeros.
+
+A useful transfer also applies to a 3-integral systematic generator H of an
+8-dimensional rational code, if its reduction is coordinate-sign-equivalent
+to `C_3`. The same minor argument proves `d_2(row_Q H) >= 72`. This is a
+conditional implication; it does not classify rational decoding codes.
+
+## 5. Scoped common-frame consequence
+
+Assume a rational code has the reduction specified in the preceding
+paragraph. If two independent channel rows in that code are both acquired
+from ports in one binary frame F, then F contains their support union.
+It therefore contains at least 72 ports. The cited PR6166 hyperplane
+capacity is 60. Every proper subspace of `F2^9` is contained in a hyperplane,
+so `F = F2^9`.
+
+Dually, suppose two independent receiver-coefficient columns are in a code
+with the same support bound. If every receiver of either column must accept
+its delivery in one common landing frame B, and partner l's legal frame is
+inside `q_l^perp`, then
+
+```text
+B subset intersection_{l in union of receiver supports} q_l^perp = {0}.
+```
+
+The equality holds because those at least 72 binary ports span `F2^9` by
+the same capacity bound. Thus a common landing frame must be ZERO.
+
+This is a conditional obstruction to common-frame synchronization. It does
+not say that two independently scheduled channels each require FULL-to-ZERO
+descent. With distinct acquisition or delivery cuts, a nine-dimensional
+partner code, extra canceling carrier directions, or public relays, the
+common-frame hypotheses can fail. No additional paid cost is inferred
+without an actual trajectory and complete invoice.
+
+## 6. Verification boundary
+
+The exhaustive claim is about the specified 104-coordinate codes. No
+selected word, native operator, compiler, outer supplier, rounded multiplier,
+or predecessor uniqueness certificate is replayed. The common-frame
+consequence uses the named predecessor capacity and the stated code/support
+hypotheses. Human and formal proof-kernel review are unclaimed.

research/p104-two-channel-support/README.md

@@ -0,0 +1,100 @@
+# Two independent P104 root-code channels need 72 ports
+
+The exact second generalized support weight of the specified P104 root code
+is **72**, both over F3 and over Q. There are **704** minimizing ternary
+two-dimensional subcodes. This is a finite certificate with a scoped proof;
+no new kappa or cheaper physical word is claimed.
+
+Matarener's [PR6166](https://github.com/CrocSwap/integer-mult-bounds/pull/6166)
+identifies the ternary code and proves its single-channel minimum 49. The
+new quantity is the minimum union of supports of two independent channels.
+An explicit independent pair attains 72. The full 5,377,560 projective-pair
+census proves the lower bound. [PROOF.md](PROOF.md) gives the coverage
+argument and lifts the result to rational coefficients by a minor argument.
+The predecessor theorem is cited, not independently validated here.
+
+The shared-frame consequence is narrow but useful. With PR6166's cited
+binary hyperplane capacity 60, a common acquisition frame for two such
+independent channels must be FULL. A common landing frame for two independent
+receiver columns satisfying the same code hypothesis must be ZERO. These
+are constraints on synchronized sharing; they do not exclude separately
+scheduled carriers, relays or larger partner codes.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/p104-two-channel-support/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p104-two-channel-support
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p104-two-channel-support --check-source-history
+```
+
+Use any CPython 3.12 interpreter in place of the local path. Both registered
+normal and optimized commands must print
+`PASS_P104_TWO_CHANNEL_SUPPORT d2=72 pairs=5377560 minimizing_subcodes=704`.
+The runner must print `PASS_REGISTERED_RESEARCH_PACKAGE`.
+
+Normal replay only reads files. The generated [RESULT.json](RESULT.json)
+binds all seven proof/input/metadata files by SHA256 and records the complete
+support histogram, census counts and rational/ternary witness. To regenerate
+it explicitly, pass `--emit-receipt /path/to/RESULT.json`. A changed receipt
+is rejected, including under optimized Python.
+
+## Source and scope
+
+`PORTS.json` retains the exact coordinate bytes from PR6166 at
+`096938513138868f0ed27639061f1a5054900f96`. Its URL, SHA256 and source role are
+in [SOURCES.json](SOURCES.json). That open PR head is external to this
+publication's ancestry; the generic source-history check covers the canonical
+catalogue and selected record, not the external head. The direct verifier
+checks the retained coordinate bytes against their recorded hash and derives
+all code entries locally. No predecessor executable or proof is copied.
+
+Base `3f0152a32eeebac0df11946dbd50cabe5a7f7839`, priority revision 8.
+The selected source-binding baseline passed. The selected conditional
+κ = 0.003125804 is unchanged. Main, merged-PR, live open-PR and Discussion
+searches found no same-question result; these bounded searches do not prove
+novelty. The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19267579)
+states the ternary target. The same certificate also supplies the rational
+lift, without another search.
+
+All loops have fixed bounds: 104 ports, nine root coordinates, eight
+coefficient coordinates, 6561 coefficient tuples, 3280 projective words and
+5,377,560 pairs. Minimizer storage is at most the finite pair count and in
+this certificate holds 4224 pairs. Each function is under 60 lines. Checks
+use explicit exceptions and remain active under `-O`. CPython and Fraction
+allocate dynamically; this is a documented Power of Ten rule 3 deviation
+bounded by these fixed census sizes and input dimensions. There is no
+recursion, network, subprocess, dynamic code execution or normal replay write.
+Warning-strict normal and optimized replay provide the recurring diagnostics.
+
+Limitations are mathematical as well as practical. This is not a theorem
+about arbitrary nine-dimensional decoding codes or asynchronous relay
+programs. Complete native, caller, restoration, stock/precision, compiler and
+outer costs remain open and are not assigned zero. No Lean, selected-native
+or complete multiplication replay is run. Independent human and formal
+proof-kernel review are unclaimed.
+
+## Open next questions
+
+- Can an asynchronous relay use distinct acquisition and delivery cuts to
+  avoid the common-frame constraint and improve a complete invoice? Start
+  with two explicit independent channel rows and pay for every transition
+  and restoration in an actual caller. That caller and its invoice are missing.
+- What joint-support bound holds for a specified nine-dimensional decoding
+  code outside the minimal-code reduction? First exhibit the code and two
+  delivered channels. Its decoding and physical delivery contracts remain
+  blockers. No larger-code census is included here.
+
+[TASK.json](TASK.json) records the same questions and scope change.
+
+## Credit
+
+This contribution was produced by Nick Petalas. Credit Matarener PR6166 for
+the decoding-code identification, source coordinates, single-channel result
+and cited frame capacity; Ali Romman PR5827 and DreamingOfClouds PR5907/6030
+for the retained local-word lineage; and their E8, native, helper, controller
+and compiler predecessors. Generalized Hamming weights and rank reduction
+by minors are standard. The new contribution is this exact joint-support
+certificate, rational lift and scoped common-frame consequence. Apache-2.0.