From 9c6a73489c5ed2465a3cf65dcc950eeeae074b05 Mon Sep 17 00:00:00 2001 From: Dylan Roy Date: Tue, 29 Sep 2026 21:30:10 -0500 Subject: [PATCH 1/5] Identify actual elder partners through hard-negative fibres Add full fixed-d>=3 contained-tube proof and thin-domain counterexample, retained endpoint-matrix exhaustion of the actual failure measure, extended spectral failure coefficient, weak actual partner/death/lifetime law, and the exact compact lifetime-density difference. Preserve initial/intermediate AMEND and final same-provider noncontributor review. Conditional author-side science; no count-law premise, status promotion or existing source change. --- .../HARD_FIBRE_LEMMA.md | 254 ++++++++++ .../NONAUTHOR_REVIEW.md | 143 ++++++ .../concave_fibre_elder_20260930/PROOF.md | 468 ++++++++++++++++++ .../concave_fibre_elder_20260930/README.md | 43 ++ .../RECONNAISSANCE.md | 32 ++ .../concave_fibre_elder_20260930/SOURCES.json | 121 +++++ .../SOURCE_INTERFACE.md | 191 +++++++ 7 files changed, 1252 insertions(+) create mode 100644 frontiers/concave_fibre_elder_20260930/HARD_FIBRE_LEMMA.md create mode 100644 frontiers/concave_fibre_elder_20260930/NONAUTHOR_REVIEW.md create mode 100644 frontiers/concave_fibre_elder_20260930/PROOF.md create mode 100644 frontiers/concave_fibre_elder_20260930/README.md create mode 100644 frontiers/concave_fibre_elder_20260930/RECONNAISSANCE.md create mode 100644 frontiers/concave_fibre_elder_20260930/SOURCES.json create mode 100644 frontiers/concave_fibre_elder_20260930/SOURCE_INTERFACE.md diff --git a/frontiers/concave_fibre_elder_20260930/HARD_FIBRE_LEMMA.md b/frontiers/concave_fibre_elder_20260930/HARD_FIBRE_LEMMA.md new file mode 100644 index 000000000..7365ed9bc --- /dev/null +++ b/frontiers/concave_fibre_elder_20260930/HARD_FIBRE_LEMMA.md @@ -0,0 +1,254 @@ +# Hard-negative fibre lift of the planar elder barrier + +Author-side deterministic contribution by OpenAI `concave_fibre_geometry`, 30 September 2026. This is a mathematical extension candidate, not a source acceptance decision. It changes no existing source, status, integration disposition or probability/count claim. Its planar input is §§2–6 of `local_elder_geometry_20260930/PROOF.md`, corresponding to the requested PR170 cut. Source-cut verification and acceptance provenance are separate obligations handled by the parent task. + +## 1. The planar input and the additional geometric condition + +Let + +\[ +P(X,Z)=2kX^3-\frac{3k}{2}X-\frac{k}{2} + +\frac{s}{2}Z^2+\frac a2(X^2-1/4)Z + +\frac\beta2XZ^2+\frac c6Z^3, +\] + +with \(k>0\), \(M=(-1/2,0)\), \(S=(1/2,0)\), +\[ +B=\beta-a^2/(12k),\qquad +D=(c-a\beta/(4k)+a^3/(72k^2))/2. +\] +Assume the strict typed condition \(s<-|B|/2\), and exclude +\[ +12kD^2+(s-B)^2(B+2s)=0,\qquad 12kD^2+B^3=0. +\] +Let \(\mathcal Y=\{S\}\cup C(P)\), where \(C(P)\) consists of the additional critical points in \(-kk\), the hard boundary obeys the relative drop estimate + \[ + g_i(x,z)\le G_i(x)-D_0\quad(x\in\overline B_R,\ z\in\partial F_i(x)). \tag{HD} + \] + A graph-centred ellipsoid tube, described below, is a concrete sufficient interpretation of this tube hypothesis. + +No uniform lower bound on the hard Hessian eigenvalues is needed if (HD) is given directly. No control is required outside this tube. Strict negativity by itself, without (HD) or an equivalent closed-barrier condition, does not suffice. + +The hard tube need not cover the whole of \(B_{R+1}\): the reduced height only needs to be defined there for the planar collar construction, whereas the full lift needs a tube over the smaller disk containing the resulting caps. The graph paths also remain in that smaller disk. + +## 2. Deterministic conclusion + +For each \(Y\in\mathcal Y\), let \(Y_i\) be the unique continued critical point of \(G_i\), taking \(S_i=S\), and let +\[ +h_i=\max_{Y\in\mathcal Y}G_i(Y_i),\qquad +\widehat Y_i=\Psi_i(Y_i,\zeta_i(Y_i)),\qquad +\widehat M_i=\Psi_i(M,\zeta_i(M)). +\] +For all sufficiently large \(i\), +\[ +\boxed{\quad d_{f_i}(\widehat M_i)=b_i+r_i^3h_i.\quad} \tag{EHD} +\] +Here \(d_f(M)=\sup_{\gamma(0)=M,\ f(\gamma(1))>f(M)}\min_t f(\gamma(t))\) is the ordinary global superlevel maximin. In particular, +\[ +\frac{d_{f_i}(\widehat M_i)-b_i}{r_i^3}\to h_*. +\] +On the actual global Morse distinct-value locus, the unique graph point \(\widehat Y_i\) attaining \(h_i\) is the actual elder merge saddle. If \(C(P)\) is empty, this is exactly the lifted pinned saddle. If \(C(P)\) is nonempty, a continued window saddle has height strictly above \(-k\) and preempts the pinned saddle. Limiting ties do not obstruct the exact statement: one compares the finitely many actual heights at index \(i\). + +The actual lifetime is therefore exactly +\[ +b_i-d_{f_i}(\widehat M_i)=-r_i^3h_i, +\] +and its normalized limit is \(-h_*\). This is a deterministic geometry/lifetime result. It supplies no higher-dimensional tilted-law exhaustion, intensity, coefficient or count statement. + +## 3. Graph regularity and full critical-point indices + +At each fibre stationary point, negative definiteness makes \(g_{zz}\) invertible. The ordinary implicit function argument gives \(\zeta_i\in C^1\) for \(g_i\in C^2\), and +\[ +D\zeta_i=-g_{zz}^{-1}g_{zx},\qquad +\nabla G_i=g_x,\qquad +\nabla^2G_i=g_{xx}-g_{xz}g_{zz}^{-1}g_{zx}. \tag{SC} +\] +Thus \(G_i\in C^2\) even though a \(C^2\) graph is unnecessary. Existence of an interior fibre maximum must be assumed or separately verified; strict concavity alone only gives uniqueness once such a point exists. + +A point of the tube is full critical if and only if it lies on the graph and its soft point is critical for \(G_i\). At such a point, for soft and hard tangent vectors \(v,w\), +\[ +(v,w)^T\nabla^2g_i(v,w) +=v^T\nabla^2G_i v + +(w+g_{zz}^{-1}g_{zx}v)^Tg_{zz}(w+g_{zz}^{-1}g_{zx}v). +\] +This is an explicit invertible triangular change of variables, so full inertia adds \(m\) negative directions to reduced inertia. A reduced maximum lifts to a full maximum; a reduced saddle lifts to a nondegenerate full saddle with one positive direction and \(d-1\) negative directions, the superlevel merge index. No parametric Morse normal-form theorem is invoked. + +## 4. A fixed soft collar works at every level above the actual highest saddle + +For completeness, this records the properties of the planar construction that the lift actually needs. + +The cubic gradient estimate off the second excluded algebraic set gives +\[ +|\nabla P(x)|\ge c_0|x|^2\quad(|x|\ge R_0). +\] +Choose \(R_0\) to contain all window roots, the pins, and a small oval about \(M\). Choose \(R\) sufficiently large to contain all doubled chords and satisfy +\[ +R-R_0>\frac{2k}{c_0R_0^2}+1. +\] +For all sufficiently large \(i\), reduced \(C^1\) convergence on \(\overline B_{R+1}\) gives +\[ +|\nabla G_i(x)|\ge(c_0/2)|x|^2 +\quad(R_0\le|x|\le R+1). +\] +There are no reduced critical points in \((h_i,0)\) inside \(B_{R+1}\). This is elementary finite-root stability: around any nondegenerate root \(Y\), the map +\(x\mapsto x-(\nabla^2P(Y))^{-1}\nabla G_i(x)\) +is a contraction on a sufficiently small closed ball and maps that ball into itself for large \(i\). It has exactly one root there. Outside these disjoint root balls, in a slightly enlarged compact height band containing \([-k,0]\), \(\nabla P\) has a positive lower bound; convergence excludes any other roots. The excluded transition set prevents an additional critical point at \(-k\), and the source proves that the only critical point at or above zero is \(M\). + +Fix \(t_0\in(h_*,0)\) sufficiently close to zero. Uniformly negative Hessians in a small ball about the exact pin give a small disk \(K_{i,0}\) with +\[ +G_i=t_0\text{ on }\partial K_{i,0},\qquad +t_0\le G_i\le0\text{ on }K_{i,0}. +\] +One can construct the disk without a Morse lemma: the radial derivative from \(M\) is strictly negative under the negative Hessian bound, so every ray meets level \(t_0\) once and the implicit function theorem gives its oval. + +For every \(h_ih_i\), choose \(h\in(h_i,\min(t,t_0))\): this is a compact full cap whose boundary is strictly below that target. These direct derivative checks supply all regularity used here. + +The barrel argument already proves global normalized death \(\le h\) for every \(h>h_i\) sufficiently close to \(h_i\). Letting \(h\downarrow h_i\) gives the exact upper bound \(\le h_i\). + +## 6. Exact lower bound on the graph, and actual pairing + +For each \(Y\in\mathcal Y\), use the moving soft critical chord +\[ +x_i(t)=M+t(Y_i-M),\qquad +q_i(t)=G_i(x_i(t)),\qquad 0\le t\le2. +\] +Exact criticality gives \(q_i'(0)=q_i'(1)=0\). Reduced \(C^2\) convergence gives convergence of these restrictions in \(C^2\) to +\[ +q(t)=P(Y)(3t^2-2t^3). +\] +The limit has \(q''(0)=6P(Y)<0\), \(q''(1)=-6P(Y)>0\), negative derivative on \((0,1)\), positive derivative on \((1,2)\), and \(q(2)=-4P(Y)>0\). Second-derivative signs near the two exact derivative zeros, followed by first-derivative convergence away from those zeros, give the same strict monotonicity for \(q_i\) for all sufficiently large \(i\). Therefore its exact minimum is \(G_i(Y_i)\), and its endpoint is older than birth. + +Lift the chord to the actual chart by +\[ +\gamma_{i,Y}(t)=\Psi_i(x_i(t),\zeta_i(x_i(t))). +\] +This path has exactly the same height restriction \(b_i+r_i^3q_i(t)\). The graph may curve sharply and its hard coordinates need not converge; no approximation by a full-dimensional straight chord is made. Its inclusion in the tube is all that is needed. There are finitely many such paths, so one sufficiently large index works for all of them. The path corresponding to an actual maximizer of \(G_i(Y_i)\) gives normalized global death \(\ge h_i\), proving (EHD). + +This also directly identifies the merge at that graph point. Just above \(h_i\), the chord's two sides lead respectively to the birth and to an older endpoint, and they are in different global superlevel components because death is \(h_i\). At level \(h_i\), the chord joins them at \(\widehat Y_i\). On the global distinct-critical-value locus, no other critical point has that same height. The Schur identity proves it is a full merge-index saddle. Hence it is the actual elder saddle under the same ordinary maximin convention as the planar theorem. No Morse–Smale assumption or separatrix identification is needed. + +## 7. A quantitative test for anisotropic hard extent + +A simple sufficient replacement for (HD) is a positive-definite matrix \(A_i(x)\), a fixed depth \(D_0>k\), and the graph-centred ellipsoid tube +\[ +F_i(x)=\{\zeta_i(x)+v:v^TA_i(x)v<2D_0\}. +\] +Assume this compact tube lies in the chart interior and, throughout every fibre, +\[ +g_{zz}(x,z)\preceq-A_i(x). +\] +Twice integrating along the hard segment from the stationary maximum gives +\[ +g_i(x,\zeta_i(x)+v)\le G_i(x)-\frac12v^TA_i(x)v. +\] +On the hard boundary the drop is at least \(D_0\); above a planar cap, \(G_i\le0\), so hard boundary height is at most \(-D_0<-k\). This proves the needed barrier. The theorem only needs this boundary estimate above the cap family; imposing it over all \(B_R\) is a convenient checkable condition. + +The semiaxes are \(\sqrt{2D_0/\lambda_j(A_i(x))}\). They may depend on \(i\), on the base point, and on direction. Thus anisotropic full-chart extent is harmless provided those ellipsoids actually fit. Uniform hard concavity combined with an arbitrarily thin chart is insufficient. In physical coordinates with straight hard fibres (or an affine map in the hard variables), if an unnormalized physical hard Hessian obeys \(f_{yy}\preceq-H_i(x)\), the corresponding physical requirement is a contained ellipsoid +\[ +v^TH_i(x)v\le2D_0r_i^3. +\] +When \(H_i\) has order-one eigenvalues, its physical semiaxes have order \(r_i^{3/2}\). This is a sufficient geometric scale, not an assertion that the actual stochastic model supplies it. + +For an arbitrary nonlinear chart, one must verify the normalized-coordinate hard Hessian/drop directly, or include the chart's extra second-derivative terms; a physical Hessian bound does not automatically transform by congruence away from a full critical point. + +The logically weaker boundary condition is that hard boundary height is at most \(h_i\) over every cap used for levels decreasing to \(h_i\). A fixed margin below \(-k\) avoids depending on the unknown actual winning height and verifies this at once. Some closed full-dimensional barrier condition is indispensable if the exterior is arbitrary; strict hard concavity is one useful means of producing its vertical part. + +## 8. Explicit vertical-escape counterexample without depth + +Choose +\[ +P(X,Z)=2X^3-\frac32X-\frac12-\frac12Z^2+\frac13Z^3. +\] +Here \(k=1,s=-1,a=\beta=0,c=2\), hence \(B=0,D=1\), and the excluded discriminants are \(10\) and \(12\). The four critical points have heights +\[ +P(-1/2,0)=0,\quad P(1/2,0)=-1,\quad +P(-1/2,1)=-1/6,\quad P(1/2,1)=-7/6. +\] +Thus \(h_*=-1/6\). + +Let \(\epsilon_i\downarrow0\), and let \(\chi\in C^\infty(\mathbb R,[0,1])\) be zero on \(( -\infty,1]\) and one on \([2,\infty)\). For definiteness use elder height \(A=\sqrt2\), and set +\[ +H_i(w)=(1-\chi(w/\epsilon_i))(-w^2) + +\chi(w/\epsilon_i)\,[A-(w-3\epsilon_i)^2], +\qquad F_i(X,Z,w)=P(X,Z)+H_i(w). +\] +On the chart \(\mathbb R^2\times(-\epsilon_i,\epsilon_i)\), +\[ +F_i=P-w^2, +\] +so the hard Hessian is the uniformly strictly negative scalar \(-2\), the unique fibre maximum graph is \(w=0\), and its reduced height is exactly \(P\) on every compact soft set. Yet the exterior has an older strict maximum at \((M,3\epsilon_i)\), of height \(A\). Along \(0\le w\le3\epsilon_i\), the first blend term vanishes for \(w\ge2\epsilon_i\) and is otherwise at least \(-4\epsilon_i^2\); the second term is nonnegative for sufficiently small \(\epsilon_i\). Hence +\[ +d_{F_i}(M,0)\ge-4\epsilon_i^2>-1/6. +\] +A maximin beginning at height zero is at most zero, so these actual death levels tend to zero, rather than to \(h_*\). The obstruction is already visible at the hard chart boundary: +\[ +F_i(M,\epsilon_i)=-\epsilon_i^2\to0. +\] +For a compact-manifold version, protect a soft neighbourhood containing the pins, the four critical points and the vertical path; for each \(i\) its normalized radius can be finite but increasing to infinity. Multiply/extend smoothly outside a larger neighbourhood into a coordinate ball of a compact manifold. This retains convergence on every fixed normalized soft disk and changes neither the chart hypotheses nor the exhibited path bound. Additional \(m-1\) hard directions can be appended as \(-|z'|^2\), giving the same failure in every \(d\ge3\). Generic arbitrarily small perturbations away from the protected chart and the protected older maximum can impose the global Morse distinct-value locus while preserving the vertical-path lower bound (with, for example, \(-5\epsilon_i^2\) in place of \(-4\epsilon_i^2\)). The height counterexample itself does not need this extra locus. + +It also realizes genuinely shrinking anisotropic charts. Choose any \(r_i\downarrow0\), take +\(\Psi_i(X,Z,w)=(r_iX,r_iZ,r_i^{3/2}w)\) +in a fixed coordinate ball, and set \(f_i\circ\Psi_i=b_i+r_i^3F_i\) on the protected region. For example, choose its normalized soft radius \(R_i=r_i^{-1/2}\); its physical radius is then \(r_i^{1/2}\), so it fits inside the fixed coordinate ball while containing every fixed normalized soft disk for all large \(i\). Extend outside the protected physical region. On the thin physical hard chart \(|y|\0` followed by the exact bytes. No source file or manifest was changed. + +## Deterministic graph, collar, cap and exact elder saddle + +**Pass, under the displayed fixed-target hypotheses.** SC's complete-jet coupling bounds the actual global C4 norm at a fixed spectral target. With positive hard eigenvalues, the physical hard Hessian stays uniformly negative on each needed soft disk of radius `Rr` and a hard ball of radius `c0r`. The hard-gradient forcing at zero is `O(r^2)`, including the `−tau_xxwj/8` term forced by the endpoint pins. Strict concavity and an inward radial derivative give the interior graph; uniqueness preserves its exact hard-coordinate pins. + +Implicit differentiation gives graph size `O(r^2)`, first soft derivatives `O(r)` and second derivatives `O(1)`. The graph substitution changes the physical potential and its first and second soft derivatives by `O(r^4)`, `O(r^3)` and `O(r^2)`. Rescaling two soft coordinates by `r` and height by `r^3` makes each correction `O(r)` in C2. No inverse hard bound from this pointwise argument is placed in the probability majorant. + +The essential geometric addition is verified: a graph-centered physical hard radius `rho r^(3/2)` fits since `Cr^2+rho r^(3/2)k`. The graph's own `r^2` width would only produce an `r^4` physical drop and would not close the `r^3` death window. + +Off Delta, the cubic gradient grows quadratically at infinity. On a large fixed annulus, C1 convergence retains a gradient floor. Finite-root stability, exact pins and the Sigma exclusion remove all active-strip critical points other than the finite continued set. The cutoff gradient flow therefore transports the small maximum oval to level `h`, and the annulus speed bound prevents its boundary reaching the fixed soft disk boundary within time less than `k`. The same sufficiently large index works for every `h_i=2`, `Lambda` is a retained hard eigenvalue. Holding `J,lambda2,...,lambdam` fixed leaves `U=J+Lambda` fixed during the `lambda1` integration. This does not assume that matrix entries or eigenvalues are independent. + +The actual second soft determinant factor is retained. The inner integral is exactly + +`integral_0^(DrU^2) lambda1(lambda1+CrU) d lambda1 = r^3[(D^3/3)U^6+(CD^2/2)U^5]`. + +Together with the original outer `r^2` weight, this gives an `r^5` unnormalized numerator. Enlarging the ordered `lambda1` interval and dropping its Gaussian factor are valid positive-majorant operations. Division once by the full `Z_r>=z_*r^2` yields the required `r^3` scale. + +Retaining `1{U>A}` in that same integral and using higher uniform residual moments gives the polynomial tail tending to zero. Retaining `1{lambda2<=epsilon}` gives the vanishing hard strip mass by Gaussian polynomial integrability, including higher-corank intersections. There is no inverse eigenvalue or inverse gap factor. The M4 exception has tilted mass `O(r^4)` and vanishes after `r^−3` scaling. + +Weyl's inequality and Hessian Lipschitz control convert endpoint tightness to actual midpoint jet tightness. At fixed `A,epsilon`, a midpoint `h2<=epsilon` on `U<=A` implies endpoint `lambda2<=2epsilon` for small radius. Sending the U tail to zero and then epsilon to zero proves E7, including negative midpoint hard values. This is exhaustion of the full selector-failure measure. No count event, near-occurrence tail, factorial estimate or remote-witness event is substituted. + +## Spectral kernel, null sets and actual marks + +**Pass.** The spectral change contributes one raw soft Jacobian `r`, the actual determinant weight is on the `r^4` soft-sector scale, and the original full normalizer is on the `r^2` scale. After failure rescaling the prefactor is exactly `c_m r^2/Z_r`. The Jacobian's one hard power and determinant weight's two hard powers give the displayed `product h_j^3`; all remaining hard Vandermonde factors are retained. + +The extended sign-frame construction is essential and is stated correctly. Normalized Haar is the reference angular measure with SC's multiplicity constant, while the anisotropic raw Gaussian density stays inside the integral. It is not silently replaced by an invariant or GOE law. Simultaneous changes of O, the complete tensor, and the soft root coordinate leave the physical location unchanged. + +On compact positive hard sectors, the two-short-column bound supplies integrable conditional domination. Exact H1 supplies pointwise convergence of the actual failure indicator on generic typed targets. The determinant-weight limit is continuous and zero on or outside the typed boundary, so no selector convergence is needed there. Sigma, Delta, repeated spectra and the additional position set `D=0` are null sets under the displayed absolute-continuity interface; none is a discarded positive leading mass. Repeated hard spectra need no inverse-gap estimate. + +Compact L1 convergence and E4–E7 give global total variation for the extended jet/failure measure. SC's deterministic integrability bound makes the limiting measure finite; open positive nonempty sectors make its mass positive. The mass is exactly SC's displayed local integral `a1+a2`, with no `beta_far` term. This consumes a deterministic kernel and integral, not SC's global count conclusion. + +The actual partner, normalized death and lifetime marks are claimed only weakly. On generic compact couplings H1 supplies the local winning root and older path; the graph's hard displacement divided by r vanishes. Conditional dominated convergence then gives the joint pushforward, and actual failure exhaustion removes sentinel/essential mass. Weak tightness with converging total masses implies actual failed-partner locality for every deterministic cutoff with `delta_r/r` tending to infinity. No growing-radius root enclosure is needed. + +The fixed-radius Morse null set is used correctly through an arbitrary fixed sequence tending to zero: disintegration and a countable intersection give the relevant joint almost-sure locus along that sequence. The deterministic graph/cap/chord argument then applies. Limits along every such sequence establish the stated limit without an unsupported common null set for uncountably many pinned laws. + +## Compact actual lifetime-density interface and retained boundaries + +**Pass for L1 at its exact population.** P is consumed with ERR's corrected congruence, BOREL's whole-field replacement, and REC's convergence-in-law and embedded-chart reading rules. P's actual radial intensity is `r A_r dr`, with the dimension powers already cancelled. Pushing forward by `ell=kr^3` yields `ell^(-1/3)A_r/(3k^(2/3))`. Multiplication by failure probability `r^3[(1-p_r)/r^3]` gives exactly the density-difference factor `A_r[(1-p_r)/r^3]/(3k^(5/3))` after division by `ell^(2/3)`. + +P supplies the required compact common bounds; these are not inferred from pointwise topology. Dominated convergence therefore gives a finite positive coefficient C_fail for the compact candidate-minus-selected density. The original full z0 cancels against A0 if substituted, with one original pin density remaining. Transverse-frame independence follows from the physical probability and its unique limit, not from false torus rotational invariance or higher-dimensional birth cancellation. + +This density is not a replacement-bar intensity: a maximum may participate in multiple rejected candidates. It is not a standalone second-order selected-density expansion, an unrestricted refined difference, a numerical coefficient, a new count/moment theorem, or a statement uniform in vanishing k, growing dimension, volume or escaping marks. Those boundaries are retained. No numerical or engineering test was treated as mathematical evidence. + +## Recorded disposition + +Initial exact cut: **AMEND**, for the six literal/scope items above. Substantive H/F/M/L1 reasoning: no load-bearing defect found at the stated conditional source scope. All failures and requested corrections are preserved in this report. Publication or integration of a revised cut requires its own exact reread; this report does not accept author changes it has not seen. + +## Intermediate reread: residual coordinate label retained as AMEND + +The first author-corrected PROOF.md had 23415 bytes, SHA256 `fa405e286cb1cc337f57bffa671035a533818a0dc31196874005e1e300c4454c`, Git blob `8c1db93878253a3aa53f48cee1062ce9f9044cb8`. The corrected SOURCE_INTERFACE.md had 18098 bytes, SHA256 `cec41136dfac1fde2247f25dcf7601e1a01a6ec25c4d5f18e8bf1450e8360e48`, Git blob `7eb203bdf1311ff56b312962ba3f5ce6d5dd9766`. I reread both complete bodies and independently checked their identities. HARD_FIBRE_LEMMA.md and SOURCES.json were unchanged. + +The finite-r/contact derivative, exact/limiting lifetime, manifest locator, dependency roles, P lifetime scope, normalized pin arguments and cumulative-sentence removal were corrected. However, PROOF.md line 157 still called the normalized moving soft chord a chord “from M”, after explicitly reserving M for the physical pin. Both my read and the read-only geometric reviewer retained **AMEND** for that remaining instance of the original coordinate finding. The deterministic lemma itself remained correct, and the law reviewer accepted its corrected slice conditionally. This intermediate failed precision outcome is not erased by the final reread. + +## Final exact reread and source-scoped disposition + +The authors changed the remaining soft-chord label to M0. I independently verified and reread the complete final PROOF.md; the complete corrected SOURCE_INTERFACE.md was already reread at its unchanged final identity. The other load-bearing packet files are unchanged. The final reviewed cut is: + +| File | Bytes | Git blob | SHA256 | +|---|---:|---|---| +| PROOF.md | 23416 | `923d3236b5291a29bd162937f172190db84dcef5` | `5681896a6808f48fb7508914d0860ec508af7646e9e706fc260d935dd951c75e` | +| HARD_FIBRE_LEMMA.md | 18907 | `7365ed9bcf145c832d1c09f0b685fbe8d6695050` | `434ffd30ac96eb635211ea627459b78c1d39806f75b0634e0f4876dce0765b33` | +| SOURCE_INTERFACE.md | 18098 | `7eb203bdf1311ff56b312962ba3f5ce6d5dd9766` | `cec41136dfac1fde2247f25dcf7601e1a01a6ec25c4d5f18e8bf1450e8360e48` | +| SOURCES.json | 7186 | `f072e1bb5c79456be3c79451b6df5b287807edfa` | `b97a29ea09f8e8270bfddda8f364f0d61e431e30c1681af4b019f3fb48709a4d` | + +**Final disposition: ACCEPT at the displayed conditional source scope.** All initial literal precision findings and the intermediate residual label are resolved in this exact cut. No remaining mathematical or packet-precision AMEND was found. I did not edit any packet file, author any amendment to its proof, or make a remote write. + +This acceptance covers the contained negative hard-tube lift and its thin-domain falsifier; exact identification of the actual highest continued elder saddle with arbitrary exterior; full retained endpoint-matrix failure exhaustion and hard-boundary removal; the extended spectral jet/failure law in total variation with coefficient a1+a2; the weak actual joint partner/death/lifetime law and actual failed-partner locality; and the positive ell^(2/3) compact candidate-minus-selected lifetime-density coefficient L1 at its exact population. + +The hypotheses remain conditions. In particular the Gaussian/regression/cap/normalizer/Borel interfaces are consumed at the immutable identities above, with ERR, BOREL and REC's reading rules. LOCAL remains the exact public draft source identified by the manifest; its prior same-provider noncontributor review is not an external verdict on it or on this successor. SC's displayed analytic and deterministic spectral integral interfaces are consumed without promoting its global count theorem. Source verification, publication and finite checks supply no mathematical acceptance by themselves. + +The final acceptance supplies no replacement-bar intensity, standalone count or moment extension, register/status action, numerical enclosure, unrestricted refined lifetime difference, separate selected-density second-order expansion, or new parameter uniformity. It carries zero organizational-independence credit. The initial and intermediate AMEND records above remain part of the honest review history. diff --git a/frontiers/concave_fibre_elder_20260930/PROOF.md b/frontiers/concave_fibre_elder_20260930/PROOF.md new file mode 100644 index 000000000..923d3236b --- /dev/null +++ b/frontiers/concave_fibre_elder_20260930/PROOF.md @@ -0,0 +1,468 @@ +# Hard-negative fibres identify the actual elder law in every fixed dimension + +Author-side successor by OpenAI, 30 September 2026. Scientific effect NONE. +Disposition: AUTHOR_SIDE / HOLD pending qualified source-bound review. +The root, concave_fibre_geometry and higher_d_source_interface are contributors; +their source audits are not nonauthor acceptance. All source conditions below +are retained. No count moment or remote-count theorem is a premise. + +The complete deterministic lift, including its counterexample, is proved in +[HARD_FIBRE_LEMMA.md](HARD_FIBRE_LEMMA.md). The detailed analytic source +interface and retained matrix integral are in +[SOURCE_INTERFACE.md](SOURCE_INTERFACE.md). [SOURCES.json](SOURCES.json) +binds the complete public sources by immutable commit/path/blob/SHA256. +Together these files expose the full new argument; source hypotheses are not +accepted merely by being linked or having verified hashes. + +## 1. Model and the actual pairing estimand + +Fix an integer d>=3, torus side L>0, birth b in R, positive gap mark k, and an +orthonormal axial/transverse frame R. Use the exact variance-one periodized +Bargmann–Fock Gaussian field of [P], with strictly positive Fourier weights. +At M=(-r/2,0), S=(r/2,0), impose the original observations + + f(M)=b, f(S)=b-k r^3, grad f(M)=grad f(S)=0. + +Q_r is this original 2(d+1)-observation Gaussian regression. Set + + W_r=F_d(H_M) F_(d-1)(H_S), Z_r=E_(Q_r) W_r, + Q_r^W=(W_r/Z_r) Q_r. + +F_j is absolute Hessian determinant restricted to j negative eigenvalues. +There is one original weight and one FULL normalizer. No adjacency restriction, +extra pin density or good-event normalizer is inserted. [P] gives +Z_r/r^2 -> z0>0, with its congruence erratum [ERR] and convergence-in-law reading +rule [REC]. The ordinary global elder death is the superlevel maximin + + d_f(M)=sup_(gamma(0)=M, f(gamma(1))>b) min_t f(gamma(t)). + +An essential maximum has d_f(M)=-infinity. On the almost-sure global Morse +distinct-value locus of [P] §8, d_f(M) is the value of the actual elder merge +saddle when finite. Define + + F_r={actual ordinary elder partner of M is not S}, + p_r=Q_r^W(F_r^c), D_r=(d_f(M)-b)/r^3. + +The event is Borel by [P] §8; whole-field marked Kac–Rice uses the exact [BOREL] +repair, not an assumption that elder selection is a continuous local mark. +These are candidate pair-Palm estimands; counting every rejected candidate +does not count each replacement elder bar once. + +## 2. Original spectral coordinates and the soft cubic + +Put m=d-1. Write the signed ordered eigenvalues of -D_y^2 f(0) as +mu1<...0, -k P in C2 + +on every fixed soft disk. Write M0=(-1/2,0), S0=(1/2,0) for the normalized +soft pins, keeping M,S for the physical original pins. The graph retains +EXACT critical pins and values G_r(M0)=0, G_r(S0)=-k, since the original hard +gradients vanish there and the hard stationary point is unique. The proof of the supplied C2 interface, +including its derivative powers, is displayed in SOURCE_INTERFACE §2. + +The missing geometry is a full-dimensional barrier, not another root count. +For a fixed soft disk containing the planar collar and doubled critical chords, +let eta=min_j h_j>0. Taylor and the fixed C4 bound give + + f_ww <= -(eta/2) I + +on that soft disk at physical r scale and on a hard ball of radius c0 r, for +all sufficiently small r. This is a pointwise fixed-target bound; constants may +depend on eta. Twice integrating along a straight hard fibre gives + + f(t,zeta_r(t)+v) <= f(t,zeta_r(t))-(eta/4)|v|^2. + +Choose fixed rho with D0=eta rho^2/4>k. The centred hard tube +|v|<=rho r^(3/2) fits inside the c0 r ball, since zeta_r=O(r^2) and +r^(3/2)=o(r). On its hard boundary the normalized drop is at least D0. +This is the quantitative hard-depth hypothesis of HARD_FIBRE_LEMMA. The r^2 +scale of the critical graph alone would give a drop of order r^4 and would +not block escape across a death window of order r^3. + +For each continued soft window root Y_r, and the exact normalized S0, put + + h_r=max({-k} union {G_r(Y_r):Y in C(P)}). + +Theorem H (actual highest partner). Under the displayed fixed-target hypotheses, +for every sufficiently small r, + + d_f(M)=b+r^3 h_r. (H1) + +On the actual global Morse distinct-value locus, the unique highest continued +graph saddle is the actual ordinary elder partner. Its full Hessian has one +positive and d-1 negative directions. If n=0 the partner is EXACTLY S; if n>0 +a continued local window saddle preempts S. Limiting ties do not obstruct H1; +the comparison is between the finitely many ACTUAL heights at that r. + +Proof. [LOCAL] §§3–6 construct, in the reduced profile, compact disks K_(r,h) +for every h_rh_* pointwise in this coupling. When D!=0, the highest soft root +Y_*(Theta) is unique and the actual partner divided by r tends, in the original +physical axial frame, to + + T_*(Theta)=R(X_*, O(Z_*,0,...,0)). (H2) + +The hard graph coordinates divided by r vanish. Sign changes of an eigenframe +change Z_*,tau and O together, leaving H2 invariant. No separatrix or +Morse–Smale premise is needed. HARD_FIBRE_LEMMA §8 gives an explicit smooth +counterexample if the contained hard-depth tube is omitted, even when graph +convergence is exact and the physical hard Hessian is uniformly negative. + +## 4. Full failure-measure exhaustion from the endpoint matrix + +H1 is pointwise in fixed jets. It does not alone identify the full rare failure +law. This section supplies the required exhaustion from the actual endpoint +matrix, independently of any count or near-occurrence event. + +On typed support put B_M=-D_y^2 f(M)>0, with ordered eigenvalues + + 0=2, + v=m(m-1)/2. + +[P] (4.2)–(4.3) regress the whole field on the ENTIRE endpoint matrix and give +an independent residual g_r. Put J=1+||g_r||C4, U=J+Lambda. All fixed J moments +are uniformly bounded, J is independent of the whole matrix, and + + K=1+||f||C4 <= C(J+||B_M||F) <= C U. (E1) + +Here Lambda is among the retained eigenvalues lambda2,...,lambdam; its being +independent of lambda1 for this conditional integration is why m>=2 matters. +No independence among matrix entries, derivative suprema or internal residual +evaluations is asserted. + +The exact global good-cap implication [CAP]/[P] §8 gives F_r subset G_r^c, + + G_r={lambda1>[4/(3k)] r M3^2, r M4<=3k/10}. + +[P] (7.7), divided by the FULL Z floor once, bounds the M4 exception by O(r^4), +which is o(r^3). On the remaining depth branch, + + lambda1<=D r U^2, + W_r<=C r^2 U^(2m) lambda1(lambda1+C r U). (E2) + +The second factor is essential: it retains the saddle mixed-square term in +[P] (6.2). The endpoint matrix density has Gaussian bound [P] (3.5); its +spectral Jacobian is at most C Lambda^v. For every retained event E depending +only on J and the hard eigenvalues, the SAME integral gives + + E_Q[W_r;depth,E] + <= C r^2 E_J integral_hard exp(-c sum_hard lambda_j^2) + Lambda^v U^(2m) 1_E + integral_0^(D r U^2) lambda1(lambda1+C rU) d lambda1 + <= C r^5 E_J integral_hard exp(-c sum_hard lambda_j^2) + Lambda^v U^(2m+6) 1_E d lambda_hard. (E3) + +The extension of the lambda1 interval beyond its actual ordered interval is +an upper bound of a nonnegative majorant. U and E are retained while integrating +lambda1; its Gaussian factor may be dropped. Equation E3 is the retained-mark +version of [P] (7.4), not a new independence or cutoff inversion. + +Taking E={U>A}, using arbitrarily high J moments and Gaussian polynomial +integrability, and dividing once by Z_r>=z_*r^2, gives, for every fixed p>0, + + limsup_r r^-3 Q_r^W(F_r,U>A) <= C_p A^-p. (E4) + +Taking E={lambda2<=epsilon} in E3 gives + + lim_epsilon->0 limsup_r + r^-3 Q_r^W(F_r,lambda2<=epsilon)=0. (E5) + +Indeed integration of the hard Gaussian polynomial over this strip tends to +zero; for epsilon<=1 a constant times epsilon suffices after integrating all +other hard variables and the J moments. All higher-corank intersections are +included, with no inverse-hard-eigenvalue or inverse-gap factor. + +Weyl's eigenvalue inequality and Hessian Lipschitz control give + + |muj-lambdaj| <= r M3/2 <= C rU. + +On the depth branch this implies + + |s|<=D U^2+C U, |h|+|tau|+K<=C U. (E6) + +Consequently E4 is tightness of the FULL failure measure in the actual midpoint +jets and derivative norm, not just a compact-near count estimate. On U<=A, +midpoint h2<=epsilon implies endpoint lambda2<=2epsilon for sufficiently small +r at fixed epsilon,A. Equations E4–E5 and the M4 exception yield + + lim_epsilon->0 limsup_r + r^-3 Q_r^W(F_r,h2<=epsilon)=0. (E7) + +Midpoint hard eigenvalues of either sign near zero can carry no lost leading +failure mass. Inverse hard eigenvalues are used only at fixed positive targets +for graph convergence; they never enter E3. The complete detailed derivation +is SOURCE_INTERFACE §§4–5. No scalar shortcut is used: for d=2 one must retain +[LOCAL] §8's separate scalar near/far split, since Lambda=lambda1 there. + +## 5. The identified full elder-failure measure + +Let the limiting hard domain be 0=2) h_j^3 + product_(2<=i0} + ds dh dO d tau. (S1) + +It is extended by zero off the stated hard/typed domain. The deterministic +classifier bound [SC] (19) proves integrability: if x=-s>0 and n>0, then +x<=2|B|+(48kD^2)^(1/3), and + + integral_s w_+ 1{n>0} <=384k^2 |B|^3+2304k^3 D^2. + +The remaining hard spectral factor is a polynomial, while h0 has uniform +Gaussian decay in the ORIGINAL orthogonally rotated raw variables. All angular +variables remain inside the integral. Positive Gaussian density on open typed +nonempty sectors gives mu_fail(total)>0. In [SC] (20)'s notation its mass is + + a_fail=a1+a2. (S2) + +This consumes the displayed deterministic integral, not [SC]'s global count +limit. Its remote singleton coefficient beta_far does not enter S1 or S2. + +Theorem F (full fixed-dimensional selector-failure law). Under the exact +source interfaces and H1, in the extended spectral law of §2, + + r^-3 Q_r^W(Theta_r in dot, F_r) -> mu_fail in total variation, + (1-p_r)/r^3 -> a1+a2>0. (S3) + +Proof. On a fixed bounded spectral box with hard eigenvalues bounded below, +[SC] §2 disintegrates the actual additional full jet. Its soft eigenvalue +change has Jacobian r c_m J_r, where + + J_r=product_(j>=2)(h_j+rs) product_(2<=i product h_j^2 w_+. Its limiting +weight is zero off the typed domain and ON the typed boundary; selector +convergence is unnecessary there. For a typed generic target H1 gives the +actual indicator I=1_F eventually equal to 1{n>0}. The excluded algebraic +sets are null, not discarded positive mass. + +The independent complete-jet coupling [SC] (5)–(6) gives +K<=C_box(1+||F||C4). Its two-short-column bound [SC] (15) bounds W_r/r^4 by an +integrable fixed polynomial in that coupling norm on the box. Thus pointwise +convergence, the exact weight limit, and dominated convergence give compact +L1 convergence of S4 to S1, including near the typed boundary. Repeated hard +spectra are null; no uniform inverse-gap estimate is required on the box. +E4–E7 exhaust the ACTUAL failure measure, and S1 is integrable. First exhaust +bounded boxes and then let the positive hard lower bound decrease to zero. +The limsup of both excluded tails tends to zero. Compact L1 plus those two +tails is global L1, which is precisely the total variation statement S3. +Taking total masses proves its coefficient. QED. + +This establishes the pairing relevance of the microscopic soft geometry. +It does not equate two extra saddle witnesses with one maximum/saddle pair. +Neither a factorial moment nor fixed-remote mixing is used to infer selection. +When the fixed-r almost-sure global Morse/distinct-value locus is used in this +conditional coupling, take a countable intersection along an arbitrary fixed +sequence r_j->0. Dominated convergence along every such sequence proves the +stated limit. No common probability-one locus for uncountably many pinned laws +is assumed. + +## 6. Actual replacement location, death and lifetime + +On F_r let T_r be the actual elder partner's displacement from the midpoint, +in the local torus chart, divided by r. Use an isolated sentinel if the partner +is essential or outside that chart. For the same reason use a sentinel in D_r +when d_f(M) is not finite. These exceptions have r^-3 mass tending to zero: +on each regular compact jet sector H1 provides a local older path and actual +partner for all sufficiently small r; E4–E7 exhaust the remaining failure mass. + +Theorem M (actual marked law). The finite measures + + r^-3 Q_r^W((Theta_r,T_r,D_r) in dot, F_r) + +converge WEAKLY to the pushforward of S1 under + + Theta -> (Theta,T_*(Theta),h_*(Theta)). (M1) + +The conditional-on-failure law is M1 divided by a_fail. The lifetime mark +(b-d_f(M))/r^3 converges in that law to -h_* in (0,k), and its fraction of the +candidate lifetime converges to -h_*/k in (0,1). + +Proof. At a generic positive hard target H1 identifies the exact actual +winning continued root. Off the additional null set D=0, [LOCAL] §6's winning +soft root is unique; continuation and the vanishing r-scaled hard graph give +H2 and D_r->h_*. Insert any bounded continuous joint test function in S4. +The same compact dominated-convergence argument proves convergence of its +integral. E4–E7 remove the tails; sentinel mass has already been excluded. +No continuity across the polynomial transition sets is assumed. QED. + +Weak, not total variation, convergence is claimed for these real-valued marks. +Tightness of M1 also gives, for EVERY deterministic delta_r->0 with +delta_r/r->infinity, + + Q_r^W(F_r, dist(actual elder partner,midpoint)>delta_r)=o(r^3). (M2) + +For a given tolerance choose a fixed large radius with arbitrarily small +limiting marked tail, use weak tightness including the sentinel, then use +delta_r/r eventually larger than that radius. This is actual failed-partner +localization, rather than localization of a count-defined witness. + +## 7. Exact compact lifetime-density consequence + +Retain [P] §§10–12's exact compact population: birth b in an interval B, gap k +in an interval K, both of positive length and K bounded away from zero, axial +orientation u in S^(d-1) with ordinary area measure, per unit midpoint volume. +Choose a Borel transverse completion R(u) as in the source. The coefficient +a_fail is independent of that completion: the original selection probability +is physical and independent of a transverse coordinate choice, and S3 is its +unique limit. This does not assert torus rotational invariance or birth-factor +cancellation in higher dimensions. + +Use the source's ACTUAL radial ledger, in every fixed d: + + A_r=12 pi_r(R(u);v_r) Z_r/r^2, + nu_cand(ell)=ell^-1/3 integral_(B x K x S^(d-1)) + A_((ell/k)^(1/3))/(3k^(2/3)). + +The selected density has the additional p_r. The dimension powers have already +cancelled in [P] §10; no new spatial Jacobian or dimension-dependent lifetime +power may be inserted. [P] (7.8) supplies a common compact-mark bound on +(1-p_r)/r^3, and [P] (10.2)–(10.3) supply common bounds and A_r->A0. These are +existing domination interfaces, not uniformity inferred from pointwise H1. + +With r=(ell/k)^(1/3), the exact nonselected candidate density therefore has + + ell^-2/3 [nu_cand^(B,K)(ell)-nu_eld^(B,K)(ell)] + = integral_(B x K x S^(d-1)) + A_r/(3k^(5/3)) [(1-p_r)/r^3]. + +Dominated convergence and S3 identify + + nu_rej^(B,K)(ell) ~ C_fail^(B,K) ell^(2/3), + C_fail^(B,K)=integral_(B x K x S^(d-1)) + A0(b,k,u) a_fail(b,k,u)/(3k^(5/3)) db dk d sigma(u). (L1) + +C_fail is finite and strictly positive. The full z0 cancels if A0=12pi0z0 is +substituted into S1; there is still one original pin density and no additional +normalization. + +L1 is the compact candidate-minus-selected counting measure. It is not a +replacement-bar intensity obtained by counting all rejected candidates, nor a +standalone second-order selected-density expansion. An unrestricted refined +difference does not follow; its far rejected population is different. No new +k->0, d->infinity, volume, or escaping-mark uniformity is claimed. + +## 8. Hypotheses, explicit falsifiers and review boundary + +H1 assumes a generic typed cubic and its pinned reduced C2 convergence, an +embedded fixed soft collar, and a CONTAINED negative hard tube with drop D0>k. +The graph and tube are proved from [SC]'s actual smooth field on fixed positive +hard targets. The exact finite-r partner additionally uses the source's actual +global Morse distinct-value locus. A unique limiting position additionally +excludes D=0, a null set. The deterministic lemma does not require probability, +Morse–Smale, a separatrix assertion or control of the exterior. + +The stochastic statements require the original positive-spectrum field, +nonsingular contact/full-jet regression, independent endpoint-matrix residual +with all C4 moments, actual cap implication, double soft-factor weight bound, +full normalizer floor, and the original spectral density/coupling interfaces. +They are source-bound conditions, not consequences of tests or publication. +All inverse-hard constants are pointwise only. The actual rare failure tail +and multiple-soft exclusion are proved by E3–E7, rather than borrowed from a +near-count event. The full typed boundary is treated by its continuous zero +weight. The Haar-gauge extension is part of the precise measure statement. + +Falsifiers: + +- A full path bypassing a contained hard-depth cap at height above h_r, or a + graph-lifted moving chord whose exact minimum is not the continued root, + invalidates H1. The thin-tube counterexample in HARD_FIBRE_LEMMA §8 explains + why graph convergence alone is not a substitute for that hypothesis. +- A leading failure mass escaping every bounded midpoint jet set, or staying + at a nonvanishing fraction on h2<=epsilon as epsilon->0, contradicts E4/E7. + A defect in the parent cap implication, original residual independence or + retained matrix soft integral would reopen that analytic step. +- A dropped saddle mixed-square factor, extra restricted normalizer, omitted + hard/sign multiplicity or GOE substitution changes S1 and invalidates S3. +- A positive leading essential/sentinel mass contradicts M1. Total variation + for real-valued location/lifetime marks is outside the claim. +- Replacement-bar, unrestricted refined-density, new parameter-uniform or + numerical uses of L1 are outside this proof's interface. + +This is a new fixed-dimensional actual elder/failure/lifetime candidate, with +full proofs and source identities exposed. d=2 remains the separate [LOCAL] +scalar proof. No controlling acceptance, status, graph, prize, Boolean, parent +proof or source history is altered. Qualified nonauthor review must bind this +successor itself; acceptance of a count packet or of [LOCAL] alone is not an +acceptance of this higher-dimensional lift. diff --git a/frontiers/concave_fibre_elder_20260930/README.md b/frontiers/concave_fibre_elder_20260930/README.md new file mode 100644 index 000000000..cd78f41c8 --- /dev/null +++ b/frontiers/concave_fibre_elder_20260930/README.md @@ -0,0 +1,43 @@ +# From the soft plane to the actual elder partner in fixed d>=3 + +[PROOF.md](PROOF.md) extends the planar actual-pair theorem through negative +hard fibres and identifies the full higher-dimensional selector-failure law. +This is an additive mathematical candidate, AUTHOR_SIDE / HOLD, conditional +on the exact public source interfaces and pending qualified nonauthor review. + +The geometric step is a contained hard tube of width r^(3/2): its height drop +matches the r^3 death window and closes every transverse escape. The actual +critical graph itself has hard displacement O(r^2), which is too narrow to +provide that barrier. The full proof and an explicit thin-tube falsifier are +in [HARD_FIBRE_LEMMA.md](HARD_FIBRE_LEMMA.md). Graph-lifted critical chords and +thickened compact planar caps identify the actual global merge saddle as the +highest continued local window saddle for all sufficiently small r. + +Retaining the residual/hard-jet tail mark in the parent's endpoint-matrix +integral exhausts the ACTUAL failure measure. No count event or factorial bound +is substituted. It gives the full extended spectral-jet failure measure in +total variation, coefficient (1-p_r)/r^3 -> a1+a2, and the weak actual +replacement-location/death/lifetime law. The remote singleton count coefficient +does not enter. Actual failed partners localize inside every shrinking cutoff +whose ratio to r tends to infinity. + +The exact compact birth/gap candidate-minus-selected density consequently has +an identified positive ell^(2/3) coefficient in every fixed dimension. This is +the parent's exact universal radial ledger, not a new dimension-dependent +power, a replacement-bar counting formula, or a standalone second-order +selected-density expansion. + +[SOURCE_INTERFACE.md](SOURCE_INTERFACE.md) displays the analytic graph and full +matrix-tail derivations. [SOURCES.json](SOURCES.json) links all 11 full public +sources with immutable identities and separates required inputs from context. +[RECONNAISSANCE.md](RECONNAISSANCE.md) records the limited primary-source +comparison without a novelty claim. [NONAUTHOR_REVIEW.md](NONAUTHOR_REVIEW.md) +preserves the initial and intermediate AMEND findings and the final conditional +source-scoped ACCEPT of the corrected exact prose. It supplies zero +organizational-independence credit; qualified external review remains pending. + +All current contributors are OpenAI, with zero organizational-independence +credit. No existing proof, count packet, register, graph, source status, prize, +Boolean, workflow or active peer branch is changed. Uniformity in varying d, +volume or k->0, unrestricted refined lifetime differences and numerical +coefficients remain outside this note. diff --git a/frontiers/concave_fibre_elder_20260930/RECONNAISSANCE.md b/frontiers/concave_fibre_elder_20260930/RECONNAISSANCE.md new file mode 100644 index 000000000..b6511fb8a --- /dev/null +++ b/frontiers/concave_fibre_elder_20260930/RECONNAISSANCE.md @@ -0,0 +1,32 @@ +# Primary-source reconnaissance for the hard-fibre elder step + +30 September 2026, OpenAI author-side reconnaissance. No novelty or literature +priority claim. This is evidence of the actual access depth, not acceptance. + +The classical comparison is reduction along nondegenerate Hessian directions. +The primary abstract of Guangcun Lu, *The splitting lemmas for nonsmooth +functionals on Hilbert spaces I*, arXiv:1211.2127v2, +https://arxiv.org/abs/1211.2127v2, was read. It discusses a splitting theorem +and critical-group results near a critical point under weaker smoothness. Only +the author abstract and bibliographic metadata were inspected; its 68-page +proof was not read and no theorem from it is used in this packet. + +Searches also exposed Golubitsky–Marsden's *The Morse Lemma in Infinite +Dimensions via Singularity Theory*. The Ohio State reprint URL and Caltech +author-record URL returned restricted-fetch errors in the available public +retrieval service. No full-source exposure or proof consumption is claimed for +those attempts, and no alternate credential or access path was used. + +The inference guiding this packet is narrower than a splitting theorem: +critical-point reduction alone does not determine which labelled maximum +merges in the arbitrary exterior. The new argument proves its own Schur +completion, fibre concavity drop, compact full-dimensional cap and graph path. +HARD_FIBRE_LEMMA §8 explicitly falsifies elder transfer from reduced graph +convergence alone. No black-box splitting lemma supplies the hard-side depth. + +All mathematical dependencies actually consumed are the full public repository +sources in SOURCES.json, read at their exact immutable identities. SC supplies +the local analytic graph but explicitly excludes elder selection; the new +barrier is therefore a separately reviewed consumer step. The retained matrix +tail and actual-pair lifetime pushforward are proved in PROOF.md and +SOURCE_INTERFACE.md rather than inferred from a count theorem or a paper title. diff --git a/frontiers/concave_fibre_elder_20260930/SOURCES.json b/frontiers/concave_fibre_elder_20260930/SOURCES.json new file mode 100644 index 000000000..f072e1bb5 --- /dev/null +++ b/frontiers/concave_fibre_elder_20260930/SOURCES.json @@ -0,0 +1,121 @@ +{ + "repository": "d6g8k5htny-coder/Math-", + "public_main": "ab13a08f5e5b0adc7a7d80cf643d9b5a0618507f", + "planar_pr": 170, + "planar_head": "79f18f0cb318fceccd5bdf4e6dad29815165bc7d", + "scientific_effect": "NONE", + "review_independence_credit": 0, + "sources": [ + { + "id": "SC", + "commit": "ab13a08f5e5b0adc7a7d80cf643d9b5a0618507f", + "path": "frontiers/spectral_cluster_closure_20260929/PROOF.md", + "git_blob": "16c56821b52fd76b0be791622b9c3809eafde75a", + "url": "https://github.com/d6g8k5htny-coder/Math-/blob/ab13a08f5e5b0adc7a7d80cf643d9b5a0618507f/frontiers/spectral_cluster_closure_20260929/PROOF.md", + "bytes": 25006, + "sha256": "e971b2cbe50a8a06b47c1219191201e0d1037c9adac23e5e3b7d2051bb70c2eb", + "role": "required: \u00a7\u00a72,5,6 raw/full jet disintegration, orthogonal spectral Jacobian, actual hard graph C2 convergence, continuous typed weight, deterministic integral; global count law NOT consumed" + }, + { + "id": "CUB", + "commit": "ab13a08f5e5b0adc7a7d80cf643d9b5a0618507f", + "path": "frontiers/planar_cubic_cluster_20260929/PROOF.md", + "git_blob": "bb446d08db8a944537a743ad550b88c1c2ad5758", + "url": "https://github.com/d6g8k5htny-coder/Math-/blob/ab13a08f5e5b0adc7a7d80cf643d9b5a0618507f/frontiers/planar_cubic_cluster_20260929/PROOF.md", + "bytes": 19889, + "sha256": "117e9299a71e6139270266889eb772ed97518e402d9af029bbdb67caf9d4a0f0", + "role": "required: displayed original planar cubic, exact classifier and polynomial null sets; count expectations NOT consumed" + }, + { + "id": "EDL", + "commit": "ab13a08f5e5b0adc7a7d80cf643d9b5a0618507f", + "path": "frontiers/elder_dimension_lift_20260928/PROOF.md", + "git_blob": "7303bd791a68a1139251f0f6e403a9f7cc89b006", + "url": "https://github.com/d6g8k5htny-coder/Math-/blob/ab13a08f5e5b0adc7a7d80cf643d9b5a0618507f/frontiers/elder_dimension_lift_20260928/PROOF.md", + "bytes": 23971, + "sha256": "b529fe3780e1909014b3cb144b9a74156d976bbdc19b6711d0c5b1a1da9e5669", + "role": "context only: preceding actual root/index interface; no count or pairing conclusion consumed" + }, + { + "id": "DL", + "commit": "ab13a08f5e5b0adc7a7d80cf643d9b5a0618507f", + "path": "frontiers/d5_dimension_lift_20260929/PROOF.md", + "git_blob": "9d82c707fdb17d3072a8930f26dabedf59e456fc", + "url": "https://github.com/d6g8k5htny-coder/Math-/blob/ab13a08f5e5b0adc7a7d80cf643d9b5a0618507f/frontiers/d5_dimension_lift_20260929/PROOF.md", + "bytes": 53727, + "sha256": "6fb94b247e8e45bca9dc02f46670ac6029fb54e0ef906001efe48fe908549b80", + "role": "scope audit only: dimension-lift count result excludes elder selection; no count conclusion consumed" + }, + { + "id": "LOCAL", + "commit": "79f18f0cb318fceccd5bdf4e6dad29815165bc7d", + "path": "frontiers/local_elder_geometry_20260930/PROOF.md", + "git_blob": "ef2aa57959ea9f721bbf2316ce94cf616c1c9113", + "url": "https://github.com/d6g8k5htny-coder/Math-/blob/79f18f0cb318fceccd5bdf4e6dad29815165bc7d/frontiers/local_elder_geometry_20260930/PROOF.md", + "bytes": 39722, + "sha256": "f68038be79b46124b0f9b31205aa6e3682b34b6f5ef81f4a5697ae81f07cc46b", + "role": "required: Theorem E compact planar collar and moving critical chords; position uniqueness off D=0; draft at exact stated source scope" + }, + { + "id": "P", + "commit": "ab13a08f5e5b0adc7a7d80cf643d9b5a0618507f", + "path": "imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md", + "git_blob": "dfed3b8d318a3ab1950957f393307733a4bef3f2", + "url": "https://github.com/d6g8k5htny-coder/Math-/blob/ab13a08f5e5b0adc7a7d80cf643d9b5a0618507f/imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md", + "bytes": 40261, + "sha256": "9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7", + "role": "required: endpoint matrix density/residual, double soft-factor bound, full Z, global cap-failure inclusion, genericity/Borel and compact lifetime ledger" + }, + { + "id": "ELDERD", + "commit": "ab13a08f5e5b0adc7a7d80cf643d9b5a0618507f", + "path": "frontiers/elder_lower_all_d_20260929/PROOF.md", + "git_blob": "7f41c9e315be0a7985d4c770a11a2cdf717bd46a", + "url": "https://github.com/d6g8k5htny-coder/Math-/blob/ab13a08f5e5b0adc7a7d80cf643d9b5a0618507f/frontiers/elder_lower_all_d_20260929/PROOF.md", + "bytes": 16485, + "sha256": "88c6bfc7973fe832918f91e2ed1f47da3e51987ed9efc1a99648e82b2eb119e5", + "role": "context only: preceding elder-failure lower event; not used as a coefficient or upper barrier" + }, + { + "id": "ERR", + "commit": "ab13a08f5e5b0adc7a7d80cf643d9b5a0618507f", + "path": "imports/lifetime_parent_20260925/ERRATUM_CONGRUENCE.md", + "git_blob": "213594d6ca6a86fb938110f4d166d9ce275a02d0", + "url": "https://github.com/d6g8k5htny-coder/Math-/blob/ab13a08f5e5b0adc7a7d80cf643d9b5a0618507f/imports/lifetime_parent_20260925/ERRATUM_CONGRUENCE.md", + "bytes": 1782, + "sha256": "bad7ef609c4ad8c41ad6af562c1b6807921e19a9d556ed793ad1a0db6e202028", + "role": "required reading rule: endpoint congruence correction" + }, + { + "id": "BOREL", + "commit": "ab13a08f5e5b0adc7a7d80cf643d9b5a0618507f", + "path": "reviews/d1_section9_borel_repair_20260925/REPAIR.md", + "git_blob": "fe9b9ce4999908bb3814b500ee2d0ceb0c6f704a", + "url": "https://github.com/d6g8k5htny-coder/Math-/blob/ab13a08f5e5b0adc7a7d80cf643d9b5a0618507f/reviews/d1_section9_borel_repair_20260925/REPAIR.md", + "bytes": 9062, + "sha256": "845abf9f9c99d672c2a10a887b5a2e7206a3d2de3d876f35f75ff6e2dc13e62f", + "role": "required reading rule: whole-field Borel weighted Kac-Rice repair" + }, + { + "id": "REC", + "commit": "ab13a08f5e5b0adc7a7d80cf643d9b5a0618507f", + "path": "reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md", + "git_blob": "75da2597971510f843f8d90c743950cb8c177342", + "url": "https://github.com/d6g8k5htny-coder/Math-/blob/ab13a08f5e5b0adc7a7d80cf643d9b5a0618507f/reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md", + "bytes": 23312, + "sha256": "451b9d7ffee072a73fc904cab891b6693e3f233808b89df10cce1b57036b65da", + "role": "required reading rules and reviewed source scope: W1 convergence-in-law and embedded-chart radius" + }, + { + "id": "CAP", + "commit": "ab13a08f5e5b0adc7a7d80cf643d9b5a0618507f", + "path": "imports/lifetime_parent_20260925/MARKED_CYLINDER_CAP_PROOF.md", + "git_blob": "0633aca3c2a2882b0de4399da0a75d64c2e6b2e1", + "url": "https://github.com/d6g8k5htny-coder/Math-/blob/ab13a08f5e5b0adc7a7d80cf643d9b5a0618507f/imports/lifetime_parent_20260925/MARKED_CYLINDER_CAP_PROOF.md", + "bytes": 15160, + "sha256": "0bf922b9203c29088b12388807aa0e2ecd020485eb0f6e919679841b5b2636fc", + "role": "required: deterministic global good-cap selection implication" + } + ], + "source_exposure": "Full public immutable sources. Required interfaces remain conditional on their displayed assumptions and actual review scope. Context sources are not mathematical premises." +} diff --git a/frontiers/concave_fibre_elder_20260930/SOURCE_INTERFACE.md b/frontiers/concave_fibre_elder_20260930/SOURCE_INTERFACE.md new file mode 100644 index 000000000..7eb203bdf --- /dev/null +++ b/frontiers/concave_fibre_elder_20260930/SOURCE_INTERFACE.md @@ -0,0 +1,191 @@ +# Source-interface audit for a higher-dimensional elder bridge + +Read-only source audit, 30 September 2026. Same-provider OpenAI contributor; zero organizational-independence credit. No mathematical acceptance, scientific-status transition, existing-proof modification, PR action, or count-law promotion is asserted. The analytic lemmas reconstructed below are new author-side consumer steps requiring source-bound review. + +## 1. Exact public source cut + +Public `Math-/main` readback was `ab13a08f5e5b0adc7a7d80cf643d9b5a0618507f`. Public PR170 is an open draft at head `79f18f0cb318fceccd5bdf4e6dad29815165bc7d`, branch `codex/local-planar-elder-f68038be`. All listed files were fetched in full from the exact public commit. The scratch copies in `sources/` have been checked against the public Git blob identities, including UTF-8 byte lengths. Existing mutable source maps were not changed. + +| Tag | Exact path | Git blob | Bytes | Interface consumed | +|---|---|---|---:|---| +| SC | `frontiers/spectral_cluster_closure_20260929/PROOF.md` | `16c56821b52fd76b0be791622b9c3809eafde75a` | 25006 | §§2,5,6: raw midpoint regression, orthogonal spectral chart, physical anisotropic normal form, hard slaving, full weight, local spectral kernel and its integrability. Its count exhaustions are not premises. | +| CUB | `frontiers/planar_cubic_cluster_20260929/PROOF.md` | `bb446d08db8a944537a743ad550b88c1c2ad5758` | 19889 | C1–C15, Theorem C and Lemma S: original-coordinate cubic, classifier, stable roots, shear only for algebra. | +| EDL | `frontiers/elder_dimension_lift_20260928/PROOF.md` | `7303bd791a68a1139251f0f6e403a9f7cc89b006` | 23971 | Explanatory context only: A7–A28 compare physical jets, bounded shear charts and actual root/index constructions. SC supplies the orthogonal graph interface used here; no EDL count or pairing conclusion is a premise. | +| ELDERD | `frontiers/elder_lower_all_d_20260929/PROOF.md` | `7f41c9e315be0a7985d4c770a11a2cdf717bd46a` | 16485 | Context only: soft eigenplane path gives an elder-failure lower event, without an upper barrier or actual replacement partner. | +| DL | `frontiers/d5_dimension_lift_20260929/PROOF.md` | `9d82c707fdb17d3072a8930f26dabedf59e456fc` | 53727 | Scope audit only: §1.3 expressly excludes elder selection. No count/first-moment conclusion is consumed. | +| P | `imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md` | `dfed3b8d318a3ab1950957f393307733a4bef3f2` | 40261 | §§3–8: endpoint matrix density, independent full-field residual, original weight and full normalizer, cap-failure inclusion, genericity and maximin; §§10–12: exact compact radial/lifetime ledger and its domination interfaces. | +| CAP | `imports/lifetime_parent_20260925/MARKED_CYLINDER_CAP_PROOF.md` | `0633aca3c2a2882b0de4399da0a75d64c2e6b2e1` | 15160 | §§1–5: deterministic all-dimensional good-cap implication. | +| ERR | `imports/lifetime_parent_20260925/ERRATUM_CONGRUENCE.md` | `213594d6ca6a86fb938110f4d166d9ce275a02d0` | 1782 | Corrected endpoint congruence in P §5. | +| BOREL | `reviews/d1_section9_borel_repair_20260925/REPAIR.md` | `fe9b9ce4999908bb3814b500ee2d0ceb0c6f704a` | 9062 | Required whole-field Borel marked Kac–Rice replacement for P §9. | +| REC | `reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md` | `75da2597971510f843f8d90c743950cb8c177342` | 23312 | §1 reading rule; §5 W1 convergence-in-law clarification and embedding radius. | +| LOCAL | `frontiers/local_elder_geometry_20260930/PROOF.md` at PR170 head | `ef2aa57959ea9f721bbf2316ce94cf616c1c9113` | 39722 | Theorem E, §§3–6: planar compact collar and exact highest continued partner; §8 scalar failure exhaustion. SHA256 `f68038be79b46124b0f9b31205aa6e3682b34b6f5ef81f4a5697ae81f07cc46b`. | + +For the first ten rows the immutable URL is `https://github.com/d6g8k5htny-coder/Math-/blob/ab13a08f5e5b0adc7a7d80cf643d9b5a0618507f/` followed by the path. For LOCAL replace the commit with `79f18f0cb318fceccd5bdf4e6dad29815165bc7d`. `SOURCES.json` gives complete URLs and SHA256 values. + +## 2. The supplied analytic graph interface + +Fix d≥3, m=d−1, one original axial frame, b∈R, k>0, and a midpoint spectral target. In SC's orthogonal coordinates + + A_mid = O diag(rs,−h2,…,−hm) Oᵀ, + 00 and fixed coupling C4 bound K, Taylor gives + + f_ww ≤ −h_min I/2, + |f_w(t,0)| ≤ C r², + |f_tw(t,w)| ≤ C r. + +The graph follows from strict concavity and the inward hard radial derivative. Implicit differentiation gives `|zeta_r|≤Cr²`, `|D_t zeta_r|≤Cr`, and `|D_t² zeta_r|≤C`. For `psi_r(t)=f(t,zeta_r(t))`, define `delta_r=psi_r(t)−f(t,0)`. Then + + |delta_r|≤Cr⁴, + |D_t delta_r|≤Cr³, + |D_t² delta_r|≤Cr². + +The Hessian identity used in the last bound is + + D_t² psi_r = f_tt−f_tw f_ww^(−1) f_wt + +evaluated on the graph. Each rescaled soft derivative contributes one factor r. Hence `(psi_r(rX,rZ)−b)/r³−(f(rX,rZ,0)−b)/r³=O(r)` in C². Inverse-hard constants are allowed at a fixed positive hard target; they must not be placed in the failure-tail majorant below. + +Since the original hard gradients vanish at each pin and the hard graph is unique, `zeta_r(M)=zeta_r(S)=0`. The reduced potential retains the exact critical pins and values 0,−k. Nondegenerate reduced critical points are actual full roots on the graph. Block congruence gives + + index(H_full)=(d−2)+index(H_reduced). + +Thus CUB's window saddles lift to actual index-(d−1) roots, and their hard coordinates are r² times `diag(h)^(−1)Q+o(1)`. Their physical coordinates divided by r tend to `(X,O(Z,0))` in the original axial/transverse frame. + +EDL's distinct construction uses the bounded determinant-one shear `y=(z,w−qz)` with q=D^(−1)v. Its original physical r-scaled location is `(X,Z,−qZ)` after the axial frame, not `(X,Z,0)`. In that chart sigma, not the raw a entry of A, is the soft curvature. Both SC's orthogonal chart and EDL's determinant-one shear preserve criticality, inertia and Hessian determinants; a general invertible linear change would introduce its squared determinant factor. SC's orthogonal chart is the appropriate global norm-controlled chart here. CUB's separate planar shear `u=X+aZ/(12k)` is only an algebraic change; reported physical X must be recovered as `u−aZ/(12k)`. + +## 3. Exact missing topological consumer step + +LOCAL Theorem E is stated on surfaces. It cannot simply be cited as a theorem about the full d-dimensional field. The new consumer needs to thicken its compact planar collar and control every hard boundary exit. + +The graph profile alone on an r²V box is insufficient. Hard side boundaries at that scale have a height drop of order r⁴, smaller than the r³ death window. A correct thickening uses a larger hard radius, for example `rho_r=A r^(3/2)` centered on zeta_r. Strict hard concavity yields + + f(t,w) ≤ psi_r(t)−(h_min/4)|w−zeta_r(t)|². + +Choose A with `h_min A²/4>k`. For every planar collar disk K_(r,h) supplied by the LOCAL §§4–6 construction for the actual reduced profile, psi_r≤b inside and psi_r=b+r³h on its boundary. The graph-centered hard tube over K_(r,h), of radius rho_r, is contained in the local chart for small r. Its soft boundary has height ≤b+r³h and its hard side boundary has height 0`, a witness event, or any remote-count estimate. + +Let `F_r={actual global ordinary partner of M is not S}` and let `B=−D_y²f(M)>0` on typed support. Order its eigenvalues + + 0[4/(3k)]r M3², r M4≤3k/10}. + +The fourth-derivative exception has tilted mass O(r⁴) by P (7.7) and the full floor (5.5), hence has zero r^(−3) limit. On the remaining depth branch, + + lambda1≤D rU². + +P (6.2), with its second soft factor retained, gives + + W_r ≤ C r² U^(2m) lambda1(lambda1+C rU). + +The endpoint matrix density has the Gaussian bound P (3.5). Its spectral Jacobian is bounded by `C Lambda^v`; the hard angular volume is finite. For fixed J and lambda2,…,lambdam, U is independent of lambda1. Thus for any retained event E depending only on J and the hard eigenvalues, + + E_Q[W_r;depth,E] + ≤ C r² E_J ∫ e^(−c sum_hard lambda_j²) Lambda^v U^(2m) + 1_E ∫_0^(DrU²) lambda1(lambda1+C rU) d lambda1 d lambda_hard + ≤ C r⁵ E_J ∫ e^(−c sum_hard lambda_j²) + Lambda^v U^(2m+6) 1_E d lambda_hard. (T1) + +The positive majorant permits extension of the lambda1 domain beyond its actual ordered interval; the Gaussian lambda1 factor can be dropped. The integral is exactly the r³ soft integral before the outer r² weight. Divide by the original full `Z_r≥z_*r²` once. + +With `E={U>A}`, every higher J moment and Gaussian polynomial integrability give, for every fixed p>0, + + limsup_(r→0) r^(−3) Q_r^W(F_r,U>A) ≤ C_p A^(−p). (T2) + +This follows directly from `U^q 1{U>A}≤A^(−p)U^(q+p)`, q=2m+6. It requires no common residual law for every r; the uniform moment bounds suffice. + +With `E={lambda2≤eta}`, averaging J's moments leaves an ordinary integrable Gaussian polynomial over the ordered positive hard eigenvalues. Its mass on the lambda2 strip tends to zero (a bound C eta for eta≤1 suffices). Consequently, + + lim_(eta→0) limsup_(r→0) + r^(−3) Q_r^W(F_r,lambda2≤eta)=0. (T3) + +This handles all higher-corank intersections in measure and never divides by a hard eigenvalue. It is a failure-measure statement, stronger for this purpose than SC §4's near-occurrence tail. + +## 5. Endpoint-to-midpoint conversion + +Let `mu1≤…≤mum` be the signed eigenvalues of `−D_y²f(0)`. Hessian Lipschitz control and Weyl's inequality give + + |muj−lambdaj|≤r M3/2≤C rU. + +With SC's midpoint variables `s=−mu1/r`, `h_j=mu_j` for j≥2 and rotated complete tensor tau, the depth branch satisfies + + |s|≤D U²+C U, + |h|+|tau|+K≤C U. (T4) + +T2 therefore implies full failure tightness in the actual midpoint spectral jets and in K. No replacement of the endpoint density by a midpoint density occurred in this tail argument. + +On U≤A, midpoint `h2≤eta` implies endpoint `lambda2≤2eta` for all sufficiently small r at each fixed eta,A. T3 then gives + + lim_(eta→0) limsup_(r→0) + r^(−3) Q_r^W(F_r,h2≤eta)=0. (T5) + +The error from U>A is sent to zero by T2 and the M4 exception is o(r³). In particular midpoint hard eigenvalues that are negative can carry no unidentified leading failure mass. Repeated hard eigenvalues need no inverse-gap estimates: the spectral chart boundary is null; on each compact sector its Jacobian is bounded and vanishes at a collision. Positive hard lower bounds are used only for pointwise graph convergence and removed using T5. + +For d=2/m=1, retain LOCAL §8's existing scalar near/far split and tail proof; T1 cannot be used with Lambda fixed because Lambda=lambda1. + +## 6. Exact resulting marked-law interface, conditional on the new geometry + +SC §2 disintegrates the raw physical midpoint (A,T) law, with density h_r→h_0. Its ordered orthogonal spectral transformation contributes `r c_m J_r`, where + + J_r=prod_(j≥2)(h_j+rs) prod_(2≤i0 the original typed weight has + + W_r/r⁴ → prod_(j≥2)h_j² w_+(s,a,beta), + w_+=9k²[B−2s]_+[−B−2s]_+, B=beta−a²/(12k). + +The continuous determinant-weight limit is zero outside the typed domain and on its boundary; no selector convergence is needed there. The full normalizer is P (5.4), with ERR and REC's W1 reading rule. For any bounded failure multiplier the exact scaled disintegration is + + (c_m r²/Z_r) J_r h_r(O diag(rs,−h)Oᵀ,Rot_O tau) + E[(W_r/r⁴) multiplier]. (T6) + +There is one raw soft-coordinate Jacobian r, one original W_r, and one full Z_r. On compact jets SC (6) and the two short-column determinant bound SC (15) provide an integrable coupling envelope without using a count event. Conditional on the deterministic fibre bridge, pointwise failure convergence is `1_F→1{n>0}` off LOCAL's polynomial null sets. The actual death and location converge to h_* and the winning physical root. Dominated convergence proves the compact marked failure law. T2–T5 exhaust the actual failure measure, so no near-occurrence exhaustion is substituted. + +The candidate finite limiting failure measure is + + dmu_fail = 1{n(s,a,beta,c)>0} (c_m/z0) + h_0(O diag(0,−h)Oᵀ,Rot_O tau) + prod_(j≥2)h_j³ prod_(2≤i Date: Wed, 30 Sep 2026 04:23:35 -0500 Subject: [PATCH 2/5] Add conditional actual elder-extreme lifetime law and companion exponent thirteen New once-per-elder consumer of the exact PR170/175 actual marked-failure interfaces and PR166/169 microscopic root measure. Select the higher inner saddle rather than the maximum-radius anchor. Explicit selected radius coefficient, algebraic lifetime density and rational moments, fourth-power lower lifetime tail, and rho^11-reweighted companion law. Original r limit precedes all extreme limits; source candidates remain conditional, no status/graph promotion. Fresh41 tests per Python mode,893 rational shapes,12 direct inner Jacobians,6 semantic mutants per mode passed locally; all12 packet blob/tree identities matched. Historical source authentication remains hosted. Nonauthor analytic review open; no self-merge. --- .github/workflows/elder-partner-extremes.yml | 39 ++ .../MANIFEST.json | 73 ++++ .../elder_partner_extremes_20260930/PLAN.md | 29 ++ .../elder_partner_extremes_20260930/PROOF.md | 390 ++++++++++++++++++ .../elder_partner_extremes_20260930/README.md | 73 ++++ .../RECONNAISSANCE.md | 33 ++ .../RESULTS.json | 62 +++ .../SOURCES.json | 50 +++ .../VALIDATION.md | 45 ++ .../elder_partner_extremes_20260930/elder.py | 250 +++++++++++ .../test_elder.py | 265 ++++++++++++ .../test_verify.py | 94 +++++ .../elder_partner_extremes_20260930/verify.py | 110 +++++ 13 files changed, 1513 insertions(+) create mode 100644 .github/workflows/elder-partner-extremes.yml create mode 100644 frontiers/elder_partner_extremes_20260930/MANIFEST.json create mode 100644 frontiers/elder_partner_extremes_20260930/PLAN.md create mode 100644 frontiers/elder_partner_extremes_20260930/PROOF.md create mode 100644 frontiers/elder_partner_extremes_20260930/README.md create mode 100644 frontiers/elder_partner_extremes_20260930/RECONNAISSANCE.md create mode 100644 frontiers/elder_partner_extremes_20260930/RESULTS.json create mode 100644 frontiers/elder_partner_extremes_20260930/SOURCES.json create mode 100644 frontiers/elder_partner_extremes_20260930/VALIDATION.md create mode 100644 frontiers/elder_partner_extremes_20260930/elder.py create mode 100644 frontiers/elder_partner_extremes_20260930/test_elder.py create mode 100644 frontiers/elder_partner_extremes_20260930/test_verify.py create mode 100644 frontiers/elder_partner_extremes_20260930/verify.py diff --git a/.github/workflows/elder-partner-extremes.yml b/.github/workflows/elder-partner-extremes.yml new file mode 100644 index 000000000..77741c122 --- /dev/null +++ b/.github/workflows/elder-partner-extremes.yml @@ -0,0 +1,39 @@ +name: Elder-selected extreme partner checks + +'on': + pull_request: + paths: + - 'frontiers/elder_partner_extremes_20260930/**' + - '.github/workflows/elder-partner-extremes.yml' + workflow_dispatch: + +permissions: + contents: read + +jobs: + exact-and-source: + runs-on: ubuntu-latest + timeout-minutes: 10 + steps: + - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 + with: + persist-credentials: false + fetch-depth: 0 + - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 + with: + python-version: '3.11.16' + - name: Fetch exact public source commits + run: | + set -euo pipefail + git fetch --no-tags origin 80059a97cd8eb32d1a17a0ad9cb22cb2a0d7b337 + git fetch --no-tags origin 56a7904f9ad7d409c31e23195c0e7eeab230613a + git fetch --no-tags origin 79f18f0cb318fceccd5bdf4e6dad29815165bc7d + git fetch --no-tags origin 9c6a73489c5ed2465a3cf65dcc950eeeae074b05 + - name: Verify five source identities, packet and both Python modes + env: + PYTHONDONTWRITEBYTECODE: '1' + GIT_NO_REPLACE_OBJECTS: '1' + run: | + set -euo pipefail + python -B -S frontiers/elder_partner_extremes_20260930/verify.py + git diff --exit-code diff --git a/frontiers/elder_partner_extremes_20260930/MANIFEST.json b/frontiers/elder_partner_extremes_20260930/MANIFEST.json new file mode 100644 index 000000000..5bd8a7dba --- /dev/null +++ b/frontiers/elder_partner_extremes_20260930/MANIFEST.json @@ -0,0 +1,73 @@ +{ + "schema": 1, + "scientific_effect": "NONE", + "review_status": "NONAUTHOR_REVIEW_OPEN", + "files": [ + { + "path": "PLAN.md", + "bytes": 1796, + "sha256": "6f8fede899bfe6418aa488216e9205725b664ea0be8070c6a97b6705b7281bff", + "git_blob": "93c56e6f6b9064022f334cdeca9a7cd562bad124" + }, + { + "path": "PROOF.md", + "bytes": 17895, + "sha256": "db6a857879e5829c0da62e3812faa55be5c140589d6d800a479197c68cc8ddd7", + "git_blob": "91f88e392fb8aa947dac4fc81c2b45f783fa66cd" + }, + { + "path": "README.md", + "bytes": 3828, + "sha256": "99b70f116ed356e3590e661993f9647f9e7cbfd71edf48f8cca37399eacd65f5", + "git_blob": "8c3d59674c6e32e839c0977cc39593b2130fa923" + }, + { + "path": "RECONNAISSANCE.md", + "bytes": 1766, + "sha256": "5558e541cb2c7f345ac60f38bfa286e48970b228a8dabdea435138713b078569", + "git_blob": "8a4f041bca4a56e2cdbdf4fba89d4cd10a22b7a6" + }, + { + "path": "RESULTS.json", + "bytes": 1719, + "sha256": "eae217e61a9bc13c808cae70ec5fa84fe0c3f88b4c73b388c1affd104114c694", + "git_blob": "7c401595253885a6e18acfe9fd4a5829d667cf2f" + }, + { + "path": "SOURCES.json", + "bytes": 2335, + "sha256": "85cd74c67d8c728f255cf29346d7c99d021afb6e44282126df1df147a0260605", + "git_blob": "e32cf644404772f35e5415bf4d8af724274e5a4c" + }, + { + "path": "VALIDATION.md", + "bytes": 2894, + "sha256": "5affaf230824469a96b61a5c9d479e378f0b714e5b24a4523d30029cbb8b8c75", + "git_blob": "938346370dbd00247f0a64e0c332856db8542da4" + }, + { + "path": "elder.py", + "bytes": 9202, + "sha256": "88ef03d73be69963b913e3ea36be75fc25b5ebdf3f8f3f5d104d49022f9d6a10", + "git_blob": "9a97c39e647c49f0396d9ee2b94aab6fef1be713" + }, + { + "path": "test_elder.py", + "bytes": 12099, + "sha256": "bc9387f5145f9c8f3ea8e7d74f225a5d05ac666d0f947b320ace0efa70886364", + "git_blob": "6f9670e8894c3d515c9b2536be7753d1460fe8b0" + }, + { + "path": "test_verify.py", + "bytes": 5318, + "sha256": "b002a7a25a133e3ac656d8eec24f2b958ffe5f9c0f0bc8b462caaf26883302ef", + "git_blob": "bef9b1a72e79e783d120923218a0a736bc10112d" + }, + { + "path": "verify.py", + "bytes": 5179, + "sha256": "3f7ab71ff385355ea4b723cf08e3757e099f7f3564b500942d7518e3b8cbd50a", + "git_blob": "c00a24caaa25840e63fdc5b65cbbfd14f0717ebf" + } + ] +} diff --git a/frontiers/elder_partner_extremes_20260930/PLAN.md b/frontiers/elder_partner_extremes_20260930/PLAN.md new file mode 100644 index 000000000..93c56e6f6 --- /dev/null +++ b/frontiers/elder_partner_extremes_20260930/PLAN.md @@ -0,0 +1,29 @@ +# Execution record: elder-selected extreme marks + +Purpose: close the precise mismatch between maximum-radius sampling and actual +elder-partner sampling, using the existing explicit microscopic measure and +actual-partner weak-limit interfaces. Preserve all source hypotheses and the +r-then-t order of limits; no new status register or original-field rate. + +Design: identify the correct once-per-elder root sector; reuse the exact physical +root integral with that selector; integrate the selected height marginal by +polynomial elimination; analyze its small-height endpoint; reweight the explicit +doublet square law by the inner radius to identify the companion ratio tail. + +Execution is foreground and isolated in a new packet/branch. The repeated +owner autonomy directive supplies authority; no stopped agents or timers are +restarted. No other writer branch or frozen source proof is changed. + +Steps completed author-side: +- Read actual ELDER2/ELDERD marked-law interfaces and the root/companion sources. +- Derive the candidate formulas and publish a narrow coordination pickup. +- Write eight failing mathematical tests, implement exact controls, expand them. +- Write13 real-Git/inventory tests, observe20 scaffold failures, implement custody. +- Run41 tests in each Python mode and six semantic mutants per mode. +- Prepare exact source pins, reconstruction notes, result file and manifest. + +Publication requires a fresh main snapshot, complete packet readback and hosted +source/full-gate verification. Analytic review is separate: A source/selector +composition; B density/endpoints; C companion reweighting. The author will not +self-accept or self-merge. Old #169/#176 source-scoped reviews are not reviews of +this new consumer; their completed reviews have been handed to nonauthor integrators. diff --git a/frontiers/elder_partner_extremes_20260930/PROOF.md b/frontiers/elder_partner_extremes_20260930/PROOF.md new file mode 100644 index 000000000..91f88e392 --- /dev/null +++ b/frontiers/elder_partner_extremes_20260930/PROOF.md @@ -0,0 +1,390 @@ +# Distant actual elder partners: selection, lifetime fractions and the thirteenth-power companion tail + +**Object:** OA-ELDER-EXTREMES-20260930-v1. +**Author:** OpenAI / GPT-6 Astra Pro, foreground owner-authorized continuation. +**Disposition:** AUTHOR-SIDE CONDITIONAL CANDIDATE; NONAUTHOR REVIEW OPEN. +**Scientific effect:** NONE. No parent proof, register, Boolean, prize or earlier +verdict changes. This conversation authored the cluster sources; no independent +revalidation or organizational independence is claimed. + +## 1. The actual estimand and the two source interfaces + +Fix d>=2, L>0, b real, k>0 and an axial/transverse orthonormal frame. Use the +exact variance-one periodized field, original endpoint observations and the +one full determinant-tilted pair-Palm law Q_r^W of the sources. Write F_r for +failure of the prescribed saddle to be the ordinary elder partner of the +prescribed maximum. Let T_r be the ACTUAL replacement-partner displacement +from the midpoint divided by r and let + + lambda_r=(b-d_f(M))/(k r^3). (1) + +Out-of-chart or essential partners may be given an isolated sentinel. The +source interface says their probability on F_r is o(r^3). We do not identify +an arbitrary witness or farthest root with an elder partner. + +The two exact input types are deliberately separate: + +- **ELDER2:** PR170 at79f18f0cb318fceccd5bdf4e6dad29815165bc7d, + PROOF.md, Theorem E and Sections8.6-8.8. In d=2 it supplies the actual highest + local saddle, the full failure measure and its weak location/lifetime marks. +- **ELDERD:** PR175 at9c6a73489c5ed2465a3cf65dcc950eeeae074b05, + PROOF.md, H1/S1-S3/M1. In d>=3 it supplies the hard-negative-fibre bridge, + the extended spectral failure measure, and the actual weak marked law. +- **R:** PR166 RADIAL_TAIL.md at80059a97cd8eb32d1a17a0ad9cb22cb2a0d7b337, + R4-R13, supplies the exact root-resolved density of the limiting microscopic + measure and its Gaussian majorant. This is used to integrate the already + identified selector, NOT to establish actual elder pairing from counts. +- **C:** PR169 PROOF.md at56a7904f9ad7d409c31e23195c0e7eeab230613a, + E10-E25, supplies the deterministic companion/height map, inner/outer sectors + and exact shape integrals. Its whole-cluster maximum theorem is not used as + an elder theorem. +- **D:** COMPANION_RATIO.md at that same PR169 head, D1-D7, supplies the exact + unit-square density/height formulas. Only Section6 below needs this input. + +All complete commit/path/blob/SHA256 bindings are in SOURCES.json. ELDER2 and +ELDERD are distinct author-side source candidates with source-bound reviews; +this consumer is conditional on their displayed mathematical interfaces. It +neither promotes their status nor discharges a missing premise by citation. +The prior source proofs and review bodies remain unchanged. + +The common limiting microscopic measure is denoted M. Its restriction to +n>0, where n is the number of extra strict-window cubic saddles, is the finite +failure measure mu_F with mass a_F=a1+a2>0. It is NOT the global nonempty count +measure: remote singleton mass is absent. With theta=(s,h,O,tau), + + dM=(c_m/z0) H(h) h0(A0,Rot_O tau) + 9k^2(4s^2-B^2) ds dh dO dtau, (2) + +on the positive hard/typed domain. Here H is the ordered hard spectral +polynomial, A0=O diag(0,-h)O^T, B=beta-a^2/(12k), and s<-|B|/2. +The scalar case has empty hard products; a normalized soft sign-frame +augmentation changes no physical integral. There is one full z0 and no +additional pin density or root multiplicity. + +The actual interface is finite-measure weak convergence, with converging masses, + + r^-3 Q_r^W((T_r,lambda_r) in dot,F_r) + -> pushforward of mu_F by (T_*,eta_*), (3) + +where T_* is the root with GREATEST cubic height P, and eta_*=-P(T_*)/k. +Thus eta_* is the SMALLEST downward height among the window roots. +The assertion that this is the actual elder partner is precisely the elder +source premise, not a conclusion of the polynomial computations below. + +**Order:** first r->0. Then the radius threshold t->infinity inside (3)'s limit. +Any further small-lifetime or large-companion limit is taken third. No uniform +simultaneous limit, finite-r inverse moment, or full lifetime-intensity claim +is made. + +## 2. A once-per-elder selector with a fixed shape domain + +Use the root variables of R/C: + + u=X+aZ/(12k), b0=3-12u^2, v=(-s)Z^2/k, + S={-3/20 on S. (4) + +A counted companion is given, off an algebraic null set, by + + Lc=4v^2-8b0uv+b0^2, + t_c=(4v^2-b0^2)/Lc, + u_c=[2b0v-u(4v^2+b0^2)]/Lc, v_c=v t_c^2. (5) + +C proves that the map is an involution, t_c<0 on doublets, and that for an +outer-|Z| root eta_ct). Then + + **Theorem 1.** + G_eld(t) ~ C_cusp E0 t^-11, + mu_F(n=2,|T_*|>t) ~ C_cusp D t^-11. (9) + +For every fixed t>0 the radius event is a continuity set of the limiting +selected measure, and therefore + + lim_(t->infinity) t^11 lim_(r->0) + r^-3 Q_r^W(F_r, |T_r|>t, T_r finite)=C_cusp E0. (10) + +Conditional on a distant actual failed partner, in that same iterated order, +its lifetime fraction and selected shape have the universal laws in Section4. +This is candidate pair-Palm sampling given failure; it does NOT count each +replacement persistence bar once across different rejected candidates. + +Proof: inserting (7) into R's root integral gives exactly + + (108 k^7 c_m/z0) Q(u,v)1_E H(h)|Z|^-12 + h0(A0,Rot_O tau(a,a^2/(12k)+k b0/Z^2, + a^3/(144k^2)+a b0/(4Z^2)+2k(v-b0u)/Z^3,xi)) + du dv dZ da dxi dh dO. (11) + +The selector 1_E is independent of Z. The radius is still +|T_*|^2=(u-aZ/(12k))^2+Z^2. Under Z=t z it tends, after division by t, to +gamma(a)|z|. For t>=3 the radius condition implies |z|>1/(2gamma(a)). +The source majorant is a polynomial in h times + + Q 1_E |z|^-12 exp[-c(|h|^2+a^2+|xi|^2)] + 1{|z|>1/(2gamma(a))}. + +Integrating z costs only a factor proportional to gamma^11; the remaining +integral is finite. Dominated convergence yields the common C_cusp times the +shape mass E0. Restriction to counted doublets replaces E by the inner sector +and gives D. No hard-eigenvalue inverse or unproved radius ordering enters. + +For each t>0 and fixed u,a, the radius equation is a nonconstant quadratic in +Z with at most two solutions, hence null in (11). Thus |T_*| has no positive +atoms. Finite-mass weak convergence in (3), including negligible sentinels, +allows the unbounded exterior-radius indicator by Portmanteau. A bounded +continuous function of the other marks can be inserted as well, since its +only new discontinuity is that sphere. The denominator G_eld(t)>0 for all t, +by the positive tail at large t and monotonicity. This proves the fixed-t +conditional transfer and then (10). No uniformity in a moving t(r) is used. +QED. + +Some exact coefficient ratios, independent of the model amplitude, are + + G_eld(t)/F_point(t) -> E0/I=296269/657408, + G_eld(t)/G_max(t) -> E0/(I-D), + mu_F(n=2,|T_*|>t)/G_eld(t) -> D/E0. (12) + +They are approximately0.450662298,0.457796706,0.0345807201, respectively. +These are three different denominators. The final doublet probability concerns +the local cubic configuration of an extreme elder, not the global torus count. +The role of n here is entirely inside the limiting measure; no global-count +moment theorem is needed to identify the actual partner. + +For nonnegative powers, the radius of this selected limiting law has moment +threshold11, and + + integral min(|T_*|,t)^11 dmu_F ~11 C_cusp E0 log t. (13) + +The proof is Tonelli applied to (9). It is not uniform integrability of the +finite-r spatial moments in (3). + +## 4. An explicit universal lifetime-fraction density + +In the extreme-selected limit, the shape density is Q1_E/E0. The normalized +radius q=|T_*|/t is independently Pareto(11), with density11q^-12 on q>1; +its sign is symmetric and the remaining cusp parameters have their original +H gamma^11 h0/J_cusp density. This follows from (11) with q=gamma(a)|z|, +using the same majorant. Projecting to physical spatial marks gives WEAK +convergence. No assertion of spatial total variation is required. + +**Theorem 2.** Let e in(0,1). Define + + p_lo(e)=sqrt(1-e)-1/2, + p_hi(e)=cos((1/3) arccos(2e-1)). (14) + +Equivalently p_hi is the unique root in(1/2,1) of +2p^3-(3/2)p+1/2=e. The limiting fraction lambda=(b-death)/(k r^3) of a distant +failed elder partner has density + + f_eld(e)=(6/E0) integral_(p_lo(e))^(p_hi(e)) + Q(-p,6(e+p-1/2)) dp. (15) + +The integrand is a polynomial, so (15) is an explicit algebraic density with +one radical and one specified cubic root. It is strictly positive on(0,1). +This is a density of the LIMITING conditional mark, not an assertion that the +original fixed-r persistence intensity has this density or converges in TV. + +Proof: eta=e sets v=6(e+p-1/2), dv=6 de. The full shape region at fixed e gives + + sqrt(1-e)-1/2 < p < 1/2+sqrt(e). + +For p>1/2 write x=p-1/2. The lower shape condition becomes x^2=1 the entire +shape interval is outer. It follows that O2 removes exactly + + p_hi(e)1/2; +4cos^3(theta)-3cos(theta)=cos(3theta) gives (14). Nonnegativity, normalization +and strict positivity follow from the original selected shape integral. + +Every nonnegative integer moment is rational. To see this directly, integrate +Q(u,v)(u+1/2+v/6)^j over S and subtract the same polynomial integral over the +two strips (6), all of which have polynomial bounds and rational endpoints. +The first three unnormalized moments are + + E0=888807/280, + E1=3524743221/1361360, + E2=190490806059/87127040. + +Thus + + E[lambda]=1174914407/1440459878, + E[lambda^2]=63496935353/92189432192. (16) + +They are approximately0.8156522961481611 and0.6887658795940618. +Neither is the point-intensity nor the maximum-anchor lifetime mean. All +shape factors are universal in the fixed model parameters; directions and +C_cusp need not be universal. QED. + +For reproducible evaluation, with x=p-1/2 the unnormalized density integrand is + + 10368(e-x^2)(e+x^2+2x)(e+2ex+x^2). (17) + +Its integration endpoints are sqrt(1-e)-1 and the nonnegative root of +3x^2+2x^3=e. The companion uses rational bisection plus interval polynomial +evaluation to enclose (15), not unconstrained floating quadrature. + +## 5. A fourth-power small-lifetime law and its inverse-moment threshold + +**Theorem 3.** In the limiting probability law of Section4, + + f_eld(e) ~ (3328/E0)e^3, + P(lambda<=e) ~ (832/E0)e^4=(232960/888807)e^4, + f_eld(1-) =1312200/296269. (18) + +Consequently E[lambda^-p] is finite exactly for nonnegative p<4. At the critical +order, the capped inverse moment has asymptotic + + E[min(lambda^-1,T)^4] ~ (3328/E0)log T. (19) + +All three limits occur INSIDE the already-formed extreme-elder mark law: r->0, +then distant-partner radius->infinity, then e->0 (or T->infinity). Weak marked +convergence alone would not justify analogous finite-r inverse moments. + +Proof: use (17), put x=sqrt(e)z and divide the density numerator by e^3. The +lower endpoint tends to0, the upper to1/sqrt(3), and the integrand tends to + + 10368*2z(1-z^4). + +The scaled intervals lie in a fixed compact set for all small e and the +integrands have a common polynomial bound. Hence their limit integral is +10368(1/3-1/81)=3328. Integrating this density asymptotic gives the CDF formula. +At e=1 the integral of (17) over x in[-1,1/2] is98415/7; division by E0 gives +the endpoint in (18). Continuity and strict positivity away from zero then +show that only the lower endpoint controls inverse-moment integrability. +Finally lambda^-1 has tail coefficient832/E0 at exponent4; Tonelli gives +4*(832/E0)log T in (19). QED. + +## 6. The more distant companion has a thirteenth-power ratio tail + +This section conditions the limiting extreme-ELDER law further on a doublet. +Let rho=|Z_inner/Z_outer| in(0,1) and z in(0,1) be D's unit-square coordinates +of the OUTER root. Write L(rho,z) for D2's unnormalized density: + + L=165888 rho z^7(z+1)^4 (rho z+1)^4(rho z+rho+1)^7 + /[(rho+1)^5(2rho z+rho+1)^9]. (20) + +Its total mass is J. The elder is the inner root. C E18-E19 give the deterministic +change-of-variables identity + + Q(T)|det DT|=Q|t_c|^11, integral rho^11 L =D. + +**Theorem 4.** Under the limiting extreme elder law given a doublet, (rho,z) +has density + + rho^11 L(rho,z)/D. (21) + +It is NOT L/J. The scalar radial ratio q=|T_*|/threshold remains independent +Pareto(11). In physical positions divided by that threshold the configuration is + + { epsilon q e_*, -epsilon q rho^-1 e_* }, (22) + +where the first point is the actual limiting elder and the second the farther, +lower saddle. Its heights are respectively + + eta_eld=rho^3 z^2(z+1)(rho z+rho+2) + /[(rho+1)(2rho z+rho+1)], + eta_other=z^2(rho z+1)(rho z+2rho+1) + /[(rho+1)(2rho z+rho+1)]. (23) + +Let V=R_other/R_eld=1/rho in this limit, and H0=6401/3960. Then + + P(V>T | extreme elder, doublet) ~ C13 T^-13, + C13=165888 H0/(13D)>0. (24) + +Its nonnegative moments are finite exactly below13. Conditional further on +V>T, (T/V,z) converges in total variation on the fixed scalar-coordinate +unit square to independent densities13y^12 and z^7(z+1)^4/H0. In particular + + eta_eld V^3 -> 2z^2(z+1), eta_other -> z^2 (25) + +as a further weak-mark consequence. No spatial TV is claimed for (22). + +Proof: the inner-selected shape measure is Q on the inner sector. Pull it +back to the outer sector through the companion involution. The weighted +Jacobian gives exactly the factor rho^11, and then D's unit-square bijection +gives (21). Equivalently the physical inner-radius cutoff has asymptotic +rho gamma(a)|Z_outer|>threshold, giving the same rho^11 after radial integration. +It is not legitimate to retain the old maximum-conditioned doublet density. +The linear transformation of the sign and the radial change q=rho gamma|Z| +yield independence and (22)-(23). + +The rational factor multiplying165888 rho z^7(z+1)^4 in (20) converges uniformly +to1 as rho->0 and is bounded on the closed square. Thus the numerator of (21) +is asymptotic to165888 rho^12 z^7(z+1)^4, whose integral over rho<1/T gives +165888 H0/(13D) T^-13. Substituting rho=y/T and dividing by that mass proves +the normalized L1/TV claim. The uniform height limits of (23) give (25). +Moment integrability follows since V>=1 and the tail coefficient is positive. +The density L/J from maximum selection instead has a second-power tail for +1/rho; that is a different measure, not a contradiction. QED. + +## 7. Review obligations and excluded conclusions + +A: actual-selector composition (1)-(11), matching ELDER2/ELDERD's failure +measure to the root density without a count substitute; no lost sign/Haar/ +normalizer; fixed-t continuity and the iterated-limit order. +B: selected shape interval, all polynomial integrals and moments, density +(15), fourth-power endpoint and inverse-moment threshold (18)-(19). +C: rho^11 reweighting, thirteenth-power companion ratio, scalar TV versus +moving spatial marks, and the independence/height statements (21)-(25). + +The tests corroborate exact algebra, root domains and interval arithmetic. +They do not prove the Gaussian or actual-pairing sources, grant the new +consumer independent acceptance, or formalize these theorems in Lean. +No original r-limit rate, growing-volume/vanishing-k uniformity, finite-r +inverse moments, unrestricted lifetime density, replacement-bar intensity, +remote singleton elder coefficient or across-pair independence is claimed. +The finite physical-radius ordering counterexample in C is retained: the +elder selector is based on height before taking any radius limit. diff --git a/frontiers/elder_partner_extremes_20260930/README.md b/frontiers/elder_partner_extremes_20260930/README.md new file mode 100644 index 000000000..8c3d59674 --- /dev/null +++ b/frontiers/elder_partner_extremes_20260930/README.md @@ -0,0 +1,73 @@ +# Distant elder partners: a selected lifetime law, not a maximum-cluster law + +OpenAI / GPT-6 Astra Pro. **Author-side conditional candidate; new nonauthor +review OPEN. Scientific effect NONE. No self-merge.** + +The actual elder rule selects the HIGHEST saddle. On a cubic doublet that is +the inner-|Z| saddle, the opposite selector to the extreme-cluster maximum +anchor. This packet composes the actual failure/partner interfaces of PR170 +(d=2) and PR175 (d>=3) with the exact microscopic root measure of PR166/169. +It does not establish actual pairing merely from a window-count law. + +## Four new conditional results + +1. The limiting actual selected partner has radius tail + `C_cusp (888807/280) t^-11`. Its coefficient is I-J, not the point coefficient + I or the maximum-cluster coefficient I-D. Only about3.458% of these distant + selected partners belong to doublets. The nonempty failure measure excludes + the remote singleton coefficient. +2. Its extreme-selected lifetime fraction e has an explicit algebraic density: + + f(e)=(6/E0) integral_[sqrt(1-e)-1/2]^[p_hi(e)] + Q(-p,6(e+p-1/2)) dp, + 2p_hi^3-(3/2)p_hi+1/2=e, p_hi in(1/2,1), E0=888807/280. + + All nonnegative integer moments are rational. The mean is exactly + 1174914407/1440459878, about0.8156522961481611. +3. The small-lifetime CDF is asymptotic to `(232960/888807)e^4`, so inverse + lifetime moments have threshold4 in THIS limiting probability law. No + finite-r inverse-moment convergence is inferred from weak convergence. +4. Given a doublet, selecting for large elder radius reweights the former + companion-ratio square density by rho^11. The other/elder radius ratio has + tail exponent13, rather than exponent2 under maximum-cluster selection. + +PROOF.md gives the full arguments, exact scope and fixed-threshold transfer. +The order is **first r->0, then the selected microscopic radius t->infinity**; +small-lifetime and relative-companion limits occur inside that second limit. +No uniform simultaneous limit, unrestricted persistence-lifetime density, +replacement-bar intensity, original finite-r rate or Gaussian coefficient +numerical enclosure is claimed. + +## Source and review boundary + +SOURCES.json binds five complete historical commit/path/Git-blob/SHA256 identities. +ELDER2/ELDERD remain separate author-side source candidates with their own +source-scoped reviews; this new consumer is conditional on their stated actual +selector/failure-measure interfaces. Linking them neither promotes their status +nor revalidates their Gaussian/topological proof. C and D were authored by this +conversation. Same account/provider is not independent scientific acceptance. + +Requested scopes: A actual-elder source composition and selected tail; B explicit +lifetime density/moments/endpoints; C rho^11 reweighting and exponent13. No new +analytic review is inferred from a code pass or an old source review. + +## Replay + +In a full checkout containing the pinned source objects: + + python -B -S frontiers/elder_partner_extremes_20260930/verify.py + +Standalone packet: + + python -B -S verify.py --local-only + +The latter reports source_pins_checked=false. The hosted workflow must fetch and +verify all five actual sources. It checks declared sizes where supplied, all +SHA256/blob identities and regular Git path modes, with replacements disabled. +Local Git fixtures test behavior; they do not authenticate project sources. + +The standard-library suite has41 methods, run under ordinary and optimized +Python. It includes893 exact rational root-shape cases, direct unsheared cubic +checks,12 independent inner-root Jacobians, polynomial interpolation, rational +root-isolation density intervals and13 real-Git/inventory tests. Six semantic +mutants must reject in each mode. No Lean formalization of these new theorems. diff --git a/frontiers/elder_partner_extremes_20260930/RECONNAISSANCE.md b/frontiers/elder_partner_extremes_20260930/RECONNAISSANCE.md new file mode 100644 index 000000000..8a4f041bc --- /dev/null +++ b/frontiers/elder_partner_extremes_20260930/RECONNAISSANCE.md @@ -0,0 +1,33 @@ +# Narrow primary-source reconnaissance — 30 September 2026 + +Actual web queries in this pass included: +- site.arxiv.org persistence elder rule Gaussian random fields critical points +- site.arxiv.org Palm theory extremes stationary regularly varying random fields anchored clusters Planinic +- site.arxiv.org "elder rule" "Gaussian" persistence + +Primary abstract/metadata pages opened: + +1. Hrvoje Planinic, Palm theory for extremes of stationary regularly varying + time series and random fields, arXiv:2104.03810. + https://arxiv.org/abs/2104.03810 + Existing framework: typical exceedances, typical clusters and their different + biases. This packet does not claim to invent anchored/Palm sampling. + +2. Bojan Basrak, Ilya Molchanov and Hrvoje Planinic, Extremal behavior of + stationary marked point processes, arXiv:2210.01474. + https://arxiv.org/abs/2210.01474 + Related marked extreme-process framework. Its hypotheses are not silently + imported as a theorem about our Gaussian pin pairs. + +Access depth: abstract/metadata only, not full-text theorem comparison. No +exhaustive novelty/priority claim or absence-from-literature conclusion is made. +No result from these pages is a missing proof step. The actual mathematical +inputs are the exact source-bound elder and root-density interfaces in SOURCES. + +The new point is source-specific: highest-height selection removes the OUTER +root sector, rather than the inner sector removed by maximum-radius anchoring. +The explicit lifetime density and companion exponent follow by recalculating +that selector's measure, not by renaming the maximum-cluster distribution. + +Consensus was not invoked in this pass (the current request names GitHub and +Superpowers). No changed quota or connector result is claimed. diff --git a/frontiers/elder_partner_extremes_20260930/RESULTS.json b/frontiers/elder_partner_extremes_20260930/RESULTS.json new file mode 100644 index 000000000..7c4015952 --- /dev/null +++ b/frontiers/elder_partner_extremes_20260930/RESULTS.json @@ -0,0 +1,62 @@ +{ + "companion_over_elder_moment_threshold": 13, + "constants": { + "double_given_extreme_elder": { + "lower": "0.034580720107731639", + "upper": "0.034580720107731640" + }, + "elder_to_maximum_tail_ratio": { + "lower": "0.457796705679599976", + "upper": "0.457796705679599977" + }, + "elder_to_point_tail_ratio": { + "lower": "0.450662297994548286", + "upper": "0.450662297994548287" + }, + "mean_lifetime_fraction": { + "lower": "0.815652296148161094", + "upper": "0.815652296148161095" + }, + "outer_over_elder_ratio_tail_constant": { + "lower": "187.906062596204997257", + "upper": "187.906062596204997258" + }, + "second_lifetime_fraction_moment": { + "lower": "0.688765879594061834", + "upper": "0.688765879594061835" + } + }, + "height_density_values": { + "1/100": { + "lower": "0.000001295538683393", + "upper": "0.000001295538683394" + }, + "1/2": { + "lower": "0.411333720068101484", + "upper": "0.411333720068101485" + }, + "1/4": { + "lower": "0.039478044779395017", + "upper": "0.039478044779395018" + }, + "3/4": { + "lower": "1.649750418945205199", + "upper": "1.649750418945205200" + }, + "99/100": { + "lower": "4.279300396681162358", + "upper": "4.279300396681162359" + } + }, + "inverse_lifetime_moment_threshold": 4, + "mathematical_acceptance": false, + "rational_shape_cases": 893, + "scientific_effect": "NONE", + "scope": "finite algebra, not validation of Gaussian or elder premises", + "selected_shape_moments": { + "0": "888807/280", + "1": "3524743221/1361360", + "2": "190490806059/87127040" + }, + "small_lifetime_cdf_coefficient": "232960/888807" +} diff --git a/frontiers/elder_partner_extremes_20260930/SOURCES.json b/frontiers/elder_partner_extremes_20260930/SOURCES.json new file mode 100644 index 000000000..e32cf6444 --- /dev/null +++ b/frontiers/elder_partner_extremes_20260930/SOURCES.json @@ -0,0 +1,50 @@ +{ + "schema": 1, + "scientific_effect": "NONE", + "scope": "Conditional exact interfaces; no parent revalidation or source-status change", + "sources": [ + { + "id": "R", + "commit": "80059a97cd8eb32d1a17a0ad9cb22cb2a0d7b337", + "path": "frontiers/two_scale_cluster_geometry_20260929/RADIAL_TAIL.md", + "bytes": 12533, + "git_blob": "0f14417ef7038b9c6f50e4b01e393a58b7b5e3a4", + "sha256": "250897858c8b314c0ff85ec1860a725efacfdae0ff7409fced4cadf7bfb85973", + "use": "R4-R13 exact root integral and Gaussian majorant; not pairing from counts." + }, + { + "id": "C", + "commit": "56a7904f9ad7d409c31e23195c0e7eeab230613a", + "path": "frontiers/extreme_cluster_sampling_20260930/PROOF.md", + "bytes": 21891, + "git_blob": "19a6044f2066643b5baab34ce5b6b6efb431e84a", + "sha256": "b90cf745e2e67bc9b501c481552f7080d27c28245580668cf72aefa5b7f04715", + "use": "E10-E25 companion/height map, sectors, exact integrals. Author exposure." + }, + { + "id": "D", + "commit": "56a7904f9ad7d409c31e23195c0e7eeab230613a", + "path": "frontiers/extreme_cluster_sampling_20260930/COMPANION_RATIO.md", + "bytes": 10032, + "git_blob": "56348f6765793cd8115041ba367b821eb173f695", + "sha256": "74ff3af5ec071f57d40938fbeca6bca1c189272d5c1bc0440e41cbe764c04d23", + "use": "D1-D7 exact square-coordinate density and heights only; reweighted anew here. Author exposure." + }, + { + "id": "ELDER2", + "commit": "79f18f0cb318fceccd5bdf4e6dad29815165bc7d", + "path": "frontiers/local_elder_geometry_20260930/PROOF.md", + "git_blob": "ef2aa57959ea9f721bbf2316ce94cf616c1c9113", + "sha256": "f68038be79b46124b0f9b31205aa6e3682b34b6f5ef81f4a5697ae81f07cc46b", + "use": "d=2 Theorem E, failure measure and actual weak partner/lifetime law in Sections8.6-8.8. Conditional candidate interface, not promoted." + }, + { + "id": "ELDERD", + "commit": "9c6a73489c5ed2465a3cf65dcc950eeeae074b05", + "path": "frontiers/concave_fibre_elder_20260930/PROOF.md", + "git_blob": "923d3236b5291a29bd162937f172190db84dcef5", + "sha256": "5681896a6808f48fb7508914d0860ec508af7646e9e706fc260d935dd951c75e", + "use": "d>=3 H1/S1-S3/M1 actual selector/failure measure/weak marks. Conditional candidate interface, not promoted." + } + ] +} diff --git a/frontiers/elder_partner_extremes_20260930/VALIDATION.md b/frontiers/elder_partner_extremes_20260930/VALIDATION.md new file mode 100644 index 000000000..938346370 --- /dev/null +++ b/frontiers/elder_partner_extremes_20260930/VALIDATION.md @@ -0,0 +1,45 @@ +# Author-side validation, not analytic acceptance + +The initial eight-method mathematics scaffold failed all eight assertions. +After implementation those eight passed. Expanded mathematics tests now total28. +The separate13-method source/inventory scaffold produced20 failing assertions, +including subtests. A local attempt to reuse an older verifier found no mounted +file at that path and left the scaffold unchanged; its failed replay was not +called success. The completed verifier was then written and all13 tests passed. + +Fresh final baseline:41 tests PASS in normal Python and41 PASS with -O, both +also under the hosted GIT_NO_REPLACE_OBJECTS=1 environment. Each mode executes +all six named semantic mutants (return1) and an unknown label (return2), with +identical deterministic baseline stdout and no stderr. Mathematical core: +-893 rational shape/selector/companion checks; +-40 direct original-cubic gradient/value/Hessian cases; +-12 independent exact inner-root Jacobians from the square coordinates; +-independent dense polynomial interpolation of moment integrals; +-rational bisection/interval enclosures for the algebraic height density; +-small-height and small-ratio finite diagnostics, strict boundaries and ties; +-the exact finite physical-radius-order counterexample retained from PR169. + +Custody tests use real temporary Git repositories: full identity fields, +missing/unsafe paths, omitted/duplicated IDs, noncommit tree/blob objects, +symlink payloads, historical replacement forgery and packet drift. These are +simulated failures, not observed tampering of the user's sources. + +All code is Python standard library. Runtime Python3.13.5; the target workflow +uses Python3.11.16 as in the existing repository. Exploratory symbolic algebra +was used privately to cross-check strip constants, not as a shipped dependency. +The final manuscript's rounded second-moment decimal was corrected against the +exact rational result before publication; no source file or earlier review changed. + +No complete project checkout could be obtained locally (the public raw-host +request failed DNS). Hence local-only replay explicitly reports +source_pins_checked=false. Historical authentication of the five ACTUAL source +objects remains the hosted requirement. The two elder source bindings supply +SHA256 and Git blob; the other three also include declared byte size. No size +was invented for an unread full-byte copy. A matching content hash is not a +proof that the source's mathematics or external review is correct. + +The new actual-source composition, infinite-dimensional domination and weak +transfer require source-bound nonauthor analytic review. Neither these finite +tests nor existing Lean workflow success formalizes this manuscript. Any +hosted success must be recorded against its actual head/run, not anticipated +in this author-time record. No self-merge or scientific register transition. diff --git a/frontiers/elder_partner_extremes_20260930/elder.py b/frontiers/elder_partner_extremes_20260930/elder.py new file mode 100644 index 000000000..9a97c39e6 --- /dev/null +++ b/frontiers/elder_partner_extremes_20260930/elder.py @@ -0,0 +1,250 @@ +"""Exact controls for elder-selected microscopic extreme laws. + +Standard library only. This is finite algebra and interval arithmetic, not a +proof of the actual Gaussian elder-selector interface or the limiting theorem. +""" +import argparse +from fractions import Fraction as F +import json +from math import comb + +MUTANTS=('choose-outer','count-both','drop-half','wrong-lifetime-sign', + 'forget-radius-bias','wrong-height-power') +_MUTANT=None + + +def rational(x): + if type(x) not in (int,F): raise TypeError('exact int/Fraction required') + return F(x) + + +def b0(u): return 3-12*u*u + +def height(u,v): return u+F(1,2)+v/6 + +def shape(u,v): + return -F(3,2) 10368 int_0^(1/sqrt(3)) 2z(1-z^4) dz. + return F(0) if _MUTANT=='wrong-height-power' else F(10368)*(F(1,3)-F(1,81)) + + +def outer_over_elder_tail_exponent(): + return 2 if _MUTANT=='forget-radius-bias' else 1+11+1 + + +def imul(a,b): + vals=[x*y for x in a for y in b] + return min(vals),max(vals) + +def iadd(a,b):return a[0]+b[0],a[1]+b[1] + +def ipoly(coefs,x): + ans=(F(0),F(0)) + for j in range(max(coefs),-1,-1): + c=coefs.get(j,F(0));ans=iadd(imul(ans,x),(c,c)) + return ans + + +def _isolate(target,func,left,right,bits): + for _ in range(bits): + mid=(left+right)/2;value=func(mid) + if value==target:return mid,mid + if value=hi:continue + for j in range(1,20): + v=lo+(hi-lo)*F(j,20);sel=selection(u,v);pair=companion(u,v) + if pair and shape(pair[0],pair[1]): + if sel+selection(pair[0],pair[1])!=1:raise ValueError('one partner per configuration') + if sel in (0,1) and sel!=1-int(outer(u,v)):raise ValueError('height/strip selector mismatch') + elif sel!=1:raise ValueError('singleton must select its one root') + n+=1 + return n + + +def result(): + n=checks() + return {'scientific_effect':'NONE','mathematical_acceptance':False, + 'scope':'finite algebra, not validation of Gaussian or elder premises', + 'rational_shape_cases':n, + 'selected_shape_moments':{str(j):str(moment(j)) for j in range(3)}, + 'small_lifetime_cdf_coefficient':str(F(832)/moment(0)), + 'inverse_lifetime_moment_threshold':4, + 'companion_over_elder_moment_threshold':13, + 'constants':{key:decimal_interval(val) for key,val in constants().items()}, + 'height_density_values':{str(e):decimal_interval(height_density_bounds(e)) for e in (F(1,100),F(1,4),F(1,2),F(3,4),F(99,100))}} + + +def main(): + parser=argparse.ArgumentParser(description=__doc__);parser.add_argument('--mutant',choices=MUTANTS);args=parser.parse_args() + global _MUTANT + _MUTANT=args.mutant + try:ans=result() + except ValueError as exc: + print(json.dumps({'passed':False,'error':str(exc)},sort_keys=True));raise SystemExit(1) + print(json.dumps(ans,indent=2,sort_keys=True)) + +if __name__=='__main__':main() diff --git a/frontiers/elder_partner_extremes_20260930/test_elder.py b/frontiers/elder_partner_extremes_20260930/test_elder.py new file mode 100644 index 000000000..6f9670e88 --- /dev/null +++ b/frontiers/elder_partner_extremes_20260930/test_elder.py @@ -0,0 +1,265 @@ +from fractions import Fraction as F +import unittest +import elder + +class InitialTests(unittest.TestCase): + def test_selected_mass(self): + self.assertEqual(elder.moment(0), F(888807,280)) + def test_selected_mean(self): + self.assertEqual(elder.moment(1)/elder.moment(0), F(1174914407,1440459878)) + def test_selected_second(self): + self.assertEqual(elder.moment(2)/elder.moment(0), F(63496935353,92189432192)) + def test_outer_not_elder(self): + self.assertEqual(elder.selection(F(-1), F(6)), 0) + def test_inner_is_elder(self): + self.assertEqual(elder.selection(F(-13,23), F(294,529)), 1) + def test_near_zero_density(self): + self.assertEqual(elder.small_height_density_coefficient(),F(3328)) + def test_upper_density(self): + lo,hi=elder.height_density_bounds(F(1)) + self.assertEqual((lo,hi),(F(1312200,296269),F(1312200,296269))) + def test_new_ratio_exponent(self): + self.assertEqual(elder.outer_over_elder_tail_exponent(),13) + + + +class GeometryTests(unittest.TestCase): + def test_full_shape_grid(self): + self.assertEqual(elder.checks(),893) + + def test_selector_matches_cubic_boundary(self): + for ip in range(-7,24): + p=F(ip,16) + for j in range(1,15): + e=F(j,15); v=6*(e+p-F(1,2)); u=-p + if not elder.shape(u,v):continue + boundary=2*p**3-F(3,2)*p+F(1,2) + expected=F(1) if p<=F(1,2) or e>boundary else F(1,2) if e==boundary else F(0) + self.assertEqual(elder.selection(u,v),expected) + + def test_actual_cubic_gradient_height_and_type(self): + # Directly differentiate the unsheared cubic, independently of selector. + cases=0 + for p in (F(1,4),F(3,5),F(3,4),F(1),F(5,4)): + u=-p; b=3-12*u*u;lo,hi=abs(b)/2,3-6*u + for j in range(1,5): + v=lo+(hi-lo)*F(j,5) + for k,a,Z in ((F(1),F(-12),F(1)),(F(3,2),F(4),F(-2))): + s=-k*v/Z**2; B=k*b/Z**2; Dc=k*(v-b*u)/Z**3 + beta=B+a*a/(12*k);c=2*Dc+a*B/(4*k)+a**3/(144*k*k) + roots=[(u,v,F(1))] + other=elder.companion(u,v) + if other and elder.shape(other[0],other[1]):roots.append(other) + es=[] + for uu,vv,t in roots: + z=t*Z;x=uu-a*z/(12*k) + gx=6*k*x*x-F(3,2)*k+a*x*z+beta*z*z/2 + gz=s*z+a*(x*x-F(1,4))/2+beta*x*z+c*z*z/2 + val=2*k*x**3-F(3,2)*k*x-k/2+s*z*z/2+a*(x*x-F(1,4))*z/2+beta*x*z*z/2+c*z**3/6 + hxx=12*k*x+a*z;hzz=s+beta*x+c*z;hxz=a*x+beta*z + self.assertEqual((gx,gz),(0,0)) + self.assertEqual(-val/k,elder.height(uu,vv)) + self.assertTrue(-k Date: Wed, 30 Sep 2026 04:48:45 -0500 Subject: [PATCH 3/5] Clarify fresh post-stop owner instruction for elder-extreme foreground work Addresses inline review4143089494 with the directly observed September30 owner messages, not a pre-stop autonomy inference. PLAN and its manifest identity only; proof91f88e39, mathematical code, source pins and workflow unchanged. No timer/agent restart or branch-protection change. Fresh41 tests in both Python modes and exact local/remote packet tree9ce9705b match. New analytic reviews remain separate and open; no self-merge. --- .../MANIFEST.json | 6 +++--- .../elder_partner_extremes_20260930/PLAN.md | 21 ++++++++++++++++--- 2 files changed, 21 insertions(+), 6 deletions(-) diff --git a/frontiers/elder_partner_extremes_20260930/MANIFEST.json b/frontiers/elder_partner_extremes_20260930/MANIFEST.json index 5bd8a7dba..a9c8e7984 100644 --- a/frontiers/elder_partner_extremes_20260930/MANIFEST.json +++ b/frontiers/elder_partner_extremes_20260930/MANIFEST.json @@ -5,9 +5,9 @@ "files": [ { "path": "PLAN.md", - "bytes": 1796, - "sha256": "6f8fede899bfe6418aa488216e9205725b664ea0be8070c6a97b6705b7281bff", - "git_blob": "93c56e6f6b9064022f334cdeca9a7cd562bad124" + "bytes": 2846, + "sha256": "656b9bd00dae549d1a76fd2dbaff3fc878178a141568e2552299d0f06d8c99b3", + "git_blob": "92a41240e99317e0206409753d45ae109b7e3634" }, { "path": "PROOF.md", diff --git a/frontiers/elder_partner_extremes_20260930/PLAN.md b/frontiers/elder_partner_extremes_20260930/PLAN.md index 93c56e6f6..92a41240e 100644 --- a/frontiers/elder_partner_extremes_20260930/PLAN.md +++ b/frontiers/elder_partner_extremes_20260930/PLAN.md @@ -10,9 +10,24 @@ root integral with that selector; integrate the selected height marginal by polynomial elimination; analyze its small-height endpoint; reweight the explicit doublet square law by the inner radius to identify the companion ratio tail. -Execution is foreground and isolated in a new packet/branch. The repeated -owner autonomy directive supplies authority; no stopped agents or timers are -restarted. No other writer branch or frozen source proof is changed. +Execution is foreground and isolated in a new packet/branch. Authority is a +NEW explicit instruction from Dylan in this ChatGPT conversation on +2026-09-30, after the repository stop of 2026-09-27, not a pre-stop autonomy +grant. Immediately before publication he instructed: "Work on closing as many +mathematical items as possible while working with and supporting the other +models in the GitHub. Also advance the mathematics in every place that's +justified based on what we currently know. Ultra tokens, ultra depth @GitHub +@Superpowers". On this continuation he again explicitly instructed "Continue +to Work on closing as many mathematical items as possible" with the same +research and collaboration scope. This is the author's transcription of direct +owner input; no public-chat permalink or cryptographic authorization receipt +is claimed. Main#95 pickup5907785003 preceded publication; review-thread +reply4143176012 records the authorization clarification. + +The new instruction authorizes this foreground research session only. It does +not re-arm a Cursor process, automation, timer, watch or loop. The general +OWNER_STOP notice and required review/branch-protection rules are unchanged. +No other writer branch or frozen mathematical proof is changed by this repair. Steps completed author-side: - Read actual ELDER2/ELDERD marked-law interfaces and the root/companion sources. From f59a6e5decbc8c110aeae8e97de3c5a1d980bb48 Mon Sep 17 00:00:00 2001 From: "Claude Fable 5.1" Date: Wed, 30 Sep 2026 13:44:30 +0000 Subject: [PATCH 4/5] Theorem R remainder identified: B_{d,L} for candidates, 0 for elder pairs (even contact expansion; author-side candidate) frontiers/remainder_vanishing_20260930/ (CL-D2-REMAINDER-VANISHING-20260930-v1): PROOF.md, even_contact_check.py, RESULTS.json, README.md, SOURCES.json; workflow remainder-vanishing.yml. - Lemma E: the contact error of [R] (R11) is r^2 H, not r(k+r)H: the endpoint corrections alpha_M = -6k + (r/12)f_4 + ..., alpha_S = 6k + (r/12)f_4 + ... cancel in the typed product (reflection symmetry of the pinned family); the inertia-flip layers carry O(r^2) products (three-case split) - Theorem R+: nu_cand(ell) = c ell^-1/3 + B_{d,L} + o(1) and nu_eld(ell) = c ell^-1/3 + o(1): Lemma E gives the ell-uniform near-diagonal majorant that [Z] section 5 records as unavailable for candidates; dominated convergence in the separation variable identifies the constant as the equal-height kernel mass B_{d,L}; Theorem Z (Z4) subtracts it - consumed: [R], [Z], [C7-K], the reconciled [P] chain (all merged, reviewed); #186/#187/#188 cited only - exact controls (stdlib): quintic pin expansions, the exact reflection identity det H_M(-r) = det H_S(r) and parity on a general pinned quintic in two variables, block/Haynsworth identities with the layer split, the ledger; mutants M1-M3 - clean-context referee pass (two rounds) applied before landing Scientific effect NONE. No register, GRAPH, STATUS, PROOF_INDEX, prize or Boolean change. Author will not merge. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU --- .github/workflows/remainder-vanishing.yml | 73 +++ .../remainder_vanishing_20260930/PROOF.md | 270 ++++++++++++ .../remainder_vanishing_20260930/README.md | 37 ++ .../remainder_vanishing_20260930/RESULTS.json | 85 ++++ .../remainder_vanishing_20260930/SOURCES.json | 142 ++++++ .../even_contact_check.py | 416 ++++++++++++++++++ 6 files changed, 1023 insertions(+) create mode 100644 .github/workflows/remainder-vanishing.yml create mode 100644 frontiers/remainder_vanishing_20260930/PROOF.md create mode 100644 frontiers/remainder_vanishing_20260930/README.md create mode 100644 frontiers/remainder_vanishing_20260930/RESULTS.json create mode 100644 frontiers/remainder_vanishing_20260930/SOURCES.json create mode 100644 frontiers/remainder_vanishing_20260930/even_contact_check.py diff --git a/.github/workflows/remainder-vanishing.yml b/.github/workflows/remainder-vanishing.yml new file mode 100644 index 000000000..e046d962d --- /dev/null +++ b/.github/workflows/remainder-vanishing.yml @@ -0,0 +1,73 @@ +name: Remainder vanishing exact controls + +'on': + pull_request: + paths: + - 'frontiers/remainder_vanishing_20260930/**' + - '.github/workflows/remainder-vanishing.yml' + # bound sources (consumed and cited_only in SOURCES.json) + - 'frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md' + - 'imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md' + - 'imports/lifetime_parent_20260925/ERRATUM_CONGRUENCE.md' + - 'reviews/d1_section9_borel_repair_20260925/REPAIR.md' + - 'reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md' + - 'frontiers/c7_total_bounded_20260929/PROOF.md' + - 'frontiers/unrestricted_selection_difference_20260929/PROOF.md' + - 'frontiers/c7_zero_gap_limit_20260929/PROOF.md' + workflow_dispatch: + +permissions: + contents: read + +jobs: + exact-controls: + runs-on: ubuntu-latest + timeout-minutes: 10 + steps: + - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 + with: + persist-credentials: false + - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 + with: + python-version: '3.11.16' + - name: Verify sources, replay both modes, reject mutants + env: + PYTHONDONTWRITEBYTECODE: '1' + run: | + set -euo pipefail + python -B -S - <<'PY' + import hashlib, json, pathlib, subprocess, sys + root = pathlib.Path('frontiers/remainder_vanishing_20260930').resolve() + manifest = json.loads((root / 'SOURCES.json').read_text()) + present = sorted(p.name for p in root.iterdir()) + expected_names = sorted([e['path'] for e in manifest['files']] + ['SOURCES.json']) + if present != expected_names: + raise ValueError('packet tree differs from manifest: ' + repr(present)) + for entry in manifest['files']: + path = root / entry['path'] + if path.is_symlink(): + raise ValueError('symlink: ' + entry['path']) + data = path.read_bytes() + if len(data) != entry['bytes'] or hashlib.sha256(data).hexdigest() != entry['sha256']: + raise ValueError('packet file identity mismatch: ' + entry['path']) + for entry in manifest['consumed'] + manifest['cited_only']: + data = pathlib.Path(entry['path']).read_bytes() + framed = b'blob ' + str(len(data)).encode() + b'\0' + data + if len(data) != entry['bytes'] or hashlib.sha256(data).hexdigest() != entry['sha256'] or hashlib.sha1(framed).hexdigest() != entry['git_blob']: + raise ValueError('merged source drifted: ' + entry['path']) + script = str(root / 'even_contact_check.py') + expected = (root / 'RESULTS.json').read_bytes() + for flags in (['-B', '-S'], ['-B', '-O', '-S']): + out = subprocess.run([sys.executable, *flags, script], check=True, capture_output=True, timeout=600).stdout + if out != expected: + raise RuntimeError('output differs from RESULTS.json under ' + ' '.join(flags)) + for m in manifest['mutants']: + rc = subprocess.run([sys.executable, *flags, script, '--mutant', m], capture_output=True, timeout=600).returncode + if rc != 1: + raise RuntimeError('mutant ' + m + ' not rejected') + rc = subprocess.run([sys.executable, *flags, script, '--mutant', 'M9'], capture_output=True, timeout=600).returncode + if rc != 2: + raise RuntimeError('unknown mutant label not rejected with exit 2') + print(json.dumps({'scientific_effect': 'NONE', 'mathematical_acceptance': False})) + PY + git diff --exit-code diff --git a/frontiers/remainder_vanishing_20260930/PROOF.md b/frontiers/remainder_vanishing_20260930/PROOF.md new file mode 100644 index 000000000..2a3659c8b --- /dev/null +++ b/frontiers/remainder_vanishing_20260930/PROOF.md @@ -0,0 +1,270 @@ +# The bounded remainder of Theorem R: `B_{d,L}` for candidates, `0` for elder pairs + +Object: CL-D2-REMAINDER-VANISHING-20260930-v1. +Author: Anthropic Claude (claude.ai session `session_01NMeKEismAyeqgdB4sy2NJU`), 30 September 2026. +Disposition: AUTHOR-SIDE PROOF CANDIDATE; NONAUTHOR REVIEW REQUIRED. Scientific effect: NONE — no register, +graph, STATUS, PROOF_INDEX, prize or Boolean change; no numerical constant is claimed. Same GitHub account as +every lane; zero organizational independence. Everything below is relative to merged, reviewed sources ([R], +[Z], [C7-K] and the reconciled [P] chain); the unmerged Math- #187/#188 are cited only, for the quantitative +Remark 2. + +## 0. Statement + +Setting, notation and every display number `(Rn)` are those of [R] (`frontiers/three_fronts_20260924/ +LIFETIME_REMAINDER.md`, blob `247b3ecf`, Theorem R; xAI R1–R6 on main #67, Anthropic full depth Math- #186): +fixed `d ≥ 2`, `L > 0`, the [P] field on `X = R^d/(LZ^d)`; near pins `M = −ru/2`, `S = ru/2` with heights `b`, +`b − kr³` and zero gradients; the observation rows `U_r`, target `v_r`, density `π_r`, the regression law `Q`, +the coupling `F_r` of [R] (R3)–(R4), `m = d − 1`, `P = 1 + |b| + k`; the scaled endpoint Hessians +`K_i = D_r^{−1}H_iD_r^{−1}` with `α_i = F_{r,xx}(i)/r`, `β_i = ∇_yF_{r,x}(i)/r`, `A_i = D_y²F_r(i)` (`i = M, S`); the +filtered determinants `F_j`; `Z_r/r² = E_Q[F_d(K_M)F_{d−1}(K_S)]`; `A_0 = D_y²F_0(0)`, +`z_0 = E[(6k)²(det A_0)²1{A_0 < 0}]`; `A_r = 12π_r(v_r)Z_r/r²`, `A_0 = 12π_0(v_0)z_0`; the majorant +`H(b,k) = CP^Ne^{−c(b²+k²)}` (`N` enlarged when needed); the near/far split at a separation `r_0`, `a = ℓ/r_0³`; and +`c = c_{d,L}` of [P] (15.2). Admissible radii: `r_0 ≤ r_0^* := min{r_0^{[R]}, L/(4√2), r_0^{[K]}, r_0^{[Z]}}` ([R]'s compactness band on +which (R2)–(R5) hold, the cap-cylinder embedding of [REC] §5, and the radii of [C7-K] (K2) and [Z] §4). [R] proves +`|A_r − A_0| ≤ r(k + r)H` ((R11), first order in `r`) and from it Theorem R, `|ν_eld(ℓ) − cℓ^{−1/3}| ≤ C`, and states +that neither convergence of the remainder nor a second coefficient is identified. + +From [Z] (`frontiers/c7_zero_gap_limit_20260929/PROOF.md`, blob `5b6328ea`; Anthropic A/B/C reads on Math- #155): +the unmarked candidate kernel and the equal-height kernel + + Ψ_ℓ^{cand}(b, y) = p_y(v_{b,ℓ}) E_{Q_{y,b,ℓ}}[W], Ψ_0(b, y) = p_y(v_{b,0}) E_{Q_{y,b,0}}[W] ((Z2)), + +`B_{d,L} = ∫_{X∖{0}}∫_R Ψ_0(b, y) db dy ∈ (0, ∞)` ((Z3)), and Theorem Z (Z4): the rejected density +`ρ_rej(ℓ) = ν_cand(ℓ) − ν_eld(ℓ) → B_{d,L}` as `ℓ ↓ 0`. + +**Lemma E (even contact expansion).** There are `C, N` depending on `d, L` only such that for all `b ∈ R`, `k > 0` +and `0 < r ≤ r_0^*` + + |Z_r/r² − z_0(b, k, u)| ≤ C r² P^N, |A_r − A_0| ≤ r² H(b, k). (E.1) + +The first-order term of (R11) is absent: the two endpoint corrections enter the typed product with opposite signs +and cancel identically (§1, Steps 1–3), and on the inertia-flip layers the product of the two typed determinants is +`O(r²)` (Step 4). + +**Theorem R+.** For every fixed `d ≥ 2`, `L > 0`, as `ℓ ↓ 0`, + + ν_cand(ℓ) = c ℓ^{−1/3} + B_{d,L} + o(1), (R+.1) + ν_eld(ℓ) = c ℓ^{−1/3} + o(1), i.e. ν_eld(ℓ) = c ℓ^{−1/3} (1 + o(ℓ^{1/3})). (R+.2) + +So the bounded remainder of Theorem R has the constant term `B_{d,L}` (the equal-height kernel mass of [Z]) for the +candidate density and `0` for the elder density. Moreover, for every `r_0 ∈ (0, r_0^*]`, + + ν_cand^{near,r_0}(ℓ) − cℓ^{−1/3} → ∫_{0 0`) or (`index A_S = m − 1` and `σ_S < 0`). +Put `u := C_1 r T (1 + T/k)` with `C_1 = C_1(d) ≥ 2` large, and the good event + + G := { λ_max(A_0) ≤ −u } ∩ { k ≥ C_1 r T }. + +On `G`: `‖A_i − A_0‖ ≤ rT ≤ u/C_1`, so `A_M, A_S < 0`; `α_S ≥ 6k − CrT > 0` and `rβ_Sᵀ(−A_S)^{−1}β_S ≥ 0`, so +`σ_S > 0`; `α_M ≤ −6k + CrT ≤ −5k` and `rβ_Mᵀ(−A_M)^{−1}β_M ≤ rT²/λ_min(−A_M) ≤ 2rT²/u ≤ 2k/C_1`, so `σ_M < 0`. Hence +on `G` the indices are `d` and `d − 1`, `1{A_0 < 0} = 1`, and + + F_d(K_M)F_{d−1}(K_S) − 36k²(det A_0)²1{A_0<0} = |det K_M det K_S| − 36k²(det A_0)², + +whose absolute value is at most the left side of (1.6). Off `G` there are three cases, on each of which both typed +products are `O(r²)` times a polynomial: + +- on `{k < C_1rT}`: `F_d(K_M)F_{d−1}(K_S) ≤ C(k + r)²T^{2d} ≤ Cr²T^{2d+2}` ([R] §4's bound `F_j(K_i) ≤ C(k + r)T^d`, + `T ≥ 1`) and `36k²(det A_0)² ≤ Cr²T^{2m+2}`; +- on `{λ_max(A_0) ≥ u} ∩ {k ≥ C_1rT}`: `λ_max(A_M) ≥ u − rT > 0`, so `K_M` is not negative definite, `F_d(K_M) = 0`, + and `1{A_0 < 0} = 0` — both products vanish (this case also contains the pattern `index A_S = m − 1`, `σ_S < 0`, + which `F_d(K_M) = 0` kills); +- on `{|λ_max(A_0)| < u} ∩ {k ≥ C_1rT}`: by Weyl, `|det A_i| ≤ (|λ_max(A_0)| + rT)T^{m−1} ≤ 2uT^{m−1}`, so + `|det K_i| ≤ (6k + CrT)·2uT^{m−1} + rT^{m+1} ≤ C(ku + rT²)T^{m−1} ≤ CkuT^{m−1}` (as `rT² ≤ ku/C_1`, i.e. + `T ≤ k + T`), hence `F_d(K_M)F_{d−1}(K_S) ≤ Ck²u²T^{2m−2}`, and likewise `36k²(det A_0)²1{A_0<0} ≤ 36k²u²T^{2m−2}`; + with `k²u² = C_1²r²T²(k + T)²` both are `≤ Cr²(k + T)²T^{2m}`. + +No smallness of the layers' probability is needed: each typed determinant on the last layer is `O(r)` and their +product `O(r²)`. + +*Step 5 (assembly).* Taking expectations, `|Z_r/r² − z_0| ≤ E[Cr²(1 + k)²T^{N_1} + Cr²(k + T)²T^{2m+2}] ≤ Cr²P^N`. +For `A_r − A_0 = 12[π_r(v_r) − π_0(v_0)]Z_r/r² + 12π_0(v_0)[Z_r/r² − z_0]`, use (R5) (`|π_r(v_r) − π_0(v_0)| ≤ +Cr²P²e^{−c(b²+k²)}`, `π_0(v_0) ≤ Ce^{−c(b²+k²)}`), (R10) (`Z_r/r² ≤ C(k + r)²P^N`) and the first bound; every term is +`r²` times a polynomial in `P` times the Gaussian factor, i.e. `≤ r²H`. ∎ + +## 2. Proof of Theorem R+ + +*The separation variable.* As in [R] §6 and [Z] (Z14), with `r = (ℓ/k)^{1/3}`, `k = ℓ/r³`, `dk = 3ℓr^{−4}dr`, + + ν_cand^{near,r_0}(ℓ) = ∫_0^{r_0}∫_R∫_{S^{d−1}} r^{−2} A_r(b, ℓ/r³, u) dσ(u) db dr, + c ℓ^{−1/3} = ∫_0^{∞}∫_R∫_{S^{d−1}} r^{−2} A_0(b, ℓ/r³, u) dσ(u) db dr, + +and, by the pin-density and determinant normalizations of [P] (10.1)–(11.1) exactly as in (Z14) but without the +mark, `r^{−2}A_r(b, ℓ/r³, u) = r^{d−1}Ψ_ℓ^{cand}(b, ru)` (the polar factor `r^{d−1}`, the pin density +`12r^{−(d+3)}π_r(v_r)` and the determinant scale `r²`). Hence + + ν_cand^{near,r_0}(ℓ) − cℓ^{−1/3} = ∫_0^{r_0}∫∫ r^{−2}(A_r − A_0)(b, ℓ/r³, u) − ∫_{r_0}^{∞}∫∫ r^{−2}A_0(b, ℓ/r³, u). (2.1) + +*Domination.* By (E.1), `|r^{−2}(A_r − A_0)(b, ℓ/r³, u)| ≤ H(b, ℓ/r³) ≤ Ce^{−cb²}`, an integrable majorant on +`(0, r_0) × R × S^{d−1}` **independent of `ℓ`** — the near-diagonal domination that [Z] §5 records as unavailable +for candidates from (R11) alone (with `r(k + r)H` the integrand is only `≤ (1 + ℓ/r⁴)H`). The second term of (2.1) +is at most `∫_{r_0}^∞ r^{−2}(ℓ/r³)²H ≤ Cℓ²r_0^{−7}` (`A_0 ≤ k²H`). + +*Pointwise limit.* Fix `r, b, u`. As `ℓ ↓ 0`, `k = ℓ/r³ ↓ 0` and `A_r(b, k, u) → A_r(b, 0, u)`: the pinned law +`Q_{r,b,k}` is the regression law with target `v_r(b,k)`, affine in the target with the `k`-free covariance of +[R] §2, so `F_r` depends continuously on `k` in `C²`, the typed product is continuous off the type boundaries +(Gaussian-null by nondegeneracy, [Z] §2), and it is dominated by a polynomial in the endpoint Hessians; `π_r(v_r)` +is continuous in the target. Also `A_0(b, k, u) → 0` (`A_0 ≤ k²H`). Since `r^{−2}A_r(b, 0, u) = r^{d−1}Ψ_0(b, ru)` +((Z2) at `y = ru`), dominated convergence in (2.1) gives + + ν_cand^{near,r_0}(ℓ) − cℓ^{−1/3} → ∫_0^{r_0}∫∫ r^{d−1}Ψ_0(b, ru) dσ db dr = ∫_{0 0`, follows as + soon as the far constant is known to be polynomial in `1/ρ` (take `ρ = ℓ^{θ}`, `θ` small, `N` larger than + `θ` times that degree); the constant's `ρ`-dependence enters through the far-pair nondegeneracy at separation + `ρ` and, for #188, the `N`-site conditional density and `ℓ_1 = ρ²/(64N²)`. None of this is proved here. +3. **Consistency.** (R+.1) with (Z4) is consistent with [C7-K] (T2) and [U] (U1) (`ρ_rej = Θ(1)`); (R+.3) with + [P] (14.1) (candidate density `O(1)` at fixed separation) and with [Z] (Z18) (rejected mass below separation `δ` + is `≤ Cδ`); Lemma E with the remark in Math- #186 ("Where the `O(1)` comes from": at fixed marks the contact error + is `O(r²)`; that remark also noted that this alone does not improve Theorem R, which is why Theorem R+ needs the + domination-plus-limit argument of §2 rather than the ledger of (R16)). The `2r_0` of #186's C7 model check is + the (R17)–(R18) loss term, i.e. the rejected mass at separations `≍ r_0`, in agreement with Remark 1. +4. **For the manuscript.** Once reviewed, (R+.2) supports reading the abstract's `(1 + o(1))` as + `(1 + o(ℓ^{1/3}))` and, for the candidate density, `cℓ^{−1/3} + B_{3,24} + o(1)`. Until then E10 of the V3 edit + pack (`(1 + O(ℓ^{1/3}))`, which rests on Theorem R and its two reads, the second still unmerged in Math- #186) + is the safe statement, and E3's "do not write an `o(1)` remainder for `ν_eld` alone" and E10's "not known to be + improvable" would be revised by this note when it lands. No `+ c_1 + o(1)` with `c_1 ≠ 0` is claimed for `ν_eld`; + the claim is precisely that its constant term is `0`. + +## 4. Sources (exact identities in `SOURCES.json`) + +| Tag | Path | Role | +|---|---|---| +| [R] | `frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md` (blob `247b3ecf`) | Theorem R; §§2–6: coupling (R2)–(R5), Lemma R3.2, (R8)–(R11), the separation-variable identity — consumed | +| [Z] | `frontiers/c7_zero_gap_limit_20260929/PROOF.md` (blob `5b6328ea`) | (Z2)–(Z4), (Z10)–(Z12), (Z14), (Z16)–(Z18) — consumed | +| [C7-K] | `frontiers/c7_total_bounded_20260929/PROOF.md` (blob `28748b08`) | §4 (T1) proof with cutoff `ρ`, (T2) — Remark 2, Remark 3 | +| [P] | `imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md` (blob `dfed3b8d`) | §§1–4, 7, 9 (as [E2]), (10.1), (11.1), 14, (15.2) — through [R], [Z] | +| [E1] | `imports/lifetime_parent_20260925/ERRATUM_CONGRUENCE.md` (blob `213594d6`) | reading rule | +| [E2] | `reviews/d1_section9_borel_repair_20260925/REPAIR.md` (blob `fe9b9ce4`) | §9 replacement | +| [REC] | `reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md` (blob `75da2597`) | W1, embedding radius, consumption contract | +| [U] | `frontiers/unrestricted_selection_difference_20260929/PROOF.md` (blob `5a55b179`) | (U1) — cited only (Remark 3) | +| #187, #188 | `frontiers/far_elder_rate_20260930/PROOF.md`, `frontiers/far_elder_flat_ridge_20260930/PROOF.md` (unmerged) | far elder rates — cited only (Remark 2) | +| #186 | `reviews/d2_remainder_full_depth_claude_20260930/REVIEW.md` (unmerged) | the review remark that motivated Lemma E — cited only | + +## 5. Exact controls (`even_contact_check.py`; stdlib; exact rationals; byte-identical under `-O`) + +E1 the axial pin identities on a quintic profile: with `f_2 = −(r²/24)f_4`, `f_3 = 12k − (r²/40)f_5` the pins +`f(∓r/2) = b, b − kr³`, `f_x(∓r/2) = 0` hold exactly and `α_M = −6k + (r/12)f_4 − (r²/120)f_5`, +`α_S = 6k + (r/12)f_4 + (r²/120)f_5`, `α_Mα_S = −36k² + r²(f_4²/144 − kf_5/10) − r⁴f_5²/14400`, at rational +`(r, k, f_4, f_5, b)` — the coefficients `1/24, 1/40, 1/12, 1/120` are the content of Step 1; mutant M1 (drop the +`(r²/40)f_5` pin term) fails. +E2 the reflection symmetry on a general pinned quintic in two variables (six pinned coefficients solved exactly, +fifteen free ones fixed at rationals): `det H_M(−r) = det H_S(r)` exactly at rational `r`; consequently +`det H_M det H_S/r²`, recovered as the polynomial of degree ten in `r` by exact interpolation at eleven rational +`r`, has only even powers, constant term `−36k²A_0²` (`A_0 = f_yy(0)`), and the recorded `r²` coefficient. The parity +is forced by the symmetry, so this is a check of the mechanism of Step 3, not of its bookkeeping; mutant M2 +applies the parity test to the single factor `det H_M/r`, which has `r¹, r³, r⁵` terms, and fails. +E3 the block identity `det K = α det A − r βᵀadj(A)β` and Haynsworth's inertia count on rational `3×3` and `4×4` +examples with `A` negative definite, of index `m − 1`, and indefinite, and the scalar Schur complement of both +signs (inertia by exact congruence diagonalisation); the Step 4 case split at rational points: `F_d(K_M) = 0` when +`λ_max(A_M) > 0`, and the layer inequality `|det A| ≤ (|λ_max(A)|)·‖A‖^{m−1}` for `|λ_max(A)|` small. +E4 the ledger of §2 and Remark 2 by exact monomial substitution `r = (ℓ/k)^{1/3}`: `r^{−2}(ℓ/r³)² = ℓ²r^{−8}` +(so `∫_{r_0}^∞ ≍ ℓ²r_0^{−7}`), `k^{−2/3}r^{3}/k = ℓk^{−8/3}`, `ℓκ^{−5/3} = κ^{7/3} = ℓ^{7/12}` at `κ = ℓ^{1/4}`, +`ℓ^{2/3}a^{−1/3} = r_0ℓ^{1/3}`, and `r ≤ k ⇔ ℓ ≤ k⁴`; mutant M3 (claims the loss exponent `1/3`) fails. +E5 the layer algebra of Step 4: `k²u² = C_1²r²T²(k + T)²` and `rT² ≤ ku/C_1` for `u = C_1rT(1 + T/k)`, exactly. +Mutants `M1`–`M3` exit 1; an unknown label exits 2. The controls check identities and bookkeeping; they do not prove +the Gaussian estimates and are not acceptance. + +## 6. Review slices + +A: Lemma E — Steps 1–3 (the expansions and the product cancellation) and Step 4 (Haynsworth, the good event, the + three layers), Step 5. +B: §2 — the separation-variable identity against [R] §6 / [Z] (Z14), the `ℓ`-uniform majorant from (E.1), the + pointwise limit `A_r(b,k,u) → A_r(b,0,u)`, the far candidate limit from [Z], and the use of (Z4). +C: the statement's scope, Remarks 1–4, and the sources' consumption (in particular that nothing unmerged is used). diff --git a/frontiers/remainder_vanishing_20260930/README.md b/frontiers/remainder_vanishing_20260930/README.md new file mode 100644 index 000000000..462c6d5e9 --- /dev/null +++ b/frontiers/remainder_vanishing_20260930/README.md @@ -0,0 +1,37 @@ +# The remainder of Theorem R: `B_{d,L}` for candidates, `0` for elder pairs (CL-D2-REMAINDER-VANISHING-20260930-v1) + +Author-side proof candidate, Anthropic Claude, 30 September 2026. Scientific effect NONE. Nonauthor review required. +Relative to merged, reviewed sources only ([R] Theorem R, [Z] Theorem Z, [C7-K], the reconciled [P] chain); +Math- #187/#188 are cited only, for a conditional rate remark. + +**Statement (Theorem R+).** For the periodized Gaussian field on the fixed torus (every `d ≥ 2`, `L > 0`), as +`ℓ ↓ 0`, + + ν_cand(ℓ) = cℓ^{−1/3} + B_{d,L} + o(1), ν_eld(ℓ) = cℓ^{−1/3} + o(1), + +where `B_{d,L} = ∫∫Ψ_0` is the equal-height kernel mass of Theorem Z. Theorem R's bounded remainder is thus +identified: its constant term is the rejected mass `B_{d,L}` for candidate pairs and `0` for elder pairs, so +`ν_eld = cℓ^{−1/3}(1 + o(ℓ^{1/3}))`. Also `ν_cand^{near,r_0} − cℓ^{−1/3} → ∫_{|y|= u kills F_d(K_M); |lambda_max| < u via Weyl); Theorem R+ restated without any dependence on Math-#188 (Theorem Z (Z4) plus the ell-uniform candidate majorant from Lemma E identify the constant B_{d,L}); Proposition L removed as a proposition (it is [C7-K] section 4), Proposition C folded into (R+.3) with its limit identified; T dominates C^7; admissible radii stated; remarks corrected (attribution of the #186 model check, the rate remark, the manuscript remark, no-second-coefficient wording); controls: E2 recorded as symmetry-forced with the exact reflection identity added, E3 exercises the indefinite layer, E4 tautology removed" + }, + "files": [ + { + "path": "PROOF.md", + "bytes": 21505, + "sha256": "aedc1e19f9fb3ec4bc48a82c607441c88f9acc7cb048939ae89c2de4a1d2065d" + }, + { + "path": "even_contact_check.py", + "bytes": 19510, + "sha256": "b6075fc55658814396d296c70affbdf1d1f39e5beb276e3622920bfe247cb001" + }, + { + "path": "RESULTS.json", + "bytes": 1391, + "sha256": "f869ad1f20c97e090819bf635525027c91c53124bb06fbcf06c5b5e1b57caacc" + }, + { + "path": "README.md", + "bytes": 3015, + "sha256": "a729cfc8d6d7fb426b3e93cb524a5940a29c1655541cdfde1bc7773368042cb5" + } + ] +} diff --git a/frontiers/remainder_vanishing_20260930/even_contact_check.py b/frontiers/remainder_vanishing_20260930/even_contact_check.py new file mode 100644 index 000000000..437b5b3c0 --- /dev/null +++ b/frontiers/remainder_vanishing_20260930/even_contact_check.py @@ -0,0 +1,416 @@ +#!/usr/bin/env python3 +"""Exact finite controls for PROOF.md (CL-D2-REMAINDER-VANISHING-20260930-v1). Standard library only; exact rationals. + + E1 axial pin identities on a quintic profile f(x) = b0 + f1 x + f2 x^2/2 + f3 x^3/6 + f4 x^4/24 + f5 x^5/120: with + b0, f1, f2, f3 solved from the four pins f(-r/2) = b, f(r/2) = b - k r^3, f'(-r/2) = f'(r/2) = 0 one finds + f2 = -(r^2/24) f4, f3 = 12k - (r^2/40) f5, and alpha_M = f''(-r/2)/r = -6k + (r/12) f4 - (r^2/120) f5, + alpha_S = f''(r/2)/r = 6k + (r/12) f4 + (r^2/120) f5, alpha_M alpha_S = -36k^2 + r^2 (f4^2/144 - k f5/10) + - r^4 f5^2/14400 -- all exact at rational (r, k, f4, f5, b); mutant M1 drops the (r^2/40) f5 term; + E2 reflection symmetry: for a general quintic in (x, y) with fifteen free rational coefficients, the six pinned + coefficients (c00, c10, c20, c30, c01, c11) are solved exactly at rational r and at -r from f(M) = b, + f(S) = b - k r^3, grad f(M) = grad f(S) = 0, M = (-r/2, 0), S = (r/2, 0); the identity det H_M(-r) = det H_S(r) + holds exactly; consequently det H_M det H_S / r^2, recovered by exact Lagrange interpolation at eleven rational r + as the polynomial of degree <= 10 in r, has only even powers, constant term -36 k^2 A0^2 (A0 = f_yy(0) = 2 c02) + and the recorded r^2 coefficient (the parity is forced by the symmetry: a check of the mechanism, not of the + bookkeeping); mutant M2 applies the parity test to the single factor det H_M / r, which is not even; + E3 the block identity det K = alpha det A - r beta^T adj(A) beta, and Haynsworth's inertia additivity + inertia(K) = inertia(A) + inertia(alpha - r beta^T A^{-1} beta), on rational 2x2/3x3 blocks A that are negative + definite, of index m - 1, and indefinite, with the scalar Schur complement of both signs (inertia by exact + congruence diagonalisation); the Step 4 case split: F_d(K_M) = 0 whenever lambda_max(A_M) > 0 (A_M has a + positive eigenvalue), and |det A| <= |lambda_max(A)| * ||A||_op^(m-1) when |lambda_max(A)| is the smallest + absolute eigenvalue, at rational points; + E4 the ledger of section 2 and Remark 2 by exact monomial substitution r = (ell/k)^(1/3): r^-2 (ell/r^3)^2 = + ell^2 r^-8 (so the far-cutoff tail is ell^2 r0^-7), k^(-2/3) r^3 / k = ell k^(-8/3), ell kappa^(-5/3) = kappa^(7/3) + = ell^(7/12) at kappa = ell^(1/4), ell^(2/3) a^(-1/3) = r0 ell^(1/3) for a = ell r0^-3, and r <= k iff ell <= k^4 at + rational (k, r) with ell = k r^3; mutant M3 claims the loss exponent 1/3; + E5 the layer algebra of Step 4: k^2 u^2 = C1^2 r^2 T^2 (k + T)^2 and r T^2 <= k u / C1 for u = C1 r T (1 + T/k), exactly. + M mutants (--mutant M1|M2|M3) exit 1; an unknown label exits 2. +""" +import argparse +import json +import sys +from fractions import Fraction as F + + +# ---------------------------------------------------------------------------------------------------- linear algebra +def solve(Mx, rhs): + n = len(Mx) + A = [list(r) + [b] for r, b in zip(Mx, rhs)] + for col in range(n): + piv = next((r for r in range(col, n) if A[r][col] != 0), None) + if piv is None: + return None + A[col], A[piv] = A[piv], A[col] + inv = 1/A[col][col] + A[col] = [v*inv for v in A[col]] + for r in range(n): + if r != col and A[r][col] != 0: + f = A[r][col] + A[r] = [a - f*b for a, b in zip(A[r], A[col])] + return [A[r][n] for r in range(n)] + + +def det(M): + n = len(M) + if n == 1: + return M[0][0] + total = F(0) + for j in range(n): + minor = [row[:j] + row[j+1:] for row in M[1:]] + total += (-1)**j*M[0][j]*det(minor) + return total + + +def adj(M): + n = len(M) + out = [[F(0)]*n for _ in range(n)] + for i in range(n): + for j in range(n): + minor = [row[:j] + row[j+1:] for r_, row in enumerate(M) if r_ != i] + out[j][i] = (-1)**(i+j)*det(minor) if n > 1 else F(1) + return out + + +def inertia(M): + """(negatives, zeros, positives) of a symmetric rational matrix by congruence diagonalisation.""" + n = len(M) + A = [row[:] for row in M] + neg = zero = pos = 0 + for i in range(n): + if A[i][i] == 0: + piv = next((j for j in range(i + 1, n) if A[j][j] != 0), None) + if piv is not None: + A[i], A[piv] = A[piv], A[i] + for row in A: + row[i], row[piv] = row[piv], row[i] + else: + j = next((j for j in range(i + 1, n) if A[i][j] != 0), None) + if j is None: + zero += 1 + continue + # row_i += row_j, col_i += col_j (congruence) makes the (i,i) entry 2 A[i][j] + A[j][j] = 2 A[i][j] + for c in range(n): + A[i][c] += A[j][c] + for r_ in range(n): + A[r_][i] += A[r_][j] + p = A[i][i] + if p == 0: + zero += 1 + continue + if p < 0: + neg += 1 + else: + pos += 1 + for r_ in range(i + 1, n): + if A[r_][i] != 0: + f = A[r_][i]/p + for c in range(n): + A[r_][c] -= f*A[i][c] + for c in range(n): + A[c][r_] -= f*A[c][i] + return neg, zero, pos + + +# ---------------------------------------------------------------------------------------------------- E1 +def check_E1(mutant): + n = 0 + for (r, k, f4, f5, b) in ((F(1, 10), F(2), F(3), F(-7), F(1, 3)), (F(1, 3), F(1, 5), F(-11), F(13), F(0)), + (F(2, 7), F(4), F(1, 2), F(1, 3), F(-5))): + f2 = -(r*r/24)*f4 + f3 = 12*k - (r*r/40)*f5 + if mutant == 'M1': + f3 = 12*k + # f1, b0 from the gradient and height pins + def fx(x, f1): + return f1 + f2*x + f3*x*x/2 + f4*x**3/6 + f5*x**4/24 + # f'(-r/2) = 0 gives f1 + f1 = -(f2*(-r/2) + f3*(r*r/4)/2 + f4*(-r/2)**3/6 + f5*(r/2)**4/24) + if fx(r/2, f1) != 0: + return False, 'gradient pin at S fails' + def f(x, b0): + return b0 + f1*x + f2*x*x/2 + f3*x**3/6 + f4*x**4/24 + f5*x**5/120 + b0 = b - (f(-r/2, F(0))) + if f(-r/2, b0) != b or f(r/2, b0) != b - k*r**3: + return False, 'height pins fail' + def fxx(x): + return f2 + f3*x + f4*x*x/2 + f5*x**3/6 + aM, aS = fxx(-r/2)/r, fxx(r/2)/r + if aM != -6*k + (r/12)*f4 - (r*r/120)*f5 or aS != 6*k + (r/12)*f4 + (r*r/120)*f5: + return False, 'alpha expansions' + if aM*aS != -36*k*k + r*r*(f4*f4/144 - k*f5/10) - r**4*f5*f5/14400: + return False, 'alpha product' + n += 1 + return True, {'points': n, 'alpha_M': '-6k + (r/12) f4 - (r^2/120) f5', 'product': '-36k^2 + r^2 (f4^2/144 - k f5/10) - r^4 f5^2/14400'} + + +# ---------------------------------------------------------------------------------------------------- E2 +MONOS = [(i, j) for i in range(6) for j in range(6 - i)] # 21 monomials x^i y^j, i + j <= 5 +PINNED = [(0, 0), (1, 0), (2, 0), (3, 0), (0, 1), (1, 1)] +FREE = [m for m in MONOS if m not in PINNED] + + +def d_coef(i, j, dx, dy, x, y): + """value of d^dx_x d^dy_y (x^i y^j) at (x, y).""" + c = F(1) + for t in range(dx): + if i - t <= 0: + return F(0) + c *= (i - t) + for t in range(dy): + if j - t <= 0: + return F(0) + c *= (j - t) + return c*x**(i - dx)*y**(j - dy) + + +def pinned_poly(r, k, b, free, sign): + """Return the full coefficient dict of the pinned quintic (sign = +1: f(S) = b - k r^3; sign = -1: b + k r^3).""" + M = (-r/2, F(0)); S = (r/2, F(0)) + conds = [((0, 0), M, b), ((0, 0), S, b - sign*k*r**3), ((1, 0), M, F(0)), ((1, 0), S, F(0)), ((0, 1), M, F(0)), ((0, 1), S, F(0))] + rows, rhs = [], [] + for (dx, dy), pt, val in conds: + rows.append([d_coef(i, j, dx, dy, *pt) for (i, j) in PINNED]) + rhs.append(val - sum(free[m]*d_coef(m[0], m[1], dx, dy, *pt) for m in FREE)) + sol = solve(rows, rhs) + coef = dict(free) + for m, v in zip(PINNED, sol): + coef[m] = v + return coef + + +def hess(coef, x, y): + fxx = sum(c*d_coef(i, j, 2, 0, x, y) for (i, j), c in coef.items()) + fxy = sum(c*d_coef(i, j, 1, 1, x, y) for (i, j), c in coef.items()) + fyy = sum(c*d_coef(i, j, 0, 2, x, y) for (i, j), c in coef.items()) + return fxx, fxy, fyy + + +def interpolate(xs, ys): + """Coefficients (low to high) of the unique polynomial of degree < len(xs) through (xs, ys): exact Lagrange.""" + n = len(xs) + coeffs = [F(0)]*n + for i in range(n): + # basis polynomial l_i + num = [F(1)] + denom = F(1) + for j in range(n): + if j != i: + num = [F(0)] + num + for t in range(len(num) - 1): + num[t] -= xs[j]*num[t + 1] + denom *= (xs[i] - xs[j]) + for t in range(n): + coeffs[t] += ys[i]*num[t]/denom + return coeffs + + +def check_E2(mutant): + k, b = F(3, 2), F(-1, 4) + free = {} + vals = [F(2), F(-1), F(1, 2), F(3), F(-2, 3), F(5), F(-1, 5), F(7, 3), F(1), F(-4), F(2, 7), F(-3, 2), F(4, 5), F(-1, 7), F(6)] + for m, v in zip(FREE, vals): + free[m] = v + sign = 1 + def dets(r): + coef = pinned_poly(r, k, b, free, sign) + fxxM, fxyM, fyyM = hess(coef, -r/2, F(0)) + fxxS, fxyS, fyyS = hess(coef, r/2, F(0)) + return fxxM*fyyM - fxyM*fxyM, fxxS*fyyS - fxyS*fxyS + # the reflection symmetry: the pinned family at -r has M and S exchanged, so det H_M(-r) = det H_S(r) + for r in (F(1, 10), F(3, 7), F(1)): + dMm, dSm = dets(-r) + dMp, dSp = dets(r) + if dMm != dSp or dSm != dMp: + return False, 'reflection identity det H_M(-r) = det H_S(r) fails' + def value(r): + dM, dS = dets(r) + if mutant == 'M2': + return dM/r # a single endpoint: NOT even in r + return dM*dS/(r*r) + xs = [F(n, 10) for n in range(1, 12)] # eleven rational r values + ys = [value(r) for r in xs] + poly = interpolate(xs, ys) + # verify at a twelfth value that the degree-10 interpolant is the polynomial (degree <= 10 in r) + r12 = F(13, 10) + if sum(c*r12**t for t, c in enumerate(poly)) != value(r12): + return False, 'not a polynomial of degree <= 10 in r' + odd = [t for t in range(1, 11, 2) if poly[t] != 0] + if odd: + return False, 'odd powers present: %s' % odd + A0 = 2*free[(0, 2)] + if poly[0] != -36*k*k*A0*A0: + return False, 'constant term is not -36 k^2 A0^2' + c02, c12, c21, c22, c31, c40, c50 = (free[(0, 2)], free[(1, 2)], free[(2, 1)], free[(2, 2)], free[(3, 1)], free[(4, 0)], free[(5, 0)]) + r2 = (16*c02**2*c40**2 - 48*c02**2*c50*k - 8*c02*c21**2*c40 + 24*c02*c21*c31*k - 72*c02*c22*k*k + + 36*c12**2*k*k - 12*c12*c21**2*k + c21**4) + if poly[2] != r2: + return False, 'r^2 coefficient differs from the displayed polynomial' + return True, {'reflection_identity': 'det H_M(-r) = det H_S(r) at 3 rational r', 'degrees_present': [t for t in range(11) if poly[t] != 0], + 'constant': str(poly[0]), 'r2_coefficient': str(poly[2])} + + +# ---------------------------------------------------------------------------------------------------- E3 +def block(alpha, beta, A, r): + n = len(A) + 1 + K = [[F(0)]*n for _ in range(n)] + K[0][0] = alpha + for i in range(len(A)): + K[0][i+1] = K[i+1][0] = r*beta[i] # sqrt(r) beta entries squared give r; with r rational we use t = r directly + for j in range(len(A)): + K[i+1][j+1] = A[i][j] + return K + + +def check_E3(mutant): + # Use K_t with entries t*beta in place of sqrt(t) beta: det = alpha det A - t^2 beta^T adj(A) beta. To test the + # displayed identity with parameter r we take t^2 = r, i.e. entries sqrt(r) beta: choose r a rational square. + cases = 0 + A_list = [ + [[F(-2), F(1, 2)], [F(1, 2), F(-3)]], # negative definite + [[F(-2), F(0)], [F(0), F(1)]], # index m-1 = 1 + [[F(-3), F(1), F(0)], [F(1), F(-2), F(1, 2)], [F(0), F(1, 2), F(-4)]], # negative definite 3x3 + [[F(-3), F(1), F(0)], [F(1), F(2), F(1, 2)], [F(0), F(1, 2), F(-4)]], # indefinite 3x3 + ] + for A in A_list: + m = len(A) + adjA = adj(A); dA = det(A) + for beta in ([F(1), F(-2)] if m == 2 else [F(1), F(-2), F(1, 3)], [F(0)]*m): + for alpha in (F(-5), F(-1, 10), F(1, 10), F(5)): + for s in (F(1, 2), F(2)): # sqrt(r) = s, r = s^2 + r = s*s + n = m + 1 + K = [[F(0)]*n for _ in range(n)] + K[0][0] = alpha + for i in range(m): + K[0][i+1] = K[i+1][0] = s*beta[i] + for j in range(m): + K[i+1][j+1] = A[i][j] + q = sum(beta[i]*sum(adjA[i][j]*beta[j] for j in range(m)) for i in range(m)) + if det(K) != alpha*dA - r*q: + return False, 'block determinant identity' + if dA != 0: + sigma = alpha - r*q/dA # alpha - r beta^T A^{-1} beta (A^{-1} = adj/det) + negK = inertia(K)[0] + negA = inertia(A)[0] + if negK != negA + (1 if sigma < 0 else 0): + return False, 'Haynsworth inertia additivity fails' + cases += 1 + # good-event inequalities: A_S negative definite and alpha_S > 0 give sigma_S > 0 + A = A_list[0]; adjA = adj(A); dA = det(A) + for beta in ([F(1), F(-2)], [F(3), F(1, 7)]): + q = sum(beta[i]*sum(adjA[i][j]*beta[j] for j in range(2)) for i in range(2)) + for alpha in (F(1, 100), F(3)): + for r in (F(1, 10), F(1)): + if not (alpha - r*q/dA > 0): + return False, 'sigma_S > 0 fails' + # sigma_M < 0 under the margins: alpha_M <= -5k, r beta^T(-A)^{-1}beta <= 2rT^2/u <= 2k/C1 + k, T, C1, r = F(1), F(4), F(100), F(1, 1000) + u = C1*r*T*(1 + T/k) + if not (2*r*T*T/u <= 2*k/C1 and -5*k + 2*k/C1 < 0): + return False, 'sigma_M margin' + # Step 4, second layer: A_M with a positive eigenvalue => K_M has a positive eigenvalue => F_d(K_M) = 0 + layer2 = 0 + for A in ([[F(-2), F(0)], [F(0), F(1, 50)]], [[F(-3), F(1)], [F(1), F(1, 10)]], [[F(-3), F(1), F(0)], [F(1), F(1, 20), F(1, 2)], [F(0), F(1, 2), F(-4)]]): + m = len(A) + if inertia(A)[2] == 0: + return False, 'test matrix has no positive eigenvalue' + for alpha in (F(-5), F(-1, 10)): + for s_ in (F(1, 2), F(1, 10)): + beta = [F(1)]*m + n = m + 1 + K = [[F(0)]*n for _ in range(n)] + K[0][0] = alpha + for i in range(m): + K[0][i+1] = K[i+1][0] = s_*beta[i] + for j in range(m): + K[i+1][j+1] = A[i][j] + if inertia(K)[2] == 0: # K negative semidefinite would give index d + return False, 'K_M negative definite although A_M has a positive eigenvalue' + layer2 += 1 + # Step 4, third layer: |det A| <= |lambda_max(A)| ||A||_op^(m-1) when lambda_max is the eigenvalue of least modulus: + # diagonal examples, exact + for diag in ([F(-3), F(-1, 100)], [F(-5), F(-2), F(1, 1000)], [F(-4), F(-3), F(-1, 10)]): + A = [[F(0)]*len(diag) for _ in diag] + for i, dv in enumerate(diag): + A[i][i] = dv + lam_max = max(diag) + opnorm = max(abs(v) for v in diag) + if not (abs(det(A)) <= abs(lam_max)*opnorm**(len(diag) - 1)): + return False, 'layer determinant bound' + return True, {'cases': cases, 'positive_eigenvalue_cases': layer2} + + +# ---------------------------------------------------------------------------------------------------- E4 +class Mono: + def __init__(self, ell=F(0), k=F(0), r0=F(0)): + self.e = (F(ell), F(k), F(r0)) + def __mul__(self, o): + return Mono(*[a + b for a, b in zip(self.e, o.e)]) + def __pow__(self, p): + p = F(p); return Mono(*[a*p for a in self.e]) + + +def check_E4(mutant): + ell, k, r0 = Mono(1, 0, 0), Mono(0, 1, 0), Mono(0, 0, 1) + r = (ell*k**(-1))**F(1, 3) + a = ell*r0**(-3) + kappa = ell**F(1, 4) + rr = Mono(0, 0, 1) # a separation variable, reusing the third slot + claims = { + 'r^-2 (ell/r^3)^2 = ell^2 r^-8': (((rr**(-2))*(ell*rr**(-3))**2).e, (F(2), F(0), F(-8))), + 'k^-2/3 r^2': ((k**F(-2, 3)*r**2).e, (F(2, 3), F(-4, 3), F(0))), + 'k^-2/3 r^3/k': ((k**F(-2, 3)*r**3*k**(-1)).e, (F(1), F(-8, 3), F(0))), + 'ell^2/3 a^-1/3': (((ell**F(2, 3))*a**F(-1, 3)).e, (F(1, 3), F(0), F(1))), + 'ell kappa^-5/3': ((ell*kappa**F(-5, 3)).e, (F(7, 12), F(0), F(0))), + 'kappa^7/3': ((kappa**F(7, 3)).e, (F(7, 12), F(0), F(0))), + 'a^7/3 ell^-1/3': ((a**F(7, 3)*ell**F(-1, 3)).e, (F(2), F(0), F(-7))), + } + for name, (got, want) in claims.items(): + if got != want: + return False, 'monomial claim fails: %s got %s' % (name, got) + # absolute loss exponent: ell^(7/12) scaled -> ell^(7/12 - 1/3) = ell^(1/4) + loss = F(7, 12) - F(1, 3) + if mutant == 'M3': + loss = F(1, 3) + if loss != F(1, 4): + return False, 'loss exponent' + # r <= k <=> ell <= k^4, with r = (ell/k)^(1/3) computed exactly where ell/k is a rational cube + for (K, rv) in ((F(1, 10), F(1, 10)), (F(1, 10), F(1, 5)), (F(1, 2), F(1, 4)), (F(1, 16), F(1, 8))): + L = K*rv**3 # ell = k r^3, so r = (ell/k)^(1/3) exactly + if (rv <= K) != (L <= K**4): + return False, 'threshold r <= k <=> ell <= k^4 fails' + return True, {name: [str(x) for x in got] for name, (got, want) in claims.items()} + + +# ---------------------------------------------------------------------------------------------------- E5 +def check_E5(mutant): + for (k, T, C1, r) in ((F(1, 3), F(5), F(50), F(1, 100)), (F(4), F(2), F(10), F(1, 7)), (F(1, 100), F(30), F(1000), F(1, 10**6))): + u = C1*r*T*(1 + T/k) + if k*k*u*u != C1*C1*r*r*T*T*(k + T)**2: + return False, 'k^2 u^2 identity' + if not (r*T*T <= k*u/C1): + return False, 'rT^2 <= ku/C1' + return True, {'identity': 'k^2 u^2 = C1^2 r^2 T^2 (k+T)^2', 'inequality': 'r T^2 <= k u / C1'} + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument('--mutant', default=None) + args = ap.parse_args() + mutant = args.mutant + if mutant is not None and mutant not in ('M1', 'M2', 'M3'): + sys.stderr.write('unknown mutant label\n'); sys.exit(2) + results = {} + ok_all = True + for name, fn in (('E1_axial_pins_quintic', check_E1), ('E2_parity_pinned_quintic_2d', check_E2), ('E3_block_and_inertia', check_E3), + ('E4_ledger', check_E4), ('E5_layer_algebra', check_E5)): + ok, info = fn(mutant) + results[name] = {'passed': bool(ok), 'info': info} + ok_all = ok_all and ok + out = {'object': 'CL-D2-REMAINDER-VANISHING-20260930-v1', 'scientific_effect': 'NONE', 'passed': ok_all, 'checks': results} + print(json.dumps(out, indent=1, sort_keys=True)) + sys.exit(0 if ok_all else 1) + + +if __name__ == '__main__': + main() From abae6d0b08f39a6b244308c4e351327c1ef56890 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 30 Sep 2026 17:06:24 +0000 Subject: [PATCH 5/5] Remainder vanishing v1.1: xAI review 5369140697 applied (R3.2 and the scaling dictionary quoted; controls' scope stated; (R4) import quoted; signed near bound proved as a separate remark) Theorem R+ packet, v1 -> v1.1. No change to Lemma E, Theorem R+ or (R+.1)-(R+.3). Scientific effect NONE. A1: [R] section 4's scaling dictionary (D_r = diag(sqrt r, I), alpha_i, beta_i, off-diagonal sqrt(r) beta_i, |det H_i|/r = |det K_i|) and Lemma R3.2 are quoted verbatim in section 0 and Step 3; det K_i = alpha_i det A_i - r q_i is R3.2 at t = r. The checker's E3 comment (which read as t^2) is corrected; the code was and is s = sqrt(r), entries s*beta, det K = alpha det A - s^2 q. A2: "What the controls do not test" paragraph in PROOF.md section 5, README and the checker docstring: Step 4 as a random-matrix statement, Step 5, section 2 are prose-only (slices A and B). A3: [R] (R4) quoted at the definition of T ("for finite p>=1 and each finite derivative order q"); q = 7 and q = 2 named. B2: the signed near bound proved (A_r >= 0 for every r, A_0 <= k^2 H, split at min(ell^{1/4}, r_0)) as a remark separate from (R+.3). B1: the not-claimed list extended (no RN/24-jet closure; R+ does not enlarge (Z4)). RESULTS.json regenerated (object v1.1; -O identical; M1-M3 exit 1, unknown label exit 2); SOURCES.json regenerated with the new packet identities; bound sources unchanged. Workflow gate replayed locally: PASS. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU --- .../remainder_vanishing_20260930/PROOF.md | 75 ++++++++++++++----- .../remainder_vanishing_20260930/README.md | 17 ++++- .../remainder_vanishing_20260930/RESULTS.json | 2 +- .../remainder_vanishing_20260930/SOURCES.json | 20 ++--- .../even_contact_check.py | 16 ++-- 5 files changed, 95 insertions(+), 35 deletions(-) diff --git a/frontiers/remainder_vanishing_20260930/PROOF.md b/frontiers/remainder_vanishing_20260930/PROOF.md index 2a3659c8b..441152dfc 100644 --- a/frontiers/remainder_vanishing_20260930/PROOF.md +++ b/frontiers/remainder_vanishing_20260930/PROOF.md @@ -1,6 +1,8 @@ # The bounded remainder of Theorem R: `B_{d,L}` for candidates, `0` for elder pairs -Object: CL-D2-REMAINDER-VANISHING-20260930-v1. +Object: CL-D2-REMAINDER-VANISHING-20260930-v1.1 (v1 → v1.1: xAI review 5369140697 on Math- #191 — A1 the scaling +dictionary and Lemma R3.2 quoted verbatim, A2 the controls' scope stated, A3 the (R4) import quoted, B2 the signed +near bound proved as a separate remark; no change to Lemma E, Theorem R+ or (R+.1)–(R+.3)). Author: Anthropic Claude (claude.ai session `session_01NMeKEismAyeqgdB4sy2NJU`), 30 September 2026. Disposition: AUTHOR-SIDE PROOF CANDIDATE; NONAUTHOR REVIEW REQUIRED. Scientific effect: NONE — no register, graph, STATUS, PROOF_INDEX, prize or Boolean change; no numerical constant is claimed. Same GitHub account as @@ -14,8 +16,11 @@ Setting, notation and every display number `(Rn)` are those of [R] (`frontiers/t LIFETIME_REMAINDER.md`, blob `247b3ecf`, Theorem R; xAI R1–R6 on main #67, Anthropic full depth Math- #186): fixed `d ≥ 2`, `L > 0`, the [P] field on `X = R^d/(LZ^d)`; near pins `M = −ru/2`, `S = ru/2` with heights `b`, `b − kr³` and zero gradients; the observation rows `U_r`, target `v_r`, density `π_r`, the regression law `Q`, -the coupling `F_r` of [R] (R3)–(R4), `m = d − 1`, `P = 1 + |b| + k`; the scaled endpoint Hessians -`K_i = D_r^{−1}H_iD_r^{−1}` with `α_i = F_{r,xx}(i)/r`, `β_i = ∇_yF_{r,x}(i)/r`, `A_i = D_y²F_r(i)` (`i = M, S`); the +the coupling `F_r` of [R] (R3)–(R4), `m = d − 1`, `P = 1 + |b| + k`; the scaled endpoint Hessians of [R] §4 +(*scaling dictionary*, quoted): "`alpha_i=F_r,xx(i)/r` and `beta_i=grad_y F_r,x(i)/r`. Let `D_r=diag(sqrt(r),I)`. +Then `K_i=D_r^(-1) H_i D_r^(-1) =[[alpha_i,sqrt(r) beta_i^T],[sqrt(r) beta_i,A_i]]`, `|det H_i|/r=|det K_i|`" — so +`H_i` (the full Hessian of `F_r` at the pin `i`, in the coordinates `(x, y)`) has entries `rα_i`, `rβ_i`, `A_i`, and +`K_i` has the scalar `α_i`, the off-diagonal `√r β_i` and the transverse block `A_i = D_y²F_r(i)` (`i = M, S`); the filtered determinants `F_j`; `Z_r/r² = E_Q[F_d(K_M)F_{d−1}(K_S)]`; `A_0 = D_y²F_0(0)`, `z_0 = E[(6k)²(det A_0)²1{A_0 < 0}]`; `A_r = 12π_r(v_r)Z_r/r²`, `A_0 = 12π_0(v_0)z_0`; the majorant `H(b,k) = CP^Ne^{−c(b²+k²)}` (`N` enlarged when needed); the near/far split at a separation `r_0`, `a = ℓ/r_0³`; and @@ -51,17 +56,24 @@ candidate density and `0` for the elder density. Moreover, for every `r_0 ∈ (0 ν_cand^{near,r_0}(ℓ) − cℓ^{−1/3} → ∫_{0=1 and each +finite derivative order q**, `||F_r-F_0||_{L^p(C^q)} <= C_{p,q} r^2 P`, `||1+||F_r||_{C^q}+||F_0||_{C^q}||_p <= C_{p,q} P`, +`P=1+|b|+k`" — the second line with `q = 7` bounds the `C^7` norms in `L^p`, the first with `q = 2` bounds +`r^{−2}‖F_r − F_0‖_{C^2}` in `L^p`, so `T := 1 + k + ‖F_r‖_{C^7} + ‖F_0‖_{C^7} + r^{−2}‖F_r − F_0‖_{C^2}` has +`‖T‖_p ≤ C_pP` for every `p` (`[R]` §4 chose `q = 4` for its `T` because (R8)–(R11) need four derivatives; the +`C^q` moments exist for every `q` because `F_r` is the Gaussian regression of the smooth [P] field on finitely many +rows, [R] §2). Write `f = F_r`, `f_j = ∂_x^jf(0)`, and `O(x)` for a quantity bounded by `C|x|` with `C = C(d)`. *Step 1 (axial pins to second order).* The third and fourth rows of `U_r` at their pinned values `0` and `12k` give, by Taylor's formula with integral remainder (the rules are centred, so the odd orders cancel), @@ -95,7 +107,16 @@ The transverse difference row `(f_y(S) − f_y(M))/r = f_{xy}(0) + (r²/24)f_{xx (The sign of `β_i` enters `q_i` quadratically. That `f_{xy}(0)` is `O(r²)` and not `O(r)` is essential: an `O(r)` value would shift `β_M` and `β_S` by a common `O(1)` and make `q_M − q_S = O(1)`.) -*Step 3 (the product of determinants).* By the exact identity `det K_i = α_i det A_i − r q_i` ([R] Lemma R3.2), +*Step 3 (the product of determinants).* [R] Lemma R3.2, quoted: "For a symmetric (n-1) by (n-1) matrix A, scalar +alpha, vector beta and t>=0, set `K_t=[[alpha,sqrt(t) beta^T],[sqrt(t) beta,A]]`. … Indeed +`det K_t=alpha det A-t beta^T adj(A) beta`, INCLUDING singular A." With `t = r` and `(alpha, beta, A) = (α_i, β_i, A_i)`, +`K_r` is the scaled Hessian `K_i` of the dictionary in §0 (off-diagonal entries `√r β_i`), so the exact identity is + + det K_i = α_i det A_i − r β_iᵀadj(A_i)β_i = α_i det A_i − r q_i, + +`q_i` as in (1.5): the parameter multiplying `q_i` is the first power of `r` because the off-diagonal entries of `K_i` +carry `√r` (with `β_i = ∇_yF_{r,x}(i)/r` already containing the `1/r` of the dictionary; in terms of the unscaled +Hessian, `det H_i = r det K_i = rα_i det A_i − r²q_i`). Hence det K_M det K_S = α_Mα_S det A_M det A_S − r(α_M det A_M q_S + α_S det A_S q_M) + r² q_M q_S. @@ -174,9 +195,18 @@ is continuous in the target. Also `A_0(b, k, u) → 0` (`A_0 ≤ k²H`). Since ` ν_cand^{near,r_0}(ℓ) − cℓ^{−1/3} → ∫_0^{r_0}∫∫ r^{d−1}Ψ_0(b, ru) dσ db dr = ∫_{0 0`, and the layer inequality `|det A| ≤ (|λ_max(A)|)·‖A‖^{m−1}` for `|λ_max(A)|` small. +E3 the block identity `det K = α det A − r βᵀadj(A)β` for `K = [[α, √r βᵀ],[√r β, A]]` (`r` a rational square, +`s = √r` rational, entries `s·β` — [R] Lemma R3.2 with `t = r`, the dictionary of §0) and Haynsworth's inertia count +on rational `3×3` and `4×4` examples with `A` negative definite, of index `m − 1`, and indefinite, and the scalar +Schur complement of both signs (inertia by exact congruence diagonalisation); the Step 4 case split at rational +points: `F_d(K_M) = 0` when `λ_max(A_M) > 0`, and the layer inequality `|det A| ≤ (|λ_max(A)|)·‖A‖^{m−1}` for +`|λ_max(A)|` small. E4 the ledger of §2 and Remark 2 by exact monomial substitution `r = (ℓ/k)^{1/3}`: `r^{−2}(ℓ/r³)² = ℓ²r^{−8}` (so `∫_{r_0}^∞ ≍ ℓ²r_0^{−7}`), `k^{−2/3}r^{3}/k = ℓk^{−8/3}`, `ℓκ^{−5/3} = κ^{7/3} = ℓ^{7/12}` at `κ = ℓ^{1/4}`, `ℓ^{2/3}a^{−1/3} = r_0ℓ^{1/3}`, and `r ≤ k ⇔ ℓ ≤ k⁴`; mutant M3 (claims the loss exponent `1/3`) fails. E5 the layer algebra of Step 4: `k²u² = C_1²r²T²(k + T)²` and `rT² ≤ ku/C_1` for `u = C_1rT(1 + T/k)`, exactly. -Mutants `M1`–`M3` exit 1; an unknown label exits 2. The controls check identities and bookkeeping; they do not prove -the Gaussian estimates and are not acceptance. +Mutants `M1`–`M3` exit 1; an unknown label exits 2. + +**What the controls do not test.** They check exact identities and finitely many rational instances of Steps 1–3 +(E1, E2), of the block/inertia facts and the case split of Step 4 (E3), of the ledger (E4) and of the layer algebra +(E5). They do **not** test Step 4 as a statement about the random matrices — the Weyl and Hadamard bounds on the +layer `{|λ_max(A_0)| < u}`, the choice of `C_1`, and the claim that the product of the two typed determinants is +`O(r²)` times a polynomial in `T` there — nor Step 5 (the `C^7` moment import from (R4) and the passage to +expectations), nor anything in §2 (the majorant, the pointwise limit, the far limit, the use of (Z4)). Those are +proved in prose only and are review slice A (Steps 4–5) and slice B (§2). The controls are not acceptance. ## 6. Review slices diff --git a/frontiers/remainder_vanishing_20260930/README.md b/frontiers/remainder_vanishing_20260930/README.md index 462c6d5e9..097ed0e6e 100644 --- a/frontiers/remainder_vanishing_20260930/README.md +++ b/frontiers/remainder_vanishing_20260930/README.md @@ -1,4 +1,4 @@ -# The remainder of Theorem R: `B_{d,L}` for candidates, `0` for elder pairs (CL-D2-REMAINDER-VANISHING-20260930-v1) +# The remainder of Theorem R: `B_{d,L}` for candidates, `0` for elder pairs (CL-D2-REMAINDER-VANISHING-20260930-v1.1) Author-side proof candidate, Anthropic Claude, 30 September 2026. Scientific effect NONE. Nonauthor review required. Relative to merged, reviewed sources only ([R] Theorem R, [Z] Theorem Z, [C7-K], the reconciled [P] chain); @@ -33,5 +33,20 @@ flip layer, repaired by the three-case split; the theorem's independence from #1 assumed; the direct identification of the constant `B_{d,L}` through Theorem Z; Proposition L being [C7-K] §4's own proof; the norms `T` controls; controls that were symmetry-forced or tautological) were applied. +**What the controls do not test.** E1–E5 check exact identities and finitely many rational instances (Steps 1–3, +the block/inertia facts and case split of Step 4, the ledger, the layer algebra). They do not test Step 4 as a +statement about random matrices (the Weyl/Hadamard layer bound, the choice of `C_1`, the `O(r²)` product on the +flip layer), nor Step 5 (the `C^7` moment import from [R] (R4), quoted in PROOF.md §1, and the expectations), nor +§2 (majorant, pointwise and far limits, the use of (Z4)). Those are proved in prose only; they are review slices A +(Steps 4–5) and B (§2). The controls are not acceptance. + +v1 → v1.1 (xAI review 5369140697 on Math- #191): A1 the scaling dictionary of [R] §4 and Lemma R3.2 quoted +verbatim in §0 and Step 3 (the `r` multiplying `q_i` is R3.2's `t = r`, the off-diagonal of `K_i` being `√r β_i`; +the checker's E3 comment, which read as `t²`, corrected — the code was and is `s = √r`, `det K = α det A − s²q`); +A2 the paragraph above; A3 [R] (R4)'s "for finite p>=1 and each finite derivative order q" quoted at the definition +of `T`; B2 the signed near bound proved in §2 as a separate remark (from `A_r ≥ 0` for every `r` and `A_0 ≤ k²H`), +not part of (R+.3); B1 the not-claimed list extended (no RN/24-jet closure; R+ does not enlarge (Z4)). Lemma E, +Theorem R+ and (R+.1)–(R+.3) unchanged. + Review slices (§6): A Lemma E; B the separation-variable limit argument and the use of Theorem Z; C scope and remarks. diff --git a/frontiers/remainder_vanishing_20260930/RESULTS.json b/frontiers/remainder_vanishing_20260930/RESULTS.json index 453c61e19..4d636012e 100644 --- a/frontiers/remainder_vanishing_20260930/RESULTS.json +++ b/frontiers/remainder_vanishing_20260930/RESULTS.json @@ -79,7 +79,7 @@ "passed": true } }, - "object": "CL-D2-REMAINDER-VANISHING-20260930-v1", + "object": "CL-D2-REMAINDER-VANISHING-20260930-v1.1", "passed": true, "scientific_effect": "NONE" } diff --git a/frontiers/remainder_vanishing_20260930/SOURCES.json b/frontiers/remainder_vanishing_20260930/SOURCES.json index 0a7e2dc88..73732cec0 100644 --- a/frontiers/remainder_vanishing_20260930/SOURCES.json +++ b/frontiers/remainder_vanishing_20260930/SOURCES.json @@ -1,12 +1,12 @@ { "schema": 1, "scientific_effect": "NONE", - "object": "CL-D2-REMAINDER-VANISHING-20260930-v1", + "object": "CL-D2-REMAINDER-VANISHING-20260930-v1.1", "kind": "author-side proof candidate: Lemma E (even contact expansion) and Theorem R+ (nu_cand = c ell^-1/3 + B_{d,L} + o(1), nu_eld = c ell^-1/3 + o(1)) relative to the merged reviewed sources [R], [Z], [C7-K] and the reconciled [P] chain; nothing unmerged consumed; nonauthor analytic review required", "author": "Anthropic Claude", "session": "https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU", "read_at": { - "branch_base": "2a10ed34e0377b84601378124dd33a8de1e0fe0b" + "branch_base": "3e0a91b69892b9717564c592e7a966492a81566a" }, "consumed": [ { @@ -120,23 +120,23 @@ "files": [ { "path": "PROOF.md", - "bytes": 21505, - "sha256": "aedc1e19f9fb3ec4bc48a82c607441c88f9acc7cb048939ae89c2de4a1d2065d" + "bytes": 25353, + "sha256": "0cb5b949261476f10e539677e2744e3288752474393af25ba787e67b1350f32a" }, { "path": "even_contact_check.py", - "bytes": 19510, - "sha256": "b6075fc55658814396d296c70affbdf1d1f39e5beb276e3622920bfe247cb001" + "bytes": 20220, + "sha256": "473ae49f2d4b3a319b5bd90a28ef34c7c9ae8a6f7af953d75ebc39969ea02f74" }, { "path": "RESULTS.json", - "bytes": 1391, - "sha256": "f869ad1f20c97e090819bf635525027c91c53124bb06fbcf06c5b5e1b57caacc" + "bytes": 1393, + "sha256": "b58b5e90419415c69aa16f1a13e09920147db9e24b131bd53864beb67fb6e428" }, { "path": "README.md", - "bytes": 3015, - "sha256": "a729cfc8d6d7fb426b3e93cb524a5940a29c1655541cdfde1bc7773368042cb5" + "bytes": 4393, + "sha256": "f3078a42edc8a0dbe88b6cca645ddff1518366756c2423b3ffc898bb283cd02f" } ] } diff --git a/frontiers/remainder_vanishing_20260930/even_contact_check.py b/frontiers/remainder_vanishing_20260930/even_contact_check.py index 437b5b3c0..5c1cd64ae 100644 --- a/frontiers/remainder_vanishing_20260930/even_contact_check.py +++ b/frontiers/remainder_vanishing_20260930/even_contact_check.py @@ -1,5 +1,5 @@ #!/usr/bin/env python3 -"""Exact finite controls for PROOF.md (CL-D2-REMAINDER-VANISHING-20260930-v1). Standard library only; exact rationals. +"""Exact finite controls for PROOF.md (CL-D2-REMAINDER-VANISHING-20260930-v1.1). Standard library only; exact rationals. E1 axial pin identities on a quintic profile f(x) = b0 + f1 x + f2 x^2/2 + f3 x^3/6 + f4 x^4/24 + f5 x^5/120: with b0, f1, f2, f3 solved from the four pins f(-r/2) = b, f(r/2) = b - k r^3, f'(-r/2) = f'(r/2) = 0 one finds @@ -13,7 +13,8 @@ as the polynomial of degree <= 10 in r, has only even powers, constant term -36 k^2 A0^2 (A0 = f_yy(0) = 2 c02) and the recorded r^2 coefficient (the parity is forced by the symmetry: a check of the mechanism, not of the bookkeeping); mutant M2 applies the parity test to the single factor det H_M / r, which is not even; - E3 the block identity det K = alpha det A - r beta^T adj(A) beta, and Haynsworth's inertia additivity + E3 the block identity det K = alpha det A - r beta^T adj(A) beta for K = [[alpha, sqrt(r) beta^T], [sqrt(r) beta, A]] + ([R] Lemma R3.2 with t = r; r a rational square, entries sqrt(r) beta), and Haynsworth's inertia additivity inertia(K) = inertia(A) + inertia(alpha - r beta^T A^{-1} beta), on rational 2x2/3x3 blocks A that are negative definite, of index m - 1, and indefinite, with the scalar Schur complement of both signs (inertia by exact congruence diagonalisation); the Step 4 case split: F_d(K_M) = 0 whenever lambda_max(A_M) > 0 (A_M has a @@ -25,6 +26,10 @@ rational (k, r) with ell = k r^3; mutant M3 claims the loss exponent 1/3; E5 the layer algebra of Step 4: k^2 u^2 = C1^2 r^2 T^2 (k + T)^2 and r T^2 <= k u / C1 for u = C1 r T (1 + T/k), exactly. M mutants (--mutant M1|M2|M3) exit 1; an unknown label exits 2. + Scope: E1-E5 check exact identities and finitely many rational instances. They do NOT test Step 4 of PROOF.md as a + statement about random matrices (the Weyl/Hadamard layer bound, the choice of C1, the O(r^2) product on the flip + layer), nor Step 5 (the C^7 moment import from [R] (R4) and the expectations), nor section 2 (majorant, pointwise + and far limits, the use of (Z4)); those are proved in prose only. The controls are not acceptance. """ import argparse import json @@ -262,8 +267,9 @@ def block(alpha, beta, A, r): def check_E3(mutant): - # Use K_t with entries t*beta in place of sqrt(t) beta: det = alpha det A - t^2 beta^T adj(A) beta. To test the - # displayed identity with parameter r we take t^2 = r, i.e. entries sqrt(r) beta: choose r a rational square. + # [R] Lemma R3.2 with t = r: K = [[alpha, sqrt(r) beta^T], [sqrt(r) beta, A]] and det K = alpha det A - r beta^T adj(A) beta. + # Exact rationals: r is chosen a rational square, s = sqrt(r) rational, and the off-diagonal entries are s*beta, + # so the identity tested is det K = alpha det A - s^2 q = alpha det A - r q with q = beta^T adj(A) beta. cases = 0 A_list = [ [[F(-2), F(1, 2)], [F(1, 2), F(-3)]], # negative definite @@ -407,7 +413,7 @@ def main(): ok, info = fn(mutant) results[name] = {'passed': bool(ok), 'info': info} ok_all = ok_all and ok - out = {'object': 'CL-D2-REMAINDER-VANISHING-20260930-v1', 'scientific_effect': 'NONE', 'passed': ok_all, 'checks': results} + out = {'object': 'CL-D2-REMAINDER-VANISHING-20260930-v1.1', 'scientific_effect': 'NONE', 'passed': ok_all, 'checks': results} print(json.dumps(out, indent=1, sort_keys=True)) sys.exit(0 if ok_all else 1)