From 1a623ad2c268b2b23878bc0cc3cf0f67b4b1b5fa Mon Sep 17 00:00:00 2001 From: Dillon Date: Wed, 21 Oct 2026 23:55:09 -0400 Subject: [PATCH 1/4] Prove adaptive gates and leaf bounds at exact moment crossings --- research/adaptive-gate-existence/PROOF.md | 585 ++++++++++++++++++ research/adaptive-gate-existence/README.md | 176 ++++++ research/adaptive-gate-existence/SOURCES.json | 54 ++ research/adaptive-gate-existence/TASK.json | 141 +++++ .../adaptive-gate-existence/VALIDATION.md | 66 ++ research/adaptive-gate-existence/VERIFY.json | 27 + research/adaptive-gate-existence/WITNESS.json | 16 + .../root_application.py | 365 +++++++++++ research/adaptive-gate-existence/verify.py | 338 ++++++++++ 9 files changed, 1768 insertions(+) create mode 100644 research/adaptive-gate-existence/PROOF.md create mode 100644 research/adaptive-gate-existence/README.md create mode 100644 research/adaptive-gate-existence/SOURCES.json create mode 100644 research/adaptive-gate-existence/TASK.json create mode 100644 research/adaptive-gate-existence/VALIDATION.md create mode 100644 research/adaptive-gate-existence/VERIFY.json create mode 100644 research/adaptive-gate-existence/WITNESS.json create mode 100644 research/adaptive-gate-existence/root_application.py create mode 100644 research/adaptive-gate-existence/verify.py diff --git a/research/adaptive-gate-existence/PROOF.md b/research/adaptive-gate-existence/PROOF.md new file mode 100644 index 0000000000..bdf142f26d --- /dev/null +++ b/research/adaptive-gate-existence/PROOF.md @@ -0,0 +1,585 @@ +# A sufficient profile criterion for adaptive compiler gates + +This note proves a sufficient existence criterion for the adaptive compiler +of zxv's [PR #4483](https://github.com/CrocSwap/integer-mult-bounds/pull/4483), +at source head `fb0c208864e6b24e3473318a058aa5b2dbd5764b`. Its new conclusion +is that a moment crossing and strict pointwise mirror capacity imply the +compiler's tail gates. The mirror condition itself supplies the strict +tilted-mean gap and makes the crossing simple. The hypotheses also imply +a fully funded majorant at the crossing exponent, with a logarithmic factor. +The criterion is sufficient; necessity or admission of every favorable +moment profile is not claimed. + +The arbitrary-height integer flow, its cancellation identities, and its +shifted-logarithmic majorant are predecessor results, used conditionally +here. Their native and physical implementation premises remain premises. +This note supplies neither a new native profile nor a new multiplication +exponent. The accompanying finite checks illustrate the hypotheses and +reject a tempting weaker criterion; they do not prove the theorem below. + +## 1. Profiles and the exact boundary hypothesis + +Let nonempty finite histograms `W_k` and `P_r` have positive integer coefficients, +with target ranks `2 <= k <= m`, where `m` is their maximum, and paid ranks +`1 <= r < m`. Define, for every real `t`, + +```text +T(t) = sum_k W_k k^t, P(t) = sum_r P_r r^t, +mu_T(t) = T'(t)/T(t), mu_P(t) = P'(t)/P(t), +q(t) = T(t)/P(t), eta(t) = t m^(t-1). +``` + +All these moment functions are smooth where used. A native paid position +is still a separate chronological position when another position has the +same rank. The histogram specifies its multiplicity; it does not authorize +pooling unfinished calls or aliasing owners. + +Use the finite mirror cells from #4483, section 2. For a pair `(r,k)`, the +exit window is `(1/r,1/k]` when `r>k`, and the inner-source window is +`(1/k,1/r]` when `k>r`. Its coefficient is `P_r W_k (rk)^t`. +Partition at all endpoints, with the indicated endpoint conventions, and +let `E_J(t)` and `S_J(t)` be the respective coefficient sums on cell `J`. +The partition is finite and does not depend on `t`. + +The **strict mirror hypothesis at t_*** means there is a number `beta_*` +such that + +```text +0 <= beta_* < eta(t_*), +E_J(t_*) <= beta_* S_J(t_*) for every cell J. (1) +``` + +In particular, a cell with zero source coefficient must have zero exit +coefficient. Every coefficient is a positive multiple of a positive +exponential. Thus either a cell's sum is identically zero, or it is positive +for every real exponent. Consequently (1) persists, with a slightly larger +factor, on a sufficiently small interval of exponents. This is a pointwise +mirror condition, not an assertion inferred from finitely sampled flows. + +### 1.1 Mirror slack supplies the mean gap and rank-one surplus + +Write `S_t(z)` and `E_t(z)` for these piecewise constant coefficient +functions, extended by zero outside their finitely many windows. Their +support lies in a compact interval bounded away from zero. For `k>r`, +the integral of `dz/z` over its source window is `log(k/r)`; for `r>k`, +subtracting the exit window gives that same signed value. Hence + +```text +integral_0^infinity [S_t(z)-E_t(z)] dz/z + = sum_(r,k) P_r W_k (rk)^t log(k/r) + = P(t) T'(t)-T(t) P'(t) + = P(t) T(t) [mu_T(t)-mu_P(t)]. +``` + +Whenever `E_t<=beta S_t` pointwise with `beta<1`, the left side is +strictly positive: every paid rank is below `m`, so a pair with target +rank `m` supplies a source window of positive length. Therefore strict +mirror slack implies `mu_T(t)>mu_P(t)`. In particular (1), with +`eta(t_*)<1`, supplies the mean gap at the crossing automatically. + +There is also positive rank-one surplus. For `00`. Thus neither the tilted-mean gap nor positive rank-one +surplus needs an additional hypothesis. These integral identities are +exact finite sums; they do not estimate the distribution of a flow. + +## 2. Existence theorem + +**Theorem.** Suppose the native profile and the conditional finite compiler +contracts of #4483 apply. Suppose that for some `t_*` in `(0,1)`, + +```text +T(t_*) = P(t_*), (2) +``` + +and the strict mirror hypothesis (1) holds. Put +`delta_* := mu_T(t_*)-mu_P(t_*)`, which is positive by section 1.1. +Then there exist positive integers `a,b`, an integer `M>1`, positive rational +numbers `s,lambda`, +and a number `epsilon>0`, with `t_*+epsilon<1`, for which all of #4483's +two-tail and ratio-ordering gates hold uniformly on +`[t_*, t_*+epsilon]`. + +More precisely, with `g=a+b`, there are constants + +```text +0 < U,V < 1, Q >= 1, d > 0, +0 <= beta_bar < eta_* := eta(t_*), +``` + +such that throughout that interval, + +```text +u(t) := M^(-s) [T(t+s)/T(t)]^a [P(t+s)/P(t)]^b <= U, +v(t) := M^lambda [T(t-lambda)/P(t)]^g <= V, +T(t+s)/T(t) >= P(t+s)/P(t), +d/dt log q(t) >= d, q(t) <= Q, +E_J(t) <= beta_bar S_J(t) for every mirror cell J, +eta(t) >= eta_* > beta_bar. (3) +``` + +There also exist `p,c,A>0` and an integer base cutoff `n0` such that the +normalized rank-one leaf cost of the resulting finite compiler satisfies + +```text +L(0)=0, +L(n) <= A n^t_* (c+log n)^p for every integer n>=1. (4) +``` + +The compiler uses elementary evaluation through `n0` and height +`G=g floor(log_M(floor(n/m)))` above `n0`. In particular, for every +`z>t_*`, it has `L(N)<=N^z` at all sufficiently large integer ranks `N`. +This is a statement about normalized leaf counts under the inherited +contracts; productive width and physical constants are not estimated here. +The theorem is existential given its hypotheses. An executable application +must certify the chosen root, or isolate its simple crossing and bound the +needed expressions on a certified interval, before it can extract numerical +constants. No algorithm for an unspecified real parameter is claimed. + +### 2.1 Integer height parameters exist + +Write `mu_P*=mu_P(t_*)` and `mu_T*=mu_T(t_*)`. Choose an integer `g>=2` +large enough that + +```text +(g-1) delta_* / log 2 > 1. +``` + +The open interval + +```text +((g mu_P* + delta_*)/log 2, g mu_T*/log 2) +``` + +has length greater than one, so it contains an integer `j`. Its lower +endpoint is positive because `mu_P*>=0` and `delta_*>0`; hence `j>=1`. +Set + +```text +a=1, b=g-1, M=2^j, h=(log M)/g. +``` + +Then both required geometric inequalities are strict: + +```text +(a mu_T* + b mu_P*)/g < h < mu_T*. (5) +``` + +This proves existence within integer height parameters. No continuously +chosen height is substituted for an integer compiler. + +### 2.2 The two tails and ratio ordering + +At the crossing exponent define + +```text +phi(s) = -s log M + +a log[T(t_*+s)/T(t_*)] + +b log[P(t_*+s)/P(t_*)]. +``` + +We have `phi(0)=0` and, by (5), + +```text +phi'(0) = -log M+a mu_T*+b mu_P* < 0. +``` + +Also define + +```text +chi(s) = log[T(t_*+s)/T(t_*)]-log[P(t_*+s)/P(t_*)]. +``` + +Here `chi(0)=0` and `chi'(0)=delta_*>0`. Therefore every sufficiently +small positive `s` satisfies `phi(s)<0` and `chi(s)>0`. Choose such an +`s` rational. It supplies `u(t_*)<1` and strict ratio ordering. + +For the root tail, let + +```text +psi(lambda) = lambda log M + +g log[T(t_*-lambda)/P(t_*)]. +``` + +The equality of moments at `t_*` is essential here: it gives `psi(0)=0`. +By (5), + +```text +psi'(0) = log M-g mu_T* < 0. +``` + +Thus some sufficiently small positive rational `lambda` gives +`v(t_*)=exp(psi(lambda))<1`. There is no restriction on the sign of +`t_*-lambda`: all native ranks are positive and these finite moment sums +exist for every real exponent. + +Fix these `a,b,M,s,lambda`. All the inequalities just proved are strict +and all their expressions are continuous in `t`. The derivative of +`log q` equals `mu_T-mu_P`, which is positive at `t_*`. There are only +finitely many mirror cells, and their nonzero denominators stay positive. +Choose `beta_bar` strictly between `beta_*` and `eta_*`; shrink an interval +to the right of `t_*` until all its mirror ratios are at most `beta_bar` +and its mean gap is at least some `d>0`. Shrink again as necessary so that +the fixed two tails and ratio ordering remain strict, and so that its +upper endpoint is below one. On this compact interval choose `U,V<1` +above the two tail maxima and finite `Q` above `q`. + +Finally, + +```text +eta'(t) = m^(t-1)(1+t log m) > 0 for t>0. +``` + +Hence `eta(t)>=eta_*` on the interval. This proves every assertion in (3). +Integrating the mean-gap inequality from the exact crossing gives + +```text +q(t) >= exp[d(t-t_*)] for t in [t_*,t_*+epsilon]. (6) +``` + +For `t>t_*` within this interval, in particular, `T(t)>P(t)`. + +### 2.3 Funding the majorant at the crossing exponent + +This step applies #4483's shifted-log construction. It also identifies the +precise endpoint change to that source: its displayed guard +`T(t0)>P(t0)` can be replaced here by `T(t_*)=P(t_*)`, because the power +used by every finite-rank induction step is strictly above `t_*`. +Equation (6) supplies the same lower bound needed in its equation (19). +No geometric sum is evaluated with a zero moment gap. + +Put + +```text +R = (1-eta_*)/(eta_*-beta_bar) > 0. +``` + +Choose a positive rational `p` large enough that + +```text +exp(d p a/log M)-1 > R, (7) +``` + +and choose `c>0` with `c>=p/(1-t_*)`. For integer `ell>=1` define + +```text +K_ell = d p (a ell+1) / + [c+log m+(ell+1)log M+log 2], + +F_ell = (1-U^ell)(exp(K_ell)-1)-Q M^lambda V^ell. +``` + +The fraction in `K_ell` is increasing: its derivative, apart from a +positive denominator and the factor `d p`, is + +```text +a(c+log m+log 2)+(a-1)log M > 0. +``` + +Both other tail factors improve as `ell` increases. Thus `F_ell` is +nondecreasing, and + +```text +lim_(ell->infinity) F_ell = exp(d p a/log M)-1 > R. +``` + +Choose an integer `ell0>=1` with `F_ell0>=R`, large enough also that, for +`n0=m M^ell0`, + +```text +tau(n0) := t_*+p/(c+log n0) <= t_*+epsilon. (8) +``` + +Such a choice exists by the strict limit and because `tau(n0)` decreases +to `t_*`. The cutoff is an actual positive integer. Use elementary +evaluation at every `n<=n0`. + +For `n>n0`, put `C_n=floor(n/m)`, `ell=floor(log_M C_n)`, and +`t=tau(n)=t_*+p/(c+log n)`. Then `ell>=ell0` and +`t_*P(t)`. +Also + +```text +n < m(M^(ell+1)+1), +log n < log m+(ell+1)log M+log 2. +``` + +Consequently (6) gives `q(t)^(a ell+1)>=exp(K_ell)`. The exact source +cancellation and the two Chernoff bounds in #4483, equations (7)--(9), +therefore give + +```text +A_t := (T(t)-P(t)) H_t - R_t + >= D_ell(t) P(t)^(G+1), + +D_ell(t) = (1-u(t)^ell)(q(t)^(a ell+1)-1) + -q(t) M^lambda v(t)^ell + >= F_ell >= F_ell0 >= R. (9) +``` + +Here `H_t` is unit column potential and `R_t` is root-source potential; +`A_t` and `R_t` are unrelated to the normalization `A` and constant `R`. +Write `I_t,B_t,F_t` for inner sources, boundary exits, and leaf exits. +The same predecessor identities are + +```text +I_t=B_t+F_t+A_t, B_t<=beta_bar I_t, +F_t<=P(t)^(G+1). +``` + +The function `(1-eta)/(eta-beta_bar)` decreases for +`beta_bar=eta_*`, (9) implies + +```text +(eta(t)-beta_bar) A_t >= (1-eta(t)) F_t. +``` + +Combining this with `(1-beta_bar)I_t<=F_t+A_t` yields + +```text +B_t+F_t <= eta(t) I_t. (10) +``` + +In particular `A_t>0`, so the inner source potential and total source +count are positive. This supplies a nonempty flow in the certified range; +a separate paid-rank-one assumption is unnecessary for this theorem. + +Set + +```text +A = n0^(1-t_*)/(c+log n0)^p, +f(0)=0, f(x)=A x^t_* (c+log x)^p for x>=1. +``` + +For `x>=1`, its local tangent exponent is +`tau(x)=t_*+p/(c+log x)<=1`, and + +```text +f'(x)=f(x) tau(x)/x, +f''(x)/f(x)=x^(-2)[tau(x)(tau(x)-1)-p/(c+log x)^2]<=0. +``` + +Moreover `(f(x)/x)'<=0` and `f(n0)=n0`. Thus every elementary base +rank `1<=n<=n0` satisfies `L(n)=n<=f(n)`. + +For positive integer exit rank `e<=n`, `log(1+y)<=y` gives + +```text +f(e)/f(n) <= (e/n)^tau(n). (11) +``` + +For an inner source rank `s>n/m`, concavity gives + +```text +f(n)-f(n-s) >= tau(n) f(n) s/n + >= eta(tau(n)) f(n) (s/n)^tau(n). (12) +``` + +When `s=n`, the first inequality follows from `tau(n)<=1` and `f(0)=0`; +otherwise its arguments lie in `[1,n]`. Root sources may be smaller than +`n/m`, but their complement capacities remain nonnegative because `f` is +increasing. The zero-rank complement has zero cost. + +Equation (10), with (11)--(12), bounds the complete exit charge by the +inner-source capacity. Hence `f` satisfies the complete recurrence + +```text +sum_s S_s f(n-s)+sum_e E_e f(e) <= (sum_s S_s) f(n). +``` + +Every recursive rank is strictly below `n`, all counts are finite, and +the source count is positive. Strong induction proves (4). Finally, + +```text +log A+p log(c+log N) <= (z-t_*) log N +``` + +holds for every sufficiently large `N` whenever `z>t_*`; its left-hand +growth is logarithmic in `log N`, while the right-hand growth is linear +in `log N`. This proves the last assertion of the theorem. QED. + +## 3. Exact feasibility criterion for the two tail gates + +The following lemma characterizes just the tail and ratio-ordering gates +at a fixed exponent. It neither supplies the mirror hypothesis nor admits +a native implementation. It helps distinguish the root hypothesis above +from the stronger inequality required away from a root. + +Fix `t` with `q(t)=T(t)/P(t)>=1`, and for `lambda>0` define + +```text +H(lambda) = [log P(t)-log T(t-lambda)]/lambda. +``` + +**Lemma.** Positive integers `a,b`, an integer `M>1`, and positive rational +`s,lambda` satisfying + +```text +M^(-s) [T(t+s)/T(t)]^a [P(t+s)/P(t)]^b < 1, +M^lambda [T(t-lambda)/P(t)]^(a+b) < 1, +T(t+s)/T(t) >= P(t+s)/P(t) +``` + +exist if and only if there is a real `lambda>0` such that + +```text +H(lambda)>mu_P(t), +``` + +or, equivalently, + +```text +T(t-lambda) exp(lambda mu_P(t)) < P(t). (13) +``` + +**Necessity.** Put `g=a+b`, `alpha=a/g`, and `h=(log M)/g`. +The root-tail gate gives `halpha mu_T(t)+(1-alpha)mu_P(t)`. If `mu_T(t)<=mu_P(t)`, this would +contradict `hmu_P(t)`, and the +weighted mean is strictly above `mu_P(t)`. Thus `H(lambda)>mu_P(t)`. +The ratio-ordering gate is not needed for this direction. + +**Sufficiency.** Suppose (13) holds. Strictness and continuity allow +`lambda` to be chosen rational. The preceding convexity bound implies +`delta:=mu_T(t)-mu_P(t)>0`. Choose an integer `g>=2` large enough that +the interval + +```text +((g mu_P(t)+delta)/log 2, g H(lambda)/log 2) +``` + +has length greater than one, and choose an integer `j` strictly inside it. +Since `mu_P(t)>=0`, its lower endpoint is positive, so `j>=1`. +Set `a=1`, `b=g-1`, `M=2^j`. Then + +```text +mu_P(t)+delta/g < h=(log M)/g < H(lambda). +``` + +The upper inequality gives the root-tail gate. As in section 2.2, the +derivative at `s=0` of the mixed-tail logarithm is negative, while the +derivative of the logarithmic forward-ratio difference is `delta>0`. +All sufficiently small positive `s` therefore give both the mixed-tail +gate and strict forward-ratio ordering. Choose one rational. QED. + +At an exact crossing `q(t)=1`, `H(lambda)` tends to `mu_T(t)` as +`lambda` decreases to zero. A positive mean gap consequently guarantees +(13), recovering the existence step of section 2. At `q(t)>1`, a +positive mean gap alone does not imply (13). The strict surplus `T(t)>P(t)` +required by a recurrence at its actual exponent remains a separate condition; +the lemma concerns only the displayed tail and ordering inequalities. + +## 4. Why fixed-exponent mean separation alone does not suffice + +The moment equality at `t_*` cannot simply be dropped from the gate-existence +argument. Consider the valid rank histograms + +```text +targets: W_4=4, W_64=17; paid: P_1=4, P_16=1; +t=1/2, m=64. +``` + +Then + +```text +T(t)=144>P(t)=8, +mu_T(t)=(26/9)log 4 > mu_P(t)=log 4. +``` + +This profile also passes strict pointwise mirror capacity. Its only exit +window is `(1/16,1/4]`, from the pair `(r,k)=(16,4)`, with coefficient +`4 sqrt(64)=32`. Throughout this window the pair `(1,64)` supplies inner +coefficient `4*17*sqrt(64)=544`. The remaining cells have no exits. Hence +the exact largest mirror ratio is `beta=32/544=1/17`, while +`eta(t)=(1/2)/sqrt(64)=1/16`. + +Nevertheless no choice of positive integers `a,b`, `M>1`, and positive +`s,lambda` satisfies both tail gates. Convexity of both logarithmic moment +functions gives, with `g=a+b`, + +```text +log u >= s[-log M+a mu_T(t)+b mu_P(t)]. +``` + +Thus `u<1` forces `h:=(log M)/g>log 4`. The rank-4 target term alone gives + +```text +T(t-lambda) >= 4*4^(1/2-lambda) = 8*4^(-lambda). +``` + +It follows that + +```text +v^(1/g)=exp(h lambda) T(t-lambda)/P(t) + >=exp(lambda[h-log 4]) >1, +``` + +a contradiction. The obstruction concerns these simultaneous Chernoff +gates, not existence of every possible compiler. Equivalently, the rank-4 +term ensures `T(t-lambda) exp(lambda mu_P(t))>=8=P(t)` for every +`lambda>0`, so the exact criterion (13) fails. For every `x>=0`, +`4*4^x>=4` and `17*64^x>16^x`, so this profile has no moment crossing in +`(0,1)`. It is outside the theorem's hypotheses despite passing the other +three fixed-exponent tests, and does not challenge #4483's certified +examples. This strengthened example was supplied by the separate +author-side proof audit for this contribution. + +## 5. Scope, evidence and credit + +The theorem inherits #4483's all-column arbitrary-input correctness, +disjoint productive owners, literal chronological paid interface, and +permitted and priced whole-job adapters, including input maps. Native +centers and scratch must remain owned until their words restore and erase +them. No input cloning, field aliasing, omitted complement, unpaid move, +or pooling of unfinished calls is introduced here. Integer widths must +still clear every actual chronological batch. Existence of a finite word +and its normalized recurrence gives no numerical productive-width bound +or physical, precision, fixed-tape, stock, analytic-transfer, or recovery +constant. Those obligations remain inherited and unresolved by this note. + +The new implication is a sufficient profile criterion for the adaptive +gates and the explicit allowance of the exact crossing as the endpoint of +the funded majorant. The finite compiler is Jacob Alan Sussman's work; +the overlapping integer flow and adaptive/shifted-log argument are zxv's +#4436 and #4483; the corrected mirror-window method is Ryanson Jonathan's +#4459. The related finite-flow, leaf, width and accounting investigations +retain their own contributions and limitations. Their native construction +lineage, including Cinna Davis and the original retained sources, is +unchanged. Prepared for Dillon with substantial OpenAI Codex assistance. +The proof is an author-side mathematical argument, not a formal-kernel +proof or independent human review. Apache-2.0. + +## Open next questions + +1. Is a weaker, distribution-dependent boundary condition sufficient when + the pointwise mirror factor reaches source capacity? The first step is + to retain the exact capped base measure on the offending windows. That + requires a new bound; this proof uses strict uniform pointwise slack. +2. Can profiles with a favorable moment but no simple crossing satisfying + the mirror condition use a different height or majorant? The exact + counterexample above shows why mean separation alone cannot establish + the present two-tail gates. It does not rule out another compiler. +3. Can the resulting chronological words be emitted with complete native + physical and precision constants? Start with one small changed-height + forest and its actual batch widths. The inherited native contracts and + complete paid implementation remain the blocking obligations. diff --git a/research/adaptive-gate-existence/README.md b/research/adaptive-gate-existence/README.md new file mode 100644 index 0000000000..955d60830d --- /dev/null +++ b/research/adaptive-gate-existence/README.md @@ -0,0 +1,176 @@ +# Adaptive compiler gates at a moment crossing + +A moment crossing plus strict pointwise mirror slack suffices for the adaptive +compiler in [zxv’s #4483](https://github.com/CrocSwap/integer-mult-bounds/pull/4483). +The tilted-mean gap follows from the mirror condition itself. The resulting +normalized rank-one leaf cost satisfies + +```text +L(n) <= A n^t* (c + log n)^p +``` + +at the **exact crossing exponent** `t*`, with a funded ordinary base range. +This answers #4483’s broader-admission question for a sufficient class of +profiles. It does not assert gate existence for every favorable moment profile. +There is no new κ or selected-frontier change. + +## The new implication + +For finite integer target and paid histograms, let +`T(t)=sum W_k k^t` and `P(t)=sum P_r r^t`, with `2<=k<=m` and `1<=r=P(t)`, the proof also gives an exact +criterion for the two tail gates and their ordering guard: they are feasible +if and only if some `lambda>0` satisfies +`T(t-lambda) exp(lambda mu_P(t)) < P(t)`. This reduces that parameter +existence question to one scalar inequality; mirror and native contracts +remain separate. + +## Exact witness and obstruction + +The abstract profile `W_16=1, W_256=4; P_1=59, P_81=1` has the exact crossing +`T(1/2)=P(1/2)=68`. It is a histogram fixture, not a claimed native word. +[WITNESS.json](WITNESS.json) uses + +```text +a=b=1, M=4096, s=lambda=1/4, +p=12, c=24, ell0=128, n0=2^1544. +``` + +The new standard-library checker certifies every exponent in +`[1/2,33/64]`, including every elementary mirror cell: + +| Guard | Exact certified bound (decimal display) | +| --- | --- | +| Mean-gap derivative | at least 4 | +| Mixed tail upper bound | below .622356 | +| Root tail upper bound | below .660349 | +| Mirror factor / source capacity | `1/80 < 1/32` | +| Funded recurrence lower bound | above 272.857919 | +| Required recurrence threshold | `155/3` | + +The funded majorant is +`A n^(1/2)(24+log n)^12`, where +`A=2^772/(24+1544 log 2)^12`. The enormous cutoff is an explicit proof +fixture; no practical threshold claim follows. + +The counterexample `W_4=4, W_64=17; P_1=4, P_16=1` at `t=1/2` passes +moment surplus, mean separation and mirror slack (`1/17 < 1/16`), yet no +positive choice of the two-tail geometry works. Jensen’s inequality and +one target term prove this for all parameters. Thus favorable tests at an +arbitrary exponent cannot replace the crossing hypothesis. This excludes +these simultaneous Chernoff gates, not all possible compilers. + +## Application to retained native inventories + +`root_application.py` checks the two frozen rank inventories used by #4483. +It authenticates the p7 receipt from #4433 and matches p16’s #4479 compact +consumer inventory to #4470’s native receipt. It executes no producer code. + +| Profile | Unique crossing within this open bracket | Mean-gap lower bound | Mirror upper bound | Capacity lower bound | +| --- | --- | ---: | ---: | ---: | +| p7 | `(.997313, .997314)` | 1.723542 | .320851 | .984543 | +| p16 | `(.996979, .996980)` | 1.042284 | .562814 | .982101 | + +These coarse outward bounds certify the **hypotheses at each actual root**. +They are not new root refinements or new κ values. The theorem therefore +supplies a critical-exponent polylog majorant for each inventory under its +inherited native contracts. The checker also certifies explicit constants at the actual roots, +using the predecessor’s authenticated geometry and logarithmic parameters: + +| Profile | Ordinary base cutoff `n0` | `p` | `c` | Funding lower bound | Required upper bound | +| --- | --- | ---: | ---: | ---: | ---: | +| p7 | `121*256^100` | `1/10` | 38 | .028589 | .023329 | +| p16 | `145*1024^650` | `2/5` | 133 | .048546 | .042809 | + +For each isolated root `theta`, set +`A=n0^(1-theta)/(c+log n0)^p`. Then the stated +`L(n)<=A n^theta(c+log n)^p` holds for every integer `n>=1`. +The uniform exponent covers are `.997483` and `.997067`; p7 uses a +conservative mirror factor `.322` for its wider interval. These are explicit +changes to the certification bounds. The native words and paid invoices +remain the source inputs. + +For each bracket, exact opposite moment signs give existence. The tilted +means satisfy `mu'(t)=Var_t(log rank)>=0`, so +`mu_T(lo)-mu_P(hi)>0` certifies uniqueness on that bracket. On each mirror +cell, `E_J(hi)/S_J(lo)` bounds every ratio inside the bracket; all ranks +are at least one. The capacity `t m^(t-1)` increases for positive `t`. +The source inventories and their native correctness remain distinct claims. + +## Reproduction and coverage + +From the repository root, with Python 3.12 and no third-party dependencies: + +```sh +python3.12 -B scripts/research_package.py --package research/adaptive-gate-existence +python3.12 -I -O -B research/adaptive-gate-existence/verify.py +``` + +The verifier authenticates its declared predecessor inputs before checking +anything scientific. It uses exact rational root brackets, logarithm-series +tails and a positive exponential partial sum; no predecessor executable is +imported. It checks the two integral identities symbolically on square-rank +fixtures, half-open mirror endpoints, an uncovered source window, and nine +semantic rejection controls. Optimized Python retains all checks. +The separate application checker uses outward binary rational log/exp +intervals, 48 exact algebraic power controls and twelve additional semantic +rejections. Finite checks corroborate the proof and its witness; they do not extrapolate +an all-rank theorem from sampled ranks. `SOURCES.json` pins the canonical +base and all consumed evidence. `TASK.json` records scope, overlap and the +checkpoint. The old task card is retained as provenance; this explicitly +changed scope follows #4483’s concrete open question. + +## Remaining obligations + +The theorem concerns normalized leaf counts under #4483’s inherited native +contract. Arbitrary-input all-column correctness, distinct owners, literal +paid chronology, whole-job adapters, restoration, integer batch widths, +movement, precision, stock, fixed-tape costs, analytic transfer and exact +recovery remain required. No native or outer producer suite was rerun. +No numerical width bound or complete multiplication theorem is established. + +## Open next questions + +- Can a weaker bound against the actual capped measure replace strict + pointwise mirror slack? First retain the mass on an offending window; + a new distribution-dependent estimate is required. +- Can the polylogarithmic loss be reduced, or its constants made useful for + a particular native profile? The p7/p16 critical-root constants are certified here; first compare + geometry choices while keeping the base normalization and complete consumer bill. +- Can an actual small adaptive word supply complete physical and precision + constants? Start from its chronological batches and owned native executor; + the histogram proof does not supply that implementation. + +Credit zxv (#4436/#4483), Jacob Alan Sussman’s integer compiler, Ryanson +Jonathan’s corrected #4459 mirror method, Cinna Davis and the retained native +and outer contributors. The p7/#4433 source and @1337isnot1337’s p7 controller lineage, +Cinna Davis’s #4470 p16 word and Dugongue’s #4479 +compact consumer retain their attribution. Related #4507/#4519 batch-width work and #4521 +expanded accounting have different scopes. Prepared by Dillon with substantial +OpenAI Codex assistance, including separate proof-development and adversarial +review agents. Apache-2.0. diff --git a/research/adaptive-gate-existence/SOURCES.json b/research/adaptive-gate-existence/SOURCES.json new file mode 100644 index 0000000000..9260f34571 --- /dev/null +++ b/research/adaptive-gate-existence/SOURCES.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "base_commit": "f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40", + "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/rank-convergence/PROOF.md", + "usage": "input", + "git_blob": "75f451837204bd141f357e7f5e5d6c6f42e1423e", + "sha256": "3c971c5670669cb36312815b111e64c83e1490a10ee82f5412bd9aee01e9c376" + }, + { + "path": "research/rank-convergence/README.md", + "usage": "input", + "git_blob": "b0370acf5395f128d322419a619087ef6dfd6a20", + "sha256": "e77af882d3f02a9d3f2dd19dce889052f63892a1c8f39fdbe0813ff5fab5e8c1" + }, + { + "path": "research/higher-moment-strictification/RESULT.json", + "usage": "input", + "git_blob": "e66b39c674028adfd22f0de3170555dccda52f6a", + "sha256": "ad79e3c0459e7b495a0ca34010553b12147779a007389e1695cc1336f123c156" + }, + { + "path": "research/compact-joint-compiler/arithmetic/RESULT.json", + "usage": "input", + "git_blob": "514d12ce4d2d824a4e0a418022bba610c8aed8ff", + "sha256": "a6caaa2a6d6460a8c1ef7e48c4853bb27976be33a52b96a4216dfa90d96c9091" + }, + { + "path": "research/joint-helper-lattice/RESULT.json", + "usage": "input", + "git_blob": "edf41a49a0350862c23378f837c7397fc5dc7596", + "sha256": "c7b2388f6511c19976b337d8c8ac374610af616866a249d75dace704eb5d9e21" + }, + { + "path": "research/rank-convergence/BENCHMARKS.json", + "usage": "input", + "git_blob": "bc58c96abda014c28de91eca3ff10a7d4ec30b32", + "sha256": "513efe2fe74af82891c1918e462ba8338b1bbd06403cbfcec284bcf3b4f8f850" + } + ] +} diff --git a/research/adaptive-gate-existence/TASK.json b/research/adaptive-gate-existence/TASK.json new file mode 100644 index 0000000000..fcbd91c705 --- /dev/null +++ b/research/adaptive-gate-existence/TASK.json @@ -0,0 +1,141 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Prove adaptive gate existence from a moment crossing and strict mirror slack, characterize fixed-exponent tail feasibility, and certify critical-exponent logarithmic leaf bounds for the retained p7 and p16 inventories.", + "scope_change_reason": "Handoff-first inspection found #4483 explicitly requesting broader admission gates. The old #4100 card predates the selected productive-helper mechanism; this scoped override proves one current compiler implication rather than repeating old transfer checks.", + "bottleneck_link": "Turn three profile-specific adaptive witnesses into a sufficient profile theorem, identifying the actual crossing hypothesis and preserving physical obligations.", + "budget_minutes": 60, + "stop_rule": "Prove this sufficient criterion, verify its exact witness and obstruction, then publish one focused package within the hour; no new native construction, frontier change or heavy historical replay.", + "outcome": "completed", + "evidence": "Written general proof and gate-obstruction counterexample; exact toy witness and symbolic mirror integrals; separately implemented p7/p16 root isolation and full critical-majorant certificates. Total 21 semantic rejections plus exact arithmetic and boundary controls.", + "author": "Dillon, with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in mathematics, code and documentation; separate proof-development and adversarial-review agents. No formal or independent human review.", + "open_questions": [ + { + "question": "Can pointwise mirror slack be replaced by a bound against the capped measure?", + "why_it_matters": "The sufficient criterion may exclude useful profiles.", + "first_step": "Retain the exact base measure on one offending mirror window.", + "blocked_by": "A new distribution-dependent estimate is needed." + }, + { + "question": "Can the logarithmic loss or funded cutoff be reduced for p7/p16 without changing the consumer bill?", + "why_it_matters": "This package certifies explicit critical-root constants but does not optimize them.", + "first_step": "Compare geometry and normalization at the exact isolated root while retaining every source, exit and paid cost.", + "blocked_by": "No optimality theorem for these sufficient guards; eventual physical constants still unknown." + }, + { + "question": "Can complete physical constants be emitted for a small adaptive word?", + "why_it_matters": "Normalized leaf counts do not measure widths, movement, scratch or precision.", + "first_step": "Bind chronological batches to an owned native executor.", + "blocked_by": "Native and physical implementation contracts are inherited." + } + ], + "canonical_discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4525", + "session_started_utc": "2026-10-22T03:28:11Z", + "verification_reserved_from_utc": "2026-10-22T04:13:11Z", + "upstream_checkpoint": { + "canonical_main": "f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc", + "checked_at_utc": "2026-10-22T03:28:11Z", + "priority_revision": 7, + "selected_record_sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9", + "selected_kappa": "23/10000", + "decision": "Start a distinct branch from canonical main; preserve completed PR4521 and all earlier frozen inputs.", + "research_recheck_utc": "2026-10-22T03:47:43Z", + "research_recheck_result": "Canonical main remains f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc; guidance and selection unchanged." + }, + "overlap": { + "open_pr_bodies": 310, + "open_prs_fetched_at": "2026-10-22T03:31:07.898501+00:00", + "discussion_records": 3403, + "discussions_fetched_at": "2026-10-22T03:31:39.205487+00:00", + "remote_pagination_complete": true, + "local_notes_searched": 5860, + "local_head_inventory_complete": true, + "additional_checks": "All-state searches for tilted, gate existence, broader admission and rank-convergence; relevant live heads and latest handoffs inspected. No competing gate-existence claim found.", + "limits": "Bounded text coverage; not arbitrary diffs or a novelty certificate. Closed work searched through local archive notes and focused all-state queries.", + "research_recheck": { + "open_pr_bodies": 312, + "open_prs_fetched_at": "2026-10-22T03:47:48.137015+00:00", + "discussion_records": 3407, + "discussions_fetched_at": "2026-10-22T03:48:24.276378+00:00", + "pagination_complete": true, + "result": "Only own claim and unrelated historical moment-crossing work match the new criterion; no matching competing gate theorem found." + } + }, + "predecessor": { + "pr": 4483, + "head": "fb0c208864e6b24e3473318a058aa5b2dbd5764b", + "author": "zxv", + "task": "Broader admission gates from tilted log means and strict mirror capacity." + }, + "baseline_orientation": { + "command": "python3 -B scripts/research_selected_baseline.py", + "result": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "reason": "Use current productive-helper adapter; historical card helper expects obsolete certificate fields. No selected scientific replay." + }, + "validation": { + "registered_python": "3.12.15", + "secondary_python": "3.14.7", + "platform": "macOS 27.0.1 arm64", + "registered_replay": "PASS_REGISTERED_RESEARCH_PACKAGE", + "metadata": "PASS_PACKAGE_METADATA_AND_PINS", + "semantic_rejections": 21, + "root_application_arithmetic_controls": 48, + "proof_review": "Separate author-side AI reviews of the theorem, exact feasibility lemma, mirror integrals, arithmetic enclosures and unknown-root quantitative guards; no formal or independent human review.", + "native_and_outer_replays": "not run; source inventories and contracts inherited" + }, + "verification_started_utc": "2026-10-22T03:54:13Z" +} diff --git a/research/adaptive-gate-existence/VALIDATION.md b/research/adaptive-gate-existence/VALIDATION.md new file mode 100644 index 0000000000..80e99fa4fb --- /dev/null +++ b/research/adaptive-gate-existence/VALIDATION.md @@ -0,0 +1,66 @@ +# Validation and reproducible scope + +Research base: canonical main `f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc`. +Selected record: conditional `23/10000`, unchanged. +Environment: macOS 27.0.1 arm64; registered replay with Python 3.12.15, +secondary isolated optimized checks with Python 3.14.7; standard library only. + +## Passed scientific checks + +```sh +python3.12 -B scripts/research_package.py --package research/adaptive-gate-existence +python3.12 -I -O -B research/adaptive-gate-existence/verify.py +python3 -B scripts/research_package.py --package research/adaptive-gate-existence --check-only +``` + +- Exact abstract critical-root witness, covering an entire exponent interval, + all mirror cells, the base range and the shifted-logarithmic funding guard. +- Exact symbolic checks of the two new mirror-integral identities on square-rank + fixtures, mirror endpoint conventions and a cell with exits but no source. +- Nine deliberate failures of the abstract witness, plus twelve source-profile + failures, including false roots, mirror violations and underfunded logarithms. +- Twenty-five rational-root enclosure controls and 48 algebraic controls for the + separately written fixed-grid logarithm/exponential evaluator. +- Source-bound p7 and p16 root isolation, uniform mirror/mean checks and explicit + quantitative majorants at the actual roots, with every parameter guard funded. +- p16 compact-consumer and native paid/productive inventories match exactly. + +`verify.py` prints a complete deterministic JSON receipt. The displayed U/V/Q +intervals enclose conservative upper estimators; `D_lower` encloses the certified +lower estimator. They need not enclose an actual extremum of the analytic +function. The written proof supplies all-rank and all-parameter arguments. +Finite checks do not substitute for those arguments. + +## Mathematical review + +Separate author-side agents checked the new crossing implication, the weighted +mirror integrals, the exact fixed-exponent feasibility criterion, the critical +endpoint and complete induction. Another pass checked the interval arithmetic, +source lineage and the unknown-root quantitative certificates. The strengthened +counterexample came from that adversarial review. No unresolved defect was +identified. These are AI-assisted author reviews, not formal-kernel verification +or independent human acceptance. + +## Publication checks + +After committing, run: + +```sh +python3 -B scripts/check_research_commit.py --package research/adaptive-gate-existence --check-source-history +python3 scripts/export_research_package.py export --package research/adaptive-gate-existence --ref HEAD --output /tmp/adaptive-gate-existence.tar +python3 scripts/export_research_package.py check /tmp/adaptive-gate-existence.tar +``` + +The direct verifier consumes only package files and the six declared inputs; +it requires neither Git nor network access. The generic registered runner +separately needs Git history to authenticate historical card/source provenance. +Final publication results are recorded in `TASK.json`. + +## Remaining obligations + +No predecessor native or outer producer suite was rerun. The abstract fixture +is not a native word. Native all-column semantics, owners, whole-job adapters, +restoration, chronological divisible widths, movement, precision, stock, +fixed-tape execution, analytic transfer and exact recovery remain inherited. +The result is a conditional leaf-count theorem with explicit certificates; +there is no new selected κ, materialized winning word or practical threshold. diff --git a/research/adaptive-gate-existence/VERIFY.json b/research/adaptive-gate-existence/VERIFY.json new file mode 100644 index 0000000000..60dde56567 --- /dev/null +++ b/research/adaptive-gate-existence/VERIFY.json @@ -0,0 +1,27 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/rank-convergence/PROOF.md", + "research/rank-convergence/README.md", + "research/higher-moment-strictification/RESULT.json", + "research/compact-joint-compiler/arithmetic/RESULT.json", + "research/joint-helper-lattice/RESULT.json", + "research/rank-convergence/BENCHMARKS.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact critical-root uniform gates, mirror integrals, universal-obstruction fixtures and semantic rejection controls. Separate exact root/mirror certificates for the p7 and p16 source inventories." + } + ] +} diff --git a/research/adaptive-gate-existence/WITNESS.json b/research/adaptive-gate-existence/WITNESS.json new file mode 100644 index 0000000000..312721f956 --- /dev/null +++ b/research/adaptive-gate-existence/WITNESS.json @@ -0,0 +1,16 @@ +{ + "targets": {"16": 1, "256": 4}, + "paid": {"1": 59, "81": 1}, + "root": "1/2", + "upper_exponent": "33/64", + "a": 1, + "b": 1, + "M": 4096, + "s": "1/4", + "lambda": "1/4", + "d": "4", + "beta": "1/80", + "p": "12", + "c": "24", + "ell0": 128 +} diff --git a/research/adaptive-gate-existence/root_application.py b/research/adaptive-gate-existence/root_application.py new file mode 100644 index 0000000000..89d6139b63 --- /dev/null +++ b/research/adaptive-gate-existence/root_application.py @@ -0,0 +1,365 @@ +#!/usr/bin/env python3 +"""Critical-root hypotheses for the retained p7 and p16 rank inventories. + +Separate exact arithmetic and mirror enumeration; no predecessor evaluator is +imported. The inventories and native contracts remain credited source inputs. +Dillon with substantial OpenAI Codex assistance; Apache-2.0. +""" +from collections import Counter +from fractions import Fraction as F +from functools import lru_cache +from hashlib import sha256 +import json +from pathlib import Path + + +GRID = 1 << 128 +PINS = { + 'research/higher-moment-strictification/RESULT.json': + 'ad79e3c0459e7b495a0ca34010553b12147779a007389e1695cc1336f123c156', + 'research/compact-joint-compiler/arithmetic/RESULT.json': + 'a6caaa2a6d6460a8c1ef7e48c4853bb27976be33a52b96a4216dfa90d96c9091', + 'research/joint-helper-lattice/RESULT.json': + 'c7b2388f6511c19976b337d8c8ac374610af616866a249d75dace704eb5d9e21', + 'research/rank-convergence/BENCHMARKS.json': + '513efe2fe74af82891c1918e462ba8338b1bbd06403cbfcec284bcf3b4f8f850', +} + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def floorq(x): + return x.numerator // x.denominator + + +def ceilq(x): + return -((-x.numerator) // x.denominator) + + +def outward(lo, hi): + return floorq(lo * GRID), ceilq(hi * GRID) + + +@lru_cache(None) +def logarithm(n): + """Integer endpoints in units 2^-128, using an exact atanh tail.""" + require(type(n) is int and n >= 1, 'positive integer logarithm') + + def series(y): + z = (y - 1) / (y + 1) + require(0 <= z <= F(1, 3), 'logarithm range reduction') + # log(y)=2 sum z^(2j+1)/(2j+1). Every omitted denominator + # is at least 121, so the geometric tail bounds all omitted terms. + term, total = z, F(0) + for j in range(60): + total += 2 * term / (2*j + 1) + term *= z*z + return total, total + 2*term / (121*(1-z*z)) + + exponent = n.bit_length() - 1 + a, b = series(F(n, 1 << exponent)) + c, d = series(F(2)) + return outward(a + exponent*c, b + exponent*d) + + +def exponential(x): + """Outward integer endpoints for exp(exact rational x).""" + x = F(x) + if x == 0: + return GRID, GRID + if x < 0: + lo, hi = exponential(-x) + return GRID*GRID // hi, -((-GRID*GRID) // lo) + squarings = 0 + while x > F(1, 2): + x /= 2 + squarings += 1 + term_lo = term_hi = total_lo = total_hi = GRID + for j in range(1, 65): + term_lo = floorq(term_lo*x/j) + term_hi = ceilq(term_hi*x/j) + total_lo += term_lo + total_hi += term_hi + # The next term is x^65/65!. Subsequent ratios are <=1/132; + # twice an upper enclosure of that term bounds the entire tail. + total_hi += 2*ceilq(term_hi*x/65) + for _ in range(squarings): + total_lo = total_lo*total_lo // GRID + total_hi = -((-total_hi*total_hi) // GRID) + return total_lo, total_hi + + +@lru_cache(None) +def power(n, t): + t = F(t) + lo, hi = logarithm(n) + endpoints = [F(lo, GRID)*t, F(hi, GRID)*t] + lower = exponential(min(endpoints))[0] + upper = exponential(max(endpoints))[1] + return F(lower, GRID), F(upper, GRID) + + +def moment(histogram, t): + lo = hi = F(0) + for rank, count in histogram.items(): + a, b = power(rank, t) + lo += count*a + hi += count*b + return lo, hi + + +def mean(histogram, t): + lo = hi = F(0) + for rank, count in histogram.items(): + a, b = power(rank, t) + c, d = logarithm(rank) + lo += count*a*F(c, GRID) + hi += count*b*F(d, GRID) + total_lo, total_hi = moment(histogram, t) + require(total_lo > 0, 'positive tilted total') + return lo/total_hi, hi/total_lo + + +def display(interval): + # These short rational bounds are rounded outward, never floating point. + unit = 10**6 + return [str(F(floorq(interval[0]*unit), unit)), + str(F(ceilq(interval[1]*unit), unit))] + + +def histogram(raw): + require(isinstance(raw, dict) and raw, 'nonempty histogram') + result = {} + for key, count in raw.items(): + rank = int(key) + require(str(rank) == str(key) and rank >= 1, + 'canonical positive integer rank') + require(type(count) is int and count > 0, 'positive multiplicity') + result[rank] = count + return result + + +def mirror_sides(targets, paid, x): + sources, exits = Counter(), Counter() + for k, w in targets.items(): + for r, count in paid.items(): + if k > r and F(1, k) < x <= F(1, r): + sources[k*r] += w*count + if r > k and F(1, r) < x <= F(1, k): + exits[k*r] += w*count + return sources, exits + + +def certify(profile, lo, hi, beta, derivative_floor): + targets, paid = (histogram(profile[key]) for key in ('targets', 'paid')) + m = max(targets) + require(min(targets) >= 2 and max(paid) < m and paid.get(1, 0) > 0, + 'native rank interface and nonempty forests') + require(0 < lo < hi < 1, 'critical exponent interval') + require(sum(k*q for k, q in targets.items()) > + sum(k*q for k, q in paid.items()), 'positive rank-one surplus') + first_t, first_p = moment(targets, lo), moment(paid, lo) + last_t, last_p = moment(targets, hi), moment(paid, hi) + first = first_t[0]-first_p[1], first_t[1]-first_p[0] + last = last_t[0]-last_p[1], last_t[1]-last_p[0] + require(first[1] < 0 < last[0], 'root sign crossing') + # Each tilted mean is nondecreasing: its derivative is the variance + # of log(rank). Thus this bounds their difference on the whole interval. + gap = mean(targets, lo)[0] - mean(paid, hi)[1] + require(gap > derivative_floor > 0, 'positive crossing derivative') + # t*m^(t-1) increases for t>0, since its derivative has the sign + # of 1+t*log(m). This lower bound therefore applies at the unknown root. + eta = lo*power(m, lo-1)[0] + require(0 <= beta < eta, 'strict mirror capacity') + points = sorted({F(0), *(F(1, k) for k in targets), + *(F(1, r) for r in paid)}) + cells, worst, worst_cell = [], F(0), None + for left, right in zip(points, points[1:]): + source, exit_ = mirror_sides(targets, paid, (left+right)/2) + require((source, exit_) == mirror_sides(targets, paid, right), + 'right-closed mirror endpoint') + ehi = moment(exit_, hi)[1] + slo = moment(source, lo)[0] + require(ehi <= beta*slo, 'uniform mirror inequality') + if exit_: + ratio = ehi/slo + cells.append({'left': str(left), 'right': str(right), + 'upper_ratio': display((ratio, ratio))[1]}) + if ratio > worst: + worst, worst_cell = ratio, [str(left), str(right)] + require(mirror_sides(targets, paid, F(0)) == (Counter(), Counter()), + 'zero mirror endpoint') + require(mirror_sides(targets, paid, 2*points[-1]) == (Counter(), Counter()), + 'empty mirror tail') + return {'critical_root_interval': [str(lo), str(hi)], + 'endpoint_target_minus_paid': [display(first), display(last)], + 'uniform_mean_gap_lower': display((gap, gap))[0], + 'derivative_floor': str(derivative_floor), + 'beta': str(beta), 'source_capacity_lower': display((eta, eta))[0], + 'mirror_upper': display((worst, worst))[1], + 'maximizing_cell': worst_cell, 'funded_mirror_cells': cells, + 'conclusion': 'Unique crossing on this bracket; critical-root hypotheses hold.', + 'scope': 'Rank-inventory admission criterion; native and outer obligations inherited.'} + + +def arithmetic_controls(): + count = 0 + for base in (1, 2, 3, 5, 16, 121, 145, 10440): + for exponent in (F(-1, 2), F(0), F(1, 4), F(1, 2), F(1), F(2)): + lo, hi = power(base, exponent) + require(lo > 0 and lo**exponent.denominator <= F(base)**exponent.numerator + <= hi**exponent.denominator, 'exact power enclosure control') + count += 1 + return count + + +def critical_guards(profile, root_lo, root_hi, witness): + """Fund a shifted-logarithmic majorant at the isolated critical root. + + Uniform inequalities cover [root_lo, upper_exponent], a superset of + every unknown-root interval needed in the written endpoint theorem. + Parameters are inherited from #4483 except the explicit cover and beta. + """ + targets, paid = (histogram(profile[key]) for key in ('targets', 'paid')) + m = max(targets) + top = F(witness['upper_exponent']) + a, b, M, ell = (witness[key] for key in ('a', 'b', 'height_base', 'ell0')) + require(all(type(v) is int and v >= 1 for v in (a, b, ell)) and + type(M) is int and M >= 2, 'critical integer geometry') + s, lam, p, c = (F(witness[key]) for key in ('s', 'lambda', 'p', 'c')) + require(0 < root_lo < root_hi < top < 1 and min(s, lam, p, c) > 0, + 'critical parameter domain') + U, V, Q, d, beta = (F(witness['guards'][key]) + for key in ('U', 'V', 'Q', 'd', 'beta')) + require(0 < U < 1 and 0 < V < 1 and Q >= 1 and d > 0, + 'critical uniform guard domain') + require(c >= p/(1-root_hi), 'critical concavity') + mean_gap = mean(targets, root_lo)[0] - mean(paid, top)[1] + require(mean_gap >= d, 'critical mean gap') + + def forward(h, t): + x, y = moment(h, t+s), moment(h, t) + return x[0]/y[1], x[1]/y[0] + + # The derivative of log(M_h(t+s)/M_h(t)) is mu_h(t+s)-mu_h(t) + # and is nonnegative, because a tilted mean has variance derivative. + ordering = forward(targets, root_lo)[0] - forward(paid, top)[1] + require(ordering >= 0, 'critical forward ordering') + actual_u = power(M, -s)[1]*forward(targets, top)[1]**a*forward(paid, top)[1]**b + actual_v = power(M, lam)[1]*(moment(targets, top-lam)[1]/moment(paid, root_lo)[0])**(a+b) + actual_q = moment(targets, top)[1]/moment(paid, root_lo)[0] + require(actual_u <= U, 'critical mixed tail') + require(actual_v <= V, 'critical root tail') + require(actual_q <= Q, 'critical moment ratio') + eta = root_lo*power(m, root_lo-1)[0] + require(0 <= beta < eta < 1, 'critical mirror capacity') + points = sorted({F(0), *(F(1, k) for k in targets), + *(F(1, r) for r in paid)}) + mirror_upper = F(0) + for left, right in zip(points, points[1:]): + sources, exits = mirror_sides(targets, paid, (left+right)/2) + numerator, denominator = moment(exits, top)[1], moment(sources, root_lo)[0] + require(numerator <= beta*denominator, 'critical mirror window') + if exits: + mirror_upper = max(mirror_upper, numerator/denominator) + + def log(n): + return tuple(F(x, GRID) for x in logarithm(n)) + + logn0_lo = log(m)[0] + ell*log(M)[0] + tau_upper = root_hi + p/(c+logn0_lo) + require(tau_upper <= top, 'critical tangent cover') + denominator = c + log(m)[1] + (ell+1)*log(M)[1] + log(2)[1] + K = d*p*(a*ell+1)/denominator + lower = (1-U**ell)*(F(exponential(K)[0], GRID)-1)-Q*power(M, lam)[1]*V**ell + required = (1-eta)/(eta-beta) + require(lower >= required, 'critical recurrence funding') + return {'parameters': witness, + 'uniform_interval': [str(root_lo), str(top)], + 'uniform_mean_gap_lower': display((mean_gap, mean_gap))[0], + 'forward_ordering_margin_lower': display((ordering, ordering))[0], + 'mixed_tail_upper': display((actual_u, actual_u))[1], + 'root_tail_upper': display((actual_v, actual_v))[1], + 'moment_ratio_upper': display((actual_q, actual_q))[1], + 'mirror_upper': display((mirror_upper, mirror_upper))[1], + 'source_capacity_lower': display((eta, eta))[0], + 'tangent_exponent_upper': display((tau_upper, tau_upper))[1], + 'funding_lower': display((lower, lower))[0], + 'required_funding_upper': display((required, required))[1], + 'ordinary_base_cutoff': str(m)+'*'+str(M)+'^'+str(ell), + 'normalization': 'A=n0^(1-theta)/(c+log(n0))^p, where theta is the isolated root', + 'conclusion': 'L(n)<=A*n^theta*(c+log(n))^p for every integer n>=1, under the stated contracts.', + 'scope': 'Critical-exponent leaf-count majorant; no new outer endpoint or physical admission.'} + + +def run(root): + root = Path(root) + sources = {} + for path, digest in PINS.items(): + raw = (root/path).read_bytes() + require(sha256(raw).hexdigest() == digest, 'source bytes: '+path) + sources[path] = json.loads(raw) + p7 = sources['research/higher-moment-strictification/RESULT.json']['invoice_oracle'] + p16 = sources['research/compact-joint-compiler/arithmetic/RESULT.json'] + native = sources['research/joint-helper-lattice/RESULT.json'] + require(all(p16[k] == native[k] for k in ('targets', 'paid')), + 'p16 consumer/native inventory equality') + cases = [('p7', p7, F('0.997313'), F('0.997314'), F('0.321'), F(1)), + ('p16', p16, F('0.996979'), F('0.996980'), F('0.564'), F(1))] + results, rejected = {}, {} + original = {row['name']: row['witness'] for row in + sources['research/rank-convergence/BENCHMARKS.json']['cases']} + for name, profile, lo, hi, beta, gap in cases: + results[name] = certify(profile, lo, hi, beta, gap) + mutations = { + 'no crossing': (F('0.998'), F('0.999'), beta, gap), + 'unfunded mirror': (lo, hi, F(0), gap), + 'false derivative': (lo, hi, beta, F(100)), + } + for label, args in mutations.items(): + try: + certify(profile, *args) + except ValueError as error: + expected = {'no crossing': 'root sign crossing', + 'unfunded mirror': 'uniform mirror inequality', + 'false derivative': 'positive crossing derivative'}[label] + require(str(error) == expected, 'unexpected control rejection') + rejected[name+': '+label] = str(error) + else: + raise ValueError('accepted root-application mutation: '+label) + # Retain the predecessor's actual geometry, tails, logarithmic power, + # concavity constant, cutoff, and U/V/Q/d guards. The root replaces its + # strict base exponent; cover endpoints and the p7 beta are explicit. + previous = original[name] + witness = {key: previous[key] for key in + ('a', 'b', 'height_base', 'ell0', 's', 'lambda', 'p', 'c')} + witness['guards'] = {key: previous['guards'][key] + for key in ('U', 'V', 'Q', 'd', 'beta')} + witness['upper_exponent'] = '.997483' if name == 'p7' else '.997067' + if name == 'p7': + witness['guards']['beta'] = '.322' + results[name]['critical_majorant'] = critical_guards(profile, lo, hi, witness) + defects = { + 'concavity': ('c', '1', 'critical concavity'), + 'tangent cover': ('ell0', 1, 'critical tangent cover'), + 'underfunded logarithm': ('p', str(F(witness['p'])/100), 'critical recurrence funding'), + } + for label, (key, value, expected) in defects.items(): + bad = dict(witness, **{key: value}) + try: + critical_guards(profile, lo, hi, bad) + except ValueError as error: + require(str(error) == expected, 'unexpected critical-guard rejection') + rejected[name+': '+label] = str(error) + else: + raise ValueError('accepted critical-guard mutation: '+label) + return {'source_sha256': PINS, 'applications': results, + 'arithmetic_controls': arithmetic_controls(), 'rejected_controls': rejected, + 'arithmetic': 'Separate exact 128-bit outward log/exp intervals; no producer execution.'} + + +if __name__ == '__main__': + print(json.dumps(run(Path(__file__).resolve().parents[2]), sort_keys=True, indent=2)) diff --git a/research/adaptive-gate-existence/verify.py b/research/adaptive-gate-existence/verify.py new file mode 100644 index 0000000000..418df3a5f5 --- /dev/null +++ b/research/adaptive-gate-existence/verify.py @@ -0,0 +1,338 @@ +#!/usr/bin/env python3 +"""Exact adaptive gate witnesses; Dillon with OpenAI Codex. Apache-2.0. + +No predecessor executable is imported. Finite checks are not a proof kernel. +""" +from fractions import Fraction as F +from functools import lru_cache +from pathlib import Path +import hashlib +import json + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def iroot(n, q): + """Floor q-th root, checked against its defining inequalities.""" + require(n >= 0 and q > 0, "invalid root") + lo, hi = 0, 1 << ((n.bit_length() + q - 1) // q) + while hi - lo > 1: + mid = (lo + hi) // 2 + if mid ** q <= n: + lo = mid + else: + hi = mid + require(lo ** q <= n < (lo + 1) ** q, "root bracket") + return lo + + +@lru_cache(None) +def power(x, t): + """Rational interval for positive integer x raised to rational t.""" + t = F(t) + require(x >= 1, "positive rank required") + if t < 0: + low, high = power(x, -t) + return 1 / high, 1 / low + if t.denominator == 1: + value = F(x ** t.numerator) + return value, value + scale = 2 ** 72 + radicand = x ** t.numerator * scale ** t.denominator + lower = iroot(radicand, t.denominator) + if lower ** t.denominator == radicand: + return F(lower, scale), F(lower, scale) + return F(lower, scale), F(lower + 1, scale) + + +def add(*intervals): + return sum((x[0] for x in intervals), F(0)), sum((x[1] for x in intervals), F(0)) + + +def mul(x, y): + require(x[0] >= 0 and y[0] >= 0, "nonnegative intervals required") + return x[0] * y[0], x[1] * y[1] + + +def div(x, y): + require(y[0] > 0, "positive denominator required") + return x[0] / y[1], x[1] / y[0] + + +def scale(x, c): + return mul(x, (F(c), F(c))) + + +@lru_cache(None) +def log_int(x): + """atanh series after exact binary range reduction; rational tail bound.""" + require(x >= 1, "log domain") + exponent = x.bit_length() - 1 + y = F(x, 2 ** exponent) + + def series(z): + # 0 <= z <= 1/3; omitted denominators are at least 2N+1. + n = 80 + low = 2 * sum(z ** (2 * j + 1) / (2 * j + 1) for j in range(n)) + tail = 2 * z ** (2 * n + 1) / ((2 * n + 1) * (1 - z * z)) + return low, low + tail + + return add(scale(series(F(1, 3)), exponent), series((y - 1) / (y + 1))) + + +def exp_lower(x): + require(x >= 0, "nonnegative exponential argument") + term = total = F(1) + for j in range(1, 81): + term *= x / j + total += term + return total + + +def moment(profile, t): + return add(*(scale(power(k, t), count) for k, count in profile.items())) + + +def mean(profile, t): + numerator = add(*(scale(mul(power(k, t), log_int(k)), count) + for k, count in profile.items())) + return div(numerator, moment(profile, t)) + + +def windows(targets, paid): + """Every mirror window is left-open/right-closed, including endpoints.""" + points = sorted({F(1, k) for k in targets} | {F(1, r) for r in paid}) + result = [] + for left, right in zip(points, points[1:]): + z = (left + right) / 2 + sources, exits = [], [] + for k, w in targets.items(): + for r, count in paid.items(): + if k > r and F(1, k) < z <= F(1, r): + sources.append((r * k, w * count)) + if r > k and F(1, r) < z <= F(1, k): + exits.append((r * k, w * count)) + result.append((left, right, sources, exits)) + return result + + +def sum_terms(terms, t): + return add(*(scale(power(rank, t), count) for rank, count in terms)) + + +def log_factors(value): + """Exact formal logarithm of a positive rational, in prime-log coordinates.""" + value = F(value) + answer = {} + for n, sign in ((value.numerator, 1), (value.denominator, -1)): + divisor = 2 + while divisor * divisor <= n: + while n % divisor == 0: + answer[divisor] = answer.get(divisor, 0) + sign + n //= divisor + divisor += 1 + if n > 1: + answer[n] = answer.get(n, 0) + sign + return {p: e for p, e in answer.items() if e} + + +def mirror_integrals(targets, paid): + """Exact symbolic checks of both new integral identities at t=1/2.""" + t = F(1, 2) + lhs_log, rhs_log = {}, {} + lhs_rank = F(0) + + def accumulate(out, weight, value): + for prime, coefficient in log_factors(value).items(): + out[prime] = out.get(prime, F(0)) + weight * coefficient + + for left, right, sources, exits in windows(targets, paid): + slo, shi = sum_terms(sources, t) + elo, ehi = sum_terms(exits, t) + require(slo == shi and elo == ehi, 'exact square-rank integral fixture') + weight = slo - elo + accumulate(lhs_log, weight, right / left) + lroot, rroot = power(left.denominator, t), power(right.denominator, t) + require(lroot[0] == lroot[1] and rroot[0] == rroot[1], 'exact endpoints') + lhs_rank += 2 * weight * (lroot[0] - rroot[0]) + for k, w in targets.items(): + for r, count in paid.items(): + coefficient = power(k * r, t) + require(coefficient[0] == coefficient[1], 'exact pair coefficient') + accumulate(rhs_log, w * count * coefficient[0], F(k, r)) + clean = lambda row: {p: v for p, v in row.items() if v} + require(clean(lhs_log) == clean(rhs_log), 'mirror log-integral identity') + T, P = moment(targets, t)[0], moment(paid, t)[0] + rhs_rank = (P * moment(targets, F(1))[0] - T * moment(paid, F(1))[0]) / (1 - t) + require(lhs_rank == rhs_rank, 'mirror rank-integral identity') + return {'log_integral_prime_coefficients': {str(p): str(v) for p, v in clean(lhs_log).items()}, + 'rank_integral': str(lhs_rank)} + + +def certify(witness): + targets = {int(k): v for k, v in witness['targets'].items()} + paid = {int(k): v for k, v in witness['paid'].items()} + require(targets and paid and min(targets) >= 2, "target domain") + require(all(isinstance(v, int) and v > 0 for v in [*targets.values(), *paid.values()]), + "positive multiplicities") + m = max(targets) + require(min(paid) >= 1 and max(paid) < m, "paid ranks must descend") + t0, thi = F(witness['root']), F(witness['upper_exponent']) + require(0 < t0 < thi < 1, "exponent domain") + a, b, M = (witness[k] for k in ('a', 'b', 'M')) + require(all(type(x) is int for x in (a, b, M)) and a > 0 and b > 0 and M > 1, + "integer geometry") + s, lam = F(witness['s']), F(witness['lambda']) + require(s > 0 and lam > 0, "positive tails") + g = a + b + T0, P0 = moment(targets, t0), moment(paid, t0) + require(T0[0] == T0[1] == P0[0] == P0[1], "exact moment crossing") + d = F(witness['d']) + require(d > 0 and mean(targets, t0)[0] - mean(paid, thi)[1] >= d, + "uniform positive crossing derivative") + # Tilted means are nondecreasing; rank >=1 makes all moments monotone. + target_forward = div(moment(targets, t0 + s), moment(targets, t0))[0] + paid_forward = div(moment(paid, thi + s), moment(paid, thi))[1] + require(target_forward >= paid_forward, "uniform forward ordering") + ut = div(moment(targets, thi + s), moment(targets, thi))[1] + up = div(moment(paid, thi + s), moment(paid, thi))[1] + U = power(M, -s)[1] * ut ** a * up ** b + V = power(M, lam)[1] * div(moment(targets, thi - lam), P0)[1] ** g + Q = div(moment(targets, thi), P0)[1] + require(U < 1, "mixed tail") + require(V < 1, "root tail") + beta = F(witness['beta']) + eta = t0 * power(m, t0 - 1)[0] + require(0 <= beta < eta < 1, "strict mirror slack") + mirror = [] + for left, right, sources, exits in windows(targets, paid): + ehi, slo = sum_terms(exits, thi)[1], sum_terms(sources, t0)[0] + require(ehi <= beta * slo, "uniform mirror window") + mirror.append({'left': str(left), 'right': str(right), + 'source_pairs': len(sources), 'exit_pairs': len(exits)}) + p, c = F(witness['p']), F(witness['c']) + ell = witness['ell0'] + require(type(ell) is int and p > 0 and c >= p / (1 - t0) and ell >= 1, + "concavity/base parameters") + logn0 = add(log_int(m), scale(log_int(M), ell)) + tauhi = t0 + p / (c + logn0[0]) + require(tauhi <= thi, "local tangent exponent cover") + denominator = c + log_int(m)[1] + (ell + 1) * log_int(M)[1] + log_int(2)[1] + exponent = d * p * (a * ell + 1) / denominator + lower = (1 - U ** ell) * (exp_lower(exponent) - 1) - Q * power(M, lam)[1] * V ** ell + threshold = (1 - eta) / (eta - beta) + require(lower >= threshold, "funded critical recurrence") + + def bracket(x, digits=6): + factor = 10 ** digits + low = x.numerator * factor // x.denominator + return [str(F(low, factor)), str(F(low + 1, factor))] + + return {'root_moment': str(T0[0]), 'uniform_d': str(d), + 'U_upper_bound': bracket(U), 'V_upper_bound': bracket(V), + 'Q_upper_bound': bracket(Q), + 'beta': str(beta), 'eta_min': str(eta), + 'tau_n0_upper': bracket(tauhi), 'D_lower': bracket(lower), + 'required_D': str(threshold), 'mirror_windows': mirror, + 'mirror_integral_controls': mirror_integrals(targets, paid), + 'n0': f'{m}*{M}^{ell}', + 'scope': 'Exact finite sufficient guards; no native profile or outer admission.'} + + +def controls(witness): + mutations = { + 'root equality': {'root': '65/128'}, + 'derivative': {'d': '100'}, + 'mixed tail': {'M': 16}, + 'root tail': {'M': 2 ** 32}, + 'mirror capacity': {'beta': '1/8'}, + 'mirror window': {'beta': '0'}, + 'tangent cover': {'ell0': 1}, + 'concavity': {'c': '1'}, + 'critical funding': {'p': '1'}, + } + rejected = {} + for name, changes in mutations.items(): + try: + certify(dict(witness, **changes)) + except ValueError as error: + rejected[name] = str(error) + else: + raise ValueError('accepted mutation: ' + name) + for base in (1, 2, 4, 81, 256): + for exponent in (F(-3, 4), F(0), F(1, 4), F(1, 2), F(33, 64)): + lo, hi = power(base, exponent) + p, q = exponent.numerator, exponent.denominator + exact_power = F(base) ** p + require(lo ** q <= exact_power <= hi ** q, 'power enclosure control') + # This exact crossing has a genuinely uncovered boundary window. + invalid = windows({4: 1, 16: 1}, {9: 2}) + require(any(sum_terms(e, F(1, 2))[0] > 0 and not s for _, _, s, e in invalid), + 'zero-source boundary control') + return rejected + + +def counterexample(): + """Fixed-exponent surplus, mean separation AND mirror slack are insufficient.""" + targets, paid, t = {4: 4, 64: 17}, {1: 4, 16: 1}, F(1, 2) + require(moment(targets, t) == (144, 144), 'counterexample target moment') + require(moment(paid, t) == (8, 8), 'counterexample paid moment') + require(mean(targets, t)[0] > mean(paid, t)[1], 'counterexample mean gap') + ratios = [] + for left, right, sources, exits in windows(targets, paid): + source, exit_ = sum_terms(sources, t), sum_terms(exits, t) + require(source[0] == source[1] and exit_[0] == exit_[1], 'exact mirror values') + require(source[0] > 0 or exit_[0] == 0, 'unfunded counterexample cell') + ratios.append(exit_[0] / source[0] if source[0] else F(0)) + # Independent endpoint classification must equal each cell's interior. + at_source, at_exit = [], [] + for k, w in targets.items(): + for r, count in paid.items(): + if k > r and F(1, k) < right <= F(1, r): + at_source.append((k * r, w * count)) + if r > k and F(1, r) < right <= F(1, k): + at_exit.append((k * r, w * count)) + require(at_source == sources and at_exit == exits, 'mirror endpoint convention') + beta = max(ratios) + eta = t * power(64, t - 1)[0] + require(beta == F(1, 17) < eta == F(1, 16), 'counterexample mirror gap') + # The single k=4 term alone gives equality at h=log4; the k=64 term + # makes the true root-tail expression strictly larger. Jensen supplies + # h>log4 from u<1. These arithmetic checks support the written all-lambda proof. + require(4 * power(4, t)[0] / moment(paid, t)[0] == 1, 'obstruction coefficient') + for lam in (F(1, 2), F(1), F(3, 2), F(2)): + lower = power(4, lam)[0] * moment(targets, t - lam)[0] / 8 + require(lower > 1, 'root-tail obstruction fixture') + return {'targets': targets, 'paid': paid, 't': str(t), 'T': 144, 'P': 8, + 'q': 18, 'beta': str(beta), 'eta': str(eta), + 'mirror_integral_controls': mirror_integrals(targets, paid), + 'scope': 'The written Jensen/single-term proof excludes every positive tail geometry.'} + + +def main(): + package = Path(__file__).resolve().parent + root = package.parent.parent + sources = json.loads((package / 'SOURCES.json').read_text()) + for row in sources['files']: + if row['usage'] == 'input': + digest = hashlib.sha256((root / row['path']).read_bytes()).hexdigest() + require(digest == row['sha256'], 'changed frozen input: ' + row['path']) + witness = json.loads((package / 'WITNESS.json').read_text()) + result = certify(witness) + result['rejections'] = controls(witness) + result['counterexample'] = counterexample() + # Compile the package-local checker directly: isolated Python omits this + # directory from sys.path, and direct source loading avoids cached bytecode. + application_path = package / 'root_application.py' + namespace = {'__file__': str(application_path), '__name__': 'root_application'} + exec(compile(application_path.read_bytes(), str(application_path), 'exec'), namespace) + result['retained_profile_applications'] = namespace['run'](root) + result['status'] = 'PASS_EXACT_ADAPTIVE_GATE_WITNESS' + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == '__main__': + main() From 644607ba59ebe401ac7ecd627ae7f331f924d1b0 Mon Sep 17 00:00:00 2001 From: Dillon Date: Wed, 21 Oct 2026 23:58:49 -0400 Subject: [PATCH 2/4] Record offline verification and upstream CI planning limitation --- research/adaptive-gate-existence/TASK.json | 26 +++++++++++++++++-- .../adaptive-gate-existence/VALIDATION.md | 16 ++++++++++++ 2 files changed, 40 insertions(+), 2 deletions(-) diff --git a/research/adaptive-gate-existence/TASK.json b/research/adaptive-gate-existence/TASK.json index fcbd91c705..6fa19dd0c3 100644 --- a/research/adaptive-gate-existence/TASK.json +++ b/research/adaptive-gate-existence/TASK.json @@ -135,7 +135,29 @@ "semantic_rejections": 21, "root_application_arithmetic_controls": 48, "proof_review": "Separate author-side AI reviews of the theorem, exact feasibility lemma, mirror integrals, arithmetic enclosures and unknown-root quantitative guards; no formal or independent human review.", - "native_and_outer_replays": "not run; source inventories and contracts inherited" + "native_and_outer_replays": "not run; source inventories and contracts inherited", + "scientific_commit": "1a623ad2c268b2b23878bc0cc3cf0f67b4b1b5fa", + "committed_bytes_and_source_history": "PASS; 15 files, canonical base reachable", + "checked_export": "PASS; 15 files", + "offline_replay": "PASS; exported tree without Git, PATH=/nonexistent, macOS sandbox-exec deny network*, Python 3.12.15 -I -O -B", + "exported_mutation_controls": "PASS; changed predecessor rejected before evaluation, underfunded logarithm rejected by recurrence guard" }, - "verification_started_utc": "2026-10-22T03:54:13Z" + "verification_started_utc": "2026-10-22T03:54:13Z", + "publication_checkpoint": { + "canonical_main": "f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc", + "checked_at_utc": "2026-10-22T03:56:15Z", + "priority_revision": 7, + "guidance_and_selection": "unchanged", + "open_pr_bodies": 316, + "discussion_records": 3411, + "remote_pagination_complete": true, + "overlap_result": "Only own claim/local package match gate existence, critical-root and mirror integral; relevant predecessor #4483 head unchanged and merged." + }, + "hosted_ci_context": { + "status": "shared upstream planning failures known before submission", + "evidence": "https://github.com/CrocSwap/integer-mult-bounds/actions/runs/39716553034/job/119619920401", + "prior_report": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4443#discussioncomment-19109289", + "cause": "Four unchanged test_research_current_status failures: stale CI target, decimal bold format, historical banner and heading. Affected blobs match canonical main. Six focused local tests reproduce four failures.", + "package_replay": "local registered replay passes; previous PR hosted replay was skipped. New PR status must be checked separately." + } } diff --git a/research/adaptive-gate-existence/VALIDATION.md b/research/adaptive-gate-existence/VALIDATION.md index 80e99fa4fb..e8c86cf58d 100644 --- a/research/adaptive-gate-existence/VALIDATION.md +++ b/research/adaptive-gate-existence/VALIDATION.md @@ -54,6 +54,11 @@ python3 scripts/export_research_package.py check /tmp/adaptive-gate-existence.ta The direct verifier consumes only package files and the six declared inputs; it requires neither Git nor network access. The generic registered runner separately needs Git history to authenticate historical card/source provenance. +A 15-file export from scientific commit +`1a623ad2c268b2b23878bc0cc3cf0f67b4b1b5fa` passed integrity and direct +Python 3.12.15 replay with `PATH=/nonexistent` under a macOS per-process +`deny network*` policy. Changed predecessor bytes and an underfunded logarithm +were rejected in copied exports; original inputs stayed unchanged. Final publication results are recorded in `TASK.json`. ## Remaining obligations @@ -64,3 +69,14 @@ restoration, chronological divisible widths, movement, precision, stock, fixed-tape execution, analytic transfer and exact recovery remain inherited. The result is a conditional leaf-count theorem with explicit certificates; there is no new selected κ, materialized winning word or practical threshold. + +## Shared hosted-planning limitation + +The earlier #4521 [hosted run](https://github.com/CrocSwap/integer-mult-bounds/actions/runs/39716553034/job/119619920401) +stopped before package replay: four shared `test_research_current_status` +failures concerning the CI target, selected decimal formatting and historical +navigation. The affected files are byte-identical on canonical main and both +research branches; six focused local tests reproduce the same four failures. +This was already [reported for #4448](https://github.com/CrocSwap/integer-mult-bounds/discussions/4443#discussioncomment-19109289). +An upstream navigation repair and hosted rerun remain separate obligations. +The local registered pass does not imply a hosted CI pass. From cca1112d6f8e462e8df92bffa0b939b8fb73d1b4 Mon Sep 17 00:00:00 2001 From: Pierre Date: Wed, 21 Oct 2026 21:18:06 -0700 Subject: [PATCH 3/4] Certify conditional multiplication kappa 0.003020165 via critical-root transfer --- .../critical-root-multiplication/PROOF.md | 118 +++++ .../critical-root-multiplication/README.md | 32 ++ .../critical-root-multiplication/RESULT.json | 265 +++++++++++ .../critical-root-multiplication/SOURCES.json | 432 ++++++++++++++++++ .../critical-root-multiplication/TASK.json | 80 ++++ .../VALIDATION.md | 19 + .../critical-root-multiplication/VERIFY.json | 111 +++++ .../critical-root-multiplication/verify.py | 108 +++++ 8 files changed, 1165 insertions(+) create mode 100644 research/critical-root-multiplication/PROOF.md create mode 100644 research/critical-root-multiplication/README.md create mode 100644 research/critical-root-multiplication/RESULT.json create mode 100644 research/critical-root-multiplication/SOURCES.json create mode 100644 research/critical-root-multiplication/TASK.json create mode 100644 research/critical-root-multiplication/VALIDATION.md create mode 100644 research/critical-root-multiplication/VERIFY.json create mode 100644 research/critical-root-multiplication/verify.py diff --git a/research/critical-root-multiplication/PROOF.md b/research/critical-root-multiplication/PROOF.md new file mode 100644 index 0000000000..717065d140 --- /dev/null +++ b/research/critical-root-multiplication/PROOF.md @@ -0,0 +1,118 @@ +# Critical-root compilation of the joint-helper supplier + +This is a conditional consequence of the pinned source contracts, not a materialized algorithm or a claim of independent human acceptance. The companion verifier binds the numerical root, mirror, majorant, final-rank and outer certificates. Apache-2.0; substantial OpenAI Codex assistance. + +## 1. Statement and credited inputs + +Assume the all-column native, productive-owner, chronological whole-job, compact movement, semantic precision, fixed-tape, stock, analytic transfer, prime-avoidance and exact-recovery contracts retained by PR4470 and PR4483. Apply the critical-root compiler theorem of PR4532 to the unchanged PR4470 mixed profile. With the finite arithmetic certificates specified below, the retained integer-multiplication reduction admits the conditional saving + +\[ +\kappa=0.003020165. +\] + +This exceeds PR4470's declared `0.00302015` by `0.000000015`. It neither changes the raw native supplier nor strengthens its physical premises. It does not identify the critical root itself as an attainable outer exponent. + +The native supplier is PR4470 at `b9a13c1673e0e9697de410de16e8bbf3207a7363`; the arbitrary-height finite compiler is PR4483 at `fb0c208864e6b24e3473318a058aa5b2dbd5764b`; the critical-root theorem is PR4532 at `644607ba59ebe401ac7ecd627ae7f331f924d1b0`. The integer/Pascal matching construction is Jacob Alan Sussman's; the overlapping flow and logarithmic majorant are zxv's; the mirror-window method is Ryanson Jonathan's; the joint-helper native lineage retains Cinna Davis and its earlier contributors; PR4532's new critical-root argument is credited to Dillon with Codex assistance. New material here is the application and the explicit conditional bridge below. Preserve the upstream licenses and attribution. + +## 2. What remains paid and productive + +Use the exact paid and target histograms authenticated against PR4470 and the compact consumer receipt. The raw unit has ambient rank145, 10,928 productive fields, all18 full supplier calls, all15 copied-query shears, the eight owned centre jobs within every full call, and all3,360 idle jobs. The updated joint-helper histogram, not an earlier controller histogram, is authoritative. + +Each productive field has an arbitrary independent input. Each paid occurrence remains a distinct chronological request even when another request has the same rank. Owned centres and query scratch are not productive fields. No input is cloned, no scratch is reclassified as a target, no field is identified with another field, and no scalar correction or idle job is dropped. + +Write +\[ +T(t)=\sum_k W_k k^t,\qquad P(t)=\sum_r P_r r^t. +\] +The companion exact interval certificate isolates a simple crossing +\[ + 0.9969798340229 377/10^12 > 0`. The companion exact compiler certificate verifies the full logarithmic inequality, including `log A` and the base cutoff, at +\[ + N=2^{10^{12}}. +\] +The certificate uses `M=1024`, height multiplier `g=2`, `p=2/5`, `c=133`, and `n0=145*1024^650`, with `A=n0^(1-t_*)/(133+log n0)^(2/5)`. The exact tail/mirror certificate funds this majorant; final absorption is checked separately. It bounds `log A<20`, `(2/5)log(133+log N)<16`, and `(z-t_*)log N>754/3`. Therefore the strict logarithmic margin exceeds `646/3`, proving `L(N)0. +\] +The finite-word constants above are fixed before the outer input grows. The positive power gaps therefore absorb fixed multiplicative constants and the retained logarithmic row-stock/descriptor factors by increasing the eventual input cutoff. The superpolynomial record-fiber argument absorbs fixed-degree descriptor preparation under its existing hypothesis. Neither assertion absorbs an omitted variable-cost operation or an unpriced change of computational model. + +The actual numerical cutoff must depend on the newly instantiated constants. No explicit overall multiplication input threshold, improvement of that threshold, practical runtime gain or materialized word is claimed. + +## 6. Admission boundary + +The conditional exponent consequence follows if the generic finite-template closure contracts retained in PR4470/PR4483 apply to the fixed compiler word just described, and the companion finite root/mirror/compiler/outer certificates pass. This is the intended inherited premise, now made explicit for the changed compiler. + +PR4532 alone proves a normalized leaf majorant. It does not supply native tensor realization, physical movement, precision, stock, prime exclusions or analytic recovery. If the generic fixed-template closure premise is not established or accepted for this algorithmically expanded word, the conclusion remains a conditional parameter consequence pending that physical bridge; it cannot be promoted to an unconditional multiplication theorem. Likewise, the absence of computed gigantic constants cannot be described as a complete numerical physical audit. + +This construction preserves all source obligations and improves only the conditional exponent consequence. It does not establish global optimality, change the selected frontier automatically, or claim independent human or formal-kernel verification. diff --git a/research/critical-root-multiplication/README.md b/research/critical-root-multiplication/README.md new file mode 100644 index 0000000000..7ef785052d --- /dev/null +++ b/research/critical-root-multiplication/README.md @@ -0,0 +1,32 @@ +# Conditional multiplication κ = 0.003020165 + +Combining PR4532's critical-root compiler with PR4470's unchanged native supplier gives the conditional multiplication saving **κ = 0.003020165**, an absolute gain of **0.000000015** over PR4470's 0.00302015. This is a small compiler-and-transfer improvement, not a new geometry or a lower native paid invoice. + +The complete p16 profile remains 10,928 productive fields and 64,620 paid jobs, including all owned centres, idle jobs, copied-query shears and independent helper outputs. Its raw moment crossing is unchanged, near 0.003020165977. The new construction certifies uniform complex saving 0.0030201656 at sufficient fixed local rank `N = 2^1000000000000`, then uses a new exact outer parameter point with all 54 strict predicates and four functional guards positive. Ordinary BIT saving remains 0.0034. + +The argument first freezes a finite integer-compiled word and replaces its precision, stock, owned-space, movement and fixed-tape constants using the general finite-template closure. It does not copy the old expanded-word constants. These constants are algorithmically specified; the enormous word is not materialized. The stated local rank is not an overall multiplication input threshold or a practical speedup. + +## Evidence and reproduction + +Run Python 3.12 from the repository root: + +```sh +python3.12 -B scripts/research_package.py --package research/critical-root-multiplication --check-only +python3.12 -B scripts/research_package.py --package research/critical-root-multiplication +``` + +The registered commands replay PR4470's unchanged dependency and native gates, then check the new exact arithmetic. The native gate covers 632 arbitrary input columns in both orientations and 423 physical frame pairs, including absolute phase. The new checker authenticates sources, reruns the PR4532 arithmetic, binds its profile to PR4470, proves finite logarithmic absorption, and checks the complete outer ledger. Mutations reject a changed paid profile, a closed root gap, an unfunded logarithmic bound and κ without uniform-supplier slack. + +`PROOF.md` supplies the mathematical combination and finite physical closure argument. `RESULT.json` is a finite arithmetic certificate, not a formal proof of that argument or of the inherited hypotheses. `VALIDATION.md` records actual commands and limitations. + +## Scope and attribution + +This branch is stacked on PR4532 at `644607ba59ebe401ac7ecd627ae7f331f924d1b0`. Its predecessor files are unchanged and are not new work here. Canonical main at preparation was `f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc`. The selected record is untouched. + +Credit Dillon's PR4532 critical-root theorem; zxv's PR4483 adaptive compiler and earlier flow/majorant work; Jacob Alan Sussman's integer compiler; Ryanson Jonathan's corrected mirror method; Cinna Davis and the credited PR4470 native lineage; Dugongue's PR4479 compact-consumer analysis; and all retained BIT, physical, precision, tape and outer-ledger authors. New combination prepared for hexapode with substantial OpenAI Codex assistance. Apache-2.0. + +The native all-column lift, whole-job implementation and movement tariffs, permitted owned erasure, semantic precision, fixed-tape execution, stock, analytic decomposition, prime avoidance and exact recovery remain explicit conditional premises. No independent human review, proof-assistant acceptance, unconditional theorem or selected-frontier promotion is claimed. PR4532's own unmerged status and proof scope remain relevant. + +## Open next questions + +The fixed-profile headroom is now small. A larger improvement needs a changed native supplier or recursive interface with a complete paid/output invoice and both operator replays. Separately, the conservative finite-word bounds could be sharpened by emitting a small adaptive forest and auditing its actual widths and routes. Neither task is solved by the present exponent certificate; see `TASK.json` for their first steps and blockers. diff --git a/research/critical-root-multiplication/RESULT.json b/research/critical-root-multiplication/RESULT.json new file mode 100644 index 0000000000..7665be4201 --- /dev/null +++ b/research/critical-root-multiplication/RESULT.json @@ -0,0 +1,265 @@ +{ + "BIT_admission": { + "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" + }, + "absorption": { + "conclusion": "A*N^theta*(133+logN)^(2/5)<=N^t above this finite cutoff; physical implementation overhead not inferred", + "cost_all_larger_N_monotonicity": true, + "cost_margin_lower": "646/3", + "logA_upper": "11588535078387598648766751054204368156120388952774219/850705917302346158658436518579420528640000000000000", + "log_threshold": 1000000000000, + "margin_lower": "299725246478781048809002279469549139266283611047225781/850705917302346158658436518579420528640000000000000", + "positive_gap": "377/1000000000000", + "primary_certified_N": "2^1000000000000", + "secondary_conservative_N_cutoff": "2^2000000000000" + }, + "critical_root": { + "beta": "141/250", + "conclusion": "Unique crossing on this bracket; critical-root hypotheses hold.", + "critical_root_interval": [ + "9969798340229/10000000000000", + "996979834023/1000000000000" + ], + "derivative_floor": "1", + "endpoint_target_minus_paid": [ + [ + "-1/1000000", + "0" + ], + [ + "0", + "1/1000000" + ] + ], + "funded_mirror_cells": [ + { + "left": "1/72", + "right": "1/65", + "upper_ratio": "141309/500000" + }, + { + "left": "1/65", + "right": "1/64", + "upper_ratio": "37509/250000" + }, + { + "left": "1/64", + "right": "1/57", + "upper_ratio": "477989/1000000" + }, + { + "left": "1/57", + "right": "1/56", + "upper_ratio": "303319/1000000" + }, + { + "left": "1/56", + "right": "1/49", + "upper_ratio": "135741/250000" + }, + { + "left": "1/49", + "right": "1/48", + "upper_ratio": "187981/500000" + }, + { + "left": "1/48", + "right": "1/41", + "upper_ratio": "562811/1000000" + }, + { + "left": "1/41", + "right": "1/40", + "upper_ratio": "25767/62500" + }, + { + "left": "1/40", + "right": "1/33", + "upper_ratio": "140197/250000" + }, + { + "left": "1/33", + "right": "1/32", + "upper_ratio": "430399/1000000" + }, + { + "left": "1/32", + "right": "1/25", + "upper_ratio": "68367/125000" + }, + { + "left": "1/25", + "right": "1/24", + "upper_ratio": "220287/500000" + }, + { + "left": "1/24", + "right": "1/17", + "upper_ratio": "52779/100000" + }, + { + "left": "1/17", + "right": "1/16", + "upper_ratio": "450273/1000000" + }, + { + "left": "1/16", + "right": "1/9", + "upper_ratio": "101799/200000" + }, + { + "left": "1/9", + "right": "1/8", + "upper_ratio": "60647/1000000" + }, + { + "left": "1/8", + "right": "1/7", + "upper_ratio": "9019/500000" + }, + { + "left": "1/7", + "right": "1/5", + "upper_ratio": "3127/250000" + }, + { + "left": "1/5", + "right": "1/4", + "upper_ratio": "13237/1000000" + } + ], + "maximizing_cell": [ + "1/48", + "1/41" + ], + "mirror_upper": "562811/1000000", + "scope": "Rank-inventory admission criterion; native and outer obligations inherited.", + "source_capacity_lower": "491053/500000", + "uniform_mean_gap_lower": "521143/500000" + }, + "finite_envelope": { + "G_depth_upper": 200000000000, + "class_envelope": "C_N <= W0*(W0+P0+1)^(G_depth+1) < 2^3400000000031", + "divisible_width_bound": "B_N < C_N^N", + "full_call_centre_episodes_per_raw_unit": 144, + "height_base": 1024, + "height_multiplier": 2, + "log2_C_N_strict_upper": 3400000000031, + "owned_space_scope": "144U and1680U bound separate raw episodes, not total live scratch. Actual compiler/parking allocations require their own O ledger.", + "primary_N": "2^1000000000000", + "proof_scope": "Height/class recurrence, denominator clearing and positive-surplus occurrence inequalities are inherited proof premises. Only their displayed integer arithmetic is checked; no gigantic word or B_N is materialized.", + "raw_occurrence_bound": "U <= B_N*N/752", + "raw_paid_jobs": 64620, + "raw_productive_fields": 10928, + "raw_rank_surplus": 752, + "thin_query_episodes_per_raw_unit": 1680 + }, + "functional_checks": 4, + "kappa": "604033/200000000", + "minimum_outer_margin_above_kappa": "29969798347/100000000000000000000", + "outer_checks": 54, + "outer_parameters": { + "a": "15100827/5000000000", + "b": "6040331/2000000000", + "beta": "9999999997/10000000000", + "bit_saving": "17/5000", + "complex_uniform_saving": "3775207/1250000000", + "d": "1/10000000000", + "epsilon": "9999999999/10000000000", + "kappa": "604033/200000000", + "layout": "1/10000000000", + "q": "30201653/10000000000", + "r0": "1/100000000000", + "stop": "1/10000000000", + "tested_saving": "30201657/10000000000" + }, + "physical_bridge": "Conditional proof premise: retained native, movement, precision, stock and fixed-tape closure must apply to the fixed expanded word; this arithmetic check does not establish physical admission.", + "rejected_mutations": { + "closedrootgap": "closed root gap", + "kappa_equals_uniform": "raw kappa lacks uniform slack", + "log_absorption_failure": "log absorption derivative", + "nativeprofile": "native profile altered" + }, + "retained_root_applications_replayed": [ + "p7", + "p16" + ], + "source_sha256": { + "research/adaptive-gate-existence/PROOF.md": "340d637feef40f44a808c718207c0fede12cc483e2c979b86c56bb736b9c1ef5", + "research/adaptive-gate-existence/SOURCES.json": "ca5f833fd92acd6fac36fef73692550f4250b39f24760840e72b5868884048d9", + "research/adaptive-gate-existence/WITNESS.json": "f1fa3d91efe8fb32e038941776f9db54a6d935eeb2b28bd2b3168aa8f70251e4", + "research/adaptive-gate-existence/root_application.py": "e656ef12f73a8dd3bdb256eca95a712de1269facb18a652fc4068ba718619b4d", + "research/adaptive-gate-existence/verify.py": "9f0c0fbddbba2d9c38a73097db911fc5cdacf8ea1d182e037f4779577dca253a", + "research/compact-joint-compiler/PROOF.md": "3f337fba12288d3b5e51af9541e2a645f79c8668fabf48b212672285fe6150b4", + "research/compact-joint-compiler/arithmetic/RESULT.json": "a6caaa2a6d6460a8c1ef7e48c4853bb27976be33a52b96a4216dfa90d96c9091", + "research/direct-mixed-flow/README.md": "78351e2419eb1ff1d645addd411158b91b381b23a962a91b6deeebeacd5192a8", + "research/fresh-helper-boundary/ARITHMETIC-RESULT.json": "5d25fec9ac4b036c93846a50dccfa4af030e2982f5cec02e28702193bf157cf7", + "research/fresh-helper-boundary/CHANGES.json": "cde73b8ff5b3c0d06e69e2293b991b24fd14a16dd4ccab7ff6b3439074a94624", + "research/fresh-helper-boundary/NATIVE-RESULT.json.gz": "37d0848458b289eb50271c47adef6e74014ae30be6363d09394b2337b566b839", + "research/fresh-helper-boundary/RESULT.json": "34163eeeef1cd712de457d7fd3b0435f98a12ac456b82256b078f33225456fbd", + "research/fresh-helper-boundary/SOURCES.json": "01998e9b86222d10811fc0114dcd5c946ff9e95025a7cacd00e67a3eefe543d0", + "research/fresh-helper-boundary/arithmetic.py": "212bae96d0ddcbc25076afe2589a47736c66b77420057f28c44c937ad087fc07", + "research/fresh-helper-boundary/native.py": "9b55a2d3c3972148fae9d112e745d9244968166bd89bd900c938f429fc76ab29", + "research/fresh-helper-boundary/verify.py": "4c18851214400cf955e10565d89357029d9e765140233831472ce23f0c3ee7bf", + "research/fresh-helper-thinned/PROOF.md": "9883b3329fef7624d3471e27bb55258cd9dc18bb6d37779a3939de99add87347", + "research/fresh-helper-thinned/README.md": "70c1c872c2327c3f71918e218d5f1ecb7a00037771a5dd1b8ae415b84cc90dc2", + "research/fresh-helper-thinned/RESULT.json": "8e7db2fed5f4be6a7f944bc59e7942ccbcc3e6c36130b5671331540c183ada21", + "research/fresh-helper-thinned/SOURCES.json": "5aec5df5096ee8a3e90618d311640b4bdfba42be5bc4bc5fab55e8be858ab2cb", + "research/fresh-helper-thinned/verify.py": "c841265ccee9b6f79045ad818ce9d27cfd7ee1f60047525a75d491f0dd8b997a", + "research/higher-moment-strictification/README.md": "ebe80b68ff026ce90f71f274c31744f4c0b36132d15ebb7e39cf2d5df4df270d", + "research/higher-moment-strictification/RESULT.json": "ad79e3c0459e7b495a0ca34010553b12147779a007389e1695cc1336f123c156", + "research/higher-moment-strictification/verify.py": "0ce7e7137422d5ffeda22085c81fa88471bbe963100fdad62e659f1e3bf89326", + "research/joint-helper-lattice/RESULT.json": "c7b2388f6511c19976b337d8c8ac374610af616866a249d75dace704eb5d9e21", + "research/joint-helper-lattice/SOURCES.json": "4045942a3b3516380c980b547e80ac254bc22e4c21c74ac16e48d3f0e46955f6", + "research/joint-helper-lattice/VERIFY.json": "1d004a782ff9d8264e4f3f6e6fbee729047ec7a24874fb03728695ef527786a8", + "research/joint-helper-lattice/native_joint.py": "50869b1bcad7493e6b4cb2a4cd5d2fd9a193a5921100483fa2c3f2c999ddfd46", + "research/joint-helper-lattice/verify.py": "8eb13f77a94315f811612cb557a17edeecb6b9d9a75dfa238b112dd6520c336f", + "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/bit-compression/carrier-reuse/reference/joint_pair_dag.py": "8a0de761642d21919e969475c3f13e5d01a4bae7343c1e1f37c586d94b676a85", + "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/sources/DATA-PHASES.json": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", + "research/kappa-causal-continuation/buffer-borrowing/verify_buffers.py": "106b4d5e052427230df452f0c901d5390a0583782960b80a8af94d9a984022c7", + "research/kappa-function-composition/complex/prune_native.py": "f2b37c183a10922eabc8e0436b426a08866430e96bd0adc7e178951c7fbb5257", + "research/kappa-rebuild/architecture/mixed_target_probe.py": "011c3c9d0cf81103dc84d709a0e36793eb7c5ae3f23c85eac27650ef13afa04a", + "research/kappa-rebuild/bit/BIT-ALLSIZE-PARAMETERS.json": "edb273f59a27356ad89f38791590c3c806b228c3510eb508e01e89f2caba95ef", + "research/kappa-rebuild/bit/BIT-P3-NATIVE-BINDING.json": "9ece46fdfda6182e757e9a3b1f513fb3d029d730f3bafdcd6ed59180a14175b0", + "research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md": "9731b93026717f5fa15851e3633cbb4bdc76eba2bffb9d6b4a3b69f7dd502443", + "research/kappa-rebuild/bit/MIXED-PRODUCTIVE-BIT.json": "2f69a19f417c0e0d141c180f9b2fae3d358391b9a230f5848ee07c45450e70bf", + "research/kappa-rebuild/bit/bit_native_binding.py": "bf6374225f388e7531fa6475cc255bd430100ff62c38d582c41601f0739de7b7", + "research/kappa-rebuild/bit/complex_controller_factor.py": "1de9aaf918e6a4f2f5448754c1f3c3da3b85e6257849ebd097af09859c4e5497", + "research/kappa-rebuild/bit/mixed_productive_bit.py": "b32291b0db7fc0d332ec444c70746ab0fb03351d2e50546f8bcb64060e3ff95e", + "research/kappa-rebuild/complex/FULL-IDENTITY.md": "c4aa88c4943ef041e9542c519b7600ecf26ed6caff92558fdb07ac88ace64c17", + "research/kappa-rebuild/complex/full-identity-certificates/RESULT.json": "943d5fad2fc529f470df05a35446e07ecaef7344abfce450d2c2eb2c9b3798f6", + "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-CANONICAL.json.gz": "6418ec3da24d548a57f5c3fe5b9062c26c9478e638504a61c387f5cfb5f4ed61", + "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz": "c54b0a3e129d28e6dbf74fa731fc3bb70fe3c6705f07256750fbecddcc842d39", + "research/kappa-rebuild/complex/native_extensions.py": "50ad007d9c386393657e86c99a96ae0a63a8fbc52872579b185002cc626e88e3", + "research/kappa-rebuild/complex/power_two_balance.py": "76929bb3887911ccf100c4593574b8a1c82ee64e96f939a8aca196869438b424", + "research/kappa-rebuild/complex/rebuild_native.py": "f94c527cc02215de49350d477618188c4c0da48bc8fb05b4e37b24c482cad7d5", + "research/kappa-rebuild/transfer-audit/FINITE-TEMPLATE-CLOSURE.md": "3f8508c63862dd83968bd30df91b08ba5afcee1e10db15ca546cdff0caef95d9", + "research/kappa-rebuild/transfer-audit/p3_native_audit.py": "5504a55a50546418d10c522984438cdeedb44993f7c1dab7bd4aa1ae0515d902", + "research/missing-join-frame/NATIVE.json.gz": "96718b257db24f4f62d3b86b36cdd514e67d2cb99947ddd7bdcb9b55a2c17841", + "research/missing-join-frame/PATCH.json": "9ab5328245ff02c9d0be21d39bcc375f50bc5d7909e9f7b9a3a9a6f812f5bd6e", + "research/missing-join-frame/PROOF.md": "50061c25d379ff5733135dbed53e8721bbd4dbee6766d1609d8a2ecdebb7dc06", + "research/missing-join-frame/RESULT.json": "25f2cbcde988847ff86f44e804982069863ec99ff68097f16e9bb7a1a17c4cd0", + "research/missing-join-frame/verify.py": "21429dd9c1b9c93ebb57e5fbb8ef674d0e4146ac8c25cc7c097c3352c02366a4", + "research/pr4359-p7-padding/P7-FACTOR.json": "6f96f6be5d8441f71cbe6ebb1657c69b543eb085b848b92b591b7ac01d6e6598", + "research/pr4359-p7-padding/TENSOR.md": "b2eba86cb979b4dc2a045f2e74bbd29e4d9e5ec87d6a2bc23ba7b54f1f58e3e3", + "research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py": "d097e55f06c3f244f2074ffd7c1a0a5f3c4b4b6a6accf9619d1dde5c0ae85e15", + "research/pr4359-p7-padding/native_inventory.py": "65539acaf45bdfe8c5aee6830f9c9b3d1107c442a60842ef803fdd7688de8f32", + "research/query-thinned-controllers/BIT-CONTROLLER.json": "39ac84fb848b908f7ba051fae4556d507900c421dc5d23501a9c0cb1d61fd08d", + "research/query-thinned-controllers/COMPLEX-CONTROLLER.json": "bf1143325d8380fab40cd5a85449f9a5412f0340deba7f4693714c92ae320088", + "research/query-thinned-controllers/RESULT.json": "6ebfc8c0f09166f4834e9d7427410cb31aefff2cd4d4ce588c8e52c9c70e9a0f", + "research/query-thinned-controllers/SOURCES.json": "74b73563d9f78a4562d376b6f33528d652e41097f65747667f112a3e1fa81d29", + "research/query-thinned-controllers/controller.py": "8b462d660487b1be4940357c4c7522967b1bfaede3c02b1c66109b85acae0fd2", + "research/query-thinned-controllers/verify.py": "07dea601d6bbaa4d90e576f20c8607c37fb01e8778c798d919fa9df435049950", + "research/rank-convergence/BENCHMARKS.json": "513efe2fe74af82891c1918e462ba8338b1bbd06403cbfcec284bcf3b4f8f850", + "research/rank-convergence/PROOF.md": "3c971c5670669cb36312815b111e64c83e1490a10ee82f5412bd9aee01e9c376", + "research/rank-convergence/README.md": "e77af882d3f02a9d3f2dd19dce889052f63892a1c8f39fdbe0813ff5fab5e8c1", + "research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962" + }, + "status": "PASS_EXACT_CONDITIONAL_PARAMETER_CERTIFICATE", + "uniform_saving": "3775207/1250000000" +} diff --git a/research/critical-root-multiplication/SOURCES.json b/research/critical-root-multiplication/SOURCES.json new file mode 100644 index 0000000000..13df2bdaf1 --- /dev/null +++ b/research/critical-root-multiplication/SOURCES.json @@ -0,0 +1,432 @@ +{ + "schema_version": 1, + "base_commit": "644607ba59ebe401ac7ecd627ae7f331f924d1b0", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40", + "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/adaptive-gate-existence/PROOF.md", + "usage": "input", + "git_blob": "bdf142f26d8b01164c9db1c021f7385a9f11a7d6", + "sha256": "340d637feef40f44a808c718207c0fede12cc483e2c979b86c56bb736b9c1ef5" + }, + { + "path": "research/adaptive-gate-existence/SOURCES.json", + "usage": "input", + "git_blob": "9260f34571b738304d02e9a2bd9c64ff9013b669", + "sha256": "ca5f833fd92acd6fac36fef73692550f4250b39f24760840e72b5868884048d9" + }, + { + "path": "research/adaptive-gate-existence/WITNESS.json", + "usage": "input", + "git_blob": "312721f956a9d7583b4758c1d1a8f3110ec6e19d", + "sha256": "f1fa3d91efe8fb32e038941776f9db54a6d935eeb2b28bd2b3168aa8f70251e4" + }, + { + "path": "research/adaptive-gate-existence/root_application.py", + "usage": "input", + "git_blob": "89d6139b63a008ad8fda0af4c92ca5dfb958eb23", + "sha256": "e656ef12f73a8dd3bdb256eca95a712de1269facb18a652fc4068ba718619b4d" + }, + { + "path": "research/adaptive-gate-existence/verify.py", + "usage": "input", + "git_blob": "418df3a5f5fde4aef0410943afc81a3317e803ef", + "sha256": "9f0c0fbddbba2d9c38a73097db911fc5cdacf8ea1d182e037f4779577dca253a" + }, + { + "path": "research/compact-joint-compiler/arithmetic/RESULT.json", + "usage": "input", + "git_blob": "514d12ce4d2d824a4e0a418022bba610c8aed8ff", + "sha256": "a6caaa2a6d6460a8c1ef7e48c4853bb27976be33a52b96a4216dfa90d96c9091" + }, + { + "path": "research/direct-mixed-flow/README.md", + "usage": "input", + "git_blob": "3be00f754b9ffa23e64b3eafe7706e3ac139993a", + "sha256": "78351e2419eb1ff1d645addd411158b91b381b23a962a91b6deeebeacd5192a8" + }, + { + "path": "research/higher-moment-strictification/RESULT.json", + "usage": "input", + "git_blob": "e66b39c674028adfd22f0de3170555dccda52f6a", + "sha256": "ad79e3c0459e7b495a0ca34010553b12147779a007389e1695cc1336f123c156" + }, + { + "path": "research/joint-helper-lattice/RESULT.json", + "usage": "input", + "git_blob": "edf41a49a0350862c23378f837c7397fc5dc7596", + "sha256": "c7b2388f6511c19976b337d8c8ac374610af616866a249d75dace704eb5d9e21" + }, + { + "path": "research/kappa-rebuild/transfer-audit/FINITE-TEMPLATE-CLOSURE.md", + "usage": "input", + "git_blob": "9917ac5543608047fd368e5e75f0851310f53584", + "sha256": "3f8508c63862dd83968bd30df91b08ba5afcee1e10db15ca546cdff0caef95d9" + }, + { + "path": "research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py", + "usage": "input", + "git_blob": "340e1f0ffb8a1a9c38fbbd9119580b6d23e01b59", + "sha256": "d097e55f06c3f244f2074ffd7c1a0a5f3c4b4b6a6accf9619d1dde5c0ae85e15" + }, + { + "path": "research/rank-convergence/BENCHMARKS.json", + "usage": "input", + "git_blob": "bc58c96abda014c28de91eca3ff10a7d4ec30b32", + "sha256": "513efe2fe74af82891c1918e462ba8338b1bbd06403cbfcec284bcf3b4f8f850" + }, + { + "path": "research/rank-convergence/PROOF.md", + "usage": "input", + "git_blob": "75f451837204bd141f357e7f5e5d6c6f42e1423e", + "sha256": "3c971c5670669cb36312815b111e64c83e1490a10ee82f5412bd9aee01e9c376" + }, + { + "path": "research/rank-convergence/README.md", + "usage": "input", + "git_blob": "b0370acf5395f128d322419a619087ef6dfd6a20", + "sha256": "e77af882d3f02a9d3f2dd19dce889052f63892a1c8f39fdbe0813ff5fab5e8c1" + }, + { + "path": "research/fresh-helper-boundary/ARITHMETIC-RESULT.json", + "usage": "input", + "sha256": "5d25fec9ac4b036c93846a50dccfa4af030e2982f5cec02e28702193bf157cf7", + "git_blob": "686c36fb19680db327f797ebdfe612487d8c53f8" + }, + { + "path": "research/fresh-helper-boundary/CHANGES.json", + "usage": "input", + "sha256": "cde73b8ff5b3c0d06e69e2293b991b24fd14a16dd4ccab7ff6b3439074a94624", + "git_blob": "45744fedd0e28967aa72586048b8bc0c72f419a9" + }, + { + "path": "research/fresh-helper-boundary/NATIVE-RESULT.json.gz", + "usage": "input", + "sha256": "37d0848458b289eb50271c47adef6e74014ae30be6363d09394b2337b566b839", + "git_blob": "e6fdb31624e4eb8c7c770bb4422cd07ea99ab152" + }, + { + "path": "research/fresh-helper-boundary/RESULT.json", + "usage": "input", + "sha256": "34163eeeef1cd712de457d7fd3b0435f98a12ac456b82256b078f33225456fbd", + "git_blob": "e26608e20be115d28f8853a8c1a12bebfc8e8ec3" + }, + { + "path": "research/fresh-helper-boundary/SOURCES.json", + "usage": "input", + "sha256": "01998e9b86222d10811fc0114dcd5c946ff9e95025a7cacd00e67a3eefe543d0", + "git_blob": "0b40275502f4263a19905f4fb50e346a3629c712" + }, + { + "path": "research/fresh-helper-boundary/arithmetic.py", + "usage": "input", + "sha256": "212bae96d0ddcbc25076afe2589a47736c66b77420057f28c44c937ad087fc07", + "git_blob": "4822f04ae09d84a16e8fa8656a533e23fd4068f0" + }, + { + "path": "research/fresh-helper-boundary/native.py", + "usage": "input", + "sha256": "9b55a2d3c3972148fae9d112e745d9244968166bd89bd900c938f429fc76ab29", + "git_blob": "1b36f6cb5f205c33bf48811e0b1b3621c55e8154" + }, + { + "path": "research/fresh-helper-boundary/verify.py", + "usage": "input", + "sha256": "4c18851214400cf955e10565d89357029d9e765140233831472ce23f0c3ee7bf", + "git_blob": "e434dbf7c68afa0390a307fd15f32348b0e87207" + }, + { + "path": "research/fresh-helper-thinned/PROOF.md", + "usage": "input", + "sha256": "9883b3329fef7624d3471e27bb55258cd9dc18bb6d37779a3939de99add87347", + "git_blob": "bf68dc2b987cb7de6431ff5e3514b60af48720a5" + }, + { + "path": "research/fresh-helper-thinned/README.md", + "usage": "input", + "sha256": "70c1c872c2327c3f71918e218d5f1ecb7a00037771a5dd1b8ae415b84cc90dc2", + "git_blob": "344616d6654a96085dd45cf2c3189ef283deeac1" + }, + { + "path": "research/fresh-helper-thinned/RESULT.json", + "usage": "input", + "sha256": "8e7db2fed5f4be6a7f944bc59e7942ccbcc3e6c36130b5671331540c183ada21", + "git_blob": "e223acd07a6b1f4f1c9f2778b8ea64d4b7a2be55" + }, + { + "path": "research/fresh-helper-thinned/SOURCES.json", + "usage": "input", + "sha256": "5aec5df5096ee8a3e90618d311640b4bdfba42be5bc4bc5fab55e8be858ab2cb", + "git_blob": "4089ad37114540b23846596e2a641c4a4bd608e2" + }, + { + "path": "research/fresh-helper-thinned/verify.py", + "usage": "input", + "sha256": "c841265ccee9b6f79045ad818ce9d27cfd7ee1f60047525a75d491f0dd8b997a", + "git_blob": "9ba85a59aa5dcc5cdaec85ee18607cb050530c55" + }, + { + "path": "research/higher-moment-strictification/README.md", + "usage": "input", + "sha256": "ebe80b68ff026ce90f71f274c31744f4c0b36132d15ebb7e39cf2d5df4df270d", + "git_blob": "0a736ca89e1eafb73a30e1f2589cc45e6b5f76c3" + }, + { + "path": "research/higher-moment-strictification/verify.py", + "usage": "input", + "sha256": "0ce7e7137422d5ffeda22085c81fa88471bbe963100fdad62e659f1e3bf89326", + "git_blob": "4b24a5096154736ce060474eb8c72dc64c303699" + }, + { + "path": "research/joint-helper-lattice/SOURCES.json", + "usage": "input", + "sha256": "4045942a3b3516380c980b547e80ac254bc22e4c21c74ac16e48d3f0e46955f6", + "git_blob": "02e8f76eab10ba009a226bbda38736de0bbda136" + }, + { + "path": "research/joint-helper-lattice/VERIFY.json", + "usage": "input", + "sha256": "1d004a782ff9d8264e4f3f6e6fbee729047ec7a24874fb03728695ef527786a8", + "git_blob": "7258f5000cabcec9cb038541fef3a38007576803" + }, + { + "path": "research/joint-helper-lattice/native_joint.py", + "usage": "input", + "sha256": "50869b1bcad7493e6b4cb2a4cd5d2fd9a193a5921100483fa2c3f2c999ddfd46", + "git_blob": "0315f80e2fdef5e0eef13e3e9b8f72066238164d" + }, + { + "path": "research/joint-helper-lattice/verify.py", + "usage": "input", + "sha256": "8eb13f77a94315f811612cb557a17edeecb6b9d9a75dfa238b112dd6520c336f", + "git_blob": "0006dd15ca5597edfa506559124d2cdf3c493ae4" + }, + { + "path": "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/bit-compression/carrier-reuse/reference/joint_pair_dag.py", + "usage": "input", + "sha256": "8a0de761642d21919e969475c3f13e5d01a4bae7343c1e1f37c586d94b676a85", + "git_blob": "8b40135a84e7f0f0cd44bed69655801310b916a7" + }, + { + "path": "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/sources/DATA-PHASES.json", + "usage": "input", + "sha256": "c5916ff312678f12aba403847643fbbc29f643acec60bdf836fa56cd3e8251fa", + "git_blob": "d9a4f84211182ca200c081ea061d724c8a2cfb70" + }, + { + "path": "research/kappa-causal-continuation/buffer-borrowing/verify_buffers.py", + "usage": "input", + "sha256": "106b4d5e052427230df452f0c901d5390a0583782960b80a8af94d9a984022c7", + "git_blob": "5a55034ec9e6185d981e16c28e1e2e455069e2cb" + }, + { + "path": "research/kappa-function-composition/complex/prune_native.py", + "usage": "input", + "sha256": "f2b37c183a10922eabc8e0436b426a08866430e96bd0adc7e178951c7fbb5257", + "git_blob": "8c3e11b2408fa96eefa3ebe7952d1b11b90b772b" + }, + { + "path": "research/kappa-rebuild/architecture/mixed_target_probe.py", + "usage": "input", + "sha256": "011c3c9d0cf81103dc84d709a0e36793eb7c5ae3f23c85eac27650ef13afa04a", + "git_blob": "4fc05ab08138218ba9f09e5c89b649afae7c914e" + }, + { + "path": "research/kappa-rebuild/bit/BIT-ALLSIZE-PARAMETERS.json", + "usage": "input", + "sha256": "edb273f59a27356ad89f38791590c3c806b228c3510eb508e01e89f2caba95ef", + "git_blob": "fbe6da7241357d89cf5c55b2e7ce2d0d046be32a" + }, + { + "path": "research/kappa-rebuild/bit/BIT-P3-NATIVE-BINDING.json", + "usage": "input", + "sha256": "9ece46fdfda6182e757e9a3b1f513fb3d029d730f3bafdcd6ed59180a14175b0", + "git_blob": "e8c5e4f077fea0bef355e6c3013c7f252d3606cf" + }, + { + "path": "research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md", + "usage": "input", + "sha256": "9731b93026717f5fa15851e3633cbb4bdc76eba2bffb9d6b4a3b69f7dd502443", + "git_blob": "a58774e237c9362869a60a22bda35be09fb85872" + }, + { + "path": "research/kappa-rebuild/bit/MIXED-PRODUCTIVE-BIT.json", + "usage": "input", + "sha256": "2f69a19f417c0e0d141c180f9b2fae3d358391b9a230f5848ee07c45450e70bf", + "git_blob": "6a139eedbc1015c13df6f2a4333e1a89b5edd18d" + }, + { + "path": "research/kappa-rebuild/bit/bit_native_binding.py", + "usage": "input", + "sha256": "bf6374225f388e7531fa6475cc255bd430100ff62c38d582c41601f0739de7b7", + "git_blob": "f4c4082d89969ea311219d9af8013082d599f6f1" + }, + { + "path": "research/kappa-rebuild/bit/complex_controller_factor.py", + "usage": "input", + "sha256": "1de9aaf918e6a4f2f5448754c1f3c3da3b85e6257849ebd097af09859c4e5497", + "git_blob": "cb0cff7c8be5f38f2ee52201d9d0907f9dfd7947" + }, + { + "path": "research/kappa-rebuild/bit/mixed_productive_bit.py", + "usage": "input", + "sha256": "b32291b0db7fc0d332ec444c70746ab0fb03351d2e50546f8bcb64060e3ff95e", + "git_blob": "9c7a8bd5d3ae4c19952648c815031858d6627b96" + }, + { + "path": "research/kappa-rebuild/complex/FULL-IDENTITY.md", + "usage": "input", + "sha256": "c4aa88c4943ef041e9542c519b7600ecf26ed6caff92558fdb07ac88ace64c17", + "git_blob": "f97a23d7d21bd7f79c9d0cb14d8c6b44fddd3f23" + }, + { + "path": "research/kappa-rebuild/complex/full-identity-certificates/RESULT.json", + "usage": "input", + "sha256": "943d5fad2fc529f470df05a35446e07ecaef7344abfce450d2c2eb2c9b3798f6", + "git_blob": "c6edcbdc43bf36bb11201235027d0ec170d07fc8" + }, + { + "path": "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-CANONICAL.json.gz", + "usage": "input", + "sha256": "6418ec3da24d548a57f5c3fe5b9062c26c9478e638504a61c387f5cfb5f4ed61", + "git_blob": "4a8c4ed26e53a72362d571c972e65aff546be784" + }, + { + "path": "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz", + "usage": "input", + "sha256": "c54b0a3e129d28e6dbf74fa731fc3bb70fe3c6705f07256750fbecddcc842d39", + "git_blob": "b46d44c6ee624968dd57be928b0c15d9d45f3b2c" + }, + { + "path": "research/kappa-rebuild/complex/native_extensions.py", + "usage": "input", + "sha256": "50ad007d9c386393657e86c99a96ae0a63a8fbc52872579b185002cc626e88e3", + "git_blob": "7f84894efc309546a903d314c7ac1473e7f594a8" + }, + { + "path": "research/kappa-rebuild/complex/power_two_balance.py", + "usage": "input", + "sha256": "76929bb3887911ccf100c4593574b8a1c82ee64e96f939a8aca196869438b424", + "git_blob": "a55ae0ce78a1861965f899a82604b276260f636c" + }, + { + "path": "research/kappa-rebuild/complex/rebuild_native.py", + "usage": "input", + "sha256": "f94c527cc02215de49350d477618188c4c0da48bc8fb05b4e37b24c482cad7d5", + "git_blob": "78a7b1b0e6e43a1347fb361f45c6e0eaff8dd27b" + }, + { + "path": "research/kappa-rebuild/transfer-audit/p3_native_audit.py", + "usage": "input", + "sha256": "5504a55a50546418d10c522984438cdeedb44993f7c1dab7bd4aa1ae0515d902", + "git_blob": "0f3a4067a4b4e20d0e6ca0f84f41851c5168f76d" + }, + { + "path": "research/missing-join-frame/NATIVE.json.gz", + "usage": "input", + "sha256": "96718b257db24f4f62d3b86b36cdd514e67d2cb99947ddd7bdcb9b55a2c17841", + "git_blob": "2f41b11d02726a60da449aaa6c603716c0310ead" + }, + { + "path": "research/missing-join-frame/PATCH.json", + "usage": "input", + "sha256": "9ab5328245ff02c9d0be21d39bcc375f50bc5d7909e9f7b9a3a9a6f812f5bd6e", + "git_blob": "f96d295d40014d4dd503f58eb3cdabcbb4b8e101" + }, + { + "path": "research/missing-join-frame/PROOF.md", + "usage": "input", + "sha256": "50061c25d379ff5733135dbed53e8721bbd4dbee6766d1609d8a2ecdebb7dc06", + "git_blob": "d240cd8e14e6d30e0e2c3d0ddcc7efa68349e24e" + }, + { + "path": "research/missing-join-frame/RESULT.json", + "usage": "input", + "sha256": "25f2cbcde988847ff86f44e804982069863ec99ff68097f16e9bb7a1a17c4cd0", + "git_blob": "e653fb4358ded67ff1539151f4b670ad9a242fb1" + }, + { + "path": "research/missing-join-frame/verify.py", + "usage": "input", + "sha256": "21429dd9c1b9c93ebb57e5fbb8ef674d0e4146ac8c25cc7c097c3352c02366a4", + "git_blob": "188135f81c9937af8232a06dc1e7b8b28260e6a8" + }, + { + "path": "research/pr4359-p7-padding/P7-FACTOR.json", + "usage": "input", + "sha256": "6f96f6be5d8441f71cbe6ebb1657c69b543eb085b848b92b591b7ac01d6e6598", + "git_blob": "04c7ef620e760cc8f1764bbf0ccd7f32c6a5bd86" + }, + { + "path": "research/pr4359-p7-padding/TENSOR.md", + "usage": "input", + "sha256": "b2eba86cb979b4dc2a045f2e74bbd29e4d9e5ec87d6a2bc23ba7b54f1f58e3e3", + "git_blob": "8ecfd3e4d0bcb449ecb1e150c4f1f4fbb39ca656" + }, + { + "path": "research/pr4359-p7-padding/native_inventory.py", + "usage": "input", + "sha256": "65539acaf45bdfe8c5aee6830f9c9b3d1107c442a60842ef803fdd7688de8f32", + "git_blob": "8d2d96e3998254c2333c43fe47cdfd074cbd811e" + }, + { + "path": "research/query-thinned-controllers/BIT-CONTROLLER.json", + "usage": "input", + "sha256": "39ac84fb848b908f7ba051fae4556d507900c421dc5d23501a9c0cb1d61fd08d", + "git_blob": "89c400d5970024b3debe870c36ce43889beed001" + }, + { + "path": "research/query-thinned-controllers/COMPLEX-CONTROLLER.json", + "usage": "input", + "sha256": "bf1143325d8380fab40cd5a85449f9a5412f0340deba7f4693714c92ae320088", + "git_blob": "39318f6ad9baf0838a274ca1042b1e3ba0e74bf9" + }, + { + "path": "research/query-thinned-controllers/RESULT.json", + "usage": "input", + "sha256": "6ebfc8c0f09166f4834e9d7427410cb31aefff2cd4d4ce588c8e52c9c70e9a0f", + "git_blob": "e0695152c98d727edfd0d2034b58a1c7e8682c0c" + }, + { + "path": "research/query-thinned-controllers/SOURCES.json", + "usage": "input", + "sha256": "74b73563d9f78a4562d376b6f33528d652e41097f65747667f112a3e1fa81d29", + "git_blob": "0f061c87ff87c43ff1ea0fc418582e9ccea3bc1d" + }, + { + "path": "research/query-thinned-controllers/controller.py", + "usage": "input", + "sha256": "8b462d660487b1be4940357c4c7522967b1bfaede3c02b1c66109b85acae0fd2", + "git_blob": "d4557e08cfb9fe57cc1ae4024705a72dc95f3583" + }, + { + "path": "research/query-thinned-controllers/verify.py", + "usage": "input", + "sha256": "07dea601d6bbaa4d90e576f20c8607c37fb01e8778c798d919fa9df435049950", + "git_blob": "f1114036fff66f57014e5c1256141fb78ff4c4a9" + }, + { + "path": "research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py", + "usage": "input", + "sha256": "2982ead07721e83358dc67c6f49c2b4c16a236a6bebdfd72f58221be1f5d0962", + "git_blob": "166841a037f069249f6f7f6dedb89248812f59e2" + }, + { + "path": "research/compact-joint-compiler/PROOF.md", + "usage": "input", + "git_blob": "5eccdd59247d3f00cfdfc4073e6fc4b224c76882", + "sha256": "3f337fba12288d3b5e51af9541e2a645f79c8668fabf48b212672285fe6150b4" + } + ] +} diff --git a/research/critical-root-multiplication/TASK.json b/research/critical-root-multiplication/TASK.json new file mode 100644 index 0000000000..41e3d6f692 --- /dev/null +++ b/research/critical-root-multiplication/TASK.json @@ -0,0 +1,80 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "644607ba59ebe401ac7ecd627ae7f331f924d1b0", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Combine the PR4532 critical-root compiler theorem with the unchanged PR4470 native profile, fresh finite-template closure constants and an exact outer point to obtain conditional kappa 0.003020165.", + "scope_change_reason": "Explicit donor assignment to improve whole conditional kappa by combining current contributions. This changes the compiler/outer admission, not the paid profile; it is not a new native hill-climbing result.", + "bottleneck_link": "The certified critical-root logarithmic majorant releases compiler slack that the previous whole-kappa point did not use.", + "budget_minutes": 60, + "stop_rule": "Publish only after pinned critical-root replay, unchanged native and BIT dependency gates, finite logarithmic absorption, full outer ledger and independent review of the conditional finite-template bridge pass.", + "outcome": "completed", + "evidence": "PROOF.md, RESULT.json, registered native/dependency/arithmetic gates; VALIDATION.md records actual runs.", + "author": "hexapode, with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance: root and three agents developed and independently checked arithmetic, source bindings and the conditional proof. No formal-kernel or independent human review.", + "open_questions": [ + { + "question": "Can a changed native supplier improve beyond the fixed p16 moment crossing?", + "why_it_matters": "The present step uses remaining compiler slack and leaves the raw profile ceiling unchanged.", + "first_step": "Specify a changed operator or recursive interface, price all independent outputs and native work, then replay both orientations.", + "blocked_by": "No verified improved native profile is supplied here." + }, + { + "question": "Can the fixed compiled word obtain a smaller explicit physical threshold?", + "why_it_matters": "The enormous local rank is sufficient, not practical, and all finite constants need fresh accounting.", + "first_step": "Instantiate a small adaptive forest and compare actual divisible widths and charged routes with the conservative bounds in PROOF.md.", + "blocked_by": "The winning near-root word is not materialized." + } + ] +} diff --git a/research/critical-root-multiplication/VALIDATION.md b/research/critical-root-multiplication/VALIDATION.md new file mode 100644 index 0000000000..8006add16e --- /dev/null +++ b/research/critical-root-multiplication/VALIDATION.md @@ -0,0 +1,19 @@ +# Validation and limits + +Environment: Python 3.12 on macOS. This package was prepared on exact PR4532 head `644607ba59ebe401ac7ecd627ae7f331f924d1b0`; canonical main was `f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc`. + +Completed: + +- PR4532's exact registered arithmetic witness, including the p16 root application; all pinned source bytes matched and its p16 invoice matched PR4470. +- Fresh PR4470 `verify.py --part dependencies`: retained native query interfaces and ordinary BIT admission 0.0034 passed. +- Fresh PR4470 `verify.py --part native`: both 632-column arbitrary-input replays and all 423 new/helper physical frame pairs passed. +- `scripts/research_package.py --package research/critical-root-multiplication --check-only`: metadata and pins passed. +- The complete registered package command: dependency, native and new arithmetic gates passed in sequence, ending `PASS_REGISTERED_RESEARCH_PACKAGE research/critical-root-multiplication outcome=completed`. +- New arithmetic authoring/default comparison under `-I -O -B`; explicit rejection checks remain active with assertions disabled. +- Separate author-side agents checked the source-bound moment, finite logarithmic absorption, full outer ledger and conditional finite-template proof. This is AI-assisted cross-checking, not independent human review. + +A final source-manifest strengthening and explicit finite-envelope arithmetic were added after the full replay. They do not change the native word or dependency implementation. The final metadata and arithmetic checks are repeated; the unchanged heavy gates are not rerun merely for those additions. + +The finite arithmetic does not prove PR4532's theorem, the general finite-template closure theorem or the inherited native, physical, analytic and recovery premises. The proof explicitly assumes those contracts. The winning finite word and its enormous constants are algorithmically specified rather than materialized. No overall numerical multiplication threshold, practical speedup, formal proof or selected-frontier admission is claimed. + +Hosted CI has not been asserted to pass. Predecessor submissions report upstream navigation/planning failures; local replay results must not be confused with hosted replay or scientific acceptance. diff --git a/research/critical-root-multiplication/VERIFY.json b/research/critical-root-multiplication/VERIFY.json new file mode 100644 index 0000000000..0038b456d9 --- /dev/null +++ b/research/critical-root-multiplication/VERIFY.json @@ -0,0 +1,111 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/adaptive-gate-existence/PROOF.md", + "research/adaptive-gate-existence/SOURCES.json", + "research/adaptive-gate-existence/WITNESS.json", + "research/adaptive-gate-existence/root_application.py", + "research/adaptive-gate-existence/verify.py", + "research/compact-joint-compiler/PROOF.md", + "research/compact-joint-compiler/arithmetic/RESULT.json", + "research/direct-mixed-flow/README.md", + "research/fresh-helper-boundary/ARITHMETIC-RESULT.json", + "research/fresh-helper-boundary/CHANGES.json", + "research/fresh-helper-boundary/NATIVE-RESULT.json.gz", + "research/fresh-helper-boundary/RESULT.json", + "research/fresh-helper-boundary/SOURCES.json", + "research/fresh-helper-boundary/arithmetic.py", + "research/fresh-helper-boundary/native.py", + "research/fresh-helper-boundary/verify.py", + "research/fresh-helper-thinned/PROOF.md", + "research/fresh-helper-thinned/README.md", + "research/fresh-helper-thinned/RESULT.json", + "research/fresh-helper-thinned/SOURCES.json", + "research/fresh-helper-thinned/verify.py", + "research/higher-moment-strictification/README.md", + "research/higher-moment-strictification/RESULT.json", + "research/higher-moment-strictification/verify.py", + "research/joint-helper-lattice/RESULT.json", + "research/joint-helper-lattice/SOURCES.json", + "research/joint-helper-lattice/VERIFY.json", + "research/joint-helper-lattice/native_joint.py", + "research/joint-helper-lattice/verify.py", + "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/bit-compression/carrier-reuse/reference/joint_pair_dag.py", + "research/kappa-0023-productive-jobs/dependencies/kappa-next-regime/direct-decoder/sources/DATA-PHASES.json", + "research/kappa-causal-continuation/buffer-borrowing/verify_buffers.py", + "research/kappa-function-composition/complex/prune_native.py", + "research/kappa-rebuild/architecture/mixed_target_probe.py", + "research/kappa-rebuild/bit/BIT-ALLSIZE-PARAMETERS.json", + "research/kappa-rebuild/bit/BIT-P3-NATIVE-BINDING.json", + "research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md", + "research/kappa-rebuild/bit/MIXED-PRODUCTIVE-BIT.json", + "research/kappa-rebuild/bit/bit_native_binding.py", + "research/kappa-rebuild/bit/complex_controller_factor.py", + "research/kappa-rebuild/bit/mixed_productive_bit.py", + "research/kappa-rebuild/complex/FULL-IDENTITY.md", + "research/kappa-rebuild/complex/full-identity-certificates/RESULT.json", + "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-CANONICAL.json.gz", + "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz", + "research/kappa-rebuild/complex/native_extensions.py", + "research/kappa-rebuild/complex/power_two_balance.py", + "research/kappa-rebuild/complex/rebuild_native.py", + "research/kappa-rebuild/transfer-audit/FINITE-TEMPLATE-CLOSURE.md", + "research/kappa-rebuild/transfer-audit/p3_native_audit.py", + "research/missing-join-frame/NATIVE.json.gz", + "research/missing-join-frame/PATCH.json", + "research/missing-join-frame/PROOF.md", + "research/missing-join-frame/RESULT.json", + "research/missing-join-frame/verify.py", + "research/pr4359-p7-padding/P7-FACTOR.json", + "research/pr4359-p7-padding/TENSOR.md", + "research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py", + "research/pr4359-p7-padding/native_inventory.py", + "research/query-thinned-controllers/BIT-CONTROLLER.json", + "research/query-thinned-controllers/COMPLEX-CONTROLLER.json", + "research/query-thinned-controllers/RESULT.json", + "research/query-thinned-controllers/SOURCES.json", + "research/query-thinned-controllers/controller.py", + "research/query-thinned-controllers/verify.py", + "research/rank-convergence/BENCHMARKS.json", + "research/rank-convergence/PROOF.md", + "research/rank-convergence/README.md", + "research/t74-native-fast/vendor/native/new/code/borrow/vendor/clifford/clifford_exact.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "research/joint-helper-lattice/verify.py", + "--part", + "dependencies" + ], + "timeout_seconds": 450, + "checks": "Unchanged PR4470 dependencies gate; native includes both arbitrary-input orientations and absolute phases." + }, + { + "argv": [ + "{python}", + "-B", + "research/joint-helper-lattice/verify.py", + "--part", + "native" + ], + "timeout_seconds": 450, + "checks": "Unchanged PR4470 native gate; native includes both arbitrary-input orientations and absolute phases." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Critical-root certificate, finite log absorption, complete outer ledger, source identity and semantic rejection controls; conditional proof is in PROOF.md." + } + ] +} diff --git a/research/critical-root-multiplication/verify.py b/research/critical-root-multiplication/verify.py new file mode 100644 index 0000000000..2f2cd6ca4b --- /dev/null +++ b/research/critical-root-multiplication/verify.py @@ -0,0 +1,108 @@ +"""Exact critical-root arithmetic composition. Native physical bridge is a separately stated proof premise. Apache-2.0; substantial OpenAI assistance.""" +from pathlib import Path +from fractions import Fraction as F +import json,hashlib +HERE=Path(__file__).resolve().parent;ROOT=HERE.parents[1] +def require(ok,msg): + if not ok:raise ValueError(msg) +def source(path,name): + ns={'__file__':str(path),'__name__':name};exec(compile(path.read_bytes(),str(path),'exec'),ns);return ns +ROOT_ENGINE=ROOT/'research/adaptive-gate-existence/root_application.py' +ENDPOINT=ROOT/'research/pr4359-p7-padding/dependencies/compiler-refill/endpoint.py' +NATIVE=ROOT/'research/joint-helper-lattice/RESULT.json' +COMPILER=ROOT/'research/compact-joint-compiler/arithmetic/RESULT.json' +BENCH=ROOT/'research/rank-convergence/BENCHMARKS.json' +REGISTERED=ROOT/'research/adaptive-gate-existence/verify.py' +PATHS=[ROOT_ENGINE,ENDPOINT,NATIVE,COMPILER,BENCH,REGISTERED,ROOT/'research/adaptive-gate-existence/verify.py',ROOT/'research/adaptive-gate-existence/PROOF.md',ROOT/'research/adaptive-gate-existence/WITNESS.json'] +def pins(): + manifest=json.loads((HERE/'SOURCES.json').read_text()) + live={row['path']:row for row in manifest['files'] if row['usage']=='input'} + for path in PATHS: + rel=path.relative_to(ROOT).as_posix() + require(rel in live,'undeclared executable/input: '+rel) + for rel,row in live.items(): + require(hashlib.sha256((ROOT/rel).read_bytes()).hexdigest()==row['sha256'],'changed source: '+rel) + return {rel:row['sha256'] for rel,row in live.items()} +def absorption(E,theta_lo,theta_hi,t,threshold=10**12): + require(theta_lo0,'log absorption derivative') + margin=gap*threshold-logA-p*log(c+threshold)[1] + require(margin>0,'log absorption margin') + require(2*log(2)[0]>1,'dyadic cutoff covers log threshold') + return {'log_threshold':threshold,'secondary_conservative_N_cutoff':'2^'+str(2*threshold),'logA_upper':str(logA),'margin_lower':str(margin),'positive_gap':str(gap),'conclusion':'A*N^theta*(133+logN)^(2/5)<=N^t above this finite cutoff; physical implementation overhead not inferred'} +def finite_envelope(profile): + targets={int(k):v for k,v in profile['targets'].items()} + paid={int(k):v for k,v in profile['paid'].items()} + W0=sum(targets.values());P0=sum(paid.values()) + surplus=sum(k*v for k,v in targets.items())-sum(k*v for k,v in paid.items()) + require((W0,P0,surplus)==(10928,64620,752),'finite envelope raw inventory') + require(W0<2**14 and W0+P0+1<2**17,'finite envelope branch bounds') + # N=2^H, M=1024=2^10, and retained height multiplier2. + H=10**12;G_depth=2*(H//10) + require(H%10==0 and G_depth==2*10**11,'finite envelope height arithmetic') + exponent=14+17*(G_depth+1) + require(exponent==3400000000031,'finite envelope class exponent') + return {'raw_productive_fields':W0,'raw_paid_jobs':P0,'raw_rank_surplus':surplus, + 'primary_N':'2^1000000000000','height_multiplier':2,'height_base':1024, + 'G_depth_upper':G_depth,'log2_C_N_strict_upper':exponent, + 'class_envelope':'C_N <= W0*(W0+P0+1)^(G_depth+1) < 2^3400000000031', + 'divisible_width_bound':'B_N < C_N^N', + 'raw_occurrence_bound':'U <= B_N*N/752', + 'full_call_centre_episodes_per_raw_unit':18*8, + 'thin_query_episodes_per_raw_unit':15*112, + 'owned_space_scope':'144U and1680U bound separate raw episodes, not total live scratch. Actual compiler/parking allocations require their own O ledger.', + 'proof_scope':'Height/class recurrence, denominator clearing and positive-surplus occurrence inequalities are inherited proof premises. Only their displayed integer arithmetic is checked; no gigantic word or B_N is materialized.'} +def run(profile_override=None,k_override=None,closed=False,small_threshold=False): + source_pins=pins();E=source(ROOT_ENGINE,'root_exact');O=source(ENDPOINT,'outer_exact') + # Re-execute source-bound registered arithmetic in this process; do not trust a status JSON. + import contextlib,io + registered=source(REGISTERED,'registered_adaptive');capture=io.StringIO() + with contextlib.redirect_stdout(capture):registered['main']() + require(json.loads(capture.getvalue())['status']=='PASS_EXACT_ADAPTIVE_GATE_WITNESS','registered source result') + native=json.loads(NATIVE.read_text());compiler=json.loads(COMPILER.read_text());profile=native if profile_override is None else profile_override + require(all(profile[x]==native[x]==compiler[x] for x in ['targets','paid']),'native profile altered') + retained=E['run'](ROOT) + witness=retained['applications']['p16']['critical_majorant']['parameters'] + require(witness['height_base']==1024 and witness['ell0']==650 and F(witness['c'])==133 and F(witness['p'])==F(2,5),'absorption parameters match critical majorant') + lo,hi=F('.9969798340229'),F('.9969798340230');t=F('.9969798344') + bracket=E['certify'](profile,lo,hi,F('.564'),F(1)) + absorb=absorption(E,lo,hi,hi if closed else t,1 if small_threshold else 10**12) + # Independent exact finite absorption at N=2^(10^12), retained from cost audit. + bound=1-F('.0030201659770');tl,th=E['moment'](E['histogram'](profile['targets']),bound);pl,ph=E['moment'](E['histogram'](profile['paid']),bound) + require(tl>ph,'cost refined root sign') + gap=F('.0030201659770')-(1-t);H=10**12 + require(F(E['logarithm'](2)[0],E['GRID'])>F(2,3) and F(E['logarithm'](2)[1],E['GRID'])<1,'elementary log2 bounds') + require(F(E['logarithm'](145)[1],E['GRID'])<8,'elementary log145 bound') + require(F('.003021')*(8+6500)<20 and 133+H<2**40,'cost log overhead below36') + require(F(2,3)*H>8+6500,'absorption cutoff above base') + require(gap*H*F(2,3)>36,'cost finite absorption margin') + require(gap-F(2,5)/(133+F(2,3)*H)>0,'cost all-size monotonicity') + absorb['primary_certified_N']='2^1000000000000';absorb['cost_margin_lower']=str(gap*H*F(2,3)-36);absorb['cost_all_larger_N_monotonicity']=True + k=F('.003020165') if k_override is None else k_override;d=F(1,10**10);uniform=1-t + require(k0 for v in outer['strict_checks'].values()),'outer strict inequality') + require(all(v>0 for v in outer['functional_checks'].values()),'outer functional guard') + require(all(v>k for v in outer['margins'].values()),'outer margin') + return {'status':'PASS_EXACT_CONDITIONAL_PARAMETER_CERTIFICATE','source_sha256':source_pins,'kappa':str(k),'uniform_saving':str(uniform),'critical_root':bracket,'absorption':absorb,'finite_envelope':finite_envelope(profile),'outer_parameters':O['encode'](a),'outer_checks':len(outer['strict_checks']),'functional_checks':len(outer['functional_checks']),'minimum_outer_margin_above_kappa':str(min(outer['margins'].values())-k),'BIT_admission':compiler['ordinary_BIT'],'physical_bridge':'Conditional proof premise: retained native, movement, precision, stock and fixed-tape closure must apply to the fixed expanded word; this arithmetic check does not establish physical admission.','retained_root_applications_replayed':list(retained['applications'])} +if __name__=='__main__': + result=run();tests={};p=json.loads(NATIVE.read_text());p['paid']['1']+=1 + for name,kwargs in [('nativeprofile',{'profile_override':p}),('closedrootgap',{'closed':True}),('kappa_equals_uniform',{'k_override':F('.0030201656')}),('log_absorption_failure',{'small_threshold':True})]: + try:run(**kwargs) + except ValueError as e: + expected={'nativeprofile':'native profile altered','closedrootgap':'closed root gap','kappa_equals_uniform':'raw kappa lacks uniform slack','log_absorption_failure':'log absorption derivative'}[name] + require(str(e)==expected,'unexpected rejection: '+name);tests[name]=str(e) + else:raise ValueError('mutation accepted: '+name) + result['rejected_mutations']=tests + import argparse + parser=argparse.ArgumentParser();parser.add_argument('--write',action='store_true');args=parser.parse_args() + target=HERE/'RESULT.json' + if args.write:target.write_text(json.dumps(result,indent=2,sort_keys=True)+'\n') + else:require(json.loads(target.read_text())==result,'stored RESULT mismatch') + print(result['status']) From a6d7237f697185e857090e174c23c1cb22c6563c Mon Sep 17 00:00:00 2001 From: Pierre Date: Wed, 21 Oct 2026 21:47:00 -0700 Subject: [PATCH 4/4] Clarify absorption margin evaluation points after independent audit --- research/critical-root-multiplication/README.md | 2 ++ research/critical-root-multiplication/RESULT.json | 3 +++ research/critical-root-multiplication/VALIDATION.md | 2 ++ research/critical-root-multiplication/verify.py | 4 ++++ 4 files changed, 11 insertions(+) diff --git a/research/critical-root-multiplication/README.md b/research/critical-root-multiplication/README.md index 7ef785052d..3e50c34d27 100644 --- a/research/critical-root-multiplication/README.md +++ b/research/critical-root-multiplication/README.md @@ -19,6 +19,8 @@ The registered commands replay PR4470's unchanged dependency and native gates, t `PROOF.md` supplies the mathematical combination and finite physical closure argument. `RESULT.json` is a finite arithmetic certificate, not a formal proof of that argument or of the inherited hypotheses. `VALIDATION.md` records actual commands and limitations. +Reporting clarification following Ryanson Jonathan's independent arithmetic check in PR4536: `absorption.margin_lower` is evaluated at `log(N)=10^12`, whereas `absorption.cost_margin_lower=646/3` is the conservative bound at the stated `N=2^(10^12)`. The certificate now labels both evaluation points explicitly. Neither the cutoffs, margins nor κ changed. PR4536 checks arithmetic, not the compiler theorem or physical premises. + ## Scope and attribution This branch is stacked on PR4532 at `644607ba59ebe401ac7ecd627ae7f331f924d1b0`. Its predecessor files are unchanged and are not new work here. Canonical main at preparation was `f9f85c1e4fa1e955ff39f10fca447e3e2a4e4adc`. The selected record is untouched. diff --git a/research/critical-root-multiplication/RESULT.json b/research/critical-root-multiplication/RESULT.json index 7665be4201..1c7af6e350 100644 --- a/research/critical-root-multiplication/RESULT.json +++ b/research/critical-root-multiplication/RESULT.json @@ -10,10 +10,13 @@ "absorption": { "conclusion": "A*N^theta*(133+logN)^(2/5)<=N^t above this finite cutoff; physical implementation overhead not inferred", "cost_all_larger_N_monotonicity": true, + "cost_margin_evaluation_N": "2^1000000000000", "cost_margin_lower": "646/3", "logA_upper": "11588535078387598648766751054204368156120388952774219/850705917302346158658436518579420528640000000000000", "log_threshold": 1000000000000, + "margin_evaluation_log_N": 1000000000000, "margin_lower": "299725246478781048809002279469549139266283611047225781/850705917302346158658436518579420528640000000000000", + "margin_scope": "margin_lower is evaluated at log(N)=log_threshold; cost_margin_lower is the conservative certified margin at primary_certified_N. The two margins use different cutoffs.", "positive_gap": "377/1000000000000", "primary_certified_N": "2^1000000000000", "secondary_conservative_N_cutoff": "2^2000000000000" diff --git a/research/critical-root-multiplication/VALIDATION.md b/research/critical-root-multiplication/VALIDATION.md index 8006add16e..8c299a58a8 100644 --- a/research/critical-root-multiplication/VALIDATION.md +++ b/research/critical-root-multiplication/VALIDATION.md @@ -17,3 +17,5 @@ A final source-manifest strengthening and explicit finite-envelope arithmetic we The finite arithmetic does not prove PR4532's theorem, the general finite-template closure theorem or the inherited native, physical, analytic and recovery premises. The proof explicitly assumes those contracts. The winning finite word and its enormous constants are algorithmically specified rather than materialized. No overall numerical multiplication threshold, practical speedup, formal proof or selected-frontier admission is claimed. Hosted CI has not been asserted to pass. Predecessor submissions report upstream navigation/planning failures; local replay results must not be confused with hosted replay or scientific acceptance. + +Published-head follow-up: hosted run 39721672717 failed on four unchanged current-status/navigation tests before research replay. The 77-file committed export, archive validation and extracted isolated arithmetic check passed. PR4536 independently reproduced its checked arithmetic and noted the different evaluation points of the two absorption margins. The reporting-only follow-up adds explicit cutoff labels, with unchanged numerical values and proof. Metadata/pins and isolated optimized arithmetic checks are repeated for this clarification; the unchanged native/dependency gates are not rerun. diff --git a/research/critical-root-multiplication/verify.py b/research/critical-root-multiplication/verify.py index 2f2cd6ca4b..cb5a01ef5a 100644 --- a/research/critical-root-multiplication/verify.py +++ b/research/critical-root-multiplication/verify.py @@ -82,6 +82,10 @@ def run(profile_override=None,k_override=None,closed=False,small_threshold=False require(gap*H*F(2,3)>36,'cost finite absorption margin') require(gap-F(2,5)/(133+F(2,3)*H)>0,'cost all-size monotonicity') absorb['primary_certified_N']='2^1000000000000';absorb['cost_margin_lower']=str(gap*H*F(2,3)-36);absorb['cost_all_larger_N_monotonicity']=True + # Distinguish the two independently checked cutoffs (PR4536 reporting note). + absorb['margin_evaluation_log_N']=absorb['log_threshold'] + absorb['cost_margin_evaluation_N']=absorb['primary_certified_N'] + absorb['margin_scope']='margin_lower is evaluated at log(N)=log_threshold; cost_margin_lower is the conservative certified margin at primary_certified_N. The two margins use different cutoffs.' k=F('.003020165') if k_override is None else k_override;d=F(1,10**10);uniform=1-t require(k