diff --git a/.github/workflows/c8-cap-failure-coefficient-dims.yml b/.github/workflows/c8-cap-failure-coefficient-dims.yml new file mode 100644 index 000000000..571abb55d --- /dev/null +++ b/.github/workflows/c8-cap-failure-coefficient-dims.yml @@ -0,0 +1,67 @@ +name: C8 cap-failure coefficient in every dimension (certified replay) + +'on': + pull_request: + paths: + - 'frontiers/c8_cap_failure_coefficient_dims_20261001/**' + - '.github/workflows/c8-cap-failure-coefficient-dims.yml' + - 'imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md' + - 'imports/lifetime_parent_20260925/MARKED_CYLINDER_CAP_PROOF.md' + - 'frontiers/spectral_cluster_closure_20260929/PROOF.md' + workflow_dispatch: + +permissions: + contents: read + +jobs: + certified-replay: + runs-on: ubuntu-latest + timeout-minutes: 20 + steps: + - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 + with: + persist-credentials: false + - uses: actions/setup-python@a26af69be951a213d495a4c3e4e4022e16d87065 + with: + python-version: '3.11.16' + - name: Verify manifest and main-resident pins, replay the certified values in both interpreter modes, reject mutants + env: + PYTHONDONTWRITEBYTECODE: '1' + run: | + set -euo pipefail + python -B -S - <<'PY' + import hashlib, json, pathlib, subprocess, sys + root = pathlib.Path('frontiers/c8_cap_failure_coefficient_dims_20261001').resolve() + manifest = json.loads((root / 'SOURCE_FILES.json').read_text())['files'] + present = sorted(p.name for p in root.iterdir()) + if present != sorted([e['path'] for e in manifest] + ['SOURCE_FILES.json']): + 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']) + pins = json.loads((root / 'SOURCE_MAP.json').read_text()) + for entry in pins['sources']: + if not entry['current_required']: + continue + data = pathlib.Path(entry['path']).read_bytes() + blob = hashlib.sha1(b'blob %d\0' % len(data) + data).hexdigest() + if len(data) != entry['bytes'] or hashlib.sha256(data).hexdigest() != entry['sha256'] or blob != entry['git_blob']: + raise ValueError('consumed source identity mismatch on this tree: ' + entry['path']) + script = str(root / 'cap_coefficient_dims.py') + for flags in (['-B', '-S'], ['-B', '-O', '-S']): + out = subprocess.run([sys.executable, *flags, script, '--check'], cwd=root, capture_output=True, timeout=600) + if out.returncode != 0: + raise RuntimeError('check failed under ' + ' '.join(flags) + ': ' + out.stdout.decode()[-400:] + out.stderr.decode()[-400:]) + print(flags, out.stdout.decode().strip()[-300:]) + for flags in (['-B', '-S'], ['-B', '-O', '-S']): + for m in ('no-y-tail', 'r3-one', 'no-bp', 'frob-omega-off'): + rc = subprocess.run([sys.executable, *flags, script, '--check', '--mutant', m], cwd=root, capture_output=True, timeout=600).returncode + if rc != 1: + raise RuntimeError('mutant ' + m + ' not rejected under ' + ' '.join(flags)) + print(json.dumps({'scientific_effect': 'NONE', 'certified_values_replayed': True, 'mutants_rejected': 8})) + PY + git diff --exit-code diff --git a/frontiers/c8_cap_failure_coefficient_dims_20261001/NOTE.md b/frontiers/c8_cap_failure_coefficient_dims_20261001/NOTE.md new file mode 100644 index 000000000..b42be5b87 --- /dev/null +++ b/frontiers/c8_cap_failure_coefficient_dims_20261001/NOTE.md @@ -0,0 +1,330 @@ +# The cap-failure coefficient in every dimension: `c_G^(d) = R_d(b) R(b) J^(d)(k)`, certified in `d = 3` + +**Object:** `CL-C8-CAP-FAILURE-COEFFICIENT-DIMS-20261001-v1`. **Author lane:** Anthropic / Claude. + +**Kind.** An author-side limit theorem (Theorem G_d, `d >= 3`) and certified enclosures of its coefficient in `d = 3` +(exact rational interval arithmetic; standard library only). + +**Scientific effect:** NONE. Catalog entry C8 (`reviews/candidates_pending_20260928/CANDIDATES.md`) stays OPEN. +- This packet supplies no `C` and no `r_*` in `d >= 3`. +- It determines the exact size of the cap-failure probability `Q^W(G_r^c)` that the proof of [LP] Theorem A bounds by + `C_cap r^3` in [LP] (7.8). +- Hence it gives a lower bound for every cap-route constant `C_cap` in `d >= 3`. It gives none for the constant of [LP] + (1.1), which bounds the smaller probability `1 - p_r` (Math-#203 v1.2, section 5 item 1). + +No STATUS, PROOF_INDEX, GRAPH or catalog edit. Same GitHub account as every lane; zero organizational-independence credit. +The author will not merge. Scope claim: Math-#203 comment 5922724441. + +**Sources** (pinned in `SOURCE_MAP.json`): +- [LP] `imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md`: + - section 1 (the model in every `d`); + - section 3 (the pins (3.1)–(3.4)); + - section 4 (the uniform moments (4.1) and the regression on the transverse Hessian (4.2)); + - section 5 (the limit (5.4) and the floor (5.5)); + - section 6 ((6.2)); + - section 7 ((7.1)–(7.4) and (7.7)). +- [CAP] `imports/lifetime_parent_20260925/MARKED_CYLINDER_CAP_PROOF.md`, section 1: the cylinder `D`, the partial-block + operator norms `M_3`, `M_4`, and condition (1). +- [SC] `frontiers/spectral_cluster_closure_20260929/PROOF.md`: the spectral change of variables and the constant `c_m` of (8). +- [G] Math-#203 at `a388580`, read-only: the planar Theorem G, the factor `R(b)`, and the certified planar `J(k)` + (`RESULTS.json`, git blob `e3a8e25a`). +- [HD] Math-#184 at `d37ff5d`, read-only: the hard-direction factor `R_d(b)`, its closed form at `b = 0`, its floating values, + and Corollary 2 (the elder-failure coefficient in dimension `d`). Used for comparison and identification only. + - Its PROOF blob `91d22fce` has OpenAI nonauthor ACCEPTs at `d29e674`: Slices A/B in review 5366497205 (Lemma 1, Lemma 2, + Theorem 1, the closed form (3)) and Slice C in review 5366261768. + - Lemma 1 below re-derives the `d = 3` contact law independently. + +## 0. Statement + +**Setting.** This is the setting of [G] section 0 in dimension `d >= 3`, with `m = d - 1` and coordinates `(x, y)` in +`R x R^m`: +- The pins are `M = (-r/2, 0)` and `S = (r/2, 0)` in the frame `R`; the law is `Q = Q_{r,b,k,R}`. +- The typed weight is `W_r = |det H_M det H_S| 1{H_M < 0, index H_S = m}`, with `Z_r = E_Q W_r` and `dQ^W = (W_r/Z_r) dQ`. +- The cylinder is `D = [-2r, 2r] x ball(0, 2r)`, and `M_j = max_{a+c=j} sup_D ||partial_x^a D_y^c f||_op`. +- The good event is `G_r = {lambda_1 > (4/(3k)) r M_3^2, r M_4 <= 3k/10}`, where `lambda_1 = lambda_min(-D_y^2 f(M))`. + +**Theorem G_d.** Fix `d >= 3`, `b`, `k > 0`, `L` and `R`. Then `Q^W(G_r^c) = c_G^(d)(b, k) r^3 + o(r^3)` as `r -> 0`, where +`c_G^(d)` is the spectral integral (3.6) below. For the reference kernel `exp(-|z|^2/2)` (equivalently `L -> infinity`): + + c_G^(d)(b, k) = R_d(b) . R(b) . J^(d)(k), + R(b) = phi_2(b) / m_(2,b), m_(2,b) = E[w^2 1{w < 0}], w ~ N(-b, 2) ([G]), + R_d(b) = N_d(b) m_(2,b) / m_(d,b), m_(d,b) = E[det(A)^2 1{A < 0}], A = -b I_m + GOE_m ([HD]), + J^(d)(k) = (216 k^3)^(-1) E[ integral_{max(a,c)}^{8 M^2} (s - a)(s - c) ds ], + a = v_1^2, c = 6k Omega_11 - v_1^2, M = max(12k, 2||v||, ||Omega||_op, ||Y||_op). + +The ingredients: +- `phi_2` is the `N(0, 2)` density. +- `N_d(b) = c_m (2 pi)^(-m(m-1)/4) integral_{0 < h_2 < ... < h_m} prod_j h_j^3 phi_2(h_j - b) prod_{i= 2.2424 x 10^7`. + - Hence the `d = 3` cap route can be nontrivial only below `r = c_G^(3)(0, 2)^(-1/3) = 3.546 x 10^-3`. + - In the plane the threshold was `5.73 x 10^-3`. + - This lower bound says nothing about the constant of [LP] (1.1) itself. +2. **The criterion against the truth.** + - [HD] Corollary 2 states that the actual `d`-dimensional elder-failure coefficient is `R_d(b) (alpha_1 + alpha_2)^(2)`, + conditional on its sources. + - Under that reading the factor `R_d(b)` cancels, and the cap criterion's overstatement of the true failure rate is the + planar one times `J^(d)/J^(2)`: + + c_G^(d) / (alpha_1 + alpha_2)^(d) = [c_G / (alpha_1 + alpha_2)]^(2) . J^(d)(k) / J^(2)(k). + + - In `d = 3` the ratio `J^(3)/J^(2)` is `1 + O(10^-4)` for `k >= 1`, from the certified enclosures. At smaller `k` it is + known from Monte Carlo only: `1.0011` at `k = 3/4` and `1.135` at `k = 1/2`. The certified `k = 3/4` enclosure is too + wide to certify `1.0011` (C208-C-01). + - At the SIDE24 gap `k = 1/6` it is `5.12 ± 0.03` (Monte Carlo): in `d = 3` the free third derivatives dominate the cap + criterion at small `k`. +3. **Where the dimension enters.** Dimension enters `c_G^(d)` in two ways: + - through the hard-direction factor `R_d(b)`, the same factor that multiplies the near cluster coefficients ([HD]); + - through the norms of the free third-derivative blocks, which matter only when they exceed the pinned `12k`. + +## 1. Lemma 1: the contact law (reference kernel) + +Given the contact jet `(f, f_x, f_xx, f_xxx, f_y, f_xy)(0) = (b, 0, 0, 12k, 0, 0)` ([LP] (3.4)): +- The transverse Hessian is `A_0 = D_y^2 f(0) = -b I + G` with `G ~ GOE_m`. +- The odd 3-jets are `f_xxy ~ N(0, 2 I)`, `f_xyy ~ GOE_m`, and `f_yyy` with independent entries of variances `6, 2, 1` + (`iii`, `iij`, `ijk`). +- All of these are mutually independent and have mean `0`. The pinned `f_xxx = 12k` has zero regression coefficient on them. + +*Proof.* +- **Covariances.** For the reference kernel, `E[partial^alpha f(0) partial^beta f(0)] = (-1)^|beta| prod_i h(alpha_i + beta_i)` + with `h(n) = (-1)^(n/2)(n-1)!!` for even `n` and `0` for odd `n`. +- **Parity.** Odd and even total orders are uncorrelated. In each coordinate, the parity classes of the transverse indices + separate the remaining covariances. +- **Example.** `Cov(f_yiyiyi, f_yi) = -3` and `Var f_yiyiyi = 15`, so the conditional variance is `15 - 9 = 6`; `Var f_yiyjyj = 3` + conditions to `3 - 1 = 2`; `Var f_y1y2y3 = 1` with no pin correlation; every conditional cross-covariance is `0`. + +`cap_coefficient_dims.py` verifies the `d = 3` instance exactly. It solves the `8 x 8` rational pin system and checks all 12 +conditional means and all 78 conditional covariances. + +For `d = 2` the law restricts to [G] section 2.2 (`v ~ N(0, 1/2)`, `Omega ~ N(0, 2)`, `Y ~ N(0, 6)`). Isotropy holds because +rotations `y -> P y` (`P in O(m)`) fix the pins and preserve the reference kernel; parity holds for every even kernel, +including `K_L`. + +**The hard-direction integral at `b = 0`.** Write `-A_0 = B`. +- **Joint density.** The ordered eigenvalues of `B` in `d = 3` have joint density + `(1/(4 sqrt(2 pi))) (lambda_2 - lambda_1) exp(-((lambda_1 - b)^2 + (lambda_2 - b)^2)/4)` on `lambda_1 < lambda_2`. This is the + `GOE_2` density times the Jacobian `|lambda_2 - lambda_1|` of `(x, y, z) -> (lambda_1, lambda_2, phi)`, which has determinant + `(cos^2 + sin^2)^2 = 1` times the gap, and `phi in [0, pi)`. +- **`m_(3,0)`.** In polar coordinates on `0 < lambda_1 < lambda_2`, + + m_(3,0) = (1/(4 sqrt(2 pi))) . integral_0^inf rho^6 e^(-rho^2/4) drho . integral_{pi/4}^{pi/2} cos^2 sin^2 (sin - cos) dtheta + = (1/(4 sqrt(2 pi))) . 120 sqrt(pi) . (7/(30 sqrt2) - 2/15) = (7 - 4 sqrt2)/2. + +- **`N_3(0)`.** `N_3(0) = sqrt(pi/2) integral_0^inf h^3 phi_2(h) dh = sqrt(pi/2) . (1/2) E|N(0, 2)|^3 = 2 sqrt2`. +- **Result.** With `m_(2,0) = 1`, `R_3(0) = 2 sqrt2 / ((7 - 4 sqrt2)/2) = (32 + 28 sqrt2)/17`, which agrees with [HD] (3). + +## 2. The `d`-dimensional weight near the soft eigenvalue + +Let `-D_y^2 f(M) = O diag(lambda_1, lambda) O^T` with `lambda = (lambda_2, ..., lambda_m)` ordered and `O in O(m)`. In the frame +`O`, write `v_1 = v . O e_1` and `Omega_11 = (O e_1)^T Omega' (O e_1)`, where +`Omega' = (D_y^2 f(S) - D_y^2 f(M))/r -> Omega`. + +The pins give, exactly, the `d`-dimensional versions of [G] (1.1): + + f_xx(M) = r^2 T - 6kr, f_xx(S) = r^2 (T + r tau) + 6kr, f_xy(M) = r v, f_xy(S) = r (r nu - v). + +**`H_M`.** By the Schur complement on `A_M = D_y^2 f(M)`, with `lambda_1 = r u`, + + det H_M = det(A_M) (f_xx(M) - f_xy(M)^T A_M^(-1) f_xy(M)) + = (-1)^m r u prod_j lambda_j . (-r c1 + r v_1^2/u + r^2 sum_{j>=2} v_j^2/lambda_j) + = (-1)^(m+1) r^2 prod_j lambda_j (c1 u - v_1^2 - r u sum_{j>=2} v_j^2/lambda_j), c1 = 6k - rT. + +**`H_S`.** With `A_S = A_M + r Omega'`: +- The soft eigenvalue of `A_S` is `-r(u - Omega'_11) + O(r^2/lambda_2)`. +- `det(A_S) = (-1)^m r (u - Omega'_11) prod_j lambda_j (1 + O(r/lambda_2))`. +- `det H_S = (-1)^m r^2 prod_j lambda_j (c2 (u - Omega'_11) + (r nu - v)_1^2) + O(r^3)`, with `c2 = 6k + rT + r^2 tau`. + +**Limit.** On the typed support, therefore, + + W_r / r^4 -> prod_{j>=2} lambda_j^2 . (6ku - v_1^2)(6k(u - Omega_11) + v_1^2) (2.1) + +pointwise along the coupling. In `s = 6ku` this is `prod_j lambda_j^2 (s - a)(s - c)`, the planar form [G] (1.2) times +`prod_j lambda_j^2`. + +## 3. Proof of Theorem G_d + +Steps 1–3 follow [G] section 2 line by line. The new ingredients are the regression on the whole transverse Hessian +([LP] (4.2)), the spectral change of variables ([SC] (8)), and the near-corank strip, which [LP] section 7 controls. + +**3.1 Regression on the transverse Hessian.** +- By [LP] (4.2), `f = mu_r + B_r . (A_r - E A_r) + g_r`, where `A_r = D_y^2 f(M)` and `g_r` is independent of `A_r`. +- Under the regression coupling ([G] 2.1), `g_r` and the coefficients converge in every `C^q` norm. +- The Gaussian density `p_{A,r}` of `A_r` on `Sym_m` converges with its derivatives to `p_{A,0}`, the law of `A_0` in + Lemma 1 ([LP] section 3). +- All moments are uniform ([LP] (4.1)). + +**3.2 Negligible parts.** +- **(i) The fourth-derivative branch.** `Q^W(r M_4 > 3k/10) = O(r^p)` for every `p`: Markov on + `E_Q[(W_r/r^2) M_4^p]` with the floor (5.5), as [LP] (7.7). +- **(ii) The depth branch with `lambda_1 > sqrt r`.** It forces `M_3 >= (3k/4)^(1/2) r^(-1/4)`, which has mass `O(r^(p/4))`. +- **(iii) The near-corank strip** `{lambda_1 <= (4/(3k)) r M_3^2, lambda_2 <= eta}`. + - Use [LP] (6.2), the inclusion (7.1) `lambda_1 <= D r U^2`, the eigenvalue-measure bound (7.2) and the integration (7.3). + - These give the integral (7.4) with `lambda_2` restricted to `[0, eta]`. + - Since `m >= 2`, the integrand of (7.4) is bounded by an integrable function of `(J_r, lambda_3, ..., lambda_m)`, uniformly + for `lambda_2` in `[0, 1]`. The `lambda_2`-integral over `[0, eta]` is therefore at most `C eta`. + - Dividing by `Z_r >= z_* r^2` gives a contribution of at most `C eta r^3`. + +**3.3 Spectral coordinates.** On `{lambda_1 <= sqrt r, lambda_2 >= eta}`, use [SC] (8) with normalized Haar `dO` and +`lambda_1 = r u`: + + E_Q[W_r 1{depth failure}] = r c_m integral_0^{r^(-1/2)} du integral_{lambda_2 >= eta} dlambda integral dO + p_{A,r}(-O diag(r u, lambda) O^T) prod_{j>=2}(lambda_j - r u) prod_{2<=i M = max(12k, 2||v||, ||Omega||_op, ||Y||_op)`. The block norms are continuous, the cylinder shrinks + to `0`, and the third partials converge uniformly; at the limit `partial_x^3 f(0) = 12k`, `partial_x^2 D_y f(0) = -2v`, + `partial_x D_y^2 f(0) = Omega` and `D_y^3 f(0) = Y`. +- **Indicator.** `1{u <= (4/(3k)) M_3^2} -> 1{s <= 8M^2}` off a null set. +- **Remaining factors.** `p_{A,r} -> p_{A,0}` and `prod (lambda_j - r u) -> prod lambda_j`. + +**3.5 Domination.** +- **Weight.** By [LP] (6.2) and (7.1), `W_r/r^4 <= C U^(2m) u (u + E U)` on `u <= D U^2`, with `U = J_r + Lambda`. +- **Eigenvalue measure.** (7.2) bounds it by `C exp(-c sum lambda_j^2) Lambda^(m(m-1)/2)`. +- **Integrability.** `J_r` is independent of `A_r` with uniform moments. The majorant of (3.1) is therefore integrable + uniformly in `r` (this is (7.4)), and dominated convergence applies in `(u, lambda, O)` and on the probability space. + +**3.6 Conclusion.** `Z_r/r^2 -> z_0^(d) = (6k)^2 E[det(A_0)^2 1{A_0 < 0}]` ([LP] (5.4)). Letting `r -> 0` and then `eta -> 0` +(by 3.2(iii) and monotone convergence), + + c_G^(d) = (c_m / z_0^(d)) integral dlambda integral dO p_{A,0}(-O diag(0, lambda) O^T) prod_j lambda_j^3 prod_{i a` (`det H_M` sign) and `s > c` (index of `H_S`), and `s <= 8M^2` is the depth failure. + +**3.7 The reference kernel.** +- **Independence and invariance.** By Lemma 1, `(v, Omega, Y)` is independent of `A_0`, and its law is invariant under + `y -> P y`. The inner expectation in (3.6) therefore equals `E[integral ...]/(6k)`, independent of `(lambda, O)`. +- **Density on the boundary.** The density of `-A_0 = b I + G` at `diag(0, lambda)` is + `(2 pi)^(-m(m-1)/4) phi_2(b) prod_j phi_2(lambda_j - b)`, since the `GOE_m` normalization is `(4 pi)^(-m/2)(2 pi)^(-m(m-1)/4)`. +- **Hard integral.** Hence the hard integral of (3.6) is `phi_2(b) N_d(b)`. +- **Assembly.** `c_G^(d) = phi_2(b) N_d(b) E[...]/(6k . 36 k^2 m_(d,b)) = R(b) R_d(b) J^(d)(k)`. QED. + +For the torus kernel `K_L` in a frame `R`, (3.6) holds with the exact torus laws. Parity still gives independence from +`A_0`, but the inner expectation can depend on `O`. The deviation from the reference value is of order `L^q e^(-L^2/2)` and is +**not enclosed here**. Every number in this packet is a reference-kernel value. + +## 4. Certified `J^(3)(k)` and `c_G^(3)(0, k)` + +Throughout, `P(s) = integral_0^s (x - a)(x - c) dx`, so `216 k^3 J^(d)(k) = E[P(8 M_d^2) - P(m_0)]` with `m_0 = max(a, c)`. Let +`t = 12k`. + +**(a) Monotone coupling.** Realize `d = 2` and `d = 3` on one space, the planar variables being `(v_1, Omega_11, Y_111)`. +- **Domination.** `M_3 >= M_2`, since each block norm dominates its `(1,1)` component. +- **Monotonicity.** `dP(8M^2)/dM = 16 M (8M^2 - a)(8M^2 - c) >= 0` for `8M^2 >= m_0`. Hence `J^(2)(k) <= J^(3)(k)`. +- **The difference.** `F(M_3) - F(M_2) = integral_{8M_2^2}^{8M_3^2} (x - a)(x - c) dx` vanishes unless `X_3 > t`, where + `X_3 = max(2||v||, ||Omega||_op, ||Y||_op)`. It is at most `[(8 Xbar^2)^3/3 + Q (8 Xbar^2)^2 + Q^2 8 Xbar^2] 1{Xbar > t}`, with: + - `Q = 2 v_1^2 + 6k|Omega_11|`, which dominates `a`, `|c|` and `m_0`; + - `Xbar = max(Z_v, Z_Om, Z_Y)`, built from: + - `Z_v = 2||v||`, with `Z_v^2 ~ 2 chi^2_2`; + - `Z_Om = ||Omega||_F >= ||Omega||_op`, with `Z_Om^2 ~ 2 chi^2_3`; + - `Z_Y = (Y_111^2 + 3 Y_112^2 + 3 Y_122^2 + Y_222^2)^(1/2) >= ||Y||_op`, with `Z_Y^2 ~ 6 chi^2_4`. + + The last inequality is Cauchy–Schwarz with the weights `binom(3, j)`. +- **Tail bound.** `Xbar^p 1{Xbar > t} <= sum Z_i^p 1{Z_i > t}`. Each `E[Q^j Z_i^p 1{Z_i > t}]` is expanded binomially and + evaluated in closed form: + - incomplete gamma functions, `e^(-x) x^j` sums for even degrees of freedom and `erfc` plus such sums for `chi^2_3`; + - the Gaussian absolute moments of `v_1` and `Omega_11`. +- **Enclosure.** Thus `J^(3)(k) in [J^(2)_lo(k), J^(2)_hi(k) + T_hi^(3)(k)/(216 k^3)]`. This uses [G]'s certified planar + enclosure, which is the only consumed numerical input. + +**(b) Self-contained bracket.** Independently of [G]: + + 216 k^3 J^(d)(k) = 512 t^6/3 - 6 t^2 - E[P(m_0)] + T^(d) + (E[a + c] = 0, E[ac] = -E v_1^4 = -3/4), + |E[P(m_0)]| <= 2 E[Q^3], + -2 E[Q^6]/(8t^2)^3 <= T^(d) <= T_hi^(d). + +The `d = 2` bracket contains [G]'s certified `J(k)` at every grid `k`; `--check` requires this. +- At `k = 2` the self-contained bracket has relative width `1.1e-6`. +- The coupling enclosure (a) has relative width `1e-13` at `k = 2`, `6e-11` at `3/2`, `1.1e-4` at `1` and `1.6%` at `3/4`. +- At `k = 1/2` the `chi^2` tails are not small (`12k = 6`), and only the lower bound and the Monte Carlo value are informative. + +**(c) Values.** `c_G^(3)(0, k) = R_3(0) R(0) J^(3)(k)` with the exact `R_3(0)` and `R(0)` of section 1; the table is in +section 0. Floating `R_3(b) R(b)` from the closed-form inner integral and a Simpson `rho`-quadrature (`RESULTS.json`, +`controls`): + +| `b` | `0` | `1/4` | `1/2` | `3/4` | `1` | +|---|---|---|---|---|---| +| `R_3(b)` | `4.2116458674` | `4.3013489393` | `4.3990369319` | `4.5051585717` | `4.6201205312` | +| `R_3(b) R(b)` | `1.188083364` | `0.908553106` | `0.685390319` | `0.509615120` | `0.373149892` | + +`R_3(0)` and `R_3(1)` agree with [HD] to `1e-10`. `R_3(b) R(b)` decreases on the grid, so the band corner `b = 0` carries +the largest value among the grid points. Monotonicity in `b` is not proved here. + +## 5. Monte Carlo controls (floating; not part of the certificate) + +`200000` samples per seed, two seeds, the laws of Lemma 1 (`RESULTS.json`, `controls.mc`): + +| `k` | `J^(2)/(2359296 k^3)` | `J^(3)/(2359296 k^3)` | ratio `J^(3)/J^(2)` | +|---|---|---|---| +| `1/6` | `52.67 ± 0.51` (certified [G]: `53.712`) | `275.02 ± 1.44` | `5.12 ± 0.03` | +| `1/2` | `1.0220 ± 0.0006` (certified: `1.0231677`) | `1.1617 ± 0.0018` | `1.135 ± 0.002` | +| `3/4` | `1.00010 ± 0.00003` (certified: `1.0001272`) | `1.00122 ± 0.00007` | `1.0011 ± 0.0001` | + +- **Agreement with the certificate.** The `d = 3` values at `k = 3/4` lie inside the certified enclosure (`--check` tests + this). At `k = 1/2` the Monte Carlo value lies inside the certified bracket. +- **Planar values.** These fall within `2.1` standard errors of [G]'s certified values. A further planar run at `k = 1/2` + (`4 x 500000` samples, fresh seeds `101`–`404`) gives `1.02363 ± 0.00031`, `1.5` standard errors above the certified + `1.0231677`. No bias is apparent. +- **`||Y||_op`.** It is computed by a 64-point scan of the circle followed by golden-section refinement. + +## 6. What this does not do + +- **Sources.** Not a proof or review of [LP], [CAP], [SC], [G] or [HD]. Their cited statements are consumed as such, and the + enclosure 4(a) uses [G]'s certified planar `J(k)`. +- **Constants.** No upper bound `C` or `C_cap` and no `r_*` in `d >= 3` (C8 stays OPEN), no lower bound for the constant of + [LP] (1.1), and no rate in the `o(r^3)`. +- **Kernel.** Reference kernel only: the finite-torus deviation is not enclosed. +- **Values.** Certified values in `d = 3` only; for `d >= 4` the formula is stated and not evaluated. `R_3(b)` for `b != 0` + is floating, as are the Monte Carlo values. +- **Comparison.** The comparison of Corollary item 2 inherits [HD] Corollary 2's conditional status. + +## 7. Verification and provenance + +- `python3 -B -S cap_coefficient_dims.py --check` (also `-B -O -S`) checks, in about one second: + - Lemma 1 exactly; + - the closed form of `m_(3,0)` against its polar evaluation; + - every certified enclosure against `RESULTS.json` (exact decimal strings), and the containment of [G]'s planar `J(k)` in the + `d = 2` bracket; + - the recorded `d = 3` Monte Carlo at `k = 3/4` against the enclosure. +- Mutants exit 1: + - `no-y-tail` drops the `Y`-block tail; + - `r3-one` sets `R_3 = 1`; + - `no-bp` drops `E[P(m_0)]`; + - `frob-omega-off` replaces the Frobenius `chi^2_3` by `chi^2_1`. +- `--controls --procs N` recomputes the floating controls (a few minutes). Without `--controls`, the script regenerates the + certified part and keeps the recorded controls. +- Workflow `.github/workflows/c8-cap-failure-coefficient-dims.yml` checks the manifest, the main-resident pins ([LP], [CAP], + [SC]), both modes, the four mutants, and a clean tree. + +Author lane Anthropic / Claude, 1 October 2026. Scientific effect NONE. The author will not merge. diff --git a/frontiers/c8_cap_failure_coefficient_dims_20261001/README.md b/frontiers/c8_cap_failure_coefficient_dims_20261001/README.md new file mode 100644 index 000000000..1d27defb1 --- /dev/null +++ b/frontiers/c8_cap_failure_coefficient_dims_20261001/README.md @@ -0,0 +1,41 @@ +# The cap-failure coefficient in every dimension (C8: what any cap-route constant must exceed in `d >= 3`) + +**Object:** `CL-C8-CAP-FAILURE-COEFFICIENT-DIMS-20261001-v1`. **Author lane:** Anthropic / Claude. **Kind:** author-side limit +theorem (Theorem G_d, `d >= 3`) with certified `d = 3` coefficients (exact rational interval arithmetic, standard library +only). **Scientific effect:** NONE: no register, catalog, GRAPH or STATUS change; C8 stays OPEN; no `C` or `r_*` is supplied. + +**Statement.** For the `d`-dimensional [LP] law and the [CAP] (1) good event with partial-block operator norms, + + Q^W(G_r^c) = c_G^(d)(b, k) r^3 + o(r^3), c_G^(d) = R_d(b) . R(b) . J^(d)(k) (reference kernel). + +- `R_d(b)` is the hard-direction factor of Math-#184. +- `R(b)` is the planar factor of Math-#203. +- `J^(d)(k)` is the planar `J` with `M = max(12k, 2||v||, ||Omega||_op, ||Y||_op)` taken over the full transverse blocks. + Here `v ~ N(0, I/2)`, `Omega ~ GOE`, and `Y` is the isotropic Gaussian cubic of Lemma 1, all independent. + +**In `d = 3`.** +- **Certified values.** + - `R_3(0) = (32 + 28 sqrt2)/17`. + - `J^(3)(k)` is enclosed tightly at `k = 1, 3/2, 2`, by monotone coupling with Math-#203's certified planar `J` plus + `chi^2` tails. + - `c_G^(3)(0, 2) in [22424320.655069, 22424320.655072]`, which equals `R_3(0) c_G(0, 2)` to `1e-13`. +- **Consequences.** + - Every `d = 3` cap-route constant at the band corner exceeds `2.24 x 10^7`. + - The `d = 3` cap route is informative only below `r = 3.55 x 10^-3`. + - The cap criterion's overstatement of the true `d`-dimensional failure is the planar one times `J^(d)/J^(2)`: + `1 + O(1e-4)` for `k >= 1` (certified); Monte Carlo `1.0011` at `k = 3/4`, `1.135` at `k = 1/2` and `5.12` at the SIDE24 + gap `k = 1/6`. + +**Files.** +- `NOTE.md`: statement, Lemma 1 (the `d = 3` contact law, exact), the `d`-dimensional weight, the proof of Theorem G_d + (spectral coordinates, the near-corank strip from [LP] (7.4), dominated convergence), the certified `J^(3)` method, + values, controls, and non-claims. +- `cap_coefficient_dims.py`: + - `--check` re-verifies Lemma 1 and every certified enclosure against `RESULTS.json` in about one second; + - `--mutant {no-y-tail, r3-one, no-bp, frob-omega-off}` must exit 1; + - `--controls` recomputes the floating Monte Carlo and quadrature controls. +- `RESULTS.json`, `SOURCE_MAP.json` (pins [LP], [CAP], [SC] on `main`; read-only references to Math-#203 and Math-#184), + `SOURCE_FILES.json`. +- Workflow `.github/workflows/c8-cap-failure-coefficient-dims.yml`. + +Same GitHub account as every other lane; zero organizational-independence credit. The author will not merge. diff --git a/frontiers/c8_cap_failure_coefficient_dims_20261001/RESULTS.json b/frontiers/c8_cap_failure_coefficient_dims_20261001/RESULTS.json new file mode 100644 index 000000000..e9fd6f377 --- /dev/null +++ b/frontiers/c8_cap_failure_coefficient_dims_20261001/RESULTS.json @@ -0,0 +1,365 @@ +{ + "certified": { + "G_containment": { + "1": true, + "1/2": true, + "2": true, + "3/2": true, + "3/4": true + }, + "J": { + "2": { + "1": { + "B_P": "2533.704151", + "T_hi": "641.782525", + "T_lo": "0.011038393522", + "bracket": [ + "2359280.269837", + "2359306.701328" + ] + }, + "1/2": { + "B_P": "442.662376", + "T_hi": "308486.267651", + "T_lo": "0.023305874468", + "bracket": [ + "294887.604234", + "306345.812224" + ] + }, + "2": { + "B_P": "17600.443507", + "T_hi": "0.000001", + "T_lo": "0.008713913945", + "bracket": [ + "18874355.814553", + "18874376.185442" + ] + }, + "3/2": { + "B_P": "7765.504728", + "T_hi": "0.001317", + "T_lo": "0.009350841600", + "bracket": [ + "7962610.681050", + "7962631.985605" + ] + }, + "3/4": { + "B_P": "1186.987126", + "T_hi": "34445.526333", + "T_lo": "0.013554133876", + "bracket": [ + "995309.640596", + "995713.695621" + ] + } + }, + "3": { + "1": { + "B_P": "2533.704151", + "T_hi": "54788.295033", + "T_lo": "0.011038393522", + "bracket": [ + "2359280.269837", + "2359557.379626" + ] + }, + "1/2": { + "B_P": "442.662376", + "T_hi": "5937285.970252", + "T_lo": "0.023305874468", + "bracket": [ + "294887.604234", + "514819.875283" + ] + }, + "2": { + "B_P": "17600.443507", + "T_hi": "0.000001", + "T_lo": "0.008713913945", + "bracket": [ + "18874355.814553", + "18874376.185442" + ] + }, + "3/2": { + "B_P": "7765.504728", + "T_hi": "0.347723", + "T_lo": "0.009350841600", + "bracket": [ + "7962610.681050", + "7962631.986081" + ] + }, + "3/4": { + "B_P": "1186.987126", + "T_hi": "1427204.546638", + "T_lo": "0.013554133876", + "bracket": [ + "995309.640596", + "1010997.745227" + ] + } + } + }, + "J3_from_G": { + "1": [ + "2359292.9611053702", + "2359546.6106262951" + ], + "1/2": [ + "301744.4364470240", + "521643.9420460952" + ], + "2": [ + "18874366.3403946310", + "18874366.3403964821" + ], + "3/2": [ + "7962621.6645357430", + "7962621.6650148570" + ], + "3/4": [ + "995454.6123240484", + "1011116.6655663147" + ] + }, + "R3_0": [ + "4.21164586743803890390", + "4.21164586743803890391" + ], + "R_0": [ + "0.28209479177387814347", + "0.28209479177387814348" + ], + "cG3_0": { + "1": [ + "2803036.717892", + "2803338.074669" + ], + "1/2": [ + "358497.545122", + "619756.489477" + ], + "2": [ + "22424320.655069", + "22424320.655072" + ], + "3/2": [ + "9460258.333462", + "9460258.334033" + ], + "3/4": [ + "1182683.064519", + "1201290.889423" + ] + }, + "contact_law_d3": "verified exactly (rational covariances)", + "m3_0": [ + "0.67157287525380990239", + "0.67157287525380990240" + ] + }, + "controls": { + "mc": [ + { + "J": 573483.2003515988, + "J_over_2359296k3": 52.50395511031484, + "d": 2, + "k": "1/6", + "n": 200000, + "se": 7655.963639568235, + "seed": 1 + }, + { + "J": 577021.0354302058, + "J_over_2359296k3": 52.827853585529105, + "d": 2, + "k": "1/6", + "n": 200000, + "se": 8090.596268903591, + "seed": 2 + }, + { + "J": 301353.7609147216, + "J_over_2359296k3": 1.0218429935530653, + "d": 2, + "k": "1/2", + "n": 200000, + "se": 228.2453051785978, + "seed": 1 + }, + { + "J": 301438.860536006, + "J_over_2359296k3": 1.0221315529242825, + "d": 2, + "k": "1/2", + "n": 200000, + "se": 247.23752542436708, + "seed": 2 + }, + { + "J": 995456.2645992065, + "J_over_2359296k3": 1.000128866664262, + "d": 2, + "k": "3/4", + "n": 200000, + "se": 38.50907583701118, + "seed": 1 + }, + { + "J": 995396.4107454626, + "J_over_2359296k3": 1.000068731860716, + "d": 2, + "k": "3/4", + "n": 200000, + "se": 43.14685176807617, + "seed": 2 + }, + { + "J": 3006541.0103511857, + "J_over_2359296k3": 275.2570505082263, + "d": 3, + "k": "1/6", + "n": 200000, + "se": 22321.928794119052, + "seed": 1 + }, + { + "J": 3001350.8276723046, + "J_over_2359296k3": 274.78187509206896, + "d": 3, + "k": "1/6", + "n": 200000, + "se": 22231.401224585792, + "seed": 2 + }, + { + "J": 342633.30348615645, + "J_over_2359296k3": 1.1618154008184016, + "d": 3, + "k": "1/2", + "n": 200000, + "se": 729.4059466274549, + "seed": 1 + }, + { + "J": 342582.8134390423, + "J_over_2359296k3": 1.1616441970453637, + "d": 3, + "k": "1/2", + "n": 200000, + "se": 725.3592836399633, + "seed": 2 + }, + { + "J": 996584.9572693007, + "J_over_2359296k3": 1.0012628573387876, + "d": 3, + "k": "3/4", + "n": 200000, + "se": 106.4037998826535, + "seed": 1 + }, + { + "J": 996510.2849659664, + "J_over_2359296k3": 1.0011878345288854, + "d": 3, + "k": "3/4", + "n": 200000, + "se": 101.74021053974676, + "seed": 2 + } + ], + "mc_planar_extra": [ + { + "J": 302149.7861437234, + "J_over_2359296k3": 1.0245421893436801, + "d": 2, + "k": "1/2", + "n": 500000, + "se": 180.72432978729194, + "seed": 101 + }, + { + "J": 301827.51055317273, + "J_over_2359296k3": 1.02344940373119, + "d": 2, + "k": "1/2", + "n": 500000, + "se": 162.3447178810032, + "seed": 202 + }, + { + "J": 301655.50639425963, + "J_over_2359296k3": 1.0228661648025839, + "d": 2, + "k": "1/2", + "n": 500000, + "se": 205.78347303003764, + "seed": 303 + }, + { + "J": 301891.48424360144, + "J_over_2359296k3": 1.0236663284084793, + "d": 2, + "k": "1/2", + "n": 500000, + "se": 172.03691473332606, + "seed": 404 + } + ], + "r3r_float": [ + { + "N3": 2.8284271247461907, + "R": 0.28209479177387814, + "R3": 4.211645867383148, + "R3R": 1.1880833639847637, + "b": 0.0, + "m2": 1.0, + "m3": 0.6715728752625627 + }, + { + "N3": 3.91113167383402, + "R": 0.2112251571194215, + "R3": 4.30134893925965, + "R3R": 0.9085531055205767, + "b": 0.25, + "m2": 1.3148117449009584, + "m3": 1.195532362807149 + }, + { + "N3": 5.3225619571944245, + "R": 0.1558046293748212, + "R3": 4.3990369319364735, + "R3R": 0.6853903187865128, + "b": 0.5, + "m2": 1.700870721283295, + "m3": 2.05794812257308 + }, + { + "N3": 7.1337059058536685, + "R": 0.11311813165479301, + "R3": 4.505158571746901, + "R3R": 0.5096151204445851, + "b": 0.75, + "m2": 2.1666570937930816, + "m3": 3.43079921823 + }, + { + "N3": 9.423300548789458, + "R": 0.0807662676888845, + "R3": 4.620120531193955, + "R3R": 0.37314989157732215, + "b": 1.0, + "m2": 2.720141106187292, + "m3": 5.54806027367761 + } + ] + }, + "mutant": null, + "object": "CL-C8-CAP-FAILURE-COEFFICIENT-DIMS-20261001-v1", + "schema": 1, + "scientific_effect": "NONE" +} diff --git a/frontiers/c8_cap_failure_coefficient_dims_20261001/SOURCE_FILES.json b/frontiers/c8_cap_failure_coefficient_dims_20261001/SOURCE_FILES.json new file mode 100644 index 000000000..f68a3b6bb --- /dev/null +++ b/frontiers/c8_cap_failure_coefficient_dims_20261001/SOURCE_FILES.json @@ -0,0 +1,40 @@ +{ + "schema": 1, + "scientific_effect": "NONE", + "certified": true, + "review_status": "AUTHOR_SIDE_LIMIT_THEOREM_WITH_CERTIFIED_COEFFICIENT", + "object": "CL-C8-CAP-FAILURE-COEFFICIENT-DIMS-20261001-v1", + "files": [ + { + "path": "NOTE.md", + "bytes": 21870, + "sha256": "893961eb500cf83c89954e02ad04b44f98006d0c5229833b1cbaa0870f99ffbf", + "git_blob": "b42be5b87514414dded25589549a009eb3f5506a" + }, + { + "path": "README.md", + "bytes": 2671, + "sha256": "168c00d3d6fa2a12ebc1198485267a1236060309ef046c355d7860ec4082860a", + "git_blob": "1d27defb1a31e3c6a98d87d9581022aef762875c" + }, + { + "path": "RESULTS.json", + "bytes": 6837, + "sha256": "1406d5138ac3d33bcb0358f6a3005a67e3a4a2dbfc2c43bc3ac2593667550608", + "git_blob": "e9fd6f377d1fd9dca9d09cc884d2bad2422e8b17" + }, + { + "path": "SOURCE_MAP.json", + "bytes": 5370, + "sha256": "6c4fdd0bf2d9a312254b5947570074eaa8fc0cdcff073361d0658956d7525e28", + "git_blob": "d94f66db9447e88b89daf2c34d54d3c2572b2bf7" + }, + { + "path": "cap_coefficient_dims.py", + "bytes": 24393, + "sha256": "76781298932a862f77bc785870017b4e627cc3b38841c2d1ac0b2405f5b7fdaf", + "git_blob": "af7e9d103f962f613c57f5e695f030165e348beb" + } + ], + "nonauthor_reads": [] +} diff --git a/frontiers/c8_cap_failure_coefficient_dims_20261001/SOURCE_MAP.json b/frontiers/c8_cap_failure_coefficient_dims_20261001/SOURCE_MAP.json new file mode 100644 index 000000000..d94f66db9 --- /dev/null +++ b/frontiers/c8_cap_failure_coefficient_dims_20261001/SOURCE_MAP.json @@ -0,0 +1,84 @@ +{ + "schema": 1, + "object": "CL-C8-CAP-FAILURE-COEFFICIENT-DIMS-20261001-v1", + "scientific_effect": "NONE", + "certified": true, + "review_status": "AUTHOR_SIDE_LIMIT_THEOREM_WITH_CERTIFIED_COEFFICIENT", + "source_repository": "d6g8k5htny-coder/Math-", + "main_at_creation": "3e0a91b69892b9717564c592e7a966492a81566a", + "note": "Theorem G_d: for the d-dimensional six-pin law of [LP] (d >= 3) and the good event G_r of [LP] section 7 / [CAP] (1) with partial-block operator norms, Q^W(G_r^c) = c_G^(d)(b, k) r^3 + o(r^3); for the reference kernel c_G^(d) = R_d(b) R(b) J^(d)(k) with R_d the hard-direction factor of Math-#184, R the planar factor of Math-#203 and J^(d) the planar J with M taken over the full transverse blocks. Certified in d = 3: R_3(0) = (32 + 28 sqrt2)/17, J^(3)(k) at k in {1, 3/2, 2} (monotone coupling with Math-#203's certified planar J plus chi-square tails), c_G^(3)(0, 2) in [22424320.655069, 22424320.655072]. Consumes [LP] (4.1), (4.2), (5.4), (5.5), (6.2), (7.1)-(7.4), (7.7) and the definitions; [CAP] for D, M_3, M_4 and (1); [SC] (8) for the spectral change of variables. Supplies no C, no r_*: C8 stays OPEN; it shows every d = 3 cap-route constant C_cap at (0, 2) exceeds 2.24e7 (not a lower bound for the constant of [LP] (1.1)).", + "sources": [ + { + "path": "imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md", + "bytes": 40261, + "sha256": "9350ad6eaba6626b93c3dedeef9e2ff816e5cdf1c8318e85fb27499141c84bc7", + "git_blob": "dfed3b8d318a3ab1950957f393307733a4bef3f2", + "id": "LP", + "commit": "3e0a91b69892b9717564c592e7a966492a81566a", + "role": "sections 1, 3, 4, 5, 6, 7: the d-dimensional model, the pins (3.1)-(3.4), the uniform moments (4.1), the regression on the transverse Hessian (4.2), the limit (5.4) and floor (5.5), the weight bound (6.2), the depth-branch inclusion and eigenvalue-measure bounds (7.1)-(7.4), the fourth-derivative bound (7.7); Theorem A (1.1) and the cap bound (7.8)", + "current_required": true, + "on_main": true + }, + { + "path": "imports/lifetime_parent_20260925/MARKED_CYLINDER_CAP_PROOF.md", + "bytes": 15160, + "sha256": "0bf922b9203c29088b12388807aa0e2ecd020485eb0f6e919679841b5b2636fc", + "git_blob": "0633aca3c2a2882b0de4399da0a75d64c2e6b2e1", + "id": "CAP", + "commit": "3e0a91b69892b9717564c592e7a966492a81566a", + "role": "section 1: the cylinder D = [-2r, 2r] x ball(0, 2r), the partial-block operator norms M_3, M_4 and condition (1) defining G_r in every d", + "current_required": true, + "on_main": true + }, + { + "path": "frontiers/spectral_cluster_closure_20260929/PROOF.md", + "bytes": 25006, + "sha256": "e971b2cbe50a8a06b47c1219191201e0d1037c9adac23e5e3b7d2051bb70c2eb", + "git_blob": "16c56821b52fd76b0be791622b9c3809eafde75a", + "id": "SC", + "commit": "3e0a91b69892b9717564c592e7a966492a81566a", + "role": "section 2 (8): the spectral change of variables for symmetric matrices with normalized Haar measure and the constant c_m", + "current_required": true, + "on_main": true + }, + { + "path": "frontiers/c8_cap_failure_coefficient_planar_20260930/RESULTS.json", + "bytes": 6427, + "sha256": "d3de1a20793fbbcbb051b5740af45628627b905827fe2e0d4758ac9e37c36088", + "git_blob": "e3a8e25a49fb572f0e3fb95c88f070ef9fa9d731", + "id": "G", + "commit": "a388580eee356a88ce31aeed3999ab3fdc302312", + "pull_request": "Math-#203", + "role": "the certified planar J(k) enclosures (embedded in cap_coefficient_dims.py as JG and used for the coupling enclosure of J^(3)); the planar Theorem G and R(b) (NOTE blob 0b64f1c2828dfae7e6c104bac044004fc72c221d)", + "current_required": false, + "on_main": false + }, + { + "path": "frontiers/c6_hard_direction_factorization_20260930/PROOF.md", + "bytes": 22456, + "sha256": "26743f82bf4b86d4ae4c7dfb085d4d15bf36014aa627dee5edfc86a75ca64c05", + "git_blob": "91d22fce0fd7d4630bfe2e2c93eab289babc97f2", + "id": "HD", + "commit": "d37ff5d0315a4f71453d37f0cae2da1f40fdef3c", + "pull_request": "Math-#184", + "role": "the definition of R_d(b), N_d(b), m_(d,b), the closed form R_3(0) (3) (re-derived here) and floating R_3(1) (compared), and Corollary 2 (the d-dimensional elder-failure coefficient R_d(b)(alpha_1 + alpha_2)^(2)), used for the comparison in Corollary item 2 only; its PROOF blob 91d22fce has OpenAI nonauthor ACCEPTs at d29e674 (Slices A/B 5366497205, Slice C 5366261768)", + "current_required": false, + "on_main": false + } + ], + "catalog_reference": { + "path": "reviews/candidates_pending_20260928/CANDIDATES.md", + "entry": "C8. Numerical constants (still open as of 2026-09-29): explicit finite C, r_*, z_*, c_{B,K}, c_{d,L} on a declared compact-mark / torus band; disposition OPEN", + "effect_here": "none; lower bound for every d = 3 cap-route constant C_cap at (b, k) = (0, 2) (reference kernel); no upper bound; C8 stays OPEN" + }, + "related_records": [ + "Math-#203 (planar Theorem G)", + "Math-#206 (planar explicit cap-route constants)", + "Math-#184 (hard-direction factor R_d)", + "Math-#195 (z_* planar)" + ], + "nonauthor_reads": [], + "nonauthor_acceptance": false, + "governing_status_changed": false, + "main_at_update": "3e0a91b69892b9717564c592e7a966492a81566a" +} diff --git a/frontiers/c8_cap_failure_coefficient_dims_20261001/cap_coefficient_dims.py b/frontiers/c8_cap_failure_coefficient_dims_20261001/cap_coefficient_dims.py new file mode 100644 index 000000000..af7e9d103 --- /dev/null +++ b/frontiers/c8_cap_failure_coefficient_dims_20261001/cap_coefficient_dims.py @@ -0,0 +1,631 @@ +#!/usr/bin/env python3 +"""The cap-failure coefficient of [LP] Theorem A's proof route in every dimension: certified values in d = 3. + +Theorem G_d (NOTE.md): for the d-dimensional six-pin law of [LP] and the good event G_r of [LP] section 7 / [CAP] (1) +(partial-block operator norms), Q^W(G_r^c) = c_G^(d)(b, k) r^3 + o(r^3), and for the reference kernel + + c_G^(d)(b, k) = R_d(b) R(b) J^(d)(k), + +R_d the hard-direction factor of Math-#184, R the planar factor of Math-#203, J^(d)(k) = (216 k^3)^-1 E[ int_{max(a,c)}^{8M^2} +(s - a)(s - c) ds ] with M = max(12k, 2|v|, ||Omega||_op, ||Y||_op) over the full transverse blocks. + +This script (standard library, exact rational interval arithmetic): + * checks the d = 3 contact law of the jets exactly (rational covariances of the reference kernel); + * certifies R_3(0) = (32 + 28 sqrt2)/17 and R(0) = 1/(2 sqrt(pi)); + * brackets J^(d)(k) for d = 2, 3 from Gaussian moments and chi-square tails (self-contained), checks that the d = 2 + bracket contains the certified planar J(k) of [G] = Math-#203, and encloses J^(3)(k) by the monotone coupling + J^(2) <= J^(3) <= J^(2) + tail; + * evaluates c_G^(3)(0, k); floating R_3(b) R(b) and Monte Carlo J^(3)(k) are recorded as controls. +""" +import argparse +import json +import math +import os +import random +import sys +from fractions import Fraction as Fr + +HERE = os.path.dirname(os.path.abspath(__file__)) +MUTANTS = ('no-y-tail', 'r3-one', 'no-bp', 'frob-omega-off') +MUT = None +PBITS = 160 +K_GRID = (Fr(1, 2), Fr(3, 4), Fr(1), Fr(3, 2), Fr(2)) +# [G] Math-#203 at a388580, RESULTS.json (git blob e3a8e25a49fb572f0e3fb95c88f070ef9fa9d731): certified planar J(k) +JG = {Fr(1, 2): ('301744.4364470241', '301744.4616663935'), + Fr(3, 4): ('995454.6123240485', '995454.6129283207'), + Fr(1): ('2359292.9611053703', '2359292.9611122569'), + Fr(3, 2): ('7962621.6645357431', '7962621.6645378716'), + Fr(2): ('18874366.3403946311', '18874366.3403964820')} + + +def require(cond, msg): + if not cond: + print(json.dumps({'check': 'FAIL', 'reason': msg, 'mutant': MUT})) + sys.exit(1) + + +def rdown(x): + return Fr(x.numerator * (1 << PBITS) // x.denominator, 1 << PBITS) + + +def rup(x): + return Fr(-((-x.numerator) * (1 << PBITS) // x.denominator), 1 << PBITS) + + +class IV: + __slots__ = ('lo', 'hi') + + def __init__(self, lo, hi=None): + lo = Fr(lo) + hi = lo if hi is None else Fr(hi) + if hi < lo: + raise ValueError('empty interval') + self.lo, self.hi = rdown(lo), rup(hi) + + def __repr__(self): + return 'IV(%s, %s)' % (float(self.lo), float(self.hi)) + + def __add__(self, o): + o = o if isinstance(o, IV) else IV(o) + return IV(self.lo + o.lo, self.hi + o.hi) + __radd__ = __add__ + + def __neg__(self): + return IV(-self.hi, -self.lo) + + def __sub__(self, o): + return self + (-(o if isinstance(o, IV) else IV(o))) + + def __rsub__(self, o): + return IV(o) - self + + def __mul__(self, o): + o = o if isinstance(o, IV) else IV(o) + c = (self.lo * o.lo, self.lo * o.hi, self.hi * o.lo, self.hi * o.hi) + return IV(min(c), max(c)) + __rmul__ = __mul__ + + def inv(self): + if self.lo <= 0 <= self.hi: + raise ZeroDivisionError('interval contains zero') + return IV(1 / self.hi, 1 / self.lo) + + def __truediv__(self, o): + o = o if isinstance(o, IV) else IV(o) + return self * o.inv() + + def __rtruediv__(self, o): + return IV(o) * self.inv() + + def sq(self): + if self.lo >= 0: + return IV(self.lo * self.lo, self.hi * self.hi) + if self.hi <= 0: + return IV(self.hi * self.hi, self.lo * self.lo) + return IV(0, max(self.lo * self.lo, self.hi * self.hi)) + + def meet(self, o): + lo, hi = max(self.lo, o.lo), min(self.hi, o.hi) + if hi < lo: + raise ValueError('inconsistent enclosures') + return IV(lo, hi) + + def width(self): + return self.hi - self.lo + + def mid(self): + return (self.lo + self.hi) / 2 + + def contains(self, x): + return self.lo <= x <= self.hi + + +def isqrt_iv(x): + """Enclosure of sqrt(x) for an interval x with x.lo > 0.""" + if x.lo <= 0: + raise ValueError('sqrt of interval reaching zero: %r' % x) + + def lo_root(v): + n = v.numerator * (1 << (2 * PBITS)) // v.denominator + s = math.isqrt(n) + return Fr(s, 1 << PBITS) + + def hi_root(v): + n = -((-v.numerator * (1 << (2 * PBITS))) // v.denominator) + s = math.isqrt(n) + 1 + return Fr(s, 1 << PBITS) + return IV(lo_root(x.lo), hi_root(x.hi)) + + +def exp_neg_point(t): + """Enclosure of exp(-t) for a rational t >= 0: halve t to t <= 1/2, evaluate the alternating series in fixed point + (ulp = 2^-(PBITS+40)) with an integer bound on the accumulated rounding error, then square back.""" + t = Fr(t) + m = 0 + while t > Fr(1, 2): + t /= 2 + m += 1 + P2 = PBITS + 40 + ONE = 1 << P2 + X = t.numerator * ONE // t.denominator # X / ONE <= t < (X + 1) / ONE + # series at x_lo = X / ONE: exp(-x_lo) = sum (-1)^n x_lo^n / n! (alternating, terms decreasing for x_lo <= 1/2) + S = ONE + T = ONE + E = 0 # error bound of T in ulps + Etot = 0 + n = 0 + while T > 0: + n += 1 + T = (T * X) // (ONE * n) + E = (E * X) // (ONE * n) + 2 + S += (-1) ** n * T + Etot += E + Etot += E + 1 # first omitted exact term is below (T_n + E) <= E + 1 ulps + # exp(-t) in [exp(-(X + 1)/ONE), exp(-X/ONE)] and exp(-(X + 1)/ONE) >= exp(-X/ONE) - 1/ONE (Lipschitz 1) + v = IV(Fr(S - Etot - 1, ONE), Fr(S + Etot, ONE)) + for _ in range(m): + v = v.sq() + return v + + +def exp_neg(t): + """exp(-t) on an interval t with t.lo >= 0 (monotone decreasing).""" + return IV(exp_neg_point(t.hi).lo, exp_neg_point(t.lo).hi) + + +def _atan_inv(n): + """Enclosure of arctan(1/n), n >= 2, alternating series.""" + x = Fr(1, n) + s = Fr(0) + term = x + k = 0 + while True: + s += term / (2 * k + 1) + k += 1 + term = term * (-x * x) + if abs(term) / (2 * k + 1) < Fr(1, 1 << (PBITS + 8)): + break + return IV(s - abs(term), s + abs(term)) + + +PI = 4 * (4 * _atan_inv(5) - _atan_inv(239)) +SQRT2 = isqrt_iv(IV(2)) +SQRT2PI = isqrt_iv(2 * PI) + + +def phi_point(x): + """Enclosure of Phi(x) = P(N(0,1) <= x) for a rational x with |x| <= 12, from the series + Phi(x) = 1/2 + (1/sqrt(2 pi)) sum_n (-1)^n x^(2n+1) / (2^n n! (2n+1)), evaluated in fixed point (ulp = 2^-(PBITS+40)) + with an explicit integer bound E on the accumulated rounding error (in ulps) and the alternating-tail bound.""" + x = Fr(x) + if x < 0: + p = phi_point(-x) + return IV(1 - p.hi, 1 - p.lo) + if x > 12: + raise ValueError('phi_point range') + P2 = PBITS + 40 + ONE = 1 << P2 + X = x.numerator * ONE // x.denominator # x_lo = X / ONE <= x < (X + 1) / ONE ; |Phi(x) - Phi(x_lo)| <= 1 ulp + if X == 0: # 0 <= x < 1 ulp: Phi(x) in [1/2, 1/2 + ulp] + return IV(Fr(1, 2), Fr(1, 2) + Fr(1, ONE)) + X2u = (X + 1) * (X + 1) # upper bound of x^2 ONE^2 + S = 0 + T = X # T_n ~ x^(2n+1) / (2^n n!) in ulps + E = 1 # error bound of T_n in ulps + Etot = 1 # error of S in ulps (starts with the x rounding) + n = 0 + while T > 0: + S += (-1) ** n * (T // (2 * n + 1)) + Etot += E + 1 + n += 1 + T = (T * X * X) // (ONE * ONE * 2 * n) + E = (E * X2u) // (ONE * ONE * 2 * n) + 2 + # once T == 0 in fixed point the remaining terms are each below 1 ulp; if x^2 >= 2 n they are still growing in + # exact arithmetic, so continue counting until they decrease: bound the tail by the first omitted exact term + # <= (T_n + E) ulps <= (E + 1) ulps when T_n == 0 ... but growth may resume; require the decreasing regime. + if x * x > 2 * n: + raise ValueError('series terminated before the decreasing regime') + Etot += E + 1 + core = IV(Fr(S - Etot, ONE), Fr(S + Etot, ONE)) / SQRT2PI + return IV(Fr(1, 2) + core.lo, Fr(1, 2) + core.hi) + + +def Phi(x): + """Phi on an interval (monotone); arguments clipped to [-12, 12] (clipping only widens).""" + lo = min(max(x.lo, Fr(-12)), Fr(12)) + hi = max(min(x.hi, Fr(12)), Fr(-12)) + if x.lo < -12: + plo = Fr(0) + else: + plo = phi_point(lo).lo + if x.hi > 12: + phi_ = Fr(1) + else: + phi_ = phi_point(hi).hi + return IV(plo, phi_) + + +# ----------------------------------------------------------------------------- exact contact law in d = 3 (reference kernel) +def _h(n): + return 0 if n % 2 else (-1) ** (n // 2) * math.prod(range(n - 1, 0, -2)) + + +def _cov(a, b): + """E[d^a f(0) d^b f(0)] = (-1)^|b| d^(a+b) exp(-|z|^2/2) at 0.""" + return Fr((-1) ** sum(b) * math.prod(_h(x + y) for x, y in zip(a, b))) + + +PINS3 = ((0, 0, 0), (1, 0, 0), (2, 0, 0), (3, 0, 0), (0, 1, 0), (1, 1, 0), (0, 0, 1), (1, 0, 1)) # contact jet [LP] (3.4) +JETS3 = {'f_xxy1': (2, 1, 0), 'f_xxy2': (2, 0, 1), 'O11': (1, 2, 0), 'O12': (1, 1, 1), 'O22': (1, 0, 2), + 'T111': (0, 3, 0), 'T112': (0, 2, 1), 'T122': (0, 1, 2), 'T222': (0, 0, 3), + 'A11': (0, 2, 0), 'A12': (0, 1, 1), 'A22': (0, 0, 2)} +CLAIM3 = {'f_xxy1': 2, 'f_xxy2': 2, 'O11': 2, 'O12': 1, 'O22': 2, 'T111': 6, 'T112': 2, 'T122': 2, 'T222': 6, + 'A11': 2, 'A12': 1, 'A22': 2} + + +def _solve(M, rhs): + n = len(M) + A = [row[:] + [x] for row, x in zip(M, rhs)] + for c in range(n): + p = next(i for i in range(c, n) if A[i][c] != 0) + A[c], A[p] = A[p], A[c] + for i in range(n): + if i != c and A[i][c] != 0: + f = A[i][c] / A[c][c] + A[i] = [x - f * y for x, y in zip(A[i], A[c])] + return [A[i][n] / A[i][i] for i in range(n)] + + +def contact_law_3(): + """Conditional law of the jets at 0 given the contact pins (f, f_x, f_xx, f_xxx, f_y1, f_xy1, f_y2, f_xy2) = (b, 0, 0, + 12k, 0, 0, 0, 0): returns (means as linear forms in (b, k), conditional covariance), exact rationals.""" + S = [[_cov(p, q) for q in PINS3] for p in PINS3] + names = list(JETS3) + W = {n: _solve(S, [_cov(JETS3[n], q) for q in PINS3]) for n in names} + mean = {n: (W[n][0], 12 * W[n][3]) for n in names} # coefficient of b and of k + C = {(m, n): _cov(JETS3[m], JETS3[n]) - sum(W[m][i] * _cov(JETS3[n], PINS3[i]) for i in range(len(PINS3))) + for m in names for n in names} + return mean, C + + +def check_contact_law(): + mean, C = contact_law_3() + for n in JETS3: + want_b = Fr(-1) if n in ('A11', 'A22') else Fr(0) + require(mean[n] == (want_b, Fr(0)), 'contact mean of ' + n) + require(C[(n, n)] == CLAIM3[n], 'contact variance of ' + n) + for m in JETS3: + for n in JETS3: + require(m == n or C[(m, n)] == 0, 'contact covariance %s, %s' % (m, n)) + return True + + +# ----------------------------------------------------------------------------- Gaussian and chi-square moments (intervals) +SQRTPI = isqrt_iv(PI) + + +def dfact(n): + return math.prod(range(n, 0, -2)) if n > 0 else 1 + + +def e_abs_std(n): + """E|Z|^n, Z ~ N(0,1).""" + if n % 2 == 0: + return IV(dfact(n - 1)) + return IV(dfact(n - 1)) * SQRT2 / SQRTPI + + +def e_v1(j): + """E[v1^(2j)], v1 ~ N(0, 1/2).""" + return Fr(dfact(2 * j - 1), 2 ** j) + + +def e_om(n): + """E|Omega11|^n, Omega11 ~ N(0, 2).""" + s = IV(2 ** (n // 2)) * (SQRT2 if n % 2 else IV(1)) + return s * e_abs_std(n) + + +def e_Q(j, k): + """E[Q^j], Q = 2 v1^2 + 6k |Omega11| (independent factors).""" + tot = IV(0) + for l in range(j + 1): + tot = tot + IV(math.comb(j, l) * 2 ** l * e_v1(l) * (6 * k) ** (j - l)) * e_om(j - l) + return tot + + +def gamma_half(two_s): + """Gamma(s) for s = two_s / 2 > 0 an integer or half-integer, as (rational, uses_sqrt_pi).""" + if two_s % 2 == 0: + return Fr(math.factorial(two_s // 2 - 1)), False + n = two_s // 2 # s = n + 1/2 + return Fr(math.factorial(2 * n), 4 ** n * math.factorial(n)), True + + +def chi_tail(nu, sigma2, p, t): + """Upper bound (interval) of E[Z^p 1{Z > t}] for Z^2 = sigma2 * chi2_nu, t > 0 rational, p >= 0 integer.""" + t = Fr(t) + y0 = t * t / sigma2 # Y = chi2_nu > y0 + x = y0 / 2 + two_s = nu + p # s = nu/2 + p/2 + g_s, pi_s = gamma_half(two_s) + g_n, pi_n = gamma_half(nu) + ratio = IV(g_s / g_n) + if pi_s and not pi_n: + ratio = ratio * SQRTPI + elif pi_n and not pi_s: + ratio = ratio / SQRTPI + # regularized upper incomplete gamma Q(s, x) + if two_s % 2 == 0: + n = two_s // 2 + Q = exp_neg(IV(x)) * IV(sum(x ** j / math.factorial(j) for j in range(n))) + else: + n = two_s // 2 # s = n + 1/2 + sx = isqrt_iv(IV(x)) if x > 0 else IV(0) + erfc = 2 * (1 - Phi(IV(t) / isqrt_iv(IV(sigma2)))) # erfc(sqrt x) = 2 Phibar(t / sigma) + acc = IV(0) + for j in range(n): + g, _ = gamma_half(2 * j + 3) # Gamma(j + 3/2) = g sqrt(pi) + acc = acc + IV(x ** j) * sx / (IV(g) * SQRTPI) + Q = erfc + exp_neg(IV(x)) * acc + sig_p = IV(sigma2 ** (p // 2)) * (isqrt_iv(IV(sigma2)) if p % 2 else IV(1)) + two_q = IV(2 ** (p // 2)) * (SQRT2 if p % 2 else IV(1)) # 2^(p/2) + val = sig_p * two_q * ratio * Q + return IV(0, val.hi) + + +# ----------------------------------------------------------------------------- the bracket of J^(d)(k) +LAWS = {2: {'v': (1, 2), 'om': (1, 2), 'Y': (1, 6)}, # (nu, sigma2): Z_v = 2|v1|, Z_Om = |Omega11|, Z_Y = |T111| + 3: {'v': (2, 2), 'om': (3, 2), 'Y': (4, 6)}} # Z_v = 2||v||, Z_Om = ||Omega||_F, Z_Y = weighted Frobenius + + +def tail_hi(d, k): + """Upper bound of T^(d)(k) = E[(P(8M^2) - P(1152 k^2)) 1{X > 12k}] (NOTE section 3), via + E[(512/3 Zbar^6 + 64 Q Zbar^4 + 8 Q^2 Zbar^2) 1{Zbar > t}] <= sum over the three blocks.""" + t = 12 * k + law = LAWS[d] + tot = IV(0) + coef = {0: Fr(512, 3), 1: Fr(64), 2: Fr(8)} # coefficient of Q^j Z^(6 - 2j) + for j in (0, 1, 2): + p = 6 - 2 * j + # block Y: independent of Q + if MUT != 'no-y-tail': + nu, s2 = law['Y'] + tot = tot + IV(coef[j]) * e_Q(j, k) * chi_tail(nu, s2, p, t) + # block Omega: Q <= 2 v1^2 + 6k Z_Om + nu, s2 = law['om'] + if MUT == 'frob-omega-off' and d == 3: + nu = 1 # wrong: |Omega11| does not dominate ||Omega||_op + for l in range(j + 1): + tot = tot + IV(coef[j] * math.comb(j, l) * 2 ** l * e_v1(l) * (6 * k) ** (j - l)) * chi_tail(nu, s2, p + j - l, t) + # block v: Q <= Z_v^2 / 2 + 6k |Omega11| + nu, s2 = law['v'] + for l in range(j + 1): + tot = tot + IV(coef[j] * math.comb(j, l) * Fr(1, 2 ** l) * (6 * k) ** (j - l)) * e_om(j - l) * chi_tail(nu, s2, p + 2 * l, t) + return tot.hi + + +def J_bracket(d, k): + """Self-contained bracket of J^(d)(k): 216 k^3 J = 512 t^6/3 - 6 t^2 - E[P(m0)] + T, t = 12k, + |E[P(m0)]| <= B_P = 2 E[Q^3], -2 E[Q^6] / (8 t^2)^3 <= T <= tail_hi.""" + k = Fr(k) + t = 12 * k + base = Fr(512) * t ** 6 / 3 - 6 * t ** 2 + bp = (2 * e_Q(3, k)).hi + if MUT == 'no-bp': + bp = Fr(0) + tlo = (2 * e_Q(6, k)).hi / (8 * t * t) ** 3 + thi = tail_hi(d, k) + den = 216 * k ** 3 + return IV((base - bp - tlo) / den, (base + bp + thi) / den), {'B_P': bp, 'T_lo': tlo, 'T_hi': thi} + + +def J3_from_G(k): + """Monotone coupling: J^(2)(k) <= J^(3)(k) <= J^(2)(k) + tail_hi(3, k) / (216 k^3), with J^(2) from [G].""" + lo, hi = (Fr(x) for x in JG[k]) + return IV(lo, hi + tail_hi(3, k) / (216 * k ** 3)) + + +def R3_0(): + """R_3(0) = N_3(0) m_(2,0) / m_(3,0) = 2 sqrt2 / ((7 - 4 sqrt2)/2) = (32 + 28 sqrt2)/17 (NOTE section 2).""" + if MUT == 'r3-one': + return IV(1) + return (32 + 28 * SQRT2) / 17 + + +R_0 = 1 / (2 * SQRTPI) # R(0) = phi_2(0) / m_(2,0) = (1/(2 sqrt pi)) / 1 + + +def m3_0_polar(): + """m_(3,0) = (1/(4 sqrt(2 pi))) * int rho^6 e^(-rho^2/4) drho * int_{pi/4}^{pi/2} c^2 s^2 (s - c) dtheta + = (30/sqrt2) * (7/(30 sqrt2) - 2/15) = (7 - 4 sqrt2)/2 (NOTE section 2): returns both sides.""" + lhs = IV(30) / SQRT2 * (IV(7) / (30 * SQRT2) - Fr(2, 15)) + rhs = (7 - 4 * SQRT2) / 2 + return lhs, rhs + + +# ----------------------------------------------------------------------------- floating controls (not part of the certificate) +def _Phi_f(x): + return 0.5 * (1 + math.erf(x / math.sqrt(2))) + + +def _phi_f(x): + return math.exp(-x * x / 2) / math.sqrt(2 * math.pi) + + +def r3r_float(b, n=4000, top=14.0): + """Floating R_3(b) R(b) = phi_2(b) N_3(b) / m_(3,b), and R_3(b) = N_3(b) m_(2,b) / m_(3,b): + N_3(b) = sqrt(pi/2) E[X_+^3], X ~ N(b, 2); m_(3,b) = E[((b + t)^2 - rho^2)^2 1{b + t > rho}], t ~ N(0,1), rho Rayleigh(1).""" + s = math.sqrt(2) + mu = b + ex3 = (mu ** 3 + 3 * mu * s * s) * _Phi_f(mu / s) + s * (mu * mu + 2 * s * s) * _phi_f(mu / s) + N3 = math.sqrt(math.pi / 2) * ex3 + m2 = (2 + b * b) * _Phi_f(b / s) + s * b * _phi_f(b / s) + + def inner(rho): # int_rho^inf (u^2 - rho^2)^2 phi(u - b) du + z = rho - b + P0 = 1 - _Phi_f(z) + ph = _phi_f(z) + # moments of u = b + x over x > z: E[x^j 1{x > z}] for x ~ N(0,1) + m = [P0, ph] + for j in range(2, 5): + m.append(z ** (j - 1) * ph + (j - 1) * m[j - 2]) + U = lambda p: sum(math.comb(p, j) * b ** (p - j) * m[j] for j in range(p + 1)) + return U(4) - 2 * rho * rho * U(2) + rho ** 4 * U(0) + h = top / n + acc = 0.0 + for i in range(n + 1): + rho = i * h + w = 1 if i in (0, n) else (4 if i % 2 else 2) + acc += w * rho * math.exp(-rho * rho / 2) * inner(rho) + m3 = acc * h / 3 + phi2 = math.exp(-b * b / 4) / (2 * math.sqrt(math.pi)) + return {'b': b, 'N3': N3, 'm2': m2, 'm3': m3, 'R3': N3 * m2 / m3, 'R': phi2 / m2, 'R3R': phi2 * N3 / m3} + + +def _ynorm(T111, T112, T122, T222, n=64): + best, bt = 0.0, 0.0 + for i in range(n): + th = math.pi * i / n + c, s = math.cos(th), math.sin(th) + y = abs(T111 * c ** 3 + 3 * T112 * c * c * s + 3 * T122 * c * s * s + T222 * s ** 3) + if y > best: + best, bt = y, th + f = lambda th: abs(T111 * math.cos(th) ** 3 + 3 * T112 * math.cos(th) ** 2 * math.sin(th) + + 3 * T122 * math.cos(th) * math.sin(th) ** 2 + T222 * math.sin(th) ** 3) + lo, hi = bt - math.pi / n, bt + math.pi / n + g = (math.sqrt(5) - 1) / 2 + for _ in range(40): + a, c = hi - g * (hi - lo), lo + g * (hi - lo) + if f(a) > f(c): + hi = c + else: + lo = a + return max(best, f((lo + hi) / 2)) + + +def mc_J(d, k, n, seed): + """Monte Carlo of J^(d)(k) (floating): v ~ N(0, I/2), Omega GOE(1), Y with T111, T222 ~ N(0,6), T112, T122 ~ N(0,2); + for d = 2 only the first components enter M.""" + rng = random.Random(seed) + tot = tot2 = 0.0 + k = float(k) + for _ in range(n): + v1, v2 = rng.gauss(0, math.sqrt(0.5)), rng.gauss(0, math.sqrt(0.5)) + o11, o22, o12 = rng.gauss(0, math.sqrt(2)), rng.gauss(0, math.sqrt(2)), rng.gauss(0, 1) + T111, T222 = rng.gauss(0, math.sqrt(6)), rng.gauss(0, math.sqrt(6)) + T112, T122 = rng.gauss(0, math.sqrt(2)), rng.gauss(0, math.sqrt(2)) + if d == 3: + vn = math.hypot(v1, v2) + tr, df = (o11 + o22) / 2, math.hypot((o11 - o22) / 2, o12) + on = max(abs(tr + df), abs(tr - df)) + yn = _ynorm(T111, T112, T122, T222) + else: + vn, on, yn = abs(v1), abs(o11), abs(T111) + M = max(12 * k, 2 * vn, on, yn) + a, c = v1 * v1, 6 * k * o11 - v1 * v1 + m0, S = max(a, c), 8 * M * M + P = lambda s: s ** 3 / 3 - (a + c) * s * s / 2 + a * c * s + x = (P(S) - P(m0)) / (216 * k ** 3) + tot += x + tot2 += x * x + m = tot / n + return {'d': d, 'k': str(Fr(k).limit_denominator(64)), 'n': n, 'seed': seed, 'J': m, 'se': math.sqrt(max(tot2 / n - m * m, 0) / n), + 'J_over_2359296k3': m / (2359296 * k ** 3)} + + +# ----------------------------------------------------------------------------- certified record, check, main +def dec_down(x, places): + x = Fr(x) + n = (x.numerator * 10 ** places) // x.denominator + s = str(abs(n)).rjust(places + 1, '0') + return ('-' if n < 0 else '') + s[:-places] + '.' + s[-places:] + + +def dec_up(x, places): + x = Fr(x) + n = -((-x.numerator * 10 ** places) // x.denominator) + s = str(abs(n)).rjust(places + 1, '0') + return ('-' if n < 0 else '') + s[:-places] + '.' + s[-places:] + + +def iv_str(x, places=10): + return [dec_down(x.lo, places), dec_up(x.hi, places)] + + +def certified(): + check_contact_law() + lhs, rhs = m3_0_polar() + require(abs(lhs.mid() - rhs.mid()) < Fr(1, 10 ** 40), 'm_(3,0) closed form') + r3 = R3_0() + out = {'contact_law_d3': 'verified exactly (rational covariances)', 'm3_0': iv_str(rhs, 20), 'R3_0': iv_str(r3, 20), + 'R_0': iv_str(R_0, 20), 'J': {}, 'J3_from_G': {}, 'cG3_0': {}, 'G_containment': {}} + for d in (2, 3): + out['J'][str(d)] = {} + for k in K_GRID: + br, parts = J_bracket(d, k) + out['J'][str(d)][str(k)] = {'bracket': iv_str(br, 6), 'B_P': dec_up(parts['B_P'], 6), + 'T_hi': dec_up(parts['T_hi'], 6), 'T_lo': dec_up(parts['T_lo'], 12)} + if d == 2: + g_lo, g_hi = (Fr(x) for x in JG[k]) + ok = br.lo <= g_lo and g_hi <= br.hi + require(ok or MUT is not None, 'planar bracket does not contain [G] at k = %s' % k) + out['G_containment'][str(k)] = ok + for k in K_GRID: + j3 = J3_from_G(k) + out['J3_from_G'][str(k)] = iv_str(j3, 10) + out['cG3_0'][str(k)] = iv_str(R3_0() * R_0 * j3, 6) + return out + + +def write_results(res): + with open(os.path.join(HERE, 'RESULTS.json'), 'w') as fh: + json.dump(res, fh, indent=1, sort_keys=True) + fh.write('\n') + + +def load_results(): + with open(os.path.join(HERE, 'RESULTS.json')) as fh: + return json.load(fh) + + +MC_PLAN = [(d, k, 200000, seed) for d in (2, 3) for k in (Fr(1, 6), Fr(1, 2), Fr(3, 4)) for seed in (1, 2)] + + +def main(): + global MUT + ap = argparse.ArgumentParser() + ap.add_argument('--check', action='store_true') + ap.add_argument('--mutant', choices=MUTANTS) + ap.add_argument('--controls', action='store_true', help='recompute the floating controls (slow)') + ap.add_argument('--procs', type=int, default=4) + args = ap.parse_args() + MUT = args.mutant + if args.check: + ref = load_results() + cur = certified() + require(cur == ref['certified'], 'certified values differ from RESULTS.json') + require(ref['mutant'] is None, 'RESULTS.json produced under a mutant') + # floating controls recorded: d = 3 Monte Carlo inside the certified enclosures where they are informative + for row in ref['controls']['mc']: + k = Fr(row['k']) + if row['d'] == 3 and k in (Fr(3, 4),): + lo, hi = (float(Fr(x)) for x in ref['certified']['J3_from_G'][str(k)]) + require(lo - 5 * row['se'] <= row['J'] <= hi + 5 * row['se'], 'MC control outside the enclosure') + print(json.dumps({'check': 'ok', 'cG3_0': cur['cG3_0'], 'mutant': MUT})) + return + res = {'schema': 1, 'object': 'CL-C8-CAP-FAILURE-COEFFICIENT-DIMS-20261001-v1', 'scientific_effect': 'NONE', + 'certified': certified(), 'mutant': MUT} + if args.controls: + import multiprocessing + with multiprocessing.Pool(args.procs) as pool: + mc = pool.starmap(mc_J, MC_PLAN) + res['controls'] = {'r3r_float': [r3r_float(b) for b in (0.0, 0.25, 0.5, 0.75, 1.0)], 'mc': mc} + else: + res['controls'] = load_results()['controls'] + write_results(res) + print(json.dumps(res['certified']['cG3_0'])) + + +if __name__ == '__main__': + main()