diff --git a/experiments/universality/README.md b/experiments/universality/README.md index b4ad40d51..424fb82fd 100644 --- a/experiments/universality/README.md +++ b/experiments/universality/README.md @@ -57,10 +57,34 @@ or gap, and do not support an unrestricted covariance floor. Its [review](finite_contact_genericity/REVIEW.md) records the exact argument and classical Sard import. Finite-r additional conditioning is a separate contract. -Actual bar selection, counting with that selection, global once-counting and -complement control, further conditional ranks, critical formal alignment and -numerical coupling remain admission obligations. The sampler and catalogue -admissibility labels retain their original meaning. +The [elder-transfer proof](finite_elder_transfer/PROOF.md) now supplies the +local-to-global topological step for the actual pinned field. Under its isolated +cubic contact limit, the nearby maximum component is enclosed above the saddle +and the saddle connects it to an older component. Compactness and the global +critical-point gaps exclude a bypass. Canonical Gaussian coupling and polynomial +domination make this the actual elder pair with determinant-weighted probability +tending to one, uniformly over compact birth/gap marks for the fixed law. Its +[review](finite_elder_transfer/REVIEW.md) records the bounded classical imports, +exact source chain and review exposure. + +The [finite H0 lifetime theorem](finite_h0_lifetime/PROOF.md) constructs a Borel +selector and counts every actual finite superlevel H0 bar exactly once. For each +fixed positive full-square ideal Gaussian law at cutoff at least 2, it proves a +finite nonnegative Borel density with leading law `C_loc * ell^(-1/3)` for its +specified canonical representative, and the intrinsic cumulative law +`(3/2) * C_loc * t^(2/3)`. The coefficient equals the candidate local jet +functional. The essential global-maximum class is excluded. The selected density +is not asserted continuous; missed near pairs contribute only `o(ell^(-1/3))`, +while the far contribution is bounded. Its +[review](finite_h0_lifetime/REVIEW.md) binds the measurable once-counting argument, +all-mark limit and precise finite Gaussian scope. + +These conventional analytic results discharge selected-bar counting and the +leading near/far intensity composition for those ideal Gaussian laws. Further +conditional ranks, literal critical formal alignment, certified sampler and +numerical/count coupling, genuinely blind law-by-law admission, higher homology +and marked point-process convergence remain separate 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_elder_transfer/PROOF.md b/experiments/universality/finite_elder_transfer/PROOF.md new file mode 100644 index 000000000..69f84eae4 --- /dev/null +++ b/experiments/universality/finite_elder_transfer/PROOF.md @@ -0,0 +1,458 @@ +# Isolated cubic contact to an actual finite H0 elder bar — conventional analytic source + +Prepared on 8 October 2026 by OpenAI/Codex `/root/benchmark_formal_audit`, +at `/root`'s request. The source and 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-6070045125). +This conventional analytic source incorporates the frozen external preparation +`finite-contact-elder-transfer-preparation.md`, 21,138 UTF-8 bytes / 418 lines, +SHA256 `1cac9b525831b7e1f37f0d0561d3231fa73c8713c4c92283dca1d5b51b8a67ce`. +Its mathematical text in Sections 2–13 is unchanged. Source-location, +consumed-source and review chronology are updated here and bound separately +in the [review record](REVIEW.md). + +The original author implemented the catalogue machinery and contributed to +the earlier contact, candidate and chart arguments. This is a source-exposed +same-team derivation, with organizational-independence credit zero. Root fully +read the original preparation; `/root/final_contract_review` freshly read and +hashed that entire original file and returned PASS with no mathematical +must-fix. Those reads bind the original preparation. Any new exact-file nonauthor +verdict must bind this incorporated source's actual new bytes and is recorded +separately in the companion. Publication, hosted checks, native review and +integration evidence are likewise separately bound when obtained. No human, +blind or provider-distinct review is claimed. + +The result below proves a deterministic selected-pair theorem and its +normalized determinant-weighted probability consequence. Its argument proves +local isolation, enclosure, an older connection and the actual saddle merger +for the specified pair. Global counting/converse obligations remain separate. +No old proof, applicability label or scientific-status record is changed. +This source is not a Lean proof, sampler certificate or numerical experiment. +No compiler, sampler or seed is used in this incorporation. + +## 1. Consumed sources and primary classical imports + +FG is [the frozen finite Gaussian contact proof](../finite_gaussian_contact/PROOF.md), +25,367 UTF-8 bytes / 554 lines, SHA256 +`7fea2656e11d986e1a5d6bfb0a05c8421bd93262d28051b8cfef05320595f474`. +Its actual source was completely read earlier, its row contract and coupling +revisited, and its current repository identity independently reproduced. +We consume its ideal Gaussian law, literal divided differences/target, +covariance floor, projector coupling, endpoint identities, compact moment +bounds and contact normalizer limit. A global selected-bar result is not +imported from FG. The original preparation recorded its earlier exposure at +`finite-gaussian-successors-worktree/experiments/universality/finite_gaussian_contact/PROOF.md`; +that is historical local-location provenance, not an operational source path +for this incorporated record. The relative repository link above identifies +the current consumed copy at the same exact hash. + +CG is [the incorporated contact-conditioned genericity proof](../finite_contact_genericity/PROOF.md), +23,431 UTF-8 bytes / 473 lines, SHA256 +`233e80421ccf78e9a9015116aaaf2d355a8425107ff109c022ddc98cd1f87fd9`, +Git blob `569a49dee2ec1b517cc231869aade4f6322f562f`. +The present author also authored CG's external predecessor and freshly reread +all 473 lines of this actual incorporated source before writing this successor; +its identity was independently reproduced. That is an author input check. +Root and `/root/final_contract_review` separately completed full reads of this +incorporated CG source at the above exact identity. Their actual review scopes +are in [CG's companion](../finite_contact_genericity/REVIEW.md). +It proves, for each fixed six-contact-pin law, isolated contact and all other +critical points Morse, with finitely many pairwise distinct values different +from b. Its K2 rank defects are handled by nonzero affine means, not arbitrary +jets. We consume that analytic result without calling it formally or +scientifically admitted. The deterministic theorem below explicitly states +what it needs. + +The original preparation instead bound CG's external predecessor +`finite-contact-global-genericity-preparation.md`, 23,103 UTF-8 bytes / 468 lines, +SHA256 `a06ec513ce4b83bdeb1e600787a0acfcf9bb20a217ab6009bb326df8c8fd6fe5`. +It truthfully recorded that CG peer review was pending when that preparation +was written. Those historical bytes remain frozen. CG's preparation and +incorporated-source reviews subsequently completed; their actual scopes and +identities are recorded separately in CG's companion. This successor consumes +the freshly reread incorporated proof above, without rebinding an earlier +verdict to new bytes. + +The same independently rehashed implementation identities remain +[models.py](../models.py), 12,385 bytes, SHA256 +`7ba088158b5e97ba6e7d715e66e6f9d14268ac3a82a6d187a776821936cc6686`, +and [models.json](../models.json), 12,914 bytes, SHA256 +`10d334b27cac985d61506b4f26118699cd1689a82a0f6e454cef8d00df21e595`. +They identify intended formulas, not an ideal-law sampler certification. + +The following bounded primary-read paragraphs preserve the original author's +exposure from the frozen preparation. No fresh primary-source fetch was +performed for this incorporation. + +Two primary sources were successfully opened and their relevant statements +read for this preparation: + +* J. Milnor, *Morse Theory*, Princeton University Press,1963, + [primary-book PDF hosted by Edinburgh](https://www.maths.ed.ac.uk/~v1ranick/papers/milnmors.pdf). + Lemma 2.2 (printed page6), Theorems 3.1–3.2 (printed pages12 and14), and + the critical-level remark following 3.3 (printed page20) were inspected + in Sections 2–3; the no-critical-level gradient-flow proof was also read. + These correspond to zero-based PDF pages5,8–9 and12 in the opened copy. + We import the smooth Morse local normal form, + homotopy equivalence of compact critical-point-free level bands, and + attachment of one index-sized cell at an isolated nondegenerate critical + level. Apply these to -f for superlevels. The actual finite Fourier fields + are smooth; only their convergence is required in C4. +* H. Edelsbrunner, D. Letscher and A. Zomorodian, *Topological Persistence and + Simplification*, Discrete & Computational Geometry 28 (2002),511–533, + [primary-paper PDF hosted by Chicago](https://www.math.uchicago.edu/~shmuel/AAT-readings/Data%20Analysis%20/Edelsbrunner-Letscher-Zomordian.pdf). + Section 4, printed page523 (zero-based PDF page12), including its component + representation and union operation, was read. Its merger pairing retains + the older representative and + pairs the merger with the younger representative. This is the H0 elder + convention. Section 8 below also gives the elementary basis justification + for the actual component merger established here. + +This is exposure to those specified statements through parsed primary PDFs, +not a claim to have read their complete texts or reproduced raw PDF byte +hashes. The isolation/enclosure and conditional transfer below are proved +here. No unstated global selection or generic birth-death theorem is imported. + +## 2. Deterministic theorem, including varying parameters + +Let X be a fixed square flat torus of side L. Consider smooth functions +f_j,f_0 on X such that f_j->f_0 in global C4. Let r_j>0 tend to 0 and suppose + + x_j -> x_0, + (u_j,v_j) -> (u_0,v_0) in O(2), + b_j -> b_0, k_j -> k_0>0. + +Assume the exact finite pins + + M_j=x_j-r_j u_j/2, S_j=x_j+r_j u_j/2, + f_j(M_j)=b_j, f_j(S_j)=d_j=b_j-k_j r_j^3, + grad f_j(M_j)=grad f_j(S_j)=0. (1) + +Assume the actual limit contact has the physical derivative data + + (f_0,D_u f_0,D_u^2 f_0,D_u^3 f_0,D_v f_0,D_u D_v f_0)(x_0) + =(b_0,0,0,12k_0,0,0), + A_0=D_v^2 f_0(x_0)<0, (2) + +in the limit frame. Assume its critical set is finite, every other critical +point is Morse, and their critical values are pairwise distinct and different +from b_0. CG supplies these conditions almost surely under its contact law; +here they are deterministic hypotheses. + +For all sufficiently large j, f_j is Morse with distinct critical values. +Its only critical points in a fixed-size neighborhood of contact are the +exact M_j,S_j, respectively a maximum and an index 1 saddle. The component +born at M_j stays enclosed until d_j. There it merges through S_j with a +component having birth height>b_j. Thus (M_j,S_j) is the actual finite H0 +superlevel elder pair, of exact lifetime k_j r_j^3. + +For a fixed-parameter family f_r->f_0, the sequence theorem implies the result +for every sufficiently small r: a contrary failing sequence contradicts it. +The threshold can depend on the whole realization, its transverse pivot, +derivative modulus and global critical height/gradient gaps. A deterministic +ensemble-wide threshold is not asserted. + +## 3. Actual transverse reduction + +In the local charts put + + g_j(s,t)=f_j(x_j+u_j s+v_j t). + +On one fixed embedded rectangle Q=[-delta,delta]x[-tau,tau], these converge +in C4 to g_0. This is a local chart operation, not rotational invariance of +the square-torus law. A_0<0 allows a small rectangle and a>0 such that + + g_0,tt<=-2a, eventually g_j,tt<=-a on Q. (3) + +Subscript commas below denote partial derivatives. The transverse implicit +function theorem gives h_0 with g_0,t(s,h_0(s))=0, h_0(0)=h_0'(0)=0. +Shrink delta until |h_0|h_0 in C3. + +Define the actual reduced ridge functions + + phi_j(s)=g_j(s,h_j(s)), phi_j'=g_j,s(s,h_j(s)). (4) + +Their third derivatives converge uniformly. The contact pins give + + phi_0(0)=b_0, phi_0'(0)=phi_0''(0)=0, + phi_0'''(0)=12k_0. + +For the last identity, h_0'(0)=0 and g_0,st(0,0)=0 kill the additional +mixed and h_0'' terms. Shrinking again gives c>0 with + + phi_0'''>=2c, eventually phi_j'''>=c>0. (5) + +This derivative sign, rather than convergence alone, controls new critical +points near the degenerate contact. + +## 4. Exactly two local critical points and their types + +The exact pins and transverse uniqueness imply h_j(±r_j/2)=0 and +phi_j'(±r_j/2)=0. By (5), p_j=phi_j' is strictly convex. With those two +zeros it is negative between them and positive outside them in the interval. +Strict monotonicity of secant slopes proves the outside signs as well as +excluding a third zero. Further, p_j'(-r_j/2)<0 and p_j'(r_j/2)>0; +integration of p_j''>=c bounds both magnitudes below by c r_j/2. + +At a ridge critical point the actual Hessian Schur pivot is + + phi_j''=g_j,ss-g_j,st^2/g_j,tt. (6) + +Since g_j,tt<0, the left negative pivot makes the Hessian negative definite; +the right positive pivot makes it index 1. Any critical point in Q must be +on the transverse ridge and a zero of phi_j'. Thus M_j,S_j are all the +local critical points, with the required actual types. + +The limit reduced derivative has a double zero at0 and positive second +derivative. It is positive elsewhere locally. Hence phi_0 is strictly +increasing and, with s_+=delta/2, + + phi_0(-delta)0 and large j, [b_j-eta,b_j+eta] contains only M_j,S_j, and +all other critical heights remain mutually distinct and distinct from them. +The imported Morse level-band/attachment facts now give a finite constructible +superlevel H0 filtration. No finite-r conditional genericity theorem has been +assumed for this conclusion. + +## 6. Exact enclosure of the newborn component + +Let Q_j^-=[-delta,r_j/2]x[-tau,tau] in the local chart. Its left boundary +has g_j<=phi_j(-delta), below b_j by a fixed gap from (7). On its right, + + g_j(r_j/2,t)<=phi_j(r_j/2)=d_j, + +with equality only at t=0. Transverse concavity gives + + g_j(s,t)<=phi_j(s)-(a/2)[t-h_j(s)]^2. + +On s<=r_j/2 the reduced signs imply phi_j<=b_j. Since |h_j|=c}. (8) + +Its s projection is one closed interval around the maximum: phi_j increases +to b_j from the left and decreases to d_j on the right. Each vertical fiber +is one interval containing the ridge. A point joins vertically to the ridge, +and the connecting ridge segment stays above c; thus C_j(c) is path connected. +It is nonempty and avoids the rectangle boundary. Its global superlevel +intersection is open and closed in X_c={f_j>=c}, because the boundary misses +X_c. So it is an actual global component. An exterior route cannot join +it to an older component before d_j. + +At c=b_j this region contains only M_j, and at c>b_j it is empty. The +component is actually born at b_j and contains no higher-birth maximum. +This proves enclosure for the actual component, rather than for a restricted +local candidate picture. + +## 7. The other saddle branch is older + +The fixed limit point p_+=x_0+u_0 s_++v_0 h_0(s_+) has f_0(p_+)>b_0. +A small fixed ball about it has values strictly above b_0. For large j its +f_j values are strictly above b_j, and the moving ridge endpoint + + p_j^+=x_j+u_j s_++v_j h_j(s_+) + +lies in that ball. The ridge from S_j to p_j^+ has phi_j>=d_j, increasing +strictly after S. It continues within the high ball to fixed p_+. Thus the +actual right branch reaches a point with height>b_j. + +For c in(d_j,b_j) its component differs from the enclosed component(8). +At c=d_j the complete ridge from M_j through S_j to p_j^+ lies in the +closed superlevel: it decreases from b_j to d_j then increases. This joins +the two actual components through S_j. The newborn component first meets +the exterior there; the other three rectangle sides remain below d_j. + +The nonsingular saddle is the only critical point at that height. Its local +Morse form has two upper sectors, belonging to the two different components +just proved. Its index 1 attachment therefore merges them, instead of making +a loop inside one component. The component on the right was born at height +at least f_j(p_+)>b_j and is strictly older for descending superlevels. + +## 8. Actual finite elder bar and endpoint convention + +H0 over any field has one generator per component. At the merger the two +generators map to the same generator. Since the older component already +exists at b_j, replace the new generator by its difference from a continued +older generator. This difference is born at b_j, survives on(d_j,b_j], +and becomes 0 at d_j, while the older generator survives. This is the +component-level elementary basis proof of the elder convention and identifies +the actual finite bar killed by S_j. + +With increasing parameter t=-c and closed superlevels {f_j>=c}, its interval +is[-b_j,-d_j); in height coordinates it is(d_j,b_j]. Its exact lifetime is + + ell_j=b_j-d_j=k_j r_j^3. (9) + +The older component may represent several earlier mergers but still has birth +above b_j. The newborn maximum is not the essential global maximum. No +planar global arrangement or isotropy assumption was used. + +## 9. Canonical coupling gives the deterministic inputs + +For the ideal finite Gaussian law let L_r(theta) be FG's coefficient matrix +of the actual six divided differences U_r, with theta=(x,u,v,b,k) and + + v_r=(b-k r^3/2,-k r^2,0,12k,0,0). + +For one theoretical standard Gaussian Z in R^N define + + m_r=L_r^T(L_r L_r^T)^(-1)v_r, + P_r=I-L_r^T(L_r L_r^T)^(-1)L_r, + xi_r=m_r+P_r Z. (10) + +This is the canonical Q_r conditional law: P_r is an orthogonal projection +and gives the correct residual covariance. For r>0 the invertible original- +pin/divided-difference map proves the exact six physical pins (1), not an +approximate contact target at finite r. + +FG extends L_r continuously to the six-contact-pin matrix L_0 and supplies a uniform +small-r covariance floor across basepoints and frames. Therefore m_r,P_r +converge to their contact versions. The finite expansion gives + + F_(r,theta)(Z)->F_(0,theta)(Z) in global C4 (11) + +for every finite Z, continuously also as theta varies through a compact +mark/basepoint/frame domain. No actual draw of Z is executed here. + +CG gives global contact genericity for each fixed theta almost surely. On +A_0=F_0,vv(x)<0, every hypothesis of Section 2 holds. Consequently almost +every such coupled Z gives the exact elder pair for every sufficiently +small r. This also proves those F_r are globally Morse with distinct heights. +It does not assume a separate static finite-r all-point conditional rank list. + +For any specified deterministic theta_j->theta_0 and r_j->0, the local chart +fields, moving pins and global fields satisfy Section 2 by (11). Its conclusion +holds eventually on the good contact/A_0<0 set for that fixed limit theta_0. +A probability-one event for an uncountable collection of targets is unnecessary. + +## 10. Measurability of the selected event + +Let E_r mean F_r is globally Morse with distinct critical values and the +distinguished M,S form the finite H0 elder pair. On all other coefficients +set its indicator to 0. This avoids assuming finite-r genericity in advance. +The event is Borel. The Morse/distinct-value coefficient set is open by finite +critical-branch persistence and the compact noncritical gradient gap. On a +local such neighborhood choose finitely many regular thresholds between the +ordered critical heights. + +Small coefficient perturbations keep every threshold regular. A parametric +level-flow aligns all these surfaces at once: take disjoint narrow bands +about them and a vector field equal there to minus the parameter derivative +of the function times its gradient divided by the squared gradient norm, +with smooth cutoffs elsewhere. Its parameter flow preserves the aligned +superlevel sets and their component inclusion maps. This is the level-flow +construction of Milnor's critical-point-free band proof with a parameter. +The finite component incidences, hence labelled elder pairing, are constant +on the neighborhood. Countable coefficient charts make E_r Borel. The +distinguished exact pins keep their critical-branch labels there. + +## 11. Normalized determinant-weighted transfer at fixed marks + +For the actual physical Hessians under Q_r let + + W_r=|det H_M| |det H_S| 1{H_M<0}1{det H_S<0}, + V_r=W_r/r^2, z_r=E_Z V_r, + Q_r^W(E)=E_Z[V_r 1_E]/z_r. (12) + +Scaling by r^2 does not alter this normalized probability. The observation +pin density cancels in the ratio; this is not an unweighted probability claim. +FG's endpoint identities and (11) give almost surely + + V_r->V_0=36k^2 A_0^2 1{A_0<0}. (13) + +The scalar A_0 has positive conditional variance, so its zero value is null; +even there the limit weight is 0. Uniform compact mark/field coefficient +bounds and the endpoint identities give the integrable envelope + + 0<=V_r<=C(1+||Z||)^4. (14) + +Indeed |det H_i|/r<=C(1+||F_r||C3)^2, while bounded targets and the +observation covariance floor give ||F_r||C3<=C(1+||Z||). These are moment +envelopes, not deterministic caps on all Gaussian realizations. + +On V_0>0, Section 9 makes 1_Er eventually 1. On V_0=0, (13) gives +V_r(1-1_Er)->0 regardless of E_r. Dominated convergence yields + + E_Z[V_r(1-1_Er)]->0, + z_r->z_0=E_Z V_0>0, + Q_r^W(E_r)->1. (15) + +Positivity follows from k>0 and the positive-variance scalar Gaussian's +negative-halfline second moment. No inverse curvature, global inverse +normalizer bound, or division by k in a conditional probability is used. + +## 12. Compact uniformity proved separately + +Fix b in a compact B, k in[k_-,k_+] with k_->0, x in X and (u,v) inO(2). +Fix one positive ideal spectrum/cutoff or a fixed finite collection, such +as the twenty Gaussian catalogue cases at L24,K2/3. FG gives a common +small-r covariance band and (14). The contact normalizer is continuous and +positive, so its minimum on this compact parameter domain is positive. + +Pointwise (15) alone would not establish uniformity. Suppose the supremum of +weighted failure did not tend to 0. Choose r_j->0 and theta_j in the compact +domain with failure>=epsilon>0. Extract theta_j->theta_0 and, in the finite +model collection, a subsequence with the same model and coefficient dimension. +Use the same theoretical Z in (10) for this subsequence. + +Then F_(r_j,theta_j)->F_(0,theta_0) in global C4 for every Z. CG applies at +that one fixed theta_0 almost surely. On V_0(theta_0)>0, Section 2's varying- +parameter theorem makes E_j eventually true; otherwise V_j->0. The common +polynomial Gaussian envelope gives + + E_Z[V_j(1-1_Ej)]->0, z_j->z_0(theta_0)>0, + +contradicting the positive normalized failure bound. Hence + + sup_theta [1-Q_(r,theta)^W(E_(r,theta))]->0. (16) + +This is a qualitative uniform probability limit on the specified compact +set. It supplies no rate, explicit usable r or samplewise common threshold +for an uncountable family. It does not extend to k_->0, unbounded birth +marks, spectral weights approaching a boundary, unbounded cutoff or an +unspecified infinite-field law. + +## 13. Remaining consumers and preservation + +For the named pair the proof gives the local-to-global elder step, exact +finite H0 lifetime and normalized determinant-weighted selection probability +tending to1, including (16). It does not say every short candidate is selected. +An actual full-bar density theorem still needs a source-bound all-Borel +counting application to the elder mark, exact once-counting of finite bars, +and a complete near/far or converse/complement ledger. Those remain separate +consumers. Higher homology, factorial moments, process limits, quantitative +windows and sampler certification also remain separate. + +The sign A_0<0 is essential to this newborn superlevel maximum. A minimum-type +fold with A_0>0 is outside this argument. All statements use the same actual +coupled field, physical derivatives, exact pins and actual endpoint heights. +C210's nonsingular physical-Hessian premise still fails at the contact itself. +No frozen source is amended, no formal owner lane is taken over, and no +scientific promotion is claimed. Exact-source nonauthor review of this new +preparation is separate and must retain the same-team author/contributor roles. diff --git a/experiments/universality/finite_elder_transfer/REVIEW.md b/experiments/universality/finite_elder_transfer/REVIEW.md new file mode 100644 index 000000000..87ff3cd2c --- /dev/null +++ b/experiments/universality/finite_elder_transfer/REVIEW.md @@ -0,0 +1,147 @@ +# Isolated cubic contact to an actual elder bar: exact-source review record + +The [proof](PROOF.md) proves a deterministic local-to-global elder-selection +result for the specified nearby pinned pair, then its normalized +Gaussian determinant-weighted selection limit. It supplies no global bar +counting identity, selected lifetime density, formal kernel execution or +sampler admission by itself. + +The source and 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-6070045125). +The original mathematical author and incorporation performer is +`/root/benchmark_formal_audit`, a prior catalogue implementer and contributor +to the contact, candidate and fold-chart routes. All contributors/readers are +same-provider and source/route exposed. Organizational-independence credit is +**zero**. No personal human, blind or provider-distinct acceptance is claimed. + +## Exact objects and consumed sources + +The incorporated proof is **23,774 UTF-8 bytes / 458 lines**, SHA256 +`c9e4fb09900888cd2b1bd96b49f85072b51c822b2503fe9f3d8891049bf66201`. This companion binds those new bytes; it does not confer a +fresh nonauthor verdict on them. + +The preserved external predecessor is +`finite-contact-elder-transfer-preparation.md`, **21,138 UTF-8 bytes / 418 lines**, +SHA256 `1cac9b525831b7e1f37f0d0561d3231fa73c8713c4c92283dca1d5b51b8a67ce`. +The actual text of Sections 2–13 is byte-unchanged. Incorporation changes only +title/provenance, source locations, consumed CG identity and review chronology +in the introductory material. The bounded primary-import text is preserved. +The earlier local-worktree location recorded in the predecessor is historical +provenance; the current repository links are operational. + +Actual consumed [FG contact proof](../finite_gaussian_contact/PROOF.md): +25,367 bytes / 554 lines, SHA256 +`7fea2656e11d986e1a5d6bfb0a05c8421bd93262d28051b8cfef05320595f474`. +Its Gaussian law, literal pin contract, covariance floor, projector coupling, +endpoint identities, polynomial moments and contact normalizer are consumed. +The actual FG copy was previously fully read and freshly rehashed here. + +Actual consumed [CG proof](../finite_contact_genericity/PROOF.md): +23,431 bytes / 473 lines, SHA256 +`233e80421ccf78e9a9015116aaaf2d355a8425107ff109c022ddc98cd1f87fd9`, +Git blob `569a49dee2ec1b517cc231869aade4f6322f562f`. +The present author freshly read all 473 lines of the actual incorporated file +and independently reproduced this identity for this incorporation. This is +an author input check, not a nonauthor review of CG. Root and +`/root/final_contract_review` separately completed full incorporated-CG reads. +CG's separately completed preparation/incorporated-source review scopes are +recorded in [its companion](../finite_contact_genericity/REVIEW.md). + +The predecessor's consumed CG object was the preserved external preparation, +23,103 bytes / 468 lines, SHA256 +`a06ec513ce4b83bdeb1e600787a0acfcf9bb20a217ab6009bb326df8c8fd6fe5`. +Its peer review was pending when the elder predecessor was written. That is +historical preparation-time status, not CG's current disposition. The old +source remains unchanged, and the new consumed CG binding is explicit above. + +Recorded formula identities were freshly rehashed: +[models.py](../models.py), 12,385 bytes, +`7ba088158b5e97ba6e7d715e66e6f9d14268ac3a82a6d187a776821936cc6686`; +[models.json](../models.json), 12,914 bytes, +`10d334b27cac985d61506b4f26118699cd1689a82a0f6e454cef8d00df21e595`. +They are not certification of the finite-word sampler as the continuous +ideal Gaussian coefficient law. + +## Actual predecessor reads and current disposition + +The original author fully reread the final 21,138-byte external preparation +and checked its deterministic enclosure and weighted transfer arguments. +Root subsequently fully read those exact bytes. These are author and +source/integration reads, respectively. + +`/root/final_contract_review` freshly read the complete actual 21,138-byte +predecessor, independently reproduced its exact hash, and returned **PASS** +with no mathematical must-fix. Its full-file verdict is separate from its +earlier attack on the communicated core before a file existed. It checked +transverse elimination and strict convexity, two-point local uniqueness, +global critical-branch persistence and critical-height gaps, the complete +maximum-component enclosure, the older ridge branch and actual merger, +H0 interval endpoints, canonical coupling, weight factor36, polynomial +moment domination and the separate compact-uniformity argument. This verdict +binds the external predecessor only. + +**Fresh full exact-file nonauthor review of the incorporated proof: PASS.** +`/root/final_contract_review` read all 458 lines of the actual 23,774-byte +source at SHA256 `c9e4fb09900888cd2b1bd96b49f85072b51c822b2503fe9f3d8891049bf66201`, +independently reproduced its hash, consumed FG/CG hashes and recorded model identities, +and inspected the complete actual predecessor diff. It verified the common +Sections 2–13 block hash +`eef0cc2fba152da76d83c6f738ca7f5fd9d531c2e919fe9d74b261dd1fbc3abe`. +Its new mathematical verdict is **PASS**, with no must-fix finding. It attacked +local critical uniqueness and types, enclosure and the older connection, +global critical control, the Borel conditional event, actual Gaussian pin +coupling, weight36, polynomial domination and compact-subsequence uniformity. +This is a fresh new-byte verdict, distinct from its original preparation read. +The reader previously authored the separate fold-chart route, did not author +this elder proof and remains source/route exposed with independence credit0. +It did not reopen the primary sources, run a compiler or sample a field. +Root also freshly read the whole incorporated proof and complete real diff. + +The original construction-stage companion was 7,161 bytes / 122 lines, +SHA256 `2ddfb932aaeafd6881af09010faaf593d1bb6f980d3797761128ca3dd776c56b`. +The author and final-contract reader each read that whole metadata file; +its then-pending new-byte disposition is superseded here by the actual verdict. +Current companion metadata receives its own separately bound read. +The next full metadata read at 8,514 bytes / SHA256 +`95d4dfd86b57336efec947baafe912a57a73f9654f43f0a350675a58641573cb` +requested AMEND: its reviewer-exposure sentence incorrectly called the separate +fold-chart route a consumed dependency. The sentence is corrected here. ET +consumes FG/CG and records model identities; fold-chart authorship is prior +route exposure. The mathematical source and its full PASS are unchanged. +New publication, hosted checks, native review and integration are prospective +until actually performed and separately recorded. No new local unit test, +compiler execution, field draw or seed consumption was performed for these +Markdown changes. Hosted existing controls, when run, retain their own scope. + +## Classical import exposure and boundaries + +The original author successfully read the specified primary Milnor statements +and gradient-flow proof at the exact URL retained in PROOF.md: Lemma2.2, +printed page6; Theorems3.1–3.2, pages12 and14; and the critical-level remark +on page20. The author also read ELZ Section4, printed page523, including its +component representation and union/elder operation. Root separately reported +successful bounded statement reads at those URLs. These are bounded parsed +primary-PDF reads; no complete-book/paper read or raw-PDF byte custody is +claimed. No fresh primary-source fetch was performed for this incorporation. + +The deterministic theorem assumes global C4 convergence, exact moving pins, +a negative transverse contact pivot and isolated contact with finite offcontact +Morse critical points and distinct values different from b. It proves local +critical-point uniqueness using transverse elimination and strict convexity, +not convergence alone; the enclosure blocks global bypasses above the saddle, +and the other ridge branch reaches a point strictly above the newborn maximum. + +The probabilistic result uses the actual six-pin canonical Gaussian coupling. +Its limiting weight is 36k^2 A_0^2 1{A_0<0}. Weighted failure tends to zero; +normalizers remain positive on compact positive-k mark windows. Qualitative +compact-mark uniformity has a separate subsequence proof. There is no rate, +usable radius, unweighted-selection claim or common samplewise event over +uncountably many conditional targets. + +Global selected-bar counting and density composition remain a separate +consumer. Higher homology, factorial moments, process limits, arbitrary +additional pins, quantitative windows, blind tests, formal source alignment +and scientific admission remain outside this source. The exact contact stays +degenerate and is not passed to C210's nonsingular-Hessian premise. No existing +formal owner lane or scientific-status/applicability array is changed. diff --git a/experiments/universality/finite_h0_lifetime/PROOF.md b/experiments/universality/finite_h0_lifetime/PROOF.md new file mode 100644 index 000000000..7a3518edd --- /dev/null +++ b/experiments/universality/finite_h0_lifetime/PROOF.md @@ -0,0 +1,526 @@ +# Finite Gaussian H0 elder-bar lifetime intensity: conventional analytic source + +Prepared on 8 October 2026 by OpenAI/Codex `/root/universality_review`, at +`/root`'s request. Incorporated by the source and integration owner OpenAI/Codex +`/root`, task `01a11cbf-068d-7102-861e-75814e715c98`, under the +[five-path claim](https://github.com/d6g8k5htny-coder/main/issues/307#issuecomment-6070045125). +This source incorporates the frozen external preparation +`finite-selected-bar-intensity-preparation.md`, 25,439 UTF-8 bytes / 501 lines, +SHA256 `5f529e5ed2632c90819746848146e3a24acda7e888cd3c9342df76edcbcbb7a3`. +Its mathematical text in Sections 2–8 is unchanged. Source locations, +elder-source identity and review chronology are updated here. Actual new-byte +reviews and integration evidence are separately bound in the +[review record](REVIEW.md). + +The original author authored the candidate-lifetime and weighted-window +preparations and reviewed the contact, fold and contact-genericity arguments. +The elder-transfer author implemented the catalogue machinery and contributed +to the earlier mathematical routes. Root fully read the original saved source. +`/root/benchmark_formal_audit` and `/root/final_contract_review` each freshly +read and hashed all 501 lines of that original preparation and returned full +PASS, without a mathematical must-fix finding. Those verdicts bind the frozen +preparation; they are not rebound to this successor. This is source and +proof-route exposure within the same OpenAI/Codex team; organizational- +independence credit is zero. No human, blind or provider-distinct acceptance, +formal Lean proof, sampler execution, seed consumption or scientific promotion +is claimed. The source supplies a Borel selector, exact once-counting and the +selected density composition using the bound elder source below. + +## 1. Exact consumed sources and read scopes + +The original author fully reread C, CG and the frozen ET preparation for the +original composition. Current consumed repository identities are: + +* **C**, incorporated candidate theorem: + [candidate proof](../finite_candidate_lifetime/PROOF.md), + 29,190 UTF-8 bytes, 577 lines, SHA256 + `ed31f562f0ffaaf6d4bd2ceb1ae3d234798e983a55d55c6983b128fce27133f5`. +* **CG**, incorporated contact-conditioned genericity: + [contact-genericity proof](../finite_contact_genericity/PROOF.md), + 23,431 UTF-8 bytes, 473 lines, SHA256 + `233e80421ccf78e9a9015116aaaf2d355a8425107ff109c022ddc98cd1f87fd9`. +* **ET**, incorporated elder-transfer proof: + [elder proof](../finite_elder_transfer/PROOF.md), 23,774 UTF-8 bytes / 458 lines, + SHA256 + `c9e4fb09900888cd2b1bd96b49f85072b51c822b2503fe9f3d8891049bf66201`. + +Root freshly read the complete incorporated ET source and its complete real +predecessor diff, and independently reproduced these current C/CG/ET byte +identities. The mathematical sections of ET are byte-identical to its frozen +preparation; the successor rebinds CG to the incorporated source and makes the +completed original-review chronology explicit. This composition consumes the +stated and proved analytic result at ET's current exact bytes; any source +correction requires reassessing this dependency. New-byte ET review verdicts +are separately recorded in [ET's companion](../finite_elder_transfer/REVIEW.md). + +The original composition instead consumed +`finite-contact-elder-transfer-preparation.md`, 21,138 UTF-8 bytes / 418 lines, +SHA256 `1cac9b525831b7e1f37f0d0561d3231fa73c8713c4c92283dca1d5b51b8a67ce`. +It recorded pending ET review when written; those original bytes remain frozen. +That original ET subsequently received a full exact-file nonauthor +`/root/final_contract_review` PASS and root complete read. Reading a source and +completing its mathematical review do not establish formal or scientific +admission. The original C/CG worktree locations are historical exposure paths; +the relative links above identify the current consumed repository copies. + +The underlying [**FG** contact proof](../finite_gaussian_contact/PROOF.md) was +previously fully read and reviewed: +25,367 UTF-8 bytes, 554 lines, SHA256 +`7fea2656e11d986e1a5d6bfb0a05c8421bd93262d28051b8cfef05320595f474`. +The original author rehashed its conditional-worktree copy; root freshly +reproduced the same current repository identity for this incorporation. +Its named moment, normalizer and envelope inputs were reread through C and ET. +No fresh full classical-paper or book fetch was performed in this composition. + +C explicitly imports equal-dimensional Sard and the weighted area formula. +Those imports, their prior primary-source exposure and their limits remain as +recorded in C; no new proof of Sard or the area formula is claimed here. +ET explicitly records its specified primary Milnor and Edelsbrunner-Letscher- +Zomorodian reads and imported Morse/elder facts. That is ET's author's read, +not a fresh primary-book read by this author. Sections 3-4 below independently +spell out the component argument and elementary H0 once-counting used here. + +The source chain used is finite Gaussian ranks/regression and envelope (FG), +unconditional genericity and all-Borel pair counting (C), contact-conditioned +genericity (CG), deterministic and weighted elder transfer (ET), then the +selector/counting/density composition proved here. No arbitrary finite-jet +independence premise is transferred across this chain. + +## 2. Fixed ideal law, observable, and precise theorem + +Fix an integer K>=2, L>0 and omega=2pi/L. On X=R^2/(L Z^2), with area V=L^2, +use the ideal real Gaussian field + + S_K={-K,...,K}^2, + q_n>0, q_n=q_-n, sum q_n=1, + F(z)=sqrt(q_0) C_0 + +sum_pairs sqrt(2q_n) + [C_n cos(omega n.z)+S_n sin(omega n.z)], (1) + +where the coefficient coordinates are independent standard real Gaussians +and one representative of each nonzero pair {n,-n} is used. The coefficient +vector xi has dimension N=(2K+1)^2. The field is smooth, stationary and +variance one. It need not be rotationally isotropic. + +Use superlevel H0 over any fixed coefficient field, with increasing filtration +parameter t=-c and sets {F>=c}. A finite elder bar born at a local maximum p +and dying at a component-merging index-one saddle q has height lifetime + + ell=F(p)-F(q)>0. + +Its interval in increasing parameter is [-F(p),-F(q)); endpoint conventions +do not alter its lifetime. The one essential class is excluded. For a Borel +I subset of (0,infinity), let N_bar(I) count all such finite bars and put + + mu_bar(I)=E N_bar(I)/V. + +The observable can be assigned value zero on the unconditional null set of +non-Morse or equal-critical-value fields. Section 4 gives a Borel version +which equals the actual finite-bar count almost surely. + +**Composition theorem.** Consuming the analytic elder-transfer result of ET +for the same fixed law (1), mu_bar has a finite nonnegative Borel density +representative nu_bar on ell>0, specified by the marked kernel below, with + + nu_bar(ell) ~ C_loc ell^(-1/3), ell decreasing to zero, (2) + E N_bar((0,t])/V ~ (3/2) C_loc t^(2/3). (3) + +The density coefficient is exactly C's finite positive candidate coefficient: + + C_loc=Gamma(7/6)/(24^(1/3) sqrt(pi)) + *integral_{S^1} p_G(0) p_Vu(0) tau_u^(4/3) + [s_u^2/2] d sigma(u), (4) + +where G=(F_u,F_v), V_u=(F_uu,F_uv), T_u=F_uuu, A_u=F_vv, +tau_u^2=Var(T_u|G=0), and s_u^2=Var(A_u|V_u=0). Every derivative and +covariance is from (1). Angular measure is unnormalized arclength of mass +2pi. The numeral 24 in (4) is the Jacobian/gamma factor, not the side L. +Whole-torus expected counts have coefficient V C_loc; at side24, V=576. + +Equation (2) concerns the particular finite Borel representative constructed +in Section 5. An arbitrary Radon-Nikodym representative can be changed on a +null set and need not retain a pointwise asymptotic. No continuity of nu_bar +is proved, and no O(1) near-term remainder is claimed. Equation (3) is an +intrinsic statement about the expected measure and follows by integration, +not by differentiating a cumulative asymptotic. + +## 3. A Borel elder-death threshold from open superlevels + +Let D be a countable dense subset of X. Fix a countable basis of open metric +balls with centers in D and rational radii below one eighth of the torus +injectivity radius. Their closures are compact, and the balls are path +connected. This basis is fixed independently of F. + +For a real level lambda, define C_lambda(p,z;xi) to mean that p,z belong to +the same path component of the open set {F_xi>lambda}. It has the following +countable description: there is a finite chain of basis balls B_1,...,B_m +such that + + p in B_1, z in B_m, + B_i intersects B_(i+1), + min_{closure B_i} F_xi > lambda for every i. (5) + +Each chain condition is Borel jointly in (lambda,p,z,xi). The minimum on +each fixed compact ball is continuous in xi, because coefficient convergence +implies uniform field convergence. The union over finite chains is countable. +Conversely, a path in {F>lambda} has compact image and can be covered by +finitely many basis balls with closures inside that open set; a chain along +the path gives (5). A chain gives a path because its balls are path connected +with consecutive nonempty intersections. Thus (5) is the exact connectivity +relation, not an approximation by a fixed finite mesh. + +For every p define the extended-real threshold + + d_xi(p)=sup{lambda in Q: + lambdaF_xi(p), + C_lambda(p,z;xi)}, (6) + +with supremum of the empty set equal to -infinity. This is a Borel function +of (p,xi), by countability of the levels and dense points. It never equals ++infinity because qualifying levels are below F_xi(p). + +The dense-point condition is equivalent to connecting to any point of height +strictly greater than F(p): strict inequality supplies an open neighborhood +containing a dense point, and a short extension of the path stays in the open +superlevel. Consequently (6) is intrinsic, despite the chosen basis. In +particular it is equivariant under torus translations. + +If no point has greater height, d=-infinity. If some point has greater height, +every sufficiently low level qualifies, since X is connected and lambda can +be taken below min F. Therefore d is finite in that case. For a nondegenerate +local maximum, a small enclosing boundary has height strictly below F(p), +which makes d0. (12) + +C already proves finiteness of its displayed candidate density at every +positive lifetime, and finite total expected candidate count. Thus (11) is +finite everywhere on ell>0, and mu_bar has finite total mass as well. + +The unconditional null exceptional set G^c need not be null in every fixed +six-pin regression fiber. Formula (9) with its indicator implies only that +the determinant-weighted exceptional contribution vanishes for almost every +location/height tuple, after disintegration. That is sufficient for (11). +We do not turn that almost-everywhere statement into a static all-target +conditional Morse assertion. The separate ET coupling proves the small-r +selection limit needed next. + +The selected factor is global and need not be continuous. C's continuity +proof uses the continuous determinant-weighted type W without S. It does +not imply continuity of the expectation in (10) or of nu_bar. Measurability, +finiteness and domination are the statements proved here. + +## 6. Exact consumption of the elder-transfer result + +In the near band let M=x-r u/2, S=x+r u/2 and use the literal six-pin law Q_r +at heights b,b-k r^3, with k>0. Its divided-difference target is + + v_r=(b-k r^3/2,-k r^2,0,12k,0,0). + +Write V_r=W_r/r^2 and z_r=E_Qr V_r. ET uses the actual coupled coefficients + + xi_r=m_r+P_r Z, + +with m_r,P_r from the six divided-difference rows. They converge to their +contact versions and give global C4 convergence of the same actual fields. +Under the contact law, CG supplies isolated contact, all other critical points +Morse, finite distinct other critical heights different from b. On A_0<0, +ET Sections 2-9 prove that the actual pinned pair is eventually the finite +elder pair and that F_r is globally Morse with distinct values. These are +exactly the conditions in the selector (7). + +ET Section 11 proves, for each fixed b,k>0,x and frame, + + E_Qr[V_r(1-1_Er)]->0, + z_r->z_0=36k^2 E[A_0^2 1{A_0<0}]>0, (13) + +where E_r is that globally good actual-pair event. The selector agrees with +1_Er on the actual pinned fields. ET proves (13) by the polynomial Gaussian +envelope and dominated convergence: V_r converges to +36k^2 A_0^2 1{A_0<0}, and selection is eventually true on its positive +support. It does not assume that every fixed finite-r pin law is globally +generic. ET Section 12 separately proves uniform normalized selection on +compact birth/gap marks, locations and frames, by varying-parameter +subsequences; pointwise convergence alone is not represented as uniform. + +Consequently the exact consumption needed here is + + E_Qr[V_r S(M,S,xi)]->z_0. (14) + +It follows by subtracting the first term in (13) from z_r. We need only the +pointwise form for every fixed mark and frame in the all-mark dominated +convergence argument. The stronger compact uniformity is available from ET, +but no all-mark normalized inverse-z bound is used. + +When z_r>0, this also reads Q_r^W(S=1)->1. If a normalizer vanishes outside +the eventual compact-mark positive band, no ratio is needed: the selected +amplitude below is defined directly by its unnormalized expectation. No +division by k, a transverse curvature, or a random inverse normalizer enters. + +## 7. Selected near-diagonal density and all-mark limit + +Choose C's common near band 0=ell/r_0^3} + B_((ell/k)^(1/3))(b,k,u)/(3k^(2/3)) + db dk d sigma(u). (18) + +This is direct height/lifetime disintegration of the selected count; it is +not a derivative of a cumulative estimate. Values at the band boundary can +be assigned by either convention without changing the integral. +Equivalently, substitute k=ell/r^3 directly in the fixed-ell polar integral +from (11): its radial factor is r^-2 B_r dr. This gives (18) pointwise for +the same representative, not just equality of two density versions almost +everywhere. + +For every fixed b,k>0,u, pi_r(v_r)->pi_0(v_0) by the contact covariance +limit, and (14) gives + + B_r->12 pi_0(v_0) z_0. (19) + +As ell decreases to0 the indicator in (18) tends to1. Equation (16) gives +the integrable majorant H/(3k^(2/3)). The product is Borel, so dominated +convergence over all marks and angles gives + + ell^(1/3) nu_bar,near(ell) + ->4 integral k^(-2/3) pi_0(v_0) z_0 db dk d sigma + =C_loc. (20) + +Each fixed mark belongs to some compact mark window, so ET's compact-mark +scope supplies its pointwise limit wherever needed. No common samplewise +event over all marks or frames is required. The integral over noncompact +marks is controlled by the unnormalized envelope, rather than by a claimed +uniform selection probability on that noncompact set. + +## 8. Far complement, cumulative conclusion, and coefficient + +At torus separation at least r_0, the original six-pin covariance has a +compact-domain positive floor. C's far candidate bound gives + + 0<=nu_bar,far(ell)<=nu_cand,far(ell)<=C, + 00`, by C's near limit and (20). +This is only an `o(ell^-1/3)` complement estimate; no `O(1)` missed-near +bound follows from the dominated-convergence argument. + +Since C_loc>0, for every relative error tolerance there is a small lifetime +band on which nu_bar is bounded above and below by the corresponding +multiples of C_loc ell^-1/3. Integrating from0 to t gives (3), with + + integral_0^t ell^-1/3 d ell=(3/2)t^(2/3). + +The cumulative statement is independent of the representative's null-set +values. No stronger near remainder or continuity is inferred. + +The coefficient in (20) is C's already evaluated contact functional. Its +parity ledger retains all within-block correlations. In particular the +law of A conditioned on F=b,V_u=0 need not be centered; birth disintegration +first reduces it to A|V_u=0, whose negative-halfline second moment is +s_u^2/2. The remaining half-Gaussian integral gives precisely the factor +Gamma(7/6)/(24^(1/3)sqrt(pi)) in (4). Thus selection changes no leading +coefficient or angular/area factor. It supplies no numerical enclosure or +model-independent coefficient. + +## 9. Finite family and remaining boundaries + +C, CG and ET cover every fixed positive symmetric full-square ideal Gaussian +law with integer K>=2 and L>0, with its own constants. In particular the ten +catalogue spectra with ideal Gaussian coefficients at L24 and K2/3 give +twenty fixed cases. The Borel and H0 arguments here are deterministic and +unchanged between them. Finite minima of the input bands and constants, and +ET's separately proved finite-family compact uniformity, are valid. Finite +many individual density limits then yield + + max_j |ell^(1/3) nu_bar,j(ell)-C_loc,j| ->0. + +Each coefficient is positive, so uniform relative leading asymptotics over +this fixed finite family follow as well. There is no uniform claim over +spectra approaching a positivity boundary, unbounded K, variable L or an +unspecified infinite-field law. K1 and non-Gaussian coefficient laws are +outside the consumed route. No finite-word or quantized sampler is identified +with the continuous ideal Gaussian coefficient law. + +This source supplies all finite superlevel H0 bars in the expected +lifetime measure, not just candidate pairs. It does not supply higher +homology, factorial moments, a point-process limit, a quantitative usable +asymptotic window, coefficient digits, blind-field validation, scientific +promotion, publication acceptance or external uptake. The exact contact +itself remains degenerate. No formal owner lane or old source is amended. + +The only new model-specific selection input consumed by the composition is +ET at the stated current exact source hash. Its CG/contact prerequisites, +original pending-review history and subsequently completed original review +remain explicit. The Borel selector, once-counting and selected near/far +dominated-convergence steps are proved here. New-byte exact-source nonauthor +verdicts are separately bound in the companion review record. diff --git a/experiments/universality/finite_h0_lifetime/REVIEW.md b/experiments/universality/finite_h0_lifetime/REVIEW.md new file mode 100644 index 000000000..115464644 --- /dev/null +++ b/experiments/universality/finite_h0_lifetime/REVIEW.md @@ -0,0 +1,164 @@ +# Actual finite Gaussian H0 lifetimes: exact-source technical review + +The [proof](PROOF.md) constructs a Borel elder selector, counts every finite +superlevel H0 bar exactly once and composes the actual selected lifetime +intensity. For each fixed positive full-square ideal Gaussian law at integer +cutoff K>=2, its specified finite Borel density has leading coefficient C_loc +and power -1/3; the intrinsic cumulative measure has coefficient 3C_loc/2 +and power 2/3. This is a conventional analytic theorem with explicit imports. + +The source and integration owner and successor incorporation performer is +OpenAI/Codex `/root`, task `01a11cbf-068d-7102-861e-75814e715c98`, under the +[five-path claim](https://github.com/d6g8k5htny-coder/main/issues/307#issuecomment-6070045125). +The original mathematical author is `/root/universality_review`, who also +authored the candidate and weighted-window preparations and reviewed +other sources in this route. All contributors/readers are source and route +exposed OpenAI/Codex. Organizational-independence credit is **zero**. No human, +blind reconstruction or provider-distinct acceptance is claimed. + +## Exact objects and dependencies + +The incorporated proof is **27,064 UTF-8 bytes / 526 lines**, SHA256 +`5ea91111fa5f3d78d7c4188ebe84b3bc2c452b05dfdfc62c74b03123cb2696d1`. +The frozen external predecessor is +`finite-selected-bar-intensity-preparation.md`, **25,439 bytes / 501 lines**, +SHA256 `5f529e5ed2632c90819746848146e3a24acda7e888cd3c9342df76edcbcbb7a3`. +Actual mathematical Sections 2–8 are byte-identical. Incorporation changes +provenance, operational source links, the exact consumed elder identity and +completed original-review chronology, plus preservation wording in Section 9. +The earlier pending-ET-review sentence remains history in the frozen original; +it is not ET's current disposition. Original and new-byte verdicts are separate. + +The exact consumed sources are: + +| Source | Bytes / lines | SHA256 | +| --- | --- | --- | +| [C: candidate theorem](../finite_candidate_lifetime/PROOF.md) | 29,190 / 577 | `ed31f562f0ffaaf6d4bd2ceb1ae3d234798e983a55d55c6983b128fce27133f5` | +| [CG: contact genericity](../finite_contact_genericity/PROOF.md) | 23,431 / 473 | `233e80421ccf78e9a9015116aaaf2d355a8425107ff109c022ddc98cd1f87fd9` | +| [ET: incorporated elder transfer](../finite_elder_transfer/PROOF.md) | 23,774 / 458 | `c9e4fb09900888cd2b1bd96b49f85072b51c822b2503fe9f3d8891049bf66201` | +| [FG: underlying contact inputs](../finite_gaussian_contact/PROOF.md) | 25,367 / 554 | `7fea2656e11d986e1a5d6bfb0a05c8421bd93262d28051b8cfef05320595f474` | + +The original author fully reread C, CG and the original elder preparation +1cac9b5258…; it had previously fully read FG and freshly rehashed it. Root +freshly read all 458 lines of the incorporated ET source and its complete +actual predecessor diff, verified its mathematical text byte-preservation, +and independently reproduced all four current dependency hashes. The +[ET review record](../finite_elder_transfer/REVIEW.md) separately records +actual new-byte review and original classical imports. A correction to ET or +another consumed source requires reassessing this composition. + +## Original exact-file reviews + +Root fully read the entire frozen 25,439-byte original preparation. This is a +source/integration read. The following are actual full nonauthor original-file +verdicts, each bound to 5f529e5ed2632c90819746848146e3a24acda7e888cd3c9342df76edcbcbb7a3: + +* `/root/benchmark_formal_audit` fully read and independently hashed all 501 + lines and returned **PASS**, with no mathematical must-fix. It checked the + Borel connectivity and elder-death rule, exclusion of the essential class, + exact once-counting, all-Borel coefficient-space counting, singular Gaussian + conditioning, fixed density-representative scope, elder-transfer consumption, + all-mark domination, constants and the near/far boundary. It tried essential- + maximum, loop-saddle, irrational-death, exceptional-fiber, small/large-mark + and false-continuity attacks. It authored ET and implemented catalogue + machinery; that dependency and contributor exposure are retained. +* `/root/final_contract_review` separately fully read and independently hashed + all 501 lines and returned **PASS**, with no mathematical must-fix. It checked + countable-ball path equivalence, rational-supremum elder death, finite H0 + decomposition, all-Borel area formula with the determinant once, canonical + conditioning and exceptional-fiber scope, pointwise polar substitution for + the specified Borel representative, selected all-mark dominated convergence, + scalar gamma constant, transverse conditional second moment, area cancellation, + far bound and intrinsic cumulative integration. It freshly confirmed C, CG, + original ET and FG identities. It previously authored the separate fold-chart + source; that is prior route exposure, not authorship of this selected proof. + +Both reviewers previously consumed mathematical sources in this route. Neither +performed a fresh full primary-book/paper fetch, formal compiler run, field +sample or seed operation for these verdicts. They confer no scientific-status +promotion, empirical coefficient confirmation or organizational independence. + +**Fresh full exact-file nonauthor reviews of the incorporated proof: PASS.** +`/root/benchmark_formal_audit` and `/root/final_contract_review` each freshly +read all 526 lines of the actual 27,064-byte incorporated source, independently +reproduced SHA256 `5ea91111fa5f3d78d7c4188ebe84b3bc2c452b05dfdfc62c74b03123cb2696d1` +and all four current dependency identities, and inspected the complete actual +predecessor diff. Both returned **PASS**, without a mathematical must-fix. +Each rechecked measurable death, essential/loop exclusions, exact once-counting, +all-Borel counting, singular canonical conditioning, exceptional-fiber scope, +pointwise density-representative binding, actual elder transfer, all-mark +integration, full-circle orientation, area/gamma constants and far complement. +The final-contract reader verified common mathematical Sections 2–8 block hash +`64b1ced2e0027c74ca63dcd60666e7381c388330b3a83d3428181b47df83e288`. +These are actual new-byte verdicts, distinct from their original5f529e5e reads. +Their dependency-authorship, source/route exposure and independence0 remain +explicit; neither performed fresh primary-source, compiler or sample work. +Root also freshly read all 526 incorporated lines and the whole real diff. + +The original construction-stage H0 companion was 8,168 bytes / 125 lines, +SHA256 `2e511959a0327a6a3146f870c43aa93d36f692bbf637c13fe152ca80c2de2035`. +Both current-source readers fully read that metadata file and the unchanged +10,559-byte README at SHA256 +`c44553c00c86fad5045ac8c9e6c90f70b1e347173d2bad6f59804b35c888e5a7`. +They found no metadata or scope must-fix. Its then-pending current-source +status is superseded by the actual verdicts above; current companion metadata +receives a separately bound read. A subsequent full metadata read at 9,863 +bytes / SHA256 `2a6af8c65ff1a924906a3ae0813e2a522d79bf325719e6ee107560d2b144fcea` +requested AMEND: one original-review exposure sentence falsely called the +separate fold-chart source a consumed dependency. The reader acknowledged +missing that phrase in its construction-stage metadata PASS; that sentence- +level conclusion is superseded. The sentence is corrected here. H0 consumes +C/CG/ET/FG; fold-chart authorship is prior route exposure. Both actual-source +mathematical verdicts and proof bytes are unchanged. The next full metadata +read at 10,417 bytes / SHA256 +`ed92f14f5e6a87bfcbd092946807ed2b07586394fbb96f0c8fb64179e67b6d26` +requested a further AMEND: the author's grouped candidate/weighted-window +exposure sentence falsely described both as consumed. It is corrected here; +the weighted-window preparation is prior authorship/exposure. The final-contract +reader acknowledged missing that phrase in earlier metadata passes; that +sentence-level conclusion is superseded. New publication, hosted checks, +native review +and integration are prospective until performed and separately recorded. +No new local unit test, Lean execution, field draw or blind benchmark is +represented by these Markdown changes. Hosted existing controls retain their +own actual execution and scientific scope when obtained. + +## Mathematical audit boundary + +The selector uses countable open-superlevel ball chains and a rational +connection-to-higher-height supremum. On the open Morse/distinct-value set, +component labels and the elder rule identify exactly one maximum–merging-saddle +pair per finite bar. The global maximum's essential class is excluded; loop +saddles and minima do not kill H0 classes. The coefficient-space area formula +accepts this Borel mark; the physical Hessian determinant is used once. + +The canonical selected kernel defines a particular Borel density at every +positive lifetime, bounded by C's finite candidate density. No continuity of +the selected kernel or density is claimed. Its pointwise asymptotic applies to +that specified representative; the cumulative measure statement is intrinsic. +An unconditional null exceptional set is not presumed null in every fixed +conditional fiber. The weighted almost-everywhere identity and ET's actual +coupling supply precisely the needed statements. + +The near amplitude converges to the same local contact weight, with full-angle +orientation and ordinary torus area. The all-mark envelope handles k near zero +and infinity. Missed near candidates are only o(ell^(-1/3)), not an O(1) +remainder; the far selected contribution is bounded by the far candidate term. +The coefficient is positive and field-dependent. There is no half-angle factor, +new coefficient digit or empirical slope estimate. + +Classical Sard and area formula remain explicit imports in C. The named Morse +and elder facts and the original bounded Milnor/ELZ exposure remain explicit +in ET. Root's separate bounded parsed-primary statement reads do not constitute +whole-book/paper reading or raw-PDF custody. The selected proof's original author +and current reviewers did not inherit a fresh classical-source read by this +composition. The measurable selector and once-counting argument are given here. + +The theorem covers each fixed positive full-square ideal Gaussian law K>=2, +and hence the twenty fixed Gaussian profile/cutoff cases. Finite-family +uniformity is not twenty empirical confirmations. Positivity-boundary spectra, +K1, non-Gaussian coefficients, infinite-field laws, numerical coupling, +quantitative usable windows, higher homology, factorial moments, process limits, +formal source alignment, blind fifty-law validation and external uptake remain +outside the result. The exact contact remains degenerate. The sampler/catalogue +and all scientific-status/applicability arrays retain their original labels.