diff --git a/research/effective-direct-flow/LOCAL_LIMIT.md b/research/effective-direct-flow/LOCAL_LIMIT.md new file mode 100644 index 0000000000..4779c05996 --- /dev/null +++ b/research/effective-direct-flow/LOCAL_LIMIT.md @@ -0,0 +1,427 @@ +# An effective interval local limit for the historical paid law + +This is a written analytic lemma for the historical raw-p7 law used by +`research/direct-flow-exponent-gate`. It replaces the ineffective use of +Stone's interval theorem in this application by an explicit bound. It is not +a new multiplication exponent, a physical supplier, or a change to the +selected certificate. The estimates are deliberately conservative. + +Prepared for @alephnan with substantial OpenAI Codex assistance. The classical +interval approximation is due to Beurling and Selberg; the paid law and its +tilt come from the credited predecessor packages. Apache-2.0 applies to this +new proof. + +## 1. Law and finite hypotheses + +Write + +``` +P = {1:37305, 2:10695, 3:3360, 4:1530, 5:300, + 8:1464, 16:448, 32:448, 48:448}, +A = sum_r P_r r^alpha, +Pr(X=log r) = P_r r^alpha/A, +E X = a = log 5, +Z = X-a, v = E Z^2 = sigma^2, c_sigma = sigma sqrt(2 pi). +``` + +All logarithms are natural. The predecessor defines the unique tilt alpha by +the displayed mean equation and brackets it in +`[0.98981438244597, 0.98981438244599]`. The new numerical checker must verify +the following six coarse hypotheses from the literal law and that bracket: + +``` +Pr(X=0) >= 1/4, +Pr(X=log 2) >= 1/8, +Pr(X=log 3) >= 1/16, +2 <= v <= 3, +E |Z|^3 <= 5, +|Z| <= 3 almost surely. (H) +``` + +For orientation, outward rational interval calculations give the three named +probabilities in `[.289256813142,.289256813143]`, +`[.164687698721,.164687698722]`, and +`[.077288932732,.077288932733]`; the variance lies in +`[2.192503074149,2.192503074150]`, and the third absolute centered moment in +`[3.978639864753,3.978639864755]`. These displayed decimals are not substituted +for the rational checks of (H). + +The argument below applies to any finite real law satisfying (H), with atoms +at exactly `0,log 2,log 3` before centering. Other atoms are unrestricted +apart from (H). In this general statement set `a=E X`, `Z=X-a`, and +`v=E Z^2`, so that `E Z=0` is an explicit hypothesis through centering; +the special value `a=log 5` is not needed. Let `Z_n` be a sum of n +independent copies of Z, and let +`G_n` have the normal law with mean zero and variance `nv`. + +## 2. Quantitative statement + +For every integer `n >= 1296`, define + +``` +B_n = 3/sqrt(n) + sqrt(n) log(n) exp(-sqrt(n)/320), +A_n = [1+4 B_n]/log(n). +``` + +For every real x, every b>=0, and every interval I with endpoints x and x+b, +regardless of whether either endpoint is included, + +``` +sqrt(n) |Pr(Z_n in I)-Pr(G_n in I)| <= A_n + b B_n. (1) +``` + +Consequently + +``` +|sqrt(n) Pr(Z_n in I) + - b exp(-x^2/(2nv))/c_sigma| + <= A_n + b B_n + b^2/(4 sqrt(n)). (2) +``` + +At b=0 this includes both the singleton `{x}` and the empty interval. +The estimates are uniform in x. In particular, for `0<=b<=5000` and +`n>=2^100`, the right sides of both (1) and (2) are at most `2/log(n)`. +Set, symbolically, + +``` +n_LLT = 2^(10^12). +``` + +Then for every integer `n>=n_LLT`, every such interval with `b<=5000`, + +``` +|c_sigma sqrt(n) Pr(Z_n in I) + - b exp(-x^2/(2nv))| <= 10^(-8). (3) +``` + +The stronger comparison with the exact Gaussian interval integral also has +error at most `10^(-8)` after multiplication by `c_sigma sqrt(n)`. +The notation `2^(10^12)` is an exact integer expression; verification does +not allocate its decimal or binary expansion. + +## 3. The sole external analytic approximation + +Use the Fourier convention + +``` +hat f(t) = integral_R f(u) exp(-itu) du, +f(u) = (1/(2pi)) integral_R hat f(t) exp(itu) dt. +``` + +The classical Beurling--Selberg interval approximation provides real +integrable continuous functions `F_-`, `F_+`, with Fourier transforms +supported in `[-T,T]`, which bound the interval indicator from below and +above and have `L1` defects `2pi/T`. Thus, for an interval of length b, + +``` +integral |F_+-1_I| = integral |1_I-F_-| = 2pi/T, +||F_+||_1, ||F_-||_1 <= b+2pi/T. (4) +``` + +An inspected statement with precisely this bandwidth and defect is Laura +Shou, *Pointwise Weyl law for graphs from quantized interval maps*, +[arXiv:2110.15301v3, Theorem 4.1, printed page 12](https://arxiv.org/pdf/2110.15301v3). +That paper credits the classical construction and cites J. D. Vaaler, +*Some extremal functions in Fourier analysis*, Bulletin of the AMS 12 +(1985), 183--216, +[DOI 10.1090/S0273-0979-1985-15349-2](https://doi.org/10.1090/S0273-0979-1985-15349-2). +Shou includes a `1/(2pi)` normalization in the forward Fourier transform; +rescaling that transform gives the convention above without changing its +support or either spatial `L1` defect. No extremality assertion is needed. + +For completeness about endpoints, even if an interval theorem adopts +half-weight indicators at its endpoints, use its majorant for +`[x-epsilon,x+b+epsilon]` and its minorant for +`[x+epsilon,x+b-epsilon]`, with `0<2epsilon=u^2/3` on `[-1,1]` gives + +``` +|phi(t)|^2 = E cos(t(Z-Z')) <= 1-(2/3)v t^2, +|phi(t)| <= exp(-v t^2/3). (6) +``` + +Taylor's theorem, `E Z=0`, and (H) give + +``` +|phi(t)-(1-vt^2/2)| <= (5/6)|t|^3, +|exp(-vt^2/2)-(1-vt^2/2)| <= v^2 t^4/8. +``` + +Here the second bound follows from `0<=exp(-u)-1+u<=u^2/2` +for `u>=0`. Since `v<=3` and `|t|<=delta`, + +``` +|phi(t)-exp(-vt^2/2)| <= (49/48)|t|^3. +``` + +For `n>=2`, telescoping the nth powers and using (6) yields + +``` +|phi(t)^n-exp(-nv t^2/2)| + <= n(49/48)|t|^3 exp[-v(n-1)t^2/3] + <= n(49/48)|t|^3 exp(-nv t^2/6). +``` + +Using `integral_R |t|^3 exp(-ct^2) dt=1/c^2` and `v>=2`, + +``` +integral_(-delta)^delta |phi(t)^n-exp(-nv t^2/2)| dt + <= 36(49/48)/(v^2 n) + <= 147/(16n) < 10/n. (7) +``` + +## 6. Quantitative separation of the two logarithmic frequencies + +For real t write + +``` +d_2(t)=dist(t log2, 2pi Z), +d_3(t)=dist(t log3, 2pi Z), +d(t)=max(d_2(t),d_3(t)). +``` + +We prove that, when `n>=1296` and +`delta<=|t|<=T=2 log n`, + +``` +d(t) >= n^(-1/4). (8) +``` + +By symmetry assume t>0. Choose nonnegative integers p,q nearest to +`t log2/(2pi)` and `t log3/(2pi)`, respectively. If p=q=0, then +`d(t)>=t log3>=1/6>=n^(-1/4)`, using `log3>1` and `1296=6^4`. + +Otherwise unique factorization gives `2^q != 3^p`, including the cases +where only one of p,q is zero. Distinct positive integers differ by at +least one, so integration of `1/u` between them gives + +``` +|q log2-p log3| >= 1/max(2^q,3^p). +``` + +The nearest-integer bounds imply + +``` +max(q log2,p log3) + <= T log2 log3/(2pi) + (log3)/2. +``` + +Writing `e_2=t log2-2pi p`, `e_3=t log3-2pi q` shows + +``` +2pi(q log2-p log3)=e_2 log3-e_3 log2. +``` + +Consequently + +``` +d(t) >= [2pi/(sqrt(3) log6)] + exp[-T log2 log3/(2pi)]. (9) +``` + +The elementary inequalities +`log2<7/10`, `131/10`, `sqrt(3)<2`, +and `log6<2` show + +``` +log2 log3/(2pi)<1/8, +2pi/(sqrt(3)log6)>1. +``` + +Substitute `T=2 log n` into (9) to obtain (8). This argument uses an +explicit integer separation, not an ineffective irrationality or +Diophantine-approximation assertion. + +Centering does not change the characteristic-function modulus. The exact +pair expansion and the three atoms in (H) give + +``` +1-|phi(t)|^2 + = 2 sum_(i= 4 p_0 min(p_log2,p_log3)[d_2(t)^2+d_3(t)^2]/pi^2 + >= d(t)^2/(16pi^2). +``` + +We used `1-cos u>=2 dist(u,2pi Z)^2/pi^2`. Since `pi^2<10`, +`sqrt(1-u)<=exp(-u/2)`, and (8) holds, + +``` +|phi(t)| <= exp[-d(t)^2/(32pi^2)] + <= exp[-1/(320 sqrt(n))] + (delta<=|t|<=T), +|phi(t)|^n <= exp[-sqrt(n)/320]. (10) +``` + +## 7. Complete the Fourier bound + +Integration by comparison with the derivative of the Gaussian gives + +``` +integral_(|t|>delta) exp(-nv t^2/2) dt + <= 2 exp(-nv delta^2/2)/(nv delta) + <= 6 exp(-n/36)/n. +``` + +Combining this with (7), (10), and `T=2 log n` gives + +``` +D_n(T) <= 10/n + 6 exp(-n/36)/n + + 4 log(n) exp[-sqrt(n)/320] + <= 16/n + 4 log(n) exp[-sqrt(n)/320]. (11) +``` + +The smoothing term in (5) is at most `1/log n`, because +`sigma>=sqrt(2)` and `pi<4`. Also `2pi>6` and +`2pi/T=pi/log n<4/log n`. Substitution of (11) into (5), rounding +`16/6` upward to 3 and `4/6` upward to 1, proves (1). + +The Gaussian density `g_n` satisfies + +``` +sup_y |g_n'(y)| = 1/[nv sqrt(2pi e)]. +``` + +Hence replacing its integral over `[x,x+b]` by `b g_n(x)` has error at +most `b^2/[2nv sqrt(2pi e)]`. Multiplying by `sqrt(n)` and using `v>=2` +proves (2). The Gaussian assigns zero mass to endpoints, so this step +introduces no convention dependence. + +## 8. The symbolic onset used by the flow proof + +We verify the simplification to `2/log n` for `b<=5000`, `n>=2^100` +without representing huge integers. Put `w=log n`. Since `log2>2/3`, +we have `w>=200/3>60`. The right side of (2) is at most + +``` +1/w + 2^23 exp(-w/2) + + 5001 w exp(w/2) exp[-exp(w/2)/320]. (12) +``` + +Indeed `b+4/w<5001`, and +`3*5001+5000^2/4=6265003<2^23`. + +For `w>=60`, `w exp(-w/2)` decreases. The positive exponential series +gives `e^3>16`, and thus `e^30>2^40`. At w=60, + +``` +2^23 w exp(-w/2) < 60/2^17 < 1/2. +``` + +The last term of (12), multiplied by w, also decreases for `w>=60`: +its logarithmic derivative is +`2/w+1/2-exp(w/2)/640<0`. At w=60, use that +`u exp(-u/320)` decreases for `u>320`, then `e^30>2^40`, to bound it by + +``` +5001*60^2*2^40 exp(-2^40/320) + < 2^65 exp(-2^31) + < 2^(65-2^31) < 1/2. +``` + +The two remainder terms in (12) therefore sum to at most `1/w`. +This proves the stated `2/log n` bound, also for (1), whose right side is +smaller. Finally, `c_sigma<5` follows from `v<=3` and `pi<4`. For +`n>=2^(10^12)`, + +``` +c_sigma * 2/log n < 10/log n + <= 15/10^12 < 10^(-8), +``` + +which proves (3) and its Gaussian-integral version. This is a mathematical +onset certificate, not a claim that this many convolution steps were run. + +## 9. Kernel forms available to callers + +For any nonnegative bounded monotone function f on a finite interval, +extended by zero outside that interval, every positive superlevel set is +an interval. Layer-cake integration of (1) therefore gives, uniformly in +the shift c and with arbitrary consistent endpoint choices, + +``` +sqrt(n) |E f(c-Z_n)-E f(c-G_n)| + <= ||f||_infinity A_n + B_n integral_R f(u) du. (13) +``` + +The same formula applies to `f(u)=exp(-tau u)1_(u>=0)`, tau>0, by monotone +convergence of its layer-cake representation. Its bound is `A_n+B_n/tau`; +there is no necessary finite tail cutoff at this step. The Gaussian +expectation can in turn be replaced by the flat central density, with + +``` +|sqrt(n) E[exp(-tau(c-G_n))1_(c-G_n>=0)] + - 1/(c_sigma tau)| + <= [c^2/tau+2|c|/tau^2+2/tau^3]/[2nv c_sigma]. (14) +``` + +To see (14), write the expectation as the integral of +`exp(-tau u) exp[-(c-u)^2/(2nv)]/c_sigma`, and use +`0<=1-exp(-z)<=z` before integrating the three polynomial terms. + +The complement-capacity kernel in the predecessor is monotone as required +by (13). For `0=F(x)` on `(0,1)`. Therefore, +when alpha<1, + +``` +d/dy {exp(alpha y) F(c exp(-y))} + = exp(alpha y)[alpha F(x)-xF'(x)] <= 0, + x=c exp(-y). +``` + +Continuity includes the possible endpoint x=1. This explains why no +unquantified step-function approximation is needed to transfer the interval +bound to the finite source and complement windows. + +The later flow argument still has to account for its exact mixed-layer +normalizations, target sums, endpoints, geometric tails, and all source, +boundary, and leaf terms. This local-limit lemma alone is not that complete +propagation argument. Neither argument discharges physical realization or +the selected multiplication theorem's inherited assumptions. diff --git a/research/effective-direct-flow/PROOF.md b/research/effective-direct-flow/PROOF.md new file mode 100644 index 0000000000..fffb7822ed --- /dev/null +++ b/research/effective-direct-flow/PROOF.md @@ -0,0 +1,463 @@ +# An explicit all-rank majorant for the fixed-height raw-p7 flow + +This is a scoped analytic theorem about the exact scalar recurrence of +`research/direct-mixed-flow/flow.py`, with its original default height and +the historical raw-p7 inventories below. It makes the upper-bound onset in +`research/direct-flow-exponent-gate/PROOF.md` effective. It is not a new +integer-multiplication exponent, a physical supplier, or a discharge of any +of the selected result's five framework assumptions. + +## 1. Statement and exact source + +Use the literal inventories + +```text +P = {1:37305, 2:10695, 3:3360, 4:1530, 5:300, + 8:1464, 16:448, 32:448, 48:448}, +T = {5:420, 6:270, 7:840, 8:1395, 9:3195, + 25:448, 41:448, 57:448, 121:224}. +``` + +Put `m=121`, `a=log(5)`, and let `P(s)` and `T(s)` denote the corresponding +power sums. For every integer `N>=121`, use exactly +`Flow(T,P,N).merged()`, with `extra_height=0` and the default `height_base=5`. +Write its complete source histogram as `c_z` and complete exit histogram as +`d_e`, retaining every multiplicity and every unmatched boundary exit. Define + +```text +C_N = sum_z c_z, +L(0) = 0, L(n) = n for 1 <= n < 121, +L(N) = [sum_z c_z L(N-z) + sum_e d_e L(e)] / C_N for N >= 121. +``` + +The source is finite and `C_N>0`. Every source satisfies +`N/121 < z <= N`; every exit satisfies `1 <= e <= 48N/121 < N`. Thus the +recurrence is well-defined by strong induction. These facts concern the +actual default-height flow, not a modified terminal cutoff. + +**Theorem.** Set + +```text +s = 99739/100000, +n_LLT = 2^(10^12), +G_0 = 2*n_LLT + 2, +N_0 = 121 * 5^G_0. +``` + +Then the exact scalar recurrence above satisfies the explicit all-rank bound + +```text +L(n) <= N_0^(1-s) * n^s for every integer n >= 1. +``` + +The threshold is deliberately enormous. Its role is to replace an +existential onset and unspecified initial-range constant by explicit +expressions. None of these enormous integers or their associated flows +needs to be materialized to check this proof. + +The source identities used below are the complete mirror decomposition and +finite conservation identity in the pinned predecessor +`research/direct-flow-exponent-gate/PROOF.md`, sections 2 and 4, themselves +derived from the exact flow of zxv's #4436 and the mirror argument of +Ryanson Jonathan / pinterbanget's #4459. Their finite source-reading checks +are inherited, not claimed as a new independent operator audit here. +Section 2 below states the decomposition precisely so that the analytic +application is reviewable. The probability estimate is supplied and proved +separately in [LOCAL_LIMIT.md](LOCAL_LIMIT.md). + +## 2. Tilted law and the exact finite decomposition + +Let `alpha` be the unique solution of `P'(alpha)/P(alpha)=a`. Define + +```text +A = P(alpha), D = T(alpha), J = A-D, q = D/A, +Pr(X=log r) = P_r*r^alpha/A, +Pr(Y=log k) = T_k*k^alpha/D, +sigma^2 = Var(X), c_sigma = sigma*sqrt(2*pi), tau = s-alpha. +``` + +All copies of `X` and `Y` below are independent. The exact interval checks +for this package establish the following conservative inequalities: + +```text +0 < alpha < 1, a < 2, log(121) < 5, +2 < sigma^2 < 5/2, c_sigma < 4, +0 < q < 247/250, 0 < J < 2000, +tau > 3/400, P(s)/121^s < 2000. +``` + +The bound for `c_sigma` follows also from `sigma^2<5/2` and `pi<16/5`. +All numerical premises here and the strict margin in section 3 are +certified by outward rational intervals; diagnostic floating values are +not acceptance gates. + +For a fixed integer `N>=121`, put + +```text +G = floor(log_5(N/121)), +B = log(N/121) = G*a + delta, 0 <= delta < a. +``` + +`Flow` uses the integer cap `floor(N/121)`. Since every product considered +by the flow is an integer, its cap test is exactly equivalent to comparison +with `exp(B)=N/121`; no approximation to the floor is made here. + +The complete finite mirror decomposition is as follows. Ordered target and +paid words carry the product of their letter multiplicities; equal products +are combined by adding those multiplicities. + +* Root sources have ranks `k*z` for every allowed product `z` of `G` target + letters with `z<=exp(B)`, with the corresponding target-word multiplicity + multiplied by `T_k`. +* Leaf exits have ranks `r*z` for every allowed product `z` of `G` paid + letters with `z<=exp(B)`, with multiplicity multiplied by `P_r`. Every + terminal `r` is retained: the terminal leaf rank is not capped again. +* For each `h=0,...,G-1`, take a common base with `h` target letters and + `G-1-h` paid letters. If its product is `z`, each pair `(r,k)` has rank + `rkz` and multiplicity equal to the base multiplicity times `P_r T_k`. + It is an inner source when `rz<=exp(B)r`, +and the boundary window is exactly `[log k,log r)` when `r>k`. The endpoint +conventions are important at finite ranks and are retained throughout. + +For the `h`th mixed layer set + +```text +ell = G-1-h, +u_h = B - sum_(i=1)^ell X_i - sum_(j=1)^h Y_j. +``` + +For leaves set `u_leaf=B-sum_(i=1)^G X_i`. Undoing the tilt multiplies a +mixed base probability by `A^(G-1) q^h exp(-alpha*B) exp(alpha*u_h)`; +for a leaf base the factor is `A^G exp(-alpha*B) exp(alpha*u_leaf)`. + +## 3. A positive finite capacity margin is enough + +Define the dimensionless finite capacity margin + +```text +D_N(s) = sum_z c_z [1-(1-z/N)^s] - sum_e d_e (e/N)^s. +``` + +The normalized child power is + +```text +H_N(s) = [sum_z c_z (1-z/N)^s + sum_e d_e (e/N)^s] / C_N + = 1-D_N(s)/C_N. +``` + +Thus `D_N(s)>0` is exactly the inequality needed for the power majorant. +There is no need to estimate the source count or divide two approximate +limits. Root-source capacity is nonnegative because every source fits in +its parent; discarding it gives a valid lower bound for `D_N`. + +For each pair use the nonnegative kernels + +```text +f^+_(r,k)(u) = exp(alpha*u) [1-(1-(rk/121)exp(-u))^s], + log r <= u < log k, when k>r; + +f^-_(r,k)(u) = (rk/121)^s exp(-tau*u), + log k <= u < log r, when r>k. +``` + +Each is zero off its stated window. Let + +```text +f(u) = sum_(k>r) P_r T_k f^+_(r,k)(u) + - sum_(r>k) P_r T_k f^-_(r,k)(u), +g(u) = exp(-tau*u) 1_(u>=0), +F_G = A^G exp(-alpha*B) / (J*c_sigma*sqrt(G)), +B_leaf = J*P(s)/121^s < 4*10^6. +``` + +For `G>0`, the exact decomposition gives + +```text +D_N/F_G >= (1-q) sum_(h=0)^(G-1) q^h + [c_sigma*sqrt(G) E f(u_h)] + - B_leaf [c_sigma*sqrt(G) E g(u_leaf)]. (1) +``` + +The inequality in (1) discards only the nonnegative root capacity; every +boundary and leaf exit remains charged. + +Write + +```text +M = integral_R f(u) du, +D_full = M - B_leaf/tau. +``` + +This `D_full` is exactly `K(s)-V(s)` from the predecessor's section 6: +the source kernels give `K(s)`, the negative mixed kernels give its +boundary-exit integral, and `B_leaf/tau` is its full leaf-exit integral. +At `s=99739/100000`, the exact positive-binomial capacity calculation with +its proved positive tail gives + +```text +D_full > 40000. (2) +``` + +This is the only numerical limiting-margin decision needed below. + +## 4. An interval bound transfers to the kernels without a mesh + +For `0=Q_s(x)` for `0=n_LLT`, every interval with left endpoint `x` +and length `0<=b<=5000`, and every choice of open or closed endpoints, + +```text +|c_sigma*sqrt(ell) Pr(Z_ell in I) + - b exp(-x^2/(2*sigma^2*ell))| <= epsilon. (3) +``` + +It is a uniform finite-length estimate, not an asymptotic statement with +an unspecified threshold. Reflection or an atom exactly on a cap does not +require changing (3). + +Assume henceforth `G>=G_0`. In particular `G>=10^18`. Set `H=3000` and +first consider `0<=h<=H`. Then `ell=G-1-h>=G-H-1>=G/2` and +`ell>=n_LLT`. Conditional on the target sum, + +```text +u_h = v-Z_ell, +v = (h+1)a + delta - sum_(j=1)^h Y_j. +``` + +Because `a<=Y_j<5` and `0<=delta2`, and +`rho-1<=(G-ell)/ell`, the interval discrepancy after scaling by +`c_sigma*sqrt(G)` is at most + +```text +rho*epsilon + b*(rho-1) + rho*b*R^2/(4*ell) + <= 2*epsilon + [30010+5*15010^2]/G + < 2*epsilon + 2*10^9/G + < 3*10^-8. (4) +``` + +The estimate is uniform in the conditional target sum and in `delta`, so +it survives averaging over that sum. Section 4 gives + +```text +|c_sigma*sqrt(G) E f(u_h) - M| < Q*3*10^-8 < 1563. (5) +``` + +Multiplication by `(1-q)q^h` and summation over `h<=H` cannot increase +this error, since those nonnegative weights sum to at most one. + +## 6. Every later mixed layer remains accounted for + +For `H=G/2-1>=n_LLT` and +`sqrt(G/ell)<=2`. On any mixed window (3) bounds the scaled probability +mass by `2*(5+epsilon)<12`. Thus + +```text +|c_sigma*sqrt(G) E f(u_h)| <= 12Q. +``` + +The omitted part of the infinite geometric weighting of `M` has magnitude +at most `5Q q^(H+1)`. Together, the middle finite layers and this limiting +tail cost at most + +```text +17Q q^(H+1) < 17Q exp(-36) < 17Q/10^15 < 1/1000. (6) +``` + +Here `q<1-3/250` gives `q^v<=exp(-3v/250)`. The elementary integer check +`(8/3)^36>10^15`, together with `exp(1)>8/3`, proves the displayed +exponential estimate; no tiny floating number is used. + +For `h>floor(G/2)`, the paid sum can have fewer than `n_LLT` letters or +even zero letters. No local-limit estimate is invoked there. The trivial +bound `sup|f|<=Q` and `c_sigma<4` give, after summing all their weights, + +```text +tail <= 4Q sqrt(G) q^(G/2) + <= 4Q G exp(-3G/500) + <= 8Q / [(3/500)^2 G] + < 1. (7) +``` + +The penultimate step uses `exp(x)>=x^2/2`; the last is an exact rational +comparison at `G>=10^18`. Thus even the no-paid-letter end layer is covered. + +Combining (5)--(7), the full mixed sum in (1) differs from `M` by less +than `1563+1/1000+1`. + +## 7. The leaf half-line, including its entire tail + +For leaves `ell=G` and `u_leaf=delta-Z_G`. On any subinterval of +`[0,5000)`, reflection has interval length at most 5000 and left endpoint +of absolute value below 5002. Therefore (3) and `sigma^2>2` give discrepancy +from Lebesgue measure at most + +```text +epsilon + 5000*5002^2/(4G) < 5*10^-8. (8) +``` + +The function `exp(-tau*u)` is decreasing and has left-end value one. +Stieltjes integration as in section 4 bounds the error of its integral on +`[0,5000)` by the same quantity. After multiplication by `B_leaf<4*10^6`, +this contributes less than `1/5`. + +For the remaining half-line partition into intervals +`[5000+j,5001+j)`, `j>=0`. Their scaled probabilities are at most +`1+epsilon<2` by (3), uniformly in location. Hence + +```text +c_sigma*sqrt(G) E[exp(-tau*u_leaf) 1_(u_leaf>=5000)] + <= 2 exp(-5000*tau)/(1-exp(-tau)) < 3*10^-14. (9) +``` + +Indeed `tau>3/400` implies `5000*tau>37.5`, and +`exp(-37.5)<10^-16`: use `exp(1)>163/60` and the exact integer comparison +`(163/60)^37>10^16`. Also + +```text +1-exp(-tau) >= tau/(1+tau) > 3/403. +``` + +The Lebesgue tail is bounded separately: + +```text +integral_5000^infinity exp(-tau*u) du + = exp(-5000*tau)/tau < 2*10^-14. (10) +``` + +Thus the total leaf error, comparing with the *whole* limiting integral +`1/tau`, is less than + +```text +B_leaf * (5*10^-8 + 5*10^-14) < 1/5 + 2*10^-7. (11) +``` + +The terminal paid rank was already summed in `P(s)`; (9) is a log-base +tail bound and does not truncate terminal ranks. + +## 8. Uniform onset and an explicit initial-range constant + +Combining (1), (2), (5)--(7), and (11), for every integer `N` with +`G>=G_0`, uniformly in its actual offset `delta`, + +```text +D_N/F_G > D_full - 1600 > 38400 > 0. +``` + +Since `F_G>0` and `C_N>0`, this proves `H_N(s)<1`. The condition +`G>=G_0` holds for every integer `N>=N_0=121*5^G_0`, not merely a +subsequence of ranks or a favorable offset. + +It remains to make the strong-induction constant explicit. At exponent one, +the exact finite conservation identity is + +```text +sum_z c_z z - sum_e d_e e + = [T(1)-P(1)] U_N(1) + = 608 U_N(1) > 0, +``` + +where `U_N(1)` is the positive complete unit-column moment. Indeed +`P(1)=131115` and `T(1)=131723`. Therefore the complete recurrence sends the +test function `n` to at most `n`. Starting from its prescribed base values, +strong induction gives `L(n)<=n` for every `n>=0`. + +For `1<=n=N_0`, all nonzero children are smaller than `n`. Assuming the +claimed bound at those children and using `L(0)=0`, the exact recurrence +gives + +```text +L(n) <= N_0^(1-s) n^s H_n(s) <= N_0^(1-s) n^s. +``` + +This finishes the proof without evaluating any initial-rank flow below +`N_0`. It supplies a sufficient threshold, not the first successful rank +and not a practical cost estimate. + +## 9. Scope, dependencies, and credit + +The predecessor establishes the exact scalar recurrence and its limiting +exponent `s_*` in `(0.99738855928,0.99738855931)`. The result here retains +its already-proved upper exponent `0.99739`; its contribution is the explicit +all-rank onset and majorant constant. It neither improves `s_*` nor changes +the source height, source matching, boundary exits or terminal leaf rule. + +The finite identities and strict complement margin are inherited at exact +source pins and checked where declared by this package. The new universal +argument is the quantitative local-limit estimate, its finite-layer/tail +propagation above, and the explicit initial-range bound. Finite controls +corroborate these calculations; they are not a substitute for the written +analytic proof, independent human acceptance or proof-kernel verification. + +The historical raw-p7 law is not the currently selected P104 supplier. +The selected conditional `kappa=0.003125804`, its admitted BIT budget, and its +five framework assumptions are unchanged. No physical native, ownership, +precision/tape, compiler-cost or integer-recovery claim follows from this +scalar recurrence theorem. + +Credit zxv (#4436/#4483), Ryanson Jonathan / pinterbanget (#4459 and the +mirror-flow lineage), DLamdata (#6118), Nick Petalas (#6125/#6128), the +full-flow exponent contribution prepared for @CubeJerry, Cinna Davis / +1337isnot1337 and the historical p7 controller, Jacob Alan Sussman's +lockstep compiler, and the retained native/precision/analytic contributors. +The Fourier approximation used in LOCAL_LIMIT.md retains its classical +Selberg/Beurling/Vaaler attribution. This successor proof was prepared for +@alephnan with substantial OpenAI Codex assistance, including separate +derivation and adversarial review. Apache-2.0. diff --git a/research/effective-direct-flow/README.md b/research/effective-direct-flow/README.md new file mode 100644 index 0000000000..9a9b7260e5 --- /dev/null +++ b/research/effective-direct-flow/README.md @@ -0,0 +1,146 @@ +# An effective all-rank bound for the fixed-height direct flow + +**Scoped analytic theorem; no new kappa.** This answers the effective-onset +question in [#6329](https://github.com/CrocSwap/integer-mult-bounds/pull/6329) +(`research/direct-flow-exponent-gate`). For its exact historical raw-p7 scalar +recurrence, retain the original height and every source, complement, boundary +exit and terminal leaf. Set + +\[ +s=\frac{99739}{100000},\qquad +G_0=2\cdot2^{10^{12}}+2,\qquad N_0=121\,5^{G_0}. +\] + +Then, for **every integer \(n\ge1\)**, + +\[ +\boxed{L(n)\le N_0^{261/100000}\,n^{99739/100000}.} +\] + +The predecessor already proved the upper exponent 0.99739 and identified the +limiting scalar exponent. Its local-limit argument supplied no effective onset +or majorant constant. This contribution supplies both. The threshold is +deliberately enormous: it proves effectivity, not practical finite-size savings, +and is not claimed to be optimal. Verification uses its exact symbolic expression; +it does not construct that integer or run a flow of that size. + +## What closes the gap + +[LOCAL_LIMIT.md](LOCAL_LIMIT.md) proves a uniform interval local-limit estimate +with explicit error O(1/log n) for the paid law. Compact Fourier interval +majorants and minorants reduce the problem to a bounded frequency range. +The elementary integer separation of powers of 2 and 3 supplies a quantitative +gap on that range. The new implication has no ineffective irrationality constant +or appeal to qualitative convergence. Atomic endpoints are covered. + +[PROOF.md](PROOF.md) transfers this estimate through all mixed target/paid +layers and the full leaf tail. Working directly with source capacity minus +exit cost avoids dividing approximate limiting masses. The independently +checked limiting margin exceeds 40000; the explicit normalized error is below +1600. Conservation at exponent one gives L(n)<=n, which provides the +initial-range constant without enumerating the ranks below N_0. + +The classical Beurling--Selberg interval approximation is a cited theorem, +with its precise normalization and an inspected primary-paper statement in +LOCAL_LIMIT.md. The universal conclusion is a written proof, not a finite +experiment or proof-assistant theorem. [REVIEW.md](REVIEW.md) records a separate +adversarial AI review and discloses the reviewer's earlier contribution. + +## Reproduce and inspect + +From the repository root with standard-library Python 3.12: + +```sh +python3 -I -W error -B research/effective-direct-flow/verify.py +python3 -I -O -W error -B research/effective-direct-flow/verify.py +python3 -B scripts/research_package.py --package research/effective-direct-flow +python3 -I -W error -B research/effective-direct-flow/independent_checks.py +``` + +The two direct verifier commands print `PASS_EFFECTIVE_DIRECT_FLOW`. The +registered replay runs both modes, independent arithmetic controls, and source +transport checks. It authenticates five source files before +using their bytes and writes no generated artifacts. The standalone verifier +does not need Git or third-party libraries. + +The new numerical checker imports none of the predecessor's numerical engine. +It uses integer endpoints on a 2^-128 grid, with directed rounding: + +- logarithms use 80 positive atanh terms after reduction to [1,2], with + tail 2z^161/[161(1-z^2)]; +- exponentials use 48 Taylor terms after division by 16, a geometric bound + on all omitted terms, and four squarings; +- exact mean-root endpoint signs, three atom masses, variance, third + absolute moment, layer ratio and leaf decay are certified; +- 512 positive binomial terms give a **lower** bound for complete complement + capacity. Omitting the remaining positive tail is valid for this one-sided + gate. The computed interval for the truncated margin is + `[47053.890913,47053.895405]`, so the full margin is above 40000; +- small rational comparisons check the symbolic onset and complete error + budget without evaluating a huge power or a tiny floating exponential. + +Ten complete histograms at depths 0 through 3 compare an ordered-word +decomposition with the authenticated original `Flow.merged()` implementation. +Controls reject an extra terminal cap, a missing mixed layer, an insufficient +onset, and invalid arithmetic domains. These finite checks corroborate the +source binding and numerical premises; they do not prove an all-size limit. +The separate exact arithmetic audit checks 3,969 signed interval pairs and +630 signed ceiling cases against independent rational extrema. Optional +`diagnostic.py` uses an independent 90-digit Decimal implementation and direct +pairwise capacity sums; its rounded output is explicitly outside acceptance. +Exact commands, environment and source-corruption checks are recorded in +[VALIDATION.json](VALIDATION.json). + +## Sources, overlap and limitations + +Canonical base: `7c49fe32c55de02c2c873655c804b16e4c3fef0a`. +[SOURCES.json](SOURCES.json) binds the literal law, original flow and #6329 +proof/README/task by SHA256 and Git blob. The current selected record and its +review are provenance, not inputs to this historical recurrence theorem. +The source law, flow and exact mirror decomposition remain predecessor work. +No frozen source is modified. + +The final live overlap refresh (2026-11-04, 07:00--07:02 UTC) covered 663 open +PRs and 6,789 discussion records with complete remote pagination; targeted +all-state PR searches and direct reading +covered the relevant archived predecessors. Sparse local coverage was incomplete. +[#6128](https://github.com/CrocSwap/integer-mult-bounds/pull/6128) already gives +a conditional leaf-tail bound; it does not give this uniform interval estimate +or a complete recurrence onset. The stronger changed-height construction of +#4483 is a different recurrence and is not replaced here. This is a bounded +overlap survey, not a claim of literature-wide novelty. + +The selected conditional P104 result remains **kappa = 0.003125804 (#6030)**. +Its construction and review were followed and its source-binding baseline +passed before this historical side question was selected. No selected cold +replay, native supplier, physical caller bill, ownership/erasure proof, +precision/tape proof, compiler-cost admission or exact integer-recovery theorem +is supplied. The five selected framework assumptions remain. + +## Open next questions + +- Can sharper frequency separation and a less conservative layer budget reduce + the explicit onset enough for a useful finite-cost comparison? Start with + certified bounds on the actual characteristic function over a chosen compact + frequency interval. A rigorous stronger spectral estimate is the blocker. +- Can an all-size physical implementation fund the complete fixed-height + recurrence? Start by binding its native operations and access, restoration + and precision costs to the exact source flow. The scalar theorem alone does + not supply that implementation or bill. + +[TASK.json](TASK.json) records the changed scope and these questions. The +[coordination claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19391591) +identifies this continuation of #6329's handoff. + +## Credit + +Prepared for **@alephnan with substantial OpenAI Codex assistance**, including +parallel mathematical derivation, exact code, writing and adversarial review. +No independent human acceptance or proof-kernel verification is claimed. + +Credit zxv (#4436/#4483), Ryanson Jonathan / pinterbanget (#4459/#4467), +DLamdata (#6118), Nick Petalas (#6125/#6128), the full-flow exponent contribution +prepared for @CubeJerry (#6329), Cinna Davis / 1337isnot1337, Jacob Alan Sussman, +and the retained native/precision/analytic lineage. Beurling, Selberg and +Vaaler retain credit for the classical Fourier approximation; Laura Shou's +primary paper provides the inspected statement. New work is Apache-2.0. diff --git a/research/effective-direct-flow/REVIEW.md b/research/effective-direct-flow/REVIEW.md new file mode 100644 index 0000000000..84dc9935d0 --- /dev/null +++ b/research/effective-direct-flow/REVIEW.md @@ -0,0 +1,155 @@ +# Separate adversarial review of the effective direct-flow argument + +**Disposition:** the reviewed written argument proves the stated explicit +upper majorant for the pinned historical scalar recurrence, conditional on +the stated classical Beurling--Selberg approximation theorem and the +authenticated predecessor flow identities. No unresolved mathematical +objection was found in this review. This is AI-assisted review, not human +peer review, a proof-kernel check, or physical supplier admission. + +Reviewed files: + +- `LOCAL_LIMIT.md`: SHA256 + `07702eabadefa4e2c435d6ea7e60c781aaa786fa875cab773a5962d8d2a2efe3`. +- `PROOF.md`: SHA256 + `e7dbe4e1705a307e9eb32f6f06b340fb2c49948cc749110d6be2c6fb3da94ea9`. + +The reviewing worker did not write these two files or the numerical verifier. +It did contribute an earlier, coarser characteristic-function separation +estimate during discovery. Consequently the later review is not claimed to +be wholly independent of the discovery of that ingredient. The sharper +constants, interval smoothing, mixed-layer propagation and final induction +were reconstructed from the submitted drafts in a separate review pass. +The numerical source law and predecessor mathematical identities remain +shared dependencies. + +## Local-limit checks + +The review checked the following implications directly from the written +hypotheses, rather than treating a small numerical experiment as an all-size +argument: + +1. The centered support and variance bounds give + `|phi(t)| <= exp(-v*t^2/3)` for `|t|<=1/6`. The Taylor remainder constant + is `5/6 + 9/48 = 49/48`; integrating the telescoping estimate gives + `147/(16n)<10/n`. +2. Nearest-integer phases at `log 2` and `log 3`, followed by separation of + the distinct integers `2^q` and `3^p`, give the stated lower bound for + the larger phase residual. The coefficient + `log(2)*log(3)/(2*pi)<1/8` permits angular cutoff `2*log(n)`. + The two retained atom pairs give the required + `exp(-sqrt(n)/320)` bound for the nth characteristic-function power. +3. With the explicitly stated angular Fourier convention, the Selberg + spatial defect is `2*pi/T`. The signed minorant has the same sufficient + absolute-integral bound as the majorant. Fourier inversion is legitimate + because the bounded Fourier transforms have compact support. +4. Enlarging the majorized interval and contracting the minorized interval + before taking their limit handles the actual atomic law, including + either convention at a cap. No density of the discrete sum is assumed. +5. Both remainder expressions used in the symbolic onset decrease on the + declared domain. The exact comparisons at `w=60`, and then + `c_sigma*2/log(n)<15/10^12<10^-8`, support the stated all-size cutoff. +6. Layer-cake transfer is valid for the exponential half-line kernel. + The complement kernel is decreasing since its inner function is convex + with `x*Q_s'(x)>=Q_s(x)`. The derivative singularity at `x=1` does not + invalidate continuity or monotone Stieltjes integration. + +The exact finite verifier authenticates the source and establishes its atom, +centered-moment and other numerical hypotheses. It was executed successfully +in this review pass, as detailed below. The analytic review does not replace +those checks or claim a formal proof of the external Selberg theorem. + +## Complete-flow and induction checks + +The review independently reconstructed the tilted normalization. A mixed +base contributes +`A^(G-1)*q^h*exp(-alpha*B)*exp(alpha*u)`. Dividing by the proposed +`F_G` therefore yields the multiplier `(1-q)*q^h*c_sigma*sqrt(G)`. +The full leaf term has coefficient `J*P(s)/121^s`; its terminal paid letter +is unconditioned. In particular no terminal cutoff or missing factor of +the paid rank is used. + +The source and boundary windows match the predecessor's strict cap tests. +Discarding root-source capacity is safe because it is nonnegative. The +signed-window error is bounded by the sum of absolute kernel heights, not +by cancellation. Stieltjes integration uses the same half-open windows as +the flow and remains valid at atoms. + +All three ranges of mixed layers were checked separately. In the retained +range, conditioning on the target letters leaves a bounded shift and at +least `n_LLT` paid letters. The middle range uses the location-uniform +probability bound only. The last range, including zero paid letters, uses +the trivial supremum bound and geometric weights. The omitted infinite +geometric weight of the limiting integral is separately charged. + +The arithmetic quantities reconstructed in this pass include + +```text +Q = 52092027504, +3*10^-8*Q = 1562.76082512, +8*Q/((3/500)^2*10^18) = 0.011576006112. +``` + +The two finite Gaussian flattening bounds, the retained-layer index limits, +and the elementary exponential comparisons for both tails were checked. +The leaf half-line includes every interval after 5000, with no uncharged +truncation. Its error and all mixed errors fit the declared total 1600. + +Finally the exact rank-one conservation surplus is 608. This makes the +linear function an all-rank upper solution of the complete recurrence, +so `L(n)<=n` follows before the improved induction starts. It supplies the +explicit initial-range constant `N0^(1-s)` without enumerating that range. +Uniformity in the actual level offset gives every integer `N>=N0`, not +just level starts. The strong induction includes zero complements via +`L(0)=0`. + +## Diagnostic corroboration and limits + +The following commands were executed successfully in the isolated worktree: + +```text +python -I -W error -B research/effective-direct-flow/verify.py +python -I -W error -B research/effective-direct-flow/independent_checks.py +python -I -W error -B research/effective-direct-flow/diagnostic.py +``` + +The exact verifier returned `PASS_EFFECTIVE_DIRECT_FLOW`, including the +outward lower bound `47053.890913` for the 512-term full margin, all numerical +premises, symbolic uniform budgets and complete-flow controls. The separate +`Fraction` oracle checked 3969 interval pairs, 1764 valid divisions, 2205 +zero-interval rejections and 630 signed ceilings. These controls exercise the +verifier's arithmetic implementation; they are not an independent proof of +the analytic theorem. The rounded 90-digit Decimal diagnostic, with literal +inventories and no repository numerical imports, gave the corroborating +512-term margin `47053.893158567844...`. It is not an acceptance gate. + +A separate elementary floating calculation, importing no package engine, +evaluated 2999 positive-binomial terms at the midpoint of the predecessor +tilt bracket. It gave approximately + +```text +K(s) = 266657973.81101257, +V(s) = 266610919.7758388, +K(s)-V(s) = 47054.035173773766. +``` + +This agrees with the claimed conservative margin `>40000` but is only a +diagnostic. The outward rational certificate, not these floats, establishes +the numerical acceptance decision. + +One minor exposition issue was reported and resolved: the local-limit +statement now explicitly includes interval length zero, and proves the +singleton inequality by continuity from above for shrinking positive-length +intervals. The final amendment also explicitly defines centering at the mean +for the general-law formulation. Both changes were checked against the +argument; neither changes any quantitative bound. No unresolved issue from +this review remains. + +The review does not establish a lower onset, a better recurrence exponent, +the physical correctness of the raw supplier, the selected P104 construction, +or any discharge of native, owned-erasure, compiler, precision/tape or +analytic-recovery assumptions. The complete finite source-flow identities +are retained predecessor mathematics, with the package's declared bounded +checks as corroboration. + +Prepared for @alephnan with substantial OpenAI Codex assistance. Apache-2.0. diff --git a/research/effective-direct-flow/SOURCES.json b/research/effective-direct-flow/SOURCES.json new file mode 100644 index 0000000000..61528641eb --- /dev/null +++ b/research/effective-direct-flow/SOURCES.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "research/direct-flow-leaf-walk/verify.py", + "usage": "input", + "git_blob": "42440e630a46c6e581797f52bfb4c0c87bbdac3a", + "sha256": "2030d79d7f136b39b4e2a3f5b033af4bba18ab87579ec352267dc1697e02157d" + }, + { + "path": "research/direct-mixed-flow/flow.py", + "usage": "input", + "git_blob": "07175cd6e1f2c2367c2e78eca7f163fef18d301d", + "sha256": "460f0b0262d7b6880973f46240b3fff1e9f04601fa1d658dda18688b1e26575a" + }, + { + "path": "research/direct-flow-exponent-gate/PROOF.md", + "usage": "input", + "git_blob": "d9f1e340bc2cc6241392a285dbcebef35630c478", + "sha256": "c6c2a52e2424186db09c28792b6956aa349ad2716ea8c81bf1f0faea875be0e4" + }, + { + "path": "research/direct-flow-exponent-gate/README.md", + "usage": "input", + "git_blob": "4abfbf70374734423ae879dd7a31de40afd42e89", + "sha256": "16cdebfdea1f1d660527c14974973fe87e3b2e3841d27adbcbfd376da71a8bcd" + }, + { + "path": "research/direct-flow-exponent-gate/TASK.json", + "usage": "input", + "git_blob": "7d98de314205d788ae149c5259686953c7c58664", + "sha256": "b20958d698cd7432cdb1f6d398325c55f60476f7ffa2aa6aa825de164f5098c7" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "docs/research/pr-intake-evidence/pr6030-audit/PROOF-REVIEW.md", + "usage": "provenance", + "git_blob": "26f2f6324bce57e69e861d2aae5a27c9de325a8e", + "sha256": "8bd158b8ef68202000f167b9b78db0b31531b5b067b5cbd91b5bf35f3ddd1ab6" + } + ] +} diff --git a/research/effective-direct-flow/TASK.json b/research/effective-direct-flow/TASK.json new file mode 100644 index 0000000000..50721ea6a2 --- /dev/null +++ b/research/effective-direct-flow/TASK.json @@ -0,0 +1,90 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "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_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "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": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Make the historical raw-p7 original fixed-height scalar recurrence bound L(n)=O(n^0.99739) fully effective: explicit uniform interval local limit, all-layer propagation, and all-rank constant.", + "scope_change_reason": "The selected6030 source and review were traced first. Taking the explicit open question of direct-flow-exponent-gate (#6329) changes the source/caller from selected P104 to its named historical scalar recurrence. This is an analytic side result, not discharge of a selected framework assumption.", + "bottleneck_link": "Removes an ineffective local-limit step preventing an explicit uniform scalar majorant. Native realization, physical cost, and all five selected assumptions remain separate.", + "budget_minutes": 120, + "stop_rule": "One explicit all-rank theorem or a precise remaining gap. Restrict to the pinned nine-atom raw-p7 law and original height; no new kappa or changed-height search. Reserve final quarter for verification and handoff.", + "outcome": "completed", + "evidence": "LOCAL_LIMIT.md proves an explicit uniform interval LLT and PROOF.md propagates it to L(n)<=N0^(261/100000)n^(99739/100000), N0=121*5^(2*2^(10^12)+2), at every integer n>=1. The independently written exact verifier passes numerical premises and finite controls. See VALIDATION.json and the disclosed adversarial REVIEW.md.", + "author": "@alephnan with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance in theory, exact checker, writing and parallel adversarial review. No independent human or proof-kernel acceptance claimed.", + "coordination_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19391591", + "open_questions": [ + { + "question": "Can the explicit onset be reduced to a rank that permits useful finite-cost comparison?", + "why_it_matters": "The proved onset is finite but extremely conservative; it is not a practical cost estimate.", + "first_step": "Replace the elementary logarithmic-frequency separation by certified compact-frequency bounds optimized for the required error, then reprice the full tail budget.", + "blocked_by": "A quantitatively stronger spectral estimate and source-bound onset calculation." + }, + { + "question": "Can a physical fixed-height supplier fund the complete scalar recurrence?", + "why_it_matters": "An explicit scalar majorant does not pay native, movement, ownership or precision costs.", + "first_step": "Bind one all-size physical implementation to the exact recurrence and account for all additional costs.", + "blocked_by": "No physical supplier implementation or admission is supplied." + } + ] +} diff --git a/research/effective-direct-flow/VALIDATION.json b/research/effective-direct-flow/VALIDATION.json new file mode 100644 index 0000000000..6abb86057f --- /dev/null +++ b/research/effective-direct-flow/VALIDATION.json @@ -0,0 +1,102 @@ +{ + "schema_version": 1, + "status": "PASS_DECLARED_CHECKS", + "checked_at_utc": "2026-11-04T07:02:34.958121+00:00", + "environment": { + "python": "3.12.2 (tags/v3.12.2:6abddd9, Feb 6 2024, 21:26:36) [MSC v.1937 64 bit (AMD64)]", + "implementation": "CPython", + "platform": "Windows-11-10.0.26300-SP0", + "third_party_dependencies": [] + }, + "scientific_base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "commands": [ + { + "argv": [ + "{python}", + "-B", + "scripts/research_package.py", + "--package", + "research/effective-direct-flow" + ], + "returncode": 0, + "elapsed_seconds": 5.032, + "stdout": "CHECK Authenticated source law and flow; independent exact tilted-law and full-complement inequalities; symbolic onset/tail budgets; finite complete-histogram and rejection controls. Written proofs establish the universal theorem.\n{\n \"status\": \"PASS_EFFECTIVE_DIRECT_FLOW\",\n \"numerical_hypotheses\": {\n \"alpha\": [\n \"0.98981438244596\",\n \"0.98981438244600\"\n ],\n \"probabilities\": {\n \"1\": [\n \"0.289256813142\",\n \"0.289256813143\"\n ],\n \"2\": [\n \"0.164687698721\",\n \"0.164687698722\"\n ],\n \"3\": [\n \"0.077288932732\",\n \"0.077288932733\"\n ]\n },\n \"variance\": [\n \"2.192503074149\",\n \"2.192503074150\"\n ],\n \"third_absolute_moment\": [\n \"3.978639864753\",\n \"3.978639864755\"\n ],\n \"tilted_gap\": [\n \"1660.00368885\",\n \"1660.00368888\"\n ],\n \"tilted_target_ratio\": [\n \"0.987128605365\",\n \"0.987128605366\"\n ],\n \"full_margin_lower_sum\": [\n \"47053.890913\",\n \"47053.895405\"\n ],\n \"binomial_terms\": 512\n },\n \"uniform_constants\": {\n \"onset_log2\": \"1000000000000\",\n \"n_LLT\": \"2^1000000000000\",\n \"G0\": \"2*2^1000000000000+2\",\n \"N0\": \"121*5^G0\",\n \"kernel_multiplier\": 52092027504,\n \"normalized_error_upper\": 1600,\n \"normalized_capacity_margin_lower\": 38400,\n \"majorant\": \"L(n) <= N0^(261/100000) * n^(99739/100000), n>=1\"\n },\n \"finite_controls\": {\n \"complete_histogram_fixtures\": 10,\n \"semantic_mutations\": 2,\n \"domain_rejections\": 4,\n \"arithmetic_controls\": 3\n },\n \"no_new_kappa\": true,\n \"scope\": \"Exact finite numerical premises and controls; written Fourier and full-flow proofs establish the universal bound.\"\n}\nCHECK Same acceptance gates with Python assertions disabled.\n{\n \"status\": \"PASS_EFFECTIVE_DIRECT_FLOW\",\n \"numerical_hypotheses\": {\n \"alpha\": [\n \"0.98981438244596\",\n \"0.98981438244600\"\n ],\n \"probabilities\": {\n \"1\": [\n \"0.289256813142\",\n \"0.289256813143\"\n ],\n \"2\": [\n \"0.164687698721\",\n \"0.164687698722\"\n ],\n \"3\": [\n \"0.077288932732\",\n \"0.077288932733\"\n ]\n },\n \"variance\": [\n \"2.192503074149\",\n \"2.192503074150\"\n ],\n \"third_absolute_moment\": [\n \"3.978639864753\",\n \"3.978639864755\"\n ],\n \"tilted_gap\": [\n \"1660.00368885\",\n \"1660.00368888\"\n ],\n \"tilted_target_ratio\": [\n \"0.987128605365\",\n \"0.987128605366\"\n ],\n \"full_margin_lower_sum\": [\n \"47053.890913\",\n \"47053.895405\"\n ],\n \"binomial_terms\": 512\n },\n \"uniform_constants\": {\n \"onset_log2\": \"1000000000000\",\n \"n_LLT\": \"2^1000000000000\",\n \"G0\": \"2*2^1000000000000+2\",\n \"N0\": \"121*5^G0\",\n \"kernel_multiplier\": 52092027504,\n \"normalized_error_upper\": 1600,\n \"normalized_capacity_margin_lower\": 38400,\n \"majorant\": \"L(n) <= N0^(261/100000) * n^(99739/100000), n>=1\"\n },\n \"finite_controls\": {\n \"complete_histogram_fixtures\": 10,\n \"semantic_mutations\": 2,\n \"domain_rejections\": 4,\n \"arithmetic_controls\": 3\n },\n \"no_new_kappa\": true,\n \"scope\": \"Exact finite numerical premises and controls; written Fourier and full-flow proofs establish the universal bound.\"\n}\nCHECK Check signed interval arithmetic against independent Fraction extrema and exact signed ceilings.\nPASS_INDEPENDENT_INTERVAL_CONTROLS interval_pairs=3969 valid_divisions=1764 zero_interval_rejections=2205 signed_ceilings=630\nCHECK Replay a minimal copy without Git or PATH, in normal and optimized modes; reject actual corruption of every declared input and verify no source writes.\n{\n \"status\": \"PASS_SOURCE_TRANSPORT_CONTROLS\",\n \"positive_replays\": 2,\n \"actual_input_corruption_rejections\": 10,\n \"declared_external_inputs\": 5,\n \"git_available\": false,\n \"child_PATH\": \"\",\n \"source_files_unchanged\": true,\n \"commands\": [\n [\n \"{python}\",\n \"-I\",\n \"-W\",\n \"error\",\n \"-B\",\n \"research/effective-direct-flow/verify.py\"\n ],\n [\n \"{python}\",\n \"-I\",\n \"-O\",\n \"-W\",\n \"error\",\n \"-B\",\n \"research/effective-direct-flow/verify.py\"\n ]\n ]\n}\nPASS_REGISTERED_RESEARCH_PACKAGE research/effective-direct-flow outcome=completed\n", + "stderr": "" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "research/effective-direct-flow/independent_checks.py" + ], + "returncode": 0, + "elapsed_seconds": 0.25, + "stdout": "PASS_INDEPENDENT_INTERVAL_CONTROLS interval_pairs=3969 valid_divisions=1764 zero_interval_rejections=2205 signed_ceilings=630\n", + "stderr": "" + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "research/effective-direct-flow/diagnostic.py" + ], + "returncode": 0, + "elapsed_seconds": 0.484, + "stdout": "{\n \"status\": \"DIAGNOSTIC_NOT_ACCEPTANCE\",\n \"scope\": \"Rounded supplementary cross-check only; no outward interval enclosures or scientific acceptance decisions. Run verify.py for the exact acceptance gate.\",\n \"method\": {\n \"engine\": \"Python standard-library decimal\",\n \"precision\": 90,\n \"mean_bisections\": 200,\n \"binomial_terms\": 512,\n \"repository_numerical_imports\": false,\n \"capacity_evaluation\": \"direct paid/target pair sum\"\n },\n \"literal_inputs\": {\n \"P\": {\n \"1\": 37305,\n \"2\": 10695,\n \"3\": 3360,\n \"4\": 1530,\n \"5\": 300,\n \"8\": 1464,\n \"16\": 448,\n \"32\": 448,\n \"48\": 448\n },\n \"T\": {\n \"5\": 420,\n \"6\": 270,\n \"7\": 840,\n \"8\": 1395,\n \"9\": 3195,\n \"25\": 448,\n \"41\": 448,\n \"57\": 448,\n \"121\": 224\n },\n \"width\": 121\n },\n \"alpha\": \"0.98981438244597755832962950090652733506542029071695065285932158090170346129969133207405672\",\n \"mean_endpoint_residuals\": [\n \"-2.1372212635283209702007821655827215137595442365332613738097393529567746280309E-9\",\n \"3.5180527673543387941936072301943580331432429863053282280905861566086133793862E-9\"\n ],\n \"mean_residual_at_computed_alpha\": \"-4.016784104867309E-70\",\n \"probabilities\": {\n \"1\": \"0.289256813142943896884068088990022220819660436237519464938989208101777421007655339806722995\",\n \"2\": \"0.164687698721100070876789919908148291971847645379710056334465422910716147725924117477746187\",\n \"3\": \"0.0772889327327933964538966194675821421935607871885601018491395686914644165591100594206499158\"\n },\n \"variance\": \"2.19250307414978345837442398361990427604600917528228276480790303906324861232266020387591989\",\n \"third_absolute_moment\": \"3.97863986475394825668320864553623131200551951068895872821349421385343339163721099903153141\",\n \"max_absolute_centered_support\": \"2.26176309847379055446341438952904433742388974099525274630476648013688979338973006466693518\",\n \"tilted_paid_mass\": \"128968.440171415248866888794943579210969433970733144489842588430188243049133769559898461904\",\n \"tilted_gap\": \"1660.003688864616223430860951852155276932826069178859900879021953058549863976813408875295\",\n \"tilted_target_ratio\": \"0.987128605365326099091651437790327212765055215178307828773956940434355586261369936884306390\",\n \"tau\": \"0.00757561755402244167037049909347266493457970928304934714067841909829653870030866792594328\",\n \"terminal_coefficient\": \"1092.58853647068677620424524590513416121430764526981567255529755848118479782660477889684815\",\n \"capacity_512_direct_pair_sum\": \"266657973.668996809304440470399121739030415187457687019183895645296480573703919224009430730\",\n \"boundary_plus_leaf\": \"266610919.775838241460291248463080406068849790935200263981338046659025783347015316044818959\",\n \"margin_512\": \"47053.893158567844149221936041332961565396522486755202557598637454790356903907964611771\",\n \"error_budget\": {\n \"retained\": \"1562.76082512\",\n \"middle\": \"0.000163234100365143950645643652754586186952468487352882276495580600386672432106636776280805275\",\n \"high\": \"0.011576006112\",\n \"complete\": \"1562.97256456021236514395064564365275458618695246848735288227649558060038667243210663677628\"\n }\n}\n", + "stderr": "" + } + ], + "package_source_sha256": { + "check_transport.py": "4822c24974bcbc7b479dec0a2ff48216b44f6f90ad66b86c6efc2b328b02e0ad", + "diagnostic.py": "efcc2d8a24b105db6a90d284be42d1fd3e2f7abd76470cc408244187ad234b9e", + "independent_checks.py": "604baef660567b94e51133400900bd8d180e2d41637c68be586037c093f991c3", + "LOCAL_LIMIT.md": "07702eabadefa4e2c435d6ea7e60c781aaa786fa875cab773a5962d8d2a2efe3", + "PROOF.md": "e7dbe4e1705a307e9eb32f6f06b340fb2c49948cc749110d6be2c6fb3da94ea9", + "README.md": "6d60e7e09588bc60e9f885bbca7e297390360880e68e67a431937bd0051462e6", + "REVIEW.md": "5fcefced3531f08920a4f4aec6e60c47e52300c4cef680566e22e0b37b150b36", + "SOURCES.json": "67db65efc2ffb1e4ee480e67a5c5e9cad1025fa0da59a6c7ae997ab64ea22826", + "TASK.json": "a432acde8dc1f64c9999f37750df5f9845aee6e11ad3fe5c422164733b8e32be", + "VERIFY.json": "c62be93f92d0c7e38dcf2b5a37afa050c26a31bf1b19841263724c8b5c19191d", + "verify.py": "0c688f6e604e3a8ec6504721c88cdfbc61f6569744b6affb7ba262dd494c3666" + }, + "selected_orientation": { + "status": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "selected_pr": 6030, + "selected_kappa": "0.003125804", + "command": "python -B scripts/research_selected_baseline.py", + "note": "Passed before this package was written; ordinary Windows path encountered MAX_PATH. Full selected cold replay was not run.", + "actual_windows_command": "python -B \"\\\\?\\C:\\Users\\rafag\\AgentsCode\\Research_integer-mult-bounds\\.worktrees\\theory-20261104\\scripts\\research_selected_baseline.py\"" + }, + "proof_status": "Written analytic theorem with disclosed separate adversarial AI review. Exact finite gates establish numerical premises and controls; no human acceptance or proof-kernel verification.", + "unrun_obligations": [ + "Independent human review of the universal proof and cited approximation input.", + "Physical implementation and complete caller cost for this historical raw-p7 recurrence.", + "All five framework assumptions of the selected P104 multiplication theorem remain." + ], + "byte_transport_note": "New package text normalized from CRLF to LF before commit, following repository .gitattributes. This is a line-ending-only transformation; review proof hashes and this receipt were updated to the publication bytes.", + "overlap_refresh": { + "open_prs": { + "fetched_at": "2026-11-04T07:00:54.030229+00:00", + "records": 663, + "complete_pagination": true + }, + "discussions": { + "fetched_at": "2026-11-04T07:02:47.225809+00:00", + "records": 6789, + "complete_pagination": true + }, + "local": { + "searched_records": 88, + "head_records": 8917, + "complete": false + }, + "note": "Bounded overlap survey, not a novelty certificate; relevant archived PRs were also searched and read." + } +} diff --git a/research/effective-direct-flow/VERIFY.json b/research/effective-direct-flow/VERIFY.json new file mode 100644 index 0000000000..3eef287a49 --- /dev/null +++ b/research/effective-direct-flow/VERIFY.json @@ -0,0 +1,50 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/direct-flow-leaf-walk/verify.py", + "research/direct-mixed-flow/flow.py", + "research/direct-flow-exponent-gate/PROOF.md", + "research/direct-flow-exponent-gate/README.md", + "research/direct-flow-exponent-gate/TASK.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Authenticated source law and flow; independent exact tilted-law and full-complement inequalities; symbolic onset/tail budgets; finite complete-histogram and rejection controls. Written proofs establish the universal theorem." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same acceptance gates with Python assertions disabled." + }, + { + "argv": ["{python}", "-I", "-W", "error", "-B", "{package}/independent_checks.py"], + "timeout_seconds": 120, + "checks": "Check signed interval arithmetic against independent Fraction extrema and exact signed ceilings." + }, + { + "argv": ["{python}", "-I", "-W", "error", "-B", "{package}/check_transport.py"], + "timeout_seconds": 120, + "checks": "Replay a minimal copy without Git or PATH, in normal and optimized modes; reject actual corruption of every declared input and verify no source writes." + } + ] +} diff --git a/research/effective-direct-flow/check_transport.py b/research/effective-direct-flow/check_transport.py new file mode 100644 index 0000000000..4a7f5500d8 --- /dev/null +++ b/research/effective-direct-flow/check_transport.py @@ -0,0 +1,87 @@ +#!/usr/bin/env python3 +"""Replay a minimal source copy without Git and reject actual input corruptions. + +No source artifact is written. Temporary copies are deleted by TemporaryDirectory. +Prepared for @alephnan with substantial OpenAI Codex assistance. Apache-2.0. +""" +from pathlib import Path +import hashlib +import json +import os +import shutil +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def digest_tree(root): + return {p.relative_to(root).as_posix(): hashlib.sha256(p.read_bytes()).hexdigest() + for p in root.rglob('*') if p.is_file()} + + +def main(): + manifest = json.loads((HERE/'VERIFY.json').read_text(encoding='utf-8')) + inputs = manifest['inputs'] + require(len(inputs) == 5, 'unexpected input closure') + commands = [] + with tempfile.TemporaryDirectory(prefix='effective-flow-') as folder: + root = Path(folder) + package = root/'research/effective-direct-flow' + package.mkdir(parents=True) + for p in HERE.iterdir(): + if p.is_file(): + shutil.copyfile(p, package/p.name) + for name in inputs: + destination = root/name + destination.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT/name, destination) + require(not (root/'.git').exists(), 'unexpected Git metadata') + initial = digest_tree(root) + env = dict(os.environ, PATH='') + positive = 0 + rejected = 0 + outputs = [] + for optimized in (False, True): + argv = [sys.executable, '-I'] + (['-O'] if optimized else []) + argv += ['-W', 'error', '-B', str(package/'verify.py')] + result = subprocess.run(argv, cwd=root, env=env, capture_output=True, + text=True, timeout=120) + require(result.returncode == 0, 'isolated positive replay failed: '+result.stderr) + value = json.loads(result.stdout) + require(value['status'] == 'PASS_EFFECTIVE_DIRECT_FLOW', 'positive status') + require(digest_tree(root) == initial, 'positive replay changed a file') + outputs.append(value) + positive += 1 + commands.append(['{python}', '-I'] + (['-O'] if optimized else []) + + ['-W', 'error', '-B', 'research/effective-direct-flow/verify.py']) + for name in inputs: + path = root/name + original = path.read_bytes() + try: + path.write_bytes(original+b'\n') + result = subprocess.run(argv, cwd=root, env=env, capture_output=True, + text=True, timeout=120) + require(result.returncode != 0 and 'source SHA256 mismatch' in result.stderr, + 'actual corrupted input escaped source gate: '+name) + rejected += 1 + finally: + path.write_bytes(original) + require(digest_tree(root) == initial, 'mutation restoration failed') + require(outputs[0] == outputs[1], 'normal/optimized results differ') + print(json.dumps({'status': 'PASS_SOURCE_TRANSPORT_CONTROLS', + 'positive_replays': positive, 'actual_input_corruption_rejections': rejected, + 'declared_external_inputs': len(inputs), 'git_available': False, + 'child_PATH': '', 'source_files_unchanged': True, + 'commands': commands}, indent=2)) + + +if __name__ == '__main__': + main() diff --git a/research/effective-direct-flow/diagnostic.py b/research/effective-direct-flow/diagnostic.py new file mode 100644 index 0000000000..b7b6556460 --- /dev/null +++ b/research/effective-direct-flow/diagnostic.py @@ -0,0 +1,113 @@ +#!/usr/bin/env python3 +"""Independent Decimal cross-check; not an acceptance certificate. + +Prepared for @alephnan with substantial OpenAI Codex assistance. Apache-2.0. +Uses only the standard library and literal historical inventories, with no +imports from repository numerical sources. Decimal results are rounded, not +outward interval enclosures. The exact verifier remains the acceptance gate. +""" + +from decimal import Decimal as D, localcontext +import json + + +P = {1: 37305, 2: 10695, 3: 3360, 4: 1530, 5: 300, + 8: 1464, 16: 448, 32: 448, 48: 448} +T = {5: 420, 6: 270, 7: 840, 8: 1395, 9: 3195, + 25: 448, 41: 448, 57: 448, 121: 224} +WIDTH = 121 +PRECISION = 90 +BISECTIONS = 200 +BINOMIAL_TERMS = 512 + + +def calculate(): + with localcontext() as context: + context.prec = PRECISION + logs = {r: D(r).ln() for r in set(P) | set(T) | {WIDTH}} + centre = logs[5] + s = D(99739) / 100000 + + def tilted(alpha): + powers = {r: (alpha * logs[r]).exp() for r in logs} + mass = sum(D(count) * powers[r] for r, count in P.items()) + residual = sum(D(count) * powers[r] * (logs[r] - centre) + for r, count in P.items()) + return powers, mass, residual + + lo, hi = D('0.98981438244597'), D('0.98981438244599') + endpoint_residuals = [tilted(lo)[2], tilted(hi)[2]] + if not endpoint_residuals[0] < 0 < endpoint_residuals[1]: + raise ArithmeticError('Diagnostic bisection endpoints do not straddle zero') + for _ in range(BISECTIONS): + mid = (lo + hi) / 2 + if tilted(mid)[2] > 0: + hi = mid + else: + lo = mid + alpha = (lo + hi) / 2 + pa, mass, residual = tilted(alpha) + probabilities = {r: D(count) * pa[r] / mass for r, count in P.items()} + variance = sum(probabilities[r] * (logs[r] - centre) ** 2 for r in P) + third = sum(probabilities[r] * abs(logs[r] - centre) ** 3 for r in P) + support = max(abs(logs[r] - centre) for r in P) + target_mass = sum(D(count) * pa[k] for k, count in T.items()) + gap, ratio, tau = mass - target_mass, target_mass / mass, s - alpha + ps = {r: (s * logs[r]).exp() for r in logs} + terminal = sum(D(count) * ps[r] for r, count in P.items()) / ps[WIDTH] + + # Evaluate every paid/target pair directly. This deliberately does not + # use the exact verifier's aggregation of coefficients by rank. + boundary = sum(D(pr * tk) * (pa[k] * ps[r] - pa[r] * ps[k]) + for r, pr in P.items() for k, tk in T.items() if r > k) + capacity, coefficient = D(0), s + for j in range(1, BINOMIAL_TERMS + 1): + integrated_term = sum( + D(pr * tk) * (pa[r] * (D(k) / WIDTH) ** j + - pa[k] * (D(r) / WIDTH) ** j) + for r, pr in P.items() for k, tk in T.items() if k > r + ) / (D(j) - alpha) + capacity += coefficient * integrated_term + coefficient *= (D(j) - s) / (j + 1) + exit_value = (gap * terminal + boundary / ps[WIDTH]) / tau + + # Supplementary rounded check of the proof's conservative error budget. + multiplier = WIDTH * sum(P.values()) * sum(T.values()) + retained = D(3 * multiplier) / 10**8 + middle = D(17 * multiplier) * (D(247) / 250) ** 3001 + high = D(8 * multiplier) / ((D(3) / 500) ** 2 * 10**18) + error_total = retained + middle + high + D(1) / 5 + D(2) / 10**7 + + return { + 'status': 'DIAGNOSTIC_NOT_ACCEPTANCE', + 'scope': ('Rounded supplementary cross-check only; no outward interval ' + 'enclosures or scientific acceptance decisions. Run verify.py ' + 'for the exact acceptance gate.'), + 'method': {'engine': 'Python standard-library decimal', + 'precision': PRECISION, 'mean_bisections': BISECTIONS, + 'binomial_terms': BINOMIAL_TERMS, + 'repository_numerical_imports': False, + 'capacity_evaluation': 'direct paid/target pair sum'}, + 'literal_inputs': {'P': P, 'T': T, 'width': WIDTH}, + 'alpha': str(alpha), + 'mean_endpoint_residuals': [str(x) for x in endpoint_residuals], + 'mean_residual_at_computed_alpha': str(residual), + 'probabilities': {str(r): str(probabilities[r]) for r in (1, 2, 3)}, + 'variance': str(variance), + 'third_absolute_moment': str(third), + 'max_absolute_centered_support': str(support), + 'tilted_paid_mass': str(mass), + 'tilted_gap': str(gap), + 'tilted_target_ratio': str(ratio), + 'tau': str(tau), + 'terminal_coefficient': str(terminal), + 'capacity_512_direct_pair_sum': str(capacity), + 'boundary_plus_leaf': str(exit_value), + 'margin_512': str(capacity - exit_value), + 'error_budget': {'retained': str(retained), 'middle': str(middle), + 'high': str(high), 'complete': str(error_total)}, + } + + +if __name__ == '__main__': + print(json.dumps(calculate(), indent=2)) diff --git a/research/effective-direct-flow/independent_checks.py b/research/effective-direct-flow/independent_checks.py new file mode 100644 index 0000000000..5ee0c4b676 --- /dev/null +++ b/research/effective-direct-flow/independent_checks.py @@ -0,0 +1,92 @@ +#!/usr/bin/env python3 +"""Independent rational controls for the new interval arithmetic implementation. + +This exercises verify.py's implementation but computes expected ranges with +fractions.Fraction, without using its grid arithmetic. The finite controls do +not replace the written proofs of directed rounding or the analytic theorem. + +Prepared for @alephnan with substantial OpenAI Codex assistance. Apache-2.0. +""" +from fractions import Fraction +from itertools import product +from pathlib import Path +import importlib.util + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def load_implementation(): + path = Path(__file__).resolve().with_name('verify.py') + spec = importlib.util.spec_from_file_location('effective_interval_under_test', path) + require(spec is not None and spec.loader is not None, 'cannot load interval implementation') + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +def run(): + implementation = load_implementation() + Box = implementation.Box + + # Non-dyadic endpoints force outward rounding. The deterministic stride + # keeps a small fixture containing positive, negative, crossing-zero and + # singleton intervals; the expected case counts are explicit below. + values = sorted({Fraction(n, d) for n in range(-5, 6) for d in (1, 3, 7)}) + intervals = [(a, b) for a, b in product(values, repeat=2) if a <= b][::7] + require(len(intervals) == 63, 'interval fixture changed') + require(any(a < b < 0 for a, b in intervals), 'missing negative interval') + require(any(0 < a < b for a, b in intervals), 'missing positive interval') + require(any(a < 0 < b for a, b in intervals), 'missing crossing interval') + require(any(a == b for a, b in intervals), 'missing singleton interval') + + pairs = divisions = zero_rejections = 0 + for a, b in intervals: + left = Box(a, b) + require(left.lo <= a <= b <= left.hi, 'constructor rounded inward') + for c, d in intervals: + right = Box(c, d) + corners = (a*c, a*d, b*c, b*d) + result = left*right + require(result.lo <= min(corners) <= max(corners) <= result.hi, + 'product excludes an exact rational corner') + + if c*d > 0: + corners = (a/c, a/d, b/c, b/d) + result = left/right + require(result.lo <= min(corners) <= max(corners) <= result.hi, + 'quotient excludes an exact rational corner') + divisions += 1 + else: + try: + left/right + except ValueError: + zero_rejections += 1 + else: + raise ValueError('division by interval containing zero accepted') + pairs += 1 + + require(pairs == 3969, 'pair coverage changed') + require(divisions + zero_rejections == pairs, 'division partition incomplete') + + # This tests ceil(a/b) for both denominator signs independently of the + # implementation's formula. The characterizing inequalities are exact. + ceilings = 0 + denominators = list(range(-9, 0)) + list(range(1, 10)) + for numerator, denominator in product(range(-17, 18), denominators): + exact = Fraction(numerator, denominator) + rounded = implementation.ceiling(numerator, denominator) + require(type(rounded) is int and rounded-1 < exact <= rounded, + 'signed ceiling violates its defining inequalities') + ceilings += 1 + require(ceilings == 630, 'ceiling coverage changed') + + print('PASS_INDEPENDENT_INTERVAL_CONTROLS ' + f'interval_pairs={pairs} valid_divisions={divisions} ' + f'zero_interval_rejections={zero_rejections} signed_ceilings={ceilings}') + + +if __name__ == '__main__': + run() diff --git a/research/effective-direct-flow/verify.py b/research/effective-direct-flow/verify.py new file mode 100644 index 0000000000..e28e169354 --- /dev/null +++ b/research/effective-direct-flow/verify.py @@ -0,0 +1,356 @@ +#!/usr/bin/env python3 +"""Exact hypotheses and finite controls for the effective direct-flow proof. + +Prepared for @alephnan with substantial OpenAI Codex assistance. Apache-2.0. +No predecessor numerical engine is imported. The all-size conclusion rests on +the written proofs and their stated classical Fourier approximation theorem. +""" +from collections import Counter +from fractions import Fraction as Q +from functools import lru_cache +from pathlib import Path +import ast +import hashlib +import json +import types + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +GRID = 1 << 128 +S = Q(99739, 100000) +ALPHA_LO = Q('0.98981438244597') +ALPHA_HI = Q('0.98981438244599') +ONSET_EXPONENT = 10**12 + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def ceiling(a, b): + return -((-a)//b) + + +class Box: + """Integer endpoints on a dyadic grid, with directed rounding.""" + def __init__(self, value=0, upper=None, *, raw=False): + if raw: + self.l, self.h = value, upper + else: + lo, hi = Q(value), Q(value if upper is None else upper) + self.l = lo.numerator*GRID//lo.denominator + self.h = ceiling(hi.numerator*GRID, hi.denominator) + need(self.l <= self.h, 'reversed interval') + + @staticmethod + def cast(value): + return value if isinstance(value, Box) else Box(value) + + @property + def lo(self): + return Q(self.l, GRID) + + @property + def hi(self): + return Q(self.h, GRID) + + def __add__(self, other): + v = self.cast(other) + return Box(self.l+v.l, self.h+v.h, raw=True) + + __radd__ = __add__ + + def __neg__(self): + return Box(-self.h, -self.l, raw=True) + + def __sub__(self, other): + return self + -self.cast(other) + + def __rsub__(self, other): + return self.cast(other) + -self + + def __mul__(self, other): + v = self.cast(other) + products = (self.l*v.l, self.l*v.h, self.h*v.l, self.h*v.h) + return Box(min(products)//GRID, ceiling(max(products), GRID), raw=True) + + __rmul__ = __mul__ + + def __truediv__(self, other): + v = self.cast(other) + need(v.l*v.h > 0, 'division interval contains zero') + return self*Box(GRID*GRID//v.h, ceiling(GRID*GRID, v.l), raw=True) + + def __pow__(self, degree): + need(type(degree) is int and 0 <= degree <= 8, 'power domain') + result = Box(1) + for _ in range(degree): + result = result*self + return result + + def display(self, digits=10): + scale = 10**digits + def fmt(value): + sign = '-' if value < 0 else '' + whole, frac = divmod(abs(value), scale) + return f'{sign}{whole}.{frac:0{digits}d}' + return [fmt(self.l*scale//GRID), fmt(ceiling(self.h*scale, GRID))] + + +def reduced_log(x): + """2 atanh((x-1)/(x+1)), 80 positive terms and geometric tail.""" + need(Q(1) <= x <= 2, 'reduced logarithm domain') + z = Box((x-1)/(x+1)) + z2, term, result = z*z, z, Box(0) + for j in range(80): + result += 2*term/(2*j+1) + term *= z2 + remainder = 2*term/(161*(1-z2)) + return Box(result.l, result.h+remainder.h, raw=True) + + +@lru_cache(None) +def log_integer(rank): + need(type(rank) is int and 1 <= rank <= 121, 'logarithm rank domain') + power = rank.bit_length()-1 + return reduced_log(Q(rank, 1 << power)) + power*reduced_log(Q(2)) + + +def exponential_point(x): + x = Q(x) + need(-6 <= x <= 6, 'exponential domain') + if x < 0: + return Box(1)/exponential_point(-x) + z = Box(x/16) + term, result = Box(1), Box(1) + for j in range(1, 49): + term = term*z/j + result += term + # Remaining terms start at 49; successive ratios are at most z/50. + tail = term*z/49/(1-z/50) + result = Box(result.l, result.h+tail.h, raw=True) + for _ in range(4): + result *= result + return result + + +def power(rank, exponent): + z = log_integer(rank)*Box.cast(exponent) + return Box(exponential_point(z.lo).l, exponential_point(z.hi).h, raw=True) + + +def authenticate(): + manifest = json.loads((HERE/'SOURCES.json').read_text(encoding='utf-8')) + inputs = {} + for entry in manifest['files']: + if entry['usage'] == 'input': + path = ROOT/entry['path'] + data = path.read_bytes() + need(hashlib.sha256(data).hexdigest() == entry['sha256'], + 'source SHA256 mismatch: '+entry['path']) + blob = hashlib.sha1(b'blob '+str(len(data)).encode()+b'\0'+data).hexdigest() + need(blob == entry['git_blob'], 'source Git blob mismatch') + inputs[entry['path']] = data + return inputs + + +def inventory(data): + values = {} + for node in ast.parse(data).body: + if isinstance(node, ast.Assign) and len(node.targets) == 1: + name = getattr(node.targets[0], 'id', None) + if name in ('P', 'W', 'M'): + values[name] = ast.literal_eval(node.value) + need(set(values) == {'P', 'W', 'M'}, 'literal inventory missing') + need(values['M'] == 121, 'wrong historical width') + return values['P'], values['W'], values['M'] + + +def certify_law(paid, targets, width): + alpha = Box(ALPHA_LO, ALPHA_HI) + centre = log_integer(5) + need(centre.hi < 2 and log_integer(121).hi < 5, 'source shift bounds') + need(Q(2, 3) < log_integer(2).lo and log_integer(2).hi < Q(7, 10), + 'log two frequency bounds') + need(1 < log_integer(3).lo and log_integer(3).hi < Q(11, 10) + and log_integer(6).hi < 2, 'log three and six frequency bounds') + for endpoint, direction in ((ALPHA_LO, -1), (ALPHA_HI, 1)): + mean_residual = sum((c*power(r, endpoint)*(log_integer(r)-centre) + for r, c in paid.items()), Box()) + need(mean_residual.h < 0 if direction < 0 else mean_residual.l > 0, + 'tilted-mean root not bracketed') + ranks = sorted(set(paid)|set(targets)) + pa = {r: power(r, alpha) for r in ranks} + ps = {r: power(r, S) for r in ranks} + mass = sum((c*pa[r] for r, c in paid.items()), Box()) + target_mass = sum((c*pa[k] for k, c in targets.items()), Box()) + probabilities = {r: c*pa[r]/mass for r, c in paid.items()} + for r, bound in ((1, Q(1, 4)), (2, Q(1, 8)), (3, Q(1, 16))): + need(r in probabilities and probabilities[r].lo > bound, 'missing atom mass') + variance, third = Box(), Box() + for r, probability in probabilities.items(): + distance = log_integer(r)-centre if r >= 5 else centre-log_integer(r) + need(distance.lo >= -Q(1, 10**30) and distance.hi < 3, 'centred support bound') + variance += probability*distance**2 + third += probability*distance**3 + need(2 < variance.lo < variance.hi < Q(5, 2), 'variance bound') + need(third.hi < 5, 'third absolute moment bound') + gap, ratio, tau = mass-target_mass, target_mass/mass, Box(S)-alpha + need(0 < gap.lo < gap.hi < 2000, 'tilted gap') + need(ratio.hi < Q(247, 250), 'geometric layer ratio') + need(tau.lo > Q(3, 400), 'leaf decay rate') + terminal = sum((c*ps[r] for r, c in paid.items()), Box())/ps[width] + need(terminal.hi < 2000, 'complete terminal leaf coefficient') + + # Exact positive-binomial lower sum for the full source capacity. + # Its omitted tail is NONNEGATIVE, so it is not needed for this lower bound. + weights = {r: Box() for r in ranks} + boundary = Box() + for r, pr in paid.items(): + for k, tk in targets.items(): + if k > r: + weights[k] += pr*tk*pa[r] + weights[r] -= pr*tk*pa[k] + elif r > k: + boundary += pr*tk*(pa[k]*ps[r]-pa[r]*ps[k]) + powers = {r: Box(1) for r in ranks} + coefficient, capacity = Box(S), Box() + for j in range(1, 513): + for r in ranks: + powers[r] *= Q(r, width) + integral = sum((weights[r]*powers[r] for r in ranks), Box())/(j-alpha) + need(integral.lo > 0, 'positive integrated binomial term') + capacity += coefficient*integral + coefficient *= Q(j-S, j+1) + exit_value = (gap*terminal+boundary/ps[width])/tau + margin = capacity-exit_value + need(margin.lo > 40000, 'full complement margin too small') + return {'alpha': alpha.display(14), 'probabilities': { + str(r): probabilities[r].display(12) for r in (1, 2, 3)}, + 'variance': variance.display(12), 'third_absolute_moment': third.display(12), + 'tilted_gap': gap.display(8), 'tilted_target_ratio': ratio.display(12), + 'full_margin_lower_sum': margin.display(6), 'binomial_terms': 512} + + +def constant_certificate(paid, targets, onset_exponent=ONSET_EXPONENT): + need(type(onset_exponent) is int and onset_exponent >= 10**12, 'onset too small') + qbound = Q(247, 250) + total_variation = 121*sum(paid.values())*sum(targets.values()) + need(total_variation == 52092027504, 'kernel multiplier') + need(sum(r*c for r, c in targets.items())-sum(r*c for r, c in paid.items()) == 608, + 'rank-one conservation surplus') + # No huge integer 2**onset_exponent is constructed. LOCAL_LIMIT.md reduces + # the remaining analytic terms to these small exact endpoint inequalities. + need(Q(15, onset_exponent) < Q(1, 10**8), 'uniform LLT accuracy') + need(2**100 > 10**18 and onset_exponent >= 100, 'G0 dominates coarse cutoff') + retained = 3*total_variation*Q(1, 10**8) + middle = 17*total_variation*qbound**3001 + high = 8*total_variation/(Q(3, 500)**2*10**18) + leaf = Q(1, 5) + tails = Q(2, 10**7) + need(retained < 1563 and middle < Q(1, 1000) and high < 1, 'mixed error budget') + need(retained+middle+high+leaf+tails < 1600, 'complete error budget') + need(Q(8, 3)**36 > 10**15, 'geometric elementary exponential bound') + need(Q(163, 60)**37 > 10**16, 'leaf elementary exponential bound') + need(Q(30010+5*15010**2, 10**18) < Q(1, 10**8), 'mixed Gaussian flattening') + need(Q(1, 10**8)+Q(5000*5002**2, 4*10**18) < Q(5, 10**8), + 'leaf Gaussian flattening') + return {'onset_log2': str(onset_exponent), 'n_LLT': '2^'+str(onset_exponent), + 'G0': '2*2^'+str(onset_exponent)+'+2', 'N0': '121*5^G0', + 'kernel_multiplier': total_variation, 'normalized_error_upper': 1600, + 'normalized_capacity_margin_lower': 38400, + 'majorant': 'L(n) <= N0^(261/100000) * n^(99739/100000), n>=1'} + + +def words(law, length, cap): + result = Counter({1: 1}) + for _ in range(length): + following = Counter() + for product, count in result.items(): + for rank, multiplicity in law.items(): + if product*rank <= cap: + following[product*rank] += count*multiplicity + result = following + return result + + +def decomposition(paid, targets, n, truncate_terminal=False, omit_layer=False): + cap, height, least = n//121, 0, 1 + while 5*least <= cap: + height, least = height+1, 5*least + source, boundary, leaf = Counter(), Counter(), Counter() + for z, count in words(targets, height, cap).items(): + for k, c in targets.items(): + source[k*z] += count*c + for z, count in words(paid, height, cap).items(): + for r, c in paid.items(): + if not truncate_terminal or r*z <= cap: + leaf[r*z] += count*c + for h in range(height): + if omit_layer and h == 0: + continue + for x, cx in words(targets, h, cap).items(): + for y, cy in words(paid, height-1-h, cap).items(): + z = x*y + for r, pr in paid.items(): + for k, tk in targets.items(): + count = cx*cy*pr*tk + if r*z <= cap < k*z: + source[r*k*z] += count + elif k*z <= cap < r*z: + boundary[r*k*z] += count + return source, boundary+leaf, boundary + + +def finite_controls(inputs, paid, targets): + module = types.ModuleType('authenticated_historical_flow') + path = 'research/direct-mixed-flow/flow.py' + exec(compile(inputs[path], path, 'exec'), module.__dict__) + ranks = (121, 122, 604, 605, 606, 3024, 3025, 3026, 15124, 15125) + for n in ranks: + actual = module.Flow(targets, paid, n).merged() + independent = decomposition(paid, targets, n) + need(independent == tuple(actual[k] for k in ('sources', 'exits', 'boundary_exits')), + 'complete ordered-word decomposition mismatch') + need(all(n < 121*z and z <= n for z in actual['sources']), 'source rank contract') + need(all(121*e <= 48*n and e < n for e in actual['exits']), 'exit rank contract') + reference = decomposition(paid, targets, 3025) + need(decomposition(paid, targets, 3025, truncate_terminal=True) != reference, + 'unpaid terminal truncation escaped control') + need(decomposition(paid, targets, 3025, omit_layer=True) != reference, + 'missing mixed layer escaped control') + rejected = 0 + for action in (lambda: constant_certificate(paid, targets, 100), + lambda: Box(1)/Box(-1, 1), + lambda: log_integer(0), lambda: exponential_point(7)): + try: + action() + except ValueError: + rejected += 1 + else: + raise ValueError('invalid hypothesis escaped control') + # Exact exponentials at zero and log-additivity provide different endpoint + # identities, while signed interval products challenge rounding direction. + need(exponential_point(0).lo <= 1 <= exponential_point(0).hi, 'exp zero') + log4 = log_integer(4)-2*log_integer(2) + need(log4.lo <= 0 <= log4.hi, 'logarithm additive control') + product = Box(-2, 3)*Box(-5, 7) + need(product.lo == -15 and product.hi == 21, 'signed interval product control') + return {'complete_histogram_fixtures': len(ranks), 'semantic_mutations': 2, + 'domain_rejections': rejected, 'arithmetic_controls': 3} + + +def main(): + inputs = authenticate() + paid, targets, width = inventory(inputs['research/direct-flow-leaf-walk/verify.py']) + result = {'status': 'PASS_EFFECTIVE_DIRECT_FLOW', 'numerical_hypotheses': + certify_law(paid, targets, width), 'uniform_constants': + constant_certificate(paid, targets), 'finite_controls': + finite_controls(inputs, paid, targets), 'no_new_kappa': True, + 'scope': 'Exact finite numerical premises and controls; written Fourier and full-flow proofs establish the universal bound.'} + print(json.dumps(result, indent=2)) + + +if __name__ == '__main__': + main()