Construct border controllers without idles and bound recovery costs (no κ)

research/controller-border-interface/BUDGET.md

@@ -0,0 +1,154 @@
+# What deleting the idle stages can and cannot save
+
+This is a bound for the stated changed controller model, not a bound for every
+native word or multiplication algorithm. The local helper and paid inventories
+are frozen to Cinna Davis's #4470 and the retained query-thinned BIT invoice.
+Changing those inventories, the number or nature of the main outputs, or the
+central-query alphabet changes this model.
+
+## A determinant invariant survives a scalar border
+
+Work over the commutative Laurent ring in independent `Q,D_0,...,D_(2p)`.
+Every shear and bridge has determinant one. A full stage multiplies exactly
+two main roles by its `D_s`; a thin query contributes no `D_s`. Signed swaps
+have determinant one. Thus, for one port of the controller with no idles,
+
+    det A = product(s full) D_s^2.
+
+There are `p+2` full stages, also when `p=1`. This determinant is a formal
+identity; no numerical specialization or field-character evaluation is used.
+
+Allow any invertible scalar matrices `L(e),R(e)` over the rational-function
+field in an auxiliary parameter e, independent of Q and the D variables.
+Suppose `L(e) A R(e)` has a finite, full-rank limit which is diagonal with
+monomial entries. Its determinant is
+
+    det L(e) det R(e) product D_s^2.
+
+The full-rank limiting determinant forces the scalar factor to have a finite
+nonzero limit. Hence the product of the limiting monomials has exactly the
+same D degrees. In the source-compatible target model, each of the `2p` main
+outputs has one central rank-one factor `Q` or `Q^-1`, and a product of fresh
+stage factors with nonnegative degrees. Its credited rank is
+`1+b*(number of stage factors)`, where b is 8 for complex or 7 for BIT.
+Consequently the total main rank at v ports is necessarily
+
+    M_p = 2v[p+b(p+2)].
+
+This argument does not allow canceled positive and negative D degrees to earn
+extra rank. Nor does it cover mixing the helpers into a different target
+family: helpers here remain the separately productive native outputs. Allowing
+any distribution of this total mass is already more favorable than requiring
+integer ranks, individual stage-degree feasibility, or the actual triangular
+controller's diagonal. For BIT this is a formal Laurent invariant before
+physical scalar-extension admission, not a claim that the native involutive
+representation has unique Laurent exponents.
+
+The actual diagonal in [DISCOVERY.md](DISCOVERY.md) has, for p>=2, four v-field
+groups of rank `1+2b` and `2(p-2)v` fields of rank `1+b`. At p=1 it has `2v`
+fields of rank `1+3b`. At complex p16 the discarded idle mass is 141,568:
+main output mass falls from 177,408 to 35,840. The same rank-mass surplus 752
+remains. Deleting the bill while retaining the old targets is therefore invalid.
+
+## An all-p optimistic ceiling, even with free extraction
+
+Let `t=1-C`, with `0<=C<=1`. Write H(t) and P(t) for the *local* productive
+helper and paid moments, and `h(t)=H(t)-P(t)`. The complete changed controller
+has `p+2` copies of both inventories and `v(p-1)` paid rank-one thin queries.
+Its optimistic surplus moment after any allowed redistribution of main ranks
+is, by concavity of `x^t`, at most
+
+    J_p(t) = (p+2)h(t) - v(p-1)
+             + 2vp [1+b+2b/p]^t.
+
+The tangent bound at `u=1+b` gives
+
+    J_p(t) <= p A(t) + B_J(t),
+    A(t)   = h(t) - v + 2v(1+b)^t,
+    B_J(t) = 2h(t) + v + 4vbt(1+b)^(t-1).
+
+The exact checker encloses the required rational powers by integer nth-root
+comparisons on a 48-bit dyadic grid. It proves both A and B_J strictly negative
+at C=.006 for complex and C=.007 for BIT. Approximate values are shown only
+for readability; `RESULT.json` contains the exact rational enclosures.
+
+| Inventory | C | A upper bound (rounded here) | B_J upper bound (rounded here) |
+|---|---:|---:|---:|
+| Complex #4470 | .006 | -2.6366097977 | -132.6282065737 |
+| Retained BIT | .007 | -3.5731057048 | -133.1717283852 |
+
+These inequalities exclude every positive integer p. The checker separately
+rejects the declared target C=.01 and verifies the actual p=1 exception.
+
+To extend the exclusion to every larger saving, combine equal-rank terms in
+h. All its positive terms lie above rank 6 in complex, and above rank 15/2
+in BIT; every negative term lies below that separator. The Jensen main base
+`1+b+2b/p` also lies above it, while the paid thin query lies below it.
+Dividing the *unlinearized* J_p(t) by separator^t makes every nonconstant
+signed summand increasing in t. Thus J_p(t)<0 at the cutoff implies J_p(t)<0
+for every smaller t in [0,1]. We do not require the tangent intercept to be
+monotone. This proves the fixed-model necessary bounds
+
+    C < .006 (complex),       C < .007 (BIT).
+
+No positive supplier is admitted by this argument. Even a positive formal
+moment must still pay for extraction, native scalar implementation, matching,
+precision and all compiler/outer obligations.
+
+The actual diagonal gives an affine surplus `p A(t)+B(t)` for p>=2, where
+
+    B(t) = 2h(t)+v+4v[(1+2b)^t-(1+b)^t].
+
+This independently agrees with explicit profiles at checked small and large p.
+Positive controls at complex `(p,C)=(32,.005)` and BIT `(64,.006)` ensure that
+the necessary moment checker is not simply rejecting every candidate. These
+are formal invoices only. Omitting the paid thin queries incorrectly makes
+the C=.01 test pass; the checker records that diagnostic undercharging fault.
+
+## Repeated whole-controller extraction loses even with fresh helpers
+
+Suppose a conversion evaluates the entire changed controller K>=2 times.
+Grant each evaluation its own independent productive helper inputs and keep
+all those helper outputs. Only the main inputs are copied and combined, so
+their target inventory is credited once. The most favorable corresponding
+surplus is
+
+    main(t) + K[(p+2)h(t)-v(p-1)].
+
+At t=1 and K=2 its rank-mass margin is exactly
+
+    complex: -1920p-3616,       BIT: -1680p-3138.
+
+For any redistribution of main ranks allowed above, Jensen bounds their moment
+by `2vp(1+b+2b/p)^t`. Dividing this envelope by the same rank separator makes
+it increasing in t. Its negativity at t=1 therefore implies negativity for
+every t in [0,1]. Also h(1)=-1856 complex and -1617 BIT; the same normalized
+monotonicity proves h(t)<0 throughout [0,1]. Each additional evaluation makes
+the bill worse. Thus this repeated-whole-unit policy fails at every concave
+moment, even granting free interpolation, routing and scalar operations.
+
+Fresh helpers matter: they are legitimate independent productive inputs, not
+copies. The checker retains their full credit. Its duplicate-main fault
+instead credits the *same* main outputs twice: at p=2,t=1 that invalid bill
+reports +160 complex or +162 BIT, while the correct bill is -7456 or -6498.
+This is an ownership distinction, not a numerical interpolation estimate.
+
+This obstruction does not cover exactification sharing paid calls between
+evaluations, using extra independent main outputs, changing the native word,
+or exploiting a different amplification theorem. [EXACTIFICATION.md](EXACTIFICATION.md)
+states why a polynomial-overhead claim for the inherited chronological product
+needs a new proof.
+
+## Decision
+
+The original symmetric C>.01 ambition is rejected for this fixed native
+inventory and output contract, including the favorable redistribution above.
+Increasing p or optimizing the same scalar filtration cannot meet it. The
+explicit border remains a possible new interface, but a construction campaign
+must first fund its recovery. A future target above .01 needs a changed native
+paid/helper profile, a different output contract, or a different controller
+query alphabet. This is a scoped stopping result, not a universal barrier.
+
+Prepared by Dillon with substantial OpenAI Codex assistance. Apache-2.0.
+Credit Cinna Davis, zxv, Jacob Alan Sussman and the source native/compiler
+lineage; Matarener's #4602 identified the large idle bill that motivated this test.

