Bound dense cross-port thin-query capacity at 528 requests (no new κ)

research/cross-port-thin-capacity/PROOF.md

@@ -0,0 +1,119 @@
+# Cross-port information capacity for the thin-query pool
+
+This is a scoped proof. The general ingredient is classical linear information
+dimension. The repository's outside-input rank probe already states the fixed-
+observation quotient formula; its centre-nonlinear-fresh-floor package applies
+dimension arguments to a different centre history. The new claim here is the
+conditional cross-port thin-pool capacity constraint and its 528-request
+consequences below. It proposes no physical primitive.
+
+## Observation contract
+
+Let K be any field. The input x ranges over the whole finite-dimensional space
+X. A row of X* is a scalar linear observable. Initially the consumer knows all
+observations in a subspace F of X*. It must return all observations in T.
+
+A request returns at most c scalar linear observations of x. Its rows may depend
+on previously observed values, including the initial free observations. Each
+request's rows are fixed once that previous transcript is fixed. Free computation,
+mixing across ports, feedback, and final decoding may be arbitrary deterministic
+functions of the known transcript. They reveal no additional information about x.
+There is no hidden input-dependent control channel. Every execution is finite.
+
+The capacity c counts scalar output coordinates. It is neither a native frame
+rank nor the number of ports with a nonzero coefficient. A field response with
+several independently readable coordinates is a vector response and must be
+charged for those coordinates. Correlated or restricted inputs are outside X.
+
+## Theorem 1: capacity on every successful transcript
+
+Put D = dim(F + T) - dim F. Every protocol correct for every x has, on every
+execution, total returned scalar capacity at least D. A sharper statement uses
+the rank of the actual returned rows modulo F, which must be at least D.
+
+Proof. Fix an execution on x, and collect its actual query rows in Q. Suppose
+there is h in ker F intersect ker Q with T h nonzero. The execution on x+h has
+the same initial transcript. Inductively, each request chooses the same rows
+and returns the same values, so it also makes the same control decisions and
+stops with the same decoder output. Its required answer differs by T h. This
+contradicts correctness. Thus ker(F + Q) is contained in ker T. By finite-
+dimensional duality, T is contained in F + Q. Therefore
+
+    D <= dim(F + Q) - dim F <= number of returned scalar coordinates
+      <= sum_j c_j.
+
+This argument permits nonlinear decoding and data-dependent query selection.
+Randomness with a correctness guarantee for every fixed random tape can be
+fixed first. No claim is made about bounded-error randomized protocols.
+
+The bound is sharp in this abstract oracle contract. Choose D target rows
+complementing F inside F+T, request them, and reconstruct every target using F.
+Group the D rows into packets of the declared capacities when their total is
+at least D. This is an information-theoretic upper bound. It does not show
+chronological availability or physical implementation of these queries.
+
+## Theorem 2: independent ports and extra free information
+
+For P independent port inputs X_p, suppose free and target rows are port-local
+and F = direct_sum F_p, T = direct_sum T_p. Then
+
+    D = sum_p [dim(F_p + T_p) - dim F_p].
+
+This follows by taking dimensions of direct sums. Theorem 1 permits every query
+row to mix all ports, so it is stronger than summing bounds for protocols
+restricted to port-local requests. An invertible linear change of all input
+coordinates preserves the dimensions. Relabeling or mixing ports cannot
+replace P independent inputs with one correlated input.
+
+If an additional free observation space S is supplied, the exact oracle
+minimum becomes D_S = dim(F + S + T) - dim(F + S). The dimension formula gives
+
+    D_S >= D - [dim(F + S) - dim F].
+
+Consequently, reducing the necessary scalar capacity by k needs at least k
+new independent free observations modulo F. This lower bound is sharp by
+choosing S inside a complement of F in F+T. Where those observations come from,
+and what they cost, are separate physical questions.
+
+## Conditional application to the reported thin-query deficit
+
+Matarener's [PR #5996](https://github.com/CrocSwap/integer-mult-bounds/pull/5996),
+head `47242572d3b22ce49371245edc561dd75bf263e8`, reports a one-port quotient
+dimension of fifteen for the retained p16 controllers. Its README at that
+head defines the scalar specialization and credits the controller lineage.
+That reported quotient dimension is an explicit premise here. Its computation
+is not rerun, and no scientific acceptance of that predecessor is claimed.
+
+If P independent copies of that observation contract are required, Theorem 2
+gives D = 15P. Thus 104 ports require total scalar capacity 1560 and 112 ports
+require 1680, even with dense cross-port encoding, arbitrary joint decoding and
+adaptive feedback as defined above. The atlas's 528-request target therefore
+requires the following output capacities.
+
+- At 104 ports, capacity at most two per request is insufficient. If every
+  request has capacity at most three, at least 504 of the 528 requests must
+  have capacity three. The remaining 24 can have capacity two. These capacities
+  sum to 1560. With fewer than 528 requests the necessary count of capacity-three
+  requests can only increase, until it is infeasible.
+- At 112 ports, capacity at most three per request is insufficient. If every
+  request has capacity at most four, at least 96 of the 528 requests must have
+  capacity four. The remaining 432 can have capacity three. Their total is 1680.
+- If all requests remain scalar, meeting 528 needs at least 1032 new free
+  dimensions at 104 ports, or 1152 at 112 ports, beyond the cited free span.
+
+For the first two statements, if n requests have maximum capacity r, their
+total capacity is at most (r-1)*528+n. Solve this necessary inequality for n.
+The displayed distributions attain equality only as abstract output budgets.
+They are not causal controllers or invoices. In particular a rank-r native
+job has not been proved to deliver r scalar observations at the desired price.
+
+## Scope of the obstruction
+
+The new exclusion is for scalar or capacity-limited observations on independent
+port inputs. A channel supported on all ports can still return only one scalar.
+A channel exposing an entire port vector can have large capacity and is not
+excluded. Restricted input families, new paid full outputs, changed target
+relations, input-dependent side channels and approximate recovery require
+different hypotheses. The proof does not identify native frame rank with
+information capacity. No physical execution, complete paid moment, compiler,
+stock, precision, tape tariff, all-size admission or new kappa is supplied.

