diff --git a/experiments/universality/README.md b/experiments/universality/README.md index 07af7d823..641b7e4fb 100644 --- a/experiments/universality/README.md +++ b/experiments/universality/README.md @@ -21,9 +21,28 @@ bound and gives a local jet coefficient functional. Its finite-r Hessian bridge and deterministic degeneracy falsifier identify a physical-chart hypothesis that exact pins alone cannot supply. These are conventional analytic inputs; the [review record](finite_gaussian_contact/REVIEW.md) preserves their exact scope. -Marked counting, actual bar selection, further residual ranks, critical formal -alignment and numerical coupling remain admission obligations. The sampler and -catalogue admissibility labels retain their original meaning. +The [candidate lifetime theorem](finite_candidate_lifetime/PROOF.md) composes +these inputs with a coefficient-space Sard and all-Borel area-formula argument. +For each fixed positive full-grid ideal Gaussian law at integer cutoff at least +2, it proves a finite continuous density for ordered positive-gap maximum–saddle +candidates, with leading law `C_loc * ell^(-1/3)` and cumulative law +`(3/2) * C_loc * t^(2/3)`. The coefficient is the stated local jet functional; +it is positive and field-dependent. This covers the twenty fixed Gaussian +profile/cutoff cases, without counting them as independent experiments. +The [candidate review](finite_candidate_lifetime/REVIEW.md) binds its argument, +classical imports and exact scope. Candidate pairs need not be persistence pairs. + +The [rescaled fold-chart proof](finite_fold_chart/PROOF.md) supplies explicit +normalizers, a common chart radius, inverse and derivative bounds, and transport +to the same physical field under stated deterministic derivative and transverse +windows. The [chart review](finite_fold_chart/REVIEW.md) preserves the source +interface limits. Physical radii still shrink at contact; window probabilities, +window removal and literal C210/Lean source alignment remain open. + +Actual bar selection, counting with that selection, global once-counting and +complement control, further residual ranks, critical formal alignment and +numerical coupling remain admission obligations. The sampler and catalogue +admissibility labels retain their original meaning. `models.py` defines the implemented finite-cutoff normalized sampler. Only cutoffs 2 and 3 are supported: at cutoff 1, Gaussian and separable spectra diff --git a/experiments/universality/finite_candidate_lifetime/PROOF.md b/experiments/universality/finite_candidate_lifetime/PROOF.md new file mode 100644 index 000000000..a27a84150 --- /dev/null +++ b/experiments/universality/finite_candidate_lifetime/PROOF.md @@ -0,0 +1,577 @@ +# Finite Gaussian candidate-pair lifetime theorem — research preparation + +Prepared on 8 October 2026 by OpenAI/Codex `/root/universality_review`, +in task `01a11cbf-068d-7102-861e-75814e715c98`, at the coordinator's request; +incorporated by `/root` in a separate source proposal after merged PR319. +This is a conventional mathematical argument about candidate pairs. It is not +a scientific-status register, a formal Lean proof, a numerical confirmation, +or a promotion of any catalogue model. No compiler state, sample or seed was +changed or consumed in preparing or incorporating this argument. + +The preparation author was the source-exposed nonauthor reviewer and a +mathematical-input contributor to the analytic source below. Its author was +`/root`. `/root/benchmark_formal_audit` independently attacked the candidate +counting route, primary Kac–Rice hypotheses, genericity, weighted-type +continuity and near/far ledger before this file was written. That contributor +also authored the catalogue implementation. These roles are not blind or +organizationally independent; organizational-independence credit is zero. +Neither that route discussion nor the preparation author's own checks are +an exact-hash nonauthor review of this file. The [review record](REVIEW.md) +binds the separate saved-preparation and incorporated-source reviews. + +## 1. Frozen sources and precisely named external imports + +The principal consumed analytic source is +[finite Gaussian contact proof](../finite_gaussian_contact/PROOF.md): **25,367 UTF-8 bytes**, SHA-256 +**`7fea2656e11d986e1a5d6bfb0a05c8421bd93262d28051b8cfef05320595f474`**. +Its full content was read and its byte identity independently reproduced. +Call this source **FG**. References to its sections below are to these exact +bytes; this preparation does not amend FG. + +The implementation identities read with FG are models.py, 12,385 bytes, +SHA-256 `7ba088158b5e97ba6e7d715e66e6f9d14268ac3a82a6d187a776821936cc6686`, +and models.json, 12,914 bytes, +SHA-256 `10d334b27cac985d61506b4f26118699cd1689a82a0f6e454cef8d00df21e595`. +They identify the intended spectral formulas and distinguish the ideal law +from the retained floating profile and finite-word sampler. The mathematical +law in Section 2, rather than a PRNG implementation, is the input here. + +FG consumes parent **P**, [UNIFORM_MATRIX_CAP_AND_LIFETIME.md at Math- +13af1089fd7991105a3d8828539bdd9a41ca87c3](https://github.com/d6g8k5htny-coder/Math-/blob/13af1089fd7991105a3d8828539bdd9a41ca87c3/imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md): +40,261 bytes, blob `dfed3b8d318a3ab1950957f393307733a4bef3f2`, SHA-256 +`9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7`. +The complete P source was read and its local byte identity checked. +Read its normalizer argument with [E1](https://github.com/d6g8k5htny-coder/Math-/blob/13af1089fd7991105a3d8828539bdd9a41ca87c3/imports/lifetime_parent_20260925/ERRATUM_CONGRUENCE.md): +1,782 bytes, blob `213594d6ca6a86fb938110f4d166d9ce275a02d0`, SHA-256 +`bad7ef609c4ad8c41ad6af562c1b6807921e19a9d556ed793ad1a0db6e202028`. +E1 was completely read and its bytes checked. The [D1 reconciliation](https://github.com/d6g8k5htny-coder/Math-/blob/13af1089fd7991105a3d8828539bdd9a41ca87c3/reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md) +supplies the complete parent reading rule, including E2 and W1/embedding. + +The independent conventional Kac–Rice route was checked against: + +* **AAL:** Diego Armentano, Jean-Marc Azaïs and José Rafael León, + [*On a general Kac-Rice formula for the measure of a level set*, + arXiv:2304.07424v3, 5 December 2023](https://arxiv.org/html/2304.07424v3). + Proposition 2.1, Theorems 2.1, 2.2 and 7.1, Remarks 7–8 and the equal-dimension + area-formula proof in Section 5 were read in the primary paper. +* **E2:** [REPAIR.md at the same Math- commit](https://github.com/d6g8k5htny-coder/Math-/blob/13af1089fd7991105a3d8828539bdd9a41ca87c3/reviews/d1_section9_borel_repair_20260925/REPAIR.md), + blob `fe9b9ce4999908bb3814b500ee2d0ceb0c6f704a`, source-record identity + 9,062 bytes/SHA-256 + `845abf9f9c99d672c2a10a887b5a2e7206a3d2de3d876f35f75ff6e2dc13e62f`. + Its complete fetched text was read. Sections 9.1–9.3 give the two-finite-measure + extension from continuous cylinders to Borel marks. Its elder-mark and + cap-selection conclusions are not imported here. + +Two classical external theorem imports are stated explicitly, not silently +replaced by a numerical test or an all-jet Gaussian assumption: + +**Sard, equal dimensions.** For a C-infinity map from an open subset of R^N +to R^N, the set of images of points where its derivative has rank less than N +has N-dimensional Lebesgue measure zero. Use countable chart/localization +covers when the domain is not one bounded Euclidean region. The primary +reference is Arthur Sard, [*The measure of the critical values of differentiable +maps*, Bulletin AMS 48 (1942), 883–890](https://doi.org/10.1090/S0002-9904-1942-07811-6). +The original paper's statement was read through the [University of Edinburgh +hosted primary-paper copy](https://webhomes.maths.ed.ac.uk/~v1ranick/papers/sard.pdf). + +**Weighted area formula, equal dimensions.** If Phi is locally Lipschitz from +an open subset U of R^N to R^N, and h is nonnegative Borel, then + + integral_U h(z) |det D Phi(z)| dz + = integral_R^N sum_{z in U : Phi(z)=xi} h(z) dxi. (AF) + +The equality is an extended nonnegative integral; no prior finiteness of the +root count is assumed. Localize to countably many bounded subsets if needed. +This is the equal-dimension weighted area formula of Herbert Federer, +*Geometric Measure Theory*, Section 3.2.3, originally 1969; [publisher edition +and identity](https://link.springer.com/book/10.1007/978-3-642-62010-2). +AAL Section 5 independently exhibits the area-formula counting mechanism. +The theorem (AF) is a named classical import; the incidence-map application +and its determinant calculation are proved below. + +Read-status precision: the publisher's Federer metadata was inspected, not +the complete licensed book or a new proof of (AF). A single attempt to open +the AMS-hosted Sard PDF returned `Internal Error`; it was not retried. The +primary-paper copy above supplied the displayed classical statement. There +is no claim of a new verification of the entire classical literature. + +## 2. Exact field, observable and theorem + +Fix an integer K>=2, L>0 and omega=2 pi/L. Let + + S_K={-K,...,K}^2, + q_n>0, q_n=q_-n, sum_{n in S_K} q_n=1. + +Choose one member of each nonzero pair {n,-n}. With independent standard real +Gaussians C_0,C_n,S_n, put + + F(x)=sqrt(q_0) C_0 + + sum_pairs sqrt(2q_n) + [C_n cos(omega n.x)+S_n sin(omega n.x)]. (1) + +The torus is X=R^2/(L Z^2), with area V=L^2. The real coefficient vector xi +has dimension N=(2K+1)^2 and standard Gaussian Lebesgue density rho_N. +The field is centered, variance one, stationary and C-infinity. It need not +be rotationally isotropic. Every fixed C^j norm is bounded by C_j ||xi||. + +For I a Borel subset of (0,infinity), define + + N_cand(I)=sum_{p!=q, gradF(p)=gradF(q)=0} + 1{H_p<0} 1{det H_q<0} 1{F(p)-F(q) in I}. (2) + +Here H is the physical two-dimensional Hessian. The first role is a local +maximum; the second is a nondegenerate index-one saddle. Both roles are +ordered. This population includes every such positive-gap pair, without +requiring a persistence pairing or excluding a maximum because it supports +the essential class. Set mu_cand(I)=E N_cand(I)/V. + +**Candidate theorem.** For every fixed law (1), mu_cand has a finite continuous +density nu_cand(ell) on ell>0, and + + nu_cand(ell) ~ C_loc ell^(-1/3), ell decreasing to zero, + 0=2,L,q above. They are the named +inputs consumed here, with short mechanisms recorded to make their scope +auditable: + +**R1 — seven contact rows (FG Sections 2–3).** +(F,F_u,F_uu,F_uuu,F_v,F_uv,F_vv) has positive unconditional covariance in every +orthonormal frame. Its Fourier multiplier is a polynomial of degree at most +three in each original frequency coordinate. If its variance is zero, positivity +of every q_n makes that polynomial zero on the full square grid. At least five +points in each coordinate force polynomial identity, and its distinct +homogeneous terms force every coefficient to vanish. Frame compactness gives +a contact covariance floor. Literal divided-difference coefficient matrices +extend continuously to contact, so that floor persists for every sufficiently +small r, uniformly over basepoints and frames. + +**R2 — original two-site first jets (FG Section 7).** +For every distinct torus pair, + + O_t=(F(p),gradF(p),F(q),gradF(q)) + +has positive covariance. Choose a coordinate in which the torus sites differ, +and let its relative phase be t!=1. Holding the other frequency fixed, a +zero-variance combination has form (a+bj)+(c+dj)t^j. Four consecutive j values +give the invertible confluent Vandermonde determinant t(t-1)^4. Varying the +other frequency then kills the remaining value and transverse-gradient +coefficients. K>=2 suffices. On any fixed compact off-diagonal domain this +six-row covariance and its four-gradient submatrix have uniform floors. +The two endpoint heights conditional on the four gradients have positive +two-dimensional covariance by the Schur complement. + +**R3 — actual conditional law and moments (FG Section 4).** +For any full-row-rank observation matrix R, conditioning R xi=z gives mean +R^T(RR^T)^(-1)z and centered covariance +P=I-R^T(RR^T)^(-1)R. P is an orthogonal projection. Uniform observation +covariance floors give bounded compact-target means and polynomial growth +in arbitrary targets. Finite coefficient expansion gives every fixed-order +field moment. Further scalar regression supplies the independent transverse +residual used in FG; no arbitrary residual jet rank is asserted. + +**R4 — literal contact normalizer (FG Section 5 with E1).** +For M=x-r u/2,S=x+r u/2, exact pins + + F(M)=b, F(S)=b-k r^3, gradF(M)=gradF(S)=0 + +give U_r target v_r=(b-k r^3/2,-k r^2,0,12k,0,0). The original six-pin +observation transform has absolute determinant 12 r^-5. With + + W_r=|det H_M det H_S| 1{H_M<0} 1{det H_S<0}, + Z_r=E_Q W_r, + +one has, uniformly on compact b windows and 0 z_0=36 k^2 E[A_0^2 1{A_0<0}]>0, (6) + +where A_0 is F_vv conditioned on U_0=(b,0,0,12k,0,0). +Endpoint gradient averages give |F_uu(i)|/r,|F_uv(i)|/r<=M_3/2, while the +height pins give F_uu(M)/r -> -6k and F_uu(S)/r -> 6k. The correct congruence +diag(r^-1/2,1) has off-diagonal sqrt(r) beta. The transverse Schur variance, +Gaussian density bound and uniform moments give type convergence and uniform +integrability. This is compact-mark convergence, not a uniform inverse-Z +bound over all marks. + +**R5 — all-mark unnormalized envelope (FG Section 6).** +On one small band 00, original six-pin density at +(b,0,b-ell,0), 00 and s_u^2>0. The centered scalar law A_u|V_u=0 has +E[A_u^2 1{A_u<0}|V_u=0]=s_u^2/2. These factors are continuous in the frame. + +No part of this proof consumes positive covariance of both full two-site +second jets. That stronger fact holds at K>=3 and fails in an axial K2 +example. Neither it nor an arbitrary finite-jet premise is needed here. + +## 4. Sard genericity before any Rice argument + +This step avoids a Morse-to-Rice-to-Morse cycle. At a physical point p, write + + gradF(p)=B(p) xi. + +B(p) has row rank two: positive coordinate-mode weights give positive +gradient variance in every nonzero direction. Cover the torus by coordinate +patches on which some two coefficient columns B_C(p) are invertible. A +finite or countable such cover exists by continuity and the finite set of +possible minors. In each patch split xi=(zeta,eta), with zeta in R^2. +The critical-point equation is equivalent to + + zeta=a(p,eta)=-B_C(p)^(-1) B_D(p) eta. + +The smooth map + + Psi(p,eta)=(a(p,eta),eta) + +has N-dimensional domain and target. Differentiating the constraint at +xi=Psi(p,eta), while taking the physical derivative of gradF at fixed xi, +gives + + D_p a=-B_C(p)^(-1) H_F(p), + |det D Psi|=|det H_F(p)|/|det B_C(p)|. (8) + +If a field has a degenerate critical point in this patch, its coefficient +vector is a critical value of Psi. Sard makes those vectors Lebesgue-null. +A countable patch union is still null, and the coefficient law has Lebesgue +density rho_N. Thus F is Morse almost surely, before any counting formula. + +The critical set is closed in the compact torus. Nondegenerate critical +points are isolated; an infinite critical set would accumulate at a critical +point and contradict local uniqueness. Hence the set is finite. + +The Morse coefficient set is open. Near a Morse coefficient vector, finitely +many implicit-function critical branches persist; outside their chosen +neighborhoods the gradient stays bounded away from zero. Countable local +coefficient neighborhoods therefore make the resulting finite root counts, +with arbitrary Borel location/coefficient marks, Borel. On the null non-Morse +set define a count as zero. No claim about every fixed conditional pin law +has entered this argument. + +## 5. Direct coefficient-space area formula for all Borel pair marks + +Let T=(XxX) minus the torus diagonal and t=(p,q). Define + + G_t=(gradF(p),gradF(q))=R(t) xi. + +R2 implies row rank four on T. On a coordinate patch U in T choose an +invertible four-column minor R_C(t). Split xi=(zeta,eta), zeta in R^4. +Then G_t=0 is equivalent to + + zeta=a(t,eta)=-R_C(t)^(-1) R_D(t) eta, + Phi(t,eta)=(a(t,eta),eta). + +Phi is smooth from UxR^(N-4) to R^N. Its preimages of a fixed coefficient +vector correspond exactly to that field's pair-gradient zeros in U. +At constraints, + + D_t a=-R_C(t)^(-1) D_tG, + D_tG=diag(H_p,H_q), + |det D Phi|=Delta_t/|det R_C(t)|, + Delta_t=|det H_p det H_q|. (9) + +Apply (AF) with rho_N(Phi(t,eta)) times any nonnegative Borel mark w(t,xi) +and a Borel restriction to a chosen subset E of U. Initially allow both sides +to be infinite. It gives + + E sum_{t in E:G_t=0} w(t,xi) + = integral_E integral_R^(N-4) + rho_N(a(t,eta),eta) w(t,(a(t,eta),eta)) + Delta_t / |det R_C(t)| d eta dt. (10) + +Localize in t and eta to apply the locally Lipschitz theorem, then use +nonnegative monotone convergence. A countable Borel partition of T subordinate +to the minor patches avoids counting a pair twice. + +For fixed t, the linear transformation (zeta,eta) -> (G_t,eta) has absolute +Jacobian |det R_C(t)|. Thus + + integral rho_N(a(t,eta),eta) f(a(t,eta),eta) + / |det R_C(t)| d eta + =p_Gt(0) E[f(xi)|G_t=0], (11) + +using the canonical Gaussian regression law. Substituting f=Delta_t w and +combining the patches yields the all-Borel pair Rice identity + + E sum_{t in D:G_t=0} w(t,xi) + =integral_D p_Gt(0) E[Delta_t w(t,xi)|G_t=0] dt. (12) + +The root-count formula was not assumed to establish genericity or finiteness. +On a compact D separated from the diagonal, the four-gradient covariance +floor bounds p_Gt(0), and conditional centered coefficients have covariance +<=I and mean zero. Delta_t is bounded by C||xi||^4. Consequently (12) with +w=1 is finite on D. This derives the local finiteness needed by a separate +E2 two-finite-measure proof; it is not a hidden premise of (10). + +Sard applied also to Phi shows regular pair roots almost surely directly. +The single-point construction in Section 4 already establishes that result +via a Morse field, so neither direction relies on a Rice/genericity cycle. + +The typed mark is + + tau_t=1{H_p<0} 1{det H_q<0}, + W_t=Delta_t tau_t. + +It is Borel, and its type sets are open. In fact W_t, unlike the bare +indicator, is continuous in both Hessians: changing type at a boundary +requires a zero determinant, which kills the jump. It has degree-four +polynomial growth. Equation (12) contains Delta exactly once, not an +additional determinant inserted into the mark. + +## 6. Distinct critical values and the independently checked AAL/E2 route + +R2 makes the two endpoint heights conditional on G_t=0 nondegenerate Gaussian. +Thus the conditional probability of F(p)=F(q) is zero for each distinct t. +Since Delta_t is finite and integrable under that conditional law, (12) with +w=1{F(p)=F(q)} gives expected tie count zero on every compact off-diagonal +domain. Countably exhaust T, for example by torus separation at least 1/j +and finitely many coordinate domains. No two distinct critical points have +equal heights almost surely. This proof uses two-site first jets only. + +For comparison, actual AAL hypotheses hold: G is C-infinity and Gaussian; +Cov(G_t) is positive definite; its density has a compact-domain bound; and + + law(xi|G_t=z)=law(R(t)^T(R(t)R(t)^T)^(-1)z+P_t eta), + P_t=I-R(t)^T(R(t)R(t)^T)^(-1)R(t) + +is continuous in (t,z) through the whole C^j field. These verify the Gaussian +base and conditional requirements. The continuous weighted base can use xi +as a constant extra Gaussian field. Its bounded continuous cylinders generate +Borel(DxR^N); equality of the two finite counting/kernel measures then extends +to the typed and height marks by E2's monotone-class mechanism. +This is an independently checked alternative to Section 5, not an assertion +that AAL's lower-semicontinuity condition covers every arbitrary Borel mark. +E2's global elder event is not used. + +## 7. Height disintegration and an actual density version + +For t=(p,q), let Q^t_(b,s) be continuous Gaussian regression on the six +observations O_t=(F(p),gradF(p),F(q),gradF(q)) at (b,0,s,0). Define + + K_t(b,s)=p_Ot(b,0,s,0) E_Q^t_(b,s) W_t. (13) + +The order of observations may be permuted, and physical gradients rotated +orthogonally, with absolute Jacobian one. The six-row rank makes the Gaussian +height disintegration legitimate. Equation (12), (11) and nonnegative +Tonelli give the expected typed-pair height measure with kernel K_t(b,s). +Push it forward under ell=b-s; ds has absolute Jacobian one. Therefore + + nu_cand(ell)=(1/V) integral_T integral_R + K_(p,q)(b,b-ell) db dp dq, ell>0, (14) + +and mu_cand(I)=integral_I nu_cand(ell) d ell for every positive-lifetime +Borel I. Initially this is a nonnegative density version, possibly infinite; +the next sections prove finiteness, continuity and its asymptotic directly. +No differentiation of a cumulative asymptotic is used. + +For distinct sites, canonical conditional coefficient means and covariance +square roots depend continuously on locations and heights. The continuous +weighted type W and degree-four growth, with finite Gaussian moments, imply +continuity of its conditional expectation. This argument allows singular +conditional Hessian covariance; it does not need full two-site second-jet rank. + +## 8. Near-diagonal ledger and dominated convergence + +Choose the R1/R5 band 00. The height change has absolute Jacobian r^3. +The literal P contact transform and R4 give original-pin density +12 r^-5 pi_r(v_r), v_r=(b-k r^3/2,-k r^2,0,12k,0,0). +The determinant expectation is Z_r. The factors are thus + + (r dr d sigma) (r^3 db dk) (12 r^-5 pi_r) Z_r + =r A_r dr db dk d sigma, + A_r=12 pi_r Z_r/r^2. (15) + +Endpoint roles are ordered. u ranges once over the full circle; no factor +1/2 or normalized-angle convention is introduced. + +At fixed k the pushforward ell=k r^3 has +dr/dell=1/(3k r^2). Formula (15), or equivalently the fixed-ell change +r=(ell/k)^(1/3), gives + + ell^(1/3) nu_near(ell) + =integral_Rx(0,infinity)xS^1 + 1{k>=ell/r_0^3} A_(ell/k)^(1/3)(b,k,u) + /(3k^(2/3)) db dk d sigma. (16) + +For each fixed b,k>0,u, R4 gives A_r -> 12 pi_0(v_0) z_0, and the indicator +in (16) tends to one. R5 supplies the integrable majorant H/(3k^(2/3)). +Dominated convergence gives + + ell^(1/3) nu_near(ell) -> + 4 integral k^(-2/3) pi_0(v_0) z_0 db dk d sigma + =C_loc. (17) + +This conclusion handles all birth heights and all positive k; its proof uses +the unnormalized product pi_r Z_r. There is no global inverse-Z estimate, +no division by k in a conditional probability, and no selection probability. + +Equation (16) bounds nu_near(ell) by C ell^-1/3 for every ell>0. It also proves +continuity for each positive ell: for ell_j -> ell>0, the integrand converges +at every fixed b,k,u except k=ell/r_0^3, a measure-zero boundary. Conditional +kernel continuity from Section 7 and the same H majorant permit dominated +convergence. This yields a particular continuous Radon–Nikodym density. + +## 9. Far contribution, finiteness and the full theorem + +On dist(p,q)>=r_0 the six-pin covariance has a compact-domain floor. +For 00. + +There is also no hidden infinite-total-count premise. For the near population, +integrating (15) over all positive gaps and all b,k is bounded by +integral_0^r0 r dr times integral H db dk d sigma, which is finite. +For the far population, the target (b,s) has Gaussian decay in both heights, +and its conditional determinant moment has degree-four polynomial growth; +the db ds integral is finite. Hence mu_cand((0,infinity)) 0. + +Each C_loc,j is positive; taking a finite minimum also gives uniform relative +leading asymptotics across these twenty cases. There is no asserted uniform +window or constant over arbitrary q approaching the boundary of the positive +weight simplex, over unbounded K, or over variable L. For each fixed positive +q, integer K>=2 and L>0, the theorem holds with its own constants. + +The K1 contact dependence and the K2 second-jet singularity in FG are retained +negative boundaries. The seventh-order axial annihilator at K3 blocks reuse +of P's arbitrary finite-jet premise but does not obstruct this finite list +of ranks. No counterexample to (3) under its stated assumptions was found. + +## 12. Exact remaining scope + +This preparation supplies a complete conventional candidate-count derivation +from the named FG inputs and the stated classical Sard/area imports. There +is no additional unproved model-specific analytic premise in that route. +Independent exact-source review is recorded separately in [REVIEW.md](REVIEW.md); +the earlier review of FG and pre-file route discussions do not substitute +for an incorporated-source review. No formal Lean implementation or kernel +execution is claimed. + +Actual persistence bars require further source-bound elder selection, +global once-counting and the appropriate complement proof. Conditional +all-point genericity for enlarged cap/collision/factorial-moment lists has +not been proved here and is not silently imported. Higher homology and a +process limit remain separate. This theorem also does not certify numerical +sampling/coupling, a usable asymptotic window, blind-field validation, +publication acceptance or external uptake. + +In particular the actual finite-word sampler is not the Gaussian coefficient +law used by Sard/null-set and Gaussian density arguments. The non-Gaussian +coefficient laws are not covered. Exact mathematical weights, actual +conditioning, density versus cumulative normalization, field-dependent +coefficient and per-area versus whole-torus counts must be preserved in any +consumer. Existing catalogue admissibility labels, applicability arrays, +graphs and scientific-status records remain unchanged. diff --git a/experiments/universality/finite_candidate_lifetime/REVIEW.md b/experiments/universality/finite_candidate_lifetime/REVIEW.md new file mode 100644 index 000000000..dd1b2e7c7 --- /dev/null +++ b/experiments/universality/finite_candidate_lifetime/REVIEW.md @@ -0,0 +1,156 @@ +# Candidate lifetime: exact-source technical review + +The [proof](PROOF.md) is a conventional argument about the expected number of +ordered positive-height-gap maximum–saddle candidates for a finite ideal +Gaussian Fourier field. Its theorem covers each fixed strictly positive, +symmetric full-square spectrum at integer cutoff `K>=2` and fixed side `L>0`. +It counts candidates, including candidates that are not persistence pairs. +It does not assign catalogue admission, graph status or scientific acceptance. + +The source/integration owner is OpenAI/Codex `/root`, task +`01a11cbf-068d-7102-861e-75814e715c98`, under the +[five-path claim](https://github.com/d6g8k5htny-coder/main/issues/307#issuecomment-6069189950). +The mathematical preparation author is `/root/universality_review`. +All contributors and technical readers are OpenAI/Codex, source and route +exposed. Organizational-independence credit is **zero**. + +## Exact reviewed objects and preserved predecessor + +The incorporated `PROOF.md` is **29,190 UTF-8 bytes**, SHA-256 +**`ed31f562f0ffaaf6d4bd2ceb1ae3d234798e983a55d55c6983b128fce27133f5`**. +Its preparation predecessor was **29,103 bytes**, SHA-256 +`21cb308f58f011355376057cde04bf9e27194d14054f30677d7f7d2c47574291`, +retained in the owner's external workspace as +`finite-candidate-lifetime-preparation.md`. + +Incorporation changed only the location/status wording, the local link to the +contact source and the pointer to this review. Equations, hypotheses, counting +argument, coefficient and limits were not changed. New-byte reviews are +recorded separately; a predecessor verdict is not rebound to the successor. + +The consumed [contact proof](../finite_gaussian_contact/PROOF.md), merged in +[PR319](https://github.com/d6g8k5htny-coder/main/pull/319), remains **25,367 bytes**, +SHA-256 `7fea2656e11d986e1a5d6bfb0a05c8421bd93262d28051b8cfef05320595f474`. +Root independently checked that identity before and after the unrelated +architecture merge. Its exact mathematics and source limitations remain +those of its [separate review](../finite_gaussian_contact/REVIEW.md). + +## Actual technical reads + +The preparation author checked the complete saved preparation. That is an +author check, not a nonauthor review. Root read the complete preparation and +compared the incorporated changes; root coordinates and incorporates this +proposal, so this check does not supply an independent integration verdict. + +`/root/final_contract_review` fully read and independently hashed both the +29,103-byte preparation and the 29,190-byte incorporated source. Its fresh +verdict is **PASS within the requested mathematical-to-physical scope**, +with no must-fix finding. It checked the ordered candidate population, +per-area and whole-torus units, torus lift/midpoint Jacobian, full-circle +orientation, six-pin and lifetime Jacobians, density/cumulative distinction, +conditional weighted-type continuity, K2 rank sufficiency and the actual +positive symmetric catalogue formulas. It did not reopen the external +primary theorem sources or inspect the underlying Lean imports in that pass. +The full measure-proof review remains a distinct record. + +`/root/benchmark_formal_audit` fully read and independently hashed the +complete preparation and the incorporated source, then isolated their actual +diff. Its separate full-source verdict for each version is **no must-fix +mathematical defect**. It attacked the Sard/Rice ordering, coefficient-space +minor and area determinant, all-Borel marks, tie removal, spatial/height +normalization, continuous conditional weighted type, integrability, density +continuity, limit interchange, coefficient and K2/finite-family extension. +It confirmed that the area identity begins with extended nonnegative measures, +that compact-annulus finiteness is derived afterward, that the determinant +appears exactly once and that no conditional second-jet floor is needed. + +This reader previously contributed candidate-route and matrix checks and +originally authored the catalogue/pilot implementation. It had primary AAL +and complete E2 exposure. Its own single Sard PDF opener failed; it did not +retry or reroute, obtain the complete paper bytes or read the complete Federer +book. Those limitations are separate from the preparation author's indexed +primary-statement read and root's later failed opener. + +The provenance/scope drafts also received a separate full read by +`/root/final_contract_review`. That audit required naming the actual E2 readers +and making indexed Sard statement exposure precise. The corrected draft was +reread; no remaining must-fix attribution, scope or local-link finding was +reported. That earlier draft still showed pending full-source verdicts; the +paragraphs above record the later completed source reviews. + +```text +ATTACK STATUS: counterexample not found +Target: d6g8k5htny-coder/main:experiments/universality/finite_candidate_lifetime/PROOF.md + Git blob a27a84150b3e70bfd794672eeeed6915425a1da4 + SHA256 ed31f562f0ffaaf6d4bd2ceb1ae3d234798e983a55d55c6983b128fce27133f5 +Attempts: genericity/counting cycle -> incidence Sard before Rice -> no cycle; + Borel mark/conditioning -> coefficient area and Gaussian fibers -> valid; + double determinant/orientation -> Jacobian ledger -> counted once; + illegal limit/remainder -> common majorant and far floor -> leading only; + K2 degeneracy -> named rank dependency slice -> second-jet floor unused. +Remaining attack surfaces: actual bar selection/global complement, enlarged +conditioning lists, formal alignment, sampler/coupling, numerical windows, +non-Gaussian laws and higher homology/process limits. +``` + +The publication commit/tree binding is recorded in the integration PR and +completion receipt. The attack record identifies the exact unchanged proof +blob; it is neither a new scientific status nor a claim of blind reconstruction. + +## External imports and source-reading limits + +The main counting argument uses the explicitly stated classical Sard theorem +and equal-dimension weighted area formula. The incidence-map determinant and +its Gaussian conditional disintegration are proved in the source. The area +identity starts with extended nonnegative integrals; compact-domain finiteness +is derived afterward. These named classical imports are mathematical +dependencies, not new Lean proofs or unidentified Gaussian jet assumptions. + +The preparation author read the original Sard introduction/statement as +indexed primary text from the hosted copy; it did not obtain full PDF bytes. +The publisher's Federer metadata was inspected; nobody +claims a complete read or new verification of the licensed book. The source +records the preparation author's failed AMS PDF attempt separately. +Root's later single attempt to open the hosted Sard copy returned +`Internal Error`; root did not retry or reroute that attempt and does not +claim that the earlier successful primary-paper read was its own. + +The primary Armentano–Azais–Leon v3 paper was read for the Gaussian base, +weighted continuous-cylinder hypotheses and area-formula mechanism. Root +also inspected Theorems 2.1, 2.2 and 7.1 and the relevant Section 5 argument. +This corroborates the separately explained alternative Rice route. It does +not make a Borel indicator lower semicontinuous by assertion. + +The full pinned E2 repair was read by `/root/universality_review` and +`/root/benchmark_formal_audit`; root separately fetched and read all **9,062 bytes**, blob +`fe9b9ce4999908bb3814b500ee2d0ceb0c6f704a`, and reproduced SHA-256 +`845abf9f9c99d672c2a10a887b5a2e7206a3d2de3d876f35f75ff6e2dc13e62f`. +Only its finite-measure/Borel extension mechanism is corroboration here; +its global elder event and parent cap estimates are not consumed. + +## Evidence actually supplied and remaining predicates + +The conventional proof establishes Morse genericity before counting, +all-Borel pair counting at gradient level zero, distinct critical heights, +height disintegration, a finite continuous lifetime density, near/far +domination, the leading exponent and the local jet coefficient. The +twenty fixed Gaussian profile/cutoff cases form a finite mathematical family; +they are not twenty independent observations or fifty continuum admissions. + +The density asymptotic is `nu(ell)~C_loc*ell^(-1/3)`; the cumulative law is +`(3/2)*C_loc*t^(2/3)`. A bounded remainder is not claimed. The coefficient is +positive and field-dependent, with ordinary circle arclength of mass `2*pi`. +Expected whole-torus counts multiply the per-area coefficient by `L^2`. + +No Lean implementation, kernel run, formal statement-alignment review, +certified coefficient digits, sampler coupling, held-out draw, blind slope +confirmation or numerical continuum window was performed for this increment. +The finite-word sampler and all non-Gaussian laws remain outside this theorem. +Actual persistence selection, global unique counting and complement control, +enlarged conditioning lists, higher homology and a marked-process limit remain. + +**Dylan Roy — delegated AI review:** actual executors and scopes are the +OpenAI/Codex readers identified above. Dylan's personal reading is **PENDING**, +an optional retrospective reading aid rather than an authorization checkpoint. +Neither delegation, a positive technical verdict nor hosted CI supplies +provider-distinct, human, formal or scientific acceptance. diff --git a/experiments/universality/finite_fold_chart/PROOF.md b/experiments/universality/finite_fold_chart/PROOF.md new file mode 100644 index 000000000..6febb6e69 --- /dev/null +++ b/experiments/universality/finite_fold_chart/PROOF.md @@ -0,0 +1,551 @@ +# Uniform derivative-controlled fold charts: research preparation + +Actual author: OpenAI/Codex, agent `/root/final_contract_review`, coordinated by +`/root`, 8 October 2026. Incorporated by `/root` in a separate source proposal +after merged PR319. This preserves a new analytic derivation; it is not a Lean +proof, scientific acceptance, or admission of a catalogue law to a full +persistence theorem. No existing applicability array, model status, or graph +node is changed by this source proposal. + +Organizational independence of the author and peer checks: zero. The peer +`/root/benchmark_formal_audit` independently checked the matrix branch algebra +and derivative constants within the same agent team before this file was +written. That was a bounded matrix check, not a full saved-file review or +nonauthor acceptance. The [review record](REVIEW.md) separately binds full +saved-preparation and incorporated-source reviews. + +## Source exposure and preservation boundary + +The final proved C210 source block was consumed from an earlier successful +read of [Math#193 comment 6066554517](https://github.com/d6g8k5htny-coder/Math-/issues/193#issuecomment-6066554517). +Its handoff-relative path is `lean-project/SourceCoordinates.lean`: 8,161 +UTF-8 bytes, 160 lines, SHA256 +`b92d2936525bd120f41badb2bd9018714546d986b6ced9c4326bee9e0b1939da`. +The already cached block was independently rehashed in this audit. No new +C210 fetch, owner-checkout read, or compiler execution was performed. The +source exposes `source_coordinates`, its actual physical `hdet` and +actual-source `hcrit` premises, the same-field Taylor constructor, and the +generic `theta`, congruence, and local-coordinate proof. It does not expose +the complete underlying `MorseCongruence` or `TaylorSymLift` implementation. + +The literal parent P was read from the local scratch copy +`finite-contact-parent-source.md`: 40,261 bytes, SHA256 +`9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7`, +Git blob `dfed3b8d318a3ab1950957f393307733a4bef3f2`, pinned at +[Math-@13af1089fd7991105a3d8828539bdd9a41ca87c3](https://github.com/d6g8k5htny-coder/Math-/blob/13af1089fd7991105a3d8828539bdd9a41ca87c3/imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md). +This derivation consumes its literal finite height/gradient pins and scalar +endpoint identities, not its candidate global selection or persistence +conclusions. The correct scaled Hessian below is derived directly by the +chain rule. It does not copy P's erroneous `diag(sqrt(r),I)` wording. + +The previously reviewed PR319 [finite Gaussian contact proof](../finite_gaussian_contact/PROOF.md) was 25,367 +bytes, SHA256 +`7fea2656e11d986e1a5d6bfb0a05c8421bd93262d28051b8cfef05320595f474`. +That proof is frozen and unchanged by this preparation. Its final section +contains the simpler finite-r determinant bridge, quintic falsifier, and +canonical shrinking-radius example. This file is the next proposed analytic +increment and is outside that merged proposal. + +No deterministic sample bounds are inferred from uniform Gaussian moments. +The derivative windows below are explicit assumptions on the actual pinned +field realization. No probability estimate for these windows is claimed. + +## Theorem and exact assumptions + +Work in an actual orthonormal physical frame `(u,v)` about a midpoint `x_*`. +Let `Q=(-1,1)^2`, and let `f` be the actual ideal finite Fourier field, or any +`C^4` field, on a neighborhood of the embedded physical box + + x_* + R D_r Q, + R=(u v), D_r=diag(r,r^(3/2)). + +For a torus field, this is an embedded local coordinate box. The supplied +frame is part of the parameter data; no rotational invariance of the field +law or global eigenvector choice is assumed. All norms below are Euclidean +vector norms, corresponding matrix operator norms, and full Frechet +derivative operator norms, except where the symmetric-matrix Frobenius norm +is explicitly specified. + +Assume `00, + A_M=f_vv(M). + +On the physical box suppose + + ||D^3 f||<=D_3, ||D^4 f||<=D_4, + +where `D_3,D_4` are fixed finite nonnegative bounds on all derivatives of +the stated orders. These are not silently identified with unspecified +partial-block cap norms. Require + + r D_3<=a_0/2, + r D_4<=kappa_-, + r D_3^2<=a_0 kappa_-. (A) + +Define the actual rescaled field and its critical points by + + Fhat_r(X,Y)=[f(x_*+R D_r(X,Y))-b]/r^3, + q_M=(-1/2,0), q_S=(1/2,0). + +Define constants depending only on the fixed windows: + + c_0=sqrt(kappa_-/a_0), + p=(1+c_0) max{sqrt(8/(21 kappa_-)), 2/sqrt(a_0)}, + Lambda=(sqrt(2)/6) p^3 D_3, + N_2=(sqrt(2)/12) p^4 D_4, + rho=min{1/(4p), 1/[16(1+Lambda)]}>0, (B) + K_2=4 Lambda+rho(6 Lambda^2+2 N_2). + +For each endpoint `i` there is an explicit real linear isomorphism `Phat_i` +and a `C^2` diffeomorphism + + e_i:B_rho(0) -> e_i(B_rho(0)) + +such that, with `J_M=-I` and `J_S=diag(1,-1)`, + + Phat_i^T Hess Fhat_r(q_i) Phat_i=2 J_i, + ||Phat_i||<=p, + e_i(0)=0, De_i(0)=I, + Fhat_r(q_i+Phat_i y) + =Fhat_r(q_i)+e_i(y)^T J_i e_i(y), (C) + B_(rho/2)(0) is contained in e_i(B_rho(0)). (D) + +The following bounds hold uniformly over actual field realizations, radii, +birth heights, gap marks, midpoints and supplied frames satisfying the +assumptions: + + ||De_i-I||<1/4, + ||D(e_i^-1)||<=4/3, + ||D^2 e_i||<=K_2, + ||D^2(e_i^-1)||<=64 K_2/27. (E) + +The inverse bounds hold throughout the image, and in particular on the +common target ball `B_(rho/2)`. This is a deterministic local theorem on +explicit derivative-controlled windows. It asserts neither a window +probability nor global pairing. + +## 1. Uniform regularity of the actual rescaled field + +For `r<=1`, `||D_r||=r`. The chain rule gives + + ||D^3 Fhat_r||<=r^-3 ||D_r||^3 D_3=D_3, + ||D^4 Fhat_r||<=r^-3 ||D_r||^4 D_4=r D_4<=D_4. + +Thus the rescaling loses no derivative in these estimates. Lower derivative +bounds follow from the exact critical pin and endpoint Hessian bounds. A +valid bound on the Hessian throughout `Q` is + + B_2=(13/2) kappa_+ +a_1+a_0/2+3D_3. + +Indeed the endpoint Hessian estimate established in Section 2 is at most +`(13/2)kappa_+ +D_3+a_1+a_0/2`, and every point of `Q` is at Euclidean +distance less than two from `q_M`. Integrating the third derivative bound +along that segment adds at most `2D_3`. Since +`Fhat_r(q_M)=0` and `D Fhat_r(q_M)=0`, another integration gives + + ||D Fhat_r||<=2B_2, |Fhat_r|<=2B_2. + +Consequently its full `C^4` norm, defined as the maximum of derivative +suprema through order four, is at most `max{2B_2,D_3,D_4}`. All segments used +here remain in the convex box. These are bounds on the actual finite-pinned +field, with no contact constraints imposed at finite `r`. + +## 2. Explicit endpoint normalizers and their bounds + +Write the physical Hessians in the supplied frame as + + H_i=[[r alpha_i,r beta_i],[r beta_i,A_i]], + alpha_i=f_uu(i)/r, beta_i=f_uv(i)/r, A_i=f_vv(i). + +The scalar pin identities give + + |alpha_M+6kappa|, |alpha_S-6kappa|<=rD_4/2, + |beta_i|<=D_3/2, + |A_S-A_M|<=rD_3. + +The average of `f_uv` on the pin interval is zero, since both transverse +gradients are zero. Subtracting this average from an endpoint value and +integrating the derivative Lipschitz bound gives `|f_uv(i)|<=rD_3/2`. +The analogous axial average and the height identity give the displayed +axial estimates. The third-derivative weighted mean is the finite pin +identity equal to `12kappa`, not a substituted midpoint condition. + +The rescaled endpoint Hessian is exactly + + Hhat_i=D_r^T H_i D_r/r^3 + =[[alpha_i,C_i],[C_i,A_i]], + C_i=sqrt(r) beta_i. + +Put `B_i=-A_i` and `tau_i=alpha_i+C_i^2/B_i`. Conditions (A) imply + + a_0/2<=B_i<=a_1+a_0/2, + tau_M<=-(21/4)kappa, + tau_S>=(11/2)kappa, + |tau_i|<=7kappa_+. + +For the maximum, the positive mixed-square correction is at most +`rD_3^2/(4a_0)<=kappa_-/4`; its axial error is at most `kappa_-/2`. +For the saddle the correction is nonnegative and at most +`rD_3^2/(2a_0)<=kappa_-/2`. These observations prove all the stated pivot +bounds. In particular both physical endpoint determinants are nonzero, +the maximum is negative definite, and the saddle has one positive and one +negative eigenvalue. + +Define + + T_i=[[1,0],[-C_i/B_i,1]], + Hhat_i=T_i^T diag(tau_i,-B_i) T_i, + Phat_i=T_i^-1 diag(sqrt(2/|tau_i|),sqrt(2/B_i)). + +This proves `Phat_i^T Hhat_i Phat_i=2J_i`. Moreover + + |C_i/B_i|<=sqrt(r)D_3/a_0<=c_0, + +so `||T_i||,||T_i^-1||<=1+c_0` and the bound `||Phat_i||<=p` in (B) +follows. There is also a uniform inverse bound + + ||Phat_i^-1||<= + (1+c_0) max{sqrt(7kappa_+/2), + sqrt((a_1+a_0/2)/2)}. (F) + +In particular `||Hhat_i^-1||<=p^2/2`, so the rescaled endpoint Hessians +have a uniform spectral gap. The normalizer uses actual scalar pivots in +the supplied frame and requires no eigenvector selection or field-law +orientation invariance. + +## 3. The actual integral Taylor matrix + +Fix an endpoint and abbreviate `Phat_i=P`, `J_i=J`. Define + + M(y)=integral_0^1 (1-t) + P^T Hess Fhat_r(q_i+tPy) P dt. + +Since `p rho<=1/4`, all the integration segments for `|y|<=rho` stay inside +`Q`: the critical points have boundary distance `1/2`. Exact criticality +and Taylor's integral formula give + + Fhat_r(q_i+Py)-Fhat_r(q_i)=y^T M(y)y. (G) + +Also `M(0)=P^T Hhat_i P/2=J`. The matrix field is `C^2` because the actual +field is `C^4`. For the symmetric-matrix Frobenius norm, + + ||DM(y)||<=sqrt(2) p^3 D_3 integral_0^1 (1-t)t dt + =Lambda, + ||D^2M(y)||<=sqrt(2) p^4 D_4 integral_0^1 (1-t)t^2 dt + =N_2. + +The factor `sqrt(2)` converts a two-dimensional symmetric bilinear-form +operator bound to Frobenius norm. The two integrals are `1/6` and `1/12`. +Consequently + + ||M(y)-J||_F<=Lambda |y|<1/16 for |y|<=rho. (H) + +No assumption `DM(0)=0` is used. + +## 4. Explicit congruence compatible with the theta structure + +For `J=diag(sigma,-1)`, `sigma` either `-1` or `1`, and symmetric `M` with +`||M-J||_F<=1/8`, define + + Z=JM, + s_0=sqrt(det Z), + t_0=sqrt(tr Z+2s_0), + R_theta(M)=(Z+s_0 I)/t_0. (I) + +The symbol `R_theta` is a new explicit analytic branch in this preparation; +it is not an identification with the particular branch selected by the +existing C210 implementation. On the stated neighborhood, + + 3/4<=det Z<=41/32, + +so both square roots and the denominator are positive and the formula is +smooth. Cayley-Hamilton gives + + (Z+s_0 I)^2=(tr Z+2s_0)Z, + R_theta(M)^2=Z. + +Since `Z^T J=JZ`, the same identity holds for the polynomial expression +`R_theta`; hence + + R_theta(M)^T J R_theta(M)=J R_theta(M)^2=JZ=M. (J) + +At `M=J`, `R_theta(J)=I`. Define + + s_theta(M)=J(R_theta(M)-I). + +Then `s_theta(M)` is symmetric, `s_theta(J)=0`, and + + R_theta(M)=I+J s_theta(M), + M-J=2s_theta(M)+s_theta(M)J s_theta(M). + +For symmetric Frobenius inputs and output operator norm, safe explicit +bounds are + + ||DR_theta(M)||<=2, + ||D^2R_theta(M)||<=6. (K) + +Here are the scalar estimates proving them. On this neighborhood, + + s_0>=3/4, s_0<=8/7, t_0>=7/4, + ||Z||op<=9/8, + |D det Z|<=8/5, |D^2 det Z|<=1, + |Ds_0|<=16/15, |D^2s_0|<=9/4, + |Dt_0|<=21/20, |D^2t_0|<=2, + ||Z+s_0 I||op<=127/56, + ||D(Z+s_0 I)||op<=31/15. + +For example the first determinant derivative is bounded by +`||adj Z||_F=||Z||_F<=sqrt(2)+1/8<8/5`. Its second derivative is the +two-by-two determinant bilinear form, of norm at most one. Differentiating +the two scalar square roots yields + + |D^2s_0|<=1474/675<9/4, + |Dt_0|<=109/105<21/20, + |D^2t_0|<=146749/77175<2. + +The first and second quotient derivatives in (I), using these inequalities, +are bounded respectively by + + 2879/1470<2, + 43878/8575<6. + +Thus (K) follows without a sampled matrix calculation. + +For comparison an upper-triangular LDL branch is also explicit. Write + + M=[[a,b],[b,c]], d=c-b^2/a, + R_LDL(M)=[[sqrt(sigma a),sigma b/sqrt(sigma a)], + [0,sqrt(-d)]]. + +On the same neighborhood `sigma a>=7/8` and `-d>=6/7`. Direct multiplication +gives `R_LDL^T J R_LDL=M` and `R_LDL(J)=I`. Its safe bounds are + + ||DR_LDL||<=1, ||D^2R_LDL||<=4. + +For the first bound, on a symmetric perturbation +`E=[[alpha,beta],[beta,gamma]]`, the absolute output-entry derivatives are +bounded by the following matrix acting on +`(|alpha|,sqrt(2)|beta|,|gamma|)`: + + [[4/7,0,0], + [32/343,6/7,0], + [1/84,1/8,7/12]]. + +Its maximum row sum is `326/343` and maximum column sum is `55/56`, both +below one, so its Euclidean operator norm is below one. For the second +bound, let `s=sqrt(sigma a)`, `w=sigma b/s`, `z=-c+b^2/a`, `q=sqrt(z)`. +For unit symmetric-Frobenius perturbations, direct differentiation gives +`|D^2s|<1/2`, `|D^2w|<2`, `|Dz|<=3/2`, `|D^2z|<=2`, and hence +`|D^2q|<=7/6+3087/3456<3`. The output Frobenius norm is therefore at most +`sqrt((1/2)^2+2^2+3^2)<4`. The theorem uses (I), since that branch also +has the symmetric `s_theta` and literal structural form `I+Js_theta`. + +## 5. Chart, common inverse ball, and C2 estimates + +Define + + e(y)=R_theta(M(y))y. + +Equations (G) and (J) prove the exact energy identity (C). At the origin, +`e(0)=0` and `De(0)=I`, since `M(0)=J` and the derivative of the matrix +factor is multiplied by `y=0`. + +Integrating (K) from `J` to `M(y)` and using (H) gives + + ||R_theta(M(y))-I||<=2Lambda |y|. + +Differentiating the product yields + + ||De(y)-I||<=4Lambda |y| + <=4Lambda rho<1/4. (L) + +The radius choice in (B) makes the last inequality strict. Therefore +`e-I` is Lipschitz with constant `q<1/4` on the convex ball, and + + (3/4)|y-z|<=|e(y)-e(z)|<=(5/4)|y-z|. + +In particular `e` is injective. For `|v| v-(e(y)-y) + +on the closed radius-rho ball. It maps that ball into the radius-`3rho/4` +ball and has contraction constant below `1/4`. It has a unique fixed point +with + + |y|<=(4/3)|v|<2rho/3. + +This proves the common inverse-image ball (D). The derivative bound (L) +makes every derivative invertible. The inverse function theorem therefore +makes `e(B_rho)` open and its inverse `C^2` throughout that image. The +injectivity above identifies the local inverse charts with one inverse. + +A second differentiation of the product gives + + ||D^2e||<=4Lambda+rho(6Lambda^2+2N_2)=K_2. + +The first and second derivatives of `e(e^-1(v))=v` then give + + ||D(e^-1)||<=4/3, + ||D^2(e^-1)||<=(4/3)^3 K_2. + +This proves all estimates in (E). Neither nonsingular pin covariance nor +Gaussian moment bounds are substituted for these deterministic estimates. + +## 6. Parameter regularity and the contact caution + +The explicit endpoint normalizer, integral Taylor matrix, and branch (I) +are continuous functions of the actual rescaled field in `C^4`, of endpoint +data, and of the supplied frame. The pivot signs are fixed by (A), so there +is no branch change. On the common target ball `B_(rho/2)`, continuity of +the inverse follows from the uniform contraction bound; its first and +second derivative formulas then give continuity in `C^2`. + +Precisely, a family whose actual rescaled fields and other input data vary +continuously in the stated norms has continuous parameter dependence of +these spatial `C^2` charts and inverses on the common domains. If the +corresponding data have stronger joint smoothness, the explicit formulas +and parameter inverse function theorem give the corresponding local joint +smoothness. This is an implication from actual input regularity, not a new +axiom about the field coupling. + +Uniform spatial `C^2` bounds plus continuous parameter dependence do not +imply joint `C^2` dependence in `r` through `r=0`. The rescaled Hessian has +mixed entry `sqrt(r) beta_i`, and anisotropic rescaling can introduce that +regularity obstruction. The theorem is stated for `r>0`. A contact extension +in a parameter such as `tau=sqrt(r)` requires proof of the appropriate +joint regularity of the actual field family; changing the parameter alone +does not prove that assumption. No such extension is asserted here. + +Uniform Gaussian `C^q` moments also do not imply deterministic uniform +sample bounds `D_3,D_4`. This theorem applies on the derivative-controlled +window specified in its assumptions; probabilistic window removal remains +separate work. + +## 7. Exact transport to the same physical field + +Define + + P_i_phys=r^(-3/2) R D_r Phat_i, + E_i(u)=r^(3/2) e_i(u/r^(3/2)). + +The physical Hessian in fixed coordinates is transported by the supplied +frame `R`, so + + P_i_phys^T Hess_phys f(x_i) P_i_phys=2J_i. + +Using (C) and the degree-two homogeneity of the quadratic form gives + + f(x_i+P_i_phys u) + =f(x_i)+E_i(u)^T J_i E_i(u) (M) + +on `B_(rho r^(3/2))`. Its image contains +`B_(rho r^(3/2)/2)`, and the inverse energy identity holds there. This uses +the actual endpoint value `f(x_i)`, which is `b-kappa r^3` at the saddle, +not a substituted common birth value. + +The bounds transport exactly: + + DE_i(0)=I, ||DE_i-I||<1/4, + ||D^2E_i||<=r^(-3/2)K_2, + ||D(E_i^-1)||<=4/3, + ||D^2(E_i^-1)||<=r^(-3/2)(64/27)K_2, + ||P_i_phys||<=p r^(-1/2). + +The physical source is the actual field on the ellipsoid +`x_i + R D_r Phat_i B_rho`, with axial scale `r` and transverse scale `r^(3/2)`. +The uniform inverse bound (F) supplies a corresponding inner rescaled +ellipsoid. These are chosen height-window scales, not a claim about every +maximal physical Morse domain. + +For the same integral Taylor construction, + + M_i_phys(u)=M_i_rescaled(u/r^(3/2)). + +This follows by inserting `P_i_phys` in the physical integral Taylor +matrix and applying the Hessian chain rule; the factor `r^-3` cancels the +rescaled height factor. Therefore (M) has the exact structural expression + + E_i(u)=[I+J_i s_theta(M_i_phys(u))]u. + +No new realization, coefficient vector, unrelated function, or renamed +source is introduced by this transport. + +## 8. Structural theta compatibility and literal branch limits + +The construction has the algebraic structure of the cached +`SourceCoordinates.theta` definition. It does not establish equality to +the particular branch, local inverse, or domains selected by the existing +`MorseCongruence` proof or the returned C210 witness. + +There is a useful analytic local uniqueness statement. If symmetric `s,t` +solve the same equation + + M-J=2s+sJs=2t+tJt, + +then, writing `d=s-t`, + + 2d+dJs+tJd=0, + 2||d||<= (||s||+||t||)||d||. + +Thus `s=t` whenever `||s||+||t||<2`. Our explicit branch is small. An +existing continuous branch with value zero at `J` therefore matches it +on some sufficiently small common neighborhood. That observation does +not reveal or quantify the existing branch's actual neighborhood or the +chosen inverse source. It supplies no bound for the radius returned by +C210. Equality to that literal chosen witness and its domains remains a +formal alignment obligation. + +For the explicit preparation branch, one can regard `s_theta` as a function +on the open Frobenius ball about `J`, or extend it as a total symmetric +matrix-valued function outside that neighborhood. Only its smoothness and +identities on that open ball are used. Such an extension changes none of +the chart or energy statements on the proved source. + +## 9. Formal API consumption and remaining boundaries + +The actually exposed reusable lemma names are + +- `SourceCoordinates.quadratic_congruence`; +- `SourceCoordinates.apply_hasFDerivAt_zero`; +- `TaylorSymLift.sourceSymMatrix_quadratic`. + +A strengthened congruence-chart constructor must add the explicit radius, +contraction and inverse bounds above to the generic local-coordinate +construction. To consume the actual I4 source, it also needs: + +1. Exact finite source-mode encoding and equality to the physical finite + field, with the actual period, frame and coefficient conventions. +2. Physical derivative/Hessian identification for that same source and the + exact critical pins. +3. A verified equality between `TaylorSymLift.sourceSymMatrix` and the + integral Taylor matrix used in this preparation, or derivative bounds + derived from its exposed actual definition. +4. The quantitative chart constructor, with the explicit chosen branch and + proved source/target domains. Identification with a pre-existing chosen + C210 branch or inverse must be proved if that identification is used. + +Finite support supplies summability after the exact source-mode encoding +is provided. `TaylorSymLift.sourceSymMatrix_quadratic` then supplies the +actual-source energy identity. `SourceCoordinates.exists_coordinates` +already gives existential local coordinates, but its current exposed +statement does not provide the quantitative radius proved here. + +No underlying formal implementation was fetched for this preparation, and +no Lean application or theorem compiling these new bounds was executed. +The result remains an analytic proof with named formal alignment work. + +The exact-contact physical Hessian is still singular. The theorem constructs +uniform charts after rescaling at the two finite-r critical points; it does +not construct an ordinary Morse chart at the degenerate contact itself. +It also supplies no marked Kac-Rice/Borel count, window-tail removal, +determinant-weighted selection, global once-counted bar identity, complement +bound, blind confirmation, coefficient enclosure, or scientific admission. diff --git a/experiments/universality/finite_fold_chart/REVIEW.md b/experiments/universality/finite_fold_chart/REVIEW.md new file mode 100644 index 000000000..2b3f9a81a --- /dev/null +++ b/experiments/universality/finite_fold_chart/REVIEW.md @@ -0,0 +1,156 @@ +# Rescaled fold charts: exact-source technical review + +The [proof](PROOF.md) is a deterministic quantitative theorem about the same +actual `C^4` field at a pinned maximum/saddle separation. Its derivative and +transverse windows are explicit hypotheses. It gives a common radius after +rescaling, a `C^2` coordinate map and inverse, and exact transport to the +physical field. It does not claim deterministic caps for every Gaussian +realization or removal of the supplied windows. + +The source/integration owner is OpenAI/Codex `/root`, task +`01a11cbf-068d-7102-861e-75814e715c98`, under the +[five-path claim](https://github.com/d6g8k5htny-coder/main/issues/307#issuecomment-6069189950). +The mathematical preparation author is `/root/final_contract_review`. +All contributors and technical readers are OpenAI/Codex, source and route +exposed. Organizational-independence credit is **zero**. + +## Exact reviewed objects and preserved predecessor + +The incorporated `PROOF.md` is **21,678 UTF-8 bytes**, SHA-256 +**`8b0ab87e9516857c1e92483bf9e39c8664af4fa76f72c6a54c4eb729f763fdba`**. +Its preparation predecessor was **21,594 bytes**, SHA-256 +`fc74f92dd81764acf0b54eb44e656028ea6456720d1c5a08c36830aaa66d2684`, +retained in the owner's external workspace as `finite-fold-chart-preparation.md`. + +Incorporation changed location/status wording, local source/review links and +the descriptive physical ellipsoid to show its center `x_i` explicitly. +The preceding same-field energy identity already fixed that center. The +hypotheses, constants, branch construction and proof are otherwise unchanged. +New-byte reviews are recorded separately; a predecessor verdict is not +rebound to the successor. + +The consumed [contact proof](../finite_gaussian_contact/PROOF.md), merged in +[PR319](https://github.com/d6g8k5htny-coder/main/pull/319), remains **25,367 bytes**, +SHA-256 `7fea2656e11d986e1a5d6bfb0a05c8421bd93262d28051b8cfef05320595f474`. +Root independently rechecked that identity after the unrelated architecture +merge. This proposal does not amend that proof or its historical review. + +## Actual technical reads + +The preparation author checked the complete saved preparation. That is an +author check. Before the file was written, `/root/benchmark_formal_audit` +contributed an independent matrix-branch/derivative-constant check. That +pre-file contribution is not represented as a full saved-source review. + +The same reader subsequently read and hashed the complete **21,594-byte** +preparation. It found no must-fix mathematical defect within its stated +deterministic assumptions. It checked the actual-field rescaling, lower-order +`C^4` bounds, explicit endpoint pivots and normalizers, Taylor/Frobenius bounds, +both matrix branches, contraction, common inverse ball, derivative constants +and exact same-field physical transport. It separately recomputed the +displayed rational quotient bounds with exact fractions. + +The reviewer suggested explicitly centering the descriptive physical +ellipsoid. It classified that omission as optional clarification, because +the actual energy identity already fixed the center. The incorporated source +includes it. The old preparation and its verdict remain preserved. + +`/root/final_contract_review` freshly read and independently hashed the +21,678-byte incorporated fold source and compared the actual predecessor +diff. It confirmed the explicit center and retained constants, assumptions, +parameter and formal boundaries. Because it authored the fold derivation, +this is an author successor check rather than a nonauthor verdict. + +`/root/benchmark_formal_audit` freshly read and independently hashed the +complete 21,678-byte incorporated source and isolated its actual predecessor +diff. Its new-source verdict is **no must-fix mathematical defect**. It +rechecked the actual rescaling and full caps, endpoint pivots/normalizers, +Taylor bounds, theta branch, common radius, contraction, inverse estimates, +parameter cautions and same-field physical transport. This is a fresh +successor verdict rather than a transfer from the preparation review. + +`/root/universality_review` separately read and hashed the complete incorporated +source. Its full-source verdict is **PASS for the bounded analytic theorem**, +with no critical, important or minor mathematical correction requested. It +checked the endpoint estimates and normalizers, both congruence/rational +bound mechanisms, contraction and inverse derivative estimates, parameter +continuity on common domains and exact physical transport. It also reread the +cached C210 main block. It did not inspect the complete underlying imports +or execute Lean. It authored the candidate preparation and reviewed the +contact proof, giving substantial route/source exposure; it is not the fold +proof's author. + +The companion draft and README received a separate provenance/scope read by +`/root/final_contract_review`. Its requested clarification now distinguishes +the Hessian-normalized `u` radius and `E_i` derivative bounds from the actual +physical ellipsoid's axial/transverse scales. The corrected draft was reread; +no remaining must-fix attribution, scope or local-link finding was reported. +That earlier draft still showed pending nonauthor verdicts; the paragraphs +above record the later completed source reviews. + +```text +ATTACK STATUS: counterexample not found +Target: d6g8k5htny-coder/main:experiments/universality/finite_fold_chart/PROOF.md + Git blob 6febb6e697a700b96d7e46a09f0bdfd725450376 + SHA256 8b0ab87e9516857c1e92483bf9e39c8664af4fa76f72c6a54c4eb729f763fdba +Attempts: deterministic caps -> actual rescaling/chain rule -> sufficient windows; + indefinite factor/sign -> explicit congruence and pivots -> valid; + local map/image gap -> common-ball contraction -> inverse exists; + physical substitution -> exact same-field Taylor/energy transport -> valid; + contact regularity/API overreach -> stated parameter/source limits -> retained. +Remaining attack surfaces: window probabilities/removal, selected-bar global +geometry, actual C210 witness/domain alignment and quantitative Lean constructor. +``` + +The publication commit/tree binding is recorded in the integration PR and +completion receipt. The attack record identifies the exact unchanged proof +blob; it is neither a new scientific status nor a claim of blind reconstruction. + +## Formal source exposure and precise interface boundary + +The author consumed the cached final proved C210 block from +[Math#193 comment6066554517](https://github.com/d6g8k5htny-coder/Math-/issues/193#issuecomment-6066554517): +`lean-project/SourceCoordinates.lean`, **8,161 UTF-8 bytes**, 160 lines, +SHA-256 `b92d2936525bd120f41badb2bd9018714546d986b6ced9c4326bee9e0b1939da`. +It independently rehashed that cached block. There was no fresh owner-checkout +fetch or compiler execution. The complete underlying `MorseCongruence` and +`TaylorSymLift` implementations were not exposed by that block. + +The theorem's explicit analytic branch has the structural form `I+J*s_theta` +with symmetric `s_theta`. The source proves local uniqueness in the stated +small ball. These facts do not identify the particular witness, returned +radius or domains chosen by the unseen C210 implementation. Actual finite +source encoding, physical derivative identification, literal Taylor-constructor +equality and a source-bound quantitative Lean construction remain work to do. + +## Evidence actually supplied and remaining predicates + +The hypotheses give a uniform rescaled `C^4` cap for the actual field and +nonzero endpoint Hessian determinants. The proof constructs endpoint +normalizers without choosing eigenvectors, gives a common positive radius, +and proves spatial `C^2` bounds and a common inverse ball by contraction. +It preserves all correlations by operating on the actual realization. + +In Hessian-normalized physical coordinates `u`, the source radius scales as +`r^(3/2)` and the second derivatives of `E_i` scale as `r^(-3/2)`. The actual +physical ellipsoid has axial scale `r` and transverse scale `r^(3/2)`. Ordinary physical Morse charts therefore +retain the shrinking-domain boundary as contact becomes degenerate. The +theorem gives neither a uniform physical radius through contact nor an +ordinary Morse chart at the exact zero-determinant contact point. + +Continuous parameter dependence assumes continuity of the actual rescaled +input family on the stated common domains. Spatial `C^2` estimates do not +imply joint `C^2` dependence in separation `r` through zero. Replacing `r` +with its square root does not itself prove that missing input regularity. + +No probability estimate for the supplied windows, window-removal argument, +global pairing/counting, lifetime process limit, new Lean implementation, +kernel execution, formal statement-alignment acceptance, numerical coupling, +held-out draw or blind confirmation is claimed. Existing catalogue labels, +applicability arrays and scientific-status records are not edited. + +**Dylan Roy — delegated AI review:** actual executors and scopes are the +OpenAI/Codex readers identified above. Dylan's personal reading is **PENDING**, +an optional retrospective reading aid rather than an authorization checkpoint. +Neither delegation, a positive technical verdict nor hosted CI supplies +provider-distinct, human, formal or scientific acceptance.