Bound every BW16 nonorthogonality clique by 126 (no κ)

research/bw16-global-clique-126/PROOF.md

@@ -0,0 +1,130 @@
+# A global upper bound of 126
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+## The finite object
+
+Coordinates are indexed by x in F2^4, represented by the integers 0 through
+15 in little-endian binary. Use ordinary real inner products. The vertex set
+V consists of the following canonical norm-eight lines, with the first
+nonzero coordinate positive:
+
+1. The 240 lines 2(e_i + s e_j), i<j and s in {+1,-1}.
+2. On each affine hyperplane H={x:a dot x=b}, a!=0, the 64 lines with entries
+   +1 or -1 on H, zero elsewhere, and an even number of negative entries.
+
+The second family has 30 supports, each of size eight. Quotienting the 128
+even sign patterns by overall sign gives 64 lines per support, so |V|=2160.
+This is the norm-eight BW16 shell in DaysSky's PR895 normalization. The shell
+setting and its two-shape description are credited premises. They can also
+be seen directly in RM(1,4)+2 RM(3,4)+4 Z^16: a norm-eight low residue has
+weight zero or eight, and RM(3,4) is the even-weight code.
+
+A clique means a subset of V with every two distinct lines nonorthogonal.
+
+## Lemma 1: the D16 equality case
+
+Let D be the first 240-line family. A clique in D has size at most 15. Every
+15-line clique has the form
+
+    S(i,s) = { 2(e_i+s_j e_j) : j!=i },  s_j in {+1,-1},
+
+up to independent overall signs of the representatives.
+
+To prove this, replace each line by its two-element coordinate support.
+Disjoint supports give orthogonal lines. Two distinct lines on the same
+support are orthogonal too, so a clique has at most one line per support.
+A pairwise intersecting family of two-element subsets either has a common
+point, or is contained in a triangle. Indeed, take {a,b} and {a,c}. Any edge
+avoiding a must be {b,c}; if that edge is present, all edges lie in the same
+triangle. A common-point family on sixteen coordinates has at most fifteen
+edges, and equality uses every other coordinate. This proves the lemma.
+
+## Lemma 2: a full star permits at most thirty lines in all
+
+If a clique C in V contains S(i,s), then |C|<=30. The bound is attained.
+
+Lemma 1 gives |C intersect D|<=15. Now consider an odd line v in C on an
+affine hyperplane H. If i is outside H, choose j distinct from i outside H;
+there are seven such choices. Both coordinates of 2(e_i+s_j e_j) vanish
+in v, contradicting compatibility. Thus i is in H.
+
+Choose the sign of v so v_i=1. For each j in H other than i, the inner
+product with the star line is 2(1+s_j v_j). This is nonzero exactly when
+v_j=s_j. Hence a fixed H permits at most one odd line. There are precisely
+fifteen affine hyperplanes containing i, one for each nonzero a with
+b=a dot i. Therefore |C|<=15+15=30. Some prescribed sign patterns fail the
+even-parity requirement; this can only reduce the count.
+
+For attainment take i=0, all s_j=+1, and the fifteen all-positive indicator
+vectors of the hyperplanes through zero. Distinct hyperplanes intersect in
+four coordinates, so these odd lines are mutually nonorthogonal. Each also
+meets every star line nonorthogonally. The resulting clique has thirty lines.
+
+## The exact nine-chart certificate
+
+List the six quadratic monomials in this order:
+
+    x0*x1, x0*x2, x0*x3, x1*x2, x1*x3, x2*x3.
+
+An integer c from 0 through 63 encodes their binary coefficients. Put
+q_c(x)=sum_{i<j} c_ij*x_i*x_j in F2 and define the integer matrix
+
+    H_c[x,b] = (-1)^(q_c(x)+b dot x),  x,b in F2^4.
+    U_c = H_c/4.
+
+Use exactly these eight forms:
+
+    0, 57, 53, 46, 35, 28, 18, 15.
+
+Together with the identity chart they satisfy the following finite facts:
+
+- H_c H_c^T=16 I for each of the eight matrices, so U_c is orthogonal.
+- D and the eight sets U_c D are pairwise disjoint subsets of V of size 240.
+  Their union is V.
+- For every c and every v in V, U_c^T v is integral and represents a line
+  in V. This exhausts 8*2160=17280 image checks. Orthogonality and the finite
+  bijection establish U_c^T V=V.
+
+`verify.py` constructs the entire shell and checks these facts with exact
+integer arithmetic. It divides only after testing divisibility. Thus these
+facts are a complete finite certificate, rather than sampled evidence or
+floating eigenvalue estimates. No theorem about an unmaterialized orbit is
+needed. Quadratic-phase Walsh bases and Kerdock/mutually unbiased bases are
+classical; the table is an explicit certificate, not a claim to those ideas.
+
+## Theorem
+
+Every clique in V has at most 126 lines.
+
+Suppose |C|>=127. The nine disjoint D16 sets partition V, so at least one
+contains fifteen members of C. Lemma 1 excludes more than fifteen. If it is
+the identity set, Lemma 2 gives |C|<=30. Otherwise apply U_c^T to the whole
+clique. The exact certificate ensures that the image is still a clique in V,
+and its intersection with D contains a full fifteen-line star. Lemma 2 again
+gives |C|<=30, a contradiction. Equivalently, every clique larger than thirty
+has at most fourteen lines in each chart, giving |C|<=9*14=126.
+
+The basic nine-chart counting bound is 135. The new step removes its D16
+equality case in every chart, improving that bound by nine. The classical
+135-frame geometry itself is not claimed as new. This is a finite geometric
+obstruction with a scoped written proof over all subsets of this fixed V;
+it is neither a failed clique search nor an all-dimensional lattice theorem.
+
+## Exact evidence and limits
+
+Besides the complete chart checks, the verifier compares the star formula
+with direct integer inner products against all 1920 odd lines on 176 named
+center/sign fixtures. It enumerates all 32768 sign patterns at center zero
+by the independent hyperplane-parity formula. The proof covers arbitrary
+signs at every center; the 176 direct fixtures are not described as an
+exhaustive census of all center/sign pairs. The thirty-line attainer has
+all 435 pairs checked.
+
+The published 72-line lower witness in PR895 is a cited result, not replayed
+here. The resulting interval 72<=omega(V)<=126 does not determine omega(V).
+A clique upper bound is not an upper bound on the binary decoder's minimum
+fitting rank. Physical native realization, scalar/helper delivery, arbitrary
+dirty restoration, a complete paid invoice and the five selected framework
+assumptions remain separate. No kappa or selected-frontier change follows.
+Independent human and formal proof-kernel review are unclaimed.

