Lower the D16 spinor upper bound from 317 to 316 (no κ)

research/spinor-integral-cap/PROOF.md

@@ -0,0 +1,104 @@
+# The integral square obstruction
+
+Let `C` be a nonempty subset of `F_2^16`, with no repeated words, such that
+`x + 1` belongs to `C` for every `x` in `C`. Here `1` is the all-ones word.
+Suppose every distance between distinct words is in
+
+```text
+S = {2,6,8,10,14,16}.
+```
+
+Write `N = |C|`. Antipodality partitions `C` into `N/2` distinct pairs.
+We prove `N <= 632`.
+
+## The inherited nonnegative square identity
+
+For a mask `u`, define the integer character sum
+
+```text
+F(u) = sum_(x in C) (-1)^(u.x).
+```
+
+For `k = 0,...,16`, the binary Krawtchouk polynomial is
+
+```text
+K_k(d) = sum_j (-1)^j binom(d,j) binom(16-d,k-j).
+```
+
+Counting masks by their intersection with the support of `x+y` gives
+`sum_(wt(u)=k) (-1)^(u.(x+y)) = K_k(d(x,y))`. Expanding the square therefore
+gives, without any averaging or transitivity assumption,
+
+```text
+sum_(wt(u)=k) F(u)^2 = sum_(x,y in C) K_k(d(x,y)).
+```
+
+Use the three nonnegative weights from PR5206's dual identity, and put
+
+```text
+f(d) = 25 K_2(d) + K_6(d) + 2 K_8(d),
+W = 25 sum_(wt(u)=2) F(u)^2
+       + sum_(wt(u)=6) F(u)^2
+     + 2 sum_(wt(u)=8) F(u)^2.
+```
+
+The binomial formula yields the complete needed table:
+
+| d | 0 | 2 | 6 | 8 | 10 | 14 | 16 |
+|---|---:|---:|---:|---:|---:|---:|---:|
+| f(d) | 36748 | -116 | -116 | -116 | -116 | -116 | 36748 |
+
+Each word has exactly one partner at distance zero, itself, and one at
+distance sixteen, its antipode. Thus the ordered-pair identity is
+
+```text
+W = 2N*36748 - 116*N*(N-2)
+  = N*(73728 - 116N).                                      (1)
+```
+
+Nonnegativity of `W` gives the inherited real bound `N <= 18432/29`.
+Since `N` is even, `N <= 634`. This is the existing cap of 317 spinor lines;
+the new step below is the integral square floor at the remaining endpoint.
+
+## The new integral floor at 317 pairs
+
+Suppose `N = 634`. Choose one representative `r` from each of the 317
+antipodal pairs. If `wt(u)` is even, the two words of a pair have the same
+character value, because `(-1)^(u.1)=1`. Hence
+
+```text
+F(u) = 2 sum_(317 representatives r) (-1)^(u.r).
+```
+
+The inner sum has an odd number of summands, each equal to `+1` or `-1`.
+It is an odd integer. Consequently `F(u) = 2 mod 4`, and `F(u)^2 >= 4`,
+for every even-weight mask. All three weights in `W` are positive, so
+
+```text
+W >= 4*(25*binom(16,2) + binom(16,6) + 2*binom(16,8))
+   = 4*(25*120 + 8008 + 2*12870)
+   = 146992.                                               (2)
+```
+
+But (1) gives
+
+```text
+W = 634*(73728 - 116*634) = 116656.
+```
+
+This contradicts (2), by `146992-116656=30336`. Thus `N` cannot be 634;
+the inherited bound and evenness give `N <= 632`.
+
+## Geometric corollary and limits
+
+In PR2244's D16+ roots-plus-spinors family, each spinor line is one antipodal
+pair of sign words. The specified allowed-distance model is exactly the
+one above, and the root contribution is 240 lines. Therefore this family
+contains at most `316` spinor lines and at most `556` total lines.
+This uses the predecessor's model identification as a cited premise.
+
+At 316 pairs the number of representatives is even; the inner character
+sum may vanish. The new square floor therefore does not exclude that case.
+Neither attainment nor a sharp code-size theorem is claimed. Other line
+systems, other spinor compatibility rules, compensation and every physical
+supplier obligation are outside this proof. No new kappa follows.

research/spinor-integral-cap/README.md

