From cf95d824d31b514bc5083a2c553ccce6b08bb822 Mon Sep 17 00:00:00 2001 From: Dylan Roy Date: Thu, 1 Oct 2026 19:07:03 +0000 Subject: [PATCH 1/4] C52 in every d >= 2: ordinary short-bar occurrence on T_L^d Additive packet frontiers/ordinary_short_bar_occurrence_all_d_20261001. It extends OpenAI/Codex's planar C52 (Math-#235) to every fixed d >= 2: E[K_tau; K_tau >= 2] = o(tau^(2/3)), p_tau = L^d (3/2) c_{d,L} tau^(2/3) + o(tau^(2/3)), the singleton conditional count law and the field-first mark law. All seven consumed sources are stated for every d >= 2. The new step is Lemma F_d: - a transverse ridge on a ball, by strict concavity; - g''' = D^3F[v,v,v] and g'' = Schur complement; - Haynsworth inertia for the pin types; - the lambda_max(A) = 0 null boundary, from the density of A on Sym(m); - the general-d mesh counts. Exact rational controls cover d = 2..6, with 17 mutants killed in both modes. Scientific effect NONE; C8 OPEN. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015wNj8LPTKXsaT68G3DgPPh --- .../ordinary-short-bar-occurrence-all-d.yml | 53 +++ .../NOTE.md | 436 ++++++++++++++++++ .../README.md | 44 ++ .../SOURCES.json | 100 ++++ .../check.py | 373 +++++++++++++++ .../test_check.py | 157 +++++++ .../verify_sources.py | 56 +++ 7 files changed, 1219 insertions(+) create mode 100644 .github/workflows/ordinary-short-bar-occurrence-all-d.yml create mode 100644 frontiers/ordinary_short_bar_occurrence_all_d_20261001/NOTE.md create mode 100644 frontiers/ordinary_short_bar_occurrence_all_d_20261001/README.md create mode 100644 frontiers/ordinary_short_bar_occurrence_all_d_20261001/SOURCES.json create mode 100644 frontiers/ordinary_short_bar_occurrence_all_d_20261001/check.py create mode 100644 frontiers/ordinary_short_bar_occurrence_all_d_20261001/test_check.py create mode 100644 frontiers/ordinary_short_bar_occurrence_all_d_20261001/verify_sources.py diff --git a/.github/workflows/ordinary-short-bar-occurrence-all-d.yml b/.github/workflows/ordinary-short-bar-occurrence-all-d.yml new file mode 100644 index 000000000..42a2ea5a5 --- /dev/null +++ b/.github/workflows/ordinary-short-bar-occurrence-all-d.yml @@ -0,0 +1,53 @@ +name: Ordinary short-bar occurrence (all d) exact controls +on: + pull_request: + paths: + - 'frontiers/ordinary_short_bar_occurrence_all_d_20261001/**' + - 'frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md' + - 'frontiers/short_bar_endpoint_law_20261001/PROOF.md' + - 'imports/lifetime_parent_20260925/**' + - 'reviews/d1_section9_borel_repair_20260925/REPAIR.md' + - 'reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md' + - '.github/workflows/ordinary-short-bar-occurrence-all-d.yml' + push: + branches: [main] + paths: + - 'frontiers/ordinary_short_bar_occurrence_all_d_20261001/**' + - 'frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md' + - 'frontiers/short_bar_endpoint_law_20261001/PROOF.md' + - 'imports/lifetime_parent_20260925/**' + - 'reviews/d1_section9_borel_repair_20260925/REPAIR.md' + - 'reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md' + - '.github/workflows/ordinary-short-bar-occurrence-all-d.yml' + workflow_dispatch: +permissions: + contents: read +concurrency: + group: ordinary-short-bar-occurrence-all-d-${{ github.ref }} + cancel-in-progress: true +jobs: + exact: + runs-on: ubuntu-latest + timeout-minutes: 10 + 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 sources and run exact controls + env: + PYTHON_MODE: ${{ matrix.mode }} + run: | + D=frontiers/ordinary_short_bar_occurrence_all_d_20261001 + if [ "$PYTHON_MODE" = optimized ]; then F="-B -O -S"; else F="-B -S"; fi + python3 $F $D/verify_sources.py + python3 $F $D/check.py + python3 $F $D/test_check.py -v + - name: Reject implementation mutants in both Python modes + if: matrix.mode == 'normal' + run: python3 -B -S frontiers/ordinary_short_bar_occurrence_all_d_20261001/test_check.py --mutants diff --git a/frontiers/ordinary_short_bar_occurrence_all_d_20261001/NOTE.md b/frontiers/ordinary_short_bar_occurrence_all_d_20261001/NOTE.md new file mode 100644 index 000000000..5a0fc6e6d --- /dev/null +++ b/frontiers/ordinary_short_bar_occurrence_all_d_20261001/NOTE.md @@ -0,0 +1,436 @@ +# Ordinary short-bar occurrence in every dimension d >= 2 + +Object: C52-ALL-D-ORDINARY-SHORT-BAR-OCCURRENCE-20261001-v1. +Author lane: Anthropic / Claude (session 015wNj8L…), under Dylan Roy's delegation. Additive conditional candidate. +Scientific effect: NONE. C8 OPEN. No STATUS, PROOF_INDEX, GRAPH, prize or premise edit. + +**Credit.** The argument is OpenAI/Codex's C52 (Math-#235, head `c463777`: `FOLD_ISOLATION.md` blob `a3d4e7c4`, +`PROOF.md` blob `69ff20a6`). C52 proves the planar case and states that it makes "no extension of the present planar +lemma to other dimensions" (FOLD_ISOLATION §8). This packet supplies that extension. Its planar case `d = 2` is exactly +C52's Theorem O, so it neither supersedes nor edits #235. C52's files are cited, not consumed as premises: every step +used here is restated and proved below in dimension d. + +## 0. Statement + +Fix `d >= 2` and `L > 0`. Let X be the centered, variance-one periodized Gaussian field on `T_L^d = R^d/(L Z^d)` with +covariance + + K_L(z) = sum_{n in Z^d} exp(-|z + L n|^2/2) / sum_{n in Z^d} exp(-|L n|^2/2). + +Use ordinary SUPERLEVEL H0 persistence. A finite bar is born at a maximum M and dies at its actual global elder-selected +merging saddle S, of index d-1. Exclude the essential global-maximum class. Let `K_tau` be the number of finite bars of +lifetime in `(0, tau]` in ONE field on the WHOLE torus. Its expectation is not divided by volume. + +The seven sources P, CAP, E1, E2, REC, R and T are pinned in `SOURCES.json` at Math- `7fe06b0`. They are the sources +C52 consumes, and each is stated for every fixed `d >= 2`: +- [P] "Fix a dimension d>=2"; +- [CAP] "Let d>=2"; +- [R] and [T] "for each fixed d>=2" and "Fix d>=2"; +- [REC] §1 "for fixed d >= 2"; +- [E2] uses the pair map into `R^(2d)`. + +[P] is read through [CAP, E1, E2, REC] under REC's mandatory reading rule, with an embedded `r_0 < L/(4 sqrt 2)`. + +**Theorem O_d (conditional on these interfaces).** As tau decreases to zero with d and L fixed, + + B_tau := E[K_tau 1{K_tau >= 2}] = o(tau^(2/3)). (O1) + +Put `m_tau = E K_tau`, `p_tau = P(K_tau > 0)` and `e_tau = m_tau - p_tau`. Then + + 0 <= e_tau = E[(K_tau - 1)_+] <= B_tau = o(tau^(2/3)), + p_tau = L^d (3/2) c_{d,L} tau^(2/3) + o(tau^(2/3)), (O2) + TV(law(K_tau | K_tau > 0), delta_1) = P(K_tau >= 2)/p_tau -> 0, (O3) + +with `c_{d,L} > 0` the coefficient of [P] Theorem C, given explicitly by [P] (15.2). + +Condition a field on `K_tau > 0` and pick one of its short bars uniformly. For every common measurable mark, the law +of that mark is within `e_tau/m_tau = o(1)` in total variation of the intensity-normalized mark law: + + TV(F_tau, I_tau) <= e_tau/m_tau. (O4) + +With T's cubic mark, the field-first law converges in total variation to + + (2/3) y^(-1/3) dy g(q) dq, g = A_0/(3 c_{d,L} k^(2/3)) on R x (0, inf) x S^(d-1). (O5) + +The only new analytic input is Lemma F_d (§2), the dimension-d ordinary-fold isolation. Sections 3–4 are C52's +consumer, transcribed with `L^d`, `S^(d-1)`, the exponent `2d` and `c_{d,L}`. + +**Not claimed:** +- a rate for the little-o; +- factorial moments, a Poisson law, or independent regions; +- an increasing-volume limit, or the limit `d -> infinity`; +- uniqueness of auxiliary witnesses; +- reacceptance of any source. + +Every source is a retained hypothesis. + +## 1. What changes from d = 2 + +| Step | C52 (d = 2) | Here (every d >= 2), m = d - 1 | +|---|---|---| +| Pins | 6 rows, `|det T_r| = 12 r^-5` | `2d+2` rows, `|det T_r| = 12 r^-(d+3)` ([P] (3.2)) | +| Transverse datum | scalar `A = F_0,zz(0)` | `m x m` block `A = D_y^2 F_0(0)`, with a density on `Sym(m)` | +| Type boundary | `A < 0`, `A > 0`, `A = 0` null | `A < 0`; `lambda_max(A) > 0`; `{lambda_max(A) = 0}` inside `{det A = 0}`, which is null | +| Ridge | intermediate value theorem in z | strict concavity on a ball with inward transverse gradient | +| Types | `2 x 2` sign of the Schur complement | Haynsworth inertia: `In(H) = (m, 0, 0) + In(s)` | +| Mesh `(q, p)` | `(3,4), (4,5), (2,3)` | `(2d-1, 2d), (2d, 2d+1), (d, d+1)` ([P] §8) | +| Volume, sphere | `L^2`, `S^1` | `L^d`, `S^(d-1)` | +| Majorant | `(1+|b|+k)^4` | `(1+|b|+k)^(2d)` ([P] (13.4)) | +| Ledger | `r` | `r` in every d ([P] §10) | + +## 2. Lemma F_d: ordinary-fold isolation in dimension d + +Fix `b` real, `k > 0` and an orthonormal frame `R = (u, e_1, ..., e_m)`. Use local coordinates `(x, y)`, with `x` +real and `y` in `R^m`, centered at the midpoint. For small `r` put + + M_r = (-r/2, 0), S_r = (r/2, 0), + f(M_r) = b, f(S_r) = b - k r^3, grad f(M_r) = grad f(S_r) = 0. + +These are `2d + 2` scalar observations. `Q_r` is the whole-field Gaussian regression law at them. The typed weight is +[P]'s + + W_r = |det H_(M_r) det H_(S_r)| 1{H_(M_r) < 0, index H_(S_r) = d - 1}. + +**Lemma F_d.** There is a coupling `F_r` of `Q_r`, with contact limit `F_0`, such that: +1. `F_r -> F_0` almost surely in `C^4(T_L^d)`. +2. Let `A = D_y^2 F_0(0)`. Almost surely on `{A < 0}` (negative definite), for all small `r`, the only critical + points of `F_r` in one fixed neighbourhood of `0` are `M_r` and `S_r`. +3. Every other critical point continues a nondegenerate critical point of `F_0`. Their limiting values are pairwise + distinct and differ from `b`. +4. For each fixed `y` in `(0, 1]`, put `tau(r) = k r^3/y`. Almost surely on `{A < 0}`, `K_(tau(r))(F_r) <= 1` + eventually. +5. On the whole coupling space, + + (W_r(F_r)/r^2) 1{K_(tau(r))(F_r) >= 2} -> 0 almost surely, (N0) + + and its expectation tends to 0. + +Thresholds may depend on the sample and on `b`, `k`, `R` and `y`. No rate is claimed. + +### 2.1 Coupling and contact law + +[P] §3 orders the observations as +`O_r = (f(a), f_x(a), f(c), f_x(c), f_y1(a), f_y1(c), ..., f_ym(a), f_ym(c))`, with `a = -r/2` and `c = r/2`. It defines +`U_r = T_r O_r` by four axial rows and two rows per transverse direction: +- the axial rows `(f(a)+f(c))/2`, `(f(c)-f(a))/r`, `(f_x(c)-f_x(a))/r` and + `(6/r^2)[f_x(a)+f_x(c)-2(f(c)-f(a))/r]`; +- for each `j`, the rows `(f_yj(a)+f_yj(c))/2` and `(f_yj(c)-f_yj(a))/r`. + +[P] (3.2)–(3.4) give + + |det T_r| = 12 r^-(d+3), + v_r = (b - k r^3/2, -k r^2, 0, 12k, 0, ..., 0), + U_0 = (f, f_x, f_xx, f_xxx, f_y1, f_xy1, ..., f_ym, f_xym)(0), + v_0 = (b, 0, 0, 12k, 0, ..., 0). (N1) + +The `check.py` controls verify the first two lines exactly for `d = 2..6`. + +For one smooth unconditioned sample F, define + + F_r(q) = F(q) + C_r(q) Sigma_r^-1 (v_r - U_r(F)), + +with `Sigma_r = Cov U_r(F)` and `C_r(q) = Cov(F(q), U_r(F))`. This is [R] §2's regression formula. Gaussian regression +gives `law(F_r) = Q_r`, and `U_r(F_r) = v_r` exactly. + +**Pathwise convergence.** Each row of `U_r(F)` converges to its row of `U_0(F)` for every smooth F. The fourth axial +row is an averaged third derivative ([P] §3): its two Taylor contributions are `(r^2/4) F_xxx` and `(r^2/12) F_xxx`. +The transverse rows are averages and difference quotients of `f_yj`. + +[P] §2's rapidly summable positive spectrum gives: +- `C_r -> C_0` in global `C^4`; +- `Sigma_r -> Sigma_0`, which is positive definite by [P] §3, so `Sigma_r^-1 -> Sigma_0^-1`. + +Hence, on the full-probability event that F is smooth, + + ||F_r - F_0||_(C^4(T_L^d)) -> 0. (N2) + +This holds along the whole continuous family `r -> 0` at fixed `(b, k, R)`, and `F_0` has the regression law at +`U_0 = v_0`. + +**The transverse block has a density.** Adjoin the `m(m+1)/2` entries `f_(yi yj)(0)`, `i <= j`, to `U_0`. They are +distinct derivative functionals, so [P] §2–§3 make the enlarged covariance positive definite. Hence + + A = D_y^2 F_0(0) has a nondegenerate Gaussian density on Sym(m), (N3) + +and correlations with the rest of the field are retained. + +`{det A = 0}` is the zero set of a nonzero polynomial on `Sym(m)`, so it has Lebesgue measure 0 and probability 0. In +particular `P(lambda_max(A) = 0) = 0`. + +### 2.2 The complete local ridge + +Fix a sample satisfying (N2), (N10) below, and `A < 0`. Choose `a_0 > 0` with `A <= -a_0 I`. Let `B_eta` be the closed +ball of radius `eta` in `R^m`. + +**Choice of the box.** +- By continuity, choose `eta > 0` and `delta_1 > 0` such that `D_y^2 F_0 <= -(a_0/2) I` on + `Q = [-delta_1, delta_1] x B_eta`. +- Since `grad_y F_0(0) = 0`, shrink to `delta <= delta_1` so that `|grad_y F_0(x, 0)| <= a_0 eta/8` for `|x| <= delta`. +- By (N2), for all small `r`, on `Q_delta = [-delta, delta] x B_eta`: + + D_y^2 F_r <= -(a_0/4) I, |grad_y F_r(x, 0)| <= a_0 eta/6. (N4a) + +**Transverse uniqueness.** Fix `|x| <= delta` and `|y| = eta`. Then + + = + int_0^1 y^T D_y^2 F_r(x, t y) y dt + <= (a_0 eta/6) eta - (a_0/4) eta^2 < 0. + +So `y -> F_r(x, y)` is strictly concave on the convex ball `B_eta`, and its gradient points strictly inward on the +boundary sphere. +- Its maximum over `B_eta` is attained in the interior, so it is a critical point. +- A strictly concave function has at most one critical point in a convex set, because any critical point is its + unique maximizer. + +Hence for every `|x| <= delta` there is exactly one `y = psi_r(x)` in the open ball with `grad_y F_r(x, psi_r(x)) = 0`. +This replaces C52's planar intermediate-value step. + +**Regularity of the ridge.** The implicit function theorem gives `psi_r` in `C^3`, because `D_y^2 F_r` is invertible +and `F_r` is in `C^4`. +- Strong monotonicity of `-grad_y F_r` gives `|psi_r(x) - psi_0(x)| <= (4/a_0) sup |grad_y F_r - grad_y F_0|`. +- The derivatives of `psi_r` are rational in derivatives of `F_r` through order four. Their only denominators are + `(D_y^2 F_r)^-1`, with norm at most `4/a_0`. For example `psi_r' = -(D_y^2 F_r)^-1 F_r,xy` on the ridge. +- Hence `psi_r -> psi_0` in `C^3([-delta, delta])`. + +**The reduced function.** Put `g_r(x) = F_r(x, psi_r(x))` and `v = (1, psi_r'(x))`. Differentiating +`grad_y F_r(x, psi_r(x)) = 0` gives `D^2 F_r[v, (0, w)] = 0` for every `w` in `R^m`. The chain rule then gives + + g_r' = F_r,x = D F_r[v], + g_r'' = D^2 F_r[v, v] + D F_r[(0, psi_r'')] = D^2 F_r[v, v], + g_r''' = D^3 F_r[v, v, v] + 3 D^2 F_r[v, (0, psi_r'')] + D F_r[(0, psi_r''')] + = D^3 F_r[v, v, v]. (N4) + +Substituting `psi_r' = -(D_y^2 F_r)^-1 F_r,xy`: + + g_r'' = F_r,xx - F_r,xy^T (D_y^2 F_r)^-1 F_r,xy =: s_r, (N5) + +which is the Schur complement of the transverse block in the Hessian. Two exact checks support these: +- `check.py` verifies (N4), (N5) and `psi' = -(D_y^2 F)^-1 F_xy` exactly, by power series of the implicit ridge, on + random rational quartics with `m = 1..5`. +- It also checks that `g'''` differs from the raw axial `F_xxx` off contact. The ridge correction is real. + +**Contact values.** By (N1), `F_0,xy(0) = 0`, so `psi_0'(0) = 0`. Hence + + g_0'(0) = g_0''(0) = 0, g_0'''(0) = F_0,xxx(0) = 12k > 0. + +**Exactly two local critical points.** Shrink `delta` so that `g_0''' >= 9k` on `[-delta, delta]`. By (N2), (N4) and +`C^3` convergence of `psi_r`, `g_r''' >= 6k` there for small `r`, so `g_r'` is strictly convex. +- At the pins, `grad F_r = 0`, so `grad_y F_r(+-r/2, 0) = 0`. Transverse uniqueness gives `psi_r(+-r/2) = 0`, and then + `g_r'(+-r/2) = 0`. +- A strictly convex function has at most two zeros. +- Every critical point of `F_r` in `Q_delta` lies on the ridge. + +Hence `M_r` and `S_r` are the only critical points of `F_r` in `Q_delta`. This holds at every intermediate scale +within the fixed box at once. + +**Types.** `g_r''` is strictly increasing, and `g_r'` vanishes at both pins, so `g_r''(-r/2) < 0 < g_r''(r/2)`. +Haynsworth's inertia additivity for `H = [[F_xx, F_xy^T], [F_xy, D_y^2 F]]` with invertible `D_y^2 F < 0` gives + + In(H) = In(D_y^2 F) + In(s) = (m, 0, 0) + In(s). (N6) + +So: +- `M_r` is a nondegenerate maximum; +- `S_r` is a nondegenerate saddle of index `m = d - 1`. + +`check.py` verifies (N6) by exact symmetric elimination for `d = 2..6`. This is a statement about Hessian type, not +about elder matching. + +**The contact field.** At `r = 0`, `g_0'(x) > 0` for every `x != 0` in `[-delta, delta]`. So `0` is the only critical +point of `F_0` in `Q_delta`. + +### 2.3 Conditional genericity of remote critical points and values + +This section concerns the contact law of `F_0` at fixed `(b, k, R)`. Consider the maps: + + Z_M(x, v) = (grad F_0(x), H F_0(x) v) in R^(2d), x != 0, |v| = 1, (q, p) = (2d-1, 2d), + Z_V(x, z) = (grad F_0(x), grad F_0(z), F_0(x) - F_0(z)) in R^(2d+1), + x != z, both != 0, (q, p) = (2d, 2d+1), + Z_b(x) = (grad F_0(x), F_0(x) - b) in R^(d+1), x != 0, (q, p) = (d, d+1). (N7) + +These are [P] §8's counts, and `check.py` lists them for `d = 2..6`; each has `p - q = 1`. For `d = 2` they are C52's +`(3,4)`, `(4,5)` and `(2,3)`. + +**Positive conditional covariance.** Suppose a nonzero combination of the entries had zero variance modulo `U_0`. By +[P] §2, `Var(T f) = sum_n a_n |T^(n)|^2` with every `a_n > 0`, and every Fourier coefficient of the corresponding +distribution `T` vanishes. Hence `T = 0` as a distribution on `T_L^d`. Its remote part is supported away from `0`, and +then: +- **`Z_M`.** The second-order part at `x` is `sum_ij beta_i v_j d_i d_j delta_x`, with symbol `(beta . xi)(v . xi)`. + This polynomial vanishes identically only if `beta = 0`, since `v != 0`. Equivalently, `H -> H v` maps `Sym(d)` + onto `R^d`; `check.py` checks the rank. The first-order part then vanishes as well. +- **`Z_V`.** The parts at the distinct supports `x` and `z` each have order zero and order one. They vanish + separately. +- **`Z_b`.** The argument is the same; the constant `b` shifts only the mean. + +**Zero exclusion.** +- Exhaust each domain by countably many compact charts at positive distance from `0`, and for `Z_V` also from the + diagonal. Cover the sphere by finitely many charts. +- Covariance continuity and positivity bound the Gaussian density uniformly on each chart, whatever the conditional + mean. +- On `{||Z||_(C^1) <= N}`, an `epsilon`-mesh and a union bound give probability `O(N^p epsilon^(p-q))`, which tends to + 0. Then take the union over `N`. + +Hence, almost surely: + + every off-origin critical point of F_0 is nondegenerate; + distinct off-origin critical points have distinct values; + no off-origin critical point has value b. (N10) + +A degenerate critical point `x` would give a zero of `Z_M` at a unit kernel vector `v`. + +### 2.4 Global root exhaustion and value separation + +This step is dimension-free; it is C52 §6 verbatim in `T_L^d`. Take a closed box `V` inside `Q_delta` with `0` in its +interior. +- Outside `int V`, `F_0` has finitely many critical points `p_1, ..., p_n`, all nondegenerate. An accumulation point + would be a degenerate critical point, contradicting (N10). +- The contraction `q -> q - H_j^-1 grad F_r(q)` on small balls `B_j` gives exactly one nondegenerate continued root + `p_j(r) -> p_j` in each. +- On the compact remainder, `|grad F_0|` has a positive minimum, so `F_r` has no critical point there for small `r`. +- §2.2 exhausts `V`. + +Hence the full critical set of `F_r` is eventually + + {M_r, S_r, p_1(r), ..., p_n(r)}. (N11) + +Let `Delta` be the minimum of 1 and of every `|v_j - b|` and `|v_i - v_j|` (`i != j`), where `v_j = F_0(p_j)`. Then +`Delta > 0` by (N10). For small `r`, every critical-value gap involving a remote point is at least `Delta/2`. The two +pins differ by exactly `k r^3`. + +Once `tau(r) < Delta/2`: +- a bar of lifetime at most `tau(r)` has its two endpoints among critical points whose values differ by less than + `Delta/2`; +- so its endpoints are `M_r` and `S_r`; +- a maximum births at most one bar. + +Hence `K_(tau(r))(F_r) <= 1`. The local pair is not asserted to be an actual elder pair; if it is not, the count is 0. + +### 2.5 The typed boundary and the weighted vanishing statement + +- **On `{A < 0}`,** §2.4 makes the event in (N0) eventually false. +- **On `{lambda_max(A) > 0}`,** let `w` be a unit eigenvector with `w^T A w > 0`. By (N2) and `M_r -> 0`, + `D_y^2 F_r(M_r) -> A`, so `(0, w)^T H_(M_r) (0, w) > 0` eventually. Then `H_(M_r)` is not negative definite, and + `W_r(F_r) = 0` eventually. +- **The remaining event** `{lambda_max(A) = 0}` has probability 0 by (N3). + +This proves (N0). + +[P] (4.1), (5.1) and (5.3) give, in every `d`, uniformly bounded moments of `W_r/r^2` of every finite order on a +compact neighbourhood of the fixed target ([P] §5: "det H_i/r and W_r/r^2 have uniformly bounded moments of every +finite order"). Almost-sure convergence plus uniform integrability give + + E[(W_r(F_r)/r^2) 1{K_(k r^3/y)(F_r) >= 2}] -> 0, (N12) + +and the same holds after multiplication by the actual elder indicator `0 <= J_eld <= 1`. This is an UNNORMALIZED +expectation; no lower floor for `Z_r` is used. + +## 3. The weighted counting identity in dimension d + +Let `H_tau(f) = 1{K_tau(f) >= 2}`. It is a bounded Borel whole-field mark on the Morse distinct-value locus, and is 0 +off it. [E2]'s finite-measure identity on location x `C^2` field space admits it. + +Counting once per actual finite bar gives + + B_tau = E sum_{(M,S) actual, 0 < ell <= tau} H_tau(f). (C) + +Use midpoint stationarity and the directed separation `S - M = r u`, with `u` in `S^(d-1)`. [P] §10's ledger is + + spatial r^(d-1) x height r^3 x pin 12 r^-(d+3) x determinant r^2 = 12 r, + +which is checked in `check.py` for `d = 2..6`. The near marked intensity per unit volume is therefore + + r A_r^(H_tau)(q) dr dq, + A_r^(H_tau) = 12 pi_r(v_r) E_Q[(W_r/r^2) J_eld H_tau] <= A_r, q = (b, k, u). (C1) + +For `ell = k r^3` and `y = ell/tau`, `r dr = tau^(2/3) y^(-1/3) dy/(3 k^(2/3))`, also checked exactly. Hence + + B_tau^near/(L^d tau^(2/3)) + = int_0^1 int_{R x (0,inf) x S^(d-1)} 1{k >= tau y/r_0^3} y^(-1/3)/(3 k^(2/3)) + A_{(tau y/k)^(1/3)}^(H_tau)(q) dsigma db dk dy. (C2) + +## 4. Proof of Theorem O_d + +**Near part.** For fixed `q` and `y`, `r = (tau y/k)^(1/3) -> 0` and `tau = k r^3/y`. By (N12) and continuity of +`pi_r(v_r)` at fixed `q`, `A_r^(H_tau)(q) -> 0`. [P] (13.4) gives, for all `b`, all `k > 0` and `0 < r <= r_0`, + + 0 <= A_r^(H_tau)(q) <= A_r(q) <= H(b, k) = C (1 + |b| + k)^(2d) exp[-c(b^2 + k^2)]. + +The dominating function `y^(-1/3) H(b, k)/(3 k^(2/3))` is integrable on `(0,1] x R x (0, inf) x S^(d-1)`: +- `int y^(-1/3) = 3/2`; +- `k^(-2/3)` is integrable at 0; +- Gaussian tails control the polynomial; +- `S^(d-1)` has finite measure. + +Dominated convergence gives `B_tau^near = o(L^d tau^(2/3))`. + +**Far part.** For `r >= r_0`, `H_tau <= 1`, and [P] (14.1) gives `nu_eld^far(ell) <= C` for `0 < ell <= 1`. So +`B_tau^far <= L^d C tau = o(tau^(2/3))`. Near and far cover all ordered distinct endpoint pairs. This proves (O1). + +**(O2) and (O3).** For every integer `K >= 0`, +- `K = 1{K > 0} + (K - 1)_+`; +- `(K - 1)_+ <= K 1{K >= 2}`; +- `2 P(K >= 2) <= E[K 1{K >= 2}]`. + +[P] Theorem C, (1.3), gives `nu_eld^all(ell) ~ c_{d,L} ell^(-1/3)` per unit volume. Integrating over `(0, tau]` gives +`m_tau = L^d (3/2) c_{d,L} tau^(2/3) + o(tau^(2/3))` ([P] §12). With (O1) this yields (O2). Then +`TV(law(K_tau | K_tau > 0), delta_1) = P(K_tau >= 2)/p_tau <= B_tau/(2 p_tau) -> 0`, which is (O3). + +**(O4).** Let `U_tau` be the empirical probability measure on a field's short bars, `I_tau = E[K_tau U_tau]/m_tau` and +`F_tau = E[1{K_tau > 0} U_tau]/p_tau`. Then + + I_tau = (p_tau/m_tau) F_tau + (e_tau/m_tau) D_tau, D_tau = E[(K_tau - 1)_+ U_tau]/e_tau, + +and therefore `TV(F_tau, I_tau) <= e_tau/m_tau`. This is dimension-free and uniform over marks. If `e_tau = 0`, the two +laws agree. + +**(O5).** [T] Proposition 3 / (T4) is stated for `q` in `R x (0, inf) x S^(d-1)` and every `d >= 2`. It gives +`I_tau -> (2/3) y^(-1/3) dy g(q) dq` in total variation, with `g = A_0/(3 c k^(2/3))` and zero cemetery mass. (O4) +transfers this to `F_tau`. The coefficient is [P] (15.2): + + c_{d,L} = Gamma(7/6)/(24^(1/3) sqrt(pi)) + int_{S^(d-1)} p_G(0) p_(V_u)(0) tau_u^(4/3) D_u dsigma(u) > 0. + +Unbounded mark moments do not converge without a separate uniform-integrability argument. + +## 5. Boundaries + +- Every source interface is a retained hypothesis: + - the actual global elder identification; + - Theorem C's positive leading mean; + - (13.4) and (14.1); + - E2's Borel-mark identity; + - T's (T4). + + This packet does not reaccept any of them. +- The count is of actual ordinary finite bars. It is not a uniqueness theorem for auxiliary witnesses or for + replacement bars. C50/C51 (Math-#233, #234) are not premises. +- `d` and `L` are fixed. No uniformity in `d` is claimed. Constants and thresholds depend on `d`, `L` and the sample. +- Same account as every other lane, so organizational-independence credit is 0. Dylan Roy's personal reading is + PENDING. + +## 6. Exact controls + +`check.py` uses the standard library and rationals only. It checks the finite identities: +- (N1) `|det T_r| = 12 r^-(d+3)` and `T_r(pins) = v_r`; +- (N4) and (N5) by exact power series of the implicit ridge, together with the contact values; +- (N6) Haynsworth inertia; +- the mesh counts and the rank of `H -> H v`; +- the ledger exponent; +- the lifetime Jacobian. + +These cover `d = 2..6`. `test_check.py` adds unit tests and 17 implementation mutants. Each mutant must fail in both +`-B -S` and `-B -O -S`. `verify_sources.py` authenticates the seven `current_required` sources by bytes, SHA256 and Git +blob. + +The controls do not prove the continuum analysis, including: +- genericity; +- uniform integrability; +- dominated convergence; +- the persistence identification. + +## 7. Requested nonauthor review (OpenAI / xAI lanes) + +- **Slice A, §2.2:** the ball argument for transverse uniqueness, the `C^3` ridge convergence, (N4)–(N6), and the + two-zero conclusion. +- **Slice B, §§2.1, 2.3, 2.5:** the density of `A` on `Sym(m)`, the `{lambda_max(A) = 0}` null boundary, the + conditional covariance positivity for (N7), and the uniform integrability. +- **Slice C, §§0, 3–5:** the source scope in general `d`, (C1)–(C2), the domination, and the occurrence and mark + conclusions. This includes checking that [T] (T4) and [E2] are indeed used only within their stated general-d scope. diff --git a/frontiers/ordinary_short_bar_occurrence_all_d_20261001/README.md b/frontiers/ordinary_short_bar_occurrence_all_d_20261001/README.md new file mode 100644 index 000000000..e0b31ca4a --- /dev/null +++ b/frontiers/ordinary_short_bar_occurrence_all_d_20261001/README.md @@ -0,0 +1,44 @@ +# Ordinary short-bar occurrence in every dimension + +This packet extends OpenAI/Codex's planar C52 theorem (Math-#235) to the periodized Gaussian field on `T_L^d` for every +`d >= 2`. A field that contains a sufficiently short ordinary finite superlevel H0 bar asymptotically contains only one +such bar. The probability that one occurs has the same leading coefficient, `L^d (3/2) c_{d,L} tau^(2/3)`, as the +expected count. Sampling a bar after conditioning the field on occurrence has the same limiting mark law as the +intensity calculation. + +[Theorem and proof](NOTE.md) · [Exact sources](SOURCES.json) + +**What is new.** The only new step is ordinary-fold isolation in dimension `d` (NOTE §2): +- the transverse ridge on a ball; +- the identities `g''' = D³F[v,v,v]` and `g'' = Schur complement`; +- Haynsworth inertia for the pin types; +- the `{lambda_max(A) = 0}` null boundary; +- the general-`d` mesh counts. + +The consumer (NOTE §§3–4) is C52's, written out with `L^d`, `S^(d-1)` and `c_{d,L}`. For `d = 2` it is C52's Theorem O. + +**Conditional.** The theorem retains the imported elder-pairing, Kac–Rice and Gaussian interfaces of the seven pinned +sources, all of which are stated for every `d >= 2`. + +**Not supplied:** +- a rate; +- factorial moments or a Poisson law; +- an increasing-volume limit; +- uniformity in `d`. + +Scientific effect NONE; C8 OPEN. + +Run from the repository root: + +```sh +python3 -B -S frontiers/ordinary_short_bar_occurrence_all_d_20261001/verify_sources.py +python3 -B -S frontiers/ordinary_short_bar_occurrence_all_d_20261001/check.py +python3 -B -S frontiers/ordinary_short_bar_occurrence_all_d_20261001/test_check.py -v +python3 -B -O -S frontiers/ordinary_short_bar_occurrence_all_d_20261001/test_check.py -v +python3 -B -S frontiers/ordinary_short_bar_occurrence_all_d_20261001/test_check.py --mutants +``` + +The exact rational controls check the finite identities for `d = 2..6`. They do not prove the continuum analysis. + +Author lane: Anthropic / Claude, under Dylan Roy's delegation; personal reading PENDING. Every lane uses the same +account, so organizational-independence credit is 0. diff --git a/frontiers/ordinary_short_bar_occurrence_all_d_20261001/SOURCES.json b/frontiers/ordinary_short_bar_occurrence_all_d_20261001/SOURCES.json new file mode 100644 index 000000000..28674a694 --- /dev/null +++ b/frontiers/ordinary_short_bar_occurrence_all_d_20261001/SOURCES.json @@ -0,0 +1,100 @@ +{ + "version": 1, + "object": "C52-ALL-D-ORDINARY-SHORT-BAR-OCCURRENCE-20261001-v1", + "scientific_effect": "NONE", + "status": "additive conditional consumer; mandatory P/CAP/E1/E2/REC reading rule retained; no source reacceptance", + "current_required": [ + { + "key": "P", + "path": "imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md", + "commit": "7fe06b01489af8181e53f26d520810829f146094", + "blob": "dfed3b8d318a3ab1950957f393307733a4bef3f2", + "bytes": 40261, + "sha256": "9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7", + "local_path": "imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md", + "role": "lifetime parent: Sections 2-5, 8, 10, 13-15 in every d>=2" + }, + { + "key": "CAP", + "path": "imports/lifetime_parent_20260925/MARKED_CYLINDER_CAP_PROOF.md", + "commit": "7fe06b01489af8181e53f26d520810829f146094", + "blob": "0633aca3c2a2882b0de4399da0a75d64c2e6b2e1", + "bytes": 15160, + "sha256": "0bf922b9203c29088b12388807aa0e2ecd020485eb0f6e919679841b5b2636fc", + "local_path": "imports/lifetime_parent_20260925/MARKED_CYLINDER_CAP_PROOF.md", + "role": "deterministic cap predecessor (d>=2)" + }, + { + "key": "E1", + "path": "imports/lifetime_parent_20260925/ERRATUM_CONGRUENCE.md", + "commit": "7fe06b01489af8181e53f26d520810829f146094", + "blob": "213594d6ca6a86fb938110f4d166d9ce275a02d0", + "bytes": 1782, + "sha256": "bad7ef609c4ad8c41ad6af562c1b6807921e19a9d556ed793ad1a0db6e202028", + "local_path": "imports/lifetime_parent_20260925/ERRATUM_CONGRUENCE.md", + "role": "corrected endpoint congruence" + }, + { + "key": "E2", + "path": "reviews/d1_section9_borel_repair_20260925/REPAIR.md", + "commit": "7fe06b01489af8181e53f26d520810829f146094", + "blob": "fe9b9ce4999908bb3814b500ee2d0ceb0c6f704a", + "bytes": 9062, + "sha256": "845abf9f9c99d672c2a10a887b5a2e7206a3d2de3d876f35f75ff6e2dc13e62f", + "local_path": "reviews/d1_section9_borel_repair_20260925/REPAIR.md", + "role": "replacement Section 9: Borel elder mark in weighted pair Kac-Rice" + }, + { + "key": "REC", + "path": "reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md", + "commit": "7fe06b01489af8181e53f26d520810829f146094", + "blob": "75da2597971510f843f8d90c743950cb8c177342", + "bytes": 23312, + "sha256": "451b9d7ffee072a73fc904cab891b6693e3f233808b89df10cce1b57036b65da", + "local_path": "reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md", + "role": "mandatory reading rule, W1, embedding radius; fixed d>=2" + }, + { + "key": "R", + "path": "frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md", + "local_path": "frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md", + "commit": "7fe06b01489af8181e53f26d520810829f146094", + "bytes": 17734, + "sha256": "380b7d0abdb0fe2de5a6564565af9560d3f1b1ce22fd5538927db0c52f4f3a4a", + "blob": "247b3ecf80bfbe896948d5d489b2d5842a81c481", + "role": "Section 2 whole-field regression coupling formula" + }, + { + "key": "T", + "path": "frontiers/short_bar_endpoint_law_20261001/PROOF.md", + "local_path": "frontiers/short_bar_endpoint_law_20261001/PROOF.md", + "commit": "7fe06b01489af8181e53f26d520810829f146094", + "bytes": 13815, + "sha256": "4fc567b5bed7967bba7b7fc609da8219b6cd2c605e9291b7b82c8a538ced1a29", + "blob": "0d47dbc1d92863d8c51b918aa47d1fa8b605cfdc", + "role": "Proposition 3 / (T4): ordinary-bar marked intensity law in every d>=2" + } + ], + "cited_unmerged": [ + { + "key": "C52-FOLD", + "path": "frontiers/ordinary_short_bar_occurrence_20261001/FOLD_ISOLATION.md", + "pr": "Math-#235", + "commit": "c46377738b711a5cc2114b58bf7726ae6e7bc553", + "blob": "a3d4e7c4c4c23d22af9d259db74afc9ba6fdac1e", + "bytes": 20771, + "sha256": "3889a0898901d03716d277e3afc2964bdbc7566d3a85803c4ad73673bdff1b52", + "role": "source of the planar argument generalized here; not consumed as a premise; d=2 case" + }, + { + "key": "C52-PROOF", + "path": "frontiers/ordinary_short_bar_occurrence_20261001/PROOF.md", + "pr": "Math-#235", + "commit": "c46377738b711a5cc2114b58bf7726ae6e7bc553", + "blob": "69ff20a6c514629373f3ad12eb2db2a2596777d6", + "bytes": 14146, + "sha256": "16d2c5f6c1fe45dd6ce8f6b69455db4908b8e6319e57d58c4ad7c9d1881bdd4d", + "role": "source of the planar consumer (Sections 3-6) generalized here; not consumed as a premise" + } + ] +} diff --git a/frontiers/ordinary_short_bar_occurrence_all_d_20261001/check.py b/frontiers/ordinary_short_bar_occurrence_all_d_20261001/check.py new file mode 100644 index 000000000..514f63fec --- /dev/null +++ b/frontiers/ordinary_short_bar_occurrence_all_d_20261001/check.py @@ -0,0 +1,373 @@ +"""Exact rational controls for C52-ALL-D (NOTE.md section 6). Standard library only. + +These check the finite identities that the general-d proof uses; they do not prove the continuum statements. + + 1. pin_transform: the exact contact transformation T_r of [P] (3.1) in dimension d, |det T_r| = 12 r^-(d+3), and the + image of the physical pin values is the target v_r of [P] (3.3). + 2. ridge_jets: for a polynomial F in (x, y_1..y_m) with grad_y F(0) = 0 and D_y^2 F(0) invertible, the transverse + critical curve psi(x) is computed as an exact power series; g(x) = F(x, psi(x)) then satisfies + g'(0) = F_x(0), g''(0) = F_xx - F_xy^T (D_y^2 F)^-1 F_xy (Schur complement), + g'''(0) = D^3 F(0)[v, v, v], v = (1, psi'(0)). (N4), (N5) + 3. inertia: a symmetric matrix whose transverse block is negative definite has m negative eigenvalues plus the sign + of its Schur complement (Sylvester, exact LDL^T). (N6) + 4. mesh_counts: parameter and range dimensions of the three overdetermined maps of (N8), with p - q = 1. + 5. hv_rank: H -> H v from symmetric d x d matrices onto R^d has rank d for v != 0 (the symbol step of (N7)). + 6. ledger: spatial (d-1) + height 3 - pin (d+3) + determinant 2 = 1, and the lifetime Jacobian + r dr = tau^(2/3) y^(-1/3) dy / (3 k^(2/3)) at exact cubes. + + python3 -B -S check.py""" +from fractions import Fraction as Fr +from itertools import product +import random +import sys + + +# ---------------------------------------------------------------------------------------------- linear algebra +def det(M): + A = [[Fr(v) for v in row] for row in M] + n, s = len(A), Fr(1) + for i in range(n): + p = next((j for j in range(i, n) if A[j][i] != 0), None) + if p is None: + return Fr(0) + if p != i: + A[i], A[p] = A[p], A[i] + s = -s + s *= A[i][i] + for j in range(i + 1, n): + f = A[j][i] / A[i][i] + if f: + A[j] = [a - f * b for a, b in zip(A[j], A[i])] + return s + + +def rank(M): + A = [[Fr(v) for v in row] for row in M] + rk, cols = 0, len(A[0]) if A else 0 + for c in range(cols): + p = next((j for j in range(rk, len(A)) if A[j][c] != 0), None) + if p is None: + continue + A[rk], A[p] = A[p], A[rk] + for j in range(len(A)): + if j != rk and A[j][c]: + f = A[j][c] / A[rk][c] + A[j] = [a - f * b for a, b in zip(A[j], A[rk])] + rk += 1 + return rk + + +def solve(M, b): + n = len(M) + A = [[Fr(v) for v in M[i]] + [Fr(b[i])] for i in range(n)] + for i in range(n): + p = next(j for j in range(i, n) if A[j][i] != 0) + A[i], A[p] = A[p], A[i] + for j in range(n): + if j != i and A[j][i]: + f = A[j][i] / A[i][i] + A[j] = [a - f * c for a, c in zip(A[j], A[i])] + return [A[i][n] / A[i][i] for i in range(n)] + + +def inertia(S): + """(negatives, zeros, positives) of a symmetric rational matrix, by exact symmetric elimination with pivoting on + the diagonal where possible (Sylvester's law of inertia)""" + A = [[Fr(v) for v in row] for row in S] + neg = zer = pos = 0 + while A: + n = len(A) + i = next((j for j in range(n) if A[j][j] != 0), None) + if i is None: + j = next(((a, b) for a in range(n) for b in range(n) if A[a][b] != 0), None) + if j is None: + zer += n + break + a, b = j # congruence e_a -> e_a + e_b makes a diagonal entry nonzero + for c in range(n): + A[a][c] += A[b][c] + for c in range(n): + A[c][a] += A[c][b] + continue + p = A[i][i] + neg, pos = neg + (p < 0), pos + (p > 0) + rest = [j for j in range(n) if j != i] + A = [[A[r][c] - A[r][i] * A[i][c] / p for c in rest] for r in rest] + return neg, zer, pos + + +# ---------------------------------------------------------------------------------------------- 1. pin transform +def pin_transform(d, r): + """rows of T_r acting on O_r = (f(a), f_x(a), f(c), f_x(c), f_y1(a), f_y1(c), ..., f_ym(a), f_ym(c))""" + r = Fr(r) + m = d - 1 + n = 4 + 2 * m + T = [[Fr(0)] * n for _ in range(n)] + T[0][0] = T[0][2] = Fr(1, 2) # (f(a) + f(c))/2 + T[1][0], T[1][2] = -1 / r, 1 / r # (f(c) - f(a))/r + T[2][1], T[2][3] = -1 / r, 1 / r # (f_x(c) - f_x(a))/r + s = 6 / r ** 2 # (6/r^2)[f_x(a) + f_x(c) - 2(f(c) - f(a))/r] + T[3][1] = T[3][3] = s + T[3][0], T[3][2] = 2 * s / r, -2 * s / r + for j in range(m): + ia, ic = 4 + 2 * j, 5 + 2 * j + T[ia][ia] = T[ia][ic] = Fr(1, 2) + T[ic][ia], T[ic][ic] = -1 / r, 1 / r + return T + + +def pin_target(d, r, b, k): + r, b, k = Fr(r), Fr(b), Fr(k) + O = [b, Fr(0), b - k * r ** 3, Fr(0)] + [Fr(0)] * (2 * (d - 1)) + T = pin_transform(d, r) + return [sum(t * o for t, o in zip(row, O)) for row in T] + + +def expected_target(d, r, b, k): + r, b, k = Fr(r), Fr(b), Fr(k) + return [b - k * r ** 3 / 2, -k * r ** 2, Fr(0), 12 * k] + [Fr(0)] * (2 * (d - 1)) + + +def det_constant(d): + return 12 + + +def det_exponent(d): + return d + 3 + + +# ---------------------------------------------------------------------------------------------- 2. ridge jets +NS = 4 # series kept mod x^NS + + +def s_mul(a, b): + out = [Fr(0)] * NS + for i, u in enumerate(a): + if u: + for j in range(NS - i): + out[i + j] += u * b[j] + return out + + +def s_pow(a, e): + out = [Fr(1)] + [Fr(0)] * (NS - 1) + for _ in range(e): + out = s_mul(out, a) + return out + + +def poly_eval_series(F, xs, ys): + """F: dict exponent tuple (ex, ey_1..ey_m) -> coeff; xs, ys: series""" + out = [Fr(0)] * NS + for e, c in F.items(): + t = s_pow(xs, e[0]) + for yj, ej in zip(ys, e[1:]): + t = s_mul(t, s_pow(yj, ej)) + out = [o + c * v for o, v in zip(out, t)] + return out + + +def poly_deriv(F, i): + out = {} + for e, c in F.items(): + if e[i]: + f = list(e) + f[i] -= 1 + out[tuple(f)] = out.get(tuple(f), 0) + c * e[i] + return out + + +def poly_at0(F): + return Fr(F.get(tuple([0] * len(next(iter(F)))), 0)) if F else Fr(0) + + +def ridge_series(F, m): + """psi(x) as series with grad_y F(x, psi(x)) = O(x^NS), psi(0) = 0 (requires grad_y F(0) = 0)""" + Fy = [poly_deriv(F, 1 + j) for j in range(m)] + J = [[poly_at0(poly_deriv(Fy[i], 1 + j)) for j in range(m)] for i in range(m)] + xs = [Fr(0), Fr(1)] + [Fr(0)] * (NS - 2) + psi = [[Fr(0)] * NS for _ in range(m)] + for _ in range(NS + 1): # each step fixes one more order (Jacobian error O(x)) + res = [poly_eval_series(Fy[i], xs, psi) for i in range(m)] + for n in range(NS): + corr = solve(J, [res[i][n] for i in range(m)]) + for j in range(m): + psi[j][n] -= corr[j] + res = [poly_eval_series(Fy[i], xs, psi) for i in range(m)] + if any(any(v for v in r_) for r_ in res): + raise ArithmeticError('ridge series did not close') + return psi + + +def multilinear0(F, nvar, order, v): + """D^order F(0)[v,...,v] = order! * sum_{|e| = order} c_e v^e""" + fact = 1 + for i in range(2, order + 1): + fact *= i + tot = Fr(0) + for e, c in F.items(): + if sum(e) == order: + t = Fr(c) + for vi, ei in zip(v, e): + t *= Fr(vi) ** ei + tot += t + return fact * tot + + +def ridge_jets(F, m): + psi = ridge_series(F, m) + xs = [Fr(0), Fr(1)] + [Fr(0)] * (NS - 2) + g = poly_eval_series(F, xs, psi) + g1, g2, g3 = g[1], 2 * g[2], 6 * g[3] + v = [Fr(1)] + [psi[j][1] for j in range(m)] + Fx = poly_deriv(F, 0) + Fxx = poly_at0(poly_deriv(Fx, 0)) + Fxy = [poly_at0(poly_deriv(Fx, 1 + j)) for j in range(m)] + Fyy = [[poly_at0(poly_deriv(poly_deriv(F, 1 + i), 1 + j)) for j in range(m)] for i in range(m)] + w = solve(Fyy, Fxy) + schur = Fxx - sum(a * b for a, b in zip(Fxy, w)) + return {'g1': g1, 'g2': g2, 'g3': g3, 'Fx': poly_at0(Fx), 'schur': schur, + 'D2vv': multilinear0(F, m + 1, 2, v), 'D3vvv': multilinear0(F, m + 1, 3, v), + 'psi1': [psi[j][1] for j in range(m)], 'psi1_formula': [-t for t in w], + 'Fxxx': poly_at0(poly_deriv(poly_deriv(Fx, 0), 0))} + + +def random_ridge_poly(m, rng, contact=False): + """random rational quartic in (x, y) with grad_y F(0) = 0 and D_y^2 F(0) negative definite; with contact=True also + F_x(0) = F_xx(0) = 0, F_xy(0) = 0 and F_xxx(0) = 12k: the limiting contact jets (N1)""" + nvar = m + 1 + F = {} + for e in product(range(5), repeat=nvar): + if 1 <= sum(e) <= 4: + F[e] = Fr(rng.randint(-9, 9), rng.randint(1, 5)) + for j in range(m): + e = [0] * nvar + e[1 + j] = 1 + F[tuple(e)] = Fr(0) # F_yj(0) = 0 + # D_y^2 F(0) = -(B B^T + I): coefficients of y_i y_j + B = [[Fr(rng.randint(-3, 3)) for _ in range(m)] for _ in range(m)] + N = [[-(sum(B[i][t] * B[j][t] for t in range(m)) + (1 if i == j else 0)) for j in range(m)] for i in range(m)] + for i in range(m): + for j in range(i, m): + e = [0] * nvar + e[1 + i] += 1 + e[1 + j] += 1 + F[tuple(e)] = N[i][j] / 2 if i == j else N[i][j] + if contact: + k = Fr(rng.randint(1, 7), rng.randint(1, 3)) + F[(1,) + (0,) * m] = Fr(0) + F[(2,) + (0,) * m] = Fr(0) + F[(3,) + (0,) * m] = 2 * k # F_xxx(0) = 3! * 2k = 12k + for j in range(m): + e = [1] + [0] * m + e[1 + j] = 1 + F[tuple(e)] = Fr(0) + return F, k + return F, None + + +# ---------------------------------------------------------------------------------------------- 4-6 +def mesh_counts(d): + """(parameter dim q, range dim p) for Z_M = (grad F(x), H F(x) v), Z_V = (grad F(x), grad F(z), F(x) - F(z)), + Z_b = (grad F(x), F(x) - b)""" + return {'Z_M': (d + (d - 1), 2 * d), 'Z_V': (2 * d, 2 * d + 1), 'Z_b': (d, d + 1)} + + +def hv_matrix(v): + """matrix of H -> H v on independent entries H_ij, i <= j""" + d = len(v) + cols = [(i, j) for i in range(d) for j in range(i, d)] + M = [[Fr(0)] * len(cols) for _ in range(d)] + for c, (i, j) in enumerate(cols): + M[i][c] += v[j] + if i != j: + M[j][c] += v[i] + return M + + +def ledger_exponent(d): + return (d - 1) + 3 - det_exponent(d) + 2 + + +def lifetime_jacobian(tau, y, k): + """r dr/dy at r = (tau y / k)^(1/3), returned as (r^2 / (3 y), tau^(2/3) y^(-1/3) / (3 k^(2/3))) for exact cubes""" + def cbrt(q): + q = Fr(q) + for a in (q.numerator, q.denominator): + c = round(abs(a) ** (1 / 3)) + if c ** 3 != abs(a): + raise ValueError('not a cube') + return Fr(round(q.numerator ** (1 / 3)), round(q.denominator ** (1 / 3))) + tau, y, k = Fr(tau), Fr(y), Fr(k) + r = cbrt(tau * y / k) + lhs = r * r / (3 * y) # r dr/dy, since dr/dy = r/(3y) + rhs = cbrt(tau) ** 2 / (cbrt(y) * 3 * cbrt(k) ** 2) + return lhs, rhs + + +# ---------------------------------------------------------------------------------------------- run +def run(verbose=True, seed=20261001, dims=(2, 3, 4, 5, 6)): + rng = random.Random(seed) + fails = 0 + + def report(ok, msg): + nonlocal fails + fails += not ok + if verbose: + print(('ok ' if ok else 'FAIL ') + msg) + + for d in dims: + for r in (Fr(1, 3), Fr(2, 7), Fr(5, 2)): + D = det(pin_transform(d, r)) + report(abs(D) == det_constant(d) * r ** -det_exponent(d), 'd=%d r=%s |det T_r| = 12 r^-(d+3)' % (d, r)) + report(pin_target(d, r, Fr(-3, 4), Fr(5, 3)) == expected_target(d, r, Fr(-3, 4), Fr(5, 3)), + 'd=%d r=%s T_r(pins) = v_r' % (d, r)) + for d in dims: + m = d - 1 + differs = False + for t in range(3 if d <= 4 else 1): + F, _ = random_ridge_poly(m, rng) + J = ridge_jets(F, m) + differs = differs or J['g3'] != J['Fxxx'] + report(J['g1'] == J['Fx'] and J['g2'] == J['schur'] == J['D2vv'] and J['g3'] == J['D3vvv'] + and J['psi1'] == J['psi1_formula'], + "d=%d ridge #%d: g' = F_x, g'' = Schur = D2F[v,v], g''' = D3F[v,v,v], psi' = -Fyy^-1 Fxy" % (d, t)) + report(differs, "d=%d falsifier: g''' differs from the raw axial F_xxx off contact" % d) + F, k = random_ridge_poly(m, rng, contact=True) + J = ridge_jets(F, m) + report(J['g1'] == 0 and J['g2'] == 0 and J['g3'] == 12 * k and all(p == 0 for p in J['psi1']), + "d=%d contact jets (N1): psi'(0) = 0, g'(0) = g''(0) = 0, g'''(0) = 12k" % d) + for d in dims: + m = d - 1 + for t in range(4): + B = [[Fr(rng.randint(-4, 4)) for _ in range(m)] for _ in range(m)] + Ayy = [[-(sum(B[i][s] * B[j][s] for s in range(m)) + (1 if i == j else 0)) for j in range(m)] + for i in range(m)] + h = [Fr(rng.randint(-5, 5), rng.randint(1, 3)) for _ in range(m)] + w = solve(Ayy, h) + for target in (Fr(-2), Fr(3)): + axx = target + sum(a * b for a, b in zip(h, w)) # Schur complement = target + H = [[axx] + h] + [[h[i]] + Ayy[i] for i in range(m)] + neg, zer, pos = inertia(H) + exp = (m + 1, 0, 0) if target < 0 else (m, 0, 1) + report((neg, zer, pos) == exp, 'd=%d inertia: Schur %s -> %s' % (d, target, exp)) + for d in dims: + mc = mesh_counts(d) + report(all(p - q == 1 for q, p in mc.values()), 'd=%d mesh counts %s, p - q = 1' % (d, mc)) + for t in range(3): + v = [Fr(rng.randint(-3, 3)) for _ in range(d)] + if not any(v): + v[0] = Fr(1) + report(rank(hv_matrix(v)) == d, 'd=%d H -> Hv onto R^d (v = %s)' % (d, [str(x) for x in v])) + report(ledger_exponent(d) == 1, 'd=%d ledger exponent (d-1)+3-(d+3)+2 = 1' % d) + report(mesh_counts(2) == {'Z_M': (3, 4), 'Z_V': (4, 5), 'Z_b': (2, 3)}, 'd=2 reduces to C52 (F7)-(F9) counts') + for tau, y, k in ((Fr(1, 8), Fr(27, 64), Fr(1, 125)), (Fr(8, 27), Fr(1), Fr(64))): + lhs, rhs = lifetime_jacobian(tau, y, k) + report(lhs == rhs, 'lifetime Jacobian at tau=%s y=%s k=%s' % (tau, y, k)) + if verbose: + print('check: %d failures' % fails) + return fails + + +if __name__ == '__main__': + sys.exit(1 if run() else 0) diff --git a/frontiers/ordinary_short_bar_occurrence_all_d_20261001/test_check.py b/frontiers/ordinary_short_bar_occurrence_all_d_20261001/test_check.py new file mode 100644 index 000000000..407a154f0 --- /dev/null +++ b/frontiers/ordinary_short_bar_occurrence_all_d_20261001/test_check.py @@ -0,0 +1,157 @@ +"""Tests and implementation mutants for C52-ALL-D. + + python3 -B -S test_check.py -v # unit tests + python3 -B -S test_check.py --mutants # each mutant of check.py must make the tests fail, in -B -S and -B -O -S""" +from fractions import Fraction as Fr +import os +import random +import shutil +import subprocess +import sys +import tempfile +import unittest + +HERE = os.path.dirname(os.path.abspath(__file__)) +sys.path.insert(0, HERE) +import check as C # noqa: E402 +import verify_sources as V # noqa: E402 + + +class Sources(unittest.TestCase): + def test_seven_sources(self): + self.assertEqual(V.verify(), 7) + + +class PinTransform(unittest.TestCase): + def test_det_and_target(self): + for d in range(2, 8): + for r in (Fr(1, 2), Fr(3, 11)): + self.assertEqual(abs(C.det(C.pin_transform(d, r))), 12 * r ** -(d + 3)) + self.assertEqual(C.pin_target(d, r, 2, Fr(1, 3)), C.expected_target(d, r, 2, Fr(1, 3))) + + def test_target_shape(self): + v = C.expected_target(3, Fr(1, 2), 1, 2) + self.assertEqual(v[:4], [1 - Fr(2, 16), -Fr(1, 2), 0, 24]) + self.assertEqual(len(v), 2 * 3 + 2) + + +class Ridge(unittest.TestCase): + def test_identities(self): + rng = random.Random(7) + for m in (1, 2, 3): + for _ in range(2): + F, _ = C.random_ridge_poly(m, rng) + J = C.ridge_jets(F, m) + self.assertEqual(J['g1'], J['Fx']) + self.assertEqual(J['g2'], J['schur']) + self.assertEqual(J['g2'], J['D2vv']) + self.assertEqual(J['g3'], J['D3vvv']) + self.assertEqual(J['psi1'], J['psi1_formula']) + + def test_contact(self): + rng = random.Random(11) + for m in (1, 2, 3): + F, k = C.random_ridge_poly(m, rng, contact=True) + J = C.ridge_jets(F, m) + self.assertEqual((J['g1'], J['g2'], J['g3']), (0, 0, 12 * k)) + + def test_known_ridge(self): + # F = x^3 + x y - y^2 (m = 1): psi = x/2, g = x^3 + x^2/4; g'' = 1/2, g''' = 6 + F = {(3, 0): Fr(1), (1, 1): Fr(1), (0, 2): Fr(-1)} + J = C.ridge_jets(F, 1) + self.assertEqual(J['psi1'], [Fr(1, 2)]) + self.assertEqual((J['g1'], J['g2'], J['g3']), (0, Fr(1, 2), 6)) + self.assertEqual(J['Fxxx'], 6) + # F = x y^2/2 ... with a curved ridge: F = x y - y^2 + x^2 y: psi = (x + x^2)/2, g = (x + x^2)^2/4 + F = {(1, 1): Fr(1), (0, 2): Fr(-1), (2, 1): Fr(1)} + J = C.ridge_jets(F, 1) + self.assertEqual((J['g2'], J['g3']), (Fr(1, 2), 3)) + self.assertNotEqual(J['g3'], J['Fxxx']) + + +class Inertia(unittest.TestCase): + def test_signatures(self): + self.assertEqual(C.inertia([[1, 0], [0, -1]]), (1, 0, 1)) + self.assertEqual(C.inertia([[0, 1], [1, 0]]), (1, 0, 1)) + self.assertEqual(C.inertia([[-1, 0, 0], [0, -2, 0], [0, 0, 0]]), (2, 1, 0)) + self.assertEqual(C.inertia([[2, 1], [1, -3]]), (1, 0, 1)) + + +class Counts(unittest.TestCase): + def test_mesh(self): + self.assertEqual(C.mesh_counts(2), {'Z_M': (3, 4), 'Z_V': (4, 5), 'Z_b': (2, 3)}) + self.assertEqual(C.mesh_counts(4), {'Z_M': (7, 8), 'Z_V': (8, 9), 'Z_b': (4, 5)}) + + def test_hv(self): + self.assertEqual(C.rank(C.hv_matrix([Fr(0), Fr(0), Fr(1)])), 3) + self.assertEqual(C.rank(C.hv_matrix([Fr(0), Fr(0), Fr(0)])), 0) + + def test_ledger(self): + for d in range(2, 12): + self.assertEqual(C.ledger_exponent(d), 1) + + def test_jacobian(self): + self.assertEqual(*C.lifetime_jacobian(Fr(1, 8), Fr(27, 64), Fr(1, 125))) + + +class Whole(unittest.TestCase): + def test_run(self): + self.assertEqual(C.run(verbose=False), 0) + + +MUTANTS = [ + ("T[0][0] = T[0][2] = Fr(1, 2)", "T[0][0] = T[0][2] = Fr(1, 3)"), + ("s = 6 / r ** 2", "s = 5 / r ** 2"), + ("T[3][0], T[3][2] = 2 * s / r, -2 * s / r", "T[3][0], T[3][2] = s / r, -2 * s / r"), + ("T[ic][ia], T[ic][ic] = -1 / r, 1 / r", "T[ic][ia], T[ic][ic] = -1 / r, 2 / r"), + ("return [b - k * r ** 3 / 2, -k * r ** 2, Fr(0), 12 * k]", "return [b - k * r ** 3 / 2, -k * r ** 2, Fr(0), 6 * k]"), + ("def det_exponent(d):\n return d + 3", "def det_exponent(d):\n return d + 2"), + ("g1, g2, g3 = g[1], 2 * g[2], 6 * g[3]", "g1, g2, g3 = g[1], 2 * g[2], 3 * g[3]"), + ("schur = Fxx - sum(", "schur = Fxx + sum("), + ("v = [Fr(1)] + [psi[j][1] for j in range(m)]", "v = [Fr(1)] + [Fr(0) for j in range(m)]"), + ("'psi1_formula': [-t for t in w]", "'psi1_formula': [t for t in w]"), + ("F[(3,) + (0,) * m] = 2 * k", "F[(3,) + (0,) * m] = k"), + ("return {'Z_M': (d + (d - 1), 2 * d)", "return {'Z_M': (d + d, 2 * d)"), + ("M[i][c] += v[j]\n if i != j:", "M[i][c] += v[j]\n if False:"), + ("return (d - 1) + 3 - det_exponent(d) + 2", "return (d - 1) + 2 - det_exponent(d) + 2"), + ("lhs = r * r / (3 * y)", "lhs = r * r / (2 * y)"), + ("neg, pos = neg + (p < 0), pos + (p > 0)", "neg, pos = neg + (p > 0), pos + (p < 0)"), + ("for _ in range(NS + 1):", "for _ in range(1):"), +] + + +def run_mutants(): + src = open(os.path.join(HERE, 'check.py')).read() + survivors = 0 + for i, (a, b) in enumerate(MUTANTS): + if src.count(a) != 1: + print('mutant %d: anchor not unique/absent: %r' % (i, a)) + survivors += 1 + continue + tmp = tempfile.mkdtemp() + try: + for f in ('test_check.py', 'verify_sources.py', 'SOURCES.json'): + shutil.copy(os.path.join(HERE, f), tmp) + open(os.path.join(tmp, 'check.py'), 'w').write(src.replace(a, b)) + killed = True + for flags in (['-B', '-S'], ['-B', '-O', '-S']): + env = dict(os.environ, C52D_SOURCE_ROOT=HERE) + p = subprocess.run([sys.executable] + flags + [os.path.join(tmp, 'test_check.py'), '--mutant-run'], + capture_output=True, text=True, env=env, timeout=300) + killed = killed and p.returncode != 0 + print('mutant %2d %s' % (i, 'killed (both modes)' if killed else 'SURVIVED')) + survivors += not killed + finally: + shutil.rmtree(tmp) + print('mutants: %d of %d killed' % (len(MUTANTS) - survivors, len(MUTANTS))) + return survivors + + +if __name__ == '__main__': + if '--mutants' in sys.argv: + sys.exit(1 if run_mutants() else 0) + if '--mutant-run' in sys.argv: + sys.argv.remove('--mutant-run') + # sources are verified against the real tree; skip that test in the temporary copy + del Sources + unittest.main() diff --git a/frontiers/ordinary_short_bar_occurrence_all_d_20261001/verify_sources.py b/frontiers/ordinary_short_bar_occurrence_all_d_20261001/verify_sources.py new file mode 100644 index 000000000..7f023e63c --- /dev/null +++ b/frontiers/ordinary_short_bar_occurrence_all_d_20261001/verify_sources.py @@ -0,0 +1,56 @@ +"""Source identity for C52-ALL-D: the seven current_required sources must match bytes, SHA256 and Git blob on the +tree. The two cited_unmerged C52 files (Math-#235) are recorded only; they are not premises. Identity only, not +analytic acceptance. + + python3 -B -S verify_sources.py""" +import hashlib +import json +import sys +from pathlib import Path, PurePosixPath + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +MANIFEST_SHA256 = '44fc416116eca6bbf56c029329930212c0b108ee1bb9174ca8f3b41ad1b78991' + + +def require(cond, msg): + if not cond: + raise ValueError(msg) + + +def contained(rel): + require(isinstance(rel, str) and rel, 'invalid path') + parts = PurePosixPath(rel) + require(not parts.is_absolute() and str(parts) == rel and all(p not in ('', '.', '..') for p in parts.parts), + 'noncanonical path ' + rel) + t = ROOT + for p in parts.parts: + t = t / p + require(not t.is_symlink(), 'symlink ' + rel) + require(t.is_file() and ROOT in t.resolve().parents, 'not a contained regular file: ' + rel) + return t + + +def verify(): + raw = contained('frontiers/ordinary_short_bar_occurrence_all_d_20261001/SOURCES.json').read_bytes() + require(hashlib.sha256(raw).hexdigest() == MANIFEST_SHA256, 'manifest digest') + man = json.loads(raw) + req = man['current_required'] + require(len(req) == 7 and len({e['key'] for e in req}) == 7, 'seven distinct required sources') + for e in req: + data = contained(e['local_path']).read_bytes() + require(type(e['bytes']) is int and len(data) == e['bytes'], 'bytes ' + e['key']) + require(hashlib.sha256(data).hexdigest() == e['sha256'], 'sha256 ' + e['key']) + blob = hashlib.sha1(b'blob ' + str(len(data)).encode() + b'\0' + data).hexdigest() + require(blob == e['blob'], 'blob ' + e['key']) + require(all(e['pr'] == 'Math-#235' for e in man['cited_unmerged']), 'cited entries') + return len(req) + + +if __name__ == '__main__': + try: + n = verify() + except ValueError as exc: + print('source verification FAILED:', exc) + sys.exit(1) + print(json.dumps({'verified_sources': n, 'scope': 'source identity only, not analytic acceptance'})) From 162166b4c40ae2e54b09d8493c655f65d4c3db7b Mon Sep 17 00:00:00 2001 From: Dylan Roy Date: Thu, 1 Oct 2026 19:15:54 +0000 Subject: [PATCH 2/4] C52 all-d v1.1: qualify Lemma F_d item 3; verify commit:path pins Applies the two Codex P2 findings on Math-#236. - NOTE Lemma F_d item 3 and section 2.4 are now stated on {A < 0}, the only case in which section 2.2's local exhaustion is proved. Off that event, section 2.5 shows only that the typed weight vanishes. Theorem O_d is unchanged, since it uses item 3 only on {A < 0}. - verify_sources.py now also checks each historical commit:path against the recorded blob, using git ls-tree --full-tree, then rechecks the bytes. The cited_unmerged C52 entries are checked when their commit is present. New tests cover six rejection cases; the workflow uses fetch-depth: 0. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015wNj8LPTKXsaT68G3DgPPh --- .../ordinary-short-bar-occurrence-all-d.yml | 1 + .../NOTE.md | 13 ++-- .../test_check.py | 19 ++++- .../verify_sources.py | 71 +++++++++++++++---- 4 files changed, 85 insertions(+), 19 deletions(-) diff --git a/.github/workflows/ordinary-short-bar-occurrence-all-d.yml b/.github/workflows/ordinary-short-bar-occurrence-all-d.yml index 42a2ea5a5..f9302704d 100644 --- a/.github/workflows/ordinary-short-bar-occurrence-all-d.yml +++ b/.github/workflows/ordinary-short-bar-occurrence-all-d.yml @@ -35,6 +35,7 @@ jobs: steps: - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 with: + fetch-depth: 0 persist-credentials: false - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 with: diff --git a/frontiers/ordinary_short_bar_occurrence_all_d_20261001/NOTE.md b/frontiers/ordinary_short_bar_occurrence_all_d_20261001/NOTE.md index 5a0fc6e6d..b22b55904 100644 --- a/frontiers/ordinary_short_bar_occurrence_all_d_20261001/NOTE.md +++ b/frontiers/ordinary_short_bar_occurrence_all_d_20261001/NOTE.md @@ -95,8 +95,9 @@ These are `2d + 2` scalar observations. `Q_r` is the whole-field Gaussian regres 1. `F_r -> F_0` almost surely in `C^4(T_L^d)`. 2. Let `A = D_y^2 F_0(0)`. Almost surely on `{A < 0}` (negative definite), for all small `r`, the only critical points of `F_r` in one fixed neighbourhood of `0` are `M_r` and `S_r`. -3. Every other critical point continues a nondegenerate critical point of `F_0`. Their limiting values are pairwise - distinct and differ from `b`. +3. Almost surely on `{A < 0}`, for all small `r`, every other critical point of `F_r` continues a nondegenerate + critical point of `F_0`, and their limiting values are pairwise distinct and differ from `b`. Off `{A < 0}` no + local exhaustion is claimed: there §2.5 shows only that the typed weight vanishes eventually. 4. For each fixed `y` in `(0, 1]`, put `tau(r) = k r^3/y`. Almost surely on `{A < 0}`, `K_(tau(r))(F_r) <= 1` eventually. 5. On the whole coupling space, @@ -278,8 +279,8 @@ A degenerate critical point `x` would give a zero of `Z_M` at a unit kernel vect ### 2.4 Global root exhaustion and value separation -This step is dimension-free; it is C52 §6 verbatim in `T_L^d`. Take a closed box `V` inside `Q_delta` with `0` in its -interior. +This step is dimension-free; it is C52 §6 verbatim in `T_L^d`. It uses §2.2, so it holds on `{A < 0}`, which is fixed +throughout this subsection. Take a closed box `V` inside `Q_delta` with `0` in its interior. - Outside `int V`, `F_0` has finitely many critical points `p_1, ..., p_n`, all nondegenerate. An accumulation point would be a degenerate critical point, contradicting (N10). - The contraction `q -> q - H_j^-1 grad F_r(q)` on small balls `B_j` gives exactly one nondegenerate continued root @@ -418,7 +419,9 @@ Unbounded mark moments do not converge without a separate uniform-integrability These cover `d = 2..6`. `test_check.py` adds unit tests and 17 implementation mutants. Each mutant must fail in both `-B -S` and `-B -O -S`. `verify_sources.py` authenticates the seven `current_required` sources by bytes, SHA256 and Git -blob. +blob. It checks both the working-tree copy and the historical `commit:path -> blob` entry, via `git ls-tree`. The two +`cited_unmerged` C52 entries are checked the same way when their commit is present locally, and otherwise reported as +unavailable; they are not premises. The controls do not prove the continuum analysis, including: - genericity; diff --git a/frontiers/ordinary_short_bar_occurrence_all_d_20261001/test_check.py b/frontiers/ordinary_short_bar_occurrence_all_d_20261001/test_check.py index 407a154f0..40a6db064 100644 --- a/frontiers/ordinary_short_bar_occurrence_all_d_20261001/test_check.py +++ b/frontiers/ordinary_short_bar_occurrence_all_d_20261001/test_check.py @@ -19,7 +19,24 @@ class Sources(unittest.TestCase): def test_seven_sources(self): - self.assertEqual(V.verify(), 7) + n, cited = V.verify() + self.assertEqual(n, 7) + self.assertEqual(set(cited), {'C52-FOLD', 'C52-PROOF'}) + + def test_historical_rejections(self): + import json + man = json.loads((V.HERE / 'SOURCES.json').read_text()) + good = dict(man['current_required'][0]) + V.historical(good) + other = man['current_required'][1] + for bad in (dict(good, blob=other['blob']), # wrong blob at that commit/path + dict(good, path=other['path']), # another path at that commit + dict(good, commit='0' * 40), # absent commit + dict(good, sha256='0' * 64), # wrong recorded digest + dict(good, bytes=good['bytes'] + 1), # wrong recorded size + dict(good, path='../' + good['path'])): # noncanonical path + with self.assertRaises(ValueError): + V.historical(bad) class PinTransform(unittest.TestCase): diff --git a/frontiers/ordinary_short_bar_occurrence_all_d_20261001/verify_sources.py b/frontiers/ordinary_short_bar_occurrence_all_d_20261001/verify_sources.py index 7f023e63c..9ff410b2b 100644 --- a/frontiers/ordinary_short_bar_occurrence_all_d_20261001/verify_sources.py +++ b/frontiers/ordinary_short_bar_occurrence_all_d_20261001/verify_sources.py @@ -1,10 +1,15 @@ -"""Source identity for C52-ALL-D: the seven current_required sources must match bytes, SHA256 and Git blob on the -tree. The two cited_unmerged C52 files (Math-#235) are recorded only; they are not premises. Identity only, not -analytic acceptance. +"""Source identity for C52-ALL-D. Identity only, not analytic acceptance. + +current_required (seven): for each entry the working-tree copy at `local_path` and the historical entry +`commit:path` must both be the recorded blob, with the recorded byte count and SHA256 (`git ls-tree --full-tree`). +cited_unmerged (two C52 files of Math-#235): checked the same way when the commit object is present locally, otherwise +reported as unavailable. They are not premises. CI checks out full history (fetch-depth: 0). python3 -B -S verify_sources.py""" import hashlib import json +import re +import subprocess import sys from pathlib import Path, PurePosixPath @@ -18,11 +23,23 @@ def require(cond, msg): raise ValueError(msg) -def contained(rel): +def git(*args): + p = subprocess.run(['git', '-C', str(ROOT)] + list(args), capture_output=True) + if p.returncode: + raise ValueError('git %s failed: %s' % (args[0], p.stderr.decode(errors='replace').strip())) + return p.stdout + + +def canonical(rel): require(isinstance(rel, str) and rel, 'invalid path') parts = PurePosixPath(rel) require(not parts.is_absolute() and str(parts) == rel and all(p not in ('', '.', '..') for p in parts.parts), 'noncanonical path ' + rel) + return parts + + +def contained(rel): + parts = canonical(rel) t = ROOT for p in parts.parts: t = t / p @@ -31,6 +48,27 @@ def contained(rel): return t +def identity_ok(data, e): + blob = hashlib.sha1(b'blob ' + str(len(data)).encode() + b'\0' + data).hexdigest() + return len(data) == e['bytes'] and hashlib.sha256(data).hexdigest() == e['sha256'] and blob == e['blob'] + + +def historical(e): + """commit:path must be exactly the recorded regular-file blob, whose bytes match the record""" + commit, path, blob = e['commit'], e['path'], e['blob'] + require(re.fullmatch('[0-9a-f]{40}', commit) and re.fullmatch('[0-9a-f]{40}', blob), 'identity format ' + e['key']) + canonical(path) + require(git('cat-file', '-t', commit).strip() == b'commit', e['key'] + ': not a commit') + listing = git('ls-tree', '--full-tree', '-z', commit, '--', path) + require(listing == ('100644 blob %s\t%s\0' % (blob, path)).encode(), e['key'] + ': commit/path/blob mismatch') + require(identity_ok(git('cat-file', 'blob', blob), e), e['key'] + ': historical bytes mismatch') + + +def commit_present(commit): + p = subprocess.run(['git', '-C', str(ROOT), 'cat-file', '-t', commit], capture_output=True) + return p.returncode == 0 and p.stdout.strip() == b'commit' + + def verify(): raw = contained('frontiers/ordinary_short_bar_occurrence_all_d_20261001/SOURCES.json').read_bytes() require(hashlib.sha256(raw).hexdigest() == MANIFEST_SHA256, 'manifest digest') @@ -38,19 +76,26 @@ def verify(): req = man['current_required'] require(len(req) == 7 and len({e['key'] for e in req}) == 7, 'seven distinct required sources') for e in req: - data = contained(e['local_path']).read_bytes() - require(type(e['bytes']) is int and len(data) == e['bytes'], 'bytes ' + e['key']) - require(hashlib.sha256(data).hexdigest() == e['sha256'], 'sha256 ' + e['key']) - blob = hashlib.sha1(b'blob ' + str(len(data)).encode() + b'\0' + data).hexdigest() - require(blob == e['blob'], 'blob ' + e['key']) - require(all(e['pr'] == 'Math-#235' for e in man['cited_unmerged']), 'cited entries') - return len(req) + require(type(e['bytes']) is int and e['bytes'] > 0, 'bytes ' + e['key']) + require(e['local_path'] == e['path'], 'local path differs from pinned path ' + e['key']) + require(identity_ok(contained(e['local_path']).read_bytes(), e), 'working-tree bytes ' + e['key']) + historical(e) + cited = {} + for e in man['cited_unmerged']: + require(e['pr'] == 'Math-#235', 'cited entry ' + e['key']) + if commit_present(e['commit']): + historical(e) + cited[e['key']] = 'verified' + else: + cited[e['key']] = 'commit not present locally (not a premise)' + return len(req), cited if __name__ == '__main__': try: - n = verify() + n, cited = verify() except ValueError as exc: print('source verification FAILED:', exc) sys.exit(1) - print(json.dumps({'verified_sources': n, 'scope': 'source identity only, not analytic acceptance'})) + print(json.dumps({'verified_sources': n, 'cited_unmerged': cited, + 'scope': 'source identity only, not analytic acceptance'})) From d7e2614f720ea7db4f544d63055b16dd3550d012 Mon Sep 17 00:00:00 2001 From: Dylan Roy Date: Thu, 1 Oct 2026 19:41:18 +0000 Subject: [PATCH 3/4] C52 all-d v1.2: disable Git replacement objects (OA-236-ENG-01) Fixes the engineering finding in review 5384571149. A local refs/replace entry could redirect a pinned commit, letting a false commit:path binding pass. - verify_sources.py: both git() and commit_present() now run git --no-replace-objects with GIT_NO_REPLACE_OBJECTS=1, following reviews/d1_external_audit_20260930/verify_sources.py. - test_check.py: a new real-Git regression test shows that a false original binding is rejected even with a matching replacement, and a genuine binding is accepted despite an unrelated replacement. It fails against the previous verifier. The six earlier rejection checks are kept. - NOTE section 0 now applies the "every fixed d >= 2" sentence to the consumed interfaces (optional Slice C note, 5384434418). Section 6 documents the replacement guard. check.py and SOURCES.json are unchanged. 14 tests pass in both modes and 17 of 17 mutants are killed. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015wNj8LPTKXsaT68G3DgPPh --- .../NOTE.md | 8 +++- .../test_check.py | 42 +++++++++++++++++++ .../verify_sources.py | 12 ++++-- 3 files changed, 57 insertions(+), 5 deletions(-) diff --git a/frontiers/ordinary_short_bar_occurrence_all_d_20261001/NOTE.md b/frontiers/ordinary_short_bar_occurrence_all_d_20261001/NOTE.md index b22b55904..9c9e6965b 100644 --- a/frontiers/ordinary_short_bar_occurrence_all_d_20261001/NOTE.md +++ b/frontiers/ordinary_short_bar_occurrence_all_d_20261001/NOTE.md @@ -22,7 +22,9 @@ merging saddle S, of index d-1. Exclude the essential global-maximum class. Let lifetime in `(0, tau]` in ONE field on the WHOLE torus. Its expectation is not divided by volume. The seven sources P, CAP, E1, E2, REC, R and T are pinned in `SOURCES.json` at Math- `7fe06b0`. They are the sources -C52 consumes, and each is stated for every fixed `d >= 2`: +C52 consumes. Each **consumed interface** is stated for every fixed `d >= 2`. CAP's numerical probabilistic corollary is +the fixed-axis planar SIDE24 statement, and it is not used here: only CAP's deterministic theorem, which holds for `d >= 2`, +enters (Slice C note, 5384434418). - [P] "Fix a dimension d>=2"; - [CAP] "Let d>=2"; - [R] and [T] "for each fixed d>=2" and "Fix d>=2"; @@ -419,7 +421,9 @@ Unbounded mark moments do not converge without a separate uniform-integrability These cover `d = 2..6`. `test_check.py` adds unit tests and 17 implementation mutants. Each mutant must fail in both `-B -S` and `-B -O -S`. `verify_sources.py` authenticates the seven `current_required` sources by bytes, SHA256 and Git -blob. It checks both the working-tree copy and the historical `commit:path -> blob` entry, via `git ls-tree`. The two +blob. It checks both the working-tree copy and the historical `commit:path -> blob` entry, via `git ls-tree`. Git +replacement objects are disabled (`--no-replace-objects`, `GIT_NO_REPLACE_OBJECTS=1`), so a local `refs/replace` entry +cannot redirect a pinned commit (OA-236-ENG-01, with a real-Git regression test). The two `cited_unmerged` C52 entries are checked the same way when their commit is present locally, and otherwise reported as unavailable; they are not premises. diff --git a/frontiers/ordinary_short_bar_occurrence_all_d_20261001/test_check.py b/frontiers/ordinary_short_bar_occurrence_all_d_20261001/test_check.py index 40a6db064..bb9c1feac 100644 --- a/frontiers/ordinary_short_bar_occurrence_all_d_20261001/test_check.py +++ b/frontiers/ordinary_short_bar_occurrence_all_d_20261001/test_check.py @@ -38,6 +38,48 @@ def test_historical_rejections(self): with self.assertRaises(ValueError): V.historical(bad) + def test_replacement_objects_ignored(self): + """OA-236-ENG-01: a refs/replace entry must neither validate a false original binding nor break a genuine one""" + import hashlib + import subprocess + import tempfile + from pathlib import Path + env = dict(os.environ, GIT_AUTHOR_NAME='F', GIT_COMMITTER_NAME='F', GIT_AUTHOR_EMAIL='f@example.invalid', + GIT_COMMITTER_EMAIL='f@example.invalid', GIT_CONFIG_NOSYSTEM='1') + env.pop('GIT_NO_REPLACE_OBJECTS', None) + saved = V.ROOT + with tempfile.TemporaryDirectory() as d: + root = Path(d) + + def g(*a, data=None): + return subprocess.run(['git'] + list(a), cwd=root, env=env, input=data, capture_output=True, + check=True).stdout.strip().decode() + try: + V.ROOT = root + g('init', '-q') + wrong = g('commit-tree', g('mktree', data=b''), data=b'empty original\n') + (root / 'P.md').write_bytes(b'fixture only\n') + g('add', 'P.md') + good = g('commit-tree', g('write-tree'), data=b'source\n') + (root / 'Q.md').write_bytes(b'unrelated\n') + g('add', 'Q.md') + other = g('commit-tree', g('write-tree'), data=b'other\n') + data = (root / 'P.md').read_bytes() + rec = dict(key='P', path='P.md', blob=g('rev-parse', good + ':P.md'), bytes=len(data), + sha256=hashlib.sha256(data).hexdigest()) + false_binding, true_binding = dict(rec, commit=wrong), dict(rec, commit=good) + with self.assertRaises(ValueError): + V.historical(false_binding) # control + V.historical(true_binding) + g('replace', wrong, good) # replacement makes the false binding look valid + with self.assertRaises(ValueError): + V.historical(false_binding) + g('replace', good, other) # unrelated replacement of the genuine commit + V.historical(true_binding) + self.assertTrue(V.commit_present(wrong)) + finally: + V.ROOT = saved + class PinTransform(unittest.TestCase): def test_det_and_target(self): diff --git a/frontiers/ordinary_short_bar_occurrence_all_d_20261001/verify_sources.py b/frontiers/ordinary_short_bar_occurrence_all_d_20261001/verify_sources.py index 9ff410b2b..50465c442 100644 --- a/frontiers/ordinary_short_bar_occurrence_all_d_20261001/verify_sources.py +++ b/frontiers/ordinary_short_bar_occurrence_all_d_20261001/verify_sources.py @@ -3,11 +3,13 @@ current_required (seven): for each entry the working-tree copy at `local_path` and the historical entry `commit:path` must both be the recorded blob, with the recorded byte count and SHA256 (`git ls-tree --full-tree`). cited_unmerged (two C52 files of Math-#235): checked the same way when the commit object is present locally, otherwise -reported as unavailable. They are not premises. CI checks out full history (fetch-depth: 0). +reported as unavailable. They are not premises. CI checks out full history (fetch-depth: 0). Git replacement objects +are disabled (--no-replace-objects, GIT_NO_REPLACE_OBJECTS=1), so a local refs/replace entry cannot redirect a pin. python3 -B -S verify_sources.py""" import hashlib import json +import os import re import subprocess import sys @@ -23,8 +25,11 @@ def require(cond, msg): raise ValueError(msg) +GIT_ENV = dict(os.environ, GIT_NO_REPLACE_OBJECTS='1') # refs/replace must never redirect a pinned commit (OA-236-ENG-01) + + def git(*args): - p = subprocess.run(['git', '-C', str(ROOT)] + list(args), capture_output=True) + p = subprocess.run(['git', '--no-replace-objects', '-C', str(ROOT)] + list(args), capture_output=True, env=GIT_ENV) if p.returncode: raise ValueError('git %s failed: %s' % (args[0], p.stderr.decode(errors='replace').strip())) return p.stdout @@ -65,7 +70,8 @@ def historical(e): def commit_present(commit): - p = subprocess.run(['git', '-C', str(ROOT), 'cat-file', '-t', commit], capture_output=True) + p = subprocess.run(['git', '--no-replace-objects', '-C', str(ROOT), 'cat-file', '-t', commit], capture_output=True, + env=GIT_ENV) return p.returncode == 0 and p.stdout.strip() == b'commit' From 3133181f500d5633896a79ed06eb70f56a33023e Mon Sep 17 00:00:00 2001 From: Dylan Roy Date: Fri, 2 Oct 2026 22:57:21 +0000 Subject: [PATCH 4/4] C52-ALL-D v1.1: Math-#235 merged; pin its two C52 files on main and require them Math-#235 merged at 7e23441 with FOLD_ISOLATION.md (a3d4e7c4) and PROOF.md (69ff20a6) byte-identical to the blobs cited since v1. SOURCES.json moves them from cited_unmerged to cited, pinned at 7e23441 with local_path; verify_sources.py now checks them on the working tree and at commit:path and requires them (it previously reported them as optional when the commit was absent). Manifest digest updated; the source test now asserts both are 'verified'; the workflow also triggers on the two #235 paths. NOTE credit paragraph and section 6 updated; new section 8 records v1.1. Provenance only: no statement, proof, check.py control or constant changed. C52 stays cited, not consumed as a premise. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_015wNj8LPTKXsaT68G3DgPPh --- .../ordinary-short-bar-occurrence-all-d.yml | 4 ++++ .../NOTE.md | 16 ++++++++++++---- .../SOURCES.json | 12 +++++++----- .../test_check.py | 2 +- .../verify_sources.py | 19 +++++++++---------- 5 files changed, 33 insertions(+), 20 deletions(-) diff --git a/.github/workflows/ordinary-short-bar-occurrence-all-d.yml b/.github/workflows/ordinary-short-bar-occurrence-all-d.yml index f9302704d..1687c868e 100644 --- a/.github/workflows/ordinary-short-bar-occurrence-all-d.yml +++ b/.github/workflows/ordinary-short-bar-occurrence-all-d.yml @@ -5,6 +5,8 @@ on: - 'frontiers/ordinary_short_bar_occurrence_all_d_20261001/**' - 'frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md' - 'frontiers/short_bar_endpoint_law_20261001/PROOF.md' + - 'frontiers/ordinary_short_bar_occurrence_20261001/FOLD_ISOLATION.md' + - 'frontiers/ordinary_short_bar_occurrence_20261001/PROOF.md' - 'imports/lifetime_parent_20260925/**' - 'reviews/d1_section9_borel_repair_20260925/REPAIR.md' - 'reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md' @@ -15,6 +17,8 @@ on: - 'frontiers/ordinary_short_bar_occurrence_all_d_20261001/**' - 'frontiers/three_fronts_20260924/LIFETIME_REMAINDER.md' - 'frontiers/short_bar_endpoint_law_20261001/PROOF.md' + - 'frontiers/ordinary_short_bar_occurrence_20261001/FOLD_ISOLATION.md' + - 'frontiers/ordinary_short_bar_occurrence_20261001/PROOF.md' - 'imports/lifetime_parent_20260925/**' - 'reviews/d1_section9_borel_repair_20260925/REPAIR.md' - 'reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md' diff --git a/frontiers/ordinary_short_bar_occurrence_all_d_20261001/NOTE.md b/frontiers/ordinary_short_bar_occurrence_all_d_20261001/NOTE.md index 9c9e6965b..a7031f68f 100644 --- a/frontiers/ordinary_short_bar_occurrence_all_d_20261001/NOTE.md +++ b/frontiers/ordinary_short_bar_occurrence_all_d_20261001/NOTE.md @@ -4,8 +4,8 @@ Object: C52-ALL-D-ORDINARY-SHORT-BAR-OCCURRENCE-20261001-v1. Author lane: Anthropic / Claude (session 015wNj8L…), under Dylan Roy's delegation. Additive conditional candidate. Scientific effect: NONE. C8 OPEN. No STATUS, PROOF_INDEX, GRAPH, prize or premise edit. -**Credit.** The argument is OpenAI/Codex's C52 (Math-#235, head `c463777`: `FOLD_ISOLATION.md` blob `a3d4e7c4`, -`PROOF.md` blob `69ff20a6`). C52 proves the planar case and states that it makes "no extension of the present planar +**Credit.** The argument is OpenAI/Codex's C52 (Math-#235, merged to main at `7e23441` with the reviewed blobs unchanged: +`FOLD_ISOLATION.md` blob `a3d4e7c4`, `PROOF.md` blob `69ff20a6`). C52 proves the planar case and states that it makes "no extension of the present planar lemma to other dimensions" (FOLD_ISOLATION §8). This packet supplies that extension. Its planar case `d = 2` is exactly C52's Theorem O, so it neither supersedes nor edits #235. C52's files are cited, not consumed as premises: every step used here is restated and proved below in dimension d. @@ -424,8 +424,8 @@ These cover `d = 2..6`. `test_check.py` adds unit tests and 17 implementation mu blob. It checks both the working-tree copy and the historical `commit:path -> blob` entry, via `git ls-tree`. Git replacement objects are disabled (`--no-replace-objects`, `GIT_NO_REPLACE_OBJECTS=1`), so a local `refs/replace` entry cannot redirect a pinned commit (OA-236-ENG-01, with a real-Git regression test). The two -`cited_unmerged` C52 entries are checked the same way when their commit is present locally, and otherwise reported as -unavailable; they are not premises. +`cited` C52 entries (merged with #235 at `7e23441`) are checked the same way, working tree and `commit:path`; they are +credited sources, not premises. The controls do not prove the continuum analysis, including: - genericity; @@ -441,3 +441,11 @@ The controls do not prove the continuum analysis, including: conditional covariance positivity for (N7), and the uniform integrability. - **Slice C, §§0, 3–5:** the source scope in general `d`, (C1)–(C2), the domination, and the occurrence and mark conclusions. This includes checking that [T] (T4) and [E2] are indeed used only within their stated general-d scope. + +## 8. Revisions + +- **v1.1 (provenance only).** Math-#235 merged at `7e23441` with `FOLD_ISOLATION.md` and `PROOF.md` byte-identical to + the blobs cited since v1 (`a3d4e7c4`, `69ff20a6`). `SOURCES.json` moves the two C52 entries from `cited_unmerged` to + `cited`, pinned at `7e23441` and verified on the working tree. `verify_sources.py` now requires them instead of + reporting them as optional, and the workflow also triggers on those two paths. No statement, proof, control or + constant changed, and C52 remains cited, not consumed as a premise. diff --git a/frontiers/ordinary_short_bar_occurrence_all_d_20261001/SOURCES.json b/frontiers/ordinary_short_bar_occurrence_all_d_20261001/SOURCES.json index 28674a694..e7cf3403a 100644 --- a/frontiers/ordinary_short_bar_occurrence_all_d_20261001/SOURCES.json +++ b/frontiers/ordinary_short_bar_occurrence_all_d_20261001/SOURCES.json @@ -75,26 +75,28 @@ "role": "Proposition 3 / (T4): ordinary-bar marked intensity law in every d>=2" } ], - "cited_unmerged": [ + "cited": [ { "key": "C52-FOLD", "path": "frontiers/ordinary_short_bar_occurrence_20261001/FOLD_ISOLATION.md", "pr": "Math-#235", - "commit": "c46377738b711a5cc2114b58bf7726ae6e7bc553", + "commit": "7e2344166e989ae94e5732e445f445598fc75c4c", "blob": "a3d4e7c4c4c23d22af9d259db74afc9ba6fdac1e", "bytes": 20771, "sha256": "3889a0898901d03716d277e3afc2964bdbc7566d3a85803c4ad73673bdff1b52", - "role": "source of the planar argument generalized here; not consumed as a premise; d=2 case" + "role": "source of the planar argument generalized here; cited, not consumed as a premise; merged to main at 7e23441; d=2 case", + "local_path": "frontiers/ordinary_short_bar_occurrence_20261001/FOLD_ISOLATION.md" }, { "key": "C52-PROOF", "path": "frontiers/ordinary_short_bar_occurrence_20261001/PROOF.md", "pr": "Math-#235", - "commit": "c46377738b711a5cc2114b58bf7726ae6e7bc553", + "commit": "7e2344166e989ae94e5732e445f445598fc75c4c", "blob": "69ff20a6c514629373f3ad12eb2db2a2596777d6", "bytes": 14146, "sha256": "16d2c5f6c1fe45dd6ce8f6b69455db4908b8e6319e57d58c4ad7c9d1881bdd4d", - "role": "source of the planar consumer (Sections 3-6) generalized here; not consumed as a premise" + "role": "source of the planar consumer (Sections 3-6) generalized here; cited, not consumed as a premise; merged to main at 7e23441", + "local_path": "frontiers/ordinary_short_bar_occurrence_20261001/PROOF.md" } ] } diff --git a/frontiers/ordinary_short_bar_occurrence_all_d_20261001/test_check.py b/frontiers/ordinary_short_bar_occurrence_all_d_20261001/test_check.py index bb9c1feac..c7a6facac 100644 --- a/frontiers/ordinary_short_bar_occurrence_all_d_20261001/test_check.py +++ b/frontiers/ordinary_short_bar_occurrence_all_d_20261001/test_check.py @@ -21,7 +21,7 @@ class Sources(unittest.TestCase): def test_seven_sources(self): n, cited = V.verify() self.assertEqual(n, 7) - self.assertEqual(set(cited), {'C52-FOLD', 'C52-PROOF'}) + self.assertEqual(cited, {'C52-FOLD': 'verified', 'C52-PROOF': 'verified'}) def test_historical_rejections(self): import json diff --git a/frontiers/ordinary_short_bar_occurrence_all_d_20261001/verify_sources.py b/frontiers/ordinary_short_bar_occurrence_all_d_20261001/verify_sources.py index 50465c442..05ba56e1c 100644 --- a/frontiers/ordinary_short_bar_occurrence_all_d_20261001/verify_sources.py +++ b/frontiers/ordinary_short_bar_occurrence_all_d_20261001/verify_sources.py @@ -2,8 +2,8 @@ current_required (seven): for each entry the working-tree copy at `local_path` and the historical entry `commit:path` must both be the recorded blob, with the recorded byte count and SHA256 (`git ls-tree --full-tree`). -cited_unmerged (two C52 files of Math-#235): checked the same way when the commit object is present locally, otherwise -reported as unavailable. They are not premises. CI checks out full history (fetch-depth: 0). Git replacement objects +cited (two C52 files of Math-#235, merged to main at 7e23441): checked the same way, working tree and commit:path, +and required. They are credited sources, not premises. CI checks out full history (fetch-depth: 0). Git replacement objects are disabled (--no-replace-objects, GIT_NO_REPLACE_OBJECTS=1), so a local refs/replace entry cannot redirect a pin. python3 -B -S verify_sources.py""" @@ -17,7 +17,7 @@ HERE = Path(__file__).resolve().parent ROOT = HERE.parents[1] -MANIFEST_SHA256 = '44fc416116eca6bbf56c029329930212c0b108ee1bb9174ca8f3b41ad1b78991' +MANIFEST_SHA256 = '7fa5215487df6282baa997efe469686677277f08bfeb210e95e13d8273a0345b' def require(cond, msg): @@ -87,13 +87,12 @@ def verify(): require(identity_ok(contained(e['local_path']).read_bytes(), e), 'working-tree bytes ' + e['key']) historical(e) cited = {} - for e in man['cited_unmerged']: + for e in man['cited']: require(e['pr'] == 'Math-#235', 'cited entry ' + e['key']) - if commit_present(e['commit']): - historical(e) - cited[e['key']] = 'verified' - else: - cited[e['key']] = 'commit not present locally (not a premise)' + require(e['local_path'] == e['path'], 'local path differs from pinned path ' + e['key']) + require(identity_ok(contained(e['local_path']).read_bytes(), e), 'working-tree bytes ' + e['key']) + historical(e) + cited[e['key']] = 'verified' return len(req), cited @@ -103,5 +102,5 @@ def verify(): except ValueError as exc: print('source verification FAILED:', exc) sys.exit(1) - print(json.dumps({'verified_sources': n, 'cited_unmerged': cited, + print(json.dumps({'verified_sources': n, 'cited': cited, 'scope': 'source identity only, not analytic acceptance'}))