research/bw16-global-clique-126/README.md

@@ -0,0 +1,104 @@
+# Global BW16 nonorthogonality clique bound 126
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Every pairwise nonorthogonal subset of the 2160 norm-eight BW16 lines has
+at most **126** lines. This is a finite certificate with a scoped written
+combinatorial proof. The [proof](PROOF.md) covers every subset of this fixed
+shell, rather than a bounded search around one clique.
+
+Nine 240-line D16 sets partition the shell. Each contains at most fifteen
+clique members. The new equality-case step shows that fifteen members in
+any one chart force the entire clique to have at most thirty lines. Thus
+any clique larger than thirty has at most fourteen members per chart:
+
+    |C| <= 9*14 = 126.
+
+The baseline nine-chart count gives 135. The new step lowers it by nine.
+The conditional thirty-line bound is attained. DaysSky's PR895 supplies the
+published 72-line lower witness as a credited premise. It is not replayed.
+The remaining global interval is therefore 72<=omega<=126.
+
+## Reproduce
+
+From the repository root, with standard-library CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/bw16-global-clique-126/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/bw16-global-clique-126/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/bw16-global-clique-126
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/bw16-global-clique-126 --check-source-history
+```
+
+Another CPython 3.12 executable may replace that absolute path. The direct
+marker is `PASS_BW16_GLOBAL_CLIQUE_126`. Verification is read-only and needs
+no Git, network, source imports, numerical library or solver. `--emit` writes
+a newly computed receipt to stdout; it is absent from registered checks.
+[RESULT.json](RESULT.json) is generated by that code, bound to the package
+source hashes and compared byte for byte in ordinary verification.
+
+The certificate checks all 2160 shell members against an independent
+Construction-D membership predicate, all nine disjoint blocks and all 17280
+inverse chart images. It also checks 176 literal star fixtures against all
+1920 odd lines, all 32768 sign patterns at center zero by a parity formula,
+and all 435 pairs of a thirty-line attainer. Six controls reject wrong norm,
+nonaffine support, odd sign parity, a damaged orthogonal matrix, duplicate
+charts and the false compatibility of the two signs on one coordinate edge.
+
+## Scope and credit
+
+Source and main predecessor: DaysSky / [PR895](https://github.com/CrocSwap/integer-mult-bounds/pull/895),
+head `3bf6fccaf17521ffdb9b3bec2740ba4886478556`. Its BW16 shell and screen
+setting motivate the global question. No source executable or source witness
+is copied or audited. Nick Petalas / [PR5118](https://github.com/CrocSwap/integer-mult-bounds/pull/5118)
+gives the earlier local insertion obstruction, not this global bound.
+DreamingOfClouds / PR446, PR595 and PR2244, Joel Pulikkan / PR620 and the
+retained decoder/lattice lineage keep their credit.
+
+Barnes-Wall, Reed-Muller, Construction-D, Walsh characters and Kerdock bases
+are classical. The classical 135-frame decomposition is also discussed in
+[Noam Elkies's lattice notes](https://people.math.harvard.edu/~elkies/M272.19/nov13.pdf).
+The broader Barnes-Wall construction is in [Nebe, Rains and Sloane](https://arxiv.org/abs/math/0207186).
+The claimed addition is the explicit global 126 bound and its equality-case
+proof and executable certificate. No general literature-priority claim is made.
+
+This changes the complex-rank-shape-decoder card to a geometric side result;
+it does not price a changed supplier. The selected-baseline binding-only
+first example passed. Canonical base is
+`7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority revision 8, selected PR6030.
+Live open/account work, recent handoffs and active Discussions, all retrieved
+BW16 PR bodies, main general-form and merged searches and local reservations
+were checked. Broader cached overlap has coverage/freshness limits; arbitrary
+diffs and unpublished work are not exhaustively covered.
+
+The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19375419)
+planned a global spectral certificate. The delivered certificate uses nine
+explicit orthogonal coordinate charts and the sharp full-star restriction.
+Discovery stopped at the first new verified bound. The classical 135 bound
+was identified as prior geometry, not claimed as an original improvement.
+
+The maximum clique, minimum binary fitting rank, native/helper/restoration
+costs, complete recursive/outer bill and multiplication theorem remain open.
+No kappa or selected-frontier change is claimed. Independent human and formal
+proof-kernel review are unclaimed. No Lean, Docker, selected cold replay or
+predecessor scientific suite was run.
+
+Power-of-ten scope is this fixed verifier. It has no recursion or dynamic
+code loading; all enumerations are bounded by sixteen coordinates, 2160
+lines, eight charts or 32768 sign patterns. Functions are below sixty lines.
+Managed Python allocation is a rule-3 deviation: live data are bounded by the
+fixed shell, nine 240-line blocks and one chart's 2160 images. The standard
+library allocates tuples/integers during checking. No process, cache, lock or
+background writer is created. Explicit exceptions keep all checks active
+under optimized Python. Input extensions need new resource bounds.
+
+## Open next questions
+
+1. Can the remaining interval 72<=omega<=126 be narrowed using compatibility
+   between distinct nonsaturated D16 charts? Start with their fourteen-line
+   equality possibilities. The present theorem does not classify them, and
+   this follow-on is not reserved.
+2. Can a changed decoder exploit a smaller set with a favorable complete
+   invoice? Start with an explicit fitting identity and charge every source,
+   target, restoration and native cost. Clique information alone cannot
+   answer that physical question.

