From e7f89290ba94322ab1cca380299932f222847603 Mon Sep 17 00:00:00 2001 From: Dylan Roy Date: Tue, 29 Sep 2026 18:18:00 -0500 Subject: [PATCH] Add rare-intensity norm control and conditional planar cluster-law closure Targeted companion to #158: field-norm insertion from landed Palm regions, credited deep-transverse mechanism, strict typed-jet tightness and local/remote separation. Conditional global one/two-cluster intensity theorem depends explicitly on the unaccepted #158 compact-sector result. No existing proof, review, graph, Boolean or prize changes. --- .github/workflows/local-cluster-tightness.yml | 40 ++ .../local_cluster_tightness_20260929/PROOF.md | 398 ++++++++++++++++++ .../README.md | 33 ++ .../RECONNAISSANCE.md | 22 + .../RESULTS.json | 9 + .../SOURCE_FILES.json | 66 +++ .../SOURCE_MAP.json | 87 ++++ .../controls.py | 61 +++ .../custody.py | 48 +++ .../test_controls.py | 65 +++ .../test_custody.py | 37 ++ .../verify.py | 64 +++ 12 files changed, 930 insertions(+) create mode 100644 .github/workflows/local-cluster-tightness.yml create mode 100644 frontiers/local_cluster_tightness_20260929/PROOF.md create mode 100644 frontiers/local_cluster_tightness_20260929/README.md create mode 100644 frontiers/local_cluster_tightness_20260929/RECONNAISSANCE.md create mode 100644 frontiers/local_cluster_tightness_20260929/RESULTS.json create mode 100644 frontiers/local_cluster_tightness_20260929/SOURCE_FILES.json create mode 100644 frontiers/local_cluster_tightness_20260929/SOURCE_MAP.json create mode 100644 frontiers/local_cluster_tightness_20260929/controls.py create mode 100644 frontiers/local_cluster_tightness_20260929/custody.py create mode 100644 frontiers/local_cluster_tightness_20260929/test_controls.py create mode 100644 frontiers/local_cluster_tightness_20260929/test_custody.py create mode 100644 frontiers/local_cluster_tightness_20260929/verify.py diff --git a/.github/workflows/local-cluster-tightness.yml b/.github/workflows/local-cluster-tightness.yml new file mode 100644 index 000000000..365bad977 --- /dev/null +++ b/.github/workflows/local-cluster-tightness.yml @@ -0,0 +1,40 @@ +name: Local cluster tightness and conditional closure controls + +'on': + pull_request: + paths: + - 'frontiers/local_cluster_tightness_20260929/**' + - '.github/workflows/local-cluster-tightness.yml' + - 'frontiers/c6_palm_route_20260929/PROOF.md' + - 'frontiers/d5_dimension_lift_20260929/PROOF.md' + - 'frontiers/remote_window_20260924/PROOF.md' + - 'frontiers/remote_collision_20260928/PROOF.md' + - 'frontiers/window_multiplicity_laws_20260928/LOCAL_MULTIPLICITY.md' + - 'frontiers/c6_rare_cluster_laws_20260929/PROOF.md' + push: + branches: [main] + paths: + - 'frontiers/local_cluster_tightness_20260929/**' + - '.github/workflows/local-cluster-tightness.yml' + workflow_dispatch: + +permissions: + contents: read + +jobs: + exact-tightness: + runs-on: ubuntu-latest + timeout-minutes: 10 + steps: + - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 + with: + fetch-depth: 0 + persist-credentials: false + - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 + with: + python-version: '3.11.16' + - name: Both modes, semantic controls and exact current/historical sources + run: | + set -euo pipefail + python -B -S frontiers/local_cluster_tightness_20260929/verify.py --repo "${GITHUB_WORKSPACE}" --output "${RUNNER_TEMP}/tightness-${GITHUB_RUN_ID}-${GITHUB_RUN_ATTEMPT}" + git diff --exit-code diff --git a/frontiers/local_cluster_tightness_20260929/PROOF.md b/frontiers/local_cluster_tightness_20260929/PROOF.md new file mode 100644 index 000000000..adffa6916 --- /dev/null +++ b/frontiers/local_cluster_tightness_20260929/PROOF.md @@ -0,0 +1,398 @@ +# Rare-intensity tightness and a conditional planar cluster-law closure + +Object: OA-LOCAL-CLUSTER-TIGHTNESS-20260929-v1. +Author: OpenAI / GPT-6 Astra Pro, 29 September 2026. +Disposition: AUTHOR-SIDE PROOF CANDIDATE. Nonauthor analytic review required. +Scientific effect NONE. No prior proof, verdict, graph, register or prize changed. + +## 1. Purpose, law and exact dependency boundary + +This is the bounded companion requested by the author of Math-#158 in #157 +comment 5900564419. It does not duplicate that source's cubic classification. +It supplies rare-event field-norm control, strict-domain tightness and a +local/remote gluing argument. The requested deterministic transverse reduction +was also written by the #158 author in source D before this companion was +published. Section3 gives a self-contained alternate-constant derivation of +that SAME mechanism, not a priority claim or an independent review of D. + +The original variance-one periodized Gaussian field, its fixed torus side T, +fixed dimension, birth b, positive gap k, and pin frame are unchanged. The pins +are M=(-r/2,0), S=(r/2,0), with f(M)=b, f(S)=b-kr^3 and both gradients zero. +Q_r is their canonical Gaussian regression law. W_r is the original typed +maximum/saddle determinant product, Z_r=E_Qr W_r is the FULL normalizer, and +P_r=Q_r^W=(W_r/Z_r)Q_r. N counts additional all-index critical points in +I_r=(b-kr^3,b), excluding M,S, on the entire torus. No other normalizer is used. + +Source P (landed Palm proof) supplies its canonical field-mark Kac--Rice formula, +all fixed conditional C6 moments and the regional density/determinant ledgers. +Source DL supplies the shell mean estimate; RM/RC the fixed-remote singleton and +second-factorial results. Source L supplies the planar ten-jet regression and +pinned cubic expansion. Exact immutable identities are in SOURCE_MAP.json. + +Source C is the NEW, still author-side #158 manuscript at325c5ebd. Its Theorems +C/G/F (classifier, compact-sector limit, finite positive coefficient integrals) +are EXPLICIT PREMISES only of Sections6--8 below. They are not revalidated or +accepted by this companion. Sections2--5 do not consume those new theorems. +Source D is the companion DEEP_TRANSVERSE_EXCLUSION.md at bfcc67dc, recovered +from comment5900634812 during this continuation. Its attribution is mandatory +and byte-bound. No new independent-provider credit is claimed by repeating its +implicit-graph mechanism with different constants. +The marked-Fourier candidate #157 is NOT an input anywhere. Thus review of #157 +is not a prerequisite to checking the field-norm lemma requested for #158. + +Let K4=1+||f||C4; any fixed full derivative norm may be used. On a fixed torus, +K4 is bounded by a fixed multiple of source P's K6. Norms in an orthonormal pin +frame are uniformly equivalent, but no rotational invariance of the torus law +is invoked. Constants depend on the fixed model/mark family, and on R or moment +orders where explicitly displayed. No numerical Gaussian constants are provided. +The final coefficient limits fix b,k,T and frame, as in source C. + +## 2. Lemma N: field-norm moments at the rare intensity scale + +For every fixed integer p>=1, in every fixed d>=2, + + E_Pr[N K4^p] <= C_p r^3. (N1) + +Consequently, for M>=1, + + r^-3 E_Pr[N 1{K4>M}] <= C_p M^-p, + r^-3 P_r(N_D>=1, K4>M) <= C_p M^-p, (N2) + +for any deterministic subregion D and its count N_D<=N. The second bound also +holds for any event implying N>=1. These are RARE-INTENSITY bounds, not a claim +that division of an unconditional derivative tail by r^3 stays small. + +Proof. Apply P Lemma5.1 first with the bounded mark W_r min(K4^p,A), and pass +monotonically to the limit A->infinity. Its explicitly fixed Gaussian regression +kernels avoid any evaluation of an arbitrary a.e. version at zero gradient. +In each region, the source proof bounds W_r |det H_X| by a deterministic +geometric factor times K6^(3d). Multiplication by K4^p changes only the moment +order. P Lemma4.4 gives + + E_Q'[K6^(3d+p)] <= C_p(1+beta)^(3d+p). (N3) + +The same conclusion for a noninteger p follows by increasing to an integer, +but it is enough to state (N1) for integers. Here Q' is the ACTUAL witness law, +including the height only in the regions that use it. The original W occurs +once inside the integrand, and the original Z once outside. + +For completeness the additional losses and their absorptions are: + +- Pin balls R1: multiply by (1+chi)^p. In the ordinary cone the penalty + exp(-c chi^2) absorbs this fixed polynomial without changing |q|^(2-d). + In the tiny axial cone chi<=1/r, so exp(-c/r^2) absorbs the extra r^-p. +- Collar R2a: beta<=C r^-10; exp(-c r^-2/3) absorbs r^-10p. +- Collar R2b: beta<=C |v|^-4; exp(-c/|v|^2) absorbs |v|^-4p. +- Collar R2c: beta is bounded, so the moment factor is a constant. +- Shell R3a: beta<=C s^-10; exp(-c s^-1/4) absorbs s^-10p. Use the + endpoint-short-column/Hadamard bound throughout the WHOLE strip, not only + at v=0. That determinant bound is already explicit in P's repaired source. +- Shell R3b: beta<=C |v|^-6; exp(-c/|v|^2) absorbs |v|^-6p. Away from zero + the same factor is uniformly bounded. The shell and height powers do not change. +- Remote R4: beta is bounded for fixed exclusion and window targets. + +For each fixed p, sup_{t>0} t^a exp(-c t^b) is finite whenever a,b,c>0, so +these absorptions cost C_p only. In the all-height inner regions their bounds +dominate the window count. The shell sum is still summable and its height +length remains kr^3. Sum exactly P/DL's tiling. This proves (N1); Markov in the +valid count-weighted direction proves (N2). No count exponential moment is used. + +## 3. Lemma T: an extra nearby point forces a soft transverse entry + +This is a self-contained version of the DETERMINISTIC planar mechanism already +written in source D, with alternative conservative constants and an absolute- +value conclusion that does not require endpoint types. It is not claimed as a +new mechanism distinct from D. Fix R>=1. Let f be C4 on a neighborhood +of the closed rectangle |x|,|z|<=Rr, with the six exact pins above. Suppose each +coordinate partial derivative through order4 is bounded by K>=1 there. Put + + A_R = 64(R+1)^2, a0=f_zz(0,0). + +If + + r <= k/[2(R+1)K], |a0| >= A_R r K^2/k, (T1) + +then the rectangle contains no critical points other than M,S. In particular, +any additional critical point in B(0,Rr), of ANY height or type, implies + + |f_zz(0)| <= A_R r K^2/k (T2) + +when the first inequality of (T1) holds. For a torus use a local lift with the +rectangle embedded, e.g. r=12k, so K>=k automatically. For +|x|<=Rr and |z|<=r/8, the C4 bound gives + + |f_xxx(x,z)-12k| <= (R+1)rK. (T4) + +Let phi(x)=f_z(x,0). Its values at +-h vanish, and |phi''|<=K. The ordinary +interpolation remainder (also valid outside the two nodes in this rectangle) +and Rolle's theorem give + + |phi(x)| <= (K/2)|x^2-h^2| <= (R+1)^2 K r^2/2, + |phi'(x)| <= (R+1/2)Kr. (T5) + +The second inequality uses a zero of phi' between the two nodes. From (T1), +|a0|>=64(R+1)^2 rK, whereas |f_zz(x,z)-a0|<=2RrK. Thus f_zz has one sign +throughout the rectangle and |f_zz|>=|a0|/2. The changes of f_z between z=0 +and z=+-Rr dominate (T5) strictly. For each |x|<=Rr there is exactly one root +z=h_r(x) of f_z=0 in the rectangle, and + + |h_r(x)| <= (R+1)^2 K r^2/|a0| <= r/8. (T6) + +The implicit function theorem makes h_r C3. Any critical point in the rectangle +lies on this graph; in particular h_r(+-r/2)=0 by uniqueness and the exact pins. +Let q=f_xz/f_zz evaluated on the graph. Equations(T5)-(T6) yield + + |f_xz(x,h_r(x))| <= (R+1)rK, + |q| <= 2(R+1)rK/|a0| <= k/[32(R+1)K] <= 1. (T7) + +Set g(x)=f_x(x,h_r(x)). Differentiating the Schur complement, NOT discarding +its mixed terms, gives + + g'=f_xx-f_xz^2/f_zz, + g''=f_xxx-3q f_xxz+3q^2 f_xzz-q^3 f_zzz. (T8) + +There is no fifth derivative, spectral frame or invariant-manifold theorem. +Together with r<=k/[2(R+1)K], (T4) and (T7) show + + g'' >=12k-k/2-7K|q| + >=12k-k/2-7k/[32(R+1)] > 10k >0. (T9) + +Thus g is strictly convex. It already vanishes at -r/2 and r/2, and a strictly +convex real function cannot have three distinct zeros. These are its only +zeros, proving the lemma. No maximum/saddle type assumption was used. + +The K^2/k dependence is essential to this argument. Merely keeping f_zz away +from zero by a multiple of rK does not make the mixed correction small relative +to k uniformly over the allowed derivative sizes. + +## 4. Tightness in the strict typed soft-jet domain + +Return to d=2 and fix R. Put + + Theta_r=(s,a,beta,c)=(f_zz(0)/r,f_xxz(0),f_xzz(0),f_zzz(0)), + B=beta-a^2/(12k), + D_k={s<-|B|/2}. + +Let A_{r,R} count additional window points in B(0,Rr). Define the finite +NONEMPTY measure + + eta_r^R(E)=r^-3 P_r(Theta_r in E, A_{r,R}>=1). (J1) + +For every epsilon>0 there is a compact C contained STRICTLY in D_k such that + + limsup_(r->0) eta_r^R(R^4 minus C) <= epsilon. (J2) + +This statement does NOT include the enormous N=0 mass outside the rare layer. + +Proof. By (N2), choose M so the scaled probability of A_{r,R}>=1 and K4>M is +at most epsilon/3. On K4<=M and sufficiently small r (depending on fixed M,R), +Lemma T gives |s|<=A_R M^2/k and |a|,|beta|,|c|<=C M. This is a compact box. + +Source L's planar ten-jet rank implies a uniform upper bound for the density +of (f_zz,f_xxz,f_xzz,f_zzz) under Q_r: appending these four variables to U_r +converges to all independent planar jets of order<=3. The physical density +change f_zz=rs has Jacobian r. On the above compact box and K4<=M, endpoint +Taylor identities show every endpoint Hessian entry is O_M(r), hence W_r<=C_Mr^4. +Because Z_r>=c r^2, for every Borel E in that box, + + r^-3 P_r(Theta_r in E,K4<=M) <= C_M Leb_4(E). (J3) + +No independence between the remainder and the jets is asserted. + +The limiting endpoint Hessians divided by r have determinants +-6k(s-B/2) at M and 6k(s+B/2) at S, with uniform O_M(r) errors on this box. +Under P_r the maximum/saddle types hold wherever W_r>0. Thus + + s-B/2 <= C_M r, s+B/2 <= C_M r. (J4) + +These inequalities put Theta_r in a shrinking neighborhood of the closed domain +D_k. Its boundary s=-|B|/2 has four-dimensional Lebesgue measure zero: for each +(a,beta,c) it is one value of s. A vertical layer of thickness 2delta in a +bounded box has volume at most 2delta times the other three side lengths. +Use (J3), first choosing delta small and then r small. The mass not satisfying +s<=-|B|/2-delta is arbitrarily small. Intersect this strict inequality with the +fixed box to get C, proving (J2). This also handles the absolute-value corner at +B=0; no differentiable boundary chart is needed. + +## 5. Local and fixed-remote events do not mix at leading order + +Fix R and delta>0. Let C_{r,delta} count points at dist(X,0)>=delta. Then + + P_r(A_{r,R}>=1, C_{r,delta}>=1)=o(r^3). (M1) + +Proof. On K4<=M, (T2) forces |f_zz(0)|<=S_{R,M}r. Upper-bound the joint event +by the marked REMOTE count with these two field restrictions. Disintegrate in +the physical scalar t=f_zz(0), the remote gradient, and its height h in I_r. +The joint frame (U_r,f_zz(0),grad f(X),f(X)) has a uniform covariance floor for +|X|>=delta, through r=0: f_zz is a new midpoint monomial and X is a distinct +remote site. Positive Fourier spectrum and compactness give the density bound. +On K4<=M and |t|<=S_{R,M}r, W_r<=C_{R,M}r^4 and |det H_X|<=C_M. Hence the +unnormalized integral is bounded by a constant times + + r^4 * r * r^3 = r^8, + +where the factors are the endpoint weight, width of the PHYSICAL f_zz band, +and remote height window. Division by the one full Z_r>=c r^2 gives O(r^6). +All constants here may depend on fixed R,M,delta. Outside K4<=M, the joint event +implies N>=1, so (N2) bounds its probability by C_p M^-p r^3. Therefore + + limsup_(r->0) r^-3 P_r(joint) <= C_p M^-p. + +Now let M->infinity. No quantitative rate in (M1) is claimed after that limit, +and no mixed-event independence assumption is used. + +## 6. Conditional closure theorem for source C's coefficient law + +From this point ASSUME the exact Theorems C/G/F of source C (#158), at their +fixed planar parameter scope. Let n(theta) in {0,1,2}, w(theta), h_0 and z_0 be +its classifier, soft determinant weight, contact four-jet density and FULL +normalizer. Define the finite positive coefficients already supplied there: + + alpha_j = integral_(D_k) (w/z_0)h_0(0,a,beta,c)1{n=j} dtheta, + j=1,2. (G1) + +Source RM defines the full contact singleton kernel Lambda_j(X) with the +endpoint weight INSIDE its conditional expectation. Set + + mu_delta = k integral_(dist(X,0)>=delta) sum_j Lambda_j(X) dX, + mu = lim_(delta->0) mu_delta. (G2) + +The factor k is required: the physical height window has length kr^3. +By RM/RC, for each FIXED delta>0, + + r^-3 Law_+(C_{r,delta}) -> mu_delta delta_1 in l1, (G3) + +where Law_+(Y)(n)=P(Y=n), n>=1. Indeed its mean is mu_delta r^3+O_delta(r^4), +and E(C_{r,delta})_2=O_delta(r^5). Its distance to (E C)delta_1 is at most twice +that second factorial moment. Also 0=1, + nu_r -> nu in l1(n^p), for every fixed integer p>=0, + nu(1)=alpha_1+mu, nu(2)=alpha_2, nu(n>=3)=0. (G4) + +This is a conditional consumer theorem until source C and the new lemmas here +have their own complete analytic reviews. It is NOT an unconditional acceptance +of #158, and it must not be used to change a scientific register. + +### Proof: the spatial and jet limits in their correct order + +DL's shell bound, summed over dyadic shells, gives for R>=4 and 0=R, its limsup after division by +r^3 is at most C R^-2. Constants in this inequality are independent of R,R',delta +within the stated geometric range, since the source shell constants are uniform; +only the small-r requirement depends on fixed R'. Circle boundaries have zero +expected count by spatial Kac--Rice and can be assigned once. + +We first establish the large-R local approximation + + limsup_(r->0) ||r^-3 Law_+(A_{r,R}) + -(alpha_1 delta_1+alpha_2 delta_2)||_1 + <= C R^-2. (G6) + +Fix R and epsilon. By(J2) choose compact C_0 strictly in D_k carrying all but +epsilon of the limsup NONEMPTY local intensity. By source C's integrability of +the nonempty coefficient, enlarge to a compact C containing C_0 such that the +coefficient mass alpha_1+alpha_2 outside C is below epsilon. Choose a fixed +R'>=max(R,R_C) as required by source C's compact-sector theorem. If A_{r,R'} +differs from A_{r,R}, there is a point in the shorter annulus, so its probability +is at most C r^3 R^-2+o(r^3), by(G5). + +Consequently the scaled nonempty law of A_{r,R'} outside C has limsup mass at +most epsilon+C R^-2. On C, source C Theorem G gives full total-variation +convergence, hence l1 convergence of the count marginal restricted to positive +counts, to alpha_1(C)delta_1+alpha_2(C)delta_2. Comparing A_{r,R} with A_{r,R'} +costs at most twice their probability of inequality. Comparing alpha_j(C) with +alpha_j costs at most epsilon. Let epsilon->0. This proves(G6). No interchange +of R_C with an unbounded jet set occurred; R' was fixed only AFTER C was chosen. +In particular we did not assume source C's compact theorem for arbitrary R. + +Now write N=A_{r,R}+B_{r,R,delta}+C_{r,delta} with disjoint regions. For any +nonnegative integer A,B,C, + + ||Law_+(A+B+C)-Law_+(A)-Law_+(C)||_1 + <=3 P(B>=1)+3 P(A>=1,C>=1). (G7) + +This follows by comparing the corresponding atomic signed measures for each +outcome; their l1 norm is at most3, and it vanishes when B=0 and at most one of +A,C is positive. Thus(G3),(G5),(M1),(G6) give + + limsup_(r->0) ||nu_r-[(alpha_1+mu)delta_1+alpha_2 delta_2]||_1 + <= C(R^-2+delta^2)+|mu_delta-mu|. (G8) + +Take R->infinity and then delta->0 (or the reverse, after the r limit). This +proves unweighted l1 convergence and identifies the UNIQUE intensity law at +fixed parameters. It does not claim a convergence rate or uniformity under +varying parameters. + +For a fixed p, source P's all-fixed-order factorial bounds and the first moment +imply sup_r sum n^(p+1) nu_r(n)M} n^p nu_r(n)<=C_{p+1}/M. Combine finite-dimensional convergence with +this uniform integrability to prove the weighted l1 assertion in(G4). No moment +series or exponential moment is needed. QED. + +## 7. Conditional numerical-free consequences + +All statements in this section retain the conditional status of Theorem G. +Writing lambda=alpha_1+alpha_2+mu and m1=alpha_1+2alpha_2+mu, + + P_r(N>=1) ~ lambda r^3, E_Pr N ~ m1 r^3, + P_r(N>=2) ~ alpha_2 r^3, E_Pr(N)_2 ~2 alpha_2 r^3, + E_Pr(N)_q=o(r^3) for each fixed integer q>=3. (C1) + +The last conclusion is NEW conditional information supplied by exhaustion, +not an inference from previous O(r^3) upper bounds. It is compatible with the +existing two-point lower event and does not assert N<=2 for finite r. + +Conditional on N>=1, the limiting probabilities at1,2 are +(alpha_1+mu)/lambda and alpha_2/lambda. Under size bias they are +(alpha_1+mu)/m1 and2alpha_2/m1. These are not the same law. + +For independent replicas, floor(t/r^3) counts sum to a unique compound-Poisson +limit with jumps1 and2, equivalently X+2Y for independent Poisson variables of +means t(alpha_1+mu), t alpha_2. This follows from the standard generating-function +identity already credited in the landed #153 packet. It is NOT a spatial Poisson +limit of points in one field. + +The birth factorization of source C's LOCAL coefficients does not automatically +extend to the GLOBAL law: mu in(G2) is a different remote integral. No global +birth independence, numerical alpha/mu, dimensional extension, explicit error +rate or selected-persistence pairing law is asserted. + +## 8. Review targets, provenance and limits + +Direct review slices: N1's marked norm insertion with all regional factors; +T3--T9's graph reduction including the three mixed derivative terms; J2/J3's +NONEMPTY tightness and typed-boundary control; M1's physical-band/height/weight +powers. Conditional closure slice: G5's uniform shell use, the choice C then R', +G7's signed-measure error, remote coefficient k, and polynomial uniform +integrability. A verdict on these implications does not accept source C's +classifier or compact-sector theorem on the reviewer's behalf. + +All local constants in the deterministic lemma are explicit; all Gaussian +constants remain existential. Large R is taken after small r. Large derivative +cutoffs are taken after the limsup in the mixed event. Gaussian full-field +marks are Borel through derivative limits of the smooth field and are truncated +before monotone convergence. Every mean/count uses original W and Z exactly once. + +The finite controls prove algebra, normalization, conservative constants and +finite-measure inequalities only. They cannot establish the Gaussian bounds, +compactness or any of the analytic theorem premises. No missing historical +program is recreated. Consensus was actually requested and quota-exhausted; +limited primary-source reconnaissance is recorded separately. No novelty or +priority claim is made for classical Schur complementation, convexity, Markov, +Kac--Rice, Gaussian regression, or elementary compound Poisson limits. diff --git a/frontiers/local_cluster_tightness_20260929/README.md b/frontiers/local_cluster_tightness_20260929/README.md new file mode 100644 index 000000000..4c84cbe0f --- /dev/null +++ b/frontiers/local_cluster_tightness_20260929/README.md @@ -0,0 +1,33 @@ +# Local cluster tightness: source-bound companion to #158 + +Author-side mathematics, nonauthor review required. Scientific effect NONE. + +The direct field-norm lemma proves a rare-intensity bound by inserting K4^p into +the LANDED Palm regional argument. It does not consume #157's still-new count +exponential theorem. The deterministic transverse argument is the SAME mechanism +already written by #158's author; it is credited and byte-bound, not claimed as +an independent discovery. The new work combines it with strict typed-boundary +control, a mixed local/remote estimate, and a carefully ordered exhaustion. + +Sections6-7 state a CONDITIONAL closure of the planar global count law using +#158's exact, still-author-side compact-sector theorem. The proposed coefficients +are nu(1)=alpha1+mu_remote and nu(2)=alpha2, with higher values zero in the scaled +limit. This is NOT acceptance of #158, finite-r support {1,2}, a spatial Poisson +limit, or a scientific-register transition. The remote coefficient includes k. + +Run all finite controls in both Python modes: + + python -B -S verify.py --output /path/to/new-output + python -B -O -S verify.py --output /path/to/other-new-output + +Each invocation checks exact packet membership, sizes/SHA256/Git blobs, executes +12 mathematical and6 synthetic custody tests in EACH Python mode, and rejects8 +semantic variants on the intended assertions. With a complete Git checkout, +add --repo /path/to/repository to verify all8 actual historical source objects +and every required current source. C and D are pinned draft-branch sources, +not required to exist on default main; their exact historical bytes are checked. +The hosted workflow performs that full-repository check. A packet-only local +replay explicitly records upstream_verified_count=null, not fictitious custody. + +The code verifies finite identities, conservative constants and source guards. +It does not verify Gaussian analytic estimates, compactness or Kac--Rice. diff --git a/frontiers/local_cluster_tightness_20260929/RECONNAISSANCE.md b/frontiers/local_cluster_tightness_20260929/RECONNAISSANCE.md new file mode 100644 index 000000000..107fc068f --- /dev/null +++ b/frontiers/local_cluster_tightness_20260929/RECONNAISSANCE.md @@ -0,0 +1,22 @@ +# Focused reconnaissance — 29 September 2026 + +Consensus.search was actually called with Gaussian weighted Kac--Rice, field +norms, rare events and transverse reduction. It returned the exhausted monthly +30-search quota with October1 reset. No Consensus result is fabricated. + +Direct primary source: Armentano, Azais and Leon, arXiv:2304.07424v3, +https://arxiv.org/abs/2304.07424v3 and its HTML version. Abstract/version record +and the main-results introduction were inspected. The tool's exact-heading +searches for 'Theorem 7.1' and 'Remark 8' did not match the HTML numbering, so no +fresh full verification of those named statements is claimed. The actual formula +consumed is the landed project P Lemma5.1 with its canonical kernel and two-measure +proof. Gass--Stecconi arXiv:2305.17586 and publisher record were read at abstract +scope only; their ordinary moment-finiteness theorem is not a substitute for the +rare-intensity estimate N1. + +The companion is a targeted response to #158 author comment5900564419. The +subsequent comment5900634812 identified its already-written deterministic addendum +D atbfcc67dc, which was fully read and is credited. The alternate constants in +Section3 are a self-contained corroboration, not a separate discovery or review. +The existing #153 replica argument is also credited and pinned. This is not an +exhaustive novelty or priority audit, and no external theorem is silently imported. diff --git a/frontiers/local_cluster_tightness_20260929/RESULTS.json b/frontiers/local_cluster_tightness_20260929/RESULTS.json new file mode 100644 index 000000000..3c07c1a98 --- /dev/null +++ b/frontiers/local_cluster_tightness_20260929/RESULTS.json @@ -0,0 +1,9 @@ +{ + "tests_per_mode": 18, + "mathematical_tests": 12, + "custody_fixture_tests": 6, + "semantic_mutants_per_mode": 8, + "paired_outputs_identical": 9, + "scientific_effect": "NONE", + "analytic_acceptance": false +} diff --git a/frontiers/local_cluster_tightness_20260929/SOURCE_FILES.json b/frontiers/local_cluster_tightness_20260929/SOURCE_FILES.json new file mode 100644 index 000000000..caac28553 --- /dev/null +++ b/frontiers/local_cluster_tightness_20260929/SOURCE_FILES.json @@ -0,0 +1,66 @@ +{ + "schema": 1, + "scientific_effect": "NONE", + "files": [ + { + "path": "PROOF.md", + "bytes": 20344, + "sha256": "95f619ee5d9c1c1ac5e87397ce06de20fda164d528d6a90a16c4416322d9f269", + "git_blob": "adffa6916d0fb57fede0486b5eb3bc6afc127c07" + }, + { + "path": "README.md", + "bytes": 1966, + "sha256": "2cc45c898f14132d6b611a5972902c96fc34e23787e8347ff2a04eace3f10b82", + "git_blob": "4c84cbe0f69b3951eb93eb2a2828e619a7fd8ecb" + }, + { + "path": "RECONNAISSANCE.md", + "bytes": 1423, + "sha256": "7aeec094d74c9629943f86819e80c5f64f823d522268bfa567d5a43b7662f851", + "git_blob": "107fc068fe73cfb85196afbf4e5d1b7bf4e008d5" + }, + { + "path": "RESULTS.json", + "bytes": 215, + "sha256": "ee2471145f3d3926023b4179b8f16dd56c5210497e15e154cf2fc97b52c36394", + "git_blob": "3c07c1a98102d14ebcb097af3c584b5e3afdbf78" + }, + { + "path": "SOURCE_MAP.json", + "bytes": 3772, + "sha256": "4b976cfa3156c41211e01be177e281f37744a153dbc1ce5c09a7209545f29102", + "git_blob": "c5b3717b955102a1fc73eec6e60ec460436a4c04" + }, + { + "path": "controls.py", + "bytes": 2156, + "sha256": "0fc13e5f00f42784197be6191edd60a7ce8a3dcc8a649dbd88fe3af83ccddf02", + "git_blob": "e6e783368104bad617007b17867e104df16883ee" + }, + { + "path": "custody.py", + "bytes": 2060, + "sha256": "9830fa6684dda1efbced351952210ed46ae40703336acbd4ef8a89f02ae92421", + "git_blob": "24bb6abd86bb0973221f7cbe9a8055166ba40ae2" + }, + { + "path": "test_controls.py", + "bytes": 3411, + "sha256": "992f8af8029efddba79ab31efbf5dfab962e1bd31675927df80d68d966b95e4d", + "git_blob": "6caf8f76e9984a6d6529d9d15be09c82f65598e0" + }, + { + "path": "test_custody.py", + "bytes": 2215, + "sha256": "e167b439cff7480d1c109ef31168d7f7885f8c3270d53964035cc0466dc18ed4", + "git_blob": "c983be24eaa43dab08a95ab19477bf42f78cc7c1" + }, + { + "path": "verify.py", + "bytes": 4206, + "sha256": "977f1e2bfcb3fc727be4d6d3556275aa07052f3c160136ef5cd33fcc2a5b0c8e", + "git_blob": "71a65ccc047c322e62f1498150f48c24ff5565cd" + } + ] +} diff --git a/frontiers/local_cluster_tightness_20260929/SOURCE_MAP.json b/frontiers/local_cluster_tightness_20260929/SOURCE_MAP.json new file mode 100644 index 000000000..c5b3717b9 --- /dev/null +++ b/frontiers/local_cluster_tightness_20260929/SOURCE_MAP.json @@ -0,0 +1,87 @@ +{ + "scientific_effect": "NONE", + "sources": [ + { + "id": "P", + "path": "frontiers/c6_palm_route_20260929/PROOF.md", + "sha256": "aa37f16040ab9e05bb2e4e3f1d678367497e8dc2cf43eef197a4d6592c2f129b", + "git_blob": "89eb8adf08fe7afc2cab9662d3a9875c05ae5cc5", + "commit": "7a1cb09a9d58d179393e6d29146252f714b9c9bf", + "current_required": true, + "role": "Landed marked Kac-Rice, conditional norm moments and regional bounds.", + "bytes": 53364 + }, + { + "id": "L", + "path": "frontiers/window_multiplicity_laws_20260928/LOCAL_MULTIPLICITY.md", + "sha256": "e6272e8709835ca6290fecb7034fa84832dde08c3c4cc990a48b8019e89e7c8d", + "git_blob": "b5c18aac5529c5f975ee5bb056b304debafc6697", + "commit": "7a1cb09a9d58d179393e6d29146252f714b9c9bf", + "current_required": true, + "role": "Planar ten-jet rank and endpoint Taylor identities.", + "bytes": 13100 + }, + { + "id": "DL", + "path": "frontiers/d5_dimension_lift_20260929/PROOF.md", + "sha256": "6fb94b247e8e45bca9dc02f46670ac6029fb54e0ef906001efe48fe908549b80", + "git_blob": "9d82c707fdb17d3072a8930f26dabedf59e456fc", + "commit": "7a1cb09a9d58d179393e6d29146252f714b9c9bf", + "current_required": true, + "role": "Landed shell estimate and global first moment.", + "bytes": 53727 + }, + { + "id": "RM", + "path": "frontiers/remote_window_20260924/PROOF.md", + "sha256": "a332bae9bdc0106ce17047f7e0409cc3d94eb610a0c7b74ba5ba2d01a1620cb7", + "git_blob": "b383bfcc88ec4ad497dff01fb6640e429ba24a84", + "commit": "7a1cb09a9d58d179393e6d29146252f714b9c9bf", + "current_required": true, + "role": "Fixed-remote singleton kernel; coefficient includes height length k.", + "bytes": 18355 + }, + { + "id": "RC", + "path": "frontiers/remote_collision_20260928/PROOF.md", + "sha256": "b9b8b58fd8266db7ffe6537078003888ef138b445d3289ec5588f116af9050c2", + "git_blob": "7b48a88e2af54e759e89a8c8219573bb450a65ea", + "commit": "7a1cb09a9d58d179393e6d29146252f714b9c9bf", + "current_required": true, + "role": "Fixed-exclusion factorial O(r^5), including near-coincident witnesses.", + "bytes": 26002 + }, + { + "id": "C", + "path": "frontiers/planar_cubic_cluster_20260929/PROOF.md", + "sha256": "117e9299a71e6139270266889eb772ed97518e402d9af029bbdb67caf9d4a0f0", + "git_blob": "bb446d08db8a944537a743ad550b88c1c2ad5758", + "commit": "325c5ebdc2ca0165b483cddce8972ee2d0252c79", + "current_required": false, + "role": "AUTHOR-SIDE #158 theorem is an explicit premise only of conditional Sections6-7; not accepted here.", + "bytes": 19889 + }, + { + "id": "D", + "path": "frontiers/planar_cubic_cluster_20260929/DEEP_TRANSVERSE_EXCLUSION.md", + "sha256": "95c03e59262cb9607a21a296a6837932839dd47ec8e15e67bdfa46782adbcd5a", + "git_blob": "309a38cab16ef67dd909351f40a48e1d83ba2c28", + "commit": "bfcc67dc8957b3ed1fbb789e5a0305e98d7359c8", + "current_required": false, + "role": "Mandatory credit for the already-written deterministic graph mechanism; no independent-review credit." + }, + { + "id": "RCL", + "path": "frontiers/c6_rare_cluster_laws_20260929/PROOF.md", + "sha256": "c52a3cf197b5cf26071a8cc951e15ef3ac564b3d7453d41647f91af540a1b8eb", + "git_blob": "2ab625cedfc2e47575c4a7fa4853413418c532da", + "commit": "7a1cb09a9d58d179393e6d29146252f714b9c9bf", + "current_required": true, + "role": "Prior independent-replica probability argument; not claimed as new.", + "bytes": 11811 + } + ], + "conditional_source_C_review_status": "AUTHOR_SIDE_NOT_ACCEPTED_HERE", + "marked_fourier_157_consumed": false, + "local_packet_replay_verifies_upstream": false +} diff --git a/frontiers/local_cluster_tightness_20260929/controls.py b/frontiers/local_cluster_tightness_20260929/controls.py new file mode 100644 index 000000000..e6e783368 --- /dev/null +++ b/frontiers/local_cluster_tightness_20260929/controls.py @@ -0,0 +1,61 @@ +"""Exact finite identities for local rare-intensity tightness. No Gaussian checker.""" +from fractions import Fraction as F +from math import ceil, prod + +MUTANT=None + +def positive(*xs): + if any(F(x)<=0 for x in xs): raise ValueError('positive parameters required') + +def reduced_third(A,U,V,W,q): + A,U,V,W,q=map(F,(A,U,V,W,q)) + return A-(2 if MUTANT=='wrong-schur-derivative' else 3)*q*U+3*q*q*V-q**3*W + +def hermite_constant(r,k): + positive(r,k) + return (6 if MUTANT=='half-hermite' else 12)*F(k) + +def soft_threshold(R,r,K,k): + positive(R,r,K,k);R,r,K,k=map(F,(R,r,K,k)) + if R<1 or K=1 and K>=k required') + return 64*(R+1)**2*r*K**(1 if MUTANT=='linear-norm-threshold' else 2)/k + +def model_extra_x(k,lam,a): + positive(k,lam) + if not a: raise ValueError('nonzero mixed coefficient required') + return -12*F(k)*F(lam)/F(a)**2 + +def norm_tail(r,C,p,M): + positive(r,C,M) + if type(p) is not int or p<1: raise ValueError('positive integer moment required') + return F(C)*F(r)**(0 if MUTANT=='lose-rare-scale' else 3)/F(M)**p + +def mixed_power(): + return 4+1+3-(4 if MUTANT=='normalizer-twice' else 2) + +def boundary_volume(J,eps): + positive(J,eps) + return 2*F(eps)*(2*F(J))**3 + +def global_rates(a1,a2,remote): + positive(a1,a2,remote) + return {1:F(a1)+(0 if MUTANT=='omit-remote-singletons' else F(remote)),2:F(a2)} + +def factorial_coefficient(rates,p): + if type(p) is not int or p<1: raise ValueError('positive integer order required') + return sum((mass*prod(n-j for j in range(p)) for n,mass in rates.items() if n>=p),F(0)) + +def decomposition_error(middle,mixed): + if min(F(middle),F(mixed))<0: raise ValueError('nonnegative errors required') + return 3*((0 if MUTANT=='ignore-middle-region' else F(middle))+F(mixed)) + +def nonempty_double(rates): + return F(rates[2])/sum(rates.values()) + +def palm_excess(rates): + denom=sum(rates.values()) if MUTANT=='palm-equals-nonempty' else sum(n*p for n,p in rates.items()) + return sum(n*(n-1)*p for n,p in rates.items())/denom + +def absorption_order(loss,target,a): + positive(a) + return max(0,ceil((F(loss)+F(target))/F(a))) diff --git a/frontiers/local_cluster_tightness_20260929/custody.py b/frontiers/local_cluster_tightness_20260929/custody.py new file mode 100644 index 000000000..24bb6abd8 --- /dev/null +++ b/frontiers/local_cluster_tightness_20260929/custody.py @@ -0,0 +1,48 @@ +"""Fail-closed current/historical source byte checks; no analytic acceptance.""" +import hashlib,json,pathlib,re,subprocess + +def require(ok,message): + if not ok:raise ValueError(message) + +def identity(b): + return {'bytes':len(b),'sha256':hashlib.sha256(b).hexdigest(),'git_blob':hashlib.sha1(f'blob {len(b)}\0'.encode()+b).hexdigest()} + +def loads(s): + def pairs(items): + d={} + for k,v in items: + require(k not in d,'duplicate JSON key');d[k]=v + return d + return json.loads(s,object_pairs_hook=pairs,parse_constant=lambda _:(_ for _ in ()).throw(ValueError('nonfinite JSON'))) + +def safe_path(s): + p=pathlib.PurePosixPath(s) + require(not p.is_absolute() and str(p)==s and '..' not in p.parts and p.parts,'unsafe path') + return p + +def unique_paths(entries): + paths=[e['path'] for e in entries] + require(len(paths)==len(set(paths)),'duplicate source path') + for p in paths:safe_path(p) + +def read_checked(root,e): + root=pathlib.Path(root);rel=safe_path(e['path']) + require(not root.is_symlink(),'root symlink forbidden') + for i in range(1,len(rel.parts)+1): + require(not root.joinpath(*rel.parts[:i]).is_symlink(),'source symlink forbidden') + path=root.joinpath(*rel.parts);require(path.is_file(),'missing regular file') + b=path.read_bytes();actual=identity(b) + require(all(actual[k]==e[k] for k in actual if k in e),'source identity mismatch') + require('sha256' in e and 'git_blob' in e,'incomplete identity') + return b + +def upstream(repo,entries): + unique_paths(entries);repo=pathlib.Path(repo) + for e in entries: + require(re.fullmatch('[0-9a-f]{40}',e['commit']) is not None,'invalid pinned commit') + obj=e['commit']+':'+e['path'] + b=subprocess.check_output(['git','-C',str(repo),'show',obj],stderr=subprocess.PIPE,timeout=20) + actual=identity(b) + require(all(actual[k]==e[k] for k in actual if k in e),'historical source differs: '+e['id']) + if e.get('current_required',True):read_checked(repo,e) + return len(entries) diff --git a/frontiers/local_cluster_tightness_20260929/test_controls.py b/frontiers/local_cluster_tightness_20260929/test_controls.py new file mode 100644 index 000000000..6caf8f76e --- /dev/null +++ b/frontiers/local_cluster_tightness_20260929/test_controls.py @@ -0,0 +1,65 @@ +"""Exact scalar/finite-measure controls, not a Gaussian theorem checker.""" +from fractions import Fraction as F +from itertools import product +from math import prod +import unittest +import controls as m + +class Controls(unittest.TestCase): + def test_reduced_third_derivative(self): + for B,C,A,U,V,W in product([F(-2),F(1,3)], [F(-3),F(2)], [F(12)], [F(3)], [F(-2)], [F(5)]): + q=B/C; hp=-q + by_chain=A+U*hp-2*q*(U+V*hp)+q*q*(V+W*hp) + self.assertEqual(m.reduced_third(A,U,V,W,q),by_chain) + def test_hermite_integral_normalization(self): + for r,k in product([F(1,2),F(1,7)], [F(1,3),F(2)]): + h=r/2 + # Integral (h^2-x^2)*12k = 2*k*r^3. + self.assertEqual(m.hermite_constant(r,k)*F(4,3)*h**3,2*k*r**3) + def test_deep_constants_uniform(self): + for R,k,K,j in product([F(1),F(2),F(5)],[F(1,5),F(1)],[F(13),F(37)],[1,4,16]): + r=k/(2*(R+1)*K*j);lam=m.soft_threshold(R,r,K,k) + q=2*(R+1)*r*K/lam + lower=12*k-(R+1)*r*K-K*(3*q+3*q*q+q**3) + self.assertGreater(lower,10*k) + self.assertLessEqual((R+1)**2*K*r*r/lam,r/8) + self.assertGreaterEqual(lam,4*R*r*K) + def test_threshold_quadratic_norm(self): + self.assertEqual(m.soft_threshold(2,F(1,100),20,1),64*9*F(1,100)*400) + self.assertEqual(m.soft_threshold(2,F(1,100),40,1)/m.soft_threshold(2,F(1,100),20,1),4) + def test_explicit_graph_extra_zero(self): + # f=2kx^3-3kr^2*x/2-kr^3/2-lam*z^2/2 + a*(x^2-r^2/4)*z/2. + for k,lam,a in product([F(1),F(2)],[F(1),F(3)],[F(1),F(2)]): + r=F(1,10);x=m.model_extra_x(k,lam,a);z=a*(x*x-r*r/4)/(2*lam) + self.assertEqual(6*k*(x*x-r*r/4)+a*x*z,0) + self.assertEqual(-lam*z+a*(x*x-r*r/4)/2,0) + def test_rare_norm_tail_keeps_scale(self): + for r in [F(1,4),F(1,16)]: + self.assertEqual(m.norm_tail(r,7,3,5),7*r**3/F(125)) + def test_mixed_local_remote_ledger(self): + self.assertEqual(m.mixed_power(),6) + for r in [F(1,4),F(1,16)]: + self.assertEqual(r**4*r*r**3/r**2,r**m.mixed_power()) + def test_boundary_tube_volume(self): + self.assertEqual(m.boundary_volume(3,F(1,10)),F(1,5)*6**3) + def test_global_rates_and_factorials(self): + rates=m.global_rates(F(2,3),F(5,7),F(11,13)) + self.assertEqual(rates,{1:F(2,3)+F(11,13),2:F(5,7)}) + self.assertEqual(m.factorial_coefficient(rates,2),F(10,7)) + for q in range(3,8):self.assertEqual(m.factorial_coefficient(rates,q),0) + def test_missing_middle_is_not_automatic(self): + self.assertGreater(m.decomposition_error(F(1,10),0),0) + # For deterministic A=B=C=1, l1(delta_3-2delta_1)=3. + self.assertGreaterEqual(m.decomposition_error(1,1),3) + def test_nonempty_and_sizebiased_differ(self): + rates={1:F(3),2:F(2)} + self.assertEqual(m.nonempty_double(rates),F(2,5)) + self.assertEqual(m.palm_excess(rates),F(4,7)) + self.assertNotEqual(m.nonempty_double(rates),m.palm_excess(rates)) + def test_exponential_absorption_for_each_fixed_power(self): + # e^{-c/u^a} <= n! (u^a/c)^n; choose an integer n to absorb a fixed loss. + for loss,target,a in product(range(3,17),[2,5],[F(1,4),F(2,3),F(2)]): + n=m.absorption_order(loss,target,a) + self.assertGreaterEqual(a*n-loss,target) + +if __name__=='__main__': unittest.main() diff --git a/frontiers/local_cluster_tightness_20260929/test_custody.py b/frontiers/local_cluster_tightness_20260929/test_custody.py new file mode 100644 index 000000000..c983be24e --- /dev/null +++ b/frontiers/local_cluster_tightness_20260929/test_custody.py @@ -0,0 +1,37 @@ +"""Synthetic source-custody regressions; no upstream proof verification claim.""" +import hashlib,json,pathlib,tempfile,unittest +import custody as c + +class Custody(unittest.TestCase): + def setUp(self): + self.tmp=tempfile.TemporaryDirectory();self.addCleanup(self.tmp.cleanup) + self.root=pathlib.Path(self.tmp.name);(self.root/'sub').mkdir() + (self.root/'sub'/'proof.txt').write_bytes(b'proof\n') + self.entry={'path':'sub/proof.txt',**c.identity(b'proof\n')} + def test_valid_source(self): + self.assertEqual(c.read_checked(self.root,self.entry),b'proof\n') + def test_changed_or_missing(self): + (self.root/'sub'/'proof.txt').write_bytes(b'amended\n') + with self.assertRaises(ValueError):c.read_checked(self.root,self.entry) + (self.root/'sub'/'proof.txt').unlink() + with self.assertRaises((ValueError,FileNotFoundError)):c.read_checked(self.root,self.entry) + def test_three_identity_fields(self): + for field in ('bytes','sha256','git_blob'): + bad=dict(self.entry);bad[field]=0 if field=='bytes' else '0'*len(bad[field]) + with self.assertRaises(ValueError):c.read_checked(self.root,bad) + def test_unsafe_relative_path(self): + for path in ('../proof','/proof','sub/../proof','sub//proof.txt'): + bad=dict(self.entry,path=path) + with self.assertRaises(ValueError):c.read_checked(self.root,bad) + def test_file_and_parent_symlinks(self): + p=self.root/'sub'/'proof.txt';p.rename(self.root/'real');p.symlink_to(self.root/'real') + with self.assertRaises(ValueError):c.read_checked(self.root,self.entry) + p.unlink();(self.root/'sub').rmdir();(self.root/'real').unlink() + (self.root/'target').mkdir();(self.root/'target'/'proof.txt').write_bytes(b'proof\n') + (self.root/'sub').symlink_to(self.root/'target',target_is_directory=True) + with self.assertRaises(ValueError):c.read_checked(self.root,self.entry) + def test_duplicate_json_and_source_paths(self): + with self.assertRaises(ValueError):c.loads('{"a":1,"a":2}') + with self.assertRaises(ValueError):c.unique_paths([self.entry,self.entry]) + +if __name__=='__main__':unittest.main() diff --git a/frontiers/local_cluster_tightness_20260929/verify.py b/frontiers/local_cluster_tightness_20260929/verify.py new file mode 100644 index 000000000..71a65ccc0 --- /dev/null +++ b/frontiers/local_cluster_tightness_20260929/verify.py @@ -0,0 +1,64 @@ +"""Exact packet replay with optional real upstream Git verification.""" +import argparse,io,json,pathlib,subprocess,sys,unittest +import custody +ROOT=pathlib.Path(__file__).resolve().parent +MUTANTS={ + 'wrong-schur-derivative':'test_reduced_third_derivative', + 'half-hermite':'test_hermite_integral_normalization', + 'linear-norm-threshold':'test_threshold_quadratic_norm', + 'lose-rare-scale':'test_rare_norm_tail_keeps_scale', + 'normalizer-twice':'test_mixed_local_remote_ledger', + 'omit-remote-singletons':'test_global_rates_and_factorials', + 'ignore-middle-region':'test_missing_middle_is_not_automatic', + 'palm-equals-nonempty':'test_nonempty_and_sizebiased_differ', +} + +def source_ids(): + mp=ROOT/'SOURCE_FILES.json' + custody.require(not mp.is_symlink() and mp.is_file(),'regular manifest required') + entries=custody.loads(mp.read_text())['files'];custody.unique_paths(entries) + custody.require(sorted(x.name for x in ROOT.iterdir())==sorted([e['path'] for e in entries]+['SOURCE_FILES.json']),'packet membership differs') + for e in entries: + custody.require(pathlib.Path(e['path']).name==e['path'],'packet must be flat') + custody.read_checked(ROOT,e) + return {p.name:custody.identity(p.read_bytes()) for p in sorted(ROOT.iterdir())} + +def child(mutant): + import controls,test_controls,test_custody + controls.MUTANT=mutant + suite=unittest.TestSuite([unittest.defaultTestLoader.loadTestsFromModule(x) for x in (test_controls,test_custody)]) + result=unittest.TextTestRunner(stream=io.StringIO()).run(suite) + print(json.dumps({'tests':result.testsRun,'passed':result.wasSuccessful(), + 'failures':sorted(t.id().split('.')[-1] for t,_ in result.failures), + 'errors':sorted(t.id().split('.')[-1] for t,_ in result.errors)},sort_keys=True)) + return 0 if result.wasSuccessful() else 1 + +def replay(out,repo): + out=out.resolve();custody.require(not out.exists() and not out.is_relative_to(ROOT),'new external output required') + before=source_ids();count=custody.upstream(repo,custody.loads((ROOT/'SOURCE_MAP.json').read_text())['sources']) if repo else None + out.mkdir(parents=True);records={} + for case in ['baseline',*MUTANTS]: + pair=[] + for mode,flags in [('normal',[]),('optimized',['-O'])]: + cmd=[sys.executable,'-B',*flags,'-S',str(ROOT/'verify.py'),'--child'] + if case!='baseline':cmd+=['--mutant',case] + p=subprocess.run(cmd,capture_output=True,timeout=30) + (out/(case+'_'+mode+'.stdout')).write_bytes(p.stdout);(out/(case+'_'+mode+'.stderr')).write_bytes(p.stderr) + r=custody.loads(p.stdout.decode());custody.require(not p.stderr and not r['errors'] and r['tests']==18,'execution error') + if case=='baseline':custody.require(p.returncode==0 and r['passed'],'baseline failed') + else:custody.require(p.returncode==1 and not r['passed'] and MUTANTS[case] in r['failures'],'intended semantic failure missing') + pair.append(p.stdout) + custody.require(pair[0]==pair[1],'Python mode disagreement');records[case]=custody.loads(pair[0].decode()) + summary={'tests_per_mode':18,'mathematical_tests':12,'custody_fixture_tests':6,'semantic_mutants_per_mode':8, + 'paired_outputs_identical':9,'scientific_effect':'NONE','analytic_acceptance':False} + custody.require(summary==custody.loads((ROOT/'RESULTS.json').read_text()),'stored summary differs') + custody.require(before==source_ids(),'sources changed') + (out/'REPORT.json').write_text(json.dumps({**summary,'upstream_verified_count':count,'source_identities':before,'cases':records},sort_keys=True,indent=2)+'\n') + print(json.dumps(summary,sort_keys=True,indent=2));return 0 + +if __name__=='__main__': + p=argparse.ArgumentParser(description=__doc__);g=p.add_mutually_exclusive_group(required=True) + g.add_argument('--child',action='store_true');g.add_argument('--output',type=pathlib.Path) + p.add_argument('--mutant',choices=MUTANTS);p.add_argument('--repo',type=pathlib.Path) + a=p.parse_args();custody.require(a.child or a.mutant is None,'mutant needs child mode') + raise SystemExit(child(a.mutant) if a.child else replay(a.output,a.repo))