From e3f10b390ae5ddd998d238206add5958d5b720bb Mon Sep 17 00:00:00 2001 From: Dylan Roy Date: Mon, 28 Sep 2026 18:01:06 -0500 Subject: [PATCH 1/4] Add fixed-dimensional elder lower-event candidate via raw Schur chart One O(r) physical-jet band, determinant-one shear, stable transverse complement and full W/Z tilt. Conditional sharp density/inverse-moment corollaries; exact finite controls, no scientific-status promotion. --- .github/workflows/elder-dimension-lift.yml | 33 ++ .../elder_dimension_lift_20260928/PROOF.md | 480 ++++++++++++++++++ .../elder_dimension_lift_20260928/README.md | 31 ++ .../RECONNAISSANCE.md | 35 ++ .../RESULTS.json | 8 + .../SOURCE_FILES.json | 54 ++ .../SOURCE_MAP.json | 42 ++ .../elder_dimension_lift_20260928/lift.py | 149 ++++++ .../test_lift.py | 146 ++++++ .../elder_dimension_lift_20260928/verify.py | 96 ++++ 10 files changed, 1074 insertions(+) create mode 100644 .github/workflows/elder-dimension-lift.yml create mode 100644 frontiers/elder_dimension_lift_20260928/PROOF.md create mode 100644 frontiers/elder_dimension_lift_20260928/README.md create mode 100644 frontiers/elder_dimension_lift_20260928/RECONNAISSANCE.md create mode 100644 frontiers/elder_dimension_lift_20260928/RESULTS.json create mode 100644 frontiers/elder_dimension_lift_20260928/SOURCE_FILES.json create mode 100644 frontiers/elder_dimension_lift_20260928/SOURCE_MAP.json create mode 100644 frontiers/elder_dimension_lift_20260928/lift.py create mode 100644 frontiers/elder_dimension_lift_20260928/test_lift.py create mode 100644 frontiers/elder_dimension_lift_20260928/verify.py diff --git a/.github/workflows/elder-dimension-lift.yml b/.github/workflows/elder-dimension-lift.yml new file mode 100644 index 000000000..fcb467a25 --- /dev/null +++ b/.github/workflows/elder-dimension-lift.yml @@ -0,0 +1,33 @@ +name: Elder dimension-lift exact controls + +'on': + pull_request: + paths: + - 'frontiers/elder_dimension_lift_20260928/**' + - '.github/workflows/elder-dimension-lift.yml' + push: + branches: [main] + paths: + - 'frontiers/elder_dimension_lift_20260928/**' + - '.github/workflows/elder-dimension-lift.yml' + workflow_dispatch: + +permissions: + contents: read + +jobs: + finite-dimension-lift: + runs-on: ubuntu-latest + timeout-minutes: 10 + steps: + - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 + with: + persist-credentials: false + - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 + with: + python-version: '3.11.16' + - name: Exact sources, both modes and intended semantic failures + run: | + set -euo pipefail + python -B -S frontiers/elder_dimension_lift_20260928/verify.py --output "${RUNNER_TEMP}/dimension-lift-${GITHUB_RUN_ID}-${GITHUB_RUN_ATTEMPT}" + git diff --exit-code diff --git a/frontiers/elder_dimension_lift_20260928/PROOF.md b/frontiers/elder_dimension_lift_20260928/PROOF.md new file mode 100644 index 000000000..7303bd791 --- /dev/null +++ b/frontiers/elder_dimension_lift_20260928/PROOF.md @@ -0,0 +1,480 @@ +# One soft transverse direction: an elder-failure lower event in every fixed dimension + +Object: OA-ELDER-DIMENSION-LIFT-20260928-v1. +Author: OpenAI / ChatGPT, foreground research continuation, 28 September 2026. +Disposition: AUTHOR-SIDE MATHEMATICAL CANDIDATE; source-bound nonauthor review required. +Scientific effect NONE. No existing proof, review verdict, registry, lemma flag or prize is changed. + +## 1. Model, precise claims, and dependence boundaries + +Fix d>=2, L>0, a compact birth interval B, and a compact gap interval +K=[k_-,k_+] with k_->0. Use exactly LP's variance-one periodized Gaussian field, + + Cov(f(x),f(y)) = sum_{n in Z^d} exp(-|x-y+Ln|^2/2) + / sum_{n in Z^d} exp(-|Ln|^2/2). + +All constants may depend on d,L,B,K. The dimension is fixed: no uniform-in-d +claim is made. All orthonormal pin frames R are allowed, without assuming the +periodized field is invariant under arbitrary rotations. Set u=R e_1 and + + M=-(r/2)u, S=(r/2)u; + f(M)=b, f(S)=b-k r^3, grad f(M)=grad f(S)=0. + +Q_r denotes continuous Gaussian regression on these original 2(d+1) observations. +Let F_j(H)=|det H| for a nonsingular Hessian with j negative eigenvalues, and zero +otherwise. Retain the ORIGINAL determinant tilt and FULL endpoint normalizer: + + W_r=F_d(H_M) F_(d-1)(H_S), Z_r=E_Qr W_r, + dQ_r^W=(W_r/Z_r)dQ_r. + +There is no adjacency conditioning. Let p_r(b,k,R) be the probability that S is +M's global ordinary superlevel elder-death partner, exactly as in LP Section 1. +On its generic locus the death height is the maximin from LP Section 8: + + d_f(M)=sup_{gamma(0)=M, f(gamma(1))>b} min_t f(gamma(t)). (A1) + +The already integrated planar source EL proves an explicit path obstruction in +d=2. This note extends that mechanism to all fixed d. The new issue is the raw +Gaussian mass of a nearly flat transverse direction coupled to d-2 stable +negative directions. Requiring every extra matrix entry to be O(r) would lose +the desired probability power. A Schur-complement coordinate chart avoids that. + +**Theorem A (direct lower event).** For all sufficiently small r, uniformly over +b,k,R in the specified ranges, there is an event E_r such that + + Q_r^W(E_r)>=c r^3, + E_r implies d_f(M)>=b-k r^3/4>f(S). (A2) + +In particular + + 1-p_r(b,k,R)>=c r^3. (A3) + +The event can be chosen also to contain two distinct additional critical points +of index d-1 and heights strictly between b-k r^3 and b, within distance C_d r +of the midpoint. If N_r counts all additional critical points in that height +window, then + + Q_r^W(N_r>=2)>=c r^3, + E_Qr^W[N_r(N_r-1)]>=c r^3. (A4) + +The second expectation may be extended-valued; this argument supplies no finite +upper bound. For d>2 it does NOT establish Q(N_r>=2)=Theta(r^3), a uniform lower +bound on Q(N_r>=2 | N_r>=1), or a global first-moment upper bound. Those would +need their own inputs. A torus-wide O(r^5) factorial bound is excluded by (A4). +The event lower bound is likewise an obstruction of order at least r^3 to any +approximation supported solely on empty and singleton configurations. + +**Corollary B (separate parent-dependent compositions).** Consuming LP Theorem A +at its stated scope gives, in every fixed d>=2, + + c r^3<=1-p_r<=C r^3. (A5) + +Consuming additionally LP's compact-mark density identity, for positive-length +B,K, gives + + nu_cand(ell)-nu_eld(ell)=Theta(ell^(2/3)) (A6) + +for its COMPACT-MARK densities. The leading constant, a numerical c or r_*, +unrestricted-mark differences, and any identification with historical q-symbols +remain outside this statement. The d=3,L=24 specialization changes none of those +limitations. The direct lower (A3) does not consume the parent upper theorem. + +**Corollary C (sharp rejected-pair inverse-moment boundary).** Under the same +compact-mark density premises, let the nonselected counting measure count +candidate pairs which are not ordinary elder pairs. Directly on that measure, + + E sum_{nonselected, 00. In the finite regime it is Theta(t^(5/3-p)). At +p=5/3 the lower-cutoff divergence is logarithmic; above it it is a power. This +is not subtraction of two infinite individual inverse-moment expectations. + +The proof below uses only the positive spectrum/contact-frame and uniform +regression facts explicitly displayed in LP Sections 2-4, elementary Taylor +estimates, a stable negative block, and the original maximin definition. It does +not consume the pending remote pair/distance limits or a SARD-G theorem. + +## 2. Complete physical third-order jets after the pin frame + +Write the orthonormal local coordinates as (x,y), with x axial and y in R^m, +m=d-1. LP's nonsingular frame U_r is an invertible re-expression of the exact pins +for r>0; it has bounded target v_r and converges, uniformly in covariance and +fixed derivative cross-covariances, to + + U_0=(f,f_x,f_xx,f_xxx,f_y1,f_xy1,...,f_ym,f_xym) at 0. (A7) + +Append the physical midpoint vector J consisting of: + +- all independent entries A=D_y^2 f(0) of the transverse Hessian; +- all independent third-order derivatives T_alpha=partial^alpha f(0), |alpha|=3, + except f_xxx (which is already in U_0). + +At r=0 the entries of (U_0,J) are exactly every independent derivative of orders +0 through 3, once each. Their count is binom(d+3,3). No repeated symmetric entries +are presented as independent coordinates. + +Every Fourier weight of the periodized covariance is positive. A zero-variance +linear combination of these derivatives would give a polynomial vanishing at +every point of the rotated dual lattice. Pulling back by the invertible rotation +gives a polynomial vanishing on Z^d. Induction on dimension, using the univariate +root theorem on each lattice line, makes it identically zero. Thus the complete +jet covariance is positive definite in every frame. + +Continuity of U_r and compactness of O(d) give a uniform covariance floor and +ceiling for (U_r,J), for r in [0,r_1]. Schur complementation then gives a uniform +covariance sandwich for the Gaussian vector J under Q_r. Its mean is bounded +because v_r is bounded. Consequently, for EVERY fixed compact set of physical +J-targets, there is a uniform positive lower bound on its Lebesgue density there. +This is a bound for RAW jets, not for a falsely Gaussian nonlinear eigenvector +or normalized-Schur variable. + +## 3. A unit-Jacobian chart around one soft transverse direction + +For d=2 use the planar argument, or interpret the empty stable block below with +determinant one. We now give the new construction for d>=3. Write y=(z,w), +w in R^n, n=d-2, and decompose + + A = [[a, v^T], [v, D]], + sigma=a-v^T D^(-1)v. (A8) + +Restrict D to a fixed positive-volume box of symmetric matrices near -I_n, with + + -3I_n/2 < D < -I_n/2. + +Restrict v to a sufficiently small fixed box of positive volume, independent of +r, such that q=D^(-1)v satisfies ||q||<=1/9. The possible physical jets remain +bounded on this domain. Use the deterministic linear shear, frozen separately +for each realization of these midpoint jets, + + y = S(z,w) = (z,w-qz), + S=[[1,0],[-q,I_n]], det S=1, + S^T A S=diag(sigma,D). (A9) + +The full coordinate transformation is L=diag(1,S) after the orthonormal pin +frame. Its determinant has absolute value one. It preserves the axis x and the +original pin points. Both L and its inverse have uniformly bounded norms. It is +not generally orthogonal, and no rotation-invariance argument is applied to it. + +Define tilde f(x,z,w)=f(R L(x,z,w)). Here R,L are CONSTANT in spatial variables +within each realization. Thus differentiating tilde f does not differentiate a +randomly varying frame. Its midpoint transverse mixed quadratic terms are zero +exactly, its stable Hessian is D, and its soft second derivative is sigma. + +Let tau be the third derivatives of tilde f, except tau_xxx. For fixed v,D the +map from the original third derivatives to tau is invertible. Explicitly + + partial_z(tilde f)= (partial_z-q.partial_w)f, + partial_w(tilde f)=partial_w f, partial_x(tilde f)=partial_x f. + +On symmetric third-derivative coordinates this substitution is triangular with +unit diagonal when ordered by z degree. The pure xxx coordinate is fixed and +uncoupled; deleting it leaves determinant one. This observation is about finite +coordinate transformations, not the law of the resulting random variables. + +The map + + (sigma,v,D,tau) -> (a,v,D,T), + a=sigma+v^T D^(-1)v (A10) + +therefore has absolute Jacobian one. Its derivative is block triangular: the +Hessian part has derivative one in sigma and identity in the other coordinates; +the cubic part has determinant one, although it depends on v,D. Only D is +inverted; the chart remains regular when A is singular at sigma=0. + +This is the step preventing a dimension-dependent loss. Neither v nor the other +n(n+1)/2 stable entries has a shrinking width. The raw entry a itself need NOT +be O(r): it follows the O(1) surface v^T D^(-1)v within an O(r) band. + +## 4. The raw rare set has volume and probability of order r + +Fix a small epsilon>0, eventually independent of r, and retain the fixed D,v +boxes. In the chart require + + |sigma+(3k/2)r|=c_J r. (A13) + +The sheared jets need not be jointly Gaussian. We integrate the RAW Gaussian +density using the explicitly justified Jacobian; we never assign an independent +or rotation-invariant distribution to sigma, v, D or tau. Replacing sigma by +sigma/r without its r Jacobian would be incorrect. + +## 5. Remainder control is conditioned after ALL the physical jets + +Regress the full smooth field on V=(U_r,J) at each target (v_r,j) in the raw set. +For one unconditioned copy F the conditional realization is + + F(z)+Cov(F(z),V)Cov(V)^(-1)((v_r,j)-V). (A14) + +The normalized pin rows are integral averages of derivatives of order at most +three. Positive-spectrum rapid Fourier summability supplies uniform derivative +cross-covariance bounds through C^4, and all finite C^4 supremum moments of F. +The joint inverse covariance from Section 2 is bounded. The targets j lie in a +fixed compact set. Therefore, for each fixed finite p, + + sup E[||f||_C4^p | U_r=v_r,J=j] < infinity. (A15) + +Choose K_4 finite so the conditional probability of ||f||_C4<=K_4 is at least +1/2 at EVERY target in the raw rare set. Integrating (A15) over that set yields + + Q_r{rare jets AND ||f||_C4<=K_4} >= (c_J/2)r. (A16) + +The bounded shear converts this to a uniform local bound on ||tilde f||_C4. +There is no assertion of independence between the jet event and the remainder. +Subtracting a fixed unconditioned tail from a mass of order r is not used. + +The constants can be selected without circularity. Fix the D,v boxes and a +compact raw-target container valid for all epsilon<=1 and small r. Choose a +uniform K_4 from that container. Then choose epsilon for the planar stability +margins, and finally reduce r_* using K_4 and those margins. The positive c_J +may shrink with epsilon, but is fixed independently of r. + +## 6. Exact pinned planar normal form on the sheared plane + +Restrict to w=0, and put + + F_r(X,Z)=[tilde f(rX,rZ,0)-b]/r^3, + s=sigma/r, a_3=tau_xxz, beta=tau_xzz, c_3=tau_zzz. + +The original axial height and gradient pins, including the transverse gradient +pins in the sheared direction, are still exact. Taylor expansion as in the +planar source gives + + F_r = 2kX^3-3kX/2-k/2+(s/2)Z^2 + +(a_3/2)(X^2-1/4)Z+(beta/2)XZ^2+(c_3/6)Z^3 + + O_C2(B3)(r K_4), (A17) + +with a dimension-dependent constant absorbing the shear norm. For clarity the +potentially dangerous coefficients follow from the pin identities: + + tilde f_xxx(0)=12k+O(rK_4), + tilde f_x(0)=-(r^2/8)tilde f_xxx(0)+O(r^3K_4), + tilde f_z(0)=-(r^2/8)tilde f_xxz(0)+O(r^3K_4), + tilde f_xx(0), tilde f_xz(0)=O(r^2K_4), + tilde f(0)-b=-(r^3/24)tilde f_xxx(0)+O(r^4K_4). + +The second-derivative z^2 coefficient is sigma, not the raw a. No stable +quadratic term survives on w=0 because (A9) eliminates it exactly. +The term -a_3 Z/8 is necessary for the transverse gradient pins. + +On (A11), the polynomial part is O(epsilon k)-close in C^2(B3) to + + G_k(X,Z)=k(2X^3-3X/2-1/2-3Z^2/4-XZ^2). (A18) + +Choose epsilon and then r_* so the C^0 difference is strictly below k/64 and the +C^2 difference meets the endpoint and saddle stability tolerances below. +The higher-dimensional directions have introduced no extra r^-1 remainder. + +## 7. Stable path above the death pin + +Use the fixed polygonal path in the sheared plane + + (-1/2,0) -> (-3/4,0) -> (-3/4,9/4) -> (-1,9/4). (A19) + +Dividing by k, the restrictions of G_k to its three consecutive segments are + + -3t^2/16-t^3/32, + -7/32, + -7/32+51t/64-9t^2/32-t^3/32, 0<=t<=1. + +Their minimum is -7/32 and the final value is 17/64. The first is nonincreasing; +the third has derivative at least 9/64. Every segment is inside B(0,3), since +the maximal endpoint squared norm is 97/16<9 and the ball is convex. +A perturbation below k/64 leaves the path above -15k/64>-k/4 and its endpoint +above k/4. After applying the fixed shear, rotation and physical r scaling, the +path starts at the actual M and ends at a point above b, entirely above +b-k r^3/4. It remains inside an embedded O(r) ball by reducing r_*. + +This is a path in the physical torus, not a separatrix claim. It proves the +second statement in (A2) for every field in the event of (A16). The use of a +plane chosen from midpoint jets causes no probabilistic problem: existence of +ONE such path suffices, and the chart is a smooth measurable function of those +jets on the chosen stable-block domain. + +## 8. Full endpoint Hessians: only two directions are soft + +In the (x,z;w) shear frame, the physical endpoint Hessians have blocks + + H_i^tilde = [[r P_i+O(r^2 K_4), C_i], [C_i^T,D_i]], + ||C_i||<=C r K_4, D_i=D+O(r K_4), (A20) + +where P_i is the Hessian of the polynomial in (A17) at the corresponding scaled +endpoint. To verify the cross-block bound, at the midpoint tilde f_zw=0 exactly +by the shear, and tilde f_xw=O(r^2K_4) by the zero endpoint w-gradients. Moving +to either endpoint changes these entries by O(rK_4). The stable block remains +uniformly negative with bounded inverse for small r. + +The exact Schur complement is + + K_i=r P_i+O(r^2 K_4)-C_i D_i^(-1) C_i^T, + K_i/r=P_i+O(r K_4+r K_4^2). (A21) + +The correction must be included. The fact that it is smaller than r, rather +than zero, is what makes the construction stable. The target two-dimensional +endpoint Hessians are diag(-6k,-k/2) and diag(6k,-5k/2), with determinants 3k^2 +and -15k^2. Uniform smallness of epsilon and r preserves their indices and +strict determinant floors after (A21). + +Block congruence gives inertia(H_i^tilde)=inertia(D_i)+inertia(K_i), and + + det H_i^tilde = det D_i det K_i. (A22) + +Hence the physical endpoints have precisely the required indices d and d-1, +and EACH determinant has magnitude at least c r^2. The d-2 stable eigenvalues +remain O(1), not O(r). Because the shear determinant has absolute value one, +physical and sheared Hessian determinants agree; general invertible congruence +preserves their inertia as well. Thus on the event + + W_r >= c_W r^4. (A23) + +The r^4 power is independent of fixed d. Replacing it by r^(2d) would correspond +to incorrectly shrinking every spatial direction's curvature. + +For the FULL normalizer, the original endpoint gradient pins give zero averages +of H u along the axial segment. Thus ||H_i u||<=C r ||f||_C3. Hadamard yields +|det H_i|<=C r (1+||f||_C3)^d, so + + Z_r <= C_Z r^2 (A24) + +by the endpoint-conditioned moment bounds of LP Section 4. The positive event +(A16),(A23) ensures Z_r>0. No restricted normalizer is used. Combining gives + + Q_r^W(E_r) >= (c_J c_W/(2C_Z)) r*r^4/r^2 = c r^3. (A25) + +Together with the path, this proves (A2)-(A3), in every fixed d>=3; EL covers +d=2. No parent upper selection theorem entered this argument. + +## 9. Two additional saddles with a stable negative complement + +A planar restriction critical point is NOT automatically a full-dimensional +critical point. We explicitly correct the stable coordinates. + +Near either planar saddle P_+ or P_- of G_k, with + + P_+/-=(-3/4,+/-sqrt(15/8)), G_k(P_+/-)=-7k/32, + det H_2 G_k(P_+/-)=-15k^2/2, + +write x=rX, z=rZ, w=r^2 W. Consider the rescaled FULL gradient map + + H_r(X,Z,W)=r^(-2) grad tilde f(rX,rZ,r^2W). (A26) + +On bounded (X,Z,W) sets, Taylor and the pin identities give in C^1 + + H_r = (grad P(X,Z), D W+Q(X,Z)) + O(r C(K_4)), (A27) + +where P is the two-dimensional polynomial in (A17), and the stable-vector +quadratic polynomial is + + Q_j(X,Z)=(tau_xxwj/2)(X^2-1/4) + +tau_xzwj XZ+(tau_zzwj/2) Z^2. (A28) + +In particular the -tau_xxwj/8 term comes from tilde f_wj(0), and is retained. +All its coefficients lie in fixed small boxes. The absence of an order-r +linear z term in the stable gradient uses tilde f_zw(0)=0 exactly. The two soft +gradient components have no O(1) dependence on W because their physical mixed +Hessian is O(r); varying w by r^2 W contributes only O(r) after /r^2. +The C^1 estimates require at most the uniform C^4 bound, not an assumed exact +cubic random field. + +For epsilon small, P has one nondegenerate saddle near each P_+/- by ordinary +C^2 stability. At such a point p, the limit vector map in (A27) has a zero at +(p,-D^(-1)Q(p)). Its derivative is block triangular with diagonal blocks H_2P(p) +and D, so its inverse is uniformly bounded over the compact jet boxes. These +zeros persist for the C^1-small perturbation (A27), uniformly after reducing r_*. +This can equivalently be obtained by a quantitative inverse-function argument +on fixed disjoint neighborhoods. The solutions have w=O(r^2); they are not +assumed to lie exactly in the w=0 plane. + +Their physical heights are b+r^3[G_k(P_+/-)+O(epsilon k)+O(r C(K_4))], strictly +inside the height window for small epsilon,r. Their full Hessian has a negative +stable block and a two-dimensional Schur complement with one negative and one +positive eigenvalue, just as in (A20)-(A22). Both therefore have index d-1. +Their physical positions lie in an O(r) ball and are distinct from each other +and the original pins. This proves the additional event in (A4); the factorial +inequality follows from N(N-1)>=2 on that event. + +Uniformity here is on the compact family of jets and stable blocks for a FIXED +d. It does not assert a uniform number of all critical points or the persistence +pairing of either extra saddle. The separate strict path gives the elder +obstruction; mere extra-point existence would not do so. + +## 10. Parent-dependent selection and density consequences + +LP Theorem A gives the opposite inequality 1-p_r<=C r^3. When consumed with +(A3), it proves (A5) and shows the Gaussian order r^3 is sharp at every fixed +d, not merely for the matrix relaxation or the planar model. + +For LP's ordered compact-mark candidate/elder densities, its exact radial ledger +is r A_r(b,k,u) dr db dk d sigma(u), with A_r uniformly positive and bounded, +and ell=k r^3. Consequently the density difference is + + ell^(-1/3)/3 * integral k^(-2/3) A_((ell/k)^(1/3))(b,k,u) + [1-p_((ell/k)^(1/3))(b,k,u)] d sigma dk db. + +The lower factor (A3) contributes ell/k. The upper factor is supplied separately +by LP Theorem A. Both bounding integrands are proportional to +ell^(2/3) k^(-5/3), integrable and of positive integral on positive-length compact +B,K and the ordinary sphere measure. This proves (A6). Integrating over +0-1, proving +(A6a). At p=5/3, truncation to eta5/3 it +gives Theta(eta^(5/3-p)) as eta decreases to zero for fixed small t. In the +finite regime the result is Theta(t^(5/3-p)), not a claimed leading constant. +The ordinary candidate and elder inverse-moment threshold 2/3 from LP Section 12 +is different. Here a rejected-pair measure is used, never infinity minus infinity. +For d=2 this is already a consequence of the integrated planar lower and LP; +for d>2 it additionally uses the new dimensional lower proof. + +For d>2 we do not import the PLANAR global first-moment estimate (IW I5) to +claim a global multiple-occurrence upper bound or conditional nonuniqueness +bounded away from zero. Only (A4) and the corresponding unconditioned TV lower +obstruction follow without another global upper input. This is intentionally +weaker than those extra planar conclusions in LOCAL_MULTIPLICITY.md. + +## 11. What is new, what is checked, and what remains for review + +The planar cubic, path and raw-jet conditioning mechanism are credited to the +unchanged EL/LOCAL sources. The new step is the full-dimensional raw Schur chart: +one shrinking scalar band, determinant-one data-dependent shear, all other +coordinates in fixed-volume boxes, and a stable negative complement. The +Gaussian law is never changed to an independently rotated or sheared ensemble. + +The exact suite checks nonorthogonal shear cancellation, the chart through a +singular contact Hessian, unit cubic-jet Jacobians, the complete nonduplicated +jet list, a finite polynomial-lattice unisolvence illustration, exact planar +pins, the path, full-dimensional Hessian determinants/inertia, the cross-block +Schur correction, stable-coordinate displacement scaling, and exponent ledgers. +It deliberately rejects replacing r by r^(d-1), r^4 by r^(2d), dropping the raw +band Jacobian, dropping transverse pin terms, and reversing the stable sign. + +Finite checks do NOT prove covariance floors, uniform conditional C^4 estimates, +uniform inverse-function neighborhoods or the Gaussian probability inequality. +Those arguments are the written Sections 2-9 and require an actual nonauthor +analytic review. The finite Fourier illustration is not substituted for positivity +of the infinite exact periodized spectrum. The code is a new shear/Schur module, +not recovery or a retry of the blocked author algebra.py from #116. + +Source identities, limited primary-source reconnaissance, and the precise role +of each parent are in SOURCE_MAP.json and RECONNAISSANCE.md. This candidate +changes no old source or canonical scientific status and claims no historical +priority. All constants and cutoffs in the Gaussian result remain existential. diff --git a/frontiers/elder_dimension_lift_20260928/README.md b/frontiers/elder_dimension_lift_20260928/README.md new file mode 100644 index 000000000..716c27595 --- /dev/null +++ b/frontiers/elder_dimension_lift_20260928/README.md @@ -0,0 +1,31 @@ +# Dimensional lift of the direct elder-failure lower event + +Author-side candidate; nonauthor analytic review required. Scientific effect NONE. + +[PROOF.md](PROOF.md) extends the original planar cubic/path mechanism to every +fixed d>=2 using a physical Hessian Schur chart and a determinant-one shear. +Only one raw scalar band has width O(r); stable transverse modes stay O(1). +The proposed direct result is 1-p_r>=c r^3 under the original full determinant +tilt. Two additional index-(d-1) window critical points persist after correcting +the stable coordinates by O(r^2). + +With separately named LP upper/density premises: the r^3 order and compact-mark +ell^(2/3) density loss are sharp in every fixed dimension. The rejected-pair +inverse-moment threshold is p<5/3; its endpoint divergence is logarithmic. +This does not assert any new all-height/global factorial upper bound, uniform-in-d +constant, numerical cutoff, unrestricted-mark difference or legacy q/p identity. + +Run the complete source/finite-control verification: + + python -B -S verify.py --output /path/to/new-output + python -B -O -S verify.py --output /path/to/other-new-output + +The output directory must be new and outside this source directory. Each runner +checks exact membership/bytes/SHA256/Git blob identities, executes both Python +modes, and requires every semantic negative to fail the intended assertion with +valid JSON and no execution errors. The 18 finite tests and 10 semantic mutants +are not proofs of the Gaussian uniformity or inverse-function arguments. + +[Source map](SOURCE_MAP.json) separates direct inputs from conditional corollary +inputs. [Reconnaissance](RECONNAISSANCE.md) records the limited literature read +and Consensus quota limitation. No frozen source or review is rewritten. diff --git a/frontiers/elder_dimension_lift_20260928/RECONNAISSANCE.md b/frontiers/elder_dimension_lift_20260928/RECONNAISSANCE.md new file mode 100644 index 000000000..dd56b21f2 --- /dev/null +++ b/frontiers/elder_dimension_lift_20260928/RECONNAISSANCE.md @@ -0,0 +1,35 @@ +# Limited primary-source reconnaissance — 28 September 2026 + +Scope: derivative geometry and critical-point correlations near collisions; +not a claim of novelty, first discovery, or an exhaustive priority audit. + +Consensus was called for Gaussian critical points, higher-dimensional Hessian +Schur complements and elder persistence. It returned its monthly 30-search quota +error with an October 1 reset. No result was invented or cited from that call. + +The following primary-source abstracts/publisher records were inspected with web +search. No external theorem is used as an unexamined replacement for this proof: + +1. Jean-Marc Azaïs and Céline Delmas, *Mean number and correlation function of + critical points of isotropic Gaussian fields and some results on GOE random + matrices*, arXiv:1911.02300; Stochastic Processes and their Applications 150 + (2022), 411-445, DOI 10.1016/j.spa.2022.04.013. + https://arxiv.org/abs/1911.02300 + This already studies adjacent-index short-range correlation effects in the + unconditioned isotropic setting. Such adjacency by itself is not a novelty + claim for this project. It does not by its abstract establish this exact + pair-conditioned full-tilt elder obstruction or its compact-window loss. +2. Louis Gass and Michele Stecconi, *The number of critical points of a Gaussian + field: finiteness of moments*, Probability Theory and Related Fields 190 + (2024), 1167-1197, DOI 10.1007/s00440-024-01273-5. + https://doi.org/10.1007/s00440-024-01273-5 + The record addresses finite moments under jet nondegeneracy. Its conclusions + are not automatically uniform at this coalescing conditioned pair, and no + global O(r^3) first moment or factorial upper bound is imported from it. + +The actual positive-spectrum, pin-frame and uniform-regression ingredients are +read from the exact LP source in SOURCE_MAP.json. The new construction is proved +thereafter with a raw physical-jet chart, not an assumed isotropic GOE law or +independent soft eigenvector. Schur complementation, congruence, Taylor bounds, +and nondegenerate-zero stability are classical; the proof writes out their role. +The generic peer-review and governing status boundaries remain separate. diff --git a/frontiers/elder_dimension_lift_20260928/RESULTS.json b/frontiers/elder_dimension_lift_20260928/RESULTS.json new file mode 100644 index 000000000..457fcb8bc --- /dev/null +++ b/frontiers/elder_dimension_lift_20260928/RESULTS.json @@ -0,0 +1,8 @@ +{ + "tests_per_mode": 18, + "semantic_mutants_per_mode": 10, + "identical_output_pairs": 11, + "all_intended_failures": true, + "scientific_effect": "NONE", + "gaussian_analysis_verified_by_code": false +} diff --git a/frontiers/elder_dimension_lift_20260928/SOURCE_FILES.json b/frontiers/elder_dimension_lift_20260928/SOURCE_FILES.json new file mode 100644 index 000000000..11a80bd6d --- /dev/null +++ b/frontiers/elder_dimension_lift_20260928/SOURCE_FILES.json @@ -0,0 +1,54 @@ +{ + "schema": 1, + "scientific_effect": "NONE", + "files": [ + { + "path": "PROOF.md", + "bytes": 23971, + "sha256": "b529fe3780e1909014b3cb144b9a74156d976bbdc19b6711d0c5b1a1da9e5669", + "git_blob": "7303bd791a68a1139251f0f6e403a9f7cc89b006" + }, + { + "path": "README.md", + "bytes": 1771, + "sha256": "64950f041cee272079f4dd5e04dcf2293f5ed6d8c3ee231df8817d2d10fce2ac", + "git_blob": "716c275954910521102d1e154ef526360f19d908" + }, + { + "path": "RECONNAISSANCE.md", + "bytes": 2214, + "sha256": "d6f0bb97f4555ebb44b06df5d35d12f90fb746bbef45fb2053b8294d6621ed28", + "git_blob": "dd56b21f2da20be803f431357c5de49e6efbf452" + }, + { + "path": "RESULTS.json", + "bytes": 205, + "sha256": "57dba071afd0e53e1317f165b5170dd0a69a456fef41d50b2f775d33ffd123f5", + "git_blob": "457fcb8bc2bcd84ad0b25c67be8869fefb9681b8" + }, + { + "path": "SOURCE_MAP.json", + "bytes": 2106, + "sha256": "8cdedee5300ecc64bc5e38ea94d9bf263f0d87c4b75ccba67fb108edcf7013b1", + "git_blob": "713cad893e3d922c971a866f9b6accd89758f6d1" + }, + { + "path": "lift.py", + "bytes": 5514, + "sha256": "e17fa8384b6d5e516223499efff26354da0d84de9ba3e9ea3d96cfe75373ee9d", + "git_blob": "03d6827ac66afeb04f70153108aa195668e58a22" + }, + { + "path": "test_lift.py", + "bytes": 6109, + "sha256": "6901d40a216db622ee6cf82dc2092cdd7cd7dae261ea81b2c00fbb72a6f4a02b", + "git_blob": "c3ff861519c6b522ad8ca049c2f1aebecebae623" + }, + { + "path": "verify.py", + "bytes": 4910, + "sha256": "f79ba38b27c40ec86b5d2bbec4f5c9891fbe27c62ba328b6d58769b6f04469dd", + "git_blob": "7bbd0612ebae56c8b05c97d22142f0086a3549cd" + } + ] +} diff --git a/frontiers/elder_dimension_lift_20260928/SOURCE_MAP.json b/frontiers/elder_dimension_lift_20260928/SOURCE_MAP.json new file mode 100644 index 000000000..713cad893 --- /dev/null +++ b/frontiers/elder_dimension_lift_20260928/SOURCE_MAP.json @@ -0,0 +1,42 @@ +{ + "scientific_effect": "NONE", + "source_repository": "d6g8k5htny-coder/Math-", + "source_commit": "d39dbbc25c25a7bc3f6c15b21f957a7fcac30615", + "inputs": [ + { + "id": "LP", + "path": "imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md", + "bytes": 40261, + "sha256": "9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7", + "git_blob": "dfed3b8d318a3ab1950957f393307733a4bef3f2", + "direct_use": "Exact model, original pins/tilt/selector, Sections 2-4 positive spectrum and contact regression; Section 8 generic locus/maximin.", + "conditional_corollary_use": "Theorem A upper bound and Sections 9-12 compact-mark density ledger/moments; not required for the new direct lower proof." + }, + { + "id": "EL", + "path": "frontiers/window_multiplicity_laws_20260928/ELDER_LOWER_AND_DENSITY_GAP.md", + "bytes": 10229, + "sha256": "8ce05a43bde8e0d718f09e2da1ffe75d3ec5893489254afdbf5b58b602cdba0c", + "git_blob": "aaefc8da9668e819591dd9db0b34442394f2362e", + "use": "Unchanged planar cubic/path and lower event; basis of d=2 and credited mechanism, not an assumed d>2 proof." + }, + { + "id": "LOCAL", + "path": "frontiers/window_multiplicity_laws_20260928/LOCAL_MULTIPLICITY.md", + "bytes": 13100, + "sha256": "e6272e8709835ca6290fecb7034fa84832dde08c3c4cc990a48b8019e89e7c8d", + "git_blob": "b5c18aac5529c5f975ee5bb056b304debafc6697", + "use": "Planar normal-form and extra-saddle data. Its planar global first-moment upper estimate is NOT imported for d>2." + } + ], + "new_obligations": [ + "Complete physical-jet covariance floor in every fixed dimension", + "Nonlinear raw Schur/shear chart with unit Jacobian and one shrinking coordinate", + "Conditional C4 control on raw jets before choosing the spatial shear", + "Full-dimensional endpoint Schur bounds and anisotropic saddle persistence" + ], + "pending_pair_distance_sources_consumed": false, + "historical_blocked_code_consumed_or_retried": false, + "nonauthor_acceptance": false, + "governing_status_changed": false +} diff --git a/frontiers/elder_dimension_lift_20260928/lift.py b/frontiers/elder_dimension_lift_20260928/lift.py new file mode 100644 index 000000000..03d6827ac --- /dev/null +++ b/frontiers/elder_dimension_lift_20260928/lift.py @@ -0,0 +1,149 @@ +"""Exact finite helpers for the one-soft-transverse-direction construction. + +No Gaussian continuum claim follows from these computations. Standard library only. +""" +from fractions import Fraction as F +from itertools import product +from math import factorial + +MUTANT=None + +def eye(n): return [[F(int(i==j)) for j in range(n)] for i in range(n)] +def tr(A): return [list(c) for c in zip(*A)] +def mm(A,B): + return [[sum((x*y for x,y in zip(row,col)),F(0)) for col in zip(*B)] for row in A] + +def solve(A,b): + n=len(A) + if n==0 or len(b)!=n or any(len(row)!=n for row in A): + raise ValueError('nonempty square linear system required') + W=[[F(x) for x in row]+[F(b[i])] for i,row in enumerate(A)] + for j in range(n): + p=next((i for i in range(j,n) if W[i][j]),None) + if p is None: raise ValueError('singular matrix') + W[j],W[p]=W[p],W[j] + pivot=W[j][j]; W[j]=[x/pivot for x in W[j]] + for i in range(n): + if i!=j: + v=W[i][j]; W[i]=[x-v*y for x,y in zip(W[i],W[j])] + return [row[-1] for row in W] + +def det(A): + n=len(A) + if not n:return F(1) + W=[[F(x) for x in row] for row in A]; out=F(1) + for j in range(n): + p=next((i for i in range(j,n) if W[i][j]),None) + if p is None:return F(0) + if p!=j:W[j],W[p]=W[p],W[j];out=-out + pivot=W[j][j];out*=pivot + for i in range(j+1,n): + z=W[i][j]/pivot + for k in range(j+1,n):W[i][k]-=z*W[j][k] + return out + +def rank(A): + W=[[F(x) for x in row] for row in A] + if not W:return 0 + h=0 + for j in range(len(W[0])): + p=next((i for i in range(h,len(W)) if W[i][j]),None) + if p is None:continue + W[h],W[p]=W[p],W[h];pivot=W[h][j] + for i in range(h+1,len(W)): + z=W[i][j]/pivot + if z: + for k in range(j,len(W[0])):W[i][k]-=z*W[h][k] + h+=1 + if h==len(W):break + return h + +def chart(D,v,sigma): + q=solve(D,v);n=len(D) + sign=-1 if MUTANT=='wrong-schur-sign' else 1 + a=F(sigma)+sign*sum((x*y for x,y in zip(v,q)),F(0)) + A=[[a,*v]]+[[v[i],*D[i]] for i in range(n)] + S=eye(n+1) + for i in range(n):S[i+1][0]=F(0) if MUTANT=='omit-shear' else -q[i] + return A,S + +def multiindices(d,degree,upto=False): + return [a for a in product(range(degree+1),repeat=d) if sum(a)<=degree] if upto else [a for a in product(range(degree+1),repeat=d) if sum(a)==degree] + +def monomial(x,a): + out=1 + for u,p in zip(x,a):out*=u**p + return out + +def jet_labels(d): + zero=(0,)*d; e=[tuple(int(i==j) for j in range(d)) for i in range(d)] + plus=lambda a,b:tuple(x+y for x,y in zip(a,b)) + ex=e[0]; two=plus(ex,ex);three=plus(two,ex) + U=[zero,ex,two,three] + for j in range(1,d):U += [e[j],plus(ex,e[j])] + J=[a for a in multiindices(d,3,upto=True) if a not in U] + if MUTANT=='duplicate-cubic-pin':J[-1]=three + return U,J + +def _pmul(P,Q): + R={} + for a,c in P.items(): + for b,e in Q.items(): + k=tuple(x+y for x,y in zip(a,b));R[k]=R.get(k,F(0))+c*e + return {a:c for a,c in R.items() if c} + +def cubic_change(d,q): + """Map third-derivative coordinates by f -> f(x,z,w-q z); pure xxx stays fixed.""" + labels=multiindices(d,3);M=[[F(0) for _ in labels] for _ in labels] + unit=[tuple(int(i==j) for j in range(d)) for i in range(d)] + substitutions=[{u:F(1)} for u in unit] + for j,v in enumerate(q):substitutions[j+2][unit[1]]=-v + def mf(a): + out=1 + for x in a:out*=factorial(x) + return out + for j,a in enumerate(labels): + P={(0,)*d:F(1,mf(a))} + for i,power in enumerate(a): + for _ in range(power):P=_pmul(P,substitutions[i]) + for i,b in enumerate(labels):M[i][j]=P.get(b,F(0))*mf(b) + return labels,M + +def rare_power(d):return d-1 if MUTANT=='rare-every-direction' else 1 +def weight_power(d):return 2*d if MUTANT=='all-directions-soft' else 4 +def band_width(r,k,epsilon):return 2*epsilon*k*(1 if MUTANT=='drop-band-jacobian' else r) + +def plane(X,Z,k,s,a,beta,c): + lin=0 if MUTANT=='drop-transverse-linear' else F(1,4) + value=2*k*X**3-F(3,2)*k*X-k/2+s*Z*Z/2+a*(X*X-lin)*Z/2+beta*X*Z*Z/2+c*Z**3/6 + dx=6*k*X*X-F(3,2)*k+a*X*Z+beta*Z*Z/2 + dz=s*Z+a*(X*X-lin)/2+beta*X*Z+c*Z*Z/2 + return value,[dx,dz] + +def blocks(A,C,D): + return [list(A[i])+list(C[i]) for i in range(len(A))]+[list(row)+list(D[i]) for i,row in enumerate(tr(C))] + +def schur(A,C,D): + invC=tr([solve(D,row) for row in C]);Q=mm(C,invC) + if MUTANT=='ignore-cross-schur':Q=[[F(0) for _ in A] for _ in A] + return [[A[i][j]-Q[i][j] for j in range(len(A))] for i in range(len(A))] + +def endpoint_model(d,r,k): + stable=1 if MUTANT=='positive-stiff' else -1 + def diag(vals):return [[v if i==j else F(0) for j in range(d)] for i,v in enumerate(vals)] + return diag([-6*k*r,-k*r/2]+[F(stable)]*(d-2)),diag([6*k*r,-5*k*r/2]+[F(stable)]*(d-2)) + +def inertia(A): + """Exact Descartes signs for a real-rooted characteristic polynomial of a symmetric matrix.""" + n=len(A);coef=[F(1)];B=eye(n) + for k in range(1,n+1): + AB=mm(A,B);c=-sum(AB[i][i] for i in range(n))/k + coef.append(c);B=[[AB[i][j]+(c if i==j else 0) for j in range(n)] for i in range(n)] + asc=list(reversed(coef));z=0 + while z0 for i,v in enumerate(asc) if v] + neg=sum(a!=b for a,b in zip(signs,signs[1:])) + return neg,z + +def loss_powers(): + return (F(-1,3)+(0 if MUTANT=='omit-loss-factor' else 1),F(-2,3)-1) diff --git a/frontiers/elder_dimension_lift_20260928/test_lift.py b/frontiers/elder_dimension_lift_20260928/test_lift.py new file mode 100644 index 000000000..c3ff86151 --- /dev/null +++ b/frontiers/elder_dimension_lift_20260928/test_lift.py @@ -0,0 +1,146 @@ +"""Finite exact controls, not a Gaussian-field theorem checker.""" +import itertools +import unittest +from fractions import Fraction as F +import lift as m + +class LiftTests(unittest.TestCase): + def test_nonorthogonal_shear_cancels_midpoint_cross_terms(self): + D = [[F(-2), F(1,5)], [F(1,5), F(-3)]] + v = [F(1,4), F(-1,7)] + sigma = F(-3,200) + A, S = m.chart(D,v,sigma) + wanted = [[sigma,F(0),F(0)], [F(0),*D[0]], [F(0),*D[1]]] + self.assertEqual(m.mm(m.tr(S),m.mm(A,S)),wanted) + self.assertNotEqual(m.mm(m.tr(S),S),m.eye(3)) + self.assertEqual(m.det(S),1) + + def test_raw_soft_entry_need_not_be_order_r(self): + A,_ = m.chart([[F(-1)]],[F(1,5)],F(-1,100)) + self.assertEqual(A[0][0],F(-1,20)) + self.assertEqual(A[0][0]-F(1,5)**2/F(-1),F(-1,100)) + + def test_chart_extends_through_singular_contact(self): + A,S = m.chart([[F(-1)]],[F(1,5)],F(0)) + self.assertEqual(m.det(A),0) + self.assertEqual(m.det(S),1) + + def test_full_dimension_determinant_identity(self): + for n in range(1,5): + D = [[-F(i+2) if i==j else F(0) for j in range(n)] for i in range(n)] + v = [F(i+1,20) for i in range(n)] + A,_ = m.chart(D,v,F(-1,17)) + self.assertEqual(m.det(A),F(-1,17)*m.det(D)) + + def test_cubic_tensor_change_has_unit_jacobian(self): + for d in range(3,6): + labels,T = m.cubic_change(d,[F(i+1,20) for i in range(d-2)]) + self.assertEqual(m.det(T),1) + pure = labels.index((3,)+(0,)*(d-1)) + self.assertEqual(T[pure],[F(int(j==pure)) for j in range(len(labels))]) + reduced = [[v for j,v in enumerate(row) if j!=pure] + for i,row in enumerate(T) if i!=pure] + self.assertEqual(m.det(reduced),1) + + def test_raw_chart_volume_is_one_power_of_r(self): + for d in range(2,9): + self.assertEqual(m.rare_power(d),1) + r = F(1,13) + self.assertEqual(m.band_width(r,F(6,5),F(1,100)),F(12,6500)) + + def test_complete_contact_jet_labels(self): + for d in range(2,8): + U,J = m.jet_labels(d) + self.assertEqual(len(U),2*(d+1)) + self.assertEqual(len(U+J),len(set(U+J))) + self.assertEqual(set(U+J),set(m.multiindices(d,3,upto=True))) + + def test_polynomial_lattice_unisolvence(self): + for d in (2,3,4): + labels = m.multiindices(d,3,upto=True) + V = [[m.monomial(n,a) for a in labels] for n in itertools.product(range(4),repeat=d)] + self.assertEqual(m.rank(V),len(labels)) + self.assertEqual(m.rank([row+[row[0]] for row in V]),len(labels)) + + def test_plane_pins_with_free_transverse_cubic(self): + k,s,a,beta,c = F(6,5),F(-2),F(3,7),F(-4,5),F(2,3) + for X,val in ((F(-1,2),0),(F(1,2),-k)): + f,g = m.plane(X,F(0),k,s,a,beta,c) + self.assertEqual(f,val) + self.assertEqual(g,[0,0]) + + def test_plane_path_polynomials(self): + k=F(6,5) + for t in [F(i,16) for i in range(17)]: + pts=[(-F(1,2)-t/4, F(0)),(-F(3,4),9*t/4),(-F(3,4)-t/4,F(9,4))] + want=[-3*t*t/16-t**3/32,F(-7,32),-F(7,32)+51*t/64-9*t*t/32-t**3/32] + for (X,Z),w in zip(pts,want): + f,_=m.plane(X,Z,k,-3*k/2,0,-2*k,0) + self.assertEqual(f,k*w) + self.assertGreater(F(-7,32)-F(1,64),F(-1,4)) + self.assertGreater(F(17,64)-F(1,64),0) + + def test_path_survives_bounded_spatial_shear(self): + q=F(1,9) + maxnorm=F(97,16) + self.assertLess((1+q)**2*maxnorm,16) + + def test_two_extra_saddle_data(self): + X,z2=F(-3,4),F(15,8) + self.assertEqual(6*X*X-F(3,2)-z2,0) + self.assertEqual(F(3,2)+2*X,0) + self.assertEqual(2*X**3-F(3,2)*X-F(1,2)-(F(3,4)+X)*z2,F(-7,32)) + self.assertEqual(-4*z2,F(-15,2)) + self.assertLess(X*X+z2,4) + + def test_stiff_modes_do_not_change_weight_power(self): + for d in range(2,9): + self.assertEqual(m.weight_power(d),4) + for r in (F(1,4),F(1,16),F(1,64)): + HM,HS=m.endpoint_model(d,r,F(1)) + self.assertEqual(abs(m.det(HM)*m.det(HS)),45*r**4) + self.assertEqual(m.inertia(HM),(d,0)) + self.assertEqual(m.inertia(HS),(d-1,0)) + + def test_endpoint_cross_blocks_need_schur_correction(self): + D=[[F(-2),F(0)],[F(0),F(-3)]] + for r in (F(1,4),F(1,16),F(1,64)): + A=[[-6*r,F(0)],[F(0),-r/2]] + C=[[r/7,r/11],[r/13,r/17]] + H=m.blocks(A,C,D) + K=m.schur(A,C,D) + self.assertEqual(m.det(H),m.det(D)*m.det(K)) + self.assertNotEqual(K,A) + self.assertEqual(m.inertia(H),(4,0)) + error=max(abs((K[i][j]-A[i][j])/r) for i in range(2) for j in range(2)) + self.assertLess(error,r) + + def test_stiff_elimination_is_order_r_squared(self): + D=[[F(-2),F(0)],[F(0),F(-3)]] + Q=[F(1,7),F(-2,9)] + z=m.solve(D,Q) + for r in (F(1,4),F(1,16),F(1,64)): + ell=[r*r*v for v in Q] + w=[-r*r*v for v in z] + for i in range(2): + self.assertEqual(sum(D[i][j]*w[j] for j in range(2))+ell[i],0) + correction=sum(w[i]*D[i][j]*w[j]/2 for i in range(2) for j in range(2))+sum(ell[i]*w[i] for i in range(2)) + self.assertEqual(correction/r**3,-r*sum(Q[i]*z[i] for i in range(2))/2) + + def test_determinant_tilt_ledger_all_dimensions(self): + for d in range(2,9): + self.assertEqual(m.rare_power(d)+m.weight_power(d)-2,3) + + def test_density_loss_ledger(self): + self.assertEqual(m.loss_powers(),(F(2,3),F(-5,3))) + self.assertEqual(F(2,3)+1,F(5,3)) + # ell=u^3 gives ell^(2/3-p) d ell = 3 u^(4-3p) du. + self.assertEqual(4-3*F(5,3),-1) + self.assertGreater(4-3*F(3,2),-1) + self.assertLess(4-3*F(2),-1) + + def test_singular_stable_block_is_excluded(self): + with self.assertRaises(ValueError): + m.chart([[F(0)]],[F(1)],F(1)) + +if __name__=='__main__': unittest.main() diff --git a/frontiers/elder_dimension_lift_20260928/verify.py b/frontiers/elder_dimension_lift_20260928/verify.py new file mode 100644 index 000000000..7bbd0612e --- /dev/null +++ b/frontiers/elder_dimension_lift_20260928/verify.py @@ -0,0 +1,96 @@ +"""Source-bound exact finite controls; not a verification of Gaussian analysis.""" +import argparse +import hashlib +import io +import json +from pathlib import Path +import subprocess +import sys +import unittest + +ROOT=Path(__file__).resolve().parent +MUTANTS={ + 'wrong-schur-sign':'test_nonorthogonal_shear_cancels_midpoint_cross_terms', + 'omit-shear':'test_nonorthogonal_shear_cancels_midpoint_cross_terms', + 'rare-every-direction':'test_raw_chart_volume_is_one_power_of_r', + 'all-directions-soft':'test_stiff_modes_do_not_change_weight_power', + 'drop-band-jacobian':'test_raw_chart_volume_is_one_power_of_r', + 'duplicate-cubic-pin':'test_complete_contact_jet_labels', + 'drop-transverse-linear':'test_plane_pins_with_free_transverse_cubic', + 'ignore-cross-schur':'test_endpoint_cross_blocks_need_schur_correction', + 'positive-stiff':'test_stiff_modes_do_not_change_weight_power', + 'omit-loss-factor':'test_density_loss_ledger', +} + +def require(ok,message): + if not ok:raise ValueError(message) + +def decode(text): + def unique(items): + d={} + for k,v in items: + require(k not in d,'duplicate JSON key: '+k);d[k]=v + return d + return json.loads(text,object_pairs_hook=unique) + +def ident(path): + require(path.is_file() and not path.is_symlink(),'regular source required') + data=path.read_bytes() + return {'bytes':len(data),'sha256':hashlib.sha256(data).hexdigest(), + 'git_blob':hashlib.sha1(f'blob {len(data)}\0'.encode()+data).hexdigest()} + +def sources(): + ident(ROOT/'SOURCE_FILES.json') + entries=decode((ROOT/'SOURCE_FILES.json').read_text())['files'] + names=[e['path'] for e in entries] + require(len(names)==len(set(names)) and all(Path(n).name==n and n!='SOURCE_FILES.json' for n in names),'unique flat paths required') + require(sorted(p.name for p in ROOT.iterdir())==sorted(names+['SOURCE_FILES.json']),'source membership differs') + for e in entries:require(ident(ROOT/e['path'])=={k:e[k] for k in ['bytes','sha256','git_blob']},'source identity differs: '+e['path']) + return {p.name:ident(p) for p in sorted(ROOT.iterdir())} + +def child(mutant): + import lift + import test_lift + lift.MUTANT=mutant + result=unittest.TextTestRunner(stream=io.StringIO()).run(unittest.defaultTestLoader.loadTestsFromModule(test_lift)) + print(json.dumps({'tests':result.testsRun,'passed':result.wasSuccessful(), + 'failures':sorted(t.id().rsplit('.',1)[-1] for t,_ in result.failures), + 'errors':sorted(t.id().rsplit('.',1)[-1] for t,_ in result.errors)},sort_keys=True)) + return 0 if result.wasSuccessful() else 1 + +def replay(out): + out=out.resolve() + require(not out.exists() and not out.is_relative_to(ROOT),'new output outside source required') + before=sources();out.mkdir(parents=True) + records={} + for case in ['baseline',*MUTANTS]: + pair=[] + for mode,flags in [('normal',[]),('optimized',['-O'])]: + command=[sys.executable,'-B',*flags,'-S',str(ROOT/'verify.py'),'--child'] + if case!='baseline':command+=['--mutant',case] + proc=subprocess.run(command,capture_output=True,timeout=30) + (out/(case+'_'+mode+'.stdout')).write_bytes(proc.stdout) + (out/(case+'_'+mode+'.stderr')).write_bytes(proc.stderr) + result=decode(proc.stdout.decode()) + require(not proc.stderr and not result['errors'],'execution error: '+case) + require(result['tests']==18,'wrong test count') + if case=='baseline':require(proc.returncode==0 and result['passed'] and not result['failures'],'baseline failed') + else:require(proc.returncode==1 and not result['passed'] and MUTANTS[case] in result['failures'],'intended semantic failure absent: '+case) + pair.append(proc.stdout) + require(pair[0]==pair[1],'Python modes disagree: '+case) + records[case]=decode(pair[0].decode()) + summary={'tests_per_mode':18,'semantic_mutants_per_mode':10,'identical_output_pairs':11, + 'all_intended_failures':True,'scientific_effect':'NONE','gaussian_analysis_verified_by_code':False} + require(summary==decode((ROOT/'RESULTS.json').read_text()),'stored summary differs') + require(sources()==before,'sources changed during replay') + report={**summary,'source_identities':before,'sources_unchanged':True,'cases':records} + (out/'REPORT.json').write_text(json.dumps(report,sort_keys=True,indent=2)+'\n') + print(json.dumps(summary,sort_keys=True,indent=2)) + return 0 + +if __name__=='__main__': + p=argparse.ArgumentParser(description=__doc__);g=p.add_mutually_exclusive_group(required=True) + g.add_argument('--child',action='store_true');g.add_argument('--output',type=Path) + p.add_argument('--mutant',choices=MUTANTS);a=p.parse_args() + require(a.child or a.mutant is None,'mutant requires child mode') + raise SystemExit(child(a.mutant) if a.child else replay(a.output)) From d5c8570d47ba49844f296e4ec9b47c0416d2ee9a Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 28 Sep 2026 23:57:36 +0000 Subject: [PATCH 2/4] review record: nonauthor review of #125 elder lower event in every fixed dimension (scientific effect NONE) Anthropic nonauthor analytic review of OA-ELDER-DIMENSION-LIFT-20260928-v1 at exact head e3f10b3 (PROOF.md blob 7303bd79, SHA256 b529fe37). Verdict: ACCEPT at the stated existential scope for Theorem A (A2)-(A4) in every fixed d >= 3; Corollaries B (A5), (A6) and C (A6a) accepted as compositions with LP Theorem A (reconciled in #126) and LP's compact-mark ledger. No defect found. Independent stdlib checker (written from the markdown): exact dual-number Jacobian of the raw chart, end-to-end physical cubic fields in d = 3, 4, 5, quartic O(r) remainder rates, a labelled float saddle-persistence group, and 9 rejected mutants; output identical in -O. Dependency exposure disclosed. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_017Mi3hxjaxV45x6zo6o1ee3 --- .../workflows/elder-dimension-lift-review.yml | 61 ++ .../RESULTS.json | 81 ++ .../REVIEW.md | 198 ++++ .../SOURCE_FILES.json | 37 + .../dimension_lift_review_check.py | 872 ++++++++++++++++++ 5 files changed, 1249 insertions(+) create mode 100644 .github/workflows/elder-dimension-lift-review.yml create mode 100644 reviews/elder_dimension_lift_claude_20260928/RESULTS.json create mode 100644 reviews/elder_dimension_lift_claude_20260928/REVIEW.md create mode 100644 reviews/elder_dimension_lift_claude_20260928/SOURCE_FILES.json create mode 100644 reviews/elder_dimension_lift_claude_20260928/dimension_lift_review_check.py diff --git a/.github/workflows/elder-dimension-lift-review.yml b/.github/workflows/elder-dimension-lift-review.yml new file mode 100644 index 000000000..6a708cba4 --- /dev/null +++ b/.github/workflows/elder-dimension-lift-review.yml @@ -0,0 +1,61 @@ +name: Elder dimension-lift nonauthor review checks + +'on': + pull_request: + paths: + - 'reviews/elder_dimension_lift_claude_20260928/**' + - '.github/workflows/elder-dimension-lift-review.yml' + workflow_dispatch: + +permissions: + contents: read + +jobs: + exact-and-probe: + runs-on: ubuntu-latest + timeout-minutes: 10 + steps: + - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 + with: + persist-credentials: false + - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 + with: + python-version: '3.11.16' + - name: Verify sources, replay both modes, reject mutants + env: + PYTHONDONTWRITEBYTECODE: '1' + run: | + set -euo pipefail + python -B -S - <<'PY' + import hashlib, json, pathlib, subprocess, sys + root = pathlib.Path('reviews/elder_dimension_lift_claude_20260928').resolve() + manifest = json.loads((root / 'SOURCE_FILES.json').read_text())['files'] + present = sorted(p.name for p in root.iterdir()) + expected_names = sorted([e['path'] for e in manifest] + ['SOURCE_FILES.json']) + if present != expected_names: + raise ValueError('packet tree differs from manifest: ' + repr(present)) + for entry in manifest: + path = root / entry['path'] + if pathlib.PurePosixPath(entry['path']).name != entry['path'] or path.is_symlink(): + raise ValueError('flat regular source required: ' + entry['path']) + data = path.read_bytes() + if len(data) != entry['bytes'] or hashlib.sha256(data).hexdigest() != entry['sha256']: + raise ValueError('source identity mismatch: ' + entry['path']) + script = str(root / 'dimension_lift_review_check.py') + expected = (root / 'RESULTS.json').read_bytes() + mutants = ['raw-a-in-plane', 'shear-sign', 'drop-transverse-pin-term', + 'no-cross-schur', 'planar-point-is-critical', 'stable-scale-r', + 'density-dr', 'threshold-two-thirds', 'weight-2d'] + for flags in (['-B', '-S'], ['-B', '-O', '-S']): + out = subprocess.run([sys.executable, *flags, script], + check=True, capture_output=True, timeout=300).stdout + if out != expected: + raise RuntimeError('output differs from RESULTS.json under ' + ' '.join(flags)) + for m in mutants: + rc = subprocess.run([sys.executable, *flags, script, '--mutant', m], + capture_output=True, timeout=300).returncode + if rc != 1: + raise RuntimeError('mutant ' + m + ' not rejected') + print(json.dumps({'scientific_effect': 'NONE', 'mathematical_acceptance': False})) + PY + git diff --exit-code diff --git a/reviews/elder_dimension_lift_claude_20260928/RESULTS.json b/reviews/elder_dimension_lift_claude_20260928/RESULTS.json new file mode 100644 index 000000000..59e62fdcd --- /dev/null +++ b/reviews/elder_dimension_lift_claude_20260928/RESULTS.json @@ -0,0 +1,81 @@ +{ + "checks": { + "CHART": { + "raw_chart_full_jacobian_is_one_d3_d4": true, + "rotated_lattice_unisolvence_degree3": true, + "schur_shear_cancels_and_det_A_equals_sigma_det_D_n1to4": true + }, + "LEDGER": { + "density_loss_ell_2_3_k_minus_5_3": true, + "inverse_moment_threshold_5_3": true, + "jet_count_U0_plus_J_is_binom_d3_3": true, + "ledger_r_r4_over_r2_is_r3_all_d": true + }, + "PATH": { + "path_segments_margins_and_saddle_data": true + }, + "PHYSICAL": { + "Hu_order_r": true, + "endpoint_blocks_A20": true, + "gradient_pin_average_A24": true, + "normal_form_A17_exact": true, + "pins": true, + "schur_det_inertia_A21_A22": true, + "shear_recovers_sigma_D_tau": true, + "weight_order_r4": true + }, + "QUARTIC": { + "A17_remainder_halves_with_r": true, + "Hu_halves_with_r": true, + "_rates": { + "A17_remainder": { + "3": [ + 2.0, + 2.0, + 2.0 + ], + "4": [ + 2.0, + 2.0, + 2.0 + ] + }, + "H_S_u": { + "3": [ + 1.9944, + 1.9972, + 1.9986 + ], + "4": [ + 2.0023, + 2.0011, + 2.0006 + ] + } + }, + "contact_frame_nonsingular": true, + "pins_exact_after_solve": true + }, + "SADDLES": { + "_ratios": { + "3": [ + 1.1962, + 1.1312 + ], + "4": [ + 1.0019, + 1.6157 + ] + }, + "distinct_from_each_other_and_pins": true, + "heights_inside_window": true, + "index_d_minus_1": true, + "planar_critical_point_not_full_critical": true, + "stable_displacement_W_converges_at_rate_r": true, + "two_extra_critical_points_exist": true + } + }, + "object": "CLAUDE-REVIEW-ELDER-DIMENSION-LIFT-20260928-v1", + "passed": true, + "scope": "exact chart/field identities and one labelled numerical saddle group; not an analytic proof" +} diff --git a/reviews/elder_dimension_lift_claude_20260928/REVIEW.md b/reviews/elder_dimension_lift_claude_20260928/REVIEW.md new file mode 100644 index 000000000..e5984338e --- /dev/null +++ b/reviews/elder_dimension_lift_claude_20260928/REVIEW.md @@ -0,0 +1,198 @@ +# Nonauthor analytic review: the elder lower event in every fixed dimension (Math-#125) + +Scientific effect: **NONE**. This file does not change `lemma_closed`, prizes, premises, `STATUS`, `PROOF_INDEX`, +`GRAPH`, landing claims or any author source. It records verdicts on the OpenAI candidate below. Integration is a +separate act. + +## Object + +| Field | Value | +|---|---| +| Object | OA-ELDER-DIMENSION-LIFT-20260928-v1 (OpenAI / ChatGPT) | +| Branch / head | `chatgpt/elder-dimension-lift-20260928` / `e3f10b390ae5ddd998d238206add5958d5b720bb` ([Math-#125](https://github.com/d6g8k5htny-coder/Math-/pull/125)), base `d39dbbc` | +| `PROOF.md` | Git blob `7303bd791a68a1139251f0f6e403a9f7cc89b006`, 23971 B, SHA256 `b529fe3780e1909014b3cb144b9a74156d976bbdc19b6711d0c5b1a1da9e5669`, 480 lines | +| Consumed, already on main | [LP] `imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md` (blob `dfed3b8d…`): §1 selector, §§2–4 spectrum, contact frame and regression, §8 maximin; Theorem A and §§9–12 for the corollaries only. [EL] `frontiers/window_multiplicity_laws_20260928/ELDER_LOWER_AND_DENSITY_GAP.md` (blob `aaefc8da…`): the planar cubic, path and d = 2 case. [LOCAL] `LOCAL_MULTIPLICITY.md` (blob `b5c18aac…`): planar saddle data. | + +## Provenance + +| Field | Value | +|---|---| +| Reviewer | Anthropic Claude, Claude Code session `session_017Mi3hxjaxV45x6zo6o1ee3` | +| Relation | Different provider from the OpenAI author. Same GitHub account as every lane, so no organizational independence is claimed. | +| Exposure | I read `PROOF.md` in full, plus the packet README, SOURCE_MAP, RECONNAISSANCE, `lift.py`, `test_lift.py` and `verify.py`. I wrote the nonauthor review of [EL]/[LOCAL] (`reviews/d1_elder_lower_claude_20260928/`), the #106 review of LP Theorem A, and the D1 chain reconciliation (Math-#126, merged at `8224783`). Corollary B's upper half consumes LP Theorem A, whose reconciliation I authored, so for that half this review is **not** independent of its inputs. The direct lower Theorem A (A2)–(A4) consumes none of those objects except [EL]'s unchanged planar cubic and path, which this review re-derives. | +| Independent derivation | Before seeing #125 I had planned a d ≥ 3 lower proof by a nonlinear ridge reduction `y = φ(x, z)` in the stable directions. Its reduced midpoint Hessian is the same Schur complement `σ = f_zz − f_zw f_ww⁻¹ f_wz`. #125's linear shear reaches the same rare set with less machinery (N3), so I review #125 instead of writing a competing candidate. | +| Author code | I ran `verify.py --output` in `-B -S` and `-B -O -S` on the exact head: 18 tests per mode, 10 intended mutant failures, identical output pairs. Source identities match. | +| Independent checks | `dimension_lift_review_check.py` is my own suite, written from `PROOF.md` without reusing `lift.py`. It checks finite identities exactly, plus one labelled floating-point group. Every Gaussian step below was argued by hand and is not replaced by those checks. | + +## Verdicts + +| Interface (PROOF.md lines) | Verdict | +|---|---| +| §2 (98–130): complete 3-jet `(U_0, J)` of size `C(d+3,3)`, positive definite in every frame; uniform floor for `(U_r, J)`; raw-jet density floor under `Q_r` | **ACCEPT**; see §1 below. | +| §3 (132–187): Schur shear (A8)–(A9), unit-Jacobian raw chart (A10) | **ACCEPT**. Exact check `CHART`, including the full Jacobian by dual numbers. | +| §4 (189–216): raw rare set (A11), volume (A12), `Q_r ≥ c_J r` (A13) | **ACCEPT**; see §2 below. | +| §5 (218–246): `C^4` control after conditioning on all physical jets (A14)–(A16); constant order | **ACCEPT**; see §3 below. | +| §6 (248–282): sheared-plane normal form (A17), pin identities, target (A18) | **ACCEPT**. Hand-derived. Exact on physical cubic fields in d = 3, 4, 5 (zero remainder); `O(r)` remainder on quartic fields. | +| §7 (284–308): path (A19), margins `k/64`, `d_f(M) ≥ b − kr³/4 > f(S)` | **ACCEPT**. Identical to [EL] (E5)–(E6); recomputed. | +| §8 (310–361): endpoint blocks (A20), Schur (A21), inertia and determinant (A22), `W ≥ c r⁴` (A23), `Z ≤ C r²` (A24), ledger (A25) | **ACCEPT**; see §4 below. | +| **Theorem A (A2)–(A3)**: `1 − p_r ≥ c r³` for every fixed d ≥ 3 (d = 2 is [EL]) | **ACCEPT** at its stated existential scope. | +| §9 (363–415), **(A4)**: two extra index-(d−1) critical points, `Q^W(N_r ≥ 2) ≥ c r³`, factorial lower bound | **ACCEPT**; see §5 below. | +| **Corollary B (A5)**: `c r³ ≤ 1 − p_r ≤ C r³` in every fixed d | **ACCEPT** as a composition with LP Theorem A (1.1), consumable at existential scope under the D1 reconciliation (Math-#126, merged at `8224783`); see §6 below. | +| **(A6)**: compact-mark loss `ν_cand − ν_eld = Θ(ℓ^{2/3})` in every fixed d | **ACCEPT** as a composition with LP's compact-mark ledger and (A5). | +| **Corollary C (A6a)**: rejected-pair inverse moments finite iff `p < 5/3`; `Θ(t^{5/3−p})`; logarithmic endpoint | **ACCEPT** as a composition with (A6). | + +No defect was found. Notes N1–N5 record observations that sharpen or delimit the text without changing it. + +--- + +## §1 — the jet floor (§2 of PROOF.md) + +The count is exact. `U_0` has `4 + 2(d−1) = 2(d+1)` entries (lines 101–105), one per pin observation. `J` has the +`m(m+1)/2` transverse Hessian entries (`m = d − 1`) and the `C(d+2,3) − 1` third derivatives other than `f_xxx`. +Order by order, `U_0 ∪ J` is every derivative of order 0–3 exactly once. Order 2 has `d` entries in `U_0` (`f_xx`, +`f_xy_j`) and `m(m+1)/2` in `J`, total `d(d+1)/2`. The total is `C(d+3,3)` (`LEDGER`, d = 2…12). + +Positivity: the periodized covariance has Fourier weights `∝ exp(−|ω|²/2) > 0` on `(2π/L)Z^d`. A linear functional +`Σ c_α ∂^α f(0)` has variance `Σ_ω w_ω |Σ c_α (iω)^α|²`. If that variance is zero, the polynomial `Σ c_α (iω)^α` vanishes +on the dual lattice, rotated by the frame. Pulled back, it vanishes on `Z^d`, hence identically. So the complete jet +covariance is positive definite for each frame. Compactness of `O(d)` and continuity make the floor uniform. +`CHART.rotated_lattice_unisolvence_degree3` illustrates this exactly on Cayley-rational rotated lattices for d = 2, 3. + +`U_r → U_0` uniformly as `r → 0` is LP §§2–4. The quartic group re-solves the `2(d+1)` U_0 jets from the pins through +that frame and finds it nonsingular. Conditioning on `U_r = v_r` is Schur complementation, so the conditional covariance +of `J` is sandwiched between the joint floor and ceiling, and its mean `Cov(J,U_r)Cov(U_r)⁻¹v_r` is bounded. A Gaussian +density with sandwiched covariance and bounded mean is bounded below on every fixed compact set. The claim is about +**raw** jets (line 129), which is what §4 integrates. + +Note on `J` being free under `Q_r`: the pins tie `f_y(0)` to `f_xxy` at order `r²`, since +`f_y(0) = −(r²/8) f_xxy + O(r³)`. That relation lives inside the `U_r` rows, not as a constraint on `J`. The +`PHYSICAL` group builds fields with arbitrary `J` and verifies all `2(d+1)` pins exactly. + +## §2 — the chart and the rare set (§§3–4) + +With `q = D⁻¹v`, `y = (z, w − qz)` gives +`yᵀAy = az² + 2z vᵀ(w − qz) + (w − qz)ᵀD(w − qz)`. The `zw` terms cancel because `qᵀD = vᵀ`. The `z²` coefficient is +`a − 2vᵀD⁻¹v + vᵀD⁻¹v = σ`. So `SᵀAS = diag(σ, D)` and `det A = σ det D` (checked exactly, n = 1…4). The chart +`(σ, v, D, τ) ↦ (a, v, D, T)` is block triangular in the order `(v, D), σ, τ`, with diagonal blocks `I`, `1` and the +substitution `w ↦ w + qz` on third-derivative coordinates, which is unipotent. + +`f_xxx` is untouched, and no other coordinate depends on it: `∂_z` of the sheared field only introduces `∂_w`, which +preserves the number of `x` indices. So deleting `xxx` leaves determinant one. My check does not rely on the triangular +argument. It differentiates the whole map with exact dual numbers for d = 3 (12 variables) and d = 4 (25 variables), +and finds a full Jacobian determinant of exactly 1. + +The rare box (A11) is a product: an interval of length `2εkr` in `σ`, fixed boxes in `v` and `D`, and width-`2εk` boxes +in the `q_3 = C(d+2,3) − 1` coordinates of `τ`. Its raw volume is therefore (A12). All inverse-chart images lie in one +compact set, because `D⁻¹`, `q` and `σ` are bounded. So (A13) follows from §1. The raw entry `a` sits on the `O(1)` +surface `vᵀD⁻¹v`, inside a band of width `O(r)`. Only one scalar shrinks. That is why the power is `r¹` in every d +(line 185). Requiring all `m(m+1)/2` transverse entries to be `O(r)` would give `r^{m(m+1)/2}` instead. No law is +assigned to the sheared variables (lines 213–216): the raw Gaussian density is integrated against a unit Jacobian. + +## §3 — conditioning order and constants (§5) + +The field is regressed on `V = (U_r, J)` at each target. The pin rows are integral averages of derivatives of order +≤ 3, so the cross-covariances of the field's derivatives through order 4 with `V` are uniformly bounded. `Cov(V)⁻¹` is +bounded by §1, and the targets are compact. Hence (A15) holds uniformly. Markov's inequality gives `K_4` with conditional +mass ≥ 1/2 at every target, and integrating over the rare set gives (A16). No independence between jets and remainder is +used, and no unconditional tail is subtracted from an `O(r)` mass. + +The constant order is sound. The raw container is valid for all `ε ≤ 1`, so `K_4` is chosen first. `ε` is then chosen +for the planar `O(εk)` margins, which do not involve `K_4`. Finally `r_*` absorbs every `O(rK_4)` and `O(rK_4²)` term. + +## §4 — normal form, endpoints, weight and normalizer (§§6, 8) + +(A17): I rederived every pin identity (lines 266–270) from the axial restrictions `φ(x) = g(x,0)` and +`ψ(x) = g_z(x,0)`. The sums of `φ'(±r/2)` and `ψ(±r/2)` give `g_x` and `g_z`. Their differences give `g_xx` and `g_xz`. +The height difference gives `g_xxx = 12k + O(rK_4)`. The `Z²` coefficient is `σ/r`, not `a/r`. The `−a_3 Z/8` term comes +from `g_z(0)`. + +Two independent exact checks support this: + +- **Cubic fields.** On physical cubic fields in d = 3, 4, 5, built from chart data with all pins imposed and then + sheared, (A17) holds with **zero** remainder. The sheared midpoint jets reproduce `σ`, `D` and `τ` exactly + (`PHYSICAL`). +- **Quartic fields.** On quartic fields, where the pins are re-solved through the contact frame, the sup of + `F_r − P` over the rational grid in `B(0,3)` halves as `r` halves (successive ratios 2.0000 to four decimals), for + `r = 1/8 … 1/64` in d = 3, 4 + (`QUARTIC`). + +The mutants `raw-a-in-plane` and `drop-transverse-pin-term` are rejected. + +(A20)–(A22): for cubic fields the endpoint blocks are exactly `r P_i` (soft), `C_i = ±(r/2)(τ_xxw; τ_xzw)` (cross) and +`D ± (r/2) τ_xww` (stable). Then `det H = det D_i · det K_i`, and inertia(H) = inertia(D_i) + inertia(K_i), with index +d at `M` and d − 1 at `S`. `|K_i/r − P_i| ≤ rk`. All of this is checked exactly, with the physical Hessian computed +independently of the sheared one. Dropping the cross-block correction is rejected (`no-cross-schur`). The target planar +Hessians `diag(−6k, −k/2)` and `diag(6k, −5k/2)` are recomputed in `PATH`. Since `|det L| = 1`, physical and sheared +determinants agree, so `W_r ≥ c r⁴` with the power independent of d. + +(A24): `∇f(S) − ∇f(M) = r∫_{−1/2}^{1/2} H(tru)u dt = 0` (checked exactly). So `H_i u = O(r‖f‖_{C³})`. On cubic +fields `H_i u = ±(r/2)(f_xxx, f_xxy_j)` exactly, and on quartic fields it halves with `r`. Hadamard's inequality gives +`|det H_i| ≤ C r (1 + ‖f‖_{C³})^d`, and LP §4's endpoint-conditioned moments give `Z_r ≤ C_Z r²`. The ledger is +`r · r⁴ / r² = r³` in every d (`LEDGER`; `weight-2d` rejected). + +## §5 — the extra saddles (§9) + +The rescaling `x = rX, z = rZ, w = r²W` is the right one. I rederived (A27) term by term: + +- **Soft components.** These are `∇F_r` plus `r⁻²·r²W·f̃_{w,(x,z)}(rX, rZ, 0) = O(rK_4|W|)`. The mixed soft–stable + Hessian is `O(rK_4)` in the `O(r)` ball, because `f̃_zw(0) = 0` exactly and `f̃_xw(0) = O(K_4 r²)`. +- **Stable components.** These are `r⁻²[f̃_w(0) + f̃_wx rX + ½(τ_xxw r²X² + 2τ_xzw r²XZ + τ_zzw r²Z²) + r²DW] + O(rK_4)`, + with `f̃_w(0) = −(r²/8)τ_xxw + O(K_4 r³)`. This is `DW + Q(X,Z)` with `Q` as in (A28). +- **C¹ closeness.** `∂_X` of the stable part is `r⁻¹f̃_wx(…) = ∂_X Q + O(rK_4)`. `∂_W` of the soft part is `O(rK_4)`. + Second derivatives of `H_r` are bounded by `K_4`, so the quantitative inverse-function theorem applies uniformly + around the block-triangular nondegenerate zero `(p, −D⁻¹Q(p))`. + +Heights are `b + r³(F_r(p) + O(r))`, strictly inside the window. The index is `n + 1 = d − 1`, by the same Schur +argument as §4. + +`SADDLES` checks this in floating point on quartic fields in d = 3, 4 for `r = 1/16 … 1/128`: + +- Both extra critical points exist, with gradient residual below `1e−15`, index d − 1 and heights in `(b − kr³, b)`. + They are distinct from each other and from the pins. +- `|w/r² − W*|/r` stays within a factor 2 across the range, so the stable correction is `O(r)`. Scaling `w` by `r` + instead of `r²` is rejected. +- At the planar restriction's critical point, `∂_w f̃/r²` is nonzero. This confirms the manuscript's warning (line + 365) that a planar critical point is not a full critical point. + +## §6 — the corollaries (§10) + +(A5) consumes LP Theorem A (1.1). The D1 reconciliation (Math-#126, `reviews/d1_chain_reconciliation_20260928/`, merged at `8224783`) +records (1.1) as ACCEPT at existential scope in every fixed d ≥ 2, read with the congruence erratum, the §9 replacement +v1.1, wording W1 and `r < L/(4√2)`. Its consumption contract (§7 there) permits exactly this use. #126 is +now merged, so (A5)'s upper half rests on a reconciled register entry. The direct lower half never depended on it. + +(A6): with `ℓ = kr³` at fixed `k`, `r dr = (1/3)ℓ^{−1/3}k^{−2/3} dℓ`. Multiplying by `1 − p ≍ r³ = ℓ/k` gives +`ℓ^{2/3}k^{−5/3}`, which is integrable with positive integral on compact `K` with `k_− > 0`. For small `ℓ` every radius +is below the common cutoff. (A6a) follows: `∫_0^t ℓ^{2/3−p} dℓ` is finite iff `p < 5/3`, logarithmic at `p = 5/3`. The +rejected-pair measure is integrated directly, never as a difference of infinities (line 444). + +**Consequence for the D1 chain.** With this review and #126, Theorem A's cubic order is **two-sided** `Θ(r³)` in every +fixed d ≥ 2, and the compact-mark density loss is `Θ(ℓ^{2/3})` in every fixed d. #126 deliberately says "no d ≥ 3 lower +bound". That caveat can be lifted by a later register PR once both #125 and #126 are integrated, not inside either. + +## Notes + +- **N1.** (A20)'s bound `‖C_i‖ ≤ CrK_4` can be read more finely as `C_i = ±(r/2)(τ_xxw; τ_xzw) + O(K_4 r²)`, so the + Schur correction is `O(r²(εk + K_4 r)²)`. Not needed, but it shows the correction is small even before `r_*` is fixed. +- **N2.** (A4) should say whether `N_r` counts additional window critical points anywhere on the torus or only in the + `C_d r` ball. The lower bounds hold for either reading, since both counts are ≥ 2 on the event. +- **N3.** Why a *linear* shear suffices. The path obstruction needs field values on one plane only. The endpoint and + saddle data need only Schur complements with `O(r)` cross blocks. A nonlinear ridge `y = φ(x,z)` would give the same + midpoint Schur complement at the cost of implicit-function bookkeeping. Neither route needs the other. +- **N4.** The bound `‖q‖ ≤ 1/9` (line 146) is used only through a uniform bound on `‖L‖`. Any fixed bound works after + adjusting `r_*`. +- **N5.** `lift.py`'s tests are finite controls of the listed identities. The end-to-end physical-field checks here + (building `f`, imposing pins, shearing and recovering) are additional to them, not a replacement. + +## What this review does not do + +It does not accept a numerical `c`, `r_*` or cutoff, a uniform-in-d bound, an unrestricted-mark difference, a +leading loss constant, a global factorial upper bound, or any identification with historical `q`/`p` symbols. The +manuscript claims none of these. It changes no register. Integration, and any register transition that lifts #126's +d ≥ 3 caveat, are separate acts for a non-Claude integrator. + +## Reproduce + + python -B -S dimension_lift_review_check.py # prints RESULTS.json byte for byte + python -B -O -S dimension_lift_review_check.py # identical + python -B -S dimension_lift_review_check.py --mutant M # exit 1 for each of the 9 mutants diff --git a/reviews/elder_dimension_lift_claude_20260928/SOURCE_FILES.json b/reviews/elder_dimension_lift_claude_20260928/SOURCE_FILES.json new file mode 100644 index 000000000..f5a8f9024 --- /dev/null +++ b/reviews/elder_dimension_lift_claude_20260928/SOURCE_FILES.json @@ -0,0 +1,37 @@ +{ + "schema": 1, + "scientific_effect": "NONE", + "review_status": "NONAUTHOR_REVIEW", + "reviewed_object": { + "pr": "d6g8k5htny-coder/Math-#125", + "head": "e3f10b390ae5ddd998d238206add5958d5b720bb", + "paths": [ + { + "path": "frontiers/elder_dimension_lift_20260928/PROOF.md", + "git_blob": "7303bd791a68a1139251f0f6e403a9f7cc89b006", + "bytes": 23971, + "sha256": "b529fe3780e1909014b3cb144b9a74156d976bbdc19b6711d0c5b1a1da9e5669" + } + ] + }, + "files": [ + { + "path": "REVIEW.md", + "bytes": 16746, + "sha256": "a937a36813faff5afb9b6ed135cb838d14dde8ddfbdbc7e6ad37534a2b5c9c62", + "git_blob": "e5984338eb48cd496d3e9b6c0ddc9322dcc1465b" + }, + { + "path": "RESULTS.json", + "bytes": 2035, + "sha256": "97a323d1d383c6bf5a8fe8d616e681d7a2ae1c2d4acee51eb6405ec8df55e8f4", + "git_blob": "59e62fdcd2e30e324ac74263a6b904b3da3d2b6e" + }, + { + "path": "dimension_lift_review_check.py", + "bytes": 37826, + "sha256": "768b0d8f84b66616f2c649c5f7ae132fa701563ead85b8f5aa20a30f2bc0bda8", + "git_blob": "36f258676a9aeb7f1b63e1f1267c3e4ebce52bb6" + } + ] +} diff --git a/reviews/elder_dimension_lift_claude_20260928/dimension_lift_review_check.py b/reviews/elder_dimension_lift_claude_20260928/dimension_lift_review_check.py new file mode 100644 index 000000000..36f258676 --- /dev/null +++ b/reviews/elder_dimension_lift_claude_20260928/dimension_lift_review_check.py @@ -0,0 +1,872 @@ +"""Independent nonauthor checks for OA-ELDER-DIMENSION-LIFT-20260928-v1 (Math- PR 125). + +Python standard library only. Written from the manuscript, not from the author's lift.py/test_lift.py. +Groups (exact rational arithmetic unless marked NUMERIC): + + CHART the Schur shear S^T A S = diag(sigma, D); the full raw chart (sigma,v,D,tau) -> (a,v,D,T) has + Jacobian determinant exactly one (forward-mode dual numbers over Fractions, d = 3, 4); the xxx + coordinate decouples; rational-orthogonal rotated lattices are unisolvent for degree <= 3. + PHYSICAL end to end on actual physical cubic fields in d = 3, 4, 5: build f from chart data and the + 2(d+1) pins, verify the pins, shear it, recover (sigma, D, tau) exactly, and check the planar + normal form (A17) with zero remainder, the endpoint blocks (A20), the Schur/determinant/inertia + identities (A21)-(A22), the gradient-pin average behind (A24) and |H u| = O(r). + QUARTIC physical quartic fields with pins re-solved through the 2(d+1)-row contact frame: the frame is + nonsingular, (A17)'s remainder is O(r) (exact values on a grid at r = 1/8 ... 1/64), and + H_i u = O(r). + SADDLES NUMERIC (floats): on the quartic fields the two extra critical points exist near (rP+-, r^2 W*), + have index d-1 and window heights, w/r^2 -> -D^{-1} Q(p) at rate O(r), and the planar + restriction's critical point is not a full critical point. + PATH the polygonal path (A19) and saddle data (A18), recomputed from the polynomial class. + LEDGER jet counts, the r * r^4 / r^2 = r^3 ledger, the density change of variables (A6) and the + inverse-moment threshold 5/3 (A6a). + +Mutants (each must make the checks fail): raw-a-in-plane, shear-sign, drop-transverse-pin-term, +no-cross-schur, planar-point-is-critical, stable-scale-r, density-dr, threshold-two-thirds, weight-2d. +This is not an analytic proof of the Gaussian covariance floor, conditional C^4 bounds or inverse-function +estimates; those are reviewed in REVIEW.md. +""" +import argparse +import json +import math +import random +import sys +from fractions import Fraction as F +from itertools import product +from math import comb, factorial + +MUTANTS = ("raw-a-in-plane", "shear-sign", "drop-transverse-pin-term", "no-cross-schur", + "planar-point-is-critical", "stable-scale-r", "density-dr", "threshold-two-thirds", "weight-2d") +MUT = None + + +# --------------------------------------------------------------------------------------------------------------- +# Polynomials: dict {exponent tuple: coefficient} +# --------------------------------------------------------------------------------------------------------------- + +def padd(*ps): + out = {} + for p in ps: + for e, c in p.items(): + out[e] = out.get(e, 0) + c + return {e: c for e, c in out.items() if c} + + +def pscale(p, s): + return {e: c * s for e, c in p.items() if c * s} + + +def pmul(p, q): + out = {} + for e1, c1 in p.items(): + for e2, c2 in q.items(): + e = tuple(a + b for a, b in zip(e1, e2)) + out[e] = out.get(e, 0) + c1 * c2 + return {e: c for e, c in out.items() if c} + + +def pconst(c, n): + return {(0,) * n: c} if c else {} + + +def pvar(i, n, c=1): + return {tuple(int(j == i) for j in range(n)): c} + + +def pcompose(p, subs, n_out): + """p(subs[0], ..., subs[n-1]) where each subs[i] is a polynomial in n_out variables.""" + out = {} + cache = {} + for e, c in p.items(): + term = pconst(c, n_out) + for i, power in enumerate(e): + if power: + key = (i, power) + if key not in cache: + acc = pconst(1, n_out) + for _ in range(power): + acc = pmul(acc, subs[i]) + cache[key] = acc + term = pmul(term, cache[key]) + out = padd(out, term) + return out + + +def pdiff(p, i): + out = {} + for e, c in p.items(): + if e[i]: + e2 = list(e) + e2[i] -= 1 + out[tuple(e2)] = out.get(tuple(e2), 0) + c * e[i] + return {e: c for e, c in out.items() if c} + + +def peval(p, pt): + total = 0 + for e, c in p.items(): + term = c + for x, k in zip(pt, e): + if k: + term *= x ** k + total += term + return total + + +def pderiv_at0(p, alpha): + """partial^alpha p (0).""" + return p.get(tuple(alpha), 0) * math.prod(factorial(a) for a in alpha) + + +def from_jets(jets, n): + """Polynomial sum_alpha jets[alpha] x^alpha / alpha!.""" + return {e: F(c) / math.prod(factorial(a) for a in e) for e, c in jets.items() if c} + + +def multi(n, deg): + return [e for e in product(range(deg + 1), repeat=n) if sum(e) == deg] + + +def unit(n, i): + return tuple(int(j == i) for j in range(n)) + + +def eplus(*es): + return tuple(map(sum, zip(*es))) + + +# --------------------------------------------------------------------------------------------------------------- +# Small exact linear algebra +# --------------------------------------------------------------------------------------------------------------- + +def solve(A, b): + n = len(A) + W = [list(map(F, row)) + [F(b[i])] for i, row in enumerate(A)] + for j in range(n): + p = next(i for i in range(j, n) if W[i][j] != 0) + W[j], W[p] = W[p], W[j] + piv = W[j][j] + W[j] = [x / piv for x in W[j]] + for i in range(n): + if i != j and W[i][j] != 0: + f = W[i][j] + W[i] = [x - f * y for x, y in zip(W[i], W[j])] + return [row[-1] for row in W] + + +def det(A): + n = len(A) + W = [list(row) for row in A] + out = 1 + for j in range(n): + p = next((i for i in range(j, n) if W[i][j] != 0), None) + if p is None: + return 0 * out + if p != j: + W[j], W[p] = W[p], W[j] + out = -out + out = out * W[j][j] + for i in range(j + 1, n): + f = W[i][j] / W[j][j] + for k in range(j, n): + W[i][k] = W[i][k] - f * W[j][k] + return out + + +def inertia(A): + """(negatives, positives, zeros) of a symmetric Fraction matrix via symmetric pivoting (Sylvester).""" + n = len(A) + W = [list(map(F, row)) for row in A] + idx = list(range(n)) + neg = pos = 0 + while idx: + j = next((i for i in idx if W[i][i] != 0), None) + if j is None: + # 2x2 pivot on a nonzero off-diagonal entry + pair = next(((i, l) for i in idx for l in idx if i < l and W[i][l] != 0), None) + if pair is None: + return neg, pos, len(idx) + i, l = pair + neg += 1 + pos += 1 + blk = [[W[i][i], W[i][l]], [W[l][i], W[l][l]]] + dB = blk[0][0] * blk[1][1] - blk[0][1] * blk[1][0] + inv = [[blk[1][1] / dB, -blk[0][1] / dB], [-blk[1][0] / dB, blk[0][0] / dB]] + rest = [m for m in idx if m not in (i, l)] + for a in rest: + for b in rest: + ca = [W[a][i], W[a][l]] + cb = [W[i][b], W[l][b]] + W[a][b] -= sum(ca[s] * inv[s][t] * cb[t] for s in range(2) for t in range(2)) + idx = rest + continue + piv = W[j][j] + neg += piv < 0 + pos += piv > 0 + rest = [m for m in idx if m != j] + for a in rest: + for b in rest: + W[a][b] -= W[a][j] * W[j][b] / piv + idx = rest + return neg, pos, 0 + + +def rank(rows): + W = [list(map(F, r)) for r in rows] + h = 0 + ncol = len(W[0]) if W else 0 + for j in range(ncol): + p = next((i for i in range(h, len(W)) if W[i][j] != 0), None) + if p is None: + continue + W[h], W[p] = W[p], W[h] + for i in range(h + 1, len(W)): + f = W[i][j] / W[h][j] + if f: + W[i] = [x - f * y for x, y in zip(W[i], W[h])] + h += 1 + return h + + +def matmul(A, B): + return [[sum(A[i][k] * B[k][j] for k in range(len(B))) for j in range(len(B[0]))] for i in range(len(A))] + + +def transpose(A): + return [list(r) for r in zip(*A)] + + +# --------------------------------------------------------------------------------------------------------------- +# Dual numbers over Fractions (forward-mode derivatives for the chart Jacobian) +# --------------------------------------------------------------------------------------------------------------- + +class Dual: + __slots__ = ("v", "g") + + def __init__(self, v, g=None): + self.v = F(v) + self.g = g or {} + + @staticmethod + def lift(x): + return x if isinstance(x, Dual) else Dual(x) + + def __add__(self, o): + o = Dual.lift(o) + g = dict(self.g) + for k, c in o.g.items(): + g[k] = g.get(k, 0) + c + return Dual(self.v + o.v, g) + + __radd__ = __add__ + + def __neg__(self): + return Dual(-self.v, {k: -c for k, c in self.g.items()}) + + def __sub__(self, o): + return self + (-Dual.lift(o)) + + def __rsub__(self, o): + return Dual.lift(o) - self + + def __mul__(self, o): + o = Dual.lift(o) + g = {k: c * o.v for k, c in self.g.items()} + for k, c in o.g.items(): + g[k] = g.get(k, 0) + c * self.v + return Dual(self.v * o.v, g) + + __rmul__ = __mul__ + + def __truediv__(self, o): + o = Dual.lift(o) + inv = Dual(1 / o.v, {k: -c / (o.v * o.v) for k, c in o.g.items()}) + return self * inv + + def __rtruediv__(self, o): + return Dual.lift(o) / self + + def __ne__(self, o): + return self.v != Dual.lift(o).v + + def __eq__(self, o): + return self.v == Dual.lift(o).v + + def __hash__(self): + return hash(self.v) + + +# --------------------------------------------------------------------------------------------------------------- +# The chart +# --------------------------------------------------------------------------------------------------------------- + +def rat(rng, lo, hi, steps=1000): + """A random rational in [lo, hi] on a grid of `steps` intervals (lo, hi may be Fractions).""" + lo, hi = F(lo), F(hi) + return lo + (hi - lo) * F(rng.randint(0, steps), steps) + + +def sample_chart(d, rng, r, k, eps=F(1, 100)): + """Chart data (sigma, v, D, tau) inside the manuscript's rare set; variables ordered (x, z, w_1..w_n).""" + n = d - 2 + D = [[F(0)] * n for _ in range(n)] + for i in range(n): + D[i][i] = -1 + rat(rng, -1 / 10, 1 / 10) + for j in range(i): + D[i][j] = D[j][i] = rat(rng, -1 / (10 * n), 1 / (10 * n)) + v = [rat(rng, -1 / (20 * n), 1 / (20 * n)) for _ in range(n)] + sigma = r * (F(-3, 2) * k + rat(rng, -eps, eps) * k) + tau = {} + for e in multi(d, 3): + tau[e] = rat(rng, -eps, eps) * k + xz, x, z = unit(d, 0), unit(d, 0), unit(d, 1) + tau[eplus(x, x, x)] = 12 * k # cubic model: pins force f_xxx = 12k exactly + tau[eplus(x, z, z)] = -2 * k + rat(rng, -eps, eps) * k + return sigma, v, D, tau + + +def shear_subs(d, q, sign=-1): + """Substitution (x, z, w) -> (x, z, w + sign*q z) as polynomials in d variables.""" + subs = [pvar(0, d), pvar(1, d)] + for j in range(d - 2): + subs.append(padd(pvar(j + 2, d), pvar(1, d, sign * q[j]))) + return subs + + +def build_physical_cubic(d, sigma, v, D, tau, r, k, b): + """Physical cubic f(x, y) with the 2(d+1) pins, transverse Hessian A = [[a, v^T], [v, D]] and physical third + derivatives T obtained from tau through the inverse shear y_w = w - q z, i.e. w = y_w + q y_z.""" + n = d - 2 + q = solve(D, v) if n else [] + a = sigma + sum(vi * qi for vi, qi in zip(v, q)) + cubic_tilde = from_jets({e: c for e, c in tau.items()}, d) + cubic_phys = pcompose(cubic_tilde, shear_subs(d, q, sign=+1), d) + T = {e: pderiv_at0(cubic_phys, e) for e in multi(d, 3)} + x = unit(d, 0) + jets = dict(T) + # transverse Hessian over y = (z, w) + A = [[a] + list(v)] + [[v[i]] + list(D[i]) for i in range(n)] + for i in range(d - 1): + for j in range(d - 1): + jets[eplus(unit(d, i + 1), unit(d, j + 1))] = A[i][j] + # pin-determined lower order jets (exact for cubic fields) + jets[(0,) * d] = b - k * r ** 3 / 2 + jets[x] = -F(3, 2) * k * r ** 2 + for j in range(1, d): + jets[unit(d, j)] = -r * r / 8 * T[eplus(x, x, unit(d, j))] + jets[eplus(x, unit(d, j))] = F(0) + jets[eplus(x, x)] = F(0) + return from_jets(jets, d), A, T, q, a + + +def hessian_at(p, pt, d): + return [[peval(pdiff(pdiff(p, i), j), pt) for j in range(d)] for i in range(d)] + + +def gradient_at(p, pt, d): + return [peval(pdiff(p, i), pt) for i in range(d)] + + +def planar_normal_form(k, s, a3, beta, c3): + """(A17) polynomial in (X, Z).""" + X, Z = pvar(0, 2), pvar(1, 2) + lin = F(0) if MUT == "drop-transverse-pin-term" else F(1, 4) + terms = [pscale(pmul(pmul(X, X), X), 2 * k), pscale(X, -F(3, 2) * k), pconst(-k / 2, 2), + pscale(pmul(Z, Z), s / 2), + pscale(pmul(padd(pmul(X, X), pconst(-lin, 2)), Z), a3 / 2), + pscale(pmul(X, pmul(Z, Z)), beta / 2), pscale(pmul(Z, pmul(Z, Z)), c3 / 6)] + return padd(*terms) + + +def scaled_plane(ftilde, d, r, b): + """F_r(X, Z) = [tilde f(rX, rZ, 0) - b] / r^3.""" + subs = [pvar(0, 2, r), pvar(1, 2, r)] + [{} for _ in range(d - 2)] + return pscale(padd(pcompose(ftilde, subs, 2), pconst(-b, 2)), 1 / r ** 3) + + +# --------------------------------------------------------------------------------------------------------------- +# CHART group +# --------------------------------------------------------------------------------------------------------------- + +def check_chart(): + out = {} + rng = random.Random(125001) + ok_cancel = True + for n in (1, 2, 3, 4): + for _ in range(3): + d = n + 2 + sigma, v, D, _ = sample_chart(d, rng, F(1, 16), F(1)) + q = solve(D, v) + a = sigma + sum(x * y for x, y in zip(v, q)) + A = [[a] + list(v)] + [[v[i]] + list(D[i]) for i in range(n)] + sgn = 1 if MUT == "shear-sign" else -1 + S = [[F(int(i == j)) for j in range(n + 1)] for i in range(n + 1)] + for i in range(n): + S[i + 1][0] = sgn * q[i] + B = matmul(transpose(S), matmul(A, S)) + want = [[sigma] + [F(0)] * n] + [[F(0)] + list(D[i]) for i in range(n)] + ok_cancel &= B == want and det(S) == 1 and det(A) == sigma * det(D) + out["schur_shear_cancels_and_det_A_equals_sigma_det_D_n1to4"] = ok_cancel + + # Full raw-chart Jacobian with dual numbers. + ok_jac = True + for d in (3, 4): + n = d - 2 + sigma, v, D, tau = sample_chart(d, rng, F(1, 16), F(1)) + names = ["sigma"] + [f"v{i}" for i in range(n)] + [f"D{i}{j}" for i in range(n) for j in range(i, n)] + cubic_labels = [e for e in multi(d, 3) if e != eplus(unit(d, 0), unit(d, 0), unit(d, 0))] + names += [f"tau{e}" for e in cubic_labels] + sd = Dual(sigma, {"sigma": F(1)}) + vd = [Dual(v[i], {f"v{i}": F(1)}) for i in range(n)] + Dd = [[None] * n for _ in range(n)] + for i in range(n): + for j in range(i, n): + Dd[i][j] = Dd[j][i] = Dual(D[i][j], {f"D{i}{j}": F(1)}) + td = {e: Dual(tau[e], {f"tau{e}": F(1)}) for e in cubic_labels} + # q = D^{-1} v with duals (Gauss-Jordan) + W = [list(Dd[i]) + [vd[i]] for i in range(n)] + for j in range(n): + piv = W[j][j] + W[j] = [x / piv for x in W[j]] + for i in range(n): + if i != j: + f = W[i][j] + W[i] = [x - f * y for x, y in zip(W[i], W[j])] + qd = [W[i][-1] for i in range(n)] + ad = sd + sum((vd[i] * qd[i] for i in range(n)), Dual(0)) + # T = substitution w -> w + q z applied to tau (dual coefficients). + cub = {e: td[e] / math.prod(factorial(x) for x in e) for e in cubic_labels} + subs = [pvar(0, d), pvar(1, d)] + [padd(pvar(j + 2, d), {unit(d, 1): qd[j]}) for j in range(n)] + phys = {} + for e, c in cub.items(): + term = {(0,) * d: c} + for i, power in enumerate(e): + for _ in range(power): + new = {} + for e1, c1 in term.items(): + for e2, c2 in subs[i].items(): + key = tuple(s + t for s, t in zip(e1, e2)) + new[key] = new.get(key, Dual(0)) + c1 * c2 + term = new + for key, c in term.items(): + phys[key] = phys.get(key, Dual(0)) + c + Td = {e: phys.get(e, Dual(0)) * math.prod(factorial(x) for x in e) for e in cubic_labels} + outputs = [ad] + vd + [Dd[i][j] for i in range(n) for j in range(i, n)] + [Td[e] for e in cubic_labels] + J = [[o.g.get(nm, F(0)) for nm in names] for o in outputs] + ok_jac &= len(J) == len(names) and det(J) == 1 + # xxx decouples: no output depends on it and it is not an input (it is pinned in U_0). + out["raw_chart_full_jacobian_is_one_d3_d4"] = ok_jac + + # Rotated-lattice unisolvence for degree <= 3 (Cayley rational orthogonal frames). + ok_uni = True + for d in (2, 3): + labels = [e for deg in range(4) for e in multi(d, deg)] + for s in ((F(1, 2),), (F(1, 3), F(2, 5), F(-1, 7))): + K = [[F(0)] * d for _ in range(d)] + idx = 0 + for i in range(d): + for j in range(i + 1, d): + K[i][j] = s[idx % len(s)] + K[j][i] = -K[i][j] + idx += 1 + I = [[F(int(i == j)) for j in range(d)] for i in range(d)] + IpK = [[I[i][j] + K[i][j] for j in range(d)] for i in range(d)] + ImK = [[I[i][j] - K[i][j] for j in range(d)] for i in range(d)] + # R = (I - K)^{-1}(I + K) + cols = [solve(ImK, [IpK[i][j] for i in range(d)]) for j in range(d)] + R = transpose(cols) + ok_uni &= matmul(transpose(R), R) == I + pts = [[sum(R[i][j] * p[j] for j in range(d)) for i in range(d)] for p in product(range(4), repeat=d)] + rows = [[math.prod(x ** a for x, a in zip(pt, e)) for e in labels] for pt in pts] + ok_uni &= rank(rows) == len(labels) == comb(d + 3, 3) + out["rotated_lattice_unisolvence_degree3"] = ok_uni + return out + + +# --------------------------------------------------------------------------------------------------------------- +# PHYSICAL group (exact cubic fields) +# --------------------------------------------------------------------------------------------------------------- + +def check_physical(): + out = {} + rng = random.Random(125002) + k, b = F(6, 5), F(1, 3) + res = {key: True for key in ("pins", "shear_recovers_sigma_D_tau", "normal_form_A17_exact", "endpoint_blocks_A20", + "schur_det_inertia_A21_A22", "gradient_pin_average_A24", "Hu_order_r", + "weight_order_r4")} + for d in (3, 4, 5): + n = d - 2 + for r in (F(1, 8), F(1, 32)): + sigma, v, D, tau = sample_chart(d, rng, r, k) + f, A, T, q, a = build_physical_cubic(d, sigma, v, D, tau, r, k, b) + M = [-r / 2] + [F(0)] * (d - 1) + S = [r / 2] + [F(0)] * (d - 1) + res["pins"] &= (peval(f, M) == b and peval(f, S) == b - k * r ** 3 + and all(g == 0 for g in gradient_at(f, M, d) + gradient_at(f, S, d))) + ft = pcompose(f, shear_subs(d, q, sign=+1 if MUT == "shear-sign" else -1), d) + Ht0 = hessian_at(ft, [F(0)] * d, d) + rec = (Ht0[1][1] == sigma and all(Ht0[1][j + 2] == 0 for j in range(n)) + and all(Ht0[i + 2][j + 2] == D[i][j] for i in range(n) for j in range(n)) + and all(pderiv_at0(ft, e) == tau[e] for e in multi(d, 3))) + res["shear_recovers_sigma_D_tau"] &= rec + # (A17): exact for cubic fields. + s_coef = (a if MUT == "raw-a-in-plane" else Ht0[1][1]) / r + x, z = unit(d, 0), unit(d, 1) + a3, beta, c3 = pderiv_at0(ft, eplus(x, x, z)), pderiv_at0(ft, eplus(x, z, z)), pderiv_at0(ft, eplus(z, z, z)) + Fr = scaled_plane(ft, d, r, b) + res["normal_form_A17_exact"] &= Fr == planar_normal_form(k, s_coef, a3, beta, c3) + # Endpoint blocks in the (x, z; w) shear frame. + P = planar_normal_form(k, Ht0[1][1] / r, a3, beta, c3) + dets = [] + for sgn, pt in ((-1, M), (1, S)): + H = hessian_at(ft, pt, d) + Xs = F(sgn, 2) + Pi = [[peval(pdiff(pdiff(P, i), j), [Xs, F(0)]) for j in range(2)] for i in range(2)] + soft = [[H[i][j] for j in range(2)] for i in range(2)] + C = [[H[i][j + 2] for j in range(n)] for i in range(2)] + Di = [[H[i + 2][j + 2] for j in range(n)] for i in range(n)] + ok20 = soft == [[r * Pi[i][j] for j in range(2)] for i in range(2)] + xxw = [pderiv_at0(ft, eplus(x, x, unit(d, j + 2))) for j in range(n)] + xzw = [pderiv_at0(ft, eplus(x, z, unit(d, j + 2))) for j in range(n)] + ok20 &= C == [[sgn * r / 2 * c for c in xxw], [sgn * r / 2 * c for c in xzw]] + ok20 &= all(Di[i][j] == D[i][j] + sgn * r / 2 * pderiv_at0(ft, eplus(x, unit(d, i + 2), unit(d, j + 2))) + for i in range(n) for j in range(n)) + res["endpoint_blocks_A20"] &= ok20 + # Schur complement K_i = soft - C D_i^{-1} C^T + DinvCT = transpose([solve(Di, [C[i][j] for j in range(n)]) for i in range(2)]) + corr = matmul(C, DinvCT) + if MUT == "no-cross-schur": + corr = [[F(0)] * 2 for _ in range(2)] + K = [[soft[i][j] - corr[i][j] for j in range(2)] for i in range(2)] + Hphys = hessian_at(f, pt, d) + ok22 = det(Hphys) == det(H) == det(Di) * det(K) + negD, _, _ = inertia(Di) + negK, posK, zK = inertia(K) + negH, posH, zH = inertia(Hphys) + ok22 &= negD == n and zK == 0 and zH == 0 and negH == negD + negK + ok22 &= (negH == d) if sgn < 0 else (negH == d - 1) + # K/r - P_i = O(r): exact size check against the explicit bound |C|^2 |D_i^{-1}| / r + ok22 &= max(abs(K[i][j] / r - Pi[i][j]) for i in range(2) for j in range(2)) <= r * k + res["schur_det_inertia_A21_A22"] &= ok22 + dets.append(abs(det(Hphys))) + # H_i u = O(r): H(0) u = 0 exactly by pins, so H_i u = sgn (r/2) (f_xxx, f_xxy...). + Hu = [Hphys[i][0] for i in range(d)] + third = [pderiv_at0(f, eplus(x, x, unit(d, i))) for i in range(d)] + res["Hu_order_r"] &= Hu == [sgn * r / 2 * c for c in third] + res["weight_order_r4"] &= (dets[0] * dets[1] / r ** (8 if MUT == "weight-2d" else 4)) > F(1, 1000) + # Gradient-pin average: r * int_{-1/2}^{1/2} H(t r u) u dt = grad f(S) - grad f(M) = 0. + t = pvar(0, 1) + line = [pscale(t, r)] + [{} for _ in range(d - 1)] + avg = [] + for i in range(d): + col = pcompose(pdiff(pdiff(f, i), 0), line, 1) + prim = {(e[0] + 1,): c / (e[0] + 1) for e, c in col.items()} + avg.append(r * (peval(prim, [F(1, 2)]) - peval(prim, [F(-1, 2)]))) + res["gradient_pin_average_A24"] &= all(v_ == 0 for v_ in avg) + out.update(res) + return out + + +# --------------------------------------------------------------------------------------------------------------- +# QUARTIC group: pins re-solved through the contact frame, O(r) remainder +# --------------------------------------------------------------------------------------------------------------- + +def build_quartic(d, rng, r, k, b, sigma, v, D, tau, quartic): + """Physical quartic field: free jets (transverse Hessian, third derivatives except xxx) from the chart, a fixed + quartic part, and the 2(d+1) U_0 jets (f, f_x, f_xx, f_xxx, f_y, f_xy) solved from the pins.""" + n = d - 2 + q = solve(D, v) if n else [] + a = sigma + sum(vi * qi for vi, qi in zip(v, q)) + x = unit(d, 0) + tau_free = {e: c for e, c in tau.items() if e != eplus(x, x, x)} + cubic_phys = pcompose(from_jets(tau_free, d), shear_subs(d, q, sign=+1), d) + base = padd(cubic_phys, quartic) + A = [[a] + list(v)] + [[v[i]] + list(D[i]) for i in range(n)] + for i in range(d - 1): + for j in range(i, d - 1): + e = eplus(unit(d, i + 1), unit(d, j + 1)) + base = padd(base, {e: A[i][j] / math.prod(factorial(t) for t in e)}) + U0 = [(0,) * d, x, eplus(x, x), eplus(x, x, x)] + for j in range(1, d): + U0 += [unit(d, j), eplus(x, unit(d, j))] + basis = [from_jets({e: 1}, d) for e in U0] + M = [-r / 2] + [F(0)] * (d - 1) + S = [r / 2] + [F(0)] * (d - 1) + rows, rhs = [], [] + for pt, val in ((M, b), (S, b - k * r ** 3)): + rows.append([peval(p, pt) for p in basis]) + rhs.append(val - peval(base, pt)) + for pt in (M, S): + for i in range(d): + rows.append([peval(pdiff(p, i), pt) for p in basis]) + rhs.append(-peval(pdiff(base, i), pt)) + frame_det = det(rows) + coeffs = solve(rows, rhs) + f = padd(base, *[pscale(p, c) for p, c in zip(basis, coeffs)]) + return f, q, frame_det + + +def random_quartic(d, rng, size): + return {e: rat(rng, -size, size) for e in multi(d, 4)} + + +def check_quartic(): + out = {} + rng = random.Random(125003) + k, b = F(6, 5), F(1, 3) + ok_frame = ok_pins = True + rates = {} + hu_rates = {} + grid = [F(i, 4) for i in range(-8, 9)] + for d in (3, 4): + quartic = random_quartic(d, rng, F(1, 2)) + base_rng_state = rng.getstate() + errs, hus = [], [] + for r in (F(1, 8), F(1, 16), F(1, 32), F(1, 64)): + rng.setstate(base_rng_state) + sigma, v, D, tau = sample_chart(d, rng, r, k) + f, q, frame_det = build_quartic(d, rng, r, k, b, sigma, v, D, tau, quartic) + ok_frame &= frame_det != 0 + M = [-r / 2] + [F(0)] * (d - 1) + S = [r / 2] + [F(0)] * (d - 1) + ok_pins &= (peval(f, M) == b and peval(f, S) == b - k * r ** 3 + and all(g == 0 for g in gradient_at(f, M, d) + gradient_at(f, S, d))) + ft = pcompose(f, shear_subs(d, q), d) + x, z = unit(d, 0), unit(d, 1) + s_coef = hessian_at(ft, [F(0)] * d, d)[1][1] / r + P = planar_normal_form(k, s_coef, pderiv_at0(ft, eplus(x, x, z)), pderiv_at0(ft, eplus(x, z, z)), + pderiv_at0(ft, eplus(z, z, z))) + Fr = scaled_plane(ft, d, r, b) + diff = padd(Fr, pscale(P, -1)) + errs.append(max(abs(peval(diff, [X, Z])) for X in grid for Z in grid if X * X + Z * Z <= 9)) + Hs = hessian_at(f, S, d) + hus.append(max(abs(Hs[i][0]) for i in range(d))) + rates[d] = [float(errs[i] / errs[i + 1]) for i in range(3)] + hu_rates[d] = [float(hus[i] / hus[i + 1]) for i in range(3)] + out["contact_frame_nonsingular"] = ok_frame + out["pins_exact_after_solve"] = ok_pins + out["A17_remainder_halves_with_r"] = all(1.6 < x_ < 2.4 for rs in rates.values() for x_ in rs) + out["Hu_halves_with_r"] = all(1.6 < x_ < 2.4 for rs in hu_rates.values() for x_ in rs) + out["_rates"] = {"A17_remainder": {str(d_): [round(x_, 4) for x_ in v_] for d_, v_ in rates.items()}, + "H_S_u": {str(d_): [round(x_, 4) for x_ in v_] for d_, v_ in hu_rates.items()}} + return out + + +# --------------------------------------------------------------------------------------------------------------- +# SADDLES group (NUMERIC) +# --------------------------------------------------------------------------------------------------------------- + +def to_float_poly(p): + return {e: float(c) for e, c in p.items()} + + +def fl_eval(p, pt): + return sum(c * math.prod(x ** k_ for x, k_ in zip(pt, e)) for e, c in p.items()) + + +def lin_solve_float(A, b): + n = len(A) + W = [list(A[i]) + [b[i]] for i in range(n)] + for j in range(n): + p = max(range(j, n), key=lambda i: abs(W[i][j])) + W[j], W[p] = W[p], W[j] + for i in range(n): + if i != j: + f = W[i][j] / W[j][j] + W[i] = [x - f * y for x, y in zip(W[i], W[j])] + return [W[i][-1] / W[i][i] for i in range(n)] + + +def float_inertia(A): + n = len(A) + W = [list(r) for r in A] + neg = 0 + for j in range(n): + piv = W[j][j] + if piv == 0: + return None + neg += piv < 0 + for i in range(j + 1, n): + f = W[i][j] / piv + for l in range(j, n): + W[i][l] -= f * W[j][l] + return neg + + +def newton(grad, hess, x0, steps=60): + x = list(x0) + for _ in range(steps): + g = [fl_eval(p, x) for p in grad] + H = [[fl_eval(p, x) for p in row] for row in hess] + dx = lin_solve_float(H, [-t for t in g]) + x = [a + b for a, b in zip(x, dx)] + if max(abs(t) for t in dx) < 1e-15: + break + return x + + +def check_saddles(): + out = {} + rng = random.Random(125004) + k, b = F(6, 5), F(1, 3) + ok_exist = ok_index = ok_height = ok_distinct = ok_not_planar = True + conv = {} + for d in (3, 4): + n = d - 2 + quartic = random_quartic(d, rng, F(1, 2)) + state = rng.getstate() + errs = [] + for r in (F(1, 16), F(1, 32), F(1, 64), F(1, 128)): + rng.setstate(state) + sigma, v, D, tau = sample_chart(d, rng, r, k) + f, q, _ = build_quartic(d, rng, r, k, b, sigma, v, D, tau, quartic) + ft = pcompose(f, shear_subs(d, q), d) + x, z = unit(d, 0), unit(d, 1) + s_coef = hessian_at(ft, [F(0)] * d, d)[1][1] / r + P = planar_normal_form(k, s_coef, pderiv_at0(ft, eplus(x, x, z)), pderiv_at0(ft, eplus(x, z, z)), + pderiv_at0(ft, eplus(z, z, z))) + Pf = to_float_poly(P) + gP = [to_float_poly(pdiff(P, i)) for i in range(2)] + hP = [[to_float_poly(pdiff(pdiff(P, i), j)) for j in range(2)] for i in range(2)] + ftf = to_float_poly(ft) + g = [to_float_poly(pdiff(ft, i)) for i in range(d)] + h = [[to_float_poly(pdiff(pdiff(ft, i), j)) for j in range(d)] for i in range(d)] + # stable quadratic Q(X, Z) of (A28) from the actual sheared third derivatives + Qs = [] + for j in range(n): + wj = unit(d, j + 2) + t_xx, t_xz, t_zz = (pderiv_at0(ft, eplus(x, x, wj)), pderiv_at0(ft, eplus(x, z, wj)), + pderiv_at0(ft, eplus(z, z, wj))) + Qs.append((float(t_xx), float(t_xz), float(t_zz))) + Df = [[float(D[i][j]) for j in range(n)] for i in range(n)] + rf = float(r) + pts = [] + for sgnZ in (1, -1): + p = newton(gP, hP, [-0.75, sgnZ * math.sqrt(15 / 8)]) + Qp = [t0 / 2 * (p[0] ** 2 - 0.25) + t1 * p[0] * p[1] + t2 / 2 * p[1] ** 2 for (t0, t1, t2) in Qs] + Wstar = lin_solve_float(Df, [-t for t in Qp]) + # the planar restriction's critical point is not a full critical point + grad_w_planar = [fl_eval(g[j + 2], [rf * p[0], rf * p[1]] + [0.0] * n) / rf ** 2 for j in range(n)] + if MUT == "planar-point-is-critical": + ok_not_planar &= max(abs(t) for t in grad_w_planar) < 1e-12 + else: + ok_not_planar &= max(abs(t) for t in grad_w_planar) > 1e-4 + scale_w = rf if MUT == "stable-scale-r" else rf ** 2 + x0 = [rf * p[0], rf * p[1]] + [rf ** 2 * t for t in Wstar] + sol = newton(g, h, x0) + gn = max(abs(fl_eval(gi, sol)) for gi in g) + ok_exist &= gn < 1e-15 and math.dist(sol[:2], x0[:2]) < 8 * rf ** 2 # O(r) shift in scaled units + H = [[fl_eval(hij, sol) for hij in row] for row in h] + ok_index &= float_inertia(H) == d - 1 + height = fl_eval(ftf, sol) + ok_height &= float(b) - float(k) * rf ** 3 < height < float(b) + Wn = [t / scale_w for t in sol[2:]] + errs.append(max(abs(a_ - b_) for a_, b_ in zip(Wn, Wstar)) / rf) + pts.append(sol) + ok_distinct &= math.dist(pts[0], pts[1]) > 0.5 * rf and all( + math.dist(pp, [s_ * rf / 2] + [0.0] * (d - 1)) > 0.5 * rf for pp in pts for s_ in (-1, 1)) + conv[d] = errs + # |w/r^2 - W*| = O(r): the normalized error |w/r^2 - W*| / r stays within a factor 2 over r = 1/16 ... 1/128, + # separately for the + and - saddle (entries alternate + / - per r). + ratios = {d_: [max(e[i::2]) / min(e[i::2]) for i in (0, 1)] for d_, e in conv.items()} + out["two_extra_critical_points_exist"] = ok_exist + out["index_d_minus_1"] = ok_index + out["heights_inside_window"] = ok_height + out["distinct_from_each_other_and_pins"] = ok_distinct + out["planar_critical_point_not_full_critical"] = ok_not_planar + out["stable_displacement_W_converges_at_rate_r"] = all(x_ < 2 for rs in ratios.values() for x_ in rs) + out["_ratios"] = {str(d_): [round(x_, 4) for x_ in rs] for d_, rs in ratios.items()} + return out + + +# --------------------------------------------------------------------------------------------------------------- +# PATH and LEDGER groups +# --------------------------------------------------------------------------------------------------------------- + +def check_path(): + k = F(1) + G = planar_normal_form(k, F(-3, 2), F(0), F(-2), F(0)) + t = pvar(0, 1) + segs = [((F(-1, 2), F(0)), (F(-3, 4), F(0))), ((F(-3, 4), F(0)), (F(-3, 4), F(9, 4))), + ((F(-3, 4), F(9, 4)), (F(-1), F(9, 4)))] + want = [{(2,): F(-3, 16), (3,): F(-1, 32)}, {(0,): F(-7, 32)}, + {(0,): F(-7, 32), (1,): F(51, 64), (2,): F(-9, 32), (3,): F(-1, 32)}] + ok = True + for (p0, p1), w in zip(segs, want): + line = [padd(pconst(p0[i], 1), pscale(t, p1[i] - p0[i])) for i in range(2)] + ok &= pcompose(G, line, 1) == w + ok &= max(p0[0] ** 2 + p0[1] ** 2, p1[0] ** 2 + p1[1] ** 2) <= F(97, 16) < 9 + d3 = {(0,): F(51, 64), (1,): F(-9, 16), (2,): F(-3, 32)} + ok &= min(peval(d3, [F(i, 64)]) for i in range(65)) >= F(9, 64) and peval(d3, [F(1)]) == F(9, 64) + ok &= F(-7, 32) - F(1, 64) > F(-1, 4) and F(17, 64) - F(1, 64) == F(1, 4) + ok &= peval(G, [F(-1, 2), F(0)]) == 0 and peval(G, [F(1, 2), F(0)]) == -1 + # extra saddles of G + Z2 = F(15, 8) + gx = pdiff(G, 0) + ok &= peval(gx, [F(-3, 4), F(0)]) + (-Z2) == 0 # G_X = 6X^2 - 3/2 - Z^2 at X=-3/4 vanishes iff Z^2 = 15/8 + ok &= F(3, 2) + 2 * F(-3, 4) == 0 # G_Z = -Z(3/2 + 2X) vanishes at X = -3/4 + ok &= 2 * F(-3, 4) ** 3 - F(3, 2) * F(-3, 4) - F(1, 2) - (F(3, 4) + F(-3, 4)) * Z2 == F(-7, 32) + ok &= 12 * F(-3, 4) * 0 - 4 * Z2 == F(-15, 2) # det [[-9, -2Z], [-2Z, 0]] = -4 Z^2 + ok &= F(9, 16) + Z2 < 9 + hm = [[peval(pdiff(pdiff(G, i), j), [F(-1, 2), F(0)]) for j in range(2)] for i in range(2)] + hs = [[peval(pdiff(pdiff(G, i), j), [F(1, 2), F(0)]) for j in range(2)] for i in range(2)] + ok &= hm == [[-6, 0], [0, F(-1, 2)]] and hs == [[6, 0], [0, F(-5, 2)]] + return {"path_segments_margins_and_saddle_data": ok} + + +def check_ledger(): + out = {} + ok = True + for d in range(2, 13): + m = d - 1 + U = 2 * (d + 1) + J = m * (m + 1) // 2 + comb(d + 2, 3) - 1 + ok &= U + J == comb(d + 3, 3) + out["jet_count_U0_plus_J_is_binom_d3_3"] = ok + rare, weight, norm = 1, (2 * 4 if MUT == "weight-2d" else 4), 2 + out["ledger_r_r4_over_r2_is_r3_all_d"] = rare + weight - norm == 3 + # ell = k r^3 at fixed k: r dr = (1/3) ell^(-1/3) k^(-2/3) d ell; times (1 - p) ~ r^3 = ell/k. + r_exp = F(1, 3) # r = ell^(1/3) k^(-1/3) + jac_exp_ell = r_exp - 1 + jac_exp_k = -r_exp + measure_ell = (0 if MUT == "density-dr" else r_exp) + jac_exp_ell + measure_k = (0 if MUT == "density-dr" else -r_exp) + jac_exp_k + loss_ell, loss_k = measure_ell + 1, measure_k - 1 + out["density_loss_ell_2_3_k_minus_5_3"] = (measure_ell, measure_k, loss_ell, loss_k) == ( + F(-1, 3), F(-2, 3), F(2, 3), F(-5, 3)) + threshold = F(2, 3) if MUT == "threshold-two-thirds" else loss_ell + 1 + ok_t = threshold == F(5, 3) + for p in (F(1), F(3, 2), F(8, 5)): + ok_t &= (loss_ell - p) > -1 # integrable at 0 + for p in (F(5, 3), F(2)): + ok_t &= (loss_ell - p) <= -1 # not integrable at 0 (log at 5/3) + out["inverse_moment_threshold_5_3"] = ok_t + return out + + +def flatten(d): + for k_, v_ in d.items(): + if k_.startswith("_"): + continue + if isinstance(v_, dict): + yield from flatten(v_) + else: + yield v_ + + +def main(): + global MUT + ap = argparse.ArgumentParser() + ap.add_argument("--mutant", choices=MUTANTS) + MUT = ap.parse_args().mutant + checks = {"CHART": check_chart(), "PHYSICAL": check_physical(), "QUARTIC": check_quartic(), + "SADDLES": check_saddles(), "PATH": check_path(), "LEDGER": check_ledger()} + passed = all(flatten(checks)) + print(json.dumps({"object": "CLAUDE-REVIEW-ELDER-DIMENSION-LIFT-20260928-v1", "checks": checks, + "passed": passed, + "scope": "exact chart/field identities and one labelled numerical saddle group; " + "not an analytic proof"}, indent=2, sort_keys=True)) + return 0 if passed else 1 + + +if __name__ == "__main__": + sys.exit(main()) From 32bec6a9384632b1d8da345674c014c7fb1cae37 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 28 Sep 2026 23:57:36 +0000 Subject: [PATCH 3/4] review record: nonauthor review of #116 C3 remote factorial-pair law (scientific effect NONE) Anthropic nonauthor analytic review of OA-WINDOW-MULTIPLICITY-REMOTE-20260928-v1 (REMOTE_PAIR_LAW.md blob 3fb60204, SHA256 b818a11f) at exact head 0507e3a. Verdict: ACCEPT at the stated fixed-E, fixed-rho existential scope for Theorem R (R4)-(R5) and Theorem H2 (R12)-(R15). No defect found. The reviewer authored RC, whose Lemmas 1, 2, 3, 5 and (3.1) C3 imports; that exposure is disclosed. Independent stdlib checker: exact pair fields with both critical points, congruence limits with exactly linear error, orientation rule vs exact inertia, windows, overlap integral, coefficient, Beta(2/3,2) moments; 5 rejected mutants; output identical in -O. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_017Mi3hxjaxV45x6zo6o1ee3 --- .github/workflows/remote-pair-law-review.yml | 60 +++++ .../RESULTS.json | 37 +++ .../remote_pair_law_claude_20260928/REVIEW.md | 176 +++++++++++++ .../SOURCE_FILES.json | 37 +++ .../remote_pair_review_check.py | 247 ++++++++++++++++++ 5 files changed, 557 insertions(+) create mode 100644 .github/workflows/remote-pair-law-review.yml create mode 100644 reviews/remote_pair_law_claude_20260928/RESULTS.json create mode 100644 reviews/remote_pair_law_claude_20260928/REVIEW.md create mode 100644 reviews/remote_pair_law_claude_20260928/SOURCE_FILES.json create mode 100644 reviews/remote_pair_law_claude_20260928/remote_pair_review_check.py diff --git a/.github/workflows/remote-pair-law-review.yml b/.github/workflows/remote-pair-law-review.yml new file mode 100644 index 000000000..9a4c5c2d9 --- /dev/null +++ b/.github/workflows/remote-pair-law-review.yml @@ -0,0 +1,60 @@ +name: Remote pair-law nonauthor review checks + +'on': + pull_request: + paths: + - 'reviews/remote_pair_law_claude_20260928/**' + - '.github/workflows/remote-pair-law-review.yml' + workflow_dispatch: + +permissions: + contents: read + +jobs: + exact-and-probe: + runs-on: ubuntu-latest + timeout-minutes: 10 + steps: + - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 + with: + persist-credentials: false + - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 + with: + python-version: '3.11.16' + - name: Verify sources, replay both modes, reject mutants + env: + PYTHONDONTWRITEBYTECODE: '1' + run: | + set -euo pipefail + python -B -S - <<'PY' + import hashlib, json, pathlib, subprocess, sys + root = pathlib.Path('reviews/remote_pair_law_claude_20260928').resolve() + manifest = json.loads((root / 'SOURCE_FILES.json').read_text())['files'] + present = sorted(p.name for p in root.iterdir()) + expected_names = sorted([e['path'] for e in manifest] + ['SOURCE_FILES.json']) + if present != expected_names: + raise ValueError('packet tree differs from manifest: ' + repr(present)) + for entry in manifest: + path = root / entry['path'] + if pathlib.PurePosixPath(entry['path']).name != entry['path'] or path.is_symlink(): + raise ValueError('flat regular source required: ' + entry['path']) + data = path.read_bytes() + if len(data) != entry['bytes'] or hashlib.sha256(data).hexdigest() != entry['sha256']: + raise ValueError('source identity mismatch: ' + entry['path']) + script = str(root / 'remote_pair_review_check.py') + expected = (root / 'RESULTS.json').read_bytes() + mutants = ['exponent-d', 'chi-orientation', 'coefficient-power', 'beta-normalizer', + 'overlap-exponent'] + for flags in (['-B', '-S'], ['-B', '-O', '-S']): + out = subprocess.run([sys.executable, *flags, script], + check=True, capture_output=True, timeout=300).stdout + if out != expected: + raise RuntimeError('output differs from RESULTS.json under ' + ' '.join(flags)) + for m in mutants: + rc = subprocess.run([sys.executable, *flags, script, '--mutant', m], + capture_output=True, timeout=300).returncode + if rc != 1: + raise RuntimeError('mutant ' + m + ' not rejected') + print(json.dumps({'scientific_effect': 'NONE', 'mathematical_acceptance': False})) + PY + git diff --exit-code diff --git a/reviews/remote_pair_law_claude_20260928/RESULTS.json b/reviews/remote_pair_law_claude_20260928/RESULTS.json new file mode 100644 index 000000000..efa24bfa6 --- /dev/null +++ b/reviews/remote_pair_law_claude_20260928/RESULTS.json @@ -0,0 +1,37 @@ +{ + "checks": { + "COEFF": { + "coefficient_54_over_5_times_12_minus_4_3_is_3_40_12_2_3": true + }, + "HEIGHT": { + "beta_normalizer_9_over_10": true, + "gap_moments_R15": true, + "h_integrates_to_one": true, + "independent_uniform_mean_gap_is_one_third": true, + "marginal_and_correlation_R15": true, + "pushforward_jacobian": true, + "triangle_density_integrates_to_one": true + }, + "LEDGER": { + "delta_exponent_is_one_all_d": true, + "r_power_is_five_all_d": true + }, + "OVERLAP": { + "R10_overlap_integral_exact": true, + "envelope_s_min_1_s_minus3_is_3_over_2": true + }, + "PAIR": { + "R2_orientation_matches_exact_inertia": true, + "R8_congruence_limits_with_O_delta_error": true, + "e_to_minus_e_exchanges_ordered_indices": true, + "pair_fields_have_both_critical_points": true, + "same_index_pairs_only_at_order_delta_squared": true + }, + "WINDOW": { + "R9_z_length_is_k_minus_s3_abs_t": true + } + }, + "object": "CLAUDE-REVIEW-REMOTE-PAIR-LAW-20260928-v1", + "passed": true, + "scope": "exact finite identities only; not an analytic proof" +} diff --git a/reviews/remote_pair_law_claude_20260928/REVIEW.md b/reviews/remote_pair_law_claude_20260928/REVIEW.md new file mode 100644 index 000000000..5c4d30ca3 --- /dev/null +++ b/reviews/remote_pair_law_claude_20260928/REVIEW.md @@ -0,0 +1,176 @@ +# Nonauthor analytic review: the leading remote factorial-pair measure and its height-gap law (Math-#116, C3) + +Scientific effect: **NONE**. This file changes no register, status, graph node, lemma flag, prize or author source. +It records a verdict on candidate C3 of `reviews/candidates_pending_20260928/CANDIDATES.md`. Integration is a +separate act. + +## Object + +| Field | Value | +|---|---| +| Object | OA-WINDOW-MULTIPLICITY-REMOTE-20260928-v1 (OpenAI / ChatGPT) | +| Branch / head | `chatgpt/window-multiplicity-laws-20260928` / `0507e3a1dbd3dede84cbeb805947c70aa16ebc36` ([Math-#116](https://github.com/d6g8k5htny-coder/Math-/pull/116)) | +| `REMOTE_PAIR_LAW.md` | Git blob `3fb602040b37158b16ba61bdfc62cc8df1ccc616`, 15878 B, SHA256 `b818a11f1abcf37616d592ecda6341b0d99365cf3ac5047bc2dbaede95da4c5e`, 325 lines | +| Consumed, on main | [RC] `frontiers/remote_collision_20260928/PROOF.md` (blob `7b48a88e…`): (3.1), (4.1)–(4.3), Lemmas 1, 2, 3, 5. [RM] `frontiers/remote_window_20260924/PROOF.md` (blob `b383bfcc…`): contact frame, (8), §4. The D1 normalizer `Z_r/r² → z_0` (reconciled in Math-#126, merged at `8224783`). | +| Request | [Owner comment 5880152796](https://github.com/d6g8k5htny-coder/Math-/pull/116#issuecomment-5880152796); claimed in [5880826796](https://github.com/d6g8k5htny-coder/Math-/pull/116#issuecomment-5880826796) | + +## Provenance and exposure + +| Field | Value | +|---|---| +| Reviewer | Anthropic Claude, Claude Code session `session_017Mi3hxjaxV45x6zo6o1ee3` | +| Relation | Different provider from the OpenAI author. Same GitHub account as every lane, so no organizational independence is claimed. | +| Exposure | **I authored [RC]**, whose Lemmas 1, 2 and 5 and formula (3.1) C3 imports verbatim. I also reviewed LP Theorem A (#106), IW (#109) and C1/C2 (#123), and I reconciled D1 (#126). This review therefore checks that C3 uses [RC] correctly. It is not independent evidence for [RC] itself. [RC]'s nonauthor review is the xAI/Harper review 5342481786 on #110, which accepted its finite identities, the (3.1) mark and the Lemma 1 mechanism. | +| Author code | `algebra.py` is absent from the tree, as `PUBLICATION.json` discloses. I did not run, request or reconstruct it. | +| Independent checks | `remote_pair_review_check.py` is my own exact-rational suite, written from the markdown. It covers finite identities only. | + +## Verdicts + +| Interface (lines) | Verdict | +|---|---| +| §1 (8–26): ordered-pair count `T_ij`, `Σ T_ij = N(N−1)`; no event asymptotic inferred | **ACCEPT** | +| §3 (81–121): coupled regression on `(U_r, V_δ)`; convergence to the `(U_0, V_0)` regression; full conditional support of `(B_0, A, T)` | **ACCEPT**; see §1 below. | +| §4 (123–159): (R7) and the congruence limits (R8); `W_r/r² → w_0`; adjacency; same-index pairs are higher order | **ACCEPT**; see §2 below. | +| §5 (161–233): blow-up ledger, windows (R9), domination, fixed-Borel translation, (R10), coefficient (R11) = (R3), separated pairs, positivity and symmetry | **ACCEPT**; see §3 below. | +| **Theorem R (R4)–(R5)**: `E T_ij(E) = r⁵ ∫_E K_ij + o(r⁵)`; `K_ij > 0` iff `|i−j| = 1`; `E N_j(N_j−1) = o(r⁵)` | **ACCEPT** at the stated fixed-`E`, fixed-`ρ`, existential scope | +| **Theorem H2 (R12)–(R15)**: TV convergence of the factorial-pair height measure to `(5/9)|a−b|^{−1/3}`; Beta(2/3, 2) gap; moments | **ACCEPT**; see §4 below. | +| §7 (306–325) exclusions | **ACCEPT** as stated. They are needed: see N2. | + +No defect was found. Notes N1–N4 delimit the result without changing it. + +--- + +## §1 — the coupled conditional frame (§3) + +`V_δ` is exactly [RC] (4.1). Its `δ = 0` extension (R6) follows from the Peano form [RC] (4.2), where +`D3_δ → −(1/12)∂_e³f(x)`. + +[RC] Lemma 1 gives the covariance sandwich for `(U_r, V_δ)` on the compact parameter set, including +`r = δ = 0`. [RC] Lemma 2 gives conditional moments polynomial in `t` and a target density decaying faster than any +power of `t`. + +C3's extra step: regress one smooth field on `O_{r,δ} = (U_r, V_δ)` and let `(r, δ) → 0`. This is sound. The +regression coefficients `Cov(F(z), O)Cov(O)⁻¹` converge because every entry is an integral derivative average +against kernels that tend to point masses, and the inverse is uniformly bounded by the floor. The targets +`a_{r,δ} → (v_0, 0, 0, b, t)`. Hence convergence holds in `L^p(C^q)` on compact target sets. The mean need not +vanish, and C3 does not claim it does (line 114). + +**Full conditional support.** The functionals `(U_0, B_0)` at `0` and `(Y, A, T)` at `x`, with `|x| ≥ ρ`, are +distinct jets of order ≤ 3 at two distinct torus points. They are jointly nondegenerate. A null combination gives +`P(ω) + Q(ω)e^{iω·x} = 0` on the dual lattice. Choose a lattice direction `v` with `v·x ∉ 2πℤ`. Along each lattice +line in direction `v`, a polynomial in `n` would equal a polynomial times `e^{in v·x}`. That forces both polynomials +to vanish, so `P = Q = 0`. + +This argument is mine; the manuscript cites [RM]'s distributional argument. It gives full support of `(B_0, A, T)` +given `(U_0, Y)`. `H ↦ He` is onto `ℝ^d`, and `He` together with `A` exhausts the Hessian entries at `x`. + +## §2 — determinant limits without inverses (§4) + +(R7): on `∇f(x) = ∇f(x+δe) = 0`, +`0 = ∫_0^δ H(x+τe)e dτ = δH_x e + (δ²/2)D³f(x)[e,e,·] + O(δ³‖f‖_{C⁴})`, which is the first line. The second follows +from `H_{x'}e = H_x e + δD³f[e,e,·] + O(δ²)`. + +In a frame beginning with `e`, conjugate by `diag(δ^{−1/2}, I)`: +- the `ee` entry becomes `∓T/2 + O(δ)`; +- the cross entries are `O(√δ)`; +- the lower block is exactly `A` at `x` and `A + O(δ)` at `x'`. + +Congruence preserves inertia and multiplies determinants by `δ^{−1}`. `F_j` is continuous everywhere, including on +singular matrices: it is `|det|` times an index indicator, and `|det| → 0` at the index boundaries. Polynomial moments +then give (R8) in `L^p`. The limit product `(T²/4)(det A)²χ_ij` has index `a+1` at `x` and `a` at `x'` when `T > 0`, +which is (R2). The normalizer `W_r/r² → w_0` and `Z_r/r² → z_0` are the D1 normalizer (I), read with the congruence +erratum `D_r = diag(r^{−1/2}, I)`. + +Exact checks (`PAIR`) use the explicit field +`f(u,v) = (T/6)u³ − (T/4)δu² + ½vᵀAv + (u² − δu)c·v` in d = 2, 3, 4: +- `∇f` vanishes at `0` and `δe`; +- `det H/δ ∓ (T/2)det A = −δ·cᵀadj(A)c` exactly; +- the orientation rule (R2) matches the exact inertia for both signs of `T` and every index of `A`. + +The same-index remark (lines 156–159) is confirmed: `f = c·v(u² − δu) + (λ/2)v²` has `T = 0`, two saddles, and +`det = −c²δ²`, which is order `δ²`. + +## §3 — blow-up, domination, translation, coefficient (§5) + +**Ledger.** The factors are: +- polar coordinates: `δ^{d−1}`; +- the value-gradient change of variables [RC] (4.3): `δ^{−d−3}`; +- the second height `dy' = δ³dt`; +- the determinants: `δ²`. + +The δ-exponent is `(d−1) − (d+3) + 3 + 2 = 1` for every d. With `δ = rs`, `y = b − r³z` and `W/Z → w_0/z_0`, the +r-power is `d + 3 + 3 − (d+3) + 2 = 5` (`LEDGER`, d = 2…10). + +**Windows (R9).** Both heights in `(b − kr³, b)` means `0 < z < k` and `s³t < z < k + s³t`. The `z`-length is +`(k − s³|t|)_+`. This is checked exactly on 400 rational instances (`WINDOW`). + +**Domination.** [RC] Lemmas 3–4 give `W_r ≤ r²K^{2d}` and `|det H_x det H_{x'}| ≤ δ²K^{2d}/4`. [RC] Lemma 2 gives +the envelope `Cs(1+|t|)^{−p}1_{(R9)}`. Integrating over `z` and `t` gives `≤ Cs·min(1, s^{−3})`, whose integral is +finite (`∫_0^∞ s·min(1,s^{−3})ds = 3/2`). The envelope is uniform in `r` and in the compact parameters, and +zero-extension beyond `s < η_0/r` is harmless. Dominated convergence applies. + +**Fixed Borel E.** The factor `1_E(x+rse)` is removed by continuity of translation in `L¹(torus)`. On bounded `s` the +shifts are at most `rS_0`, and the envelope controls `s > S_0`. No boundary regularity is used, and none is claimed +for `r`-dependent `E_r`. The argument is correct as written (lines 193–203). + +**Coefficient.** Integrating `z` gives `(k − s³|t|)_+`. Then +`∫_0^{s_max} s(k − s³|t|) ds = (3/10)k·s_max² = (3/10)k^{5/3}|t|^{−2/3}` (R10), checked exactly (`OVERLAP`). +Multiplying by `36t²` gives `(54/5)k^{5/3}|t|^{4/3}`. With `t = −T/12`, this becomes +`(54/5)·12^{−4/3} = (3/40)·12^{2/3}`, since `54/5 = (3/40)·144` (`COEFF`). The conditional density of `t` given `Y` +converts to `E[·|Y]` with no extra Jacobian. The surface measure and the ordered-pair convention match (R3). Tonelli +away from `t = 0` is the right way to handle the `|t|^{−2/3}` factor. + +**Separated pairs.** [RC] Lemma 5 gives `O(r⁶)|E|²`, which is `o(r⁵)` for fixed `E`. + +**Positivity and symmetry.** The integrand is positive on an open set by §1. Under `e ↦ −e`, `T ↦ −T` while `A` and +`w_0` are unchanged, and the linear map on `Y` has `|det| = 1` at the symmetric target `(0,0,b)`. So +`χ_ij(A,−T) = χ_ji(A,T)` (checked), and `∫_S K_ij = ∫_S K_ji`. Hence (R5). + +## §4 — the factorial-pair height law (§6) + +(R12) is a normalized factorial-moment measure. §6 says explicitly that it is not the event-conditioned pair law, and +this review accepts only the former. + +The dominated convergence of §3 is `L¹` convergence of the blown-up nonnegative densities, not only of their masses. +Pushforward to `(θ, θ') = (z/k, (z − s³t)/k)` contracts TV, and dividing by the converging positive total mass +preserves TV convergence. + +**Jacobian.** With `g = s³|t|/k`, `s ds = (1/3)(k/|t|)^{2/3}g^{−1/3}dg`. This is checked as the exact identity +`s/(dg/ds) = k/(3s|t|)` (`HEIGHT`). With `dz = k dθ` and `θ ∈ (0, 1−g)`, each sign of `T` gives a density +proportional to `g^{−1/3}` on its triangle, of mass `∫_0^1 g^{−1/3}(1−g)dg = 9/10`. The two triangles carry equal +mass by `e ↦ −e`. + +This gives `h = (5/9)|a−b|^{−1/3}`. The index-resolved density is `(10/9)(b−a)^{−1/3}` on `a < b` for `i = j+1`: the +index-`(a+1)` point lies above its adjacent partner. The gap is Beta(2/3, 2), and the following are all exact +(`HEIGHT`): +- the CDF (R14); +- `E g^n = 10/((3n+2)(3n+5))`; +- `E g = 1/4` and `Var g = 9/176`; +- the marginal `(5/6)(a^{2/3} + (1−a)^{2/3})`; +- `E a² = 29/88`, `E ab = 3/11` and `Corr = 2/7`. + +## Notes + +- **N1.** (R3) has hidden `k`-dependence beyond `k^{5/3}`, because `Q_0` conditions on `f_xxx = 12k`. Nothing in + C3 claims otherwise. The coefficient should be read as "`k^{5/3}` times a `k`-dependent Gaussian conditional + integral". +- **N2.** The fixed exclusion `ρ` is load-bearing. [RC] Lemma 1's floor is not uniform as `ρ → 0` ([RC] §8). + LOCAL_MULTIPLICITY shows that pairs near the pins have order `r³`. §7's exclusions are therefore required, not + cosmetic. +- **N3.** A factorial-moment asymptotic does not give `Q(N ≥ 2) ~ (r⁵/2)∫ΣK` without higher factorial moments. + §7 says so, and this review adds nothing there. +- **N4.** Novelty boundary: generic adjacent-index attraction of critical points in the unconditioned isotropic + setting is prior work (Azaïs–Delmas, arXiv:1911.02300). What this review accepts is the pinned, tilted, fixed-`ρ` + coefficient (R3) and the factorial-pair height law (R13), at existential scope. + +## What this review does not do + +It does not review C4 (`REMOTE_DISTANCE_MOMENTS.md`), C5 or C6. It does not accept an event-conditioned pair law, a +global factorial upper bound, uniformity in `ρ → 0` or in oscillating `E_r`, or any numerical coefficient. It does +not run or reconstruct `algebra.py`, and it changes no register. + +## Reproduce + + python -B -S remote_pair_review_check.py # prints RESULTS.json byte for byte + python -B -O -S remote_pair_review_check.py # identical + python -B -S remote_pair_review_check.py --mutant M # exit 1 for each of the 5 mutants diff --git a/reviews/remote_pair_law_claude_20260928/SOURCE_FILES.json b/reviews/remote_pair_law_claude_20260928/SOURCE_FILES.json new file mode 100644 index 000000000..61bcc9c1e --- /dev/null +++ b/reviews/remote_pair_law_claude_20260928/SOURCE_FILES.json @@ -0,0 +1,37 @@ +{ + "schema": 1, + "scientific_effect": "NONE", + "review_status": "NONAUTHOR_REVIEW", + "reviewed_object": { + "pr": "d6g8k5htny-coder/Math-#116", + "head": "0507e3a1dbd3dede84cbeb805947c70aa16ebc36", + "paths": [ + { + "path": "frontiers/window_multiplicity_laws_20260928/REMOTE_PAIR_LAW.md", + "git_blob": "3fb602040b37158b16ba61bdfc62cc8df1ccc616", + "bytes": 15878, + "sha256": "b818a11f1abcf37616d592ecda6341b0d99365cf3ac5047bc2dbaede95da4c5e" + } + ] + }, + "files": [ + { + "path": "REVIEW.md", + "bytes": 11936, + "sha256": "c6837a64e5883ed102f346de9f38425d34a813081396cf96aab8434ee0e6fa1d", + "git_blob": "5c4d30ca33a4c5eb66cfe211f72d460b7433003c" + }, + { + "path": "RESULTS.json", + "bytes": 1153, + "sha256": "cab1fe5b10031de837bd8064090db7f276328940fe17d668ec5b6c3645b19fa4", + "git_blob": "efa24bfa60d576063c841c4c9794761a0dbf3b71" + }, + { + "path": "remote_pair_review_check.py", + "bytes": 11665, + "sha256": "2cd9b7f06d15aa26d0c3305294ed95f210689bda52ef149e8d6a43b637dbf9ad", + "git_blob": "20bc1ae2ba45b57143a89344c2f1e6289b159526" + } + ] +} diff --git a/reviews/remote_pair_law_claude_20260928/remote_pair_review_check.py b/reviews/remote_pair_law_claude_20260928/remote_pair_review_check.py new file mode 100644 index 000000000..20bc1ae2b --- /dev/null +++ b/reviews/remote_pair_law_claude_20260928/remote_pair_review_check.py @@ -0,0 +1,247 @@ +"""Independent nonauthor checks for OA-WINDOW-MULTIPLICITY-REMOTE-20260928-v1 (Math-#116, REMOTE_PAIR_LAW.md). + +Python standard library only; exact rational arithmetic throughout. Written from the markdown; the author's absent +algebra.py is neither run nor reconstructed. Groups: + + LEDGER radial and r-power ledgers of the blown-up pair Kac-Rice integral: (d-1)-(d+3)+3+2 = 1 and r^5, d = 2..10. + WINDOW (R9): for rational (z-range, s, t) the admissible z-length is exactly (k - s^3|t|)_+. + OVERLAP (R10) on exact instances with k/|t| a rational cube; the envelope integral of s*min(1, s^-3) is 3/2. + COEFF 36*(3/10) = 54/5 and (54/5)*12^(-4/3) = (3/40)*12^(2/3), i.e. 54/5 = (3/40)*144. + PAIR explicit polynomial fields in d = 2, 3, 4 with critical points at x and x + delta*e: exact congruence limits + F_i(H_x)/delta -> F_i(diag(-T/2, A)), F_j(H_x')/delta -> F_j(diag(T/2, A)) with O(delta) error, the + orientation rule (R2) for both signs of T and every index of A, the e -> -e exchange, and the negative + control: T = 0 with a mixed cubic gives two same-index points with determinants of order delta^2. + HEIGHT the pushforward Jacobian s ds = (1/3)(k/|t|)^(2/3) g^(-1/3) dg; the Beta(2/3, 2) normalization 9/10; h + integrates to 1; the index-resolved triangle density (10/9)(b-a)^(-1/3); moments (R15) and Corr = 2/7. + +Mutants (each must fail): exponent-d, chi-orientation, coefficient-power, beta-normalizer, overlap-exponent. +Not an analytic proof: the Gaussian limit, domination and translation steps are reviewed in REVIEW.md. +""" +import argparse +import json +import random +import sys +from fractions import Fraction as F + +MUTANTS = ("exponent-d", "chi-orientation", "coefficient-power", "beta-normalizer", "overlap-exponent") +MUT = None + + +def det(A): + n = len(A) + M = [list(map(F, r)) for r in A] + d = F(1) + for c in range(n): + p = next((i for i in range(c, n) if M[i][c] != 0), None) + if p is None: + return F(0) + if p != c: + M[c], M[p] = M[p], M[c] + d = -d + d *= M[c][c] + for i in range(c + 1, n): + f = M[i][c] / M[c][c] + M[i] = [x - f * y for x, y in zip(M[i], M[c])] + return d + + +def negatives(A): + """Number of negative eigenvalues of a symmetric rational matrix (sign changes of leading minors, generic).""" + n = len(A) + minors = [F(1)] + [det([row[:k] for row in A[:k]]) for k in range(1, n + 1)] + if any(m == 0 for m in minors): + return None + return sum(1 for a, b in zip(minors, minors[1:]) if (a > 0) != (b > 0)) + + +def chi(i, j, neg_a, T): + """(R2): orientation of the adjacent pair; zero on T = 0.""" + if T == 0: + return 0 + sign = 1 if (T > 0) != (MUT == "chi-orientation") else -1 + return int((i, j) == ((neg_a + 1, neg_a) if sign > 0 else (neg_a, neg_a + 1))) + + +# --------------------------------------------------------------------------------------------------------------- + +def check_ledger(): + ok_delta = ok_r = True + for d in range(2, 11): + polar, density, second_height, dets = d - 1, -(d + 3), 3, 2 + if MUT == "exponent-d": + polar = d + ok_delta &= polar + density + second_height + dets == 1 + # r-powers with delta = r s, y = b - r^3 z: polar r^d, dy r^3, dy' = r^3 s^3 dt, density r^(-d-3), dets r^2, + # W/Z -> w0/z0 (r^2 / r^2). + ok_r &= d + 3 + 3 - (d + 3) + 2 == 5 + return {"delta_exponent_is_one_all_d": ok_delta, "r_power_is_five_all_d": ok_r} + + +def check_window(): + rng = random.Random(116301) + ok = True + for _ in range(400): + k = F(rng.randint(1, 40), rng.randint(1, 9)) + s = F(rng.randint(1, 30), rng.randint(1, 9)) + t = F(rng.randint(-60, 60), rng.randint(1, 9)) + # z in (0,k) and (z-k)/s^3 < t < z/s^3 <=> s^3 t < z < k + s^3 t + lo, hi = max(F(0), s ** 3 * t), min(k, k + s ** 3 * t) + length = max(F(0), hi - lo) + ok &= length == max(F(0), k - s ** 3 * abs(t)) + return {"R9_z_length_is_k_minus_s3_abs_t": ok} + + +def check_overlap(): + ok = True + for m in (1, 2, 3, 5): + for tt in (F(1), F(2), F(1, 3), F(7, 5)): + k = F(m) ** 3 * tt # then s_max = (k/|t|)^(1/3) = m + smax = F(m) + integral = k * smax ** 2 / 2 - tt * smax ** 5 / 5 + expo = F(1, 3) if MUT == "overlap-exponent" else F(2, 3) + # (3/10) k^(5/3) |t|^(-2/3) = (3/10) k (k/|t|)^(2/3) = (3/10) k smax^(3*expo) + ok &= integral == F(3, 10) * k * smax ** (3 * expo) + envelope = F(1, 2) + F(1) # int_0^1 s ds + int_1^inf s^-2 ds + return {"R10_overlap_integral_exact": ok, "envelope_s_min_1_s_minus3_is_3_over_2": envelope == F(3, 2)} + + +def check_coeff(): + # (54/5) 12^(-4/3) = c 12^(2/3) <=> 54/5 = c 12^2 ; mutant uses 12^(-2/3) on the right, i.e. 54/5 = c 12^(2/3+2/3) + power = F(2) if MUT != "coefficient-power" else F(4, 3) + c = F(3, 40) + ok = F(36) * F(3, 10) == F(54, 5) and (power.denominator == 1 and F(54, 5) == c * 12 ** int(power)) + return {"coefficient_54_over_5_times_12_minus_4_3_is_3_40_12_2_3": ok} + + +def pair_field_hessians(T, A, c, delta): + """f(u, v) = (T/6)u^3 - (T/4)delta u^2 + (1/2) v^T A v + (u^2 - delta u) c.v on R x R^(d-1). + grad f vanishes at (0,0) and (delta,0); returns the two Hessians and the gradients there.""" + n = len(A) + def hess(u): + Huu = T * u - T * delta / 2 + Huv = [(2 * u - delta) * ci for ci in c] + return [[Huu] + Huv] + [[Huv[i]] + list(A[i]) for i in range(n)] + def grad(u): + return [T / 2 * u * u - T / 2 * delta * u] + [(u * u - delta * u) * ci for ci in c] + return hess(F(0)), hess(delta), grad(F(0)), grad(delta) + + +def check_pair(): + rng = random.Random(116302) + ok_crit = ok_limit = ok_orient = ok_swap = True + for d in (2, 3, 4): + n = d - 1 + for trial in range(12): + # A diagonal-dominant with a chosen number of negative eigenvalues + a_neg = trial % (n + 1) + A = [[F(0)] * n for _ in range(n)] + for i in range(n): + A[i][i] = F(-(i + 2)) if i < a_neg else F(i + 2) + for j in range(i): + A[i][j] = A[j][i] = F(rng.randint(-2, 2), 10) + if negatives(A) != a_neg: + continue + c = [F(rng.randint(-9, 9), 7) for _ in range(n)] + T = F(rng.choice([-1, 1]) * rng.randint(1, 20), 3) + detA = det(A) + errs = [] + for delta in (F(1, 10), F(1, 100), F(1, 1000)): + Hx, Hy, gx, gy = pair_field_hessians(T, A, c, delta) + ok_crit &= all(v == 0 for v in gx + gy) + # exact: det H / delta -/+ (T/2) det A = -delta c^T adj(A) c, so (error / delta) is delta-independent + errs.append(((det(Hx) / delta - (-T / 2) * detA) / delta, (det(Hy) / delta - (T / 2) * detA) / delta)) + nx, ny = negatives(Hx), negatives(Hy) + if nx is not None and ny is not None: + ok_orient &= all(chi(i, j, a_neg, T) == int((i, j) == (nx, ny)) + for i in range(d + 1) for j in range(d + 1)) + # the limit error is exactly linear in delta, with the same slope at both witnesses + ok_limit &= len(set(errs)) == 1 and errs[0][0] == errs[0][1] + # e -> -e flips T and exchanges the ordered indices + ok_swap &= all(chi(i, j, a_neg, -T) == chi(j, i, a_neg, T) for i in range(d + 1) for j in range(d + 1)) + # Negative control: T = 0 and a mixed cubic give two same-index points with det of order delta^2. + ok_neg = True + for lam, cc in ((F(3), F(2)), (F(-5, 2), F(1, 3))): + for delta in (F(1, 10), F(1, 100)): + H0 = [[F(0), -cc * delta], [-cc * delta, lam]] + H1 = [[F(0), cc * delta], [cc * delta, lam]] + ok_neg &= det(H0) == det(H1) == -(cc * delta) ** 2 + ok_neg &= det(H0) / delta ** 2 == -cc * cc # order delta^2, so zero at the delta^1 scale of (R8) + return {"pair_fields_have_both_critical_points": ok_crit, + "R8_congruence_limits_with_O_delta_error": ok_limit, + "R2_orientation_matches_exact_inertia": ok_orient, + "e_to_minus_e_exchanges_ordered_indices": ok_swap, + "same_index_pairs_only_at_order_delta_squared": ok_neg} + + +def check_height(): + out = {} + # pushforward Jacobian on rational points: s ds/dg = k/(3 s |t|) equals (1/3)(k/|t|)^(2/3) g^(-1/3), g = s^3|t|/k. + ok = True + for s, tt, k in ((F(2), F(1), F(8)), (F(3, 2), F(4, 3), F(9, 4)), (F(1, 2), F(5), F(5, 8))): + g = s ** 3 * tt / k + lhs = s / (3 * s * s * tt / k) # s / (dg/ds) + # (k/|t|)^(2/3) g^(-1/3) = (k/|t|)^(2/3) (k/(s^3 |t|))^(1/3) = (k/|t|) / s + rhs = F(1, 3) * (k / tt) / s + ok &= lhs == rhs + out["pushforward_jacobian"] = ok + # int_0^1 g^(-1/3) (1-g) dg = 3/2 - 3/5 = 9/10 + norm = F(3, 2) - F(3, 5) + target = F(1) if MUT == "beta-normalizer" else F(9, 10) + out["beta_normalizer_9_over_10"] = norm == F(9, 10) and norm == target + # h(a,b) = (5/9)|a-b|^(-1/3) integrates to 1: 2 * int_0^1 int_0^b (b-a)^(-1/3) da db = 2 * (3/2)(3/5) + out["h_integrates_to_one"] = F(5, 9) * 2 * F(3, 2) * F(3, 5) == 1 + # index-resolved triangle density (10/9)(b-a)^(-1/3) on a= 1 and rational q > 0: B(p,q) = (p-1)! / (q (q+1) ... (q+p-1)).""" + assert p.denominator == 1 and p >= 1 + out = F(1) + for i in range(int(p) - 1): + out *= F(i + 1) + den = F(1) + for i in range(int(p)): + den *= (q + i) + return out / den + + +def flatten(d): + for v in d.values(): + if isinstance(v, dict): + yield from flatten(v) + else: + yield v + + +def main(): + global MUT + ap = argparse.ArgumentParser() + ap.add_argument("--mutant", choices=MUTANTS) + MUT = ap.parse_args().mutant + checks = {"LEDGER": check_ledger(), "WINDOW": check_window(), "OVERLAP": check_overlap(), "COEFF": check_coeff(), + "PAIR": check_pair(), "HEIGHT": check_height()} + passed = all(flatten(checks)) + print(json.dumps({"object": "CLAUDE-REVIEW-REMOTE-PAIR-LAW-20260928-v1", "checks": checks, "passed": passed, + "scope": "exact finite identities only; not an analytic proof"}, indent=2, sort_keys=True)) + return 0 if passed else 1 + + +if __name__ == "__main__": + sys.exit(main()) From a18bd244b132df3b512c60636bc4af5514b2522f Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 29 Sep 2026 00:08:33 +0000 Subject: [PATCH 4/4] review records: dependency and wording clarifications requested in 5881054670 (scientific effect NONE) - #125 record, section 5: the floating-point SADDLES group is described as a numerical illustration (numerical roots with residual below 1e-15; the factor-2 band is consistent with the O(r) estimate proved analytically, not established by finite samples). Existence comes from the uniform inverse-function argument. - C3 record, Object row and section 2: Z_r is RM's full endpoint-only normalizer; W_r/r^2 -> w_0 under the additional pair conditioning follows from C3 section 3's coupled moment bounds plus RM section 4's endpoint identities, not from the unconditioned D1 normalizer limit alone. N2 now says the planar local result gives an r^3 lower obstruction (and a factorial lower bound), not an all-dimensional exact factorial asymptotic. Checker programs, RESULTS.json bytes and scoped verdicts are unchanged; the two SOURCE_FILES.json manifests are regenerated. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_017Mi3hxjaxV45x6zo6o1ee3 --- .../REVIEW.md | 14 ++++++++------ .../SOURCE_FILES.json | 6 +++--- .../remote_pair_law_claude_20260928/REVIEW.md | 16 +++++++++++----- .../SOURCE_FILES.json | 6 +++--- 4 files changed, 25 insertions(+), 17 deletions(-) diff --git a/reviews/elder_dimension_lift_claude_20260928/REVIEW.md b/reviews/elder_dimension_lift_claude_20260928/REVIEW.md index e5984338e..e2b9fcdc8 100644 --- a/reviews/elder_dimension_lift_claude_20260928/REVIEW.md +++ b/reviews/elder_dimension_lift_claude_20260928/REVIEW.md @@ -145,12 +145,14 @@ The rescaling `x = rX, z = rZ, w = r²W` is the right one. I rederived (A27) ter Heights are `b + r³(F_r(p) + O(r))`, strictly inside the window. The index is `n + 1 = d − 1`, by the same Schur argument as §4. -`SADDLES` checks this in floating point on quartic fields in d = 3, 4 for `r = 1/16 … 1/128`: - -- Both extra critical points exist, with gradient residual below `1e−15`, index d − 1 and heights in `(b − kr³, b)`. - They are distinct from each other and from the pins. -- `|w/r² − W*|/r` stays within a factor 2 across the range, so the stable correction is `O(r)`. Scaling `w` by `r` - instead of `r²` is rejected. +`SADDLES` illustrates this in floating point on quartic fields in d = 3, 4 for `r = 1/16 … 1/128`. It is a numerical +illustration only: existence and the `O(r)` estimate come from the uniform inverse-function argument above, not from +the solver or finite samples. + +- Newton finds two numerical roots of the full gradient near `(rP_±, r²W*)`, with gradient residual below `1e−15`, + index d − 1 and heights in `(b − kr³, b)`. They are distinct from each other and from the pins. +- `|w/r² − W*|/r` stays within a factor 2 across the range. This is consistent with the `O(r)` estimate proved + analytically above; finite samples do not establish it. Scaling `w` by `r` instead of `r²` is rejected. - At the planar restriction's critical point, `∂_w f̃/r²` is nonzero. This confirms the manuscript's warning (line 365) that a planar critical point is not a full critical point. diff --git a/reviews/elder_dimension_lift_claude_20260928/SOURCE_FILES.json b/reviews/elder_dimension_lift_claude_20260928/SOURCE_FILES.json index f5a8f9024..4fce098c6 100644 --- a/reviews/elder_dimension_lift_claude_20260928/SOURCE_FILES.json +++ b/reviews/elder_dimension_lift_claude_20260928/SOURCE_FILES.json @@ -17,9 +17,9 @@ "files": [ { "path": "REVIEW.md", - "bytes": 16746, - "sha256": "a937a36813faff5afb9b6ed135cb838d14dde8ddfbdbc7e6ad37534a2b5c9c62", - "git_blob": "e5984338eb48cd496d3e9b6c0ddc9322dcc1465b" + "bytes": 17030, + "sha256": "032bb4c79e4a985e5b53f5abb6bb06da4d643ec7345e4df9591e2046fb287e12", + "git_blob": "e2b9fcdc8d24f6a4d532afb7d02627e4716158d1" }, { "path": "RESULTS.json", diff --git a/reviews/remote_pair_law_claude_20260928/REVIEW.md b/reviews/remote_pair_law_claude_20260928/REVIEW.md index 5c4d30ca3..d45accbbc 100644 --- a/reviews/remote_pair_law_claude_20260928/REVIEW.md +++ b/reviews/remote_pair_law_claude_20260928/REVIEW.md @@ -11,7 +11,7 @@ separate act. | Object | OA-WINDOW-MULTIPLICITY-REMOTE-20260928-v1 (OpenAI / ChatGPT) | | Branch / head | `chatgpt/window-multiplicity-laws-20260928` / `0507e3a1dbd3dede84cbeb805947c70aa16ebc36` ([Math-#116](https://github.com/d6g8k5htny-coder/Math-/pull/116)) | | `REMOTE_PAIR_LAW.md` | Git blob `3fb602040b37158b16ba61bdfc62cc8df1ccc616`, 15878 B, SHA256 `b818a11f1abcf37616d592ecda6341b0d99365cf3ac5047bc2dbaede95da4c5e`, 325 lines | -| Consumed, on main | [RC] `frontiers/remote_collision_20260928/PROOF.md` (blob `7b48a88e…`): (3.1), (4.1)–(4.3), Lemmas 1, 2, 3, 5. [RM] `frontiers/remote_window_20260924/PROOF.md` (blob `b383bfcc…`): contact frame, (8), §4. The D1 normalizer `Z_r/r² → z_0` (reconciled in Math-#126, merged at `8224783`). | +| Consumed, on main | [RC] `frontiers/remote_collision_20260928/PROOF.md` (blob `7b48a88e…`): (3.1), (4.1)–(4.3), Lemmas 1, 2, 3, 5. [RM] `frontiers/remote_window_20260924/PROOF.md` (blob `b383bfcc…`): contact frame, (8), the §4 deterministic endpoint identities, and its full endpoint-only normalizer `Z_r/r² → z_0` (the same limit as D1 (I), reconciled in Math-#126, merged at `8224783`). | | Request | [Owner comment 5880152796](https://github.com/d6g8k5htny-coder/Math-/pull/116#issuecomment-5880152796); claimed in [5880826796](https://github.com/d6g8k5htny-coder/Math-/pull/116#issuecomment-5880826796) | ## Provenance and exposure @@ -78,8 +78,13 @@ In a frame beginning with `e`, conjugate by `diag(δ^{−1/2}, I)`: Congruence preserves inertia and multiplies determinants by `δ^{−1}`. `F_j` is continuous everywhere, including on singular matrices: it is `|det|` times an index indicator, and `|det| → 0` at the index boundaries. Polynomial moments then give (R8) in `L^p`. The limit product `(T²/4)(det A)²χ_ij` has index `a+1` at `x` and `a` at `x'` when `T > 0`, -which is (R2). The normalizer `W_r/r² → w_0` and `Z_r/r² → z_0` are the D1 normalizer (I), read with the congruence -erratum `D_r = diag(r^{−1/2}, I)`. +which is (R2). + +The weight and normalizer limits have two separate sources. `Z_r` is [RM]'s full endpoint-only normalizer, so +`Z_r/r² → z_0` is unconditioned; it is the same limit as D1 (I). The weight limit `W_r/r² → w_0` is needed *under the +additional pair conditioning* on `V_δ`. It follows from C3 §3's coupled conditional moment bounds together with +[RM] §4's deterministic endpoint identities, which use the congruence `D_r = diag(r^{−1/2}, I)`. The unconditioned D1 +normalizer limit alone would not establish this extra-conditioned weight limit. Exact checks (`PAIR`) use the explicit field `f(u,v) = (T/6)u³ − (T/4)δu² + ½vᵀAv + (u² − δu)c·v` in d = 2, 3, 4: @@ -155,8 +160,9 @@ index-`(a+1)` point lies above its adjacent partner. The gap is Beta(2/3, 2), an C3 claims otherwise. The coefficient should be read as "`k^{5/3}` times a `k`-dependent Gaussian conditional integral". - **N2.** The fixed exclusion `ρ` is load-bearing. [RC] Lemma 1's floor is not uniform as `ρ → 0` ([RC] §8). - LOCAL_MULTIPLICITY shows that pairs near the pins have order `r³`. §7's exclusions are therefore required, not - cosmetic. + Near the pins, the integrated planar LOCAL_MULTIPLICITY result gives an `r³` lower obstruction for the probability + of multiple occurrences (and a factorial *lower* bound). It does not establish an all-dimensional or global exact + `r³` factorial asymptotic. §7's exclusions are therefore required, not cosmetic. - **N3.** A factorial-moment asymptotic does not give `Q(N ≥ 2) ~ (r⁵/2)∫ΣK` without higher factorial moments. §7 says so, and this review adds nothing there. - **N4.** Novelty boundary: generic adjacent-index attraction of critical points in the unconditioned isotropic diff --git a/reviews/remote_pair_law_claude_20260928/SOURCE_FILES.json b/reviews/remote_pair_law_claude_20260928/SOURCE_FILES.json index 61bcc9c1e..05948195f 100644 --- a/reviews/remote_pair_law_claude_20260928/SOURCE_FILES.json +++ b/reviews/remote_pair_law_claude_20260928/SOURCE_FILES.json @@ -17,9 +17,9 @@ "files": [ { "path": "REVIEW.md", - "bytes": 11936, - "sha256": "c6837a64e5883ed102f346de9f38425d34a813081396cf96aab8434ee0e6fa1d", - "git_blob": "5c4d30ca33a4c5eb66cfe211f72d460b7433003c" + "bytes": 12618, + "sha256": "b08f1cdca8e179d9910be89e37e4a03a864b8c1cbcbc6e71cd1fdc359d2a391f", + "git_blob": "d45accbbc92756c24e7eada96ddd0bea0a703c22" }, { "path": "RESULTS.json",