research/bw16-global-clique-126/RESULT.json

@@ -0,0 +1,65 @@
+{
+  "block_sha256": [
+    "eb83acde02828b331447740e29e70860b76fadd1e8195539af660a945872c520",
+    "764f5983da5bbaa4f72107ee33bf0437a5f2662763b4f60fcdf9c79bf4d68e27",
+    "65ba5a9092a25f868251ac6855d9052017df6d2079a527331019381837ddf80f",
+    "02a24faf95dd2617ee0cce8e61afab59ac27c042cb7741160d625db259cf0736",
+    "c4b0c2cbc3ce2f29f3a13c298228d3d072a52f128819946270be278d7a3e076d",
+    "5c7f3d562b9739783b14e1a0ae330021b18f18386ffa85afd1a055f634f5b01e",
+    "4e314f41ad1235a5e4a2fa98655b388ad6f0db8c4da07f2c4904f6a7c495d518",
+    "c6996d13070d08bba9b159d0ec02aa3d4fcd4af486eb34532dcfdc2c176b87d6",
+    "a0d13f6d00a9e175e4d6a471711de28c14ee3f6e2c00a184268d85f974be4c97"
+  ],
+  "block_sizes": [
+    240,
+    240,
+    240,
+    240,
+    240,
+    240,
+    240,
+    240,
+    240
+  ],
+  "claim_type": "finite certificate with a scoped combinatorial proof",
+  "compatible_odd_histogram_at_center_zero": {
+    "0": 1024,
+    "15": 1024,
+    "7": 15360,
+    "8": 15360
+  },
+  "conditional_star_clique_maximum": 30,
+  "controls": [
+    "odd_sign_parity",
+    "nonaffine_support",
+    "wrong_norm",
+    "damaged_hadamard",
+    "duplicate_chart",
+    "same_edge_signs_are_orthogonal"
+  ],
+  "full_star_sign_patterns": 32768,
+  "global_clique_upper_bound": 126,
+  "inverse_transport_checks": 17280,
+  "literal_star_fixtures": 176,
+  "quadratic_forms": [
+    0,
+    57,
+    53,
+    46,
+    35,
+    28,
+    18,
+    15
+  ],
+  "schema_version": 1,
+  "shell_lines": 2160,
+  "shell_sha256": "1ec1067400299e389af79713c6713fbb50c0271ddadee16f9da838c5843f9134",
+  "source_sha256": {
+    "PROOF.md": "cfdfb4b412a8461045ea31ad39572713ddd1d9ff1faa0f6b0982d5d8088dc8ae",
+    "README.md": "47adadbe6c6e67459fab82c1a5c40aab035585606481d5ad70dc7285a5c78ea6",
+    "SOURCES.json": "911ffe8b456c49ccd19ee42c8e21b226a56dacba515e857300aa28cc1db87be7",
+    "TASK.json": "19930226c3438c68779af4ba15d2a2ae4310b6fec1510c81099950ef123b2e6e",
+    "VERIFY.json": "70b4e98924712f9a57a96ad5c0c9492e7f51865446aab15f7ac4eded2c86a371",
+    "verify.py": "a22fe0360e3c8a57dd929151b9ce91fe650d2a4f105795d0dadad890af86c503"
+  }
+}

research/bw16-global-clique-126/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    }
+  ]
+}