From e8b83e96e63d6f85e54573424e4b2139cd7602ac Mon Sep 17 00:00:00 2001 From: pinterbanget Date: Thu, 22 Oct 2026 14:25:19 +0700 Subject: [PATCH 1/3] =?UTF-8?q?Independent=20proof=20check=20of=20#4532=20?= =?UTF-8?q?=C2=A72.2-2.3=20(the=20critical-root=20majorant=20under=20#4535?= =?UTF-8?q?'s=20=CE=BA):=20every=20step=20verified,=20no=20gap=20(no=20new?= =?UTF-8?q?=20=CE=BA)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-Authored-By: Claude Opus 5.5 --- research/pr4532-proof-check/.gitattributes | 1 + research/pr4532-proof-check/PR4532-PROOF.md | 585 ++++++++++++++++++++ research/pr4532-proof-check/README.md | 51 ++ research/pr4532-proof-check/SOURCES.json | 24 + research/pr4532-proof-check/TASK.json | 100 ++++ research/pr4532-proof-check/VERIFY.json | 20 + research/pr4532-proof-check/verify.py | 223 ++++++++ 7 files changed, 1004 insertions(+) create mode 100644 research/pr4532-proof-check/.gitattributes create mode 100644 research/pr4532-proof-check/PR4532-PROOF.md create mode 100644 research/pr4532-proof-check/README.md create mode 100644 research/pr4532-proof-check/SOURCES.json create mode 100644 research/pr4532-proof-check/TASK.json create mode 100644 research/pr4532-proof-check/VERIFY.json create mode 100644 research/pr4532-proof-check/verify.py diff --git a/research/pr4532-proof-check/.gitattributes b/research/pr4532-proof-check/.gitattributes new file mode 100644 index 0000000000..5a401f1ff8 --- /dev/null +++ b/research/pr4532-proof-check/.gitattributes @@ -0,0 +1 @@ +PR4532-PROOF.md -text diff --git a/research/pr4532-proof-check/PR4532-PROOF.md b/research/pr4532-proof-check/PR4532-PROOF.md new file mode 100644 index 0000000000..bdf142f26d --- /dev/null +++ b/research/pr4532-proof-check/PR4532-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/pr4532-proof-check/README.md b/research/pr4532-proof-check/README.md new file mode 100644 index 0000000000..f6832e9bcf --- /dev/null +++ b/research/pr4532-proof-check/README.md @@ -0,0 +1,51 @@ +# Independent proof check of #4532 §2.2–2.3: the funded critical-root majorant + +**Task:** independent-moment (independent source-bound coverage). **Base:** canonical main `f626db5c`. **No new κ.** + +hexapode's #4535 (conditional κ = 0.003020165) rests on Dillon's #4532 theorem. Under the critical-root hypotheses, the finite compiler's normalised leaf count satisfies + +```text +L(n) ≤ A n^(t*) (c + log n)^p, A = n0^(1−t*)/(c + log n0)^p, n0 = m·M^ℓ0. +``` + +My #4537 checked #4532's finite figures, and #4565 retuned the witness. This package checks the **written proof** of §2.2–2.3, step by step, in the form each step is used. The text is vendored as `PR4532-PROOF.md` (blob `bdf142f2`, SHA256-pinned), from #4535 head `a6d7237f`. + +## Results + +Every checked step holds. I found no gap. + +| Step | What is checked | How | +|---|---|---| +| S1 | `(ln f)' = τ/x` and `f''/f = x^−2[τ(τ−1) − p/(c+log x)²]` | identity of rational functions in `(t, p, y = c+log x)` with `dy/dx = 1/x`, exact at 2,000 random rational points | +| S2 | `τ ≤ 1 ⟸ c ≥ p/(1−t*)`; `(f/x)' = f(τ−1)/x² ≤ 0`; `f(n0) = n0`, hence `L(n) = n ≤ f(n)` on the base range | 60-digit decimals on log-spaced grids `1…n0` | +| S3 | (11): `f(e)/f(n) ≤ (e/n)^τ(n)` for `1 ≤ e ≤ n` (from `log(1+y) ≤ y`) | grids above `n0` | +| S4 | (12): `f(n) − f(n−s) ≥ τ f(n) s/n ≥ η(τ) f(n)(s/n)^τ` for `n/m < s ≤ n`, including `s = n` | grids above `n0` | +| S5 | the recurrence closure: (10) bounds the exit charge by inner-source capacity | algebraic chain on 5,000 random potentials | +| S6 | `K_ℓ`'s derivative numerator `a(c + log m + log 2) + (a−1) log M`, and `n < m·M^(ℓ+1)` for `C_n = ⌊n/m⌋`, `ℓ = ⌊log_M C_n⌋` | exact rational identity; 17,118 exhaustive integer cases | +| S7 | monotonicity directions behind the endpoint evaluation in `critical_guards`: forward ratios, tilted means, every mirror cell sum and `η` nondecreasing; the root-tail and moment-ratio endpoint bounds; (6) `log q(t) ≥ d(t − t*)` from the crossing | the actual p16 profile on 121-point grids over each witness's cover interval | + +S2–S4 and S7 are run for **both** witnesses: +- #4532's p16 witness: `M = 1024`, `a = b = 1`, `ℓ0 = 650`, `p = 2/5`, `c = 133`, cover `.997067`; +- my #4565 retuned witness: `M = 2^24`, `a = 3`, `b = 2`, `ℓ0 = 64`, `p = 3/10`, `c = 101`, cover `.99725`. + +**One remark, not a defect.** The proof bounds `log n < log m + (ℓ+1) log M + log 2`. The sharper `n < m·M^(ℓ+1)` (S6) shows the `log 2` is slack. Removing it would only enlarge `K_ℓ` slightly. + +## Verify + +```text +python3 -B research/pr4532-proof-check/verify.py +``` + +This runs in about 70 s with the standard library only. + +## Limitations + +- **Not re-proved.** The predecessor identities that #4532 imports from #4483 are not re-proved: the exact cancellation (2), the Chernoff bounds (7)–(9) and the mirror identity. My #4529 and #4551 check parts of them. +- **Not established.** Native, physical and outer premises are out of scope. +- **Finite checks.** The analytic inequalities are checked on finite grids, and S1 by exact evaluation at random rational points. Each is also a one-line calculus fact, given in the proof. + +## Open next questions + +- An independent proof check of #4532 §1.1, the mirror-slack integral identities that supply the mean gap and the rank-one surplus. First step: verify both integral identities exactly on the p16 cells as finite sums. + +Credit: Dillon (#4532), hexapode (#4535), zxv and Jacob Alan Sussman (#4483 compiler and majorant lineage). Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. diff --git a/research/pr4532-proof-check/SOURCES.json b/research/pr4532-proof-check/SOURCES.json new file mode 100644 index 0000000000..56b69922c9 --- /dev/null +++ b/research/pr4532-proof-check/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40", + "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/compact-joint-compiler/arithmetic/RESULT.json", + "usage": "input", + "git_blob": "514d12ce4d2d824a4e0a418022bba610c8aed8ff", + "sha256": "a6caaa2a6d6460a8c1ef7e48c4853bb27976be33a52b96a4216dfa90d96c9091" + } + ] +} diff --git a/research/pr4532-proof-check/TASK.json b/research/pr4532-proof-check/TASK.json new file mode 100644 index 0000000000..95a1544cdc --- /dev/null +++ b/research/pr4532-proof-check/TASK.json @@ -0,0 +1,100 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 7, + "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1", + "original_card": { + "id": "independent-moment", + "question": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/staged544-mixed-fourth-entry/README.md", + "research/staged-fourth-mixture-ceiling/README.md", + "research/r437-two-window-carrier/README.md" + ], + "methods": [ + "Independently reconstruct one changed paid ledger or pooled dual with exact source and model binding.", + "Check a genuinely uncovered moment implication with a different enclosure method and semantic controls." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Choose one uncovered implication in #4088 literal mixed fill, #4091 pooled dual/model binding or #4067 changed frame/host bill. #4091 pins an earlier #4088 head: validate word, capacity and stock equivalence before applying that ceiling to the later fill.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Independently reconstruct one changed ledger or pooled certificate with a positive case and a semantic failure control. Compare exact sources and name what existing checks miss. Keep this separate from supplier-boundary-audit (ordinary/outer dispatch) and uniform-transfer-audit (all-size proof). Stop after the chosen implication; more digits of an unchanged root are not additional mechanism coverage.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification.", + "Calling an aggregate histogram or source archive an independently accepted physical supplier." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering", + "4088", + "4091", + "4067", + "staged544-mixed-fourth-entry", + "staged-fourth-mixture-ceiling", + "r437-two-window-carrier" + ], + "existing_checks": [ + { + "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.", + "evidence": "research/staged-fourth-mixture-ceiling/README.md", + "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.", + "status": "author-checked", + "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.", + "evidence": "research/r437-two-window-carrier/README.md", + "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.", + "status": "author-checked", + "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "unchanged", + "actual_scope": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?", + "scope_change_reason": null, + "bottleneck_link": "Independent proof-level coverage of the majorant theorem underlying the best open conditional kappa (#4535).", + "budget_minutes": 45, + "stop_rule": "Stop at #4532 sections 2.2-2.3.", + "outcome": "completed", + "evidence": "S1 identity (2,000 exact points); S2-S4 base range, (11), (12) on 60-digit grids for both witnesses; S5 closure chain; S6 K_ell identity and 17,118 integer rank cases; S7 monotonicity directions and (6) on the p16 profile over both cover intervals; 6 statements bound.", + "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance", + "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance; no independent human review.", + "open_questions": [ + { + "question": "Independent proof check of #4532 section 1.1 (mirror-slack integral identities).", + "why_it_matters": "They supply the mean gap and rank-one surplus used at the crossing.", + "first_step": "Verify both identities exactly on the p16 cells as finite sums.", + "blocked_by": "None." + } + ] +} diff --git a/research/pr4532-proof-check/VERIFY.json b/research/pr4532-proof-check/VERIFY.json new file mode 100644 index 0000000000..aff837e170 --- /dev/null +++ b/research/pr4532-proof-check/VERIFY.json @@ -0,0 +1,20 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/compact-joint-compiler/arithmetic/RESULT.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 300, + "checks": "Step-by-step check of #4532 sections 2.2-2.3 (identity, base range, (11), (12), closure, K_ell, rank bound, monotonicity directions, (6)) on both p16 witnesses; binding to vendored PROOF.md (sha256)." + } + ] +} diff --git a/research/pr4532-proof-check/verify.py b/research/pr4532-proof-check/verify.py new file mode 100644 index 0000000000..11145c505a --- /dev/null +++ b/research/pr4532-proof-check/verify.py @@ -0,0 +1,223 @@ +#!/usr/bin/env python3 +"""Independent proof check of PR #4532 (Dillon), PROOF.md sections 2.2-2.3: the funded critical-root majorant +L(n) <= A n^t (c + log n)^p used by #4535 (kappa = 0.003020165). Text vendored from #4535 head a6d7237f. + +Every analytic step of section 2.3 is checked in the form it is used: + S1 (ln f)' = tau/x and f''/f = x^-2 [tau(tau-1) - p/(c+log x)^2]: identity of rational functions in (t, p, y = c+log x) + after the chain rule dy/dx = 1/x, checked exactly at 2,000 random rational points; + S2 tau(x) <= 1 for x >= 1 iff c >= p/(1-t); (f(x)/x)' = f(tau-1)/x^2 <= 0 and f(n0) = n0, so L(n) = n <= f(n) on the + base range (checked with 60-digit decimals on log-spaced grids for both witnesses below); + S3 (11) f(e)/f(n) <= (e/n)^tau(n) for 1 <= e <= n (log(1+y) <= y), on grids; + S4 (12) f(n) - f(n-s) >= tau(n) f(n) s/n >= eta(tau(n)) f(n) (s/n)^tau(n) for n/m < s <= n, including s = n, on grids; + S5 the recurrence closure: with (10), the exit charge is bounded by inner-source capacity (algebraic chain, checked + on random nonnegative potentials satisfying (10)); + S6 K_ell's derivative numerator a(c + log m + log 2) + (a-1) log M (exact rational identity) and n < m M^(ell+1) + for C_n = floor(n/m), ell = floor(log_M C_n) (exhaustive integer ranges); + S7 the monotonicity directions that the endpoint evaluation in critical_guards relies on, on the actual p16 profile + over each witness's cover interval: T(t+s)/T(t) and P(t+s)/P(t) nondecreasing, tilted means nondecreasing, every + mirror cell sum nondecreasing, eta increasing, and (6) log q(t) >= d (t - t*) from the isolated crossing. +Witnesses: #4532's p16 (M = 1024, a = b = 1, ell0 = 650, p = 2/5, c = 133, cover .997067) and #4565's retuned +(M = 2^24, a = 3, b = 2, ell0 = 64, p = 3/10, c = 101, cover .99725). +Ryanson Jonathan with Claude Code (Claude Opus 5.5) assistance. Apache-2.0. +""" +import decimal +from decimal import Decimal as D +from fractions import Fraction as Fr +import hashlib +import json +import math +from pathlib import Path +import random +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SPEC = HERE / "PR4532-PROOF.md" # #4535 head a6d7237f, research/adaptive-gate-existence/PROOF.md, blob bdf142f2 +SPEC_SHA256 = "340d637feef40f44a808c718207c0fede12cc483e2c979b86c56bb736b9c1ef5" +PROFILE = ROOT / "research/compact-joint-compiler/arithmetic/RESULT.json" +PROFILE_SHA256 = "a6caaa2a6d6460a8c1ef7e48c4853bb27976be33a52b96a4216dfa90d96c9091" +T_STAR = D("0.99697983402295") # inside #4535's bracket [0.9969798340229, 0.996979834023] +WITNESSES = { + "4532_p16": dict(M=1024, a=1, b=1, ell=650, p=Fr(2, 5), c=133, s=Fr(1, 20), lam=Fr(1, 10), d=Fr(103, 100), top=D("0.997067")), + "4565_retuned": dict(M=1 << 24, a=3, b=2, ell=64, p=Fr(3, 10), c=101, s=Fr(1, 10), lam=Fr(1, 5), d=Fr(104, 100), top=D("0.99725")), +} + + +def need(condition, message): + if not condition: + raise AssertionError(message) + + +decimal.getcontext().prec = 60 + + +def S1(rng): + for _ in range(2000): + t = Fr(rng.randint(1, 999), 1000) + p = Fr(rng.randint(1, 999), 1000) + y = Fr(rng.randint(1, 10 ** 6), 1000) + x = Fr(rng.randint(1, 10 ** 6), 1000) + tau = t + p / y + gp = tau / x # (ln f)' = t/x + p/(x y) + need(gp == t / x + p / (x * y), "(ln f)'") + gpp = -tau / x ** 2 + (-p / y ** 2) * (1 / x) / x # d/dx (tau/x) with dtau/dx = -p/(y^2 x) + need(gpp + gp ** 2 == (tau * (tau - 1) - p / y ** 2) / x ** 2, "f''/f identity") + return 2000 + + +def fval(w, x): + lnx = D(x).ln() + n0 = D(145) * D(w["M"]) ** w["ell"] + p = D(w["p"].numerator) / w["p"].denominator + c = D(w["c"]) + lnA = (1 - T_STAR) * n0.ln() - p * (c + n0.ln()).ln() + return (lnA + T_STAR * lnx + p * (c + lnx).ln()).exp(), p, c + + +def tau(w, x): + p = D(w["p"].numerator) / w["p"].denominator + return T_STAR + p / (D(w["c"]) + D(x).ln()) + + +def S2_S3_S4(): + checks = 0 + for name, w in WITNESSES.items(): + p = w["p"] + need(Fr(w["c"]) >= p / (1 - Fr(str(T_STAR))), "c >= p/(1-t)") + need(tau(w, 1) <= 1, "tau(1) <= 1") + n0 = 145 * w["M"] ** w["ell"] + f0, _, _ = fval(w, n0) + need(abs(f0 / D(n0) - 1) < D(10) ** -40, "f(n0) = n0") + # S2: base range, log-spaced integers 1..n0. + for k in range(0, 60): + n = max(1, int(D(n0) ** (D(k) / 59))) + need(fval(w, n)[0] >= D(n) * (1 - D(10) ** -40), "L(n) = n <= f(n) on the base range") + checks += 1 + # S3 and S4 on grids above n0. + m = 145 + for kn in range(1, 12): + n = n0 * (7 ** kn) + kn + fn = fval(w, n)[0] + tn = tau(w, n) + eta = tn * D(m) ** (tn - 1) + for ke in range(0, 16): + e = max(1, int(D(n) ** (D(ke) / 15))) + need(fval(w, e)[0] / fn <= (D(e) / D(n)) ** tn * (1 + D(10) ** -40), "(11)") + checks += 1 + for frac in (Fr(1, 145) + Fr(1, 10 ** 6), Fr(1, 100), Fr(1, 10), Fr(1, 2), Fr(9, 10), Fr(1)): + s = max(n // m + 1, (n * frac.numerator) // frac.denominator) + fns = fval(w, n - s)[0] if n - s >= 1 else D(0) + need(fn - fns >= tn * fn * D(s) / D(n) * (1 - D(10) ** -40), "(12) concavity step") + need(tn * D(s) / D(n) >= eta * (D(s) / D(n)) ** tn * (1 - D(10) ** -40), "(12) eta step") + checks += 1 + return checks + + +def S5(rng): + for _ in range(5000): + eta = Fr(rng.randint(500, 999), 1000) + I = Fr(rng.randint(1, 10 ** 6), 7) + BF = eta * I * Fr(rng.randint(0, 1000), 1000) # (10): B + F <= eta I + fn = Fr(rng.randint(1, 10 ** 6), 11) + exit_charge_upper = fn * BF # sum_e E_e f(e) <= f(n) sum_e E_e (e/n)^tau = f(n) (B+F) / n^tau, normalised + capacity_lower = fn * eta * I # sum_inner S_s (f(n) - f(n-s)) >= f(n) eta I / n^tau, normalised + need(exit_charge_upper <= capacity_lower, "recurrence closure") + return 5000 + + +def S6(rng): + for _ in range(2000): + a = rng.randint(1, 8) + cp = Fr(rng.randint(1, 10 ** 5), 100) + L = Fr(rng.randint(1, 10 ** 4), 100) + ell = Fr(rng.randint(1, 10 ** 4), 10) + need(a * (cp + (ell + 1) * L) - (a * ell + 1) * L == a * cp + (a - 1) * L, "K_ell derivative numerator") + n_cases = 0 + for m in (2, 3, 145): + for M in (2, 3, 4, 1024): + for n in range(m * M, m * M ** 3 + 50, max(1, (m * M ** 3) // 3000)): + C = n // m + ell = 0 + while M ** (ell + 1) <= C: + ell += 1 + need(n < m * M ** (ell + 1), "n < m M^(ell+1)") + n_cases += 1 + return n_cases + + +def S7(): + prof = json.loads(PROFILE.read_bytes()) + need(hashlib.sha256(PROFILE.read_bytes()).hexdigest() == PROFILE_SHA256, "pinned p16 profile") + T = {int(k): v for k, v in prof["targets"].items()} + P = {int(k): v for k, v in prof["paid"].items()} + m = max(T) + + def mom(h, t): + return sum(c * k ** t for k, c in h.items()) + + def mean(h, t): + return sum(c * k ** t * math.log(k) for k, c in h.items()) / mom(h, t) + + pts = sorted({0.0, *(1 / k for k in T), *(1 / r for r in P)}) + cells = [] + for left, right in zip(pts, pts[1:]): + x = (left + right) / 2 + src, ex = {}, {} + for k, w in T.items(): + for r, cnt in P.items(): + if k > r and 1 / k < x <= 1 / r: + src[k * r] = src.get(k * r, 0) + w * cnt + if r > k and 1 / r < x <= 1 / k: + ex[k * r] = ex.get(k * r, 0) + w * cnt + cells.append((src, ex)) + # isolate the crossing in floats (validation only; the certified bracket is #4535's) + lo, hi = 0.9969, 0.9971 + for _ in range(80): + mid = (lo + hi) / 2 + lo, hi = (mid, hi) if mom(T, mid) < mom(P, mid) else (lo, mid) + ts = lo + checks = 0 + for name, w in WITNESSES.items(): + top = float(w["top"]) + s, lam, d = float(w["s"]), float(w["lam"]), float(w["d"]) + grid = [ts + (top - ts) * k / 120 for k in range(121)] + prev = None + for t in grid: + cur = (mom(T, t + s) / mom(T, t), mom(P, t + s) / mom(P, t), mean(T, t), mean(P, t), + [mom(src, t) for src, _ in cells], [mom(ex, t) for _, ex in cells], t * m ** (t - 1)) + need(math.log(mom(T, t) / mom(P, t)) >= d * (t - ts) - 1e-12, "(6) from the crossing") + need(mom(T, t - lam) / mom(P, t) <= mom(T, top - lam) / mom(P, ts) * (1 + 1e-12), "root-tail endpoint bound") + need(mom(T, t) / mom(P, t) <= mom(T, top) / mom(P, ts) * (1 + 1e-12), "moment-ratio endpoint bound") + if prev is not None: + need(cur[0] >= prev[0] * (1 - 1e-13) and cur[1] >= prev[1] * (1 - 1e-13), "forward ratios nondecreasing") + need(cur[2] >= prev[2] - 1e-13 and cur[3] >= prev[3] - 1e-13, "tilted means nondecreasing") + need(all(a >= b * (1 - 1e-13) for a, b in zip(cur[4], prev[4])), "source cells nondecreasing") + need(all(a >= b * (1 - 1e-13) for a, b in zip(cur[5], prev[5])), "exit cells nondecreasing") + need(cur[6] > prev[6], "eta increasing") + prev = cur + checks += 1 + return checks, ts + + +def check_binding(): + raw = SPEC.read_bytes() + need(hashlib.sha256(raw).hexdigest() == SPEC_SHA256, "vendored #4532 PROOF.md") + text = raw.decode("utf-8") + for s in ("f(e)/f(n) <= (e/n)^tau(n).", "f(n)-f(n-s) >= tau(n) f(n) s/n", "a(c+log m+log 2)+(a-1)log M > 0.", + "q(t) >= exp[d(t-t_*)]", "f''(x)/f(x)=x^(-2)[tau(x)(tau(x)-1)-p/(c+log x)^2]<=0.", + "sum_s S_s f(n-s)+sum_e E_e f(e) <= (sum_s S_s) f(n)."): + need(s in text, f"PROOF.md states: {s}") + return 6 + + +def main(): + rng = random.Random(45321) + s7, ts = S7() + report = {"status": "PASS_PR4532_PROOF_CHECK", "S1_identity_points": S1(rng), "S2_S3_S4_grid_checks": S2_S3_S4(), + "S5_closure_cases": S5(rng), "S6_integer_cases": S6(rng), "S7_profile_grid_points": s7, + "float_crossing": ts, "spec_statements_bound": check_binding(), "new_kappa_claimed": False} + print(json.dumps(report, indent=1)) + + +if __name__ == "__main__": + sys.exit(main()) From 2ef4e8e67da057894407b529d445fa5f73a8aa94 Mon Sep 17 00:00:00 2001 From: pinterbanget Date: Thu, 22 Oct 2026 14:32:19 +0700 Subject: [PATCH 2/3] Add #4532 section 1.1 mirror-slack identities as exact finite sums on the p16 windows Co-Authored-By: Claude Opus 5.5 --- research/pr4532-proof-check/README.md | 5 +-- research/pr4532-proof-check/TASK.json | 10 +++--- research/pr4532-proof-check/verify.py | 49 +++++++++++++++++++++++++-- 3 files changed, 54 insertions(+), 10 deletions(-) diff --git a/research/pr4532-proof-check/README.md b/research/pr4532-proof-check/README.md index f6832e9bcf..077a0c8b8e 100644 --- a/research/pr4532-proof-check/README.md +++ b/research/pr4532-proof-check/README.md @@ -1,4 +1,4 @@ -# Independent proof check of #4532 §2.2–2.3: the funded critical-root majorant +# Independent proof check of #4532 §1.1 and §2.2–2.3: the funded critical-root majorant **Task:** independent-moment (independent source-bound coverage). **Base:** canonical main `f626db5c`. **No new κ.** @@ -16,6 +16,7 @@ Every checked step holds. I found no gap. | Step | What is checked | How | |---|---|---| +| S0 | §1.1: `∫(S−E)dz/z = PT' − TP'` and `∫(S−E)z^(t−2)dz = (P(t)T(1) − T(t)P(1))/(1−t)`; strict slack gives a positive mean gap | exact finite sums over the actual p16 windows at seven exponents, 50-digit decimals | | S1 | `(ln f)' = τ/x` and `f''/f = x^−2[τ(τ−1) − p/(c+log x)²]` | identity of rational functions in `(t, p, y = c+log x)` with `dy/dx = 1/x`, exact at 2,000 random rational points | | S2 | `τ ≤ 1 ⟸ c ≥ p/(1−t*)`; `(f/x)' = f(τ−1)/x² ≤ 0`; `f(n0) = n0`, hence `L(n) = n ≤ f(n)` on the base range | 60-digit decimals on log-spaced grids `1…n0` | | S3 | (11): `f(e)/f(n) ≤ (e/n)^τ(n)` for `1 ≤ e ≤ n` (from `log(1+y) ≤ y`) | grids above `n0` | @@ -46,6 +47,6 @@ This runs in about 70 s with the standard library only. ## Open next questions -- An independent proof check of #4532 §1.1, the mirror-slack integral identities that supply the mean gap and the rank-one surplus. First step: verify both integral identities exactly on the p16 cells as finite sums. +- With §1.1 now covered here, the remaining unchecked part of #4532 is §3, the exact feasibility criterion for the tail gates, which #4535 does not need. First step: check its `H(λ)` characterisation on the p16 profile. Credit: Dillon (#4532), hexapode (#4535), zxv and Jacob Alan Sussman (#4483 compiler and majorant lineage). Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. diff --git a/research/pr4532-proof-check/TASK.json b/research/pr4532-proof-check/TASK.json index 95a1544cdc..db84b125ca 100644 --- a/research/pr4532-proof-check/TASK.json +++ b/research/pr4532-proof-check/TASK.json @@ -84,16 +84,16 @@ "scope_change_reason": null, "bottleneck_link": "Independent proof-level coverage of the majorant theorem underlying the best open conditional kappa (#4535).", "budget_minutes": 45, - "stop_rule": "Stop at #4532 sections 2.2-2.3.", + "stop_rule": "Stop at #4532 sections 1.1 and 2.2-2.3.", "outcome": "completed", - "evidence": "S1 identity (2,000 exact points); S2-S4 base range, (11), (12) on 60-digit grids for both witnesses; S5 closure chain; S6 K_ell identity and 17,118 integer rank cases; S7 monotonicity directions and (6) on the p16 profile over both cover intervals; 6 statements bound.", + "evidence": "S0 section 1.1 identities as exact finite sums on the p16 windows (7 exponents); S1 identity (2,000 exact points); S2-S4 on 60-digit grids for both witnesses; S5 closure; S6 K_ell identity and 17,118 integer cases; S7 monotonicity directions and (6) on both cover intervals; 6 statements bound.", "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance", "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance; no independent human review.", "open_questions": [ { - "question": "Independent proof check of #4532 section 1.1 (mirror-slack integral identities).", - "why_it_matters": "They supply the mean gap and rank-one surplus used at the crossing.", - "first_step": "Verify both identities exactly on the p16 cells as finite sums.", + "question": "Independent check of #4532 section 3 (exact tail-gate feasibility criterion).", + "why_it_matters": "Completes #4532; not needed by #4535.", + "first_step": "Check the H(lambda) characterisation on the p16 profile.", "blocked_by": "None." } ] diff --git a/research/pr4532-proof-check/verify.py b/research/pr4532-proof-check/verify.py index 11145c505a..ff9e0be499 100644 --- a/research/pr4532-proof-check/verify.py +++ b/research/pr4532-proof-check/verify.py @@ -1,8 +1,10 @@ #!/usr/bin/env python3 -"""Independent proof check of PR #4532 (Dillon), PROOF.md sections 2.2-2.3: the funded critical-root majorant +"""Independent proof check of PR #4532 (Dillon), PROOF.md sections 1.1 and 2.2-2.3: the funded critical-root majorant L(n) <= A n^t (c + log n)^p used by #4535 (kappa = 0.003020165). Text vendored from #4535 head a6d7237f. -Every analytic step of section 2.3 is checked in the form it is used: +Every analytic step of section 2.3 is checked in the form it is used, and section 1.1's identities: + S0 the two mirror-slack integral identities (dz/z gives P T' - T P'; z^(t-2) dz gives (P(t)T(1) - T(t)P(1))/(1-t)), + as exact finite sums over the actual p16 windows at seven exponents, and strict-slack positivity; S1 (ln f)' = tau/x and f''/f = x^-2 [tau(tau-1) - p/(c+log x)^2]: identity of rational functions in (t, p, y = c+log x) after the chain rule dy/dx = 1/x, checked exactly at 2,000 random rational points; S2 tau(x) <= 1 for x >= 1 iff c >= p/(1-t); (f(x)/x)' = f(tau-1)/x^2 <= 0 and f(n0) = n0, so L(n) = n <= f(n) on the @@ -199,6 +201,47 @@ def mean(h, t): return checks, ts +def S0(): + """Section 1.1: the two mirror-slack integral identities, as exact finite sums over the actual p16 windows. + + For pair (r, k) with coefficient P_r W_k (rk)^t: a source window (1/k, 1/r] (k > r) or an exit window (1/r, 1/k] + (r > k) integrated against dz/z gives the same signed log(k/r); against z^(t-2) dz it gives + (k r^t - r k^t)/(1 - t) (k > r) or minus the mirrored value (r > k). Summing must give P T' - T P' and + (P(t) T(1) - T(t) P(1))/(1 - t). Integrals are evaluated cell by cell from the window endpoints; checked at 7 + exponents with 50-digit decimals, plus the strict-slack positivity (1 - beta) * integral of S > 0. + """ + prof = json.loads(PROFILE.read_bytes()) + T = {int(k): v for k, v in prof["targets"].items()} + P = {int(k): v for k, v in prof["paid"].items()} + checks = 0 + for t in (D("0.5"), D("0.9"), D("0.99"), T_STAR, D("0.99725"), D("0.999"), D("0.3")): + lhs1 = lhs2 = D(0) + source_mass = D(0) + for k, w in T.items(): + for r, cnt in P.items(): + if k == r: + continue + coef = D(w * cnt) * (D(r) * D(k)) ** t + lo, hi = (D(1) / k, D(1) / r) if k > r else (D(1) / r, D(1) / k) + sign = 1 if k > r else -1 # source windows count positively, exit windows negatively + lhs1 += sign * coef * (hi.ln() - lo.ln()) + lhs2 += sign * coef * (hi ** (t - 1) - lo ** (t - 1)) / (t - 1) + if k > r: + source_mass += coef * (hi.ln() - lo.ln()) + Tt = sum(D(c) * D(k) ** t for k, c in T.items()) + Pt = sum(D(c) * D(r) ** t for r, c in P.items()) + Td = sum(D(c) * D(k) ** t * D(k).ln() for k, c in T.items()) + Pd = sum(D(c) * D(r) ** t * D(r).ln() for r, c in P.items()) + T1 = sum(D(c) * k for k, c in T.items()) + P1 = sum(D(c) * r for r, c in P.items()) + need(abs(lhs1 - (Pt * Td - Tt * Pd)) <= D(10) ** -30 * abs(Pt * Td), "dz/z identity = P T' - T P'") + need(abs(lhs2 - (Pt * T1 - Tt * P1) / (1 - t)) <= D(10) ** -30 * abs(Pt * T1), "z^(t-2) identity") + checks += 1 + # Strict slack: with E <= beta S pointwise (beta = .564 < 1), the dz/z integral is >= (1 - beta) * source mass > 0. + need(lhs1 > 0 and (1 - D("0.564")) * source_mass > 0, "strict mirror slack gives a positive mean gap") + return checks + + def check_binding(): raw = SPEC.read_bytes() need(hashlib.sha256(raw).hexdigest() == SPEC_SHA256, "vendored #4532 PROOF.md") @@ -213,7 +256,7 @@ def check_binding(): def main(): rng = random.Random(45321) s7, ts = S7() - report = {"status": "PASS_PR4532_PROOF_CHECK", "S1_identity_points": S1(rng), "S2_S3_S4_grid_checks": S2_S3_S4(), + report = {"status": "PASS_PR4532_PROOF_CHECK", "S0_section_1_1_identities": S0(), "S1_identity_points": S1(rng), "S2_S3_S4_grid_checks": S2_S3_S4(), "S5_closure_cases": S5(rng), "S6_integer_cases": S6(rng), "S7_profile_grid_points": s7, "float_crossing": ts, "spec_statements_bound": check_binding(), "new_kappa_claimed": False} print(json.dumps(report, indent=1)) From c4607e578e09a7cc7fe60ee0b7685b941822135d Mon Sep 17 00:00:00 2001 From: pinterbanget Date: Thu, 22 Oct 2026 14:35:53 +0700 Subject: [PATCH 3/3] Add #4532 section 3 tail-gate feasibility lemma checks on the p16 profile Co-Authored-By: Claude Opus 5.5 --- research/pr4532-proof-check/README.md | 6 ++- research/pr4532-proof-check/TASK.json | 10 ++--- research/pr4532-proof-check/verify.py | 65 ++++++++++++++++++++++++++- 3 files changed, 72 insertions(+), 9 deletions(-) diff --git a/research/pr4532-proof-check/README.md b/research/pr4532-proof-check/README.md index 077a0c8b8e..cdddb6c147 100644 --- a/research/pr4532-proof-check/README.md +++ b/research/pr4532-proof-check/README.md @@ -1,4 +1,4 @@ -# Independent proof check of #4532 §1.1 and §2.2–2.3: the funded critical-root majorant +# Independent proof check of #4532 §1.1, §2.2–2.3 and §3: the funded critical-root majorant **Task:** independent-moment (independent source-bound coverage). **Base:** canonical main `f626db5c`. **No new κ.** @@ -25,6 +25,8 @@ Every checked step holds. I found no gap. | S6 | `K_ℓ`'s derivative numerator `a(c + log m + log 2) + (a−1) log M`, and `n < m·M^(ℓ+1)` for `C_n = ⌊n/m⌋`, `ℓ = ⌊log_M C_n⌋` | exact rational identity; 17,118 exhaustive integer cases | | S7 | monotonicity directions behind the endpoint evaluation in `critical_guards`: forward ratios, tilted means, every mirror cell sum and `η` nondecreasing; the root-tail and moment-ratio endpoint bounds; (6) `log q(t) ≥ d(t − t*)` from the crossing | the actual p16 profile on 121-point grids over each witness's cover interval | +| S8 | §3 lemma: the convexity bound `H(λ) ≤ μ_T − log q/λ`; (13) at the crossing; the sufficiency construction (`g = 2`, `j = 9`, so `a = b = 1`, `M = 512`) passing all three gates; necessity on 149 random passing gate samples | p16 profile, floats | + S2–S4 and S7 are run for **both** witnesses: - #4532's p16 witness: `M = 1024`, `a = b = 1`, `ℓ0 = 650`, `p = 2/5`, `c = 133`, cover `.997067`; - my #4565 retuned witness: `M = 2^24`, `a = 3`, `b = 2`, `ℓ0 = 64`, `p = 3/10`, `c = 101`, cover `.99725`. @@ -47,6 +49,6 @@ This runs in about 70 s with the standard library only. ## Open next questions -- With §1.1 now covered here, the remaining unchecked part of #4532 is §3, the exact feasibility criterion for the tail gates, which #4535 does not need. First step: check its `H(λ)` characterisation on the p16 profile. +- #4532 is now covered: §1.1, §2.2–2.3 and §3 here, plus §4's counterexample in my #4537. What remains open is #4532's own question, replacing pointwise mirror slack by a bound against the capped measure. Credit: Dillon (#4532), hexapode (#4535), zxv and Jacob Alan Sussman (#4483 compiler and majorant lineage). Prepared by Ryanson Jonathan with substantial Claude Code (Claude Opus 5.5) assistance. diff --git a/research/pr4532-proof-check/TASK.json b/research/pr4532-proof-check/TASK.json index db84b125ca..49a24176e3 100644 --- a/research/pr4532-proof-check/TASK.json +++ b/research/pr4532-proof-check/TASK.json @@ -84,16 +84,16 @@ "scope_change_reason": null, "bottleneck_link": "Independent proof-level coverage of the majorant theorem underlying the best open conditional kappa (#4535).", "budget_minutes": 45, - "stop_rule": "Stop at #4532 sections 1.1 and 2.2-2.3.", + "stop_rule": "Stop at #4532 sections 1.1, 2.2-2.3 and 3.", "outcome": "completed", - "evidence": "S0 section 1.1 identities as exact finite sums on the p16 windows (7 exponents); S1 identity (2,000 exact points); S2-S4 on 60-digit grids for both witnesses; S5 closure; S6 K_ell identity and 17,118 integer cases; S7 monotonicity directions and (6) on both cover intervals; 6 statements bound.", + "evidence": "S0 section 1.1 identities as exact finite sums on the p16 windows (7 exponents); S1 identity (2,000 exact points); S2-S4 on 60-digit grids for both witnesses; S5 closure; S6 K_ell identity and 17,118 integer cases; S7 monotonicity directions and (6) on both cover intervals; 6 statements bound. S8 section 3 lemma on the p16 profile (convexity bound, (13), sufficiency construction, necessity on 149 samples).", "author": "Ryanson Jonathan, with Claude Code (Claude Opus 5.5) assistance", "ai_assistance": "Substantial Claude Code (Claude Opus 5.5) assistance; no independent human review.", "open_questions": [ { - "question": "Independent check of #4532 section 3 (exact tail-gate feasibility criterion).", - "why_it_matters": "Completes #4532; not needed by #4535.", - "first_step": "Check the H(lambda) characterisation on the p16 profile.", + "question": "Can pointwise mirror slack be replaced by a bound against the capped measure? (#4532's own question)", + "why_it_matters": "Would widen admissible profiles.", + "first_step": "Retain the exact base measure on one offending mirror window.", "blocked_by": "None." } ] diff --git a/research/pr4532-proof-check/verify.py b/research/pr4532-proof-check/verify.py index ff9e0be499..4bab2b635a 100644 --- a/research/pr4532-proof-check/verify.py +++ b/research/pr4532-proof-check/verify.py @@ -1,5 +1,5 @@ #!/usr/bin/env python3 -"""Independent proof check of PR #4532 (Dillon), PROOF.md sections 1.1 and 2.2-2.3: the funded critical-root majorant +"""Independent proof check of PR #4532 (Dillon), PROOF.md sections 1.1, 2.2-2.3 and 3: the funded critical-root majorant L(n) <= A n^t (c + log n)^p used by #4535 (kappa = 0.003020165). Text vendored from #4535 head a6d7237f. Every analytic step of section 2.3 is checked in the form it is used, and section 1.1's identities: @@ -15,6 +15,8 @@ on random nonnegative potentials satisfying (10)); S6 K_ell's derivative numerator a(c + log m + log 2) + (a-1) log M (exact rational identity) and n < m M^(ell+1) for C_n = floor(n/m), ell = floor(log_M C_n) (exhaustive integer ranges); + S8 section 3's tail-gate feasibility lemma on the p16 profile (convexity bound, (13) at the crossing, the + sufficiency construction, and necessity on random passing gate samples); S7 the monotonicity directions that the endpoint evaluation in critical_guards relies on, on the actual p16 profile over each witness's cover interval: T(t+s)/T(t) and P(t+s)/P(t) nondecreasing, tilted means nondecreasing, every mirror cell sum nondecreasing, eta increasing, and (6) log q(t) >= d (t - t*) from the isolated crossing. @@ -242,6 +244,65 @@ def S0(): return checks +def S8(rng): + """Section 3 lemma on the p16 profile (floats; validation of a written convexity proof). + + (i) the convexity bound H(lambda) <= mu_T(t) - log q(t)/lambda on a grid of t >= t* and lambda; + (ii) at the crossing, (13) T(t - lambda) exp(lambda mu_P) < P(t) holds for small lambda; + (iii) sufficiency: the proof's construction g, j, a = 1, b = g - 1, M = 2^j yields, for a small s, all three gates; + (iv) necessity: every random (a, b, M, s, lambda) passing the three gates has H(lambda) > mu_P(t). + """ + prof = json.loads(PROFILE.read_bytes()) + T = {int(k): v for k, v in prof["targets"].items()} + P = {int(k): v for k, v in prof["paid"].items()} + + def mom(h, t): + return sum(c * k ** t for k, c in h.items()) + + def mean(h, t): + return sum(c * k ** t * math.log(k) for k, c in h.items()) / mom(h, t) + + def H(t, lam): + return (math.log(mom(P, t)) - math.log(mom(T, t - lam))) / lam + + ts = float(T_STAR) + checks = 0 + for t in (ts, ts + 1e-4, ts + 1e-3, 0.999): + q = mom(T, t) / mom(P, t) + for lam in (1e-3, 1e-2, 0.05, 0.1, 0.3, 1.0): + need(H(t, lam) <= mean(T, t) - math.log(q) / lam + 1e-9, "convexity bound on H") + checks += 1 + muT, muP = mean(T, ts), mean(P, ts) + lam = 1e-3 + need(mom(T, ts - lam) * math.exp(lam * muP) < mom(P, ts), "(13) at the crossing") + delta = muT - muP + Hl = H(ts, lam) + g = 2 + while g * Hl / math.log(2) - (g * muP + delta) / math.log(2) <= 1: + g += 1 + j = math.floor((g * muP + delta) / math.log(2)) + 1 + need((g * muP + delta) / math.log(2) < j < g * Hl / math.log(2), "integer j inside the interval") + a, b, M = 1, g - 1, 2.0 ** j + s = 1e-4 + u = M ** (-s) * (mom(T, ts + s) / mom(T, ts)) ** a * (mom(P, ts + s) / mom(P, ts)) ** b + v = M ** lam * (mom(T, ts - lam) / mom(P, ts)) ** (a + b) + need(u < 1 and v < 1 and mom(T, ts + s) / mom(T, ts) >= mom(P, ts + s) / mom(P, ts), "constructed gates hold") + passing = 0 + for _ in range(4000): + a2, b2 = rng.randint(1, 6), rng.randint(1, 6) + M2 = 2.0 ** rng.randint(2, 40) + s2, lam2 = rng.uniform(0.001, 0.5), rng.uniform(0.001, 0.5) + t = ts + rng.uniform(0, 1e-3) + u2 = M2 ** (-s2) * (mom(T, t + s2) / mom(T, t)) ** a2 * (mom(P, t + s2) / mom(P, t)) ** b2 + v2 = M2 ** lam2 * (mom(T, t - lam2) / mom(P, t)) ** (a2 + b2) + order = mom(T, t + s2) / mom(T, t) >= mom(P, t + s2) / mom(P, t) + if u2 < 1 and v2 < 1 and order: + need(H(t, lam2) > mean(P, t), "necessity: gates imply H(lambda) > mu_P") + passing += 1 + need(passing > 50, "enough passing gate samples") + return {"convexity_points": checks, "constructed": {"g": g, "j": j}, "necessity_samples": passing} + + def check_binding(): raw = SPEC.read_bytes() need(hashlib.sha256(raw).hexdigest() == SPEC_SHA256, "vendored #4532 PROOF.md") @@ -257,7 +318,7 @@ def main(): rng = random.Random(45321) s7, ts = S7() report = {"status": "PASS_PR4532_PROOF_CHECK", "S0_section_1_1_identities": S0(), "S1_identity_points": S1(rng), "S2_S3_S4_grid_checks": S2_S3_S4(), - "S5_closure_cases": S5(rng), "S6_integer_cases": S6(rng), "S7_profile_grid_points": s7, + "S5_closure_cases": S5(rng), "S6_integer_cases": S6(rng), "S7_profile_grid_points": s7, "S8_section_3": S8(rng), "float_crossing": ts, "spec_statements_bound": check_binding(), "new_kappa_claimed": False} print(json.dumps(report, indent=1))