diff --git a/.github/workflows/ordinary-short-bar-occurrence.yml b/.github/workflows/ordinary-short-bar-occurrence.yml new file mode 100644 index 000000000..77c172cd6 --- /dev/null +++ b/.github/workflows/ordinary-short-bar-occurrence.yml @@ -0,0 +1,53 @@ +name: Ordinary short-bar occurrence exact controls +on: + pull_request: + paths: + - 'frontiers/ordinary_short_bar_occurrence_20261001/**' + - 'frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md' + - 'frontiers/short_bar_endpoint_law_20261001/PROOF.md' + - 'imports/lifetime_parent_20260925/**' + - 'reviews/d1_section9_borel_repair_20260925/REPAIR.md' + - 'reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md' + - '.github/workflows/ordinary-short-bar-occurrence.yml' + push: + branches: [main] + paths: + - 'frontiers/ordinary_short_bar_occurrence_20261001/**' + - 'frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md' + - 'frontiers/short_bar_endpoint_law_20261001/PROOF.md' + - 'imports/lifetime_parent_20260925/**' + - 'reviews/d1_section9_borel_repair_20260925/REPAIR.md' + - 'reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md' + - '.github/workflows/ordinary-short-bar-occurrence.yml' + workflow_dispatch: +permissions: + contents: read +concurrency: + group: ordinary-short-bar-occurrence-${{ github.ref }} + cancel-in-progress: true +jobs: + exact: + runs-on: ubuntu-latest + timeout-minutes: 5 + strategy: + matrix: + mode: [normal, optimized] + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 + with: + persist-credentials: false + - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 + with: + python-version: '3.11' + - name: Verify pinned sources and rational falsifiers + env: + PYTHON_MODE: ${{ matrix.mode }} + run: | + if [ "$PYTHON_MODE" = optimized ]; then + python3 -B -O -S frontiers/ordinary_short_bar_occurrence_20261001/test_check.py -v + else + python3 -B -S frontiers/ordinary_short_bar_occurrence_20261001/test_check.py -v + fi + - name: Reject implementation mutations in both Python modes + if: matrix.mode == 'normal' + run: python3 -B -S frontiers/ordinary_short_bar_occurrence_20261001/test_check.py --mutants diff --git a/frontiers/ordinary_short_bar_occurrence_20261001/FOLD_ISOLATION.md b/frontiers/ordinary_short_bar_occurrence_20261001/FOLD_ISOLATION.md new file mode 100644 index 000000000..a3d4e7c4c --- /dev/null +++ b/frontiers/ordinary_short_bar_occurrence_20261001/FOLD_ISOLATION.md @@ -0,0 +1,421 @@ +# A typical ordinary fold is the only possible short-bar pair + +Object: OA-ORDINARY-FOLD-ISOLATION-20261001-v1. +Authors: OpenAI/Codex root and c52_fold_feasibility, under Dylan Roy's delegation. +This is an analytic candidate with the exact retained source interfaces below. +It is coauthor work, not an independent review or a scientific-status change. + +## 1. The observable and the precise new lemma + +Fix the planar torus T_L²=R²/(LZ²), with L>0 fixed, and exactly the centered, +unit-variance periodized Gaussian covariance in [P, §1]. Keep the ordinary +finite SUPERLEVEL H0 convention of [P, §8], with the essential global-maximum +class excluded. Write K_tau(f) for the number of such bars whose lifetime is +in (0,tau]. On the Morse/distinct-critical-value locus it is finite; assign +K_tau=0 outside that locus. No spatial, birth-height, gap-mark or witness +restriction is imposed on this count. + +Fix b in R, k>0 and an orthonormal planar frame R=(u,e_z). Work in its local +coordinates (x,z), centered at the midpoint. Choose all sufficiently small +r>0 below the embedding radius in [REC, §1]. The exact pins are + + M_r=(-r/2,0), S_r=(r/2,0), + f(M_r)=b, f(S_r)=b-k r³, grad f(M_r)=grad f(S_r)=0. + +Let Q_r=Q_(r,b,k,R) be the whole-field Gaussian regression law at these six +observations. Its typed determinant weight is the unchanged parent weight + + W_r=|det H_(M_r) det H_(S_r)| + 1{H_(M_r)<0, index(H_(S_r))=1}, + +where index counts negative eigenvalues. This file does not replace W_r by +an unweighted pin probability or by a good-event normalizer. + +**Lemma F (ordinary-fold isolation).** There is an explicit coupling F_r +of Q_r, together with its six-contact-jet limit F_0, such that: + +1. F_r converges almost surely to F_0 in C4(T_L²) as r decreases to zero. + The limit obeys + + (F_0,F_0,x,F_0,xx,F_0,xxx,F_0,z,F_0,xz)(0) + =(b,0,0,12k,0,0). (F1) + +2. Put A=F_0,zz(0). Almost surely on {A<0}, the only critical points of + F_r in one fixed neighborhood of the origin, for all sufficiently small + r, are M_r and S_r. Every other critical point continues from a finite + collection of nondegenerate critical points of F_0. Their limiting values + are pairwise distinct and all different from b. + +3. For each fixed y in (0,1], put tau(r)=k r³/y. Almost surely on {A<0}, + + K_(tau(r))(F_r)<=1 eventually as r->0. (F2) + + On the entire coupling space, + + (W_r(F_r)/r²) 1{K_(tau(r))(F_r)>=2}->0 + almost surely. (F3) + +The neighborhood and the small-radius threshold may depend on the complete +coupled sample, b,k,R,y. No uniform samplewise threshold, rate, growing-volume +limit, or higher-dimensional assertion is made. In (F2) even the identity of +the local pins as actual elder partners is unnecessary: they are the only +possible endpoints of a short finite bar. Positive mean intensity and actual +elder selection remain the separate retained inputs used by PROOF.md. + +The same pathwise argument works for any deterministic tau(r)->0. The displayed +choice is the one required when integrating ordinary lifetimes ell=tau y and +the exact pair mark k=ell/r³. + +## 2. Exact retained interfaces + +The source identities are those fixed by the companion SOURCES.json. The +parent [P] is read together with [CAP,E1,E2,REC], as required by [REC, §1]. +In particular its endpoint congruence is the corrected diag(r^(-1/2),1), +and E2 replaces the parent's original §9. The use in this lemma is narrower +than an acceptance or re-proof of the complete source chain. + +- [P, §2] gives a smooth Fourier realization on the compact torus, all finite + moments of global derivative suprema, and linear independence of distinct + derivative evaluations at distinct sites. Its proof uses every positive + Fourier coefficient, not a finite spectral sample. +- [P, §3] gives the exact six-row desingularization U_r, its target v_r, and + positive contact covariance. Appending f_zz(0) gives a positive covariance + because it is a distinct jet entry. +- [R, §2, R2–R4] gives the same whole-field regression coupling and its smooth + covariance convergence. The pathwise convergence needed here is proved + directly below from that regression formula and the averaged functionals; + it is not inferred from Lp convergence alone. +- [P, §8] supplies the finite-dimensional rank plus overdetermined mesh method. + Section 4 below checks its covariance hypotheses at the new contact law, + including both kinds of critical-value separation. +- [P, §5] with [E1] supplies the endpoint determinant scale and conditional + moments. The endpoint type boundary is also addressed directly in §7. +- [P, §8; E2, §9.4; P, §14] specify the ordinary global elder observable: + every finite bar has one maximum birth and one distinct merging-saddle + death. A local ascending branch is not substituted for that global mark. + +Neither the C50/C51 replacement-bar theorem nor a double-soft cubic cluster +limit is used as an analytic premise. Those concern a different population. + +## 3. Global smooth coupling at an ordinary six-pin contact + +For a=-r/2 and c=r/2, [P, §3] defines U_r by the four axial rows + + (f(a,0)+f(c,0))/2, + (f(c,0)-f(a,0))/r, + (f_x(c,0)-f_x(a,0))/r, + (6/r²)[f_x(a,0)+f_x(c,0) + -2(f(c,0)-f(a,0))/r], + +followed by the two transverse rows + + (f_z(a,0)+f_z(c,0))/2, + (f_z(c,0)-f_z(a,0))/r. + +Its exact target and limit are + + v_r=(b-k r³/2,-k r²,0,12k,0,0), + U_0=(f,f_x,f_xx,f_xxx,f_z,f_xz)(0), + v_0=(b,0,0,12k,0,0). (F4) + +For a smooth unconditioned field F, write + + Sigma_r=Cov(U_r(F)), C_r(q)=Cov(F(q),U_r(F)), + F_r(q)=F(q)+C_r(q) Sigma_r^(-1)(v_r-U_r(F)). (F5) + +Use the same underlying F for every r, and the analogous expression at r=0. +Gaussian regression proves law(F_r)=Q_r. Applying U_r to (F5) shows that the +pins hold exactly, because U_r(C_r)=Sigma_r. There is no artificial independent +field introduced for the remote part of the torus. + +Here is a pathwise justification for the limit. For every deterministic +smooth F, each row of U_r(F) tends to its row of U_0(F). For the fourth row, +Taylor expansion on the centered interval gives + + F_x(a,0)+F_x(c,0)=2F_x(0)+(r²/4)F_xxx(0)+o(r²), + 2(F(c,0)-F(a,0))/r=2F_x(0)+(r²/12)F_xxx(0)+o(r²), + +and their difference times 6/r² tends to F_xxx(0). Equivalently this row +is an averaged third derivative with a bounded integral kernel, as in [P, §3]. +The apparent negative powers of r therefore cause no pathwise discontinuity. + +The positive and rapidly decreasing Fourier spectrum in [P, §2] permits +termwise differentiation of the covariance to every fixed finite order. +Consequently C_r->C_0 in global C4, Sigma_r->Sigma_0, and Sigma_r^(-1) +converges because Sigma_0 is positive definite. Together with (F4), passing +to the limit term by term in (F5) proves + + ||F_r-F_0||_(C4(T_L²))->0 (F6) + +on the probability-one event that F is smooth. This is convergence of the +whole continuous family as r->0, not just convergence along one subsequence. +It is asserted for each fixed b,k,R; a common probability-one set over all +uncountably many target laws is not required. + +The limiting field has the regression law at U_0=v_0 and satisfies (F1). +The conditional variance of A=F_0,zz(0) is strictly positive: adjoining f_zz +to the six entries of U_0 is an independent list by [P, §2]. Thus A has a +nondegenerate scalar Gaussian density, in particular P(A=0)=0. Correlations +between A and the remaining field are retained. + +## 4. Conditional genericity of all remote critical points and values + +All assertions in this section concern the contact-conditioned law of F_0 +at a fixed b,k,R. The forced degenerate critical point at 0 is excluded from +the remote domains. + +First, at x!=0 and |v|=1 consider + + Z_M(x,v)=(grad F_0(x),H F_0(x)v) in R4. (F7) + +Its conditional covariance is positive definite. Otherwise a nonzero linear +combination of these four functionals would lie in the Gaussian L2 span of +U_0. With the positive Fourier spectrum, subtracting this contact combination +gives a distribution of derivative evaluations whose every Fourier coefficient +is zero. The distribution is therefore zero. Its supports x and 0 are +disjoint, so its part at x must vanish. The first-derivative and second- +derivative orders cannot cancel. The symbol for the latter is +`(beta dot xi)(v dot xi)`; since v!=0, it vanishes identically only if beta=0. +The first-derivative coefficients then vanish also, a contradiction. + +For two distinct points x,z both different from 0 consider + + Z_V(x,z)=(grad F_0(x),grad F_0(z), + F_0(x)-F_0(z)) in R5. (F8) + +The same covariance argument applies. At support x a putative zero +distribution has an order-zero coefficient lambda and its two independent +first-derivative coefficients. They all vanish; this gives lambda=0 and +then the two first-derivative coefficients at z vanish. None can be canceled +by the observations supported at 0. Thus the residual covariance is positive. + +To exclude a critical value equal to the contact birth b use + + Z_b(x)=(grad F_0(x),F_0(x)-b) in R3, x!=0. (F9) + +The constant b changes the mean, not the covariance. The three remote jet +entries are linearly independent modulo U_0 by the same disjoint-support +argument, so the covariance is again positive definite. + +For completeness, the zero-exclusion step is as follows. Exhaust these +parameter domains by countably many compact sets with positive distance +from 0 and, for (F8), from x=z. Cover the unit circle in (F7) by finitely +many coordinate charts. On each compact chart, covariance continuity and +positivity give a uniform upper bound for the Gaussian density of each +Z-map. Its conditional mean has no effect on that density upper bound. + +If a random C1 map from a compact q-dimensional chart to Rp has a zero and +its C1 norm is at most M, one of O(epsilon^(-q)) points in an epsilon-mesh +has image of norm at most C M epsilon. The probability at each mesh point +is at most C'(M epsilon)^p by the bounded density. The union bound therefore +gives C'' M^p epsilon^(p-q), which tends to zero whenever p>q. Fix M first, +then take the countable union over integer M. Smoothness makes the random +C1 norm finite. No independence among mesh values is assumed. + +In (F7), (F8) and (F9), respectively, (q,p) is (3,4), (4,5), and (2,3). +The compact exhaustion therefore proves, almost surely: + +- every off-origin critical point of F_0 is nondegenerate; +- two distinct off-origin critical points have different values; +- no off-origin critical point has value b. (F10) + +These are statements about the actual smooth contact-conditioned field. +They do not follow merely from nonsingularity at a finite set of sampled +locations. They remain valid on intersection with {A<0}, without imposing +an independent law on the remote field. + +## 5. A complete local ridge and exactly two pinned critical points + +Fix one sample satisfying (F6), (F10), and A<0. Set a0=-A>0. By continuity, +choose a coordinate rectangle around 0 on which + + F_0,zz <= -a0/2. + +First choose a sufficiently small transverse half-width eta>0 inside that +rectangle. Since F_0,z(0)=F_0,xz(0)=0, shrinking an axial half-width delta>0 +ensures |F_0,z(x,0)|<=a0 eta/8 for |x|<=delta. Integration in z then gives +strict opposite signs on z=-eta and z=eta, with a margin at least +3 a0 eta/8. By global C4 convergence, for all small enough r, + + F_r,zz <= -a0/4, + F_r,z(x,-eta)>0>F_r,z(x,eta), |x|<=delta. (F11) + +It follows by the intermediate-value theorem and strict decrease in z that, +for every |x|<=delta, exactly one z=psi_r(x) in (-eta,eta) solves F_r,z=0. +The implicit-function theorem gives psi_r in C3. The uniform derivative +floor in (F11), uniform convergence of the derivatives of F_r through order +four, and implicit differentiation give + + psi_r->psi_0 in C3([-delta,delta]). (F12) + +For example psi_r'=-F_r,xz/F_r,zz on the ridge. The formulas for the next +two derivatives have bounded denominators consisting of powers of F_r,zz +and numerators formed from derivatives through order four. Uniform convergence +of the roots follows first from strict monotonicity and uniform convergence +of F_r,z, and these formulas then prove (F12). Thus the assertion holds on +the entire fixed interval, not merely near a single point. + +Define the reduced scalar function and its tangent by + + g_r(x)=F_r(x,psi_r(x)), v_ridge=(1,psi_r'(x)). + +Here v_ridge is not the pin-target vector v_r from (F4). Along the ridge, + + g_r'=F_r,x, + D²F_r[v_ridge,e_z]=d(F_r,z(x,psi_r(x)))/dx=0. + +The chain rule through third order yields the exact identity + + g_r'''=D³F_r[v_ridge,v_ridge,v_ridge] + +3D²F_r[v_ridge,(0,psi_r'')] + +DF_r[(0,psi_r''')] + =D³F_r[v_ridge,v_ridge,v_ridge]. (F13) + +The last two terms vanish by the displayed ridge identities. At the limit +origin, psi_0(0)=0 and psi_0'(0)=-F_0,xz(0)/A=0, so + + g_0'(0)=g_0''(0)=0, g_0'''(0)=12k>0. (F14) + +Shrink delta again if necessary so that g_0'''>=9k on the whole interval. +Equations (F6),(F12),(F13) then give g_r'''>=6k there for all small r. The +function g_r' is therefore strictly convex. Both exact gradient pins lie +in the rectangle, and transverse uniqueness implies + + psi_r(-r/2)=psi_r(r/2)=0, + g_r'(-r/2)=g_r'(r/2)=0. + +A strictly convex function has at most two distinct zeros: if it had three, +the middle zero would lie strictly below the chord between the outer two, +which is zero, a contradiction. Hence these are the only zeros of g_r'. +Every critical point of F_r in the rectangle lies on the ridge, so the two +pins are the only local critical points. This controls all intermediate +spatial scales within a fixed neighborhood at once; no gap between a ball +of radius O(r) and a fixed-radius region is omitted. + +Their types can also be checked without a normal-form approximation. +Strictly increasing g_r'' and the equality of g_r' at its two zeros imply + + g_r''(-r/2)<00 imply g_0'(x)>0 for every nonzero x in the same +interval: integrate the sign of g_0'' from its zero at 0 on either side. +Consequently 0 is the only critical point of F_0 in the fixed rectangle. + +## 6. Complete global root exhaustion and critical-value separation + +Choose a smaller closed coordinate box V strictly inside the rectangle +from §5, containing 0 in its interior. The limit has no other critical point +in the larger rectangle, so in particular its gradient is nonzero on the +boundary of V. All critical points of F_0 outside the interior of V are +nondegenerate by (F10). There are finitely many: an infinite sequence in this +compact set would have a critical accumulation point there, contradicting +isolation of a nondegenerate critical point. Name them p_1,...,p_m. + +Choose disjoint small closed coordinate balls B_j around the p_j, all outside +V, such that the Hessian in each is uniformly close to the invertible matrix +H_j=H F_0(p_j). By C2 convergence the same is true for F_r. The map + + q -> q-H_j^(-1) grad F_r(q) + +is a contraction on a sufficiently small fixed B_j, mapping it into itself +for all small enough r: its derivative norm is uniformly below one, and +its value at p_j approaches p_j. The contraction principle supplies exactly +one critical point p_j(r) in B_j, with p_j(r)->p_j. The same Hessian estimate +also makes this root nondegenerate. + +On the compact complement of the interiors of V and the B_j, the limiting +gradient has a positive minimum. Uniform C1 convergence excludes any F_r +critical point there for small r. Section 5 already exhausts the roots in V +by the two exact pins. Hence the complete critical set of F_r, eventually, +is exactly + + {M_r,S_r,p_1(r),...,p_m(r)}. (F15) + +This includes neighborhoods of every chosen boundary; there is no unexamined +boundary layer between the local and remote parts of the domain. + +Let v_j=F_0(p_j). By (F10), the finite set of numbers + + {|v_j-b|:1<=j<=m} + union {|v_j-v_i|:1<=iv_j. Both pinned values approach b, +and their positive difference is exactly k r³. For all sufficiently small r, +every absolute difference of two critical values involving at least one +remote critical point is at least Delta/2. The only remaining difference +is that of the two local pins. In particular F_r is then Morse and has +distinct critical values, including at the pins. + +If tau(r)->0, then eventually tau(r)0}, global C2 convergence gives F_r,zz(M_r)->A>0. A negative definite +Hessian must have negative value on the transverse coordinate vector. Hence +the maximum-type indicator in W_r is zero for every sufficiently small r; +again the expression in (F3) is identically zero eventually. The remaining +event A=0 is null, as proved in §3. No estimate on a thin neighborhood of +A=0 is silently inferred from this null-set fact. + +This proves (F3) almost surely. It can also be integrated at fixed b,k,R,y. +Indeed [P, (4.1),(5.1),(5.3)] gives a uniformly bounded moment of W_r/r² of +some order greater than one on a compact parameter neighborhood of these +fixed targets. The bounded event factor preserves uniform integrability. +Almost-sure convergence plus uniform integrability therefore gives + + E[(W_r(F_r)/r²) 1{K_(k r³/y)(F_r)>=2}]->0. (F16) + +Multiplication by the bounded actual elder indicator does not change this +conclusion. Formula (F16) is an UNNORMALIZED weighted expectation, not a +quotient requiring a target-uniform positive lower bound for Z_r. The +removal of all b,k,y cutoffs uses the independent unnormalized intensity +majorant and off-diagonal estimate in PROOF.md. This lemma itself asserts +no rate of convergence in (F16), no global factorial moment, and no Poisson +or spatial-independence statement. + +## 8. What the proof does and does not identify + +The new analytic input is isolation of an ordinary fold together with the +absence of a second vanishing critical-value gap anywhere else in the same +conditioned field. Positivity of the transverse Gaussian density, complete +ridge root exhaustion, and remote critical-value separation are all used. +Merely separating remote critical-point positions would not suffice. + +The bound counts actual ordinary short finite bars in one field. It is not +a uniqueness theorem for nearby auxiliary witnesses, rejected candidate +saddles, ascent trajectories or critical points in a shrinking height window. +It does not supersede a historical witness-localization or RN/24-jet node. +The existing parent selection theorem supplies any needed identification of +the selected mean persistence intensity; no new global elder theorem is +asserted by replacing that input with (F2). + +The limit is fixed L, fixed b,k,R first, with the exact lifetime substitution +tau=k r³/y at fixed y>0. All exceptional-set assertions are for each such +law; integration over targets is handled by measurability and domination in +the consumer. There is no exchange with L->infinity, no numerical radius +threshold, and no extension of the present planar lemma to other dimensions. diff --git a/frontiers/ordinary_short_bar_occurrence_20261001/PROOF.md b/frontiers/ordinary_short_bar_occurrence_20261001/PROOF.md new file mode 100644 index 000000000..69ff20a6c --- /dev/null +++ b/frontiers/ordinary_short_bar_occurrence_20261001/PROOF.md @@ -0,0 +1,175 @@ +# Ordinary short bars: occurrence and field-first sampling + +Object C52-ORDINARY-SHORT-BAR-OCCURRENCE-20261001-v1. Additive conditional mathematical candidate, OpenAI/Codex. Scientific-status effect NONE; C8 remains OPEN. The theorem consumes the exact analytic interfaces listed below; this packet does not reaccept those interfaces, formalize Gaussian persistence, or certify the whole program. + +## 1. Frozen target and source contract + +Fix L>0 and d=2. Let X be the centered, variance-one smooth Gaussian field on the fixed flat torus T_L^2 with covariance +$$ +K_L(z)=\frac{\sum_{n\in\mathbb Z^2}e^{-|z+Ln|^2/2}} + {\sum_{n\in\mathbb Z^2}e^{-|Ln|^2/2}}. +$$ +Use ordinary SUPERLEVEL H0 persistence. A finite bar is born at a maximum M and dies at its actual global elder-selected merging saddle S; M is the dying component's maximum, not the older surviving maximum. Exclude the essential global-maximum class. Let K_tau be the total number of such bars of lifetime in (0,tau] in ONE field on the WHOLE torus. Its expectation is not divided by volume. + +Sources P, CAP, E1, E2, REC, R and T are pinned by path, bytes, SHA256 and Git blob in SOURCES.json, all at Math- commit 7fe06b01489af8181e53f26d520810829f146094. P is the lifetime parent; CAP its deterministic predecessor; E1 corrects the congruence; E2 replaces P§9; REC supplies the mandatory reading rule/W1/embedding radius; R§2 supplies the regression construction; T§Proposition3 supplies the ordinary-bar marked intensity law. In particular: + +- Interpret P through CAP/E1/E2/REC, with an embedded r_00), e_tau=m_tau-p_tau. Then +$$ +0\le e_\tau=E[(K_\tau-1)_+]\le B_\tau=o(\tau^{2/3}),\qquad +p_\tau=L^2\frac32c_{2,L}\tau^{2/3}+o(\tau^{2/3}), \tag{O2} +$$ +and +$$ +\operatorname{TV}(\mathcal L(K_\tau\mid K_\tau>0),\delta_1) +=P(K_\tau\ge2)/p_\tau\longrightarrow0. \tag{O3} +$$ +If a field is conditioned on K_tau>0 and one of its short bars is then chosen uniformly, the law of any common measurable mark differs in TV from the intensity-normalized short-bar mark law by at most e_tau/m_tau=o(1). This includes the explicit mark limit in §6. + +These are small-lifetime, fixed-volume occurrence/mark statements. No speed for the little-o, factorial-moment asymptotic, Poisson process, independent-region construction, higher-dimensional extension or infinite-volume limit is asserted. K_tau counts actual persistence bars, not auxiliary window witnesses or the rejected-candidate replacement population of C50/C51. Those packets are not premises of this proof. + +## 2. Whole-field isolation under one ordinary fold + +Write q=(b,k,u), with b real, k>0 and u in S^1. Let r>0, M=-ru/2, S=ru/2, and condition on X(M)=b, X(S)=b-kr³ and both gradients zero. This is the exact six-observation continuous Gaussian regression law Q_{r,q}. Let +$$ +W_r=|\det H_M\det H_S|1_{\{H_M<0,\operatorname{index}(H_S)=1\}},\quad +Z_r=E_Q W_r . +$$ +There is no second determinant or adjacency factor in W_r. The exact scaled height gap is k=ell/r³, rather than a Taylor approximation. + +The coauthored [fold isolation lemma](FOLD_ISOLATION.md) proves on the original full-field regression coupling, for each fixed q and y in (0,1] and r=(tau y/k)^(1/3), +$$ +\frac{W_r}{r^2}1_{\{K_\tau(F_r)\ge2\}}\longrightarrow0 +\quad\hbox{almost surely}. \tag{I} +$$ +Its ingredients are stated here to make the new dependency visible: +1. The actual coupled F_r converge globally in C4 almost surely to the six-jet contact field F_0. This is derived from averaged-derivative observations on a smooth sample, not from an invalid upgrade of Lp convergence. +2. Residual finite-jet rank plus the overdetermined mesh argument show that off the contact, F_0 has Morse roots with pairwise distinct critical values, none equal to the contact value b. +3. If A=F_{0,zz}(0)<0, a fixed rectangle has a unique transverse ridge. The reduced derivative has strictly positive second derivative because the reduced third derivative at contact is12k>0. The two exact pinned roots exhaust ALL local critical points. Outside the rectangle, root stability and the positive minimum of the finitely many remaining critical-value gaps exclude every additional lifetime-small endpoint pair. +4. If A>0, the maximum-type weight vanishes for sufficiently small r. A=0 is null under the conditional nondegenerate scalar Gaussian law. + +Thus the typed contact sector has at most one possible short bar eventually. This does not identify whether the pinned pair is itself the elder pair. The actual elder indicator is retained below. Random exclusion radii and critical-value gaps need not be uniform over q or sample paths. The argument uses per-fixed-law probability-one statements and then integration; it does not assert a common probability-one set for every uncountable parameter choice. + +## 3. The bounded mark and exact weighted counting identity + +Let H_tau(f)=1{K_tau(f)>=2}. On the Morse distinct-critical-value locus this is a bounded Borel function of the whole field: critical roots/values and their elder pairings are locally stable, and the finite counting function at a threshold is Borel; alternatively apply the countable path representation of E2 and thresholded point-count measures. Define the bar count and mark to be zero on the null complement for the unconditional field. For every r>0 the conditional kernels in E2 specify the same Borel mark; the isolation proof applies on their eventual generic locus. + +Let J_eld(M,S;f) be the actual global elder indicator. Pathwise counting once per finite bar yields +$$ +B_\tau=E\sum_{\substack{(M,S)\ \mathrm{actual}\ 0<\ell\le\tau}} +H_\tau(f). \tag{C} +$$ +There is no extra factor K_tau inside the pair integral: summing the bounded mark already supplies it. Monotone exhaustion away from the diagonal and E2 extend this identity to all separations. + +Use midpoint stationarity and oriented displacement S-M=ru. The endpoints have fixed, different types (maximum, saddle); they are ordered once. Reversing u exchanges spatial positions but is not an additional copy of the same ordered pair. For r1 as r decreases. Together with (I), uniform integrability gives +$$ +E_Q[(W_r/r²)H_\tau]\longrightarrow0 . +$$ +Since 0<=J_eld<=1, the expectation in (C1) also tends to zero; continuity of pi_r(v_r) at fixed q proves A_r^{H_tau}(q)->0. No continuity of the global elder indicator along a degenerate contact field is needed. + +At all birth heights and all positive k, P(13.4) gives +$$ +0\le A_r^{H_\tau}(q)\le +H(b,k)=C(1+|b|+k)^4 e^{-c(b²+k²)},\quad0=r_0, H_tau and J_eld are bounded by1, so P(14.1) gives +$$ +0\le B_\tau^{\rm far}/L²\le C\tau=o(\tau^{2/3}). +$$ +No moving-cutoff RN assertion has been inferred from a fixed-cutoff bound. Near and far exhaust all ordered distinct endpoints (a spatial boundary has zero measure). This proves(O1). + +Limit order: fix L and r_0, then fix q,y while tau decreases, use the coupled pathwise limit and conditional uniform integrability, then dominated convergence in(y,b,k,u). There is no L-limit, auxiliary-witness separation limit or interchange of a derivative with a cumulative asymptotic. Constants depend on the fixed field and source bounds; none is a numerical cutoff. + +## 5. From weighted counts to field occurrence + +Every field has finitely many critical points almost surely and hence finitely many finite bars. Integrability follows from the imported pair bounds. For every nonnegative integer K, +$$ +K=1_{\{K>0\}}+(K-1)_+,\qquad +(K-1)_+\le K1_{\{K\ge2\}},\qquad +2P(K\ge2)\le E[K1_{\{K\ge2\}}]. +$$ +Apply these to K_tau and(O1). The positive leading mean supplied by P Theorem C gives(O2) and p_tau>0 for small tau. Dividing the last inequality by p_tau gives(O3). The excess and multi-count first moment are of the same little-o order, but neither statement controls K(K-1). Rare counts of growing size can invalidate such an inference; exact finite counterexamples are included with the controls. + +## 6. Removing field-size bias from marks + +Allow any common tau-dependent Borel bar mark in a standard Borel space. On a field with K_tau>0 let U_tau be its empirical probability measure assigning mass1/K_tau to each eligible bar. Define +$$ +I_\tau=E[K_\tau U_\tau]/m_\tau,\qquad +F_\tau=E[1_{\{K_\tau>0\}}U_\tau]/p_\tau . +$$ +I_tau is the intensity-normalized law; F_tau is obtained by first conditioning the FIELD on occurrence and then choosing a bar uniformly. When e_tau>0 put +D_tau=E[(K_tau-1)_+U_tau]/e_tau. The exact identity +$$ +I_\tau=(p_\tau/m_\tau)F_\tau+(e_\tau/m_\tau)D_\tau +$$ +proves, for TV=sup over measurable sets, +$$ +\operatorname{TV}(F_\tau,I_\tau)\le e_\tau/m_\tau=o(1). \tag{O4} +$$ +If e_tau=0 the laws agree. This bound is uniform over the choice of mark, but has no numerical convergence rate. + +For T's cubic mark, retain y=ell/tau and q=(b,k,u) for pairs at r0. +$$ +Here tau_u²=Var(partial_u³X|grad X=0), V_u=H_Xu, and +D_u=E[A_u²1_{A_u<0}|V_u=0]. The numerical factor24 is not L. No reference-space coefficient is substituted for the finite-torus coefficient. + +## 7. Boundaries, review and falsifiers + +The new obligation is ordinary-fold isolation and its use inside the bounded whole-field marked pair integral. The proof retains actual global elder identification and the positive leading mean as source interfaces. If those interfaces or the all-mark bound fail, the corresponding theorem here fails. The proof neither replaces their reviews nor grants them new acceptance. + +The conclusion does not close the historical auxiliary shrinking-witness uniqueness problem: its random variable and normalization are different. Nor does it promote C8, RN/24-jet numerical gates, a covariance-class universality theorem, higher homology, higher dimensions, factorial moments or an increasing-volume cluster process. Mathematical completeness of this conditional theorem is separate from the project's other open nodes. + +Review must inspect: conditional remote root AND critical-value genericity, complete local ridge rather than an O(r) window only, actual all-field coupling, A=0 null boundary, weight uniform integrability, exact tau/lifetime factors, all-target domination, field-first size-bias identity and the absence of an accidental factorial claim. + +Exact rational programs check the finite identities and meaningful counterexamples. They do not prove continuum probability estimates, topological identification, dominated convergence, or analytic source acceptance. AI coauthors and fresh AI technical reviewers are named in the delivery; same-provider review earns organizational-independence credit0. Dylan Roy delegated AI work; personal reading PENDING. diff --git a/frontiers/ordinary_short_bar_occurrence_20261001/README.md b/frontiers/ordinary_short_bar_occurrence_20261001/README.md new file mode 100644 index 000000000..8826f25dc --- /dev/null +++ b/frontiers/ordinary_short_bar_occurrence_20261001/README.md @@ -0,0 +1,21 @@ +# When one very short bar occurs + +For the fixed planar periodized Gaussian field, the candidate theorem shows that a field containing a sufficiently short ordinary finite superlevel H0 bar asymptotically contains only one such bar. Its occurrence probability has the same leading coefficient as its expected count. + +[Theorem and proof](PROOF.md) · [New fold isolation lemma](FOLD_ISOLATION.md) · [Exact sources](SOURCES.json) + +The new step controls the expected count on fields containing multiple short bars. It also removes the bias introduced by sampling bars across fields: conditioning a field on occurrence and choosing its bar uniformly has the same limiting mark law as the intensity calculation. + +This is a conditional mathematical candidate. It retains the imported global elder-pairing, Kac–Rice and Gaussian bounds. It supplies no factorial-moment or Poisson theorem, quantitative convergence rate, increasing-volume limit, higher-dimensional extension or whole-program closure. Scientific-status effect NONE; C8 remains OPEN. + +Run the exact finite controls from the repository root: + +```sh +python3 -B -S frontiers/ordinary_short_bar_occurrence_20261001/test_check.py -v +python3 -B -O -S frontiers/ordinary_short_bar_occurrence_20261001/test_check.py -v +python3 -B -S frontiers/ordinary_short_bar_occurrence_20261001/test_check.py --mutants +``` + +These standard-library controls verify source identities, rational counting and sampling identities, cubic-scale Jacobians, and counterexamples to invalid inferences. Implementation mutations must be rejected in both modes. They do not prove the continuum analysis. Fresh mathematical review and engineering review are recorded separately on the source-bound pull request. + +Actual authoring: OpenAI/Codex root and named coauthors in the delivery. Dylan Roy — delegated AI work; personal reading PENDING. Same-provider technical review carries zero organizational-independence credit. diff --git a/frontiers/ordinary_short_bar_occurrence_20261001/SOURCES.json b/frontiers/ordinary_short_bar_occurrence_20261001/SOURCES.json new file mode 100644 index 000000000..6d9b3fb93 --- /dev/null +++ b/frontiers/ordinary_short_bar_occurrence_20261001/SOURCES.json @@ -0,0 +1,71 @@ +{ + "version": 1, + "source_commit": "7fe06b01489af8181e53f26d520810829f146094", + "scientific_effect": "NONE", + "status": "C52 conditional consumer; mandatory P/CAP/E1/E2/REC reading rule retained; no source reacceptance", + "sources": [ + { + "key": "P", + "path": "imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md", + "commit": "7fe06b01489af8181e53f26d520810829f146094", + "blob": "dfed3b8d318a3ab1950957f393307733a4bef3f2", + "bytes": 40261, + "sha256": "9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7", + "local_path": "imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md" + }, + { + "key": "CAP", + "path": "imports/lifetime_parent_20260925/MARKED_CYLINDER_CAP_PROOF.md", + "commit": "7fe06b01489af8181e53f26d520810829f146094", + "blob": "0633aca3c2a2882b0de4399da0a75d64c2e6b2e1", + "bytes": 15160, + "sha256": "0bf922b9203c29088b12388807aa0e2ecd020485eb0f6e919679841b5b2636fc", + "local_path": "imports/lifetime_parent_20260925/MARKED_CYLINDER_CAP_PROOF.md" + }, + { + "key": "E1", + "path": "imports/lifetime_parent_20260925/ERRATUM_CONGRUENCE.md", + "commit": "7fe06b01489af8181e53f26d520810829f146094", + "blob": "213594d6ca6a86fb938110f4d166d9ce275a02d0", + "bytes": 1782, + "sha256": "bad7ef609c4ad8c41ad6af562c1b6807921e19a9d556ed793ad1a0db6e202028", + "local_path": "imports/lifetime_parent_20260925/ERRATUM_CONGRUENCE.md" + }, + { + "key": "E2", + "path": "reviews/d1_section9_borel_repair_20260925/REPAIR.md", + "commit": "7fe06b01489af8181e53f26d520810829f146094", + "blob": "fe9b9ce4999908bb3814b500ee2d0ceb0c6f704a", + "bytes": 9062, + "sha256": "845abf9f9c99d672c2a10a887b5a2e7206a3d2de3d876f35f75ff6e2dc13e62f", + "local_path": "reviews/d1_section9_borel_repair_20260925/REPAIR.md" + }, + { + "key": "REC", + "path": "reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md", + "commit": "7fe06b01489af8181e53f26d520810829f146094", + "blob": "75da2597971510f843f8d90c743950cb8c177342", + "bytes": 23312, + "sha256": "451b9d7ffee072a73fc904cab891b6693e3f233808b89df10cce1b57036b65da", + "local_path": "reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md" + }, + { + "key": "R", + "path": "frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md", + "local_path": "frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md", + "commit": "7fe06b01489af8181e53f26d520810829f146094", + "bytes": 17734, + "sha256": "380b7d0abdb0fe2de5a6564565af9560d3f1b1ce22fd5538927db0c52f4f3a4a", + "blob": "247b3ecf80bfbe896948d5d489b2d5842a81c481" + }, + { + "key": "T", + "path": "frontiers/short_bar_endpoint_law_20261001/PROOF.md", + "local_path": "frontiers/short_bar_endpoint_law_20261001/PROOF.md", + "commit": "7fe06b01489af8181e53f26d520810829f146094", + "bytes": 13815, + "sha256": "4fc567b5bed7967bba7b7fc609da8219b6cd2c605e9291b7b82c8a538ced1a29", + "blob": "0d47dbc1d92863d8c51b918aa47d1fa8b605cfdc" + } + ] +} diff --git a/frontiers/ordinary_short_bar_occurrence_20261001/check.py b/frontiers/ordinary_short_bar_occurrence_20261001/check.py new file mode 100644 index 000000000..ce4e33bd8 --- /dev/null +++ b/frontiers/ordinary_short_bar_occurrence_20261001/check.py @@ -0,0 +1,181 @@ +"""Exact finite controls, not proofs of Gaussian or persistence hypotheses. + +All probabilities and scalar inputs must be integers or Fractions. Marks are +arbitrary hashable labels in a finite model. Total variation means half the L1 +distance between probability measures, equivalently the supremum over events. +""" + +from collections import defaultdict +from fractions import Fraction + + +def _rational(value): + if isinstance(value, bool) or not isinstance(value, (int, Fraction)): + raise ValueError("exact integer or Fraction required") + return Fraction(value) + + +def _integer(value, *, positive=False): + if isinstance(value, bool) or not isinstance(value, int): + raise ValueError("integer required") + if positive and value <= 0: + raise ValueError("positive integer required") + return value + + +def _probabilities(law): + weights = {label: _rational(p) for label, p in law.items()} + if any(p < 0 for p in weights.values()) or sum(weights.values()) != 1: + raise ValueError("probabilities must be nonnegative and sum to one") + return weights + + +def count_statistics(law): + """Statistics of a finite distribution of a nonnegative integer count.""" + for k in law: + if _integer(k) < 0: + raise ValueError("count must be nonnegative") + weights = _probabilities(law) + mean = sum((p * k for k, p in weights.items()), Fraction(0)) + occurrence = sum((p for k, p in weights.items() if k > 0), Fraction(0)) + excess = sum((p * max(k - 1, 0) for k, p in weights.items()), Fraction(0)) + multi_mass = sum((p * k for k, p in weights.items() if k >= 2), Fraction(0)) + factorial = sum((p * k * (k - 1) for k, p in weights.items()), Fraction(0)) + multi_probability = sum((p for k, p in weights.items() if k >= 2), Fraction(0)) + return {"mean": mean, "occurrence": occurrence, "excess": excess, + "multi_mass": multi_mass, "second_factorial": factorial, + "conditional_multi": multi_probability / occurrence if occurrence else None} + + +def total_variation(left, right): + """Exact TV of finite probability measures, with missing atoms given mass 0.""" + left, right = _probabilities(left), _probabilities(right) + return sum((abs(left.get(label, 0) - right.get(label, 0)) + for label in set(left) | set(right)), Fraction(0)) / 2 + + +def mark_statistics(fields): + """Compare intensity sampling with field-first uniform-bar sampling. + + Each input is (field probability, sequence of that field's bar marks). + Repeated marks retain their bar multiplicity. A zero occurrence probability + produces None for normalized laws rather than inventing a conditional law. + """ + rows = [] + counts = defaultdict(Fraction) + for probability, marks in fields: + p = _rational(probability) + if not isinstance(marks, (tuple, list)): + raise ValueError("marks must be a finite tuple or list") + marks = tuple(marks) + try: + for label in marks: + hash(label) + except TypeError as exc: + raise ValueError("marks must be hashable") from exc + if p < 0: + raise ValueError("negative field probability") + rows.append((p, marks)) + counts[len(marks)] += p + summary = count_statistics(counts) + m, p, e = summary["mean"], summary["occurrence"], summary["excess"] + if not p: + return dict(summary, field_first=None, intensity=None, excess_law=None, + tv=None, tv_bound=None) + intensity, field, defect = (defaultdict(Fraction) for _ in range(3)) + for probability, marks in rows: + k = len(marks) + if not k or not probability: + continue + for label in marks: + intensity[label] += probability + field[label] += probability / k + defect[label] += probability * (k - 1) / k + intensity = {label: value / m for label, value in intensity.items() if value} + field = {label: value / p for label, value in field.items() if value} + defect = {label: value / e for label, value in defect.items() if value} if e else None + return dict(summary, field_first=field, intensity=intensity, excess_law=defect, + tv=total_variation(field, intensity), tv_bound=e / m) + + +def radial_pushforward(amplitude, radial_power, gap_power=3): + """A r^a dr under ell=k r^q: (prefactor, k-power, ell-power). + + Fractional powers remain symbolic; no floating evaluation is substituted. + """ + amplitude = _rational(amplitude) + a, q = _integer(radial_power), _integer(gap_power, positive=True) + order = Fraction(a + 1, q) + return amplitude / q, -order, order - 1 + + +def radial_cumulative(amplitude, radial_power, gap_power=3): + """Integral from zero of A r^a dr, requiring a > -1.""" + amplitude = _rational(amplitude) + a, q = _integer(radial_power), _integer(gap_power, positive=True) + if a <= -1: + raise ValueError("radial measure is not integrable at zero") + order = Fraction(a + 1, q) + return amplitude / (a + 1), -order, order + + +def radial_density_at_r(amplitude, radial_power, kappa, r, gap_power=3): + """Evaluate A r^a / (d ell / dr) in exact rational arithmetic.""" + amplitude = _rational(amplitude) + a, q = _integer(radial_power), _integer(gap_power, positive=True) + kappa, r = _rational(kappa), _rational(r) + if kappa <= 0 or r <= 0: + raise ValueError("positive gap coefficient and separation required") + return amplitude * r ** a / (q * kappa * r ** (q - 1)) + + +def fold_jet(a, r, x): + """(g,g',g'',g''') for g=a(x^3/3-r^2 x/4), a,r>0. + + g' is strictly convex since g'''=2a>0. The left endpoint is a longitudinal + maximum and the right endpoint a longitudinal minimum. Adding negative + transverse quadratic directions gives the local max/saddle model only; + this finite calculation does not identify an actual persistence pairing. + """ + a, r, x = _rational(a), _rational(r), _rational(x) + if a <= 0 or r <= 0: + raise ValueError("positive cubic coefficient and separation required") + return (a * (x ** 3 / 3 - r ** 2 * x / 4), + a * (x ** 2 - r ** 2 / 4), 2 * a * x, 2 * a) + + +def curved_ridge_third(k, r, q, x): + """Raw f_xxx versus reduced g''' for a polynomial with a curved ridge. + + f=-kr^3/2+2kx^3-3kr^2*x/2-(z-q(x^2-r^2/4))^2/2. + Differentiate its bivariate coefficients directly, then use the implicit + ridge tangent v=-f_xz/f_zz. This checks the derivative correction omitted by + the false substitution g'''=f_xxx away from the contact point. + """ + k, r, q, x = map(_rational, (k, r, q, x)) + if k <= 0 or r <= 0: + raise ValueError("positive gap coefficient and separation required") + coefficients = {(0, 0): -k * r ** 3 / 2 - q ** 2 * r ** 4 / 32, + (3, 0): 2 * k, (1, 0): -3 * k * r ** 2 / 2, + (0, 2): Fraction(-1, 2), (2, 1): q, + (0, 1): -q * r ** 2 / 4, (4, 0): -q ** 2 / 2, + (2, 0): q ** 2 * r ** 2 / 4} + z = q * (x ** 2 - r ** 2 / 4) + + def derivative(dx, dz): + answer = Fraction(0) + for (i, j), coefficient in coefficients.items(): + if i < dx or j < dz: + continue + factor = 1 + for step in range(dx): + factor *= i - step + for step in range(dz): + factor *= j - step + answer += coefficient * factor * x ** (i - dx) * z ** (j - dz) + return answer + + raw = derivative(3, 0) + v = -derivative(1, 1) / derivative(0, 2) + reduced = raw + 3 * derivative(2, 1) * v + 3 * derivative(1, 2) * v ** 2 + derivative(0, 3) * v ** 3 + return raw, reduced diff --git a/frontiers/ordinary_short_bar_occurrence_20261001/test_check.py b/frontiers/ordinary_short_bar_occurrence_20261001/test_check.py new file mode 100644 index 000000000..c6965e47d --- /dev/null +++ b/frontiers/ordinary_short_bar_occurrence_20261001/test_check.py @@ -0,0 +1,328 @@ +"""Exact finite controls; none substitutes for the packet's analytic proof.""" + +from fractions import Fraction as F +from pathlib import Path +import hashlib +import json +import shutil +import subprocess +import sys +import tempfile +import unittest + +import check +import verify_sources + + +class CountControls(unittest.TestCase): + def test_counts_preserve_bar_multiplicity(self): + # Replacing K by 1{K>0} loses both the mean and the weighted multi mass. + self.assertEqual( + check.count_statistics({0: F(1, 2), 1: F(1, 3), 3: F(1, 6)}), + {"mean": F(5, 6), "occurrence": F(1, 2), + "excess": F(1, 3), "multi_mass": F(1, 2), + "second_factorial": F(1), "conditional_multi": F(1, 3)}, + ) + + def test_first_moment_alone_does_not_select_one_bar(self): + for n in (2, 5, 16, 31): + epsilon = F(1, n * n) + s = check.count_statistics({0: 1 - epsilon / 2, 2: epsilon / 2}) + self.assertEqual(s["mean"], epsilon) + self.assertEqual(s["occurrence"], epsilon / 2) + self.assertEqual(s["multi_mass"], epsilon) + self.assertEqual(s["conditional_multi"], 1) + + def test_small_multi_probability_does_not_bound_multi_mass(self): + for n in (2, 5, 16, 31): + p1, pn = F(1, n * n), F(1, n ** 3) + s = check.count_statistics({0: 1 - p1 - pn, 1: p1, n: pn}) + self.assertEqual(pn / p1, F(1, n)) + self.assertEqual(s["multi_mass"] / p1, 1) + + def test_multi_mass_control_does_not_control_factorials(self): + for n in (2, 5, 16, 31): + p1, pn = F(1, n * n), F(1, n ** 4) + s = check.count_statistics({0: 1 - p1 - pn, 1: p1, n: pn}) + self.assertEqual(s["multi_mass"] / p1, F(1, n)) + self.assertEqual(s["second_factorial"] / p1, 1 - F(1, n)) + + def test_count_identities_and_singleton_tv(self): + for n in (2, 3, 7, 15): + s = check.count_statistics({0: F(1, 4), 1: F(1, 4), n: F(1, 2)}) + self.assertEqual(s["mean"] - s["occurrence"], s["excess"]) + self.assertLessEqual(s["excess"], s["multi_mass"]) + self.assertLessEqual(s["multi_mass"], 2 * s["excess"]) + self.assertEqual(s["conditional_multi"], F(2, 3)) + + def test_zero_occurrence_does_not_invent_a_conditional_law(self): + s = check.count_statistics({0: F(1)}) + self.assertEqual(s["mean"], 0) + self.assertEqual(s["excess"], 0) + self.assertIsNone(s["conditional_multi"]) + + def test_invalid_count_laws_are_rejected(self): + for law in ({-1: 1}, {True: 1}, {1.0: 1}, {0: F(1, 2)}, + {0: 2, 1: -1}, {1: 1.0}, {1: True}, {}): + with self.subTest(law=law), self.assertRaises(ValueError): + check.count_statistics(law) + + +class MarkControls(unittest.TestCase): + def test_marked_laws_retain_two_different_samplings(self): + s = check.mark_statistics([(F(1, 2), ()), (F(1, 3), ("red",)), + (F(1, 6), ("blue", "blue", "green"))]) + self.assertEqual(s["intensity"], {"red": F(2, 5), "blue": F(2, 5), "green": F(1, 5)}) + self.assertEqual(s["field_first"], {"red": F(2, 3), "blue": F(2, 9), "green": F(1, 9)}) + self.assertEqual(s["excess_law"], {"blue": F(2, 3), "green": F(1, 3)}) + self.assertEqual(s["tv"], F(4, 15)) + self.assertEqual(s["tv_bound"], F(2, 5)) + + def test_excess_mixture_identity_and_total_variation_bound(self): + # Vary actual fields and marks, including a tuple-valued mark. + for i in range(7): + for j in range(7 - i): + s = check.mark_statistics([(F(i, 6), ()), + (F(j, 6), ("a",)), + (F(6 - i - j, 6), ("b", ("c", 1), "b"))]) + if s["mean"] == 0: + self.assertIsNone(s["tv"]) + continue + p, m, e = s["occurrence"], s["mean"], s["excess"] + for label in set(s["field_first"]) | set(s["intensity"]): + defect = (s["excess_law"] or {}).get(label, F(0)) + self.assertEqual(s["intensity"].get(label, 0), + p / m * s["field_first"].get(label, 0) + e / m * defect) + self.assertLessEqual(s["tv"], e / m) + + def test_no_excess_and_empty_field_cases(self): + s = check.mark_statistics([(F(1, 2), ()), (F(1, 3), ("a",)), (F(1, 6), ("b",))]) + self.assertEqual(s["field_first"], {"a": F(2, 3), "b": F(1, 3)}) + self.assertEqual(s["field_first"], s["intensity"]) + self.assertIsNone(s["excess_law"]) + self.assertEqual(s["tv"], 0) + z = check.mark_statistics([(F(1), ())]) + for name in ("field_first", "intensity", "excess_law", "tv", "tv_bound"): + self.assertIsNone(z[name]) + + def test_tv_uses_half_the_l1_distance(self): + self.assertEqual(check.total_variation({"a": F(3, 4), "b": F(1, 4)}, + {"b": F(1, 2), "c": F(1, 2)}), F(3, 4)) + self.assertEqual(check.total_variation({"a": F(1)}, {"b": F(1)}), 1) + + def test_coalescing_equal_marks_does_not_size_bias_fields(self): + s = check.mark_statistics([(F(1, 2), ("a",)), (F(1, 2), ("b", "b", "b"))]) + self.assertEqual(s["field_first"], {"a": F(1, 2), "b": F(1, 2)}) + self.assertEqual(s["intensity"], {"a": F(1, 4), "b": F(3, 4)}) + self.assertEqual(s["tv"], F(1, 4)) + + def test_invalid_mark_laws_are_rejected(self): + cases = [[], [(F(1, 2), ("a",))], [(-1, ()), (2, ("a",))], + [(1.0, ("a",))], [(True, ())], [(1, "not-a-mark-sequence")], + [(1, ([1],))]] + for fields in cases: + with self.subTest(fields=fields), self.assertRaises(ValueError): + check.mark_statistics(fields) + for left in ({}, {"a": F(1, 2)}, {"a": -1, "b": 2}, {"a": 1.0}): + with self.subTest(left=left), self.assertRaises(ValueError): + check.total_variation(left, {"a": 1}) + + +class ScalingControls(unittest.TestCase): + def test_radial_and_pin_jacobians_give_twelve_over_three(self): + self.assertEqual(check.radial_pushforward(12, 1), (F(4), F(-2, 3), F(-1, 3))) + self.assertEqual(check.radial_pushforward(7, 5), (F(7, 3), F(-2), F(1))) + self.assertEqual(check.radial_pushforward(6, 0, 2), (F(3), F(-1, 2), F(-1, 2))) + + def test_cumulative_integral_agrees_with_density(self): + self.assertEqual(check.radial_cumulative(12, 1), (F(6), F(-2, 3), F(2, 3))) + for power in (0, 1, 3, 5): + density = check.radial_pushforward(F(7, 2), power) + cumulative = check.radial_cumulative(F(7, 2), power) + self.assertEqual(cumulative[0] * cumulative[2], density[0]) + self.assertEqual(cumulative[1], density[1]) + self.assertEqual(cumulative[2] - 1, density[2]) + + def test_density_evaluation_uses_gap_derivative(self): + self.assertEqual(check.radial_density_at_r(12, 1, 2, F(1, 4)), 8) + self.assertEqual(check.radial_density_at_r(2, 5, 3, F(1, 2)), F(1, 36)) + self.assertEqual(check.radial_density_at_r(5, 0, 3, F(1, 2), 2), F(5, 3)) + + def test_error_orders_include_the_jacobian(self): + # A radial density r^a dr becomes ell^((a-2)/3), not ell^(a/3). + table = {1: F(-1, 3), 2: F(0), 4: F(2, 3), 5: F(1)} + for power, expected in table.items(): + self.assertEqual(check.radial_pushforward(1, power)[2], expected) + + def test_invalid_scaling_inputs_are_rejected(self): + for args in ((1, 1, 0), (1.0, 1, 3), (1, True, 3), (1, 1, True)): + with self.subTest(args=args), self.assertRaises(ValueError): + check.radial_pushforward(*args) + with self.assertRaises(ValueError): + check.radial_cumulative(1, -1) + for k, r in ((0, 1), (1, 0), (-1, 1), (1, -1)): + with self.subTest(k=k, r=r), self.assertRaises(ValueError): + check.radial_density_at_r(1, 1, k, r) + + +class FoldControls(unittest.TestCase): + def test_endpoint_jet_and_third_derivative(self): + self.assertEqual(check.fold_jet(12, F(1, 2), F(-1, 4)), + (F(1, 8), F(0), F(-6), F(24))) + self.assertEqual(check.fold_jet(12, F(1, 2), F(1, 4)), + (F(-1, 8), F(0), F(6), F(24))) + self.assertEqual(check.fold_jet(12, F(1, 2), 0), + (F(0), F(-3, 4), F(0), F(24))) + + def test_fold_gap_matches_kappa_r_cubed(self): + for a, r in ((F(3), F(1, 5)), (F(7, 3), F(2, 7)), (F(12), F(1, 2))): + left, right = check.fold_jet(a, r, -r / 2), check.fold_jet(a, r, r / 2) + self.assertEqual(left[1], 0) + self.assertEqual(right[1], 0) + self.assertLess(left[2], 0) + self.assertGreater(right[2], 0) + self.assertEqual(left[0] - right[0], a * r ** 3 / 6) + self.assertEqual(left[3], 2 * a) + + def test_derivative_is_strictly_convex_and_two_root_model_is_oriented(self): + r, a = F(2, 3), F(9, 2) + values = [check.fold_jet(a, r, x)[1] for x in (-r, -r / 2, 0, r / 2, r)] + self.assertEqual(values, [F(3, 2), F(0), F(-1, 2), F(0), F(3, 2)]) + for x, y in ((F(-2), F(1)), (F(-1, 3), F(2, 5))): + slope = (check.fold_jet(a, r, y)[2] - check.fold_jet(a, r, x)[2]) / (y - x) + self.assertEqual(slope, 9) + self.assertEqual(check.fold_jet(a, r, (x + y) / 2)[3], slope) + + def test_degenerate_or_inexact_fold_inputs_are_rejected(self): + for a, r, x in ((0, 1, 0), (-1, 1, 0), (1, 0, 0), (1, -1, 0), + (1.0, 1, 0), (1, 1, 0.1), (True, 1, 0)): + with self.subTest(a=a, r=r, x=x), self.assertRaises(ValueError): + check.fold_jet(a, r, x) + + def test_curved_ridge_third_derivative_is_not_raw_partial(self): + # f=b-kr^3/2+2kx^3-3kr^2*x/2-(z-q(x^2-r^2/4))^2/2. + # Raw f_xxx vanishes at x=1/4 here; reduced g''' remains 12. + self.assertEqual(check.curved_ridge_third(1, F(1, 2), 2, F(1, 4)), (F(0), F(12))) + self.assertEqual(check.curved_ridge_third(1, F(1, 2), 2, F(1, 8)), (F(6), F(12))) + self.assertEqual(check.curved_ridge_third(F(1, 2), F(1, 3), 1, F(-1, 4)), (F(9), F(6))) + self.assertEqual(check.curved_ridge_third(2, F(1, 2), 0, 3), (F(24), F(24))) + for args in ((0, 1, 1, 1), (1, 0, 1, 1), (1, 1, 0.5, 1)): + with self.subTest(args=args), self.assertRaises(ValueError): + check.curved_ridge_third(*args) + + +class SourceControls(unittest.TestCase): + def test_seven_exact_imported_source_identities(self): + self.assertEqual(verify_sources.verify_sources(), 7) + + @staticmethod + def entry(path, data): + return {"local_path": path, "bytes": len(data), + "sha256": hashlib.sha256(data).hexdigest(), + "blob": hashlib.sha1(b"blob " + str(len(data)).encode() + b"\0" + data).hexdigest()} + + def test_source_byte_and_metadata_tampering_are_rejected(self): + with tempfile.TemporaryDirectory() as directory: + root = Path(directory) + data = b"exact source\n" + (root / "source").write_bytes(data) + entry = self.entry("source", data) + verify_sources.verify_entry(root, entry) + for key, value in (("bytes", len(data) + 1), ("sha256", "0" * 64), ("blob", "0" * 40)): + with self.subTest(key=key), self.assertRaises(ValueError): + verify_sources.verify_entry(root, dict(entry, **{key: value})) + (root / "source").write_bytes(b"wrong source\n") + with self.assertRaises(ValueError): + verify_sources.verify_entry(root, entry) + + def test_source_path_escape_and_symlink_are_rejected(self): + with tempfile.TemporaryDirectory() as directory: + root = Path(directory) + data = b"source" + (root / "real").write_bytes(data) + (root / "alias").symlink_to(root / "real") + for path in ("../real", str(root / "real"), "./real", "alias"): + with self.subTest(path=path), self.assertRaises(ValueError): + verify_sources.verify_entry(root, self.entry(path, data)) + + def test_manifest_whitespace_tampering_is_rejected(self): + packet = Path(__file__).resolve().parent + with tempfile.TemporaryDirectory() as directory: + manifest = Path(directory) / "SOURCES.json" + manifest.write_bytes((packet / "SOURCES.json").read_bytes() + b" ") + with self.assertRaisesRegex(ValueError, "manifest digest"): + verify_sources.verify_sources(packet.parents[1], manifest) + + +MUTATIONS = ( + ("mean-loses-multiplicity", "p * k for k, p in weights.items()), Fraction(0))", "p * (k > 0) for k, p in weights.items()), Fraction(0))"), + ("occurrence-size-biased", "p for k, p in weights.items() if k > 0", "p * k for k, p in weights.items() if k > 0"), + ("excess-drops-minus-one", "p * max(k - 1, 0)", "p * k"), + ("multi-loses-count-weight", "p * k for k, p in weights.items() if k >= 2", "p for k, p in weights.items() if k >= 2"), + ("factorial-becomes-excess", "p * k * (k - 1)", "p * max(k - 1, 0)"), + ("conditional-multi-wrong-divisor", "multi_probability / occurrence", "multi_probability / mean"), + ("accept-bool-probability", "isinstance(value, bool) or not isinstance(value, (int, Fraction))", "not isinstance(value, (int, Fraction))"), + ("negative-probability", "any(p < 0 for p in weights.values()) or sum(weights.values()) != 1", "sum(weights.values()) != 1"), + ("tv-misses-half", "Fraction(0)) / 2", "Fraction(0))"), + ("intensity-loses-size-bias", "intensity[label] += probability", "intensity[label] += probability / k"), + ("field-sampling-size-biased", "field[label] += probability / k", "field[label] += probability"), + ("excess-mark-misses-minus-one", "probability * (k - 1) / k", "probability"), + ("tv-bound-wrong-normalizer", "tv_bound=e / m", "tv_bound=e / p"), + ("pushforward-misses-cubic-divisor", "return amplitude / q, -order, order - 1", "return amplitude, -order, order - 1"), + ("pushforward-wrong-kappa-power", "return amplitude / q, -order, order - 1", "return amplitude / q, order, order - 1"), + ("pushforward-misses-jacobian-power", "return amplitude / q, -order, order - 1", "return amplitude / q, -order, Fraction(a, q)"), + ("cumulative-misses-integration", "return amplitude / (a + 1), -order, order", "return amplitude, -order, order"), + ("density-wrong-gap-derivative", "q * kappa * r ** (q - 1)", "kappa * r ** q"), + ("fold-gap-wrong-sign", "x ** 3 / 3 - r ** 2 * x / 4", "x ** 3 / 3 + r ** 2 * x / 4"), + ("fold-critical-pins-shift", "a * (x ** 2 - r ** 2 / 4)", "a * (x ** 2 - r ** 2)"), + ("fold-third-derivative-dropped", "2 * a * x, 2 * a)", "2 * a * x, Fraction(0))"), + ("curved-ridge-tangent-sign", "v = -derivative(1, 1) / derivative(0, 2)", "v = derivative(1, 1) / derivative(0, 2)"), + ("curved-ridge-raw-for-reduced", "return raw, reduced", "return raw, raw"), +) + + +def run_mutations(): + """Change executable behavior in scratch trees; reject each in both modes.""" + packet = Path(__file__).resolve().parent + source = (packet / "check.py").read_text() + manifest = json.loads((packet / "SOURCES.json").read_text()) + results = [] + with tempfile.TemporaryDirectory(prefix="c52-finite-mutants-") as directory: + root = Path(directory) + target = root / "frontiers" / packet.name + target.mkdir(parents=True) + for name in ("test_check.py", "verify_sources.py", "SOURCES.json"): + shutil.copyfile(packet / name, target / name) + for entry in manifest["sources"]: + destination = root / entry["local_path"] + destination.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(packet.parents[1] / entry["local_path"], destination) + for name, old, new in (("baseline", "", ""),) + MUTATIONS: + if name != "baseline" and source.count(old) != 1: + raise RuntimeError("mutation anchor is not unique: " + name) + mutated = source if name == "baseline" else source.replace(old, new, 1) + (target / "check.py").write_text(mutated) + for optimized in (False, True): + command = [sys.executable, "-B"] + (["-O"] if optimized else []) + ["-S", str(target / "test_check.py")] + run = subprocess.run(command, capture_output=True, text=True, timeout=30) + output = run.stdout + run.stderr + if name == "baseline": + good = run.returncode == 0 and "\nOK\n" in output + else: + good = run.returncode != 0 and "Ran " in output and "FAILED (" in output + row = {"mutation": name, "mode": "optimized" if optimized else "normal", + "returncode": run.returncode, "expected_outcome": good} + results.append(row) + if not good: + print(output) + print(json.dumps(results, indent=2)) + raise RuntimeError("unexpected mutation outcome: " + name) + print(json.dumps({"mutations_per_mode": len(MUTATIONS), "baseline_modes": 2, + "results": results, "scope": "Finite implementation controls only"}, indent=2)) + + +if __name__ == "__main__": + if sys.argv[1:] == ["--mutants"]: + run_mutations() + else: + unittest.main() diff --git a/frontiers/ordinary_short_bar_occurrence_20261001/verify_sources.py b/frontiers/ordinary_short_bar_occurrence_20261001/verify_sources.py new file mode 100644 index 000000000..0ffd6b5e9 --- /dev/null +++ b/frontiers/ordinary_short_bar_occurrence_20261001/verify_sources.py @@ -0,0 +1,60 @@ +"""Finite exact controls and source identity; not a continuum proof certificate.""" +from fractions import Fraction as F +import hashlib +import json +from pathlib import Path, PurePosixPath + +SOURCE_MANIFEST_SHA256 = '1676f2411b86e607aecbe061130cf10ba805c1cf39bba8fff56c5fa796b91d03' + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def contained_file(root, relative): + require(isinstance(relative, str) and bool(relative), 'invalid source path') + parts = PurePosixPath(relative) + require(not parts.is_absolute() and str(parts) == relative + and all(p not in ('', '.', '..') for p in parts.parts) + and '\\\\' not in relative, 'noncanonical source path') + target = root + for part in parts.parts: + target = target / part + require(not target.is_symlink(), 'symlink source') + require(target.is_file() and root in target.resolve().parents, + 'source must be a contained regular file') + return target + + +def verify_entry(root, entry): + root = Path(root).resolve() + data = contained_file(root, entry.get('local_path')).read_bytes() + require(type(entry.get('bytes')) is int and len(data) == entry['bytes'], + 'source byte count') + require(hashlib.sha256(data).hexdigest() == entry.get('sha256'), + 'source SHA256') + blob = hashlib.sha1(b'blob '+str(len(data)).encode('ascii')+b'\0'+data).hexdigest() + require(blob == entry.get('blob'), 'source Git blob') + + +def verify_sources(repo=None, manifest_path=None): + script = Path(__file__).absolute() + require(not script.is_symlink(), 'symlink checker') + root = Path(repo).resolve() if repo is not None else script.resolve().parents[2] + if manifest_path is None: + manifest_path = contained_file(root, 'frontiers/ordinary_short_bar_occurrence_20261001/SOURCES.json') + data = Path(manifest_path).read_bytes() + require(hashlib.sha256(data).hexdigest() == SOURCE_MANIFEST_SHA256, + 'source manifest digest') + manifest = json.loads(data) + entries = manifest['sources'] + require(len(entries) == 7, 'seven exact sources required') + require(len({e['key'] for e in entries}) == 7, 'duplicate source key') + for entry in entries: + verify_entry(root, entry) + return len(entries) + + +if __name__ == "__main__": + print(json.dumps({"verified_sources": verify_sources(), "scope": "Source identity only, not analytic acceptance"}))