Exclude saturated Gram systems at every even window h >= 6 (no κ)

research/even-window-saturation-gap/PROOF.md

@@ -0,0 +1,139 @@
+# Even-window saturation is impossible from window six onward
+
+## Statement
+
+Let `k >= 3`, `T >= 1`, and let `r_1,...,r_v` be nonzero vectors in a real or
+complex inner-product space of dimension `T`. Assume there are labels
+`p_i` in a `2k`-dimensional symplectic vector space `V` over `F_2` and a nonzero
+`w` such that
+
+1. `b(p_i,w)=1` for every `i`;
+2. for distinct `i,j`, `b(p_i,p_j)=0` implies `<r_i,r_j>=0`.
+
+Repeated labels are allowed. Then
+
+```text
+v <= 2^k T - 1.                                      (1)
+```
+
+In particular, for the exact nonorthogonality adjacency `A` of a real line
+system, if `rank_F2 A=2k` and `1` belongs to `col A`, its even window is `h=2k`
+and (1) applies. At `h=6` and `h=8`, respectively, `v=8T` and `v=16T` are
+impossible. This answers PR5282's first open next question in the negative.
+
+The label reduction and the upper bound `v <= 2^k T` are prior work of
+DreamingOfClouds in PR2244. Matarener's PR5282 poses the equality question and
+explains its relevance to short-window decoder screens. We use those statements
+as premises. The new step is the complementary-label projection identity (5).
+The proof below also derives the needed counting bound to make its equality
+conditions explicit; predecessor vector systems or invoices are not replayed.
+
+## Affine basis equations
+
+Put `H={p in V: b(p,w)=1}`. A generator is a maximal totally isotropic
+subspace of `V`, hence has dimension `k`. Let `N_j` be the number of generators
+in symplectic dimension `2j`, with `N_0=1`. Counting incident nonzero points
+and generators gives
+
+```text
+N_j (2^j-1) = (2^(2j)-1) N_(j-1),
+N_j = product_(a=1..j) (2^a+1).
+```
+
+Here generators containing a point correspond to generators of its symplectic
+quotient. Write `r=N_(k-1)` and `s=N_(k-2)`, so `r=(2^(k-1)+1)s`.
+
+Let `G` be the family of generators not containing `w`. Its size is
+
+```text
+|G| = N_k-N_(k-1) = 2^k r.
+```
+
+Each `L` in `G` meets `H` in an affine hyperplane of `L`, of size `2^(k-1)`.
+Indeed, `L=L^perp`, so `w not in L` makes `b(-,w)` a nonzero functional on `L`.
+Each point of `H` belongs to `r` members of `G`. Distinct `p,q` in `H` belong
+together to `s` members exactly when `b(p,q)=0`, and to none otherwise.
+The former count uses the symplectic quotient of the isotropic plane
+`span(p,q)`. None of these generators can contain `w`, since `b(p,w)=1`.
+
+The vectors whose labels lie in any `L` are pairwise orthogonal, including
+vectors of the same label. There are at most `T` of them. Sum this inequality
+over `G`. Each vector occurs `r` times, so `rv <= 2^k r T`.
+
+Suppose equality `v=2^k T` holds. Then every one of these finite inequalities
+is an equality. The vectors with labels in `L` form an orthogonal basis of
+the ambient space for every `L` in `G`.
+
+For each `p` in `H`, let `E_p` be the orthogonal projection onto the span of
+the vectors carrying label `p`. Set it to zero for an unused label. The basis
+condition says
+
+```text
+sum_(p in L intersect H) E_p = I      for every L in G.       (2)
+```
+
+Summing (2) over all generators gives
+
+```text
+sum_(p in H) E_p = 2^k I.                                   (3)
+```
+
+## Complementary labels force an impossible projection sum
+
+Fix `p` in `H` and write `p'=p+w`. These are distinct points of `H` and
+`b(p,p')=1`, so no generator contains both. For any other `q` in `H`,
+
+```text
+b(p',q) = b(p,q)+1 in F_2.
+```
+
+Consequently exactly one of `p,p'` is orthogonal to `q`. Sum equations (2)
+over the `2r` generators containing either `p` or `p'`. The two selected labels
+occur `r` times each, and every other label occurs `s` times. Therefore
+
+```text
+(r-s)(E_p+E_p') + s sum_(q in H) E_q = 2r I.                (4)
+```
+
+Substitute (3), use `r=(2^(k-1)+1)s`, and divide by `r-s`:
+
+```text
+E_p + E_(p+w) = 2^(2-k) I.                                 (5)
+```
+
+For `k>=3` the scalar `c=2^(2-k)` lies strictly between zero and one.
+Choose any occupied label `p` and a unit vector `x` in the range of `E_p`.
+Since orthogonal projections are positive semidefinite, (5) gives
+
+```text
+c = <x,(E_p+E_(p+w))x> = 1 + <x,E_(p+w)x> >= 1,
+```
+
+a contradiction. There is an occupied label because `v=2^k T>0`.
+Thus equality cannot hold. Since `v` is an integer, (1) follows.
+
+The restriction `k>=3` matters. At `k=2`, (5) has scalar one and two
+complementary nonzero projections satisfy it. The proof makes no assertion
+that they extend to an exact line system. This is an algebraic exception,
+not a claimed attaining construction.
+
+## Checkable linear certificate
+
+The verifier enumerates maximal isotropic subspaces by unique reduced row
+echelon bases for `k=2,3,4`. For every unordered pair `{p,p+w}`, it forms an
+integer linear combination of the incidence rows of (2):
+
+```text
+r * sum_(L contains p or p+w) row(L) - s * sum_(L in G) row(L).
+```
+
+Its left side has coefficient `r(r-s)` at the two selected labels and zero
+elsewhere. Its right side is `2r^2-s|G|=2rs`. Division gives exactly (5).
+This is a finite certificate of the elimination step at the two windows in
+the question and the exceptional window four. The all-`k` result comes from
+the written incidence argument, not extrapolation from those computations.
+
+No optimal asymptotic replacement for `2^k` is established. A sequence with
+`v/T` tending to `2^k` as `T` increases is not excluded by (1). This result
+does not close short windows below their cap, address arbitrary pairings, or
+supply a native word, restoration schedule, complete signed invoice or new κ.

