diff --git a/.github/workflows/replacement-bar-occurrence.yml b/.github/workflows/replacement-bar-occurrence.yml new file mode 100644 index 000000000..e77d6fa44 --- /dev/null +++ b/.github/workflows/replacement-bar-occurrence.yml @@ -0,0 +1,50 @@ +name: Replacement-bar occurrence exact controls +on: + pull_request: + paths: + - 'frontiers/replacement_bar_occurrence_20261001/**' + - 'frontiers/local_elder_geometry_20260930/PROOF.md' + - 'frontiers/planar_cubic_cluster_20260929/PROOF.md' + - 'imports/lifetime_parent_20260925/**' + - 'reviews/d1_section9_borel_repair_20260925/REPAIR.md' + - 'reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md' + - '.github/workflows/replacement-bar-occurrence.yml' + push: + branches: [main] + paths: + - 'frontiers/replacement_bar_occurrence_20261001/**' + - 'frontiers/local_elder_geometry_20260930/PROOF.md' + - 'frontiers/planar_cubic_cluster_20260929/PROOF.md' + - 'imports/lifetime_parent_20260925/**' + - 'reviews/d1_section9_borel_repair_20260925/REPAIR.md' + - 'reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md' + - '.github/workflows/replacement-bar-occurrence.yml' + workflow_dispatch: +permissions: + contents: read +concurrency: + group: replacement-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/replacement_bar_occurrence_20261001/test_exact.py -v + else + python3 -B -S frontiers/replacement_bar_occurrence_20261001/test_exact.py -v + fi diff --git a/frontiers/replacement_bar_occurrence_20261001/GLOBAL.md b/frontiers/replacement_bar_occurrence_20261001/GLOBAL.md new file mode 100644 index 000000000..e3e4a7ada --- /dev/null +++ b/frontiers/replacement_bar_occurrence_20261001/GLOBAL.md @@ -0,0 +1,376 @@ +# Isolation of a single selected maximum in the full-field coupling + +Object: OA-SELECTED-BAR-OCCURRENCE-GLOBAL-20261001-v1. +Author/coauthor: OpenAI/Codex `/root/c51_excess_feasibility`, under the +delegation of `/root` and Dylan Roy. Same-provider author-side mathematical +work; no independent-provider or organizational-independence credit. +Scientific effect NONE. This is an additive conditional proof candidate; +no imported hypothesis, acceptance, status, prize, premise, C8 conclusion, +or program closure is changed. + +## 1. Scope and exact source interfaces + +Use the fixed planar torus and exact covariance of [P] §1. The seven +retained source files [P], [CAP], [E1], [E2], [REC], [CUB], [ELDER] have the +same bytes as C50 `SOURCES.json`, pinned at Math commit +`044d42d5bd7f31df6f7e6b9034d6711e8fb7ee43`. They remain imported hypotheses, +read with [REC]'s W1/embedded-chart rule, [E1]'s congruence erratum, and +[E2]'s Section 9 replacement. No new analytic input is silently substituted. + +The specific interfaces used below are: + +* [P] §§2–3: strictly positive Fourier spectrum, smooth full-field version, + finite derivative-functional rank, and convergent averaged contact + functionals. Its §8 supplies the rank-plus-mesh proof method; the + full-contact-jet adaptation is proved explicitly below. +* [CUB] (C1)–(C13), (G6)–(G9): the exact cubic, nonsingular appended + ten-dimensional jet covariance, full-field regression coupling, global + C4 envelope, and fixed-disk rescaled C2 convergence. +* [ELDER] §4: the homogeneous cubic gradient has no nonzero zero off Delta; + the elementary calculation is repeated below. +* C50 `ROOTS.md` R1: finite all-root classification and the additional + all-root Hessian null set; these algebraic details are also displayed + below. Its R3 supplies the fixed-disk root-continuation argument. + +No cap-failure estimate, factorial count moment, spatial independence, or +multi-point Kac–Rice calculation is needed in this companion. The main +consumer separately retains [ELDER] S9 to exhaust its failure measure. + +Let `B_birth` and `K_gap` be C50's fixed positive-length compact intervals, +with `K_gap subset (0,infinity)`, and let `00}. + +Use C50's actual elder convention and exclusion of the essential class; +set N_h to zero off the Morse/distinct-value locus. Every selected maximum +has a distinct saddle within distance C0 h. This necessary condition is +the only feature of the selection rule used in this companion. + +## 2. Cubic notation and generic parameters + +Fix `b in R`, `k>0`, an oriented orthonormal frame, and +`theta=(s,a,beta,q)`. In its original Euclidean coordinates put + + P(X,Z)=2kX^3-3kX/2-k/2+sZ^2/2 + +(a/2)(X^2-1/4)Z+(beta/2)XZ^2+(q/6)Z^3, + M0=(-1/2,0), S0=(1/2,0), + u=X+aZ/(12k), + Bs=beta-a^2/(12k), + Ds=(q-a beta/(4k)+a^3/(72k^2))/2. + +The strict endpoint-typing condition is + + s < -|Bs|/2. (1) + +The leading homogeneous cubic is + + H3(X,Z)=2kX^3+(a/2)X^2 Z+(beta/2)XZ^2+(q/6)Z^3. + +After the displayed invertible shear, + + H3=2ku^3+(Bs/2)u Z^2+(Ds/3)Z^3. + +Retain C50's generic exclusions. In particular define + + Delta=12k Ds^2+Bs^3, + H=12k Ds^2+Bs^3-4Bs s^2, + Sigma=12k Ds^2+(s-Bs)^2(Bs+2s). + +Work outside `Delta=0`, `H=0`, `Sigma=0`, and `Ds=0`. The last two +exclusions are inherited for compatibility; only Delta and H are needed +for the isolation argument below. Each is a nonzero polynomial zero set +after clearing positive powers of k, hence is Lebesgue null at fixed k. + +For H, the exact polynomial numerator is + + U=12k beta-a^2, + V=72k^2 q-18ka beta+a^3, + H_poly=V^2+U^3-576k^2 U s^2, + H=H_poly/(1728k^3). + +The q² coefficient of H_poly is `5184k^4>0`. This is a genuine null +exclusion, not a quantitative estimate on neighborhoods of degeneracy. + +**Lemma 1 (finite nondegenerate cubic roots and one maximum).** Under (1) +and H!=0, P has at most four finite critical points, all nondegenerate, +and M0 is its only critical point with negative-definite Hessian. + +**Proof.** The two pins are critical. Every additional root has Z!=0 and +satisfies the conic and line + + 6k(u^2-1/4)+(Bs/2)Z^2=0, + s+Bs u+Ds Z=0. (2) + +When Bs and Ds are nonzero, elimination gives + + (12k Ds^2+Bs^3)u^2+2Bs^2 s u+Bs s^2-3k Ds^2=0. + +Its linear coefficient is nonzero because s<0, so the polynomial is not +identically zero and has at most two roots. Each determines Z. If Ds=0 +and Bs!=0, the line fixes u and the conic gives at most two Z. If Bs=0 +and Ds!=0, the conic fixes u=+/-1/2 and the line fixes Z. If both are +zero, s<0 excludes every extra root. Thus the total is at most four. + +At an extra root, the identities from (2) are + + det Hess P=-3k(Bs+4su), + H Z^2=3k(Bs+4su)^2. (3) + +The second follows by expanding `12k(Ds Z)^2` using the line and replacing +`Bs Z^2` by the conic. It involves no division by Bs or Ds. An extra +degenerate root therefore forces H=0. At the pins the determinants are +`3k(Bs-2s)` and `3k(Bs+2s)`; their axial entries are -6k and 6k. Condition +(1) makes M0 a strict maximum and S0 a saddle, both nondegenerate. + +Finally every polynomial of degree at most three has at most one critical +point with negative-definite Hessian. If p and q were two, set v=q-p. +Its Hessian is affine, so along their segment it is the convex combination +of two negative-definite matrices. Thus + + 0=(grad P(q)-grad P(p)).v + =integral_0^1 v^T Hess P(p+tv) v dt <0, + +a contradiction. Applying this to P proves the last assertion. QED. + +**Lemma 2 (homogeneous gradient coercivity).** If Delta!=0, there is c>0 +such that `|grad H3(x)|>=c|x|^2` in the original coordinates. + +**Proof.** In the sheared coordinates the equations for a homogeneous +critical direction are + + 6ku^2+(Bs/2)Z^2=0, + Z(Bs u+Ds Z)=0. + +A nonzero solution has Z!=0. If Bs=0 it exists exactly when Ds=0. If +Bs!=0, eliminate u to get `12k Ds^2+Bs^3=0`. Thus Delta!=0 excludes a +gradient zero on the unit circle. Compactness and homogeneity give the +bound there and at every radius. An invertible linear shear preserves the +bound up to a positive constant. QED. + +## 3. Global convergence of the fully conditioned fields + +For physical scale r, the exact six pins are at +`M_r=(-r/2,0)`, `S_r=(r/2,0)`, with values `b,b-kr^3` and zero gradients. +Append the physical midpoint jet + + J=(f_zz,f_xxz,f_xzz,f_zzz)=(rs,a,beta,q). + +Let f_r^theta be CUB (G6)'s full-field regression coupling, using one +unconditioned smooth field F: + + f_r^theta=F+Cov(F,V_r) Gamma_r^(-1)(t_r(theta)-V_r(F)), + V_r=(U_r,J), t_r=(v_r,rs,a,beta,q). (4) + +Here U_r is P §3's nonsingular six-component contact frame, v_r its exact +target, and Gamma_r the covariance of V_r. In particular all random-field +correlations and the prescribed endpoint pins are retained. + +**Lemma 3 (global contact limit).** For each fixed target and every +sequence r_i->0, this coupling satisfies, almost surely, + + f_ri^theta -> f_0^theta in C4(T_L^2), (5) + +where the limiting field has exactly the Gaussian law conditioned on the +full ten-component planar jet + + f(0)=b, grad f(0)=0, Hess f(0)=0, + (f_xxx,f_xxz,f_xzz,f_zzz)(0)=(12k,a,beta,q). (6) + +Also the rescaled fields converge to P in C2 on every fixed disk. + +**Proof.** P §3 expresses every U_r component as an evaluation or an +averaged derivative, including the apparently singular axial third +component. For every smooth F these converge to the corresponding contact +derivative. Together with J their limits are exactly all ten independent +jet entries through order three. Their covariance Gamma_0 is positive +definite by P §2 or CUB's full jet rank, and Gamma_r and its inverse +converge. The cross-covariance coefficient functions in (4) converge in +global C4 by the smooth Fourier covariance and its rapidly summable +derivatives. The targets converge to (6). Taking the limit term by term +in (4) proves (5), with its stated Gaussian regression law. In particular +the sequence has bounded global C4 norm pathwise. The rescaled C2 statement +is exactly CUB (G8); a countable exhaustion of disk radii gives it on +every fixed disk for the same sequence. QED. + +The limit's dependence on s disappears from (6), because rs->0. This does +not discard the s coordinate from the finite-r disintegration or the +cubic unfolding. + +## 4. Morse genericity off the forced contact point + +**Lemma 4 (conditional off-origin Morse property).** For every fixed +target (6), f_0^theta is almost surely Morse on `T_L^2 \ {0}`. + +**Proof.** At x!=0 and a unit vector v, consider the random vector + + Z(x,v)=(grad f_0^theta(x), Hess f_0^theta(x)v) in R^4. + +Its conditional covariance given (6) is positive definite. Otherwise a +nonzero linear combination of these four observations would equal a +linear combination of the ten contact observations in Gaussian L2. +By P §2's positive Fourier spectrum, the resulting distribution of +derivative evaluations annihilates every Fourier mode and hence is zero. +Its supports x and 0 are disjoint, so its part at x must be zero. +First derivatives and second derivatives are independent orders; the +second derivative part has polynomial symbol `(beta.xi)(v.xi)` and is +zero only when beta=0, since v!=0. The first derivative coefficients then +also vanish. This contradicts a nonzero four-component combination. + +On every compact set of x separated from 0, times the unit circle, the +covariance varies continuously and has a positive minimum eigenvalue. +The corresponding four-dimensional Gaussian densities are uniformly +bounded. The conditional mean does not affect the upper density bound. + +For completeness apply P §8's mesh argument here. The parameter manifold +(x,v) has dimension three. Cover it by finitely many bounded charts and +an epsilon mesh with O(epsilon^-3) sites. On the event that the C1 norm of +Z is at most M, a zero implies some mesh value has size O(M epsilon). +The density bound and the union bound give probability at most +`C M^4 epsilon`, which tends to zero. First fix M, then let M increase; +the random C1 norm is finite by smoothness. Countably exhaust the torus +away from 0. With probability one there is no simultaneous zero of +`grad f_0(x)` and `Hess f_0(x)v` anywhere with x!=0, which is the assertion. +QED. + +This lemma is proved for fixed conditional targets, as are the source +couplings. Fubini permits its use under the absolutely continuous theta +integral. No common probability-one event over uncountably many targets +is required. Distinct remote critical values are not needed for isolation. + +## 5. A deterministic bridge across intermediate spatial scales + +**Lemma 5 (root-free annulus).** Consider a fixed sequence f_i with scales +r_i->0 in the coupling of Lemma 3 and a generic theta satisfying Lemmas +1–2. On any realization for which (5) and the rescaled convergence hold, +there are fixed R and delta>0 such that, for all sufficiently large i, + + grad f_i(x) != 0 whenever Rr_i <= |x| <= delta. (7) + +The constants can depend on theta and the realization; delta is chosen +inside an embedded torus chart. + +**Proof.** The sequence has a finite global C4 bound by (5). Add and +subtract the second-order Taylor expansions of the gradient at the exact +two pins +/-r_i e_x/2. Since both endpoint gradients vanish, + + grad f_i(0)=O(r_i^2), + Hess f_i(0)e_x=O(r_i^2). + +The remainders are O(r_i^3) under the C4 bound. The other independent +Hessian entry is exactly `f_i,zz(0)=r_i s`, hence +`||Hess f_i(0)||=O(r_i)`. By (5)–(6) the third derivatives at zero +converge to those of H3. Taylor's formula for the gradient therefore +gives constants C0 such that + + |grad f_i(x)-grad H3(x)| + <= C r_i^2+C r_i |x|+epsilon_i |x|^2+C |x|^3 (8) + +on a fixed sufficiently small coordinate disk. All derivatives and norms +in (8) are in the original Euclidean coordinates. The r_i² and r_i terms +are consequences of the exact pins, not merely of global convergence. + +Let c>0 be Lemma 2's constant. First choose R so that +`C/R²+C/R0 so that `C delta= (c/4)|x|^2 >0. + +This proves (7). The choices are R first, then delta, then i. The +argument does not apply fixed-disk convergence on a growing disk. QED. + +The limit itself has an isolated origin: (6) and Taylor's formula give +`grad f_0(x)=grad H3(x)+O(|x|^3)`. After decreasing delta if necessary, +there is no critical point of f_0 in `0<|x|<=delta`. + +## 6. Eventual absence of a second selected maximum + +**Theorem G (full-field isolation).** Fix b,k,frame and a typed generic +theta as in §2. Under the full conditional coupling (4), for every fixed +`t>0` and every sequence r_i->0, almost surely + + N_(r_i/t)(f_ri^theta) <= 1 + +for all sufficiently large i. In particular this holds for each fixed +`t in [c0,C0]` used in the radial integral. The conclusion also holds for +any selection of maxima that requires a distinct saddle within distance +`C0 r_i/t`; actual elder and mark restrictions only reduce that population. + +**Proof.** Work on the probability-one event of Lemmas 3–4. Choose R and +delta as in Lemma 5, increasing R to contain all cubic roots. By Lemma 1 +all roots are nondegenerate. On the fixed rescaled disk B_R, choose small +disjoint neighborhoods of those roots. C2 convergence supplies exactly +one continued critical root in each, with unchanged inertia. For explicit +uniqueness, fix the inverse limiting Hessian in each neighborhood; the +Newton map `x -> x-H_root^(-1) grad g_i(x)` is a contraction on a +sufficiently small closed ball and maps it into itself. On the compact +complement of these balls the cubic gradient has a positive floor, so +there are no further roots. Thus the physical disk B_(Rr_i) contains +exactly the continued cubic roots. It has exactly one maximum, the exact +pin M_i, whose value remains b. This is all-root stability, including +roots outside the original height window. + +By Lemma 5 no additional critical root occurs between that disk and the +fixed disk B_delta. The limiting origin is isolated, and by Lemma 4 all +other critical points of f_0 are nondegenerate. There are finitely many: +they lie in a compact set away from the origin, and any accumulating +critical sequence would have a critical limit, contradicting local root +isolation at a nondegenerate point. + +Choose small disjoint balls around the finitely many remote critical +points, all separated from B_(delta/2). Global C2 convergence in Lemma 3 +and the same contraction argument give exactly one continued root in +each ball, with unchanged inertia. On the compact remainder outside +B_(delta/2), the limiting gradient has a positive minimum, so it has no +other continued or newly formed roots. Together with the annulus and +inner-disk control, this accounts for all critical points of f_i. + +The finitely many remote roots have a positive minimum pairwise distance, +and a positive minimum distance from the origin. These separations +persist with a smaller positive lower bound for their continuations; +the local roots converge to the origin in physical coordinates. Since +`C0 r_i/t -> 0`, for all sufficiently large i every distinct critical +pair at distance at most `C0 r_i/t` lies wholly in the local cubic +cluster. That cluster has only the one maximum M_i. + +Every selected maximum counted in N_(r_i/t) has a distinct saddle within +this distance. Hence at most M_i can be selected. The restrictions on +birth, positive normalized gap, finiteness, and the actual global elder +partner cannot create another candidate maximum. This proves the claim +on the Morse/distinct-value locus. Off that locus the prescribed N=0 +extension also satisfies the claim. QED. + +## 7. What this supplies to the occurrence consumer + +For fixed outer b,k,frame,t and almost every typed theta, Theorem G proves +pathwise eventual vanishing of the bounded whole-field event + + 1{N_(r_i/t)(f_ri^theta)>=2}. + +On the typed complement and its boundary, the consumer uses ELDER S11's +zero limiting typed determinant weight. The exceptional cubic sets are +null under the absolutely continuous physical midpoint-jet density. +No convergence or uniform rate is asserted on those exceptional sets. + +The consumer can therefore insert the bounded event into C50's exact +once-per-bar identity and the original physical-jet disintegration. Its +reciprocal denominator is at least one on an eligible pair; the event's +eventual vanishing means no cutoff-boundary convergence of that denominator +is needed. The source C4 determinant envelope handles compact theta boxes, +and the unchanged S9 actual-failure tail handles their complement. + +This companion does not itself assert a factorial moment estimate, +quantitative rate, uniformity as marks or L escape their fixed ranges, +Poisson behavior, infinite-volume theorem, higher-dimensional law, or +unrestricted short-bar exhaustion. The full-torus conclusion here is +restricted to the conditional coupling and the stated eventual bounded +event. All seven source hypotheses remain retained exactly. diff --git a/frontiers/replacement_bar_occurrence_20261001/PROOF.md b/frontiers/replacement_bar_occurrence_20261001/PROOF.md new file mode 100644 index 000000000..724258d33 --- /dev/null +++ b/frontiers/replacement_bar_occurrence_20261001/PROOF.md @@ -0,0 +1,273 @@ +# From replacement-bar intensity to field occurrence + +Object: OA-REPLACEMENT-BAR-OCCURRENCE-20261001-v1. +Authors: OpenAI/Codex root and c51_excess_feasibility, under Dylan Roy's delegation. +This is a conditional mathematical candidate. It does not change scientific status. +The source identities, including the unmerged C50 candidate, are fixed in SOURCES.json. + +## 1. Fix the observable before taking a limit + +Use exactly [U50, §1]: the centered unit-variance periodized Gaussian field on the +fixed planar torus T_L²; ordinary finite superlevel H0 bars indexed by their +birth maximum M; the actual global elder death saddle S_*(M); and exclusion of +the essential global maximum. Fix L, a positive-length compact birth interval +B, a positive-length compact K=[k_-,k_+] with k_->0, and 00, +and N_h=|A_h(f)|. Work on the almost-sure Morse/distinct-value locus and assign +these quantities zero off it. Define V_h(M) exactly as in [U50]: + + V_h(M)=(f(M), disp(M,S_*(M))/h, (f(M)-f(S_*(M)))/h³). + +The displacement uses U50's fixed half-open shortest torus chart. There is no +additional cutoff on the actual partner. Distinct maxima give distinct finite +bars. N_h does not count multiple rejected saddles for the same maximum. + +Write C_U(Phi) for the coefficient in [U50, (3)], and +lambda_U=L² C_U(1)>0. U50 supplies, for bounded continuous Phi, + + E sum_(M in A_h) Phi(V_h(M)) + = L² C_U(Phi) h^5 + o(h^5). (O1) + +This is a first moment. The new question is whether the same leading mass is +carried by fields with exactly one selected bar. + +## 2. The conditional theorem and exact dependencies + +**Theorem O.** Conditional on [U50] and its retained analytic interfaces, +for the population just fixed, + + E[N_h 1{N_h>=2}] = o(h^5), (O2) + E[(N_h-1)_+] = o(h^5). (O3) + +Consequently, + + P(N_h>0) = lambda_U h^5 + o(h^5), (O4) + Law(N_h | N_h>0) -> delta_1 in total variation. (O5) + +For the experiment which first conditions a field on N_h>0 and then chooses +one of its N_h selected bars uniformly, its mark has the weak limit + + E[ N_h^-1 sum_(M in A_h) Phi(V_h(M)) | N_h>0 ] + -> C_U(Phi)/C_U(1). (O6) + +The zero-denominator expression is defined as zero when N_h=0 before +conditioning. Formula (O6) is for every bounded continuous Phi on +B x R² x [0,infinity). It does not assert total-variation convergence of marks. + +[U50] is the exact source at published head +b5bf02879a5645da9a69d9944dee610e6bb14bf6: PROOF.md and ROOTS.md are reproduced +unchanged under sources/c50 with their original source map. At candidate +creation this parent is reviewed but still an unmerged draft; consuming it is +an explicit mathematical hypothesis, not an integration or acceptance claim. + +Its seven underlying sources [P,CAP,E1,E2,REC,CUB,ELDER] are pinned at +044d42d5bd7f31df6f7e6b9034d6711e8fb7ee43. In particular: + +- [P, §§2–4]: positive Fourier spectrum, distinct finite derivative rank, + nonsingular averaged contact frame, and global smooth Gaussian regression. + The rank and mesh argument in §8 is used at a new full-contact conditioning; + GLOBAL.md gives that argument explicitly instead of quoting pinned Morse + genericity at a different conditioning. +- [CUB, G6–G10]: the full-field ten-jet coupling, physical midpoint-jet density, + compact-sector C4 envelope and r^4 determinant scaling. +- [ELDER, S9 in §8.3 and the subsequent determinant bounds]: exhaustion of the + *actual weighted failure* outside compact soft-jet boxes. This is not inferred + from finiteness of a limiting integral. +- [U50, §§4–7]: Borel reciprocal counting, exact pair/radial formula, its outer + uniform bound and the positive finite coefficient. [U50 ROOTS] supplies the + generic all-root nondegeneracy and finite cubic critical set. + +GLOBAL.md proves the new deterministic and Gaussian mechanism needed for (O2). +The rest of this note inserts it into the existing weighted integral and +derives the probability consequences. No new joint Kac–Rice integrability, +independence between regions, factorial bound or inverse Hessian moment is +assumed. Existing analytic-source hypotheses and acceptance boundaries remain. + +## 3. The pathwise mechanism + +Fix b,k,u and an interior t in [c0,C0]; put r=t h. In the full-field coupling, +fix generic theta=(s,a,beta,q) on the typed sector. GLOBAL.md proves: + + N_(r/t)(f_r^theta) <= 1 eventually as r -> 0, (O7) + +almost surely under that coupling. The threshold may depend on the complete +coupled sample, theta, t and the outer parameters; no uniform random threshold +is claimed or needed. + +There are three essential pieces. The contact-conditioned limit is almost +surely Morse away from its single forced degenerate point. A quantitative +Taylor bound excludes critical points at every intermediate distance +Rr <= |x| <= delta, with R finite and delta positive selected for that sample. +Inside Rr all critical points continue from the generic pinned cubic, whose +affine Hessian permits at most one strict local maximum. Outside delta, +ordinary C2 structural stability gives finitely many separated critical roots; +for small h none can form a pair at distance at most C0 h. + +Thus all admissible rejected pairs must use the single possible local +maximum. This is a statement about the actual field's critical points, not a +statement that a cubic describes the field on a growing disk. No candidate +cutoff-boundary convergence is needed for (O7): the global number of maxima +capable of having a nearby saddle is at most one before applying B or K or the +actual-elder rejection mark. + +## 4. A bounded whole-field mark, not a second-moment calculation + +For each fixed h, define H_h(f)=1{N_h(f)>=2}. The root-chart/Borel argument in +[U50, §4] makes N_h and H_h Borel on the full field space. Every Morse function +on the compact torus has finitely many critical points, so these are ordinary +finite sums. Extend by zero off the stated Borel generic locus. + +The exact pathwise reciprocal identity remains valid with this global mark: + + N_h H_h + = sum_(admissible rejected (M,S), M finite) + H_h / D_h(M). (O8) + +The denominator is positive on every summand and 1/D_h<=1. Multiplication by +H_h preserves the full-field Borel property. It does not introduce a second +selected maximum into the Kac–Rice pin list and it assumes no independent +relationship between H_h and the pinned field. + +Set J_h=L^-2 E[N_h H_h]. The same marked finite-measure identity [E2] used by +U50 gives, with its ordered maximum/saddle convention, + + J_h = integral_(B x K x S1) integral_(c0 h)^(C0 h) + r A_r E_QrW[1_F 1_finite H_h / D_h(M)] + dr db dk d sigma(u). (O9) + +Here F is failure of the sampled saddle to be the actual elder partner, +A_r=12 pi_r Z_r/r², and QrW is the *original* weighted pin law W_r/Z_r. +There is no extra full-field probability normalization. The midpoint +integration is L² and has already been divided out in J_h. The integrand is +bounded by the one-failure integrand, so its finiteness follows from the same +compact-parameter bounds as U50. + +## 5. Vanishing within the physical weighted disintegration + +Keep t,b,k,u fixed. Define the bounded mark under the pin law + + G_r=1_F 1_finite H_(r/t) / D_(r/t)(M), 0<=G_r<=1_F. + +Disintegrate the physical midpoint jet as in [CUB G10; U50 (9)] with +f_zz(0)=r s. On a compact theta box, the rescaled marked density is + + (r²/Z_r) h_r(rs,a,beta,q) + E[(W_r(f_r^theta)/r^4) G_r(f_r^theta)]. (O10) + +This expression already includes the Jacobian r of f_zz=r s. It has precisely +the scaling r^-3 times r times r^4 divided by Z_r. No second normalizer has +been inserted. + +For almost every theta in the typed sector, (O7) makes H_(r/t)=0 eventually, +so the expectation's integrand tends to zero pathwise. On the complement of +the limiting typed sector, the determinant-times-type factor W_r/r^4 tends +to zero; no global selector or count convergence is required there. The +typed boundary is null, and the same determinant continuity suffices there +as well. The generic null sets and the conditional almost-sure sets are +handled by Fubini at each fixed parameter, or along each sequence r_i->0; +there is no common-null-set assertion over all uncountably many pins. + +The source envelope on each compact theta box is + + W_r/r^4 <= C_T (1+||F||_C4)^4, + +with finite expectation, locally bounded h_r and bounded r²/Z_r. +Since 0<=G_r<=1, dominated convergence in theta and the coupled field gives +zero for the limit of the integral of (O10) on that box. + +The actual complement is bounded, without changing the conditioning, by + + r^-3 QrW(F, ||Theta_r||>T). + +[ELDER S9], the same retained tail input used by U50, gives + + lim_(T->infinity) limsup_(r->0) + r^-3 QrW(F, ||Theta_r||>T) = 0. + +First take r->0 on a fixed box, then exhaust the boxes. Consequently + + r^-3 E_QrW G_r -> 0. (O11) + +This is where integrability of the multi-occurrence statistic is obtained. +Almost-sure stabilization by itself would not justify taking an expectation +of the unbounded count N_h; (O8) and the bounded mark supply the needed +weighted domination. + +## 6. Radial integration and count-to-probability conversion + +Substitute r=t h into (O9): + + h^-5 J_h = integral_(B x K x S1) integral_c0^C0 + t^4 A_(th) [(th)^-3 E_Q(th)W G_(th)] + dt db dk d sigma(u). (O12) + +The full count has order h^5 because r dr times the weighted failure factor +r³ is r^4 dr. The new bounded mark tends to zero at that same scale. +[P (7.8)] gives r^-3 E G_r <= C on these fixed compact outer parameters; +A_r is uniformly bounded by the source radial interface. Since t is in a +fixed compact interval away from zero, this is an integrable common +majorant. Dominated convergence using (O11) proves J_h=o(h^5), hence (O2). +The fixed factor L² converts per-volume intensity back to a probability +coefficient; it cannot be omitted. + +For every finite nonnegative integer n, + + 0 <= (n-1)_+ <= n 1{n>=2}, + n - 1{n>0} = (n-1)_+, + 2 1{n>=2} <= n 1{n>=2}. (O13) + +Taking expectations proves (O3) and, using (O1) with Phi=1, + + P(N_h>0)=E N_h-E[(N_h-1)_+] + =lambda_U h^5+o(h^5). + +For small enough h this probability is positive. The total-variation +distance in (O5) is exactly P(N_h>=2 | N_h>0), which is bounded by +E[N_h 1{N_h>=2}]/(2P(N_h>0)) and tends to zero. + +For bounded Phi, let S_h(Phi)=sum_(M in A_h) Phi(V_h(M)). Pointwise, + + |S_h(Phi)-1{N_h>0} S_h(Phi)/N_h| + <= ||Phi||_infinity (N_h-1)_+. (O14) + +Thus the unconditional numerator of the field-first sampling experiment is +L² C_U(Phi)h^5+o(h^5), by (O1), (O3) and (O14). +Dividing by (O4) proves (O6). It is now legitimate to use the normalized +intensity law for this different sampling experiment because the excess +has been bounded, rather than because the laws were declared identical. + +## 7. What this closes and what remains outside it + +The estimate closes the C50 next-step excess-multiplicity obligation for its +precisely defined compact-band population, conditional on the named sources. +It identifies the first occurrence coefficient lambda_U=L² C_U(1) and the +corresponding weak field-conditioned mark law. + +It does not prove a bound for E[N_h(N_h-1)], convergence of higher moments, +a quantitative o(h^5) rate, independence of occurrences, a Poisson process, +all birth/gap marks, growing torus volume, infinite volume, higher dimensions, +or a broader universal persistence theorem. In particular probability +convergence to a single selected bar does not control arbitrarily rare +fields with large counts at second-moment scale. Ordinary short-bar leading +laws, C8 and formal statement alignment are not promoted by this result. + +Limit order: fix L,B,K,c0,C0 and each outer t,b,k,u; on each fixed compact jet +box use the full-field coupling as r->0, with sample-dependent R and delta +only inside its pointwise proof; remove the jet box with the original +weighted-failure tail; integrate the fixed outer parameters. No exchange +of a growing-domain limit with the coupling is used. + +The finite exact controls check count identities, normalization, a Taylor +annulus budget and algebraic counterexamples to omitted hypotheses. They +do not establish off-contact Morse genericity, the coupling, or weighted +tail exhaustion. Those analytic steps are in GLOBAL.md, §§4–6 above and +the explicitly retained sources, and require substantive nonauthor review. + diff --git a/frontiers/replacement_bar_occurrence_20261001/README.md b/frontiers/replacement_bar_occurrence_20261001/README.md new file mode 100644 index 000000000..2e0a5b0b7 --- /dev/null +++ b/frontiers/replacement_bar_occurrence_20261001/README.md @@ -0,0 +1,46 @@ +# When a rare replacement bar occurs + +The previous result counts selected finite persistence bars in expectation. +This companion asks a different question: how often does a random field +contain such a bar, and what does that bar look like after conditioning on +its occurrence? + +For the same fixed planar torus and fixed compact birth, gap and shrinking +distance bands, the conditional theorem proves + + E[N_h 1{N_h >= 2}] = o(h^5), + P(N_h > 0) = L² C_U(1) h^5 + o(h^5). + +Here N_h counts distinct selected actual bars, and C_U is the previously +identified, multiplicity-corrected coefficient. Given occurrence, there is +one selected bar with probability tending to one. Its weak mark law is +C_U(Phi)/C_U(1). + +[Theorem and probability argument](PROOF.md) · +[Global isolation proof](GLOBAL.md) · [Exact source identities](SOURCES.json) + +The key new step uses the whole conditioned field. A generic local cubic +has only one strict maximum; a Taylor estimate excludes roots at intermediate +scales; the limiting field is Morse away from the forced contact, so its +remote critical points remain separated. A bounded event indicator then +fits into the existing weighted counting identity without assuming a +second moment or spatial independence. + +The result is conditional on C50 and its seven retained analytic interfaces. +C50's consumed proof, root analysis and original source map are copied +unchanged under sources/c50 at their published commit because its separate +integration is pending. This is not acceptance of those premises. + +No quantitative rate, factorial-moment bound, Poisson law, all-mark +exhaustion, higher-dimensional theorem, infinite-volume limit or complete +research-program proof is claimed. + +From the repository root, run the finite exact controls: + + python3 -B -S frontiers/replacement_bar_occurrence_20261001/test_exact.py -v + python3 -B -O -S frontiers/replacement_bar_occurrence_20261001/test_exact.py -v + +They check source identity, rational count/probability distinctions, marked +sampling, and finite algebraic controls. They do not prove the continuum +Gaussian or limiting arguments. The proof requires substantive source review. + diff --git a/frontiers/replacement_bar_occurrence_20261001/SOURCES.json b/frontiers/replacement_bar_occurrence_20261001/SOURCES.json new file mode 100644 index 000000000..d764eb81f --- /dev/null +++ b/frontiers/replacement_bar_occurrence_20261001/SOURCES.json @@ -0,0 +1,98 @@ +{ + "version": 1, + "source_commit": "Mixed exact historical commits; each entry is authoritative for its bytes", + "scientific_effect": "NONE", + "status": "C51 conditional consumer; C50 is an unmerged reviewed candidate at the pinned head, not a new premise acceptance", + "sources": [ + { + "key": "P", + "path": "imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md", + "commit": "044d42d5bd7f31df6f7e6b9034d6711e8fb7ee43", + "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": "044d42d5bd7f31df6f7e6b9034d6711e8fb7ee43", + "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": "044d42d5bd7f31df6f7e6b9034d6711e8fb7ee43", + "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": "044d42d5bd7f31df6f7e6b9034d6711e8fb7ee43", + "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": "044d42d5bd7f31df6f7e6b9034d6711e8fb7ee43", + "blob": "75da2597971510f843f8d90c743950cb8c177342", + "bytes": 23312, + "sha256": "451b9d7ffee072a73fc904cab891b6693e3f233808b89df10cce1b57036b65da", + "local_path": "reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md" + }, + { + "key": "CUB", + "path": "frontiers/planar_cubic_cluster_20260929/PROOF.md", + "commit": "044d42d5bd7f31df6f7e6b9034d6711e8fb7ee43", + "blob": "bb446d08db8a944537a743ad550b88c1c2ad5758", + "bytes": 19889, + "sha256": "117e9299a71e6139270266889eb772ed97518e402d9af029bbdb67caf9d4a0f0", + "local_path": "frontiers/planar_cubic_cluster_20260929/PROOF.md" + }, + { + "key": "ELDER", + "path": "frontiers/local_elder_geometry_20260930/PROOF.md", + "commit": "044d42d5bd7f31df6f7e6b9034d6711e8fb7ee43", + "blob": "ef2aa57959ea9f721bbf2316ce94cf616c1c9113", + "bytes": 39722, + "sha256": "f68038be79b46124b0f9b31205aa6e3682b34b6f5ef81f4a5697ae81f07cc46b", + "local_path": "frontiers/local_elder_geometry_20260930/PROOF.md" + }, + { + "key": "U50", + "path": "frontiers/unique_replacement_bar_intensity_20261001/PROOF.md", + "local_path": "frontiers/replacement_bar_occurrence_20261001/sources/c50/PROOF.md", + "commit": "b5bf02879a5645da9a69d9944dee610e6bb14bf6", + "blob": "9c79a672f5d81e04972032b2f1faf185f4664fa5", + "bytes": 17545, + "sha256": "ba1901cbb4bac037befb21d648172ac3ba04aa370f5377a2919c0da988572552" + }, + { + "key": "U50_ROOTS", + "path": "frontiers/unique_replacement_bar_intensity_20261001/ROOTS.md", + "local_path": "frontiers/replacement_bar_occurrence_20261001/sources/c50/ROOTS.md", + "commit": "b5bf02879a5645da9a69d9944dee610e6bb14bf6", + "blob": "b27d9ac8111c83f4967d837eee22057583c41eae", + "bytes": 11969, + "sha256": "29e79b60a382b95cc0fa2375b82845a5558942cf81a2a836262e7479f9d570e6" + }, + { + "key": "U50_MAP", + "path": "frontiers/unique_replacement_bar_intensity_20261001/SOURCES.json", + "local_path": "frontiers/replacement_bar_occurrence_20261001/sources/c50/SOURCES.json", + "commit": "b5bf02879a5645da9a69d9944dee610e6bb14bf6", + "blob": "210dcacaac4eb0f4a2480959fdf342daff5d41cc", + "bytes": 2515, + "sha256": "e3cdd6858125ca0e65e6f72d7032bc7267390a7b628f494f9d768035d5a8e91a" + } + ] +} diff --git a/frontiers/replacement_bar_occurrence_20261001/check_exact.py b/frontiers/replacement_bar_occurrence_20261001/check_exact.py new file mode 100644 index 000000000..6e8f263e2 --- /dev/null +++ b/frontiers/replacement_bar_occurrence_20261001/check_exact.py @@ -0,0 +1,107 @@ +"""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 = '320f64d3feebd7a694fc33458cf5c768207411525e89df6fd786f75990f5fc60' + + +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/replacement_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) == 10, 'ten exact sources required') + require(len({e['key'] for e in entries}) == 10, 'duplicate source key') + for entry in entries: + verify_entry(root, entry) + return len(entries) + + +def rational(value): + require(type(value) in (int, F), 'exact rational required') + return F(value) + + +def count_statistics(law): + require(isinstance(law, dict) and bool(law), 'nonempty count law required') + require(all(type(n) is int and n >= 0 for n in law), 'invalid count') + probs = {n:rational(p) for n,p in law.items()} + require(all(p >= 0 for p in probs.values()) and sum(probs.values()) == 1, + 'invalid probability law') + return tuple(sum((p*term(n) for n,p in probs.items()),F(0)) for term in + (lambda n:n,lambda n:int(n>0),lambda n:max(n-1,0), + lambda n:n if n>=2 else 0,lambda n:n*(n-1))) + + +def mark_statistics(fields): + total=average=event=excess=F(0) + probability=F(0) + for raw_probability,raw_marks in fields: + p=rational(raw_probability) + require(p>=0, 'negative probability') + marks=tuple(rational(v) for v in raw_marks) + n=len(marks) + probability += p + total += p*sum(marks,F(0)) + if n: + average += p*sum(marks,F(0))/n + event += p + excess += p*(n-1) + require(probability==1, 'invalid probability law') + return total,average,event,excess + + +def cubic_hessian(parameters, point): + k,s,a,beta,q=map(rational,parameters) + x,z=map(rational,point) + return 12*k*x+a*z, a*x+beta*z, s+beta*x+q*z + + +def annulus_budget(C,R,delta,epsilon): + C,R,delta,epsilon=map(rational,(C,R,delta,epsilon)) + require(C>=0 and R>0 and delta>=0 and epsilon>=0, 'invalid annulus parameters') + return C/R**2+C/R+epsilon+C*delta + + +if __name__=='__main__': + print(json.dumps({'verified_sources':verify_sources(), + 'scope':'Exact source identity only; run test_exact.py for finite controls.'})) diff --git a/frontiers/replacement_bar_occurrence_20261001/sources/c50/PROOF.md b/frontiers/replacement_bar_occurrence_20261001/sources/c50/PROOF.md new file mode 100644 index 000000000..9c79a672f --- /dev/null +++ b/frontiers/replacement_bar_occurrence_20261001/sources/c50/PROOF.md @@ -0,0 +1,207 @@ +# Counting rare replacement bars once + +Object: OA-UNIQUE-REPLACEMENT-BAR-20261001-v1. Authors: OpenAI/Codex `/root`, `/root/c50_multiplicity_feasibility` and its `boundary_nullity` contributor, under Dylan Roy's delegation. This is an additive source-bound mathematical candidate. Technical review, imported-source acceptance, organizational independence and scientific acceptance remain separate. Scientific effect NONE; no controlling status is changed. + +## 1. Model, population and the result + +Fix the planar torus `T_L^2`, with `L>0` fixed before all limits, and the centered unit-variance Gaussian field with covariance + +``` +K_L(z) = sum_(n in Z^2) exp(-|z+Ln|^2/2) + / sum_(n in Z^2) exp(-|Ln|^2/2). +``` + +Use ordinary superlevel H0 persistence with distinct critical values: a finite bar is indexed by its birth maximum `M`, its actual global elder partner `S_*(M)`, and death `d_f(M)=f(S_*(M))`. Its length is `f(M)-d_f(M)>0`. Exclude the essential global-maximum class. Work on the almost-sure Morse/distinct-value locus supplied by [P,REC]; give all expressions value zero off it. No Morse–Smale, branch-adjacency or separatrix convention is substituted. + +Fix intervals `B=[b_-,b_+]`, `K=[k_-,k_+]` of positive lengths, with `00` small enough that `C_0 h R`, set + +``` +I_h(Phi) = L^-2 E sum_(finite maxima M, + f(M) in B, D_h(M)>0) Phi(V_h(M)). (1) +``` + +Each actual bar is counted once. The shrinking selection concerns its rejected candidates; it does not impose the same distance/gap cutoff on its actual partner. This is an expected intensity, not sampling a field conditioned on having such a bar. + +The source quantities used in the theorem are defined in §3. Conditional on the exact imported interfaces in §2, the new conclusion is + +``` +h^-5 I_h(Phi) -> C_U(Phi), (2) + +C_U(Phi) = integral_(B x K x S^1) integral_(c_0)^(C_0) + t^4 A_0(b,k,u) + integral [ Phi(b, t R_u(Y_*-M_0), -t^3 h_*) / D_(t,k)(theta) ] + d mu_fail^(b,k,u)(theta) + dt db dk d sigma(u). (3) +``` + +`sigma` is ordinary arc measure, and `R_u=(u,Ju)` is the oriented orthonormal frame, with J the counterclockwise quarter-turn. The limit integrates only the nonempty typed failure sector. On its generic part, `D_(t,k)` is either 1 or 2. With `C_R` the corresponding coefficient obtained by replacing `1/D` by 1, + +``` +0 < C_R/2 <= C_U(1) <= C_R < infinity. (4) +``` + +Thus `I_h(1) ~ C_U(1) h^5`. Formula (3) identifies a finite weak limiting measure in the displayed birth/location/lifetime variables. It does not assert a density in any of those variables, a rate, finite-h moment convergence, all-mark exhaustion, an infinite-volume limit, or a higher-dimensional result. + +## 2. Exact dependencies and division of work + +All consumed files are pinned at Math commit `044d42d5bd7f31df6f7e6b9034d6711e8fb7ee43` in SOURCES.json. The historical source headers are preserved, not treated as current acceptance decisions. + +- **[P]** `imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md`: §§1–5 for model, regression and one full normalizer; (7.8) for the uniform compact-parameter failure bound; §§8–10 for the global selector, marked pair measure and `r A_r dr` ledger. Read with **[CAP]** the marked cylinder-cap proof, **[E1]** the congruence erratum, **[E2]** the full-field Borel Section9 repair, and **[REC]** the reconciliation's W1/embedded-chart and source-reading rules. These are retained analytic inputs, not re-proved or newly accepted by this paper. +- **[CUB]** `frontiers/planar_cubic_cluster_20260929/PROOF.md`: the pinned cubic and conic/line equations; nonsingular joint jet and positive Gaussian density; conditional full-field coupling (G6)–(G9), physical jet disintegration (G10), positive finite failure-sector integrals (G11)–(G13). +- **[ELDER]** `frontiers/local_elder_geometry_20260930/PROOF.md`: Theorem E for exact eventual actual partner identification, §§8.3–8.6 for the original weighted failure-tail exhaustion and determinant envelope, §8.8 for partner marks, §9 for the already supplied compact parameter bounds. In particular its §9 explicitly does not count each replacement bar once. + +The new work is the reciprocal counting identity and its legitimate whole-field mark, all-root and cutoff stability in ROOTS.md, their insertion into the existing disintegration, and radial integration. The endpoint law in `frontiers/short_bar_endpoint_law_20261001/PROOF.md` is contextual: it already concerns ordinary finite bars, but its leading law does not identify this h^5 rare subset. Neither it nor a factorial-moment bound substitutes for the present count correction. + +## 3. Cubic notation and the exact multiplicity + +Under the six endpoint pins use midpoint coordinates with `M_0=(-1/2,0)`, `S_0=(1/2,0)`, heights `0,-k`. The limiting cubic is + +``` +P_theta(X,Z)=2kX^3-3kX/2-k/2+sZ^2/2 + +(a/2)(X^2-1/4)Z+(beta/2)XZ^2+(q/6)Z^3, +theta=(s,a,beta,q), +B_s=beta-a^2/(12k), +D_s=(q-a beta/(4k)+a^3/(72k^2))/2, +T_k={s<-|B_s|/2}. +``` + +The subscripts on `B_s,D_s` distinguish shear coefficients from the birth interval and multiplicity. Let `n(theta)` count the extra critical points in `-k0, let `Y_*` be the unique highest window saddle and `h_*=P_theta(Y_*)`. Then `-k0} ds da d beta dq, +A_r=12 pi_r Z_r/r^2, A_0=12 pi_0 z_0. (6) +``` + +Here h_0 is the full midpoint-jet Gaussian density conditional on contact `(b,0,0,12k,0,0)`; its correlations, b,k,u,L dependence are retained. In (3), `A_0 dmu_fail=12 pi_0 w h_0 1_{T_k,n>0}dtheta`: exactly one z_0 cancels. There is no extra pin density, factor 1/2, GOE replacement or adjacency normalization. + +## 4. Exact once-per-bar identity and measurability + +A Morse function on a compact torus has finitely many critical points. For each eligible finite maximum M, the summand `Phi(V_h(M))` is independent of which rejected candidate S is used to represent it. Therefore, pathwise, + +``` +sum_(finite M, f(M) in B, D_h(M)>0) Phi(V_h(M)) + = sum_(admissible rejected (M,S), M finite) + Phi(V_h(M))/D_h(M). (7) +``` + +There are D_h(M) equal terms on the right for that maximum. This identity works for signed bounded Phi; there is no independence assumption about different candidates. Essential maxima appear on neither side. + +The marked Kac–Rice use of (7) is legitimate. Around any C2 Morse function on the compact torus, its finitely many critical roots have continuous local charts, their inertia is constant, and the remaining compact set has a gradient floor. A sufficiently small C2 neighborhood has exactly these roots. The separable C2 function space admits a countable subcover of these neighborhoods. On each neighborhood, distance, heights and normalized positive-distance gaps of each pair are continuous. The global elder death is Borel by [P,E2]; finiteness and partner inequality are Borel. Consequently each finite root sum defining D_h and the actual-partner mark is Borel. Overlapping root enumerations give identical counts. Extending by zero off the Borel Morse/distinct-value locus gives a whole-field Borel mark. With the zero-denominator convention, its absolute value in (7) is bounded by `||Phi||_infinity`. + +Apply [E2]'s equality of finite measures on compact pair domains separated from the diagonal, then its height disintegration and [P]'s exact radial ledger. For each fixed h the radial band is separated from zero; its expected pair count is finite by the uniform bound on A_r. Translation invariance turns the midpoint integral into L²; hence the per-volume identity is + +``` +I_h(Phi)= integral_(B x K x S^1) integral_(c_0 h)^(C_0 h) + r A_r E_QrW[1_F 1_finite Phi(V_h(M))/D_h(M)] + dr db dk d sigma(u), (8) +``` + +where F is failure of the sampled saddle to be the actual global partner. The same full `W_r/Z_r` is used in (6) and (8). Signed tests follow by subtraction of their nonnegative parts. No unordered pair multiplicity is introduced: maximum/saddle roles order the pair, and u records its directed separation. + +## 5. Joint multiplicity stability at fixed outer parameters + +Put r=th. For almost every `(t,k,theta)` under Lebesgue measure with t,k in their intervals, ROOTS.md proves: + +1. Every finite cubic critical point is nondegenerate outside an explicit nonzero-polynomial null set. The actual candidates lie in the fixed scaled disk `|Y-M_0|<=C_0/t<=C_0/c_0`; all roots in an enlarged fixed disk continue, and the compact complement has a gradient floor. Thus there are no unaccounted roots inside the admissibility band. This is fixed-disk C2 stability, not a growing-domain assertion. +2. The boundaries `t|Y-M_0|=c_0,C_0` are null by integrating t. The normalized-gap endpoint boundaries are null by positive simultaneous scaling of `(k,s,a,beta,q)`: roots stay fixed and each positive normalized gap scales strictly. The integrated joint jet measure is absolutely continuous in those variables. The conclusion is joint almost-everywhere stability; no assertion at every fixed k is required. +3. On the failure sector, [ELDER] gives the eventual actual partner among the continued roots. Its exclusion in D_h therefore stabilizes jointly with all cutoff memberships. In particular `D_(r/t)(M)->D_(t,k)(theta)` (eventually equality of integers), and the actual scaled mark tends to `(b,t R_u(Y_*-M_0),-t^3 h_*)`. + +The retained null sets include the source Sigma_k, Delta_k, D_s=0 and the all-root Hessian discriminant in ROOTS.md. They are excluded only under absolutely continuous integration. A zero-probability exact degeneracy has not been used to assert a quantitative near-degeneracy rate. Such a rate is unnecessary for bounded marked convergence with the source envelope. + +## 6. Weighted disintegration and actual-failure exhaustion + +Fix a generic `(t,k)` and b,u. Use the full-field regression coupling [CUB G6] on an ambient compact theta box. It preserves the six pins and satisfies C2 convergence on every fixed disk and the C4 moment envelope. On the generic typed domain, the previous section and [ELDER E] give pointwise convergence of the bounded multiplier + +``` +G_r = 1_F 1_finite Phi(V_(r/t)(M))/D_(r/t)(M) + -> 1_{n>0} Phi(b,t R_u(Y_*-M_0),-t^3 h_*)/D_(t,k). +``` + +On the typed complement no selector convergence is needed: the limiting typed determinant weight is zero. On its boundary the same follows from continuity of determinant times inertia, as in [ELDER S11]. The physical midpoint change `f_zz(0)=rs` has Jacobian r, so the rescaled marked integral has density + +``` +(r^2/Z_r) h_r(rs,a,beta,q) E[(W_r/r^4) G_r]. (9) +``` + +This is `r^-3 * r * r^4 / Z_r`, not an extra Palm renormalization. The envelope `W_r/r^4 <= C_T(1+||F_0||_C4)^4` from [ELDER S12], bounded local densities, and the normalizer floor dominate (9). Compact-box dominated convergence gives the desired limit with the reciprocal mark. Weak convergence of the old location/death marginal alone would not justify this discontinuous root-count mark; (9) supplies the new argument. + +Now exhaust theta boxes. The omitted actual contribution is at most + +``` +||Phi||_infinity r^-3 Q_r^W(F,||Theta_r||>T), +``` + +which vanishes in the iterated limit by [ELDER S9]. The limit tail is bounded by `||Phi||_infinity mu_fail(||theta||>T)`, which vanishes by [CUB G13]. This proves + +``` +r^-3 E_QrW G_r -> integral Phi(b,t R_u(Y_*-M_0),-t^3 h_*) + /D_(t,k) dmu_fail. (10) +``` + +The essential class and any out-of-chart actual partner have no limiting contribution: they disappear on every generic compact coupled sector by [ELDER E], and the same actual-failure exhaustion controls their remainder. They were included until this bound, not removed by a presumed local/global equivalence. + +The sequence formulation of the source coupling suffices: prove (10) along each sequence r decreasing to zero, with exceptional null sets handled under the corresponding integrals. No common probability-one event over uncountably many pins or parameters is asserted. + +## 7. Radial limit, coefficient, and what changes + +Substitute r=th in (8). Exactly, + +``` +h^-5 I_h(Phi)= integral_(B x K x S^1) integral_(c_0)^(C_0) + t^4 A_(th) [(th)^-3 E_Q(th)W G_(th)] dt db dk d sigma(u). (11) +``` + +The exponent ledger is the parent's `r dr` times the rare-failure factor `r^3`, hence `r^4 dr=h^5 t^4 dt`. The bounded reciprocal introduces no power and no singular denominator. It corrects counting rather than changing the rare-event order. + +By [P (7.8)], `|r^-3 E G_r|<=C ||Phi||_infinity` uniformly on these compact b,k,u ranges for sufficiently small r. By [P (10.3)], A_r has a common finite bound and converges to A_0. Since t lies in a compact interval bounded away from zero, the right side of (11) has an integrable common majorant. Joint boundary nullity plus Fubini permits (10) for almost every outer t,k, and dominated convergence proves (2)–(3). The limit order is: fix L,B,K,c_0,C_0; compact-box coupling limit r→0 at fixed t; exhaust theta boxes using S9/G13; integrate fixed outer variables using the common source bound. No limit L→infinity or K→(0,infinity) is taken. + +For Phi=1, the coefficient without reciprocal is + +``` +C_R=((C_0^5-c_0^5)/5) + integral_(B x K x S^1) A_0(b,k,u)(alpha_1+alpha_2) db dk d sigma(u). +``` + +It is finite and positive by the imported bounds and positive failure-sector density. Since `1/2<=1/D<=1` almost everywhere on that sector, (4) follows. The coefficient is an identified Gaussian/angular integral; no numerical enclosure is supplied. In general the reciprocal depends on t,k and the full cubic, so multiplying C_R by an arbitrary constant (for example 1/2) is not justified. ROOTS.md supplies exact open-set fixtures with D=1 and D=2 for one fixed choice of bands, demonstrating that both multiplicities can matter. + +This closes, conditional on the explicitly retained analytic interfaces, the compact-band unique-count consumer left open by [ELDER §9]. It does not close all shrinking-witness, occurrence-conditioned or per-field cluster questions. In particular the limit describes intensity-weighted selected bars; dividing by its total mass gives that limiting intensity-normalized mark law, not the law of a bar sampled uniformly after conditioning a random field to contain one. + +## 8. Review and falsification targets + +Review A: pathwise identity and Borel full-field mark; Review B: ROOTS all-root and null-boundary proofs; Review C: physical disintegration, failure exhaustion, outer domination and normalization. A fresh nonauthor review must bind exact files and consumed source slices; no same-author calculation counts as peer review. + +Useful falsifiers include a generic admissible cubic with an uncounted extra critical root; a non-null membership boundary under the actual integrated measure; a finite bar counted with weights summing differently from one; a near-layer tail escaping the source S9 bound; or a second normalizer/pin-density inserted in (8)–(11). The supplied exact script checks finite algebra and count fixtures, with deliberately wrong alternatives. It does not prove the continuum coupling, imported cap theorem, or domination. Those are analytic obligations of this proof and its named dependencies. diff --git a/frontiers/replacement_bar_occurrence_20261001/sources/c50/ROOTS.md b/frontiers/replacement_bar_occurrence_20261001/sources/c50/ROOTS.md new file mode 100644 index 000000000..b27d9ac81 --- /dev/null +++ b/frontiers/replacement_bar_occurrence_20261001/sources/c50/ROOTS.md @@ -0,0 +1,292 @@ +# All-root stability and null membership boundaries + +Object: OA-UNIQUE-REPLACEMENT-BAR-ROOTS-20261001-v1. +Authors: OpenAI/Codex root and delegated coauthor +`/root/c50_multiplicity_feasibility`; the latter's child +`boundary_nullity` independently derived the scaling-nullity and algebraic +exclusion arguments. This is disclosed author-side work, not independent review. +Scientific effect: NONE. This additive consumer does not change a source proof, +review verdict, status, graph, prize, or premise. + +The exact source cut is Math- `044d42d5bd7f31df6f7e6b9034d6711e8fb7ee43`. +We consume [CUB](../planar_cubic_cluster_20260929/PROOF.md), blob +`bb446d08db8a944537a743ad550b88c1c2ad5758`, equations (C1)--(C13), +and [ELDER](../local_elder_geometry_20260930/PROOF.md), blob +`ef2aa57959ea9f721bbf2316ce94cf616c1c9113`, Theorem E and its unique-position +conclusion. Their dispositions are retained; the following lemmas are new +deterministic and measure-theoretic consumer steps. In particular, CUB's +window-only Lemma S is NOT used as an all-root stability assertion. + +## R1. Explicit all-root exclusion + +Use distinct notation for the distance band `00`, `theta=(s,a,beta,q)`, let + +```text +P(X,Z)=2kX^3-3kX/2-k/2+(s/2)Z^2 + +(a/2)(X^2-1/4)Z+(beta/2)XZ^2+(q/6)Z^3, +M0=(-1/2,0), S0=(1/2,0), +u=X+aZ/(12k), B_s=beta-a^2/(12k), +D_s=(q-a beta/(4k)+a^3/(72k^2))/2. +``` + +Assume strict endpoint typing `s<-|B_s|/2`. Besides the two pins, every +critical point satisfies + +```text +Q=6k(u^2-1/4)+(B_s/2)Z^2=0, +s+B_s u+D_s Z=0, Z!=0. (R1.1) +``` + +There are at most two such points anywhere in the plane. For `B_s,D_s!=0` +elimination gives + +```text +(12k D_s^2+B_s^3)u^2+2B_s^2 s u+B_s s^2-3k D_s^2=0. (R1.2) +``` + +This polynomial cannot vanish identically: its linear coefficient is nonzero +because `B_s!=0` and `s<0`. Each root determines one `Z`. If `D_s=0,B_s!=0`, +the line determines `u=-s/B_s`, and `Q` gives at most two `Z`. If `B_s=0,D_s!=0`, +`Q` determines `u=+/-1/2`, and the line determines `Z=-s/D_s`. If `B_s=D_s=0`, +the strict inequality `s<0` rules out every extra point. + +At every extra critical point, CUB (C8) gives + +```text +det Hess P=-3k(B_s+4su). +``` + +Put + +```text +H=12k D_s^2+B_s^3-4B_s s^2. +``` + +Multiplying the two equations in (R1.1) gives the identity + +```text +H Z^2=3k(B_s+4su)^2. (R1.3) +``` + +For an explicit verification, substitute `D_s Z=-s-B_s u` in `12k D_s^2 Z^2` +and substitute `B_s Z^2=-12k(u^2-1/4)` in the remaining two terms of +`HZ^2`; the sum is `3k(B_s+4su)^2`. This involves no division by `B_s` or +`D_s` and includes their zero cases. Since `Z!=0`, a degenerate extra root +forces `H=0`. The pins have determinants `3k(B_s-2s)` and `3k(B_s+2s)`, +both nonzero under strict typing. Thus outside `H=0`, EVERY finite +critical point of the cubic is nondegenerate, including points below `-k`. + +This additional exclusion is a genuine null algebraic set. Define + +```text +U=12k beta-a^2, +V=72k^2 q-18ka beta+a^3, +H_poly=V^2+U^3-576k^2 U s^2. +``` + +Then `H=H_poly/(1728k^3)`. At fixed `k>0`, the `q^2` coefficient +of `H_poly` is `5184k^4>0`, so it is a nonzero polynomial in `theta`. +Its zero set is Lebesgue null for each fixed `k`, and also for the +integrated `dk dtheta` measure. No numerical probe is used for this fact. + +Retain the source exclusions + +```text +Sigma=12k D_s^2+(s-B_s)^2(B_s+2s), +Delta=12k D_s^2+B_s^3, +D_s=0. +``` + +They respectively support window stability, ELDER's global escape argument, +and a unique limiting partner position. They are nonzero polynomial zero +sets after clearing positive `k` denominators. The new `H=0` exclusion +does not replace them. On strict typing outside this finite union, +the cubic has at most four critical points, all nondegenerate; on failure +ELDER selects a unique highest window saddle `Y_*`. + +## R2. Null membership boundaries under the integrated measure + +Fix a compact positive gap interval `K=[k_-,k_+]` with +`00`, `P(Y)<0`, and +`P(Y)^2=q0^2 (|Y-M0|^2)^3`. Projection gives a semialgebraic set. + +It is null for `dk dtheta` on the typed domain. Set `eta=theta/k`. +The map `(k,eta)->(k,k eta)` is a smooth bijection for `k>0`, with +absolute Jacobian `k^4`. Because all coefficients scale together, + +```text +P_(k,k eta)=k P_(1,eta). +``` + +Thus all root locations remain fixed on each positive scaling ray, while +each gap ratio is multiplied by `k`. Strict typing is also preserved: +`B_s(k,k eta)=k B_s(1,eta)` and `s=k eta_s`. For fixed typed `eta`, R1's +root finiteness shows that (R2.1) permits at most one positive `k` per +root. Its `k`-section is therefore finite. Fubini in `(k,eta)`, followed +by the Jacobian `k^4`, proves nullity. This proof includes all roots +below `-k`; no window restriction was imposed. + +For the radius boundaries, fix `(k,theta)` with its finite root set. +For any root `Y!=M0`, either equality + +```text +t |Y-M0|=c_0 or C_0 +``` + +permits at most one value of `t` for each endpoint. Fubini proves that +their union is null for `dt dk dtheta`, in particular when +`t in [c_0,C_0]`. The endpoints of the `t` and `k` integration +intervals themselves are null. + +All these nullities persist under any measure absolutely continuous +with respect to `dt dk dtheta`, and after appending other parameters +with absolutely continuous measures. This includes the integrated +Gaussian failure measure used in PROOF.md: CUB supplies a nonsingular +ten-dimensional contact-jet covariance, hence an actual Gaussian +density `h_0(0,a,beta,q)`; multiplying it by a determinant weight, +an indicator, `z_0^(-1)`, or the outer candidate density preserves +absolute continuity. No independence between coefficients is required. + +The gap-boundary assertion is deliberately integrated in `k`. At the +fixed slice `k=q0`, the pinned saddle itself has gap ratio `q0` for +every `theta`. It would be false to declare all fixed-`k` boundary +slices null. Fubini provides good `(k,t)` slices for almost every +outer integration parameter, which is exactly what the consumer uses. + +## R3. Stability of all admissible roots and of the rejected count + +Fix typed `(k,theta,t)` outside the exclusions of R1 and membership +boundaries of R2, with `t in (c_0,C_0)` and `k in (k_-,k_+)`. +Suppose `g_i` are normalized local functions from ELDER Theorem E, +retaining the exact two pins, their gradients and values `0,-k`, +and converging to `P` in `C^2` on every fixed disk. Their physical +scales are `r_i->0`; put `h_i=r_i/t`. Assume the actual global +fields are Morse with distinct critical values, as in the source. + +Every saddle admissible for the physical `h_i` distance band belongs +in scaled coordinates to the fixed disk + +```text +|Y-M0|<=C_0/t<=C_0/c_0. (R3.1) +``` + +Choose a larger fixed disk with root-free boundary, possible because +R1 gives only finitely many roots in the whole plane. Choose disjoint +small balls around each root inside that disk. All their Hessians +are nonsingular by R1. On each ball, fix the inverse Hessian at the +limiting root. By reducing the ball and the `C^2` error, the map +`x -> x-H_root^(-1) grad g_i(x)` is a contraction carrying the ball +into itself. It gives exactly one continued root there. The continued +root converges to the limiting one and has the same Hessian inertia. +On the compact complement of these balls, `|grad P|` has a positive +minimum. `C^1` convergence therefore excludes every additional root +there. Roots outside the larger disk cannot be candidates by (R3.1). +This proves complete root control in the band; no in-window count +lemma, growth of the disk with `i`, or unproved global Morse property +of the cubic is used. + +The continuations retain their distance and gap membership because +the inequalities have strict limiting margins, by R2. The denominator +in a gap ratio is bounded away from zero at any admissible root; +the only zero-distance root is the exact maximum pin, whose inertia +is stable and which cannot become a saddle. The height restriction +`P(Y)<0` adds no unhandled boundary: a root at height zero has gap +ratio zero and cannot enter `K`, whose lower endpoint is positive. + +If `n(theta)>0`, ELDER Theorem E and `D_s!=0` give that the actual +global partner is eventually the continuation of `Y_*`; the global +bar is eventually finite. Hence removing the actual partner from +the finite candidate list also stabilizes. Define + +```text +mathcal D_(t,k)(theta)=#{saddles Y: + P(Y)<0, Y!=Y_*, + c_0<=t|Y-M0|<=C_0, + -P(Y)/|Y-M0|^3 in K}. +``` + +Then the actual physical rejected-candidate count at scale `h_i` +is eventually exactly `mathcal D_(t,k)(theta)`. On `n=0`, ELDER +instead says that the failure indicator is eventually zero; the +consumer's failure-weighted reciprocal mark is therefore eventually +zero regardless of any other rejected candidates. + +On `n>0`, the pinned saddle is admissible and rejected because +its distance is one, its gap ratio is `k`, and its height is `-k`. +Thus `mathcal D_(t,k)>=1`. There are at most two extra roots, and one of +them is the actual partner `Y_*`. Only the pinned saddle and at most +one other extra root can remain as rejected saddles. Consequently + +```text +mathcal D_(t,k)(theta) in {1,2} (R3.2) +``` + +on the limiting failure population. This bound concerns the cubic +limit, not an asserted deterministic upper bound on all finite-scale +Gaussian configurations. + +## R4. Exact finite checks and their limits + +`check_exact.py` uses only standard-library rational arithmetic and +explicit conditional guards, so its checks remain active under +`python -O`. It verifies gradients, heights, Hessian determinants, +typing, all exclusion values being nonzero, and exact distance/gap +membership with strict boundary margins, without computing floating-point +square roots. It also verifies the seven entries of SOURCES.json against +repository-contained canonical paths, rejects symlink path components, +and checks byte lengths, SHA-256 digests and Git blob identities. An +executed wrong-digest probe must be rejected. These byte checks bind +inputs; they do not validate their mathematical content. + +The original two-window fixture is + +```text +k=1,a=0,beta=-3,s=-21/10,q=3/5, +Y1=(-5/8,3/4), P(Y1)=-23/320, det Hess=-27/4, +Y2=(-5/6,-4/3), P(Y2)=-13/45, det Hess=-12. +``` + +For band `[1/2,2]`, gap range `[1/10,2]`, and `t=1`, the count is +two; at `t=8/5` it is one. Both extras are in `(-1,0)`, so this +fixture alone does NOT detect omission of candidates below the pin. + +A separate below-window fixture supplies that control: + +```text +k=1,a=0,beta=-3,s=-39/16,q=3/2, +Y1=(-5/8,3/4), P(Y1)=-53/512, det Hess=-297/32, +Y2=(-37/24,-35/12), P(Y2)=-11125/4608,det Hess=-1155/32. +``` + +Here `P(Y2)<-1`, the pin determinants are `45/8,-189/8`, and +`Y1` is the unique highest window saddle. For band `[1/2,4]`, +gap range `[1/100,2]`, and `t=1`, both `S0` and `Y2` are rejected +admissible candidates: + +```text +|Y2-M0|^2=5525/576, +(-P(Y2)/|Y2-M0|^3)^2=71289/10793861. +``` + +The full count is two; the incorrect count restricted to the +original height window plus `S0` is one. A third fixture uses a +nonzero shear and catches use of sheared distances. Further controls +catch inclusion of the actual partner, omission of reciprocal +multiplicity, and retaining a root after a radius-boundary crossing. + +These are finite arithmetic checks of proof fixtures. They do not +prove continuum root stability, nullity, Kac--Rice measurability, +Palm integrability, dominated convergence, or any scientific status. diff --git a/frontiers/replacement_bar_occurrence_20261001/sources/c50/SOURCES.json b/frontiers/replacement_bar_occurrence_20261001/sources/c50/SOURCES.json new file mode 100644 index 000000000..210dcacaa --- /dev/null +++ b/frontiers/replacement_bar_occurrence_20261001/sources/c50/SOURCES.json @@ -0,0 +1,64 @@ +{ + "version": 1, + "source_commit": "044d42d5bd7f31df6f7e6b9034d6711e8fb7ee43", + "scientific_effect": "NONE", + "status": "Exact identities; analytic interfaces retained, not newly accepted", + "sources": [ + { + "key": "P", + "path": "imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md", + "commit": "044d42d5bd7f31df6f7e6b9034d6711e8fb7ee43", + "blob": "dfed3b8d318a3ab1950957f393307733a4bef3f2", + "bytes": 40261, + "sha256": "9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7" + }, + { + "key": "CAP", + "path": "imports/lifetime_parent_20260925/MARKED_CYLINDER_CAP_PROOF.md", + "commit": "044d42d5bd7f31df6f7e6b9034d6711e8fb7ee43", + "blob": "0633aca3c2a2882b0de4399da0a75d64c2e6b2e1", + "bytes": 15160, + "sha256": "0bf922b9203c29088b12388807aa0e2ecd020485eb0f6e919679841b5b2636fc" + }, + { + "key": "E1", + "path": "imports/lifetime_parent_20260925/ERRATUM_CONGRUENCE.md", + "commit": "044d42d5bd7f31df6f7e6b9034d6711e8fb7ee43", + "blob": "213594d6ca6a86fb938110f4d166d9ce275a02d0", + "bytes": 1782, + "sha256": "bad7ef609c4ad8c41ad6af562c1b6807921e19a9d556ed793ad1a0db6e202028" + }, + { + "key": "E2", + "path": "reviews/d1_section9_borel_repair_20260925/REPAIR.md", + "commit": "044d42d5bd7f31df6f7e6b9034d6711e8fb7ee43", + "blob": "fe9b9ce4999908bb3814b500ee2d0ceb0c6f704a", + "bytes": 9062, + "sha256": "845abf9f9c99d672c2a10a887b5a2e7206a3d2de3d876f35f75ff6e2dc13e62f" + }, + { + "key": "REC", + "path": "reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md", + "commit": "044d42d5bd7f31df6f7e6b9034d6711e8fb7ee43", + "blob": "75da2597971510f843f8d90c743950cb8c177342", + "bytes": 23312, + "sha256": "451b9d7ffee072a73fc904cab891b6693e3f233808b89df10cce1b57036b65da" + }, + { + "key": "CUB", + "path": "frontiers/planar_cubic_cluster_20260929/PROOF.md", + "commit": "044d42d5bd7f31df6f7e6b9034d6711e8fb7ee43", + "blob": "bb446d08db8a944537a743ad550b88c1c2ad5758", + "bytes": 19889, + "sha256": "117e9299a71e6139270266889eb772ed97518e402d9af029bbdb67caf9d4a0f0" + }, + { + "key": "ELDER", + "path": "frontiers/local_elder_geometry_20260930/PROOF.md", + "commit": "044d42d5bd7f31df6f7e6b9034d6711e8fb7ee43", + "blob": "ef2aa57959ea9f721bbf2316ce94cf616c1c9113", + "bytes": 39722, + "sha256": "f68038be79b46124b0f9b31205aa6e3682b34b6f5ef81f4a5697ae81f07cc46b" + } + ] +} diff --git a/frontiers/replacement_bar_occurrence_20261001/test_exact.py b/frontiers/replacement_bar_occurrence_20261001/test_exact.py new file mode 100644 index 000000000..4b997e33a --- /dev/null +++ b/frontiers/replacement_bar_occurrence_20261001/test_exact.py @@ -0,0 +1,125 @@ +"""Finite corroborating controls; the continuum proof is not tested here.""" +from fractions import Fraction as F +from pathlib import Path +import json +import tempfile +import unittest +import check_exact as c + + +class ExactControls(unittest.TestCase): + def test_ten_exact_sources_are_verified(self): + self.assertEqual(c.verify_sources(), 10) + + def test_counts_include_multifields_with_their_full_weight(self): + self.assertEqual(c.count_statistics({0:F(3,4),1:F(1,8),2:F(1,8)}), + (F(3,8),F(1,4),F(1,8),F(1,4),F(1,4))) + + def test_exact_count_occurrence_identity(self): + for n in range(12): + e,p,x,m,s=c.count_statistics({n:F(1)}) + self.assertEqual(e-p,x) + self.assertLessEqual(x,m) + self.assertLessEqual(2*(n>=2),m) + + def test_first_moment_alone_does_not_identify_occurrence(self): + h=F(1,4); lam=F(3,2); p=lam*h**5/2 + e,event,excess,multi,second=c.count_statistics({0:1-p,2:p}) + self.assertEqual(e,lam*h**5) + self.assertEqual(event/h**5,lam/2) + self.assertEqual(excess/h**5,lam/2) + + def test_small_multi_probability_does_not_control_weight(self): + # As h=1/m ->0: P(N>=2)/h^5=h, but E[N;N>=2]/h^5=1. + for m in [2,3,10]: + h=F(1,m); p=h**6 + e,event,excess,multi,second=c.count_statistics({0:1-p,m:p}) + self.assertEqual(event/h**5,h) + self.assertEqual(multi/h**5,1) + + def test_first_moment_excess_does_not_control_second_moment(self): + # P(N=m)=h^7 gives multi/h^5=h but factorial/h^5=1-h. + for m in [2,3,10]: + h=F(1,m); p=h**7 + e,event,excess,multi,second=c.count_statistics({0:1-p,m:p}) + self.assertEqual(multi/h**5,h) + self.assertEqual(second/h**5,1-h) + + def test_signed_field_first_mark_and_error(self): + fields=[(F(1,2),()),(F(1,4),(F(-1),)),(F(1,4),(F(1),F(1)))] + total,average,event,excess=c.mark_statistics(fields) + self.assertEqual((total,average,event,excess),(F(1,4),F(0),F(1,2),F(1,4))) + self.assertLessEqual(abs(total-average),excess) + + def test_empty_field_zero_denominator(self): + self.assertEqual(c.mark_statistics([(F(1),())]),(F(0),)*4) + + def test_single_selected_bar_mark_law(self): + h=F(1,5) + total,average,event,excess=c.mark_statistics([(1-h**5,()),(h**5,(F(2,3),))]) + self.assertEqual(total/event,F(2,3)) + self.assertEqual(average/event,F(2,3)) + self.assertEqual(excess,0) + + def test_volume_factor_for_occurrence(self): + L=F(24); coefficient=F(7,13); h=F(1,100) + probability=L**2*coefficient*h**5 + self.assertEqual(probability/h**5,L**2*coefficient) + self.assertNotEqual(probability/h**5,coefficient) + + def test_radial_measure_exponent(self): + self.assertEqual(F(1)+F(3)+F(1),5) # r, failure r^3, dr + self.assertEqual((F(3)**5-F(1)**5)/5,F(242,5)) + + def test_affine_hessian_midpoint(self): + pars=(F(1),F(-2),F(2),F(3),F(5)) + a=(F(-1,2),F(1,3)); b=(F(2,3),F(-1,4)) + self.assertEqual(c.cubic_hessian(pars,a),(F(-16,3),F(0),F(-11,6))) + midpoint=tuple((x+y)/2 for x,y in zip(a,b)) + ha,hb,hm=(c.cubic_hessian(pars,z) for z in (a,b,midpoint)) + self.assertEqual(hm,tuple((x+y)/2 for x,y in zip(ha,hb))) + + def test_degree_three_restriction_is_essential(self): + # Quartic -(x²-1)²-y² has two critical strict maxima. + for x in [F(-1),F(1)]: + self.assertEqual(-4*x*(x*x-1),0) + self.assertEqual(-12*x*x+4,-8) + # Its Hessian at x=0 is +4, not midpoint of endpoint values -8. + self.assertNotEqual(F(4),F(-8)) + + def test_homogeneous_coercivity_requires_discriminant(self): + # H=x³ alone has grad H=0 along nonzero y-axis. + x,y=F(0),F(1) + self.assertEqual((3*x*x,F(0)),(F(0),F(0))) + self.assertNotEqual(x*x+y*y,0) + + def test_annulus_budget_includes_linear_term(self): + self.assertEqual(c.annulus_budget(F(2),F(16),F(1,64),F(1,16)),F(29,128)) + self.assertLess(c.annulus_budget(F(2),F(16),F(1,64),F(1,16)),F(3,4)) + # A false budget dropping C/R can accept R=1 even when error exceeds c. + self.assertGreater(c.annulus_budget(F(3,5),F(1),F(1,1000),F(1,1000)),1) + + def test_invalid_count_laws_rejected(self): + for law in [{-1:F(1)},{True:F(1)},{0:F(1,2)},{0:F(-1),1:F(2)}]: + with self.assertRaises(ValueError): c.count_statistics(law) + + def test_wrong_manifest_digest_rejected(self): + with tempfile.TemporaryDirectory() as tmp: + path=Path(tmp)/'SOURCES.json'; path.write_text('{}') + with self.assertRaisesRegex(ValueError,'manifest digest'): + c.verify_sources(Path(tmp),path) + + def test_source_bytes_and_blob_fail_closed(self): + with tempfile.TemporaryDirectory() as tmp: + root=Path(tmp); (root/'x').write_bytes(b'abc') + good={'local_path':'x','bytes':3, + 'sha256':'ba7816bf8f01cfea414140de5dae2223b00361a396177a9cb410ff61f20015ad', + 'blob':'f2ba8f84ab5c1bce84a7b441cb1959cfc7093b7f'} + c.verify_entry(root,good) + for key,value in [('bytes',True),('sha256','0'*64),('blob','0'*40),('local_path','../x')]: + with self.assertRaises(ValueError): c.verify_entry(root,dict(good,**{key:value})) + (root/'link').symlink_to(root/'x') + with self.assertRaises(ValueError): c.verify_entry(root,dict(good,local_path='link')) + +if __name__=='__main__': + unittest.main()