diff --git a/.github/workflows/unique-replacement-bars.yml b/.github/workflows/unique-replacement-bars.yml new file mode 100644 index 000000000..ae38aa728 --- /dev/null +++ b/.github/workflows/unique-replacement-bars.yml @@ -0,0 +1,62 @@ +name: Unique replacement-bar exact controls +on: + pull_request: + paths: + - 'frontiers/unique_replacement_bar_intensity_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/unique-replacement-bars.yml' + push: + branches: [main] + paths: + - 'frontiers/unique_replacement_bar_intensity_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/unique-replacement-bars.yml' + workflow_dispatch: +permissions: + contents: read +concurrency: + group: unique-replacement-bars-${{ 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 + - name: Ensure pinned source commit is available + env: + GIT_NO_REPLACE_OBJECTS: '1' + GIT_NO_LAZY_FETCH: '1' + GIT_TERMINAL_PROMPT: '0' + run: | + source_commit=044d42d5bd7f31df6f7e6b9034d6711e8fb7ee43 + if ! git --no-lazy-fetch cat-file -e "$source_commit^{commit}" 2>/dev/null; then + git -c fetch.recurseSubmodules=false fetch --no-tags --depth=1 origin "$source_commit" + fi + - 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/unique_replacement_bar_intensity_20261001/test_sources.py + python3 -B -O -S frontiers/unique_replacement_bar_intensity_20261001/check_exact.py + else + python3 -B -S frontiers/unique_replacement_bar_intensity_20261001/test_sources.py + python3 -B -S frontiers/unique_replacement_bar_intensity_20261001/check_exact.py + fi diff --git a/frontiers/unique_replacement_bar_intensity_20261001/PROOF.md b/frontiers/unique_replacement_bar_intensity_20261001/PROOF.md new file mode 100644 index 000000000..9c79a672f --- /dev/null +++ b/frontiers/unique_replacement_bar_intensity_20261001/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/unique_replacement_bar_intensity_20261001/README.md b/frontiers/unique_replacement_bar_intensity_20261001/README.md new file mode 100644 index 000000000..043cf1830 --- /dev/null +++ b/frontiers/unique_replacement_bar_intensity_20261001/README.md @@ -0,0 +1,47 @@ +# Rare replacement bars, counted once + +One maximum can have several nearby candidate saddles that are not its actual persistence partner. Pushing every rejected candidate onto that maximum's bar counts the same bar repeatedly. This packet weights each candidate by the reciprocal of its eligible multiplicity, so one bar contributes exactly one count. + +For the stated planar Gaussian field on a fixed torus, fixed birth and positive-gap intervals, and a fixed shrinking distance band, the candidate theorem gives + +``` +expected number per unit area = C_U h^5 + o(h^5), +0 < C_R/2 <= C_U <= C_R < infinity. +``` + +Here C_R is the corresponding rejected-candidate coefficient; C_U is an explicitly identified Gaussian/angular integral with the reciprocal multiplicity inside it. This is a rare selected population of **actual finite ordinary superlevel H0 bars**, conditional on the exact imported analytic interfaces. It is not the ordinary short-bar leading law, a new all-mark theorem, or a statement about fields conditioned on containing a bar. + +- [Proof and exact population](PROOF.md): counting identity, measurable mark, weighted limit, normalization and scope. +- [Root and cutoff analysis](ROOTS.md): all saddles, including below the original window; null boundaries and exact counterexamples to wrong counts. +- [Source identities](SOURCES.json): seven exact imported sources, with hypotheses retained. +- [Exact controls](check_exact.py): rational algebra, source integrity and deliberately wrong alternatives; these checks do not prove the continuum limit. +- [Historical-source regressions](test_sources.py): real temporary Git repositories test commit/path binding, missing history, replacement objects and Git environment isolation. + +From the repository root, with Python3.11 and Git supporting +`--no-lazy-fetch` available: + +```sh +python3.11 -B -S frontiers/unique_replacement_bar_intensity_20261001/check_exact.py +python3.11 -B -O -S frontiers/unique_replacement_bar_intensity_20261001/check_exact.py +python3.11 -B -S frontiers/unique_replacement_bar_intensity_20261001/test_sources.py +python3.11 -B -O -S frontiers/unique_replacement_bar_intensity_20261001/test_sources.py +``` + +The verifier requires the pinned commit +`044d42d5bd7f31df6f7e6b9034d6711e8fb7ee43` and its source objects in this +repository. It checks that the object is a commit, each historical path is a +regular blob, and that its blob identity and bytes match the manifest and +working file. Replacement objects and inherited Git repository/configuration +environment overrides are disabled. Missing history fails closed; the checker +does not fetch. For a shallow checkout, explicitly fetch only the pinned commit +before running the checks: + +```sh +git fetch --no-tags --depth=1 origin 044d42d5bd7f31df6f7e6b9034d6711e8fb7ee43 +``` + +The packet workflow performs this bounded fetch only when needed; it does not +require full repository history. This source-binding repair changes neither +PROOF.md, ROOTS.md nor SOURCES.json, and does not re-vote their mathematical review. + +Authors: OpenAI/Codex root and the named contributors in ROOTS.md, under Dylan Roy's delegation. Source-bound review is recorded in the associated PR. Scientific effect NONE; no imported theorem, independence requirement, formal alignment or controlling scientific status is promoted by these files or green checks. diff --git a/frontiers/unique_replacement_bar_intensity_20261001/ROOTS.md b/frontiers/unique_replacement_bar_intensity_20261001/ROOTS.md new file mode 100644 index 000000000..b27d9ac81 --- /dev/null +++ b/frontiers/unique_replacement_bar_intensity_20261001/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/unique_replacement_bar_intensity_20261001/SOURCES.json b/frontiers/unique_replacement_bar_intensity_20261001/SOURCES.json new file mode 100644 index 000000000..210dcacaa --- /dev/null +++ b/frontiers/unique_replacement_bar_intensity_20261001/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/unique_replacement_bar_intensity_20261001/check_exact.py b/frontiers/unique_replacement_bar_intensity_20261001/check_exact.py new file mode 100644 index 000000000..6521bed3c --- /dev/null +++ b/frontiers/unique_replacement_bar_intensity_20261001/check_exact.py @@ -0,0 +1,312 @@ +#!/usr/bin/env python3 +"""Exact finite fixtures for ROOTS.md; not a continuum theorem certificate.""" + +from fractions import Fraction as F +import hashlib +import json +import os +from pathlib import Path, PurePosixPath +import subprocess + + +def require(condition, message): + if not condition: + raise RuntimeError(message) + + +SOURCE_COMMIT = '044d42d5bd7f31df6f7e6b9034d6711e8fb7ee43' +SOURCE_KEYS = {'P', 'CAP', 'E1', 'E2', 'REC', 'CUB', 'ELDER'} + + +def contained_file(repo, relative): + require(isinstance(relative, str) and bool(relative), 'source path must be text') + pure = PurePosixPath(relative) + require(not pure.is_absolute() and str(pure) == relative + and all(part not in ('', '.', '..') for part in pure.parts) + and '\\' not in relative, 'source path must be canonical and relative') + target = repo + for part in pure.parts: + target = target / part + require(not target.is_symlink(), 'source path must not contain symlinks') + require(target.is_file(), 'source path must name a regular file') + resolved = target.resolve(strict=True) + require(resolved == target and repo in resolved.parents, + 'source path must remain within repository') + return target + + +def source_git(repo, *args): + # Bind reads to this repository, not inherited Git directories/configuration. + env = {key: value for key, value in os.environ.items() + if not key.startswith('GIT_')} + env.update(GIT_CONFIG_NOSYSTEM='1', GIT_CONFIG_GLOBAL=os.devnull, + GIT_NO_REPLACE_OBJECTS='1', GIT_NO_LAZY_FETCH='1', + GIT_TERMINAL_PROMPT='0', GIT_OPTIONAL_LOCKS='0') + try: + result = subprocess.run( + ['git', '--no-replace-objects', '--no-lazy-fetch', '--literal-pathspecs', + '-C', str(repo), *args], + env=env, stdout=subprocess.PIPE, stderr=subprocess.PIPE, check=False) + except OSError as exc: + raise RuntimeError('Git is required to verify historical sources') from exc + require(result.returncode == 0, 'historical Git read failed: ' + args[0]) + return result.stdout + + +def verify_historical_source(repo, entry, data): + top = source_git(repo, 'rev-parse', '--show-toplevel') + require(Path(os.fsdecode(top.removesuffix(b'\n'))).resolve() == repo, + 'historical source repository root mismatch') + require(source_git(repo, 'cat-file', '-t', SOURCE_COMMIT).strip() == b'commit', + 'historical source object must be a commit') + records = source_git(repo, 'ls-tree', '-z', SOURCE_COMMIT, '--', entry['path']).split(b'\0') + require(len(records) == 2 and records[1] == b'', + 'historical source path must name one tree entry') + fields = records[0].split(b'\t', 1) + require(len(fields) == 2 and fields[1] == os.fsencode(entry['path']), + 'historical source path mismatch') + metadata = fields[0].split() + require(len(metadata) == 3 and metadata[0] in (b'100644', b'100755') + and metadata[1] == b'blob', 'historical source must be a regular blob') + require(metadata[2].decode('ascii') == entry['blob'], + 'historical source Git blob mismatch') + historical_data = source_git(repo, 'cat-file', 'blob', entry['blob']) + require(historical_data == data, 'historical source bytes mismatch') + + +def verify_source_entry(repo, entry): + require(isinstance(entry, dict), 'source entry must be an object') + require(entry.get('commit') == SOURCE_COMMIT, 'source commit mismatch') + target = contained_file(repo, entry.get('path')) + data = target.read_bytes() + require(type(entry.get('bytes')) is int and len(data) == entry['bytes'], + 'source byte length mismatch') + require(hashlib.sha256(data).hexdigest() == entry.get('sha256'), + 'source SHA-256 mismatch') + blob = hashlib.sha1(b'blob ' + str(len(data)).encode('ascii') + b'\0' + data).hexdigest() + require(blob == entry.get('blob'), 'source Git blob mismatch') + verify_historical_source(repo, entry, data) + return entry['key'] + + +def verify_sources(): + script = Path(__file__).absolute() + require(not script.is_symlink(), 'check script must not be a symlink') + repo = script.resolve(strict=True).parents[2] + relative = 'frontiers/unique_replacement_bar_intensity_20261001/SOURCES.json' + manifest = json.loads(contained_file(repo, relative).read_text()) + require(manifest.get('source_commit') == SOURCE_COMMIT, 'manifest source cut mismatch') + entries = manifest.get('sources') + require(isinstance(entries, list) and len(entries) == 7, 'exactly seven source entries required') + keys = [verify_source_entry(repo, entry) for entry in entries] + require(len(set(keys)) == 7 and set(keys) == SOURCE_KEYS, 'source key set mismatch') + require(len({entry['path'] for entry in entries}) == 7, 'duplicate source paths') + mutant = dict(entries[0]) + mutant['sha256'] = '0' * 64 + rejected_wrong_digest = False + try: + verify_source_entry(repo, mutant) + except RuntimeError as exc: + require(str(exc) == 'source SHA-256 mismatch', 'wrong-digest probe failed for another reason') + rejected_wrong_digest = True + require(rejected_wrong_digest, 'wrong source digest was not rejected') + return {'verified_keys': sorted(keys), 'source_commit': SOURCE_COMMIT, + 'checks': ['canonical_relative_paths', 'no_symlinks', 'repository_containment', + 'byte_lengths', 'sha256', 'git_blob', 'historical_commit_type', + 'historical_regular_blob', 'historical_blob_and_bytes', + 'git_environment_isolation', 'replacement_objects_disabled'], + 'wrong_digest_probe': 'REJECTED'} + + +M = (F(-1, 2), F(0)) +S = (F(1, 2), F(0)) + + +def value(p, y): + k, s, a, beta, c3 = p + x, z = y + return (2*k*x**3 - 3*k*x/2 - k/2 + s*z**2/2 + + a*(x**2-F(1, 4))*z/2 + beta*x*z**2/2 + c3*z**3/6) + + +def gradient(p, y): + k, s, a, beta, c3 = p + x, z = y + return (6*k*x**2-3*k/2+a*x*z+beta*z**2/2, + s*z+a*(x**2-F(1, 4))/2+beta*x*z+c3*z**2/2) + + +def determinant(p, y): + k, s, a, beta, c3 = p + x, z = y + xx, xz, zz = 12*k*x+a*z, a*x+beta*z, s+beta*x+c3*z + return xx*zz-xz*xz + + +def shear_data(p): + k, s, a, beta, c3 = p + b = beta-a*a/(12*k) + d = (c3-a*beta/(4*k)+a**3/(72*k*k))/2 + sigma = 12*k*d*d+(s-b)**2*(b+2*s) + delta = 12*k*d*d+b**3 + h = delta-4*b*s*s + return b, d, sigma, delta, h + + +def distance_squared(p, y, use_shear=False): + x, z = y + if use_shear: + x += p[2]*z/(12*p[0]) + return (x-M[0])**2+z*z + + +def admissible(p, y, band, gaps, t, use_shear=False): + if determinant(p, y) >= 0 or value(p, y) >= 0: + return False + d2 = distance_squared(p, y, use_shear) + lo, hi = band + if not (lo*lo <= t*t*d2 <= hi*hi): + return False + klo, khi = gaps + height_squared = value(p, y)**2 + return klo*klo*d2**3 <= height_squared <= khi*khi*d2**3 + + +def verify_strict_margins(name, p, roots, band, gaps, t, use_shear=False): + for y in roots: + if determinant(p, y) >= 0: + continue + d2 = distance_squared(p, y, use_shear) + require(d2 > 0, name + ': saddle separated from maximum') + require(all(t*t*d2 != endpoint*endpoint for endpoint in band), + name + ': strict radius membership margins') + require(all(value(p, y)**2 != endpoint*endpoint*d2**3 for endpoint in gaps), + name + ': strict gap membership margins') + + +def rejected(p, roots, partner, band, gaps, t, *, window_only=False, + include_partner=False, use_shear=False): + answer = [] + for y in roots: + if y == partner and not include_partner: + continue + if window_only and y != S and not (-p[0] < value(p, y) < 0): + continue + if admissible(p, y, band, gaps, t, use_shear): + answer.append(y) + return answer + + +def verify_fixture(name, p, extra, expected_heights, expected_dets): + roots = [M, S] + extra + require(len(set(roots)) == 4, name + ': roots must be distinct') + b, d, sigma, delta, h = shear_data(p) + require(p[1] < -abs(b)/2, name + ': strict endpoint typing') + for label, number in [('D', d), ('Sigma', sigma), ('Delta', delta), ('H', h)]: + require(number != 0, name + ': excluded ' + label) + for y in roots: + require(gradient(p, y) == (0, 0), name + ': critical gradient') + require(determinant(p, y) != 0, name + ': Morse root') + require(value(p, M) == 0 and value(p, S) == -p[0], name + ': pin heights') + for y, expected_height, expected_det in zip(extra, expected_heights, expected_dets): + require(value(p, y) == expected_height, name + ': extra height') + require(determinant(p, y) == expected_det, name + ': extra determinant') + u = y[0]+p[2]*y[1]/(12*p[0]) + require(h*y[1]**2 == 3*p[0]*(b+4*p[1]*u)**2, + name + ': all-root identity') + window = [y for y in extra if -p[0] < value(p, y) < 0] + require(bool(window), name + ': failure window must be nonempty') + partner = max(window, key=lambda y: value(p, y)) + require(sum(value(p, y) == value(p, partner) for y in window) == 1, + name + ': unique highest window saddle') + return roots, partner + + +def main(): + source_binding = verify_sources() + p1 = (F(1), F(-21, 10), F(0), F(-3), F(3, 5)) + y11, y12 = (F(-5, 8), F(3, 4)), (F(-5, 6), F(-4, 3)) + roots1, partner1 = verify_fixture('two_window', p1, [y11, y12], + [F(-23, 320), F(-13, 45)], + [F(-27, 4), F(-12)]) + band1, gaps1 = (F(1, 2), F(2)), (F(1, 10), F(2)) + verify_strict_margins('two_window', p1, roots1, band1, gaps1, F(1)) + verify_strict_margins('radius_crossed', p1, roots1, band1, gaps1, F(8, 5)) + count1 = len(rejected(p1, roots1, partner1, band1, gaps1, F(1))) + require(count1 == 2, 'two_window: full count') + require(sum(F(1, count1) for _ in range(count1)) == 1, + 'reciprocal multiplicity must count maximum once') + require(count1 != 1, 'negative control: omission of reciprocal must differ') + include_actual = len(rejected(p1, roots1, partner1, band1, gaps1, F(1), + include_partner=True)) + require(include_actual == 3, 'negative control: actual partner inclusion') + crossed = len(rejected(p1, roots1, partner1, band1, gaps1, F(8, 5))) + require(crossed == 1 and crossed != count1, 'negative control: radius crossing') + require(len(rejected(p1, roots1, partner1, band1, gaps1, F(1), + window_only=True)) == count1, + 'original fixture must not claim below-window coverage') + + p2 = (F(1), F(-39, 16), F(0), F(-3), F(3, 2)) + y21, y22 = (F(-5, 8), F(3, 4)), (F(-37, 24), F(-35, 12)) + roots2, partner2 = verify_fixture('below_window', p2, [y21, y22], + [F(-53, 512), F(-11125, 4608)], + [F(-297, 32), F(-1155, 32)]) + require(value(p2, y22) < -p2[0], 'below_window: genuinely below pin') + require(determinant(p2, M) == F(45, 8) and determinant(p2, S) == F(-189, 8), + 'below_window: pin determinants') + d22 = distance_squared(p2, y22) + q22 = value(p2, y22)**2/d22**3 + require(d22 == F(5525, 576), 'below_window: original coordinate distance') + require(q22 == F(71289, 10793861), 'below_window: gap ratio squared') + band2, gaps2 = (F(1, 2), F(4)), (F(1, 100), F(2)) + verify_strict_margins('below_window', p2, roots2, band2, gaps2, F(1)) + count2 = len(rejected(p2, roots2, partner2, band2, gaps2, F(1))) + window_count = len(rejected(p2, roots2, partner2, band2, gaps2, F(1), + window_only=True)) + require(count2 == 2 and window_count == 1, + 'negative control: below-window omission must change count') + + p3 = (F(1), F(-21, 10), F(12), F(9), F(18, 5)) + y31, y32 = (F(-11, 8), F(3, 4)), (F(1, 2), F(-4, 3)) + roots3, partner3 = verify_fixture('nonzero_shear', p3, [y31, y32], + [F(-23, 320), F(-13, 45)], + [F(-27, 4), F(-12)]) + band3, gaps3 = (F(1, 2), F(3, 2)), (F(1, 100), F(2)) + verify_strict_margins('nonzero_shear_physical', p3, roots3, band3, gaps3, F(1)) + verify_strict_margins('nonzero_shear_mutant', p3, roots3, band3, gaps3, F(1), True) + physical_count = len(rejected(p3, roots3, partner3, band3, gaps3, F(1))) + shear_count = len(rejected(p3, roots3, partner3, band3, gaps3, F(1), + use_shear=True)) + require(physical_count == 1 and shear_count == 2, + 'negative control: sheared distance must change count') + + scale = F(7, 3) + scaled = tuple(scale*v for v in p2) + for y in roots2: + require(gradient(scaled, y) == (0, 0), 'positive scaling preserves roots') + require(value(scaled, y) == scale*value(p2, y), 'positive scaling of values') + require(shear_data(scaled)[0] == scale*shear_data(p2)[0], 'scaling of B') + require(shear_data(scaled)[1] == scale*shear_data(p2)[1], 'scaling of D') + + print(json.dumps({ + 'status': 'PASS_EXACT_FINITE_FIXTURES', + 'source_binding': source_binding, + 'arithmetic': 'fractions.Fraction; no floating-point root tests', + 'guards': 'explicit conditionals active under python -O', + 'counts': {'two_window': count1, 'radius_crossed': crossed, + 'include_actual_mutant': include_actual, + 'below_window': count2, 'window_only_mutant': window_count, + 'physical_coordinates': physical_count, + 'sheared_coordinates_mutant': shear_count}, + 'below_window_exact': {'height': str(value(p2, y22)), + 'distance_squared': str(d22), + 'gap_ratio_squared': str(q22)}, + 'negative_controls': ['omit_reciprocal', 'include_actual_partner', + 'retain_after_radius_crossing', 'omit_below_window', + 'use_sheared_distances'], + 'scope': 'Finite fixture checks only; not continuum proof or scientific acceptance.' + }, indent=2, sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/frontiers/unique_replacement_bar_intensity_20261001/test_sources.py b/frontiers/unique_replacement_bar_intensity_20261001/test_sources.py new file mode 100644 index 000000000..37bf1e31b --- /dev/null +++ b/frontiers/unique_replacement_bar_intensity_20261001/test_sources.py @@ -0,0 +1,167 @@ +#!/usr/bin/env python3 +"""Historical-source regressions using real isolated Git repositories. + +Removing historical commit/path verification must make the current-only path +and changed historical blob tests fail. Fixture SOURCE_COMMIT values are pinned +to temporary commits; no Git subprocess or source verifier is mocked. +""" +import hashlib +import importlib.util +import os +from pathlib import Path +import subprocess +import tempfile +import unittest + +SPEC = importlib.util.spec_from_file_location( + "unique_replacement_check", Path(__file__).with_name("check_exact.py")) +c = importlib.util.module_from_spec(SPEC) +SPEC.loader.exec_module(c) + + +class HistoricalSourceTests(unittest.TestCase): + def setUp(self): + self.tmp = tempfile.TemporaryDirectory(prefix="c50-history-") + self.addCleanup(self.tmp.cleanup) + self.repo = Path(self.tmp.name).resolve() / "repo" + self.repo.mkdir() + self.saved_pin = c.SOURCE_COMMIT + self.addCleanup(setattr, c, "SOURCE_COMMIT", self.saved_pin) + self.git("init", "--quiet") + self.git("config", "user.name", "Source fixture") + self.git("config", "user.email", "fixture@example.invalid") + self.git("config", "commit.gpgsign", "false") + self.git("config", "core.hooksPath", str(self.repo / "no-hooks")) + self.path = "source.md" + self.write(b"historical source\n") + self.commit = self.commit_all() + c.SOURCE_COMMIT = self.commit + + def git(self, *args, repo=None): + env = {k: v for k, v in os.environ.items() if not k.startswith("GIT_")} + env.update(GIT_CONFIG_NOSYSTEM="1", GIT_CONFIG_GLOBAL=os.devnull, + GIT_TERMINAL_PROMPT="0") + return subprocess.check_output( + ["git", "-C", str(repo or self.repo), *args], + env=env, stderr=subprocess.PIPE).decode().strip() + + def write(self, data, path=None): + (self.repo / (path or self.path)).write_bytes(data) + + def commit_all(self): + self.git("add", "-A") + self.git("commit", "--quiet", "-m", "fixture source") + return self.git("rev-parse", "HEAD") + + def entry(self, path=None): + relative = path or self.path + data = (self.repo / relative).read_bytes() + return {"key": "P", "commit": c.SOURCE_COMMIT, "path": relative, + "bytes": len(data), "sha256": hashlib.sha256(data).hexdigest(), + "blob": hashlib.sha1( + b"blob " + str(len(data)).encode() + b"\0" + data).hexdigest()} + + def environment(self, **changes): + before = {k: os.environ.get(k) for k in changes} + os.environ.update(changes) + def restore(): + for key, old in before.items(): + if old is None: + os.environ.pop(key, None) + else: + os.environ[key] = old + self.addCleanup(restore) + + def test_accepts_exact_historical_regular_blob(self): + self.assertEqual(c.verify_source_entry(self.repo, self.entry()), "P") + + def test_rejects_current_only_path(self): + self.write(b"valid current file absent from pinned commit\n", "later.md") + self.commit_all() + with self.assertRaises(RuntimeError): + c.verify_source_entry(self.repo, self.entry("later.md")) + + def test_rejects_changed_historical_blob_even_with_matching_current_manifest(self): + self.write(b"updated source with matching manifest\n") + self.commit_all() + with self.assertRaises(RuntimeError): + c.verify_source_entry(self.repo, self.entry()) + + def test_rejects_missing_historical_commit(self): + c.SOURCE_COMMIT = "f" * 40 + with self.assertRaises(RuntimeError): + c.verify_source_entry(self.repo, self.entry()) + + def test_rejects_tree_object_as_source_commit(self): + c.SOURCE_COMMIT = self.git("rev-parse", self.commit + "^{tree}") + with self.assertRaises(RuntimeError): + c.verify_source_entry(self.repo, self.entry()) + + def test_rejects_tag_object_as_source_commit(self): + self.git("tag", "-a", "source-tag", "-m", "fixture tag") + c.SOURCE_COMMIT = self.git("rev-parse", "source-tag") + with self.assertRaises(RuntimeError): + c.verify_source_entry(self.repo, self.entry()) + + def test_rejects_historical_symlink_with_matching_current_regular_bytes(self): + (self.repo / self.path).unlink() + (self.repo / self.path).symlink_to("target.md") + c.SOURCE_COMMIT = self.commit_all() + (self.repo / self.path).unlink() + self.write(b"target.md") + with self.assertRaises(RuntimeError): + c.verify_source_entry(self.repo, self.entry()) + + def test_commit_replacement_cannot_make_wrong_history_pass(self): + self.write(b"replacement commit content\n") + replacement = self.commit_all() + self.git("replace", self.commit, replacement) + self.environment(GIT_NO_REPLACE_OBJECTS="0") + with self.assertRaises(RuntimeError): + c.verify_source_entry(self.repo, self.entry()) + + def test_blob_replacement_is_ignored_for_valid_history(self): + old_blob = self.git("rev-parse", self.commit + ":" + self.path) + self.write(b"replacement blob content\n") + self.commit_all() + replacement_blob = self.git("rev-parse", "HEAD:" + self.path) + self.git("replace", old_blob, replacement_blob) + self.write(b"historical source\n") + self.assertEqual(c.verify_source_entry(self.repo, self.entry()), "P") + + def test_hostile_git_environment_does_not_redirect_valid_repository(self): + self.environment(GIT_DIR=str(self.repo / "nonexistent"), + GIT_WORK_TREE=str(self.repo / "wrong-worktree"), + GIT_COMMON_DIR=str(self.repo / "wrong-common"), + GIT_OBJECT_DIRECTORY=str(self.repo / "wrong-objects"), + GIT_CONFIG_COUNT="1", GIT_CONFIG_KEY_0="core.bare", + GIT_CONFIG_VALUE_0="true") + self.assertEqual(c.verify_source_entry(self.repo, self.entry()), "P") + + def test_external_git_directory_cannot_supply_missing_local_history(self): + empty = Path(self.tmp.name).resolve() / "empty" + empty.mkdir() + self.git("init", "--quiet", repo=empty) + (empty / self.path).write_bytes(b"historical source\n") + entry = self.entry() + self.environment(GIT_DIR=str(self.repo / ".git"), + GIT_WORK_TREE=str(self.repo)) + with self.assertRaises(RuntimeError): + c.verify_source_entry(empty, entry) + + def test_parent_repository_cannot_substitute_for_requested_repository(self): + nested = self.repo / "nested" + nested.mkdir() + (nested / self.path).write_bytes(b"historical source\n") + with self.assertRaises(RuntimeError): + c.verify_source_entry(nested, self.entry()) + + def test_existing_working_file_digest_guard_remains_active(self): + entry = self.entry() + self.write(b"modified after manifest\n") + with self.assertRaises(RuntimeError): + c.verify_source_entry(self.repo, entry) + + +if __name__ == "__main__": + unittest.main(verbosity=2)