research/even-window-saturation-gap/README.md

@@ -0,0 +1,110 @@
+# No saturated even-window Gram systems at h >= 6
+
+Scoped proof with exact finite corroboration, produced by Nick Petalas.
+
+For a real or complex Gram line system of dimension `T >= 1`, suppose its
+nonorthogonality adjacency `A` has `rank_F2 A=2k` and `1 in col A`. For every
+`k >= 3`,
+
+```text
+v <= 2^k T - 1.
+```
+
+Thus a saturated system with `v=8T` at `h=6`, or `v=16T` at `h=8`, does not
+exist. This answers [Matarener's PR5282, open question 1](https://github.com/CrocSwap/integer-mult-bounds/pull/5282).
+The [proof](PROOF.md) establishes the stronger label-based statement even when
+additional orthogonalities are permitted.
+
+The new step is an equality obstruction. Saturation makes each affine
+Lagrangian class an orthogonal basis. Summing those basis equations forces
+`E_p + E_(p+w) = 2^(2-k) I` for orthogonal projections onto complementary label
+classes. A nonzero projection cannot lie below a scalar smaller than one.
+
+The prior cap `v <= 2^k T`, its label reduction and the Lagrangian counting
+framework belong to DreamingOfClouds's [PR2244](https://github.com/CrocSwap/integer-mult-bounds/pull/2244).
+PR5282 poses the equality question and supplies its historical decoder-screen
+motivation. Those results are cited premises; no predecessor construction,
+invoice or numerical result is audited or replayed here.
+
+## Evidence and reproduction
+
+The all-`k` theorem is a written proof. The standard-library verifier constructs
+integer linear elimination certificates from independently enumerated RREF
+generators. It returns the following finite data:
+
+- `k=2`: 8 labels, 12 affine generators, 4 pair certificates, scalar `1`.
+- `k=3`: 32 labels, 120 affine generators, 16 pair certificates, scalar `1/2`.
+- `k=4`: 128 labels, 2160 affine generators, 64 pair certificates, scalar `1/4`.
+
+It also checks a complementary-projection exception at `k=2`, 30 exact scalar
+instances of the idempotent obstruction, and nine rejecting cases. The cases
+remove or duplicate a generator, change the partner or scalar, or supply one
+of five invalid dimension contracts. Checks use explicit exceptions and remain
+active under optimized Python.
+
+From the repository root, run:
+
+```sh
+~/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/even-window-saturation-gap/verify.py
+~/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/even-window-saturation-gap/verify.py
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/even-window-saturation-gap
+~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/even-window-saturation-gap --check-source-history
+```
+
+Expected tokens are `PASS_EVEN_WINDOW_SATURATION_GAP`,
+`PASS_REGISTERED_RESEARCH_PACKAGE`, and `PASS_RESEARCH_COMMIT_BYTES`.
+CPython 3.12 or later suffices; the interpreter path above records the
+local environment. The two registered checks each take less than one second
+on the local macOS run. This is a runtime bound for these checks, not a claimed
+speed improvement.
+
+An optional `--receipt /absolute/path/outside-the-checkout.json` writes a
+generated receipt containing the enumerated data, source hashes, package hashes
+and interpreter version. Normal runs only print their result. The contextual
+source documents, base commit, catalogue and selected record are pinned in
+[SOURCES.json](SOURCES.json). No external library, solver or network is needed.
+
+## Limits
+
+This excludes equality, with an integer gap of one. It does not prove an
+optimal dimension-independent density gap or exclude near-saturation as `T`
+increases. The exception `k=2` is an algebra control, not an attaining exact
+line-system construction. Arbitrary pairings and non-Gram decoder matrices are
+outside the claim.
+
+There is no native word, physical delivery, dirty restoration, complete current
+signed invoice, supplier admission or new κ. PR5282's historical invoice is not
+repriced. The selected frontier and all five retained assumptions are unchanged.
+Independent human and formal proof-kernel review are unclaimed.
+
+## Open next questions
+
+The structured questions are in [TASK.json](TASK.json).
+
+- Determine the optimal supremum of `v/T` at `h=6` or `h=8`. Begin with positive
+  semidefinite deficits in the affine-basis equations. A quantitative deficit
+  bound is missing; the integer gap here need not survive division by `T`.
+- Test a concrete nonsaturated even-window system against a current complex
+  caller. First specify its literal decoder, targets, paid children and
+  restoration contract. Native realization, uniform closure and a complete
+  signed invoice remain blockers.
+
+## Implementation bounds
+
+The verifier has no recursion or background processes. The RREF search is
+restricted to `2 <= k <= 4`, with at most `256 * 2^16` candidates and at most
+256 labels. Functions are below 60 lines and checks survive `-O`. Runtime
+allocation is a Python deviation from the fixed-allocation rule. Live storage
+is bounded by the finite RREF candidate and generator collections; no unbounded
+input can expand the search. A systems-language fixed-buffer implementation
+would be needed only if this verifier becomes a memory-constrained component.
+Warnings-as-errors, syntax inspection and both registered commands are the
+available local diagnostics; no dedicated Python linter or type checker is
+installed on PATH. This package changes no shared build configuration.
+
+## Credit
+
+The complementary-label equality obstruction, proof and standalone verifier were
+produced by Nick Petalas. Credit Matarener for PR5282's question and screen,
+DreamingOfClouds for PR2244's line-count and label framework, and the decoder
+lineage credited in those unchanged source documents. New work is Apache-2.0.

research/even-window-saturation-gap/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc",
+  "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/line-system-saturation/README.md",
+      "usage": "input",
+      "git_blob": "8e998ee15db765ce90d52d53d4a61f3fd75e5dae",
+      "sha256": "a99a58bc58e42348596534ce8f73809255ac89b330589b0f4d9cf2199d669e87"
+    },
+    {
+      "path": "research/window-break-even-4470/README.md",
+      "usage": "input",
+      "git_blob": "89b5e4150e7dfe9804b7e1a65fba1fea8d77da8b",
+      "sha256": "103d9cd0943958115007cff7b2451da15182c6036be3320fa811b867d9d94ffd"
+    }
+  ]
+}

