Prove fixed common bases cannot improve idle coalescing (no κ)

research/fixed-basis-idle-coalescing/PROOF.md

@@ -0,0 +1,104 @@
+# A fixed independent idle family reduces to coordinates
+
+## Contract
+
+Let F be any field, V=F^n with named coordinate basis e_1,...,e_n,
+and let stages s=1,...,m have coordinate masks M_s contained in {1,...,n}.
+Write U_s=span{e_i : i in M_s}. Fix integers 0<=q_s<=|M_s|.
+
+Choose one basis v_1,...,v_n of V for the entire schedule. A feasible
+allocation chooses J_s contained in {1,...,n}, with |J_s|=q_s and
+v_j in U_s for every j in J_s. Put I_j={s:j in J_s} and d_j=|I_j|.
+Directions are independent globally, not merely separately at each stage.
+A direction's scalar multiple represents the same line. No direction changes
+between its uses. Choosing a different basis for a different allocation is
+allowed. All basis setup, scalar mixing and transport costs are optimistically
+zero. Eligibility uses only the output direction's support, so imposing
+additional right-vector or physical restrictions can only shrink this model.
+
+The coordinate model is the special case v_j=e_j. Its schedules have exactly
+q_s distinct idle coordinates in M_s at each stage. Neither model preserves
+a prescribed HOST action or imposes chronological barriers on coalescing.
+
+## Theorem
+
+For every feasible fixed-basis allocation there is a coordinate allocation
+and a permutation pi of {1,...,n} with
+
+    I'_{pi(j)} = I_j for every j.
+
+In particular, the two models have exactly the same feasible multisets of
+idle stage sets, and exactly the same feasible idle-degree multisets.
+They have the same minimum sum_j f(d_j) for every real-valued function
+f on {0,...,m}. No concavity or monotonicity assumption is needed for
+this equality. More generally any objective invariant under relabeling the
+directions has the same attainable values in both models.
+
+The same reduction holds for a globally independent family of at most n
+directions. Extend the family to a basis and give every added direction
+the empty stage set. The permutation argument then applies to the original
+family as an injection into the coordinate indices.
+
+## Proof
+
+Let B have columns v_j in the coordinate basis. Since det B is nonzero,
+the determinant expansion has a nonzero summand. There is a permutation pi
+such that B_{pi(j),j} is nonzero for every j. A nonzero sum must have a
+nonzero summand over every field, including characteristic two. Thus pi(j)
+belongs to the support of v_j.
+
+If j belongs to J_s, all coordinates in the support of v_j belong to M_s,
+because v_j belongs to U_s. Hence pi(j) belongs to M_s. Set
+J'_s={pi(j):j in J_s}. The permutation is injective, so |J'_s|=q_s,
+and J'_s is contained in M_s. This is a feasible coordinate allocation.
+Moreover pi(j) belongs to J'_s exactly when j belongs to J_s, proving
+the equality of stage sets and of degrees.
+
+This constructs one inclusion of feasible multiset collections. The reverse
+inclusion holds because the coordinate basis is itself an allowed fixed
+basis. Objective equality follows by relabeling. All allocation domains are
+finite at the stage-set level, even when F is infinite, so every nonempty
+set of attainable objective values has a minimum. Coordinate feasibility
+also follows directly from 0<=q_s<=|M_s|. This proves the theorem.
+
+The support-matching fact is classical. Equivalently, every subset of the
+independent columns has support union of size at least its cardinality,
+and Hall's marriage theorem supplies the injection. The new contribution
+is the degree-preserving reduction for this idle-coalescing question.
+
+## Application to the connected eighteen-stage root
+
+CubeJerry's [#7002](https://github.com/CrocSwap/integer-mult-bounds/pull/7002)
+defines a coordinate-role relaxation in
+[IDLE-COALESCING.md](../connected-l18-root-caller/IDLE-COALESCING.md).
+It optimistically allows any two eligible coordinates to be hosted at a stage,
+leaves the other mask coordinates idle, and coalesces all occurrences of a
+coordinate for free. Its costs depend on idle degrees alone. Set
+q_s=|M_s|-2 in the theorem.
+
+Consequently, allowing an arbitrary fixed common basis, or a fixed globally
+independent subset, cannot lower that relaxation's optimum. The predecessor's
+stated coordinate optimum and fixed-profile failure therefore apply to this
+larger subclass as a corollary. This is a new applicability step. The
+predecessor's numerical optimum, transcendental bounds and complete invoice
+are cited premises; this package does not recompute or certify them.
+
+The proof maps optimistic allocations, not physical operators. It need not
+map the HOSTs or retain a source's original endpoint. This causes no gap in
+the lower-bound use: every admitted fixed-basis allocation maps to a feasible
+member of the already optimistic coordinate relaxation. A map in the other
+direction with physical HOSTs would require a separate construction.
+
+## Boundary
+
+Three directions e_1,e_2,e_1+e_2 in F_2^2 are dependent and cannot receive
+distinct coordinate anchors. The matching proof therefore cannot cover
+arbitrary dependent families, even if every individual stage uses independent
+directions. This observation does not prove that dependent directions save
+cost. A basis that changes between stages, changing a direction's identity,
+also falls outside the contract. No theorem about either extension is claimed.
+
+Noncoordinate common bases are thus insufficient on their own. A route
+around this obstruction must change at least one premise, for example use
+dependent directions across the complete schedule, rotate the basis, or
+change masks, idle counts, native profile or the degree-only tariff.