research/cross-port-thin-capacity/README.md

@@ -0,0 +1,98 @@
+# Dense port mixing does not reduce scalar thin-query information
+
+Claim type: scoped mathematical proof with exact finite corroboration. No new
+kappa or selected-frontier change.
+
+The [proof](PROOF.md) extends a port-local information deficit to arbitrary
+linear queries mixing independent ports, with adaptive query selection and
+arbitrary deterministic decoding. If each port needs fifteen dimensions beyond
+its free information, P ports need total returned scalar capacity at least 15P.
+Touching many ports with one scalar response does not increase its capacity.
+
+This builds on Matarener's [PR #5996](https://github.com/CrocSwap/integer-mult-bounds/pull/5996),
+exact head `47242572d3b22ce49371245edc561dd75bf263e8`, and its question about
+cross-port channels. The reported per-port deficit is cited as a premise. This
+package does not replay or validate it. The linear information principle is
+classical; the new contribution is the cross-port observation contract and its
+conditional thin-pool capacity constraints. The repository's
+[outside-input rank probe](../outside-input-research-targets/README.md) already
+states the fixed-observation quotient formula. Matarener's
+[nonlinear centre floor](../centre-nonlinear-fresh-floor/README.md) covers a
+different history and continuous or semialgebraic fresh encoders. Neither is
+replayed here, and neither source's general dimension principle is claimed new.
+
+For 528 requests on 104 independent ports, scalar capacity two is insufficient;
+with capacity at most three, at least 504 requests need capacity three. For 112
+ports, capacity three is insufficient; with capacity at most four, at least 96
+requests need capacity four. Keeping every request scalar instead requires at
+least 1032 or 1152 additional free dimensions respectively.
+
+These are necessary information budgets, not physical schedules. Scalar output
+capacity is explicitly different from native frame rank. Binding the actual
+multi-port data and its free operations to this contract remains an obligation.
+An entire independently readable output vector is charged by its coordinates.
+
+## Reproduce
+
+From the repository root, with CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/cross-port-thin-capacity/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/cross-port-thin-capacity/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/cross-port-thin-capacity
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/cross-port-thin-capacity --check-source-history
+```
+
+The standalone verifier needs no Git, network or predecessor source. It
+enumerates all triples of binary free/query/target subspaces in dimensions zero
+through four. Through dimension three, a separate literal input-fiber oracle
+checks whether any lookup-table decoder exists. Rational recoding and
+side-information fixtures, adaptive decision trees, packet arithmetic, and
+semantic/boundary controls corroborate the written proof. The universal theorem
+rests on that proof, not these finite examples. `--receipt PATH` writes a new
+receipt bound to package file hashes outside the package.
+
+The run enumerates 304,993 subspace triples and makes 4,230 independent fiber
+comparisons. It also checks 116 rational fixtures, 510 complete adaptive
+transcripts, 255 ambiguous shortened transcripts, four semantic controls and
+four invalid-input rejections. Normal and optimized commands each completed
+locally in under one second; these are replay-budget observations, not speedups.
+
+## Verifier bounds
+
+No recursive code, solver, subprocess, network access or hidden input is used.
+The largest subspace census has 67 spaces, 4489 pair joins and 67 cubed triples.
+Binary vectors have at most eight bits, spans at most 256 elements, and rational
+matrices at most 32 rows by 16 columns. Adaptive trees enumerate at most 256
+inputs per dimension. Every function is below sixty lines. Invariants use
+explicit exceptions and stay enabled under optimization. The four indirect
+control calls have a fixed, visible target list. Source hashing reads six files
+of at most one MiB each. The optional receipt is created exclusively.
+
+Power-of-Ten rule 3 deviation: Python's managed objects and Fraction arithmetic
+allocate during verification, so fixed allocation after initialization is not
+claimed. The finite dimensions above bound live collections and integer sizes;
+there is no unbounded input arithmetic. The compensation is checked by the
+boundary controls and both registered executions. A larger-input verifier must
+declare new bounds before extending these constants. Rule 10 uses warning-strict
+normal and optimized replay; no separate Python static analyzer is configured
+for this isolated package.
+
+## Open next questions
+
+- Can a physical thin query deliver enough independently readable coordinates
+  to meet the capacity distribution above at a favorable complete cost? First
+  specify its input/output maps and native frame tariff. Physical realization,
+  dirty restoration and causal availability are unproved.
+- Do the actual port data and every allowed free operation admit the independent
+  direct-sum observation model? First give the input-coordinate and free-span
+  maps. This package does not establish that application premise.
+- Can a changed producer supply the required new free information more cheaply
+  than the omitted scalar requests? First price one new independent observable,
+  including its later consumption and restoration. No such producer is supplied.
+
+The proof and verifier were produced by Nick Petalas. Credit Matarener for the
+per-port deficit and question, Cinna Davis for the controllers, Ali Romman for
+the direct-controller construction, Dugongue for the target atlas, and the
+predecessor lineage retained in PR #5996. Independent human and formal
+proof-kernel review are unclaimed. Apache-2.0.

research/cross-port-thin-capacity/SOURCES.json

@@ -0,0 +1,18 @@
+{
+  "schema_version": 1,
+  "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    }
+  ]
+}