research/even-window-saturation-gap/TASK.json

@@ -0,0 +1,87 @@
+{
+  "schema_version": 1,
+  "task_id": "complex-new-helper-inventory",
+  "priority_revision": 8,
+  "base_commit": "2485805a6d47f36ea83ddde6327d453ac82d44dc",
+  "original_card": {
+    "id": "complex-new-helper-inventory",
+    "question": "Can a changed helper inventory earn productive credit that survives completion, compilation and the actual caller?",
+    "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"
+    ],
+    "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": "Specify all arbitrary inputs, owned fields, restored outputs and a physically legal consumer. Compare complete P and T, including target debits and precision/stock costs. #5599 is a positive control for target refinement, not permission to split every helper for free. #5614 is a hypothetical compiler budget, not an emitted 145-split word. Stop at the first unpaid boundary or a failing optimistic full bill.",
+    "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": [
+      "productive helper",
+      "target refinement",
+      "5599",
+      "5614"
+    ],
+    "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 even-window Lagrangian line-count cap cannot be attained for k >= 3, resolving PR5282 open question 1 at h=6 and h=8.",
+  "scope_change_reason": "Replace the current card's source-bound productive-helper first experiment with PR5282's explicit even-window line-system equality question. This excludes a proposed complex-decoder inventory premise; it does not construct or price a new helper caller.",
+  "bottleneck_link": "A saturated h=6 or h=8 line system is an explicitly proposed input to a cheaper complex decoder. The new projection identity excludes equality in this branch while leaving nonsaturated constructions and the selected invoice open.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop at the first verified original obstruction; do not optimize a stronger ratio or a new construction.",
+  "outcome": "completed",
+  "evidence": "PROOF.md proves v <= 2^k T - 1 for every k >= 3 under the affine symplectic label contract. verify.py constructs exact incidence elimination certificates at k=2,3,4 and tests the scalar obstruction and rejection controls.",
+  "author": "Nick Petalas",
+  "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.",
+  "open_questions": [
+    {
+      "question": "What is the optimal supremum of v/T at even windows h=6 and h=8?",
+      "why_it_matters": "An integer gap of one excludes saturation but does not remove near-saturated systems from a complete supplier screen.",
+      "first_step": "Use the same affine-generator equations with positive semidefinite basis deficits instead of setting all deficits to zero.",
+      "blocked_by": "No dimension-independent quantitative deficit bound is proved here."
+    },
+    {
+      "question": "Can a nonsaturated even-window system produce a favorable complete paid profile on a current complex caller?",
+      "why_it_matters": "The selected complex supplier binds, but the historical PR5282 scaled invoice does not certify a current native supplier.",
+      "first_step": "Specify one concrete line system, its literal decoder and its full current target, paid-child and restoration contract before a search.",
+      "blocked_by": "Native realization, dirty restoration, compiler closure and a complete signed invoice are absent."
+    }
+  ],
+  "coordination": {
+    "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19294714",
+    "question_source": "PR #5282, Open next questions 1",
+    "source_author": "Matarener",
+    "upstream_checked": "2485805a6d47f36ea83ddde6327d453ac82d44dc",
+    "overlap_limitations": "Open PR titles and relevant bodies, latest handoffs and active Discussions, recent account PR bodies, merged searches and main README terms were checked. Search coverage is not a novelty proof."
+  }
+}