@@ -0,0 +1,115 @@
+# Integral Fourier squares lower the D16 spinor cap to 316
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+**Claim type: scoped mathematical proof with exact finite corroboration.**
+Every antipodal binary length-sixteen code whose nonzero distances belong to
+`{2,6,8,10,14,16}` has at most **632 words, or 316 antipodal pairs**.
+Consequently, the roots-plus-spinors family of DreamingOfClouds's
+[PR2244](https://github.com/CrocSwap/integer-mult-bounds/pull/2244) has at most
+**240 + 316 = 556 lines**, improving its upper bound of 557 by one.
+Attainment of 316 spinor lines is not asserted.
+
+The new step answers the integrality question in Nick Petalas's older
+[PR5206](https://github.com/CrocSwap/integer-mult-bounds/pull/5206).
+Its real two-point optimum and dual identity are cited predecessors.
+No predecessor scientific executable is imported or replayed. The new proof
+uses the fact that, with 317 antipodal pairs, every even-weight character sum
+is twice an odd integer. Its square is at least four. The inherited weighted
+dual identity then requires the same sum of squares to be both at least
+146,992 and exactly 116,656. The contradiction gap is 30,336.
+[PROOF.md](PROOF.md) gives a self-contained derivation.
+
+## Reproduction and evidence
+
+From the worktree root, with CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/spinor-integral-cap/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/spinor-integral-cap/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/spinor-integral-cap
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/spinor-integral-cap --check-source-history
+```
+
+Another CPython 3.12 path may replace the local interpreter path. The direct
+checker prints a generated receipt bound to all six package files, followed by
+
+```text
+PASS_SPINOR_INTEGRAL_CAP spinor_lines=316 roots_plus_spinors=556 gap=30336 no_new_kappa
+```
+
+The checker enumerates all 20,998 character masks at weights two, six and eight.
+Literal character evaluation corroborates the seven entries of the weighted
+kernel table, separately from its binomial calculation. It checks 25,440
+possible sign counts for odd pair counts up to 317. Fifteen actual small
+antipodal codes supply 314,970 character evaluations and 320 ordered pairs;
+167,984 of those character evaluations have odd pair count. These fixture
+families overlap and are not a census of codes of size 634.
+
+Seven rejecting controls cover altered dual coefficients, forbidden distance,
+duplicate words, out-of-range words and missing antipodes. Three further
+discriminators show why even pair counts, missing antipodality and omission of
+the square's factor four do not give the contradiction. Every check remains
+active under optimized execution. No receipt is hand-written or stored.
+
+The universal code-size bound follows from the written parity argument and
+character identity. Finite execution corroborates those identities and arithmetic;
+it is not an enumeration of all large codes or a formal proof-kernel check.
+
+## Scope and credit
+
+PR2244 supplies the D16+ roots-plus-spinors distance model and original
+317-spinor-line cap, with its PR2228, PR2125, PR968 and lattice/decoder lineage.
+PR5206 supplies the exact antipodal real relaxation and its three-multiplier
+dual identity. Both remain unchanged and retain their credit. Classical
+character orthogonality, Krawtchouk polynomials and parity refinements of code
+bounds retain their credit; no general literature-priority claim is made.
+
+This is a geometric side result under `complex-rank-shape-decoder`, with the
+scope change recorded in TASK.json. The current selected-baseline binding
+command passed at selected PR6030, kappa `781451/250000000`. No physical
+decoder, compensation, native realization, routing, restoration, compiler,
+precision/tape, stock, supplier admission or new kappa follows. The five
+selected framework assumptions remain. Independent human and formal
+proof-kernel review are unclaimed. Selected cold replay, Lean and Docker are
+unrun. This package stops at the first proved improvement.
+
+## Open next questions
+
+Can the even pair count 316 be excluded or attained? Its even-weight character
+sums can vanish, so the odd-pair square floor used here does not settle it.
+A first step is an integral or triple-distance feasibility test at exactly
+632 words, before a larger construction search. Neither that test nor a
+632-word construction is supplied or reserved. TASK.json records the relevance
+and blocker.
+
+## Verifier resource contract
+
+The verifier has no arguments, recursion, subprocesses, network access or
+predecessor imports. It enumerates at most 65,536 candidate masks, stores
+20,998 selected masks and uses at most eight words in each positive code
+fixture. Each helper accepts at most sixteen fixture words. Nested bounds are
+explicit; no code space is searched. All functions are under sixty lines.
+Receipts read six fixed regular files, each at most 1 MiB, one at a time.
+Warning-strict normal and optimized runs provide interpreter diagnostics;
+repository-wide configuration is unchanged.
+
+Power of Ten rule 3 has a managed-runtime deviation in `verify.py`: Python
+allocates exact integers, tuples and dictionaries during checking. The fixed
+domains above bound live state, and receipt buffers are released after each
+file. A fixed-buffer port is the follow-up if allocation-free execution is
+required. No unbounded service, callback dispatch or dynamic code generation
+is introduced.
+
+## Overlap and provenance
+
+The advance [CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19372180)
+records the target before packaging. Live handoffs, active Discussions, open
+PRs, recent account work, main README formulas and merged spinor work were
+searched. PR5206 was published October 23, outside the seven-day restriction.
+It is the question's source; no other active local reservation used that source.
+Main and merged searches found the predecessor cap and real optimum, with no
+identified 316-spinor-line bound. Sparse notes, arbitrary historical diffs and
+unpublished work remain search limits. SOURCES.json binds the two predecessor
+notes and the historical task/selected context to canonical main
+`7c49fe32c55de02c2c873655c804b16e4c3fef0a`.

research/spinor-integral-cap/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "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"
+    },
+    {
+      "path": "research/antipodal-spinor-lp-optimum/README.md",
+      "usage": "input",
+      "git_blob": "ac42860825ef7f17e29a70f3937d5d4357314ad4",
+      "sha256": "776e021ff42ec443f563a35afb83f6dbff9b6d7b30ea64abb5bef793d0e1bba9"
+    },
+    {
+      "path": "research/line-system-saturation/README.md",
+      "usage": "input",
+      "git_blob": "8e998ee15db765ce90d52d53d4a61f3fd75e5dae",
+      "sha256": "a99a58bc58e42348596534ce8f73809255ac89b330589b0f4d9cf2199d669e87"
+    }
+  ]
+}

research/spinor-integral-cap/TASK.json

@@ -0,0 +1,94 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-rank-shape-decoder",
+  "priority_revision": 8,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "original_card": {
+    "id": "complex-rank-shape-decoder",
+    "question": "Can a legal decoder or coframe change improve the full signed moment, including changed helper targets?",
+    "starting_points": [
+      "docs/research/current-priorities.md",
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+      "docs/research/recursive-invoice-preflight.md"
+    ],
+    "methods": [
+      "Construct and independently check one source-bound instance of the stated first experiment.",
+      "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change."
+    ],
+    "acceptance_gate": "A source-bound arbitrary-input identity and legal producer/consumer boundary with the complete paid and productive target invoice, including restoration, ownership, native alignment and extra charges. Price under the actual current model; historical ceiling.py assumptions must be established before use. A favorable optimistic relaxation keeps a route open but is not a completed supplier. A scoped local result remains useful; expansion requires the family-level budget gate.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_selected_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.",
+      "scope": "Source-bound orientation only, not a supplier replay or theorem proof."
+    },
+    "first_experiment": "Price one complete changed itinerary with both paid and productive histograms. Check #5693/#5698 for overlap and their exact hypotheses before another coframe search. Use the signed invoice preflight where its boundary contract agrees; an inconclusive concave comparison is not a power crossing. Stop if an optimistic complete budget fails at the chosen target or native delivery remains unspecified.",
+    "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.",
+    "allowed_variations": [
+      "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes."
+    ],
+    "scope_change_triggers": [
+      "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.",
+      "Treating an archived proposal or local numerical pass as complete supplier admission."
+    ],
+    "overlap_terms": [
+      "coframe",
+      "signed moment",
+      "5693",
+      "5698"
+    ],
+    "existing_checks": [
+      {
+        "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.",
+        "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md",
+        "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.",
+        "status": "reviewed",
+        "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137",
+        "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Prove that the antipodal length-sixteen spinor distance model has at most 632 codewords, or 316 spinor lines, by an integral Fourier-square floor.",
+  "scope_change_reason": "This is a geometric side bound answering PR5206, rather than a completed paid decoder itinerary. It adds integrality to the real two-point model and improves its integer cap by one line.",
+  "bottleneck_link": "Scoped side result: the D16+ roots-plus-spinors family has at most 556 lines. No paid profile, physical decoder, compensation or supplier gain is inferred.",
+  "budget_minutes": 60,
+  "stop_rule": "Ship the first verified improvement, the exclusion of 317 antipodal pairs; do not extend to even pair counts or a three-point search.",
+  "outcome": "completed",
+  "evidence": "Written parity and character proof; exact contradiction 146992 > 116656. New independent literal character/kernel and ordered-pair checks corroborate the identities without importing predecessor scientific code.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "Can 316 antipodal spinor pairs be excluded or attained?",
+      "why_it_matters": "It determines whether the new 556-line roots-plus-spinors upper cap can be sharpened or matched in the same family.",
+      "first_step": "Test integral or triple-distance feasibility at exactly 632 codewords before attempting a larger construction.",
+      "blocked_by": "At even pair count character sums may vanish; no 632-word realization or stronger integral certificate is supplied."
+    }
+  ],
+  "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19372180",
+  "source_question": {
+    "pr": 5206,
+    "author": "petalas",
+    "published": "2026-10-23T12:33:08Z"
+  },
+  "environment": {
+    "python": "3.12.15",
+    "platform": "macOS-27.0.1-arm64-arm-64bit",
+    "dependencies": "standard library only"
+  },
+  "overlap_coverage": {
+    "open_prs": 539,
+    "discussion_records": 6561,
+    "remote_pagination_complete": true,
+    "open_fetched_at": "2026-11-03T11:00:37Z",
+    "discussions_fetched_at": "2026-11-03T11:01:56Z",
+    "limits": "Sparse working notes, arbitrary historical diffs and unpublished work; separate main README and merged-PR searches performed."
+  }
+}

research/spinor-integral-cap/VERIFY.json

@@ -0,0 +1,37 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/antipodal-spinor-lp-optimum/README.md",
+    "research/line-system-saturation/README.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Exact integrality obstruction, all selected character masks, literal code identities, seven rejecting controls and three semantic discriminators."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 60,
+      "checks": "Repeat every exact check with Python assertions disabled."
+    }
+  ]
+}