research/fixed-basis-idle-coalescing/README.md

@@ -0,0 +1,127 @@
+# Fixed common bases cannot improve idle coalescing
+
+This contribution is produced by Nick Petalas. Claim type: scoped written
+proof with exact finite corroboration. No new kappa.
+
+For coordinate stage masks over every field, allowing one arbitrary fixed
+common basis gives exactly the same feasible idle-degree multisets as the
+coordinate basis. Match each basis vector to a distinct coordinate in its
+support. Replacing its idle uses by that coordinate preserves every stage
+and every degree. The result also covers fixed globally independent
+subfamilies. [PROOF.md](PROOF.md) gives the contract and proof.
+
+This settles a subclass of the noncoordinate-direction gap in CubeJerry's
+[#7002](https://github.com/CrocSwap/integer-mult-bounds/pull/7002). Its
+coordinate-role idle-coalescing obstruction now applies to arbitrary fixed
+common bases under the same degree-only tariff. The predecessor's coordinate
+optimum and numerical shortfall are cited inputs, not replayed results.
+
+The equality holds for every common function of idle degree, including its
+concave rank-power tariff. It does not require concavity. The theorem does
+not cover dependent direction families, a basis that changes between stages,
+changed masks or idle counts, or a changed native/caller contract. Those are
+possible routes beyond the obstruction, rather than proved improvements.
+
+## Evidence and reproduction
+
+From the repository root, use standard-library CPython 3.12:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/fixed-basis-idle-coalescing/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/fixed-basis-idle-coalescing/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/fixed-basis-idle-coalescing
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/fixed-basis-idle-coalescing --check-source-history
+```
+
+Any CPython 3.12 interpreter may replace that absolute interpreter path.
+The direct marker is `PASS_FIXED_BASIS_IDLE_COALESCING`; the runner also
+reports `PASS_REGISTERED_RESEARCH_PACKAGE`. The verifier writes nothing.
+Each execution emits a generated JSON receipt containing the exact census
+counts and SHA256 hashes of all six package files.
+
+The checker enumerates 85,833 square matrices and checks 31,617 bases and
+1,251,947 eligible stage/subset pairs. Its domains are F2 in dimensions one
+through four and F3 in dimensions one through three. For each basis it compares
+an augmenting-path matching with all supported permutations. It then tests
+every coordinate mask and every eligible subset of directions. A separate
+five-stage noncoordinate fixture checks the complete degree vector. Six
+invalid input controls reject, and two boundary controls expose dependence
+and the need to match within support. Explicit exceptions keep every check
+active under optimized execution. The universal theorem comes from the
+written determinant argument, not extrapolation from these finite domains.
+
+## Scope and provenance
+
+Base is canonical main `e54523517d0f03e58352e647c403a5af3e525a57`, priority
+revision 8. The selected record still names conditional #7000. SOURCES.json
+pins #7002's README and IDLE-COALESCING.md as historical mathematical context.
+They are not executable inputs. The standalone verifier imports no predecessor
+code or data and does not repeat a predecessor census or invoice check.
+TASK.json declares a changed joint-query-controller scope, a local allocation
+obstruction rather than a completed producer/consumer program.
+
+The card's first binding-only command passed. Live open PRs, active
+Discussions, recent account contributions, local claims, merged searches and
+all-main README searches were checked before the
+[CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19540656).
+The cached overlap helper reports incomplete sparse-local coverage; absence
+of a search hit is not a novelty certificate. The related open packages below
+construct normalized schedules; this theorem concerns all fixed globally
+independent families and imports neither schedule nor numerical comparison.
+
+Native implementation, HOST compatibility, paid basis changes, chronological
+transport, dirty restoration, ordinary costs, precision/tape, stock, compiler,
+supplier admission and the full multiplication theorem remain outside scope.
+No numerical frontier, selected files or predecessor files are changed. The
+selected cold replay, Lean, Docker, independent human review and formal proof
+kernel are unrun. The application to #7002 uses its published coordinate
+obstruction as a premise without independently validating that result.
+
+## Related open work
+
+- Rohan Arun's [#7098](https://github.com/CrocSwap/integer-mult-bounds/pull/7098)
+  constructs and prices a noncoordinate projector relocation for #7002.
+  This proof gives a fixed globally independent family obstruction, without
+  recomputing that schedule or its price.
+- Rohan Arun's [#7106](https://github.com/CrocSwap/integer-mult-bounds/pull/7106)
+  extends the normalized projector scheduling work. Its construction enforces
+  compatibility on overlapping intervals. This theorem requires global
+  independence across the whole schedule, a stricter premise. No numerical
+  agreement or disagreement is claimed.
+
+## Open next questions
+
+- Can a globally dependent family of directions lower a fully specified idle
+  bill while each stage still has independent idle directions? Start with
+  three lines in a two-dimensional coordinate space and a short mask sequence.
+  A favorable allocation and the actual paid preparation/restoration are
+  missing. The matching theorem does not decide this case.
+- Can changing the basis between stages improve a complete connected-root
+  caller after paying conversion and HOST compatibility costs? Start with
+  two explicit bases and one transition. No legal conversion or favorable
+  complete bill is supplied here.
+
+Structured relevance, first steps and blockers appear in TASK.json.
+
+## Credit and engineering
+
+Credit CubeJerry, Jerry Chen, #7002 for the connected-root question and
+coordinate coalescing relaxation; DreamingOfClouds #6937 for the connected
+mask lineage, and the retained #6936/#6912 native/root authors. The support
+matching fact is classical determinant expansion or Hall matching. The new
+step is its stage-set-preserving application, not the predecessor optimum.
+Independent human and formal proof-kernel review are unclaimed. Apache-2.0.
+
+The investigation playbook guided the work. Build the Lever supplied a
+standalone checker; Prove It Works required all eligible stage subsets and
+the chronological degree fixture. Power of Ten bounds dimensions by four,
+fields by three, matching paths by dimension, and census domains explicitly.
+All functions have fewer than sixty lines and there is no recursion, dynamic
+code execution, subprocess, network or shared mutable state. Python allocation
+is a managed-runtime deviation: matrices have at most sixteen entries,
+permutation lists at most twenty-four entries and vector tables at most
+eighty-one entries under the enforced entry-point caps. Runtime allocator
+internals are not inspected. Receipt files are limited to 128 KiB each.
+Warning-strict normal and optimized commands are registered diagnostics.
+Ruff and mypy were unavailable on PATH. No repository-wide diagnostic policy
+was changed for this isolated package.

research/fixed-basis-idle-coalescing/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8",
+      "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/connected-l18-root-caller/IDLE-COALESCING.md",
+      "usage": "provenance",
+      "git_blob": "91df672c3d5f4b56321e7b07ad98f011949484e3",
+      "sha256": "ba9d8e2caf41b18352e01edc69a3a47c1e1385f6b4ae3b2ab8c681b3bd44f5ad"
+    },
+    {
+      "path": "research/connected-l18-root-caller/README.md",
+      "usage": "provenance",
+      "git_blob": "6ef3bae7d8fb6081f7c6441d04a5d929cbd7016b",
+      "sha256": "349341634d97c3f105bdc5003de1a2e7252a31fc52e25dc7bdfd39550586ccbd"
+    }
+  ]
+}