From 1a623ad2c268b2b23878bc0cc3cf0f67b4b1b5fa Mon Sep 17 00:00:00 2001 From: Dillon Date: Wed, 21 Oct 2026 23:55:09 -0400 Subject: [PATCH 1/2] 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/2] 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.