diff --git a/.github/workflows/c8-cap-failure-coefficient-planar.yml b/.github/workflows/c8-cap-failure-coefficient-planar.yml new file mode 100644 index 000000000..e072c919b --- /dev/null +++ b/.github/workflows/c8-cap-failure-coefficient-planar.yml @@ -0,0 +1,72 @@ +name: C8 planar cap-failure coefficient (certified replay) + +'on': + pull_request: + paths: + - 'frontiers/c8_cap_failure_coefficient_planar_20260930/**' + - '.github/workflows/c8-cap-failure-coefficient-planar.yml' + - 'imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md' + - 'imports/lifetime_parent_20260925/MARKED_CYLINDER_CAP_PROOF.md' + - 'frontiers/c6_cluster_coefficients_numerics_20260930/RESULTS.json' + - 'frontiers/local_elder_geometry_20260930/PROOF.md' + workflow_dispatch: + +permissions: + contents: read + +jobs: + certified-replay: + runs-on: ubuntu-latest + timeout-minutes: 75 + 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, recompute every certified enclosure in both interpreter modes, reject mutants + env: + PYTHONDONTWRITEBYTECODE: '1' + run: | + set -euo pipefail + python -B -S - <<'PY' + import concurrent.futures, hashlib, json, pathlib, subprocess, sys + root = pathlib.Path('frontiers/c8_cap_failure_coefficient_planar_20260930').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.py') + for flags in (['-B', '-S'], ['-B', '-O', '-S']): + out = subprocess.run([sys.executable, *flags, script, '--check', '--procs', '2'], cwd=root, capture_output=True, timeout=2400) + 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:]) + # each mutant fails on the first k value (about four minutes); run them two at a time + def mutant(args): + flags, m = args + return m, flags, subprocess.run([sys.executable, *flags, script, '--check', '--procs', '1', '--mutant', m], cwd=root, capture_output=True, timeout=2400).returncode + jobs = [(flags, m) for flags in (['-B', '-S'], ['-B', '-O', '-S']) for m in ['no-third-jet', 'sign-lo', 'variance-yyy']] + with concurrent.futures.ThreadPoolExecutor(max_workers=2) as ex: + for m, flags, rc in ex.map(mutant, jobs): + if rc != 1: + raise RuntimeError('mutant ' + m + ' not rejected under ' + ' '.join(flags)) + print(json.dumps({'scientific_effect': 'NONE', 'certified_enclosures_replayed': True, 'mutants_rejected': 6})) + PY + git diff --exit-code diff --git a/frontiers/c8_cap_failure_coefficient_planar_20260930/NOTE.md b/frontiers/c8_cap_failure_coefficient_planar_20260930/NOTE.md new file mode 100644 index 000000000..2838b76b2 --- /dev/null +++ b/frontiers/c8_cap_failure_coefficient_planar_20260930/NOTE.md @@ -0,0 +1,336 @@ +# The cap-failure probability in the proof of Theorem A has an exact leading coefficient in the plane + +**Object:** `CL-C8-CAP-FAILURE-COEFFICIENT-PLANAR-20260930-v1`. **Author lane:** Anthropic / Claude. +**Kind:** author-side limit theorem (Theorem G) with certified enclosures of its coefficient (exact rational interval +arithmetic; standard library only). **Scientific effect:** NONE. Catalog entry C8 (`reviews/candidates_pending_20260928/CANDIDATES.md`: +"explicit finite `C`, `r_*`, `z_*`, `c_{B,K}`, `c_{d,L}` on a declared band; OPEN") stays OPEN: this packet supplies neither +`C` nor `r_*`; it determines the exact size of the cap-failure probability `Q^W(G_r^c)` that the proof of Theorem A bounds +([LP] (7.8)), hence a lower bound for every cap-route constant `C_cap`; it gives no lower bound for the constant of Theorem A +itself, which bounds the smaller probability `1 - p_r` (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. + +Sources (pinned in `SOURCE_MAP.json`): [LP] `imports/lifetime_parent_20260925/UNIFORM_MATRIX_CAP_AND_LIFETIME.md` +(sections 1, 3, 4, 5, 7: the law `Q`, the weight `W_r`, the normalizer `Z_r`, the contact frame, the coupling (4.2), the +limit (5.4), the good event `G_r` and the bounds (7.5)–(7.8)); [CAP] `imports/lifetime_parent_20260925/MARKED_CYLINDER_CAP_PROOF.md` +(the cylinder `D`, the partial-block norms `M_3`, `M_4`, condition (1), and the recorded constants (2)–(3)); [NUM] +`frontiers/c6_cluster_coefficients_numerics_20260930/RESULTS.json` (the exact planar contact structure and the values of +`alpha_1`, `alpha_2`); [S] `frontiers/local_elder_geometry_20260930/PROOF.md` (Theorem S, (S2): `r^-3 (1 - p_r) -> alpha_1 + alpha_2`); +[Z] `frontiers/c8_normalizer_floor_planar_20260930/NOTE.md` at Math-#195 (the midpoint-jet coordinates; read, not consumed). + +## 0. Statement + +Setting of [LP] section 1 in `d = 2`: the torus `X = (R / L Z)^2`, the kernel `K_L` (periodized Gaussian, `K_L(0) = 1`), +an orthonormal frame `R` with axial direction `u`, the pins `M = -(r/2) u`, `S = (r/2) u`, `f(M) = b`, `f(S) = b - k r^3`, +`grad f(M) = grad f(S) = 0`, the Gaussian regression law `Q = Q_{r,b,k,R}`, the typed weight +`W_r = |det H_M det H_S| 1{H_M < 0, det H_S < 0}`, `Z_r = E_Q W_r`, `dQ^W = (W_r / Z_r) dQ`. In the frame's coordinates +`(x, y)` let `D = [-2r, 2r]^2` and, for `j = 3, 4`, `M_j = max_{a + c = j} sup_D |partial_x^a partial_y^c f|` ([CAP] section 1; +in `d = 2` the partial-block norm is the maximum of the coordinate partials). The good event of [LP] section 7 / [CAP] (1) is + + G_r = { -f_yy(M) > (4/(3k)) r M_3^2, r M_4 <= 3k/10 } + +(on the typed support `-f_yy(M) = lambda_min(-A_M)`). Theorem A of [LP] is `0 <= 1 - p_r <= C r^3` for `0 < r <= r_*` +([LP] (1.1); `p_r` is the `Q^W` probability that the global ordinary elder death partner of `M` is `S`). Its proof establishes +the stronger cap bound [LP] (7.8), `Q^W(G_r^c) <= C_3 r^3 + C_4 r^4 <= C r^3`, and deduces (1.1) from `1 - p_r <= Q^W(G_r^c)` +([LP] section 8: on `G_r` the global elder partner is `S`). A **cap-route constant** is any `C_cap` with +`Q^W(G_r^c) <= C_cap r^3` for `0 < r <= r_*`; every cap-route constant is a constant for [LP] (1.1), not conversely. + +**Theorem G.** Fix `b in R`, `k > 0`, `L`, `R`. Then + + Q^W(G_r^c) = c_G(b, k) r^3 + o(r^3), r -> 0, + + c_G(b, k) = R(b) J(k), + R(b) = p_w(0) / E[w^2 1{w < 0}], + J(k) = (216 k^3)^(-1) E[ integral_{max(a, c)}^{8 M^2} (s - a)(s - c) ds ], + a = v^2, c = 6k om - v^2, M = max(12k, 2|v|, |om|, |Y|), + +where `w` has the law of `f_yy(0)` given `(f, f_xx, f_xy)(0) = (b, 0, 0)`, `p_w` is its density, and `(v, om, Y)` has the law of +`(-f_xxy/2, f_xyy, f_yyy)(0)` given `(f_x, f_y, f_xxx)(0) = (0, 0, 12k)`, all under the unconditioned field with kernel +`K_L(R .)`; `w` is independent of `(v, om, Y)`. For the reference kernel `exp(-|z|^2/2)` (equivalently `L -> infinity`), + + w ~ N(-b, 2), v ~ N(0, 1/2), om ~ N(0, 2), Y ~ N(0, 6), independent, + + R(b) = [phi(b/sqrt2) / sqrt2] / [(2 + b^2) Phi(b/sqrt2) + sqrt2 b phi(b/sqrt2)], + +and `J(k) = 2359296 k^3 (1 + delta(k))`, where on the certified grid `delta(1/6) = 52.7`, `delta(1/2) = 0.0232`, +`delta(3/4) = 1.3e-4`, `delta(1) = -1.3e-6`, `delta(3/2) = -3.0e-7`, `delta(2) = -8.6e-8` (both signs occur; `delta(k) -> 0` as +`k -> infinity` by Remark (b), without a uniform rate proved here). + +**Certified values (reference kernel only).** `J(k)` at `k in {1/6, 1/2, 3/4, 1, 3/2, 2}`, `R(b)` at `b in {0, 1/4, 1/2, 3/4, 1, 6/5}` +and the products, all as rational enclosures (section 4). Two headline numbers: + + c_G(0, 2) in [5324360.4426, 5324360.4427] (the maximum over the Math-#195 band B = [0, 1], K = [1/2, 2] among the grid points), + c_G(6/5, 1/6) in [35736.7352, 35736.8785] (SIDE24's fixed-axis parameters, the only pair for which an explicit C is on record; + reference-kernel value only: no bound on SIDE24's finite-L jet-law deviation is claimed or enclosed here). + +**Corollary (what this says about `C_cap` and `r_*`).** Every cap-route constant `C_cap` at `(b, k)` (for a given kernel and +frame) satisfies `C_cap >= c_G(b, k)` for that kernel and frame. This is not a lower bound for every constant `C` of [LP] (1.1): +the only relation between the two events is `1 - p_r <= Q^W(G_r^c)`, and the smaller probability has the smaller coefficient +`alpha_1 + alpha_2` of [S] (S2) (Remark (d); section 5, items 1 and 4). The certified numbers are the reference-kernel +values `c_G^{ref}`; for the torus kernel `K_L` in a frame `R` the coefficient is `c_G^{L,R}`, the same formula on the exact +torus jet law, whose deviation from `c_G^{ref}` is **not enclosed here** (section 6). So, as a +reference-kernel statement (equivalently `L -> infinity`): every band containing `(0, 2)` needs `C_cap > 5.3 x 10^6`, and the +cap route cannot give a nontrivial bound (`C_cap r^3 < 1`) above `r = c_G^{-1/3}`, which is `5.7 x 10^-3` at `(0, 2)`, +`3.4 x 10^-2` at `(1, 1/2)`, and `3.0 x 10^-2` at `(6/5, 1/6)`; for a finite torus only the symbolic statements hold, with +`c_G^{L,R}` in place of `c_G^{ref}`; no numerical value is claimed there. The recorded cap-route constant of [CAP] (2)–(3), +`C3_new + C4_new / 20 ≈ 2.36 x 10^23` (`< 2.4 x 10^23`) at `(6/5, 1/6)`, exceeds the reference-kernel sharp cap coefficient +`c_G^{ref}(6/5, 1/6)` by a factor above `6 x 10^18` (the comparison with SIDE24's own finite-`L` coefficient is not enclosed). Against the true failure coefficient `alpha_1 + alpha_2` of [S] (S2) (the +actual elder-pairing failure, values from [NUM]) the cap criterion overstates the failure rate by the `b`-free factor +`36 k^2 J(k) / (J_1(k) + J_2(k))`: `7.4 x 10^4` at `k = 1/2`, `4.9 x 10^5` at `k = 1`, `2.4 x 10^6` at `k = 2` (section 5). + +## 1. Notation and the exact identities + +Write `lambda = -f_yy(M)`, and the six midpoint-jet coordinates of [Z] section 2 (exact for every `C^2` function with the +pins; only their definitions are used here): + + w = f_yy(M), om = (f_yy(S) - f_yy(M)) / r, + T = (f_xx(M) + 6 k r) / r^2, tau = (f_xx(S) - f_xx(M) - 12 k r) / r^3, + v = f_xy(M) / r, nu = (f_xy(S) + f_xy(M)) / r^2. + +They recover `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)`, +`f_yy(S) = w + r om`. Each of `T`, `tau`, `nu`, `v`, `om` is a linear functional of `f` annihilating the polynomials of +degree `<= 3, 4, 3, 2, 2` respectively along the pin segment (the pins supply `f_x(M) = f_x(S) = f_y(M) = f_y(S) = 0` +and `f(S) - f(M) = -k r^3`), so by Taylor's formula with integral remainder + + |T| <= C ||f||_{C^4(D)}, |tau| <= C ||f||_{C^5(D)}, |nu| <= C ||f||_{C^4(D)}, |v| <= C ||f||_{C^3(D)}, |om| <= C ||f||_{C^3(D)} (1.1) + +with absolute constants, for `r <= 1`, and as `r -> 0` (pathwise, for a `C^5` function) `T -> f_xxxx(0)/12`, +`v -> -f_xxy(0)/2`, `om -> f_xyy(0)`, `nu -> f_xxxy(0)/... ` (a fixed combination of the 4-jet), `tau` to a fixed combination of the 5-jet. +The determinants are exactly + + det H_M = r^2 [ (6k - r T) u_r - v^2 ], u_r := lambda / r = -w / r, + det H_S = r^2 [ (6k + r T + r^2 tau)(om - u_r) - (r nu - v)^2 ], (1.2) + +so on `{u_r = u}`: `W_r = r^4 |(6k - rT) u - v^2| |(6k + rT + r^2 tau)(om - u) - (r nu - v)^2| 1{type}`, with `type` = +`{f_xx(M) < 0, det H_M > 0, det H_S < 0}`. + +## 2. Proof of Theorem G + +**2.1 Coupling.** Let `G` be the unconditioned field (kernel `K_L(R .)`) and `U_r(G)` the six pin functionals in the +preconditioned form [LP] (3.1), with target `v_r` and covariance `Sigma_r`. The Gaussian regression coupling + + f_r = G + kappa_r(z) . (v_r - U_r(G)), kappa_r(z) = Cov(G(z), U_r) Sigma_r^{-1}, (2.1) + +realizes `Q_r` for every `r` on one probability space ([LP] (4.2)). As `r -> 0`, `U_r(G) -> U_0(G) = (f, f_x, f_xx, f_xxx, f_y, f_xy)(0)` +(Taylor), `v_r -> v_0 = (b, 0, 0, 12k, 0, 0)`, `Sigma_r -> Sigma_0` (positive definite, [LP] section 3), and +`Cov(G(z), U_{r,i}) -> Cov(G(z), U_{0,i})` in every `C^q(X)` (difference quotients of derivatives of `K_L`). Hence +`f_r -> f_0 := G + kappa_0 . (v_0 - U_0(G))` in `C^q(X)` almost surely and in every `L^p`, for every `q`; `f_0` has the +contact law `Q_0` (the field given the contact jet `U_0 = v_0`). All `Q_r`-moments of `||f_r||_{C^q(X)}` are bounded +uniformly in `r <= 1` ([LP] (4.1)). + +**2.2 Regression on `w`.** Under `Q_r`, `w = f_r,yy(M)` is `N(mu_w(r), sigma_w(r)^2)` with `(mu_w, sigma_w) -> (mu_w(0), sigma_w(0))`, +the parameters of `f_yy(0)` given the contact pins (`(-b, sqrt2)` for the reference kernel). Put `g_r(z) = Cov_Q(f_r(z), w) / sigma_w(r)^2` +and `f_r^perp = f_r - (w - mu_w(r)) g_r`, independent of `w`, with `g_r -> g_0` in every `C^q` and `f_r^perp -> f_0^perp` as in 2.1. +For any functional `Psi`, + + E_Q[Psi(f_r)] = integral p_{w,r}(omega) E[Psi(f_r^perp + (omega - mu_w(r)) g_r)] d omega. (2.2) + +The law of `f_r^perp + (0 - mu_w(0)) g_0` in the limit is the contact law given `f_yy(0) = 0`: by the parity of `K_L` +(`K_L(-z) = K_L(z)`, so all odd-order derivatives of `K_L` vanish at 0), the odd jets `(f_x, f_y, f_xxx, f_xxy, f_xyy, f_yyy)(0)` +are independent of the even jets `(f, f_xx, f_xy, f_yy)(0)`, and the conditioning on `f_yy(0) = 0` leaves the law of the odd +3-jet given `(f_x, f_y, f_xxx) = (0, 0, 12k)` unchanged. That law is `N(mu_odd, Sigma_odd)`; for the reference kernel the odd +covariances are `E f_x^2 = E f_y^2 = 1`, `E f_x f_xxx = -3`, `E f_x f_xyy = E f_y f_xxy = -1`, `E f_y f_yyy = -3`, +`E f_xxx^2 = E f_yyy^2 = 15`, `E f_xxy^2 = E f_xyy^2 = 3`, `E f_xxx f_xyy = E f_xxy f_yyy = 3`, the rest zero, so the two groups +`(f_x, f_xxx, f_xyy)` and `(f_y, f_xxy, f_yyy)` are independent, and the regression gives `f_xyy | (f_x = 0, f_xxx = 12k) ~ N(0, 2)`, +`(f_xxy, f_yyy) | f_y = 0 ~ N(0, diag(2, 6))`; likewise `f_yy | (f, f_xx, f_xy) = (b, 0, 0) ~ N(-b, 2)` ([NUM] `exact_structure`). +Hence `v = -f_xxy/2 ~ N(0, 1/2)`, `om = f_xyy ~ N(0, 2)`, `Y = f_yyy ~ N(0, 6)`, independent, as stated. + +**2.3 The three negligible parts.** (i) `Q^W(r M_4 > 3k/10) <= (10 r / 3k)^p E_Q[(W_r/r^2) M_4^p] / (Z_r / r^2) = O(r^p)` for every +`p`, by the uniform moments and the floor [LP] (5.5) (this is [LP] (7.7) with `p = 4`). (ii) On the depth failure +`{lambda <= (4/(3k)) r M_3^2}`, the part `{lambda > sqrt r}` is contained in `{M_3 >= (3k/4)^(1/2) r^(-1/4)}`, so its `Q^W`-mass is +at most `E_Q[(W_r/r^2) M_3^p] (4/(3k))^(p/2) r^(p/4) / z_* = O(r^(p/4))`, which is `o(r^3)` for `p > 12`. (iii) `Z_r / r^2 -> z_0(b, k) = 36 k^2 E[w^2 1{w < 0}]` +by [LP] (5.4). It remains to show + + r^(-5) E_Q[ W_r 1{lambda <= (4/(3k)) r M_3^2} 1{lambda <= sqrt r} ] -> p_w(0) E[ I(v, om, Y) ], + I = integral_{max(a, c)}^{8 M^2} (s - a)(s - c) ds / (6k). (2.3) + +**2.4 The main term.** Apply (2.2) with `omega = -r u`, `u in (0, r^(-1/2)]`: + + r^(-5) E_Q[...] = integral_0^{r^(-1/2)} p_{w,r}(-r u) E[ r^(-4) W_r(u) 1{u <= (4/(3k)) M_3(u)^2} ] du, + +where `W_r(u)`, `M_3(u)` are evaluated on the field `f_r(u) := f_r^perp + (-r u - mu_w(r)) g_r`. Since `r u <= sqrt r`, the +field `f_r(u)` differs from `f_r^perp - mu_w(r) g_r` by at most `sqrt r ||g_r||_{C^5}` in `C^5(X)`, uniformly in `u`. + +*Pointwise limit.* Fix `u > 0`. By 2.1, 2.2 and (1.1), the coordinates of `f_r(u)` converge almost surely: +`v -> v`, `om -> om`, `T`, `tau`, `nu` to finite limits, `M_3(u) -> max(|f_xxx|, |f_xxy|, |f_xyy|, |f_yyy|)(0) = max(12k, 2|v|, |om|, |Y|) = M` +(the supremum of a continuous function over the shrinking square `D_r`, the third partials of `f_r(u)` converging uniformly to +those of the limit field, whose `f_xxx(0)` is pinned at `12k`). By (1.2), `r^(-4) W_r(u) -> (6ku - v^2)(6k(u - om) + v^2)` +on `{6ku > v^2, 6k(om - u) - v^2 < 0}` and to `0` on the complement, except on the null set `{6ku = v^2} cup {6k(u - om) = -v^2}` +(`(v, om)` has a density); `f_xx(M) = r^2 T - 6kr < 0` eventually. With `s = 6ku`, `a = v^2`, `c = 6k om - v^2`, the limit is +`(s - a)(s - c) 1{s > max(a, c)}`. The indicator `1{u <= (4/(3k)) M_3(u)^2}` converges to `1{u <= (4/(3k)) M^2} = 1{s <= 8 M^2}` +for every `u` with `P(u = (4/(3k)) M^2) = 0`, i.e. for all `u` except `u = 192 k` (the atom of `M` at `12k`); a single `u` is +Lebesgue-null. And `p_{w,r}(-ru) -> p_w(0)`. + +*Domination.* Let `N_r = 1 + ||f_r^perp||_{C^5(X)} + ||g_r||_{C^5(X)}`. For `r <= 1` and `u <= r^(-1/2)`, all of `|T|, |tau|, |nu|, |v|, |om|` +on `f_r(u)` are bounded by `C N_r` by (1.1), so `r^(-4) W_r(u) <= C (1 + u)^2 N_r^4`, and `M_3(u) <= C N_r`, so +`1{u <= (4/(3k)) M_3(u)^2} <= 1{u <= C N_r^2}`. Therefore the `u`-integrand is bounded by `sup_r sup p_{w,r} . C (1 + u)^2 N_r^4 1{u <= C N_r^2}`, +whose `du`-integral is at most `C N_r^{10}`, with `sup_r E N_r^{10} < infinity` by 2.1. Explicitly, taking the expectation +first: at fixed `u` the expected integrand is at most `C (1 + u)^2 min(E N_r^4, (C/u)^4 E N_r^{12})` (Markov on +`{N_r^2 >= u/C}`), which is bounded uniformly in `r <= 1` by the integrable function `C' (1 + u)^2 min(1, u^-4)` +(`sup_r E N_r^{12} < infinity` by 2.1); and at fixed `u` the integrand converges almost surely under the coupling and is +uniformly integrable (`sup_r E N_r^8 < infinity`). Vitali's theorem at fixed `u` and dominated convergence in `u` give (2.3), +where the limit field is the contact field given `f_yy(0) = 0` and `E` is over the law of 2.2. + +**2.5 Conclusion.** `Q^W(G_r^c) = [E_Q(W_r 1_{depth, lambda <= sqrt r}) + o(r^5)] / Z_r = r^3 [p_w(0) E I + o(1)] / [z_0 + o(1)]`, and +`p_w(0) E[I] / z_0 = p_w(0) / (36 k^2 E[w^2 1{w<0}]) . E[I] = R(b) J(k)`, with `J(k) = E[I] / (36 k^2) = (216 k^3)^(-1) E[integral (s-a)(s-c) ds]`. +The lower limit `max(a, c) <= 8 M^2` always: `M >= 2|v|` gives `8 M^2 >= 32 v^2 >= a`, and `M >= max(12k, |om|)` gives +`8 M^2 >= 96 k |om| >= 6k om >= c`. QED. + +**Remarks.** (a) `R(b)` for the reference kernel: with `beta = b / sqrt2`, `p_w(0) = phi(beta)/sqrt2` and +`E[w^2 1{w<0}] = (2 + b^2) Phi(beta) + sqrt2 b phi(beta)` (integrate `(sqrt2 t - b)^2 phi(t)` over `t < beta`); `R` is strictly +decreasing on `b >= 0` (numerator decreasing; the denominator's derivative is `2 b Phi(beta) + 2 sqrt2 phi(beta) > 0`). +(b) The leading size of `J`: since `M >= 12k` is forced by the pinned `f_xxx(0)`, `E[F(8M^2)] >= (512/3)(12k)^6 - 8 E[v^4 M^2]`, +and `J(k) = (512/3)(12k)^6 / (216 k^3) (1 + delta(k)) = 2359296 k^3 (1 + delta(k))` with `delta -> 0` as `k` grows (the +free third derivatives `2|v|, |om|, |Y|` rarely exceed `12k`); `delta(k) > 0` for `k <= 3/4` and `|delta(k)| < 2e-6` for +`k >= 1` on the grid (both signs; the term `-8 E[v^4 M^2]` is negative). (c) For the torus kernel in a general frame the +same formula holds with the exact Gaussian laws `w ~ N(mu_w, sigma_w^2)`, `(v, om, Y) ~ N(mu_odd, Sigma_odd)` read off the +derivatives of `K_L(R .)` at 0; these differ from the reference values by `O(L^6 e^{-L^2/2})` (image sums), which is not +enclosed here (section 6). (d) Theorem G is a statement about the sufficient criterion `G_r`, not about the elder pairing: +the actual failure `1 - p_r` is `(alpha_1 + alpha_2) r^3 + o(r^3)` by [S] (S2), and `G_r^c` contains the failure event +([LP] section 8), so `c_G >= alpha_1 + alpha_2` necessarily; the size of the gap is in section 5. Hence `c_G` bounds +cap-route constants only: a constant for [LP] (1.1) itself is bounded below by `alpha_1 + alpha_2` where (S2) holds, not by `c_G`. + +## 3. Reduction of `J(k)` to three one-dimensional integrals + +With `F(s) = s^3/3 - (a + c) s^2/2 + a c s`, `integral_{max(a,c)}^{8M^2} (s-a)(s-c) ds = F(8M^2) - F(max(a, c))`. Since `M` depends on +`om` only through `|om|`, and `a + c = 6k om`, `a c = v^2 (6k om - v^2)` are odd in `om` up to the `-v^4` term, +`E[(a + c) M^4] = 0` and `E[a c M^2] = -E[v^4 M^2]`. Hence + + 216 k^3 J(k) = (512/3) I1 - 8 I2 - I3, I1 = E[M^6], I2 = E[v^4 M^2], I3 = E[F(max(a, c))]. + +Write `m = 12k`, `F_1(t) = P(|N(0,2)| <= t) = 2 Phi(t/sqrt2) - 1` (the law of `2|v|` and of `|om|`), `F_3(t) = 2 Phi(t/sqrt6) - 1` +(the law of `|Y|`), `sigma_v^2 = 1/2`. + +- `I1 = m^6 + integral_m^infinity 6 t^5 [1 - F_1(t)^2 F_3(t)] dt` (`P(M > t) = 1 - F_1^2 F_3` for `t >= m`). +- `I2 = H E[v^4 1{|v| <= 6k}] + 4 E[v^6 1{|v| > 6k}] + integral_m^infinity 2t [1 - F_1(t) F_3(t)] E[v^4 1{6k < |v| < t/2}] dt`, where + `H = m^2 + integral_m^infinity 2t [1 - F_1 F_3] dt = E[max(m, |om|, |Y|)^2]`: condition on `v`; `E[max(m_v, |om|, |Y|)^2] = m_v^2 + integral_{m_v}^infinity 2t (1 - F_1 F_3)` + with `m_v = max(m, 2|v|)`, and exchange the order of integration on `{2|v| > m}`. +- `I3 = 2 integral_0^infinity G(v) rho_v(v) dv`, where for fixed `v` the `om`-expectation is closed: with `theta = v^2/(3k)` + (the point `c = a`), `F(max(a,c)) = -(2/3) v^6 + 3k v^4 om` on `{om <= theta}` and `= [3 v^2 c^2 - c^3]/6` on `{om > theta}`, `c = 6k om - v^2`; + the truncated moments `E[om^j 1{om <= theta}]`, `E[om^j 1{om > theta}]`, `j <= 3`, are `Phi`, `phi` at `theta/sqrt2` times polynomials. + +Every remaining integral is one-dimensional with an integrand built from polynomials, `Phi(t/sigma)` and `phi(t/sigma)`. +The truncated Gaussian moments use `M_j(x) = integral_x^infinity u^j phi(u) du`, `M_0 = 1 - Phi`, `M_1 = phi`, `M_j = x^(j-1) phi(x) + (j-1) M_(j-2)`. + +## 4. Certification and values + +`cap_coefficient.py` (standard library; exact rational interval arithmetic with outward rounding to `2^-160`; `exp(-t)` by the +alternating series in fixed point with an integer rounding budget, `pi` by Machin, `Phi` by the fixed-point series of [Z]). +Each one-dimensional integral over `[m, m + 30]` (in `t`) or `[0, 8]` (in `v`) is enclosed by cells of width `1/512` with the +mean-value bound + + integral_cell f in h f(mid) +- (h^2/8) width(f'(cell)), + +`f'` obtained by forward-mode interval differentiation (a pair (value, derivative) propagated through `+`, `x`, `Phi`, `phi`, `M_j`); +the tails beyond the ranges are bounded in closed form (`1 - F_1^2 F_3 <= 2(1 - F_1) + (1 - F_3)`, `integral_T^infinity t^5 (1 - Phi(t/sigma)) dt <= (sigma^6/6) M_6(T/sigma)`, and +polynomial majorants of `|F(max(a,c))|` against the incomplete moments of `v`). The enclosures of `I1`, `I2`, `I3` are combined exactly; +`J`, `R` and `c_G` are printed as decimal brackets (rounded outward). + +| `k` | `J(k)` | width | `J / (2359296 k^3)` | +|---|---|---|---| +| `1/6` | `[586678.1211613003, 586680.4730695802]` | `2.35190827979` | `[53.71198619, 53.71220152]` | +| `1/2` | `[301744.4364470241, 301744.4616663935]` | `0.025219369345` | `[1.02316771, 1.02316780]` | +| `3/4` | `[995454.6123240485, 995454.6129283207]` | `0.000604272143` | `[1.00012720, 1.00012721]` | +| `1` | `[2359292.9611053703, 2359292.9611122569]` | `0.000006886435` | `[0.99999871, 0.99999872]` | +| `3/2` | `[7962621.6645357431, 7962621.6645378716]` | `0.000002128399` | `[0.99999970, 0.99999971]` | +| `2` | `[18874366.3403946311, 18874366.3403964820]` | `0.000001850785` | `[0.99999991, 0.99999992]` | + +| `b` | `R(b)` | +|---|---| +| `0` | `[0.282094791773, 0.282094791774]` | +| `1/4` | `[0.211225157119, 0.211225157120]` | +| `1/2` | `[0.155804629374, 0.155804629375]` | +| `3/4` | `[0.113118131654, 0.113118131655]` | +| `1` | `[0.080766267688, 0.080766267689]` | +| `6/5` | `[0.060913700223, 0.060913700224]` | + +`c_G(b, k) = R(b) J(k)` (four decimals, rounded outward): + +| `b` \ `k` | `1/6` | `1/2` | `3/4` | `1` | `3/2` | `2` | +|---|---|---|---|---|---|---| +| `0` | `[165498.8424, 165499.5059]` | `[85120.5339, 85120.5411]` | `[280812.5615, 280812.5618]` | `[665544.2565, 665544.2566]` | `[2246214.1004, 2246214.1005]` | `[5324360.4426, 5324360.4427]` | +| `1/4` | `[123921.1783, 123921.6752]` | `[63736.0159, 63736.0214]` | `[210265.0568, 210265.0571]` | `[498342.0264, 498342.0265]` | `[1681906.0121, 1681906.0122]` | `[3986740.9957, 3986740.9958]` | +| `1/2` | `[91407.1672, 91407.5337]` | `[47013.1800, 47013.1841]` | `[155096.4369, 155096.4371]` | `[367588.7653, 367588.7654]` | `[1240613.3172, 1240613.3173]` | `[2940713.6523, 2940713.6524]` | +| `3/4` | `[66363.9329, 66364.1990]` | `[34132.7668, 34132.7698]` | `[112603.9658, 112603.9660]` | `[266878.8117, 266878.8118]` | `[900716.8857, 900716.8858]` | `[2135033.0565, 2135033.0566]` | +| `1` | `[47383.8021, 47383.9922]` | `[24370.7719, 24370.7740]` | `[80399.1536, 80399.1538]` | `[190551.2868, 190551.2869]` | `[643111.2328, 643111.2329]` | `[1524412.1243, 1524412.1244]` | +| `6/5` | `[35736.7352, 35736.8785]` | `[18380.3701, 18380.3717]` | `[60636.8238, 60636.8239]` | `[143713.2641, 143713.2642]` | `[485032.7490, 485032.7491]` | `[1149707.4931, 1149707.4932]` | + +**Controls (floating, not part of the certificate).** Monte Carlo of `J(k)` from the definition (`2 x 10^5` samples of +`(v, om, Y)`, seed 2026) and a two-dimensional midpoint quadrature in `(v, om)` with the `Y`-expectation in closed form: +- `k = 1/6`: Monte Carlo `574856.1 +- 7874.9` (`-1.50` s.e. from the certified midpoint), quadrature `586681.402`. +- `k = 1/2`: Monte Carlo `301413.4 +- 238.0` (`-1.39` s.e. from the certified midpoint), quadrature `301744.426`. +- `k = 3/4`: Monte Carlo `995377.2 +- 43.1` (`-1.80` s.e. from the certified midpoint), quadrature `995454.613`. +- `k = 1`: Monte Carlo `2359221.4 +- 58.1` (`-1.23` s.e. from the certified midpoint), quadrature `2359292.961`. +- `k = 3/2`: Monte Carlo `7962462.0 +- 130.8` (`-1.22` s.e. from the certified midpoint), quadrature `7962621.665`. +- `k = 2`: Monte Carlo `18874082.4 +- 232.6` (`-1.22` s.e. from the certified midpoint), quadrature `18874366.340`. + +The `--check` mode requires the Monte Carlo value within four standard errors and the quadrature within `3 x 10^-4` of the +certified midpoint, the enclosure widths below `10^-5` relative, `J >= 2359296 k^3` for `k <= 3/4` and `|J / (2359296 k^3) - 1| < 2 x 10^-6` +for `k >= 1`, the closed-form `R(b)` against a floating evaluation, `R` decreasing on the grid (consecutive enclosures disjoint), the two headline inequalities, +and the exact arithmetic of [CAP] (3). + +## 5. Consequences for `C_cap`, `r_*`, and the size of the cap criterion's slack + +All numbers in this section are reference-kernel values (`c_G^{ref}`). For the torus kernel `K_L` in a frame `R` only the +symbolic statements transfer (`C_cap >= c_G^{L,R}`; `C_cap r^3 < 1` forces `r < (c_G^{L,R})^{-1/3}`); no numerical value of +`c_G^{L,R}` is claimed, and its deviation from `c_G^{ref}` is not enclosed here (section 6). + +1. **Lower bound for every cap-route constant `C_cap`.** If `Q^W(G_r^c) <= C_cap r^3` for all small `r` at `(b, k)`, then + `C_cap >= c_G(b, k)` (for the kernel and frame in question). This does not bound a constant `C` of [LP] (1.1) itself: the + only relation is `1 - p_r <= Q^W(G_r^c)`, and a coefficient of the larger probability does not bound the constants of the + smaller one (logical countermodel of review 5372981851 on Math-#203: one uniform `U`, `F_r = {U <= r^3}` inside + `G_r^c = {U <= 2 r^3}`; the cap coefficient is 2 while `C = 1` is admissible for `F_r`). On the band of Math-#195 + (`B = [0, 1]`, `K = [1/2, 2]`) the grid maximum of `c_G^{ref}` is at `(0, 2)`: `C_cap > 5.32 x 10^6` for the reference kernel. Since `R` is decreasing in `b`, the band maximum + over `b` is at `b = 0` for every `k`; the dependence on `k` is `~ k^3`. +2. **Where the cap route can be nontrivial.** `C_cap r^3 < 1` forces `r < c_G(b,k)^{-1/3}`: `5.7 x 10^-3` at `(0, 2)`, + `3.4 x 10^-2` at `(1, 1/2)` (the band's smallest `c_G` among the grid points), `3.0 x 10^-2` at `(6/5, 1/6)`. Any `r_*` + for which the cap bound [LP] (7.8) is informative on the band is below `6 x 10^-3` at the band's corner, whatever the proof + of (7.8). A proof of [LP] (1.1) that does not pass through `Q^W(G_r^c)` is not constrained by this item. +3. **The recorded constant.** [CAP] (2)–(3) give, for the fixed-axis SIDE24 law (`b = 6/5`, `k = 1/6`), + `C3_new + C4_new/20 ≈ 2.36 x 10^23` (`< 2.4 x 10^23`; exact rational arithmetic, replayed in `--check`), against the + reference-kernel value `c_G^{ref}(6/5, 1/6) = 35736.8`: a factor above `6 x 10^18` between the recorded cap-route constant + and the reference-kernel sharp cap coefficient (`--check` verifies it with `C3_new` alone against the upper end of the + enclosure; the comparison with SIDE24's own finite-`L` coefficient is not enclosed). The slack is in the moment bounds + (`||T||_8 < 320` for a supremum over a set of diameter `<= 6r`, `||M_4||_8 < 340`), not in the geometry. +4. **The criterion against the truth.** The actual elder-pairing failure has coefficient `alpha_1 + alpha_2` ([S] (S2)), and + by [NUM] `alpha_j = (p_b(0)/z_0) J_j(k)` with the same `b`-factor as `c_G` (`R(b) = 36 k^2 p_b(0)/z_0`), so the ratio is `b`-free: + + c_G / (alpha_1 + alpha_2) = 36 k^2 J(k) / (J_1(k) + J_2(k)), + + with `J_1 + J_2` from [NUM] (GH60: `36.785`, `172.87`, `1112.3` at `k = 1/2, 1, 2`): `7.4 x 10^4`, `4.9 x 10^5`, `2.4 x 10^6`. + (At `b = 0`: `alpha_1 + alpha_2 = 1.153, 1.355, 2.179` against `c_G = 8.5 x 10^4, 6.7 x 10^5, 5.3 x 10^6`.) The sufficient + condition `lambda > (4/(3k)) r M_3^2` with `M_3 >= 12k` forced fails whenever `lambda <= 192 k r`, a set of `w`-probability of + order `192 k r p_w(0)` whose typed weight is of order `(192 k r)^2`, while the actual failure requires the competing saddle + geometry of [S]; the ratio grows like `k^3 . 36 k^2 / (J_1 + J_2)(k)`. + +## 6. What this does not do + +Not a proof or a review of [LP] Theorem A, of [CAP], or of [S]: (5.4), (5.5), (7.6)–(7.7), the coupling (4.2) and the +uniform moments (4.1) are consumed as statements; [S] (S2) and the [NUM] values are quoted for comparison only. No upper +bound `C` or `C_cap` and no `r_*` are supplied (C8 stays OPEN on both), and no lower bound for the constant of [LP] (1.1) +itself (section 5, item 1). No rate in the `o(r^3)`. The certified numbers are for the +reference kernel; for the torus kernel `K_L` in a frame `R` the coefficient is the same formula with the exact jet law at 0, +whose deviation from the reference (`O(L^6 e^{-L^2/2})`) is not enclosed here, so every numerical consequence in sections 0 +and 5 is a reference-kernel statement (a certified finite-`L`, all-frame enclosure is a natural successor). Planar only (`d = 2`); the same argument in +`d >= 3` would need the eigenvalue boundary layer of [LP] section 7 and is not attempted. Nothing on `p_r` beyond the +comparison in section 5. + +## 7. Verification and provenance + +`python3 -B -S cap_coefficient.py --check --procs 2` (also `-B -O -S`): recomputes every enclosure and compares the decimal +records exactly with `RESULTS.json`; about four minutes per `k` on one core (`k = 1/6` first, then the others in parallel). +Mutants `no-third-jet` (drop `|Y|` from `M`), `sign-lo` (add `I3` instead of subtracting), `variance-yyy` (`Var Y = 2`) exit 1. +`cap_coefficient.py --procs 4` regenerates `RESULTS.json` (about eight minutes on four cores); `--quick K` certifies one `k`. +Workflow `.github/workflows/c8-cap-failure-coefficient-planar.yml`: manifest, main-resident pins ([LP], [CAP], [NUM], [S]), +both modes, mutants, clean tree. + +Revisions: v1.1 (Codex review 5372193385 on Math-#203: the `|v| > V_MAX` tail majorant, disjoint monotonicity enclosures, +reference-kernel qualification, `delta(k)` on the grid only; `RESULTS.json` unchanged). v1.2 (OpenAI review 5372981851, +confirmed by xAI review 5373266293: the lower bound concerns cap-route constants `C_cap` of [LP] (7.8) only, not the constant +of [LP] (1.1); the domination step of 2.4 made explicit; no numerical change, `RESULTS.json` and `cap_coefficient.py` unchanged). +v1.2.1 (Slice C successor read 5974168378 on Math-#203, findings F1–F3, wording only: the unenclosed finite-`L` bound for +SIDE24 is removed from section 0; the [CAP] comparison is stated against `c_G^{ref}`, with the value `≈ 2.36 x 10^23`; only +the symbolic statements transfer to a finite torus; no order is asserted for the deviation of `c_G` itself (Remark (c) derives +it for the jet-law parameters only); `RESULTS.json` and `cap_coefficient.py` unchanged). + +Author lane Anthropic / Claude, 30 September 2026. Scientific effect NONE. The author will not merge. diff --git a/frontiers/c8_cap_failure_coefficient_planar_20260930/README.md b/frontiers/c8_cap_failure_coefficient_planar_20260930/README.md new file mode 100644 index 000000000..0c0adf6af --- /dev/null +++ b/frontiers/c8_cap_failure_coefficient_planar_20260930/README.md @@ -0,0 +1,31 @@ +# The cap-failure coefficient in the plane (C8: what any cap-route constant `C_cap` must exceed) + +**Object:** `CL-C8-CAP-FAILURE-COEFFICIENT-PLANAR-20260930-v1`. **Author lane:** Anthropic / Claude. **Kind:** author-side +limit theorem with certified enclosures of its coefficient (exact rational interval arithmetic; standard library only). +**Scientific effect:** NONE (no register, catalog, GRAPH or STATUS change; C8 stays OPEN: no `C`, no `r_*` supplied). + +For the planar six-pin law of [LP] and the good event `G_r = {lambda_min(-A_M) > (4/(3k)) r M_3^2, r M_4 <= 3k/10}` of +[LP] section 7 / [CAP] (1), Theorem G (`NOTE.md`) gives the exact leading behaviour of the cap-failure probability that the +proof of Theorem A bounds ([LP] (7.8)): + + Q^W(G_r^c) = c_G(b, k) r^3 + o(r^3), c_G(b, k) = R(b) J(k), + +with `R(b)` in closed form and `J(k)` a three-dimensional Gaussian expectation reduced to one-dimensional integrals and +certified at `k in {1/6, 1/2, 3/4, 1, 3/2, 2}` for the reference kernel (`J(k) = 2359296 k^3 (1 + delta(k))`, `delta -> 0`; +the finite-torus jet-law deviation, of order `L^6 e^{-L^2/2}`, is not enclosed). Reference-kernel consequences: every +cap-route constant `C_cap` (any constant with `Q^W(G_r^c) <= C_cap r^3`) at `(b, k)` is at least `c_G(b, k)`; on the +Math-#195 band `C_cap > 5.3 x 10^6` (not a lower bound for the constant of Theorem A's `1 - p_r <= C r^3`, which bounds a +smaller probability); the cap route is informative only below `r = c_G^{-1/3}` (`6 x 10^-3` at the band's corner `(0, 2)`); +the recorded cap-route constant `≈ 2.36 x 10^23` of [CAP] at `(6/5, 1/6)` exceeds the reference-kernel sharp cap coefficient +`c_G^{ref}(6/5, 1/6)` by more than `6 x 10^18` (the comparison with SIDE24's own finite-`L` coefficient is not enclosed); the criterion overstates the true failure rate `alpha_1 + alpha_2` by `10^4`–`10^6`. + +- `NOTE.md` — statement, proof of Theorem G (coupling, regression on `f_yy(M)`, dominated convergence, parity), the + one-dimensional reduction, certification method, tables, consequences, non-claims. +- `cap_coefficient.py` — `--check --procs N` recomputes every enclosure and compares exactly with `RESULTS.json` (about four + minutes per `k` on one core); `--mutant {no-third-jet, sign-lo, variance-yyy}` must exit 1; no flags regenerates + `RESULTS.json`; `--quick K` certifies one `k`. +- `RESULTS.json`, `SOURCE_MAP.json` (pins [LP], [CAP], [NUM], [S] on `main`), `SOURCE_FILES.json`. +- Workflow `.github/workflows/c8-cap-failure-coefficient-planar.yml` replays manifest, pins, both interpreter modes and the + six mutant runs on every pull request. + +Same GitHub account as every other lane; zero organizational-independence credit. The author will not merge. diff --git a/frontiers/c8_cap_failure_coefficient_planar_20260930/RESULTS.json b/frontiers/c8_cap_failure_coefficient_planar_20260930/RESULTS.json new file mode 100644 index 000000000..e3a8e25a4 --- /dev/null +++ b/frontiers/c8_cap_failure_coefficient_planar_20260930/RESULTS.json @@ -0,0 +1,394 @@ +{ + "J": [ + { + "I1_E_M6": [ + "3437.9998534153", + "3438.0136333034" + ], + "I2_E_v4M2": [ + "9.4118754485", + "9.4118817190" + ], + "I3_E_F_lo": [ + "-1.4413227303", + "-1.4412321736" + ], + "J": [ + "586678.1211613003", + "586680.4730695802" + ], + "J_over_lead": [ + "53.71198619", + "53.71220152" + ], + "J_width": "2.351908279790", + "k": "1/6", + "lead_2359296_k3": "32768/3" + }, + { + "I1_E_M6": [ + "47738.1342147530", + "47738.1382032075" + ], + "I2_E_v4M2": [ + "27.1261695254", + "27.1261697283" + ], + "I3_E_F_lo": [ + "-8.5543347518", + "-8.5541096317" + ], + "J": [ + "301744.4364470241", + "301744.4616663935" + ], + "J_over_lead": [ + "1.02316771", + "1.02316780" + ], + "J_width": "0.025219369345", + "k": "1/2", + "lead_2359296_k3": "294912" + }, + { + "I1_E_M6": [ + "531511.2852574257", + "531511.2855777997" + ], + "I2_E_v4M2": [ + "60.7520277408", + "60.7520277468" + ], + "I3_E_F_lo": [ + "-28.2140373386", + "-28.2136502281" + ], + "J": [ + "995454.6123240485", + "995454.6129283207" + ], + "J_over_lead": [ + "1.00012720", + "1.00012721" + ], + "J_width": "0.000604272143", + "k": "3/4", + "lead_2359296_k3": "995328" + }, + { + "I1_E_M6": [ + "2985984.8149263452", + "2985984.8149313068" + ], + "I2_E_v4M2": [ + "108.0000083673", + "108.0000083674" + ], + "I3_E_F_lo": [ + "-68.5187047156", + "-68.5180640157" + ], + "J": [ + "2359292.9611053703", + "2359292.9611122569" + ], + "J_over_lead": [ + "0.99999871", + "0.99999872" + ], + "J_width": "0.000006886435", + "k": "1", + "lead_2359296_k3": "2359296" + }, + { + "I1_E_M6": [ + "34012224.0000008010", + "34012224.0000008011" + ], + "I2_E_v4M2": [ + "243.0000000000", + "243.0000000001" + ], + "I3_E_F_lo": [ + "-241.4479716269", + "-241.4464200259" + ], + "J": [ + "7962621.6645357431", + "7962621.6645378716" + ], + "J_over_lead": [ + "0.99999970", + "0.99999971" + ], + "J_width": "0.000002128399", + "k": "3/2", + "lead_2359296_k3": "7962624" + }, + { + "I1_E_M6": [ + "191102976.0000000000", + "191102976.0000000001" + ], + "I2_E_v4M2": [ + "432.0000000000", + "432.0000000001" + ], + "I3_E_F_lo": [ + "-588.2051207267", + "-588.2019225718" + ], + "J": [ + "18874366.3403946311", + "18874366.3403964820" + ], + "J_over_lead": [ + "0.99999991", + "0.99999992" + ], + "J_width": "0.000001850785", + "k": "2", + "lead_2359296_k3": "18874368" + } + ], + "R": { + "0": [ + "0.282094791773", + "0.282094791774" + ], + "1": [ + "0.080766267688", + "0.080766267689" + ], + "1/2": [ + "0.155804629374", + "0.155804629375" + ], + "1/4": [ + "0.211225157119", + "0.211225157120" + ], + "3/4": [ + "0.113118131654", + "0.113118131655" + ], + "6/5": [ + "0.060913700223", + "0.060913700224" + ] + }, + "c_G": { + "b=0,k=1": [ + "665544.2565", + "665544.2566" + ], + "b=0,k=1/2": [ + "85120.5339", + "85120.5411" + ], + "b=0,k=1/6": [ + "165498.8424", + "165499.5059" + ], + "b=0,k=2": [ + "5324360.4426", + "5324360.4427" + ], + "b=0,k=3/2": [ + "2246214.1004", + "2246214.1005" + ], + "b=0,k=3/4": [ + "280812.5615", + "280812.5618" + ], + "b=1,k=1": [ + "190551.2868", + "190551.2869" + ], + "b=1,k=1/2": [ + "24370.7719", + "24370.7740" + ], + "b=1,k=1/6": [ + "47383.8021", + "47383.9922" + ], + "b=1,k=2": [ + "1524412.1243", + "1524412.1244" + ], + "b=1,k=3/2": [ + "643111.2328", + "643111.2329" + ], + "b=1,k=3/4": [ + "80399.1536", + "80399.1538" + ], + "b=1/2,k=1": [ + "367588.7653", + "367588.7654" + ], + "b=1/2,k=1/2": [ + "47013.1800", + "47013.1841" + ], + "b=1/2,k=1/6": [ + "91407.1672", + "91407.5337" + ], + "b=1/2,k=2": [ + "2940713.6523", + "2940713.6524" + ], + "b=1/2,k=3/2": [ + "1240613.3172", + "1240613.3173" + ], + "b=1/2,k=3/4": [ + "155096.4369", + "155096.4371" + ], + "b=1/4,k=1": [ + "498342.0264", + "498342.0265" + ], + "b=1/4,k=1/2": [ + "63736.0159", + "63736.0214" + ], + "b=1/4,k=1/6": [ + "123921.1783", + "123921.6752" + ], + "b=1/4,k=2": [ + "3986740.9957", + "3986740.9958" + ], + "b=1/4,k=3/2": [ + "1681906.0121", + "1681906.0122" + ], + "b=1/4,k=3/4": [ + "210265.0568", + "210265.0571" + ], + "b=3/4,k=1": [ + "266878.8117", + "266878.8118" + ], + "b=3/4,k=1/2": [ + "34132.7668", + "34132.7698" + ], + "b=3/4,k=1/6": [ + "66363.9329", + "66364.1990" + ], + "b=3/4,k=2": [ + "2135033.0565", + "2135033.0566" + ], + "b=3/4,k=3/2": [ + "900716.8857", + "900716.8858" + ], + "b=3/4,k=3/4": [ + "112603.9658", + "112603.9660" + ], + "b=6/5,k=1": [ + "143713.2641", + "143713.2642" + ], + "b=6/5,k=1/2": [ + "18380.3701", + "18380.3717" + ], + "b=6/5,k=1/6": [ + "35736.7352", + "35736.8785" + ], + "b=6/5,k=2": [ + "1149707.4931", + "1149707.4932" + ], + "b=6/5,k=3/2": [ + "485032.7490", + "485032.7491" + ], + "b=6/5,k=3/4": [ + "60636.8238", + "60636.8239" + ] + }, + "certified": true, + "float_controls": [ + { + "J_mc": 574856.1198204531, + "J_mc_se": 7874.938783619914, + "J_quad2d": 586681.402397974, + "k": "1/6" + }, + { + "J_mc": 301413.4425319479, + "J_mc_se": 237.99553228948025, + "J_quad2d": 301744.4261346985, + "k": "1/2" + }, + { + "J_mc": 995377.204072532, + "J_mc_se": 43.05318717060184, + "J_quad2d": 995454.612652818, + "k": "3/4" + }, + { + "J_mc": 2359221.4292606898, + "J_mc_se": 58.11555748163625, + "J_quad2d": 2359292.961109003, + "k": "1" + }, + { + "J_mc": 7962462.002485035, + "J_mc_se": 130.82447172777563, + "J_quad2d": 7962621.664536541, + "k": "3/2" + }, + { + "J_mc": 18874082.40721163, + "J_mc_se": 232.61705608413584, + "J_quad2d": 18874366.340394832, + "k": "2" + } + ], + "kind": "certified enclosures of the limit coefficient c_G(b, k) = R(b) J(k) of Theorem G (NOTE.md); the limit theorem itself is author-side", + "mutant": null, + "object": "CL-C8-CAP-FAILURE-COEFFICIENT-PLANAR-20260930-v1", + "parameters": { + "CELL": "1/512", + "LEAD": 2359296, + "PBITS": 160, + "T_SPAN": "30", + "V_MAX": "8", + "b_grid": [ + "0", + "1/4", + "1/2", + "3/4", + "1", + "6/5" + ], + "k_grid": [ + "1/6", + "1/2", + "3/4", + "1", + "3/2", + "2" + ] + }, + "schema": 1, + "scientific_effect": "NONE", + "statement": "Q^W(G_r^c) = c_G(b, k) r^3 + o(r^3) as r -> 0 for the planar six-pin law of [LP] with the good event G_r of [LP] section 7 / [CAP] (1); reference-kernel jet law" +} diff --git a/frontiers/c8_cap_failure_coefficient_planar_20260930/SOURCE_FILES.json b/frontiers/c8_cap_failure_coefficient_planar_20260930/SOURCE_FILES.json new file mode 100644 index 000000000..51cee3e6c --- /dev/null +++ b/frontiers/c8_cap_failure_coefficient_planar_20260930/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-PLANAR-20260930-v1", + "files": [ + { + "path": "NOTE.md", + "bytes": 29358, + "sha256": "b3e8d67f7c9f0ee3204e0cfc2e9ce134087f3ff56e26ec4b8a9268040e24a8dc", + "git_blob": "2838b76b21a884bd77d18f294d1730780b3ed3ab" + }, + { + "path": "README.md", + "bytes": 2744, + "sha256": "ee24910a9b9c570b44a7d63a7637bd6a5030c8be4b0e836006c4838f15b4db32", + "git_blob": "0c0adf6af489dffde48d1d22f4da4c27aa1d10cd" + }, + { + "path": "RESULTS.json", + "bytes": 6427, + "sha256": "d3de1a20793fbbcbb051b5740af45628627b905827fe2e0d4758ac9e37c36088", + "git_blob": "e3a8e25a49fb572f0e3fb95c88f070ef9fa9d731" + }, + { + "path": "SOURCE_MAP.json", + "bytes": 6542, + "sha256": "6a3cb4148f856f9838c867660153d030a319cfe47216b165c6d84108d5aa6869", + "git_blob": "bb978458dc78895d8289dab6a8b6c47219ce7fd1" + }, + { + "path": "cap_coefficient.py", + "bytes": 28336, + "sha256": "6f29e07f3f28d04d87bad265096699f15bd663f57872359c7f7484c84531a0c7", + "git_blob": "cfdaa4d7ceaaf707ed7c066570215862879cce65" + } + ], + "nonauthor_reads": [] +} diff --git a/frontiers/c8_cap_failure_coefficient_planar_20260930/SOURCE_MAP.json b/frontiers/c8_cap_failure_coefficient_planar_20260930/SOURCE_MAP.json new file mode 100644 index 000000000..bb978458d --- /dev/null +++ b/frontiers/c8_cap_failure_coefficient_planar_20260930/SOURCE_MAP.json @@ -0,0 +1,120 @@ +{ + "schema": 1, + "object": "CL-C8-CAP-FAILURE-COEFFICIENT-PLANAR-20260930-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: for the planar six-pin law of [LP] and the good event G_r of [LP] section 7 / [CAP] (1), Q^W(G_r^c) = c_G(b, k) r^3 + o(r^3) with c_G = R(b) J(k) explicit (R closed form; J a Gaussian expectation reduced to one-dimensional integrals and certified on a k-grid). Consumes [LP] (4.1), (4.2), (5.4), (5.5), (7.6)-(7.7) and the definitions of Q, W_r, Z_r, G_r as statements; [CAP] for D, M_3, M_4 and its recorded constant; [NUM] for the exact contact structure and the alpha values; [S] (S2) for the comparison only. Supplies neither C nor r_*: C8 stays OPEN; it shows every cap-route constant C_cap (Q^W(G_r^c) <= C_cap r^3, the bound [LP] (7.8)) on the Math-#195 band exceeds 5.3e6 and locates the cap route's informative range below r = c_G^(-1/3); it gives no lower bound for the constant of [LP] (1.1), which bounds the smaller probability 1 - p_r (v1.2, review 5372981851).", + "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, 7: the law Q, the weight W_r, the normalizer Z_r, the preconditioned contact frame (3.1)-(3.4), the coupling (4.2) and the uniform moments (4.1), the limit (5.4) and the floor (5.5), the good event G_r of section 7 and the bounds (7.5)-(7.8); Theorem A; section 16 lists a numerical r_*, C among the items not supplied", + "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 norms M_3, M_4 (coordinate partials in d = 2), condition (1); the probabilistic corollary (2)-(3) with C3_new, C4_new for the fixed-axis SIDE24 law (b = 6/5, k = 1/6): the only explicit C on record, compared with c_G(6/5, 1/6) here", + "current_required": true, + "on_main": true + }, + { + "path": "frontiers/c6_cluster_coefficients_numerics_20260930/RESULTS.json", + "bytes": 4095, + "sha256": "9c88ea85b6ba08199996c9b5ff74ecd06afc0f458e08c28b4c3af6191f437fcb", + "git_blob": "2648314f8c11f0637ce301ba76360142a8309e8f", + "id": "NUM", + "commit": "3e0a91b69892b9717564c592e7a966492a81566a", + "role": "exact_structure: the planar contact law (f_yy | even pins ~ N(-b, 2); odd 3-jet | odd pins ~ N(0, diag(2, 2, 6))) used in Theorem G's identification of (w, v, om, Y); prefactor: the values alpha_1, alpha_2 (GH60) quoted in section 5 for the comparison with the true failure coefficient (Math-#168, merged)", + "current_required": true, + "on_main": true + }, + { + "path": "frontiers/local_elder_geometry_20260930/PROOF.md", + "bytes": 39722, + "sha256": "f68038be79b46124b0f9b31205aa6e3682b34b6f5ef81f4a5697ae81f07cc46b", + "git_blob": "ef2aa57959ea9f721bbf2316ce94cf616c1c9113", + "id": "S", + "commit": "3e0a91b69892b9717564c592e7a966492a81566a", + "role": "Theorem S, (S2): r^-3 (1 - p_r) -> alpha_1 + alpha_2 (the actual planar elder-failure coefficient), quoted for the comparison in section 5 only; not consumed by Theorem G (Math-#170, merged)", + "current_required": true, + "on_main": true + } + ], + "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; this packet supplies a lower bound for every cap-route constant C_cap (not for the constant of (1.1)) and no upper bound; C8 stays OPEN on C and r_*" + }, + "related_records": [ + "Math-#195 (z_*)", + "Math-#197 (c_{B,K})", + "Math-#199, Math-#200 (c_{d,L}, d = 4, 5)" + ], + "nonauthor_reads": [ + { + "comment": "5372193385", + "pr": "Math-#203", + "lane": "OpenAI / Codex (automated Codex review)", + "scope": "review of 8968f5ef82; findings applied in v1.1", + "kind": "pull_request_review" + }, + { + "comment": "5372981851", + "pr": "Math-#203", + "lane": "OpenAI (as recorded in the v1.2 revision note)", + "scope": "P1: lower bound concerns cap-route constants only; applied in v1.2", + "kind": "pull_request_review" + }, + { + "comment": "5373266293", + "pr": "Math-#203", + "lane": "xAI / Grok team", + "scope": "Slice C at 683ed30: P1 confirmed", + "kind": "pull_request_review" + }, + { + "comment": "5373441664", + "pr": "Math-#203", + "lane": "nonauthor (lane not stated in the review)", + "scope": "P1 amendment verified at a388580: scoped PASS_TECHNICAL", + "kind": "pull_request_review" + }, + { + "comment": "5378711140", + "pr": "Math-#203", + "lane": "xAI / Grok team", + "scope": "bounded Slice A (sections 1-2) and reduction note at a388580; not a certificate acceptance", + "kind": "pull_request_review" + }, + { + "comment": "5402161720", + "pr": "Math-#203", + "lane": "OpenAI / GPT-5.6 Sol", + "scope": "Slice B (sections 3-4, cap_coefficient.py, RESULTS.json): PASS_TECHNICAL_SCOPED / ACCEPT_SCOPED at a388580", + "kind": "pull_request_review" + }, + { + "comment": "5974168378", + "pr": "Math-#203", + "lane": "Grok Bot agent 14 (Grok support, routed by the Chief of Staff 5974102560)", + "scope": "R7 Slice C successor read of the v1.2 wording at a388580, no execution: ACCEPT_WITH_FINDINGS; F1 (required) and F2-F3 (recommended) applied in v1.2.1, wording only", + "kind": "issue_comment" + } + ], + "nonauthor_acceptance": false, + "governing_status_changed": false, + "main_at_update": "3e0a91b69892b9717564c592e7a966492a81566a" +} diff --git a/frontiers/c8_cap_failure_coefficient_planar_20260930/cap_coefficient.py b/frontiers/c8_cap_failure_coefficient_planar_20260930/cap_coefficient.py new file mode 100644 index 000000000..cfdaa4d7c --- /dev/null +++ b/frontiers/c8_cap_failure_coefficient_planar_20260930/cap_coefficient.py @@ -0,0 +1,728 @@ +#!/usr/bin/env python3 +"""Exact leading coefficient of the cap-failure probability of [LP] Theorem A in the plane. + +G_r = {lambda_min(-A_M) > (4/(3k)) r M_3^2, r M_4 <= 3k/10} is the good event of [LP] section 7 / [CAP] (1), with M_3, M_4 the +partial-block derivative norms on the cylinder D = [-2r, 2r] x [-2r, 2r] and Q^W = W_r Q / Z_r the typed pair law. NOTE.md +Theorem G: Q^W(G_r^c) = c_G(b, k) r^3 + o(r^3), c_G = R(b) J(k), + + R(b) = p_w(0) / E[w^2 1{w < 0}], w ~ N(-b, 2) (closed form in Phi, phi), + J(k) = (216 k^3)^(-1) E[ integral_{max(a, c)}^{8 M^2} (s - a)(s - c) ds ], + a = v^2, c = 6k om - v^2, M = max(12k, 2|v|, |om|, |Y|), v ~ N(0, 1/2), om ~ N(0, 2), Y ~ N(0, 6) independent + +(the contact jets -f_xxy/2, f_xyy, f_yyy at the pins' midpoint given the six pins, reference kernel). By symmetry in om the +expectation reduces to three one-dimensional integrals (NOTE.md section 3): + + 216 k^3 J(k) = (512/3) I1 - 8 I2 - I3, + I1 = E[M^6], I2 = E[v^4 M^2], I3 = E[F(max(a, c))], F(s) = s^3/3 - (a + c) s^2/2 + a c s. + +Certification: exact rational interval arithmetic (outward rounding to 2^-160; exp by alternating series, pi by Machin, +Phi by a fixed-point series with an integer rounding budget); each one-dimensional integral by cells with the mean-value +enclosure integral_cell f in h f(mid) +- (h^2/8) width(f'(cell)), f' from forward-mode interval differentiation, and +closed-form Gaussian tails. Standard library only; deterministic. The interval toolkit is the one of +frontiers/c8_normalizer_floor_planar_20260930/floor.py (Math-#195). +""" +import argparse +import json +import math +import multiprocessing +import os +import random +import sys +from fractions import Fraction as Fr + +HERE = os.path.dirname(os.path.abspath(__file__)) +MUTANTS = ('no-third-jet', 'sign-lo', 'variance-yyy') +MUT = None +PBITS = 160 +K_GRID = (Fr(1, 6), Fr(1, 2), Fr(3, 4), Fr(1), Fr(3, 2), Fr(2)) +B_GRID = (Fr(0), Fr(1, 4), Fr(1, 2), Fr(3, 4), Fr(1), Fr(6, 5)) +CELL = Fr(1, 512) # cell width of the certified quadratures +T_SPAN = Fr(30) # integrate t on [12k, 12k + T_SPAN]; the rest is a closed-form tail +V_MAX = Fr(8) # integrate v on [0, V_MAX]; the rest is a closed-form tail +LEAD = 2359296 # J(k) ~ LEAD k^3 = (512/3)(12k)^6 / (216 k^3): the pinned f_xxx forces M >= 12k + + +def require(cond, msg): + if not cond: + print(json.dumps({'check': 'FAIL', 'reason': msg, 'mutant': MUT})) + sys.exit(1) + + +# ----------------------------------------------------------------------------- rational intervals (from floor.py, Math-#195) +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_) + + +def phi_iv(x): + """Standard normal density on an interval (via exp(-x^2/2) monotone in x^2).""" + return exp_neg(x.sq() * Fr(1, 2)) / SQRT2PI + + +# ----------------------------------------------------------------------------- forward-mode interval differentiation +class DV: + """Pair (value interval, derivative interval) of a function of one real variable, both rigorous on a cell.""" + __slots__ = ('v', 'd') + + def __init__(self, v, d): + self.v = v if isinstance(v, IV) else IV(v) + self.d = d if isinstance(d, IV) else IV(d) + + @staticmethod + def var(x): + return DV(x, IV(1)) + + @staticmethod + def const(c): + return DV(c, IV(0)) + + def __add__(self, o): + o = o if isinstance(o, DV) else DV.const(o) + return DV(self.v + o.v, self.d + o.d) + __radd__ = __add__ + + def __neg__(self): + return DV(-self.v, -self.d) + + def __sub__(self, o): + return self + (-(o if isinstance(o, DV) else DV.const(o))) + + def __rsub__(self, o): + return DV.const(o) - self + + def __mul__(self, o): + o = o if isinstance(o, DV) else DV.const(o) + return DV(self.v * o.v, self.d * o.v + self.v * o.d) + __rmul__ = __mul__ + + def scale(self, c): + c = Fr(c) + return DV(self.v * c, self.d * c) + + def sq(self): + return DV(self.v.sq(), self.d * self.v * 2) + + def pow(self, n): + out = DV.const(1) + for _ in range(n): + out = out * self + return out + + +def Phi_dv(x): + """Phi(x) with derivative phi(x) x'.""" + return DV(Phi(x.v), phi_iv(x.v) * x.d) + + +def phi_dv(x): + """phi(x) with derivative -x phi(x) x'.""" + p = phi_iv(x.v) + return DV(p, -(x.v * p) * x.d) + + +def upper_moment(j, x): + """M_j(x) = integral_x^infinity u^j phi(u) du (x >= 0), as DV in x (derivative -x^j phi(x) x'); by the recursion + M_0 = 1 - Phi, M_1 = phi, M_j = x^(j-1) phi(x) + (j - 1) M_(j-2).""" + p = phi_iv(x.v) + P = Phi(x.v) + vals = [IV(1) - P, p] + for m in range(2, j + 1): + xp = IV(x.v.lo ** (m - 1), x.v.hi ** (m - 1)) + vals.append(xp * p + vals[m - 2] * (m - 1)) + xj = IV(x.v.lo ** j, x.v.hi ** j) if j > 0 else IV(1) + return DV(vals[j], -(xj * p) * x.d) + + +def abs_moment_between(j, sigma2, lo, hi): + """E[|X|^j 1{lo < |X| < hi}] for X ~ N(0, sigma2), lo, hi DV in the integration variable (0 <= lo <= hi).""" + sig = isqrt_iv(IV(sigma2)) + sigj = IV(sig.lo ** j, sig.hi ** j) + inv = sig.inv() + a = DV(lo.v * inv, lo.d * inv) + b = DV(hi.v * inv, hi.d * inv) + return (upper_moment(j, a) - upper_moment(j, b)) * DV.const(sigj * 2) + + +def abs_moment_tail(j, sigma2, lo): + """E[|X|^j 1{|X| > lo}] for X ~ N(0, sigma2), lo rational >= 0 (interval).""" + sig = isqrt_iv(IV(sigma2)) + sigj = IV(sig.lo ** j, sig.hi ** j) + return upper_moment(j, DV.const(IV(lo) * sig.inv())).v * sigj * 2 + + +# ----------------------------------------------------------------------------- certified one-dimensional quadrature +def integrate(f, a, b, h, nf=1): + """Enclosures of integral_a^b f_i for f: DV -> (DV, ..., DV) (nf components, rigorous on intervals), by cells of + width h with the mean-value enclosure integral_cell f_i in h f_i(mid) +- (h^2 / 8) width(f_i'(cell)) (pair t and + 2 mid - t: f(t) + f(2 mid - t) - 2 f(mid) = (t - mid)(f'(xi_1) - f'(xi_2)) is bounded by |t - mid| width(f'(cell))).""" + a, b, h = Fr(a), Fr(b), Fr(h) + n = int(math.ceil((b - a) / h)) + tot = [IV(0) for _ in range(nf)] + t0 = a + for i in range(n): + t1 = min(b, a + (i + 1) * h) + w = t1 - t0 + mid = (t0 + t1) / 2 + fm = f(DV.var(IV(mid))) + cell = f(DV.var(IV(t0, t1))) + for j in range(nf): + err = cell[j].d.width() * w * w / 8 + tot[j] = tot[j] + fm[j].v * w + IV(-err, err) + t0 = t1 + return tot + + +# ----------------------------------------------------------------------------- the model +SIG2_V = Fr(1, 2) # v = -f_xxy(0)/2 +SIG2_OM = Fr(2) # om = f_xyy(0) +SIG2_Y = Fr(6) # Y = f_yyy(0) +SIG2_2V = Fr(2) # 2|v| has the law of |N(0, 2)|, as |om| + + +def sig2_y(): + return Fr(2) if MUT == 'variance-yyy' else SIG2_Y + + +def F_abs(t, sigma2): + """P(|N(0, sigma2)| <= t) = 2 Phi(t / sigma) - 1 as DV.""" + inv = isqrt_iv(IV(sigma2)).inv() + return Phi_dv(DV(t.v * inv, t.d * inv)).scale(2) - 1 + + +def F3(t): + if MUT == 'no-third-jet': + return DV.const(1) + return F_abs(t, sig2_y()) + + +def tail_t5(T): + """integral_T^infinity 6 t^5 (1 - F1(t)^2 F3(t)) dt <= sum over the union bound 2(1 - F1) + (1 - F3), each + integral_T^inf 6 t^5 2(1 - Phi(t/sigma)) dt <= 12 (sigma^6 / 6) M_6(T / sigma).""" + tot = IV(0) + for mult, s2 in ((2, SIG2_2V), (1, sig2_y())): + if MUT == 'no-third-jet' and s2 == sig2_y(): + continue + sig = isqrt_iv(IV(s2)) + tot = tot + upper_moment(6, DV.const(IV(T) * sig.inv())).v * IV(sig.lo ** 6, sig.hi ** 6) * (2 * mult) + return IV(0, tot.hi) + + +def tail_t1(T): + """integral_T^infinity 2 t (1 - F1(t) F3(t)) dt <= sum_i integral_T^inf 2 t 2(1 - Phi(t/sigma_i)) dt <= sum_i 2 sigma_i^2 M_2(T/sigma_i).""" + tot = IV(0) + for s2 in (SIG2_2V, sig2_y()): + if MUT == 'no-third-jet' and s2 == sig2_y(): + continue + sig = isqrt_iv(IV(s2)) + tot = tot + upper_moment(2, DV.const(IV(T) * sig.inv())).v * sig.sq() * 2 + return IV(0, tot.hi) + + +def certify_k(k): + """Enclosures of I1, I2, I3 and J(k) at a rational k > 0.""" + k = Fr(k) + m = 12 * k + T = m + T_SPAN + six_k = 6 * k + + def F1(t): + return F_abs(t, SIG2_2V) + + # one pass over t in [m, T] for the three t-integrands + # f1 = 6 t^5 (1 - F1^2 F3) -> I1 = E[M^6] = m^6 + integral_m^inf f1 + # h1 = 2 t (1 - F1 F3) -> H = E[max(m, |om|, |Y|)^2] = m^2 + integral_m^inf h1 + # f2 = h1 E[v^4 1{6k < |v| < t/2}] -> the t-integral in I2 = E[v^4 M^2] + def fv(t): + a1 = F1(t) + a3 = F3(t) + f1 = t.pow(5).scale(6) * (1 - a1.sq() * a3) + h1 = t.scale(2) * (1 - a1 * a3) + B = abs_moment_between(4, SIG2_V, DV.const(six_k), t.scale(Fr(1, 2))) + return (f1, h1, h1 * B) + q1, qh, q2 = integrate(fv, m, T, CELL, 3) + I1 = IV(m ** 6) + q1 + tail_t5(T) + H = IV(m * m) + qh + tail_t1(T) + # I2 = E[v^4 M^2] = H E[v^4 1{|v| <= 6k}] + 4 E[v^6 1{|v| > 6k}] + integral_m^inf 2t (1 - F1 F3) E[v^4 1{6k < |v| < t/2}] dt + Ev4_in = abs_moment_between(4, SIG2_V, DV.const(0), DV.const(six_k)).v + Ev6_out = abs_moment_tail(6, SIG2_V, six_k) + Ev4 = IV(3 * SIG2_V * SIG2_V) # E v^4 = 3 sigma^4 = 3/4 + I2 = H * Ev4_in + Ev6_out * 4 + q2 + tail_t1(T) * Ev4 + + # I3 = E[F(max(a, c))], F(max) = -a^3/6 + a^2 c/2 on {c <= a} (om <= v^2/(3k)), = -c^3/6 + a c^2/2 on {c > a} + sig_om = isqrt_iv(IV(SIG2_OM)) + sig_v = isqrt_iv(IV(SIG2_V)) + inv_sv = sig_v.inv() + + def G(v): + # om-expectations at threshold theta = v^2/(3k): u = theta / sigma_om + theta = v.sq().scale(1 / (3 * k)) + u = DV(theta.v * sig_om.inv(), theta.d * sig_om.inv()) + P = Phi_dv(u) + p = phi_dv(u) + E0le = P + E1le = -(p * DV.const(sig_om)) + E0gt = 1 - P + E1gt = p * DV.const(sig_om) + E2gt = (u * p + 1 - P) * DV.const(sig_om.sq()) + E3gt = (u.sq() * p + p.scale(2)) * DV.const(sig_om.sq() * sig_om) + v2 = v.sq() + v4 = v2.sq() + v6 = v4 * v2 + piece1 = -(v6 * E0le).scale(Fr(2, 3)) + (v4 * E1le).scale(3 * k) + # c = 6k om - v^2: c^2 = 36k^2 om^2 - 12k v^2 om + v^4 ; c^3 = 216k^3 om^3 - 108k^2 v^2 om^2 + 18k v^4 om - v^6 + c2 = E2gt.scale(36 * k * k) - (v2 * E1gt).scale(12 * k) + v4 * E0gt + c3 = E3gt.scale(216 * k ** 3) - (v2 * E2gt).scale(108 * k * k) + (v4 * E1gt).scale(18 * k) - v6 * E0gt + piece2 = ((v2 * c2).scale(3) - c3).scale(Fr(1, 6)) + return piece1 + piece2 + + def f3(v): + rho = phi_dv(DV(v.v * inv_sv, v.d * inv_sv)) * DV.const(inv_sv) + return G(v) * rho + # tail |v| > V: |F(max)| <= (2/3) v^6 + 3k v^4 |om| + [3 v^2 c^2 + |c|^3] / 6 with |c| <= 6k|om| + v^2; expanding + # (6k|om| + v^2)^2 and (6k|om| + v^2)^3 and collecting powers of |v|: + # <= (4/3) v^6 + 12k |om| v^4 + 36k^2 om^2 v^2 + 36k^3 |om|^3 (v^6: 2/3 + 1/2 + 1/6; v^4 |om|: 3k + 6k + 3k; + # v^2 om^2: 18k^2 + 18k^2; |om|^3: 216k^3/6) + # with E|om| <= sqrt2, E om^2 = 2, E|om|^3 <= sqrt(E om^6) = sqrt(120) < 11 + Eom1, Eom2, Eom3 = IV(SQRT2.hi), IV(2), IV(11) + coef = {6: Fr(4, 3), 4: 12 * k * Eom1.hi, 2: 36 * k * k * Eom2.hi, 0: 36 * k ** 3 * Eom3.hi} + tail3 = IV(0) + for j, cj in coef.items(): + tail3 = tail3 + abs_moment_tail(j, SIG2_V, V_MAX) * cj + I3 = integrate(lambda v: (f3(v),), 0, V_MAX, CELL)[0] * 2 + IV(-tail3.hi, tail3.hi) + + sign = 1 if MUT == 'sign-lo' else -1 + J = (I1 * Fr(512, 3) - I2 * 8 + I3 * sign) / (216 * k ** 3) + return {'k': str(k), 'I1': I1, 'I2': I2, 'I3': I3, 'J': J} + + +def R_of_b(b): + """R(b) = [phi(beta) / sqrt(2)] / [(2 + b^2) Phi(beta) + sqrt(2) b phi(beta)], beta = b / sqrt(2).""" + b = Fr(b) + beta = IV(b) / SQRT2 + ph = phi_iv(beta) + P = Phi(beta) + num = ph / SQRT2 + den = P * (2 + b * b) + ph * SQRT2 * b + return num / den + + +# ----------------------------------------------------------------------------- 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 float_I(k, v, om, Y): + a = v * v + c = 6 * k * om - v * v + M = max(12 * k, 2 * abs(v), abs(om), abs(Y)) + top = 8 * M * M + lo = max(a, c) + + def F(s): + return s ** 3 / 3 - (a + c) * s * s / 2 + a * c * s + return (F(top) - F(lo)) / (6 * k) + + +def float_mc(k, n, seed): + rng = random.Random(seed) + s = s2 = 0.0 + for _ in range(n): + v = rng.gauss(0, math.sqrt(0.5)) + om = rng.gauss(0, math.sqrt(2)) + Y = rng.gauss(0, math.sqrt(6)) + x = float_I(k, v, om, Y) / (36 * k * k) + s += x + s2 += x * x + mean = s / n + return mean, math.sqrt(max(s2 / n - mean * mean, 0.0) / n) + + +def float_quad2d(k, n=240, V=7.0, O=11.0): + """Midpoint rule in (v, om) with the Y-expectation in closed form.""" + sig_y = math.sqrt(6) + tot = 0.0 + sv, so = math.sqrt(0.5), math.sqrt(2) + for i in range(n): + v = -V + (i + 0.5) * (2 * V / n) + wv = _phi_f(v / sv) / sv * (2 * V / n) + for j in range(n): + om = -O + (j + 0.5) * (2 * O / n) + wo = _phi_f(om / so) / so * (2 * O / n) + a = v * v + c = 6 * k * om - a + lo = max(a, c) + m0 = max(12 * k, 2 * abs(v), abs(om)) + coeffs = [-(lo ** 3 / 3 - (a + c) * lo * lo / 2 + a * c * lo), 8 * a * c, -(a + c) * 32, 512 / 3] + t = m0 / sig_y + A = [1 - _Phi_f(t)] + for jj in range(1, 4): + A.append(t ** (2 * jj - 1) * _phi_f(t) + (2 * jj - 1) * A[jj - 1]) + P_in = 2 * _Phi_f(t) - 1 + ey = sum(cj * (m0 ** (2 * jj) * P_in + 2 * sig_y ** (2 * jj) * A[jj]) for jj, cj in enumerate(coeffs)) + tot += wv * wo * ey / (6 * k) + return tot / (36 * k * k) + + +def float_R(b): + be = b / math.sqrt(2) + return (_phi_f(be) / math.sqrt(2)) / ((2 + b * b) * _Phi_f(be) + math.sqrt(2) * b * _phi_f(be)) + + +# ----------------------------------------------------------------------------- records +def dec_down(x, digits=10): + x = Fr(x) + n = x.numerator * 10 ** digits // x.denominator + s_ = str(abs(n)).rjust(digits + 1, '0') + return ('-' if n < 0 else '') + s_[:-digits] + '.' + s_[-digits:] + + +def dec_up(x, digits=10): + x = Fr(x) + n = -((-x.numerator * 10 ** digits) // x.denominator) + s_ = str(abs(n)).rjust(digits + 1, '0') + return ('-' if n < 0 else '') + s_[:-digits] + '.' + s_[-digits:] + + +def enclosure(iv, digits=10): + return [dec_down(iv.lo, digits), dec_up(iv.hi, digits)] + + +def k_record(k): + rec = certify_k(k) + lead = LEAD * Fr(k) ** 3 + out = {'k': str(Fr(k)), 'J': enclosure(rec['J']), 'J_width': dec_up(rec['J'].width(), 12), + 'I1_E_M6': enclosure(rec['I1']), 'I2_E_v4M2': enclosure(rec['I2']), 'I3_E_F_lo': enclosure(rec['I3']), + 'lead_2359296_k3': str(lead), 'J_over_lead': enclosure(rec['J'] / lead, 8)} + return out, rec + + +def controls_k(k): + kf = float(Fr(k)) + mc, se = float_mc(kf, 200000, 2026) + q = float_quad2d(kf) + return {'k': str(Fr(k)), 'J_mc': mc, 'J_mc_se': se, 'J_quad2d': q} + + +def worker(k): + out, rec = k_record(k) + return out + + +def full_run(procs): + with multiprocessing.Pool(procs) as pool: + recs = pool.map(worker, list(K_GRID)) + ctrls = pool.map(controls_k, list(K_GRID)) + Rs = {str(b): enclosure(R_of_b(b), 12) for b in B_GRID} + cg = {} + for b in B_GRID: + for rec in recs: + J = IV(Fr(rec['J'][0]), Fr(rec['J'][1])) + cg['b=%s,k=%s' % (b, rec['k'])] = enclosure(R_of_b(b) * J, 4) + res = { + 'schema': 1, + 'object': 'CL-C8-CAP-FAILURE-COEFFICIENT-PLANAR-20260930-v1', + 'scientific_effect': 'NONE', + 'certified': True, + 'kind': 'certified enclosures of the limit coefficient c_G(b, k) = R(b) J(k) of Theorem G (NOTE.md); the limit theorem itself is author-side', + 'statement': 'Q^W(G_r^c) = c_G(b, k) r^3 + o(r^3) as r -> 0 for the planar six-pin law of [LP] with the good event G_r of [LP] section 7 / [CAP] (1); reference-kernel jet law', + 'parameters': {'PBITS': PBITS, 'CELL': str(CELL), 'T_SPAN': str(T_SPAN), 'V_MAX': str(V_MAX), 'LEAD': LEAD, + 'k_grid': [str(k) for k in K_GRID], 'b_grid': [str(b) for b in B_GRID]}, + 'J': recs, + 'R': Rs, + 'c_G': cg, + 'float_controls': ctrls, + 'mutant': MUT, + } + return res + + +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) + + +def check_run(procs): + ref = load_results() + require(ref['parameters'] == {'PBITS': PBITS, 'CELL': str(CELL), 'T_SPAN': str(T_SPAN), 'V_MAX': str(V_MAX), 'LEAD': LEAD, + 'k_grid': [str(k) for k in K_GRID], 'b_grid': [str(b) for b in B_GRID]}, 'parameters differ from RESULTS.json') + require(ref['mutant'] is None, 'RESULTS.json was produced under a mutant') + # constants + require(abs(PI.mid() - Fr('3.14159265358979323846')) < Fr(1, 10 ** 19) and PI.width() < Fr(1, 10 ** 30), 'pi enclosure') + require(abs(Phi(IV(1)).mid() - Fr('0.841344746068542948585')) < Fr(1, 10 ** 19) and Phi(IV(1)).width() < Fr(1, 10 ** 30), 'Phi(1) enclosure') + require(abs(exp_neg(IV(1)).mid() - Fr('0.367879441171442321595')) < Fr(1, 10 ** 19) and exp_neg(IV(1)).width() < Fr(1, 10 ** 30), 'exp(-1) enclosure') + # the six certified values, recomputed and compared exactly with the stored decimal strings + stored = {rec['k']: rec for rec in ref['J']} + recs = {} + + def take(k, out): + require(out == stored[str(k)], 'certified record for k = %s differs from RESULTS.json' % k) + J = IV(Fr(out['J'][0]), Fr(out['J'][1])) + lead = LEAD * Fr(k) ** 3 + # J(k) = LEAD k^3 (1 + delta(k)): delta positive and large for small k (the free third derivatives exceed 12k), + # within 2e-6 of zero for k >= 1 (both signs occur: the -8 E[v^4 M^2] term is negative) + if Fr(k) <= Fr(3, 4): + require(J.lo >= lead, 'J(k) below %s k^3 at k = %s' % (LEAD, k)) + else: + require(abs(J.mid() / lead - 1) < Fr(2, 10 ** 6), 'J(k) not within 2e-6 of %s k^3 at k = %s' % (LEAD, k)) + require(J.width() / J.lo < Fr(1, 10 ** 5), 'J(k) enclosure wider than 1e-5 relative at k = %s' % k) + ctrl = [c for c in ref['float_controls'] if c['k'] == str(k)][0] + Jf = float(J.mid()) + require(abs(ctrl['J_mc'] - Jf) <= 4 * ctrl['J_mc_se'] + 1e-9 * Jf, 'Monte Carlo control off by more than four standard errors at k = %s' % k) + require(abs(ctrl['J_quad2d'] / Jf - 1) < 3e-4, 'two-dimensional quadrature control off by more than 3e-4 at k = %s' % k) + recs[str(k)] = out + take(K_GRID[0], worker(K_GRID[0])) # first value sequentially: a mutant fails here + with multiprocessing.Pool(procs) as pool: + for k, out in zip(K_GRID[1:], pool.map(worker, list(K_GRID[1:]))): + take(k, out) + for b in B_GRID: + Rb = R_of_b(b) + require(enclosure(Rb, 12) == ref['R'][str(b)], 'R(b) differs at b = %s' % b) + require(abs(float_R(float(b)) - float(Rb.mid())) < 1e-12, 'R(b) float control at b = %s' % b) + for k in K_GRID: + J = IV(Fr(stored[str(k)]['J'][0]), Fr(stored[str(k)]['J'][1])) + require(enclosure(Rb * J, 4) == ref['c_G']['b=%s,k=%s' % (b, k)], 'c_G differs at (%s, %s)' % (b, k)) + # monotonicity of R on the grid and the two headline numbers + Rvals = [Fr(ref['R'][str(b)][0]) for b in B_GRID] + require(all(Fr(ref['R'][str(B_GRID[i])][0]) > Fr(ref['R'][str(B_GRID[i + 1])][1]) for i in range(len(B_GRID) - 1)), 'R not decreasing on the grid (disjoint enclosures required)') + require(Fr(ref['c_G']['b=0,k=2'][0]) > 5300000, 'c_G(0, 2) headline') + require(Fr(ref['c_G']['b=6/5,k=1/6'][0]) > 35000, 'c_G(6/5, 1/6) headline') + # [CAP] (3): C3_new + C4_new / 20 < 2.4e23, exact; and the recorded constant is at least 6e18 times c_G(6/5, 1/6) + C3 = Fr(10, 51) * (Fr(32 ** 3, 3) * 320 ** 8 + Fr(3 * 32 ** 2, 2) * 320 ** 7) + C4 = Fr(23, 5) * (10240 ** 4 + 6800 ** 4) + require(C3 + C4 / 20 < Fr(24, 10) * 10 ** 23, '[CAP] (3) arithmetic') + require(C3 / Fr(ref['c_G']['b=6/5,k=1/6'][1]) > 6 * 10 ** 18, 'ratio of the recorded constant to c_G(6/5, 1/6)') + print(json.dumps({'check': 'ok', 'k_values': len(K_GRID), 'c_G(0,2)': ref['c_G']['b=0,k=2'], 'c_G(6/5,1/6)': ref['c_G']['b=6/5,k=1/6'], 'mutant': MUT})) + + +def main(): + global MUT + ap = argparse.ArgumentParser() + ap.add_argument('--check', action='store_true') + ap.add_argument('--mutant', choices=MUTANTS) + ap.add_argument('--procs', type=int, default=4) + ap.add_argument('--quick', type=str, default=None, help='certify one k (rational) and print the record') + args = ap.parse_args() + MUT = args.mutant + if args.quick: + import time + t0 = time.time() + out, rec = k_record(Fr(args.quick)) + print(json.dumps(out), 'time', round(time.time() - t0, 1)) + print('mc', float_mc(float(Fr(args.quick)), 100000, 1), 'quad2d', float_quad2d(float(Fr(args.quick)), 160)) + return + if args.check: + check_run(args.procs) + return + res = full_run(args.procs) + write_results(res) + print(json.dumps({r['k']: r['J'] for r in res['J']})) + + +if __name__ == '__main__': + main()