diff --git a/research/controller-border-interface/BUDGET.md b/research/controller-border-interface/BUDGET.md new file mode 100644 index 0000000000..e58271a614 --- /dev/null +++ b/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. diff --git a/research/controller-border-interface/DECODER.md b/research/controller-border-interface/DECODER.md new file mode 100644 index 0000000000..1d656c2279 --- /dev/null +++ b/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=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 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. diff --git a/research/controller-border-interface/DISCOVERY.md b/research/controller-border-interface/DISCOVERY.md new file mode 100644 index 0000000000..745cf3dfa6 --- /dev/null +++ b/research/controller-border-interface/DISCOVERY.md @@ -0,0 +1,214 @@ +# An explicit no-idle border controller + +The ambitious question was whether the controller can eliminate its entire +whole-idle invoice, which the contemporaneous #4602 planning screen identifies +as roughly 56–59% of the paid moment. Deleting those calls and retaining their +productive credit is invalid. The actual controller below loses precisely the +corresponding productive rank mass. It nevertheless has an explicit diagonal +border with a better *formal* moment. This is a changed interface, not another +frame-lattice search. Its conversion to a paid exact supplier is a separate +obligation; the calculations here do not establish a new multiplication bound. + +The construction uses the no-idle event word of +`research/kappa-rebuild/bit/complex_controller_factor.py`, followed by the +query thinning in `research/query-thinned-controllers/controller.py`. The local +native contract remains the source one. The formal variables commute; they +are not evaluated at Fourier characters or treated as involutions over Q. +The source authors are zxv and Cinna Davis with the controller and native +predecessor chain retained in those packages. + +## Exact all-pairs formula + +Take p >= 2 pairs `(X_j,Y_j)`, indexed 0 through p-1. Retain full native stages +`0,1,3,...,2p-1,2p`; replace every other local stage by the credited paid query +shear. Delete every whole IDLE event. Keep every bridge and final signed swap. +There are p+2 full native calls and p-1 queries per port. Define commuting units + +``` +d_0 = D_0 D_1, +d_j = D_(2j+1) (0 < j < p-1), +d_(p-1) = D_(2p-1) D_(2p). +``` + +The resulting matrix A has no mixed X/Y blocks. Its X block is `Q^-1 U` and +its Y block is `Q V`, where + +``` +U_ii = d_i, +U_ij = (-1)^(j-i-1) (1-d_j) (i < j), +U_ij = 0 (i > j), + +V_ii = d_i, +V_ij = (-1)^(i-j-1) (product(k=j..i-1) d_k) (1-d_i) (i > j), +V_ij = 0 (i < j). +``` + +For p=1, the original F/B/F triple is already diagonal with +`d_0=D_0 D_1 D_2`. All these formulas have integral coefficients and therefore +reduce coefficientwise modulo two. That reduction checks the formal algebra; +it does not supply the physical BIT scalar-extension implementation. + +### Derivation from the actual chronology + +Let x_j,y_j denote the original input values. After a pair's backward stage, +its two bridges and its forward stage, but before the reverse chain of bridges, +write the pair values as a_j,b_j. Direct substitution of the source shear +formulas gives + +``` +a_j = -Q d_j y_j - d_j a_(j-1), a_-1=0, +b_j = Q^-1 (d_j x_j + x_(j+1)) (j < p-1), +b_(p-1) = Q^-1 d_(p-1) x_(p-1). +``` + +For j=0 the initial forward stage makes the backward-stage X value +`-Q D_0 D_1 y_0`. For an interior pair, the preceding two bridges present +`Y_j = y_j + Q^-1 x_j + Q^-1 a_(j-1)` to its backward stage; this gives the +recurrence for a_j. The same pair's thin forward shear and bridge update give +the displayed b_j and prepare the next Y input. At the final pair, the last +full forward stage multiplies both outputs by D_(2p), giving the last d_j. +This proves the recurrence by induction through the source events. + +The reverse bridge chain, in decreasing j, changes the X values to +`a_j+a_(j-1)` and the Y values to +`b_j-b_(j+1)+b_(j+2)-...`. The final signed swap therefore returns + +``` +X'_j = sum(k=j..p-1) (-1)^(k-j) b_k, +Y'_j = -(a_j+a_(j-1)). +``` + +Substitution of the recurrence proves U and V term by term. Setting all +formal variables to one gives A(1)=I. Thus no additional constant +normalization is required in this example. In particular, a claimed control +that omits A(1)^-1 would be vacuous and is not counted as evidence. + +## An explicit filtration + +Put `w(X_j)=j` and `w(Y_j)=p-1-j`, and let E(epsilon) be the diagonal matrix +with entries `epsilon^w`. In + +``` +B(epsilon) = E(epsilon)^-1 A E(epsilon), +``` + +an entry at row i, column j acquires exponent `w(j)-w(i)`. Every diagonal +entry has exponent zero; every nonzero off-diagonal entry has positive exponent. +Consequently B is a polynomial in epsilon of degree exactly p-1, and + +``` +B(0) = diag(Q^-1 d_0, Q d_0, ..., Q^-1 d_(p-1), Q d_(p-1)). +``` + +All local helper outputs remain the source's separate diagonal productive +operators when the epsilon wrappers act only on main fields. This statement +uses the full arbitrary-input native endpoint contract. It does not grant +productive credit to owned interpolation copies or fresh scratch. + +`border_algebra.py` independently builds this closed formula and compares every +Laurent coefficient with the literal source emitter for p=1,...,8. The source +emitter is loaded by extracting only its three pure polynomial functions; +source imports, unrelated verification code and external files are not executed. +The checker also verifies A(1)=I, the exact border degree, integral coefficients, +wrong-backward-sign rejection, and rejection of reversed scaling weights. + +## The actual formal invoice + +For p>=2, per port the diagonal has four rank `1+2b` fields and `2(p-2)` rank +`1+b` fields, with b=8 for the complex source and b=7 for BIT. It has p+2 copies +of the source's local productive helpers and local paid jobs, plus p-1 paid +rank-one queries per port. There are no whole-idle paid jobs. The rank-one +surplus is still `48(p+2)-ports`: deleting idle work also deletes its productive +rank mass. No new rank mass has been created by a singular limit. + +For complex p16, the resulting *formal border* profiles are + +``` +T = {4:504, 7:126, 8:846, 9:9004, 17:448}, +P = {1:41946, 2:6984, 3:8892, 4:2646, 5:648, 8:144}. +``` + +Their rank masses are 98,318 and 97,566, leaving surplus 752. The original +#4470 main target mass was 177,408; the removed idle mass was 141,568; the new +main target mass is 35,840. Keeping the old 177,408 would be an unearned credit. + +Exploratory floating-point moment roots (not certified endpoints) are: + +| p | Complex formal border root | BIT formal border root | +|---|---:|---:| +| 2 | 0.002118505300 | 0.002463371003 | +| 4 | 0.003220993919 | 0.003716919894 | +| 8 | 0.004162555165 | 0.004785768721 | +| 16 | 0.004822180518 | 0.005533618177 | +| 32 | 0.005222843492 | 0.005987486573 | +| 64 | 0.005445483624 | 0.006239566631 | + +The checker recomputes every p=1,...,64 and also a favorable relaxation that +balances the same main target mass across all 2p ports. At p16 that relaxation +has complex root approximately 0.004855075634, so this topology cannot plausibly +supply the original >0.01 ambition merely by balancing these main ranks. +That explicit limitation is part of the outcome. If exactification can preserve +the formal moment asymptotically, removing the idle requirement would still be +a qualitative new compiler interface. We do not rebrand its roughly 60% p16 +formal headroom as the more ambitious factor-three target. + +## Costs that must be paid before using the border + +The inverse epsilon powers in the input/output wrappers prevent executing the +limit by setting epsilon to zero. A valid conversion must construct a finite +exact algorithm, count every evaluation of the native word, retain all separate +arbitrary productive inputs, and charge copying, combination, scalar coefficients, +owned storage and eventual erasure. Conditioning and bit precision must follow +the actual interpolation nodes and tensor power. + +Over characteristic two, evaluation may require a finite extension or another +coefficient-extraction representation. Its coordinate expansion, copies, scalar +linear maps, and return to ordinary BIT must be explicit. A characteristic-zero +argument is not a proof of that conversion. Any tensor amplification must use +an allowed product of the actual operator word rather than silently replacing a +product of sums by a tensor of a chosen endpoint. Native matching, the mixed +compiler, ordinary BIT conversion and every outer cost row remain obligations. + +## Open next questions + +Can one prove a fully charged border-to-exact theorem for these mixed-target +native words, with only subexponential overhead under a legal amplification? +The first test is exact coefficient extraction for the p2 polynomial, including +all borrowed/owned fields and both orientations. A positive algebraic identity +alone does not close that question. A negative moment after charging extraction +must stop a dependent construction round or force a genuinely different +interface or topology. + +### The chronological-product obstacle + +The source moment-product theorem is not the ordinary tensor product of the +whole endpoint matrix. It pauses parallel U copies at every paid position and +runs V on their current requested fields. Its proof uses the exact diagonal +endpoint of V before resuming U. Replacing V by a polynomial with off-diagonal +errors inserts new cross-copy errors at every such position. Correctness modulo +epsilon can survive, while polynomial degree may grow with the expanded +chronological program rather than linearly in the number of product levels. +Therefore the familiar linear-degree interpolation argument for a tensor power +is not available merely from the degree-p-1 raw border. + +One possible invariant would use a compatible global filtration on every +suspended field and owned bank. It must prove that errors cannot move down in +an outer role while moving up in an inner role. Without such compatibility, +lexicographic weights can grow exponentially and erase the hoped-for moment +gain. No such invariant is proved here. + +There is also a simple losing exact-correction route. Let S be strictly upper +triangular with `S_ij=(-1)^(j-i-1)` for i=2`. +The helper block is independent of epsilon. The inverse powers in the +conjugation prevent executing the word by substituting epsilon zero. + +Over a characteristic-zero field, choose `d+1` distinct nonzero rational +nodes `a_0,...,a_d`. Define + +``` +lambda_j = product over i != j of (-a_i)/(a_j-a_i). +``` + +Lagrange interpolation gives the exact operator identity + +``` +D = sum_j lambda_j C(a_j). +``` + +This is a construction only when the interface permits copying each original +input to owned fields in the required entry charts and combining returned +fields in their common output charts. Under those explicit assumptions, run +the first `d` evaluations on owned copies and retain their returned values. +Run the final evaluation on the original input owners, multiply those outputs +by its nonzero Lagrange weight, and add the other weighted outputs. Erase +only the owned copies. This schedule never erases an original arbitrary +input owner. Arbitrary-input correctness permits correlations among copies; +it does not create additional productive inputs. + +If one evaluation has target inventory `T` and paid inventory `P`, this +construction has the original target inventory `T` and paid inventory +`(d+1)P`, before any extra paid adapters. Its native calls on copied helper +inputs are paid on every evaluation too. There is no credit for `(d+1)` +independent copies of the original helper inputs. Copying, accumulation, +initialization, erasure, node coefficients, coefficient heights and storage +are additional implementation obligations. They are not included in a claim +that only the paid inventory scales by `d+1`. + +### The stronger fresh-helper policy + +For the present controller the exact full endpoint is block diagonal between +mains and helpers. Helper inputs do not influence main outputs, and each +helper is returned through its own target operator. Thus each evaluation can +instead use a **fresh, independent productive helper inventory**, retaining +all those outputs separately. Only the main inputs are copied and combined. +Writing `K=d+1`, the more favorable inventory is + +``` +targets = T_main + K T_helper, +paid = K P. +``` + +These extra helper inputs must be allocated as distinct original productive +fields, not initialized owned copies of one helper set. The first `K-1` +evaluations use owned copies of the main fields; the final evaluation uses +their original owners as above. All `K` helper inventories keep their +independent input and output ownership. The construction still needs the +copy, combination, chart, storage and physical charges already listed. + +This policy is stronger than copying every input and discarding all but one +helper output. For example, the p16 complex border in DISCOVERY.md has main +rank mass 35,840, helper rank mass 62,478 and paid rank mass 97,566. Generic +degree-15 interpolation would give the favorable rank-one masses + +``` +target = 35,840 + 16 * 62,478 = 1,035,488, +paid = 16 * 97,566 = 1,561,056. +``` + +It therefore loses 525,568 units of rank-one mass before any extra charges. + +The rejection holds for every `p>=2` in this family. The complex local helper +rank mass is 3,471 and the local paid rank mass is 5,327. The per-port target +formula in DISCOVERY.md and the `p-1` paid queries give + +``` +T_main(1) = 2016 p + 3584, +T_helper(1) = 3471 (p+2), +P(1) = 5439 p + 10542. +``` + +With `K=p` evaluations, paid mass minus productive mass is therefore + +``` +p P(1) - T_main(1) - p T_helper(1) + = 1968 p^2 + 1584 p - 3584. +``` + +It is 7,456 at `p=2` and strictly increases for integer `p>=2`. For the BIT +formal invoice, local helper mass 3,512 and local paid mass 5,129 similarly +give + +``` +T_main(1) = 1776 p + 3108, +T_helper(1) = 3512 (p+2), +P(1) = 5240 p + 10147, +p P(1) - T_main(1) - p T_helper(1) + = 1728 p^2 + 1347 p - 3108. +``` + +The last expression is 6,498 at `p=2` and strictly increases thereafter. BIT +still needs its scalar-extension implementation before this evaluation +policy is available; its idealized invoice already has the displayed loss. +Thus generic direct interpolation with these fresh-helper inventories loses +rank-one mass for every `p>=2`, before extra charges. This rejects this +conversion policy, not every border conversion. New policies with other +retained outputs must state their complete operator and paid inventory. + +[BUDGET.md](BUDGET.md) proves the stronger scoped rejection: with these fresh +helper inventories, already `K>=2` complete evaluations lose at every moment +`0<=t<=1`, for every `p>=2`. The rank-one formulas above are transparent +special cases, not the sharpest rejection established in this package. + +For a required inverse-transpose orientation, the corresponding border is +`E A^(-T) E^(-1)`, since it is the inverse transpose of +`E^(-1) A E`. The opposite scalar wrappers must be used and the full backward +word, charts and costs must be checked; reusing the forward weights without +transposing their placement is not that orientation. + +### A black-box evaluation lower bound + +Suppose a procedure must recover the constant coefficient of an **arbitrary** +polynomial of degree at most `d`, using its values at `K` distinct nonzero +nodes. If `K<=d`, the polynomial + +``` +g(epsilon) = product_(j=1..K) (epsilon-a_j) +``` + +vanishes at all queried nodes but has `g(0)!=0`. The zero polynomial has the +same evaluation transcript and a different constant coefficient. Thus such +a procedure needs at least `d+1` nodes. The argument also applies to an +adaptive deterministic procedure by taking its nodes on the all-zero +transcript. Multiplying `g` by a fixed nonzero matrix gives the operator-valued +version. + +This does not prove that the special controller needs `d+1` evaluations: +additional identities or sparse coefficient support can reduce a particular +problem. It proves that a generic interpolation claim needs a degree or +support bound. Nor does it exclude a non-evaluation exactification method. + +## 2. Chronological amplification needs a new degree theorem + +The inherited product is a chronological program substitution. In +[`research/higher-moment-strictification/vendor/p7-TENSOR.md`](../higher-moment-strictification/vendor/p7-TENSOR.md), +section 1, copies of one supplier pause at a paid position and the other +supplier completes all current jobs before the parents resume. Its proof +uses exact independent endpoints on the current owners. The statement there +explicitly distinguishes this schedule from tensoring a sum of matrix +operators. The same distinction is retained in +[`research/query-thinned-controllers/PROOF.md`](../query-thinned-controllers/PROOF.md), +section 3. + +An ordinary matrix tensor power of a degree-`d` polynomial has degree `vd`. +That observation does not establish a `vd` degree bound for the repository's +chronological supplier product. At nonzero epsilon the border word couples +different productive roles. Those are precisely the endpoints which an exact +child call would have returned separately. A proposed formal substitution +must first check its owner maps, scalar rings, matchers, complete spectators +and every intermediate suspended call. + +Even after that semantic construction, positivity of endpoint powers alone +does not bound degree polynomially in substitution depth. Here is an explicit +generic counterexample. Let `N=2^v`, use `N+1` scalar roles, and let `E_(i,j)` +be the matrix unit. Compose the elementary upper triangular maps in order: + +``` +F_i(epsilon) = I + epsilon E_(i,i+1), i=1,...,N, +F(epsilon) = F_1(epsilon) ... F_N(epsilon). +``` + +Each elementary map has diagonal identity, degree one and only positive +off-diagonal epsilon powers. Every intermediate product has the same +properties, apart from its growing degree. The `(1,N+1)` entry of the final +product is exactly `epsilon^N`: the only contributing chain uses all `N` +successive matrix units. Hence the degree is `2^v`. The ordered composition +can be represented by a binary substitution tree of height `v`, with the +children executed serially. Its execution still contains `2^v` elementary +maps; tree height is not execution length. + +This example is not a counterexample to the specific native controller or a +claim that its degree must grow exponentially. It refutes the implication +“nonnegative endpoint powers plus substitution depth `v` implies degree +`O(v)`.” A compatible global grading, special coefficient support or another +extraction method remains necessary before claiming polynomial extraction +overhead for the actual product. + +In particular, if an exactification of a legal amplified word uses `K_v` +evaluations **and retains only its original productive inventory**, its +paid/target moment ratio before additional charges is + +``` +K_v * (P_t/T_t)^v, +``` + +before completion, extra adapters or other charges. Retaining fresh productive +helper outputs changes the denominator and requires a separate inventory, +as in section 1. In either policy, an exponential repetition count cannot +simply be discarded as a polynomial factor. Formal moment advantage alone +does not pay it. + +## 3. A sufficient finite complex approximation lemma + +Approximation offers a different route over the complex numbers. The +following lemma applies to a **fully flattened finite circuit**, with all +scalar operations and paid calls included. It is a numerical statement; +it assumes no unproved native implementation or cost theorem. + +Fix a norm on every intermediate space. Include owned-zero initialization +and the final output projection as linear embeddings/projections of norm at +most one. Suppose the exact circuit endpoint is `C(epsilon)` and, for every +`0=1` and `h>=0` are fixed. +3. The numerical execution has at most `J>=1` additive error sites. The + error inserted at each site has norm at most `2^(-P)`. + +Site 3 can include input rounding and approximate paid calls. A coefficient +approximation is covered only after its action on the bounded operand has +been shown to meet that additive-error allowance. Merely storing each +coefficient to `P` fractional bits does not establish that premise. + +Let requested precision `s>=1` be an integer and assume +`||x||<=2^(b s)` for a fixed `b>=0`. Choose integers + +``` +k >= max(1, ceil((b+1)s + log2(4H))), +epsilon = 2^(-k), +P >= ceil(s + 2 + log2(JH) + h k). +``` + +Then the returned numerical value `y` satisfies + +``` +||y-Dx|| <= 2^(-s-1) < 2^(-s). +``` + +**Proof.** The exact border error is bounded by + +``` +||C(epsilon)x-Dx|| <= H 2^(-k) 2^(b s) <= 2^(-s-2). +``` + +Each local numerical error propagates through a suffix of norm at most +`H 2^(h k)`. Linearity and the triangle inequality therefore give total +rounding error at most + +``` +J H 2^(h k) 2^(-P) <= 2^(-s-2). +``` + +Adding the two bounds proves the claim. This propagation uses the exact +linear operators with local numerical discrepancies represented as additive +errors; it does not assume that each gate itself is stable. QED. + +The same subword bound gives, at every intermediate cut, + +``` +||computed state|| + <= H 2^(h k) (2^(b s) + J 2^(-P)) + <= 2 H 2^(h k + b s). +``` + +For fixed `H,h,J,b`, both the required fractional precision and this magnitude +allowance are `O(s)` bits. If the scalar coefficients of the finite word are +fixed Laurent expressions in epsilon, their exponents are fixed and their +epsilon-dependent dyadic shifts also have `O(s)` length. These are numerical +size bounds, not a proof of the execution time of shifts, scalar arithmetic, +coefficient generation, movement or paid primitives. + +The finite constants can be obtained crudely when every primitive is a fixed +Laurent polynomial in epsilon with bounded operator coefficients: expand +each finite contiguous subword, bound its negative exponents, and sum its +coefficient norms. The resulting `h,H` may be enormous. This general +observation alone does not give a uniform all-column bound; the next +subsection supplies one for the raw forward controller under explicit norm +contracts. + +### Conditional raw-controller norm bound at every column multiplicity + +The following specialization connects the lemma to the changed **raw forward +complex controller**, without asserting an implementation of its paid primitives. +Use the infinity norm on the complete vector of live data and owned fields. +At column multiplicity `f>=1`, assume: + +- each completed paid rank-`r` oracle and each rank-`r` Gaussian factor used + in the endpoint formula, in either required orientation, has operator norm + at most `2^(r f)`; +- each retained monomial route has norm one; +- the literal scalar word has fixed coefficients independent of `f`, or its + aggregate scalar norm allowance below is bounded by `S_0+S_1 f`. + +These are norm assumptions on completed operations. They do not bound a +paid primitive's internal numerical errors or runtime. Whole-job adapters +which are not unit-norm monomial routes must receive their actual norm +allowance as well. + +For each scalar record choose an upper bound `a_j>=1` for its operator norm, +and put `S=sum_j log2(a_j)`. A scalar ADD of coefficient `c` has bound +`1+|c|`; a SCALE has bound `max(1,|c|)`. A COPY which *replaces* its destination, +a clear and a signed swap have norm at most one. If copying is emitted as a +clear followed by ADD, count that ADD with norm two when bounding every +intermediate cut. Its zero-destination invariant alone does not bound errors +inserted between those two records. Integer upper bounds such as +`ceil(log2(a_j))` may be used to compute `S` without transcendental arithmetic. + +Let `R=sum_r r P_r` be the raw paid rank mass, with every occurrence counted. +Every contiguous subword of the unwrapped raw word then has norm at most + +``` +H_0(f) = 2^(R f + S). +``` + +Indeed, multiply the corresponding record bounds. All bounds are at least +one, so any contiguous subword is bounded by the product for the complete +word. With the p16 complex invoice in DISCOVERY.md, `R=97,566` exactly. +The scalar allowance `S` is finite and computable from the retained literal +coefficient list; no numerical value is claimed here. The predecessor's +`10^9` nonrecursive-record allowance is not by itself a bound on coefficient +heights and is not substituted for `S`. + +Now put the contracting wrapper `E(epsilon)` before the raw word and the +expanding wrapper `E(epsilon)^(-1)` after it, acting only on main fields. +The largest weight is `p-1`. Every partial input wrapper has norm at most +one. Every partial output wrapper has norm at most `epsilon^(-(p-1))`: +its individual scalings act on distinct fields, so their combined infinity +norm is their maximum, not their product. Consequently every contiguous +subword of this wrapped circuit has norm at most + +``` +H_0(f) epsilon^(-(p-1)). +``` + +The endpoint remainder has a separate bound from the explicit U,V formulas. +Every off-diagonal row has at most `p-1` entries. Each entry is a signed +difference of two products containing at most `p+2` stage factors, each used +at most once, and one central rank-one factor. Noninitial stage factors have +rank eight. The initial factor is `D_0=F_9 Q^(-1)`, as specified in the source +controller proof. Bound it by `2^(10f)` using its rank-nine and rank-one +factors separately; no cancellation or phase normalization is needed for +this conservative estimate. Thus each term has norm at most +`2^([3+8(p+2)] f)`. Dividing the off-diagonal +polynomial by epsilon leaves nonnegative powers whose values are at most one +for `0.01 target. + +The exact algebra succeeded. The full budget rejected that target: removing +idles also removes their credited output ranks. Even granting recovery free, +a determinant/Jensen bound excludes supplier saving C>=.006 complex and +C>=.007 BIT for every positive p in the stated fixed-inventory model. We have +stopped that target rather than relabeling a smaller formal gain as success. + +Two natural recovery routes also fail. Repeating the whole controller K>=2 +times loses every concave moment, even when each evaluation earns all its +fresh independent helper outputs. A copied-input decoder needs p-1 new query +jobs per port to correct the X block, and that bill already loses before the +Y block is corrected. Neither result excludes shared internal queries, +cross-port constructions, different native words, or other output contracts. + +## Reviewable results + +| Artifact | Established scope | +|---|---| +| [DISCOVERY.md](DISCOVERY.md) | All-p triangular formula, explicit scalar filtration, actual changed profiles and clearly labelled exploratory roots | +| [BUDGET.md](BUDGET.md) | Determinant-constrained all-p ceilings; repeated-evaluation rejection with full fresh-helper credit | +| [DECODER.md](DECODER.md) | Exact copied-input correction and forced per-port query rank; all-concave-moment rejection in that decoder model | +| [EXACTIFICATION.md](EXACTIFICATION.md) | Exact interpolation ownership; why ordinary tensor-degree reasoning does not apply automatically; finite global complex approximation lemma and BIT limitation | +| [RESULT.json](RESULT.json) | Source-bound exact arithmetic and finite checks; excludes floating discovery roots | +| [REVIEW.md](REVIEW.md) | Separate author-side AI proof review and independent rational implementation; no human or formal-kernel review | + +For orientation only, the p16 complex border has targets +`{4:504,7:126,8:846,9:9004,17:448}` and paid calls +`{1:41946,2:6984,3:8892,4:2646,5:648,8:144}`. Target and paid rank masses +are 98,318 and 97,566, with surplus 752. Its exploratory raw moment crossing +is approximately .00482218; this is **not an admitted saving**. A nonzero +parameter still couples main outputs, so the exact source compiler cannot +simply accept those counts. The current selected result remains .0023; +pending #4610 claims .00302152 for a different exact word. + +## Full boundary and expansion decision + +Inputs are the existing arbitrary main fields plus separate arbitrary helpers +for every full native call. Scalar parameter wrappers act only on mains. +The formal constant term gives separate target operators; at a nonzero +parameter the main outputs are coupled. Owned copies and centers earn no +productive credit. Helper restoration and main ownership follow the source +contract; exact recovery must preserve them. + +| Obligation | Status | +|---|---| +| Retained full native calls, thin queries, helpers and changed main ranks | Explicitly counted; source native/physical contracts inherited | +| Whole-idle calls | Deleted from both paid work and corresponding target rank credit | +| Formal endpoint and singular scalar wrappers | Proved algebraically; inverse parameter powers prevent evaluation at zero | +| Repeated evaluations with fresh helpers | Constructed at the linear-operator level under copying/combination assumptions; optimistic paid budget fails | +| Per-port copied-input X correction | Exact logical construction and rank bound; full added-query budget fails | +| Shared-work exactification, all-column physical scalar implementation, legal amplification | Unknown; not priced as zero in an admitted construction | +| Global approximation and recursive precision | Finite sufficient lemma only; actual caller and runtime obligations remain | +| BIT scalar extension and return to ordinary BIT | Unknown; complex small-parameter rounding does not supply it | + +Decision: retain the new formal interface and the negative full-cost decisions; +stop fixed-inventory attempts at the original .01 target. Do not expand into +more pair counts or scalar-weight searches. A further construction round must +change a costed native/query/output premise or close the recovery contract. + +## Reproduction + +From the repository root, Python 3.12 and standard library only: + +```sh +python3.12 -B scripts/research_package.py --package research/controller-border-interface +python3.12 -I -O -B research/controller-border-interface/verify.py +``` + +The verifier authenticates three live inputs, compares every Laurent coefficient +for p=1..8, checks exact budget certificates valid for all p, and runs a separate +rational event implementation at p2/p3. Controls include incorrect orientation, +reversed parameter weights, lost decoder queries, duplicated main credit, +omitted thin-query charges, polynomial degree growth and underfunded precision. +The exact receipt is regenerated only with the explicit authoring `--write` +option. [VALIDATION.md](VALIDATION.md) records actual execution and export checks. +No complete native, selected cold replay, Lean or historical suite is claimed. + +## Sources, overlap and credit + +Scientific base is canonical main `f626db5c3a3d781d8f7695038776c621651f75e1`, +priority revision 7. All source pins remain immutable. The task explicitly +changes the historical `joint-query-controller` card to the live controller +handoff. The canonical investigation is +[#4611](https://github.com/CrocSwap/integer-mult-bounds/discussions/4611). +The entry overlap refresh covered 387 open PRs, 3,539 Discussion records and +5,860 local note records with complete reported pagination. That is bounded +coordination evidence, not proof of novelty or an exhaustive code-diff search. + +Credit Cinna Davis / 1337isnot1337 for #4440/#4470, zxv for the native and +productive compiler lineage, Jacob Alan Sussman for mixed-target compilation, +and the retained BIT, Clifford, scalar, precision and outer-framework authors. +Matarener/Mark's #4602/#4603 motivated the whole-controller question and +separated already tested query-fusion models. DaysSky's #4596 and Ryanson +Jonathan's #4604 informed the comparison of alternative avenues. Those works +are predecessors or strategic context, not claims recertified by this package. +New work prepared by Dillon with substantial OpenAI Codex assistance and +parallel AI strategy, construction, budget, exactification and review workers. +Apache-2.0; no independent human review or formal proof kernel. + +## Open next questions + +1. Can retained internal query information or another shared-work construction + recover the diagonal with a favorable full bill? First give an explicit + arbitrary-input endpoint and ownership schedule. The fresh-query lower + bound does not cover that changed information boundary. +2. Can the complex border meet one global precision and runtime contract at + the actual recursive caller? First bind the numerical lemma to the native + all-column word and a legally flattened compiler. BIT needs a separate + scalar representation and return cost. +3. What changed native inventory, query alphabet or output contract can reach + .01? First identify actual removed paid work or additional independent + output credit. Larger p within the proved ceiling cannot answer it. + +Structured first steps and blockers are retained in [TASK.json](TASK.json). diff --git a/research/controller-border-interface/RESULT.json b/research/controller-border-interface/RESULT.json new file mode 100644 index 0000000000..5342a03ec5 --- /dev/null +++ b/research/controller-border-interface/RESULT.json @@ -0,0 +1,702 @@ +{ + "algebra": { + "cases": [ + { + "border_degree": 0, + "decoder": { + "fresh_query_rank": 0, + "missing_query_rejected": false, + "owned_saved_fields": 0, + "scalar_additions": 0 + }, + "exact_formula": true, + "integral_reduction": true, + "laurent_coefficients": 2, + "pairs": 1 + }, + { + "border_degree": 1, + "decoder": { + "fresh_query_rank": 1, + "missing_query_rejected": true, + "owned_saved_fields": 1, + "scalar_additions": 2 + }, + "exact_formula": true, + "integral_reduction": true, + "laurent_coefficients": 6, + "pairs": 2 + }, + { + "border_degree": 2, + "decoder": { + "fresh_query_rank": 2, + "missing_query_rejected": true, + "owned_saved_fields": 2, + "scalar_additions": 4 + }, + "exact_formula": true, + "integral_reduction": true, + "laurent_coefficients": 10, + "pairs": 3 + }, + { + "border_degree": 3, + "decoder": { + "fresh_query_rank": 3, + "missing_query_rejected": true, + "owned_saved_fields": 3, + "scalar_additions": 6 + }, + "exact_formula": true, + "integral_reduction": true, + "laurent_coefficients": 15, + "pairs": 4 + }, + { + "border_degree": 4, + "decoder": { + "fresh_query_rank": 4, + "missing_query_rejected": true, + "owned_saved_fields": 4, + "scalar_additions": 8 + }, + "exact_formula": true, + "integral_reduction": true, + "laurent_coefficients": 21, + "pairs": 5 + }, + { + "border_degree": 5, + "decoder": { + "fresh_query_rank": 5, + "missing_query_rejected": true, + "owned_saved_fields": 5, + "scalar_additions": 10 + }, + "exact_formula": true, + "integral_reduction": true, + "laurent_coefficients": 28, + "pairs": 6 + }, + { + "border_degree": 6, + "decoder": { + "fresh_query_rank": 6, + "missing_query_rejected": true, + "owned_saved_fields": 6, + "scalar_additions": 12 + }, + "exact_formula": true, + "integral_reduction": true, + "laurent_coefficients": 36, + "pairs": 7 + }, + { + "border_degree": 7, + "decoder": { + "fresh_query_rank": 7, + "missing_query_rejected": true, + "owned_saved_fields": 7, + "scalar_additions": 14 + }, + "exact_formula": true, + "integral_reduction": true, + "laurent_coefficients": 45, + "pairs": 8 + } + ], + "corrected_all_moment_certificate": { + "bit": [ + { + "at_p2": 5514, + "rank": 1, + "slope_in_p": 1545 + }, + { + "at_p2": 16250, + "rank": 2, + "slope_in_p": 4229 + }, + { + "at_p2": 17198, + "rank": 3, + "slope_in_p": 4466 + }, + { + "at_p2": 17902, + "rank": 4, + "slope_in_p": 4642 + }, + { + "at_p2": 19942, + "rank": 5, + "slope_in_p": 5152 + }, + { + "at_p2": 20206, + "rank": 6, + "slope_in_p": 5218 + }, + { + "at_p2": 20738, + "rank": 7, + "slope_in_p": 5351 + }, + { + "at_p2": 6690, + "rank": 8, + "slope_in_p": 63 + }, + { + "at_p2": 30, + "rank": 15, + "slope_in_p": 63 + } + ], + "complex": [ + { + "at_p2": 9172, + "rank": 1, + "slope_in_p": 2461 + }, + { + "at_p2": 12276, + "rank": 2, + "slope_in_p": 3237 + }, + { + "at_p2": 18204, + "rank": 3, + "slope_in_p": 4719 + }, + { + "at_p2": 20108, + "rank": 4, + "slope_in_p": 5195 + }, + { + "at_p2": 20828, + "rank": 5, + "slope_in_p": 5375 + }, + { + "at_p2": 20632, + "rank": 7, + "slope_in_p": 5326 + }, + { + "at_p2": 19384, + "rank": 8, + "slope_in_p": 5014 + }, + { + "at_p2": 7648, + "rank": 9, + "slope_in_p": 64 + }, + { + "at_p2": 32, + "rank": 17, + "slope_in_p": 64 + } + ] + }, + "discovery_not_certified": "Floating root estimates are omitted from this exact receipt.", + "p16_profiles": { + "bit": { + "paid": { + "1": 25479, + "2": 24156, + "3": 1422, + "4": 792, + "5": 1836, + "6": 198, + "7": 342 + }, + "targets": { + "15": 444, + "8": 11010 + } + }, + "complex": { + "paid": { + "1": 41946, + "2": 6984, + "3": 8892, + "4": 2646, + "5": 648, + "8": 144 + }, + "targets": { + "17": 448, + "4": 504, + "7": 126, + "8": 846, + "9": 9004 + } + } + }, + "status": "PASS_EXACT_NO_IDLE_BORDER_ALGEBRA" + }, + "budget": { + "power_precision_bits": 48, + "profiles": { + "BIT": { + "block": 7, + "ceiling_strict": "7/1000", + "checks": [ + { + "A": { + "lower": "-7148257702946515/281474976710656", + "upper": "-7148257702944257/281474976710656" + }, + "Jensen_B": { + "lower": "-644206222949527999/3518437208883200", + "upper": "-10307299567191556661/56294995342131200" + }, + "exact_B": { + "lower": "-27236812340961643/140737488355328", + "upper": "-27236812340959163/140737488355328" + }, + "h": { + "lower": "-465516309772989523/281474976710656", + "upper": "-465516309772987487/281474976710656" + }, + "p_one_margin": { + "lower": "-63668410771382769/281474976710656", + "upper": "-63668410771376439/281474976710656" + }, + "p_two_margin": { + "lower": "-1074533438872123/4398046511104", + "upper": "-17192535021951821/70368744177664" + }, + "saving": "1/100", + "t": "99/100" + }, + { + "A": { + "lower": "-1005739845061211/281474976710656", + "upper": "-1005739845058953/281474976710656" + }, + "Jensen_B": { + "lower": "-37484509145759069833/281474976710656000", + "upper": "-14993803658301844821/112589990684262400" + }, + "exact_B": { + "lower": "-19780501118246309/140737488355328", + "upper": "-19780501118243829/140737488355328" + }, + "h": { + "lower": "-462437695982266463/281474976710656", + "upper": "-462437695982264427/281474976710656" + }, + "p_one_margin": { + "lower": "-42015113250999393/281474976710656", + "upper": "-42015113250993063/281474976710656" + }, + "p_two_margin": { + "lower": "-10393120481653649/70368744177664", + "upper": "-5196560240825751/35184372088832" + }, + "saving": "7/1000", + "t": "993/1000" + } + ], + "controls": { + "invalid_missing_thin_queries": { + "invalid_margin": { + "lower": "728196197233558803/140737488355328", + "upper": "728196197233633095/140737488355328" + }, + "omitted_rank_one_calls": 6993, + "p": 64, + "saving": "1/100" + }, + "smaller_saving_pass": { + "margin": { + "lower": "8195908666210827/70368744177664", + "upper": "8195908666247973/70368744177664" + }, + "p": 64, + "saving": "3/500", + "scope": "Necessary moment test only; no border extraction or native admission claimed." + } + }, + "excluded_savings": [ + "7/1000", + "1" + ], + "ports": 111, + "repeated_evaluation_obstruction": { + "all_integer_p_at_least": 1, + "all_savings": [ + "0", + "1" + ], + "independent_helpers_credited_per_evaluation": true, + "invalid_duplicate_main_credit_control": { + "correct_margin": -6498, + "p": 2, + "saving": "0", + "wrong_margin": 162 + }, + "local_rank_helper_minus_paid": -1617, + "main_outputs_credited_once": true, + "minimum_evaluations": 2, + "scope": "Whole-controller repeated evaluations with unchanged local invoices; no general exactification barrier.", + "two_evaluation_rank_margin": { + "coefficient_of_p": -1680, + "constant": -3138 + } + }, + "separator": "15/2", + "signed_helpers_minus_paid": { + "1": -1323, + "2": -1342, + "3": -79, + "4": -44, + "5": -102, + "6": -11, + "7": -19, + "8": 439 + } + }, + "complex": { + "block": 8, + "ceiling_strict": "3/500", + "checks": [ + { + "A": { + "lower": "-5061202168248065/140737488355328", + "upper": "-10122404336494425/281474976710656" + }, + "Jensen_B": { + "lower": "-73622911781864053/351843720888320", + "upper": "-736229117818598577/3518437208883200" + }, + "exact_B": { + "lower": "-15581165633330801/70368744177664", + "upper": "-31162331266659673/140737488355328" + }, + "h": { + "lower": "-266859255404283409/140737488355328", + "upper": "-533718510808565337/281474976710656" + }, + "p_one_margin": { + "lower": "-37412804113461763/140737488355328", + "upper": "-74825608226918859/281474976710656" + }, + "p_two_margin": { + "lower": "-10321183900789377/35184372088832", + "upper": "-20642367801577161/70368744177664" + }, + "saving": "1/100", + "t": "99/100" + }, + { + "A": { + "lower": "-371069840716135/140737488355328", + "upper": "-742139681430565/281474976710656" + }, + "Jensen_B": { + "lower": "-10499490381522587891/79164837199872000", + "upper": "-20998980763043287001/158329674399744000" + }, + "exact_B": { + "lower": "-9853925786777143/70368744177664", + "upper": "-19707851573552357/140737488355328" + }, + "h": { + "lower": "-264619326945483735/140737488355328", + "upper": "-529238653890965989/281474976710656" + }, + "p_one_margin": { + "lower": "-20803355175761525/140737488355328", + "upper": "-41606710351518383/281474976710656" + }, + "p_two_margin": { + "lower": "-5112497813746583/35184372088832", + "upper": "-10224995627491573/70368744177664" + }, + "saving": "3/500", + "t": "497/500" + } + ], + "controls": { + "invalid_missing_thin_queries": { + "invalid_margin": { + "lower": "318982223900328415/70368744177664", + "upper": "637964447800712871/140737488355328" + }, + "omitted_rank_one_calls": 7056, + "p": 64, + "saving": "1/100" + }, + "smaller_saving_pass": { + "margin": { + "lower": "9067778047262867/140737488355328", + "upper": "2266944511822907/35184372088832" + }, + "p": 32, + "saving": "1/200", + "scope": "Necessary moment test only; no border extraction or native admission claimed." + } + }, + "excluded_savings": [ + "3/500", + "1" + ], + "ports": 112, + "repeated_evaluation_obstruction": { + "all_integer_p_at_least": 1, + "all_savings": [ + "0", + "1" + ], + "independent_helpers_credited_per_evaluation": true, + "invalid_duplicate_main_credit_control": { + "correct_margin": -7456, + "p": 2, + "saving": "0", + "wrong_margin": 160 + }, + "local_rank_helper_minus_paid": -1856, + "main_outputs_credited_once": true, + "minimum_evaluations": 2, + "scope": "Whole-controller repeated evaluations with unchanged local invoices; no general exactification barrier.", + "two_evaluation_rank_margin": { + "coefficient_of_p": -1920, + "constant": -3616 + } + }, + "separator": "6", + "signed_helpers_minus_paid": { + "1": -2237, + "2": -388, + "3": -494, + "4": -119, + "5": -36, + "7": 7, + "8": 39, + "9": 326 + } + } + }, + "scope": "All positive integer p, unchanged full-call and thin-query invoices, 2vp main fields and determinant rank sum 2v[p+b(p+2)], even granting coefficient extraction and extra routing free.", + "status": "PASS_OPTIMISTIC_BORDER_BUDGET_CEILING", + "target_saving": "1/100" + }, + "claim": "Formal border construction and scoped cost obstructions; no admitted supplier or kappa.", + "independent": { + "all_columns": true, + "conditioning_controls": [ + { + "dyadic_epsilon_exponent": 5, + "funded_error": "1/16", + "funded_fractional_bits": 10, + "pole_order": 1, + "requested_bits": 2, + "underfunded_error": "33/32" + }, + { + "dyadic_epsilon_exponent": 5, + "funded_error": "1/16", + "funded_fractional_bits": 15, + "pole_order": 2, + "requested_bits": 2, + "underfunded_error": "1025/32" + }, + { + "dyadic_epsilon_exponent": 5, + "funded_error": "1/16", + "funded_fractional_bits": 25, + "pole_order": 4, + "requested_bits": 2, + "underfunded_error": "1048577/32" + }, + { + "dyadic_epsilon_exponent": 8, + "funded_error": "1/128", + "funded_fractional_bits": 16, + "pole_order": 1, + "requested_bits": 5, + "underfunded_error": "257/256" + }, + { + "dyadic_epsilon_exponent": 8, + "funded_error": "1/128", + "funded_fractional_bits": 24, + "pole_order": 2, + "requested_bits": 5, + "underfunded_error": "65537/256" + }, + { + "dyadic_epsilon_exponent": 8, + "funded_error": "1/128", + "funded_fractional_bits": 40, + "pole_order": 4, + "requested_bits": 5, + "underfunded_error": "4294967297/256" + }, + { + "dyadic_epsilon_exponent": 12, + "funded_error": "1/2048", + "funded_fractional_bits": 24, + "pole_order": 1, + "requested_bits": 9, + "underfunded_error": "4097/4096" + }, + { + "dyadic_epsilon_exponent": 12, + "funded_error": "1/2048", + "funded_fractional_bits": 36, + "pole_order": 2, + "requested_bits": 9, + "underfunded_error": "16777217/4096" + }, + { + "dyadic_epsilon_exponent": 12, + "funded_error": "1/2048", + "funded_fractional_bits": 60, + "pole_order": 4, + "requested_bits": 9, + "underfunded_error": "281474976710657/4096" + } + ], + "degree_growth_controls": [ + { + "actual_degree": 2, + "binary_tree_depth": 1, + "executed_factors": 2 + }, + { + "actual_degree": 4, + "binary_tree_depth": 2, + "executed_factors": 4 + }, + { + "actual_degree": 8, + "binary_tree_depth": 3, + "executed_factors": 8 + }, + { + "actual_degree": 16, + "binary_tree_depth": 4, + "executed_factors": 16 + } + ], + "exact_instances": 24, + "forward_and_inverse_transpose_extraction": true, + "samples": [ + { + "literal_matrix": [ + [ + "9/2", + "0", + "-3/4", + "0" + ], + [ + "0", + "2", + "0", + "0" + ], + [ + "0", + "0", + "9/4", + "0" + ], + [ + "0", + "-1", + "0", + "1" + ] + ], + "p": 2, + "q": "2/3", + "stages": [ + "2", + "3/2", + "4/3", + "5/4", + "6/5" + ] + }, + { + "literal_matrix": [ + [ + "9/2", + "0", + "-3/8", + "0", + "1/2", + "0" + ], + [ + "0", + "2", + "0", + "0", + "0", + "0" + ], + [ + "0", + "0", + "15/8", + "0", + "-1/2", + "0" + ], + [ + "0", + "-1/2", + "0", + "5/6", + "0", + "0" + ], + [ + "0", + "0", + "0", + "0", + "2", + "0" + ], + [ + "0", + "5/6", + "0", + "-5/18", + "0", + "8/9" + ] + ], + "p": 3, + "q": "2/3", + "stages": [ + "2", + "3/2", + "4/3", + "5/4", + "6/5", + "7/6", + "8/7" + ] + } + ], + "status": "PASS_INDEPENDENT_RATIONAL_P2_P3", + "wrong_weight_controls_rejected": 48 + }, + "source_sha256": { + "research/joint-helper-lattice/RESULT.json": "c7b2388f6511c19976b337d8c8ac374610af616866a249d75dace704eb5d9e21", + "research/kappa-rebuild/bit/complex_controller_factor.py": "1de9aaf918e6a4f2f5448754c1f3c3da3b85e6257849ebd097af09859c4e5497", + "research/query-thinned-controllers/BIT-CONTROLLER.json": "39ac84fb848b908f7ba051fae4556d507900c421dc5d23501a9c0cb1d61fd08d" + }, + "status": "PASS_SCOPED_CONTROLLER_BORDER_INTERFACE" +} diff --git a/research/controller-border-interface/REVIEW.md b/research/controller-border-interface/REVIEW.md new file mode 100644 index 0000000000..112adc3943 --- /dev/null +++ b/research/controller-border-interface/REVIEW.md @@ -0,0 +1,133 @@ +# Author-side independent mathematical review + +This review was performed in a separate OpenAI agent context for Dillon on +2026-10-22. It is independent author-side AI checking, not independent human +review or formal-kernel verification. The package's authenticated source pins +remain the authority for the inherited native contracts and invoices. + +## What was checked + +The all-p proof in DISCOVERY.md was checked against the source chronology: +the forward and backward shears, both bridges, the reverse bridge chain and +final signed swaps. The displayed upper X block and lower Y block agree with +that chronology. Opposite weights on the X and Y chains make every nonzero +off-diagonal coefficient have positive epsilon degree. The endpoint degree is +p-1, while its diagonal is unchanged. This reasoning uses commuting formal +units and the stated arbitrary-input native endpoint, including its separate +helper block. It does not evaluate formal variables at Fourier characters or +replace the physical complex Q inverse by Q. + +`independent_check.py` uses a separate exact implementation with no imports +from the construction or its predecessor emitter. It executes numerical +rational shears on every input column and compares with separately hardcoded +p2 and p3 matrices. Across 24 parameter instances it verifies their complete +matrices, forward Lagrange extraction, and inverse-transpose extraction with +the opposite scalar wrappers. Forty-eight wrong-weight controls fail as +required. These finite rational checks support the symbolic proof; they do +not establish the all-p identity by enumeration. + +The checker also multiplies polynomial matrix factors for four triangular +chains of lengths 2, 4, 8 and 16. Their actual top-right coefficients have +those respective epsilon degrees, despite binary execution trees of depths +1, 2, 3 and 4. Reversing the factor order destroys that coefficient. This +checks the generic degree-growth counterexample in EXACTIFICATION.md, not a +claim about the actual native compiler's degree. + +Nine exact dyadic scalar circuits test the approximation lemma's precision +accounting. Each has gates epsilon^h, 1+epsilon and epsilon^-h, with a positive +additive error immediately before the final gate. The funded precision +succeeds; omitting the h*k conditioning term fails. The finite complex norm +lemma was also reviewed algebraically: the border error and propagated +additive errors each use at most one quarter of the requested tolerance. +The magnitude bound follows from the same subword norm hypothesis. + +The added raw forward-controller bound was reviewed at the level of completed paid +oracles. Under its explicit norm contracts, multiplying per-record bounds +gives `H_0(f)=2^(R f+S)`. Disjoint-role wrapper scalings require only the +largest inverse epsilon power, so `h_f=p-1`. The two-term off-diagonal +formulas give the stated exponential-in-f forward remainder bound. Bounding +the initial `D_0=F_9 Q^-1` by its two factors avoids relying on native phase +cancellation. This establishes +linear-in-f logarithmic constants for the fixed raw controller under those +contracts, not for the backward endpoint remainder, paid-oracle interiors +or an amplified recursive compiler. + +The BUDGET.md proof was checked separately: scalar border transformations +preserve the formal stage determinant degrees; fixed output count and rank +mass give the Jensen upper bound; rank separation makes the unlinearized +normalized envelope monotone. The 48-bit outward rational power engine uses +integer nth-root comparisons. The proof correctly retains fresh independent +helpers in every repeated evaluation, credits main outputs once, and rejects +K>=2 whole-unit evaluation policies at every t in [0,1]. This result depends +on the stated inventory, output count and rank-mass model. + +For DECODER.md, writing U=(I-S)D+S and requiring M U+N=D makes independent +coefficient comparison force M=(I-S)^-1=I+J and N=-J. Its rank is p-1 over Q +and over F2. This proves the fresh-query lower bound in that explicitly +restricted endpoint decoder model. It is not a lower bound against reuse of +internal transcripts, cross-port schemes, changed native words or general +operator-valued adapters. + +## Ownership and implementation limits + +The source native endpoint is valid on arbitrary inputs. Consequently, +main-only scalar conjugation leaves the separate arbitrary helper outputs +unchanged. Finite interpolation can legitimately retain a fresh helper set +for each evaluation. Copied main fields are owned scratch and receive no +additional productive credit. Running the final evaluation in place on the +original main owners allows earlier copied outputs to be accumulated without +erasing any original input owner. Copying, charts, scalar operations, movement, +storage and owned erasure still need their physical implementation and cost. + +A nonzero epsilon execution is a coupled endpoint. It is not already the +exact diagonal supplier required by the chronological compiler. The complex +approximation lemma is a conditional finite-circuit numerical result. Its +raw all-column macro bounds follow under the stated completed-oracle norm +contracts; native numerical oracle interiors, legally amplified all-column +bounds, recursive precision, scalar implementation and physical costs remain +open. Its constants cannot simply +be reset independently at every recursive call. + +Reduction of an integral formal identity modulo two does not create small +native BIT scalars. Ordinary BIT has no Archimedean limit. Finite extensions +or polynomial-coordinate representations require explicit native operations, +coordinate charges and return costs. The complex approximation result does +not discharge any of those obligations. + +## Reproduction and review status + +The direct check completed with Python 3.14.7 and Python 3.12.15, including +optimized mode: + +```sh +python3 -I -O -B research/controller-border-interface/independent_check.py +``` + +Three separate temporary-file mutations were also rejected under Python +3.12.15 with `-I -O -B`: reversing the p2 X-coupling sign, using forward +weights in the backward extraction, and dropping the conditioning bits from +the precision request. Each failed its corresponding mathematical check. +No package source was edited for those mutation executions. + +The mathematical review above found no remaining contradiction in the stated +scoped claims. Clarifications about retaining fresh helper credit, reversing +inverse-transpose wrappers, restricting the repeated-evaluation ratio, and +keeping determinant rank credit source-compatible were communicated during +review. The package reports no new admitted supplier, certified kappa or +complete multiplication theorem. + +## Open next questions + +Can a legal amplification or shared-query implementation bypass the priced +whole-unit extraction and fresh-query decoder policies? Its first obligation +is a complete arbitrary-input endpoint and ownership schedule, followed by +its paid inventory. Existing erased query transcripts are not automatically +available. Can the complex border instead satisfy one global all-column +approximation and precision contract at the actual recursive caller? The +finite norm lemma identifies sufficient numerical hypotheses, but the native +program and caller must supply them. + +Apache-2.0. Credit the native/controller work of zxv and Cinna Davis, the +compiler work of Jacob Alan Sussman, and the predecessor sources retained in +SOURCES.json. New review and independent checks prepared with substantial +OpenAI assistance. diff --git a/research/controller-border-interface/SOURCES.json b/research/controller-border-interface/SOURCES.json new file mode 100644 index 0000000000..c1b44f6d22 --- /dev/null +++ b/research/controller-border-interface/SOURCES.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40", + "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/joint-helper-lattice/RESULT.json", + "usage": "input", + "git_blob": "edf41a49a0350862c23378f837c7397fc5dc7596", + "sha256": "c7b2388f6511c19976b337d8c8ac374610af616866a249d75dace704eb5d9e21" + }, + { + "path": "research/kappa-rebuild/bit/complex_controller_factor.py", + "usage": "input", + "git_blob": "cb0cff7c8be5f38f2ee52201d9d0907f9dfd7947", + "sha256": "1de9aaf918e6a4f2f5448754c1f3c3da3b85e6257849ebd097af09859c4e5497" + }, + { + "path": "research/kappa-rebuild/bit/mixed_productive_bit.py", + "usage": "provenance", + "git_blob": "9c7a8bd5d3ae4c19952648c815031858d6627b96", + "sha256": "b32291b0db7fc0d332ec444c70746ab0fb03351d2e50546f8bcb64060e3ff95e" + }, + { + "path": "research/query-thinned-controllers/BIT-CONTROLLER.json", + "usage": "input", + "git_blob": "89c400d5970024b3debe870c36ce43889beed001", + "sha256": "39ac84fb848b908f7ba051fae4556d507900c421dc5d23501a9c0cb1d61fd08d" + }, + { + "path": "research/query-thinned-controllers/COMPLEX-CONTROLLER.json", + "usage": "provenance", + "git_blob": "39318f6ad9baf0838a274ca1042b1e3ba0e74bf9", + "sha256": "bf1143325d8380fab40cd5a85449f9a5412f0340deba7f4693714c92ae320088" + }, + { + "path": "research/query-thinned-controllers/controller.py", + "usage": "provenance", + "git_blob": "d4557e08cfb9fe57cc1ae4024705a72dc95f3583", + "sha256": "8b462d660487b1be4940357c4c7522967b1bfaede3c02b1c66109b85acae0fd2" + }, + { + "path": "research/higher-moment-strictification/vendor/p7-TENSOR.md", + "usage": "provenance", + "git_blob": "8ecfd3e4d0bcb449ecb1e150c4f1f4fbb39ca656", + "sha256": "b2eba86cb979b4dc2a045f2e74bbd29e4d9e5ec87d6a2bc23ba7b54f1f58e3e3" + }, + { + "path": "research/query-thinned-controllers/PROOF.md", + "usage": "provenance", + "git_blob": "9068f429896112082664455ab00bab083c99d1d8", + "sha256": "5ade59641f2ed70d045d6f60e89db7d979b1d1e9967f3acbe5c56eac81312841" + }, + { + "path": "docs/research/pr-intake-evidence/pr4470/PROOF-REVIEW.md", + "usage": "provenance", + "git_blob": "f4dc043b6d35cae2811c9bcc064e04877f9e0549", + "sha256": "5c111dd56beb53dc44ab727d96e1af03aaf50f3023d4342e2b0a89ede6cf585b" + } + ] +} diff --git a/research/controller-border-interface/TASK.json b/research/controller-border-interface/TASK.json new file mode 100644 index 0000000000..0b7a0bc7a7 --- /dev/null +++ b/research/controller-border-interface/TASK.json @@ -0,0 +1,127 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 7, + "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1", + "original_card": { + "id": "joint-query-controller", + "question": "Can the installed QQ16 caller win a complete matched protocol bill, or can a changed demand eliminate actual paid work?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/qq16-caller-install/README.md" + ], + "methods": [ + "Derive the matched whole-caller physical bill for installed and baseline protocols.", + "Change the actual demanded observations and prove a cheaper legal producer/consumer contract." + ], + "acceptance_gate": "Name the changed premise of the fixed F0/B1 observation obstruction. Show exactly which query is recovered, legal native reads and restoration, and a full favorable budget including cover maps, helpers and endpoints. Local inverse identities alone do not close the global controller. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #4166 COST.md and ADMISSION.json. An actual caller connection is now proposed. Its native-component profile loses; parent park/restore versus external-call costs remain unresolved. Retain the producer and recovery lineage rather than rebuild it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "At the actual installed cut, compare matched complete parent park/restore and external input/return protocols at the same bank/packet geometry, including every later root call and service cost. Alternatively pin both bridge observations and derive a genuinely smaller source-compatible demand. Stop if the complete necessary inequality fails or an essential cost is unknown; no larger decoder scan from a local tape-action saving.", + "bottleneck_link": "The native local words exist; retained query information and its physical access are the missing link to a composed recursive interface.", + "allowed_variations": [ + "One paid query, one changed first pair, or one precisely specified affine helper state.", + "A counterexample or lower bound for that exact proposed repair.", + "One unresolved obligation of a newer local decoder, with exact source heads and a distinct claim/domain." + ], + "scope_change_triggers": [ + "Retaining the fixed first pair and ordinary schedule while allowing only homogeneous selected-only control, already excluded by the witness.", + "Treating cover-map counts as zero-cost physical address operations.", + "Recreating the pending complete local decoder or early-record/output-bank coalescing already under investigation without a distinct audit or changed premise.", + "Treating a completed-output defect inequality as a producer-interior, dirty-range or physical-cost certificate.", + "Recreating completed-output recovery or caller wiring already supplied by #4166 without new independent coverage.", + "Dropping retained later root calls or claiming native-profile dominance from the isolated publication saving." + ], + "overlap_terms": [ + "QQ16", + "joint-query", + "changing-chart controller", + "selected observation", + "1969", + "2540", + "early record", + "output-bank retention", + "complete native decoder", + "2965", + "producer defect", + "dirty-helper range", + "F17 consumer", + "4166", + "qq16-caller-install" + ], + "existing_checks": [ + { + "scope": "PR #4166: author-checked installed producer/service/return/bridge connection; native-component comparison loses.", + "evidence": "research/qq16-caller-install/README.md", + "remaining": "Complete matched physical protocol bill, or changed source-compatible demand/circuit; no affordable supplier yet.", + "status": "author-checked", + "source_commit": "0b082d22a0e9a442d264ab0633e35ef26c790630", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Explore a filtered productive controller that deletes whole-idle transforms, using a Laurent-parameter degeneration to independent monomial outputs; test exact recovery and full paid budgets on both suppliers.", + "scope_change_reason": "The donor explicitly requested a risky mechanism with transformative payoff and at least five minutes of strategic selection. Live #4602 identifies controller idles as 56\u201359% of the paid moment; old QQ16 card and fixed local windows do not address this changed endpoint contract. Compared quotient repair, native caller integration and compiler widths before choosing at 10:05 UTC.", + "bottleneck_link": "Remove whole-idle paid transforms by changing scalar endpoint factorization; must charge lost target ranks, extraction, copies, coefficient lanes, restoration, precision and every inherited native/outer obligation.", + "budget_minutes": 60, + "stop_rule": "Target kappa > .01 on both suppliers. First exact p2/p3 algebra and complete optimistic moment screen; stop that target if even free extraction cannot meet it. Do not report raw border moments as an admitted supplier. Research cutoff 10:41 UTC; verification and handoff through about 10:56 UTC.", + "outcome": "partial", + "evidence": "Exact all-p triangular border proof; p1..8 complete Laurent replay; independent p2/p3 rational event execution and extraction; determinant/Jensen all-p ceilings; fresh-helper repeated-evaluation and per-port decoder obstructions; finite complex approximation lemma. No admitted supplier or kappa.", + "author": "Dillon", + "ai_assistance": "Substantial OpenAI Codex assistance with parallel strategy, algebra, exactification, budget and independent review workers; no formal-kernel or independent human review.", + "open_questions": [ + { + "question": "Can shared-work exactification or a compatible global grading turn this border into a paid exact supplier?", + "why_it_matters": "Would remove the whole-idle endpoint requirement and create a different compiler interface. Repeated whole-unit evaluations and the stated per-port fresh-query decoder are already losing.", + "first_step": "Expose actual internal query transcripts or give a two-level chronological substitution with explicit degree, arbitrary-input endpoint and owner maps; price its complete new inventory.", + "blocked_by": "Exact independent endpoints are required at suspended calls; polynomial degree in tensor depth is unproved; copies receive no new main-output credit." + }, + { + "question": "Can an approximate complex border satisfy the actual recursive caller at one globally funded precision?", + "why_it_matters": "A numerical realization might avoid exact coefficient extraction while retaining paid-call savings.", + "first_step": "Bind the finite norm lemma and explicit epsilon wrappers to all-column native prefix norms, then a legally flattened compiler and its actual precision/cost recurrence.", + "blocked_by": "Uniform implementation/runtime and recursive precision are unproved; ordinary BIT has no corresponding small scalar parameter." + }, + { + "question": "What changed native inventory or output/query contract can exceed the .01 target?", + "why_it_matters": "The determinant-constrained fixed inventory fails even with free extraction at .006 complex/.007 BIT for every p.", + "first_step": "Specify an actual removed paid call or new independent output before repricing; compare the full producer/consumer bill.", + "blocked_by": "No such word or ownership-preserving consumer is supplied here; larger p or rearranged target degrees cannot suffice." + } + ], + "session": { + "started_utc": "2026-10-22T09:56:24Z", + "guidance_read_utc": "2026-10-22T09:59:29Z", + "selection_utc": "2026-10-22T10:05:00Z", + "upstream_checkpoint": "f626db5c3a3d781d8f7695038776c621651f75e1", + "overlap": { + "open_prs": 387, + "discussion_records": 3539, + "local_records": 5860, + "fetched_at": "2026-10-22T10:03:47Z", + "complete_reported_pagination": true + }, + "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4611", + "comparison_pending_pr": 4610, + "submission_checkpoint": { + "upstream": "f626db5c3a3d781d8f7695038776c621651f75e1", + "checked_at": "2026-10-22T10:33:41Z", + "priority_revision": 7, + "guidance_selected_and_inputs_changed": false, + "open_prs": 397, + "discussion_records": 3560, + "complete_reported_pagination": true, + "decision": "Continue the pinned formal-interface result; no competing construction found in bounded overlap; latest #4610 changes a different exact native word and is not covered by these frozen budgets." + } + } +} diff --git a/research/controller-border-interface/VALIDATION.md b/research/controller-border-interface/VALIDATION.md new file mode 100644 index 0000000000..28afcf3b60 --- /dev/null +++ b/research/controller-border-interface/VALIDATION.md @@ -0,0 +1,98 @@ +# Executed validation and limits + +Prepared by Dillon with substantial OpenAI Codex assistance, 2026-10-22. +Environment: macOS ARM64, Python 3.12.15 for the registered replay and +Python 3.14.7 for the second isolated optimized replay. Standard library only. +Scientific base: canonical main `f626db5c3a3d781d8f7695038776c621651f75e1`. + +## Scientific checks completed + +```sh +python3.12 -B scripts/research_package.py --package research/controller-border-interface --check-only +python3.12 -B scripts/research_package.py --package research/controller-border-interface +python3.12 -I -O -B research/controller-border-interface/verify.py +python3 -I -O -B research/controller-border-interface/verify.py +git diff --check +``` + +All pass. The registered replay reports +`PASS_REGISTERED_RESEARCH_PACKAGE ... outcome=partial`. A metadata pass alone +does not verify mathematics; the separate scientific command actually executes +the checkers and compares the exact receipt. The explicit authoring `--write` +command was used once to create RESULT.json before normal comparison runs. +Floating-point discovery roots are intentionally excluded from that receipt. + +The checks cover all Laurent coefficients for p=1..8, including orientations, +filtration degree and exact decoder matrices; exact integer-power enclosures +for the all-p budget certificates; independent rational event execution on 24 +p2/p3 instances and all columns; 48 wrong-weight controls; four actual +polynomial degree-growth examples; and nine exact conditioning examples. +The written proofs, rather than finite extrapolation, establish the all-p +claims. Repeated-evaluation checks credit fresh independent helpers correctly. +Omitted thin queries and duplicated main credit demonstrate invalid invoices +that would reverse the decision. They are fault controls, not new candidates. + +A separate author-side AI worker reviewed the proofs and wrote the independent +rational implementation without importing either controller implementation. +Three temporary-source mutations of that independent checker were rejected in +optimized Python 3.12: wrong p2 X coupling, wrong reverse wrapper, and omission +of the conditioning term in the precision budget. REVIEW.md records coverage +and corrections made during review. This is not independent human review or +a formal-kernel proof. + +The selected-baseline helper separately passed source/metadata orientation. +No selected native cold replay, whole historical suite, Lean build or Docker +run was needed or performed. Existing native, physical, ordinary BIT, analytic +and recovery premises are inherited, not recertified by these checks. + +## Publication checks + +Scientific commit `d5f8e3fdad3b7e2f168b33cf17c4a70131b7e501` passed +committed-byte/source-history preflight. Its export contains all 15 package +files and the three declared live inputs (18 files total); archive integrity +also passes. All source pins resolve to the retained canonical-main ancestor. + +The extracted verifier passes Python 3.12.15 with `-I -O -B`, `PATH=/nonexistent` +and a macOS process sandbox denying network access. It therefore needs neither +Git nor a network connection after export. The exact receipt matches the normal +and optimized in-tree replays. Commands: + +```sh +python3.12 -B scripts/check_research_commit.py --package research/controller-border-interface --check-source-history +python3.12 -B scripts/export_research_package.py export --package research/controller-border-interface --output /tmp/controller-border.tar +python3.12 -B scripts/export_research_package.py check /tmp/controller-border.tar +``` + +Four separate mutations of extracted copies fail in optimized Python 3.12: +changed source bytes fail authentication; a false RESULT status fails exact +receipt comparison; a changed X orientation fails the Laurent identity; and +an omitted thin-query bill fails the rank-surplus control. Together with the +three independent-checker mutations above, these exercise source transport, +receipt, algebra, accounting, orientation and precision failure paths. + +Canonical main was fetched again before publication and remained `f626db5c3`. +Guidance, priorities, selected record and pinned scientific inputs were unchanged. +The 10:33 UTC overlap refresh covered 397 open PRs, 3,560 Discussion records +and the complete 5,860 tracked note inventory, with reported complete remote +pagination. The newer #4610 changes a different exact native word; it is not +included in these frozen-inventory ceilings. No competing border-controller +construction was found in this bounded search. Hosted CI is separate from +these local and exported checks; no hosted pass is claimed here. + +## Research decision and remaining obligations + +The hour began at 09:56:24 UTC. Guidance was read from refreshed upstream at +09:59:29, and selection followed at 10:05 after comparing several major avenues. +The original greater-than-.01 target is rejected within the proved fixed +inventory and output contract. The exact formal construction remains a partial +interface result; no new supplier, kappa or frontier update is reported. + +The raw complex norm specialization is conditional on explicitly stated +completed-operation norm bounds. A numerical implementation must still bind +oracle errors, coefficient heights, movement, input magnitudes and runtime. +A chronological amplified/recursive word needs its own global bound. BIT +needs an explicit scalar-extension representation and complete return cost. +The scoped recovery obstructions leave shared internal queries, cross-port +schemes, changed native words and changed output contracts open. + +Apache-2.0. Retain the predecessor attribution in README.md and SOURCES.json. diff --git a/research/controller-border-interface/VERIFY.json b/research/controller-border-interface/VERIFY.json new file mode 100644 index 0000000000..e16a4e5545 --- /dev/null +++ b/research/controller-border-interface/VERIFY.json @@ -0,0 +1,22 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/joint-helper-lattice/RESULT.json", + "research/kappa-rebuild/bit/complex_controller_factor.py", + "research/query-thinned-controllers/BIT-CONTROLLER.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Source authentication; exact all-p formula against literal words for p=1..8; independent rational event replay and interpolation; determinant/Jensen all-size budget certificates; explicit exactification failure controls." + } + ] +} diff --git a/research/controller-border-interface/border_algebra.py b/research/controller-border-interface/border_algebra.py new file mode 100644 index 0000000000..56d32486d3 --- /dev/null +++ b/research/controller-border-interface/border_algebra.py @@ -0,0 +1,256 @@ +#!/usr/bin/env python3 +"""Exact no-idle controller identity and exploratory border-profile pricing. + +Apache-2.0; Dillon with substantial OpenAI assistance. The literal source +controller is credited to zxv / Cinna Davis and its retained predecessor chain. +Floating-point root estimates below are discovery evidence, not certificates. +""" +from collections import Counter +from fractions import Fraction as Q +from pathlib import Path +import ast +import json +import math + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE = ROOT/'research/kappa-rebuild/bit/complex_controller_factor.py' + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def reference_functions(): + """Load only three pure functions; no source imports or external loaders.""" + tree = ast.parse(SOURCE.read_text()) + wanted = {'plus', 'monomial_times', 'controller'} + body = [node for node in tree.body + if isinstance(node, ast.FunctionDef) and node.name in wanted] + need({node.name for node in body} == wanted, 'Exact reference function set') + space = {'Q': Q} + exec(compile(ast.Module(body=body, type_ignores=[]), str(SOURCE), 'exec'), space) + return space + + +def thin_reference(p, wrong_reverse_sign=False): + source = reference_functions() + coeff, events, idles = source['controller'](p, 0, wrong_reverse_sign) + need(not any(e[0] == 'IDLE' for e in events), 'Every whole idle omitted') + thick = {0, 2*p, *range(1, 2*p, 2)} + out = {} + for term, matrix in coeff.items(): + key = (term[0],)+tuple(x if s in thick else 0 + for s, x in enumerate(term[1:])) + target = out.setdefault(key, [[Q(0)]*(2*p) for _ in range(2*p)]) + for i, row in enumerate(matrix): + for j, value in enumerate(row): + target[i][j] += value + return {k: v for k, v in out.items() if any(any(row) for row in v)} + + +def formula(p): + """Independent closed formula in the original Q,D_0,...,D_(2p) variables.""" + need(p >= 1, 'At least one pair') + size = 2*p + width = 2*p+2 + zero = (0,)*width + stages = [[0, 1, 2]] if p == 1 else ( + [[0, 1]]+[[2*j+1] for j in range(1, p-1)]+[[2*p-1, 2*p]]) + ds = [tuple(int(s in selected) for s in range(2*p+1)) for selected in stages] + out = {} + + def put(i, j, q, factors, value): + term = (q,)+tuple(sum(ds[k][s] for k in factors) for s in range(2*p+1)) + matrix = out.setdefault(term, [[Q(0)]*size for _ in range(size)]) + matrix[i][j] += value + + for i in range(p): + put(2*i, 2*i, -1, [i], 1) + put(2*i+1, 2*i+1, 1, [i], 1) + for j in range(i+1, p): + sign = (-1)**(j-i-1) + put(2*i, 2*j, -1, [], sign) + put(2*i, 2*j, -1, [j], -sign) + for j in range(i): + sign = (-1)**(i-j-1) + put(2*i+1, 2*j+1, 1, range(j, i), sign) + put(2*i+1, 2*j+1, 1, range(j, i+1), -sign) + return {k: v for k, v in out.items() if any(any(row) for row in v)} + + +def weighted_limit(coeff, p, reverse=False): + weights = [j if parity == 0 else p-1-j for j in range(p) for parity in (0, 1)] + if reverse: + weights = [-x for x in weights] + constant = {} + degrees = set() + for term, matrix in coeff.items(): + for i, row in enumerate(matrix): + for j, value in enumerate(row): + if not value: + continue + degree = weights[j]-weights[i] + need(degree >= 0, 'No negative border degree') + need(i == j or degree > 0, 'Every off-diagonal term vanishes') + degrees.add(degree) + if degree == 0: + constant.setdefault(term, [[Q(0)]*(2*p) for _ in range(2*p)])[i][j] += value + return constant, sorted(degrees) + + + +def decoder_check(p): + def multiply(a, b): + return [[sum(x*y for x, y in zip(row, col)) for col in zip(*b)] for row in a] + def rank(matrix): + work = [[Q(x) for x in row] for row in matrix] + pivots = 0 + for j in range(p): + chosen = next((i for i in range(pivots, p) if work[i][j]), None) + if chosen is None: + continue + work[pivots], work[chosen] = work[chosen], work[pivots] + factor = work[pivots][j] + work[pivots] = [x/factor for x in work[pivots]] + for i in range(p): + if i != pivots: + factor = work[i][j] + work[i] = [a-factor*b for a, b in zip(work[i], work[pivots])] + pivots += 1 + return pivots + identity = [[int(i == j) for j in range(p)] for i in range(p)] + S = [[(-1)**(j-i-1) if i < j else 0 for j in range(p)] for i in range(p)] + M = [[int(i == j)+int(j == i+1) for j in range(p)] for i in range(p)] + N = [[-int(j == i+1) for j in range(p)] for i in range(p)] + IS = [[identity[i][j]-S[i][j] for j in range(p)] for i in range(p)] + need(multiply(M, IS) == identity, 'Unique decoder coefficient on every d_j') + MS = multiply(M, S) + need(all(MS[i][j]+N[i][j] == 0 for i in range(p) for j in range(p)), 'Exact copied-input correction') + need(rank(N) == p-1, 'Fresh-query correction rank') + if p > 1: + wrong = [row[:] for row in N] + wrong[0][1] = 0 + need(any(MS[i][j]+wrong[i][j] != 0 for i in range(p) for j in range(p)), 'Missing query correction rejected') + return {'fresh_query_rank': p-1, 'scalar_additions': 2*(p-1), + 'owned_saved_fields': p-1, 'missing_query_rejected': p > 1} + + +def main_profile(p, block, ports): + return Counter({1+3*block: 2*ports}) if p == 1 else Counter( + {1+2*block: 4*ports, 1+block: 2*(p-2)*ports}) + + +def local_profiles(): + complex_data = json.loads((ROOT/'research/joint-helper-lattice/RESULT.json').read_text()) + bit = json.loads((ROOT/'research/query-thinned-controllers/BIT-CONTROLLER.json').read_text())['invoice'] + full, thin = bit['thick_calls'], bit['thin_queries'] + bt, bp = Counter({int(k): v for k, v in bit['targets'].items()}), Counter({int(k): v for k, v in bit['paid'].items()}) + bt.subtract({int(k): v for k, v in bit['main'].items()}) + bp.subtract({int(k): v for k, v in bit['whole_idle'].items()}) + bp[1] -= thin + need(all(v >= 0 and v % full == 0 for v in [*bt.values(), *bp.values()]), 'Integral BIT local source decomposition') + return { + 'complex': (8, 112, {int(k): v for k, v in complex_data['local_helpers'].items()}, + {int(k): v for k, v in complex_data['local_paid'].items()}), + 'bit': (7, 111, {k: v//full for k, v in bt.items() if v}, + {k: v//full for k, v in bp.items() if v})} + + +def profiles(p, kind, locals_): + block, ports, helpers, paid = locals_[kind] + targets = Counter({k: (p+2)*v for k, v in helpers.items()}) + targets.update(main_profile(p, block, ports)) + bill = Counter({k: (p+2)*v for k, v in paid.items()}) + bill[1] += ports*(p-1) + need(sum(k*v for k, v in targets.items())-sum(k*v for k, v in bill.items()) == 48*(p+2)-ports, + 'No-idle rank-mass identity') + return +targets, +bill + + + +def correction_moment_certificate(locals_): + certificates = {} + for kind, (_, ports, _, _) in locals_.items(): + cumulative = [] + for p in (2, 3, 4): + targets, paid = profiles(p, kind, locals_) + paid[1] += ports*(p-1) + total, row = 0, {} + for r in sorted(set(targets) | set(paid)): + total += r*(paid[r]-targets[r]) + row[r] = total + cumulative.append(row) + base, second, third = cumulative + need(base.keys() == second.keys() == third.keys(), 'Constant corrected support') + rows = [] + for r, value in base.items(): + slope = second[r]-value + need(value > 0 and slope > 0, 'Positive cumulative rank-mass for every p>=2') + need(third[r] == value+2*slope, 'Affine count control') + rows.append({'rank': r, 'at_p2': value, 'slope_in_p': slope}) + certificates[kind] = rows + return certificates + + +def estimate_root(targets, paid): + def margin(c): + return sum(v*k**(1-c) for k, v in targets.items())-sum(v*k**(1-c) for k, v in paid.items()) + lo, hi = 0., .2 + need(margin(lo) > 0 and margin(hi) < 0, 'Discovery root bracket') + for _ in range(54): + mid = (lo+hi)/2 + if margin(mid) > 0: + lo = mid + else: + hi = mid + return (lo+hi)/2 + + +def run(): + cases = [] + for p in range(1, 9): + actual = thin_reference(p) + need(actual == formula(p), 'Full exact Laurent formula, p='+str(p)) + size = 2*p + total = [[sum(m[i][j] for m in actual.values()) for j in range(size)] for i in range(size)] + need(total == [[Q(i == j) for j in range(size)] for i in range(size)], 'A(1)=identity; no normalization needed') + limit, degrees = weighted_limit(actual, p) + need(sum(sum(m[i][i] for m in limit.values()) for i in range(size)) == size, 'Full diagonal rank') + need(max(degrees) == p-1, 'Exact border degree') + # Reduction mod 2 is coefficientwise; no complex-to-BIT native lift is claimed. + need(all(x.denominator == 1 for m in actual.values() for row in m for x in row), 'Integral identity reduces to characteristic two') + need(thin_reference(p, True) != actual, 'Incorrect reverse sign is rejected over Q') + if p > 1: + try: + weighted_limit(actual, p, reverse=True) + except ValueError: + pass + else: + raise ValueError('Reversed scaling must be rejected') + cases.append({'pairs': p, 'laurent_coefficients': len(actual), 'border_degree': p-1, + 'exact_formula': True, 'integral_reduction': True, 'decoder': decoder_check(p)}) + locals_ = local_profiles() + sweep = [] + for p in range(1, 65): + row = {'pairs': p} + for kind in locals_: + targets, paid = profiles(p, kind, locals_) + block, ports, helpers, _ = locals_[kind] + main = main_profile(p, block, ports) + mean = sum(k*v for k, v in main.items())/sum(main.values()) + optimistic = Counter({k: (p+2)*v for k, v in helpers.items()}) + optimistic[mean] += sum(main.values()) + row[kind] = {'raw_border_root_estimate': estimate_root(targets, paid), + 'balanced_main_root_estimate': estimate_root(optimistic, paid)} + if p == 16: + row[kind].update(targets=dict(sorted(targets.items())), paid=dict(sorted(paid.items()))) + sweep.append(row) + return {'status': 'PASS_EXACT_NO_IDLE_BORDER_ALGEBRA', 'cases': cases, + 'root_evidence': 'floating-point discovery only; no certified kappa or admitted supplier', + 'sweep': sweep, 'corrected_all_moment_certificate': correction_moment_certificate(locals_)} + + +if __name__ == '__main__': + print(json.dumps(run(), sort_keys=True, indent=2)) diff --git a/research/controller-border-interface/budget.py b/research/controller-border-interface/budget.py new file mode 100644 index 0000000000..82f8cbe95f --- /dev/null +++ b/research/controller-border-interface/budget.py @@ -0,0 +1,208 @@ +"""Exact optimistic moment obstruction for idle-free border controllers. + +This proves a finite-invoice obstruction, conditional on the stated determinant +and output-count invariants. It does not certify a native border implementation. +All numerical bounds use integer comparisons, not floating point arithmetic. +Prepared by Dillon with substantial OpenAI Codex assistance. Apache-2.0. +""" +from collections import Counter +from fractions import Fraction as Q +from functools import lru_cache +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PRECISION = 48 + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +@lru_cache(None) +def power(base, exponent): + """Outward dyadic enclosure of integer base**rational exponent in [0,1].""" + exponent = Q(exponent) + need(isinstance(base, int) and base >= 1, "Positive integer power base") + need(0 <= exponent <= 1, "Power exponent in [0,1]") + if exponent in (0, 1) or base == 1: + value = Q(base if exponent else 1) + return value, value + scale = 1 << PRECISION + a, q = exponent.numerator, exponent.denominator + target = base ** a * scale ** q + lo, hi = scale, base * scale + while hi - lo > 1: + mid = (lo + hi) // 2 + if mid ** q <= target: + lo = mid + else: + hi = mid + need(lo ** q <= target < (lo + 1) ** q, "Exact nth-root enclosure") + return Q(lo, scale), Q(lo + 1, scale) + + +def add(*values): + return sum(x[0] for x in values), sum(x[1] for x in values) + + +def scale(value, factor): + products = [value[0] * factor, value[1] * factor] + return min(products), max(products) + + +def point(value): + return Q(value), Q(value) + + +def moment(profile, t): + return add(*(scale(power(r, t), count) for r, count in profile.items())) + + +def shown(value): + return {"lower": str(value[0]), "upper": str(value[1])} + + +def read_profiles(): + complex_data = json.loads((ROOT / "research/joint-helper-lattice/RESULT.json").read_text()) + bit_data = json.loads((ROOT / "research/query-thinned-controllers/BIT-CONTROLLER.json").read_text())["invoice"] + complex_h = {int(r): n for r, n in complex_data["local_helpers"].items()} + complex_c = {int(r): n for r, n in complex_data["local_paid"].items()} + full = bit_data["thick_calls"] + bit_target = Counter({int(r): n for r, n in bit_data["targets"].items()}) + bit_cost = Counter({int(r): n for r, n in bit_data["paid"].items()}) + bit_target.subtract({int(r): n for r, n in bit_data["main"].items()}) + bit_cost.subtract({int(r): n for r, n in bit_data["whole_idle"].items()}) + bit_cost[1] -= bit_data["thin_queries"] + need(full > 0 and all(n >= 0 and n % full == 0 for n in [*bit_target.values(), *bit_cost.values()]), + "Exact BIT local profile division") + bit_h = {r: n // full for r, n in bit_target.items() if n} + bit_c = {r: n // full for r, n in bit_cost.items() if n} + need(complex_h == {4: 28, 7: 7, 8: 47, 9: 326}, "Pinned complex helpers") + need(complex_c == {1: 2237, 2: 388, 3: 494, 4: 147, 5: 36, 8: 8}, "Pinned complex paid calls") + need(bit_h == {8: 439}, "Pinned BIT helpers") + need(bit_c == {1: 1323, 2: 1342, 3: 79, 4: 44, 5: 102, 6: 11, 7: 19}, "Pinned BIT paid calls") + return {"complex": (8, 112, complex_h, complex_c, Q(6)), + "BIT": (7, 111, bit_h, bit_c, Q(15, 2))} + + +def coefficients(b, v, helpers, paid, saving): + t = 1 - Q(saving) + h = add(moment(helpers, t), scale(moment(paid, t), -1)) + a = add(scale(power(1 + b, t), 2 * v), h, point(-v)) + exact_b = add(scale(add(power(1 + 2 * b, t), scale(power(1 + b, t), -1)), 4 * v), scale(h, 2), point(v)) + # Concavity gives x**t <= u**t + t*u**(t-1)*(x-u). + # Here u=1+b, x=1+b+2b/p; using u**(t-1)=u**t/u. + jensen_b = add(scale(power(1 + b, t), Q(4 * v * b) * t / (1 + b)), scale(h, 2), point(v)) + first = add(scale(power(1 + 3 * b, t), 2 * v), scale(h, 3)) + second = add(scale(power(1 + 2 * b, t), 4 * v), scale(h, 4), point(-v)) + return {"saving": str(saving), "t": str(t), "h": h, "A": a, + "exact_B": exact_b, "Jensen_B": jensen_b, + "p_one_margin": first, "p_two_margin": second} + + +def explicit_profiles(b, v, helpers, paid, p): + need(isinstance(p, int) and p >= 1, "Positive controller parameter") + target = Counter({r: (p + 2) * n for r, n in helpers.items()}) + cost = Counter({r: (p + 2) * n for r, n in paid.items()}) + cost[1] += v * (p - 1) + if p == 1: + target[1 + 3 * b] += 2 * v + else: + target[1 + 2 * b] += 4 * v + target[1 + b] += 2 * v * (p - 2) + return target, cost + + +def run(): + output = {"status": "PASS_OPTIMISTIC_BORDER_BUDGET_CEILING", "power_precision_bits": PRECISION, + "scope": "All positive integer p, unchanged full-call and thin-query invoices, 2vp main fields and determinant rank sum 2v[p+b(p+2)], even granting coefficient extraction and extra routing free.", + "target_saving": "1/100", "profiles": {}} + for name, (b, v, helpers, paid, separator) in read_profiles().items(): + cutoff = Q(3, 500) if name == "complex" else Q(7, 1000) + signed = {r: helpers.get(r, 0) - paid.get(r, 0) for r in set(helpers) | set(paid)} + positive = {r: n for r, n in signed.items() if n > 0} + negative = {r: -n for r, n in signed.items() if n < 0} + need(all(r > separator for r in positive), "All positive helper terms above separator") + need(all(r < separator for r in negative), "All negative helper terms below separator") + need(1 + b > separator > 1, "Jensen main base above and thin query below separator") + # Dividing the Jensen envelope by separator**t makes every summand + # strictly increasing in t. Failure at the cutoff therefore extends + # to every saving in [cutoff,1], with Jensen valid for t in [0,1]. + checks = [] + for saving in (Q(1, 100), cutoff): + row = coefficients(b, v, helpers, paid, saving) + need(row["A"][1] < 0 and row["Jensen_B"][1] < 0, "All-p Jensen upper bound is negative") + need(row["p_one_margin"][1] < 0 and row["p_two_margin"][1] < 0, "Explicit p=1 and p=2 are negative") + need(row["exact_B"][1] < 0, "Explicit affine intercept is negative") + checks.append({k: shown(value) if isinstance(value, tuple) else value for k, value in row.items()}) + controls = {} + for p in (1, 2, 3, 16, 64): + targets, costs = explicit_profiles(b, v, helpers, paid, p) + rank_margin = sum(r * n for r, n in targets.items()) - sum(r * n for r, n in costs.items()) + need(rank_margin == 48 * p - (16 if name == "complex" else 15), "Independent exact rank-surplus control") + if p >= 2: + row = coefficients(b, v, helpers, paid, cutoff) + direct = add(moment(targets, 1 - cutoff), scale(moment(costs, 1 - cutoff), -1)) + affine = add(scale(row["A"], p), row["exact_B"]) + need(max(direct[0], affine[0]) <= min(direct[1], affine[1]), "Direct invoice and affine formula agree") + # A cheaper exponent passes this optimistic necessary test. This guards + # against a verifier that rejects every controller by construction. + saving, p = (Q(1, 200), 32) if name == "complex" else (Q(3, 500), 64) + targets, costs = explicit_profiles(b, v, helpers, paid, p) + margin = add(moment(targets, 1 - saving), scale(moment(costs, 1 - saving), -1)) + need(margin[0] > 0, "Strict positive optimistic invoice control") + controls["smaller_saving_pass"] = {"saving": str(saving), "p": p, "margin": shown(margin), + "scope": "Necessary moment test only; no border extraction or native admission claimed."} + # Omitting the thin-query bill reverses the target-exponent conclusion. + # The row is a deliberately invalid invoice, never a candidate result. + targets, costs = explicit_profiles(b, v, helpers, paid, 64) + costs[1] -= v * 63 + undercharged = add(moment(targets, Q(99, 100)), scale(moment(costs, Q(99, 100)), -1)) + need(undercharged[0] > 0, "Missing-query-cost fault reverses the conclusion") + controls["invalid_missing_thin_queries"] = {"saving": "1/100", "p": 64, + "omitted_rank_one_calls": v * 63, + "invalid_margin": shown(undercharged)} + # Repeated whole-controller evaluations may keep every independent + # helper, but only one copy of each intended main output is required. + # K>=2 therefore has main + K*(full helpers - full costs - thin costs). + # At K=2,t=1 the determinant fixes an affine, strictly negative margin. + # Rank separation proves negativity for all t in [0,1], and h(t)<0 + # makes every additional evaluation strictly worse. + local_rank_difference = sum(r * n for r, n in signed.items()) + need(local_rank_difference < 0, "Local helper-minus-paid moment negative at t=1") + k2_slope = 2 * v * (1 + b) + 2 * local_rank_difference - 2 * v + k2_intercept = 4 * v * b + 4 * local_rank_difference + 2 * v + need(k2_slope < 0 and k2_intercept < 0, "Two-evaluation rank margin negative for every p") + for trial_p in (1, 2, 3, 16, 64): + trial_targets, trial_costs = explicit_profiles(b, v, helpers, paid, trial_p) + trial_targets.update({r: (trial_p + 2) * n for r, n in helpers.items()}) + direct_k2_rank = sum(r * n for r, n in trial_targets.items()) - 2 * sum(r * n for r, n in trial_costs.items()) + need(direct_k2_rank == k2_slope * trial_p + k2_intercept, + "Direct twice-evaluated invoice credits fresh helpers and main once") + # Deliberately crediting duplicate main outputs is an invalid positive + # control: repetition does not produce additional independent outputs. + targets, costs = explicit_profiles(b, v, helpers, paid, 2) + single_rank_margin = sum(r * n for r, n in targets.items()) - sum(r * n for r, n in costs.items()) + need(single_rank_margin > 0, "Duplicating every credited output would spuriously pass at t=1") + repeated = {"minimum_evaluations": 2, "all_integer_p_at_least": 1, + "all_savings": ["0", "1"], + "two_evaluation_rank_margin": {"coefficient_of_p": k2_slope, "constant": k2_intercept}, + "local_rank_helper_minus_paid": local_rank_difference, + "independent_helpers_credited_per_evaluation": True, + "main_outputs_credited_once": True, + "scope": "Whole-controller repeated evaluations with unchanged local invoices; no general exactification barrier.", + "invalid_duplicate_main_credit_control": {"p": 2, "saving": "0", "wrong_margin": 2 * single_rank_margin, + "correct_margin": 2 * k2_slope + k2_intercept}} + output["profiles"][name] = {"block": b, "ports": v, "ceiling_strict": str(cutoff), + "excluded_savings": [str(cutoff), "1"], "separator": str(separator), + "signed_helpers_minus_paid": dict(sorted(signed.items())), + "checks": checks, "controls": controls, + "repeated_evaluation_obstruction": repeated} + return output + + +if __name__ == "__main__": + print(json.dumps(run(), indent=2, sort_keys=True)) diff --git a/research/controller-border-interface/independent_check.py b/research/controller-border-interface/independent_check.py new file mode 100644 index 0000000000..45bf36a9de --- /dev/null +++ b/research/controller-border-interface/independent_check.py @@ -0,0 +1,186 @@ +#!/usr/bin/env python3 +"""Independent exact p2/p3 event check; Apache-2.0. + +Prepared by Dillon with substantial OpenAI assistance. This is an independent +AI review path, not independent human review or formal-kernel verification. +No local construction or predecessor implementation is imported. +""" +from fractions import Fraction as F +from itertools import product +import json + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def identity(n): + return [[F(i == j) for j in range(n)] for i in range(n)] + + +def literal(p, q, stage): + # Numeric exact execution on all input columns; no source emitter imported. + rows=identity(2*p) + def add(dst,src,c): + rows[dst]=[a+c*b for a,b in zip(rows[dst],rows[src])] + def forward(pair,d): + x,y=2*pair,2*pair+1 + add(y,x,1/q) + rows[x]=[d*a for a in rows[x]] + rows[y]=[d*a for a in rows[y]] + def backward(pair,d): + x,y=2*pair,2*pair+1 + add(x,y,-q) + rows[x]=[d*a for a in rows[x]] + rows[y]=[d*a for a in rows[y]] + def bridge(dst,src,c): + add(2*dst,2*src,c) + add(2*src+1,2*dst+1,-c) + forward(0,stage[0]) + for pair in range(p): + backward(pair,stage[2*pair+1]) + if pair+1F(1,2**requested_bits), + 'Dropping h*k fails for an actual permitted additive error') + cases.append({'requested_bits':requested_bits, 'pole_order':pole_order, + 'dyadic_epsilon_exponent':k, 'funded_fractional_bits':fractional_bits, + 'funded_error':str(abs(computed-x)), + 'underfunded_error':str(abs(wrong-x))}) + return cases + + +def run(): + checks=0 + samples=[] + for p in (2,3): + for seed in range(1,13): + q=F(seed+1,seed+2) + stage=[F(seed+2*j+3,2*j+2) for j in range(2*p+1)] + A=literal(p,q,stage) + expected,ds=closed(p,q,stage) + need(A==expected, 'Literal event matrix agrees with independently hardcoded p2/p3 matrix') + wanted=[[A[i][j] if i==j else F(0) for j in range(2*p)] for i in range(2*p)] + extracted=extraction([scaled(A,p,F(e)) for e in range(1,p+1)]) + need(extracted==wanted, 'Forward Lagrange extraction returns every diagonal column') + wrong=extraction([scaled(A,p,F(e),True) for e in range(1,p+1)]) + need(wrong!=wanted, 'Opposite weights must fail forward extraction') + inverse_transpose=list(map(list,zip(*inverse(A)))) + backward=extraction([scaled(inverse_transpose,p,F(e),True) for e in range(1,p+1)]) + wanted_back=[[1/A[i][j] if i==j else F(0) for j in range(2*p)] for i in range(2*p)] + need(backward==wanted_back, 'Inverse-transpose extraction with reversed weights') + wrong_back=extraction([scaled(inverse_transpose,p,F(e)) for e in range(1,p+1)]) + need(wrong_back!=wanted_back, 'Same forward weights must fail inverse-transpose extraction') + checks+=1 + if seed==1:samples.append({'p':p,'q':str(q),'stages':list(map(str,stage)), + 'literal_matrix':[[str(x) for x in row] for row in A]}) + return {'status':'PASS_INDEPENDENT_RATIONAL_P2_P3', 'exact_instances':checks,'all_columns':True,'forward_and_inverse_transpose_extraction':True, 'wrong_weight_controls_rejected':2*checks,'samples':samples, 'degree_growth_controls':degree_controls(), 'conditioning_controls':precision_controls()} + + +if __name__ == "__main__": + print(json.dumps(run(), sort_keys=True, indent=2)) diff --git a/research/controller-border-interface/verify.py b/research/controller-border-interface/verify.py new file mode 100644 index 0000000000..825e283958 --- /dev/null +++ b/research/controller-border-interface/verify.py @@ -0,0 +1,81 @@ +#!/usr/bin/env python3 +"""Replay scoped border identities and costs; no native admission. + +Dillon with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +import hashlib +import importlib.util +import json +from pathlib import Path +import sys + +sys.dont_write_bytecode = True +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def module(name): + spec = importlib.util.spec_from_file_location('border_' + name, HERE / (name + '.py')) + out = importlib.util.module_from_spec(spec) + spec.loader.exec_module(out) + return out + + +def replay(): + pins = json.loads((HERE / 'SOURCES.json').read_text()) + hashes = {} + for row in pins['files']: + if row['usage'] != 'input': + continue + digest = hashlib.sha256((ROOT / row['path']).read_bytes()).hexdigest() + need(digest == row['sha256'], 'Authenticated scientific input: ' + row['path']) + hashes[row['path']] = digest + algebra = module('border_algebra').run() + # Discovery roots are deliberately excluded from the exact receipt. + sweep = algebra.pop('sweep') + p16 = next(row for row in sweep if row['pairs'] == 16) + algebra.pop('root_evidence') + algebra['p16_profiles'] = { + name: {key: p16[name][key] for key in ('targets', 'paid')} + for name in ('complex', 'bit') + } + algebra['discovery_not_certified'] = 'Floating root estimates are omitted from this exact receipt.' + result = { + 'status': 'PASS_SCOPED_CONTROLLER_BORDER_INTERFACE', + 'claim': 'Formal border construction and scoped cost obstructions; no admitted supplier or kappa.', + 'source_sha256': hashes, + 'algebra': algebra, + 'budget': module('budget').run(), + 'independent': module('independent_check').run(), + } + return json.loads(json.dumps(result, sort_keys=True)) + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--write', action='store_true', help='Authoring only: replace the exact receipt') + args = parser.parse_args() + result = replay() + receipt = HERE / 'RESULT.json' + if args.write: + receipt.write_text(json.dumps(result, indent=2, sort_keys=True) + '\n') + else: + need(result == json.loads(receipt.read_text()), 'Exact receipt matches replay') + print(json.dumps({ + 'status': result['status'], + 'exact_laurent_pair_counts': [x['pairs'] for x in result['algebra']['cases']], + 'independent_rational_instances': result['independent']['exact_instances'], + 'wrong_weight_rejections': result['independent']['wrong_weight_controls_rejected'], + 'budget_scope': 'all positive p; fixed inventories and declared determinant/output contract', + 'new_kappa': None, + }, sort_keys=True)) + + +if __name__ == '__main__': + main()