diff --git a/research/kappa-architecture-frontier/CLAIMS.md b/research/kappa-architecture-frontier/CLAIMS.md new file mode 100644 index 0000000000..91b6ae1fb6 --- /dev/null +++ b/research/kappa-architecture-frontier/CLAIMS.md @@ -0,0 +1,75 @@ +# Claims since κ=.0023: architecture, evidence and limits + +Checkpoint: canonical main `32890bc5de034ab8fc93ac88ead7279a6a416d04`, +2026-10-25. Source heads, blob IDs and SHA256 are in SOURCES.json and ORIGINS.json. These are +selected milestones and relevant high claims, not an exhaustive claim census. +No PR, Discussion or intake disposition is changed by this local draft. + +| Claim | Architectural change | Status used here | +|---|---|---| +| [#4359](https://github.com/CrocSwap/integer-mult-bounds/pull/4359), .0023 | Credit independent productive helpers; mixed-rank recursive compiler and a complete outer bill | Historical selected conditional result, not a cap on descendants | +| [#4440](https://github.com/CrocSwap/integer-mult-bounds/pull/4440), .00296 | Replace FULL stages by genuine queries, losing their helper credit and specializing their stage factors | Historical conditional proposal in selected ancestry | +| [#4470](https://github.com/CrocSwap/integer-mult-bounds/pull/4470), .00302015 | Longer optimized productive path and native/helper lineage | Historical selected conditional checkpoint | +| [#4610](https://github.com/CrocSwap/integer-mult-bounds/pull/4610), .0030217758 | Native paid-profile improvement under retained productive path | Historical selected conditional checkpoint; new arithmetic sharpens its all-path cap to <.00302177587079 | +| [#5377](https://github.com/CrocSwap/integer-mult-bounds/pull/5377), .00302235; [#5383](https://github.com/CrocSwap/integer-mult-bounds/pull/5383), .00302666 | Owned helper relations change the charged local debt | Retained ancestry; not merely outer rounding | +| [#5387](https://github.com/CrocSwap/integer-mult-bounds/pull/5387), .003026674765 | Smaller compiler/completion reserve | Funding improvement to the same economic proposal | +| [#5392](https://github.com/CrocSwap/integer-mult-bounds/pull/5392), .00302725; [#5398](https://github.com/CrocSwap/integer-mult-bounds/pull/5398), .00302728823 | Owned circuit transposition, then a direct backward caller | Stronger fully charged local contract; raw profile later retained by neutral completion | +| [#5413](https://github.com/CrocSwap/integer-mult-bounds/pull/5413), .003027288235 | Complete the coupled provider, paying and crediting equal extra H8 jobs | Current selected conditional result; signed moment unchanged by that neutral completion | +| [#5462](https://github.com/CrocSwap/integer-mult-bounds/pull/5462), .0030272882389; [#5468](https://github.com/CrocSwap/integer-mult-bounds/pull/5468), .0030272882489783 | Compiler/precision headroom inside the same raw profile | Open numerical refinements, not new recursive economics; bounded by the same raw root | +| [#5544](https://github.com/CrocSwap/integer-mult-bounds/pull/5544), .00304057 | Productive P104 provider with 104 ports and 527 helper outputs | Open complete conditional proposal; source receipt independently rebound to path arithmetic here | +| [#5545](https://github.com/CrocSwap/integer-mult-bounds/pull/5545), .00304117 | Legal paid contact H1+H5 -> H6 | Open proposal; strict raw benefit at every 0 1 and local debt L. The new +parts are the application to P104, the price frontier and the closure result. + +## Price frontier for changed providers + +Write the optimal invoice with n FULLs as C_n = nL + v·c_n(t), where c_n +depends only on the path geometry and t. Then λ_b(t) = max_n (−c_n/n). A +provider that keeps v, b and the controller contract must cut net local debt +per FULL by more than min_n C_n/n. Each new repair request counts against that +saving. The minimizing n depends only on b and t, not on the local word. Three +rational signs certify it over all n, so no large-controller search is needed. + +| Target C | Best FULL count | Net saving needed per FULL from [#5551](https://github.com/CrocSwap/integer-mult-bounds/pull/5551) | From [#5413](https://github.com/CrocSwap/integer-mult-bounds/pull/5413) | +|---|---:|---:|---:| +| .0031 | 18 | .80638594481 | .99667194384 | +| .0033 | 17 | 3.54923453123 | 3.72139618536 | +| .0034 | 16 | 4.91394927369 | 5.07657009697 | +| .004 | 14 | 12.96623724304 | 13.06167562796 | +| .006 | 9 | 38.56153416704 | 38.34368776890 | +| .01 | 5 | 85.66448729816 | 84.53539335470 | + +Values are rounded down; the exact outward endpoints are in RESULT.json. Units +are rank-power moments, not ADD counts. For scale, [#5551](https://github.com/CrocSwap/integer-mult-bounds/pull/5551)'s net local debt is +L(t) ≈ 1736 at C=.0034. At C=.006 and C=.01, the 112-port neutral bill needs *less* +saving than the 104-port [#5551](https://github.com/CrocSwap/integer-mult-bounds/pull/5551). P104's advantage near the current crossing +does not persist at every tested target; a changed provider's port count must +be included in the comparison. + +**Why .0034:** it is the selected outer contract's admitted BIT budget. With +that budget fixed, a change to COMPLEX alone cannot promote κ ≥ .0034, whatever +the frontier says. This limit belongs to the outer interface. It is not a BIT +impossibility result. + +**Why the margins are small:** every completed native profile here has +L(1) = 17v − 48. At t = 1 the optimal invoice therefore has surplus exactly +48n − v: 752 for the selected n=18 invoice and 760 for P104. The positive-C +crossing still depends on how paid and target ranks are distributed. + +To price a new autonomous bill (`ports`, `paid`, `helper_targets`): + +```sh +python3.12 -B research/kappa-architecture-frontier/verify.py --price PROFILE.json --C 0.0034 +``` + +The command reports exact discount bounds and the all-n certificate. If an +interval sign is ambiguous, or the minimizer lies beyond n=4096, it fails as +unknown. It does not inspect a native word or admit a supplier. + +## Closure: what cannot amplify a failed bill + +Fix t and take bills that each fail the moment test. None of the following +produces a passing bill: + +- disjoint combinations; +- positive scaling; +- declared tensor products; +- exact acyclic typed cancellation; +- charged splitting or completion. + +So more tensor depth, batching, repetition or a finer funding grid cannot +rescue a failed bill. A mixture of compatible autonomous providers cannot beat +its best member. None of this covers: + +- a new cross-boundary consumer; +- correlated or coded outputs; +- a changed idle law or controller graph; +- an arbitrary native refactorization. + +## Relation to other claims + +The frontier assumes autonomous outputs, so it neither refutes nor supports +the coded, centre-free p19 proposal +[#5440](https://github.com/CrocSwap/integer-mult-bounds/pull/5440) +(.0033999964). That PR is outside this contract. Its source at `c0f52b5b` +reports `FINDING_PRECOMPILATION_CONTRACT_MISSING` and +`kappa_attached_to_physical_chain: false`. The claim map lists it separately +from admitted results for that reason. The floating-point LP screens in +[#5465](https://github.com/CrocSwap/integer-mult-bounds/pull/5465) are not used +as lower bounds. They cover one word or commutation poset, not a redesigned +native word. + +## Evidence and scope + +The selected construction, frontier, allocation and queue dispositions remain unchanged. + +See [the proof](PROOF.md), [claim map](CLAIMS.md), [exact receipt](RESULT.json), +[source origins](ORIGINS.json) and [validation](VALIDATION.md). The checks use +an independent rational engine written with only the Python standard library: +interval arithmetic on a 2²²⁴ grid, with no floating-point acceptance. The +engine: + +- reconstructs every coefficient of four complete source invoices; +- proves six all-length gates that also cover every larger saving; +- proves thirteen all-length discount gates; +- checks 912 small-mask comparisons. + +Fourteen rejection controls reject changed source bytes, forged Git trees, +omitted query/idle/helper bills and false admission receipts. They pass in +both normal and optimized Python. + +Validation used CPython 3.12.8, registered serial replays and a Git-free, +network-free read-only export (archive SHA256 `c741d2d2…`). The caps are raw +moment theorems under the stated controller and local contracts. Native words +and the five framework assumptions are inherited. This package does not claim +a whole selected replay, a proof-kernel theorem, hosted CI or independent +human acceptance. + +## Open next questions + +- **Native lower bound at .0034.** Can any legal rank-eight native + factorization beat [#5551](https://github.com/CrocSwap/integer-mult-bounds/pull/5551) by more than 4.91394927369 units per FULL? A yes needs a + complete charged word. A no must cover arbitrary factorizations, not one + poset. +- **Lower [#5440](https://github.com/CrocSwap/integer-mult-bounds/pull/5440)'s coded consumer.** Price its actual native event chain, + keeping recodings, phases, ownership and all later calls. +- **Change an invariant.** Change one query, idle, state or geometry + invariant and derive its full optimistic invoice before extending a search. +- **Check the ratio-frontier proof.** Independently check the written proof, + especially the n=2/3 convexity junction and the J_(n+1)−J_n sign gate. The + finite controls do not replace this check. + +We retain the productive/compiler lineage of +[Cinna Davis](https://github.com/1337isnot1337), +[Cao Yifan](https://github.com/intqwq), +[Dillon Amburgey](https://github.com/dillona), +[Jacob Alan Sussman](https://github.com/jacobalansussman), +[Ali Romman](https://github.com/aliromman), +[Chris R](https://github.com/Clear1nsight), +[Gareth Davidson](https://github.com/bitplane), +[David Arias](https://github.com/DavidAriasC), +[thu-nmrc](https://github.com/thu-nmrc), +[zxv](https://github.com/zxv) and all notices in the unchanged source extracts. +Prepared with substantial OpenAI Codex assistance; Apache-2.0. diff --git a/research/kappa-architecture-frontier/PROOF.md b/research/kappa-architecture-frontier/PROOF.md new file mode 100644 index 0000000000..619859b959 --- /dev/null +++ b/research/kappa-architecture-frontier/PROOF.md @@ -0,0 +1,402 @@ +# Architectural limits of productive-helper path constructions + +Prepared for [zxv](https://github.com/zxv) with substantial OpenAI Codex +assistance. Apache-2.0. This is a written proof with exact arithmetic support, +not a proof-kernel theorem or a new supplier admission. + +## 1. The architecture, and the question it actually answers + +The change introduced by [PR4359](https://github.com/CrocSwap/integer-mult-bounds/pull/4359) +at κ=.0023 was **productive mixed jobs**. Arbitrary independent helper inputs +finish with autonomous transforms and earn output credit. Their ranks need not +match one another or the paid recursive ranks. A finite compiler turns that +mixed template into a uniform supplier. The supplier test is + +\[ + M_t(P)1 per FULL; b=8 in every numerical + application here; +* an autonomous local paid histogram P and productive helper histogram H, + with local net debt L(t)=M_t(P)-M_t(H); +* any pair count p>=1, any split a+(p-1-a), and any binary mask on 2p+1 + stage positions; +* every QUERY costs v rank-one jobs and earns no helper credit; +* main and whole-idle jobs are exactly those in equation (1) below. Native + realization is allowed to restrict the family further. + +These are architectural hypotheses, not an enumeration of a fixed word. +All p, all splits and all masks are included. Different local words can be +substituted provided the same controller contract is established. A changed +query tariff, nonautonomous outputs, another connection graph, another idle +law or a different degree/rank rule is a different problem. + +For n FULL stages, let h_j count the FULL stages preceding a side window in +its outside-to-inside reading, excluding its even stage e_j in {0,1}. For +left windows j<=a this is h_j=sum_(s<2j) x_s; for right windows j>a it is +h_j=sum_(s>2j) x_s. Put f(z)=z^t, f(0)=0. The complete paid-minus-target bill is + +\[ + E=v(2p+1)+(L-v)n-2v f(1+bn) + +2v\sum_{j=1}^{p-1}\{f(bh_j)+e_j f(b)-f(1+b(h_j+e_j))\}. \tag{1} +\] + +In particular, turning an even stage FULL restores its paid middle idle. +Deleting its query while retaining old helper credit is a different, invalid +invoice. Recomputing the n=18 invoice from (1)'s canonical mask reproduces +**every paid and productive coefficient** in the retained neutral5413 and +three P104 source receipts. This binds the arithmetic to those submitted +bills. It does not freshly validate their native words or universal premises. + +## 2. All masks reduce to one canonical invoice per FULL count + +This section generalizes the existing exchange and convexity proofs of +[PR5405](https://github.com/CrocSwap/integer-mult-bounds/pull/5405) and +[PR5409](https://github.com/CrocSwap/integer-mult-bounds/pull/5409) to arbitrary +v, b>1 and L. Their frozen proofs are retained in `inputs/`; the reduction is +credited prior work. The new application to P104 and the per-FULL price +frontier below use that parameter independence explicitly. + +Let delta(z)=f(z+1)-f(z). It is positive and strictly decreasing for z>=0, +with delta(0)=1. On either side read one end bit, then pairs (o,e). At fixed +n the local term does not change, so compare only query and window costs. +The following changes never increase E: + +1. Delete a 00 pair. Its change divided by 2v is -1+delta(bk)<=0, where k + is the preceding FULL count. +2. Replace 01 by 10. The change is f(b(k+1))-f(bk)-f(b)<=0 by subadditivity. +3. Split 11 into 10,10. The change is + 1+f(bk+2b)-f(bk+b+1)-f(b)<0. Both differences compare integrals of + t*z^(t-1) over intervals of length b-1: [1,b] and [bk+b+1,bk+2b]. + +Each change includes all added/deleted QUERY costs. After these operations +only 10 side pairs remain. Move their FULL bits into any missing end/central +unpaired positions. Each move deletes one pair and changes E/(2v) by +-1+delta(bk)<0 for k>=1. For n<=2 this leaves p=1, all n FULL bits unpaired. +For n>=3 all three unpaired positions become FULL, leaving n-3 side pairs. + +Finally balance the two sides. A side with q pairs contributes +-sum_(k=2)^(q+1) delta(bk). Its successive increments are increasing, so a +transfer from a side at least two pairs longer to the shorter side decreases +cost. Thus a=floor((n-3)/2), d=ceil((n-3)/2) attain the minimum. + +The **attained optimistic minimum** at fixed n is therefore + +\[ + C_n(t)=3v+(L-v)n-2v(1+bn)^t,\qquad n=0,1,2, \tag{2} +\] + +and, for n>=3, + +\[ + C_n(t)=nL+v(n-3)-2v(1+bn)^t + -2v\left[\sum_{k=2}^{a+1}\delta(bk)+\sum_{k=2}^{d+1}\delta(bk)\right]. \tag{3} +\] + +Empty sums vanish. The first expression extended to n=3 equals the second. +These are invoice comparisons. They need not be physical rewrites preserving +one particular caller's inputs. + +For completeness put A_n=f(bn+b+1)-f(bn+1), D_n=C_(n+1)-C_n. Then + +\[ + D_n=L-v-2vA_n\quad(n=0,1,2), +\] + +\[ + D_n=L+v-2vA_n-2v\delta(b\lfloor(n+1)/2\rfloor)\quad(n>=3). +\] + +A_n strictly decreases. Across the only junction, +D_3-D_2=2v[1-delta(2b)+A_2-A_3]>0. Thereafter the delta correction never +increases. Hence C_n is strictly discretely convex on **every integer n>=0**, +independently of L. The three signs + +\[ + C_m>0,\quad D_{m-1}<0,\quad D_m>0 \tag{4} +\] + +prove E>0 for every p, split and mask. There is no unsearched large-p tail. + +## 3. A price frontier for every changed local provider + +Write C_n=nL+v c_n, where c_n depends only on b,t,n. For n>=1 define + +\[ + \lambda_b(t)=\max_{n>=1}\frac{-c_n(t)}n. +\] + +The maximum exists: c_1=2-2(1+b)^t<0, whereas c_n/n tends to 1. +For the latter limit, the main term is O(n^t) and the side sums are O(n^t), +using delta(bk)<=t*(bk)^(t-1). Dividing by n makes both vanish. A negative +minimum of c_n/n is therefore attained at a finite n. + +Then equation (1)'s entire controller family has a positive raw surplus +if and only if + +\[ + \boxed{L(t)\Delta_{\rm req}(t) + :=L(t)-v\lambda_b(t)=\min_{n>=1}C_n(t)/n.} \tag{6} +\] + +A fixed boundary charge is additional; a per-FULL repair reduces Delta by +its full price. No free repair allowance is implicit. + +This is an **architectural search filter**: a proposal can be rejected +before constructing a long controller if its optimistic net saving does not +cross (6). It applies to any local mechanism satisfying these interfaces, +not just neighboring edits of the selected native word. + +The infinite ratio minimization also needs only three values. Let + +\[ + J_n=nC_{n+1}-(n+1)C_n. +\] + +Then + +\[ + J_{n+1}-J_n=(n+1)(D_{n+1}-D_n)>0, +\] + +and C_(n+1)/(n+1)-C_n/n has the sign of J_n. Thus +J_(m-1)<0=1. +Both J signs are independent of L; c_n and the optimal count are independent +of v as well. **The best FULL count for a fixed required per-FULL discount +is determined by the path geometry and exponent, not by the local word.** + +This ratio gate is distinct from minimizing C_n for a fixed provider. Using +the latter minimizer in (6) without a new argument is invalid. + +## 4. Extend point exclusions to every larger exponent saving + +A sign at one C alone is not an interval theorem. Here is a reusable +sufficient condition for monotonicity. Let b>1 and define + +\[ + U=-\frac{P_1\log b}{b} + +\sum_{r>b}P_r\frac rb\log(r/b) + +\sum_{rb using (r/b)^t<=r/b, +and those from helper ranks r=1 every remaining window has h>=1 if e=0, +or h>=0,e=1. Its normalized term is + +\[ + h^t+e-(h+e+1/b)^t. +\] + +Its derivative is negative, because z^t log z increases for z>=1; the +h=0,e=1 case is 1-(1+1/b)^t. The normalized long target has negative +derivative, and the nonnegative query term decreases. The local part is +strictly decreasing by U<0. Thus normalized E decreases in t. Every reduced +invoice positive at t0 stays positive for 0=C0, C<1**. +The verifier proves U<0 separately for every numerical profile here, with +upper bounds below -549. No unsupported signed-moment monotonicity is used. + +## 5. New all-length numerical consequences + +The exact integer interval engine independently reconstructs each source +invoice. It uses a 2^224 grid, atanh logarithms with a rational tail and +Taylor exponentials with a rational tail; see section 8. It verifies a +negative canonical witness at each lower endpoint and (4) and U<0 at each +upper endpoint. Hence these enclose the supremum over the **entire** stated +path family: + +| Local contract | Lower raw crossing | Upper raw crossing | FULL count at upper gate | +|---|---:|---:|---:| +| #4610 round-three word | .00302177587077 | .00302177587079 | 18 | +| #5413 complete neutral signed invoice | .00302728824993 | .00302728824995 | 18 | +| #5544 P104 productive caller | .00304057807630 | .00304057807631 | 18 | +| #5545 P104 frame contact | .00304117181649 | .00304117181650 | 18 | +| #5551 P104 coupled contacts | .00304153116714 | .00304153116715 | 18 | +| Neutral bill minus all eight paid H8 completions | .00807671283977 | .00807671283979 | 7 | + +The P104 rows extend the submitted fixed p16 crossing calculations to all +controller lengths/splits/masks under the same invoice law. They do not +freshly certify the proposed native circuits. The final row is an unrealized +optimistic relaxation, retaining all helper targets and making the actual +eight H8 completion requests free. Its n=7 canonical controller has p=5, +split 2/2. It is not a construction or a universal minimum completion cost. + +In particular **any** change whose net saving is at most 8*8^t per FULL, +relative to the neutral bill, retaining this path contract, cannot reach +C=.01, even with arbitrary controller length. At .01 it would still need +more than 21.85249430914 further units per FULL. The earlier centre-free +#4610 bound near .0080596239 is a different, slightly weaker local profile; +it is not silently reused for the neutral word. + +All completed native profiles above have L(1)=17v-48. Equation (3) gives + +\[ + M_1(T)-M_1(P)=48n-v\quad(n>=3). +\] + +Thus the selected n=18 invoice has surplus 752 and P104 has surplus 760. +This conservation law explains the small productive margin. It does **not** +fix the positive-C crossing: the distributions of paid and target ranks +matter. The P104 successors preserve this mass while strictly lowering +positive-C price. + +At target C, a changed #5551 provider must save more than the following +amount **per FULL**, with optimal length already included. Displayed +thresholds are rounded down; exact outward endpoints are in RESULT.json. + +| C | Optimal FULL count for (6) | Required net discount from #5551 | From #5413 | +|---|---:|---:|---:| +| .0031 | 18 | .80638594481 | .99667194384 | +| .0033 | 17 | 3.54923453123 | 3.72139618536 | +| .0034 | 16 | 4.91394927369 | 5.07657009697 | +| .004 | 14 | 12.96623724304 | 13.06167562796 | +| .006 | 9 | 38.56153416704 | 38.34368776890 | +| .01 | 5 | 85.66448729816 | 84.53539335470 | + +## 6. Why derivatives cannot amplify an exhausted bill + +Here "derivative" means a construction obtained using the following allowed +operations, with their actual invoices. It does not mean all native rewrites. + +**Potential closure theorem.** Fix t and a collection of rules each satisfying +M_t(P)>=M_t(T). Allow disjoint unions, positive whole-array scaling, declared +tensor-product invoices, finite acyclic exact typed job matching/cancellation, +splitting of one job into disjoint-axis parts, and target completion with its +complement paid. None yields a rule with M_t(P)=0 to paid-minus-target cost. Additional paid reserve cannot +reverse the sign. This also permits a catalyst that returns unchanged and +cancels once on each side. It does not permit double credit for a shared +input, a new joint consumer, correlated outputs, or an unpriced conversion. ∎ + +This is a limitation of the stated moment-based construction closure, not a +lower bound on all algorithms. It rules out more tensor depth, more integer +batching, repetitions, or a finer funding grid rescuing a failed fixed bill. +A new cross-boundary identity that changes the bill escapes the theorem. + +**Compatible provider menus.** If several autonomous FULL providers have +identical v,b and main contracts, let L_min(t)=min_i L_i(t). Substituting +L_min at every FULL only decreases the invoice. Therefore a mixture of +providers cannot beat the best provider's all-length ceiling at that t. +The minimum over providers and over n commutes. Different geometries or +coupled helper contracts cannot be put in this menu without a new argument. + +**Partial-helper completion.** If rank a and complementary rank b are paid +separately to finish a helper at rank a+b, the net change is +(a+b)^t-a^t-b^t<0 in target-minus-paid surplus. Merely relabeling a partial +helper as full, with a properly charged completion, cannot improve κ. +Conversely, a legal paid-path fusion a,b -> a+b reduces price strictly. +This distinction explains the genuine direction of the P104 contact gains. +For #5551 its delta is + +\[ + 2-3\,2^t+3^t-4^t+5^t + =[3^t-2^t]+[5^t-4^t]-2[2^t-1]<0, +\] + +by decreasing unit increments. No rank-mass saving is required. + +## 7. What has and has not been closed architecturally + +There is a definitive closure of **controller-only growth at a fixed local +contract**, including arbitrary length and the composition operations above. +There is also a complete numerical filter (5) for any changed provider in +the same rank-eight path architecture. There is **no proof here that every +possible native provider obeys a particular lower bound on L(t)**. Proving +such a lower bound is exactly what a ceiling for the whole local-mechanism +architecture would require. + +For example, the claim "productive helpers cannot exceed κ≈.003" does not +follow from the all-length theorem: it freezes a profile that P104 changes. +The free-completion relaxation also has favorable raw invoices near .008, +so the path topology alone cannot imply a .003 ceiling. It does not follow +that that relaxation is physically achievable. The broad mixed-job compiler +is still more general than this path and has no architectural cap proved here. + +A universal statement would need one of the following *new* results: + +* a native lower bound L(t)>=v*lambda_b(t) over the full allowed provider + language, with arbitrary helper factorization and all charged repairs; +* a stronger typed potential valid also for coded/coupled states and their + actual consumers, rather than treating them as autonomous Gaussian jobs; +* a different invariant controlling all allowed controller graphs and idle + incidences. The prefix/suffix proof does not quantify over those graphs. + +The unchanged selected outer contract separately requires effective complex +and BIT budgets strictly above κ. Its admitted BIT budget is .0034. Thus a +COMPLEX-only change cannot promote κ>=.0034 using that fixed budget. This is +an outer-interface restriction, not a BIT impossibility theorem; the actual +ordinary BIT saving, later BIT improvements and a rederived outer contract +are separate questions. Likewise the first-order mass identity 48n-v does +not supply the missing native bound. + +## 8. Exact arithmetic and replay boundary + +For a positive integer r, put k=floor(log2 r) and z=(r-2^k)/(r+2^k) in +[0,1/3]. Use log r=k log2+2 atanh z, with log2=2 atanh(1/3). After 96 +terms the omitted positive log tail is bounded by + +\[ + \frac{2z^{193}}{193(1-z^2)}. +\] + +Every operation is enclosed on the 2^224 grid by floor/ceiling integer +arithmetic. To evaluate exp(x), 0<=x<=16, evaluate exp(x/16) through degree +64. Since 0<=x/16<=1, its remaining tail is at most +66/(65*65!). Four outward squarings enclose exp(x). No floating-point number, +optimizer result, sampling assumption or decimal tolerance accepts a sign. + +The code authenticates raw retained sources with SHA256, Git blob IDs and +complete hash-checked commit/tree paths in ORIGINS.json. Pending source commits +are not claimed as publication ancestors. Compressed Git tree objects are +size-bounded before parsing. It +rebuilds all four current complete invoices, and compares fresh results to +the entire frozen typed receipt. Controls enumerate every mask/split through +p=3 at two rational exponents and check canonical dominance, source accounting, +concavity directions, exact elementary identities and rejection of a false +ceiling below the P104 crossing. The infinite statements rest on the written +proof, not the finite controls. All acceptance predicates survive Python -O. + +There is no imported native interpreter, enormous uniform template, Lean +build, Docker run, whole selected replay, or independent human audit in this +package. Source publication/review status is preserved in CLAIMS.md; copying +an exact source receipt does not turn its author-side checks into new native +verification. diff --git a/research/kappa-architecture-frontier/README.md b/research/kappa-architecture-frontier/README.md new file mode 100644 index 0000000000..aed6dbad18 --- /dev/null +++ b/research/kappa-architecture-frontier/README.md @@ -0,0 +1,163 @@ +# Architectural κ ceilings and a price frontier for productive helpers + +**The rank-eight productive-helper path is exhausted at a fixed local bill; +productive-helper recursion as a whole is not proved exhausted.** This package +turns that distinction into a usable mathematical filter for new constructions. +It supplies no new admitted κ and changes no selected result or task allocation. + +The selected conditional result at canonical main +`32890bc5de034ab8fc93ac88ead7279a6a416d04` is +[PR5413](https://github.com/CrocSwap/integer-mult-bounds/pull/5413), +κ=.003027288235. The newer P104 candidates change the local paid profile, so +an old fixed-profile ceiling does not exclude them. Their strongest retained +candidate is [PR5551](https://github.com/CrocSwap/integer-mult-bounds/pull/5551), +κ=.00304153, head `1123635a6f63f23638df9459c994160e5e649d30`, still an +unselected author-checked proposal at this checkpoint. + +Read [PROOF.md](PROOF.md) for the complete architecture, universal reductions, +closure theorem and rigorous numerical method; [CLAIMS.md](CLAIMS.md) for the +post-.0023 claims and their different admission boundaries. [RESULT.json](RESULT.json) +contains every exact sign, root bracket, discount interval and source-derived +histogram. Canonical provenance is in [SOURCES.json](SOURCES.json); +[ORIGINS.json](ORIGINS.json) includes the exact commit/tree/blob paths for all +retained extracts, including pending PR heads. Their offline checks need no +cached PR branch and make no publication-ancestry claim for those pending heads. [RESEARCH-CONTEXT.json](RESEARCH-CONTEXT.json) records overlap coverage +and live heads. Submitted for review as +[PR5554](https://github.com/CrocSwap/integer-mult-bounds/pull/5554); +publication does not imply scientific acceptance. + +## What is actually proved + +For an autonomous local provider with v ports, rank-eight fresh blocks, one +rank-one query per port, and the retained prefix/suffix idle law, **all** +controller lengths, splits and FULL/QUERY masks reduce to a strictly convex +sequence indexed only by the FULL count n. The exchange/convexity argument +extends credited [PR5405](https://github.com/CrocSwap/integer-mult-bounds/pull/5405) +and [PR5409](https://github.com/CrocSwap/integer-mult-bounds/pull/5409). +The P104 applications and the architectural per-FULL discount curve are new +results in this package, without a claim of exhaustive novelty. + +The supremum of the relaxed raw moment saving lies in these intervals: + +| Local contract | Supremum interval over every length/split/mask | +|---|---| +| #4610 native word | (.00302177587077, .00302177587079) | +| #5413 complete neutral signed bill | (.00302728824993, .00302728824995) | +| #5544 P104 productive word | (.00304057807630, .00304057807631) | +| #5545 P104 single contact | (.00304117181649, .00304117181650) | +| #5551 P104 coupled contacts | (.00304153116714, .00304153116715) | +| Neutral bill with all eight H8 completion calls free | (.00807671283977, .00807671283979) | + +The last row is a hypothetical upper relaxation, not an attainable supplier. +The first two sharpen retained ceilings; the P104 rows extend submitted +fixed-caller crossings to this unbounded architecture. Native source validity +and the five selected framework assumptions remain inherited, not freshly replayed. + +The new **price frontier** is especially useful when a local mechanism changes. +Let L(t)=sum P_r*r^t - sum H_r*r^t, t=1-C. There is an explicitly defined +geometry-only threshold lambda_8(t) such that the entire path has a favorable +raw invoice exactly when L(t)=1) C_n(t)/n. A new three-value gate +certifies that minimum over all n, with no large-controller search. + +For the #5551 baseline, the necessary net saving per FULL is: + +| Target C | Minimum saving per FULL, rounded down | Optimal FULL count | +|---|---:|---:| +| .0031 | .80638594481 | 18 | +| .0033 | 3.54923453123 | 17 | +| .0034 | 4.91394927369 | 16 | +| .004 | 12.96623724304 | 14 | +| .006 | 38.56153416704 | 9 | +| .01 | 85.66448729816 | 5 | + +These are rank-power moment units, not scalar ADD counts or wall time. +All new repair requests reduce the net saving; compiler, BIT and outer losses +need additional margin. Even making the neutral bill's eight paid H8 jobs free +still misses .01 by more than 21.85249430914 units per FULL. + +## Search directions and stopping rules + +| Architectural regime | Decision justified by the proof | What reopens it | +|---|---|---| +| Same bill, different tensor depth, integer batching or funding precision | Cannot exceed its raw crossing through the stated moment-preserving compiler closure | A changed fully charged bill or a different compiler method | +| Same local provider, arbitrary retained FULL/QUERY path | Stop controller-only κ search at its all-length cap above | Changed local debt, query price, fresh-block rank, targets or idle law | +| Compatible menu of autonomous providers with the same port/main contract | No mixture beats the best menu member at the candidate exponent | A cross-boundary consumer or a changed state/interface contract | +| Same path, redesigned native/helper factorization | Open; use the price frontier before building a controller | Complete changed local paid/helper invoice crossing the required discount | +| Coded/coupled outputs and centre removal | Open; a decoder/consumer can retain more raw headroom, but all conversions must be priced | Actual native lowering, independent targets and complete compiler/outer join | +| Other graphs, observation/state retention, larger geometry or changed coverage | Outside these ceilings | Derive that architecture's own complete optimistic bill | +| COMPLEX improvement with the selected admitted BIT budget fixed at .0034 | Cannot obtain κ>=.0034 under that fixed outer contract | A higher funded BIT budget or a changed outer transfer | + +A large architectural impossibility theorem would additionally have to bound +L(t) over **every** legal native provider. This package does not prove that +missing lower bound. The productive-helper framework is broader than a +rank-eight path, so none of these caps is a universal multiplication barrier. + +## Reproduce and screen a new bill + +Python 3.12, standard library; no heavy scientific replay is required: + +```sh +python3.12 -B scripts/research_package.py --package research/kappa-architecture-frontier +python3 -B research/kappa-architecture-frontier/verify.py --price research/kappa-architecture-frontier/EXAMPLE-PROFILE.json --C 0.0034 +``` + +The example's JSON contains `ports`, `paid`, and `helper_targets`. Replace these +with a source-bound autonomous profile only after checking the main/path contract. +The pricing command reports exact discount bounds and an all-n ratio certificate. +Positive discount means the supplied bill still needs that much net saving per +FULL; negative discount is raw margin, before extra costs. It does not inspect +a native word or admit a supplier. Ambiguous interval signs or a minimizer +beyond the explicit 4096-FULL computational cap fail as unknown. The all-n theorem +applies only after the sign gate succeeds. + +Direct offline replay of the retained package also works: + +```sh +python3 -I -B research/kappa-architecture-frontier/verify.py +python3 -I -O -B research/kappa-architecture-frontier/verify.py +``` + +The fresh checker binds four complete source invoices, proves six all-n/all-larger-C +exclusions, checks thirteen all-n price gates and 912 small-mask controls, and +compares the entire exact result. Proof and source applicability still need human +or formal review. [VALIDATION.md](VALIDATION.md) records actual executed checks. + +## Open next questions + +1. **Prove a native local-debt lower bound.** Start at C=.0034: can any legal + rank-eight native factorization under the same contract beat #5551 by more + than 4.91394927369 moment units per FULL? A positive answer needs a full + word; a negative answer must cover arbitrary factorizations, not one poset. +2. **Close a coded consumer instead of refining its root.** The p19 proposal + [PR5440](https://github.com/CrocSwap/integer-mult-bounds/pull/5440) explicitly + leaves chain-to-native-event compilation open. Bind and price one complete + actual path; symbolic diagonalization alone does not discharge that obligation. +3. **Change an architectural invariant.** Start with one changed query/idle + law, retained-state interface or geometry and derive an optimistic full bill. + Do not transfer the path's cap until the new law is shown equivalent. +4. **Validate the written universal proof.** The novel ratio frontier and its + all-n gate are small targets for human or formal checking. Finite Python + controls do not replace that audit. + +Structured questions, blockers and a bounded first step are in [TASK.json](TASK.json). + +## Credit and significance + +[Ali Romman](https://github.com/aliromman) supplies the earlier path ceiling, +owned/transposed/direct caller and P104 descendants; +[Cinna Davis](https://github.com/1337isnot1337) supplies productive helpers and +paired/query controllers; [Chris R](https://github.com/Clear1nsight) supplies +independent convexity and admission work; [Cao Yifan](https://github.com/intqwq) +supplies the native profile; [Dillon Amburgey](https://github.com/dillona) +supplies the coupled provider; [Jacob Alan Sussman](https://github.com/jacobalansussman) +supplies mixed-target recursion. Preserve [Gareth Davidson](https://github.com/bitplane), +[David Arias](https://github.com/DavidAriasC), [thu-nmrc](https://github.com/thu-nmrc), +the compiler/precision work of [zxv](https://github.com/zxv), and the predecessor +credits/notices in the unchanged source extracts. [LITERATURE.md](LITERATURE.md) +separates direct predecessors from related spectral-potential literature. + +Prepared for [zxv](https://github.com/zxv) with substantial OpenAI Codex assistance. +The practical contribution is an exact stopping rule for controller derivatives +and a measurable admission target for new local mechanisms, while keeping +unproved architectural exclusions out of research-agent guidance. diff --git a/research/kappa-architecture-frontier/RESEARCH-CONTEXT.json b/research/kappa-architecture-frontier/RESEARCH-CONTEXT.json new file mode 100644 index 0000000000..9a7ecde6c1 --- /dev/null +++ b/research/kappa-architecture-frontier/RESEARCH-CONTEXT.json @@ -0,0 +1,84 @@ +{ + "canonical_base": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "observed_at": "2026-10-25T13:46:16.783816+00:00", + "priority_revision": 7, + "selected": "0.003027288235", + "scoped_prs": [ + { + "number": 5440, + "title": "Price the p19 coded-reverse chain: conditional \u03ba = 0.0033999964", + "headRefOid": "c0f52b5b18bba78a6a5e8057edf9571bade88549", + "state": "OPEN", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5440" + }, + { + "number": 5551, + "title": "Improve complete conditional \u03ba to 0.00304153 via coupled P104 contacts", + "headRefOid": "1123635a6f63f23638df9459c994160e5e649d30", + "state": "OPEN", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5551" + }, + { + "number": 5544, + "title": "Conditional \u03ba = 0.00304057 (+1.3281765e-5 over #5413)", + "headRefOid": "e2a6cce2f9db5a2c5f9714f4b9e5292dd3a10581", + "state": "OPEN", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5544" + }, + { + "number": 5545, + "title": "Conditional \u03ba = 0.00304117 (+6.0e-7 over #5544)", + "headRefOid": "18968423711fd902aaee1099979497d55603e1dc", + "state": "OPEN", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5545" + }, + { + "number": 5462, + "title": "Conditional \u03ba = 0.0030272882389 (+3.9e-12 over #5413, numerical headroom only); exact owned-relation optimum closes the relation lever", + "headRefOid": "eb289efb4f129a0c4e592b96002dc7849e5a9e4c", + "state": "OPEN", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5462" + }, + { + "number": 5465, + "title": "Research (no \u03ba claim): reorder, re-frame and re-ranking ceilings on the #4610 productive-helper word", + "headRefOid": "b123ff44a211b9fc96b9f8fd1538e9965a95b34e", + "state": "OPEN", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5465" + } + ], + "overlap": { + "searched_at": "2026-10-25T13:48:32.652261+00:00", + "coverage": { + "local": { + "head": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "records": 1, + "head_records": 7402, + "complete_head_inventory": false + }, + "open_prs": { + "fetched_at": "2026-10-25T13:47:25.386776+00:00", + "complete_pagination": true, + "records": 410 + }, + "discussions": { + "fetched_at": "2026-10-25T13:48:31.485094+00:00", + "complete_pagination": true, + "records": 4833 + } + }, + "matches_total": 444, + "limitations": [ + "local: 7401 HEAD note paths were not searched; inspect coverage.local.unsearched_head_paths in --json output and materialize relevant notes before treating a lack of matches as evidence.", + "Relevant frozen notes additionally read through exact Git objects; not an exhaustive literature or queue census." + ] + }, + "publication": { + "status": "SUBMITTED_FOR_REVIEW", + "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/5554", + "is_draft": false, + "initial_head": "739e3095c9864f53af1da7c7af5a634c7a369d2c" + }, + "intake_decisions_changed": false, + "initial_publication": "LOCAL_DRAFT_ONLY" +} diff --git a/research/kappa-architecture-frontier/RESULT.json b/research/kappa-architecture-frontier/RESULT.json new file mode 100644 index 0000000000..1fccef0029 --- /dev/null +++ b/research/kappa-architecture-frontier/RESULT.json @@ -0,0 +1,516 @@ +{ + "claims_are_raw_moment_bounds": true, + "controls": { + "accounting_controls": 3, + "arithmetic_identities": 4, + "concavity_controls": 9, + "false_ceiling_rejected": true, + "tiny_mask_comparisons": 912 + }, + "discounts": { + "neutral5413": [ + { + "C": "31/10000", + "discount": { + "lower": "13435111225355571331756923051397943420338548743584571525746347524607/13479973333575319897333507543509815336818572211270286240551805124608", + "upper": "13435111225355571331756923051397943420338548743584571525746370253927/13479973333575319897333507543509815336818572211270286240551805124608" + }, + "minimizing_full_count": 18, + "next_ratio_numerator": { + "lower": "41369429537091919579918373588873825733947128764515469904942288753953/13479973333575319897333507543509815336818572211270286240551805124608", + "upper": "41369429537091919579918373588873825733947128764515469904958186074447/13479973333575319897333507543509815336818572211270286240551805124608" + }, + "previous_ratio_numerator": { + "lower": "-31669794144442014629503574842857285054987807310792873773846140086757/13479973333575319897333507543509815336818572211270286240551805124608", + "upper": "-31669794144442014629503574842857285054987807310792873773832563688203/13479973333575319897333507543509815336818572211270286240551805124608" + } + }, + { + "C": "33/10000", + "discount": { + "lower": "50164321342425608720207746144231985624749244324847321534793300981777/13479973333575319897333507543509815336818572211270286240551805124608", + "upper": "50164321342425608720207746144231985624749244324847321534793322542781/13479973333575319897333507543509815336818572211270286240551805124608" + }, + "minimizing_full_count": 17, + "next_ratio_numerator": { + "lower": "62188127465679389003408242653599699622800843711133290773363554388875/13479973333575319897333507543509815336818572211270286240551805124608", + "upper": "62188127465679389003408242653599699622800843711133290773377082373589/13479973333575319897333507543509815336818572211270286240551805124608" + }, + "previous_ratio_numerator": { + "lower": "-4365714639701698733786574044895646993380320300645324314710758015879/1684996666696914987166688442938726917102321526408785780068975640576", + "upper": "-4365714639701698733786574044895646993380320300645324314709323494417/1684996666696914987166688442938726917102321526408785780068975640576" + } + }, + { + "C": "17/5000", + "discount": { + "lower": "68432029533213544708961805851028357735072014971626947370831270058459/13479973333575319897333507543509815336818572211270286240551805124608", + "upper": "68432029533213544708961805851028357735072014971626947370831290624399/13479973333575319897333507543509815336818572211270286240551805124608" + }, + "minimizing_full_count": 16, + "next_ratio_numerator": { + "lower": "282828661067020932558454998566798440548573718824488437569652750525/421249166674228746791672110734681729275580381602196445017243910144", + "upper": "282828661067020932558454998566798440548573718824488437570010380233/421249166674228746791672110734681729275580381602196445017243910144" + }, + "previous_ratio_numerator": { + "lower": "-2215222074033864360443544012183020961965791710744912855095974554495/421249166674228746791672110734681729275580381602196445017243910144", + "upper": "-2215222074033864360443544012183020961965791710744912855095674946603/421249166674228746791672110734681729275580381602196445017243910144" + } + }, + { + "C": "1/250", + "discount": { + "lower": "352142078313581828675748055887482270973995334241928104545591543040117/26959946667150639794667015087019630673637144422540572481103610249216", + "upper": "352142078313581828675748055887482270973995334241928104545591580197473/26959946667150639794667015087019630673637144422540572481103610249216" + }, + "minimizing_full_count": 14, + "next_ratio_numerator": { + "lower": "15278288194985232875943467572389856730002827331783939954954936650977/3369993333393829974333376885877453834204643052817571560137951281152", + "upper": "15278288194985232875943467572389856730002827331783939954956933960375/3369993333393829974333376885877453834204643052817571560137951281152" + }, + "previous_ratio_numerator": { + "lower": "-8141296755171998117734526840617333941813554218193767611208161249405/3369993333393829974333376885877453834204643052817571560137951281152", + "upper": "-8141296755171998117734526840617333941813554218193767611206517099891/3369993333393829974333376885877453834204643052817571560137951281152" + } + }, + { + "C": "3/500", + "discount": { + "lower": "1033743777271554374582524697057465044922375045810586878410787231158155/26959946667150639794667015087019630673637144422540572481103610249216", + "upper": "516871888635777187291262348528732522461187522905293439205393629074305/13479973333575319897333507543509815336818572211270286240551805124608" + }, + "minimizing_full_count": 9, + "next_ratio_numerator": { + "lower": "30466110883618098238830248698690440011772352034142358923193029491929/6739986666787659948666753771754907668409286105635143120275902562304", + "upper": "30466110883618098238830248698690440011772352034142358923194294150887/6739986666787659948666753771754907668409286105635143120275902562304" + }, + "previous_ratio_numerator": { + "lower": "-14092465552448043713654497009086861788339346291712548047625827878223/1684996666696914987166688442938726917102321526408785780068975640576", + "upper": "-14092465552448043713654497009086861788339346291712548047625592917383/1684996666696914987166688442938726917102321526408785780068975640576" + } + }, + { + "C": "1/100", + "discount": { + "lower": "569767424082377898524682710323872463605366538008857460824132872567135/6739986666787659948666753771754907668409286105635143120275902562304", + "upper": "1139534848164755797049365420647744927210733076017714921648265754289859/13479973333575319897333507543509815336818572211270286240551805124608" + }, + "minimizing_full_count": 5, + "next_ratio_numerator": { + "lower": "2840488524600177893361152778384174690909685381026597817876617596615/842498333348457493583344221469363458551160763204392890034487820288", + "upper": "2840488524600177893361152778384174690909685381026597817876654130509/842498333348457493583344221469363458551160763204392890034487820288" + }, + "previous_ratio_numerator": { + "lower": "-3721585567362612084991689218763520831692262988633136058161827013509/210624583337114373395836055367340864637790190801098222508621955072", + "upper": "-14886342269450448339966756875054083326769051954532544232647286318125/842498333348457493583344221469363458551160763204392890034487820288" + } + } + ], + "neutral_free_eight_H8": [ + { + "C": "1/100", + "discount": { + "lower": "147285520279684187910890110061971286111545759339627167495999715226431/6739986666787659948666753771754907668409286105635143120275902562304", + "upper": "294571040559368375821780220123942572223091518679254334991999439561443/13479973333575319897333507543509815336818572211270286240551805124608" + }, + "minimizing_full_count": 5, + "next_ratio_numerator": { + "lower": "2840488524600177893361152778384174690909685381026597817876617684755/842498333348457493583344221469363458551160763204392890034487820288", + "upper": "2840488524600177893361152778384174690909685381026597817876654042369/842498333348457493583344221469363458551160763204392890034487820288" + }, + "previous_ratio_numerator": { + "lower": "-3721585567362612084991689218763520831692262988633136058161826998819/210624583337114373395836055367340864637790190801098222508621955072", + "upper": "-14886342269450448339966756875054083326769051954532544232647286376885/842498333348457493583344221469363458551160763204392890034487820288" + } + } + ], + "p104_5551": [ + { + "C": "31/10000", + "discount": { + "lower": "21740122065360455269535245049364532588634596703780030831266783371205/26959946667150639794667015087019630673637144422540572481103610249216", + "upper": "1358757629085028454345952815585283286789662293986251926954176737495/1684996666696914987166688442938726917102321526408785780068975640576" + }, + "minimizing_full_count": 18, + "next_ratio_numerator": { + "lower": "9603617571110624188195336725988566688237726320333948370790079393099/3369993333393829974333376885877453834204643052817571560137951281152", + "upper": "9603617571110624188195336725988566688237726320333948370793959406351/3369993333393829974333376885877453834204643052817571560137951281152" + }, + "previous_ratio_numerator": { + "lower": "-7351916497816896253277615588520441173479312411434059983214367325021/3369993333393829974333376885877453834204643052817571560137951281152", + "upper": "-7351916497816896253277615588520441173479312411434059983211046051309/3369993333393829974333376885877453834204643052817571560137951281152" + } + }, + { + "C": "33/10000", + "discount": { + "lower": "95687173671257084959753938883188673085976753485216550596169871488479/26959946667150639794667015087019630673637144422540572481103610249216", + "upper": "95687173671257084959753938883188673085976753485216550596169913744139/26959946667150639794667015087019630673637144422540572481103610249216" + }, + "minimizing_full_count": 17, + "next_ratio_numerator": { + "lower": "57746118360988004074593368178342578221172212017480912860980104650343/13479973333575319897333507543509815336818572211270286240551805124608", + "upper": "57746118360988004074593368178342578221172212017480912860993343771945/13479973333575319897333507543509815336818572211270286240551805124608" + }, + "previous_ratio_numerator": { + "lower": "-253367367482687872942970815105550941580107874591023286121608844151/105312291668557186697918027683670432318895095400549111254310977536", + "upper": "-1013469469930751491771883260422203766320431498364093144486083545429/421249166674228746791672110734681729275580381602196445017243910144" + } + }, + { + "C": "17/5000", + "discount": { + "lower": "33119952585962594860759107363400598526575675188063391062858246919281/6739986666787659948666753771754907668409286105635143120275902562304", + "upper": "4139994073245324357594888420425074815821959398507923882857282126965/842498333348457493583344221469363458551160763204392890034487820288" + }, + "minimizing_full_count": 16, + "next_ratio_numerator": { + "lower": "525253227695896017608559283052625675304494049245478526915050762959/842498333348457493583344221469363458551160763204392890034487820288", + "upper": "525253227695896017608559283052625675304494049245478526915752194163/842498333348457493583344221469363458551160763204392890034487820288" + }, + "previous_ratio_numerator": { + "lower": "-4113983851777176669395153165482753215079327462811981016606826325925/842498333348457493583344221469363458551160763204392890034487820288", + "upper": "-4113983851777176669395153165482753215079327462811981016606237033257/842498333348457493583344221469363458551160763204392890034487820288" + } + }, + { + "C": "1/250", + "discount": { + "lower": "174784532273083063966897910713565383237036918589054782200365750834861/13479973333575319897333507543509815336818572211270286240551805124608", + "upper": "87392266136541531983448955356782691618518459294527391100182884593393/6739986666787659948666753771754907668409286105635143120275902562304" + }, + "minimizing_full_count": 14, + "next_ratio_numerator": { + "lower": "56747927581373722110647165268876610711439072946626062689832390784461/13479973333575319897333507543509815336818572211270286240551805124608", + "upper": "56747927581373722110647165268876610711439072946626062689840271486275/13479973333575319897333507543509815336818572211270286240551805124608" + }, + "previous_ratio_numerator": { + "lower": "-30239102233495993008728242550864383212450344239005422555916227751545/13479973333575319897333507543509815336818572211270286240551805124608", + "upper": "-30239102233495993008728242550864383212450344239005422555909720402983/13479973333575319897333507543509815336818572211270286240551805124608" + } + }, + { + "C": "3/500", + "discount": { + "lower": "32488028267094640260477371606278585811496152867060647393529592786531/842498333348457493583344221469363458551160763204392890034487820288", + "upper": "1039616904547028488335275891400914745967876891745940716592946996431519/26959946667150639794667015087019630673637144422540572481103610249216" + }, + "minimizing_full_count": 9, + "next_ratio_numerator": { + "lower": "28289960106216805507485230934498265725217184031703619000107763600513/6739986666787659948666753771754907668409286105635143120275902562304", + "upper": "28289960106216805507485230934498265725217184031703619000109036924959/6739986666787659948666753771754907668409286105635143120275902562304" + }, + "previous_ratio_numerator": { + "lower": "-13085860870130326305536318651294943089172250128018794615652564358177/1684996666696914987166688442938726917102321526408785780068975640576", + "upper": "-1635732608766290788192039831411867886146531266002349326956540797575/210624583337114373395836055367340864637790190801098222508621955072" + } + }, + { + "C": "1/100", + "discount": { + "lower": "2309510008827372147755540751820925291577935187741880459973063445970147/26959946667150639794667015087019630673637144422540572481103610249216", + "upper": "2309510008827372147755540751820925291577935187741880459973063465156997/26959946667150639794667015087019630673637144422540572481103610249216" + }, + "minimizing_full_count": 5, + "next_ratio_numerator": { + "lower": "21100771897029892922111420639425297703900519973340440932797714340615/6739986666787659948666753771754907668409286105635143120275902562304", + "upper": "21100771897029892922111420639425297703900519973340440932798018489449/6739986666787659948666753771754907668409286105635143120275902562304" + }, + "previous_ratio_numerator": { + "lower": "-55292128429387379548447954107343738070856478688263735721261435374023/3369993333393829974333376885877453834204643052817571560137951281152", + "upper": "-55292128429387379548447954107343738070856478688263735721261343722575/3369993333393829974333376885877453834204643052817571560137951281152" + } + } + ] + }, + "grid": "26959946667150639794667015087019630673637144422540572481103610249216", + "native_or_outer_admission": false, + "profiles": { + "neutral5413": { + "all_exponent_derivative_upper": { + "lower": "-14819453259751087327681736535623410179955395429977366944489843696284011/26959946667150639794667015087019630673637144422540572481103610249216", + "upper": "-1852431657468885915960217066952926272494424428747170868061230462011269/3369993333393829974333376885877453834204643052817571560137951281152" + }, + "all_n_upper_gate": { + "C": "60545764999/20000000000000", + "minimizing_full_count": 18, + "minimum": { + "lower": "17365981811369536624542685309676679789464709308378030066743/6739986666787659948666753771754907668409286105635143120275902562304", + "upper": "17365981811369536624542685309676679789464709308378235132523/6739986666787659948666753771754907668409286105635143120275902562304" + }, + "next_difference": { + "lower": "306644532268807331246480182824904395892844907695217969738895153991/13479973333575319897333507543509815336818572211270286240551805124608", + "upper": "306644532268807331246480182824904395892844907695217969739757062083/13479973333575319897333507543509815336818572211270286240551805124608" + }, + "previous_difference": { + "lower": "-3657637398192586363104458510199967189985942317913526055576153953101/13479973333575319897333507543509815336818572211270286240551805124608", + "upper": "-3657637398192586363104458510199967189985942317913526055575375554585/13479973333575319897333507543509815336818572211270286240551805124608" + } + }, + "helper_targets": { + "4": 28, + "7": 7, + "8": 55, + "9": 318 + }, + "lower_witness": { + "lower": "-15898299427311844329560382407514249936093956453396927459983/6739986666787659948666753771754907668409286105635143120275902562304", + "upper": "-31796598854623688659120764815028499872187912906793446136167/13479973333575319897333507543509815336818572211270286240551805124608" + }, + "paid": { + "1": 2193, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "ports": 112, + "rank_surplus_per_full": 48, + "root_bracket": [ + "0.00302728824993", + "0.00302728824995" + ] + }, + "neutral_free_eight_H8": { + "all_exponent_derivative_upper": { + "lower": "-14819453259751087327681736535623410179955395429977366944489843696284011/26959946667150639794667015087019630673637144422540572481103610249216", + "upper": "-1852431657468885915960217066952926272494424428747170868061230462011269/3369993333393829974333376885877453834204643052817571560137951281152" + }, + "all_n_upper_gate": { + "C": "807671283979/100000000000000", + "minimizing_full_count": 7, + "minimum": { + "lower": "26646295441119935566844262936347077293006517884192560087301/26959946667150639794667015087019630673637144422540572481103610249216", + "upper": "6661573860279983891711065734086769323251629471048179172435/6739986666787659948666753771754907668409286105635143120275902562304" + }, + "next_difference": { + "lower": "12185604611510325457184480647133511257331968342016764101225319136243/6739986666787659948666753771754907668409286105635143120275902562304", + "upper": "48742418446041301828737922588534045029327873368067056404901632488827/26959946667150639794667015087019630673637144422540572481103610249216" + }, + "previous_difference": { + "lower": "-17320189741819345121133976116836762337015007662192294847269989529619/26959946667150639794667015087019630673637144422540572481103610249216", + "upper": "-8660094870909672560566988058418381168507503831096147423634854417603/13479973333575319897333507543509815336818572211270286240551805124608" + } + }, + "helper_targets": { + "4": 28, + "7": 7, + "8": 55, + "9": 318 + }, + "lower_witness": { + "lower": "-8778238229058483356581362680043895110957210261337031207597/13479973333575319897333507543509815336818572211270286240551805124608", + "upper": "-17556476458116966713162725360087790221914420522673905814701/26959946667150639794667015087019630673637144422540572481103610249216" + }, + "paid": { + "1": 2193, + "2": 412, + "3": 510, + "4": 127, + "5": 40 + }, + "ports": 112, + "rank_surplus_per_full": 112, + "root_bracket": [ + "0.00807671283977", + "0.00807671283979" + ] + }, + "p104_5544": { + "all_exponent_derivative_upper": { + "lower": "-7761263711189648296500478678115347130838972559207812737530880925045833/13479973333575319897333507543509815336818572211270286240551805124608", + "upper": "-15522527422379296593000957356230694261677945118415625475061761849795603/26959946667150639794667015087019630673637144422540572481103610249216" + }, + "all_n_upper_gate": { + "C": "304057807631/100000000000000", + "minimizing_full_count": 18, + "minimum": { + "lower": "5985686962159911019938784587993077886315646894191413040763/13479973333575319897333507543509815336818572211270286240551805124608", + "upper": "374105435134994438746174036749567367894727930886988295599/842498333348457493583344221469363458551160763204392890034487820288" + }, + "next_difference": { + "lower": "1245721742708767195514430977892748274558260908990995033425723858057/26959946667150639794667015087019630673637144422540572481103610249216", + "upper": "622860871354383597757215488946374137279130454495497516713701417025/13479973333575319897333507543509815336818572211270286240551805124608" + }, + "previous_difference": { + "lower": "-3074124439514336577340200022443425099777343867246644595928509647409/13479973333575319897333507543509815336818572211270286240551805124608", + "upper": "-6148248879028673154680400044886850199554687734493289191855499957155/26959946667150639794667015087019630673637144422540572481103610249216" + } + }, + "helper_targets": { + "4": 51, + "5": 36, + "7": 24, + "8": 122, + "9": 294 + }, + "lower_witness": { + "lower": "-6873292907668418781237140228084874073323461681706225072123/3369993333393829974333376885877453834204643052817571560137951281152", + "upper": "-6873292907668418781237140228084874073323461681706125102929/3369993333393829974333376885877453834204643052817571560137951281152" + }, + "paid": { + "1": 2429, + "2": 557, + "3": 389, + "4": 112, + "5": 108, + "6": 16, + "7": 13, + "9": 1 + }, + "ports": 104, + "rank_surplus_per_full": 48, + "root_bracket": [ + "0.00304057807630", + "0.00304057807631" + ] + }, + "p104_5545": { + "all_exponent_derivative_upper": { + "lower": "-3878879929561663339473306936422833672773057703611185571690872000237545/6739986666787659948666753771754907668409286105635143120275902562304", + "upper": "-7757759859123326678946613872845667345546115407222371143381744000327095/13479973333575319897333507543509815336818572211270286240551805124608" + }, + "all_n_upper_gate": { + "C": "6082343633/2000000000000", + "minimizing_full_count": 18, + "minimum": { + "lower": "7663894726077874865740588430377130380513057231044182588549/3369993333393829974333376885877453834204643052817571560137951281152", + "upper": "15327789452155749731481176860754260761026114462088564782929/6739986666787659948666753771754907668409286105635143120275902562304" + }, + "next_difference": { + "lower": "79745722345286193943079728408270534411367578817466928597769793289/1684996666696914987166688442938726917102321526408785780068975640576", + "upper": "637965778762289551544637827266164275290940630539735428782996273075/13479973333575319897333507543509815336818572211270286240551805124608" + }, + "previous_difference": { + "lower": "-3059728323561390422573404983694193652008942019567886988698433292545/13479973333575319897333507543509815336818572211270286240551805124608", + "upper": "-764932080890347605643351245923548413002235504891971747174418732499/3369993333393829974333376885877453834204643052817571560137951281152" + } + }, + "helper_targets": { + "4": 51, + "5": 36, + "7": 24, + "8": 122, + "9": 294 + }, + "lower_witness": { + "lower": "-2816683198789060987670803086900470154333403814839979213909/13479973333575319897333507543509815336818572211270286240551805124608", + "upper": "-1408341599394530493835401543450235077166701907419790868037/6739986666787659948666753771754907668409286105635143120275902562304" + }, + "paid": { + "1": 2428, + "2": 557, + "3": 389, + "4": 112, + "5": 107, + "6": 17, + "7": 13, + "9": 1 + }, + "ports": 104, + "rank_surplus_per_full": 48, + "root_bracket": [ + "0.00304117181649", + "0.00304117181650" + ] + }, + "p104_5551": { + "all_exponent_derivative_upper": { + "lower": "-15529535126511939828108686966770053832263659422386508663360035699233151/26959946667150639794667015087019630673637144422540572481103610249216", + "upper": "-1941191890813992478513585870846256729032957427798313582920004462367127/3369993333393829974333376885877453834204643052817571560137951281152" + }, + "all_n_upper_gate": { + "C": "60830623343/20000000000000", + "minimizing_full_count": 18, + "minimum": { + "lower": "14258400059275768604622942150690359450126349481897137595519/13479973333575319897333507543509815336818572211270286240551805124608", + "upper": "7129200029637884302311471075345179725063174740948768939521/6739986666787659948666753771754907668409286105635143120275902562304" + }, + "next_difference": { + "lower": "1294215420278687351067398338098074118122147848071167409127935998337/26959946667150639794667015087019630673637144422540572481103610249216", + "upper": "161776927534835918883424792262259264765268481008895926141201929479/3369993333393829974333376885877453834204643052817571560137951281152" + }, + "previous_difference": { + "lower": "-1525507686545301162683253422387430173029376627639360332679947300969/6739986666787659948666753771754907668409286105635143120275902562304", + "upper": "-6102030746181204650733013689549720692117506510557441330718268122675/26959946667150639794667015087019630673637144422540572481103610249216" + } + }, + "helper_targets": { + "4": 51, + "5": 36, + "7": 24, + "8": 122, + "9": 294 + }, + "lower_witness": { + "lower": "-19209878913248771314666727502341551822285447011715683458631/13479973333575319897333507543509815336818572211270286240551805124608", + "upper": "-4802469728312192828666681875585387955571361752928821043591/3369993333393829974333376885877453834204643052817571560137951281152" + }, + "paid": { + "1": 2430, + "2": 554, + "3": 390, + "4": 111, + "5": 108, + "6": 17, + "7": 13, + "9": 1 + }, + "ports": 104, + "rank_surplus_per_full": 48, + "root_bracket": [ + "0.00304153116714", + "0.00304153116715" + ] + }, + "round3_4610": { + "all_exponent_derivative_upper": { + "lower": "-1859439361601529151067946677492285843080138732718054056359504311176987/3369993333393829974333376885877453834204643052817571560137951281152", + "upper": "-7437757446406116604271786709969143372320554930872216225438017244610729/13479973333575319897333507543509815336818572211270286240551805124608" + }, + "all_n_upper_gate": { + "C": "302177587079/100000000000000", + "minimizing_full_count": 18, + "minimum": { + "lower": "2794673998164790825159557423095572822503452784446523431017/842498333348457493583344221469363458551160763204392890034487820288", + "upper": "11178695992659163300638229692382291290013811137786195953219/3369993333393829974333376885877453834204643052817571560137951281152" + }, + "next_difference": { + "lower": "38899178163491392398301040940561448328502594200583489903320931735/3369993333393829974333376885877453834204643052817571560137951281152", + "upper": "77798356326982784796602081881122896657005188401166979807071550745/6739986666787659948666753771754907668409286105635143120275902562304" + }, + "previous_difference": { + "lower": "-1900798545561878532684598373420267171581600504237378550656139324923/6739986666787659948666753771754907668409286105635143120275902562304", + "upper": "-950399272780939266342299186710133585790800252118689275327875485139/3369993333393829974333376885877453834204643052817571560137951281152" + } + }, + "helper_targets": { + "4": 28, + "7": 7, + "8": 47, + "9": 326 + }, + "lower_witness": { + "lower": "-10968113917561668611233645841225390694491248887721241193941/6739986666787659948666753771754907668409286105635143120275902562304", + "upper": "-21936227835123337222467291682450781388982497775442072019967/13479973333575319897333507543509815336818572211270286240551805124608" + }, + "paid": { + "1": 2201, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "ports": 112, + "rank_surplus_per_full": 48, + "root_bracket": [ + "0.00302177587077", + "0.00302177587079" + ] + } + }, + "retained_admitted_BIT_budget": "17/5000", + "schema": "kappa-architecture-frontier/v1" +} diff --git a/research/kappa-architecture-frontier/SOURCES.json b/research/kappa-architecture-frontier/SOURCES.json new file mode 100644 index 0000000000..6b0993b829 --- /dev/null +++ b/research/kappa-architecture-frontier/SOURCES.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903", + "retained_path": "inputs/selected.json" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "certificates/frontier5413/CLAIM.json", + "usage": "provenance", + "git_blob": "b2b7e3edb561ab1c371513dc46c9d292bab78ae4", + "sha256": "344a955984f2daee912592d63810af9e7c8e61771b871c77a25b5b8c76809694", + "retained_path": "inputs/selected-claim.json" + }, + { + "path": "docs/research/pr-intake-evidence/pr5413/fresh/primary/invoice-funding/INVOICE-NEUTRAL-LITERAL.json", + "usage": "provenance", + "git_blob": "d66216ad80b502c4042979269655bacb9f6668b9", + "sha256": "e7df9fe1a7a00f67bbf35e9b155537fd26a0c05b61788653b878bd84d9006450", + "retained_path": "inputs/neutral-invoice.json" + }, + { + "path": "research/controller-thinning-global-ceiling/PROOF.md", + "usage": "provenance", + "git_blob": "92b6fc3c7cf45a9b1c5dde8e89a1b6469b33f304", + "sha256": "f412e272b2dcfefce6917881b173069e335d4bcd908b7e8fd946e10d43981f9a", + "retained_path": "inputs/round3-proof.md" + }, + { + "path": "research/controller-ceiling-convexity/numerical/inputs/5405-concavity-exchange-reduction.md", + "usage": "provenance", + "git_blob": "e0f0ce8a01fc3bce3df5b9cb2a2d33ede4d824ef", + "sha256": "0e575a88d28db5aecc5ccf24504923a0508ff976d05f92e91e6d48408b7688ea", + "retained_path": "inputs/exchange-proof.md" + }, + { + "path": "research/controller-ceiling-convexity/numerical/inputs/5405-discrete-convexity-three-value-gate.md", + "usage": "provenance", + "git_blob": "d464faf030fe15acbe95d44177e19580d88a66ed", + "sha256": "bdad476f31b450e1ac4d1fd0d9530b43e33ebac48accc0956b38a9634b40a929", + "retained_path": "inputs/convexity-proof.md" + } + ] +} diff --git a/research/kappa-architecture-frontier/TASK.json b/research/kappa-architecture-frontier/TASK.json new file mode 100644 index 0000000000..843b143922 --- /dev/null +++ b/research/kappa-architecture-frontier/TASK.json @@ -0,0 +1,118 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 7, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "original_card": { + "id": "independent-moment", + "question": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/staged544-mixed-fourth-entry/README.md", + "research/staged-fourth-mixture-ceiling/README.md", + "research/r437-two-window-carrier/README.md" + ], + "methods": [ + "Independently reconstruct one changed paid ledger or pooled dual with exact source and model binding.", + "Check a genuinely uncovered moment implication with a different enclosure method and semantic controls." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Choose one uncovered implication in #4088 literal mixed fill, #4091 pooled dual/model binding or #4067 changed frame/host bill. #4091 pins an earlier #4088 head: validate word, capacity and stock equivalence before applying that ceiling to the later fill.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Independently reconstruct one changed ledger or pooled certificate with a positive case and a semantic failure control. Compare exact sources and name what existing checks miss. Keep this separate from supplier-boundary-audit (ordinary/outer dispatch) and uniform-transfer-audit (all-size proof). Stop after the chosen implication; more digits of an unchanged root are not additional mechanism coverage.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification.", + "Calling an aggregate histogram or source archive an independently accepted physical supplier." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering", + "4088", + "4091", + "4067", + "staged544-mixed-fourth-entry", + "staged-fourth-mixture-ceiling", + "r437-two-window-carrier" + ], + "existing_checks": [ + { + "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.", + "evidence": "research/staged-fourth-mixture-ceiling/README.md", + "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.", + "status": "author-checked", + "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.", + "evidence": "research/r437-two-window-carrier/README.md", + "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.", + "status": "author-checked", + "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove architectural limits of post-.0023 productive-helper path descendants, including an all-length local-debt frontier and source-bound P104 ceilings.", + "scope_change_reason": "Explicit donor assignment asks for architectural regime limits and a local draft PR, rather than the historical card's individual ledger audit.", + "bottleneck_link": "An exact local-debt threshold eliminates exhausted controller derivatives and states the quantitative obligation for new native mechanisms.", + "budget_minutes": 60, + "stop_rule": "Finish source-bound arithmetic, universal written arguments, normal/optimized and Git-free replays and local PR draft. Do not run the whole frontier or publish externally.", + "outcome": "completed", + "evidence": "PROOF.md, RESULT.json, CLAIMS.md, SOURCES.json and VALIDATION.md", + "author": "zxv", + "ai_assistance": "Substantial OpenAI Codex assistance, one agent. Written universal proof and arithmetic checks; no human or proof-kernel acceptance.", + "open_questions": [ + { + "question": "Does any legal redesigned native rank-eight factorization beat the local-debt threshold at C=.0034?", + "why_it_matters": "This is the missing theorem needed to exclude the entire native provider architecture rather than one bill.", + "first_step": "Produce a fully charged local profile saving more than 4.91394927369 net moment units per FULL over PR5551, or prove a native lower bound covering arbitrary factorizations.", + "blocked_by": "A bound on one fixed word/poset cannot close the full native language." + }, + { + "question": "Can the coded p19 chain be lowered to an authenticated native event program with the claimed cost?", + "why_it_matters": "Its larger planning root cannot be attached to an actual supplier while this compilation obligation remains open.", + "first_step": "Bind one complete p19 gate-to-event path including code conversions, phases, owned lifetimes and actual tariffs.", + "blocked_by": "PR5440 explicitly records missing precompilation/native attachment." + }, + { + "question": "Can another idle, observation or retained-state law cross the current path price frontier?", + "why_it_matters": "A changed architectural invariant escapes the current theorem and may remove an actual paid obligation.", + "first_step": "State one replacement interface and derive its optimistic complete invoice before extending a search.", + "blocked_by": "Its own source-compatible consumer, restoration and ordinary/outer bill must be supplied." + }, + { + "question": "Can a human or proof kernel independently validate the universal ratio frontier?", + "why_it_matters": "The infinite-family conclusions rest on the written proof, not finite code controls.", + "first_step": "Check the n=2/3 convexity junction and J_(n+1)-J_n identity against equations (2)-(3).", + "blocked_by": "Separate review or formal proof effort." + } + ] +} diff --git a/research/kappa-architecture-frontier/VALIDATION.md b/research/kappa-architecture-frontier/VALIDATION.md new file mode 100644 index 0000000000..a5aa6c3037 --- /dev/null +++ b/research/kappa-architecture-frontier/VALIDATION.md @@ -0,0 +1,80 @@ +# Validation and remaining obligations + +Executed locally on 2026-10-25, macOS, CPython 3.12.8, standard library. +The default `python3` here is 3.11.11: the registered launcher correctly +refused it before scientific execution. The registered runs below use +`python3.12`. Direct standalone checks also passed under 3.11. + +## Executed scientific checks + +```sh +python3.12 -B scripts/research_package.py --package research/kappa-architecture-frontier --check-only +python3.12 -B scripts/research_package.py --package research/kappa-architecture-frontier +python3.12 -B research/kappa-architecture-frontier/verify.py --price research/kappa-architecture-frontier/EXAMPLE-PROFILE.json --C 0.0034 +``` + +Metadata/pins and all three registered commands pass serially. The first two +commands freshly reproduce the entire RESULT.json under ordinary and optimized +Python. They verify four complete source histograms, six universal ceiling +gates with lower witnesses and all-larger-saving derivative gates, thirteen +universal ratio-minimum gates, 912 finite mask comparisons, elementary power/log +identities, concavity controls and rejection of a proposed ceiling below an +actual positive P104 witness. + +The third registered command performs **14 rejection controls** in disposable +normal/optimized copies. Changed source bytes, a forged Git tree, and a false +admission receipt are rejected end-to-end. The missing-query, missing-idle, +fake-helper and consistently changed local/global-cost cases deliberately +isolate arithmetic from source authentication; they prove the accounting and +old-ceiling gates reject even when the harness bypasses the stronger origin +check. There is no authentication-bypass mode in the accepting CLI. + +An additional independently expressed 90-digit Decimal check corroborated 30 +power enclosures, including ranks 145 and 65536. Decimal arithmetic is not an +acceptance engine or a proof of its own rounding error. + +## Source and claim coverage + +ORIGINS.json retains raw Git commits and compressed raw trees, with every object +hash and exact path edge independently checked. All thirteen retained source +extracts are authenticated without Git or network. Standard SOURCES.json pins +canonical-base provenance; pending source heads are bound through the separate +origin proof and are **not** claimed as publication ancestors. No cached PR +branch is required at runtime or for the standard metadata check. + +The last canonical fetch still returned +`32890bc5de034ab8fc93ac88ead7279a6a416d04`; the strongest retained P104 PR5551 +was still open at `1123635a6f63f23638df9459c994160e5e649d30`. The overlap +snapshot covered 410 open PRs and 4,833 Discussion records with complete remote +pagination. Sparse local note coverage was incomplete and explicitly reported; +relevant existing and pending packages were additionally read through exact +Git objects. This is not an exhaustive novelty or literature certificate. + +The full selected/native/outer replays, all-history suites, Lean and Docker were +not run. No finite program here verifies the universal written proof, proves a +native lower bound over all factorizations, or discharges the five inherited +framework assumptions. No hosted CI, independent human review or frontier +promotion is claimed. The initial PR description was prepared locally; +publication status is tracked in README.md. + +## Committed transport and offline export + +The committed-byte preflight passed on scientific commit +`83d5c58c9556065c95556cfc645cf7bd89fcd44a` for all 28 package files. +The official exporter and archive checker both passed: + +```sh +python3.12 -B scripts/check_research_commit.py --package research/kappa-architecture-frontier +python3.12 -B scripts/export_research_package.py export --package research/kappa-architecture-frontier --ref 83d5c58c9556065c95556cfc645cf7bd89fcd44a --output /tmp/kappa-architecture-frontier-83d5c58c9.tar.gz +python3.12 -B scripts/export_research_package.py check /tmp/kappa-architecture-frontier-83d5c58c9.tar.gz +``` + +The exported archive SHA256 is +`c741d2d29a36fccd43a089e79b0a8ff3ff0b2bc1a6f4ee7ef82393decccefd87`. +Its 28 payload files plus export manifest were made read-only. With empty PATH, +no Git checkout and no network calls, `/opt/local/bin/python3.12 -I -B` and +`-I -O -B` both passed the fresh checker. A source-byte mutation was rejected; +after restoring it, every file hash and mode matched the pre-run census. +No archive container hash determines mathematical equality: the complete typed +scientific receipt is compared independently. Later validation-only prose does +not alter the scientific code, source inputs or expected results at this commit. diff --git a/research/kappa-architecture-frontier/VERIFY.json b/research/kappa-architecture-frontier/VERIFY.json new file mode 100644 index 0000000000..d3f0506509 --- /dev/null +++ b/research/kappa-architecture-frontier/VERIFY.json @@ -0,0 +1,40 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Authenticate retained source bytes; rebuild four complete invoices; prove six all-n/all-larger-saving gates and thirteen all-n per-FULL price gates; run exact finite controls; compare all scientific fields." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Repeat the same explicit predicates with Python optimization enabled." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/check_controls.py" + ], + "timeout_seconds": 30, + "checks": "Reject corrupted sources and forged Git trees end-to-end; isolate semantic rejection of omitted query/idle/helper bills and changed profile under an obsolete cap; reject a false admission receipt. Repeat normal/optimized." + } + ] +} diff --git a/research/kappa-architecture-frontier/check_controls.py b/research/kappa-architecture-frontier/check_controls.py new file mode 100644 index 0000000000..ffb42afd24 --- /dev/null +++ b/research/kappa-architecture-frontier/check_controls.py @@ -0,0 +1,91 @@ +#!/usr/bin/env python3 +"""Acceptance mutations in disposable copies; no predecessor workloads.""" +from pathlib import Path +import base64 +import json +import shutil +import subprocess +import sys +import tempfile +import zlib + +ROOT = Path(__file__).resolve().parent + + +def require(c,m): + if not c: + raise ValueError(m) + + +def run(p,ok,needle='',optimized=False,semantic_only=False): + argv = [sys.executable,'-I','-B'] + (['-O'] if optimized else []) + if semantic_only: + # Deliberately isolate arithmetic/accounting rejection from the stronger + # Merkle source gate. This is a test harness, never an acceptance mode. + code = ('import importlib.util,sys; ' + 's=importlib.util.spec_from_file_location("frontier",sys.argv[1]); ' + 'm=importlib.util.module_from_spec(s); s.loader.exec_module(m); ' + 'm.authenticate=lambda:None; m.calculate()') + argv += ['-c',code,str(p/'verify.py')] + else: + argv += [str(p/'verify.py')] + r = subprocess.run(argv,text=True,capture_output=True,timeout=15) + require((r.returncode == 0) == ok,'unexpected verifier status: '+r.stdout+r.stderr) + require(needle in r.stdout+r.stderr,'missing expected rejection: '+r.stdout+r.stderr) + + +def main(): + count = 0 + for optimized in (False,True): + with tempfile.TemporaryDirectory(prefix='kappa-frontier-control-') as temp: + p = Path(temp)/'package' + shutil.copytree(ROOT,p) + run(p,True,optimized=optimized) + path = p/'inputs/p104-5551.json' + original = path.read_bytes() + origins = (p/'ORIGINS.json').read_bytes() + # Authentication failure. + path.write_bytes(original+b' ') + run(p,False,'retained source hash',optimized) + count += 1 + path.write_bytes(original) + d = json.loads(origins) + record = next(r for r in d['objects'].values() if r['type'] == 'tree') + raw = zlib.decompress(base64.b64decode(record['zlib_base64'])) + record['zlib_base64'] = base64.b64encode(zlib.compress(raw+b' ')).decode() + (p/'ORIGINS.json').write_text(json.dumps(d)) + run(p,False,'origin object hash',optimized) + count += 1 + (p/'ORIGINS.json').write_bytes(origins) + # Isolated semantic gates must reject omitted or invented work. + for kind in ('query','idle','helper'): + d = json.loads(original) + if kind == 'query': + d['complete_cost']['paid']['1'] -= 104*15 + elif kind == 'idle': + d['complete_cost']['paid']['72'] -= 208 + else: + d['local']['helpers']['9'] += 1 + path.write_text(json.dumps(d)) + run(p,False,'P104 source path invoice',optimized,semantic_only=True) + count += 1 + # Change both local and global cost consistently. This gets past + # invoice equality but must invalidate the old ceiling. + d = json.loads(original) + d['local']['paid']['1'] -= 1 + d['complete_cost']['paid']['1'] -= 18 + path.write_text(json.dumps(d)) + run(p,False,'all-n exclusion gate failed',optimized,semantic_only=True) + count += 1 + path.write_bytes(original) + expected = p/'RESULT.json' + d = json.loads(expected.read_text()) + d['native_or_outer_admission'] = True + expected.write_text(json.dumps(d)) + run(p,False,'fresh scientific result differs',optimized) + count += 1 + print('PASS_FRONTIER_ACCEPTANCE_CONTROLS:',count,'disposable normal/optimized rejections') + + +if __name__ == '__main__': + main() diff --git a/research/kappa-architecture-frontier/inputs/convexity-proof.md b/research/kappa-architecture-frontier/inputs/convexity-proof.md new file mode 100644 index 0000000000..d464faf030 --- /dev/null +++ b/research/kappa-architecture-frontier/inputs/convexity-proof.md @@ -0,0 +1,128 @@ +# #5405: strict discrete convexity and a three-value gate for the unbounded family + +**The analytic claim is valid.** For every fixed `0=0. This includes the small-count junction. Consequently one positive candidate value and the two correct neighboring signs prove positivity of the entire unbounded invoice family at that fixed t. The n>=96 tail and the author's dynamic program are unnecessary for that implication. + +This note supplies the analytic gate only. It does not evaluate the actual local profile moment, any claimed kappa, or the three numerical inequalities. A separately assigned numerical worker owns that certificate. No new paper dependency, physical caller transformation, source/native execution or coupled #5402 transfer is introduced. + +## Premises and exact canonical sequence + +The underlying primary source is [#5405 equation (1)](../../upstream-monitor-resume-20261024/5405-PROOF.md), pinned at head `314b56a6c0056c2358538f072c6fde9d365be44d`. The preceding frozen exchange proof establishes that each invoice with FULL count n has E>=C_n and that C_n is attained by another invoice in the same permitted family. That reduction, including its accounting and source scope, is a premise here. + +Write + +``` +f(z)=z^t for z>0, f(0)=0, +delta(z)=f(z+1)-f(z), +A_n=f(8n+9)-f(8n+1), +D_n=C_(n+1)-C_n. +``` + +Since 00. These follow directly by integrating the strictly decreasing positive derivative `t z^(t-1)` over intervals of fixed length eight and one respectively. + +The canonical values are + +``` +C_n=336+(L-112)n-224f(1+8n), n=0,1,2, +C_n=nL+112(n-3)-224f(1+8n) + -224[sum_(k=2)^(a+1)delta(8k) + +sum_(k=2)^(b+1)delta(8k)], n>=3, +a=floor((n-3)/2), b=ceil((n-3)/2). +``` + +Empty sums are zero. The first formula, extended to n=3, agrees with the second. + +## Exact first differences and the small-count junction + +The two balanced side counts increase alternately. When n increases to n+1, the shorter side gains a pair; on the next step the other side gains a pair at the same partial FULL count. Therefore, putting `k_n=floor((n+1)/2)` for n>=3, + +``` +D_n=L-112-224A_n, n=0,1,2, +D_n=L+112-224A_n-224delta(8k_n), n>=3. +``` + +The side correction appears twice at each successive k: k_3=k_4=2, k_5=k_6=3, and so on. In particular its first argument is 16, not 8. + +Explicit small values check both the branch point and that first repeated correction: + +``` +C_0=112, +C_1=L+224-224f(9), +C_2=2L+112-224f(17), +C_3=3L-224f(25), +C_4=4L+112-224f(33)-224delta(16), +C_5=5L+224-224f(41)-448delta(16). +``` + +For n=0,1, + +``` +D_(n+1)-D_n=224(A_n-A_(n+1))>0. +``` + +At the only junction, n=2, + +``` +D_3-D_2=224[1-delta(16)+A_2-A_3]>0. +``` + +For every n>=3, + +``` +D_(n+1)-D_n + =224[A_n-A_(n+1) + +delta(8k_n)-delta(8k_(n+1))]>0. +``` + +The first term is strictly positive. The last difference is nonnegative because k_(n+1)>=k_n; it is zero on alternate steps. Thus **D_(n+1)>D_n for every n>=0**, which is strict discrete convexity on the whole nonnegative integer domain. L cancels from each second difference, so the result is independent of its value. Dependence of L on t causes no issue because t is fixed throughout this argument. + +Equivalently, define B_n=336+(L-112)n-224f(1+8n) and C_n=B_n+224T_n. Then + +``` +T_(n+1)-T_n=0, n=0,1,2, +T_(n+1)-T_n=1-delta(8 floor((n+1)/2)), n>=3. +``` + +These increments are nondecreasing, including the positive jump at n=3. B_n is already strictly discretely convex, and T_n is discretely convex. This gives the same proof without treating the balanced side contribution as strictly convex on each step: its increments deliberately repeat. + +## The exact three-value gate + +For any integer m>=1, suppose at one fixed t that + +``` +C_m>0, D_(m-1)<=0, D_m>=0. +``` + +For nm, every D_j with m<=j<=n-1 is at least D_m>=0, so + +``` +C_n-C_m=sum_(j=m)^(n-1)D_j>=0. +``` + +Hence C_n>=C_m>0 for every n>=0, and every original invoice has E>=C_n>0. This is an exact unbounded conclusion from finite neighboring comparisons; no tail estimate, large-n limit or assumption of eventual growth is used. If both neighboring inequalities are strict, m is the unique minimizing FULL count. Non-strict signs still suffice for positivity, with a possible adjacent tie. Strict discrete convexity prevents a longer interval of tied minima. For m=0, the one-sided condition D_0>=0 is sufficient. + +At m=18, the numerical worker can use the directly simplified expressions + +``` +C_18=18L+1680-224f(145) + -224[2 sum_(k=2)^8 delta(8k)+delta(72)], +D_17=L+112-224[f(145)-f(137)+delta(72)], +D_18=L+112-224[f(153)-f(145)+delta(72)]. +``` + +Thus the needed outward certificates are a positive lower bound for C_18, a nonpositive upper bound for D_17, and a nonnegative lower bound for D_18. Direct evaluation of these differences can avoid extra interval widening from subtracting separately enclosed C values. This is an evaluation plan, not an asserted sign or numerical result. + +## Verification, provenance and limits + +The [exact bounded controls](../tests/5405-DISCRETE-CONVEXITY-CONTROLS.json) use t=1/2 and only small n. They check the first-difference formula against the original canonical expression, all junction values, the convex correction decomposition, strict second differences, independence from an arbitrary affine L term, and a synthetic local-minimum example. Square-factor normalization detects exact identities; outward integer square-root bounds certify signs. The script has a ten-second alarm and imports no author/source code. Its finite examples check indexing and implementation; the all-n, all-t proof is the analytic argument above. + +The source profile remains P={1:2193,2:412,3:510,4:127,5:40}, H={4:28,7:7,8:47,9:318}, with 112 ports, fresh rank-eight FULL stages, rank-one QUERY price, and the same prefix/suffix idle law. The theorem's affine-L independence does not alter the validity obligations of the source equation or grant a changed helper/coded-output contract. Coupled #5402 outputs remain outside this family. + +The three-value implication is at a **fixed t=1-kappa**. Extending a certified sign to a whole interval of kappa requires a separate monotonicity argument; discrete convexity in n alone does not provide it. No actual kappa inequality, interval-tail certificate, DP replay, source/native execution, physical optimum, recursive admission or improved exponent is established by this note. + +Credit Ali Romman for the primary invoice family, original unbounded ceiling and exact dynamic program; Cinna Davis for the paired controller; the retained source/helper/compiler/interval contributors; and root for proposing the discrete-convexity conjecture. This independent check and its exact controls were prepared with substantial OpenAI Codex assistance. Local only; no external publication. The preceding 66-entry checkpoint and its frozen exchange note remain unchanged. diff --git a/research/kappa-architecture-frontier/inputs/exchange-proof.md b/research/kappa-architecture-frontier/inputs/exchange-proof.md new file mode 100644 index 0000000000..e0f0ce8a01 --- /dev/null +++ b/research/kappa-architecture-frontier/inputs/exchange-proof.md @@ -0,0 +1,160 @@ +# #5405: concavity reduces every fixed-FULL-count invoice to one balanced mask + +The proposed exchange reduction is valid for the exact invoice family in #5405 equation (1), with `0=3, all three unpaired endpoint/central stages are FULL, every side pair is `10`, and the pair counts are as balanced as possible. For n=0,1,2, p=1 suffices. The proof is elementary concavity and does not need a new published theorem or a replay of the author's dynamic program. + +This is an independent mathematical verification of the reduction, not a new kappa certificate. No values of the actual profile moment L, the proposed ceiling exponent, or the author's tail interval bounds were recomputed. The frozen autonomous provider profile, port count and idle law are essential. The coupled #5402 contract is outside this result. + +## Exact source and reduced objective + +The primary source is the sole monitor's [#5405 proof](../../upstream-monitor-resume-20261024/5405-PROOF.md), source head `314b56a6c0056c2358538f072c6fde9d365be44d`. The full equation (1), recurrence, tail and scope sections were read. Its local profiles are + +``` +P={1:2193,2:412,3:510,4:127,5:40}, +H={4:28,7:7,8:47,9:318}. +``` + +Fix t in (0,1), `f(r)=r^t` for r>0, `f(0)=0`, and `L=sum P[r]f(r)-sum H[r]f(r)`. For any p>=1, split a+b=p-1 and FULL/QUERY stage mask x, the source defines + +``` +E = 112(2p+1)+(L-112)n-224 f(1+8n) + +224 sum_j g(h_j,e_j), +g(h,e)=f(8h)+e f(8)-f(1+8(h+e)). +``` + +At fixed n, all terms except + +``` +J := p + sum_j g(h_j,e_j) +``` + +are constant: `E=224J+112+(L-112)n-224f(1+8n)`. Thus every change below compares J exactly and preserves the local FULL/helper census n. It also accounts explicitly for every added/deleted QUERY and retained idle summand. It does not preserve a given physical caller or its productive input set; the resulting mask is another member of the source's optimistic invoice family. + +Read each side from its outside end toward the central stage. The left side is `x0,(x1,x2),...,(x_(2a-1),x_(2a))`; the right side is `x_(2p),(x_(2p-1),x_(2p-2)),...,(x_(2a+3),x_(2a+2))`. The central indicator is `c=x_(2a+1)`. For a pair `(o,e)` preceded by k FULL stages on that side, its summand is `g(k+o,e)`. A change preserving the total o+e leaves every later partial count unchanged. + +Write `delta(z)=f(z+1)-f(z)`. Strict concavity gives `00, `delta(0)=1`, and delta strictly decreases with z. For each fixed positive length d, `f(z+d)-f(z)` also strictly decreases with z. + +## 1. Reduce side pairs to 10 + +**Delete 00.** This reduces p by one and removes `g(k,0)=-delta(8k)`. Therefore + +``` +Delta J = -1+delta(8k) <= 0. +``` + +Equality occurs exactly when k=0. The side may become empty; p remains at least one because a side pair existed before deletion. + +**Replace 01 by 10.** This leaves p and n fixed, and leaves all later partial counts fixed. The exact change is + +``` +Delta J = f(8k+8)-f(8k)-f(8) <= 0. +``` + +This is subadditivity of the concave power. Equality holds exactly at k=0; it is strict for k>0. + +**Split 11 into 10,10 on the same side.** This adds one pair, so p increases by one, while n and all later partial counts are unchanged. It adds two QUERY stages and their paid cost, which is the `+1` below in units of 224: + +``` +Delta J = 1+g(k+1,0)+g(k+2,0)-g(k+1,1) + = 1+f(8k+16)-f(8k+9)-f(8). +``` + +For k>=0, decreasing seven-step increments imply + +``` +f(8k+16)-f(8k+9) <= f(16)-f(9) < f(8)-f(1). +``` + +The last strict inequality compares the integrals of `t z^(t-1)` over [9,16] and [1,8]. Since f(1)=1, the split strictly decreases J for every k>=0. Equivalently, the equal-sum pair (16,1) is more spread than (9,8), but no separate majorization theorem is required. + +Apply these replacements independently to the finitely many original side pairs. No replacement introduces a pair type other than 10, so the process terminates. Afterwards every side consists only of 10 pairs. The three unpaired indicators are still arbitrary bits. + +## 2. Move FULL stages to the unpaired positions + +Let q_L,q_R count the remaining 10 pairs, and let l,r,c be the left-end, right-end and central indicators. Then + +``` +n = l+r+c+q_L+q_R, p=q_L+q_R+1. +``` + +**A nonempty side with QUERY end.** Replace its first 10 pair and QUERY end by a FULL end, deleting the pair. The removed pair had h=1. Later partial counts are identical: both old and new prefixes contain one FULL before the next pair. Thus + +``` +Delta J = -1+delta(8) < 0. +``` + +Perform this on each side that qualifies. Every remaining QUERY end is now on an empty side. + +**Fill a QUERY central stage or an empty QUERY side end.** Remove the last 10 pair from any nonempty donor side and turn that unpaired QUERY indicator into FULL. Removing the last pair affects no later donor partial count. The central indicator belongs to no side partial count; an empty recipient side has no summands. If the donor pair ends with k FULL stages on its side, k>=1, and + +``` +Delta J = -1+delta(8k) < 0. +``` + +The donor side loses one pair, p decreases by one, and the moved FULL keeps n fixed. A donor always exists while an unpaired position needs filling and the target number of FULL unpaired positions has not been reached: `q_L+q_R=n-(l+r+c)>0`. + +For n>=3, repeat until l=r=c=1. The final number of pairs is n-3 and `p=n-2`. For n<=2, repeat only until all n FULL stages occupy unpaired positions; then q_L=q_R=0 and p=1. The same reasoning gives p=1 for n=3 with all three indicators FULL. The construction works also when one side initially has no pairs or both sides are empty. + +This proves the small-count reduction without assuming n>=3 during a transfer. For n=0, deleting 00 pairs has equality throughout, and every all-QUERY invoice already has E=112. + +## 3. Balance the two sides + +For n>=3 both side ends are FULL. The j-th 10 pair on either side therefore has `h=j+1`, including h=2 for the first pair. Define + +``` +F(q) = -sum_(k=2)^(q+1) delta(8k), F(0)=0. +``` + +The side contribution is F(q), and + +``` +F(q+1)-F(q)=-delta(8(q+2)). +``` + +These increments strictly increase with q, so F is strictly discretely convex. If a>=b+2, moving the last pair of the longer side to the end of the shorter side changes the score by + +``` +F(a-1)+F(b+1)-F(a)-F(b) + = delta(8(a+1))-delta(8(b+2)) < 0. +``` + +Thus at fixed a+b=n-3, the minimum has + +``` +a=floor((n-3)/2), b=ceil((n-3)/2), +``` + +up to reflection. Balanced reflected masks have the same invoice. This balancing changes the permitted split and the mask; it does not claim a free physical retiming of one caller. + +## 4. Exact canonical minimum for each n + +Every original invoice has been transformed to an admissible canonical invoice with no larger E. Conversely the canonical invoice is itself in the stated family. Consequently its value is the **global minimum over all p, splits and stage masks with that FULL count n**. + +For n=0,1,2, + +``` +C_n(t) = 336+(L(t)-112)n-224(1+8n)^t. +``` + +For n>=3, put a=floor((n-3)/2), b=ceil((n-3)/2). Then + +``` +C_n(t) = n L(t)+112(n-3)-224(1+8n)^t + -224[sum_(k=2)^(a+1) delta(8k) + +sum_(k=2)^(b+1) delta(8k)]. +``` + +The formulas agree at n=3 if the first expression is extended there. For n=18 they select p=16,a=7,b=8, with side FULL counts eight and nine and a FULL central stage, matching the location reported by the author's dynamic program. This is an index/formula comparison, not a replay of its numerical minimum. + +The result holds separately for every 0=96 tail certificate at its specified exponent is accepted, the finite part can be independently checked using only **96 canonical invoices, n=0,...,95**, instead of 10,290,000 dynamic-program combinations. This note does not rerun that tail certificate, those 96 numerical inequalities, the author's interval engine, or the extension to all larger kappa. It establishes the analytic reduction that would permit the smaller independent verification. + +The [bounded exact controls](../tests/5405-EXCHANGE-TOY-CONTROLS.json) use t=1/2, p<=4 and n<=6 so both compared invoices stay within p<=4. They compare square-root expressions using symbolic square-factor normalization and outward rational bounds on a 2^80 grid, under a ten-second alarm. They check the side-index translation against equation (1), the zero/strict cases of each exchange, balancing, and attainment of the canonical minimum in the bounded domain. No actual profile moment L is evaluated because it cancels at fixed n. + +The previous #5397 primary PR body describes classical concave-order invoice preflight and explicitly separates that arithmetic from physical legality and funding. The existing literature ledger was checked first; no earlier paper dependency is needed for the elementary derivative proof above. This is not an application of Douglas's unrelated operator-majorization theorem. No new paper was added. + +The local P/H profiles are autonomous jobs, each FULL has 112 ports and a fresh rank-eight stage block, and the prefix/suffix idle law is fixed. Coded or coupled helper outputs, altered target lists, changed stage ranks, different idle incidence, or another controller graph require a new comparison. In particular this does not apply to #5402. No physical optimum, native query lower bound, compiler admission or improved exponent follows. + +Credit Ali Romman for #5405's source family, equation, original unbounded ceiling and exact dynamic program; Cinna Davis for the paired controller; the retained native/helper/compiler/interval contributors; and root for proposing the exchange conjecture checked here. This note independently checks the moves, indices, strictness and small counts, with substantial OpenAI Codex assistance. Local only; no external publication. diff --git a/research/kappa-architecture-frontier/inputs/neutral-invoice.json b/research/kappa-architecture-frontier/inputs/neutral-invoice.json new file mode 100644 index 0000000000..d66216ad80 --- /dev/null +++ b/research/kappa-architecture-frontier/inputs/neutral-invoice.json @@ -0,0 +1,2460 @@ +{ + "accepted_local_route_receipt_comparison": "PENDING_SEPARATE_SOURCE_BOUND_BINDING", + "caller_events": { + "ADD": 90, + "IDLE": 15, + "LOCAL": 18, + "QUERY_SHEAR": 15, + "Q_POWER": 4, + "SIGNED_SWAP": 20 + }, + "chronology": [ + { + "event": [ + "SIGNED_SWAP", + 1, + 0 + ], + "index": 0, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "Q_POWER", + 0, + 2 + ], + "index": 1, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "LOCAL", + 0, + 0, + true + ], + "index": 2, + "ordinary_record_funded": false, + "paid": { + "1": 2193, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "productive": { + "4": 28, + "7": 7, + "8": 55, + "9": 318 + } + }, + { + "event": [ + "SIGNED_SWAP", + 0, + 1 + ], + "index": 3, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "Q_POWER", + 1, + -2 + ], + "index": 4, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "LOCAL", + 1, + 0, + true + ], + "index": 5, + "ordinary_record_funded": false, + "paid": { + "1": 2193, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "productive": { + "4": 28, + "7": 7, + "8": 55, + "9": 318 + } + }, + { + "event": [ + "IDLE", + 1, + [ + 0, + 1 + ] + ], + "index": 6, + "ordinary_record_funded": false, + "paid": { + "16": 224 + }, + "productive": {} + }, + { + "event": [ + "ADD", + 0, + 2, + 1 + ], + "index": 7, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 3, + 1, + -1 + ], + "index": 8, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "QUERY_SHEAR", + 2, + 0, + false + ], + "index": 9, + "ordinary_record_funded": false, + "paid": { + "1": 112 + }, + "productive": {} + }, + { + "event": [ + "ADD", + 0, + 2, + -1 + ], + "index": 10, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 3, + 1, + 1 + ], + "index": 11, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "LOCAL", + 3, + 1, + true + ], + "index": 12, + "ordinary_record_funded": false, + "paid": { + "1": 2193, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "productive": { + "4": 28, + "7": 7, + "8": 55, + "9": 318 + } + }, + { + "event": [ + "IDLE", + 2, + [ + 0, + 1, + 3 + ] + ], + "index": 13, + "ordinary_record_funded": false, + "paid": { + "24": 224 + }, + "productive": {} + }, + { + "event": [ + "ADD", + 2, + 4, + 1 + ], + "index": 14, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 5, + 3, + -1 + ], + "index": 15, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "QUERY_SHEAR", + 4, + 1, + false + ], + "index": 16, + "ordinary_record_funded": false, + "paid": { + "1": 112 + }, + "productive": {} + }, + { + "event": [ + "ADD", + 2, + 4, + -1 + ], + "index": 17, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 5, + 3, + 1 + ], + "index": 18, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "LOCAL", + 5, + 2, + true + ], + "index": 19, + "ordinary_record_funded": false, + "paid": { + "1": 2193, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "productive": { + "4": 28, + "7": 7, + "8": 55, + "9": 318 + } + }, + { + "event": [ + "IDLE", + 3, + [ + 0, + 1, + 3, + 5 + ] + ], + "index": 20, + "ordinary_record_funded": false, + "paid": { + "32": 224 + }, + "productive": {} + }, + { + "event": [ + "ADD", + 4, + 6, + 1 + ], + "index": 21, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 7, + 5, + -1 + ], + "index": 22, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "QUERY_SHEAR", + 6, + 2, + false + ], + "index": 23, + "ordinary_record_funded": false, + "paid": { + "1": 112 + }, + "productive": {} + }, + { + "event": [ + "ADD", + 4, + 6, + -1 + ], + "index": 24, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 7, + 5, + 1 + ], + "index": 25, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "LOCAL", + 7, + 3, + true + ], + "index": 26, + "ordinary_record_funded": false, + "paid": { + "1": 2193, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "productive": { + "4": 28, + "7": 7, + "8": 55, + "9": 318 + } + }, + { + "event": [ + "IDLE", + 4, + [ + 0, + 1, + 3, + 5, + 7 + ] + ], + "index": 27, + "ordinary_record_funded": false, + "paid": { + "40": 224 + }, + "productive": {} + }, + { + "event": [ + "ADD", + 6, + 8, + 1 + ], + "index": 28, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 9, + 7, + -1 + ], + "index": 29, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "QUERY_SHEAR", + 8, + 3, + false + ], + "index": 30, + "ordinary_record_funded": false, + "paid": { + "1": 112 + }, + "productive": {} + }, + { + "event": [ + "ADD", + 6, + 8, + -1 + ], + "index": 31, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 9, + 7, + 1 + ], + "index": 32, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "LOCAL", + 9, + 4, + true + ], + "index": 33, + "ordinary_record_funded": false, + "paid": { + "1": 2193, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "productive": { + "4": 28, + "7": 7, + "8": 55, + "9": 318 + } + }, + { + "event": [ + "IDLE", + 5, + [ + 0, + 1, + 3, + 5, + 7, + 9 + ] + ], + "index": 34, + "ordinary_record_funded": false, + "paid": { + "48": 224 + }, + "productive": {} + }, + { + "event": [ + "ADD", + 8, + 10, + 1 + ], + "index": 35, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 11, + 9, + -1 + ], + "index": 36, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "QUERY_SHEAR", + 10, + 4, + false + ], + "index": 37, + "ordinary_record_funded": false, + "paid": { + "1": 112 + }, + "productive": {} + }, + { + "event": [ + "ADD", + 8, + 10, + -1 + ], + "index": 38, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 11, + 9, + 1 + ], + "index": 39, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "LOCAL", + 11, + 5, + true + ], + "index": 40, + "ordinary_record_funded": false, + "paid": { + "1": 2193, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "productive": { + "4": 28, + "7": 7, + "8": 55, + "9": 318 + } + }, + { + "event": [ + "IDLE", + 6, + [ + 0, + 1, + 3, + 5, + 7, + 9, + 11 + ] + ], + "index": 41, + "ordinary_record_funded": false, + "paid": { + "56": 224 + }, + "productive": {} + }, + { + "event": [ + "ADD", + 10, + 12, + 1 + ], + "index": 42, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 13, + 11, + -1 + ], + "index": 43, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "QUERY_SHEAR", + 12, + 5, + false + ], + "index": 44, + "ordinary_record_funded": false, + "paid": { + "1": 112 + }, + "productive": {} + }, + { + "event": [ + "ADD", + 10, + 12, + -1 + ], + "index": 45, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 13, + 11, + 1 + ], + "index": 46, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "LOCAL", + 13, + 6, + true + ], + "index": 47, + "ordinary_record_funded": false, + "paid": { + "1": 2193, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "productive": { + "4": 28, + "7": 7, + "8": 55, + "9": 318 + } + }, + { + "event": [ + "IDLE", + 7, + [ + 0, + 1, + 3, + 5, + 7, + 9, + 11, + 13 + ] + ], + "index": 48, + "ordinary_record_funded": false, + "paid": { + "64": 224 + }, + "productive": {} + }, + { + "event": [ + "ADD", + 12, + 14, + 1 + ], + "index": 49, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 15, + 13, + -1 + ], + "index": 50, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "QUERY_SHEAR", + 14, + 6, + false + ], + "index": 51, + "ordinary_record_funded": false, + "paid": { + "1": 112 + }, + "productive": {} + }, + { + "event": [ + "ADD", + 12, + 14, + -1 + ], + "index": 52, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 15, + 13, + 1 + ], + "index": 53, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "LOCAL", + 15, + 7, + true + ], + "index": 54, + "ordinary_record_funded": false, + "paid": { + "1": 2193, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "productive": { + "4": 28, + "7": 7, + "8": 55, + "9": 318 + } + }, + { + "event": [ + "ADD", + 14, + 16, + 1 + ], + "index": 55, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 17, + 15, + -1 + ], + "index": 56, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "QUERY_SHEAR", + 16, + 7, + false + ], + "index": 57, + "ordinary_record_funded": false, + "paid": { + "1": 112 + }, + "productive": {} + }, + { + "event": [ + "ADD", + 14, + 16, + -1 + ], + "index": 58, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 17, + 15, + 1 + ], + "index": 59, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "LOCAL", + 17, + 8, + true + ], + "index": 60, + "ordinary_record_funded": false, + "paid": { + "1": 2193, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "productive": { + "4": 28, + "7": 7, + "8": 55, + "9": 318 + } + }, + { + "event": [ + "ADD", + 16, + 18, + 1 + ], + "index": 61, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 19, + 17, + -1 + ], + "index": 62, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "QUERY_SHEAR", + 18, + 8, + false + ], + "index": 63, + "ordinary_record_funded": false, + "paid": { + "1": 112 + }, + "productive": {} + }, + { + "event": [ + "ADD", + 16, + 18, + -1 + ], + "index": 64, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 19, + 17, + 1 + ], + "index": 65, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "LOCAL", + 19, + 9, + true + ], + "index": 66, + "ordinary_record_funded": false, + "paid": { + "1": 2193, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "productive": { + "4": 28, + "7": 7, + "8": 55, + "9": 318 + } + }, + { + "event": [ + "ADD", + 18, + 20, + 1 + ], + "index": 67, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 21, + 19, + -1 + ], + "index": 68, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "QUERY_SHEAR", + 20, + 9, + false + ], + "index": 69, + "ordinary_record_funded": false, + "paid": { + "1": 112 + }, + "productive": {} + }, + { + "event": [ + "ADD", + 18, + 20, + -1 + ], + "index": 70, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 21, + 19, + 1 + ], + "index": 71, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "LOCAL", + 21, + 10, + true + ], + "index": 72, + "ordinary_record_funded": false, + "paid": { + "1": 2193, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "productive": { + "4": 28, + "7": 7, + "8": 55, + "9": 318 + } + }, + { + "event": [ + "ADD", + 20, + 22, + 1 + ], + "index": 73, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 23, + 21, + -1 + ], + "index": 74, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "QUERY_SHEAR", + 22, + 10, + false + ], + "index": 75, + "ordinary_record_funded": false, + "paid": { + "1": 112 + }, + "productive": {} + }, + { + "event": [ + "ADD", + 20, + 22, + -1 + ], + "index": 76, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 23, + 21, + 1 + ], + "index": 77, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "LOCAL", + 23, + 11, + true + ], + "index": 78, + "ordinary_record_funded": false, + "paid": { + "1": 2193, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "productive": { + "4": 28, + "7": 7, + "8": 55, + "9": 318 + } + }, + { + "event": [ + "ADD", + 22, + 24, + 1 + ], + "index": 79, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 25, + 23, + -1 + ], + "index": 80, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "QUERY_SHEAR", + 24, + 11, + false + ], + "index": 81, + "ordinary_record_funded": false, + "paid": { + "1": 112 + }, + "productive": {} + }, + { + "event": [ + "ADD", + 22, + 24, + -1 + ], + "index": 82, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 25, + 23, + 1 + ], + "index": 83, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "LOCAL", + 25, + 12, + true + ], + "index": 84, + "ordinary_record_funded": false, + "paid": { + "1": 2193, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "productive": { + "4": 28, + "7": 7, + "8": 55, + "9": 318 + } + }, + { + "event": [ + "ADD", + 24, + 26, + 1 + ], + "index": 85, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 27, + 25, + -1 + ], + "index": 86, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "QUERY_SHEAR", + 26, + 12, + false + ], + "index": 87, + "ordinary_record_funded": false, + "paid": { + "1": 112 + }, + "productive": {} + }, + { + "event": [ + "ADD", + 24, + 26, + -1 + ], + "index": 88, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 27, + 25, + 1 + ], + "index": 89, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "LOCAL", + 27, + 13, + true + ], + "index": 90, + "ordinary_record_funded": false, + "paid": { + "1": 2193, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "productive": { + "4": 28, + "7": 7, + "8": 55, + "9": 318 + } + }, + { + "event": [ + "ADD", + 26, + 28, + 1 + ], + "index": 91, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 29, + 27, + -1 + ], + "index": 92, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "QUERY_SHEAR", + 28, + 13, + false + ], + "index": 93, + "ordinary_record_funded": false, + "paid": { + "1": 112 + }, + "productive": {} + }, + { + "event": [ + "ADD", + 26, + 28, + -1 + ], + "index": 94, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 29, + 27, + 1 + ], + "index": 95, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "LOCAL", + 29, + 14, + true + ], + "index": 96, + "ordinary_record_funded": false, + "paid": { + "1": 2193, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "productive": { + "4": 28, + "7": 7, + "8": 55, + "9": 318 + } + }, + { + "event": [ + "ADD", + 28, + 30, + 1 + ], + "index": 97, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 31, + 29, + -1 + ], + "index": 98, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "QUERY_SHEAR", + 30, + 14, + false + ], + "index": 99, + "ordinary_record_funded": false, + "paid": { + "1": 112 + }, + "productive": {} + }, + { + "event": [ + "ADD", + 28, + 30, + -1 + ], + "index": 100, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 31, + 29, + 1 + ], + "index": 101, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "LOCAL", + 31, + 15, + true + ], + "index": 102, + "ordinary_record_funded": false, + "paid": { + "1": 2193, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "productive": { + "4": 28, + "7": 7, + "8": 55, + "9": 318 + } + }, + { + "event": [ + "SIGNED_SWAP", + 31, + 30 + ], + "index": 103, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "Q_POWER", + 30, + 2 + ], + "index": 104, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "LOCAL", + 32, + 15, + true + ], + "index": 105, + "ordinary_record_funded": false, + "paid": { + "1": 2193, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "productive": { + "4": 28, + "7": 7, + "8": 55, + "9": 318 + } + }, + { + "event": [ + "SIGNED_SWAP", + 30, + 31 + ], + "index": 106, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "Q_POWER", + 31, + -2 + ], + "index": 107, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "IDLE", + 7, + [ + 17, + 19, + 21, + 23, + 25, + 27, + 29, + 31, + 32 + ] + ], + "index": 108, + "ordinary_record_funded": false, + "paid": { + "72": 224 + }, + "productive": {} + }, + { + "event": [ + "IDLE", + 8, + [ + 19, + 21, + 23, + 25, + 27, + 29, + 31, + 32 + ] + ], + "index": 109, + "ordinary_record_funded": false, + "paid": { + "64": 224 + }, + "productive": {} + }, + { + "event": [ + "IDLE", + 9, + [ + 21, + 23, + 25, + 27, + 29, + 31, + 32 + ] + ], + "index": 110, + "ordinary_record_funded": false, + "paid": { + "56": 224 + }, + "productive": {} + }, + { + "event": [ + "IDLE", + 10, + [ + 23, + 25, + 27, + 29, + 31, + 32 + ] + ], + "index": 111, + "ordinary_record_funded": false, + "paid": { + "48": 224 + }, + "productive": {} + }, + { + "event": [ + "IDLE", + 11, + [ + 25, + 27, + 29, + 31, + 32 + ] + ], + "index": 112, + "ordinary_record_funded": false, + "paid": { + "40": 224 + }, + "productive": {} + }, + { + "event": [ + "IDLE", + 12, + [ + 27, + 29, + 31, + 32 + ] + ], + "index": 113, + "ordinary_record_funded": false, + "paid": { + "32": 224 + }, + "productive": {} + }, + { + "event": [ + "IDLE", + 13, + [ + 29, + 31, + 32 + ] + ], + "index": 114, + "ordinary_record_funded": false, + "paid": { + "24": 224 + }, + "productive": {} + }, + { + "event": [ + "IDLE", + 14, + [ + 31, + 32 + ] + ], + "index": 115, + "ordinary_record_funded": false, + "paid": { + "16": 224 + }, + "productive": {} + }, + { + "event": [ + "ADD", + 30, + 28, + 1 + ], + "index": 116, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 29, + 31, + -1 + ], + "index": 117, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 28, + 26, + 1 + ], + "index": 118, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 27, + 29, + -1 + ], + "index": 119, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 26, + 24, + 1 + ], + "index": 120, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 25, + 27, + -1 + ], + "index": 121, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 24, + 22, + 1 + ], + "index": 122, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 23, + 25, + -1 + ], + "index": 123, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 22, + 20, + 1 + ], + "index": 124, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 21, + 23, + -1 + ], + "index": 125, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 20, + 18, + 1 + ], + "index": 126, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 19, + 21, + -1 + ], + "index": 127, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 18, + 16, + 1 + ], + "index": 128, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 17, + 19, + -1 + ], + "index": 129, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 16, + 14, + 1 + ], + "index": 130, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 15, + 17, + -1 + ], + "index": 131, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 14, + 12, + 1 + ], + "index": 132, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 13, + 15, + -1 + ], + "index": 133, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 12, + 10, + 1 + ], + "index": 134, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 11, + 13, + -1 + ], + "index": 135, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 10, + 8, + 1 + ], + "index": 136, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 9, + 11, + -1 + ], + "index": 137, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 8, + 6, + 1 + ], + "index": 138, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 7, + 9, + -1 + ], + "index": 139, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 6, + 4, + 1 + ], + "index": 140, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 5, + 7, + -1 + ], + "index": 141, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 4, + 2, + 1 + ], + "index": 142, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 3, + 5, + -1 + ], + "index": 143, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 2, + 0, + 1 + ], + "index": 144, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "ADD", + 1, + 3, + -1 + ], + "index": 145, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "SIGNED_SWAP", + 0, + 1 + ], + "index": 146, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "SIGNED_SWAP", + 2, + 3 + ], + "index": 147, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "SIGNED_SWAP", + 4, + 5 + ], + "index": 148, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "SIGNED_SWAP", + 6, + 7 + ], + "index": 149, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "SIGNED_SWAP", + 8, + 9 + ], + "index": 150, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "SIGNED_SWAP", + 10, + 11 + ], + "index": 151, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "SIGNED_SWAP", + 12, + 13 + ], + "index": 152, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "SIGNED_SWAP", + 14, + 15 + ], + "index": 153, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "SIGNED_SWAP", + 16, + 17 + ], + "index": 154, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "SIGNED_SWAP", + 18, + 19 + ], + "index": 155, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "SIGNED_SWAP", + 20, + 21 + ], + "index": 156, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "SIGNED_SWAP", + 22, + 23 + ], + "index": 157, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "SIGNED_SWAP", + 24, + 25 + ], + "index": 158, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "SIGNED_SWAP", + 26, + 27 + ], + "index": 159, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "SIGNED_SWAP", + 28, + 29 + ], + "index": 160, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + }, + { + "event": [ + "SIGNED_SWAP", + 30, + 31 + ], + "index": 161, + "ordinary_record_funded": false, + "paid": {}, + "productive": {} + } + ], + "economic_profile_gain": 0, + "explicit_new_helper_axis_alias_maps": 16, + "explicit_paid_child_axis_route_maps": 16, + "forward_packet_bound": true, + "forward_used_in_old_controller": false, + "fresh_complete_precision": null, + "full_ordinary_budget": null, + "global_scientific_admission": false, + "helper_normalizer_maps": 800, + "helper_normalizer_records": 400, + "histograms": { + "paid": { + "1": 41154, + "16": 448, + "2": 7416, + "24": 448, + "3": 9180, + "32": 448, + "4": 2286, + "40": 448, + "48": 448, + "5": 720, + "56": 448, + "64": 448, + "72": 224, + "8": 144 + }, + "productive": { + "145": 224, + "17": 448, + "25": 448, + "33": 448, + "4": 504, + "41": 448, + "49": 448, + "57": 448, + "65": 448, + "7": 126, + "73": 224, + "8": 990, + "9": 5724 + } + }, + "known_complete_local_monomial_maps": 1536, + "known_complete_local_scalar_tariff": 179806, + "known_local_extension_scalar_tariff": 4784, + "known_provider_scalar_tariff": 175022, + "local_ADD_coefficients": { + "-1/2": 176, + "1": 8, + "1/2": 272 + }, + "local_extra_paid": { + "8": 8 + }, + "local_extra_productive": { + "8": 8 + }, + "local_operation_census": { + "ADD": 456, + "CLEAR": 16, + "GAUSSIAN": 8, + "MONOMIAL": 1072, + "PROVIDER_5402": 1, + "SWAP": 8, + "ZERO_RETAG": 8 + }, + "local_owned_arbitrary_inputs": 17, + "local_paid": { + "1": 2193, + "2": 412, + "3": 510, + "4": 127, + "5": 40, + "8": 8 + }, + "local_persistent_arbitrary_inputs": 632, + "local_productive_helpers": { + "4": 28, + "7": 7, + "8": 55, + "9": 318 + }, + "main": { + "145": 224, + "17": 448, + "25": 448, + "33": 448, + "41": 448, + "49": 448, + "57": 448, + "65": 448, + "73": 224 + }, + "native_physical_tariff": null, + "new_helper_canonical_axes": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ], + "paid_child_realized_active_axes": [ + 1, + 2, + 3, + 4, + 5, + 6, + 7, + 8 + ], + "paid_child_standard_axes": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ], + "paid_count": 64260, + "paid_rank_mass": 238990, + "productive_count": 10928, + "productive_rank_mass": 239742, + "raw_ceiling_changed": false, + "raw_moment_delta_all_exponents": 0, + "route_proof": "Plain involutive axis0/8 permutation fixes phases, sendsC8 toD8 andD8 toC8, extends by identity on all other/fibre axes", + "schema": "actual-routed-neutral-standard-p16-invoice/1", + "scope": "Every LOCAL/query/wholeidle/main counted. Native and local all-input phase/ownership, full ordinary machine work and fresh precision are external root gates. This neutral construction supplies no economic saving or new raw root.", + "signed_profile_identical_to_5398": true, + "source_bindings": [ + { + "path": "swarm-coupled-caller-sol-high-20261024/agents/caller/NEUTRAL-BACKWARD-v16c.json", + "sha256": "cc297ee54c2743615dfe857838d5f40424ccd33fdb08ecfafbc41b1710416d91" + }, + { + "path": "swarm-coupled-caller-sol-high-20261024/agents/caller/NEUTRAL-FORWARD-v16c.json", + "sha256": "dfa125a8c26b86cfa2024edab9f8ed3c95ebe23bffc1bedfd3c90aa471e80ae0" + }, + { + "path": "swarm-coupled-caller-sol-high-20261024/agents/challenge/CURRENT-HELPER-ALIASES-v2.json", + "sha256": "5184c975c9a5a6364334fe665d27235c6aab96c14f7cd269ff68c1e0f4f16a6d" + }, + { + "path": "swarm-next-gain-sol-high-20261024/repository/research/kappa-backward-controller-20261023/CONTROLLER.json", + "sha256": "60cc512b39cdb9ea2c2ac6c6634c8d3f9627d96ace08ffa659a9d9472444122b" + }, + { + "path": "swarm-next-gain-sol-high-20261024/agents/numeric/INVOICE-v2.json", + "sha256": "a53bdbc009830f83b91233cf7cc2c8e9a03d76cff93c73bdd4f52fceb742e73f" + }, + { + "path": "swarm-provider-audit-sol-high-20261024/agents/budget/inputs/ALL-PINS.json", + "sha256": "a37fa9735bbb2697811de72a706b243842d1303243f6e6a0300bd5046d4f3d66" + } + ], + "status": "INDEPENDENT_LITERAL_INVOICE_WITH_EXTERNAL_PHYSICAL_GATES", + "whole_idles": { + "16": 448, + "24": 448, + "32": 448, + "40": 448, + "48": 448, + "56": 448, + "64": 448, + "72": 224 + } +} diff --git a/research/kappa-architecture-frontier/inputs/p104-5544.json b/research/kappa-architecture-frontier/inputs/p104-5544.json new file mode 100644 index 0000000000..5637130d4a --- /dev/null +++ b/research/kappa-architecture-frontier/inputs/p104-5544.json @@ -0,0 +1,315 @@ +{ + "complete_cost": { + "compiler": { + "H": 64215200000000, + "N": "2^64215200000000", + "eta": { + "lower": "0.000000185845792706621973271570", + "upper": "0.000000185845792706621973271571" + }, + "gap": "1/1400000000", + "integer_test_exponent": 45868, + "logarithm_power": 1000, + "theta": "63/64", + "uniform_saving": "1064201/350000000", + "word_materialized": false + }, + "full_forward_calls": 18, + "gain": "2656353/200000000000", + "kappa": "304057/100000000", + "kappa_decimal": ".00304057", + "margin_at_previous": { + "lower": "3.300756773058285958096643251393", + "upper": "3.300756773058285958096643251394" + }, + "negative_controls": { + "old_BIT": "Rejected by outer inequalities", + "old_cutoff": "Rejected by completion-tail ratio greater than one" + }, + "nonrecursive": { + "fixed_scalar_growth_bound": "At most 2^(16*26000) before native factors; a declared constant, not an attained norm.", + "local_routes": 5335000, + "local_scalar": 217428, + "peak_owned_fields": 1, + "raw_budget": 1000000000, + "raw_scalar_upper": 184647552, + "tensor_native_growth_bound": "Each rank-r Gaussian has row l1 norm at most 2^(rf); sum of local ranks is 5894." + }, + "ordinary_BIT": { + "admitted": "17/5000", + "after_cover": "69/20000", + "atom": "1/250", + "before_cover": "3459/1000000", + "ordinary_saving": "8590884599/2500000000000", + "prime_rule": "odd q > 2^26*N^5 avoiding all fixed denominators and rank witnesses" + }, + "outer": { + "functional_checks": { + "actual_new_BIT_stock_sublinear": "348599999253/350000000000", + "fixed_halo_explicit_metadata_branch": "26950000001/350000000", + "new_BIT_row_stock_sublinear_in_active_group": "1395799997009/1400000000000", + "new_semantic_group_guard": "3/1400000000" + }, + "margins": { + "boundary_algebraic_matrix": "5959522795743199/1960000000000000000", + "fused_gaussian": "5959522787229597/1960000000000000000", + "global_coordinate_router": "2128401/700000000", + "group_bit_router": "2979762093614797/980000000000000000", + "group_scans": "699999999/700000000", + "main_transform": "5959521395743199/1960000000000000000", + "microbox_face_corrections": "26950000001/350000000", + "polynomial_products": "1399999999/1400000000", + "sparse_union_movement": "802209522795743199/1960000000000000000" + }, + "parameters": { + "a": "2128401/700000000", + "b": "4256803/1400000000", + "beta": "1399999997/1400000000", + "bit_saving": "17/5000", + "cap_xi": "1782209521395743199/1960000000000000000", + "complex_uniform_saving": "1064201/350000000", + "d": "1/1400000000", + "epsilon": "1399999999/1400000000", + "kappa": "304057/100000000", + "lambda_": "398783771/400000000", + "lambda_prime": "1395743199/1400000000", + "layout": "1/1400000000", + "q": "4256801/1400000000", + "r0": "1/14000000000", + "stop": "1/1400000000", + "tested_saving": "121623/40000000" + }, + "strict_checks": { + "actual_bit_above_effective": "251599/700000000", + "actual_logarithmic_gamma_guard": "1/1400000000", + "actual_logarithmic_group_guard": "177790480704256801/980000000000000000", + "alpha_logarithm_absorption": "1/14000000000", + "boundary_algebraic_matrix_above_kappa": "5595743199/1960000000000000000", + "cap_above_band": "802209521395743199/1960000000000000000", + "cap_below_cell": "177790477204256801/1960000000000000000", + "cap_below_phase_cell_power": "2137790478604256801/1960000000000000000", + "complex_above_effective": "1/1400000000", + "complex_below_one_over_32": "39493197/1400000000", + "complex_endpoint": "1/700000000", + "epsilon_below_one": "1/1400000000", + "epsilon_positive": "1399999999/1400000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "5587229597/1960000000000000000", + "gaussian_above_main": "695743199/980000000000000000", + "global_coordinate_router_above_kappa": "1/350000000", + "global_gamma_power_slack": "9/14000000000", + "group_below_dimension": "1/700000000", + "group_bit_router_above_kappa": "3493614797/980000000000000000", + "group_gauge_power_slack": "177790480634256801/980000000000000000", + "group_key_fits_record": "1/700000000", + "group_positive": "1399999997/1400000000", + "group_scans_above_kappa": "1744679/1750000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "654799790400418148631/500000000000000000000000", + "lambda_above_internal": "1/2800000000", + "lambda_above_sigma": "3/2800000000", + "lambda_above_tau": "1/2800000000", + "lambda_prime_above_lambda": "1/2800000000", + "lambda_prime_above_leaf": "2795743197/1960000000000000000", + "leaf_saving_above_effective": "1395743197/1960000000000000000", + "main_transform_above_kappa": "4195743199/1960000000000000000", + "membership_arithmetic_fits_record": "1/1400000000", + "microbox_face_corrections_above_kappa": "53897871603/700000000", + "microbox_halo_volume": "110600000003/1400000000", + "new_complex_uniform_saving_above_b": "1/1400000000", + "new_semantic_guard_with_C1_one": "1/1400000000", + "polynomial_products_above_kappa": "1395743201/1400000000", + "positive_layout_slack": "1/1400000000", + "q_below_effective": "1/1400000000", + "q_below_internal": "1/1400000000", + "q_below_leaf": "2795743197/1960000000000000000", + "q_positive": "4256801/1400000000", + "short_record_fallback": "1395743197/1400000000", + "source_axis_superpolynomial": "1/1400000000", + "sparse_union_movement_above_kappa": "796250005595743199/1960000000000000000", + "stop_below_one": "1399999999/1400000000", + "stop_positive": "1/1400000000", + "strassen_integer_power_gap": "1951441519231", + "support_router_span": "3/1400000000", + "theta_positive_polynomial_power": "2", + "union_header_fits_record": "3/1400000000", + "union_tag_work_per_visit_fits_record": "3/1400000000" + } + }, + "paid": { + "1": 45282, + "16": 416, + "2": 10026, + "24": 416, + "3": 7002, + "32": 416, + "4": 2016, + "40": 416, + "48": 416, + "5": 1944, + "56": 416, + "6": 288, + "64": 416, + "7": 234, + "72": 208, + "9": 18 + }, + "paid_calls": 69930, + "previous_selected": "605457647/200000000000", + "productive_fields": 12814, + "query_shears": 15, + "rank_mass_surplus": 760, + "raw_headroom": [ + "80763/10000000000000", + "807631/100000000000000" + ], + "raw_root_interval": [ + "30405780763/10000000000000", + "304057807631/100000000000000" + ], + "relative_gain_percent": "265635300/605457647", + "strictification": { + "alpha": { + "lower": "0.999999996781290806577194629544", + "upper": "0.999999996781290806577194629545" + }, + "cutoff": 17, + "delta": { + "lower": "0.963354732998265185478252854607", + "upper": "0.963354732998265185478252854608" + }, + "floor": 18, + "gamma": { + "lower": "0.965182172149361102612340648898", + "upper": "0.965182172149361102612340648899" + }, + "normalized_paid_upper": "5242880004882813/5242880536870912", + "power": 1024, + "reserve": "1/10000000000", + "tail_offset": "1/5", + "tested": "121623/40000000" + }, + "targets": { + "145": 208, + "17": 416, + "25": 416, + "33": 416, + "4": 918, + "41": 416, + "49": 416, + "5": 648, + "57": 416, + "65": 416, + "7": 432, + "73": 208, + "8": 2196, + "9": 5292 + }, + "whole_idle_jobs": 3120 + }, + "limits": [ + "Conditional on the retained native all-column, owned-erasure, compiler, precision/tape and analytic-recovery framework.", + "The winning uniform compiler word and complete integer multiplier are not materialized.", + "No proof-kernel check or independent human review is claimed." + ], + "local": { + "endpoint_coefficients": 552049, + "helpers": { + "4": 51, + "5": 36, + "7": 24, + "8": 122, + "9": 294 + }, + "owned_lifetimes": 8, + "paid": { + "1": 2429, + "2": 557, + "3": 389, + "4": 112, + "5": 108, + "6": 16, + "7": 13, + "9": 1 + }, + "peak_owned_fields": 1, + "public_inputs": 735, + "real_scalar_allowance": 217428 + }, + "native": { + "distinct_maps": 2981, + "helper_normalizers": 1054, + "helpers": { + "4": 51, + "5": 36, + "7": 24, + "8": 122, + "9": 294 + }, + "main_adapters": 208, + "proof": "Every signed Pauli image and exact global phase; frame induction at every positive tensor width", + "recipe_payload_sha256": "0a12b2a43238496b226b47dd0e790882d03d1b1b66107308ab37dd6ce21a0481", + "wrong_phase_rejected": true + }, + "negative_controls": { + "missing_central_translation": "Rejected by the complete Laurent endpoint", + "omitted_copy": "Rejected by full arbitrary-input endpoint", + "unearned_helper": "Rejected by native helper census", + "wrong_frame": "Rejected by literal source-frame check" + }, + "physical_caller": { + "central_square_columns": 53248, + "full_calls": 18, + "main_targets": { + "145": 208, + "17": 416, + "25": 416, + "33": 416, + "41": 416, + "49": 416, + "57": 416, + "65": 416, + "73": 208 + }, + "new_paid_jobs": 0, + "physical_contacts": 7488, + "ports": 104, + "route_payload_sha256": "7f4f0ca768ffbc4f93dcff575592c4c67411f46b4289e45b73f715a2ad47b142", + "tensor_rule": "Factorwise native maps; scalar signs stay outside the tensor power.", + "whole_idle_jobs": { + "16": 416, + "24": 416, + "32": 416, + "40": 416, + "48": 416, + "56": 416, + "64": 416, + "72": 208 + }, + "wrapper_sites": [ + 1, + 3, + 5, + 7, + 9, + 11, + 13, + 15, + 17, + 19, + 21, + 23, + 25, + 27, + 29, + 31 + ] + }, + "separate_columns": { + "arithmetic": "Dense integer rows with binary denominators; reverse chronology", + "coefficients": 552049, + "columns": 743 + }, + "source_inputs_authenticated": 16, + "status": "PASS_P104_PRODUCTIVE_COMPLETE_KAPPA_00304057" +} diff --git a/research/kappa-architecture-frontier/inputs/p104-5545.json b/research/kappa-architecture-frontier/inputs/p104-5545.json new file mode 100644 index 0000000000..a4daa8e3f1 --- /dev/null +++ b/research/kappa-architecture-frontier/inputs/p104-5545.json @@ -0,0 +1,326 @@ +{ + "complete_cost": { + "compiler": { + "H": 337848000000000, + "N": "2^337848000000000", + "eta": { + "lower": "0.000000185282065079605829383859", + "upper": "0.000000185282065079605829383860" + }, + "gap": "1/7000000000", + "integer_test_exponent": 48264, + "logarithm_power": 1000, + "theta": "63/64", + "uniform_saving": "5322049/1750000000", + "word_materialized": false + }, + "full_forward_calls": 18, + "gain": "3/5000000", + "kappa": "304117/100000000", + "kappa_decimal": ".00304117", + "margin_at_previous": { + "lower": "0.149437868133364955605863720182", + "upper": "0.149437868133364955605863720183" + }, + "negative_controls": { + "old_BIT": "Rejected by outer inequalities", + "old_cutoff": "Rejected by completion-tail ratio greater than one" + }, + "nonrecursive": { + "fixed_scalar_growth_bound": "At most 2^(16*26000) before native factors; a declared constant, not an attained norm.", + "local_routes": 5334000, + "local_scalar": 217428, + "peak_owned_fields": 1, + "raw_budget": 1000000000, + "raw_scalar_upper": 184647552, + "tensor_native_growth_bound": "Each rank-r Gaussian has row l1 norm at most 2^(rf); sum of local ranks is 5894." + }, + "ordinary_BIT": { + "admitted": "17/5000", + "after_cover": "69/20000", + "atom": "1/250", + "before_cover": "3459/1000000", + "ordinary_saving": "8590884599/2500000000000", + "prime_rule": "odd q > 2^26*N^5 avoiding all fixed denominators and rank witnesses" + }, + "outer": { + "functional_checks": { + "actual_new_BIT_stock_sublinear": "1742999999253/1750000000000", + "fixed_halo_explicit_metadata_branch": "134750000001/1750000000", + "new_BIT_row_stock_sublinear_in_active_group": "6978999997009/7000000000000", + "new_semantic_group_guard": "3/7000000000" + }, + "margins": { + "boundary_algebraic_matrix": "149017357978711807/49000000000000000000", + "fused_gaussian": "149017357936135421/49000000000000000000", + "global_coordinate_router": "10644097/3500000000", + "group_bit_router": "74508682468067709/24500000000000000000", + "group_scans": "3499999999/3500000000", + "main_transform": "149017350978711807/49000000000000000000", + "microbox_face_corrections": "134750000001/1750000000", + "polynomial_products": "6999999999/7000000000", + "sparse_union_movement": "20055267357978711807/49000000000000000000" + }, + "parameters": { + "a": "10644097/3500000000", + "b": "4257639/1400000000", + "beta": "6999999997/7000000000", + "bit_saving": "17/5000", + "cap_xi": "44555267350978711807/49000000000000000000", + "complex_uniform_saving": "5322049/1750000000", + "d": "1/7000000000", + "epsilon": "6999999999/7000000000", + "kappa": "304117/100000000", + "lambda_": "1993917659/2000000000", + "lambda_prime": "6978711807/7000000000", + "layout": "1/7000000000", + "q": "21288193/7000000000", + "r0": "1/70000000000", + "stop": "1/7000000000", + "tested_saving": "3041171/1000000000" + }, + "strict_checks": { + "actual_bit_above_effective": "1255903/3500000000", + "actual_logarithmic_gamma_guard": "1/7000000000", + "actual_logarithmic_group_guard": "4444732659521288193/24500000000000000000", + "alpha_logarithm_absorption": "1/70000000000", + "boundary_algebraic_matrix_above_kappa": "27978711807/49000000000000000000", + "cap_above_band": "20055267350978711807/49000000000000000000", + "cap_below_cell": "4444732642021288193/49000000000000000000", + "cap_below_phase_cell_power": "53444732649021288193/49000000000000000000", + "complex_above_effective": "1/7000000000", + "complex_below_one_over_32": "39492361/1400000000", + "complex_endpoint": "1/3500000000", + "epsilon_below_one": "1/7000000000", + "epsilon_positive": "6999999999/7000000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "27936135421/49000000000000000000", + "gaussian_above_main": "3478711807/24500000000000000000", + "global_coordinate_router_above_kappa": "1/1750000000", + "global_gamma_power_slack": "9/70000000000", + "group_below_dimension": "1/3500000000", + "group_bit_router_above_kappa": "17468067709/24500000000000000000", + "group_gauge_power_slack": "4444732659171288193/24500000000000000000", + "group_key_fits_record": "1/3500000000", + "group_positive": "6999999997/7000000000", + "group_scans_above_kappa": "27260593/27343750", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "655099790400418148631/500000000000000000000000", + "lambda_above_internal": "1/14000000000", + "lambda_above_sigma": "3/14000000000", + "lambda_above_tau": "1/14000000000", + "lambda_prime_above_lambda": "1/14000000000", + "lambda_prime_above_leaf": "2795742361/9800000000000000000", + "leaf_saving_above_effective": "1395742361/9800000000000000000", + "main_transform_above_kappa": "20978711807/49000000000000000000", + "membership_arithmetic_fits_record": "1/7000000000", + "microbox_face_corrections_above_kappa": "269489355907/3500000000", + "microbox_halo_volume": "553000000003/7000000000", + "new_complex_uniform_saving_above_b": "1/7000000000", + "new_semantic_guard_with_C1_one": "1/7000000000", + "polynomial_products_above_kappa": "6978711809/7000000000", + "positive_layout_slack": "1/7000000000", + "q_below_effective": "1/7000000000", + "q_below_internal": "1/7000000000", + "q_below_leaf": "2795742361/9800000000000000000", + "q_positive": "21288193/7000000000", + "short_record_fallback": "1395742361/1400000000", + "source_axis_superpolynomial": "1/7000000000", + "sparse_union_movement_above_kappa": "19906250027978711807/49000000000000000000", + "stop_below_one": "6999999999/7000000000", + "stop_positive": "1/7000000000", + "strassen_integer_power_gap": "1951441519231", + "support_router_span": "3/7000000000", + "theta_positive_polynomial_power": "2", + "union_header_fits_record": "3/7000000000", + "union_tag_work_per_visit_fits_record": "3/7000000000" + } + }, + "paid": { + "1": 45264, + "16": 416, + "2": 10026, + "24": 416, + "3": 7002, + "32": 416, + "4": 2016, + "40": 416, + "48": 416, + "5": 1926, + "56": 416, + "6": 306, + "64": 416, + "7": 234, + "72": 208, + "9": 18 + }, + "paid_calls": 69912, + "previous_open_pr5544": "304057/100000000", + "productive_fields": 12814, + "query_shears": 15, + "rank_mass_surplus": 760, + "raw_headroom": [ + "181649/100000000000000", + "3633/2000000000000" + ], + "raw_root_interval": [ + "304117181649/100000000000000", + "6082343633/2000000000000" + ], + "relative_gain_percent": "6000/304057", + "strictification": { + "alpha": { + "lower": "0.999999999145880726810628283573", + "upper": "0.999999999145880726810628283574" + }, + "cutoff": 17, + "delta": { + "lower": "0.963355080494670721016731077055", + "upper": "0.963355080494670721016731077056" + }, + "floor": 18, + "gamma": { + "lower": "0.965211488800306029729343582168", + "upper": "0.965211488800306029729343582169" + }, + "normalized_paid_upper": "5242880004882813/5242880536870912", + "power": 1024, + "reserve": "1/10000000000", + "tail_offset": "1/5", + "tested": "3041171/1000000000" + }, + "targets": { + "145": 208, + "17": 416, + "25": 416, + "33": 416, + "4": 918, + "41": 416, + "49": 416, + "5": 648, + "57": 416, + "65": 416, + "7": 432, + "73": 208, + "8": 2196, + "9": 5292 + }, + "whole_idle_jobs": 3120 + }, + "complete_paid_delta": { + "1": -18, + "5": -18, + "6": 18 + }, + "limits": [ + "The five framework assumptions of PR5544 remain.", + "The uniform compiler word and complete rounded multiplier are not materialized.", + "No independent human or proof-kernel acceptance is claimed." + ], + "local": { + "endpoint_coefficients": 552049, + "helpers": { + "4": 51, + "5": 36, + "7": 24, + "8": 122, + "9": 294 + }, + "owned_lifetimes": 8, + "paid": { + "1": 2428, + "2": 557, + "3": 389, + "4": 112, + "5": 107, + "6": 17, + "7": 13, + "9": 1 + }, + "peak_owned_fields": 1, + "public_inputs": 735, + "real_scalar_allowance": 217428 + }, + "local_paid_delta": { + "1": -1, + "5": -1, + "6": 1 + }, + "native": { + "distinct_maps": 2981, + "helper_normalizers": 1054, + "helpers": { + "4": 51, + "5": 36, + "7": 24, + "8": 122, + "9": 294 + }, + "main_adapters": 208, + "proof": "Every signed Pauli image and exact global phase; frame induction at every positive tensor width", + "recipe_payload_sha256": "5901f62355998c69803fb961c5b0d20415f7006880b2cefbb4a57fbdb982d9a4", + "wrong_phase_rejected": true + }, + "negative_controls": { + "intervening_source_read": "No intervening read or write", + "missing_central_translation": "Rejected by the complete Laurent endpoint", + "one_operand_only": "Common scalar chart", + "uncharged_call": "Complete field and call counts", + "wrong_contact_sign": "All 743 public and owned rows" + }, + "physical_caller": { + "central_square_columns": 53248, + "full_calls": 18, + "main_targets": { + "145": 208, + "17": 416, + "25": 416, + "33": 416, + "41": 416, + "49": 416, + "57": 416, + "65": 416, + "73": 208 + }, + "new_paid_jobs": 0, + "physical_contacts": 7488, + "ports": 104, + "route_payload_sha256": "7f4f0ca768ffbc4f93dcff575592c4c67411f46b4289e45b73f715a2ad47b142", + "tensor_rule": "Factorwise native maps; scalar signs stay outside the tensor power.", + "whole_idle_jobs": { + "16": 416, + "24": 416, + "32": 416, + "40": 416, + "48": 416, + "56": 416, + "64": 416, + "72": 208 + }, + "wrapper_sites": [ + 1, + 3, + 5, + 7, + 9, + 11, + 13, + 15, + 17, + 19, + 21, + 23, + 25, + 27, + 29, + 31 + ] + }, + "separate_columns": { + "arithmetic": "Dense integer rows with binary denominators; reverse chronology", + "coefficients": 552049, + "columns": 743 + }, + "source_inputs_authenticated": 22, + "status": "PASS_P104_CONTACT_COMPLETE_KAPPA_00304117" +} diff --git a/research/kappa-architecture-frontier/inputs/p104-5551.json b/research/kappa-architecture-frontier/inputs/p104-5551.json new file mode 100644 index 0000000000..a83db6d025 --- /dev/null +++ b/research/kappa-architecture-frontier/inputs/p104-5551.json @@ -0,0 +1,332 @@ +{ + "complete_cost": { + "compiler": { + "H": 690116000000000, + "N": "2^690116000000000", + "eta": { + "lower": "0.000000184942858502899385581767", + "upper": "0.000000184942858502899385581768" + }, + "gap": "1/14000000000", + "integer_test_exponent": 49294, + "logarithm_power": 1000, + "theta": "63/64", + "uniform_saving": "21290713/7000000000", + "word_materialized": false + }, + "full_forward_calls": 18, + "gain": "9/25000000", + "kappa": "304153/100000000", + "kappa_decimal": ".00304153", + "margin_at_previous": { + "lower": "0.089671185966380263298820901941", + "upper": "0.089671185966380263298820901942" + }, + "negative_controls": { + "old_BIT": "Rejected by outer inequalities", + "old_cutoff": "Rejected by completion-tail ratio greater than one" + }, + "nonrecursive": { + "fixed_scalar_growth_bound": "At most 2^(16*26000) before native factors; a declared constant, not an attained norm.", + "local_routes": 5334000, + "local_scalar": 217428, + "peak_owned_fields": 1, + "raw_budget": 1000000000, + "raw_scalar_upper": 184647552, + "tensor_native_growth_bound": "Each rank-r Gaussian has row l1 norm at most 2^(rf); sum of local ranks is 5894." + }, + "ordinary_BIT": { + "admitted": "17/5000", + "after_cover": "69/20000", + "atom": "1/250", + "before_cover": "3459/1000000", + "ordinary_saving": "8590884599/2500000000000", + "prime_rule": "odd q > 2^26*N^5 avoiding all fixed denominators and rank witnesses" + }, + "outer": { + "functional_checks": { + "actual_new_BIT_stock_sublinear": "3485999999253/3500000000000", + "fixed_halo_explicit_metadata_branch": "269500000001/3500000000", + "new_BIT_row_stock_sublinear_in_active_group": "13957999997009/14000000000000", + "new_semantic_group_guard": "3/14000000000" + }, + "margins": { + "boundary_algebraic_matrix": "596139935957418577/196000000000000000000", + "fused_gaussian": "596139935872255731/196000000000000000000", + "global_coordinate_router": "2661339/875000000", + "group_bit_router": "37258746867015983/12250000000000000000", + "group_scans": "6999999999/7000000000", + "main_transform": "596139921957418577/196000000000000000000", + "microbox_face_corrections": "269500000001/3500000000", + "polynomial_products": "13999999999/14000000000", + "sparse_union_movement": "80221139935957418577/196000000000000000000" + }, + "parameters": { + "a": "2661339/875000000", + "b": "1703257/560000000", + "beta": "13999999997/14000000000", + "bit_saving": "17/5000", + "cap_xi": "178221139921957418577/196000000000000000000", + "complex_uniform_saving": "21290713/7000000000", + "d": "1/14000000000", + "epsilon": "13999999999/14000000000", + "kappa": "304153/100000000", + "lambda_": "3987833879/4000000000", + "lambda_prime": "13957418577/14000000000", + "layout": "1/14000000000", + "q": "42581423/14000000000", + "r0": "1/140000000000", + "stop": "1/14000000000", + "tested_saving": "6083061/2000000000" + }, + "strict_checks": { + "actual_bit_above_effective": "313661/875000000", + "actual_logarithmic_gamma_guard": "1/14000000000", + "actual_logarithmic_group_guard": "17778860099042581423/98000000000000000000", + "alpha_logarithm_absorption": "1/140000000000", + "boundary_algebraic_matrix_above_kappa": "55957418577/196000000000000000000", + "cap_above_band": "80221139921957418577/196000000000000000000", + "cap_below_cell": "17778860064042581423/196000000000000000000", + "cap_below_phase_cell_power": "213778860078042581423/196000000000000000000", + "complex_above_effective": "1/14000000000", + "complex_below_one_over_32": "15796743/560000000", + "complex_endpoint": "1/7000000000", + "epsilon_below_one": "1/14000000000", + "epsilon_positive": "13999999999/14000000000", + "fine_prime_halo_umbrella": "7/2", + "fused_gaussian_above_kappa": "55872255731/196000000000000000000", + "gaussian_above_main": "6957418577/98000000000000000000", + "global_coordinate_router_above_kappa": "1/3500000000", + "global_gamma_power_slack": "9/140000000000", + "group_below_dimension": "1/7000000000", + "group_bit_router_above_kappa": "4367015983/12250000000000000000", + "group_gauge_power_slack": "17778860098342581423/98000000000000000000", + "group_key_fits_record": "1/7000000000", + "group_positive": "13999999997/14000000000", + "group_scans_above_kappa": "6978709289/7000000000", + "halo_covers_generic_inverse_radius": "5", + "improvement_over_user_baseline": "655279790400418148631/500000000000000000000000", + "lambda_above_internal": "1/28000000000", + "lambda_above_sigma": "3/28000000000", + "lambda_above_tau": "1/28000000000", + "lambda_prime_above_lambda": "1/28000000000", + "lambda_prime_above_leaf": "1118296743/7840000000000000000", + "leaf_saving_above_effective": "558296743/7840000000000000000", + "main_transform_above_kappa": "41957418577/196000000000000000000", + "membership_arithmetic_fits_record": "1/14000000000", + "microbox_face_corrections_above_kappa": "134744677323/1750000000", + "microbox_halo_volume": "1106000000003/14000000000", + "new_complex_uniform_saving_above_b": "1/14000000000", + "new_semantic_guard_with_C1_one": "1/14000000000", + "polynomial_products_above_kappa": "13957418579/14000000000", + "positive_layout_slack": "1/14000000000", + "q_below_effective": "1/14000000000", + "q_below_internal": "1/14000000000", + "q_below_leaf": "1118296743/7840000000000000000", + "q_positive": "42581423/14000000000", + "short_record_fallback": "558296743/560000000", + "source_axis_superpolynomial": "1/14000000000", + "sparse_union_movement_above_kappa": "79625000055957418577/196000000000000000000", + "stop_below_one": "13999999999/14000000000", + "stop_positive": "1/14000000000", + "strassen_integer_power_gap": "1951441519231", + "support_router_span": "3/14000000000", + "theta_positive_polynomial_power": "2", + "union_header_fits_record": "3/14000000000", + "union_tag_work_per_visit_fits_record": "3/14000000000" + } + }, + "paid": { + "1": 45300, + "16": 416, + "2": 9972, + "24": 416, + "3": 7020, + "32": 416, + "4": 1998, + "40": 416, + "48": 416, + "5": 1944, + "56": 416, + "6": 306, + "64": 416, + "7": 234, + "72": 208, + "9": 18 + }, + "paid_calls": 69912, + "previous_open_pr5545": "304117/100000000", + "productive_fields": 12814, + "query_shears": 15, + "rank_mass_surplus": 760, + "raw_headroom": [ + "58357/50000000000000", + "23343/20000000000000" + ], + "raw_root_interval": [ + "152076558357/50000000000000", + "60830623343/20000000000000" + ], + "relative_gain_percent": "3600/304117", + "strictification": { + "alpha": { + "lower": "0.999999999302190665441264809032", + "upper": "0.999999999302190665441264809033" + }, + "cutoff": 17, + "delta": { + "lower": "0.963355290100190429734309350200", + "upper": "0.963355290100190429734309350201" + }, + "floor": 18, + "gamma": { + "lower": "0.965231303139134897171411452319", + "upper": "0.965231303139134897171411452320" + }, + "normalized_paid_upper": "5242880004882813/5242880536870912", + "power": 1024, + "reserve": "1/10000000000", + "tail_offset": "1/5", + "tested": "6083061/2000000000" + }, + "targets": { + "145": 208, + "17": 416, + "25": 416, + "33": 416, + "4": 918, + "41": 416, + "49": 416, + "5": 648, + "57": 416, + "65": 416, + "7": 432, + "73": 208, + "8": 2196, + "9": 5292 + }, + "whole_idle_jobs": 3120 + }, + "complete_paid_delta": { + "1": 36, + "2": -54, + "3": 18, + "4": -18, + "5": 18 + }, + "independent_peer_science_sha256": "357bf2617d364fb951c704b0bba7bb920629494686ab3866fed910fb0f2f57fc", + "limits": [ + "The five framework assumptions retained by PR5544/5545 remain.", + "The uniform compiler word and complete rounded multiplier are not materialized.", + "No independent human or proof-kernel acceptance, selected promotion, or core-contributor status is claimed." + ], + "local": { + "endpoint_coefficients": 552049, + "helpers": { + "4": 51, + "5": 36, + "7": 24, + "8": 122, + "9": 294 + }, + "owned_lifetimes": 8, + "paid": { + "1": 2430, + "2": 554, + "3": 390, + "4": 111, + "5": 108, + "6": 17, + "7": 13, + "9": 1 + }, + "peak_owned_fields": 1, + "public_inputs": 735, + "real_scalar_allowance": 217428 + }, + "local_paid_delta": { + "1": 2, + "2": -3, + "3": 1, + "4": -1, + "5": 1 + }, + "native": { + "distinct_maps": 2979, + "helper_normalizers": 1054, + "helpers": { + "4": 51, + "5": 36, + "7": 24, + "8": 122, + "9": 294 + }, + "main_adapters": 208, + "proof": "Every signed Pauli image and exact global phase; frame induction at every positive tensor width", + "recipe_payload_sha256": "f7dac0d38942f0b02ad21c166281aeed704bc133421843f2b0ededaaf654e4a9", + "wrong_phase_rejected": true + }, + "negative_controls": { + "missing_central_translation": "Rejected by the complete Laurent endpoint", + "one_operand_or_contact_left_at_old_chart": "Scalar destination and coefficient", + "stale_source_or_changed_read": "Exact source ADD at 10461", + "uncharged_recursive_call": "Complete field and call counts", + "wrong_butterfly_coefficient": "All 743 public and owned rows" + }, + "physical_caller": { + "central_square_columns": 53248, + "full_calls": 18, + "main_targets": { + "145": 208, + "17": 416, + "25": 416, + "33": 416, + "41": 416, + "49": 416, + "57": 416, + "65": 416, + "73": 208 + }, + "new_paid_jobs": 0, + "physical_contacts": 7488, + "ports": 104, + "route_payload_sha256": "7f4f0ca768ffbc4f93dcff575592c4c67411f46b4289e45b73f715a2ad47b142", + "tensor_rule": "Factorwise native maps; scalar signs stay outside the tensor power.", + "whole_idle_jobs": { + "16": 416, + "24": 416, + "32": 416, + "40": 416, + "48": 416, + "56": 416, + "64": 416, + "72": 208 + }, + "wrapper_sites": [ + 1, + 3, + 5, + 7, + 9, + 11, + 13, + 15, + 17, + 19, + 21, + 23, + 25, + 27, + 29, + 31 + ] + }, + "retained_source_files": 33, + "separate_columns": { + "arithmetic": "Dense integer rows with binary denominators; reverse chronology", + "coefficients": 552049, + "columns": 743 + }, + "source_commit": "18968423711fd902aaee1099979497d55603e1dc", + "status": "PASS_P104_JOINT_CONTACT_COMPLETE_KAPPA_00304153" +} diff --git a/research/kappa-architecture-frontier/inputs/p104-caller-proof.md b/research/kappa-architecture-frontier/inputs/p104-caller-proof.md new file mode 100644 index 0000000000..e0bb34fbef --- /dev/null +++ b/research/kappa-architecture-frontier/inputs/p104-caller-proof.md @@ -0,0 +1,212 @@ +# Productive P104 caller and complete conditional cost + +This construction gives conditional `kappa = 304057/100000000 = 0.00304057`. +It changes the complete recursive profile. It does not change the selected +record. The five retained framework assumptions are native all-column +implementation, owned erasure, the uniform compiler, precision and tape cost, +and analytic recovery. This package checks the new finite interfaces and +all parameters of that conditional calculation. It does not claim an +unconditional integer multiplication theorem. + +## 1. The complete source word + +Use Gareth Davidson's PR2305 composition of David Arias's PR2152 coalesced +P104 word and Cinna Davis's PR2219 private reuse. `local.construct()` rebuilds +that exact word from its archived source and compares the full report with +PR2305. It does not run or reuse the old owner-price model. `WORD.json.gz` +contains the emitted word, all binary frames, all public boundaries and the +104 retained port indices. It has 25,311 events and 735 independent public +inputs. The 208 live main fields are X_r and Y_r for the 104 retained indices. +All other public fields are independent helpers, including the 16 punctured +main roles. Eight distinct owned lifetime labels can use one physical slot. + +At each frame V let Phi_V be the pinned nine-axis native chart. A register +in frame V contains Phi_V times its logical value. A MOVE applies +Phi_new Phi_old^(-1). Each ADD or SCALE uses the same frame on every operand. +COPY reads into a cleared owned field; each final private CLEAR uses the +retained owned-erasure contract. The exact endpoint is + +```text +X_r -> X_r +Y_r -> Y_r + X_r for every retained port r +h -> h for every one of the 527 helpers +owned -> 0 for all eight owned lifetime labels +``` + +The first interpreter checks this matrix on all 743 public and owned rows, +including arbitrary owned entrance values before initialization. A separate +interpreter applies the transposed instruction matrices in reverse order. +It uses dense integer rows with binary denominators. Both checks cover all +552,049 coefficients, including zeros. The private slot is initialized before +use and is cleared after use; its peak occupancy is one. It receives no +productive credit. The source word, correction and reuse are predecessor +results, not new local circuits. + +For each positive width f replace every chart by its factorwise tensor power. +Every common-chart scalar step still acts on the same logical values, with +its scalar coefficient outside the tensor power. The frame induction and +rational endpoint therefore hold at every f. Native phase checks include the +absolute scalar phase. Equality of an unsigned tableau alone is not used. +The pinned compiler produces each native recipe; a separate Gaussian +interpreter checks every Pauli image and the global phase. This establishes +the ideal linear identities. The retained all-column implementation and +rounded arithmetic hypotheses remain explicit. + +## 2. The local productive interface + +All public paths are nested. For each helper h, the complete boundary map +Phi_final Phi_initial^(-1) has Gaussian rank +`dim(final) - dim(initial)`. Native lowering checks this rank and supplies +its two monomial boundary maps. These maps give independent ordinary +Gaussian targets at these ranks: + +```text +helpers = {4:51, 5:36, 7:24, 8:122, 9:294} +paid = {1:2429, 2:557, 3:389, 4:112, 5:108, 6:16, 7:13, 9:1} +``` + +There are 527 helper targets and 3,625 paid calls. The paid rank mass is +5,894. Helper rank mass is 4,174. The main boundary progress is +`2*104*8 = 1664`, leaving 56 paid private-copy ranks. The unused helper 711 +keeps its paid H9 and its productive H9; they cancel in the moment. It is +not silently removed from one side of the calculation. + +The 2,981 distinct native maps include every paid occurrence and every helper +boundary. The 208 intrinsic main adapters have rank zero. Their phases give +these physical maps on port q: + +```math +Q_q=\frac{1+i}{2}I+\frac{1-i}{2}X_q,\qquad +F_s=D_s\begin{pmatrix}1&0\\Q_q^{-1}&1\end{pmatrix}. +``` + +At stage zero, `D_0=H9 Q_q^(-1)`. At later stages D_s acts on eight fresh +axes. The complete source accepts arbitrary main fields and arbitrary helper +fields, so this is a full interface, not a main-input subspace restriction. +Each full call uses a fresh independent helper inventory. + +## 3. A forward source supplies both caller orientations + +Retain Cinna Davis's literal p16/a7 controller from `joint-helper-lattice`. +Its 18 full sites formerly used two forward and sixteen backward interfaces. +Use the inverse of the direct wrapper in Ali Romman's PR5398. Put + +```math +R=\begin{pmatrix}0&1\\-Q^{-2}&0\end{pmatrix},\quad +B_s=R^{-1}F_sR + =D_s\begin{pmatrix}1&-Q\\0&1\end{pmatrix}. +``` + +For each backward site, the emitted execution order is + +```text +x <- Q^-2 x +(x,y) <- (y,-x) +execute the unchanged complete forward supplier +y <- Q^2 y +(x,y) <- (-y,x) +``` + +All 18 +full invocations now use the published forward word. No instruction-level +transpose of its COPY or CLEAR operations is needed. The wrapper acts only +on the two main fields; every helper and owned exit remains the source exit. + +Exact Gaussian arithmetic gives `Q^2=Q^-2=X_q`, with phase +1. It is a native +address translation, at every positive tensor width. Scalar minus signs stay +outside tensor substitution. D_s commutes with Q. Thus both signed exchanges +and both translations are ordinary operations. They add no Gaussian call. +The full Laurent replay retains Q as a formal invertible variable; it does +not impose Q^2=I to prove the caller identity. + +The physical check binds all 104 ports at all 18 full sites. It checks the +orthogonal route, inverse route, fixed central direction, four boundary +contacts and exact cross term. This gives 7,488 boundary contacts in the +265-axis layout. The 53,248 central-square column checks cover all nine-axis +columns at every port. Each route changes at most 17 axes. The phase check +also binds all 3,328 main targets and every whole idle job. If an idle includes +stage zero, its first eight axes are the actual orthonormal basis of +q-perpendicular; the residual translation is charged as ordinary work. +Unused fresh axes are spectators and can be deleted by an injective relabeling. + +The 15 thin queries keep the existing paid implementation: initialize an +owned field, COPY the source, perform Q or Q^-1, ADD to the target, and erase +the owned field. There is one paid rank-one call per port and no target +credit for that field. Q^-1 uses a positive Gaussian and its translation. +The one physical owned slot is reused sequentially by full and thin calls. + +## 4. The complete invoice + +For each full site add the local paid and helper profiles. For each thin +site add 104 H1 calls. For each idle with j stages add 208 H(8j) calls. +Each main Laurent diagonal gives 104 targets of rank `1+8j`. +A separate count from the two path lengths 7 and 8 gives the same invoice. +The resulting complete counts are + +```text +paid calls: 69930 +productive fields: 12814 = 18*527 + 32*104 +thin paid calls: 1560 +whole idle jobs: 3120 +rank mass surplus: 760 +maximum target: 145 +maximum paid rank: 72 +``` + +`RESULT.json` gives both full histograms. Every helper boundary and main target +has a native map. All COPY paths, source correction, cleanup, thin calls and +whole idles are included. The old fixed-window owner assignment is not used. +The retained mixed-target theorem supplies the productive matching and +uniform recursion from this complete field interface. No new helper output +is treated as free work without its corresponding paid path. + +Two rational interval engines check `sum(T_r*r^(1-k)) - sum(P_r*r^(1-k))`. +A sign-changing crossing is enclosed in +`(0.00304057807630, 0.00304057807631)`. This is a bound for the stated profile, +not an optimum over local words or controllers. The tested saving is +0.003040575. The claimed kappa 0.00304057 leaves more than 8.0763e-9 to this +crossing and improves selected 0.003027288235 by 0.000013281765. + +The complete tail calculation uses power 1024, cutoff 17, target floor 18, +offset 1/5, and reserve 1e-10. The paid ratio is less than +0.999999996781291. The higher-moment ratio is less than 0.965182173 and the +completion ratio is less than 0.963354733. Both tail ratios are below 0.97; +`0.97^128 < 1/16`. Splitting and rounding give the strict normalized bound +`5242880004882813/5242880536870912 < 1`. The old cutoff 20 fails for this +larger helper inventory and is rejected by a control. + +With complement factor 63/64 and logarithm power 1000, the compiler uses +`H=64215200000000` and `N=2^H`. The integer test exponent is 45,868; +`(H+1)^1000 < 2^45868`, and the preceding grid point fails. The arithmetic +checks all 54 strict outer predicates and four functional predicates. +The retained ordinary BIT saving is 0.0034, above the new complex requirement. +No stronger BIT result is needed. The uniform compiler word is specified by +the retained finite algorithm and is not materialized. + +## 5. Ordinary work, storage and precision boundary + +The source scalar allowance is 217,428 real operations. The route allowance +counts each paid map, both normalizers for every helper, all intrinsic main +adapters, all four fresh-stage contacts per port, and the eight owned +lifetimes. Each fixed map is on at most 17 active axes and has a 1,000-unit +allowance. The sum is below 10^7 per full call. The global raw allowance is +184,647,552, below the funded 10^9 bound. It includes thin COPY/ADD/erase, +scalar boundary programs, all signed exchanges and translations. One owned +field suffices in addition to the independent public fields. No helper +initialization assumes its arbitrary dirt is zero. + +The source checks fewer than 26,000 events and `1+abs(coefficient) < 2^16` +for every scalar update. A safe local scalar growth bound is 2^(16*26000). +Each rank-r tensor Gaussian has row l1 norm at most 2^(rf). The complete +raw implementation therefore has a conservative growth bound +`2^(10^9 + R*f)`, where R is the sum of the full paid ranks in RESULT.json. +Independent local defects can be bounded by the number of raw operations +and paid calls times this factor. These are finite upper bounds, not sharp +or attained norms. They include the intermediate growth in the three-ADD +signed exchange. They provide parameters for the retained precision/tape +contract; a complete rounded integer multiplier is not executed here. + +The claim retains the five framework assumptions stated at the start. +Normal and optimized Python checks, immutable source authentication, failure +controls and a Git-free export are verification of this conditional package. +They are not independent human acceptance or a proof-kernel theorem. diff --git a/research/kappa-architecture-frontier/inputs/p104-contact-proof.md b/research/kappa-architecture-frontier/inputs/p104-contact-proof.md new file mode 100644 index 0000000000..d1c5fb2211 --- /dev/null +++ b/research/kappa-architecture-frontier/inputs/p104-contact-proof.md @@ -0,0 +1,161 @@ +# Coupled contacts and complete conditional price + +The endpoint is `kappa = 304153/100000000 = .00304153`, improving Ali +Romman's PR5545 endpoint `.00304117` by `9/25000000 = .00000036`. +Source head: `18968423711fd902aaee1099979497d55603e1dc`. +The selected record is unchanged. All five framework premises remain: +native all-column implementation, owned erasure, uniform compiler, +precision and tape costs, and analytic recovery. This proves an ideal +operator change and a complete conditional price; the enormous uniform +word and rounded integer multiplier are not materialized. + +## Literal change and all-width implication + +`construct.py` pins these six zero-based source events: + +| Event | Unchanged scalar operation | Old frame | New frame | +| --- | --- | --- | --- | +| 10461 | `297 += 303` | 335 | 17 | +| 10462 | `303 -= 297/2` | 335 | 17 | +| 13970 | `152 -= 297/2` | 335 | 17 | +| 15479 | `198 += 319` | 915 | 207 | +| 15639 | `205 += 198` | 915 | 207 | +| 15640 | `198 -= 205/2` | 915 | 207 | + +Frame 335 has dimension two. Frame 17 is `span(145)`, dimension one. +Frame 915 has dimension seven. Frame 207 has dimension eight and basis +`[2,5,8,17,33,65,129,257]`. All are existing source canonical charts. +No new coordinate transformation is granted for free. + +The emitter issues every nested MOVE needed to place both operands at +the declared common frame. SCALE occurs at its operand's current frame; +terminal public MOVEs finish at the original exits. Fifteen SCALE chart +annotations change; every scalar coefficient and its order is retained. +INIT/COPY/CLEAR lifetimes are unchanged. Every actual intervening source +read and write is included in the complete replay. The word has 25,310 events. + +The separate [peer proof](peer/PROOF.md) and +[role histories](peer/RECEIPT.json) bind the actual field versions. In the +first group, role 297 coalesces two rank-one rises into rank two; role 303 +splits rank two into two rank-one rises; role 152 replaces two rank-two +rises by ranks one and three. Their net delta is `H1 - 2H2 + H3`. +In the second group, role 198 replaces ranks four plus one by rank five; +role 319 exchanges the order of ranks one and two with zero profile delta; +role 205 splits rank two into two rank-one rises. The net delta is +`H1 - H2 - H4 + H5`. + +Let Phi_F be the exact canonical source chart. At field width f, a role +stores Phi_F tensor-power f applied to its logical value. A MOVE F to G +applies `Phi_G Phi_F^{-1}` tensor-power f, preserving that logical value. +Same-chart ADD/COPY acts on logical values with its scalar applied once, +outside tensor powers. SCALE commutes with transport by linearity. Thus +the unchanged scalar/owned word and fixed endpoint charts imply exactly +the same complete physical operator at every positive f. This is a +compositional induction: no sum is tensor-powered and no width-one +linear-independence claim is used. + +Three exact endpoint checks cover all 743 rows and 552,049 coefficients: +sparse rational forward rows, dense integer reverse columns with binary +denominators, and an independently written integer/dyadic peer interpreter +that imports neither constructor nor native checker. All 735 public inputs +remain arbitrary. All 527 productive helpers retain their targets. Eight +owned lifetimes retain peak occupancy one and the original erasure premise. + +The source native compiler freshly lowers every MOVE, helper boundary and +main adapter. Its separate Gaussian interpreter compares every signed Pauli +image and absolute global phase: 2,979 distinct maps, 1,054 helper normalizers +and 208 main adapters. Wrong phase is rejected. These exact base identities +tensor to every positive f. The unchanged complete caller is freshly checked +through its Laurent identity, 265-axis phase polynomial, 104 ports, both +orientations and actual orthogonal routes. This algebraic check is distinct +from materializing exponential-size all-column matrices. + +The added independent dense audit checks all 512 columns of each of the +four new MOVE maps: `17 -> 720` (rank 2), `17 -> 782` (rank 3), +`615 -> 207` (rank 5), and `775 -> 207` (rank 2). It compares +1,048,576 exact complex entries, including +absolute phase, column norm and support. The unchanged credited PR5548 +arithmetic engine executes the literal source charts and lowered recipes; +the source/vendor tableau is not used for matrix equality. Phase-only +faults invisible to signed Pauli images are rejected. The exact base +equalities tensor factorwise, with phase i^theta lifted as i^(f theta). +This checks the new map interfaces only, and retains the old native and +uniform implementation premises. + +## Complete moment and transfer + +The new local paid profile is + +```text +{1:2430, 2:554, 3:390, 4:111, 5:108, 6:17, 7:13, 9:1}. +``` + +Its delta from PR5545 is + +```text +local: +2H1 -3H2 +H3 -H4 +H5 +complete: +36H1 -54H2 +18H3 -18H4 +18H5 +target: zero at every rank. +``` + +For `H_r=r^t`, `0 H6` edit +and lies outside PR5548's narrow repetition ceiling. + +Each invocation retains helper targets `{4:51,5:36,7:24,8:122,9:294}`. +The full bill includes 18 forward invocations, 15 genuine queries, 15 whole +idles and 32 main banks: 69,912 paid calls, 12,814 productive fields and rank +surplus 760. Maximum paid/target ranks remain 72/145. No helper is omitted. + +`pricing.py` retains PR5544/5545's funding argument. New mathematical +parameters are claimed/tested saving and comparison endpoint; its input +histogram comes from the freshly replayed word. Two independent full +invoice counts and both inherited rational moment engines must agree. +The strict raw crossing enclosure is + +```text +.00304153116714 < raw crossing < .00304153116715. +``` + +The separate funding peer implements a third rational interval engine: +50-term atanh logarithms with rigorous tails and 128-bit outward grids, +followed by alternating exponential bounds of degrees 15/14. It imports +neither retained moment engine. Its four sign enclosures and full invoice +recount agree. The wrapper binds the audited word, source and complete +receipt to this publication. + +Tested saving is `.0030415305`. Cutoff 17, floor 18, tail offset 1/5, +power 1024, reserve `10^-10` and logarithm power 1000 fund completion, +splitting and rounding. Compiler gap is `1/14000000000`, integer height +`H=690116000000000`, test exponent 49,294; the preceding integer point +fails. Ordinary/admitted BIT stock checks and all 54 strict plus four +functional outer predicates pass. `RESULT.json` records exact rationals. +The endpoint gain is not claimed to equal the raw-crossing difference, +which has different safety margins. No global optimum is claimed. + +Scalar coefficients and counts are unchanged. The 26,000-event bound, +per-event scalar growth below `2^16`, total local Gaussian rank 5,894 and +owned peak one still bound reordered prefixes. Local native ranks stay +at most nine. Routing, normalization, COPY, caller and erasure allowances +are recomputed; no precision/tape cost is set to zero. The same five +framework premises remain necessary. + +## Controls, source retention and credit + +The verifier rejects an old-chart contact, wrong butterfly coefficient, +changed source event and uncharged recursive call. The peer also rejects +missing owned CLEAR. Inherited checks reject missing central translation, +wrong native phase, adverse completion cutoff and inadequate BIT saving. +All 33 dependency files are authenticated before imports. The closed +official export retains the exact PR5545 bytes and source attribution. + +Prepared for thu-nmrc with substantial OpenAI Codex assistance, Apache-2.0. +These are author-side checks, not independent human/proof-kernel acceptance. +Credit Ali Romman for PR5544/5545's caller and price; Gareth Davidson for +PR2305; David Arias for PR2152; Cinna Davis for PR2219/controller; Jacob +Alan Sussman for productive recursion; zxv for compiler/outer machinery; +Cao Yifan for pricing; and all geometry, common-chart, dual-ADD, native, +COPY, precision and analytic predecessors in the retained proofs. The +new contribution is this coupled literal itinerary and conditional gain. diff --git a/research/kappa-architecture-frontier/inputs/p19-precompilation.json b/research/kappa-architecture-frontier/inputs/p19-precompilation.json new file mode 100644 index 0000000000..9a5ea04e5d --- /dev/null +++ b/research/kappa-architecture-frontier/inputs/p19-precompilation.json @@ -0,0 +1,66 @@ +{ + "chronology": { + "bridges": 108, + "endpoint_link": "P19_UNITS.json", + "final_unloads": 19, + "idles": 36, + "initial_gauges": 19, + "operator_link": "P19_LIFT.json", + "primitive_link": "P19_LOWERING.json", + "signed_swaps": 19 + }, + "new_p19_condition": true, + "paid_work": { + "monomial_field_maps": 17248, + "owned_clears": 1232, + "rank_cost": 0, + "recodings": 77, + "recursive_gaussian_children": 0, + "scalar_adds": 68992 + }, + "primitive_contract": { + "all_column": "not established by this probe", + "arbitrary_inputs": "symbolic inputs only", + "fixed_precision_interface": "not established by this probe", + "owned_erasure": "not executed by the macro replay", + "owned_scratch": "not executed by the macro replay", + "source": "research/coded-native-caller/PHYSICAL.md", + "source_sha256": "4321b159ff8d3fe705419adaaa1beef75606e869e34341bda553f17d598a6078" + }, + "proof_boundary": { + "frozen_program_replay": "inherited base evidence", + "macro_replay": "P19_NATIVE_MACRO_REPLAY.json", + "missing": [ + "the complete p19 macro still requires the inherited finite native interface", + "literal forward/reverse programs are checked as formal owned-work macros, not serialized native records" + ], + "native_event_encoding": "typed finite macro contract over inherited PHYSICAL.md primitives", + "p19_specific_event_encoder": "P19_NATIVE_MACRO.json" + }, + "status": "FINDING_PRECOMPILATION_CONTRACT_MISSING", + "targets": { + "equals_invoice": true, + "source": "P19_DIAGCENSUS.json" + }, + "theorem": "research/direct-mixed-flow/vendor/FINITE-PRECOMPILATION.md", + "theorem_scope": "finite chronological composition under inherited native hypotheses", + "whole_job_adapters": { + "bracketed_middle_retained": true, + "link": "P19_BRIDGE.json", + "per_direction": 448 + }, + "word": { + "ambient_rank": 153, + "gate_kinds": { + "BRIDGE": 108, + "FORWARD": 20, + "GAUGE_LOAD": 19, + "GAUGE_UNLOAD": 19, + "IDLE": 36, + "LETTER": 19, + "REVERSE": 19, + "SWAP": 19 + }, + "gates": 259 + } +} diff --git a/research/kappa-architecture-frontier/inputs/p19-readme.md b/research/kappa-architecture-frontier/inputs/p19-readme.md new file mode 100644 index 0000000000..22dfb31401 --- /dev/null +++ b/research/kappa-architecture-frontier/inputs/p19-readme.md @@ -0,0 +1,146 @@ +# The p19 coded chain: conditional κ candidate 0.0033999964 + +**The controller word's factorized diagonal realises the inherited invoiced target multiset +exactly** — ranks 9…73 at 448 targets each and rank 153 at 224 — so the κ candidate is attached to +the physical chain, conditional on the inherited native/operation-level admission and the other +base premises. Nothing here is unconditional and the native lowering is not proved. + +Complex supplier **0.007578535190**, BIT supplier **17/5000**, +κ = **951999/280000000 = 0.0033999964**, **+12.58 %** over the selected record +`60403/20000000 = 0.00302015` and **+12.31 %** over the maintainer-reported `0.00302728823`. + +## Two objects, and the census that joins them + +- the **priced physical chain** — 259 gates, 77 recodings, 17,248 monomial maps, 68,992 adds, + 1,232 clears, zero recursive Gaussian children, ambient rank 153; +- the **formal reference** — 241 gates, zero recodings, the controller trace with denominators `[1]`. + +A target is what a role **ends holding**, i.e. an entry of the factorisation diagonal, not the row +or column closure of the thinned matrix. Measured on the diagonal, the target multiset is + +| p | realised diagonal sizes | designed | +|---|---|---| +| 3 | `{1:4, 3:2}` | identical | +| 4 | `{1:4, 2:2, 4:2}` | identical | +| 5 | `{1:4, 2:4, 5:2}` | identical | +| 8 | `{1:4, 2:4, 3:4, 4:2, 8:2}` | identical | +| 19 | `{1:4, 2:4, …, 9:4, 19:2}` | identical | + +so at p=19 the histogram is `{9:448, 17:448, 25:448, 33:448, 41:448, 49:448, 57:448, 65:448, +73:448, 153:224}` — the invoiced census, derived from the word. + +An earlier version of this package measured the **row closure** of the thinned matrix instead and +concluded the census did not match. That was the wrong observable: rows saturate, every role can see +every retained stage, while the diagonal keeps the prefix/suffix structure the invoice counts. Every +result built on the row closure — the invariance under rescheduling, the two-sided conjugacy bound, +the boundary gauge, the factor search, the cascade, the 0.2098 reprice — is retained only as a +superseded diagnostic, listed in `RESULT.json` under `superseded_diagnostics`. + +## The price and the paid accounting + +`invoice(p, pattern, thick, profile)` takes the pattern, the retained stages and the paid profile; +it names no adapter, operation or inventory quantity. The `I⁹T⁹` pattern with the odd stages +retained and the frozen paid profile gives the complex root 0.007578535190, reproducing the base's +own model (which the base checks at p=16 against its published 0.0030201659770). The endpoint is +BIT-bound: at exactly 0.0034 one ledger predicate fails, so the candidate is 0.0034 minus five grid +steps. + +Guards at the endpoint: α 0.995794142, γ 0.963763313, δ 0.951560608, both decay blocks under 1/16, +power-1024 tails under 2⁻³². Compiler: the shape-correct majorant at `v = 1024`, `h = 1/64`, +`B = (5+8h)v`, `H0 ≥ 8v` gives H0 = 5,170,423,668,736, with `20⁶⁴ < 21⁶³` and max target rank +153 < 256. Ledger: 54 strict + 4 functional predicates. + +## Physical binding + +`p19_lift.py` proves the gate list realises the controller operator: `Φ` is multiplicative over +263,169 exponent pairs, every axis pair commutes as full operators, `Φ(1) = I`, and the stage, +thick and block coverage is enumerated. `p19_bank.py` is a labelled control at p=2, pattern `T`, +over 2¹⁷ addresses per role. The chain replay in `p19_word.py` compares the 259 gates with the +standard word on 2,179,072 dense entries — randomised, and labelled as such. + +## D: the frozen base event profile, and the priced profile + +Two different objects, never to be conflated: + +| object | value | source | +|---|---|---| +| **frozen base event profile** | `{1:2201, 2:412, 3:510, 4:127, 5:40, 8:8}` | derived from the frozen word's event trace (`P19_NATIVE_APPLY.json`) | +| **priced D profile** | `{1:2201, 2:412, 3:510, 4:127, 5:40}` | inherited base invoice input (`P_NEW`, PR4929) | + +**Rank 8 is excluded by construction, not by omission.** `coded-reverse-controller/verify.py:167-168` +defines two profiles — `P_OLD` (joint-helper-lattice, includes `8:8`) and `P_NEW` (PR4929, does not) — +and `invoice()` prices exactly the dict it is handed; it has no built-in rank-8 rule. The eight rank-8 +events are the owned C₀ centre calls that the PR4929 center-free construction removes, and the p19 +chain emits **no CENTRE gate at all**, so `P_NEW` is the applicable profile. The frozen comparison +word still contains its centre calls, which is why its own declared profile shows `8:8`. + +## The frozen word's trace + +`p19_native_apply.py` re-implements the record -> event encoding and the frame/tariff transitions of +the pinned specification (`research/kappa-lean-verification-20261022/NativeCore.lean` and +`native_generate.py`, the PR4470/PR4610 lineage) and executes it on the frozen word: + +| direction | records | state steps | persistent frames | paid histogram | scalar tariff | +|---|---|---|---|---|---| +| forward | 21,449 | 20,991 | end on `canonical.final` | `{1:2201, 2:412, 3:510, 4:127, 5:40, 8:8}` | 158,120 | +| backward | 21,449 | 20,991 | end on `canonical.final` | same | 158,168 | + +So every record's declared input frame equals the role's current frame at all 20,991 transitions, the +schedule is legal, and the **frozen base program's** paid histogram — the invoice's **D** — is *counted +off its trace* rather than read from a profile. That profile is then **reused here as an inherited +input**: this package does not encode the 259-gate chain into the native event stream, so the chain's +own D is not derived here and must not be described as such. Ranks 1..5 are the invoice profile; the `8:8` are the eight owned C₀ centre +jobs the invoice charges separately. As a control, the lineage's own word +(the word frozen in `research/warp-interface-20261022/`, payload `4409d2d9…`) runs through the same code and derives its own declared +profile `{1:2201, 2:412, 3:506, 4:135, 5:36, 8:8}` — a different variant, so the derivation is not +tuned to this word. + +The specification excludes amplitudes, Clifford phases and the symbolic endpoint algebra +(`NativeCore.lean` says so), so this proves the frame and tariff semantics; the operator side rests on +`P19_LOWERING.json` and the lifting lemma. + +## Unconditional here, conditional there + +Established: the finite controller arithmetic; the trace identity; the adapter-bearing replay on +the tested states; the 77-recoding census; the invoice and root arithmetic with the outer ledger; +the adapters stay in the inherited unit; the helper-profile mismatch and the Option-A reuse are +recorded; **the diagonal target census equals the invoiced census**. + +The inherited producer/compiler contract admits this finite p=19 unit composition with the +recorded native lowering, endpoint, field-state, ownership, precision, helper, fixed-tape, +compiler-schedule, hosting, and review interfaces. + +**Recorded finding, not hidden**: `P19_PRECOMPILATION.json` reports +`FINDING_PRECOMPILATION_CONTRACT_MISSING` — there is no serialized chain-to-event compiler in the +repository, so the single inherited premise cannot be discharged here. The macro, forward, reverse and +resource receipts are formal owned-work and operator checks; they are not serialized native event +programs, and none of them is presented as a compiler. + +## Reproduce + +```sh +python3 -B research/coded-reverse-word-p19/p19_diagcensus.py --p19 # the census, expensive half +python3 -B research/coded-reverse-word-p19/p19_diagcensus.py # the census, p=3,4,5,8 +python3 -B research/coded-reverse-word-p19/p19_targets.py # the base definition, applied +python3 -B research/coded-reverse-word-p19/p19_units.py # unit composition, endpoint typing +python3 -B research/coded-reverse-word-p19/p19_lift.py # operator-level lemma +python3 -B research/coded-reverse-word-p19/p19_bridge.py # inherited unit, pricer dependence +python3 -B research/coded-reverse-word-p19/p19_word.py # the priced chain (~4 min) +python3 -B research/coded-reverse-word-p19/p19_claim.py +python3 -B research/coded-reverse-word-p19/p19_gates.py # every acceptance gate in one table +python3 -B research/coded-reverse-word-p19/verify.py +python3.12 -B scripts/research_package.py --package research/coded-reverse-word-p19 +``` + +## Open next questions + +- Is a p=19 chain of the inherited unit admissible at the same profiles? +- Do the producer-side compiler schedules carry over to a 19-stage chain unchanged? +- Is the diagonal-target reading of the census the one the base intends? It is the only reading + under which the invoice's numbers are derivable from the word at all five tested sizes. + +## Credit + +The coded producer, the native word, the helper construction and the compiler lineage are +predecessor work; this package adds the p19 chain, the census measurement on the diagonal, and the +conditional κ candidate. New work is Apache-2.0. diff --git a/research/kappa-architecture-frontier/inputs/round3-proof.md b/research/kappa-architecture-frontier/inputs/round3-proof.md new file mode 100644 index 0000000000..92b6fc3c7c --- /dev/null +++ b/research/kappa-architecture-frontier/inputs/round3-proof.md @@ -0,0 +1,211 @@ +# A ceiling for every thinning of the retained paired-path moment + +Prepared for Cinna Davis with substantial OpenAI Codex assistance. Apache-2.0. + +## Scope and conclusion + +Freeze Cao Yifan's PR4610 round-three profile at +`1eb8da6cfb35512c0cc2533413e5ca42f48e13c6`: + +``` +H = {4:28, 7:7, 8:47, 9:326} +P = {1:2201, 2:412, 3:510, 4:127, 5:40, 8:8}. +``` + +There are 112 ports, fresh block width 8, and one paid rank-one query per +port at each thin stage. Keep the predecessor's paired-path scalar word, +all its middle idle windows, a prefix of initial idle windows and the +complementary suffix of terminal idle windows. Allow **every** pair count +`p>=1`, every split `a+b=p-1`, and every binary subset of the `2p+1` full +stages. Specialize every removed stage multiplier to the identity in both +the idle words and the advertised main targets. Keep all productive helper +losses, paid native jobs, owned centres and thin queries. + +Under this retained endpoint/invoice contract, no such word has positive +raw surplus at any saving `0.0030217759 <= C < 1`. The p16, a7/a8 word +has positive surplus at `C=0.0030217758`. Thus the best raw crossing is +in that interval of width `10^-10`; p16 with the existing alternating +full-stage pattern attains it. This is an infinite-family **moment theorem**, +not a new operator-admission theorem or a global barrier for other words. + +The endpoint pattern is an explicit hypothesis inherited from the path +construction: one pair has all stage factors; the other pairs have the +successive prefix or suffix factors below. We do not infer a new universal +native/phase identity from finite tests. The verifier independently checks +the literal source's exact rational projectors and the complete formula +for every split and stage subset through p5. Those tests bind the stated +contract to the retained examples; the reductions and calculus below are +the infinite part of the theorem. + +## 1. Arbitrary-mask formula + +Fix `0=0`, by subadditivity of x^t. This includes +equality when c=0. + +**Remove an empty pair.** For `(0,0)` remove that window and its two +thin stages. Its contribution is `g(c)=h(c)-f(c)<=1`, including g(0)=1. +The query saving is 224, so the surplus gain is `224(1-g(c))>=0`. +The side length and p each decrease by one; no full stage or helper is lost. + +**Split a double-full pair.** Replace `(1,1)` by two successive `(1,0)` +pairs, adding one window and two stages, with k unchanged. The extra thin +query charge is 224. The surplus gain divided by 224 is + +``` +h(c+1) - f(c+2) + f(1) - 1 + = (8^t-1) - [(8(c+2))^t-(8(c+1)+1)^t] > 0. +``` + +Both differences on the right integrate the strictly decreasing derivative +`t*x^(t-1)` over an interval of length 7. The first interval starts at 1; +the second starts at `8(c+1)+1>=9`. This proves strict positivity. + +Apply the first move to even-only pairs and split every double-full pair. +Then remove all empty pairs. The process terminates with only `(1,0)` +pairs. It preserves the three separate bits `l=s_0`, `r=s_(2p)`, and m +at the intervening odd stage, each in {0,1}. Splitting may increase p; +no finite pair-count cutoff is used. + +## 3. Eight concave sequences replace the infinite mask search + +Write `S=a+b`, `B=l+r+m`, `k=S+B`, and `g(j)=h(j)-f(j)`. +For a normalized mask, + +``` +F(S,a,b;l,r,m) = k A(t) + + 224 [h(k) + sum_(j=1)^a g(l+j) + sum_(j=1)^b g(r+j)] + - 112(2S+3-k). +``` + +The positive sequence g(j) is strictly decreasing for integer j>=1. +For fixed S and bits, the largest side sum is obtained by merging the +two decreasing lists `g(l+1),g(l+2),...` and `g(r+1),g(r+2),...`, taking +their S largest terms. This uses only integer argument order, not floating +comparisons. Let their sum be G(S). + +For each of the eight bit triples, the resulting upper envelope has increment + +``` +F(S+1)-F(S) = A(t)-112 + +224 [h(S+B+1)-h(S+B) + (G(S+1)-G(S))]. +``` + +The h increment strictly decreases and the next merged g term never increases. +Thus F is strictly discretely concave. A strict positive preceding increment +and strict negative following increment certify its unique integer maximum +over **all S>=0**. No tail search or unexplored large-p assumption remains. + +At `C=0.0030217759` the exact interval certificate gives: + +| l,r,m | Maximizing S | Upper bound for F | +|---|---:|---:| +| 0,0,0 | 18 | -7.78098 | +| 1,0,0 | 17 | -5.66497 | +| 0,1,0 | 17 | -5.66497 | +| 1,1,0 | 16 | -3.54895 | +| 0,0,1 | 17 | -4.23203 | +| 1,0,1 | 16 | -2.11602 | +| 0,1,1 | 16 | -2.11602 | +| 1,1,1 | 15 | -0.00000722 | + +Displayed bounds are rounded upward; exact outward enclosures and adjacent +increments are in RESULT.json. All eight maxima are strictly negative. +For bits (1,1,1), S=15 means p=16, with sides 7 and 8 in either order. +Its surplus is strictly positive at the stated lower endpoint. + +## 4. Exclude every larger C, rather than only one sampled exponent + +Let `L(t)=P(t)-H(t)`. Its derivative divided by 9^t is + +``` +sum_(r=2,3,4,5) n_r (r/9)^t log r + - 7(7/9)^t log 7 - 39(8/9)^t log 8 - 326 log 9, +n_2=412, n_3=510, n_4=99, n_5=40. +``` + +For `1/4<=t<=1`, upper-bound the positive terms at t=1/4 and +upper-bound each negative term at t=1. The exact resulting bound is below +`-9.53`. Hence L strictly decreases on this whole interval. Each h(k) +increases in t; so does each g(j), since `x^t log x` increases in x>=1. +Consequently every normalized F increases in t on [1/4,1]. Negativity +at `t=1-0.0030217759` excludes all smaller t down to 1/4. + +For `0=3298 and H(t)<=2*408, since `9^(1/4)<2`. +Thus L(t)>=2482. Concavity gives `h(k)<=1+8kt` and `g(j)<=t` +for integer j>=1. Therefore every normalized surplus satisfies + +``` +F <= -112 + k(112+1792t-2482) + 224S(t-1) < 0. +``` + +This also covers k=S=0. Combining the two ranges and the dominance +reduction excludes every `0.0030217759<=C<1` in the stated family. + +## 5. Even free owned centres do not reach C=0.01 + +As an explicitly unrealized optimistic relaxation, remove all eight paid +rank-eight owned-centre jobs, keeping every other charge and target. The +same dominance proof applies. The local derivative L' becomes still smaller, +and the small-t lower bound becomes 2474, which still exceeds 560. + +Reoptimizing **all** pair counts, splits and thinning masks, rather than +keeping p16, puts the best relaxed crossing in +`(0.0080596238,0.0080596239)`, at p5 with both side lengths 2 and all three +separate flags full. The eight maximizing S values at the upper endpoint, +in the bit order used above, are `7,6,6,5,6,5,5,4`; all maxima are strictly +negative, and their adjacent differences have the required strict signs. +The p5 surplus is positive at the lower endpoint. Exact certificates are +in RESULT.json. The same monotonicity and small-t argument excludes every +larger C<1 in this relaxed family. + +Thus even deleting the entire owned-centre bill cannot reach C=0.01 by +retuning this path. A C>=0.01 attack needs another changed hypothesis. +This is a planning obstruction, not an implementation of free centres. + +## Implication and limits + +The existing p16 allocation already attains this family's best raw crossing +with the frozen round-three inventory. More pair counts, asymmetric splits, +partial thinning, or mixtures of even and odd full stages cannot beat it. +The scope does not cover changed idle masks outside the prefix/suffix contract, +changed scalar words, nonbinary replacements, altered queries, different local +profiles, noncommuting stage actions, or a different supplier interface. + +No new kappa, selected-frontier change, BIT improvement, compiler admission, +absolute-phase proof, physical implementation or multiplication theorem follows. +The remaining productive direction is to change one of those hypotheses. +Credit Cao Yifan and the source's full PR4470/native/controller lineage, +including Cinna Davis, zxv, Jacob Alan Sussman and the retained predecessors. diff --git a/research/kappa-architecture-frontier/inputs/selected-claim.json b/research/kappa-architecture-frontier/inputs/selected-claim.json new file mode 100644 index 0000000000..b2b7e3edb5 --- /dev/null +++ b/research/kappa-architecture-frontier/inputs/selected-claim.json @@ -0,0 +1,33 @@ +{ + "schema": "proposed-conditional-integer-multiplication-claim/1", + "kappa": "605457647/200000000000", + "source_result": "research/coupled-helper-neutral-completion/reports/expected/funding.json", + "uniform_templates": [ + { + "family": "complex", + "rank_encoding": "2^38569300000000000", + "saving": "4238203541/1400000000000" + }, + { + "family": "BIT before cover", + "rank_encoding": "2^25986965159937", + "saving": "3459/1000000" + } + ], + "ordinary_BIT_saving": "8590884599/2500000000000", + "admitted_BIT_saving": "17/5000", + "nine_outer_savings": { + "boundary_algebraic_matrix": "593348495179152359293/196000000000000000000000", + "fused_gaussian": "593348495177457077879/196000000000000000000000", + "global_coordinate_router": "4238203537/1400000000000", + "group_bit_router": "2966742477287285389389/980000000000000000000000", + "group_scans": "349999999999/350000000000", + "main_transform": "593348494899152359293/196000000000000000000000", + "microbox_face_corrections": "13475000000001/175000000000", + "polynomial_products": "699999999999/700000000000", + "sparse_union_movement": "80218348495179152359293/196000000000000000000000" + }, + "limiting_outer_saving": "593348494899152359293/196000000000000000000000", + "strict_limiting_slack": "839152359293/196000000000000000000000", + "scope": "Maintainer-reviewed conditional PR5413 complete neutral caller, with PR5407 provider and PR5414 companion audits. The five selected framework assumptions are unchanged. Uniform words are not materialized." +} diff --git a/research/kappa-architecture-frontier/inputs/selected.json b/research/kappa-architecture-frontier/inputs/selected.json new file mode 100644 index 0000000000..fc3d4ba105 --- /dev/null +++ b/research/kappa-architecture-frontier/inputs/selected.json @@ -0,0 +1,103 @@ +{ + "status": "Selected maintainer-reviewed conditional PR5413 completion, with PR5407 provider and PR5414 companion audits and explicit inherited foundation reuse", + "kappa": "605457647/200000000000", + "decimal": "0.003027288235", + "source_prs": [ + 5413, + 5414, + 5402, + 5407, + 5398, + 5400, + 4610, + 5241, + 4470, + 4447, + 4441, + 4440, + 4416, + 4433, + 4359, + 4268, + 3945, + 4085, + 2979, + 4076, + 4088, + 1673, + 1758, + 1786, + 23, + 555, + 589 + ], + "source_manifest": "certificates/frontier5413-source.json", + "certificate": "certificates/frontier5413/CLAIM.json", + "certificate_sha256": "344a955984f2daee912592d63810af9e7c8e61771b871c77a25b5b8c76809694", + "proof": "docs/research/pr-intake-evidence/pr5413-promotion/PROMOTION.md", + "proof_supplements": { + "notes/batched-bit-rows.tex": "ef72c0ead19373cbc19c8a3aacb44dd0f75353ee5f4d055f775a986a4878022c", + "notes/batched-complex-rows.tex": "64c70926a8705874f1c9b42a2f703e42cad4e90f927f544458cfdf729540236c", + "notes/compact-control-movement.tex": "b963c3d2f4e1b7059aa289bb4b4ac89b688920bcf42f5b20d7698cdef0132cc6", + "notes/general-clifford-frames.tex": "c9bb9655b594583c6b4bab8cb485233f1d1e588f83858cf1e4c3530cee8fed54", + "notes/stopped-product-complex.tex": "4738089103a4b263b3b0ef458f5ef35519c696f1ea871ae79e508d3720f5870a", + "notes/three-stage-cover-bit.tex": "47123a756f823c83a0d48cca2bf5add6472cd88410b13aed345e70c8834fb511", + "notes/three-stage-cover-rows.tex": "6ad97a5cd7d6aecf978a81226e1c2763d37840caca130c61f3bf5c4ac111c5c8", + "references/semantic-bulk/pr23/semantic-bulk-17-note.tex": "652242b05174bb776ffc6165af170df9c8cf220dbd0fc26c24d778f320dbabc8", + "research/e8-bit-carrier-skeleton/code/bit/export_records.py": "8a5999601f917dbb492bb9ae9a344611f18cc7cedc53dc3c76496a369e530eb3", + "research/e8-bit-carrier-skeleton/code/nine/geometry.py": "36eeda3184bd009e89462b65c8725d10860c444f8da8f1f87e5f6e50120011ca", + "research/e8-bit-p111-tuned/code/gen_p3.py": "438b83f10d70ceca7cf78049420204b7de2dc61682f913c50a62596106ad84cd", + "research/e8-bit-p111-tuned/code/xcheck_p.py": "af3decc877e27c00001cf56f50c6c09566e8e101297ab34c7860aed96a06d80e", + "research/e8-bit-p111-tuned/tune/EXPECTED.json": "b9f0e5ca038abe837b0007c8fe006f366a6f02009244ac57705a8a200e2301f4", + "research/e8-bit-p111-tuned/tune/apply.py": "806ae4cb2648e4f05dcf56bd089891fd3ba33a6ee5fe76d3329e322c6770c1a1", + "research/e8-bit-p111-tuned/tune/wlib.py": "a37fdf3cdf5f62945c2a90193401c0e9edc9dd3cda8d8cb36a3b9c329ebe4dbc", + "research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962", + "docs/research/pr-intake-evidence/pr4359/PROOF-REVIEW.md": "7d67bb814285f7634029fbd378c6457156545f0b38858cc1c6ec34b68cd9d162", + "docs/research/pr-intake-evidence/pr4470/PROOF-REVIEW.md": "5c111dd56beb53dc44ab727d96e1af03aaf50f3023d4342e2b0a89ede6cf585b", + "docs/research/pr-intake-evidence/pr4416/PROOF-REVIEW.md": "2c2bbe6fe1bab44778192118f27e59a0d23dbe02c47aa8a42845093f1ce46f49", + "docs/research/pr-intake-evidence/pr4610/PROOF-REVIEW.md": "b84f833e3072cbab372fbda2ece98fbc031c15e590cf73003ddea35a5222e148", + "research/final4610-independent-admission/PROOF.md": "e573cbbe6fa5481c0533e773de404e10f4dc7907b5ebfe404bdcd02dcf9844d8", + "research/final4610-independent-admission/SPECIALIZATION.md": "70430114f744108223bc1d44b98bc25b696c4b408b7b044c2a8bbdfdb434ac5c", + "docs/research/pr-intake-evidence/pr5413-promotion/PROMOTION.md": "9419931de95e317f5e08ffa98c86e069836b53f6438c2f413b0722377819aa44", + "docs/research/pr-intake-evidence/pr5413/PROOF-REVIEW.md": "1edba0567d35b099e67d5503cf335d5d143782b5cf4c1e4f98fc2d620ed4c644", + "research/coupled-helper-neutral-completion/reports/proofs/NEUTRAL-PROOF-v16c.md": "dca94625cd0d49de6b81e4a7dd4108b8b6f711e90496d9116806242d30b35737", + "research/coupled-helper-neutral-completion/reports/proofs/WHOLECALLER-COMPLETION-THEOREM.md": "ecefd9b890ccaa46e9f00a6e43faf16aaaf8ec8c992ab48bf245af38aa3e3f23", + "research/coupled-helper-neutral-completion/reports/proofs/V16-APPLICATION-PROOF-v3.md": "cda8f596f7854f42a228f757d5f8e68f6b2256a19c5ae3771fb40753cedc5b39" + }, + "review": "docs/research/pr-intake-evidence/pr5413-promotion/PROMOTION.md", + "validation": "docs/research/pr-intake-evidence/pr5413-promotion/VALIDATION.json", + "integration": "docs/research/pr-intake-evidence/pr5413-promotion/INTEGRATION.json", + "reproduce": "make frontier5413-verify", + "scope": "Maintainer-reviewed conditional PR5413 complete neutral caller, with PR5407 provider and PR5414 companion audits. The five selected framework assumptions are unchanged. Uniform words are not materialized.", + "previous_kappa": "15108879/5000000000", + "previous_record": "certificates/checkpoints/frontier4610.json", + "audited_source_head": "0c1fa2f47fb5ea17b93a4b67063d08e49cc38e51", + "source_certificate": "research/coupled-helper-neutral-completion/reports/expected/funding.json", + "source_certificate_sha256": "70ab7d13548962097ad83ad393b8482f52e827b8996869011ce6d071146bd3eb", + "replay_mode": "Fresh serial provider, primary eight-engine and companion replay in a closed export; source-bound PR4610 foundation reuse; explicit Darwin resource adapter where needed", + "contributors": "docs/research/community-neutral5413-contributors.md", + "assumptions": [ + { + "id": "native_all_columns", + "statement": "Retained native operators, phase conventions, spectators and whole-job adapters work at every positive column multiplicity." + }, + { + "id": "owned_erasure", + "statement": "Owned streams and suspended centers obey the retained allocation, erasure and ownership contracts." + }, + { + "id": "compiler", + "statement": "The finite mixed-target compiler and chronological product, completion and splitting satisfy the retained uniform closure contract." + }, + { + "id": "precision_tape", + "statement": "Retained fixed-tape movement and precision/storage prescriptions apply to the new fixed finite template." + }, + { + "id": "analytic_recovery", + "statement": "Analytic decomposition, fine-prime avoidance and exact integer recovery follow the retained upstream/outer framework." + } + ], + "audit_pr": 5414, + "audit_head": "bc37fb01c58d20e799d3299dec63e654f67d9d1b" +} diff --git a/research/kappa-architecture-frontier/verify.py b/research/kappa-architecture-frontier/verify.py new file mode 100644 index 0000000000..a9137e3bdf --- /dev/null +++ b/research/kappa-architecture-frontier/verify.py @@ -0,0 +1,430 @@ +#!/usr/bin/env python3 +"""Exact architectural price gates; no native supplier or outer replay. +Prepared for zxv with substantial OpenAI Codex assistance. Apache-2.0. +Exchange/convexity predecessors: Ali Romman, Cinna Davis and Chris R. +""" +from collections import Counter +from fractions import Fraction as F +from functools import lru_cache +from hashlib import sha256, sha1 +from itertools import product +from math import factorial +from pathlib import Path +import argparse +import base64 +import json +import zlib + +ROOT = Path(__file__).resolve().parent +Q = 1 << 224 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def ceildiv(a, b): + return -((-a) // b) + + +class I: + """Closed interval of integers divided by Q, with directed rounding.""" + def __init__(self, lo, hi=None): + self.lo, self.hi = lo, lo if hi is None else hi + require(self.lo <= self.hi, 'reversed interval') + + @staticmethod + def of(x): + if isinstance(x, I): + return x + x = F(x) + return I(x.numerator * Q // x.denominator, + ceildiv(x.numerator * Q, x.denominator)) + + def __add__(self, other): + o = I.of(other) + return I(self.lo + o.lo, self.hi + o.hi) + __radd__ = __add__ + + def __neg__(self): + return I(-self.hi, -self.lo) + + def __sub__(self, other): + return self + (-I.of(other)) + + def __rsub__(self, other): + return I.of(other) - self + + def __mul__(self, other): + o = I.of(other) + products = [a*b for a in (self.lo,self.hi) for b in (o.lo,o.hi)] + return I(min(products)//Q, ceildiv(max(products),Q)) + __rmul__ = __mul__ + + def __truediv__(self, n): + require(type(n) is int and n > 0, 'positive integer divisor required') + return I(self.lo//n, ceildiv(self.hi,n)) + + def positive(self): + return self.lo > 0 + + def negative(self): + return self.hi < 0 + + def contains_zero(self): + return self.lo <= 0 <= self.hi + + def json(self): + return {'lower':str(F(self.lo,Q)), 'upper':str(F(self.hi,Q))} + + +def log_series(z): + """2 atanh(z), 0<=z<=1/3; rational remainder after 96 terms.""" + require(0 <= z <= F(1,3), 'log series domain') + x = I.of(z) + x2 = x*x + term, total = x, I.of(0) + for j in range(96): + total += term/(2*j+1) + term = term*x2 + tail = 2*z**193/(193*(1-z*z)) + return 2*total + I(0,ceildiv(tail.numerator*Q,tail.denominator)) + + +@lru_cache(None) +def log_int(n): + require(type(n) is int and n > 0, 'positive log input') + k = n.bit_length()-1 + return k*log_series(F(1,3)) + log_series(F(n-2**k,n+2**k)) + + +def exp_positive(x): + require(x.lo >= 0 and x.hi <= 16*Q, 'exp domain') + y = x/16 + term, total = I.of(1), I.of(1) + for j in range(1,65): + term = (term*y)/j + total += term + # y<=1: tail <= 1/65! * sum_(k>=0) (1/66)^k. + tail = F(66,65*factorial(65)) + total += I(0,ceildiv(tail.numerator*Q,tail.denominator)) + for _ in range(4): + total = total*total + return total + + +@lru_cache(None) +def power(r,t): + require(type(r) is int and r >= 0 and 0 <= t <= 1, 'power domain') + if r == 0: + require(t > 0, 'zero to zero excluded') + return I.of(0) + if t == 0 or r == 1: + return I.of(1) + if t == 1: + return I.of(r) + return exp_positive(log_int(r)*t) + + +def moment(hist,t): + return sum((w*power(r,t) for r,w in hist.items()),I.of(0)) + + +def clean(hist): + return {int(k):v for k,v in hist.items() if v} + + +def canonical(n,v,paid,helpers,b=8): + """Complete attained minimum at fixed FULL count, including n=0,1,2.""" + P = Counter({r:n*w for r,w in paid.items()}) + T = Counter({r:n*w for r,w in helpers.items()}) + T[1+b*n] += 2*v + if n < 3: + P[1] += v*(3-n) + else: + P[1] += v*(n-3) + a = (n-3)//2 + for length in (a,n-3-a): + for k in range(2,length+2): + P[b*k] += 2*v + T[1+b*k] += 2*v + return clean(P),clean(T) + + +def cost(profile,n,C): + p,h = canonical(n,*profile) + return moment(p,1-C)-moment(h,1-C) + + +def derivative_gate(profile,b=8): + """Upper bound on d/dt [L(t)/b^t] throughout 0 b: + U += F(w*r,b)*(log_int(r)-log_int(b)) + for r,w in H.items(): + if r < b: + U += w*(log_int(b)-log_int(r)) + require(U.negative(),'local monotonicity not certified') + return U + + +def gate(profile,C,n): + x = cost(profile,n,C) + before = x-cost(profile,n-1,C) + after = cost(profile,n+1,C)-x + require(x.positive() and before.negative() and after.positive(), + 'all-n exclusion gate failed') + return {'C':str(C),'minimizing_full_count':n,'minimum':x.json(), + 'previous_difference':before.json(),'next_difference':after.json()} + + +def ratio_gate(profile,C,n): + # J_j=j*C_(j+1)-(j+1)*C_j. Strict convexity makes J strictly increasing. + x = cost(profile,n,C) + before = (n-1)*x-n*cost(profile,n-1,C) + after = n*cost(profile,n+1,C)-(n+1)*x + require(before.negative() and after.positive(),'all-n discount gate failed') + return {'C':str(C),'minimizing_full_count':n,'discount':(x/n).json(), + 'previous_ratio_numerator':before.json(),'next_ratio_numerator':after.json()} + + +def authenticate(): + origins = json.loads((ROOT/'ORIGINS.json').read_text()) + objects = {} + for oid,record in origins['objects'].items(): + decoder = zlib.decompressobj() + raw = decoder.decompress(base64.b64decode(record['zlib_base64']),2**20+1) + require(len(raw) <= 2**20 and decoder.eof and not decoder.unused_data, + 'origin object size or stream') + kind = record['type'] + require(kind in ('tree','commit'),'origin object type') + header = (kind+' '+str(len(raw))+'\0').encode() + require(sha1(header+raw).hexdigest() == oid,'origin object hash') + objects[oid] = (kind,raw) + def obj(oid,kind): + require(oid in objects and objects[oid][0] == kind,'missing origin object') + return objects[oid][1] + def edge(tree,name): + raw = obj(tree,'tree') + offset = 0 + matches = [] + while offset < len(raw): + end = raw.index(b'\0',offset) + mode,label = raw[offset:end].split(b' ',1) + require(end+21 <= len(raw),'truncated origin tree') + if label == name.encode(): + matches.append((mode,raw[end+1:end+21].hex())) + offset = end+21 + require(len(matches) == 1,'origin edge missing or ambiguous') + return matches[0] + for row in origins['files']: + raw = (ROOT/row['retained_path']).read_bytes() + require(sha256(raw).hexdigest() == row['sha256'],'retained source hash') + header = ('blob '+str(len(raw))+'\0').encode() + require(sha1(header+raw).hexdigest() == row['git_blob'],'retained Git blob') + commit = obj(row['commit'],'commit') + first = commit.splitlines()[0] + require(first.startswith(b'tree '),'origin commit root') + tree = first[5:].decode() + parts = row['path'].split('/') + for index,part in enumerate(parts): + mode,tree = edge(tree,part) + require(mode in ((b'100644',b'100755') if index == len(parts)-1 else (b'40000',)), + 'origin edge mode') + require(tree == row['git_blob'],'origin leaf differs') + + +def load_profiles(): + neutral = json.loads((ROOT/'inputs/neutral-invoice.json').read_text()) + profiles = {'neutral5413':(112,clean(neutral['local_paid']), + clean(neutral['local_productive_helpers']))} + for pr in (5544,5545,5551): + d = json.loads((ROOT/f'inputs/p104-{pr}.json').read_text()) + prof = (104,clean(d['local']['paid']),clean(d['local']['helpers'])) + profiles[f'p104_{pr}'] = prof + require(canonical(18,*prof) == (clean(d['complete_cost']['paid']), + clean(d['complete_cost']['targets'])),'P104 source path invoice') + require(canonical(18,*profiles['neutral5413']) == + (clean(neutral['histograms']['paid']),clean(neutral['histograms']['productive'])), + 'neutral source path invoice') + profiles['round3_4610'] = (112,{1:2201,2:412,3:510,4:127,5:40,8:8}, + {4:28,7:7,8:47,9:326}) + source = (ROOT/'inputs/round3-proof.md').read_text() + require('P = {1:2201, 2:412, 3:510, 4:127, 5:40, 8:8}' in source and + 'H = {4:28, 7:7, 8:47, 9:326}' in source,'round3 profile binding') + v,p,h = profiles['neutral5413'] + free_p = dict(p) + require(free_p.pop(8) == 8,'free-centre relaxation source') + profiles['neutral_free_eight_H8'] = (v,free_p,dict(h)) + return profiles + + +def mask_invoice(profile,p,a,bits): + """Literal path equation, separate from canonical implementation.""" + v,paid,helpers = profile + n = sum(bits) + P = Counter({r:n*w for r,w in paid.items()}) + H = Counter({r:n*w for r,w in helpers.items()}) + P[1] += v*(2*p+1-n) + H[1+8*n] += 2*v + for j in range(1,p): + h = sum(bits[:2*j]) if j <= a else sum(bits[2*j+1:]) + e = bits[2*j] + if h: + P[8*h] += 2*v + if e: + P[8] += 2*v + H[1+8*(h+e)] += 2*v + return clean(P),clean(H) + + +def controls(profiles): + require(log_int(1).contains_zero(),'ln 1') + require((log_int(4)-2*log_int(2)).contains_zero(),'log identity') + require((power(9,F(1,2))-3).contains_zero(),'sqrt identity') + require((power(81,F(1,4))-3).contains_zero(),'fourth root identity') + checks = 0 + prof = profiles['p104_5551'] + for t in (F(1,2),F(999,1000)): + for p in range(1,4): + for a in range(p): + for bits in product((0,1),repeat=2*p+1): + P,H = mask_invoice(prof,p,a,bits) + cp,ch = canonical(sum(bits),*prof) + delta = Counter(P) + for hist,sign in ((H,-1),(cp,-1),(ch,1)): + for r,w in hist.items(): + delta[r] += sign*w + delta = clean(delta) + require(not delta or moment(delta,t).positive(), + 'mask dominance control failed') + checks += 1 + for t in (F(1,10),F(1,2),F(999,1000)): + require((power(6,t)-1-power(5,t)).negative(),'H1+H5 -> H6') + delta = 2-3*power(2,t)+power(3,t)-power(4,t)+power(5,t) + require(delta.negative(),'joint contact concavity') + require((power(9,t)-power(8,t)-1).negative(),'completion must be charged') + p,h = canonical(18,*prof) + bad_p = dict(p); bad_p[1] -= 104*15 + require((bad_p,h) != canonical(18,*prof),'missing query not rejected') + bad_h = dict(h); bad_h[9] += 1 + require((p,bad_h) != canonical(18,*prof),'fake helper not rejected') + bad_idle = dict(p); bad_idle.pop(72) + require((bad_idle,h) != canonical(18,*prof),'missing idle not rejected') + try: + gate(prof,F('0.00304153'),18) + except ValueError: + pass + else: + raise ValueError('positive raw witness falsely excluded') + return {'tiny_mask_comparisons':checks,'arithmetic_identities':4, + 'concavity_controls':9,'accounting_controls':3,'false_ceiling_rejected':True} + + +def calculate(): + authenticate() + profiles = load_profiles() + brackets = { + 'round3_4610':('0.00302177587077','0.00302177587079',18), + 'neutral5413':('0.00302728824993','0.00302728824995',18), + 'p104_5544':('0.00304057807630','0.00304057807631',18), + 'p104_5545':('0.00304117181649','0.00304117181650',18), + 'p104_5551':('0.00304153116714','0.00304153116715',18), + 'neutral_free_eight_H8':('0.00807671283977','0.00807671283979',7), + } + result = {'schema':'kappa-architecture-frontier/v1','grid':str(Q), + 'claims_are_raw_moment_bounds':True,'native_or_outer_admission':False, + 'profiles':{},'discounts':{}} + for name,(lo,hi,n) in brackets.items(): + prof = profiles[name] + lower = cost(prof,n,F(lo)) + require(lower.negative(),'lower raw witness failed') + result['profiles'][name] = { + 'ports':prof[0],'paid':prof[1],'helper_targets':prof[2], + 'root_bracket':[lo,hi],'lower_witness':lower.json(), + 'all_n_upper_gate':gate(prof,F(hi),n), + 'all_exponent_derivative_upper':derivative_gate(prof).json(), + 'rank_surplus_per_full':17*prof[0]+sum(r*w for r,w in prof[2].items()) + -sum(r*w for r,w in prof[1].items()), + } + for name in ('neutral5413','p104_5551'): + result['discounts'][name] = [ratio_gate(profiles[name],F(c),n) + for c,n in [('0.0031',18),('0.0033',17),('0.0034',16), + ('0.004',14),('0.006',9),('0.01',5)]] + result['discounts']['neutral_free_eight_H8'] = [ratio_gate( + profiles['neutral_free_eight_H8'],F('0.01'),5)] + claim = json.loads((ROOT/'inputs/selected-claim.json').read_text()) + result['retained_admitted_BIT_budget'] = claim['admitted_BIT_saving'] + result['controls'] = controls(profiles) + return result + + +def price_profile(path,C): + """Optimistic raw filter for a new autonomous rank-eight path provider.""" + d = json.loads(path.read_text()) + require(type(d.get('ports')) is int and 1 <= d['ports'] <= 10**6, + 'ports must be an integer in 1..1000000') + histograms = [] + for key in ('paid','helper_targets'): + require(isinstance(d.get(key),dict),'paid/helper_targets dictionaries required') + hist = {} + for r,w in d[key].items(): + rank = int(r) + require(str(rank) == r and 1 <= rank <= 65536, + 'canonical integer ranks in 1..65536 required') + require(type(w) is int and 0 <= w <= 10**9,'integer multiplicities required') + if w: + hist[rank] = w + histograms.append(hist) + require(0 < C < 1,'saving must lie strictly between zero and one') + prof = (d['ports'],*histograms) + def J(n): + return n*cost(prof,n+1,C)-(n+1)*cost(prof,n,C) + if J(1).positive(): + return {'C':str(C),'minimizing_full_count':1, + 'discount':cost(prof,1,C).json(),'next_ratio_numerator':J(1).json(), + 'scope':'Raw path invoice only; independent helper and main contracts assumed.'} + require(J(1).negative(),'unresolved interval at initial ratio gate') + lo,hi = 1,2 + while J(hi).negative() and hi < 4096: + lo,hi = hi,2*hi + require(J(hi).positive(),'unknown: ratio gate unresolved or beyond 4096 FULLs') + while hi-lo > 1: + mid = (lo+hi)//2 + if J(mid).negative(): + lo = mid + else: + require(J(mid).positive(),'unresolved interval during ratio search') + hi = mid + result = ratio_gate(prof,C,hi) + result['scope'] = 'Raw path invoice only; independent helper and main contracts assumed.' + return result + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument('--write',type=Path,help='write a new receipt without overwriting') + parser.add_argument('--price',type=Path,help='JSON with ports, paid, helper_targets; assumes the path contract') + parser.add_argument('--C',type=F,help='exact candidate supplier saving for --price') + args = parser.parse_args() + if args.price: + require(args.C is not None and args.write is None,'--price requires --C and excludes --write') + print(json.dumps(price_profile(args.price,args.C),sort_keys=True,indent=2)) + return + require(args.C is None,'--C requires --price') + result = calculate() + encoded = json.dumps(result,sort_keys=True,indent=2)+'\n' + if args.write: + require(not args.write.exists(),'refusing to overwrite receipt') + args.write.write_text(encoded) + else: + require(json.loads(encoded) == json.loads((ROOT/'RESULT.json').read_text()), + 'fresh scientific result differs') + print('PASS_KAPPA_ARCHITECTURE_FRONTIER: six all-n ceilings, thirteen price gates, finite controls') + + +if __name__ == '__main__': + main()