research/controller-border-interface/DECODER.md

@@ -0,0 +1,165 @@
+# Exact copied-input correction: a losing full-rank test
+
+The no-idle controller in [DISCOVERY.md](DISCOVERY.md) has X-block
+
+```
+X' = Q^-1 U x,
+U = (I-S) D + S,
+D = diag(d_0,...,d_(p-1)),
+S_ij = (-1)^(j-i-1) for i<j, and zero otherwise.
+```
+
+Let J have ones immediately above its diagonal and zeros elsewhere. Since
+J^p=0,
+
+```
+S = J(I+J)^-1,       I-S = (I+J)^-1.
+```
+
+The following copied-input correction is exact for every p and every input:
+
+```
+z = (I+J) X' - Q^-1 J x = Q^-1 D x.
+```
+
+Coordinatewise, `z_i = X'_i + X'_(i+1) - Q^-1 x_(i+1)` for i<p-1,
+and `z_(p-1)=X'_(p-1)`. It needs the original input values; using the updated
+outputs in their place is invalid.
+
+## Rank is forced in this explicit correction model
+
+Fix one port and consider only corrections of the form
+
+```
+z = M X' + Q^-1 N x,
+```
+
+where M,N are constant rational matrices, independent of the separate formal
+variables d_j, and require the exact endpoint `z=Q^-1 D x` for arbitrary x.
+Comparison of each independent coefficient d_j forces
+
+```
+M(I-S) = I.
+```
+
+Thus M is uniquely `(I-S)^-1=I+J`. The constant coefficient then forces
+
+```
+N = -MS = -J.
+```
+
+Consequently `rank(N)=p-1`. The statement also holds over F2 with signs
+reduced, although it supplies no physical scalar-extension theorem.
+
+If each fresh Q query accepts one scalar linear combination of the copied
+inputs and returns its Q transform, while constant scalar maps prepare and
+combine queries, q such queries produce a correction matrix of rank at most q.
+Therefore q>=p-1 in this specified model. Querying each `x_(i+1)` achieves the
+bound. This is a lower bound for fresh rank-one Q-query corrections with a
+constant output map; it does not cover reuse of retained internal queries,
+changes to the original word, more general operator-valued adapters or all
+possible physical decoders. Multiplying the count by 112 or 111 below assumes
+the correction is performed separately on each port. The lower bound does
+not exclude a joint cross-port native operation or sharing between ports.
+
+## Complete logical correction bill and p16 rejection
+
+A literal forward implementation can copy the p-1 raw inputs to owned scratch
+before running the controller, apply one Q^-1 job to each saved field, and
+update the outputs in increasing i. Increasing order preserves each still-needed
+`X'_(i+1)`. It then erases the scratch. Per port the added correction ledger is:
+
+| Item | Count | Status and scope |
+|---|---:|---|
+| Extra recursive rank-one Q jobs | p-1 | Exact in the stated fresh-query model |
+| Copies of raw fields into owned storage | p-1 | Explicit logical COPY; physical movement requires its native contract |
+| Scalar additions/subtractions | 2(p-1) | Explicit above; coefficient sizes are one |
+| Simultaneously retained owned fields | p-1 | No productive input credit |
+| Final scratch erasures | p-1 | Explicit; owned-erasure premise retained |
+| Physical routes, entry/exit matching, precision | Unknown | Not assigned zero |
+| Y-block exactification | Unknown | Additional to this X-only bill |
+
+With 112 complex ports and p=16, the X correction alone adds **1,680** paid
+rank-one jobs to a formal rank-one surplus of **752**, producing surplus
+**-928** before any Y correction or other new charge. This is already
+unfavorable at exponent one. The cumulative certificate below strengthens
+this to every concave moment in this specific correction model.
+
+More generally, the complex X-corrected rank-one surplus in this model is
+
+```
+48(p+2)-112 -112(p-1) = 96-64p,
+```
+
+which is negative for every p>=2. The BIT analogue is `96-63p`, also negative
+for p>=2. A claimed complete construction using this fresh-query correction
+must therefore address the failed rank-one criterion rather than inherit the
+uncorrected border's surplus. This test prices actual eliminated idle work and
+an actual replacement, and rejects that replacement in the stated source
+compiler's positive-surplus admission route.
+
+## All concave moments fail in this correction model
+
+Let T_r be the actual formal border targets and let P_r include the p-1 fresh
+X-correction queries per port. Define
+
+```
+A_r(p) = sum(k<=r) k(P_k-T_k).
+```
+
+All counts are affine in p for p>=2. The following exact values give
+`A_r(p)=base+slope*(p-2)` at every support threshold:
+
+| Complex rank r | Base at p=2 | Slope |
+|---|---:|---:|
+| 1 | 9172 | 2461 |
+| 2 | 12276 | 3237 |
+| 3 | 18204 | 4719 |
+| 4 | 20108 | 5195 |
+| 5 | 20828 | 5375 |
+| 7 | 20632 | 5326 |
+| 8 | 19384 | 5014 |
+| 9 | 7648 | 64 |
+| 17 | 32 | 64 |
+
+| BIT rank r | Base at p=2 | Slope |
+|---|---:|---:|
+| 1 | 5514 | 1545 |
+| 2 | 16250 | 4229 |
+| 3 | 17198 | 4466 |
+| 4 | 17902 | 4642 |
+| 5 | 19942 | 5152 |
+| 6 | 20206 | 5218 |
+| 7 | 20738 | 5351 |
+| 8 | 6690 | 63 |
+| 15 | 30 | 63 |
+
+Every base and slope is positive. For 0<t<=1 the function f(r)=r^(t-1) is
+positive and nonincreasing. Discrete summation by parts, with R the maximum
+rank, gives
+
+```
+P_t-T_t = A_R(p) f(R)
+          + sum(r=1..R-1) A_r(p) [f(r)-f(r+1)] > 0.
+```
+
+Missing thresholds have the same cumulative value as the preceding listed
+one. Thus this exact fresh-query X correction alone destroys every favorable
+concave moment, on both suppliers, for every p>=2. Additional Y corrections
+and physical charges cannot repair that inequality unless the construction or
+the target interface also changes. This conclusion remains restricted to the
+specified fresh-query correction model.
+
+`border_algebra.py` checks the geometric-series identities and exact ranks
+for p=1,...,8, rejects deletion of a required query, and reconstructs every
+base and slope in the all-moment certificate from the pinned source profiles. These finite checks
+support the stated symbolic proof; they are not a general native-query lower
+bound or an independently reviewed multiplication theorem.
+
+## Open next questions
+
+Do the p-1 already-paid thin queries expose the required raw `Q^-1 x_(i+1)`
+values at a usable chronological cut, with legal retention and restoration?
+The current source interfaces do not grant those values. An explicit reused
+query/consumer contract would change the lower-bound hypothesis and is the
+smallest concrete route to reopening this exact correction strategy.