From 4d62e0219d99ada8646a880612fe46ebf0f9e7db Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 29 Sep 2026 15:52:23 +0000 Subject: [PATCH 1/7] D5 in every fixed dimension: lift the pin, collar, intermediate and global window bounds to d >= 2 Author-side proof candidate CL-D5-DIMENSION-LIFT-20260929-v1 under frontiers/d5_dimension_lift_20260929. Scientific effect NONE; nonauthor analytic review required; no status, index, graph, claim or lemma flag changes. Every D5 upper bound in the repository was planar (d = 2) while the program's application dimension is d = 3, and remote_collision Corollary F leaves the d > 2 upper half conditional on a dimension-matched global first moment. This packet writes the d-dimensional replacement of each planar-specific step of PUNCTURED_PIN_PROOF (P2), COLLAR_PROOF (C1, C2) and intermediate_window (I3, I4, I5), keeping the exact model, original weight, full normalizer and Kac-Rice framework of the sources: - Theorem P_d: all-height punctured pin ball with the integrable weight max(|q|, r|p|)^(2-d), count O(r^3), nested ball O(r^5). - Theorem C_d: compact collar E N_j(rE) <= C r^3 |E| and the scaled ball minus pins. - Theorem I_d: height-window shells C r^3[(r/s)^2 + s^2] and the dyadic sum C r^3(A_0^-2 + rho^2). - Theorem G_d: global height-window first moment O(r^3) on the torus minus the pins, by tiling with remote_window Theorem A. - Corollaries F_d and M_d: Q^W(A_r) and Q^W(N_r >= 2) are Theta(r^3) in every fixed d, discharging the d > 2 conditional; no O(r^5) torus-wide second factorial moment. Five linear-algebra devices do the new work: a two-soft-direction determinant bound through the second exterior power, Hadamard for one soft direction, Gram floors for the jet functionals S -> S beta, beta^T C beta and D[beta, beta, beta] (explicit pin-frame floor (9/64)^(d-1)/2048, the planar 9/131072 at d = 2), a transverse block determinant identity driven by the Euler quadratic form and the gradient equation, and the integrable pin weight. lift_exact_check.py (standard library, exact rational and polynomial arithmetic) verifies the exterior-power inequality, frame ranks and floors, confluent degree-five interpolation in d = 2, 3, 4 with the degree-four negative control, the d = 3 row operation and Euler identity on a pinned cubic, the block determinant identity, the three functional norms, all power ledgers for d = 2..6 and the pin-weight exponents; RESULTS.json is its byte-identical output in -B -S and -B -O -S modes and ten named mutants are rejected. SOURCE_MAP.json pins the eight consumed sources at dbccbb4; SOURCE_FILES.json is the packet manifest; the new workflow replays the manifest, both modes and the mutants on pull requests touching the packet. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_015wNj8LPTKXsaT68G3DgPPh --- .github/workflows/d5-dimension-lift.yml | 61 ++ frontiers/d5_dimension_lift_20260929/PROOF.md | 539 ++++++++++++ .../d5_dimension_lift_20260929/README.md | 52 ++ .../RECONNAISSANCE.md | 24 + .../d5_dimension_lift_20260929/RESULTS.json | 125 +++ .../SOURCE_FILES.json | 43 + .../SOURCE_MAP.json | 86 ++ .../lift_exact_check.py | 773 ++++++++++++++++++ 8 files changed, 1703 insertions(+) create mode 100644 .github/workflows/d5-dimension-lift.yml create mode 100644 frontiers/d5_dimension_lift_20260929/PROOF.md create mode 100644 frontiers/d5_dimension_lift_20260929/README.md create mode 100644 frontiers/d5_dimension_lift_20260929/RECONNAISSANCE.md create mode 100644 frontiers/d5_dimension_lift_20260929/RESULTS.json create mode 100644 frontiers/d5_dimension_lift_20260929/SOURCE_FILES.json create mode 100644 frontiers/d5_dimension_lift_20260929/SOURCE_MAP.json create mode 100644 frontiers/d5_dimension_lift_20260929/lift_exact_check.py diff --git a/.github/workflows/d5-dimension-lift.yml b/.github/workflows/d5-dimension-lift.yml new file mode 100644 index 000000000..e81691867 --- /dev/null +++ b/.github/workflows/d5-dimension-lift.yml @@ -0,0 +1,61 @@ +name: D5 dimension-lift checks + +'on': + pull_request: + paths: + - 'frontiers/d5_dimension_lift_20260929/**' + - '.github/workflows/d5-dimension-lift.yml' + workflow_dispatch: + +permissions: + contents: read + +jobs: + exact-and-probe: + runs-on: ubuntu-latest + timeout-minutes: 15 + steps: + - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 + with: + persist-credentials: false + - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 + with: + python-version: '3.11.16' + - name: Verify sources, replay both modes, reject mutants + env: + PYTHONDONTWRITEBYTECODE: '1' + run: | + set -euo pipefail + python -B -S - <<'PY' + import hashlib, json, pathlib, subprocess, sys + root = pathlib.Path('frontiers/d5_dimension_lift_20260929').resolve() + manifest = json.loads((root / 'SOURCE_FILES.json').read_text())['files'] + present = sorted(p.name for p in root.iterdir()) + expected_names = sorted([e['path'] for e in manifest] + ['SOURCE_FILES.json']) + if present != expected_names: + raise ValueError('packet tree differs from manifest: ' + repr(present)) + for entry in manifest: + path = root / entry['path'] + if pathlib.PurePosixPath(entry['path']).name != entry['path'] or path.is_symlink(): + raise ValueError('flat regular source required: ' + entry['path']) + data = path.read_bytes() + if len(data) != entry['bytes'] or hashlib.sha256(data).hexdigest() != entry['sha256']: + raise ValueError('source identity mismatch: ' + entry['path']) + script = str(root / 'lift_exact_check.py') + expected = (root / 'RESULTS.json').read_bytes() + mutants = ['drop-frobenius-order', 'drop-s0-block', 'drop-a4-column', 'degree-four', + 'row-operation-third', 'euler-coefficient', 'adjugate-sign', 'one-soft-direction', + 'flat-shell', 'weight-one-less-power'] + for flags in (['-B', '-S'], ['-B', '-O', '-S']): + out = subprocess.run([sys.executable, *flags, script], + check=True, capture_output=True, timeout=600).stdout + if out != expected: + raise RuntimeError('output differs from RESULTS.json under ' + ' '.join(flags)) + for m in mutants: + rc = subprocess.run([sys.executable, *flags, script, '--mutant', m], + capture_output=True, timeout=600).returncode + if rc != 1: + raise RuntimeError('mutant ' + m + ' not rejected') + print(json.dumps({'scientific_effect': 'NONE', 'mathematical_acceptance': False})) + PY + git diff --exit-code diff --git a/frontiers/d5_dimension_lift_20260929/PROOF.md b/frontiers/d5_dimension_lift_20260929/PROOF.md new file mode 100644 index 000000000..887a79634 --- /dev/null +++ b/frontiers/d5_dimension_lift_20260929/PROOF.md @@ -0,0 +1,539 @@ +# D5 in every fixed dimension: punctured pin balls, the compact collar, intermediate height-window shells, and the global window first moment + +**Object:** CL-D5-DIMENSION-LIFT-20260929-v1. +**Author:** Anthropic Claude (Claude Code session `session_015wNj8LPTKXsaT68G3DgPPh`), 29 September 2026. +**Disposition:** author-side proof candidate. **Nonauthor analytic review is required.** +**Scientific effect:** NONE. No `STATUS`, `PROOF_INDEX` verdict, `GRAPH` node, claim, `lemma_closed` flag, prize or source body changes. + +## 0. Why this note exists + +Every D5 estimate of the last three days is planar. The punctured endpoint disk [PP], the compact collar [CP], the intermediate shells and the global first moment (I5) [IW], and the planar halves of Corollary F [RC] and Theorem L [LOCAL] all fix `d = 2`. The fixed-remote Theorem A [RM] and the lower bounds of [RC] (F-) and [EDL] (A4) hold in every fixed `d`. [RC] states the consequence exactly: for `d > 2` the matching upper bound on the window event "stays conditional on a dimension-matched global first moment", and no source supplies one. The program's own application is `d = 3` (SIDE24, `L = 24` in [LP] §1). + +This note supplies that first moment in every fixed `d >= 2`. It lifts the three planar D5 components and their composition. The planar proofs are followed step by step; every step that is not literally dimension-free is replaced here by a written `d`-dimensional argument. Five devices do all the new work (§3). Nothing else changes: the model, the pins, the weight, the normalizer, the Kac–Rice framework and the regression estimates are those of the sources. + +## 1. Setting and results + +### 1.1 Model + +Fix `d >= 2`, `m = d - 1`, and `L > 0`. `f` is the centered variance-one Gaussian field on `X = R^d/(L Z^d)` with the exact normalized periodized Gaussian covariance of [LP] §1. Fix compact `B = [b_-, b_+]` and `K = [k_-, k_+]` with `0 < k_-`. Frames `R` range over `O(d)`; `u = R e_1` is the axial direction and `y in R^m` are the transverse coordinates. For small `r > 0` the pins are + + M = -(r/2) u, S = (r/2) u, f(M) = b, f(S) = b - k r^3, grad f(M) = grad f(S) = 0. + +`Q_r` is Gaussian regression on these `2(d+1)` observations (not an adjacency or elder law). For a symmetric matrix `H`, `F_j(H) = |det H|` if `H` is nonsingular with `j` negative eigenvalues, and `0` otherwise. Retain the original weight, the full normalizer and the tilted law + + W_r = F_d(H_M) F_(d-1)(H_S), Z_r = E_(Q_r) W_r, dQ_r^W = (W_r/Z_r) dQ_r, + +and the between-pin height window `I_r = (b - k r^3, b)`. `N_j(B)` counts index-`j` critical points of `f` in a Borel set `B` at all heights; `N_(r,j)(B)` counts those with height in `I_r`. Constants `C, c, r_*, s_0` depend on `d, L, B, K` and on the fixed chart radii named in each statement; never on `r, s, b, k, R, j` or the Borel set. No constant is evaluated numerically. Nothing is uniform as `k -> 0`, as marks grow, or as `d` or `L` vary. + +Throughout, `K` also denotes a fixed multiple of `1 + ||f||_(C^6(X))` (the sources use the same letter for the mark interval; the meaning is always clear from context), and `L <= K` a Hessian Lipschitz constant on the relevant chart. + +### 1.2 Statements + +Write a point of the scaled chart around `M` as `X = M + r (p, q)` with `p in R`, `q in R^m`, and put + + D = { (p, q) : 0 < p^2 + |q|^2 <= 1/16 }, + omega_d(p, q) = max(|q|, r |p|)^(2-d) (omega_2 = 1). (1.1) + +**Theorem P_d (all-height punctured pin ball).** There are `C, r_* > 0` such that for `0 < r <= r_*`, all `b, k, R, j` and every Borel `E` contained in `D`, + + E_(Q_r^W) N_j(M + r E) <= C r^3 integral_E omega_d(p, q) dp dq <= C' r^3. (1.2) + +The same holds for the punctured ball about `S` (§4.9). For a nested ball `p^2 + |q|^2 <= kappa^2 r^2` (physical radius `kappa r^2`), the right side is `O(r^5)`. For `d = 2` this is [PP] (P2). + +**Theorem C_d (compact collar).** In midpoint scaled coordinates `X = r (u, v)`, `u in R`, `v in R^m`, fix `R >= 1` and `0 < eta <= 1/4`, and let `C(eta, R)` be the closed ball of radius `R` with the two open balls of radius `eta` about `(-1/2, 0)` and `(1/2, 0)` removed. There are `C, r_* > 0` such that for every Borel `E` contained in `C(eta, R)`, + + E_(Q_r^W) N_j(r E) <= C r^3 |E|. (1.3) + +Consequently, for every Borel subset `E` of the scaled ball of radius `R` with the two pins removed, + + E_(Q_r^W) N_j(r E) <= C r^3 (1 + integral_(E cap pin balls) omega_d) <= C' r^3. (1.4) + +For `d = 2` these are [CP] (C1), (C2). + +**Theorem I_d (intermediate height-window shells).** There are `C, s_0 > 0` such that for `0 < r <= s/4` and `0 < s <= s_0`, + + E_(Q_r^W) N_(r,j)({ s <= |X| <= 2 s }) <= C r^3 [ (r/s)^2 + s^2 ], (1.5) + +and hence, uniformly for `A_0 >= 4` and `A_0 r < rho <= s_0`, + + E_(Q_r^W) N_(r,j)({ A_0 r <= |X| <= rho }) <= C r^3 ( A_0^(-2) + rho^2 ). (1.6) + +For `d = 2` these are [IW] (I3), (I4). + +**Theorem G_d (global height-window first moment).** There are `C, r_* > 0` such that + + E_(Q_r^W) N_(r,j)( X minus {M, S} ) <= C r^3. (1.7) + +For `d = 2` this is [IW] (I5). + +**Corollary F_d.** Let `A_r` be the event that some critical point other than `M, S` has height in `I_r`. In every fixed `d >= 2`, + + c r^3 <= Q_r^W(A_r) <= C r^3. (1.8) + +The lower half is [RC] Corollary (F-), which holds in every fixed `d`. The upper half is Markov's inequality applied to (1.7), summed over the `d+1` indices. This discharges the sentence in [RC] §1 that leaves the `d > 2` upper half conditional. + +**Corollary M_d (window multiplicity in every dimension).** Let `N_r` count all window critical points other than `M, S`. In every fixed `d >= 2`, + + c r^3 <= Q_r^W{ N_r >= 2 } <= C r^3, E_(Q_r^W)[ N_r (N_r - 1) ] >= c r^3. (1.9) + +The lower bounds are [EDL] (A4). The upper bound is `1{N >= 2} <= N/2` and (1.7). In particular a torus-wide `O(r^5)` second factorial moment is excluded in every `d`, the global window point process is at total-variation distance `Theta(r^3)` from its exact-mean Bernoulli approximation (the elementary identity of [LOCAL] §7 is dimension-free), and no upper bound on the second factorial moment is claimed. + +### 1.3 What the results are not + +They are first moments and event probabilities. They are not an all-height intermediate or global count, a torus-wide second factorial moment, a shrinking-separation collision estimate outside the fixed remote region, an elder-selection statement, a numerical constant, a 24-jet certificate, or a status transition. §8 lists the non-claims. + +## 2. Sources consumed, with the exact interface + +| Tag | Source (identities in `SOURCE_MAP.json`) | What is consumed | +|---|---|---| +| [LP] | `imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md` | §2 positive Fourier spectrum and distinct-site jet rank; §3 contact frame `U_r`, uniform regression; (4.1) uniform `C^q` moments of every order under `Q_r`; (5.1) `|alpha_i|, ||beta_i|| <= M_3/2`; (5.3) `det H_i / r = alpha_i det A_i - r beta_i^T adj(A_i) beta_i`; (5.5) `Z_r >= z_* r^2`. All in every fixed `d`; accepted as A1–A4 in the D1 reconciliation. | +| [PP] | `reviews/d5_local_collar_20260928/PUNCTURED_PIN_PROOF.md` | The planar template for Theorem P_d: (P3)–(P20). | +| [CP] | `reviews/d5_local_collar_20260928/COLLAR_PROOF.md` | The planar template for Theorem C_d: (C3)–(C20). | +| [IW] | `frontiers/intermediate_window_20260928/PROOF.md` | The planar template for Theorems I_d, G_d: (I6)–(I34). | +| [RM] | `frontiers/remote_window_20260924/PROOF.md` | Theorem A in every `d`, reviewed (main#76): the outer tile in §7. | +| [RC] | `frontiers/remote_collision_20260928/PROOF.md` | (F-) lower bound; the conditional sentence for `d > 2`. | +| [EDL] | `frontiers/elder_dimension_lift_20260928/PROOF.md` | (A4) `Q^W(N_r >= 2) >= c r^3` in every `d`. | +| [LOCAL] | `frontiers/window_multiplicity_laws_20260928/LOCAL_MULTIPLICITY.md` | The total-variation identity of §7 only. | + +External framework: Armentano, Azaïs and León, arXiv:2304.07424v3, Theorems 2.1, 2.2 and 7.1 with Remarks 7–8, exactly as in [LP] §9, [RM] §5, [PP] §9, [CP] §9 and [IW] §9. The zero-counted field is `grad f : X -> R^d`; parameter and value dimensions agree. + +Planar steps that are dimension-free are cited by their source label and not reproved. A reviewer should read each cited step in its source; this note is not self-contained without them. + +## 3. Five devices + +The planar proofs use, at several places, the two-dimensional facts that a `2 x 2` matrix with two small columns has a small determinant, that a `2 x 2` symmetric matrix is a scalar plus a small correction, and that a bounded intensity integrates to `O(r^3)` over a disk of area `r^2`. The following replace them. + +**Lemma D1 (two soft directions).** Let `H` be a real `d x d` matrix with `||H||_op <= K`, and let `e, e'` be unit vectors with `sigma = ||e wedge e'|| > 0` (the sine of their angle). Then + + |det H| <= ||H e|| ||H e'|| K^(d-2) / sigma, (3.1) + +and every unit vector `w` in `span(e, e')` satisfies `||H w|| <= ( ||H e|| + ||H e'|| ) / sigma`. + +*Proof.* Let `0 <= sigma_1 <= ... <= sigma_d` be the singular values of `H`. Then `|det H| = prod sigma_i <= sigma_1 sigma_2 K^(d-2)`. The singular values of the second exterior power `Lambda^2 H` are the products `sigma_i sigma_j`, `i < j`, so its smallest singular value is `sigma_1 sigma_2`. Apply it to the unit decomposable 2-vector `omega = (e wedge e')/sigma`: `sigma_1 sigma_2 <= ||Lambda^2 H omega|| = ||H e wedge H e'|| / sigma <= ||He|| ||He'|| / sigma`. For the second claim write `w = a e + b e'`; in the plane, Cramer's rule gives `a = ||w wedge e'|| / ||e wedge e'||`, so `|a| <= 1/sigma`, and likewise `|b| <= 1/sigma`. ∎ + +For `d = 2` and `e = e_x`, (3.1) is the planar two-column bound of [PP] §8.1 and [CP] (C18). The finite control `X` checks `det(H)^2 ||u_1 wedge u_2||^2 <= ||Hu_1 wedge Hu_2||^2 ||H||_F^(2(d-2))` on random rational matrices and the equality case on a diagonal family. + +**Lemma D2 (one soft direction).** For a unit vector `e`, `|det H| <= ||H e|| K^(d-1)`. *Proof.* Hadamard's inequality in an orthonormal basis containing `e`; or `sigma_1 <= ||He||`. ∎ + +**Lemma D3 (jet functionals on `R^m`).** Let `beta in R^m`. Coordinates on symmetric matrices, symmetric 3-tensors, and vectors are their independent entries. + +- The linear map `S -> S beta`, `Sym_m -> R^m`, has Gram matrix `G_beta` (over independent entries) with `G_beta >= (|beta|^2 / 2) I_m`. +- The functional `C -> (1/2) beta^T C beta` on `Sym_m` has squared norm `>= |beta|^4 / 4`. +- The functional `D -> D[beta, beta, beta] / 12` on symmetric 3-tensors has squared norm `>= |beta|^6 / 144`. + +*Proof.* For `xi in R^m`, `xi . S beta = sum_i xi_i beta_i S_ii + sum_(i= (1/4) sum_(i,j) (xi_i beta_j + xi_j beta_i)^2 + = (1/4) || xi beta^T + beta xi^T ||_F^2 = (1/2)( |xi|^2 |beta|^2 + (xi . beta)^2 ) >= (1/2) |beta|^2 |xi|^2. + +For the other two, an independent entry with multiplicity `mu in {1, 2}` (resp. `{1, 3, 6}`) carries the coefficient `mu beta_i beta_j / 2` (resp. `mu beta_i beta_j beta_k / 12`); since `mu^2 >= mu`, the squared norm is at least `(1/4) sum_(all ordered) (beta_i beta_j)^2 = |beta|^4/4` (resp. `|beta|^6 / 144`). ∎ + +The finite control `N` checks all three on random rational vectors. + +**Lemma D4 (transverse block determinant).** Let `S in Sym_m`, `hat v` a unit vector, `epsilon = hat v^T S hat v`, `w = S hat v - epsilon hat v` (so `w` is orthogonal to `hat v`), and `S'` the compression of `S` to `hat v^perp`. Then + + det S = epsilon det S' - w^T adj(S') w, |det S| <= |epsilon| ||S||^(m-1) + |S hat v|^2 ||S||^(m-2), (3.2) + +with `det S' = 1`, `adj(S') = 0` when `m = 1`, and `adj(S') = 1` when `m = 2`. + +*Proof.* In an orthonormal basis beginning with `hat v`, `S = [[epsilon, w^T], [w, S']]`, and the first identity is the cofactor expansion (Schur's formula when `S'` is invertible, and by continuity otherwise). Then `||adj(S')||_op <= ||S'||^(m-2)` and `|w| <= |S hat v|`. ∎ + +The finite control `TB` checks the identity and the bound on random rational matrices for `m = 2, 3, 4`. + +**Lemma D5 (pin weight).** For `d >= 2` and `0 < a <= 1/4`, + + integral_(|q| <= a) |q|^(2-d) dq = |S^(m-1)| a (with |S^0| = 2), hence + integral_D omega_d <= (1/2) |S^(m-1)| (1/4), integral_(p^2+|q|^2 <= kappa^2 r^2) omega_d <= 2 kappa r |S^(m-1)| kappa r. + +*Proof.* Polar coordinates in `R^m`: the radial exponent is `(2-d) + (m-1) = 0`. Since `omega_d <= |q|^(2-d)`, both bounds follow. ∎ + +The finite control `W` checks the radial exponent and the nested-ball count exponent `3 + 2 = 5` for `d = 2, ..., 6`. + +## 4. Proof of Theorem P_d + +We follow [PP] §§3–10. Coordinates: translate so that `M = 0` and `S = (r, 0)`; `X = (rp, rq)`, `|p|, |q| <= 1/4`, `(p, q) != 0`. + +### 4.1 Uniform endpoint regression ([PP] §3) + +Let `g(x) = f(x, 0)` and `h(x) = grad_y f(x, 0) in R^m`. The unconditional observation vector + + E_r = ( g(0), g'(0), h(0), [g'(r) - g'(0)]/r, (12/r^3)[ g(r) - g(0) - (r/2)(g'(r) + g'(0)) ], [h(r) - h(0)]/r ) + +has `2 + m + 1 + 1 + m = 2(d+1)` coordinates, is invertibly equivalent to the raw pins for each `r > 0`, has target `e = (b, 0, 0, 0, -12k, 0)` independent of `r`, and contact limit `E_0 = (f, f_x, grad_y f, f_xx, -f_xxx, grad_y f_x)(0)`. Taylor's integral formula gives `E_r - E_0 = O_(L^s)(r)` for every finite `s`, uniformly over frames and locations. The contact functionals are distinct one-site derivative monomials, so [LP] §2 gives positive definite covariance; compactness of `O(d)` makes the floor uniform. The regression coupling `f_(Q_r) = f + Cov(f, E_r) Cov(E_r)^(-1) (e - E_r)` and [LP] (4.1) give, for every fixed `n, s`, uniformly bounded `s`-th moments of the `C^n` norm on the whole torus. + +Define the midpoint jets (all at `0 = M`) + + J = ( A_4, T_3, S_0, C_3 ) = ( f_xxxx, grad_y f_xx in R^m, D_y^2 f in Sym_m, D_y^2 f_x in Sym_m ). + +Their independent entries are distinct derivative monomials of orders `4, 3, 2, 3`, none in `E_0`. So the covariance of `J` after conditioning on `E_r` is uniformly sandwiched and its mean is bounded: a Schur-complement statement for the exact field, as in [PP]. + +### 4.2 Relative remainders ([PP] §4) + +[PP] (P4) is a statement about the axial function `g` alone and is unchanged: + + g'(rp) = 6 k r^2 p(p-1) + (r^3 A_4 / 12) p(p-1)(2p-1) + O(r^4 |p| K). + +Since `h(0) = h(r) = 0` and `h''(0) = T_3`, + + h(rp) = (r^2/2) p(p-1) T_3 + O(r^3 |p| K), h'(rp) = r (p - 1/2) T_3 + O(r^2 K), + +componentwise, by the same two-point Hermite argument. Expanding in `y = rq`, + + f_x(X)/r^2 = 6k p(p-1) + (r A_4/12) p(p-1)(2p-1) + (p - 1/2) q . T_3 + (1/2) q^T C_3 q + epsilon_1, + grad_y f(X)/r = (r/2) p(p-1) T_3 + S_0 q + epsilon_2, (4.1) + +with the pathwise bounds of [PP] (P7) holding for `|epsilon_1|` and `||epsilon_2||` verbatim (norms replace absolute values). The finite control `RO` checks the analogous expansion exactly on a pinned cubic in `d = 3` (there the remainders vanish). + +### 4.3 A stable gradient frame on the whole punctured ball ([PP] §5) + +Set `Delta = (|q|^2 + r^2 p^2)^(1/2) > 0`, `alpha = r p / Delta in [-1, 1]`, `beta = q / Delta in R^m`, so `alpha^2 + |beta|^2 = 1`, and + + Y = ( f_x(X) / (r^2 Delta), grad_y f(X) / (r Delta) ) in R^d. + +From (4.1), + + Y = ( 6k p(p-1) / Delta, 0 ) + B J + R, ||R||_(L^s(Q_r)) <= C_s r, (4.2) + +where the `d x (independent entries of J)` matrix `B = B(p, alpha, beta, Delta)` acts by + + row 1: a(p) alpha A_4 + c(p) beta . T_3 + (Delta/2) beta^T C_3 beta, + rows 2..d: b(p) alpha T_3 + S_0 beta, + a = (p-1)(2p-1)/12, b = (p-1)/2, c = p - 1/2. (4.3) + +The remainder is uniform even when `p` or `q` is arbitrarily small, exactly as in [PP]: `Delta >= |q|` and `Delta >= r|p|` give `r^2|p|/Delta <= r` and `r|q|/Delta <= r`. + +**Rank and floor.** On `|p| <= 1/4`, `|a| >= 1/32`, `|b| >= 3/8`, `|c| >= 1/4` and `b^2 <= 25/64`. Let `B_core` be `B` without the `C_3` block. The `C_3` block only adds a positive semidefinite term to `B B^T`, so `B B^T >= B_core B_core^T`. The `A_4` column contributes `a^2 alpha^2` to the `(1,1)` entry; the `T_3` block contributes the rank-one-plus-diagonal matrix `[[c^2 |beta|^2, c b alpha beta^T], [c b alpha beta, b^2 alpha^2 I_m]]`; the `S_0` block contributes `diag(0, G_beta)` with `G_beta >= (|beta|^2/2) I_m` by Lemma D3. Hence + + B_core B_core^T >= N := [[ a^2 alpha^2 + c^2 |beta|^2, c b alpha beta^T ], [ c b alpha beta, (b^2 alpha^2 + |beta|^2/2) I_m ]]. + +`N` is positive definite on `alpha^2 + |beta|^2 = 1`, and its Schur complement on the first coordinate is + + a^2 alpha^2 + c^2 |beta|^2 - c^2 b^2 alpha^2 |beta|^2 / (b^2 alpha^2 + |beta|^2/2) + = a^2 alpha^2 + c^2 |beta|^4 / (2 b^2 alpha^2 + |beta|^2) + >= min{ a^2/2, c^2 / (4(b^2 + 1)) } >= 1/2048, + +by the case split `|beta|^2 >= 1/2` (second term at least `c^2 (1/4)/(b^2 + 1)`) or `alpha^2 >= 1/2` (first term). Since `det(N) = (Schur complement) (b^2 alpha^2 + |beta|^2/2)^m` and `b^2 alpha^2 + |beta|^2/2 >= min(b^2, 1/2) >= 9/64`, + + det(B B^T) >= det(B_core B_core^T) >= det(N) >= (9/64)^(d-1) / 2048. (4.4) + +For `d = 2` the right side is `9/131072`, the constant of [PP] (P9). The entries of `B` are bounded on the chart, so (4.4) gives a uniform floor `lambda_min(B B^T) >= c_d > 0` on the whole compact parameter set `{|p| <= 1/4} x S^(d-1)`. The finite control `G` checks rank `d`, the block-Schur lower bound and (4.4) on random rational points of the sphere, including `alpha = 0` and `beta = 0`. + +By §4.1, `Cov_(Q_r)(B J) = B Cov(J) B^T >= c B B^T >= c c_d I_d`. The centered `L^2` triangle inequality applied to (4.2), with `r_*` reduced to absorb the `O(r)` remainder, gives + + c_0 I_d <= Sigma := Cov_(Q_r)(Y) <= C_0 I_d. (4.5) + +The axis `q = 0`, `p != 0` (`beta = 0`) is covered by the `A_4, T_3` columns, and the transverse direction `p = 0` (`alpha = 0`) by the `T_3, S_0` blocks. This is a `2(d+1) + d` observation all-height problem; no witness value is pinned. + +### 4.4 Density and the full conditional moment ([PP] §6) + +Put `chi = |p| / Delta`. The mean of `Y` is `dvec + O(1)` with `dvec = (6k p(p-1)/Delta, 0)`, and `(9 k_-/2) chi <= |dvec| <= C chi`. The raw gradient map `grad f(X) -> Y` has Jacobian `(r^2 Delta) (r Delta)^m = r^(d+1) Delta^d`. With `|dvec + z|^2 >= |dvec|^2/2 - |z|^2` and (4.5) in the `d`-dimensional Gaussian density, + + p_( grad f(X) | pins )(0) <= C r^(-(d+1)) Delta^(-d) exp(-c chi^2). (4.6) + +Let `K` dominate the Hessian supremum and its Lipschitz constant on the whole chart. For every fixed `n`, + + E_(Q_r)[ K^n | grad f(X) = 0 ] <= C_n (1 + chi^n). (4.7) + +The argument is [PP] (P12) verbatim: the cross-covariance of `f` and its derivatives through order three with `Y` is bounded by Cauchy–Schwarz and (4.5); the Gaussian residual `f - m_f - C(x) Sigma^(-1)(Y - m_Y)` is independent of `Y` with uniformly bounded `C^3` moments; conditioning `Y = 0` replaces the mean by a function of `C^3` norm at most `C(1 + chi)`. + +### 4.5 The original normalizer, once only + +[LP] (5.5): `Z_r >= z_* r^2` in every fixed `d`. (For `d = 2` [PP] (P14) is an alternative proof.) It is never replaced by a witness-conditioned quantity. + +### 4.6 Two pathwise determinant estimates ([PP] §8) + +Let `A = M`, `B = S`, `C = X` be three exact critical points, `|B - A| = r`, `|C - A| =: d_X = r (p^2 + |q|^2)^(1/2) <= r/4`, `ell = |B - C| <= 5r/4`. The critical-segment identity [PP] (P15), `||H_U e|| <= L |V - U| / 2` for `e = (V-U)/|V-U|`, is one-dimensional along the segment and holds in every `d`. + +**Angle-sensitive bound.** Let `sigma = |sin angle(B - A, C - A)| > 0`, i.e. `q != 0`. Apply Lemma D1 at `A` with `e = e_AB`, `e' = e_AC`: `|det H_A| <= (Lr/2)(L d_X/2) K^(d-2) / sigma`, and `||H_A w|| <= L (r + d_X)/(2 sigma)` for unit `w` in the triangle plane `P`. At `B`, `||H_B e_BA|| <= Lr/2` by the segment `BA`; for the unit vector `w` in `P` orthogonal to `e_BA`, transport gives `||H_B w|| <= ||H_A w|| + L r <= L(r + d_X)/(2 sigma) + L r <= 13 L r / (8 sigma)`; so by Lemma D1 with `sigma = 1`, `|det H_B| <= (13/16) L^2 r^2 K^(d-2) / sigma`. At `C`, the sine of the angle is `r sigma / ell`, and the segments `CA`, `CB` give `|det H_C| <= (L d_X/2)(L ell/2) K^(d-2) ell / (r sigma) <= (25/64) L^2 r d_X K^(d-2) / sigma`. Multiplying, and using `sigma <= 1`, + + |det H_M det H_S det H_X| <= L^6 r^4 d_X^2 K^(3(d-2)) / sigma^4 + = L^6 K^(3(d-2)) r^6 |q|^2 ( 1 + p^2/|q|^2 )^3. (4.8) + +For `d = 2` this is [PP] (P16). Only the `K^(3(d-2))` factor is new; it is the price of the `d - 2` directions in which no Hessian is forced small. + +**Angle-free bound.** Lemma D2 with the short segment `AC` at `A` and at `C`, and the segment `BA` at `B`: + + |det H_M det H_S det H_X| <= (1/8) L^3 K^(3(d-1)) r d_X^2 = (1/8) L^3 K^(3d-3) r^3 (p^2 + |q|^2). (4.9) + +This holds on collinear triangles. The two factors of `d_X` are load-bearing, as in [PP]. + +### 4.7 Weighted Kac–Rice ([PP] §9) + +Unchanged: the counted field is `grad f : X -> R^d`; the nonnegative mark is `W_r 1{H_X in O_j}`, where `O_j` is the open set of nonsingular symmetric matrices of index `j`; the witness determinant enters once through the Jacobian factor; the conditional gradient covariance is positive definite on compact punctures by distinct-site nondegeneracy ([LP] §2), and continuous Gaussian regression supplies the remaining hypotheses of arXiv:2304.07424v3 Theorem 7.1 (Remarks 7–8). Truncation and monotone convergence remove the growth restriction. Thus the intensity per unit physical volume is + + rho_j^W(X) = Z_r^(-1) p_( grad f(X) | pins )(0) E_(Q_r)[ W_r F_j(H_X) | grad f(X) = 0 ]. (4.10) + +### 4.8 The crossover, and the integrable weight ([PP] §10) + +**Region I: `|q| >= r |p|`.** Here `q != 0`. Put `t = |p|/|q|`, so `r^2 t^2 <= 1`, `chi^2 = t^2/(1 + r^2 t^2) in [t^2/2, t^2]`, and `|q|^2 Delta^(-d) <= |q|^(2-d)` because `Delta >= |q|`. Insert (4.8), dropping types, and (4.6), (4.7) with `n = 3d`, and [LP] (5.5) into (4.10): + + rho_j^W(X) <= C r^(-2) r^(-(d+1)) Delta^(-d) e^(-c chi^2) r^6 |q|^2 (1 + t^2)^3 (1 + chi^(3d)) + <= C r^(3-d) |q|^(2-d) sup_t (1 + t^2)^3 (1 + t^(3d)) e^(-c t^2/2) + <= C' r^(3-d) |q|^(2-d). (4.11) + +**Region II: `|q| < r |p|`.** Here `p != 0`, `Delta >= r|p|`, `Delta^2 <= 2 r^2 p^2`, `chi^2 in [1/(2r^2), 1/r^2]`, and `p^2 + |q|^2 <= 2 p^2 = 2 (r|p|)^2 / r^2`. Insert (4.9) instead: + + rho_j^W(X) <= C r^(-2) r^(-(d+1)) (r|p|)^(-d) e^(-c chi^2) r^3 (r|p|)^2 r^(-2) (1 + chi^(3d)) + <= C r^(-2-4d) e^(-c/(2r^2)) (r|p|)^(2-d) + <= C r^(3-d) (r|p|)^(2-d), (4.12) + +the middle step using `1 + chi^(3d) <= 2 r^(-3d)`, and the last step `e^(-c/(2r^2)) <= n! (2/c)^n r^(2n)` with `2n >= 5 + 3d`. The longitudinal axis `q = 0` is included; no division by `q` is made. + +**Integration.** In both regions `rho_j^W(X) <= C r^(3-d) omega_d(p, q)` with `omega_d` from (1.1). Apply (4.10) on increasing compact punctures and use monotone convergence. Since `dX = r^d dp dq`, + + E_(Q_r^W) N_j(M + rE) = integral_(rE) rho_j^W <= C r^3 integral_E omega_d(p, q) dp dq, + +which is (1.2). Lemma D5 gives the finite right side and the `O(r^5)` nested-ball bound. For `d = 2`, `omega_2 = 1` and this is [PP] (P2) with a bounded intensity; for `d >= 3` the intensity is unbounded on the axis but its weight is integrable, which is exactly why the count still has order `r^3`. ∎ + +### 4.9 Reflection to `S` + +[PP] §10.1 applies verbatim: use the reflected local field `tilde f(x, y) = f(S - x e_1 + R_y y)` for any orthogonal map `R_y` of the transverse space (a reflection of one transverse axis keeps the orientation if desired; only orthogonality matters), with `tilde b = b - k r^3`, `tilde k = -k`. Sections 4.1–4.4 use only boundedness of the targets and `|k| >= k_-`; the deterministic estimates are index-free; the weighted Kac–Rice argument uses the relabeled original mark `F_(d-1)(H_0) F_d(H_r)`, the same random variable as `W_r`; and the original `Z_r` is retained. The two physical balls of radius `r/4` about `M` and `S` are disjoint. + +## 5. Proof of Theorem C_d + +We follow [CP] §§3–10 in midpoint coordinates `X = r(u, v)`, `u in R`, `v in R^m`, with the exact endpoint cubic `H_r(x) = b - k r^3/2 - (3k r^2/2) x + 2k x^3` and the midpoint jets `T_3 = grad_y f_xx(0) in R^m`, `C_3 = D_y^2 f_x(0) in Sym_m`, `S_0 = D_y^2 f(0) in Sym_m`. + +### 5.1 Degree-five value-and-gradient interpolation at three sites ([CP] §3) + +Let `a = (-1/2, 0)`, `b = (1/2, 0)`, `c = (u, v)` be the three sites of the collar; pairwise distances are at least `min(1, eta)`. Let `P_5` be the polynomials on `R^d` of total degree at most five; `dim P_5 = C(d+5, 5) >= 3(d+1)`. Consider + + B_c : P_5 -> R^(3(d+1)), P -> ( P(a), grad P(a), P(b), grad P(b), P(c), grad P(c) ). + +**Lemma.** `B_c` is onto for every `c` in `C(eta, R)`, including collinear configurations and `c = 0`, and its smallest row singular value has a uniform positive lower bound on `C(eta, R)` in the fixed monomial basis. + +*Proof.* Choose a unit direction `w` such that the three projections `t_i = w . x_i` are distinct: for each of the three pairs the directions orthogonal to `x_i - x_j` form a great subsphere of `S^(d-1)`, a closed set with empty interior, so such `w` exists. Complete `w` to an orthonormal basis `w, w_1, ..., w_m` and write `z_j = w_j . x`, `z_(i,j) = w_j . x_i`. With the degree-two Lagrange polynomials `L_i(t)` at `t_1, t_2, t_3`, the polynomials + + h_i(t) = [ 1 - 2 L_i'(t_i)(t - t_i) ] L_i(t)^2, + d_i(t) = (t - t_i) L_i(t)^2, + e_(i,j)(t, z) = (z_j - z_(i,j)) L_i(t)^2, j = 1, ..., m, + +have total degree at most five. At the three sites, `h_i` has value `delta_(ij)` and zero gradient; `d_i` has zero value, `w`-derivative `delta_(ij)` and zero transverse derivatives; `e_(i,j)` has zero value and `w`-derivative and transverse derivative `delta_(ij)` in the `w_j` direction. These `3(1 + 1 + m) = 3(d+1)` polynomials prescribe arbitrary values and gradients, so `B_c` is onto in the original coordinates. Its entries are polynomials in `(u, v)`; surjectivity at every point of the compact collar gives a positive minimum of the least eigenvalue of `B_c B_c^T`. A single continuous choice of `w` is not needed. ∎ + +### 5.2 The coarse uniform floor ([CP] §4) + +Collect the `3(d+1)` observations `V_r = ( f(ra), r grad f(ra), f(rb), r grad f(rb), f(rc), r grad f(rc) )`. With `J_5` the `C(d+5, 5)` midpoint Taylor coefficients `D^alpha f(0)/alpha!` and `D_r = diag(r^|alpha|)`, Taylor's formula through total degree five gives `V_r = B_c D_r J_5 + R_r`, `||R_r||_(L^s) <= C_s r^6` (the gradient entries carry `r . O(r^5)`), using [LP] (4.1) for the sixth derivatives. `Cov(J_5)` is uniformly positive definite (distinct one-site monomials, [LP] §2, compactness in the frame). For a unit row `t`, `std(t B_c D_r J_5) >= c r^5 ||t B_c|| >= c' r^5`, and the `L^2` triangle inequality gives `Cov(V_r) >= c r^10 I_(3(d+1))` for small `r`. Delete the auxiliary witness value (a principal submatrix keeps the floor), unscale the gradient entries by `r^(-1) >= 1`, and take the Schur complement on the `2(d+1)` pins. Hence + + Sigma_X := Cov_(Q_r)( grad f(X) ) >= c r^10 I_d, Sigma_X <= C I_d. (5.1) + +Only `2(d+1) + d` observations are conditioned; no witness value and no height window appear. + +### 5.3 The pinned drift ([CP] §5) + +With `D(u) = u^2 - 1/4`, the endpoint pins and Taylor's formula give, uniformly on `|u|, |v| <= R`, + + G_1 := f_x(ru, rv)/r^2 = 6k D(u) + u v . T_3 + (1/2) v^T C_3 v + O_(L^s)(r), + G_2 := grad_y f(ru, rv)/r = S_0 v + O_(L^s)(r), (5.2) + +exactly as [CP] (C7), with `v . T_3`, `v^T C_3 v` and `S_0 v` replacing the planar products. Hence `|E_(Q_r) G_1 - 6k D(u)| <= C(|v| + r)` and `Var_(Q_r)(G_1) <= C(|v|^2 + r^2)`. On `|v| <= v_0 <= eta/2` the collar gives `|D(u)| >= eta^2/4`, so `|E_(Q_r) G_1| >= d_0 > 0` after reducing `v_0` and `r_*`. The one-coordinate Mahalanobis bound `m^T Sigma^(-1) m >= m_1^2 / Sigma_11` [CP] (C10) supplies the factor `exp[-c/(r^2 + |v|^2)]` in the joint `d`-dimensional density. + +### 5.4 Very near the axis: `|v| <= r^(1/3)` ([CP] §6) + +By (5.1) the density prefactor is at most `C r^(-5d)`, so + + p_( grad f(X) | pins )(0) <= C r^(-5d) exp[-c r^(-2/3)]. + +Regress the whole field on `grad f(X)`: `||Sigma_X^(-1)|| <= C r^(-10)`, bounded cross-covariances, bounded targets, and the independent residual give `E_(Q_r)[ K^(3d) | grad f(X) = 0 ] <= C r^(-30d)`. The product of three absolute determinants is at most `K^(3d)`. Divide once by [LP] (5.5): + + rho_j^W(X) <= C r^(-2-35d) exp[-c r^(-2/3)] <= C r^(3-d), + +by the `n`-th term of the exponential series with `2n/3 >= 5 + 34d`. The exact midpoint and the whole axis `v = 0` are covered. + +### 5.5 The rest of the near-axis strip: `r^(1/3) <= |v| <= v_0` ([CP] §7) + +Write `G = (G_1, G_2) = (6k D(u), 0) + B J + R`, `J = (T_3, C_3, S_0)`, `||R||_(L^2) <= C r`, with + + row 1: u v . T_3 + (1/2) v^T C_3 v, rows 2..d: S_0 v. + +The `C_3` block acts only on row 1 and the `S_0` block only on rows `2..d`, so by Lemma D3 + + B B^T >= diag( |v|^4/4, (|v|^2/2) I_m ) >= (|v|^4/4) I_d (|v| <= sqrt 2), + +and `trace(B B^T) <= C_R |v|^2`. The conditional covariance of `J` is uniformly sandwiched (§4.1, now at the midpoint), so `Cov(B J) >= c |v|^4 I_d`. Since `r/|v|^2 <= r^(1/3)`, the centered remainder is at most half the leading standard deviation for small `r`, and + + c |v|^4 I_d <= Cov_(Q_r)(G) <= C |v|^2 I_d. (5.3) + +The physical gradient map is `diag(r^2, r I_m)` with determinant `r^(d+1)`. Using §5.3 and (5.3), + + p_( grad f(X) | pins )(0) <= C r^(-(d+1)) |v|^(-2d) exp[-c/|v|^2], (5.4) + E_(Q_r)[ K^(3d) | grad f(X) = 0 ] <= C |v|^(-12d), (5.5) + +the latter by regression on `G` with `||Cov(G)^(-1)|| <= C |v|^(-4)`. + +**Three soft Hessians in the collar.** The segment `MS` gives `||H_M e_x|| <= Lr/2`. From `grad f(X) = grad f(M) = 0`, `||H_M (X - M)|| <= L |X - M|^2 / 2 <= C_R L r^2`; since `X - M = r((u + 1/2) e_x + v)`, subtracting the controlled `e_x` component gives `||H_M v|| <= C_R L r`, hence `||H_M hat v|| <= C_R L r / |v|`. The plane `P = span(e_x, hat v)` is orthonormal because `v` is transverse. Lemma D1 with `sigma = 1` gives `|det H_M| <= C_R L^2 r^2 K^(d-2) / |v|`, and for every unit `w in P`, `||H_M w|| <= C_R L r / |v|` (using `|v| <= R`). Transport to `S` and to `X` (distances at most `(R+1) r`) keeps `||H_S w||, ||H_X w|| <= C_R L r / |v|` on `P`, so `|det H_S|, |det H_X| <= C_R L^2 r^2 K^(d-2) / |v|^2`. Therefore + + |det H_M det H_S det H_X| <= C_R K^(3d) r^6 |v|^(-6) (5.6) + +(we used `|v|^(-5) <= 2 |v|^(-6)` for `|v| <= 2` and `L <= K`). For `d = 2` this is [CP] (C18). Combining [LP] (5.5), (5.4), (5.5), (5.6): + + rho_j^W(X) <= C r^(3-d) |v|^(-(14d+6)) exp[-c/|v|^2] <= C' r^(3-d). (5.7) + +The radius powers are `-2 - (d+1) + 6 = 3 - d`. No height-window factor appears. + +### 5.6 Transverse compact remainder: `|v| >= v_0` ([CP] §8) + +`B` has a fixed positive singular-value floor, the `O(r)` error is absorbed uniformly, the reduced mean, inverse covariance and conditional `C^3` moments are bounded, the density is `O(r^(-(d+1)))`, (5.6) gives `O(r^6)`, and division by `Z_r` leaves `rho_j^W <= C r^(3-d)`. No assertion that `D(u)` is separated from zero is needed here. + +### 5.7 Integration and synthesis ([CP] §§9–10) + +Weighted Kac–Rice on an open neighbourhood of the compact collar (distinct-site nondegeneracy, or the local polynomial floor), with the mark `W_r 1{H_X in O_j}`, gives (4.10) there. Since `dX = r^d du dv` and `rho_j^W <= C r^(3-d)` on all three strips, `E_(Q_r^W) N_j(rE) <= C r^3 |E|`, which is (1.3). + +For (1.4), take `eta = 1/4`, partition a Borel subset of the scaled ball into its intersections with the two punctured pin balls of scaled radius `1/4` (Theorem P_d in endpoint coordinates; translation preserves volume) and the remaining collar (this theorem); assign boundaries once. Take the minimum of the radius cutoffs and the maximum of the constants. Choosing `R` larger than the inner radius of a scaled annulus supplies an overlapping cover of it. ∎ + +## 6. Proof of Theorem I_d + +We follow [IW] §§3–10 with `epsilon = r/s in (0, 1/4]`, the endpoint frame `U_r` of [IW] (I7) extended by the `2m` transverse rows `L_r(0) in R^m`, `L_r'(0) in R^m` (affine interpolants of `grad_y f` at `+-r/2`), the scaled vector + + V_(r,s,w) = ( S_s U_r, f(sw), s grad f(sw) ), S_s = diag(1, s, s^2, s^3, s I_m, s^2 I_m), w = (u, v) in A = {1 <= |w| <= 2}, + +which has `2(d+1) + (d+1)` coordinates, and the endpoint-law inputs [IW] (I6), which are [LP] (4.1) and (5.5) in every `d`. + +### 6.1 Polynomial row rank through `epsilon = 0` ([IW] §3.1) + +For `epsilon > 0` the three sites `(-epsilon/2, 0)`, `(epsilon/2, 0)`, `w` are distinct and §5.1 gives rank `3(d+1)` on `P_5`, hence rank `3(d+1)` for the transformed rows (the Hermite transform is invertible). At `epsilon = 0` the `2(d+1)` contact rows `(f, f_x, f_xx, f_xxx, grad_y f, grad_y f_x)(0)` are independent. Polynomials of degree at most five annihilated by all of them are spanned by the monomials other than `1, x, x^2, x^3, y_j, x y_j`. To control the remaining `d + 1` rows: + +- if `v != 0`, rotate the transverse frame so `v = |v| e_1` (the contact functionals are covariant under transverse rotations), and use `y_1^2, y_1^3, x y_1^2, y_j y_1^2 (j = 2..m)`. Their value/gradient matrix at `w` is block triangular: the `y_j`-derivative block is `|v|^2 I_(m-1)`, and the `3 x 3` block on `(value, d/dx, d/dy_1)` has determinant `-|v|^6`, so the total determinant is `-|v|^(2d+2) != 0`; +- if `v = 0`, then `|u| >= 1`, and `x^4, x^5, x^2 y_j` have value/gradient determinant `u^8 . u^(2m) = u^(2d+6) != 0`. + +So the `(3(d+1)) x dim P_5` matrix `B_(epsilon, w)` has full row rank also at confluence. Its entries are polynomial in `epsilon`, hence continuous at `epsilon = 0`; compactness of `[0, 1/4] x A` supplies a uniform positive smallest row singular value. Degree four fails: on the axis, the annihilated monomials of degree at most four have proportional value and `x`-derivative at `(u, 0)` (only `x^4` contributes), so the witness rows have rank at most `d < d + 1`. The finite control `R` checks the two explicit families, a general rational transverse direction with a rational basis of its orthogonal complement, the degree-five rank `d + 1` and the degree-four rank `d` on the axis, for `d = 2, 3, 4`. + +### 6.2 Taylor remainder, floor and conditional floor ([IW] §3.2) + +[IW]'s divided-difference argument is one-dimensional along the axis and applies to each transverse component: every scaled endpoint coordinate is a bounded functional on `C^3` uniformly for `0 <= epsilon <= 1/4`, with the mass-one kernel identity for `H'''(0)` unchanged. Hence `V = B_(epsilon, w) D_s J_5 + R`, `||R||_(L^p) <= C_p s^6`, the standard-deviation floor `c s^5 ||a B||`, and + + Cov(V_(r,s,w)) >= c s^10 I, Sigma_X := Cov_(Q_r)( grad f(X), f(X) ) >= c s^10 I_(d+1), (6.1) + +by unscaling and the Schur variational identity, exactly as [IW] (I10), (I11). + +### 6.3 Midpoint expansions and the height coordinate ([IW] §4) + +Let `T_3 = grad_y f_xx(0) in R^m`, `C_3 = D_y^2 f_x(0) in Sym_m`, `D_3 = D_y^3 f(0)` (symmetric 3-tensor), `S_0 = D_y^2 f(0) in Sym_m`. The endpoint constraints give, pathwise with `K` a fixed multiple of `1 + ||f||_(C^6)`, + + |f(0) - b_bar| <= C r^4 K, f_x(0) = -3k r^2/2 + O(r^4 K), grad_y f(0) = -r^2 T_3/8 + O(r^4 K), + |f_xx(0)| + ||grad_y f_x(0)|| <= C r^2 K, f_xxx(0) = 12k + O(r^2 K), (6.2) + +by the same averaged endpoint identities as [IW] (I12), applied to each transverse component. With `d_e = u^2 - epsilon^2/4`, at `X = s(u, v)`, + + f_x(X)/s^2 = 6k d_e + u v . T_3 + (1/2) v^T C_3 v + O(sK), + grad_y f(X)/s = S_0 v + (s/2) d_e T_3 + s u C_3 v + (s/2) D_3[v, v] + O(s^2 K), + [f(X) - b_bar]/s^3 = k(2u^3 - 3 epsilon^2 u/2) + v^T S_0 v/(2s) + (d_e/2) v . T_3 + (u/2) v^T C_3 v + (1/6) D_3[v,v,v] + O(sK). (6.3) + +The row operation `Z = ( f_x/s^2, grad_y f/s, [f - b_bar - (s/2) v . grad_y f]/s^3 )` removes the `S_0/s` term and the `C_3` term from the height row: + + Z = ( 6k d_e, 0, k(2u^3 - 3 epsilon^2 u/2) ) + B J + O_(L^p)(s), J = (T_3, C_3, D_3, S_0), + row 1: u v . T_3 + (1/2) v^T C_3 v, + rows 2..d: S_0 v, + row d+1: (d_e/4) v . T_3 - (1/12) D_3[v, v, v]. (6.4) + +The map from `Z` to `(f_x, grad_y f, f - b_bar)` is triangular with determinant `s^(2 + m + 3) = s^(d+4)`. The target at height `y in I_r` and zero gradient is `tau = (0, 0, (y - b_bar)/s^3)`, `|tau_(d+1)| <= (k_+/2) epsilon^3`, bounded through `epsilon -> 0`. The finite control `RO` checks (6.3)–(6.4) exactly on a pinned cubic in `d = 3`: no negative power of `s`, `S_0` and `C_3` absent from the height row, and the displayed coefficients. + +### 6.4 Euler suppression and the transverse determinants ([IW] §5) + +Suppose the pins hold, `grad f(X) = 0` and `f(X) = y in I_r`. Taylor expansion about `0` through degree three and Euler's identity for homogeneous polynomials give, in every `d`, + + 3[f(X) - f(0)] - X . grad f(X) = 2 grad f(0) . X + (1/2) X^T H_0 X + O(s^4 K), (6.5) + +the cubic terms cancelling because their Euler degree is three (finite control `EU` in `d = 3`). Here `(1/2) X^T H_0 X = (s^2/2)[ u^2 f_xx(0) + 2u grad_y f_x(0) . v + v^T S_0 v ]`. By (6.2), `|y - b_bar| <= k_+ r^3/2` and `r <= s/4 <= 1`, every term other than `(s^2/2) v^T S_0 v` is `O(K(r^2 s + s^4))`, so for `v != 0`, with `hat v = v/|v|`, + + | hat v^T S_0 hat v | <= C K (r^2/s + s^2) / |v|^2 <= C K (r + s^2) / |v|^2. (6.6) + +This is [IW] (I18) for the quadratic form in the direction `v`. It controls one entry of `S_0`, not the matrix. The second piece of information is the transverse gradient equation: from `grad_y f(X) = 0` and the second line of (6.3), `S_0 v = O(sK)`, that is + + | S_0 hat v | <= C s K / |v|. (6.7) + +**Endpoint determinants.** Let `A_i = D_y^2 f(i)` for `i in {M, S}`; then `A_i = S_0 + O(rK)` by the Lipschitz bound over distance `r/2`, so `|hat v^T A_i hat v| <= C K (r + s^2)/|v|^2` (absorbing `rK <= 4 rK/|v|^2`) and `|A_i hat v| <= C s K/|v|`. Lemma D4 gives + + |det A_i| <= C K^(d-2) (r + s^2)/|v|^2 + C K^(d-3) s^2 K^2/|v|^2 <= C K^(d-1) (r + s^2)/|v|^2 + +(the second term is absent when `d = 2`, where `A_i` is the scalar `epsilon_i`). With [LP] (5.3) and (5.1), `|det H_i| = r |alpha_i det A_i - r beta_i^T adj(A_i) beta_i| <= r K |det A_i| + r^2 K^d`, hence + + |det H_M|, |det H_S| <= C r K^d (r + s^2) / |v|^2. (6.8) + +For `d = 2` this is [IW] (I19). The second term of Lemma D4, of size `s^2/|v|^2`, is of the same order as the `s^2` part of the Euler bound; that coincidence is what makes the lift work without loss. + +**Witness determinant.** As in [IW] (I20), `||H_M e_x|| <= Lr/2` and `||H_M (X - M)|| <= C K s^2` give `||H_M hat v|| <= C K s/|v|`; transport over distance at most `3s` gives `||H_X e_x|| <= C K s` and `||H_X hat v|| <= C K s/|v|`. Lemma D1 on the orthonormal pair `(e_x, hat v)`: + + |det H_X| <= C s^2 K^d / |v|. (6.9) + +Combining (6.8), (6.9), dividing once by [LP] (5.5) and using `r^2/s <= r`, + + W_r |det H_X| / Z_r <= C K^(3d) s^2 (r + s^2)^2 |v|^(-5). (6.10) + +On the axis, retain only the two endpoint short columns (Lemma D2 with `e_x`): `W_r |det H_X| <= C r^2 K^(3d)`, which cancels the normalizer with no division by `v`. + +### 6.5 Small axial strip ([IW] §6) + +On `A` and `|v| <= v_0`, `|u|` is bounded below and `d_e >= c > 0`; the first line of (6.3) gives `|E_(Q_r)[f_x(X)/s^2]| >= c_0` and `Var <= C(|v|^2 + s^2)`; the one-coordinate Mahalanobis bound applies to the full `(d+1)`-dimensional exponent. On `|v| <= s^(1/8)`, (6.1) gives the joint density bound `C s^(-5(d+1)) exp[-c s^(-1/4)]`, regression on `Y_X = (grad f(X), f(X))` with `||Sigma_X^(-1)|| <= C s^(-10)` gives `E[K^(3d) | grad f(X) = 0, f(X) = y] <= C s^(-30d)`, and with the axis bound of §6.4 and [LP] (5.5) the intensity per unit volume and height is bounded by `C s^(-N) exp[-c s^(-1/4)] <= C`. The strip has volume `O(s^d) <= O(s^2)` and the window length is `k r^3`, so it contributes at most `C r^3 s^2` to the shell count. + +### 6.6 Transverse region: `s^(1/8) <= |v| <= 2` ([IW] §7) + +In (6.4) the three jet blocks `C_3`, `S_0`, `D_3` act on disjoint row sets, so by Lemma D3 + + B B^T >= diag( |v|^4/4, (|v|^2/2) I_m, |v|^6/144 ), det(B B^T) >= c |v|^(2d+8), sigma_min(B) >= c |v|^3, + +and `||B|| <= C|v|`. The conditional covariance of `J` is uniformly sandwiched, so the leading standard deviation of `a . Z` is at least `c ||aB|| >= c |v|^3 ||a||`, while the centered `O(s)` error is at most `C s ||a||`; since `s/|v|^3 <= s^(5/8)`, the error is at most half the leading term for small `s`, giving the relative bound + + Cov_(Q_r)(Z) >= c B B^T, det Cov_(Q_r)(Z) >= c |v|^(2d+8), ||Cov_(Q_r)(Z)^(-1)|| <= C |v|^(-6), Cov_(Q_r)(Z) <= C |v|^2 I. (6.11) + +With the Jacobian `s^(d+4)` and the Gaussian penalty `exp(-c/|v|^2)` from §6.5 (or a constant for `|v| >= v_0`), + + p_( grad f(X), f(X) | pins )(0, y) <= C s^(-(d+4)) |v|^(-(d+4)) exp(-c/|v|^2), (6.12) + E_(Q_r)[ K^(3d) | grad f(X) = 0, f(X) = y ] <= C |v|^(-18d), (6.13) + +the latter by regression on `Z` with (6.11) and the bounded target `tau`. + +### 6.7 The shell ledger ([IW] §8) + +Insert (6.10) into the conditional expectation of the weighted density and apply (6.12), (6.13): + + Lambda_(r,j)(X, y) <= C s^(-(d+2)) (r + s^2)^2 |v|^(-(19d+9)) exp(-c/|v|^2) <= C' s^(-(d+2)) (r + s^2)^2. (6.14) + +Every inverse power of `|v|` is absorbed by its Gaussian factor uniformly down to `s^(1/8)`. Integrate over the physical shell (volume `O(s^d)`) and the window (length `k r^3`): + + E N_(r,j)(shell, transverse) <= C r^3 (r + s^2)^2 / s^2 <= 2C r^3 [ (r/s)^2 + s^2 ], (6.15) + +by `(a + b)^2 <= 2a^2 + 2b^2`; equivalently `2[(r/s)^2 + s^2] - (r + s^2)^2/s^2 = (r/s - s)^2 >= 0` (finite control `L`). Adding the axial contribution of §6.5 proves (1.5). The `r` powers are `-2 + 2 + 3 = 3` and the `s` powers `-(d+4) + 2 + d = -2` in every `d`. + +### 6.8 Kac–Rice with height disintegration, and the dyadic sum ([IW] §§9–10) + +For each `r, s > 0` the closed shell is separated from the pins; (6.1) gives nondegeneracy of `(grad f(X), f(X))`; the marked critical-point formula with the mark `W_r 1{H_X in O_j} 1{f(X) in I_r}` and height disintegration gives + + E_(Q_r^W) N_(r,j)(B) = integral_B integral_(I_r) Lambda_(r,j)(X, y) dy dX, + Lambda_(r,j)(X, y) = Z_r^(-1) p_( grad f(X), f(X) | pins )(0, y) E_(Q_r)[ W_r F_j(H_X) | grad f(X) = 0, f(X) = y ], + +exactly as [IW] (I33), with the same framework citation. The dyadic sum [IW] (I34) is dimension-free: `sum_j (r/s_j)^2 <= 4/(3 A_0^2)` and `sum_j s_j^2 <= (4/3) rho^2` for `s_j = 2^j A_0 r`. This proves (1.6). ∎ + +## 7. Proof of Theorem G_d and the corollaries + +Use one `(Q_r, W_r, Z_r)` throughout, distances from the midpoint, and the tiling of [IW] §10 and its review (N1): + +| Region | Source | Parameters | Heights | +|---|---|---|---| +| `|X| <= 4r`, pins removed | Theorem C_d, (1.4) with `R = 4` | fixed | all heights, which contain `I_r` | +| `4r <= |X| <= s_0` | Theorem I_d, (1.6) with `A_0 = 4`, `rho = s_0` | fixed `s_0` | `I_r` | +| `|X| >= s_0` | [RM] Theorem A, "fix `0 < rho < L/4`", reviewed ACCEPT in every fixed `d` (main#76) | `rho = s_0` | `I_r` | + +Boundaries are assigned once and `r` is taken below all three cutoffs. No annulus is left uncovered, no regional normalizer is multiplied, and no pin-density Jacobian is inserted. Summing the three bounds gives (1.7). + +*Corollary F_d.* `Q_r^W(A_r) <= E_(Q_r^W) sum_j N_(r,j)(X minus {M, S}) <= (d+1) C r^3` by Markov; the lower bound is [RC] (F-), whose proof uses only [RM] (A) and the fixed-remote second factorial moment (D), both valid in every fixed `d`. ∎ + +*Corollary M_d.* [EDL] (A4) gives `Q_r^W(N_r >= 2) >= c r^3` and `E[N_r(N_r - 1)] >= c r^3` in every fixed `d`. For the upper bound, `1{N >= 2} <= N/2` and (1.7). The total-variation statement is [LOCAL] §7 (an identity for any finite point process with mean mass at most one) applied with (1.7) and (A4). ∎ + +## 8. What this note does not establish + +- An all-height intermediate or global `O(r^3)` count. The height window in (6.6) is load-bearing, as [IW] and its reviews record; the all-height shell method gives `O(r)`, not `O(r^3)`. +- A torus-wide second factorial moment upper bound, or any collision estimate outside the fixed remote region of [RC]. +- Elder selection; D1 Theorem A covers it separately. +- Uniformity as `k -> 0`, as marks grow, as `L` or `d` vary, or any numerical `C`, `c`, `r_*`, `s_0`. +- Any recovery of historical RN/JETMOD/24-jet carriers, or any change to their `BLOCKED_ABSENT` / `OPEN_HISTORICAL` classifications. Theorem G_d in `d = 3` is an analytic, existential-constant statement about the same kind of object those carriers were meant to certify numerically; whether the registers should record a regional supersession is a separate source-bound reconciliation, not something this note asserts. +- Organizational independence: every lane shares one GitHub account. + +The candidate's own review obligations are listed in `README.md`. A defect in any of the five devices, or in any planar step cited here as dimension-free, blocks consumption of the corresponding theorem. + +## 9. Finite controls + +`lift_exact_check.py` (standard library, exact rational and polynomial arithmetic) checks the nine groups listed in its docstring and rejects ten deliberate mutations: the exterior-power order, the two frame blocks, the interpolation degree, the row-operation constant, the Euler coefficient, the adjugate sign, one soft direction instead of two, a non-summable shell factor, and a non-integrable pin weight. `RESULTS.json` is its exact output, identical in normal and optimized modes. These checks verify identities, ranks, floors and exponents. They do not verify the Gaussian, compactness, regression, or Kac–Rice steps, which are the written arguments above and in the sources. + +## 10. Attribution and reconnaissance + +The mechanisms are those of the planar sources; the contribution here is the written `d`-dimensional replacement of each planar-specific step and the five devices of §3, which are classical linear algebra (exterior powers, Hadamard, Schur complements) applied at the right places. Nothing is claimed as new beyond this explicit application. `RECONNAISSANCE.md` records the limited external check and its failure mode. diff --git a/frontiers/d5_dimension_lift_20260929/README.md b/frontiers/d5_dimension_lift_20260929/README.md new file mode 100644 index 000000000..08fbe759d --- /dev/null +++ b/frontiers/d5_dimension_lift_20260929/README.md @@ -0,0 +1,52 @@ +# D5 in every fixed dimension (CL-D5-DIMENSION-LIFT-20260929-v1) + +Author-side proof candidate by Anthropic Claude. **Nonauthor analytic review required.** Scientific effect: NONE. + +## What it proves, if the arguments hold + +The three planar D5 components and their composition, in every fixed `d >= 2`, for the exact model of `imports/lifetime_parent_20260925` with compact marks, the original endpoint weight and the full normalizer: + +| Result | Statement | Planar source it lifts | +|---|---|---| +| Theorem P_d | all-height punctured pin ball: `E N_j(M + rE) <= C r^3 ∫_E max(|q|, r|p|)^(2-d)` | `PUNCTURED_PIN_PROOF.md` (P2) | +| Theorem C_d | compact collar `E N_j(rE) <= C r^3 |E|` and the fixed scaled ball minus pins | `COLLAR_PROOF.md` (C1), (C2) | +| Theorem I_d | height-window shells `E N <= C r^3[(r/s)^2 + s^2]`, dyadic sum `C r^3(A_0^-2 + rho^2)` | `intermediate_window_20260928` (I3), (I4) | +| Theorem G_d | global window first moment `E_(Q^W) N(T^d minus {M,S}) <= C r^3` | `intermediate_window_20260928` (I5) | +| Corollary F_d | `c r^3 <= Q^W(A_r) <= C r^3` in every `d` | closes the `d > 2` conditional in `remote_collision_20260928` Corollary F | +| Corollary M_d | `Q^W(N_r >= 2) = Theta(r^3)` in every `d`; no `O(r^5)` global factorial bound | `LOCAL_MULTIPLICITY.md` Theorem L, `elder_dimension_lift` (A4) | + +The application dimension of the program is `d = 3` (SIDE24). Until now every D5 upper bound was planar. + +## The five devices (PROOF.md §3) + +1. Two soft directions: `|det H| <= ||He|| ||He'|| K^(d-2) / sigma` through the second exterior power. Replaces the planar two-column bound at each of the three Hessians. +2. One soft direction: `|det H| <= ||He|| K^(d-1)` (Hadamard). The angle-free bound. +3. Jet functionals on `R^m`: the Gram of `S -> S beta` is at least `|beta|^2/2`; the `C` and `D` functionals have norms at least `|beta|^2/2` and `|beta|^3/12`. Gives the frame floors, including the explicit pin-frame floor `det(BB^T) >= (9/64)^(d-1)/2048`, which is the planar `9/131072` at `d = 2`. +4. Transverse block determinant: `det S = eps det S' - w^T adj(S') w`. The Euler identity controls `eps` and the gradient equation controls `w`; together they control `det` of the endpoint transverse blocks with the same `(r + s^2)/|v|^2` as the planar scalar. +5. Integrable pin weight `max(|q|, r|p|)^(2-d)`: the intensity is unbounded on the axis for `d >= 3`, but its integral over the ball is `O(1)`, so the count keeps order `r^3`. + +## Run + + python -B -S lift_exact_check.py # rc 0, output = RESULTS.json + python -B -O -S lift_exact_check.py # rc 0, byte-identical + python -B -S lift_exact_check.py --mutant NAME # rc 1 for each of the ten names in the docstring + +Nine groups of exact checks (`X G R RO EU TB N L W`): exterior-power inequality and its equality case, frame rank and floors on rational points of the sphere, confluent interpolation rank in `d = 2, 3, 4` with the degree-four negative control, the `d = 3` row operation on an exactly pinned cubic, the `d = 3` Euler identity, the block-determinant identity, the three jet-functional norms, all power ledgers for `d = 2..6`, and the pin-weight exponents. They verify identities, ranks, floors and exponents only. + +## Review requests (exact interfaces) + +1. Lemma D1: the singular values of `Λ²H` are the pairwise products; the plane coefficient bound `1/sigma`. +2. Lemma D3: the Gram of `S -> S beta` over independent entries, `>= |beta|^2/2`; the block-Schur computation (4.4). +3. Lemma D4 and its use in (6.8): that `hat v^T S_0 hat v` (Euler) and `S_0 hat v` (gradient equation) together control `det A_i`, with the `s^2/|v|^2` cross term. +4. Lemma D5: integrability of the weight and the `O(r^5)` nested-ball bound; the region I/II ledgers (4.11), (4.12). +5. §5.1 and §6.1: degree-five interpolation in `d` variables, the confluent families, and the compactness step. +6. The tiling in §7, and the claim that [RM] Theorem A, [RC] (F-) and [EDL] (A4) are consumed at their stated every-`d` scope. +7. Every step cited as "verbatim" from a planar source: confirm it is in fact dimension-free. + +## What this does not do + +No all-height global count, no torus-wide second factorial moment, no collision estimate outside the fixed remote region, no elder-selection claim, no numerical constant, no uniformity in `k`, `L` or `d`, no recovery of historical carriers, no register change. The relation to `hist.OBL-H5-JETMOD` and the D5 region nodes of `frontiers/downstream_gate_20260925/GRAPH.json` is a matter for a later source-bound reconciliation after nonauthor review; this packet asserts nothing about them. + +## Provenance + +Consumed sources and their exact identities: `SOURCE_MAP.json`. This packet's own inventory: `SOURCE_FILES.json`. External check: `RECONNAISSANCE.md`. Same GitHub account as every lane; zero organizational-independence credit. The planar sources are OpenAI-authored and were reviewed by Anthropic and xAI lanes at their exact heads; those reviews are cited for their own scopes only and do not transfer to this note. diff --git a/frontiers/d5_dimension_lift_20260929/RECONNAISSANCE.md b/frontiers/d5_dimension_lift_20260929/RECONNAISSANCE.md new file mode 100644 index 000000000..8263d7456 --- /dev/null +++ b/frontiers/d5_dimension_lift_20260929/RECONNAISSANCE.md @@ -0,0 +1,24 @@ +# Limited external reconnaissance — 29 September 2026 + +Scope: whether the `d`-dimensional lift of the pinned D5 estimates, or its five linear-algebra devices, is already in the literature in this conditioned form. Not a novelty, priority or exhaustiveness claim. + +## What was attempted + +The Consensus connector was called once with the query "critical points Gaussian random field conditioned on nearby maximum saddle pair Kac-Rice higher dimension expected number". It returned its monthly quota error ("You've used all 30 searches this month; resets on October 1st"), the same failure recorded in `frontiers/elder_dimension_lift_20260928/RECONNAISSANCE.md`. No result was invented or cited from that call. No web search was performed in this pass. + +## Records already cited by the consumed sources + +These are read from the reconnaissance sections of the consumed planar sources, not re-inspected here; none is imported as a theorem: + +- D. Armentano, J.-M. Azaïs, J. R. León, *On a general Kac-Rice formula for the measure of a level set*, arXiv:2304.07424v3 — the Kac–Rice framework (Theorems 2.1, 2.2, 7.1, Remarks 7–8) used by every consumed source and by this note. +- L. Gass, M. Stecconi, *The number of critical points of a Gaussian field: finiteness of moments*, PTRF 190 (2024) — finiteness of moments under jet nondegeneracy; not uniform at a coalescing conditioned pair, not consumed. +- J.-M. Azaïs, C. Delmas, *Mean number and correlation function of critical points of isotropic Gaussian fields ...*, SPA 150 (2022) — unconditioned isotropic setting; not consumed. +- S. Muirhead, SPL 160 (2020); S. Ladgham and R. Lachièze-Rey, SPA 2023; D. Beliaev, V. Cammarota, I. Wigman, ECP 2020 — cited by `remote_collision_20260928` for two-point methods; not consumed. + +## Classical facts used without a citation + +The singular values of the second exterior power of a matrix are the pairwise products of its singular values; Hadamard's inequality; the Schur complement / cofactor expansion of a block symmetric matrix; monotonicity of the determinant on the positive semidefinite cone. These are textbook multilinear and linear algebra. Their role is written out in PROOF.md §3 rather than assumed. + +## Assessment + +The consumed planar sources (September 2026) already present the mechanism; the contribution of this note is the explicit dimension-free rewriting of each planar-specific step and the verification that the power ledgers close in every `d`. No claim of first discovery is made for any device, and the general peer-review and governing-status boundaries remain separate. diff --git a/frontiers/d5_dimension_lift_20260929/RESULTS.json b/frontiers/d5_dimension_lift_20260929/RESULTS.json new file mode 100644 index 000000000..3f704a414 --- /dev/null +++ b/frontiers/d5_dimension_lift_20260929/RESULTS.json @@ -0,0 +1,125 @@ +{ + "checks": { + "EU_euler_identity_d3": { + "cubic_terms_cancel": true, + "euler_remainder_is_minus_quartic_part_d3": true + }, + "G_pin_frame_block_gram": { + "S_to_S_beta_gram_identity_and_half_beta2_floor": true, + "block_schur_lower_bound_d2": true, + "block_schur_lower_bound_d3": true, + "block_schur_lower_bound_d4": true, + "floor_d2_equals_planar_9_over_131072": true, + "frame_rank_d_on_alpha_beta_sphere_d2": true, + "frame_rank_d_on_alpha_beta_sphere_d3": true, + "frame_rank_d_on_alpha_beta_sphere_d4": true, + "gram_det_floor_9_64_pow_d_minus_1_over_2048_d2": true, + "gram_det_floor_9_64_pow_d_minus_1_over_2048_d3": true, + "gram_det_floor_9_64_pow_d_minus_1_over_2048_d4": true + }, + "L_ledgers": { + "collar_r_exponent_d2": 3, + "collar_r_exponent_d3": 3, + "collar_r_exponent_d4": 3, + "collar_r_exponent_d5": 3, + "collar_r_exponent_d6": 3, + "dyadic_partial_sums_below_4_over_3": true, + "dyadic_shell_sum_bounded_by_A0_and_rho_terms": true, + "intermediate_gram_det_exponent_2d_plus_8_d2": 12, + "intermediate_gram_det_exponent_2d_plus_8_d3": 14, + "intermediate_gram_det_exponent_2d_plus_8_d4": 16, + "intermediate_gram_det_exponent_2d_plus_8_d5": 18, + "intermediate_gram_det_exponent_2d_plus_8_d6": 20, + "jacobian_exponent_d_plus_4_d2": 6, + "jacobian_exponent_d_plus_4_d3": 7, + "jacobian_exponent_d_plus_4_d4": 8, + "jacobian_exponent_d_plus_4_d5": 9, + "jacobian_exponent_d_plus_4_d6": 10, + "pin_region_II_absorption_power_needed_d2": 11, + "pin_region_II_absorption_power_needed_d3": 14, + "pin_region_II_absorption_power_needed_d4": 17, + "pin_region_II_absorption_power_needed_d5": 20, + "pin_region_II_absorption_power_needed_d6": 23, + "pin_region_II_pointwise_r_exponent_before_absorption_d2": -10, + "pin_region_II_pointwise_r_exponent_before_absorption_d3": -14, + "pin_region_II_pointwise_r_exponent_before_absorption_d4": -18, + "pin_region_II_pointwise_r_exponent_before_absorption_d5": -22, + "pin_region_II_pointwise_r_exponent_before_absorption_d6": -26, + "pin_region_I_r_exponent_d2": 3, + "pin_region_I_r_exponent_d3": 3, + "pin_region_I_r_exponent_d4": 3, + "pin_region_I_r_exponent_d5": 3, + "pin_region_I_r_exponent_d6": 3, + "shell_inequality_2_bracket_minus_ratio_is_square": true, + "shell_r_exponent_d2": 3, + "shell_r_exponent_d3": 3, + "shell_r_exponent_d4": 3, + "shell_r_exponent_d5": 3, + "shell_r_exponent_d6": 3, + "shell_s_exponent_d2": -2, + "shell_s_exponent_d3": -2, + "shell_s_exponent_d4": -2, + "shell_s_exponent_d5": -2, + "shell_s_exponent_d6": -2, + "shells_summed": 16 + }, + "N_jet_functional_norms": { + "C_functional_norm2_ge_v4_over_4": true, + "D_functional_norm2_ge_v6_over_144": true, + "S_to_Sv_gram_ge_half_v2": true + }, + "RO_row_operation_d3": { + "S0_and_C3_cancel_from_height_row": true, + "eight_pins_exact": true, + "height_row_no_negative_power_of_s": true, + "height_row_s0_equals_mean_plus_BJ": true, + "row1_f_x_over_s2_exact": true, + "rows_grad_y_over_s_exact": true + }, + "R_confluent_rank": { + "axis_family_det_u_pow_2d_plus_6_d2": true, + "axis_family_det_u_pow_2d_plus_6_d3": true, + "axis_family_det_u_pow_2d_plus_6_d4": true, + "axis_rank_degree4_d2": 2, + "axis_rank_degree4_d3": 3, + "axis_rank_degree4_d4": 4, + "axis_rank_degree5_d2": 3, + "axis_rank_degree5_d3": 4, + "axis_rank_degree5_d4": 5, + "general_transverse_direction_nonsingular_d2": true, + "general_transverse_direction_nonsingular_d3": true, + "general_transverse_direction_nonsingular_d4": true, + "transverse_family_det_minus_v_pow_2d_plus_2_d2": true, + "transverse_family_det_minus_v_pow_2d_plus_2_d3": true, + "transverse_family_det_minus_v_pow_2d_plus_2_d4": true + }, + "TB_transverse_block_determinant": { + "det_S_equals_eps_detSp_minus_wT_adj_w": true, + "wT_adj_w_squared_le_w4_frobenius_power": true + }, + "W_pin_weight": { + "nested_ball_count_exponent_d2": 5, + "nested_ball_count_exponent_d3": 5, + "nested_ball_count_exponent_d4": 5, + "nested_ball_count_exponent_d5": 5, + "nested_ball_count_exponent_d6": 5, + "weight_d2_is_one": true, + "weight_radial_exponent_d2": 0, + "weight_radial_exponent_d3": 0, + "weight_radial_exponent_d4": 0, + "weight_radial_exponent_d5": 0, + "weight_radial_exponent_d6": 0 + }, + "X_two_soft_directions": { + "cramer_coefficient_a2_wedge_identity": true, + "det2_wedge_le_Hwedge_frobenius_power_d2": true, + "det2_wedge_le_Hwedge_frobenius_power_d3": true, + "det2_wedge_le_Hwedge_frobenius_power_d4": true, + "equality_on_diagonal_family_operator_norm_d3": true, + "equality_on_diagonal_family_operator_norm_d4": true + } + }, + "passed": true, + "scientific_effect": "NONE", + "scope": "exact identities, ranks, floors and power ledgers only; Gaussian, compactness, regression and Kac-Rice steps are argued in PROOF.md" +} diff --git a/frontiers/d5_dimension_lift_20260929/SOURCE_FILES.json b/frontiers/d5_dimension_lift_20260929/SOURCE_FILES.json new file mode 100644 index 000000000..51922dea3 --- /dev/null +++ b/frontiers/d5_dimension_lift_20260929/SOURCE_FILES.json @@ -0,0 +1,43 @@ +{ + "schema": 1, + "scientific_effect": "NONE", + "review_status": "AUTHOR_SIDE_REVIEW_REQUIRED", + "files": [ + { + "path": "PROOF.md", + "bytes": 47881, + "sha256": "3b0a4be490c7095f26d094e86a8aee40bff6882487ab8b6eea4375af817ae885", + "git_blob": "887a796345c8a6a22bedd5900a23d6f7547eecbc" + }, + { + "path": "README.md", + "bytes": 5096, + "sha256": "293e3a4f6eac0d1e74d8c98abf14e230d1257d03fa59ceed9e53c9d7925101cd", + "git_blob": "08fbe759d1d46540c4707732611893f968bfc5dc" + }, + { + "path": "RECONNAISSANCE.md", + "bytes": 2607, + "sha256": "e815a3e379cadf1b95ad5d5a99169c0dd61baa53d7be09c058cf51accf10581b", + "git_blob": "8263d7456292a23f9a2329727e080eb86e64bcc3" + }, + { + "path": "RESULTS.json", + "bytes": 5184, + "sha256": "ae9ca864ff9db1f239910fa7c349c297aa1b5ffbd9863786ca20a61a6c1814e5", + "git_blob": "3f704a414752fb8f40a5344236bdd0f60dc74105" + }, + { + "path": "SOURCE_MAP.json", + "bytes": 4646, + "sha256": "b900314945177b20e88e327c723eee33b3a32999aae47919072cc91e71a30a04", + "git_blob": "2b32c60c5b467addf60b05f779ea8260ec7ae9e3" + }, + { + "path": "lift_exact_check.py", + "bytes": 30404, + "sha256": "116b0af02790ffba2269e6c4d03801b8dd6bda3556259da05fbbba14a90c0538", + "git_blob": "460efe46126bb1b7b45954a7a8e0ef2f8e93c739" + } + ] +} diff --git a/frontiers/d5_dimension_lift_20260929/SOURCE_MAP.json b/frontiers/d5_dimension_lift_20260929/SOURCE_MAP.json new file mode 100644 index 000000000..2b32c60c5 --- /dev/null +++ b/frontiers/d5_dimension_lift_20260929/SOURCE_MAP.json @@ -0,0 +1,86 @@ +{ + "scientific_effect": "NONE", + "source_repository": "d6g8k5htny-coder/Math-", + "source_commit": "dbccbb41a58f2328b3bec6c4609a4b8fb3ac811f", + "inputs": [ + { + "id": "LP", + "path": "imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md", + "bytes": 40261, + "sha256": "9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7", + "git_blob": "dfed3b8d318a3ab1950957f393307733a4bef3f2", + "use": "Exact model in every d; positive Fourier spectrum and distinct-site jet rank (section 2); contact frame U_r and uniform regression (section 3); uniform C^q moments (4.1); endpoint identities (5.1)-(5.3); full normalizer floor (5.5). These are the A1-A4 interfaces accepted in the D1 reconciliation." + }, + { + "id": "PP", + "path": "reviews/d5_local_collar_20260928/PUNCTURED_PIN_PROOF.md", + "bytes": 23771, + "sha256": "f972e50bc07674ebce9d971d1a1bd4dba2f8036dde37ecb57d8a44a35650f76a", + "git_blob": "d8acf0bcb9025b1562c03c077c8e0094ae282060", + "use": "Planar all-height punctured endpoint disk (P2): the d = 2 case and the template. Steps (P3)-(P20) are followed; the d-dimensional replacements are written in full." + }, + { + "id": "CP", + "path": "reviews/d5_local_collar_20260928/COLLAR_PROOF.md", + "bytes": 20318, + "sha256": "794babe0fd039c3a93c401c0b8978316331af009fad45f953e63fbe7e1e31aab", + "git_blob": "b5647907a8a589635855b59cc4246b23efce2801", + "use": "Planar compact collar (C1) and scaled-ball synthesis (C2): the d = 2 case and the template." + }, + { + "id": "IW", + "path": "frontiers/intermediate_window_20260928/PROOF.md", + "bytes": 27775, + "sha256": "b3eb9456d7058b5b78149cfca4e072679beda85cd1a0293d209664a542db66cf", + "git_blob": "f53a527ce0204fda271f24730b62b4223a5e43ec", + "use": "Planar intermediate height-window shells (I3), dyadic sum (I4) and global first moment (I5): the d = 2 case and the template." + }, + { + "id": "RM", + "path": "frontiers/remote_window_20260924/PROOF.md", + "bytes": 18355, + "sha256": "a332bae9bdc0106ce17047f7e0409cc3d94eb610a0c7b74ba5ba2d01a1620cb7", + "git_blob": "b383bfcc88ec4ad497dff01fb6640e429ba24a84", + "use": "Fixed-remote Theorem A in every d >= 2 (reviewed ACCEPT, main#76): the outer tile of the global synthesis." + }, + { + "id": "RC", + "path": "frontiers/remote_collision_20260928/PROOF.md", + "bytes": 26002, + "sha256": "b9b8b58fd8266db7ffe6537078003888ef138b445d3289ec5588f116af9050c2", + "git_blob": "7b48a88e2af54e759e89a8c8219573bb450a65ea", + "use": "Corollary (F-), the lower bound c r^3 on the window event in every fixed d, and the sentence leaving the d > 2 upper half conditional on a dimension-matched first moment. That conditional is what Theorem G_d supplies." + }, + { + "id": "EDL", + "path": "frontiers/elder_dimension_lift_20260928/PROOF.md", + "bytes": 23971, + "sha256": "b529fe3780e1909014b3cb144b9a74156d976bbdc19b6711d0c5b1a1da9e5669", + "git_blob": "7303bd791a68a1139251f0f6e403a9f7cc89b006", + "use": "Lower bound (A4): Q^W(N_r >= 2) >= c r^3 in every fixed d. Combined with Theorem G_d only in Corollary M_d." + }, + { + "id": "LOCAL", + "path": "frontiers/window_multiplicity_laws_20260928/LOCAL_MULTIPLICITY.md", + "bytes": 13100, + "sha256": "e6272e8709835ca6290fecb7034fa84832dde08c3c4cc990a48b8019e89e7c8d", + "git_blob": "b5c18aac5529c5f975ee5bb056b304debafc6697", + "use": "Planar Theorem L and the total-variation identity (L16), whose d-dimensional form is stated in Corollary M_d; not consumed for d > 2 beyond that elementary identity." + } + ], + "new_obligations": [ + "Two-soft-direction determinant bound through exterior powers, replacing the planar two-column argument at each of the three Hessians", + "Block Gram floor for the d-dimensional pin gradient frame through the map S -> S beta", + "Transverse-block determinant control from the Euler quadratic form together with the small gradient column", + "Integrable pin weight max(|q|, r|p|)^(2-d) replacing the planar bounded intensity", + "Degree-five confluent value/gradient interpolation at three sites in d variables" + ], + "consumed_reviews": [ + "main#76 (remote Theorem A, every d)", + "Math-#106 A1-A4 (LP sections 2-5)", + "Math-#105 comment 5872932723 and reviews/d5_collar_count_20260928 (planar PP and CP)", + "reviews/d5_intermediate_window_claude_20260928 and reviews/d5_i5_planar_f_20260928 (planar IW)" + ], + "nonauthor_acceptance": false, + "governing_status_changed": false +} diff --git a/frontiers/d5_dimension_lift_20260929/lift_exact_check.py b/frontiers/d5_dimension_lift_20260929/lift_exact_check.py new file mode 100644 index 000000000..460efe461 --- /dev/null +++ b/frontiers/d5_dimension_lift_20260929/lift_exact_check.py @@ -0,0 +1,773 @@ +"""Exact finite controls for CL-D5-DIMENSION-LIFT-20260929-v1 (frontiers/d5_dimension_lift_20260929/PROOF.md). + +Python standard library only; exact rational arithmetic and exact multivariate Laurent polynomials. + + X two soft directions: det(H)^2 ||u1^u2||^2 <= ||H u1 ^ H u2||^2 ||H||_F^(2(d-2)) for d = 2, 3, 4; + equality on a diagonal family with the operator norm; the Cramer coefficient identity a^2 ||e^e'||^2 = ||u^e'||^2 + G pin-ball gradient frame in d dimensions: the Gram of S -> S beta over independent entries, rank d on the whole + (alpha, beta) sphere including alpha = 0 and beta = 0, the block-Schur lower bound, and the explicit floor + det(B_core B_core^T) >= (9/64)^(d-1) / 2048, which is the planar 9/131072 at d = 2 + R confluent value/gradient rank with degree-five polynomials in d variables (contact rows at the midpoint plus + value and gradient at a witness): explicit annihilating families with determinants -|v|^(2d+2) and u^(2d+6); + degree four fails on the axis in every d + RO the height row operation in d = 3 on an exactly pinned cubic: no negative power of s, S_0 and C_3 cancel, + the s^0 part is the displayed mean plus B J + EU Euler identity in d = 3: 3[f(X)-f(0)] - X.grad f(X) - 2 grad f(0).X - X^T H_0 X / 2 = -(quartic part of f) + TB transverse block determinant: det S = eps det S' - w^T adj(S') w and (w^T adj(S') w)^2 <= |w|^4 (||S'||_F^2)^(m-2) + N jet-functional norms: S -> S v has Gram >= |v|^2/2 I; C -> v^T C v / 2 has norm^2 >= |v|^4/4; + D -> D[v,v,v] / 12 has norm^2 >= |v|^6/144 (all over independent entries) + L radius, scale and volume ledgers for d = 2..6: pin region I, pin region II, collar, intermediate shell, the + Jacobian exponent d+4, the Gram determinant exponent 2d+8, the exact shell inequality and the dyadic sums + W the pin weight max(|q|, r|p|)^(2-d): radial exponent zero (integrable), nested-ball count exponent 5 + +Mutants (each must exit 1): drop-frobenius-order, drop-s0-block, drop-a4-column, degree-four, row-operation-third, +euler-coefficient, adjugate-sign, one-soft-direction, flat-shell, weight-one-less-power. + +These checks verify exact identities, ranks, floors and power ledgers. They do not prove the Gaussian, compactness, +regression or Kac-Rice steps, which are argued in PROOF.md. +""" +import argparse +import itertools +import json +import random +import sys +from fractions import Fraction as F + +MUTANTS = ['drop-frobenius-order', 'drop-s0-block', 'drop-a4-column', 'degree-four', 'row-operation-third', + 'euler-coefficient', 'adjugate-sign', 'one-soft-direction', 'flat-shell', 'weight-one-less-power'] + + +def require(ok, message): + if not ok: + raise AssertionError(message) + + +# ---------------------------------------------------------------- exact multivariate Laurent polynomials + +def _mono_mul(a, b): + d = dict(a) + for v, e in b: + n = d.get(v, 0) + e + if n: + d[v] = n + else: + d.pop(v, None) + return tuple(sorted(d.items())) + + +class P: + __slots__ = ('t',) + + def __init__(self, t=None): + self.t = {m: c for m, c in (t or {}).items() if c != 0} + + @staticmethod + def c(x): + return P({(): F(x)}) + + @staticmethod + def v(name, e=1): + return P({((name, e),): F(1)}) + + @staticmethod + def lift(o): + return o if isinstance(o, P) else P.c(o) + + def __add__(self, o): + o = P.lift(o) + t = dict(self.t) + for m, c in o.t.items(): + t[m] = t.get(m, 0) + c + return P(t) + + __radd__ = __add__ + + def __neg__(self): + return P({m: -c for m, c in self.t.items()}) + + def __sub__(self, o): + return self + (-P.lift(o)) + + def __rsub__(self, o): + return P.lift(o) - self + + def __mul__(self, o): + o = P.lift(o) + t = {} + for m1, c1 in self.t.items(): + for m2, c2 in o.t.items(): + m = _mono_mul(m1, m2) + t[m] = t.get(m, 0) + c1 * c2 + return P(t) + + __rmul__ = __mul__ + + def __pow__(self, n): + r = P.c(1) + for _ in range(n): + r = r * self + return r + + def __eq__(self, o): + return (self - P.lift(o)).is_zero() + + def is_zero(self): + return not self.t + + def d(self, name): + t = {} + for m, c in self.t.items(): + dm = dict(m) + e = dm.get(name, 0) + if e == 0: + continue + if e == 1: + dm.pop(name) + else: + dm[name] = e - 1 + key = tuple(sorted(dm.items())) + t[key] = t.get(key, 0) + c * e + return P(t) + + def subs(self, name, q): + q = P.lift(q) + r = P() + for m, c in self.t.items(): + dm = dict(m) + e = dm.pop(name, 0) + if e < 0: + raise ValueError('negative exponent substitution') + r = r + P({tuple(sorted(dm.items())): c}) * (q ** e) + return r + + def coeff(self, name, e): + t = {} + for m, c in self.t.items(): + dm = dict(m) + if dm.pop(name, 0) == e: + t[tuple(sorted(dm.items()))] = c + return P(t) + + def exponents(self, name): + return sorted({dict(m).get(name, 0) for m in self.t}) if self.t else [] + + def const(self): + if any(m for m in self.t): + raise ValueError('polynomial is not constant: ' + repr(sorted(self.t))) + return self.t.get((), F(0)) + + def variables(self): + return sorted({v for m in self.t for v, _ in m}) + + def total_degree_terms(self, names): + out = {} + for m, c in self.t.items(): + dm = dict(m) + deg = sum(dm.get(n, 0) for n in names) + out.setdefault(deg, {})[m] = c + return {k: P(v) for k, v in out.items()} + + +# ---------------------------------------------------------------- exact linear algebra + +def det(M): + n = len(M) + A = [row[:] for row in M] + sign = F(1) + for i in range(n): + p = next((r for r in range(i, n) if A[r][i] != 0), None) + if p is None: + return F(0) + if p != i: + A[i], A[p] = A[p], A[i] + sign = -sign + for r in range(i + 1, n): + f = A[r][i] / A[i][i] + if f: + for c in range(i, n): + A[r][c] -= f * A[i][c] + out = sign + for i in range(n): + out *= A[i][i] + return out + + +def rank(M): + A = [row[:] for row in M] + if not A: + return 0 + rows, cols = len(A), len(A[0]) + r = 0 + for c in range(cols): + p = next((i for i in range(r, rows) if A[i][c] != 0), None) + if p is None: + continue + A[r], A[p] = A[p], A[r] + for i in range(rows): + if i != r and A[i][c] != 0: + f = A[i][c] / A[r][c] + for k in range(c, cols): + A[i][k] -= f * A[r][k] + r += 1 + if r == rows: + break + return r + + +def minor(M, i, j): + return [row[:j] + row[j + 1:] for k, row in enumerate(M) if k != i] + + +def adj(M): + n = len(M) + if n == 1: + return [[F(1)]] + return [[(-1) ** (i + j) * det(minor(M, j, i)) for j in range(n)] for i in range(n)] + + +def matvec(M, v): + return [sum(M[i][j] * v[j] for j in range(len(v))) for i in range(len(M))] + + +def transpose(M): + return [list(col) for col in zip(*M)] + + +def matmul(A, B): + return [[sum(A[i][k] * B[k][j] for k in range(len(B))) for j in range(len(B[0]))] for i in range(len(A))] + + +def dot(a, b): + return sum(x * y for x, y in zip(a, b)) + + +def gram2(a, b): + """||a ^ b||^2 = |a|^2 |b|^2 - (a.b)^2 (Lagrange identity).""" + return dot(a, a) * dot(b, b) - dot(a, b) ** 2 + + +def frob2(M): + return sum(x * x for row in M for x in row) + + +def diag(entries): + n = len(entries) + return [[entries[i] if i == j else F(0) for j in range(n)] for i in range(n)] + + +def unitvec(n, i): + return [F(1) if j == i else F(0) for j in range(n)] + + +def rand_frac(rng, lo=-3, hi=3, den=5): + return F(rng.randint(lo * den, hi * den), den) + + +def rand_vec(rng, n, lo=-3, hi=3, den=5): + while True: + v = [rand_frac(rng, lo, hi, den) for _ in range(n)] + if any(v): + return v + + +def rand_sym(rng, n, lo=-3, hi=3, den=5): + M = [[F(0)] * n for _ in range(n)] + for i in range(n): + for j in range(i, n): + M[i][j] = M[j][i] = rand_frac(rng, lo, hi, den) + return M + + +def rational_unit(rng, n): + """A rational point of the unit sphere S^(n-1) by stereographic projection of a random rational y in R^(n-1).""" + y = [F(rng.randint(-6, 6), rng.randint(1, 4)) for _ in range(n - 1)] + s = dot(y, y) + x = [2 * yi / (s + 1) for yi in y] + [(s - 1) / (s + 1)] + require(dot(x, x) == 1, 'stereographic point is not on the sphere') + return x + + +# ---------------------------------------------------------------- X: two soft directions + +def check_x(mut, rng): + out = {} + for d in (2, 3, 4): + order = d - 2 if mut != 'drop-frobenius-order' else max(0, d - 3) + ok = True + for _ in range(150): + H = rand_sym(rng, d) + u1 = rand_vec(rng, d) + u2 = rand_vec(rng, d) + lhs = det(H) ** 2 * gram2(u1, u2) + rhs = gram2(matvec(H, u1), matvec(H, u2)) * frob2(H) ** order + ok = ok and lhs <= rhs + require(ok, 'two-soft-direction exterior inequality failed in d=%d' % d) + out['det2_wedge_le_Hwedge_frobenius_power_d%d' % d] = ok + for d in (3, 4): + s1, s2, big = F(1, 3), F(2, 5), F(7, 2) + H = diag([s1, s2] + [big] * (d - 2)) + e1, e2 = unitvec(d, 0), unitvec(d, 1) + lhs = det(H) ** 2 * gram2(e1, e2) + rhs = gram2(matvec(H, e1), matvec(H, e2)) * big ** (2 * (d - 2)) + require(lhs == rhs, 'diagonal family is not an equality case') + out['equality_on_diagonal_family_operator_norm_d%d' % d] = True + ok = True + for _ in range(100): + d = rng.choice((2, 3, 4)) + e, e2 = rand_vec(rng, d), rand_vec(rng, d) + a, b = rand_frac(rng), rand_frac(rng) + u = [a * e[i] + b * e2[i] for i in range(d)] + ok = ok and a * a * gram2(e, e2) == gram2(u, e2) + require(ok, 'Cramer coefficient identity failed') + out['cramer_coefficient_a2_wedge_identity'] = ok + return out + + +# ---------------------------------------------------------------- G: pin-ball gradient frame in d dimensions + +def frame_core(p, alpha, beta, drop_s0=False, drop_a4=False): + """Columns of the frame matrix B over the jets (A_4, T_3, S_0), rows (f_x/(r^2 Delta), grad_y f/(r Delta)). + + The C_3 block is a positive-semidefinite addition to B B^T and is omitted from the core.""" + m = len(beta) + a = (p - 1) * (2 * p - 1) / 12 + b = (p - 1) / 2 + c = p - F(1, 2) + cols = [] + if not drop_a4: + cols.append([a * alpha] + [F(0)] * m) + for j in range(m): + col = [c * beta[j]] + [F(0)] * m + col[1 + j] = b * alpha + cols.append(col) + if not drop_s0: + for i in range(m): + for j in range(i, m): + col = [F(0)] * (m + 1) + if i == j: + col[1 + i] = beta[i] + else: + col[1 + i] = beta[j] + col[1 + j] = beta[i] + cols.append(col) + B = [[cols[k][r] for k in range(len(cols))] for r in range(m + 1)] + return B, (a, b, c) + + +def check_g(mut, rng): + out = {} + drop_s0 = mut == 'drop-s0-block' + drop_a4 = mut == 'drop-a4-column' + for d in (2, 3, 4): + m = d - 1 + floor = F(9, 64) ** m / 2048 + samples = [] + for _ in range(40): + samples.append((F(rng.randint(-16, 16), 64), rational_unit(rng, d))) + for p in (F(0), F(1, 4), F(-1, 4)): + samples.append((p, [F(0)] + rational_unit(rng, m))) # alpha = 0 + samples.append((p, [F(1)] + [F(0)] * m)) # beta = 0 + samples.append((p, [F(-1)] + [F(0)] * m)) + ok_rank = ok_floor = ok_schur = True + for p, ab in samples: + alpha, beta = ab[0], ab[1:] + B, (a, b, c) = frame_core(p, alpha, beta, drop_s0, drop_a4) + G = matmul(B, transpose(B)) + ok_rank = ok_rank and rank(B) == d + dg = det(G) + b2 = dot(beta, beta) + schur = a * a * alpha * alpha + (c * c * b2 * b2 / (2 * b * b * alpha * alpha + b2) + if (2 * b * b * alpha * alpha + b2) else F(0)) + lower = schur * (b * b * alpha * alpha + b2 / 2) ** m + ok_schur = ok_schur and dg >= lower + ok_floor = ok_floor and dg >= floor + require(ok_rank, 'frame rank drop in d=%d' % d) + require(ok_schur, 'block-Schur lower bound failed in d=%d' % d) + require(ok_floor, 'explicit Gram floor failed in d=%d' % d) + out['frame_rank_d_on_alpha_beta_sphere_d%d' % d] = True + out['block_schur_lower_bound_d%d' % d] = True + out['gram_det_floor_9_64_pow_d_minus_1_over_2048_d%d' % d] = True + out['floor_d2_equals_planar_9_over_131072'] = (F(9, 64) / 2048 == F(9, 131072)) + require(out['floor_d2_equals_planar_9_over_131072'], 'planar constant mismatch') + # quadratic form of the Gram of S -> S beta over independent entries + ok = True + for _ in range(80): + m = rng.choice((1, 2, 3)) + beta = rand_vec(rng, m) + xi = rand_vec(rng, m) + q = sum(xi[i] ** 2 * beta[i] ** 2 for i in range(m)) + sum( + (xi[i] * beta[j] + xi[j] * beta[i]) ** 2 for i in range(m) for j in range(i + 1, m)) + _, _ = frame_core(F(0), F(0), beta) + B, _ = frame_core(F(0), F(0), beta) + Bt = transpose(B) + # rows 1..m of B restricted to S_0 columns: the last m(m+1)/2 columns + S_cols = [row[-(m * (m + 1) // 2):] for row in B[1:]] + Gs = matmul(S_cols, transpose(S_cols)) + qf = dot(xi, matvec(Gs, xi)) + ok = ok and qf == q and 2 * qf >= dot(beta, beta) * dot(xi, xi) + require(ok, 'S -> S beta Gram identity or floor failed') + out['S_to_S_beta_gram_identity_and_half_beta2_floor'] = ok + return out + + +# ---------------------------------------------------------------- R: confluent rank in d variables + +def spatial(d): + return ['x'] + ['y%d' % j for j in range(1, d)] + + +def contact_functionals(d): + """Derivative multi-orders at the midpoint: f, f_x, f_xx, f_xxx, f_yj, f_xyj.""" + names = spatial(d) + base = [(), ('x',), ('x', 'x'), ('x', 'x', 'x')] + for j in range(1, d): + base.append(('y%d' % j,)) + base.append(('x', 'y%d' % j)) + return names, base + + +def apply_functional(poly, order, names): + q = poly + for n in order: + q = q.d(n) + for n in names: + q = q.subs(n, 0) + return q.const() + + +def value_gradient_row(poly, point, names): + row = [] + q = poly + for n, val in zip(names, point): + q = q.subs(n, val) + row.append(q.const()) + for n in names: + q = poly.d(n) + for n2, val in zip(names, point): + q = q.subs(n2, val) + row.append(q.const()) + return row + + +def monomial(exps, names): + p = P.c(1) + for n, e in zip(names, exps): + if e: + p = p * P.v(n, e) + return p + + +def check_r(mut, rng): + out = {} + for d in (2, 3, 4): + m = d - 1 + names, contact = contact_functionals(d) + contact_exps = {(0,) * d, (1,) + (0,) * m, (2,) + (0,) * m, (3,) + (0,) * m} + for j in range(m): + e = [0] * d + e[1 + j] = 1 + contact_exps.add(tuple(e)) + e[0] = 1 + contact_exps.add(tuple(e)) + u = F(3, 2) + axis = (u,) + (F(0),) * m + for maxdeg, label in ((4, 'degree4'), (5, 'degree5')): + exps = [e for e in itertools.product(range(maxdeg + 1), repeat=d) if sum(e) <= maxdeg and e not in contact_exps] + rows = [value_gradient_row(monomial(e, names), axis, names) for e in exps] + out['axis_rank_%s_d%d' % (label, d)] = rank(rows) + require(out['axis_rank_degree5_d%d' % d] == d + 1, 'degree five does not give full witness rank on the axis') + expected_deg4 = d + 1 if mut == 'degree-four' else d + require(out['axis_rank_degree4_d%d' % d] == expected_deg4, 'degree-four axis rank is not d') + # explicit axis family x^4, x^5, x^2 y_j + fam = [monomial((4,) + (0,) * m, names), monomial((5,) + (0,) * m, names)] + for j in range(m): + e = [0] * d + e[0] = 2 + e[1 + j] = 1 + fam.append(monomial(tuple(e), names)) + for q in fam: + require(all(apply_functional(q, o, names) == 0 for o in contact), 'axis family is not contact-annihilated') + D = det([value_gradient_row(q, axis, names) for q in fam]) + require(abs(D) == u ** (2 * d + 6), 'axis family determinant is not u^(2d+6)') + out['axis_family_det_u_pow_2d_plus_6_d%d' % d] = True + # explicit transverse family with v along y1: y1^2, y1^3, x y1^2, y_j y1^2 (j >= 2) + for vmag in (F(1, 2), F(3, 4), F(2)): + w = (F(-2, 3), vmag) + (F(0),) * (m - 1) + y1 = P.v('y1') + fam = [y1 ** 2, y1 ** 3, P.v('x') * y1 ** 2] + [P.v('y%d' % j) * y1 ** 2 for j in range(2, d)] + for q in fam: + require(all(apply_functional(q, o, names) == 0 for o in contact), 'transverse family not annihilated') + D = det([value_gradient_row(q, w, names) for q in fam]) + require(D == -vmag ** (2 * d + 2), 'transverse family determinant is not -|v|^(2d+2)') + out['transverse_family_det_minus_v_pow_2d_plus_2_d%d' % d] = True + # general rational transverse direction v with a rational basis of its orthogonal complement + ok = True + for _ in range(12): + v = rand_vec(rng, m) + v2 = dot(v, v) + ys = [P.v('y%d' % j) for j in range(1, d)] + vy = sum((v[j] * ys[j] for j in range(m)), P.c(0)) + perp = [] + for j in range(m): + e = unitvec(m, j) + wj = [e[i] - v[i] * v[j] / v2 for i in range(m)] + if any(wj) and rank(perp + [wj]) == len(perp) + 1: + perp.append(wj) + require(len(perp) == m - 1, 'orthogonal complement basis has wrong size') + fam = [vy ** 2, vy ** 3, P.v('x') * vy ** 2] + [ + sum((wj[j] * ys[j] for j in range(m)), P.c(0)) * vy ** 2 for wj in perp] + require(all(apply_functional(q, o, names) == 0 for q in fam for o in contact), 'general family not annihilated') + w = (F(5, 4),) + tuple(v) + ok = ok and det([value_gradient_row(q, w, names) for q in fam]) != 0 + require(ok, 'general transverse family singular') + out['general_transverse_direction_nonsingular_d%d' % d] = ok + return out + + +# ---------------------------------------------------------------- RO: row operation on a pinned cubic, d = 3 + +def pinned_cubic_d3(): + x, y1, y2 = P.v('x'), P.v('y1'), P.v('y2') + k, r, bb = P.v('k'), P.v('r'), P.v('bb') + T = [P.v('T1'), P.v('T2')] + S = [[P.v('S11'), P.v('S12')], [P.v('S12'), P.v('S22')]] + C = [[P.v('C11'), P.v('C12')], [P.v('C12'), P.v('C22')]] + Dsym = {(0, 0, 0): P.v('D111'), (0, 0, 1): P.v('D112'), (0, 1, 1): P.v('D122'), (1, 1, 1): P.v('D222')} + + def Dt(i, j, kk): + return Dsym[tuple(sorted((i, j, kk)))] + y = [y1, y2] + f = bb - F(3, 2) * k * r ** 2 * x + 2 * k * x ** 3 + for j in range(2): + f = f + F(1, 2) * T[j] * (x ** 2 - r ** 2 * F(1, 4)) * y[j] + for i in range(2): + for j in range(2): + f = f + F(1, 2) * S[i][j] * y[i] * y[j] + F(1, 2) * x * C[i][j] * y[i] * y[j] + for i in range(2): + for j in range(2): + for kk in range(2): + f = f + F(1, 6) * Dt(i, j, kk) * y[i] * y[j] * y[kk] + return f, (k, r, bb, T, S, C, Dt) + + +def check_ro(mut): + out = {} + f, (k, r, bb, T, S, C, Dt) = pinned_cubic_d3() + names = ['x', 'y1', 'y2'] + # exact pins: f(-r/2,0) = bb + k r^3/2, f(r/2,0) = bb - k r^3/2, gradients zero + def at(q, xv): + return q.subs('x', xv).subs('y1', 0).subs('y2', 0) + half = P.v('r') * F(1, 2) + require(at(f, -half) == bb + k * r ** 3 * F(1, 2) and at(f, half) == bb - k * r ** 3 * F(1, 2), 'height pins') + for n in names: + require(at(f.d(n), -half).is_zero() and at(f.d(n), half).is_zero(), 'gradient pins') + out['eight_pins_exact'] = True + # X = s (u, v1, v2), r = eps s + s, eps, u, v1, v2 = P.v('s'), P.v('eps'), P.v('u'), P.v('v1'), P.v('v2') + fx, fy1, fy2 = f.d('x'), f.d('y1'), f.d('y2') + + def scale(q): + return q.subs('x', s * u).subs('y1', s * v1).subs('y2', s * v2).subs('r', eps * s) + inv = lambda n: P.v('s', -n) + Z1 = scale(fx) * inv(2) + Z2 = scale(fy1) * inv(1) + Z3 = scale(fy2) * inv(1) + frac = F(1, 2) if mut != 'row-operation-third' else F(1, 3) + Z4 = (scale(f) - bb - frac * s * (v1 * scale(fy1) + v2 * scale(fy2))) * inv(3) + de = u ** 2 - eps ** 2 * F(1, 4) + vT = v1 * T[0] + v2 * T[1] + vCv = C[0][0] * v1 ** 2 + 2 * C[0][1] * v1 * v2 + C[1][1] * v2 ** 2 + require(Z1 == 6 * k * de + u * vT + F(1, 2) * vCv, 'first row expansion') + out['row1_f_x_over_s2_exact'] = True + Sv = [S[0][0] * v1 + S[0][1] * v2, S[1][0] * v1 + S[1][1] * v2] + Cv = [C[0][0] * v1 + C[0][1] * v2, C[1][0] * v1 + C[1][1] * v2] + v = [v1, v2] + Dvv = [sum((Dt(i, j, kk) * v[j] * v[kk] for j in range(2) for kk in range(2)), P.c(0)) for i in range(2)] + for i, Zi in enumerate((Z2, Z3)): + require(Zi == Sv[i] + F(1, 2) * s * de * T[i] + s * u * Cv[i] + F(1, 2) * s * Dvv[i], 'gradient row expansion') + out['rows_grad_y_over_s_exact'] = True + require(min(Z4.exponents('s')) >= 0, 'height row has a negative power of s') + out['height_row_no_negative_power_of_s'] = True + Z40 = Z4.coeff('s', 0) + Dvvv = sum((Dt(i, j, kk) * v[i] * v[j] * v[kk] for i in range(2) for j in range(2) for kk in range(2)), P.c(0)) + target = k * (2 * u ** 3 - F(3, 2) * eps ** 2 * u) + F(1, 4) * de * vT - F(1, 12) * Dvvv + require(Z40 == target, 'height row s^0 part differs from mean + B J') + out['height_row_s0_equals_mean_plus_BJ'] = True + require(not any(n.startswith('S') or n.startswith('C') for n in Z40.variables()), 'S_0 or C_3 survives') + out['S0_and_C3_cancel_from_height_row'] = True + return out + + +# ---------------------------------------------------------------- EU: Euler identity in d = 3 + +def check_eu(mut): + names = ['x', 'y1', 'y2'] + X = [P.v(n) for n in names] + f = P.c(0) + coefs = {} + for e in itertools.product(range(5), repeat=3): + if sum(e) <= 4: + name = 'c%d%d%d' % e + coefs[e] = P.v(name) + f = f + coefs[e] * monomial(e, names) + at0 = lambda q: q.subs('x', 0).subs('y1', 0).subs('y2', 0) + grads = [f.d(n) for n in names] + lead = 3 if mut != 'euler-coefficient' else 2 + E = lead * (f - at0(f)) - sum((X[i] * grads[i] for i in range(3)), P.c(0)) + E = E - 2 * sum((at0(grads[i]) * X[i] for i in range(3)), P.c(0)) + H0 = [[at0(grads[i].d(names[j])) for j in range(3)] for i in range(3)] + E = E - F(1, 2) * sum((H0[i][j] * X[i] * X[j] for i in range(3) for j in range(3)), P.c(0)) + quartic = f.total_degree_terms(names).get(4, P.c(0)) + require(E == -quartic, 'Euler identity remainder is not minus the quartic part') + return {'euler_remainder_is_minus_quartic_part_d3': True, + 'cubic_terms_cancel': (E.total_degree_terms(names).get(3, P.c(0))).is_zero()} + + +# ---------------------------------------------------------------- TB: transverse block determinant + +def check_tb(mut, rng): + ok_id = ok_bd = True + for _ in range(120): + m = rng.choice((2, 3, 4)) + S = rand_sym(rng, m) + eps = S[0][0] + w = [S[i][0] for i in range(1, m)] + Sp = [row[1:] for row in S[1:]] + adjS = adj(Sp) + quad = dot(w, matvec(adjS, w)) + sign = -1 if mut != 'adjugate-sign' else 1 + ok_id = ok_id and det(S) == eps * det(Sp) + sign * quad + ok_bd = ok_bd and quad ** 2 <= dot(w, w) ** 2 * frob2(Sp) ** (m - 2) + require(ok_id, 'block determinant identity failed') + require(ok_bd, 'adjugate quadratic-form bound failed') + return {'det_S_equals_eps_detSp_minus_wT_adj_w': True, 'wT_adj_w_squared_le_w4_frobenius_power': True} + + +# ---------------------------------------------------------------- N: jet-functional norms over independent entries + +def check_n(rng): + ok_s = ok_c = ok_d = True + for _ in range(80): + m = rng.choice((1, 2, 3)) + v = rand_vec(rng, m) + v2 = dot(v, v) + xi = rand_vec(rng, m) + q = sum(xi[i] ** 2 * v[i] ** 2 for i in range(m)) + sum( + (xi[i] * v[j] + xi[j] * v[i]) ** 2 for i in range(m) for j in range(i + 1, m)) + ok_s = ok_s and 2 * q >= v2 * dot(xi, xi) + nc = sum(((1 if i == j else 2) * v[i] * v[j] / 2) ** 2 for i in range(m) for j in range(i, m)) + ok_c = ok_c and 4 * nc >= v2 ** 2 + nd = F(0) + for i in range(m): + for j in range(i, m): + for kk in range(j, m): + mult = len(set(itertools.permutations((i, j, kk)))) + nd += (mult * v[i] * v[j] * v[kk] / 12) ** 2 + ok_d = ok_d and 144 * nd >= v2 ** 3 + require(ok_s and ok_c and ok_d, 'jet functional norm floors failed') + return {'S_to_Sv_gram_ge_half_v2': ok_s, 'C_functional_norm2_ge_v4_over_4': ok_c, + 'D_functional_norm2_ge_v6_over_144': ok_d} + + +# ---------------------------------------------------------------- L: ledgers + +def check_l(mut): + out = {} + soft_B = 6 if mut != 'one-soft-direction' else 5 + for d in range(2, 7): + # pin region I: Z^-1 (-2), gradient density r^-(d+1), angle-sensitive product r^6, volume r^d + out['pin_region_I_r_exponent_d%d' % d] = -2 - (d + 1) + soft_B + d + # collar and remaining collar strips: same ledger + out['collar_r_exponent_d%d' % d] = -2 - (d + 1) + soft_B + d + # pin region II, pointwise, with the weight (r|p|)^(2-d) factored out: + # Z^-1 (-2), density prefactor r^-(d+1), angle-free product r^3 (p^2+|q|^2) <= 2 r (r|p|)^2 (+1), chi^(3d) <= r^-3d + out['pin_region_II_pointwise_r_exponent_before_absorption_d%d' % d] = -2 - (d + 1) + 1 - 3 * d + out['pin_region_II_absorption_power_needed_d%d' % d] = (3 - d) - (-2 - (d + 1) + 1 - 3 * d) + out['jacobian_exponent_d_plus_4_d%d' % d] = 2 + (d - 1) + 3 + out['intermediate_gram_det_exponent_2d_plus_8_d%d' % d] = 4 + 2 * (d - 1) + 6 + # intermediate shell: r: -2 (Z) +2 (endpoint product) +3 (window) = 3; s: -(d+4) density +2 (|det H_X|) + d (volume) + out['shell_r_exponent_d%d' % d] = -2 + 2 + 3 + out['shell_s_exponent_d%d' % d] = -(d + 4) + 2 + d + require(all(out['pin_region_I_r_exponent_d%d' % d] == 3 for d in range(2, 7)), 'pin region I ledger is not r^3') + require(all(out['collar_r_exponent_d%d' % d] == 3 for d in range(2, 7)), 'collar ledger is not r^3') + require(all(out['pin_region_II_pointwise_r_exponent_before_absorption_d%d' % d] == -2 - 4 * d + and out['pin_region_II_absorption_power_needed_d%d' % d] == 5 + 3 * d for d in range(2, 7)), + 'region II ledger') + require(all(out['shell_r_exponent_d%d' % d] == 3 and out['shell_s_exponent_d%d' % d] == -2 for d in range(2, 7)), + 'shell ledger') + require(out['jacobian_exponent_d_plus_4_d2'] == 6 and out['intermediate_gram_det_exponent_2d_plus_8_d2'] == 12, + 'planar exponents') + r, s = P.v('r'), P.v('s') + lhs = 2 * ((r * P.v('s', -1)) ** 2 + s ** 2) - (r + s ** 2) ** 2 * P.v('s', -2) + require(lhs == (r * P.v('s', -1) - s) ** 2, 'shell inequality identity') + out['shell_inequality_2_bracket_minus_ratio_is_square'] = True + partial = F(0) + ok = True + for j in range(60): + partial += F(1, 4 ** j) + ok = ok and partial < F(4, 3) + out['dyadic_partial_sums_below_4_over_3'] = ok + rr = F(1, 2 ** 20) + rho = F(1, 8) + total = F(0) + j = 0 + extra = F(0) if mut != 'flat-shell' else F(1) + while True: + sj = 2 ** j * 4 * rr + if sj > rho: + break + total += (rr / sj) ** 2 + sj ** 2 + extra + j += 1 + require(total <= F(4, 3) / 16 + F(4, 3) * rho ** 2, 'shell sum is not bounded by the dyadic constants') + out['dyadic_shell_sum_bounded_by_A0_and_rho_terms'] = True + out['shells_summed'] = j + return out + + +# ---------------------------------------------------------------- W: the pin weight + +def check_w(mut): + out = {} + shift = 2 if mut != 'weight-one-less-power' else 1 + for d in range(2, 7): + radial = (shift - d) + (d - 2) + out['weight_radial_exponent_d%d' % d] = radial + require(radial > -1, 'pin weight is not integrable in d=%d' % d) + out['nested_ball_count_exponent_d%d' % d] = 3 + 1 + (radial + 1) + require(out['nested_ball_count_exponent_d%d' % d] == 5, 'nested-ball count is not O(r^5)') + out['weight_d2_is_one'] = (F(0) == F(shift - 2)) + return out + + +def flatten(dd): + return {k: (v if not isinstance(v, F) else str(v)) for k, v in sorted(dd.items())} + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument('--mutant', choices=MUTANTS) + mut = ap.parse_args().mutant + rng = random.Random(20260929) + checks = { + 'X_two_soft_directions': flatten(check_x(mut, rng)), + 'G_pin_frame_block_gram': flatten(check_g(mut, rng)), + 'R_confluent_rank': flatten(check_r(mut, rng)), + 'RO_row_operation_d3': flatten(check_ro(mut)), + 'EU_euler_identity_d3': flatten(check_eu(mut)), + 'TB_transverse_block_determinant': flatten(check_tb(mut, rng)), + 'N_jet_functional_norms': flatten(check_n(rng)), + 'L_ledgers': flatten(check_l(mut)), + 'W_pin_weight': flatten(check_w(mut)), + } + result = { + 'checks': checks, + 'passed': True, + 'scientific_effect': 'NONE', + 'scope': 'exact identities, ranks, floors and power ledgers only; Gaussian, compactness, regression and ' + 'Kac-Rice steps are argued in PROOF.md', + } + sys.stdout.write(json.dumps(result, indent=2, sort_keys=True) + '\n') + + +if __name__ == '__main__': + main() From 278d82c6f3ebd3d7e2dafa79eece5d43af998843 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 29 Sep 2026 16:02:30 +0000 Subject: [PATCH 2/7] Provenance: cite the committed (P2) continuum review record; re-verify source pins on current main SOURCE_MAP.json now names reviews/d5_punctured_pin_continuum_claude_20260929/REVIEW.md, the committed record of the Math-#105 analytic review of the planar punctured-pin proof that this packet consumes, in place of the bare comment reference, and records that all eight consumed inputs are byte-identical (same git blobs) on Math- main e947ade. SOURCE_FILES.json is regenerated for the changed manifest entry. No proof text, script or result changes. Scientific effect NONE. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_015wNj8LPTKXsaT68G3DgPPh --- frontiers/d5_dimension_lift_20260929/SOURCE_FILES.json | 6 +++--- frontiers/d5_dimension_lift_20260929/SOURCE_MAP.json | 5 +++-- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/frontiers/d5_dimension_lift_20260929/SOURCE_FILES.json b/frontiers/d5_dimension_lift_20260929/SOURCE_FILES.json index 51922dea3..d7094a49e 100644 --- a/frontiers/d5_dimension_lift_20260929/SOURCE_FILES.json +++ b/frontiers/d5_dimension_lift_20260929/SOURCE_FILES.json @@ -29,9 +29,9 @@ }, { "path": "SOURCE_MAP.json", - "bytes": 4646, - "sha256": "b900314945177b20e88e327c723eee33b3a32999aae47919072cc91e71a30a04", - "git_blob": "2b32c60c5b467addf60b05f779ea8260ec7ae9e3" + "bytes": 5000, + "sha256": "b7feb9cc7540aa656aab6457d3ebee5724430aad5a688fe42f069f3d1420ffe2", + "git_blob": "ed2f3a77624c59b8513ceaf4005cffb3e45bad1e" }, { "path": "lift_exact_check.py", diff --git a/frontiers/d5_dimension_lift_20260929/SOURCE_MAP.json b/frontiers/d5_dimension_lift_20260929/SOURCE_MAP.json index 2b32c60c5..ed2f3a776 100644 --- a/frontiers/d5_dimension_lift_20260929/SOURCE_MAP.json +++ b/frontiers/d5_dimension_lift_20260929/SOURCE_MAP.json @@ -78,9 +78,10 @@ "consumed_reviews": [ "main#76 (remote Theorem A, every d)", "Math-#106 A1-A4 (LP sections 2-5)", - "Math-#105 comment 5872932723 and reviews/d5_collar_count_20260928 (planar PP and CP)", + "reviews/d5_punctured_pin_continuum_claude_20260929/REVIEW.md (committed record of the Math-#105 comment 5872932723 analytic review of planar PP: ACCEPT, existential, no defect) and reviews/d5_collar_count_20260928 (planar PP and CP)", "reviews/d5_intermediate_window_claude_20260928 and reviews/d5_i5_planar_f_20260928 (planar IW)" ], "nonauthor_acceptance": false, - "governing_status_changed": false + "governing_status_changed": false, + "source_commit_note": "All eight inputs re-verified byte-identical (same git blobs) on Math- main e947ade51defcec1fb75444efbe91ac7fcf43f60 on 2026-09-29; the pins above remain the exact consumed bytes." } From 35573a7f6d7f984b36ab264edb5819d96a22f8ca Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 29 Sep 2026 16:43:59 +0000 Subject: [PATCH 3/7] =?UTF-8?q?Add=20D1-C/D/E=20full-depth=20nonauthor=20r?= =?UTF-8?q?eview=20(reconciliation=20=C2=A78=20item=203)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Answers the D1 chain reconciliation's §8 invitation, item 3: a full-depth Anthropic/Claude review of interfaces D1-C (parent §10 radial ledger), D1-D (§§13–14 majorant and off-diagonal), and D1-E (§15 parity/disintegration/ gamma factor), where xAI/Grok was the only full-depth provider and Claude was previously partial. This converts those three interfaces to two full-depth providers. Verdict: ACCEPT at the reconciliation §2 existential scope, no defect found. Every displayed identity is re-derived (det T_r = 12 r^-(d+3) from (3.1); the Gamma(7/6) tau^(4/3)/(24^(1/3) sqrt pi) factor; (14.1); amplitude a^-2/3), and the (15.2) reference specialization is shown algebraically identical to the coefficients/side24_v1 closed form. Checker cde_review_check.py: Python stdlib only, fail-closed via SystemExit, byte-identical under -O, three semantic mutants (M1 det-T_r factor, M2 ledger height power, M3 gamma exponent) each exit 1. Workflow guards source identity + both replay modes + mutant rejection, matching the sard-g-r3r4 pattern. Scientific effect: NONE. No register, GRAPH, STATUS, lemma_closed, prize or premise is changed; no numerical C/r_*/z_*/coefficient; no d>=3 lower bound; scoped, not unconditional. Delivered under a new explicit owner instruction (claude.ai session, 2026-09-29); OWNER_STOP left in place; no self-merge — a non-Claude lane should review and merge. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU --- .github/workflows/d1-cde-fulldepth-review.yml | 59 +++++ .../RESULTS.json | 60 +++++ .../REVIEW.md | 152 ++++++++++++ .../SOURCE_FILES.json | 59 +++++ .../cde_review_check.py | 224 ++++++++++++++++++ 5 files changed, 554 insertions(+) create mode 100644 .github/workflows/d1-cde-fulldepth-review.yml create mode 100644 reviews/d1_cde_full_depth_claude_20260929/RESULTS.json create mode 100644 reviews/d1_cde_full_depth_claude_20260929/REVIEW.md create mode 100644 reviews/d1_cde_full_depth_claude_20260929/SOURCE_FILES.json create mode 100644 reviews/d1_cde_full_depth_claude_20260929/cde_review_check.py diff --git a/.github/workflows/d1-cde-fulldepth-review.yml b/.github/workflows/d1-cde-fulldepth-review.yml new file mode 100644 index 000000000..fa03e30ab --- /dev/null +++ b/.github/workflows/d1-cde-fulldepth-review.yml @@ -0,0 +1,59 @@ +name: D1-C/D/E full-depth nonauthor review checks + +'on': + pull_request: + paths: + - 'reviews/d1_cde_full_depth_claude_20260929/**' + - '.github/workflows/d1-cde-fulldepth-review.yml' + workflow_dispatch: + +permissions: + contents: read + +jobs: + exact-and-probe: + runs-on: ubuntu-latest + timeout-minutes: 10 + steps: + - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 + with: + persist-credentials: false + - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 + with: + python-version: '3.11.16' + - name: Verify sources, replay both modes, reject mutants + env: + PYTHONDONTWRITEBYTECODE: '1' + run: | + set -euo pipefail + python -B -S - <<'PY' + import hashlib, json, pathlib, subprocess, sys + root = pathlib.Path('reviews/d1_cde_full_depth_claude_20260929').resolve() + manifest = json.loads((root / 'SOURCE_FILES.json').read_text())['files'] + present = sorted(p.name for p in root.iterdir()) + expected_names = sorted([e['path'] for e in manifest] + ['SOURCE_FILES.json']) + if present != expected_names: + raise ValueError('packet tree differs from manifest: ' + repr(present)) + for entry in manifest: + path = root / entry['path'] + if pathlib.PurePosixPath(entry['path']).name != entry['path'] or path.is_symlink(): + raise ValueError('flat regular source required: ' + entry['path']) + data = path.read_bytes() + if len(data) != entry['bytes'] or hashlib.sha256(data).hexdigest() != entry['sha256']: + raise ValueError('source identity mismatch: ' + entry['path']) + script = str(root / 'cde_review_check.py') + expected = (root / 'RESULTS.json').read_bytes() + mutants = ['M1', 'M2', 'M3'] + for flags in (['-B', '-S'], ['-B', '-O', '-S']): + out = subprocess.run([sys.executable, *flags, script], + check=True, capture_output=True, timeout=300).stdout + if out != expected: + raise RuntimeError('output differs from RESULTS.json under ' + ' '.join(flags)) + for m in mutants: + rc = subprocess.run([sys.executable, *flags, script, '--mutant', m], + capture_output=True, timeout=300).returncode + if rc != 1: + raise RuntimeError('mutant ' + m + ' not rejected') + print(json.dumps({'scientific_effect': 'NONE', 'mathematical_acceptance': False})) + PY + git diff --exit-code diff --git a/reviews/d1_cde_full_depth_claude_20260929/RESULTS.json b/reviews/d1_cde_full_depth_claude_20260929/RESULTS.json new file mode 100644 index 000000000..21ab159fb --- /dev/null +++ b/reviews/d1_cde_full_depth_claude_20260929/RESULTS.json @@ -0,0 +1,60 @@ +{ + "object": "CL-D1-CDE-FULLDEPTH-20260929-v1-CHECKS", + "passed": true, + "results": { + "C1_detTr_exact_12_r_minus_d_plus_3": [ + [ + 2, + "1/7", + "201684" + ], + [ + 2, + "3/5", + "12500/81" + ], + [ + 2, + "1", + "12" + ], + [ + 2, + "9/4", + "4096/19683" + ], + [ + 3, + "1/7", + "1411788" + ], + [ + 3, + "3/5", + "62500/243" + ], + [ + 3, + "1", + "12" + ], + [ + 3, + "9/4", + "16384/177147" + ] + ], + "C2_radial_ledger_power": 1, + "C3_target_coercivity_13_1": "grid 6x4x3 exact", + "C4_pushforward_11_1_cubed_identity": "exact", + "C5_gamma_factor_15_2": "rel<1e-9 at tau=1,2.5", + "C6_half_gaussian_moment": "rel<1e-9", + "C7_amplitude_scaling_exponent": "-2/3 all d in 2..10", + "C8_specialization_concordance": { + "c2": "0.073406919306034296", + "c3": "0.041775931840598357" + }, + "C9_E1_congruence": "det(DHD)=det(H)/r exact; sqrt-r mutant differs" + }, + "scope": "finite exact/numerical controls for parent Sections 10, 13-14, 15 as read with E1/E2/W1; not the Gaussian proof" +} diff --git a/reviews/d1_cde_full_depth_claude_20260929/REVIEW.md b/reviews/d1_cde_full_depth_claude_20260929/REVIEW.md new file mode 100644 index 000000000..f05700e24 --- /dev/null +++ b/reviews/d1_cde_full_depth_claude_20260929/REVIEW.md @@ -0,0 +1,152 @@ +# Nonauthor-lane full-depth review: D1-C, D1-D, D1-E (parent §§10, 13–14, 15) + +Scientific effect: **NONE**. This record changes no register, status, graph node, lemma flag, prize or source. +It answers the reconciliation's §8 invitation, item 3: a full-depth Claude review of the three interfaces where +xAI is full-depth and Claude was previously partial. Integration is a separate act, by a non-Claude lane, after +reading, and only when the owner stop is lifted or an explicit owner instruction authorizes it. + +## Object and exposure + +| Field | Value | +|---|---| +| Object | UNIFORM-MATRIX-CAP-LIFETIME-20260924-v1 (OpenAI/ChatGPT), interfaces D1-C (§10), D1-D (§§13–14), D1-E (§15) | +| Parent bytes | `imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md`, blob `dfed3b8d318a3ab1950957f393307733a4bef3f2`, 40261 B, SHA256 `9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7` | +| Reading rule | Parent read WITH E1 (blob `213594d6…`), E2 §9 replacement v1.1 (blob `fe9b9ce4…`), W1 and the embedding radius, exactly per `reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md` §1 | +| Read at | Math- default head `dbccbb41a58f2328b3bec6c4609a4b8fb3ac811f` (shallow clone, 2026-09-29) | +| Reviewer | Anthropic Claude (claude.ai session `session_01NMeKEismAyeqgdB4sy2NJU`), a different Claude session from reconciler/reviewer C1–C2 (`session_017Mi3hxjaxV45x6zo6o1ee3`) | +| Exposure | Same provider as C1/C2 and same shared GitHub account: this record converts Claude's partial depth on D1-C/D/E to full depth; it does NOT add a third provider, does not revalidate §§2–9 (outside scope), and claims no organizational independence. This session separately audited the superseded 2026-08-01 SIDE24 packet and maintains the 06B verification suite; that prior work is disclosed, and none of it is treated as review evidence here. | +| Own checks | `cde_review_check.py`: exact Fraction controls C1–C4, C7, C9 and numerical controls C5, C6, C8 (tolerances stated inline); byte-identical under `-O`; three semantic mutants exit 1. Finite controls only — not the Gaussian proof. | + +## Verdicts + +| Interface | Parent lines | Verdict | +|---|---|---| +| **D1-C §10** — exact radial ledger | 310–336 | **ACCEPT** (full depth) | +| **D1-D §13** — target-growth majorant, removal of all birth/gap cutoffs | 386–434 | **ACCEPT** (full depth) | +| **D1-D §14** — off-diagonal bound (14.1) and Theorem C composition | 435–446 | **ACCEPT** (full depth) | +| **D1-E §15** — parity, b-disintegration, gamma factor, (15.2) | 447–481 | **ACCEPT** (full depth) | + +No defect was found in the reviewed sections as read under the reading rule. Everything accepted is at the +reconciliation §2 existential scope: no numerical `C`, `r_*`, `z_*`, `c_{B,K}` or `c_{d,L}`, no `d ≥ 3` lower +bound, no unrestricted difference rate. + +## Re-derivations — D1-C (§10) + +1. **(10.1) pin-density transfer.** `U_r = T_r O_r` with `T_r` linear invertible, so + `density_{O_r}(pins) = |det T_r| · π_r(v_r)`. I re-derived `|det T_r|` from the (3.1) display by exact block + computation: basis change `(f(a),f(c)) → (p,q)` and `(f_x(a),f_x(c)) → (p_x,q_x)` contributes `|det| = 4`; + in the new basis the axial rows are triangular with pivots `1/2, 1/r, 1/r, 6/r²`, product `3/r⁴`; total + axial factor `12/r⁴`. Each transverse pair contributes `det [[1/2,1/2],[−1/r,1/r]] = 1/r`. Hence + `|det T_r| = 12 r^{−4} · r^{−m} = 12 r^{−(d+3)}`, agreeing with (3.2). Checked exactly for `d = 2, 3` at four + rationals each (checker C1). +2. **Measure factors.** `(M,S) → (z,h)` has absolute determinant 1 (standard midpoint/difference block matrix); + `h = ru` polar gives `r^{d−1} dr dσ(u)` with ordinary (unnormalized) surface measure; at fixed `r` the height + map `(b,k) → (f(M), f(S)) = (b, b − kr³)` has Jacobian matrix `[[1,0],[1,−r³]]`, absolute determinant `r³`. +3. **Power ledger.** `(d−1) + 3 − (d+3) + 2 = 1` for every `d` (checker C2), giving the intensity + `r A_r dr db dk dσ(u)` with `A_r = 12 π_r(v_r)(Z_r/r²)` — exactly (10.2). The `Z_r/r²` normalizer is the §5 + object; its use here consumes (5.5) only through boundedness/positivity already reviewed at A3. +4. **No 1/2 factor.** The pair is typed (maximum vs index-(d−1) saddle), and the antipodal direction `−u` + corresponds to the role-swapped pair, which is a different typed configuration; no double count and no + half-factor. This agrees with an independent check of the same convention I ran against the superseded + 2026-08 line (ordered-pair/directed-sphere module), a useful cross-era consistency datum. +5. **Frame invariance.** (10.2) depends on the frame only through `u`: a transverse orthogonal change fixes the + pins, the typed indicator and `|det H_M det H_S|`, and `π_r(v_r)` is computed at a target invariant under + that change. The uniformity transfer from the compact orthogonal group to the sphere is sound; no global + transverse frame on `S^{d−1}` is needed. + +## Re-derivations — D1-D (§13) + +1. **(13.1).** `|v_r| ≤ C(|b| + k)` is immediate from the five displayed coordinates with `r ≤ 1`. For the lower + bound, `b² ≤ 2(b − kr³/2)² + 2(kr³/2)² ≤ 2(b − kr³/2)² + k²/2`, so + `(b − kr³/2)² + 144k² ≥ b²/2 − k²/4 + 144k² ≥ (b² + k²)/2`. Verified exactly on a 6×4×3 rational grid + (checker C3). +2. **(13.2).** §3's eigenvalue band for `Σ_r` on `r ≤ r₀` is target-free, so the Gaussian density bound + `π_r(v_r) ≤ C exp(−c|v_r|²) ≤ C exp(−c(b²+k²))` follows with `c = 1/(2λ_max)` uniform in frame and radius. +3. **(13.3).** The conditional mean of each standardized Fourier coefficient is `Cov(ξ, U_r) Σ_r^{−1} v_r`, with + norm `≤ C_ξ |v_r|` and `Σ C_ξ < ∞` by the rapidly decaying spectral weights; centered conditional variances + are ≤ 1. The Minkowski/summability argument is the same mechanism as (4.1), which is already reviewed at A1/A4; + its polynomial-growth version here is a correct rereading, not a new estimate (see N1). +4. **Weight bound without k-division.** From (5.1) and the canceled-pivot identity (5.3), + `|det H_i|/r ≤ |α_i| ‖A_i‖^{m} + r ‖β_i‖² ‖A_i‖^{m−1}` up to fixed constants, and `|α_i|, ‖β_i‖ ≤ M3/2`, + so `W_r/r² ≤ C (1 + ‖f‖_{C³})^{2d}`. No division by `k` or by `Z_r` occurs, which is what lets the majorant + cover the `k → 0` boundary. +5. **(13.4)–(13.5).** The unnormalized product `A_r = 12 π_r (Z_r/r²)` is then dominated by + `H(b,k) = C(1+|b|+k)^{2d} e^{−c(b²+k²)}`. The near-restriction indicator is exactly `k ≥ ℓ/r₀³` under + `r = (ℓ/k)^{1/3}`; the pushforward factor is (11.1), whose cubed form + `[r dr/dℓ]³ = 1/(27k²ℓ)` I verified exactly (checker C4). `H(b,k) k^{−2/3}` is integrable on + `R × (0,∞)`: exponent `−2/3 > −1` at zero, Gaussian tails elsewhere. +6. **`Z_r > 0` at fixed parameters.** Appending both endpoint transverse Hessians to the §2-distinct pin list + gives a nondegenerate joint Gaussian; the open cone product (negative-definite at `M`, index-(d−1) at `S`) + has positive probability, and `W_r` is strictly positive there. So `p_r` is defined for every fixed + `(r, b, k, R)` without any global floor — the step the majorant route genuinely needs. +7. **DCT and (13.6).** Pointwise in `(b,k,u)`: the indicator → 1, `A_r → A_0` (§§3, 5 uniform-on-compacts + convergence), `p_r → 1` (Theorem A applied on a compact neighborhood). Dominated convergence gives the common + limit for candidate and elder densities and `c_{B,K} ↑ c_{d,L}` along exhausting mark rectangles. The text + correctly refuses to manufacture an unrestricted remainder rate from DCT. + +## Re-derivations — D1-D (§14) + +1. **(14.1).** On the compact far domain (torus distance ≥ r₀), the 2(d+1) value/gradient pin covariance is + uniformly positive definite (§2 distinct-site rank + compactness; no diagonal singularity), the target + `(b, 0, …, 0, b−ℓ, 0, …, 0)` has squared norm ≥ b², the height pair Jacobian is exactly 1, and conditional + determinant-product moments grow at most polynomially in `|b|`. Integrating `C(1+|b|)^{2d} e^{−cb²}` over `b` + and the compact position domain gives `ν_cand^far(ℓ) ≤ C` uniformly on `0 < ℓ ≤ 1`, and the elder mark ≤ 1 + gives `ν_eld^far ≤ ν_cand^far`. Hence `ℓ^{1/3} ν^far → 0`, which is all Theorem C consumes. +2. **Consistency triangle.** (14.1) is an upper `O(1)`; the separately reviewed Theorem U + (`frontiers/unrestricted_selection_difference_20260929`, OpenAI review 2026-09-29) gives a positive lower + constant for far rejected pairs. Together: far rejected density `Θ(1)` — consistent, and jointly they refute + any `ν^far = O(ℓ)`-type claim, of the kind that appeared (unproven) in the superseded 2026-08-01 line and + was tagged there by this session as finding F-02. The current parent never makes that claim. +3. **Covering and multiplicity.** Near/far cover all distinct ordered pairs (the boundary is spatially null); + stationarity converts to per-volume densities; on the Morse distinct-value locus each finite ordinary + superlevel H0 bar has exactly one maximum birth and one index-(d−1) merge death, so the selected count is the + bar count; the essential class is excluded. Accepted as written. + +## Re-derivations — D1-E (§15) + +1. **Parity split.** Real stationarity gives `K(−z) = K(z)`, so every odd-total-order derivative covariance at 0 + vanishes: `(G, t_u)` (orders 1, 3) is independent of `(f, V_u, A_u)` (orders 0, 2, 2). The §3 contact vector + is exactly `(f, V_u) ⊕ (G, t_u)`, so `π_0(v_0) = p_{(f,V_u)}(b,0) · p_G(0) · φ_{τ_u}(12k)` with + `t_u | G = 0` centered (odd regression on odd, evaluated at 0) and `τ_u² > 0` by §2 jet rank. +2. **b-disintegration.** `A_u` is even, so conditioning it on `(f, V_u) = (b, 0)` only; then + `∫_R p_{(f,V_u)}(b,0) E[(det A_u)² 1{A_u<0} | f=b, V_u=0] db = p_{V_u}(0) D_u` by ordinary Gaussian + disintegration. This is the exact analogue of the birth-integration collapse in the superseded line, now in + clean form. +3. **Gamma factor.** `z_0 = (6k)² E[…]` and the leading 4 give `4·36 = 144`; with `t = 12k`, + `∫_0^∞ k^{4/3} φ_τ(12k) dk = 12^{−7/3} ∫_0^∞ t^{4/3} φ_τ(t) dt = 12^{−7/3} · τ^{4/3} 2^{−1/3} Γ(7/6)/√π`, + and `144 · 12^{−7/3} · 2^{−1/3} = 12^{−1/3} 2^{−1/3} = 24^{−1/3}`. Hence the display + `Γ(7/6) τ^{4/3} / (24^{1/3} √π)` is exact (checker C5/C6 numerically to < 1e−9; the reconciliation's own + check is corroborated). The parent's remark that 24 is a Jacobian/gamma constant, not the side length, is + correct. +4. **Amplitude normalization.** Under `f → af`: `p_G(0) ∼ a^{−d}`, `p_{V_u}(0) ∼ a^{−d}`, `τ_u^{4/3} ∼ a^{4/3}`, + `D_u ∼ a^{2(d−1)}`; the exponent sum is `−2/3` for every `d` (checker C7), matching + `ν_{af}(ℓ) = a^{−1} ν_f(ℓ/a)`. +5. **Specialization concordance (context, not part of the verdict).** For the nonperiodic reference law + (`Cov G = I_d`, `V_u ∼ diag(3,1,…,1)`, `τ² = 6`), (15.2) reduces to + `Γ(7/6)(3/2)^{1/3} D_{d−1} / (2√3 π^{d−1} √π)` — exactly `coefficients/side24_v1/PROOF.md` eq. (1) — and for + `d = 3` this equals `2^{−23/6} 3^{−8/3} (29√6 − 36) Γ(1/6) π^{−5/2}` identically + (`Γ(7/6) = Γ(1/6)/6`; `(3/2)^{1/3} = 6^{2/3}/24^{1/3}`, checker C8), whose 40-digit value + `0.0417759318405983433429366654285755564666…` lies in the #65-reviewed enclosure. A clean-context agent + re-derived `D₂ = 29/6 − √6` by two further independent routes on 2026-09-29 (eigenvalue-density quadrature to + 28 digits; exact symbolic `s/R²` integration). This corroborates the arithmetic chain; it does not enlarge + the existential scope of Theorem C, which still carries no numerical enclosure for the periodized `c_{d,L}`. + +## Notes + +- **N1.** (13.3) rests on the same summable-Fourier/Minkowski mechanism as (4.1) (interface A1/A4, C1-accepted). + I re-derived the mechanism rather than treating A1/A4's acceptance as covering it, but a reviewer who rejects + A1/A4 would have to revisit (13.3) too; the dependency is real and one-directional. +- **N2.** §13 deliberately never uses a globally uniform `Z_r` floor or a globally uniform Theorem-A constant; + every global statement passes through the unnormalized product `π_r Z_r`. This is the load-bearing design + point of the section and it is sound. +- **N3.** My checker's C5, C6, C8 are numerical (tolerances 1e−9 for C5 and C6; 1e−12 and 1e−15 within C8); + C1–C4, C7, C9 are exact rational. None of them proves a continuum estimate. +- **N4.** The parent bytes standalone still contain the incorrect §5 congruence display (`diag(√r, I)`); E1 is + load-bearing and consumers must keep the reading rule. My checker's C9 verifies the E1 identity and that the + uncorrected factor genuinely differs. + +## Reproduce + + python -B -S cde_review_check.py # prints RESULTS.json byte for byte + python -B -O -S cde_review_check.py # identical output + python -B -S cde_review_check.py --mutant M # exit 1 for M in {M1, M2, M3} diff --git a/reviews/d1_cde_full_depth_claude_20260929/SOURCE_FILES.json b/reviews/d1_cde_full_depth_claude_20260929/SOURCE_FILES.json new file mode 100644 index 000000000..8ee87d8d6 --- /dev/null +++ b/reviews/d1_cde_full_depth_claude_20260929/SOURCE_FILES.json @@ -0,0 +1,59 @@ +{ + "author": "Anthropic Claude", + "delivered_under": "owner instruction in claude.ai session 2026-09-29 (resumes the reconciliation \u00a78 item-3 invitation); OWNER_STOP left in place, no self-merge, scientific effect NONE", + "files": [ + { + "bytes": 13279, + "path": "REVIEW.md", + "sha256": "8f137401f1f27b76f0202f7d4c271f47899f786cf3bb7064249b46c1c268d09c" + }, + { + "bytes": 8692, + "path": "cde_review_check.py", + "sha256": "a5f5a874a396aba358b81cb41c8ee82b668efc8f50e805b254470a8c24a3daf5" + }, + { + "bytes": 1238, + "path": "RESULTS.json", + "sha256": "97b44def5a7659d500e81817b19eb54dd8de9c7e31b0db683b9eb35b430e38f0" + } + ], + "mathematical_acceptance_by_this_record": "scoped ACCEPT, nonauthor lane, existential scope only", + "mutants": [ + "M1", + "M2", + "M3" + ], + "object": "CL-D1-CDE-FULLDEPTH-20260929-v1", + "read_at_head": "dbccbb41a58f2328b3bec6c4609a4b8fb3ac811f", + "reviewed_sources": [ + { + "blob": "dfed3b8d318a3ab1950957f393307733a4bef3f2", + "bytes": 40261, + "path": "imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md", + "role": "parent (P)", + "sha256": "9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7" + }, + { + "blob": "213594d6ca6a86fb938110f4d166d9ce275a02d0", + "bytes": 1782, + "path": "imports/lifetime_parent_20260925/ERRATUM_CONGRUENCE.md", + "role": "amendment E1", + "sha256": "bad7ef609c4ad8c41ad6af562c1b6807921e19a9d556ed793ad1a0db6e202028" + }, + { + "blob": "fe9b9ce4999908bb3814b500ee2d0ceb0c6f704a", + "bytes": 9062, + "path": "reviews/d1_section9_borel_repair_20260925/REPAIR.md", + "role": "amendment E2", + "sha256": "845abf9f9c99d672c2a10a887b5a2e7206a3d2de3d876f35f75ff6e2dc13e62f" + }, + { + "blob": "75da2597971510f843f8d90c743950cb8c177342", + "path": "reviews/d1_chain_reconciliation_20260928/RECONCILIATION.md", + "role": "reading rule" + } + ], + "reviewer_session": "https://claude.ai/code/session_01NMeKEismAyeqgdB4sy2NJU", + "scientific_effect": "NONE" +} diff --git a/reviews/d1_cde_full_depth_claude_20260929/cde_review_check.py b/reviews/d1_cde_full_depth_claude_20260929/cde_review_check.py new file mode 100644 index 000000000..59fbf3d77 --- /dev/null +++ b/reviews/d1_cde_full_depth_claude_20260929/cde_review_check.py @@ -0,0 +1,224 @@ +#!/usr/bin/env python3 +# cde_review_check.py — finite exact/numerical controls for the full-depth +# review of D1-C (parent Section 10), D1-D (Sections 13-14), D1-E (Section 15) +# of UNIFORM-MATRIX-CAP-LIFETIME-20260924-v1 (read with E1/E2/W1). +# +# Python standard library only. Fail-closed: any failed check raises +# SystemExit(1) via check(); no `assert` statements are used, so `-O` +# output is byte-identical. Mutants: run with --mutant M1|M2|M3 -> exit 1. +# +# These are finite algebra/implementation controls. They do NOT prove the +# continuum Gaussian estimates; the analytic review lives in REVIEW.md. + +import json +import math +import sys +from fractions import Fraction as F + +FAILURES = [] + + +def check(name, cond): + if not cond: + FAILURES.append(name) + print("FAIL " + name) + raise SystemExit(1) + + +def det_fraction(mat): + """Exact determinant of a square Fraction matrix by fraction-free + Gaussian elimination with partial pivoting (exact over Q).""" + n = len(mat) + m = [row[:] for row in mat] + det = F(1) + for col in range(n): + piv = None + for row in range(col, n): + if m[row][col] != 0: + piv = row + break + if piv is None: + return F(0) + if piv != col: + m[col], m[piv] = m[piv], m[col] + det = -det + det *= m[col][col] + inv = F(1) / m[col][col] + for row in range(col + 1, n): + factor = m[row][col] * inv + if factor != 0: + for k in range(col, n): + m[row][k] -= factor * m[col][k] + return det + + +def build_T(r, d, u3_coeff=F(6)): + """Exact matrix of the Section 3 transformation U_r = T_r O_r. + Ordering of O_r: (f(a), f_x(a), f(c), f_x(c), + f_y1(a), f_y1(c), ..., f_ym(a), f_ym(c)). + u3_coeff is 6 in the parent display (3.1); mutant M1 uses 3.""" + m = d - 1 + n = 4 + 2 * m + T = [[F(0)] * n for _ in range(n)] + # U0 = (f(a)+f(c))/2 + T[0][0] = F(1, 2) + T[0][2] = F(1, 2) + # U1 = (f(c)-f(a))/r + T[1][0] = -F(1) / r + T[1][2] = F(1) / r + # U2 = (f_x(c)-f_x(a))/r + T[2][1] = -F(1) / r + T[2][3] = F(1) / r + # U3 = (c6/r^2)[f_x(a)+f_x(c) - 2(f(c)-f(a))/r] + c6 = u3_coeff / (r * r) + T[3][0] = c6 * F(2) / r + T[3][1] = c6 + T[3][2] = -c6 * F(2) / r + T[3][3] = c6 + # per transverse j: Vj0=(f_yj(a)+f_yj(c))/2, Vj1=(f_yj(c)-f_yj(a))/r + for j in range(m): + i0 = 4 + 2 * j + T[i0][i0] = F(1, 2) + T[i0][i0 + 1] = F(1, 2) + T[i0 + 1][i0] = -F(1) / r + T[i0 + 1][i0 + 1] = F(1) / r + return T + + +def main(argv): + mutant = None + if len(argv) == 3 and argv[1] == "--mutant": + mutant = argv[2] + elif len(argv) != 1: + print("usage: cde_review_check.py [--mutant M1|M2|M3]") + raise SystemExit(2) + + results = {} + + # ---- C1: |det T_r| = 12 r^-(d+3) exactly (parent (3.2), used in (10.1)) + u3 = F(3) if mutant == "M1" else F(6) + c1 = [] + for d in (2, 3): + for r in (F(1, 7), F(3, 5), F(1), F(9, 4)): + got = abs(det_fraction(build_T(r, d, u3))) + want = F(12) * r ** (-(d + 3)) + check("C1_detTr_d%d_r%s" % (d, r), got == want) + c1.append([d, str(r), str(got)]) + results["C1_detTr_exact_12_r_minus_d_plus_3"] = c1 + + # ---- C2: Section 10 radial power ledger sums to exactly 1 for every d + # spatial (d-1) + height-mark 3 + pin -(d+3) + determinant-normalizer 2 + height_power = 0 if mutant == "M2" else 3 + for d in range(2, 11): + total = (d - 1) + height_power - (d + 3) + 2 + check("C2_ledger_power_d%d" % d, total == 1) + results["C2_radial_ledger_power"] = 1 + + # ---- C3: (13.1) coercivity on an exact rational grid, r <= 1 + grid_b = [F(-3), F(-1), F(0), F(1, 2), F(2), F(5)] + grid_k = [F(1, 10), F(1), F(3), F(10)] + grid_r = [F(1, 10), F(1, 2), F(1)] + for b in grid_b: + for k in grid_k: + for r in grid_r: + x = b - k * r ** 3 / 2 + check("C3a", b * b <= 2 * x * x + k * k / 2) + check("C3b", x * x + 144 * k * k >= (b * b + k * k) / 2) + results["C3_target_coercivity_13_1"] = "grid %dx%dx%d exact" % ( + len(grid_b), len(grid_k), len(grid_r)) + + # ---- C4: (11.1) lifetime pushforward, checked exactly via cubes: + # with ell = k r^3, [r dr/d ell]^3 = 1/(27 k^2 ell) + for r in (F(1, 5), F(2, 3), F(7, 4)): + for k in (F(1, 3), F(1), F(8)): + ell = k * r ** 3 + lhs_cubed = (F(1) / (3 * k * r)) ** 3 + rhs_cubed = F(1) / (27 * k * k * ell) + check("C4_pushforward", lhs_cubed == rhs_cubed) + results["C4_pushforward_11_1_cubed_identity"] = "exact" + + # ---- C5/C6: the (15.2) gamma factor, numerically (Simpson) + # 144 * int_0^inf k^(4/3) phi_tau(12k) dk = Gamma(7/6) tau^(4/3) / (24^(1/3) sqrt(pi)) + def simpson(f, a, b, n): + if n % 2: + n += 1 + h = (b - a) / n + s = f(a) + f(b) + for i in range(1, n): + s += f(a + i * h) * (4 if i % 2 else 2) + return s * h / 3 + + exponent = 5.0 / 6.0 if mutant == "M3" else 7.0 / 6.0 + for tau in (1.0, 2.5): + def integrand(k, tau=tau): + if k <= 0.0: + return 0.0 + return 144.0 * k ** (4.0 / 3.0) * math.exp( + -(12.0 * k) ** 2 / (2.0 * tau * tau)) / ( + tau * math.sqrt(2.0 * math.pi)) + got = simpson(integrand, 0.0, 4.0 * tau, 400000) + want = math.gamma(exponent) * tau ** (4.0 / 3.0) / ( + 24.0 ** (1.0 / 3.0) * math.sqrt(math.pi)) + rel = abs(got - want) / want + check("C5_gamma_factor_tau%s" % tau, rel < 1e-9) + results["C5_gamma_factor_15_2"] = "rel<1e-9 at tau=1,2.5" + + # C6: the underlying half-Gaussian moment + # int_0^inf t^(4/3) phi_tau(t) dt = tau^(4/3) 2^(-1/3) Gamma(7/6)/sqrt(pi) + tau = 1.7 + got = simpson(lambda t: 0.0 if t <= 0 else t ** (4.0 / 3.0) * math.exp( + -t * t / (2 * tau * tau)) / (tau * math.sqrt(2 * math.pi)), + 0.0, 12.0 * tau, 400000) + want = tau ** (4.0 / 3.0) * 2.0 ** (-1.0 / 3.0) * math.gamma( + 7.0 / 6.0) / math.sqrt(math.pi) + check("C6_half_gaussian_moment", abs(got - want) / want < 1e-9) + results["C6_half_gaussian_moment"] = "rel<1e-9" + + # ---- C7: amplitude-scaling exponent of (15.2): a^(-2/3) for every d + for d in range(2, 11): + total = F(-d) + F(-d) + F(4, 3) + F(2) * (d - 1) + check("C7_amplitude_d%d" % d, total == F(-2, 3)) + results["C7_amplitude_scaling_exponent"] = "-2/3 all d in 2..10" + + # ---- C8: specialization concordance ((15.2) -> side24_v1 eq (1) -> value) + check("C8_cube_identity", F(36, 24) == F(3, 2)) # (6^(2/3)/24^(1/3))^3 + D2 = 29.0 / 6.0 - math.sqrt(6.0) + g76 = math.gamma(7.0 / 6.0) + c3_spec = (g76 / (24.0 ** (1.0 / 3.0) * math.sqrt(math.pi))) * \ + 4.0 * math.pi * (2.0 * math.pi) ** -3.0 * 3.0 ** -0.5 * \ + 6.0 ** (2.0 / 3.0) * D2 + c3_formula1 = g76 * (1.5) ** (1.0 / 3.0) * D2 / ( + 2.0 * math.sqrt(3.0) * math.pi ** 2.5) + check("C8_spec_eq_formula1", + abs(c3_spec - c3_formula1) / c3_formula1 < 1e-12) + check("C8_value_d3", abs(c3_formula1 - 0.041775931840598343) < 1e-15) + c2_formula1 = g76 * (1.5) ** (1.0 / 3.0) * (4.0 / 3.0) / ( + 2.0 * math.sqrt(3.0) * math.pi ** 1.5) + check("C8_value_d2", abs(c2_formula1 - 0.073406919306034271) < 1e-15) + results["C8_specialization_concordance"] = { + "c3": "%.18f" % c3_formula1, "c2": "%.18f" % c2_formula1} + + # ---- C9: E1 congruence D_r = diag(r^(-1/2), I): det(D H D) = det(H)/r, + # exact over Q for m=1 (the sqrt(r) entries only ever appear squared) + for r in (F(1, 4), F(2, 3), F(5)): + for (al, be, A) in ((F(3), F(1, 2), F(-2)), (F(-1), F(4), F(7, 3))): + detH = (r * al) * A - (r * be) * (r * be) + det_scaled_correct = al * A - r * be * be # diag(r^-1/2, 1) + det_scaled_wrong = (r * r * al) * A - (r ** 3) * be * be # diag(r^1/2,1) + check("C9_E1_identity", det_scaled_correct == detH / r) + if r != 1: + check("C9_E1_mutant_differs", det_scaled_wrong != detH / r) + results["C9_E1_congruence"] = "det(DHD)=det(H)/r exact; sqrt-r mutant differs" + + out = { + "object": "CL-D1-CDE-FULLDEPTH-20260929-v1-CHECKS", + "scope": ("finite exact/numerical controls for parent Sections 10, " + "13-14, 15 as read with E1/E2/W1; not the Gaussian proof"), + "results": results, + "passed": True, + } + print(json.dumps(out, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main(sys.argv) From b69debb2ee68772b0e4f42ce1c0a9c750e90d7d3 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 29 Sep 2026 16:51:29 +0000 Subject: [PATCH 4/7] Write out the d-dimensional Taylor remainders (4.1') behind the pin-ball expansion Answers the xAI Slice A flag (Math-#141 comment 5894274124): planar (P7) bounds two scalars, so the vector-valued remainders of (4.1) in d > 2 are now derived in section 4.2 rather than cited as verbatim. The transverse gradient h(x) = grad_y f(x, 0) is treated componentwise through the two-point identity h_i(x) = x(x - r) h_i''(xi)/2 and the derivative identity h'(0) = -(r/2) T_3 + O(r^2 K); the transverse Taylor expansion in y = r q is written with its two remainders R_3, R_2 and the Lipschitz shifts of C_3 and S_0 over the axial distance r|p|. The resulting bounds (4.1') have the powers of (P7) with |q| the Euclidean norm; only the constants depend on d. The six ratio bounds used in section 4.3 are listed. No statement, ledger, script or result changes; SOURCE_FILES.json is regenerated for the changed PROOF.md. Scientific effect NONE. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_015wNj8LPTKXsaT68G3DgPPh --- frontiers/d5_dimension_lift_20260929/PROOF.md | 40 ++++++++++++++++++- .../SOURCE_FILES.json | 6 +-- 2 files changed, 42 insertions(+), 4 deletions(-) diff --git a/frontiers/d5_dimension_lift_20260929/PROOF.md b/frontiers/d5_dimension_lift_20260929/PROOF.md index 887a79634..7b4bbe9bf 100644 --- a/frontiers/d5_dimension_lift_20260929/PROOF.md +++ b/frontiers/d5_dimension_lift_20260929/PROOF.md @@ -183,7 +183,45 @@ componentwise, by the same two-point Hermite argument. Expanding in `y = rq`, f_x(X)/r^2 = 6k p(p-1) + (r A_4/12) p(p-1)(2p-1) + (p - 1/2) q . T_3 + (1/2) q^T C_3 q + epsilon_1, grad_y f(X)/r = (r/2) p(p-1) T_3 + S_0 q + epsilon_2, (4.1) -with the pathwise bounds of [PP] (P7) holding for `|epsilon_1|` and `||epsilon_2||` verbatim (norms replace absolute values). The finite control `RO` checks the analogous expansion exactly on a pinned cubic in `d = 3` (there the remainders vanish). +with the pathwise bounds + + |epsilon_1| <= C K ( r^2 |p| + r |q| + r |p| |q|^2 + r |q|^3 ), + ||epsilon_2|| <= C K ( r^2 |p| + r |p| |q| + r |q|^2 ), (4.1') + +which are [PP] (P7) with `|q|` the Euclidean norm of `q in R^m`. Since (P7) is written for two scalars, the +`d`-dimensional remainders are derived here rather than cited. Let `h(x) = grad_y f(x, 0) in R^m`, so `h(0) = h(r) = 0` +and `h''(0) = T_3`. Every bound below is pathwise, `K` dominating the derivatives of `f` through order five on the +chart. + +- *Axial rows.* [PP] (P4) concerns the scalar `g(x) = f(x, 0)` alone and is unchanged: + `g'(rp) = 6 k r^2 p(p-1) + (r^3 A_4/12) p(p-1)(2p-1) + O(r^4 |p| K)`. +- *Transverse rows along the axis.* Componentwise, `h_i(0) = h_i(r) = 0` gives `h_i(x) = x(x - r) h_i''(xi_i)/2` with + `xi_i` in the convex hull of `{0, r, x}`, hence `|xi_i| <= r` for `x = rp`, `|p| <= 1/4`, and + `h(rp) = (r^2/2) p(p-1) T_3 + O(r^3 |p| K)`. For the derivative, `h(r) = 0` and Taylor's formula at `0` give + `h'(0) = -(r/2) T_3 + O(r^2 K)`, so `h'(rp) = r (p - 1/2) T_3 + O(r^2 K)`. Both are vector statements: each + component obeys the one-dimensional estimate and the norm of a vector is at most `sqrt(m)` times its largest + component. +- *Transverse Taylor expansion.* With `y = r q`, expand in `y` about `y = 0` at fixed `x = rp`: + + f_x(X) = g'(rp) + y . h'(rp) + (1/2) y^T D_y^2 f_x(rp, 0) y + R_3, |R_3| <= (1/6) |y|^3 sup ||D_y^3 f_x|| <= C K r^3 |q|^3, + grad_y f(X) = h(rp) + D_y^2 f(rp, 0) y + R_2, ||R_2|| <= (1/2) |y|^2 sup ||D_y^3 f|| <= C K r^2 |q|^2, + + the suprema over the segment from `(rp, 0)` to `X`, and `D_y^2 f_x(rp, 0) = C_3 + O(r |p| K)`, + `D_y^2 f(rp, 0) = S_0 + O(r |p| K)` by the Lipschitz bound over the axial distance `r|p|`. +- *Collecting.* Insert the four expansions and divide by `r^2` and `r` respectively: + + epsilon_1 = O(r^2 |p| K) + O(r |q| K) + O(r |p| |q|^2 K) + O(r |q|^3 K), + epsilon_2 = O(r^2 |p| K) + O(r |p| |q| K) + O(r |q|^2 K), + + where the four terms of `epsilon_1` come from the axial remainder, `r q . O(r^2 K)/r^2`, `(1/2) q^T O(r|p|K) q` and + `R_3/r^2`, and the three terms of `epsilon_2` from the axial remainder `O(r^3|p|K)/r`, `O(r|p|K) q` and `R_2/r`. + This is (4.1'). The only place the dimension enters is the constant, through `sqrt(m)` and the operator norms of + the tensors `C_3`, `S_0`, `D_y^3 f`; the powers of `r`, `|p|`, `|q|` are those of (P7). + +The ratios used in §4.3, `r^2|p|/Delta <= r`, `r|q|/Delta <= r`, `r|p||q|^2/Delta <= r|p||q|`, `r|q|^3/Delta <= r|q|^2`, +`r|p||q|/Delta <= r|p|`, `r|q|^2/Delta <= r|q|`, all follow from `Delta >= |q|` and `Delta >= r|p|`, exactly as in the +planar continuum record `reviews/d5_punctured_pin_continuum_claude_20260929/REVIEW.md` (its note n2). The finite +control `RO` checks the expansions (4.1) exactly on a pinned cubic in `d = 3` (there the remainders vanish). ### 4.3 A stable gradient frame on the whole punctured ball ([PP] §5) diff --git a/frontiers/d5_dimension_lift_20260929/SOURCE_FILES.json b/frontiers/d5_dimension_lift_20260929/SOURCE_FILES.json index d7094a49e..51dae27a5 100644 --- a/frontiers/d5_dimension_lift_20260929/SOURCE_FILES.json +++ b/frontiers/d5_dimension_lift_20260929/SOURCE_FILES.json @@ -5,9 +5,9 @@ "files": [ { "path": "PROOF.md", - "bytes": 47881, - "sha256": "3b0a4be490c7095f26d094e86a8aee40bff6882487ab8b6eea4375af817ae885", - "git_blob": "887a796345c8a6a22bedd5900a23d6f7547eecbc" + "bytes": 50592, + "sha256": "5acc035dccb3244bf5f14dd08d3f9786b362925cc242843cf21854376397844a", + "git_blob": "7b4bbe9bf8eb246e2845d80776a7cc5ab39bb78d" }, { "path": "README.md", From c709854d7050a5e63f3bf195b3946ed18696ddca Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 29 Sep 2026 17:33:41 +0000 Subject: [PATCH 5/7] Continuum crosswalk for the d >= 3 read; vector-valued endpoint identities (6.2) and collar expansion (5.2) derived CONTINUUM_CROSSWALK.md lists every continuum step held by the xAI Slice A and Slice B records with its planar source line (PUNCTURED_PIN_PROOF (P4)-(P20), COLLAR_PROOF (C4)-(C20), intermediate_window (I6)-(I34)), the place in PROOF.md where the d-dimensional argument is written, the complete list of what changes with the dimension, and the verdicts already on file (xAI planar (P2) continuum ACCEPT 5894512272; Slice A/B identity and rank ACCEPTs). PROOF.md section 6.3 now derives the vector-valued endpoint identities (6.2) componentwise from the four symmetric Taylor formulas at the midpoint, in place of citing the two-scalar (I12); section 5.3 records that the collar expansion (5.2) is (6.3) at s = r, epsilon = 1 on the compact chart, so no vector-valued statement is cited as verbatim from a planar scalar source. README lists the crosswalk as the eighth review interface. No statement, ledger, script or result changes; SOURCE_FILES.json regenerated. Scientific effect NONE. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_015wNj8LPTKXsaT68G3DgPPh --- .../CONTINUUM_CROSSWALK.md | 75 +++++++++++++++++++ frontiers/d5_dimension_lift_20260929/PROOF.md | 28 ++++++- .../d5_dimension_lift_20260929/README.md | 5 +- .../SOURCE_FILES.json | 18 +++-- 4 files changed, 117 insertions(+), 9 deletions(-) create mode 100644 frontiers/d5_dimension_lift_20260929/CONTINUUM_CROSSWALK.md diff --git a/frontiers/d5_dimension_lift_20260929/CONTINUUM_CROSSWALK.md b/frontiers/d5_dimension_lift_20260929/CONTINUUM_CROSSWALK.md new file mode 100644 index 000000000..bff14692b --- /dev/null +++ b/frontiers/d5_dimension_lift_20260929/CONTINUUM_CROSSWALK.md @@ -0,0 +1,75 @@ +# Continuum crosswalk: every held step, its planar line, and its `d`-dimensional replacement + +Review aid for the `d >= 3` continuum read of CL-D5-DIMENSION-LIFT-20260929-v1. Scientific effect NONE; this file +asserts no verdict. It lists, for each continuum step that the xAI Slice A and Slice B records hold (Math-#141 +comments 5894274124 and 5894406926), the exact planar line it lifts, the place in `PROOF.md` where the +`d`-dimensional argument is written, and the only things that change. Planar line numbers refer to the byte-pinned +sources of `SOURCE_MAP.json`: [PP] blob `d8acf0bc`, [CP] blob `b5647907`, [IW] blob `f53a527c`. + +Verdict columns record what is already on file; they are not claims. "xAI planar" refers to the planar (P2) +continuum record 5894512272 (Grok: (P10), (P11), (P12), (P18), region II ACCEPT for the planar source, no `d > 2` +transfer) and to #111; "xAI lift" refers to Slice A/B on this packet. Identities and rank claims accepted by Slice A/B +are listed only where a continuum step depends on them. + +## A. Pin ball, Theorem P_d (§4), planar source [PP] + +| Step | [PP] line | `PROOF.md` | What changes in `d` dimensions | Verdicts on file | +|---|---|---|---|---| +| (P4) axial Hermite expansion of `g'(rp)` | 115 | §4.2, first bullet | Nothing: `g(x) = f(x, 0)` is scalar in every `d`. | planar ACCEPT (#111 (P4)) | +| (P7) remainders `ε_1`, `ε_2` | 143 | §4.2, (4.1') with the four-bullet derivation | Vector-valued: `h = grad_y f(·, 0) ∈ R^m` handled componentwise; transverse Taylor remainders `R_3`, `R_2` written with `|y|^3`, `|y|^2`; same powers, constants carry `sqrt(m)` and tensor norms. | lift: derived in this packet (answers the Slice A flag) | +| (P8) error ratios `‖R‖_{L^s} ≤ C_s r` | 162 | §4.2 last paragraph, §4.3 remark after (4.3) | Nothing: the six ratios use only `Δ ≥ |q|`, `Δ ≥ r|p|`. | planar ACCEPT (continuum record n2) | +| (P9) frame floor `det ≥ 9/131072` | 187 | (4.4), block-Schur | `det(BB^T) ≥ (9/64)^{d-1}/2048` via Lemma D3; equals the planar constant at `d = 2`. | lift ACCEPT (Slice A identity) | +| (P10) Schur/compactness floor `c_0 I ≤ Σ ≤ C_0 I` | 193 | (4.5) and the sentence before it | `J` has `2 + 2m + m(m+1)` entries (orders 4, 3, 2, 3), none in `E_0`; positivity by distinct one-site monomials ([LP] §2); compactness over `O(d) × {|p| ≤ 1/4} × S^{d-1}`; `λ_min(BB^T) ≥ det(BB^T)/λ_max^{d-1}` from (4.4); the centered `L^2` triangle inequality with (P8) is unchanged. | xAI planar ACCEPT (P10); lift: pending | +| (P11) density `≤ C r^{-3} Δ^{-2} e^{-cχ^2}` | 210 | (4.6) | Jacobian `r^{d+1} Δ^d` in place of `r^3 Δ^2` (the map `grad f ↦ Y` is `diag(r^2Δ, rΔ I_m)`); the mean `dvec` is axial and unchanged; `|dvec + z|^2 ≥ |dvec|^2/2 - |z|^2` in `R^d`. | xAI planar ACCEPT (P11); lift: pending | +| (P12) conditional moment `E[K^6 | grad f(X) = 0] ≤ C(1 + χ^6)` | 217 | (4.7) | Same regression on `Y`; stated for every `n` (used at `n = 3d`); cross-covariances through order three bounded by Cauchy–Schwarz and (4.5). | xAI planar ACCEPT (P12); lift: pending | +| (P13)–(P14) normalizer `Z_r ≥ c_Z r^2` | 241, 249 | §4.5 | Replaced by [LP] (5.5), which holds in every fixed `d` (accepted as A1–A4 in the D1 reconciliation, Math-#106). | consumed at its accepted row | +| (P15)–(P16) angle-sensitive product | 261, 289 | (4.8) | Lemma D1 replaces the `2 × 2` two-column bound at each Hessian; new factor `K^{3(d-2)}`; segment identity (P15) is one-dimensional. | lift ACCEPT (Slice A, Lemma D1) | +| (P17) angle-free product | 308 | (4.9) | Lemma D2 (Hadamard) in place of the planar two-column bound. | lift ACCEPT (Slice A, Lemma D2 is Hadamard) | +| (P18) weighted Kac–Rice at the zero level | 323 | §4.7, (4.10) | Field `grad f : X → R^d`, parameter and value dimensions agree; same mark `W_r 1{H_X ∈ O_j}`; same framework citation. | xAI planar ACCEPT (P18); lift: pending | +| (P19) region I | 341 | (4.11) | `|q|^2 Δ^{-d} ≤ |q|^{2-d}` supplies the weight `ω_d`; `χ^2 ∈ [t^2/2, t^2]` unchanged; `n = 3d` in (4.7). | lift: pending (ledger identity accepted) | +| (P20) region II | 361 | (4.12) | Pointwise `r^{-2-4d}` and absorption `2n ≥ 5 + 3d` in place of the planar sixth term; axis included; no division by `q`. | xAI planar ACCEPT (region II); lift: pending | +| Integration and Lemma D5 | 367 | §4.8 "Integration", Lemma D5 | Weight `ω_d` integrable: radial exponent `(2-d) + (m-1) = 0`; nested ball `O(r^5)`. | lift ACCEPT (Slice A, weight only) | +| §10.1 reflection to `S` | 377–386 | §4.9 | Any orthogonal transverse map; `b̃ = b - kr^3`, `k̃ = -k`; the original `Z_r` retained. | lift: pending (dimension-free wording) | + +## B. Collar, Theorem C_d (§5), planar source [CP] + +| Step | [CP] line | `PROOF.md` | What changes in `d` dimensions | Verdicts on file | +|---|---|---|---|---| +| §3 degree-five interpolation, three sites | 61–85 | §5.1 | Explicit families `h_i, d_i, e_{i,j}` in `d` variables; generic projection direction. | lift ACCEPT (Slice B, rank) | +| (C4)–(C6) coarse floor `Cov(V_r) ≥ c r^{10} I` | 95, 109, 116 | (5.1) | `3(d+1)` observations; `dim P_5 = C(d+5, 5)`; same `r^5` floor versus `r^6` remainder; principal submatrix and Schur complement unchanged. | lift: pending | +| (C7) midpoint expansion `G_1, G_2` | 133 | (5.2) with the sentence after it, and §6.3 (6.2)–(6.3) at `s = r`, `ε = 1` | Vector form: `u v·T_3`, `v^T C_3 v`, `S_0 v`; derived from the vector-valued endpoint identities (6.2), written componentwise in §6.3. | lift: derived in this packet | +| (C8)–(C10) drift, variance, Mahalanobis | 138, 142, 148 | §5.3 | First physical coordinate only; `(C10)` is Cauchy–Schwarz in the covariance inner product in any dimension. | lift: pending | +| (C11)–(C13) near-axis strip | 157, 161, 167 | §5.4 | Prefactor `r^{-5d}` (from `det Σ_X ≥ c r^{10d}`), moment `r^{-30d}` (for `K^{3d}`), pointwise `r^{-2-35d}`, absorption `2n/3 ≥ 5 + 34d`. | lift: pending | +| (C14)–(C15) frame `B` and `c v^4 ≤ Cov(G) ≤ C v^2` | 180, 193 | §5.5, (5.3) | `BB^T ≥ diag(|v|^4/4, (|v|^2/2) I_m)` by Lemma D3 in place of the explicit `2 × 3` rows; the same `r/|v|^2 ≤ r^{1/3}` perturbation. | Lemma D3 ACCEPT (Slice A); floor use: pending | +| (C16)–(C17) density and moment | 198, 202 | (5.4), (5.5) | Jacobian `r^{d+1}`; prefactor `|v|^{-2d}`; moment `|v|^{-12d}`. | lift: pending | +| (C18) three soft Hessians | 208 | (5.6) | Lemma D1 with `σ = 1` on the orthonormal pair `(e_x, v̂)`; factor `K^{3(d-2)}`. | lift ACCEPT (Slice B, D1 use) | +| (C19) ledger | 214 | (5.7) | `r^{3-d}` per unit scaled volume; `|v|^{-(14d+6)}` absorbed by `e^{-c/|v|^2}`. | ledger identity accepted; count: pending | +| §8 compact remainder | 218–223 | §5.6 | Fixed singular-value floor of `B` for `|v| ≥ v_0`; unchanged. | lift: pending | +| (C20) Kac–Rice and gluing | 231, 235–242 | §5.7 | `dX = r^d du dv`; the two punctured balls and the collar with `η = 1/4`. | lift ACCEPT (Slice B, tiling bookkeeping) | + +## C. Shells, Theorem I_d (§6), planar source [IW] + +| Step | [IW] line | `PROOF.md` | What changes in `d` dimensions | Verdicts on file | +|---|---|---|---|---| +| (I6)–(I8) endpoint inputs and shell | 73, 88, 94 | §6 preamble | [LP] (4.1), (5.5) in every `d`; `U_r` extended by the `2m` transverse rows. | consumed at accepted rows | +| §3.1 rank through confluence | 96–147 | §6.1 | Explicit confluent families with determinants `-|v|^{2d+2}` and `u^{2d+6}`; degree-four negative control. | lift ACCEPT (Slice B, rank) | +| (I9)–(I11) remainder and floors `c s^{10}` | 124, 149, 153 | (6.1) | `(d+1)`-dimensional `Σ_X`; the divided-difference argument is one-dimensional along the axis and is applied to each transverse component. | lift: pending | +| (I12) endpoint identities at the midpoint | 167 | (6.2), now with the componentwise derivation in §6.3 | Vector-valued: `grad_y f(0) = -r^2 T_3/8 + O(r^4 K)` and `grad_y f_x(0) = O(r^2 K)` componentwise from the symmetric Taylor formulas; axial identities unchanged. | lift: derived in this packet | +| (I13)–(I16) expansions, row operation, target | 179, 185, 192, 197 | (6.3), (6.4), the Jacobian `s^{d+4}` | Vector form; the row operation subtracts `(s/2) v·grad_y f`; target `τ_{d+1}` bounded through `ε → 0`; exact finite control `RO` in `d = 3`. | lift: derived; `RO` exact | +| (I17)–(I18) Euler identity and `|S_0|` | 208, 212 | (6.5), (6.6) | Euler degree three in every `d`; controls the quadratic form `v̂^T S_0 v̂` only (one entry, not the matrix). | lift: pending (finite control `EU` in `d = 3`) | +| (I19) endpoint determinants | 218 | (6.7), (6.8) | Lemma D4 with the gradient equation `|S_0 v̂| ≤ C s K/|v|` supplying the transverse column; same shape `(r + s^2)/|v|^2`. | Lemma D4 and the shape ACCEPT (Slice B); constants: pending | +| (I20) witness determinant | 223 | (6.9) | Lemma D1 on `(e_x, v̂)`. | lift: pending | +| (I21)–(I22) combined product, axis bound | 230, 236 | (6.10) and the sentence after it | `K^{3d}`; on the axis Lemma D2 with `e_x`. | lift: pending | +| (I23)–(I26) small axial strip | 245, 258, 264, 270 | §6.5 | Prefactor `s^{-5(d+1)}`, moment `s^{-30d}`, strip volume `O(s^d) ≤ O(s^2)`. | lift: pending | +| (I27)–(I30) transverse floor, density, moment | 279, 290, 297, 301 | (6.11), (6.12), (6.13) | `BB^T ≥ diag(|v|^4/4, (|v|^2/2) I_m, |v|^6/144)` by Lemma D3; `det ≥ c|v|^{2d+8}`; `σ_min(B) ≥ c|v|^3`; prefactor `|v|^{-(d+4)}`; moment `|v|^{-18d}`. | Lemma D3 ACCEPT; floor use: pending | +| (I31)–(I32) shell ledger | 311, 319 | (6.14), (6.15) | `s^{-(d+2)}` in place of `s^{-4}`; `r` powers `-2 + 2 + 3 = 3`, `s` powers `-(d+4) + 2 + d = -2`. | ledger arithmetic ACCEPT (Slice B); count: pending | +| (I33) marked Kac–Rice with height disintegration | 334 | §6.8 | Same framework; `(grad f(X), f(X))` nondegenerate on the closed shell by (6.1). | lift: pending | +| (I34) dyadic sum | 347 | §6.8 | Unchanged. | lift ACCEPT (Slice B) | + +## D. What "pending" means here + +Every pending row is a `d`-dimensional instance of a planar step whose planar version now carries a nonauthor +ACCEPT (xAI 5894512272 for the pin ball; `reviews/d5_collar_count_20260928/` for the collar; `reviews/d5_i5_planar_f_20260928/` +for the shells), with the change listed in the fourth column. A reader can therefore check each row by (i) confirming +the planar step at the cited line, (ii) confirming that the fourth column is the complete list of changes, and (iii) +confirming the exponent arithmetic in `RESULTS.json` (groups `L`, `W`) where it applies. diff --git a/frontiers/d5_dimension_lift_20260929/PROOF.md b/frontiers/d5_dimension_lift_20260929/PROOF.md index 7b4bbe9bf..faf7b23db 100644 --- a/frontiers/d5_dimension_lift_20260929/PROOF.md +++ b/frontiers/d5_dimension_lift_20260929/PROOF.md @@ -363,7 +363,11 @@ With `D(u) = u^2 - 1/4`, the endpoint pins and Taylor's formula give, uniformly G_1 := f_x(ru, rv)/r^2 = 6k D(u) + u v . T_3 + (1/2) v^T C_3 v + O_(L^s)(r), G_2 := grad_y f(ru, rv)/r = S_0 v + O_(L^s)(r), (5.2) -exactly as [CP] (C7), with `v . T_3`, `v^T C_3 v` and `S_0 v` replacing the planar products. Hence `|E_(Q_r) G_1 - 6k D(u)| <= C(|v| + r)` and `Var_(Q_r)(G_1) <= C(|v|^2 + r^2)`. On `|v| <= v_0 <= eta/2` the collar gives `|D(u)| >= eta^2/4`, so `|E_(Q_r) G_1| >= d_0 > 0` after reducing `v_0` and `r_*`. The one-coordinate Mahalanobis bound `m^T Sigma^(-1) m >= m_1^2 / Sigma_11` [CP] (C10) supplies the factor `exp[-c/(r^2 + |v|^2)]` in the joint `d`-dimensional density. +exactly as [CP] (C7), with `v . T_3`, `v^T C_3 v` and `S_0 v` replacing the planar products. Since (C7) is stated for +two scalars, the vector form is derived in §6.3: (5.2) is (6.3) with `s = r` and `epsilon = 1` (so `d_e = D(u)`), on +the compact chart `|u|, |v| <= R`, whose `O(sK)` and `O(s^2 K)` remainders are `O(rK)`; the terms `(r/2) D(u) T_3`, +`r u C_3 v` and `(r/2) D_3[v, v]` of the transverse line are absorbed into the `O_(L^s)(r)` of the second line of +(5.2), and the inputs are the vector-valued endpoint identities (6.2). Hence `|E_(Q_r) G_1 - 6k D(u)| <= C(|v| + r)` and `Var_(Q_r)(G_1) <= C(|v|^2 + r^2)`. On `|v| <= v_0 <= eta/2` the collar gives `|D(u)| >= eta^2/4`, so `|E_(Q_r) G_1| >= d_0 > 0` after reducing `v_0` and `r_*`. The one-coordinate Mahalanobis bound `m^T Sigma^(-1) m >= m_1^2 / Sigma_11` [CP] (C10) supplies the factor `exp[-c/(r^2 + |v|^2)]` in the joint `d`-dimensional density. ### 5.4 Very near the axis: `|v| <= r^(1/3)` ([CP] §6) @@ -450,7 +454,27 @@ Let `T_3 = grad_y f_xx(0) in R^m`, `C_3 = D_y^2 f_x(0) in Sym_m`, `D_3 = D_y^3 f |f(0) - b_bar| <= C r^4 K, f_x(0) = -3k r^2/2 + O(r^4 K), grad_y f(0) = -r^2 T_3/8 + O(r^4 K), |f_xx(0)| + ||grad_y f_x(0)|| <= C r^2 K, f_xxx(0) = 12k + O(r^2 K), (6.2) -by the same averaged endpoint identities as [IW] (I12), applied to each transverse component. With `d_e = u^2 - epsilon^2/4`, at `X = s(u, v)`, +by the same averaged endpoint identities as [IW] (I12), applied to each transverse component. Since (I12) is stated for +two transverse scalars, the vector-valued identities are derived here. Write `g(x) = f(x e_1)` and +`h(x) = grad_y f(x e_1) in R^m`, so the pins read `g(-r/2) = b`, `g(r/2) = b - k r^3`, `g'(±r/2) = 0`, `h(±r/2) = 0`. +Taylor's formula at `0` through order four, with `K` bounding the fifth derivatives, gives for each of `g` and each +component `h_i`: + + phi(r/2) - phi(-r/2) = r phi'(0) + (r^3/24) phi'''(0) + O(r^5 K), + phi(r/2) + phi(-r/2) = 2 phi(0) + (r^2/4) phi''(0) + O(r^4 K), + phi'(r/2) - phi'(-r/2) = r phi''(0) + O(r^3 K), + phi'(r/2) + phi'(-r/2) = 2 phi'(0) + (r^2/4) phi'''(0) + O(r^4 K). + +For `phi = g`: the third line gives `f_xx(0) = O(r^2 K)`; the fourth gives `g'(0) = -(r^2/8) g'''(0) + O(r^4 K)`; +inserting this into the first, whose left side is `-k r^3`, gives `-(r^3/12) g'''(0) = -k r^3 + O(r^5 K)`, hence +`f_xxx(0) = 12k + O(r^2 K)` and `f_x(0) = -3k r^2/2 + O(r^4 K)`; the second gives `f(0) = b - k r^3/2 - (r^2/8) f_xx(0) ++ O(r^4 K) = b_bar + O(r^4 K)`. For `phi = h_i`, both left sides vanish: the first line gives `h_i'(0) = O(r^2 K)`, +that is `grad_y f_x(0) = O(r^2 K)`, and the second gives `h_i(0) = -(r^2/8) h_i''(0) + O(r^4 K)`, that is +`grad_y f(0) = -(r^2/8) T_3 + O(r^4 K)`. Each is a one-dimensional identity applied to one component; the vector norm +costs a factor `sqrt(m)` in the constant. This is (6.2). + +The expansions (6.3) below hold for any bounded `(u, v)` and any `epsilon <= 1`, with constants depending on the +bound; §5.3 uses them with `s = r`, `epsilon = 1` on `|u|, |v| <= R`. With `d_e = u^2 - epsilon^2/4`, at `X = s(u, v)`, f_x(X)/s^2 = 6k d_e + u v . T_3 + (1/2) v^T C_3 v + O(sK), grad_y f(X)/s = S_0 v + (s/2) d_e T_3 + s u C_3 v + (s/2) D_3[v, v] + O(s^2 K), diff --git a/frontiers/d5_dimension_lift_20260929/README.md b/frontiers/d5_dimension_lift_20260929/README.md index 08fbe759d..1e449f976 100644 --- a/frontiers/d5_dimension_lift_20260929/README.md +++ b/frontiers/d5_dimension_lift_20260929/README.md @@ -41,7 +41,10 @@ Nine groups of exact checks (`X G R RO EU TB N L W`): exterior-power inequality 4. Lemma D5: integrability of the weight and the `O(r^5)` nested-ball bound; the region I/II ledgers (4.11), (4.12). 5. §5.1 and §6.1: degree-five interpolation in `d` variables, the confluent families, and the compactness step. 6. The tiling in §7, and the claim that [RM] Theorem A, [RC] (F-) and [EDL] (A4) are consumed at their stated every-`d` scope. -7. Every step cited as "verbatim" from a planar source: confirm it is in fact dimension-free. +7. Every step cited as "verbatim" from a planar source: confirm it is in fact dimension-free. The vector-valued + statements behind (4.1), (5.2) and (6.2) are derived in §4.2, §5.3 and §6.3 rather than cited. +8. For the `d >= 3` continuum read: `CONTINUUM_CROSSWALK.md` lists every held continuum step with its planar line, + the place where the `d`-dimensional argument is written, and the complete list of changes. ## What this does not do diff --git a/frontiers/d5_dimension_lift_20260929/SOURCE_FILES.json b/frontiers/d5_dimension_lift_20260929/SOURCE_FILES.json index 51dae27a5..93be3022a 100644 --- a/frontiers/d5_dimension_lift_20260929/SOURCE_FILES.json +++ b/frontiers/d5_dimension_lift_20260929/SOURCE_FILES.json @@ -3,17 +3,23 @@ "scientific_effect": "NONE", "review_status": "AUTHOR_SIDE_REVIEW_REQUIRED", "files": [ + { + "path": "CONTINUUM_CROSSWALK.md", + "bytes": 10595, + "sha256": "41ca261dc1425d18ff181c4a4c92bea376244451edc48de736a5fc5f6aff7181", + "git_blob": "bff14692b73fd6cea2e40e4a6f86bc3e63efe930" + }, { "path": "PROOF.md", - "bytes": 50592, - "sha256": "5acc035dccb3244bf5f14dd08d3f9786b362925cc242843cf21854376397844a", - "git_blob": "7b4bbe9bf8eb246e2845d80776a7cc5ab39bb78d" + "bytes": 52605, + "sha256": "ab0ae58d9ad94560104bd12077523ba061fff54e9411259041f219224a1926d8", + "git_blob": "faf7b23dbc06439462728a490c6ab22e28bfa408" }, { "path": "README.md", - "bytes": 5096, - "sha256": "293e3a4f6eac0d1e74d8c98abf14e230d1257d03fa59ceed9e53c9d7925101cd", - "git_blob": "08fbe759d1d46540c4707732611893f968bfc5dc" + "bytes": 5424, + "sha256": "052e5c567ecf8156df3779f2885768cd8d4aaa2acbc8fd8550a146f4b9a14901", + "git_blob": "1e449f97679f8a26c58bec7e5238c1ce855af402" }, { "path": "RECONNAISSANCE.md", From cd6872358ef9c415eddcdf7a95311dca5dd4dc7d Mon Sep 17 00:00:00 2001 From: d6g8k5htny-coder Date: Tue, 29 Sep 2026 20:15:37 +0000 Subject: [PATCH 6/7] D5 lift: record OpenAI crosswalk A+B acceptance and write in its two reading clarifications MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - PROOF.md §5.2: the unscaling step is stated as the congruence plus the Schur variational identity (not eigenvalue monotonicity under entrywise scaling) - PROOF.md §5.7: collar constants depend on fixed d, R, eta and the mark compacts; nothing uniform as d grows - CONTINUUM_CROSSWALK.md: tables A and B verdict columns cite review 5357858391; table C stays pending; section D updated - README.md interface 8 and SOURCE_MAP.json consumed_reviews updated - SOURCE_FILES.json regenerated No statement, ledger, script or result changed. Scientific effect NONE. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_015wNj8LPTKXsaT68G3DgPPh --- .../CONTINUUM_CROSSWALK.md | 40 +++++++++++-------- frontiers/d5_dimension_lift_20260929/PROOF.md | 4 +- .../d5_dimension_lift_20260929/README.md | 7 +++- .../SOURCE_FILES.json | 24 +++++------ .../SOURCE_MAP.json | 3 +- 5 files changed, 46 insertions(+), 32 deletions(-) diff --git a/frontiers/d5_dimension_lift_20260929/CONTINUUM_CROSSWALK.md b/frontiers/d5_dimension_lift_20260929/CONTINUUM_CROSSWALK.md index bff14692b..808524f5b 100644 --- a/frontiers/d5_dimension_lift_20260929/CONTINUUM_CROSSWALK.md +++ b/frontiers/d5_dimension_lift_20260929/CONTINUUM_CROSSWALK.md @@ -9,7 +9,11 @@ sources of `SOURCE_MAP.json`: [PP] blob `d8acf0bc`, [CP] blob `b5647907`, [IW] b Verdict columns record what is already on file; they are not claims. "xAI planar" refers to the planar (P2) continuum record 5894512272 (Grok: (P10), (P11), (P12), (P18), region II ACCEPT for the planar source, no `d > 2` transfer) and to #111; "xAI lift" refers to Slice A/B on this packet. Identities and rank claims accepted by Slice A/B -are listed only where a continuum step depends on them. +are listed only where a continuum step depends on them. "OpenAI A+B" refers to the OpenAI nonauthor review 5357858391 +(bound to `c709854`): ACCEPT of every pending row of tables A and B at fixed `d`, fixed torus, compact marks and small +`r`, subject to the accepted algebraic lemmas, hence Theorems P_d and C_d analytically discharged at that source; +source-exposed (the reviewer authored the planar [PP]/[CP] inputs), with the xAI planar record as the independent base. +Table C (shells, Theorem I_d and hence G_d) is not covered by that review and stays pending. ## A. Pin ball, Theorem P_d (§4), planar source [PP] @@ -19,32 +23,32 @@ are listed only where a continuum step depends on them. | (P7) remainders `ε_1`, `ε_2` | 143 | §4.2, (4.1') with the four-bullet derivation | Vector-valued: `h = grad_y f(·, 0) ∈ R^m` handled componentwise; transverse Taylor remainders `R_3`, `R_2` written with `|y|^3`, `|y|^2`; same powers, constants carry `sqrt(m)` and tensor norms. | lift: derived in this packet (answers the Slice A flag) | | (P8) error ratios `‖R‖_{L^s} ≤ C_s r` | 162 | §4.2 last paragraph, §4.3 remark after (4.3) | Nothing: the six ratios use only `Δ ≥ |q|`, `Δ ≥ r|p|`. | planar ACCEPT (continuum record n2) | | (P9) frame floor `det ≥ 9/131072` | 187 | (4.4), block-Schur | `det(BB^T) ≥ (9/64)^{d-1}/2048` via Lemma D3; equals the planar constant at `d = 2`. | lift ACCEPT (Slice A identity) | -| (P10) Schur/compactness floor `c_0 I ≤ Σ ≤ C_0 I` | 193 | (4.5) and the sentence before it | `J` has `2 + 2m + m(m+1)` entries (orders 4, 3, 2, 3), none in `E_0`; positivity by distinct one-site monomials ([LP] §2); compactness over `O(d) × {|p| ≤ 1/4} × S^{d-1}`; `λ_min(BB^T) ≥ det(BB^T)/λ_max^{d-1}` from (4.4); the centered `L^2` triangle inequality with (P8) is unchanged. | xAI planar ACCEPT (P10); lift: pending | -| (P11) density `≤ C r^{-3} Δ^{-2} e^{-cχ^2}` | 210 | (4.6) | Jacobian `r^{d+1} Δ^d` in place of `r^3 Δ^2` (the map `grad f ↦ Y` is `diag(r^2Δ, rΔ I_m)`); the mean `dvec` is axial and unchanged; `|dvec + z|^2 ≥ |dvec|^2/2 - |z|^2` in `R^d`. | xAI planar ACCEPT (P11); lift: pending | -| (P12) conditional moment `E[K^6 | grad f(X) = 0] ≤ C(1 + χ^6)` | 217 | (4.7) | Same regression on `Y`; stated for every `n` (used at `n = 3d`); cross-covariances through order three bounded by Cauchy–Schwarz and (4.5). | xAI planar ACCEPT (P12); lift: pending | +| (P10) Schur/compactness floor `c_0 I ≤ Σ ≤ C_0 I` | 193 | (4.5) and the sentence before it | `J` has `2 + 2m + m(m+1)` entries (orders 4, 3, 2, 3), none in `E_0`; positivity by distinct one-site monomials ([LP] §2); compactness over `O(d) × {|p| ≤ 1/4} × S^{d-1}`; `λ_min(BB^T) ≥ det(BB^T)/λ_max^{d-1}` from (4.4); the centered `L^2` triangle inequality with (P8) is unchanged. | xAI planar ACCEPT (P10); lift ACCEPT (OpenAI A+B, item 1) | +| (P11) density `≤ C r^{-3} Δ^{-2} e^{-cχ^2}` | 210 | (4.6) | Jacobian `r^{d+1} Δ^d` in place of `r^3 Δ^2` (the map `grad f ↦ Y` is `diag(r^2Δ, rΔ I_m)`); the mean `dvec` is axial and unchanged; `|dvec + z|^2 ≥ |dvec|^2/2 - |z|^2` in `R^d`. | xAI planar ACCEPT (P11); lift ACCEPT (OpenAI A+B, item 2) | +| (P12) conditional moment `E[K^6 | grad f(X) = 0] ≤ C(1 + χ^6)` | 217 | (4.7) | Same regression on `Y`; stated for every `n` (used at `n = 3d`); cross-covariances through order three bounded by Cauchy–Schwarz and (4.5). | xAI planar ACCEPT (P12); lift ACCEPT (OpenAI A+B, item 2) | | (P13)–(P14) normalizer `Z_r ≥ c_Z r^2` | 241, 249 | §4.5 | Replaced by [LP] (5.5), which holds in every fixed `d` (accepted as A1–A4 in the D1 reconciliation, Math-#106). | consumed at its accepted row | | (P15)–(P16) angle-sensitive product | 261, 289 | (4.8) | Lemma D1 replaces the `2 × 2` two-column bound at each Hessian; new factor `K^{3(d-2)}`; segment identity (P15) is one-dimensional. | lift ACCEPT (Slice A, Lemma D1) | | (P17) angle-free product | 308 | (4.9) | Lemma D2 (Hadamard) in place of the planar two-column bound. | lift ACCEPT (Slice A, Lemma D2 is Hadamard) | -| (P18) weighted Kac–Rice at the zero level | 323 | §4.7, (4.10) | Field `grad f : X → R^d`, parameter and value dimensions agree; same mark `W_r 1{H_X ∈ O_j}`; same framework citation. | xAI planar ACCEPT (P18); lift: pending | -| (P19) region I | 341 | (4.11) | `|q|^2 Δ^{-d} ≤ |q|^{2-d}` supplies the weight `ω_d`; `χ^2 ∈ [t^2/2, t^2]` unchanged; `n = 3d` in (4.7). | lift: pending (ledger identity accepted) | -| (P20) region II | 361 | (4.12) | Pointwise `r^{-2-4d}` and absorption `2n ≥ 5 + 3d` in place of the planar sixth term; axis included; no division by `q`. | xAI planar ACCEPT (region II); lift: pending | +| (P18) weighted Kac–Rice at the zero level | 323 | §4.7, (4.10) | Field `grad f : X → R^d`, parameter and value dimensions agree; same mark `W_r 1{H_X ∈ O_j}`; same framework citation. | xAI planar ACCEPT (P18); lift ACCEPT (OpenAI A+B, item 3) | +| (P19) region I | 341 | (4.11) | `|q|^2 Δ^{-d} ≤ |q|^{2-d}` supplies the weight `ω_d`; `χ^2 ∈ [t^2/2, t^2]` unchanged; `n = 3d` in (4.7). | lift ACCEPT (OpenAI A+B, item 4; ledger identity Slice A) | +| (P20) region II | 361 | (4.12) | Pointwise `r^{-2-4d}` and absorption `2n ≥ 5 + 3d` in place of the planar sixth term; axis included; no division by `q`. | xAI planar ACCEPT (region II); lift ACCEPT (OpenAI A+B, item 4) | | Integration and Lemma D5 | 367 | §4.8 "Integration", Lemma D5 | Weight `ω_d` integrable: radial exponent `(2-d) + (m-1) = 0`; nested ball `O(r^5)`. | lift ACCEPT (Slice A, weight only) | -| §10.1 reflection to `S` | 377–386 | §4.9 | Any orthogonal transverse map; `b̃ = b - kr^3`, `k̃ = -k`; the original `Z_r` retained. | lift: pending (dimension-free wording) | +| §10.1 reflection to `S` | 377–386 | §4.9 | Any orthogonal transverse map; `b̃ = b - kr^3`, `k̃ = -k`; the original `Z_r` retained. | lift ACCEPT (OpenAI A+B, item 5) | ## B. Collar, Theorem C_d (§5), planar source [CP] | Step | [CP] line | `PROOF.md` | What changes in `d` dimensions | Verdicts on file | |---|---|---|---|---| | §3 degree-five interpolation, three sites | 61–85 | §5.1 | Explicit families `h_i, d_i, e_{i,j}` in `d` variables; generic projection direction. | lift ACCEPT (Slice B, rank) | -| (C4)–(C6) coarse floor `Cov(V_r) ≥ c r^{10} I` | 95, 109, 116 | (5.1) | `3(d+1)` observations; `dim P_5 = C(d+5, 5)`; same `r^5` floor versus `r^6` remainder; principal submatrix and Schur complement unchanged. | lift: pending | +| (C4)–(C6) coarse floor `Cov(V_r) ≥ c r^{10} I` | 95, 109, 116 | (5.1) | `3(d+1)` observations; `dim P_5 = C(d+5, 5)`; same `r^5` floor versus `r^6` remainder; principal submatrix and Schur complement unchanged. | lift ACCEPT (OpenAI A+B, item 6) | | (C7) midpoint expansion `G_1, G_2` | 133 | (5.2) with the sentence after it, and §6.3 (6.2)–(6.3) at `s = r`, `ε = 1` | Vector form: `u v·T_3`, `v^T C_3 v`, `S_0 v`; derived from the vector-valued endpoint identities (6.2), written componentwise in §6.3. | lift: derived in this packet | -| (C8)–(C10) drift, variance, Mahalanobis | 138, 142, 148 | §5.3 | First physical coordinate only; `(C10)` is Cauchy–Schwarz in the covariance inner product in any dimension. | lift: pending | -| (C11)–(C13) near-axis strip | 157, 161, 167 | §5.4 | Prefactor `r^{-5d}` (from `det Σ_X ≥ c r^{10d}`), moment `r^{-30d}` (for `K^{3d}`), pointwise `r^{-2-35d}`, absorption `2n/3 ≥ 5 + 34d`. | lift: pending | -| (C14)–(C15) frame `B` and `c v^4 ≤ Cov(G) ≤ C v^2` | 180, 193 | §5.5, (5.3) | `BB^T ≥ diag(|v|^4/4, (|v|^2/2) I_m)` by Lemma D3 in place of the explicit `2 × 3` rows; the same `r/|v|^2 ≤ r^{1/3}` perturbation. | Lemma D3 ACCEPT (Slice A); floor use: pending | -| (C16)–(C17) density and moment | 198, 202 | (5.4), (5.5) | Jacobian `r^{d+1}`; prefactor `|v|^{-2d}`; moment `|v|^{-12d}`. | lift: pending | +| (C8)–(C10) drift, variance, Mahalanobis | 138, 142, 148 | §5.3 | First physical coordinate only; `(C10)` is Cauchy–Schwarz in the covariance inner product in any dimension. | lift ACCEPT (OpenAI A+B, item 7) | +| (C11)–(C13) near-axis strip | 157, 161, 167 | §5.4 | Prefactor `r^{-5d}` (from `det Σ_X ≥ c r^{10d}`), moment `r^{-30d}` (for `K^{3d}`), pointwise `r^{-2-35d}`, absorption `2n/3 ≥ 5 + 34d`. | lift ACCEPT (OpenAI A+B, item 7) | +| (C14)–(C15) frame `B` and `c v^4 ≤ Cov(G) ≤ C v^2` | 180, 193 | §5.5, (5.3) | `BB^T ≥ diag(|v|^4/4, (|v|^2/2) I_m)` by Lemma D3 in place of the explicit `2 × 3` rows; the same `r/|v|^2 ≤ r^{1/3}` perturbation. | Lemma D3 ACCEPT (Slice A); floor use ACCEPT (OpenAI A+B, item 8) | +| (C16)–(C17) density and moment | 198, 202 | (5.4), (5.5) | Jacobian `r^{d+1}`; prefactor `|v|^{-2d}`; moment `|v|^{-12d}`. | lift ACCEPT (OpenAI A+B, item 8) | | (C18) three soft Hessians | 208 | (5.6) | Lemma D1 with `σ = 1` on the orthonormal pair `(e_x, v̂)`; factor `K^{3(d-2)}`. | lift ACCEPT (Slice B, D1 use) | -| (C19) ledger | 214 | (5.7) | `r^{3-d}` per unit scaled volume; `|v|^{-(14d+6)}` absorbed by `e^{-c/|v|^2}`. | ledger identity accepted; count: pending | -| §8 compact remainder | 218–223 | §5.6 | Fixed singular-value floor of `B` for `|v| ≥ v_0`; unchanged. | lift: pending | +| (C19) ledger | 214 | (5.7) | `r^{3-d}` per unit scaled volume; `|v|^{-(14d+6)}` absorbed by `e^{-c/|v|^2}`. | ledger identity accepted; count ACCEPT (OpenAI A+B, items 8–9) | +| §8 compact remainder | 218–223 | §5.6 | Fixed singular-value floor of `B` for `|v| ≥ v_0`; unchanged. | lift ACCEPT (OpenAI A+B, item 8) | | (C20) Kac–Rice and gluing | 231, 235–242 | §5.7 | `dX = r^d du dv`; the two punctured balls and the collar with `η = 1/4`. | lift ACCEPT (Slice B, tiling bookkeeping) | ## C. Shells, Theorem I_d (§6), planar source [IW] @@ -68,8 +72,12 @@ are listed only where a continuum step depends on them. ## D. What "pending" means here -Every pending row is a `d`-dimensional instance of a planar step whose planar version now carries a nonauthor +After OpenAI review 5357858391 the pending rows are exactly those of table C. Every pending row is a `d`-dimensional instance of a planar step whose planar version now carries a nonauthor ACCEPT (xAI 5894512272 for the pin ball; `reviews/d5_collar_count_20260928/` for the collar; `reviews/d5_i5_planar_f_20260928/` for the shells), with the change listed in the fourth column. A reader can therefore check each row by (i) confirming the planar step at the cited line, (ii) confirming that the fourth column is the complete list of changes, and (iii) confirming the exponent arithmetic in `RESULTS.json` (groups `L`, `W`) where it applies. + +The two reading clarifications of review 5357858391 are written into `PROOF.md`: the unscaling step of §5.2 is the +congruence and the Schur variational identity, not an eigenvalue-monotonicity claim under entrywise scaling; and the +collar constants depend on the fixed `d`, `R`, `eta` and the mark compacts (§5.7), with nothing uniform as `d` grows. diff --git a/frontiers/d5_dimension_lift_20260929/PROOF.md b/frontiers/d5_dimension_lift_20260929/PROOF.md index faf7b23db..47553b84e 100644 --- a/frontiers/d5_dimension_lift_20260929/PROOF.md +++ b/frontiers/d5_dimension_lift_20260929/PROOF.md @@ -350,7 +350,7 @@ have total degree at most five. At the three sites, `h_i` has value `delta_(ij)` ### 5.2 The coarse uniform floor ([CP] §4) -Collect the `3(d+1)` observations `V_r = ( f(ra), r grad f(ra), f(rb), r grad f(rb), f(rc), r grad f(rc) )`. With `J_5` the `C(d+5, 5)` midpoint Taylor coefficients `D^alpha f(0)/alpha!` and `D_r = diag(r^|alpha|)`, Taylor's formula through total degree five gives `V_r = B_c D_r J_5 + R_r`, `||R_r||_(L^s) <= C_s r^6` (the gradient entries carry `r . O(r^5)`), using [LP] (4.1) for the sixth derivatives. `Cov(J_5)` is uniformly positive definite (distinct one-site monomials, [LP] §2, compactness in the frame). For a unit row `t`, `std(t B_c D_r J_5) >= c r^5 ||t B_c|| >= c' r^5`, and the `L^2` triangle inequality gives `Cov(V_r) >= c r^10 I_(3(d+1))` for small `r`. Delete the auxiliary witness value (a principal submatrix keeps the floor), unscale the gradient entries by `r^(-1) >= 1`, and take the Schur complement on the `2(d+1)` pins. Hence +Collect the `3(d+1)` observations `V_r = ( f(ra), r grad f(ra), f(rb), r grad f(rb), f(rc), r grad f(rc) )`. With `J_5` the `C(d+5, 5)` midpoint Taylor coefficients `D^alpha f(0)/alpha!` and `D_r = diag(r^|alpha|)`, Taylor's formula through total degree five gives `V_r = B_c D_r J_5 + R_r`, `||R_r||_(L^s) <= C_s r^6` (the gradient entries carry `r . O(r^5)`), using [LP] (4.1) for the sixth derivatives. `Cov(J_5)` is uniformly positive definite (distinct one-site monomials, [LP] §2, compactness in the frame). For a unit row `t`, `std(t B_c D_r J_5) >= c r^5 ||t B_c|| >= c' r^5`, and the `L^2` triangle inequality gives `Cov(V_r) >= c r^10 I_(3(d+1))` for small `r`. Delete the auxiliary witness value (a principal submatrix keeps the floor), then pass from the scaled entries `r grad f` to the physical entries `grad f` by the congruence `V |-> diag(1, r^(-1) I_d, ...) V`, which multiplies the covariance by `r^(-2) >= 1` on the gradient block and, by the Schur variational identity `Cov(grad f(X) | pins) = min over affine predictors`, keeps the conditional covariance of the physical witness gradient at least `c r^10 I_d` (this is a statement about the congruence and the variational formula, not eigenvalue monotonicity under an arbitrary entrywise scaling), and take the Schur complement on the `2(d+1)` pins. Hence Sigma_X := Cov_(Q_r)( grad f(X) ) >= c r^10 I_d, Sigma_X <= C I_d. (5.1) @@ -420,7 +420,7 @@ The radius powers are `-2 - (d+1) + 6 = 3 - d`. No height-window factor appears. Weighted Kac–Rice on an open neighbourhood of the compact collar (distinct-site nondegeneracy, or the local polynomial floor), with the mark `W_r 1{H_X in O_j}`, gives (4.10) there. Since `dX = r^d du dv` and `rho_j^W <= C r^(3-d)` on all three strips, `E_(Q_r^W) N_j(rE) <= C r^3 |E|`, which is (1.3). -For (1.4), take `eta = 1/4`, partition a Borel subset of the scaled ball into its intersections with the two punctured pin balls of scaled radius `1/4` (Theorem P_d in endpoint coordinates; translation preserves volume) and the remaining collar (this theorem); assign boundaries once. Take the minimum of the radius cutoffs and the maximum of the constants. Choosing `R` larger than the inner radius of a scaled annulus supplies an overlapping cover of it. ∎ +For (1.4), take `eta = 1/4`, partition a Borel subset of the scaled ball into its intersections with the two punctured pin balls of scaled radius `1/4` (Theorem P_d in endpoint coordinates; translation preserves volume) and the remaining collar (this theorem); assign boundaries once. Take the minimum of the radius cutoffs and the maximum of the constants. Choosing `R` larger than the inner radius of a scaled annulus supplies an overlapping cover of it. Every constant and cutoff of §5 depends on the fixed `d`, `R`, `eta`, `L`, `B` and the mark compacts, as stated in §1.1; nothing in this section is uniform as `d` grows. ∎ ## 6. Proof of Theorem I_d diff --git a/frontiers/d5_dimension_lift_20260929/README.md b/frontiers/d5_dimension_lift_20260929/README.md index 1e449f976..fb861534b 100644 --- a/frontiers/d5_dimension_lift_20260929/README.md +++ b/frontiers/d5_dimension_lift_20260929/README.md @@ -44,7 +44,12 @@ Nine groups of exact checks (`X G R RO EU TB N L W`): exterior-power inequality 7. Every step cited as "verbatim" from a planar source: confirm it is in fact dimension-free. The vector-valued statements behind (4.1), (5.2) and (6.2) are derived in §4.2, §5.3 and §6.3 rather than cited. 8. For the `d >= 3` continuum read: `CONTINUUM_CROSSWALK.md` lists every held continuum step with its planar line, - the place where the `d`-dimensional argument is written, and the complete list of changes. + the place where the `d`-dimensional argument is written, and the complete list of changes. Tables A and B (pin + ball, collar) carry the OpenAI nonauthor ACCEPT 5357858391 at `c709854` (Theorems P_d, C_d discharged at that + source; source-exposed, xAI planar record as the independent base). Table C (shells; Theorem I_d and hence G_d, + F_d, M_d) is the one remaining pending slice: the height-marked shell covariance and row operation (6.1)–(6.4), + Euler suppression (6.5)–(6.6), the transverse determinant floor (6.11)–(6.13) and the `s^(-2)` shell ledger + (6.14)–(6.15). ## What this does not do diff --git a/frontiers/d5_dimension_lift_20260929/SOURCE_FILES.json b/frontiers/d5_dimension_lift_20260929/SOURCE_FILES.json index 93be3022a..62ad1dda2 100644 --- a/frontiers/d5_dimension_lift_20260929/SOURCE_FILES.json +++ b/frontiers/d5_dimension_lift_20260929/SOURCE_FILES.json @@ -5,21 +5,21 @@ "files": [ { "path": "CONTINUUM_CROSSWALK.md", - "bytes": 10595, - "sha256": "41ca261dc1425d18ff181c4a4c92bea376244451edc48de736a5fc5f6aff7181", - "git_blob": "bff14692b73fd6cea2e40e4a6f86bc3e63efe930" + "bytes": 11778, + "sha256": "a0e85044ab9a35803251c5a31ea3f48af3618ca885a68c58d48a48bbcded0a42", + "git_blob": "808524f5b402cfa6bdc122afb39a1e0c6088cc39" }, { "path": "PROOF.md", - "bytes": 52605, - "sha256": "ab0ae58d9ad94560104bd12077523ba061fff54e9411259041f219224a1926d8", - "git_blob": "faf7b23dbc06439462728a490c6ab22e28bfa408" + "bytes": 53252, + "sha256": "3da173dd356ae78776e0cde3d1e9e89beb3b8a6e3767df58a3a0f060194ed0b4", + "git_blob": "47553b84e53c0cb0c0a4a1cd5e352a585fe2aee2" }, { "path": "README.md", - "bytes": 5424, - "sha256": "052e5c567ecf8156df3779f2885768cd8d4aaa2acbc8fd8550a146f4b9a14901", - "git_blob": "1e449f97679f8a26c58bec7e5238c1ce855af402" + "bytes": 5924, + "sha256": "75a7cfaab76e7918e0749ae6e5068adaea0856bdcbbc20c66de3586dd8da5894", + "git_blob": "fb861534b300ba00f430066fdfd1acb5256ab156" }, { "path": "RECONNAISSANCE.md", @@ -35,9 +35,9 @@ }, { "path": "SOURCE_MAP.json", - "bytes": 5000, - "sha256": "b7feb9cc7540aa656aab6457d3ebee5724430aad5a688fe42f069f3d1420ffe2", - "git_blob": "ed2f3a77624c59b8513ceaf4005cffb3e45bad1e" + "bytes": 5411, + "sha256": "64851314e280576a2bf3ac81abb6731b4eb549213ae63aaf8b13c60b8ff859f8", + "git_blob": "2ab8ac1eb7d61970e72ccea2babfa3fb9e41ae6d" }, { "path": "lift_exact_check.py", diff --git a/frontiers/d5_dimension_lift_20260929/SOURCE_MAP.json b/frontiers/d5_dimension_lift_20260929/SOURCE_MAP.json index ed2f3a776..2ab8ac1eb 100644 --- a/frontiers/d5_dimension_lift_20260929/SOURCE_MAP.json +++ b/frontiers/d5_dimension_lift_20260929/SOURCE_MAP.json @@ -79,7 +79,8 @@ "main#76 (remote Theorem A, every d)", "Math-#106 A1-A4 (LP sections 2-5)", "reviews/d5_punctured_pin_continuum_claude_20260929/REVIEW.md (committed record of the Math-#105 comment 5872932723 analytic review of planar PP: ACCEPT, existential, no defect) and reviews/d5_collar_count_20260928 (planar PP and CP)", - "reviews/d5_intermediate_window_claude_20260928 and reviews/d5_i5_planar_f_20260928 (planar IW)" + "reviews/d5_intermediate_window_claude_20260928 and reviews/d5_i5_planar_f_20260928 (planar IW)", + "Math-#141 review 5357858391 (OpenAI nonauthor, bound to c709854): ACCEPT of the d-dimensional continuum rows of CONTINUUM_CROSSWALK.md tables A and B (Theorems P_d, C_d discharged at that source; source-exposed, xAI planar record 5894512272 as the independent base); table C (Theorem I_d, hence G_d, F_d, M_d) not covered; its two reading clarifications are written into PROOF.md \u00a75.2 and \u00a75.7" ], "nonauthor_acceptance": false, "governing_status_changed": false, From 914229a4ea15c9abdbbb75efe3f1e15b0b7b09fd Mon Sep 17 00:00:00 2001 From: d6g8k5htny-coder Date: Tue, 29 Sep 2026 20:20:37 +0000 Subject: [PATCH 7/7] D5 lift: record OpenAI crosswalk C acceptance, axis-safe strip bound, landing note MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - PROOF.md §6.4: the axis bound is stated as the axis-safe endpoint-short-column / Hadamard bound W_r |det H_X| / Z_r <= C K^(3d), valid throughout the strip |v| <= s^(1/8) including v = 0; §6.5 cites it as such - CONTINUUM_CROSSWALK.md: table C verdict column cites review 5357882570; no row of the crosswalk is pending; section D updated - README.md: interface 8 updated; landing note listing the three wording clarifications, the two reviews, and the retained HOLD history - SOURCE_MAP.json: consumed_reviews and the main re-verification note - SOURCE_FILES.json regenerated No statement, ledger, script or result changed. Scientific effect NONE. Co-Authored-By: Claude Fable 5.1 Claude-Session: https://claude.ai/code/session_015wNj8LPTKXsaT68G3DgPPh --- .../CONTINUUM_CROSSWALK.md | 32 +++++++++++-------- frontiers/d5_dimension_lift_20260929/PROOF.md | 4 +-- .../d5_dimension_lift_20260929/README.md | 27 ++++++++++++++-- .../SOURCE_FILES.json | 24 +++++++------- .../SOURCE_MAP.json | 5 +-- 5 files changed, 60 insertions(+), 32 deletions(-) diff --git a/frontiers/d5_dimension_lift_20260929/CONTINUUM_CROSSWALK.md b/frontiers/d5_dimension_lift_20260929/CONTINUUM_CROSSWALK.md index 808524f5b..45e4324ff 100644 --- a/frontiers/d5_dimension_lift_20260929/CONTINUUM_CROSSWALK.md +++ b/frontiers/d5_dimension_lift_20260929/CONTINUUM_CROSSWALK.md @@ -13,7 +13,10 @@ are listed only where a continuum step depends on them. "OpenAI A+B" refers to t (bound to `c709854`): ACCEPT of every pending row of tables A and B at fixed `d`, fixed torus, compact marks and small `r`, subject to the accepted algebraic lemmas, hence Theorems P_d and C_d analytically discharged at that source; source-exposed (the reviewer authored the planar [PP]/[CP] inputs), with the xAI planar record as the independent base. -Table C (shells, Theorem I_d and hence G_d) is not covered by that review and stays pending. +"OpenAI C" refers to the follow-up OpenAI nonauthor review 5357882570 (same binding `c709854`): ACCEPT of every pending +row of table C and of the analytic G_d composition at that source, same scope; with it the crosswalk A+B+C is complete. +Its one wording clarification (the §6.5 "axis bound" is the axis-safe endpoint-short-column/Hadamard bound valid +throughout the small strip) is written into `PROOF.md` §6.4–§6.5. ## A. Pin ball, Theorem P_d (§4), planar source [PP] @@ -57,27 +60,30 @@ Table C (shells, Theorem I_d and hence G_d) is not covered by that review and st |---|---|---|---|---| | (I6)–(I8) endpoint inputs and shell | 73, 88, 94 | §6 preamble | [LP] (4.1), (5.5) in every `d`; `U_r` extended by the `2m` transverse rows. | consumed at accepted rows | | §3.1 rank through confluence | 96–147 | §6.1 | Explicit confluent families with determinants `-|v|^{2d+2}` and `u^{2d+6}`; degree-four negative control. | lift ACCEPT (Slice B, rank) | -| (I9)–(I11) remainder and floors `c s^{10}` | 124, 149, 153 | (6.1) | `(d+1)`-dimensional `Σ_X`; the divided-difference argument is one-dimensional along the axis and is applied to each transverse component. | lift: pending | +| (I9)–(I11) remainder and floors `c s^{10}` | 124, 149, 153 | (6.1) | `(d+1)`-dimensional `Σ_X`; the divided-difference argument is one-dimensional along the axis and is applied to each transverse component. | lift ACCEPT (OpenAI C, item 1) | | (I12) endpoint identities at the midpoint | 167 | (6.2), now with the componentwise derivation in §6.3 | Vector-valued: `grad_y f(0) = -r^2 T_3/8 + O(r^4 K)` and `grad_y f_x(0) = O(r^2 K)` componentwise from the symmetric Taylor formulas; axial identities unchanged. | lift: derived in this packet | | (I13)–(I16) expansions, row operation, target | 179, 185, 192, 197 | (6.3), (6.4), the Jacobian `s^{d+4}` | Vector form; the row operation subtracts `(s/2) v·grad_y f`; target `τ_{d+1}` bounded through `ε → 0`; exact finite control `RO` in `d = 3`. | lift: derived; `RO` exact | -| (I17)–(I18) Euler identity and `|S_0|` | 208, 212 | (6.5), (6.6) | Euler degree three in every `d`; controls the quadratic form `v̂^T S_0 v̂` only (one entry, not the matrix). | lift: pending (finite control `EU` in `d = 3`) | -| (I19) endpoint determinants | 218 | (6.7), (6.8) | Lemma D4 with the gradient equation `|S_0 v̂| ≤ C s K/|v|` supplying the transverse column; same shape `(r + s^2)/|v|^2`. | Lemma D4 and the shape ACCEPT (Slice B); constants: pending | -| (I20) witness determinant | 223 | (6.9) | Lemma D1 on `(e_x, v̂)`. | lift: pending | -| (I21)–(I22) combined product, axis bound | 230, 236 | (6.10) and the sentence after it | `K^{3d}`; on the axis Lemma D2 with `e_x`. | lift: pending | -| (I23)–(I26) small axial strip | 245, 258, 264, 270 | §6.5 | Prefactor `s^{-5(d+1)}`, moment `s^{-30d}`, strip volume `O(s^d) ≤ O(s^2)`. | lift: pending | -| (I27)–(I30) transverse floor, density, moment | 279, 290, 297, 301 | (6.11), (6.12), (6.13) | `BB^T ≥ diag(|v|^4/4, (|v|^2/2) I_m, |v|^6/144)` by Lemma D3; `det ≥ c|v|^{2d+8}`; `σ_min(B) ≥ c|v|^3`; prefactor `|v|^{-(d+4)}`; moment `|v|^{-18d}`. | Lemma D3 ACCEPT; floor use: pending | -| (I31)–(I32) shell ledger | 311, 319 | (6.14), (6.15) | `s^{-(d+2)}` in place of `s^{-4}`; `r` powers `-2 + 2 + 3 = 3`, `s` powers `-(d+4) + 2 + d = -2`. | ledger arithmetic ACCEPT (Slice B); count: pending | -| (I33) marked Kac–Rice with height disintegration | 334 | §6.8 | Same framework; `(grad f(X), f(X))` nondegenerate on the closed shell by (6.1). | lift: pending | +| (I17)–(I18) Euler identity and `|S_0|` | 208, 212 | (6.5), (6.6) | Euler degree three in every `d`; controls the quadratic form `v̂^T S_0 v̂` only (one entry, not the matrix). | lift ACCEPT (OpenAI C, item 2; finite control `EU` in `d = 3`) | +| (I19) endpoint determinants | 218 | (6.7), (6.8) | Lemma D4 with the gradient equation `|S_0 v̂| ≤ C s K/|v|` supplying the transverse column; same shape `(r + s^2)/|v|^2`. | Lemma D4 and the shape ACCEPT (Slice B); constants ACCEPT (OpenAI C, item 3) | +| (I20) witness determinant | 223 | (6.9) | Lemma D1 on `(e_x, v̂)`. | lift ACCEPT (OpenAI C, item 3) | +| (I21)–(I22) combined product, axis bound | 230, 236 | (6.10) and the sentence after it | `K^{3d}`; on the axis Lemma D2 with `e_x`. | lift ACCEPT (OpenAI C, item 3; axis-safe reading written into §6.4) | +| (I23)–(I26) small axial strip | 245, 258, 264, 270 | §6.5 | Prefactor `s^{-5(d+1)}`, moment `s^{-30d}`, strip volume `O(s^d) ≤ O(s^2)`. | lift ACCEPT (OpenAI C, item 4) | +| (I27)–(I30) transverse floor, density, moment | 279, 290, 297, 301 | (6.11), (6.12), (6.13) | `BB^T ≥ diag(|v|^4/4, (|v|^2/2) I_m, |v|^6/144)` by Lemma D3; `det ≥ c|v|^{2d+8}`; `σ_min(B) ≥ c|v|^3`; prefactor `|v|^{-(d+4)}`; moment `|v|^{-18d}`. | Lemma D3 ACCEPT; floor use ACCEPT (OpenAI C, item 5) | +| (I31)–(I32) shell ledger | 311, 319 | (6.14), (6.15) | `s^{-(d+2)}` in place of `s^{-4}`; `r` powers `-2 + 2 + 3 = 3`, `s` powers `-(d+4) + 2 + d = -2`. | ledger arithmetic ACCEPT (Slice B); count ACCEPT (OpenAI C, item 6) | +| (I33) marked Kac–Rice with height disintegration | 334 | §6.8 | Same framework; `(grad f(X), f(X))` nondegenerate on the closed shell by (6.1). | lift ACCEPT (OpenAI C, item 7) | | (I34) dyadic sum | 347 | §6.8 | Unchanged. | lift ACCEPT (Slice B) | ## D. What "pending" means here -After OpenAI review 5357858391 the pending rows are exactly those of table C. Every pending row is a `d`-dimensional instance of a planar step whose planar version now carries a nonauthor +After OpenAI reviews 5357858391 (tables A, B) and 5357882570 (table C) no row of this crosswalk is pending; the +verdict columns record the item of the review that covers each row. Before those reviews, every pending row is a `d`-dimensional instance of a planar step whose planar version now carries a nonauthor ACCEPT (xAI 5894512272 for the pin ball; `reviews/d5_collar_count_20260928/` for the collar; `reviews/d5_i5_planar_f_20260928/` for the shells), with the change listed in the fourth column. A reader can therefore check each row by (i) confirming the planar step at the cited line, (ii) confirming that the fourth column is the complete list of changes, and (iii) confirming the exponent arithmetic in `RESULTS.json` (groups `L`, `W`) where it applies. -The two reading clarifications of review 5357858391 are written into `PROOF.md`: the unscaling step of §5.2 is the +The three clarifications of reviews 5357858391 and 5357882570 are written into `PROOF.md`: the unscaling step of §5.2 is the congruence and the Schur variational identity, not an eigenvalue-monotonicity claim under entrywise scaling; and the -collar constants depend on the fixed `d`, `R`, `eta` and the mark compacts (§5.7), with nothing uniform as `d` grows. +collar constants depend on the fixed `d`, `R`, `eta` and the mark compacts (§5.7), with nothing uniform as `d` grows; +and the axis bound of §6.4 is stated as the axis-safe endpoint-short-column/Hadamard bound `W_r |det H_X| / Z_r <= C K^(3d)` +valid throughout `|v| <= s^(1/8)`, which is what §6.5 uses. diff --git a/frontiers/d5_dimension_lift_20260929/PROOF.md b/frontiers/d5_dimension_lift_20260929/PROOF.md index 47553b84e..9d82c707f 100644 --- a/frontiers/d5_dimension_lift_20260929/PROOF.md +++ b/frontiers/d5_dimension_lift_20260929/PROOF.md @@ -521,11 +521,11 @@ Combining (6.8), (6.9), dividing once by [LP] (5.5) and using `r^2/s <= r`, W_r |det H_X| / Z_r <= C K^(3d) s^2 (r + s^2)^2 |v|^(-5). (6.10) -On the axis, retain only the two endpoint short columns (Lemma D2 with `e_x`): `W_r |det H_X| <= C r^2 K^(3d)`, which cancels the normalizer with no division by `v`. +**Axis-safe bound, valid throughout the strip `|v| <= s^(1/8)`, including `v = 0`.** The two endpoint short columns `H_M e_x`, `H_S e_x`, of size at most `Lr/2` by [LP] (5.3), do not involve the witness position, so Lemma D2 (Hadamard with `e_x`) gives `|det H_M|, |det H_S| <= C r K^(d-1)` for every `X`; with the trivial `|det H_X| <= K^d`, `W_r |det H_X| <= C r^2 K^(3d)` and, dividing once by [LP] (5.5), `W_r |det H_X| / Z_r <= C K^(3d)` on the whole strip, with no division by `|v|`. A bound stated only at `v = 0` would not control nonzero `v`; it is this uniform bound that §6.5 uses. ### 6.5 Small axial strip ([IW] §6) -On `A` and `|v| <= v_0`, `|u|` is bounded below and `d_e >= c > 0`; the first line of (6.3) gives `|E_(Q_r)[f_x(X)/s^2]| >= c_0` and `Var <= C(|v|^2 + s^2)`; the one-coordinate Mahalanobis bound applies to the full `(d+1)`-dimensional exponent. On `|v| <= s^(1/8)`, (6.1) gives the joint density bound `C s^(-5(d+1)) exp[-c s^(-1/4)]`, regression on `Y_X = (grad f(X), f(X))` with `||Sigma_X^(-1)|| <= C s^(-10)` gives `E[K^(3d) | grad f(X) = 0, f(X) = y] <= C s^(-30d)`, and with the axis bound of §6.4 and [LP] (5.5) the intensity per unit volume and height is bounded by `C s^(-N) exp[-c s^(-1/4)] <= C`. The strip has volume `O(s^d) <= O(s^2)` and the window length is `k r^3`, so it contributes at most `C r^3 s^2` to the shell count. +On `A` and `|v| <= v_0`, `|u|` is bounded below and `d_e >= c > 0`; the first line of (6.3) gives `|E_(Q_r)[f_x(X)/s^2]| >= c_0` and `Var <= C(|v|^2 + s^2)`; the one-coordinate Mahalanobis bound applies to the full `(d+1)`-dimensional exponent. On `|v| <= s^(1/8)`, (6.1) gives the joint density bound `C s^(-5(d+1)) exp[-c s^(-1/4)]`, regression on `Y_X = (grad f(X), f(X))` with `||Sigma_X^(-1)|| <= C s^(-10)` gives `E[K^(3d) | grad f(X) = 0, f(X) = y] <= C s^(-30d)`, and with the axis-safe bound of §6.4 (`W_r |det H_X| / Z_r <= C K^(3d)` throughout the strip) the intensity per unit volume and height is bounded by `C s^(-N) exp[-c s^(-1/4)] <= C`. The strip has volume `O(s^d) <= O(s^2)` and the window length is `k r^3`, so it contributes at most `C r^3 s^2` to the shell count. ### 6.6 Transverse region: `s^(1/8) <= |v| <= 2` ([IW] §7) diff --git a/frontiers/d5_dimension_lift_20260929/README.md b/frontiers/d5_dimension_lift_20260929/README.md index fb861534b..3b1001c75 100644 --- a/frontiers/d5_dimension_lift_20260929/README.md +++ b/frontiers/d5_dimension_lift_20260929/README.md @@ -47,9 +47,30 @@ Nine groups of exact checks (`X G R RO EU TB N L W`): exterior-power inequality the place where the `d`-dimensional argument is written, and the complete list of changes. Tables A and B (pin ball, collar) carry the OpenAI nonauthor ACCEPT 5357858391 at `c709854` (Theorems P_d, C_d discharged at that source; source-exposed, xAI planar record as the independent base). Table C (shells; Theorem I_d and hence G_d, - F_d, M_d) is the one remaining pending slice: the height-marked shell covariance and row operation (6.1)–(6.4), - Euler suppression (6.5)–(6.6), the transverse determinant floor (6.11)–(6.13) and the `s^(-2)` shell ledger - (6.14)–(6.15). + F_d, M_d) carries the follow-up OpenAI nonauthor ACCEPT 5357882570 at the same binding. With both, no row of the + crosswalk is pending: the continuum replacement under P_d, C_d, I_d and G_d has a complete non-Claude read at + that source, and the reviewer records no remaining analytic gap under G_d there. + +## Landing note (29 September 2026, after the OpenAI continuum reviews) + +Reviews 5357858391 (crosswalk A+B) and 5357882570 (crosswalk C), both bound to `c709854`, accept every held continuum +row at fixed `d`, fixed torus, compact marks and small `r`, subject to the identities and rank claims that the xAI +Slice A/B records accepted. Both are source-exposed (the reviewer authored the planar [PP], [CP], [IW] inputs); the xAI +planar continuum record 5894512272 is the independent base verdict, and xAI's finite-algebra verdicts are credited +separately. Three wording clarifications from those reviews are written into `PROOF.md` after `c709854`, and are the +only changes to its bytes since that binding: + +1. §5.2: the unscaling step is the congruence together with the Schur variational identity, not eigenvalue + monotonicity under an arbitrary entrywise scaling; the floor (5.1) is unchanged. +2. §5.7: the collar constants depend on the fixed `d`, `R`, `eta`, `L`, `B` and the mark compacts; nothing is uniform + as `d` grows. +3. §6.4–§6.5: the "axis bound" is the axis-safe endpoint-short-column/Hadamard bound `W_r |det H_X| / Z_r <= C K^(3d)`, + valid throughout the strip `|v| <= s^(1/8)` including `v = 0`; a statement at `v = 0` alone would not control + nonzero `v`. + +No statement, ledger, script or result changed. The old HOLD records (xAI Slice A/B counts; #111 planar (P2) before +5894512272) are retained above and in `CONTINUUM_CROSSWALK.md` as history. Scientific effect NONE: this packet still +changes no STATUS, PROOF_INDEX, GRAPH, catalog or numerical carrier; integration is a separate source-bound step. ## What this does not do diff --git a/frontiers/d5_dimension_lift_20260929/SOURCE_FILES.json b/frontiers/d5_dimension_lift_20260929/SOURCE_FILES.json index 62ad1dda2..060f5f43b 100644 --- a/frontiers/d5_dimension_lift_20260929/SOURCE_FILES.json +++ b/frontiers/d5_dimension_lift_20260929/SOURCE_FILES.json @@ -5,21 +5,21 @@ "files": [ { "path": "CONTINUUM_CROSSWALK.md", - "bytes": 11778, - "sha256": "a0e85044ab9a35803251c5a31ea3f48af3618ca885a68c58d48a48bbcded0a42", - "git_blob": "808524f5b402cfa6bdc122afb39a1e0c6088cc39" + "bytes": 12620, + "sha256": "bdb83c28ef77041ae8d5903b1e46ec96b8046660a07be439bcd60cac02f8c7dc", + "git_blob": "45e4324ff262f6dba1880431a2cdfe25c231a9e2" }, { "path": "PROOF.md", - "bytes": 53252, - "sha256": "3da173dd356ae78776e0cde3d1e9e89beb3b8a6e3767df58a3a0f060194ed0b4", - "git_blob": "47553b84e53c0cb0c0a4a1cd5e352a585fe2aee2" + "bytes": 53727, + "sha256": "6fb94b247e8e45bca9dc02f46670ac6029fb54e0ef906001efe48fe908549b80", + "git_blob": "9d82c707fdb17d3072a8930f26dabedf59e456fc" }, { "path": "README.md", - "bytes": 5924, - "sha256": "75a7cfaab76e7918e0749ae6e5068adaea0856bdcbbc20c66de3586dd8da5894", - "git_blob": "fb861534b300ba00f430066fdfd1acb5256ab156" + "bytes": 7620, + "sha256": "8cf417db179ac66fe44018d42d16bc055355c9d075349ed8ac9b3dd72fd4859f", + "git_blob": "3b1001c750a9d2698644dbdfb86ce290a921755e" }, { "path": "RECONNAISSANCE.md", @@ -35,9 +35,9 @@ }, { "path": "SOURCE_MAP.json", - "bytes": 5411, - "sha256": "64851314e280576a2bf3ac81abb6731b4eb549213ae63aaf8b13c60b8ff859f8", - "git_blob": "2ab8ac1eb7d61970e72ccea2babfa3fb9e41ae6d" + "bytes": 5908, + "sha256": "7e343409eb3e23dc0ed1a37d7fc44b84e259079fd88a2ebefab57aecd23b5ef2", + "git_blob": "fc37e51a1956b94f56beaa228015e3a6414eaf12" }, { "path": "lift_exact_check.py", diff --git a/frontiers/d5_dimension_lift_20260929/SOURCE_MAP.json b/frontiers/d5_dimension_lift_20260929/SOURCE_MAP.json index 2ab8ac1eb..fc37e51a1 100644 --- a/frontiers/d5_dimension_lift_20260929/SOURCE_MAP.json +++ b/frontiers/d5_dimension_lift_20260929/SOURCE_MAP.json @@ -80,9 +80,10 @@ "Math-#106 A1-A4 (LP sections 2-5)", "reviews/d5_punctured_pin_continuum_claude_20260929/REVIEW.md (committed record of the Math-#105 comment 5872932723 analytic review of planar PP: ACCEPT, existential, no defect) and reviews/d5_collar_count_20260928 (planar PP and CP)", "reviews/d5_intermediate_window_claude_20260928 and reviews/d5_i5_planar_f_20260928 (planar IW)", - "Math-#141 review 5357858391 (OpenAI nonauthor, bound to c709854): ACCEPT of the d-dimensional continuum rows of CONTINUUM_CROSSWALK.md tables A and B (Theorems P_d, C_d discharged at that source; source-exposed, xAI planar record 5894512272 as the independent base); table C (Theorem I_d, hence G_d, F_d, M_d) not covered; its two reading clarifications are written into PROOF.md \u00a75.2 and \u00a75.7" + "Math-#141 review 5357858391 (OpenAI nonauthor, bound to c709854): ACCEPT of the d-dimensional continuum rows of CONTINUUM_CROSSWALK.md tables A and B (Theorems P_d, C_d discharged at that source; source-exposed, xAI planar record 5894512272 as the independent base); table C (Theorem I_d, hence G_d, F_d, M_d) not covered; its two reading clarifications are written into PROOF.md \u00a75.2 and \u00a75.7", + "Math-#141 review 5357882570 (OpenAI nonauthor, bound to c709854): ACCEPT of the d-dimensional continuum rows of CONTINUUM_CROSSWALK.md table C and of the analytic G_d composition at that source (Theorems I_d, G_d and Corollaries F_d, M_d discharged there; same scope; source-exposed); its wording clarification is written into PROOF.md sections 6.4-6.5" ], "nonauthor_acceptance": false, "governing_status_changed": false, - "source_commit_note": "All eight inputs re-verified byte-identical (same git blobs) on Math- main e947ade51defcec1fb75444efbe91ac7fcf43f60 on 2026-09-29; the pins above remain the exact consumed bytes." + "source_commit_note": "All eight inputs re-verified byte-identical (same git blobs) on Math- main e947ade51defcec1fb75444efbe91ac7fcf43f60 on 2026-09-29; the pins above remain the exact consumed bytes. Re-verified byte-identical on Math- main 4d062e2a976abc8800a1ae63a49a943526b6bc0d on 29 September 2026 at the restack onto current main." }